:: SUPINF_2 semantic presentation begin notationsynonym :::"0."::: for :::"0"::: ; end; definition:: original: :::"0."::: redefine func :::"0."::: -> ($#m1_subset_1 :::"R_eal":::); let "x" be ($#m1_subset_1 :::"R_eal":::); :: original: :::"-"::: redefine func :::"-"::: "x" -> ($#m1_subset_1 :::"R_eal":::); let "y" be ($#m1_subset_1 :::"R_eal":::); :: original: :::"+"::: redefine func "x" :::"+"::: "y" -> ($#m1_subset_1 :::"R_eal":::); :: original: :::"-"::: redefine func "x" :::"-"::: "y" -> ($#m1_subset_1 :::"R_eal":::); end; theorem :: SUPINF_2:1 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"R_eal":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "b")))) "holds" (Bool (Set (Set (Var "x")) ($#k3_supinf_2 :::"+"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k7_real_1 :::"+"::: ) (Set (Var "b")))))) ; theorem :: SUPINF_2:2 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"R_eal":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "a")))) "holds" (Bool (Set ($#k2_supinf_2 :::"-"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set (Var "a")))))) ; theorem :: SUPINF_2:3 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"R_eal":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "b")))) "holds" (Bool (Set (Set (Var "x")) ($#k4_supinf_2 :::"-"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k9_real_1 :::"-"::: ) (Set (Var "b")))))) ; notationlet "X", "Y" be ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ); synonym "X" :::"+"::: "Y" for "X" :::"++"::: "Y"; end; definitionlet "X", "Y" be ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ); :: original: :::"+"::: redefine func "X" :::"+"::: "Y" -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ); end; notationlet "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ); synonym :::"-"::: "X" for :::"--"::: "X"; end; definitionlet "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ); :: original: :::"-"::: redefine func :::"-"::: "X" -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ); end; theorem :: SUPINF_2:4 canceled; theorem :: SUPINF_2:5 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"R_eal":::) "holds" (Bool "(" (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "iff" (Bool (Set ($#k2_supinf_2 :::"-"::: ) (Set (Var "z"))) ($#r2_hidden :::"in"::: ) (Set ($#k6_supinf_2 :::"-"::: ) (Set (Var "X")))) ")" ))) ; theorem :: SUPINF_2:6 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) "iff" (Bool (Set ($#k6_supinf_2 :::"-"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set ($#k6_supinf_2 :::"-"::: ) (Set (Var "Y")))) ")" )) ; theorem :: SUPINF_2:7 (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"R_eal":::) "holds" (Bool "(" (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) "iff" (Bool (Set ($#k2_supinf_2 :::"-"::: ) (Set (Var "z"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) ")" )) ; definitionlet "X" be ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; :: original: :::"inf"::: redefine func :::"inf"::: "X" -> ($#m1_subset_1 :::"R_eal":::); :: original: :::"sup"::: redefine func :::"sup"::: "X" -> ($#m1_subset_1 :::"R_eal":::); end; theorem :: SUPINF_2:8 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool (Set ($#k8_supinf_2 :::"sup"::: ) (Set "(" (Set (Var "X")) ($#k5_supinf_2 :::"+"::: ) (Set (Var "Y")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k8_supinf_2 :::"sup"::: ) (Set (Var "X")) ")" ) ($#k3_supinf_2 :::"+"::: ) (Set "(" ($#k8_supinf_2 :::"sup"::: ) (Set (Var "Y")) ")" )))) ; theorem :: SUPINF_2:9 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool (Set (Set "(" ($#k7_supinf_2 :::"inf"::: ) (Set (Var "X")) ")" ) ($#k3_supinf_2 :::"+"::: ) (Set "(" ($#k7_supinf_2 :::"inf"::: ) (Set (Var "Y")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k7_supinf_2 :::"inf"::: ) (Set "(" (Set (Var "X")) ($#k5_supinf_2 :::"+"::: ) (Set (Var "Y")) ")" )))) ; theorem :: SUPINF_2:10 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v4_xxreal_2 :::"bounded_above"::: ) ) & (Bool (Set (Var "Y")) "is" ($#v4_xxreal_2 :::"bounded_above"::: ) )) "holds" (Bool (Set ($#k8_supinf_2 :::"sup"::: ) (Set "(" (Set (Var "X")) ($#k5_supinf_2 :::"+"::: ) (Set (Var "Y")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k8_supinf_2 :::"sup"::: ) (Set (Var "X")) ")" ) ($#k3_supinf_2 :::"+"::: ) (Set "(" ($#k8_supinf_2 :::"sup"::: ) (Set (Var "Y")) ")" )))) ; theorem :: SUPINF_2:11 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v3_xxreal_2 :::"bounded_below"::: ) ) & (Bool (Set (Var "Y")) "is" ($#v3_xxreal_2 :::"bounded_below"::: ) )) "holds" (Bool (Set (Set "(" ($#k7_supinf_2 :::"inf"::: ) (Set (Var "X")) ")" ) ($#k3_supinf_2 :::"+"::: ) (Set "(" ($#k7_supinf_2 :::"inf"::: ) (Set (Var "Y")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k7_supinf_2 :::"inf"::: ) (Set "(" (Set (Var "X")) ($#k5_supinf_2 :::"+"::: ) (Set (Var "Y")) ")" )))) ; theorem :: SUPINF_2:12 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"R_eal":::) "holds" (Bool "(" (Bool (Set (Var "a")) "is" ($#m1_xxreal_2 :::"UpperBound"::: ) "of" (Set (Var "X"))) "iff" (Bool (Set ($#k2_supinf_2 :::"-"::: ) (Set (Var "a"))) "is" ($#m2_xxreal_2 :::"LowerBound"::: ) "of" (Set ($#k6_supinf_2 :::"-"::: ) (Set (Var "X")))) ")" ))) ; theorem :: SUPINF_2:13 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"R_eal":::) "holds" (Bool "(" (Bool (Set (Var "a")) "is" ($#m2_xxreal_2 :::"LowerBound"::: ) "of" (Set (Var "X"))) "iff" (Bool (Set ($#k2_supinf_2 :::"-"::: ) (Set (Var "a"))) "is" ($#m1_xxreal_2 :::"UpperBound"::: ) "of" (Set ($#k6_supinf_2 :::"-"::: ) (Set (Var "X")))) ")" ))) ; theorem :: SUPINF_2:14 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool (Set ($#k7_supinf_2 :::"inf"::: ) (Set "(" ($#k6_supinf_2 :::"-"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_supinf_2 :::"-"::: ) (Set "(" ($#k8_supinf_2 :::"sup"::: ) (Set (Var "X")) ")" )))) ; theorem :: SUPINF_2:15 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool (Set ($#k8_supinf_2 :::"sup"::: ) (Set "(" ($#k6_supinf_2 :::"-"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_supinf_2 :::"-"::: ) (Set "(" ($#k7_supinf_2 :::"inf"::: ) (Set (Var "X")) ")" )))) ; definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ); let "F" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set (Const "Y")); :: original: :::"rng"::: redefine func :::"rng"::: "F" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ); end; definitionlet "D" be ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "D")); let "F" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); func :::"sup"::: "F" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) equals :: SUPINF_2:def 1 (Set ($#k8_supinf_2 :::"sup"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) "F" ")" )); func :::"inf"::: "F" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) equals :: SUPINF_2:def 2 (Set ($#k7_supinf_2 :::"inf"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) "F" ")" )); end; :: deftheorem defines :::"sup"::: SUPINF_2:def 1 : (Bool "for" (Set (Var "D")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool (Set ($#k10_supinf_2 :::"sup"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k8_supinf_2 :::"sup"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "F")) ")" ))))))); :: deftheorem defines :::"inf"::: SUPINF_2:def 2 : (Bool "for" (Set (Var "D")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool (Set ($#k11_supinf_2 :::"inf"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k7_supinf_2 :::"inf"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "F")) ")" ))))))); definitionlet "F" be ($#v2_valued_0 :::"ext-real-valued"::: ) ($#m1_hidden :::"Function":::); let "x" be ($#m1_hidden :::"set"::: ) ; :: original: :::"."::: redefine func "F" :::"."::: "x" -> ($#m1_subset_1 :::"R_eal":::); end; definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "Y", "Z" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ); let "F" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set (Const "Y")); let "G" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set (Const "Z")); func "F" :::"+"::: "G" -> ($#m1_subset_1 :::"Function":::) "of" "X" "," (Set "(" "Y" ($#k5_supinf_2 :::"+"::: ) "Z" ")" ) means :: SUPINF_2:def 3 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "X" "holds" (Bool (Set it ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "F" ($#k12_supinf_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k3_supinf_2 :::"+"::: ) (Set "(" "G" ($#k12_supinf_2 :::"."::: ) (Set (Var "x")) ")" )))); end; :: deftheorem defines :::"+"::: SUPINF_2:def 3 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Z")) (Bool "for" (Set (Var "b6")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set "(" (Set (Var "Y")) ($#k5_supinf_2 :::"+"::: ) (Set (Var "Z")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k13_supinf_2 :::"+"::: ) (Set (Var "G")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "b6")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k3_supinf_2 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x")) ")" )))) ")" )))))); theorem :: SUPINF_2:16 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Z")) "holds" (Bool (Set ($#k9_supinf_2 :::"rng"::: ) (Set "(" (Set (Var "F")) ($#k13_supinf_2 :::"+"::: ) (Set (Var "G")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k9_supinf_2 :::"rng"::: ) (Set (Var "F")) ")" ) ($#k5_supinf_2 :::"+"::: ) (Set "(" ($#k9_supinf_2 :::"rng"::: ) (Set (Var "G")) ")" ))))))) ; theorem :: SUPINF_2:17 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Z")) "holds" (Bool (Set ($#k10_supinf_2 :::"sup"::: ) (Set "(" (Set (Var "F")) ($#k13_supinf_2 :::"+"::: ) (Set (Var "G")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k10_supinf_2 :::"sup"::: ) (Set (Var "F")) ")" ) ($#k3_supinf_2 :::"+"::: ) (Set "(" ($#k10_supinf_2 :::"sup"::: ) (Set (Var "G")) ")" ))))))) ; theorem :: SUPINF_2:18 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Z")) "holds" (Bool (Set (Set "(" ($#k11_supinf_2 :::"inf"::: ) (Set (Var "F")) ")" ) ($#k3_supinf_2 :::"+"::: ) (Set "(" ($#k11_supinf_2 :::"inf"::: ) (Set (Var "G")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k11_supinf_2 :::"inf"::: ) (Set "(" (Set (Var "F")) ($#k13_supinf_2 :::"+"::: ) (Set (Var "G")) ")" ))))))) ; definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ); let "F" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set (Const "Y")); func :::"-"::: "F" -> ($#m1_subset_1 :::"Function":::) "of" "X" "," (Set "(" ($#k6_supinf_2 :::"-"::: ) "Y" ")" ) means :: SUPINF_2:def 4 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "X" "holds" (Bool (Set it ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k2_supinf_2 :::"-"::: ) (Set "(" "F" ($#k12_supinf_2 :::"."::: ) (Set (Var "x")) ")" )))); end; :: deftheorem defines :::"-"::: SUPINF_2:def 4 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set "(" ($#k6_supinf_2 :::"-"::: ) (Set (Var "Y")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k14_supinf_2 :::"-"::: ) (Set (Var "F")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "b4")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k2_supinf_2 :::"-"::: ) (Set "(" (Set (Var "F")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x")) ")" )))) ")" ))))); theorem :: SUPINF_2:19 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool (Set ($#k9_supinf_2 :::"rng"::: ) (Set "(" ($#k14_supinf_2 :::"-"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_supinf_2 :::"-"::: ) (Set "(" ($#k9_supinf_2 :::"rng"::: ) (Set (Var "F")) ")" )))))) ; theorem :: SUPINF_2:20 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set ($#k11_supinf_2 :::"inf"::: ) (Set "(" ($#k14_supinf_2 :::"-"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_supinf_2 :::"-"::: ) (Set "(" ($#k10_supinf_2 :::"sup"::: ) (Set (Var "F")) ")" ))) & (Bool (Set ($#k10_supinf_2 :::"sup"::: ) (Set "(" ($#k14_supinf_2 :::"-"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_supinf_2 :::"-"::: ) (Set "(" ($#k11_supinf_2 :::"inf"::: ) (Set (Var "F")) ")" ))) ")" )))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ); let "F" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set (Const "Y")); attr "F" is :::"bounded_above"::: means :: SUPINF_2:def 5 (Bool (Set ($#k10_supinf_2 :::"sup"::: ) "F") ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) )); attr "F" is :::"bounded_below"::: means :: SUPINF_2:def 6 (Bool (Set ($#k2_supinf_1 :::"-infty"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k11_supinf_2 :::"inf"::: ) "F")); end; :: deftheorem defines :::"bounded_above"::: SUPINF_2:def 5 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v1_supinf_2 :::"bounded_above"::: ) ) "iff" (Bool (Set ($#k10_supinf_2 :::"sup"::: ) (Set (Var "F"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) )) ")" )))); :: deftheorem defines :::"bounded_below"::: SUPINF_2:def 6 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v2_supinf_2 :::"bounded_below"::: ) ) "iff" (Bool (Set ($#k2_supinf_1 :::"-infty"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k11_supinf_2 :::"inf"::: ) (Set (Var "F")))) ")" )))); definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ); let "F" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set (Const "Y")); attr "F" is :::"bounded"::: means :: SUPINF_2:def 7 (Bool "(" (Bool "F" "is" ($#v1_supinf_2 :::"bounded_above"::: ) ) & (Bool "F" "is" ($#v2_supinf_2 :::"bounded_below"::: ) ) ")" ); end; :: deftheorem defines :::"bounded"::: SUPINF_2:def 7 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v3_supinf_2 :::"bounded"::: ) ) "iff" (Bool "(" (Bool (Set (Var "F")) "is" ($#v1_supinf_2 :::"bounded_above"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_supinf_2 :::"bounded_below"::: ) ) ")" ) ")" )))); registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ); cluster ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FUNCT_2("X" "," "Y") ($#v3_supinf_2 :::"bounded"::: ) -> ($#v1_supinf_2 :::"bounded_above"::: ) ($#v2_supinf_2 :::"bounded_below"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1("X" "," "Y")))); cluster ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FUNCT_2("X" "," "Y") ($#v1_supinf_2 :::"bounded_above"::: ) ($#v2_supinf_2 :::"bounded_below"::: ) -> ($#v3_supinf_2 :::"bounded"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1("X" "," "Y")))); end; theorem :: SUPINF_2:21 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v3_supinf_2 :::"bounded"::: ) ) "iff" (Bool "(" (Bool (Set ($#k10_supinf_2 :::"sup"::: ) (Set (Var "F"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) )) & (Bool (Set ($#k2_supinf_1 :::"-infty"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k11_supinf_2 :::"inf"::: ) (Set (Var "F")))) ")" ) ")" )))) ; theorem :: SUPINF_2:22 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v1_supinf_2 :::"bounded_above"::: ) ) "iff" (Bool (Set ($#k14_supinf_2 :::"-"::: ) (Set (Var "F"))) "is" ($#v2_supinf_2 :::"bounded_below"::: ) ) ")" )))) ; theorem :: SUPINF_2:23 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v2_supinf_2 :::"bounded_below"::: ) ) "iff" (Bool (Set ($#k14_supinf_2 :::"-"::: ) (Set (Var "F"))) "is" ($#v1_supinf_2 :::"bounded_above"::: ) ) ")" )))) ; theorem :: SUPINF_2:24 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v3_supinf_2 :::"bounded"::: ) ) "iff" (Bool (Set ($#k14_supinf_2 :::"-"::: ) (Set (Var "F"))) "is" ($#v3_supinf_2 :::"bounded"::: ) ) ")" )))) ; theorem :: SUPINF_2:25 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set ($#k2_supinf_1 :::"-infty"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "F")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x")))) & (Bool (Set (Set (Var "F")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) )) ")" ))))) ; theorem :: SUPINF_2:26 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set ($#k1_numbers :::"REAL"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k2_supinf_1 :::"-infty"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "F")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x")))) & (Bool (Set (Set (Var "F")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) )) ")" ))))) ; theorem :: SUPINF_2:27 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set ($#k11_supinf_2 :::"inf"::: ) (Set (Var "F"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "F")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x")))) & (Bool (Set (Set (Var "F")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k10_supinf_2 :::"sup"::: ) (Set (Var "F")))) ")" ))))) ; theorem :: SUPINF_2:28 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set ($#k1_numbers :::"REAL"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v1_supinf_2 :::"bounded_above"::: ) ) "iff" (Bool (Set ($#k10_supinf_2 :::"sup"::: ) (Set (Var "F"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) ")" )))) ; theorem :: SUPINF_2:29 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set ($#k1_numbers :::"REAL"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v2_supinf_2 :::"bounded_below"::: ) ) "iff" (Bool (Set ($#k11_supinf_2 :::"inf"::: ) (Set (Var "F"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) ")" )))) ; theorem :: SUPINF_2:30 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set ($#k1_numbers :::"REAL"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v3_supinf_2 :::"bounded"::: ) ) "iff" (Bool "(" (Bool (Set ($#k11_supinf_2 :::"inf"::: ) (Set (Var "F"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) & (Bool (Set ($#k10_supinf_2 :::"sup"::: ) (Set (Var "F"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) ")" ) ")" )))) ; theorem :: SUPINF_2:31 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "F1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "F2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Z")) "st" (Bool (Bool (Set (Var "F1")) "is" ($#v1_supinf_2 :::"bounded_above"::: ) ) & (Bool (Set (Var "F2")) "is" ($#v1_supinf_2 :::"bounded_above"::: ) )) "holds" (Bool (Set (Set (Var "F1")) ($#k13_supinf_2 :::"+"::: ) (Set (Var "F2"))) "is" ($#v1_supinf_2 :::"bounded_above"::: ) ))))) ; theorem :: SUPINF_2:32 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "F1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "F2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Z")) "st" (Bool (Bool (Set (Var "F1")) "is" ($#v2_supinf_2 :::"bounded_below"::: ) ) & (Bool (Set (Var "F2")) "is" ($#v2_supinf_2 :::"bounded_below"::: ) )) "holds" (Bool (Set (Set (Var "F1")) ($#k13_supinf_2 :::"+"::: ) (Set (Var "F2"))) "is" ($#v2_supinf_2 :::"bounded_below"::: ) ))))) ; theorem :: SUPINF_2:33 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "F1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "F2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Z")) "st" (Bool (Bool (Set (Var "F1")) "is" ($#v3_supinf_2 :::"bounded"::: ) ) & (Bool (Set (Var "F2")) "is" ($#v3_supinf_2 :::"bounded"::: ) )) "holds" (Bool (Set (Set (Var "F1")) ($#k13_supinf_2 :::"+"::: ) (Set (Var "F2"))) "is" ($#v3_supinf_2 :::"bounded"::: ) ))))) ; theorem :: SUPINF_2:34 (Bool "(" (Bool (Set ($#k6_funct_3 :::"incl"::: ) (Set ($#k5_numbers :::"NAT"::: ) )) "is" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k7_numbers :::"ExtREAL"::: ) )) & (Bool (Set ($#k6_funct_3 :::"incl"::: ) (Set ($#k5_numbers :::"NAT"::: ) )) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k5_numbers :::"NAT"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" ($#k6_funct_3 :::"incl"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ")" ))) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" ($#k6_funct_3 :::"incl"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ")" )) "is" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) )) ")" ) ; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "IT" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "D")); :: original: :::"countable"::: redefine attr "IT" is :::"countable"::: means :: SUPINF_2:def 8 (Bool "(" (Bool "IT" "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," "D" "st" (Bool "IT" ($#r1_hidden :::"="::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "F"))))) ")" ); end; :: deftheorem defines :::"countable"::: SUPINF_2:def 8 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v4_card_3 :::"countable"::: ) ) "iff" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "D")) "st" (Bool (Set (Var "IT")) ($#r1_hidden :::"="::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "F"))))) ")" ) ")" ))); registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_membered :::"ext-real-membered"::: ) bbbadV4_CARD_3() for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set ($#k7_numbers :::"ExtREAL"::: ) ))); end; definitionmode Denum_Set_of_R_EAL is ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) bbbadV4_CARD_3() ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ); end; definitionlet "IT" be ($#m1_hidden :::"set"::: ) ; attr "IT" is :::"nonnegative"::: means :: SUPINF_2:def 9 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"R_eal":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "IT")) "holds" (Bool (Set ($#k1_supinf_2 :::"0."::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "x")))); end; :: deftheorem defines :::"nonnegative"::: SUPINF_2:def 9 : (Bool "for" (Set (Var "IT")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v5_supinf_2 :::"nonnegative"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"R_eal":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "IT")))) "holds" (Bool (Set ($#k1_supinf_2 :::"0."::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "x")))) ")" )); registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_membered :::"ext-real-membered"::: ) ($#v4_card_3 :::"countable"::: ) ($#v5_supinf_2 :::"nonnegative"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set ($#k7_numbers :::"ExtREAL"::: ) ))); end; definitionmode Pos_Denum_Set_of_R_EAL is ($#v5_supinf_2 :::"nonnegative"::: ) ($#m1_subset_1 :::"Denum_Set_of_R_EAL":::); end; definitionlet "D" be ($#m1_subset_1 :::"Denum_Set_of_R_EAL":::); mode :::"Num"::: "of" "D" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) means :: SUPINF_2:def 10 (Bool "D" ($#r1_hidden :::"="::: ) (Set ($#k2_relset_1 :::"rng"::: ) it)); end; :: deftheorem defines :::"Num"::: SUPINF_2:def 10 : (Bool "for" (Set (Var "D")) "being" ($#m1_subset_1 :::"Denum_Set_of_R_EAL":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_supinf_2 :::"Num"::: ) "of" (Set (Var "D"))) "iff" (Bool (Set (Var "D")) ($#r1_hidden :::"="::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "b2")))) ")" ))); definitionlet "D" be ($#m1_subset_1 :::"Denum_Set_of_R_EAL":::); let "N" be ($#m1_supinf_2 :::"Num"::: ) "of" (Set (Const "D")); func :::"Ser"::: "(" "D" "," "N" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) means :: SUPINF_2:def 11 (Bool "(" (Bool (Set it ($#k12_supinf_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set "N" ($#k12_supinf_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"R_eal":::) "st" (Bool (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set it ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))))) "holds" (Bool (Set it ($#k12_supinf_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k3_supinf_2 :::"+"::: ) (Set "(" "N" ($#k12_supinf_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )))) ")" ) ")" ); end; :: deftheorem defines :::"Ser"::: SUPINF_2:def 11 : (Bool "for" (Set (Var "D")) "being" ($#m1_subset_1 :::"Denum_Set_of_R_EAL":::) (Bool "for" (Set (Var "N")) "being" ($#m1_supinf_2 :::"Num"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k15_supinf_2 :::"Ser"::: ) "(" (Set (Var "D")) "," (Set (Var "N")) ")" )) "iff" (Bool "(" (Bool (Set (Set (Var "b3")) ($#k12_supinf_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "N")) ($#k12_supinf_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"R_eal":::) "st" (Bool (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b3")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k12_supinf_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k3_supinf_2 :::"+"::: ) (Set "(" (Set (Var "N")) ($#k12_supinf_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )))) ")" ) ")" ) ")" )))); theorem :: SUPINF_2:35 (Bool "for" (Set (Var "D")) "being" ($#m1_subset_1 :::"Pos_Denum_Set_of_R_EAL":::) (Bool "for" (Set (Var "N")) "being" ($#m1_supinf_2 :::"Num"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k1_supinf_2 :::"0."::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "N")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))))))) ; theorem :: SUPINF_2:36 (Bool "for" (Set (Var "D")) "being" ($#m1_subset_1 :::"Pos_Denum_Set_of_R_EAL":::) (Bool "for" (Set (Var "N")) "being" ($#m1_supinf_2 :::"Num"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k15_supinf_2 :::"Ser"::: ) "(" (Set (Var "D")) "," (Set (Var "N")) ")" ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k15_supinf_2 :::"Ser"::: ) "(" (Set (Var "D")) "," (Set (Var "N")) ")" ")" ) ($#k12_supinf_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) & (Bool (Set ($#k1_supinf_2 :::"0."::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k15_supinf_2 :::"Ser"::: ) "(" (Set (Var "D")) "," (Set (Var "N")) ")" ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "n")))) ")" )))) ; theorem :: SUPINF_2:37 (Bool "for" (Set (Var "D")) "being" ($#m1_subset_1 :::"Pos_Denum_Set_of_R_EAL":::) (Bool "for" (Set (Var "N")) "being" ($#m1_supinf_2 :::"Num"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k15_supinf_2 :::"Ser"::: ) "(" (Set (Var "D")) "," (Set (Var "N")) ")" ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k15_supinf_2 :::"Ser"::: ) "(" (Set (Var "D")) "," (Set (Var "N")) ")" ")" ) ($#k12_supinf_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Set (Var "m")) ")" )))))) ; definitionlet "D" be ($#m1_subset_1 :::"Denum_Set_of_R_EAL":::); mode :::"Set_of_Series"::: "of" "D" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) means :: SUPINF_2:def 12 (Bool "ex" (Set (Var "N")) "being" ($#m1_supinf_2 :::"Num"::: ) "of" "D" "st" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" ($#k15_supinf_2 :::"Ser"::: ) "(" "D" "," (Set (Var "N")) ")" ")" )))); end; :: deftheorem defines :::"Set_of_Series"::: SUPINF_2:def 12 : (Bool "for" (Set (Var "D")) "being" ($#m1_subset_1 :::"Denum_Set_of_R_EAL":::) (Bool "for" (Set (Var "b2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m2_supinf_2 :::"Set_of_Series"::: ) "of" (Set (Var "D"))) "iff" (Bool "ex" (Set (Var "N")) "being" ($#m1_supinf_2 :::"Num"::: ) "of" (Set (Var "D")) "st" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" ($#k15_supinf_2 :::"Ser"::: ) "(" (Set (Var "D")) "," (Set (Var "N")) ")" ")" )))) ")" ))); definitionlet "D" be ($#m1_subset_1 :::"Pos_Denum_Set_of_R_EAL":::); let "N" be ($#m1_supinf_2 :::"Num"::: ) "of" (Set (Const "D")); func :::"SUM"::: "(" "D" "," "N" ")" -> ($#m1_subset_1 :::"R_eal":::) equals :: SUPINF_2:def 13 (Set ($#k8_supinf_2 :::"sup"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set "(" ($#k15_supinf_2 :::"Ser"::: ) "(" "D" "," "N" ")" ")" ) ")" )); end; :: deftheorem defines :::"SUM"::: SUPINF_2:def 13 : (Bool "for" (Set (Var "D")) "being" ($#m1_subset_1 :::"Pos_Denum_Set_of_R_EAL":::) (Bool "for" (Set (Var "N")) "being" ($#m1_supinf_2 :::"Num"::: ) "of" (Set (Var "D")) "holds" (Bool (Set ($#k16_supinf_2 :::"SUM"::: ) "(" (Set (Var "D")) "," (Set (Var "N")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_supinf_2 :::"sup"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set "(" ($#k15_supinf_2 :::"Ser"::: ) "(" (Set (Var "D")) "," (Set (Var "N")) ")" ")" ) ")" ))))); definitionlet "D" be ($#m1_subset_1 :::"Pos_Denum_Set_of_R_EAL":::); let "N" be ($#m1_supinf_2 :::"Num"::: ) "of" (Set (Const "D")); pred "D" :::"is_sumable"::: "N" means :: SUPINF_2:def 14 (Bool (Set ($#k16_supinf_2 :::"SUM"::: ) "(" "D" "," "N" ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k1_numbers :::"REAL"::: ) )); end; :: deftheorem defines :::"is_sumable"::: SUPINF_2:def 14 : (Bool "for" (Set (Var "D")) "being" ($#m1_subset_1 :::"Pos_Denum_Set_of_R_EAL":::) (Bool "for" (Set (Var "N")) "being" ($#m1_supinf_2 :::"Num"::: ) "of" (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Var "D")) ($#r1_supinf_2 :::"is_sumable"::: ) (Set (Var "N"))) "iff" (Bool (Set ($#k16_supinf_2 :::"SUM"::: ) "(" (Set (Var "D")) "," (Set (Var "N")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) ")" ))); theorem :: SUPINF_2:38 (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "F"))) "is" ($#m1_subset_1 :::"Denum_Set_of_R_EAL":::))) ; definitionlet "F" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ); :: original: :::"rng"::: redefine func :::"rng"::: "F" -> ($#m1_subset_1 :::"Denum_Set_of_R_EAL":::); end; definitionlet "F" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ); func :::"Ser"::: "F" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) means :: SUPINF_2:def 15 (Bool "for" (Set (Var "N")) "being" ($#m1_supinf_2 :::"Num"::: ) "of" (Set ($#k17_supinf_2 :::"rng"::: ) "F") "st" (Bool (Bool (Set (Var "N")) ($#r2_funct_2 :::"="::: ) "F")) "holds" (Bool it ($#r2_funct_2 :::"="::: ) (Set ($#k15_supinf_2 :::"Ser"::: ) "(" (Set "(" ($#k17_supinf_2 :::"rng"::: ) "F" ")" ) "," (Set (Var "N")) ")" ))); end; :: deftheorem defines :::"Ser"::: SUPINF_2:def 15 : (Bool "for" (Set (Var "F")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k18_supinf_2 :::"Ser"::: ) (Set (Var "F")))) "iff" (Bool "for" (Set (Var "N")) "being" ($#m1_supinf_2 :::"Num"::: ) "of" (Set ($#k17_supinf_2 :::"rng"::: ) (Set (Var "F"))) "st" (Bool (Bool (Set (Var "N")) ($#r2_funct_2 :::"="::: ) (Set (Var "F")))) "holds" (Bool (Set (Var "b2")) ($#r2_funct_2 :::"="::: ) (Set ($#k15_supinf_2 :::"Ser"::: ) "(" (Set "(" ($#k17_supinf_2 :::"rng"::: ) (Set (Var "F")) ")" ) "," (Set (Var "N")) ")" ))) ")" )); definitionlet "R" be ($#m1_hidden :::"Relation":::); attr "R" is :::"nonnegative"::: means :: SUPINF_2:def 16 (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) "R") "is" ($#v5_supinf_2 :::"nonnegative"::: ) ); end; :: deftheorem defines :::"nonnegative"::: SUPINF_2:def 16 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ) "iff" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R"))) "is" ($#v5_supinf_2 :::"nonnegative"::: ) ) ")" )); definitionlet "F" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ); func :::"SUM"::: "F" -> ($#m1_subset_1 :::"R_eal":::) equals :: SUPINF_2:def 17 (Set ($#k8_supinf_2 :::"sup"::: ) (Set "(" ($#k17_supinf_2 :::"rng"::: ) (Set "(" ($#k18_supinf_2 :::"Ser"::: ) "F" ")" ) ")" )); end; :: deftheorem defines :::"SUM"::: SUPINF_2:def 17 : (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool (Set ($#k19_supinf_2 :::"SUM"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k8_supinf_2 :::"sup"::: ) (Set "(" ($#k17_supinf_2 :::"rng"::: ) (Set "(" ($#k18_supinf_2 :::"Ser"::: ) (Set (Var "F")) ")" ) ")" )))); theorem :: SUPINF_2:39 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool (Set ($#k1_supinf_2 :::"0."::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "F")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))))) ")" ))) ; theorem :: SUPINF_2:40 (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "F")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) )) "holds" (Bool "(" (Bool (Set (Set "(" ($#k18_supinf_2 :::"Ser"::: ) (Set (Var "F")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k18_supinf_2 :::"Ser"::: ) (Set (Var "F")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) & (Bool (Set ($#k1_supinf_2 :::"0."::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k18_supinf_2 :::"Ser"::: ) (Set (Var "F")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "n")))) ")" ))) ; theorem :: SUPINF_2:41 (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) )) "holds" (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k18_supinf_2 :::"Ser"::: ) (Set (Var "F")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k18_supinf_2 :::"Ser"::: ) (Set (Var "F")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Set (Var "m")) ")" ))))) ; theorem :: SUPINF_2:42 (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "F1")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "F2")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n")))) ")" )) "holds" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k18_supinf_2 :::"Ser"::: ) (Set (Var "F1")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k18_supinf_2 :::"Ser"::: ) (Set (Var "F2")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "n")))))) ; theorem :: SUPINF_2:43 (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "F1")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "F2")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n")))) ")" )) "holds" (Bool (Set ($#k19_supinf_2 :::"SUM"::: ) (Set (Var "F1"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k19_supinf_2 :::"SUM"::: ) (Set (Var "F2"))))) ; theorem :: SUPINF_2:44 (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k18_supinf_2 :::"Ser"::: ) (Set (Var "F")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k12_supinf_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"R_eal":::) "st" (Bool (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k18_supinf_2 :::"Ser"::: ) (Set (Var "F")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))))) "holds" (Bool (Set (Set "(" ($#k18_supinf_2 :::"Ser"::: ) (Set (Var "F")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k3_supinf_2 :::"+"::: ) (Set "(" (Set (Var "F")) ($#k12_supinf_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )))) ")" ) ")" )) ; theorem :: SUPINF_2:45 (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ) & (Bool "ex" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Set (Var "F")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) )))) "holds" (Bool (Set ($#k19_supinf_2 :::"SUM"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) ))) ; definitionlet "F" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ); attr "F" is :::"summable"::: means :: SUPINF_2:def 18 (Bool (Set ($#k19_supinf_2 :::"SUM"::: ) "F") ($#r2_hidden :::"in"::: ) (Set ($#k1_numbers :::"REAL"::: ) )); end; :: deftheorem defines :::"summable"::: SUPINF_2:def 18 : (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v7_supinf_2 :::"summable"::: ) ) "iff" (Bool (Set ($#k19_supinf_2 :::"SUM"::: ) (Set (Var "F"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) ")" )); theorem :: SUPINF_2:46 (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ) & (Bool "ex" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Set (Var "F")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) )))) "holds" (Bool "not" (Bool (Set (Var "F")) "is" ($#v7_supinf_2 :::"summable"::: ) ))) ; theorem :: SUPINF_2:47 (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "F1")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "F1")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "F2")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n")))) ")" ) & (Bool (Set (Var "F2")) "is" ($#v7_supinf_2 :::"summable"::: ) )) "holds" (Bool (Set (Var "F1")) "is" ($#v7_supinf_2 :::"summable"::: ) )) ; theorem :: SUPINF_2:48 (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) )) "holds" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool "(" "for" (Set (Var "r")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r")))) "holds" (Bool (Set (Set (Var "F")) ($#k12_supinf_2 :::"."::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set ($#k1_supinf_2 :::"0."::: ) )) ")" )) "holds" (Bool (Set ($#k19_supinf_2 :::"SUM"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k18_supinf_2 :::"Ser"::: ) (Set (Var "F")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "n")))))) ; theorem :: SUPINF_2:49 (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "F")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) ")" )) "holds" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k18_supinf_2 :::"Ser"::: ) (Set (Var "F")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_numbers :::"REAL"::: ) )))) ; theorem :: SUPINF_2:50 (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ) & (Bool "ex" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k")))) "holds" (Bool (Set (Set (Var "F")) ($#k12_supinf_2 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k1_supinf_2 :::"0."::: ) )) ")" ) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "F")) ($#k12_supinf_2 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) )) ")" ) ")" ))) "holds" (Bool (Set (Var "F")) "is" ($#v7_supinf_2 :::"summable"::: ) )) ; theorem :: SUPINF_2:51 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_supinf_2 :::"0."::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "F")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))))) ")" ))) ; theorem :: SUPINF_2:52 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set ($#k1_supinf_2 :::"0."::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "F")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n")))) ")" )) "holds" (Bool (Set (Var "F")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ))) ;