:: EUCLID semantic presentation begin definitionlet "n" be ($#m1_hidden :::"Nat":::); func :::"REAL"::: "n" -> ($#m1_finseq_2 :::"FinSequenceSet"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) equals :: EUCLID:def 1 (Set "n" ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )); end; :: deftheorem defines :::"REAL"::: EUCLID:def 1 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )))); registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k1_euclid :::"REAL"::: ) "n") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster -> "n" ($#v3_card_1 :::"-element"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) "n"); end; definitionfunc :::"absreal"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: EUCLID:def 2 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set ($#k18_complex1 :::"abs"::: ) (Set (Var "r"))))); end; :: deftheorem defines :::"absreal"::: EUCLID:def 2 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k2_euclid :::"absreal"::: ) )) "iff" (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_seq_1 :::"."::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set ($#k18_complex1 :::"abs"::: ) (Set (Var "r"))))) ")" )); definitionlet "x" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::); :: original: :::"|."::: redefine func :::"abs"::: "x" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) equals :: EUCLID:def 3 (Set (Set ($#k2_euclid :::"absreal"::: ) ) ($#k3_relat_1 :::"*"::: ) "x"); end; :: deftheorem defines :::"abs"::: EUCLID:def 3 : (Bool "for" (Set (Var "x")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k3_euclid :::"abs"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_euclid :::"absreal"::: ) ) ($#k3_relat_1 :::"*"::: ) (Set (Var "x"))))); definitionlet "n" be ($#m1_hidden :::"Nat":::); func :::"0*"::: "n" -> ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) equals :: EUCLID:def 4 (Set "n" ($#k5_finseq_2 :::"|->"::: ) (Set ($#k6_numbers :::"0"::: ) )); end; :: deftheorem defines :::"0*"::: EUCLID:def 4 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k4_euclid :::"0*"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k5_finseq_2 :::"|->"::: ) (Set ($#k6_numbers :::"0"::: ) )))); definitionlet "n" be ($#m1_hidden :::"Nat":::); :: original: :::"0*"::: redefine func :::"0*"::: "n" -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) "n"); end; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "x" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Const "n"))); :: original: :::"-"::: redefine func :::"-"::: "x" -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) "n"); end; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "x", "y" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Const "n"))); :: original: :::"+"::: redefine func "x" :::"+"::: "y" -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) "n"); :: original: :::"-"::: redefine func "x" :::"-"::: "y" -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) "n"); end; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "x" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Const "n"))); let "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"(#)"::: redefine func "r" :::"*"::: "x" -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) "n"); end; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "x" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Const "n"))); :: original: :::"|."::: redefine func :::"abs"::: "x" -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set "n" ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )); end; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "x" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Const "n"))); :: original: :::"^2"::: redefine func :::"sqr"::: "x" -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set "n" ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )); end; definitionlet "f" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::); func :::"|.":::"f":::".|"::: -> ($#m1_subset_1 :::"Real":::) equals :: EUCLID:def 5 (Set ($#k7_square_1 :::"sqrt"::: ) (Set "(" ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k12_rvsum_1 :::"sqr"::: ) "f" ")" ) ")" )); end; :: deftheorem defines :::"|."::: EUCLID:def 5 : (Bool "for" (Set (Var "f")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k12_euclid :::"|."::: ) (Set (Var "f")) ($#k12_euclid :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k7_square_1 :::"sqrt"::: ) (Set "(" ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k12_rvsum_1 :::"sqr"::: ) (Set (Var "f")) ")" ) ")" )))); theorem :: EUCLID:1 canceled; theorem :: EUCLID:2 canceled; theorem :: EUCLID:3 canceled; theorem :: EUCLID:4 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k10_euclid :::"abs"::: ) (Set "(" ($#k5_euclid :::"0*"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k5_finseq_2 :::"|->"::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: EUCLID:5 (Bool "for" (Set (Var "f")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k54_valued_1 :::"abs"::: ) (Set "(" ($#k30_valued_1 :::"-"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k54_valued_1 :::"abs"::: ) (Set (Var "f"))))) ; theorem :: EUCLID:6 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "f")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k3_euclid :::"abs"::: ) (Set "(" (Set (Var "r")) ($#k10_rvsum_1 :::"*"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k18_complex1 :::"abs"::: ) (Set (Var "r")) ")" ) ($#k10_rvsum_1 :::"*"::: ) (Set "(" ($#k3_euclid :::"abs"::: ) (Set (Var "f")) ")" ))))) ; theorem :: EUCLID:7 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" ($#k5_euclid :::"0*"::: ) (Set (Var "n")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: EUCLID:8 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set ($#k12_euclid :::"|."::: ) (Set (Var "x")) ($#k12_euclid :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k5_euclid :::"0*"::: ) (Set (Var "n")))))) ; theorem :: EUCLID:9 (Bool "for" (Set (Var "f")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k12_euclid :::"|."::: ) (Set (Var "f")) ($#k12_euclid :::".|"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; registrationlet "f" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::); cluster (Set ($#k12_euclid :::"|."::: ) "f" ($#k12_euclid :::".|"::: ) ) -> ($#~v3_xxreal_0 "non" ($#v3_xxreal_0 :::"negative"::: ) ) ; end; theorem :: EUCLID:10 (Bool "for" (Set (Var "f")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" ($#k6_rvsum_1 :::"-"::: ) (Set (Var "f")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k12_euclid :::"|."::: ) (Set (Var "f")) ($#k12_euclid :::".|"::: ) ))) ; theorem :: EUCLID:11 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "f")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "r")) ($#k10_rvsum_1 :::"*"::: ) (Set (Var "f")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k18_complex1 :::"abs"::: ) (Set (Var "r")) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k12_euclid :::"|."::: ) (Set (Var "f")) ($#k12_euclid :::".|"::: ) ))))) ; theorem :: EUCLID:12 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "x1")) ($#k7_euclid :::"+"::: ) (Set (Var "x2")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set ($#k12_euclid :::"|."::: ) (Set (Var "x1")) ($#k12_euclid :::".|"::: ) ) ($#k7_real_1 :::"+"::: ) (Set ($#k12_euclid :::"|."::: ) (Set (Var "x2")) ($#k12_euclid :::".|"::: ) ))))) ; theorem :: EUCLID:13 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "x1")) ($#k8_euclid :::"-"::: ) (Set (Var "x2")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set ($#k12_euclid :::"|."::: ) (Set (Var "x1")) ($#k12_euclid :::".|"::: ) ) ($#k7_real_1 :::"+"::: ) (Set ($#k12_euclid :::"|."::: ) (Set (Var "x2")) ($#k12_euclid :::".|"::: ) ))))) ; theorem :: EUCLID:14 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set ($#k12_euclid :::"|."::: ) (Set (Var "x1")) ($#k12_euclid :::".|"::: ) ) ($#k9_real_1 :::"-"::: ) (Set ($#k12_euclid :::"|."::: ) (Set (Var "x2")) ($#k12_euclid :::".|"::: ) )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "x1")) ($#k7_euclid :::"+"::: ) (Set (Var "x2")) ")" ) ($#k12_euclid :::".|"::: ) )))) ; theorem :: EUCLID:15 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set ($#k12_euclid :::"|."::: ) (Set (Var "x1")) ($#k12_euclid :::".|"::: ) ) ($#k9_real_1 :::"-"::: ) (Set ($#k12_euclid :::"|."::: ) (Set (Var "x2")) ($#k12_euclid :::".|"::: ) )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "x1")) ($#k8_euclid :::"-"::: ) (Set (Var "x2")) ")" ) ($#k12_euclid :::".|"::: ) )))) ; theorem :: EUCLID:16 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool "(" (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "x1")) ($#k8_euclid :::"-"::: ) (Set (Var "x2")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "iff" (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Var "x2"))) ")" ))) ; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "x1" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Const "n"))); cluster (Set ($#k12_euclid :::"|."::: ) (Set "(" "x1" ($#k8_euclid :::"-"::: ) "x1" ")" ) ($#k12_euclid :::".|"::: ) ) -> ($#v1_xboole_0 :::"zero"::: ) ; end; theorem :: EUCLID:17 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (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 "x2")))) "holds" (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "x1")) ($#k8_euclid :::"-"::: ) (Set (Var "x2")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: EUCLID:18 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "x1")) ($#k8_euclid :::"-"::: ) (Set (Var "x2")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "x2")) ($#k8_euclid :::"-"::: ) (Set (Var "x1")) ")" ) ($#k12_euclid :::".|"::: ) )))) ; theorem :: EUCLID:19 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "x1")) ($#k8_euclid :::"-"::: ) (Set (Var "x2")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "x1")) ($#k8_euclid :::"-"::: ) (Set (Var "x")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#k7_real_1 :::"+"::: ) (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "x")) ($#k8_euclid :::"-"::: ) (Set (Var "x2")) ")" ) ($#k12_euclid :::".|"::: ) ))))) ; definitionlet "n" be ($#m1_hidden :::"Nat":::); func :::"Pitag_dist"::: "n" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k1_euclid :::"REAL"::: ) "n" ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) "n" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: EUCLID:def 6 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) "n") "holds" (Bool (Set it ($#k2_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "x")) ($#k8_euclid :::"-"::: ) (Set (Var "y")) ")" ) ($#k12_euclid :::".|"::: ) ))); end; :: deftheorem defines :::"Pitag_dist"::: EUCLID:def 6 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k13_euclid :::"Pitag_dist"::: ) (Set (Var "n")))) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set (Var "b2")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "x")) ($#k8_euclid :::"-"::: ) (Set (Var "y")) ")" ) ($#k12_euclid :::".|"::: ) ))) ")" ))); theorem :: EUCLID:20 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k12_rvsum_1 :::"sqr"::: ) (Set "(" (Set (Var "x")) ($#k8_rvsum_1 :::"-"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k12_rvsum_1 :::"sqr"::: ) (Set "(" (Set (Var "y")) ($#k8_rvsum_1 :::"-"::: ) (Set (Var "x")) ")" )))) ; theorem :: EUCLID:21 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k13_euclid :::"Pitag_dist"::: ) (Set (Var "n"))) ($#r1_pcomps_1 :::"is_metric_of"::: ) (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))))) ; definitionlet "n" be ($#m1_hidden :::"Nat":::); func :::"Euclid"::: "n" -> ($#v1_metric_1 :::"strict"::: ) ($#l1_metric_1 :::"MetrSpace":::) equals :: EUCLID:def 7 (Set ($#g1_metric_1 :::"MetrStruct"::: ) "(#" (Set "(" ($#k1_euclid :::"REAL"::: ) "n" ")" ) "," (Set "(" ($#k13_euclid :::"Pitag_dist"::: ) "n" ")" ) "#)" ); end; :: deftheorem defines :::"Euclid"::: EUCLID:def 7 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k14_euclid :::"Euclid"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#g1_metric_1 :::"MetrStruct"::: ) "(#" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k13_euclid :::"Pitag_dist"::: ) (Set (Var "n")) ")" ) "#)" ))); registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k14_euclid :::"Euclid"::: ) "n") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_metric_1 :::"strict"::: ) ; end; definitionlet "n" be ($#m1_hidden :::"Nat":::); func :::"TOP-REAL"::: "n" -> ($#v5_rltopsp1 :::"strict"::: ) ($#l1_rltopsp1 :::"RLTopStruct"::: ) means :: EUCLID:def 8 (Bool "(" (Bool (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" it) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set "(" ($#k14_euclid :::"Euclid"::: ) "n" ")" ))) & (Bool (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" it) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" it) "," (Set "the" ($#u1_rlvect_1 :::"Mult"::: ) "of" it) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#k10_funcsdom :::"RealVectSpace"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) "n" ")" ))) ")" ); end; :: deftheorem defines :::"TOP-REAL"::: EUCLID:def 8 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b2")) "being" ($#v5_rltopsp1 :::"strict"::: ) ($#l1_rltopsp1 :::"RLTopStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")))) "iff" (Bool "(" (Bool (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "b2"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ))) & (Bool (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))) "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set (Var "b2"))) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "b2"))) "," (Set "the" ($#u1_rlvect_1 :::"Mult"::: ) "of" (Set (Var "b2"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#k10_funcsdom :::"RealVectSpace"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ))) ")" ) ")" ))); registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k15_euclid :::"TOP-REAL"::: ) "n") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_rltopsp1 :::"strict"::: ) ; end; registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k15_euclid :::"TOP-REAL"::: ) "n") -> ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v5_rlvect_1 :::"vector-distributive"::: ) ($#v6_rlvect_1 :::"scalar-distributive"::: ) ($#v7_rlvect_1 :::"scalar-associative"::: ) ($#v8_rlvect_1 :::"scalar-unital"::: ) ($#v5_rltopsp1 :::"strict"::: ) ; end; theorem :: EUCLID:22 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))))) ; theorem :: EUCLID:23 (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")) "is" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) )))) ; theorem :: EUCLID:24 (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")) "is" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) )))) ; registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k15_euclid :::"TOP-REAL"::: ) "n") -> ($#v2_monoid_0 :::"constituted-FinSeqs"::: ) ($#v5_rltopsp1 :::"strict"::: ) ; end; registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster -> ($#v1_finseq_1 :::"FinSequence-like"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" )); end; registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster -> ($#v3_valued_0 :::"real-valued"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" )); end; registrationlet "r", "s" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; let "n" be ($#m1_hidden :::"Nat":::); let "p" be ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); let "f" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::); identify ; end; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "p", "q" be ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); let "f", "g" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::); identify ; end; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "p" be ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); let "f" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::); identify ; end; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "p", "q" be ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); let "f", "g" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::); identify ; end; registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster -> "n" ($#v3_card_1 :::"-element"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" )); end; notationlet "n" be ($#m1_hidden :::"Nat":::); synonym :::"0.REAL"::: "n" for :::"0*"::: "n"; end; definitionlet "n" be ($#m1_hidden :::"Nat":::); :: original: :::"0*"::: redefine func :::"0.REAL"::: "n" -> ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ); end; theorem :: EUCLID:25 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set ($#k13_rvsum_1 :::"sqr"::: ) (Set "(" ($#k10_euclid :::"abs"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k11_euclid :::"sqr"::: ) (Set (Var "x")))))) ; theorem :: EUCLID:26 (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 (Set "(" (Set (Var "p1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "p2")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "p3"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p1")) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "p2")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "p3")) ")" ))))) ; theorem :: EUCLID:27 (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 (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set (Set (Var "p")) ($#k3_rlvect_1 :::"+"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "p"))) ")" ))) ; theorem :: EUCLID:28 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "x")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ))))) ; theorem :: EUCLID:29 (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 (Num 1) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set (Set ($#k6_numbers :::"0"::: ) ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ))) ")" ))) ; theorem :: EUCLID:30 (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")) ")" ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k11_binop_2 :::"*"::: ) (Set (Var "y")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "y")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p")) ")" )))))) ; theorem :: EUCLID:31 (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")) ")" ) (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" "not" (Bool (Set (Set (Var "x")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ))) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ))) ")" )))) ; theorem :: EUCLID:32 (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 (Set (Var "x")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "p1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "p2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p1")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p2")) ")" )))))) ; theorem :: EUCLID: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")) ")" ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k9_binop_2 :::"+"::: ) (Set (Var "y")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p")) ")" )))))) ; theorem :: EUCLID:34 (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 "(" "not" (Bool (Set (Set (Var "x")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p2")))) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool (Set (Var "p1")) ($#r1_hidden :::"="::: ) (Set (Var "p2"))) ")" )))) ; theorem :: EUCLID:35 canceled; theorem :: EUCLID: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 (Set (Var "p")) ($#k3_rlvect_1 :::"+"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ))))) ; theorem :: EUCLID:37 (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")) ")" ) "st" (Bool (Bool (Set (Set (Var "p1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "p2"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" )))) "holds" (Bool (Set (Var "p1")) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "p2")))))) ; theorem :: EUCLID:38 (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 ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "p1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "p2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "p1")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p2")))))) ; theorem :: EUCLID:39 (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_algstr_0 :::"-"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p")))))) ; theorem :: EUCLID: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")) ")" ) (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "x")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_binop_2 :::"-"::: ) (Set (Var "x")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p")))) & (Bool (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "x")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "p")) ")" ))) ")" )))) ; theorem :: EUCLID:41 (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 (Set (Var "p1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p1")) ($#k3_rlvect_1 :::"+"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "p2")) ")" ))))) ; theorem :: EUCLID: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 (Set (Set (Var "p")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ))))) ; theorem :: EUCLID:43 (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")) ")" ) "st" (Bool (Bool (Set (Set (Var "p1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p2"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" )))) "holds" (Bool (Set (Var "p1")) ($#r1_hidden :::"="::: ) (Set (Var "p2"))))) ; theorem :: EUCLID:44 (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 "(" (Bool (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "p1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "p2")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p1")))) & (Bool (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "p1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "p1")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "p2")))) ")" ))) ; theorem :: EUCLID:45 (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 (Set (Var "p1")) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "p2")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p3")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "p2")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p3")))))) ; theorem :: EUCLID:46 (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 (Set (Var "p1")) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "p2")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "p3")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p2")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p3")))))) ; theorem :: EUCLID:47 (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 (Set (Var "p1")) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "p2")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p3")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p2")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "p3")))))) ; theorem :: EUCLID:48 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "," (Set (Var "p1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "p1")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p1")))) & (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p1")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "p1")))) ")" ))) ; theorem :: EUCLID:49 (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 (Set (Var "x")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "p1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p1")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "x")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p2")) ")" )))))) ; theorem :: EUCLID:50 (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")) ")" ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k10_binop_2 :::"-"::: ) (Set (Var "y")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "y")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p")) ")" )))))) ; theorem :: EUCLID:51 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "ex" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )))) ; definitionlet "p" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); func "p" :::"`1"::: -> ($#m1_subset_1 :::"Real":::) equals :: EUCLID:def 9 (Set "p" ($#k1_seq_1 :::"."::: ) (Num 1)); func "p" :::"`2"::: -> ($#m1_subset_1 :::"Real":::) equals :: EUCLID:def 10 (Set "p" ($#k1_seq_1 :::"."::: ) (Num 2)); end; :: deftheorem defines :::"`1"::: EUCLID:def 9 : (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Num 1)))); :: deftheorem defines :::"`2"::: EUCLID:def 10 : (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Num 2)))); notationlet "x", "y" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; synonym :::"|[":::"x" "," "y":::"]|"::: for :::"<*":::"x" "," "y":::"*>":::; end; definitionlet "x", "y" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"|["::: redefine func :::"|[":::"x" "," "y":::"]|"::: -> ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); end; theorem :: EUCLID:52 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Set ($#k19_euclid :::"|["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k19_euclid :::"]|"::: ) ) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Set ($#k19_euclid :::"|["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k19_euclid :::"]|"::: ) ) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" )) ; theorem :: EUCLID:53 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k19_euclid :::"|["::: ) (Set "(" (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ")" ) ($#k19_euclid :::"]|"::: ) ))) ; theorem :: EUCLID:54 (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k19_euclid :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) )) ; theorem :: EUCLID:55 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set (Set (Var "p1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "p2"))) ($#r1_hidden :::"="::: ) (Set ($#k19_euclid :::"|["::: ) (Set "(" (Set "(" (Set (Var "p1")) ($#k17_euclid :::"`1"::: ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "p2")) ($#k17_euclid :::"`1"::: ) ")" ) ")" ) "," (Set "(" (Set "(" (Set (Var "p1")) ($#k18_euclid :::"`2"::: ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "p2")) ($#k18_euclid :::"`2"::: ) ")" ) ")" ) ($#k19_euclid :::"]|"::: ) ))) ; theorem :: EUCLID:56 (Bool "for" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x2")) "," (Set (Var "y2")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k19_euclid :::"|["::: ) (Set (Var "x1")) "," (Set (Var "y1")) ($#k19_euclid :::"]|"::: ) ) ($#k3_rlvect_1 :::"+"::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "x2")) "," (Set (Var "y2")) ($#k19_euclid :::"]|"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k19_euclid :::"|["::: ) (Set "(" (Set (Var "x1")) ($#k9_binop_2 :::"+"::: ) (Set (Var "x2")) ")" ) "," (Set "(" (Set (Var "y1")) ($#k9_binop_2 :::"+"::: ) (Set (Var "y2")) ")" ) ($#k19_euclid :::"]|"::: ) ))) ; theorem :: EUCLID:57 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set (Set (Var "x")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k19_euclid :::"|["::: ) (Set "(" (Set (Var "x")) ($#k4_real_1 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ")" ) ")" ) "," (Set "(" (Set (Var "x")) ($#k4_real_1 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ")" ) ")" ) ($#k19_euclid :::"]|"::: ) )))) ; theorem :: EUCLID:58 (Bool "for" (Set (Var "x")) "," (Set (Var "x1")) "," (Set (Var "y1")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "x")) ($#k1_rlvect_1 :::"*"::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "x1")) "," (Set (Var "y1")) ($#k19_euclid :::"]|"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k19_euclid :::"|["::: ) (Set "(" (Set (Var "x")) ($#k11_binop_2 :::"*"::: ) (Set (Var "x1")) ")" ) "," (Set "(" (Set (Var "x")) ($#k11_binop_2 :::"*"::: ) (Set (Var "y1")) ")" ) ($#k19_euclid :::"]|"::: ) ))) ; theorem :: EUCLID:59 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k19_euclid :::"|["::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ")" ) ")" ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ")" ) ")" ) ($#k19_euclid :::"]|"::: ) ))) ; theorem :: EUCLID:60 (Bool "for" (Set (Var "x1")) "," (Set (Var "y1")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k4_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "x1")) "," (Set (Var "y1")) ($#k19_euclid :::"]|"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k19_euclid :::"|["::: ) (Set "(" ($#k7_binop_2 :::"-"::: ) (Set (Var "x1")) ")" ) "," (Set "(" ($#k7_binop_2 :::"-"::: ) (Set (Var "y1")) ")" ) ($#k19_euclid :::"]|"::: ) ))) ; theorem :: EUCLID:61 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set (Set (Var "p1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p2"))) ($#r1_hidden :::"="::: ) (Set ($#k19_euclid :::"|["::: ) (Set "(" (Set "(" (Set (Var "p1")) ($#k17_euclid :::"`1"::: ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "p2")) ($#k17_euclid :::"`1"::: ) ")" ) ")" ) "," (Set "(" (Set "(" (Set (Var "p1")) ($#k18_euclid :::"`2"::: ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "p2")) ($#k18_euclid :::"`2"::: ) ")" ) ")" ) ($#k19_euclid :::"]|"::: ) ))) ; theorem :: EUCLID:62 (Bool "for" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x2")) "," (Set (Var "y2")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k19_euclid :::"|["::: ) (Set (Var "x1")) "," (Set (Var "y1")) ($#k19_euclid :::"]|"::: ) ) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "x2")) "," (Set (Var "y2")) ($#k19_euclid :::"]|"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k19_euclid :::"|["::: ) (Set "(" (Set (Var "x1")) ($#k10_binop_2 :::"-"::: ) (Set (Var "x2")) ")" ) "," (Set "(" (Set (Var "y1")) ($#k10_binop_2 :::"-"::: ) (Set (Var "y2")) ")" ) ($#k19_euclid :::"]|"::: ) ))) ; theorem :: EUCLID:63 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "Q")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set (Var "Q")))) "holds" (Bool (Set (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) ($#k1_pre_topc :::"|"::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set "(" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ) ($#k1_topmetr :::"|"::: ) (Set (Var "Q")) ")" )))))) ; theorem :: EUCLID:64 (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 "r1")) "," (Set (Var "r2")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "p1")) ($#r1_hidden :::"="::: ) (Set (Var "r1"))) & (Bool (Set (Var "p2")) ($#r1_hidden :::"="::: ) (Set (Var "r2")))) "holds" (Bool (Set (Set (Var "p1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "p2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r1")) ($#k1_valued_1 :::"+"::: ) (Set (Var "r2"))))))) ; theorem :: EUCLID:65 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "r")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "r")))) "holds" (Bool (Set (Set (Var "x")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k24_valued_1 :::"(#)"::: ) (Set (Var "r")))))))) ; theorem :: EUCLID:66 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k16_euclid :::"0.REAL"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" )))) ; theorem :: EUCLID:67 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" )))) ; theorem :: EUCLID:68 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "r1")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "p1")) ($#r1_hidden :::"="::: ) (Set (Var "r1")))) "holds" (Bool (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "p1"))) ($#r1_hidden :::"="::: ) (Set ($#k30_valued_1 :::"-"::: ) (Set (Var "r1"))))))) ; theorem :: EUCLID:69 (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 "r1")) "," (Set (Var "r2")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "p1")) ($#r1_hidden :::"="::: ) (Set (Var "r1"))) & (Bool (Set (Var "p2")) ($#r1_hidden :::"="::: ) (Set (Var "r2")))) "holds" (Bool (Set (Set (Var "p1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r1")) ($#k45_valued_1 :::"-"::: ) (Set (Var "r2"))))))) ; theorem :: EUCLID:70 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_euclid :::"0*"::: ) (Set (Var "n"))))) ; theorem :: EUCLID:71 (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 "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "p")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) )))) ; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "D" be ($#m1_hidden :::"set"::: ) ; cluster (Set "n" ($#k4_finseq_2 :::"-tuples_on"::: ) "D") -> ($#v3_finseq_1 :::"FinSequence-membered"::: ) ; end; registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k1_euclid :::"REAL"::: ) "n") -> ($#v3_finseq_1 :::"FinSequence-membered"::: ) ; end; registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k1_euclid :::"REAL"::: ) "n") -> ($#v3_valued_2 :::"real-functions-membered"::: ) ; end; definitionlet "n" be ($#m1_hidden :::"Nat":::); func :::"1*"::: "n" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) equals :: EUCLID:def 11 (Set "n" ($#k5_finseq_2 :::"|->"::: ) (Num 1)); end; :: deftheorem defines :::"1*"::: EUCLID:def 11 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k20_euclid :::"1*"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k5_finseq_2 :::"|->"::: ) (Num 1)))); definitionlet "n" be ($#m1_hidden :::"Nat":::); :: original: :::"1*"::: redefine func :::"1*"::: "n" -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) "n"); end; definitionlet "n" be ($#m1_hidden :::"Nat":::); func :::"1.REAL"::: "n" -> ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ) equals :: EUCLID:def 12 (Set ($#k21_euclid :::"1*"::: ) "n"); end; :: deftheorem defines :::"1.REAL"::: EUCLID:def 12 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k22_euclid :::"1.REAL"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k21_euclid :::"1*"::: ) (Set (Var "n"))))); theorem :: EUCLID:72 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k10_euclid :::"abs"::: ) (Set "(" ($#k21_euclid :::"1*"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k5_finseq_2 :::"|->"::: ) (Num 1)))) ; theorem :: EUCLID:73 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" ($#k21_euclid :::"1*"::: ) (Set (Var "n")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_square_1 :::"sqrt"::: ) (Set (Var "n"))))) ; theorem :: EUCLID:74 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" ($#k22_euclid :::"1.REAL"::: ) (Set (Var "n")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_square_1 :::"sqrt"::: ) (Set (Var "n"))))) ; theorem :: EUCLID:75 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k12_euclid :::"|."::: ) (Set "(" ($#k22_euclid :::"1.REAL"::: ) (Set (Var "n")) ")" ) ($#k12_euclid :::".|"::: ) ))) ; theorem :: EUCLID:76 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ))) & (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ")" )) ")" )) ; theorem :: EUCLID:77 (Bool (Set ($#k1_euclid :::"REAL"::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k1_tarski :::"}"::: ) )) ;