:: EUCLID_2 semantic presentation begin theorem :: EUCLID_2:1 (Bool "for" (Set (Var "n")) "," (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) "holds" (Bool (Set (Set "(" ($#k14_rvsum_1 :::"mlt"::: ) "(" (Set (Var "v")) "," (Set "(" ($#k5_euclid :::"0*"::: ) (Set (Var "n")) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: EUCLID_2:2 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) "holds" (Bool (Set ($#k14_rvsum_1 :::"mlt"::: ) "(" (Set (Var "v")) "," (Set "(" ($#k5_euclid :::"0*"::: ) (Set (Var "n")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_euclid :::"0*"::: ) (Set (Var "n")))))) ; begin theorem :: EUCLID_2:3 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Var "y1"))) & (Bool (Set (Var "x2")) ($#r1_hidden :::"="::: ) (Set (Var "y2")))) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 1) ($#k18_binop_2 :::"/"::: ) (Num 4) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "x1")) ($#k7_euclid :::"+"::: ) (Set (Var "x2")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "x1")) ($#k8_euclid :::"-"::: ) (Set (Var "x2")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" )))))) ; theorem :: EUCLID_2:4 (Bool "for" (Set (Var "x")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set (Set ($#k12_euclid :::"|."::: ) (Set (Var "x")) ($#k12_euclid :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x")) "," (Set (Var "x")) ($#k23_rvsum_1 :::")|"::: ) ))) ; theorem :: EUCLID_2:5 (Bool "for" (Set (Var "x")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k12_euclid :::"|."::: ) (Set (Var "x")) ($#k12_euclid :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k7_square_1 :::"sqrt"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x")) "," (Set (Var "x")) ($#k23_rvsum_1 :::")|"::: ) )))) ; theorem :: EUCLID_2:6 (Bool "for" (Set (Var "x")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k12_euclid :::"|."::: ) (Set (Var "x")) ($#k12_euclid :::".|"::: ) ))) ; theorem :: EUCLID_2:7 (Bool "for" (Set (Var "x")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x")) "," (Set (Var "x")) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "iff" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k5_euclid :::"0*"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "x")) ")" ))) ")" )) ; theorem :: EUCLID_2:8 (Bool "for" (Set (Var "x")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x")) "," (Set (Var "x")) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "iff" (Bool (Set ($#k12_euclid :::"|."::: ) (Set (Var "x")) ($#k12_euclid :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ; theorem :: EUCLID_2:9 (Bool "for" (Set (Var "x")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x")) "," (Set "(" ($#k5_euclid :::"0*"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "x")) ")" ) ")" ) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: EUCLID_2:10 (Bool "for" (Set (Var "x")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" ($#k5_euclid :::"0*"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "x")) ")" ) ")" ) "," (Set (Var "x")) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: EUCLID_2:11 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y"))))) "holds" (Bool (Set (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "x")) ($#k4_rvsum_1 :::"+"::: ) (Set (Var "y")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k12_euclid :::"|."::: ) (Set (Var "x")) ($#k12_euclid :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "y")) "," (Set (Var "x")) ($#k23_rvsum_1 :::")|"::: ) ) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set ($#k12_euclid :::"|."::: ) (Set (Var "y")) ($#k12_euclid :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" )))) ; theorem :: EUCLID_2:12 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y"))))) "holds" (Bool (Set (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "x")) ($#k8_rvsum_1 :::"-"::: ) (Set (Var "y")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k12_euclid :::"|."::: ) (Set (Var "x")) ($#k12_euclid :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "y")) "," (Set (Var "x")) ($#k23_rvsum_1 :::")|"::: ) ) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set ($#k12_euclid :::"|."::: ) (Set (Var "y")) ($#k12_euclid :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" )))) ; theorem :: EUCLID_2:13 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y"))))) "holds" (Bool (Set (Set "(" (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "x")) ($#k4_rvsum_1 :::"+"::: ) (Set (Var "y")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "x")) ($#k8_rvsum_1 :::"-"::: ) (Set (Var "y")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" (Set ($#k12_euclid :::"|."::: ) (Set (Var "x")) ($#k12_euclid :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set ($#k12_euclid :::"|."::: ) (Set (Var "y")) ($#k12_euclid :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" )))) ; theorem :: EUCLID_2:14 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y"))))) "holds" (Bool (Set (Set "(" (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "x")) ($#k4_rvsum_1 :::"+"::: ) (Set (Var "y")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "x")) ($#k8_rvsum_1 :::"-"::: ) (Set (Var "y")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Num 4) ($#k11_binop_2 :::"*"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k23_rvsum_1 :::")|"::: ) )))) ; theorem :: EUCLID_2:15 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y"))))) "holds" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k23_rvsum_1 :::")|"::: ) )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set ($#k12_euclid :::"|."::: ) (Set (Var "x")) ($#k12_euclid :::".|"::: ) ) ($#k11_binop_2 :::"*"::: ) (Set ($#k12_euclid :::"|."::: ) (Set (Var "y")) ($#k12_euclid :::".|"::: ) )))) ; theorem :: EUCLID_2:16 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y"))))) "holds" (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "x")) ($#k4_rvsum_1 :::"+"::: ) (Set (Var "y")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set ($#k12_euclid :::"|."::: ) (Set (Var "x")) ($#k12_euclid :::".|"::: ) ) ($#k9_binop_2 :::"+"::: ) (Set ($#k12_euclid :::"|."::: ) (Set (Var "y")) ($#k12_euclid :::".|"::: ) )))) ; begin theorem :: EUCLID_2:17 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p1")) "," (Set (Var "p2")) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 1) ($#k18_binop_2 :::"/"::: ) (Num 4) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "p2")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p2")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ))))) ; theorem :: EUCLID_2:18 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" (Set (Var "p1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "p2")) ")" ) "," (Set (Var "p3")) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p1")) "," (Set (Var "p3")) ($#k23_rvsum_1 :::")|"::: ) ) ($#k9_binop_2 :::"+"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p2")) "," (Set (Var "p3")) ($#k23_rvsum_1 :::")|"::: ) ))))) ; theorem :: EUCLID_2:19 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" (Set (Var "x")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p1")) ")" ) "," (Set (Var "p2")) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k11_binop_2 :::"*"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p1")) "," (Set (Var "p2")) ($#k23_rvsum_1 :::")|"::: ) )))))) ; theorem :: EUCLID_2:20 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p1")) "," (Set "(" (Set (Var "x")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p2")) ")" ) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k11_binop_2 :::"*"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p1")) "," (Set (Var "p2")) ($#k23_rvsum_1 :::")|"::: ) )))))) ; theorem :: EUCLID_2:21 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "p1")) ")" ) "," (Set (Var "p2")) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k7_binop_2 :::"-"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p1")) "," (Set (Var "p2")) ($#k23_rvsum_1 :::")|"::: ) ))))) ; theorem :: EUCLID_2:22 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p1")) "," (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "p2")) ")" ) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k7_binop_2 :::"-"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p1")) "," (Set (Var "p2")) ($#k23_rvsum_1 :::")|"::: ) ))))) ; theorem :: EUCLID_2:23 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "p1")) ")" ) "," (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "p2")) ")" ) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p1")) "," (Set (Var "p2")) ($#k23_rvsum_1 :::")|"::: ) )))) ; theorem :: EUCLID_2:24 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" (Set (Var "p1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p2")) ")" ) "," (Set (Var "p3")) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p1")) "," (Set (Var "p3")) ($#k23_rvsum_1 :::")|"::: ) ) ($#k10_binop_2 :::"-"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p2")) "," (Set (Var "p3")) ($#k23_rvsum_1 :::")|"::: ) ))))) ; theorem :: EUCLID_2:25 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p1")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p2")) ")" ) ")" ) "," (Set (Var "p3")) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k11_binop_2 :::"*"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p1")) "," (Set (Var "p3")) ($#k23_rvsum_1 :::")|"::: ) ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k11_binop_2 :::"*"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p2")) "," (Set (Var "p3")) ($#k23_rvsum_1 :::")|"::: ) ) ")" )))))) ; theorem :: EUCLID_2:26 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q1")) "," (Set (Var "q2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p")) "," (Set "(" (Set (Var "q1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "q2")) ")" ) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p")) "," (Set (Var "q1")) ($#k23_rvsum_1 :::")|"::: ) ) ($#k9_binop_2 :::"+"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p")) "," (Set (Var "q2")) ($#k23_rvsum_1 :::")|"::: ) ))))) ; theorem :: EUCLID_2:27 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q1")) "," (Set (Var "q2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p")) "," (Set "(" (Set (Var "q1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "q2")) ")" ) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p")) "," (Set (Var "q1")) ($#k23_rvsum_1 :::")|"::: ) ) ($#k10_binop_2 :::"-"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p")) "," (Set (Var "q2")) ($#k23_rvsum_1 :::")|"::: ) ))))) ; theorem :: EUCLID_2:28 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q1")) "," (Set (Var "q2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" (Set (Var "p1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "p2")) ")" ) "," (Set "(" (Set (Var "q1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "q2")) ")" ) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p1")) "," (Set (Var "q1")) ($#k23_rvsum_1 :::")|"::: ) ) ($#k9_binop_2 :::"+"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p1")) "," (Set (Var "q2")) ($#k23_rvsum_1 :::")|"::: ) ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p2")) "," (Set (Var "q1")) ($#k23_rvsum_1 :::")|"::: ) ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p2")) "," (Set (Var "q2")) ($#k23_rvsum_1 :::")|"::: ) ))))) ; theorem :: EUCLID_2:29 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q1")) "," (Set (Var "q2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" (Set (Var "p1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p2")) ")" ) "," (Set "(" (Set (Var "q1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "q2")) ")" ) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p1")) "," (Set (Var "q1")) ($#k23_rvsum_1 :::")|"::: ) ) ($#k10_binop_2 :::"-"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p1")) "," (Set (Var "q2")) ($#k23_rvsum_1 :::")|"::: ) ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p2")) "," (Set (Var "q1")) ($#k23_rvsum_1 :::")|"::: ) ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p2")) "," (Set (Var "q2")) ($#k23_rvsum_1 :::")|"::: ) ))))) ; theorem :: EUCLID_2:30 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" (Set (Var "p")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "q")) ")" ) "," (Set "(" (Set (Var "p")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "q")) ")" ) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p")) "," (Set (Var "p")) ($#k23_rvsum_1 :::")|"::: ) ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k23_rvsum_1 :::")|"::: ) ) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "q")) "," (Set (Var "q")) ($#k23_rvsum_1 :::")|"::: ) ))))) ; theorem :: EUCLID_2:31 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" (Set (Var "p")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "q")) ")" ) "," (Set "(" (Set (Var "p")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "q")) ")" ) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p")) "," (Set (Var "p")) ($#k23_rvsum_1 :::")|"::: ) ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k23_rvsum_1 :::")|"::: ) ) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "q")) "," (Set (Var "q")) ($#k23_rvsum_1 :::")|"::: ) ))))) ; theorem :: EUCLID_2:32 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p")) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) ")" ) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: EUCLID_2:33 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) ")" ) "," (Set (Var "p")) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: EUCLID_2:34 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) ")" ) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) ")" ) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: EUCLID_2:35 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p")) "," (Set (Var "p")) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: EUCLID_2:36 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p")) "," (Set (Var "p")) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) )))) ; theorem :: EUCLID_2:37 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k7_square_1 :::"sqrt"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p")) "," (Set (Var "p")) ($#k23_rvsum_1 :::")|"::: ) ))))) ; theorem :: EUCLID_2:38 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) )))) ; theorem :: EUCLID_2:39 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: EUCLID_2:40 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool "(" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p")) "," (Set (Var "p")) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "iff" (Bool (Set ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))) ; theorem :: EUCLID_2:41 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool "(" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p")) "," (Set (Var "p")) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "iff" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ))) ")" ))) ; theorem :: EUCLID_2:42 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool "(" (Bool (Set ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "iff" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ))) ")" ))) ; theorem :: EUCLID_2:43 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ))) "iff" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p")) "," (Set (Var "p")) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))) ; theorem :: EUCLID_2:44 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ))) "iff" (Bool (Set ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) ) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))) ; theorem :: EUCLID_2:45 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "q")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "q")) "," (Set (Var "p")) ($#k23_rvsum_1 :::")|"::: ) ) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set ($#k12_euclid :::"|."::: ) (Set (Var "q")) ($#k12_euclid :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ))))) ; theorem :: EUCLID_2:46 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "q")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "q")) "," (Set (Var "p")) ($#k23_rvsum_1 :::")|"::: ) ) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set ($#k12_euclid :::"|."::: ) (Set (Var "q")) ($#k12_euclid :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ))))) ; theorem :: EUCLID_2:47 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set (Set "(" (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "q")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "q")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" (Set ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set ($#k12_euclid :::"|."::: ) (Set (Var "q")) ($#k12_euclid :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ))))) ; theorem :: EUCLID_2:48 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set (Set "(" (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "q")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "q")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Num 4) ($#k11_binop_2 :::"*"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k23_rvsum_1 :::")|"::: ) ))))) ; theorem :: EUCLID_2:49 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 1) ($#k18_binop_2 :::"/"::: ) (Num 4) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "q")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "q")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ))))) ; theorem :: EUCLID_2:50 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p")) "," (Set (Var "p")) ($#k23_rvsum_1 :::")|"::: ) ) ($#k9_binop_2 :::"+"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "q")) "," (Set (Var "q")) ($#k23_rvsum_1 :::")|"::: ) ))))) ; theorem :: EUCLID_2:51 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k23_rvsum_1 :::")|"::: ) )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) ) ($#k11_binop_2 :::"*"::: ) (Set ($#k12_euclid :::"|."::: ) (Set (Var "q")) ($#k12_euclid :::".|"::: ) ))))) ; theorem :: EUCLID_2:52 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "q")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) ) ($#k9_binop_2 :::"+"::: ) (Set ($#k12_euclid :::"|."::: ) (Set (Var "q")) ($#k12_euclid :::".|"::: ) ))))) ; theorem :: EUCLID_2:53 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set (Var "p")) "," (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" )) ($#r1_rvsum_1 :::"are_orthogonal"::: ) ))) ; theorem :: EUCLID_2:54 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" )) "," (Set (Var "p")) ($#r1_rvsum_1 :::"are_orthogonal"::: ) ))) ; theorem :: EUCLID_2:55 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool "(" (Bool (Set (Var "p")) "," (Set (Var "p")) ($#r1_rvsum_1 :::"are_orthogonal"::: ) ) "iff" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ))) ")" ))) ; theorem :: EUCLID_2:56 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r1_rvsum_1 :::"are_orthogonal"::: ) )) "holds" (Bool (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p"))) "," (Set (Var "q")) ($#r1_rvsum_1 :::"are_orthogonal"::: ) )))) ; theorem :: EUCLID_2:57 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r1_rvsum_1 :::"are_orthogonal"::: ) )) "holds" (Bool (Set (Var "p")) "," (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "q"))) ($#r1_rvsum_1 :::"are_orthogonal"::: ) )))) ; theorem :: EUCLID_2:58 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool "(" "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r1_rvsum_1 :::"are_orthogonal"::: ) ) ")" )) "holds" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ))))) ;