:: INTEGRA3 semantic presentation begin definitionlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_measure5 :::"closed_interval"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ); let "D" be ($#m1_integra1 :::"Division"::: ) "of" (Set (Const "A")); func :::"delta"::: "D" -> ($#m1_subset_1 :::"Real":::) equals :: INTEGRA3:def 1 (Set ($#k1_xxreal_2 :::"max"::: ) (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set "(" ($#k4_integra1 :::"upper_volume"::: ) "(" (Set "(" ($#k7_rfunct_1 :::"chi"::: ) "(" "A" "," "A" ")" ")" ) "," "D" ")" ")" ) ")" )); end; :: deftheorem defines :::"delta"::: INTEGRA3:def 1 : (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_measure5 :::"closed_interval"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "D")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) "holds" (Bool (Set ($#k1_integra3 :::"delta"::: ) (Set (Var "D"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xxreal_2 :::"max"::: ) (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set "(" ($#k4_integra1 :::"upper_volume"::: ) "(" (Set "(" ($#k7_rfunct_1 :::"chi"::: ) "(" (Set (Var "A")) "," (Set (Var "A")) ")" ")" ) "," (Set (Var "D")) ")" ")" ) ")" ))))); definitionlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_measure5 :::"closed_interval"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ); let "T" be ($#m1_subset_1 :::"DivSequence":::) "of" (Set (Const "A")); func :::"delta"::: "T" -> ($#m1_subset_1 :::"Real_Sequence":::) means :: INTEGRA3:def 2 (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k1_integra3 :::"delta"::: ) (Set "(" "T" ($#k2_integra2 :::"."::: ) (Set (Var "i")) ")" )))); end; :: deftheorem defines :::"delta"::: INTEGRA3:def 2 : (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_measure5 :::"closed_interval"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"DivSequence":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k2_integra3 :::"delta"::: ) (Set (Var "T")))) "iff" (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b3")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k1_integra3 :::"delta"::: ) (Set "(" (Set (Var "T")) ($#k2_integra2 :::"."::: ) (Set (Var "i")) ")" )))) ")" )))); theorem :: INTEGRA3:1 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_measure5 :::"closed_interval"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "D1")) "," (Set (Var "D2")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "D1")) ($#r1_integra1 :::"<="::: ) (Set (Var "D2")))) "holds" (Bool (Set ($#k1_integra3 :::"delta"::: ) (Set (Var "D1"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k1_integra3 :::"delta"::: ) (Set (Var "D2")))))) ; theorem :: INTEGRA3:2 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_measure5 :::"closed_interval"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "D")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set ($#k3_integra1 :::"vol"::: ) (Set (Var "A"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "ex" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "D")))) & (Bool (Set ($#k3_integra1 :::"vol"::: ) (Set "(" ($#k2_integra1 :::"divset"::: ) "(" (Set (Var "D")) "," (Set (Var "i")) ")" ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )))) ; theorem :: INTEGRA3:3 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_measure5 :::"closed_interval"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "D")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool "ex" (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "D")))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_integra1 :::"divset"::: ) "(" (Set (Var "D")) "," (Set (Var "j")) ")" )) ")" ))))) ; theorem :: INTEGRA3:4 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_measure5 :::"closed_interval"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "D1")) "," (Set (Var "D2")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) (Bool "ex" (Set (Var "D")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) "st" (Bool "(" (Bool (Set (Var "D1")) ($#r1_integra1 :::"<="::: ) (Set (Var "D"))) & (Bool (Set (Var "D2")) ($#r1_integra1 :::"<="::: ) (Set (Var "D"))) & (Bool (Set ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "D"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "D1")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "D2")) ")" ))) ")" )))) ; theorem :: INTEGRA3:5 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_measure5 :::"closed_interval"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "D1")) "," (Set (Var "D")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set ($#k1_integra3 :::"delta"::: ) (Set (Var "D1"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k2_xxreal_2 :::"min"::: ) (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set "(" ($#k4_integra1 :::"upper_volume"::: ) "(" (Set "(" ($#k7_rfunct_1 :::"chi"::: ) "(" (Set (Var "A")) "," (Set (Var "A")) ")" ")" ) "," (Set (Var "D")) ")" ")" ) ")" )))) "holds" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "D1")))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "D")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k2_integra1 :::"divset"::: ) "(" (Set (Var "D1")) "," (Set (Var "i")) ")" ")" ))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "D")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k2_integra1 :::"divset"::: ) "(" (Set (Var "D1")) "," (Set (Var "i")) ")" ")" )))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))))))) ; theorem :: INTEGRA3:6 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "q")))) & (Bool (Set (Var "p")) "is" ($#v5_valued_0 :::"increasing"::: ) ) & (Bool (Set (Var "q")) "is" ($#v5_valued_0 :::"increasing"::: ) )) "holds" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "q")))) ; theorem :: INTEGRA3:7 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_measure5 :::"closed_interval"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "D")) "," (Set (Var "D1")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "D")) ($#r1_integra1 :::"<="::: ) (Set (Var "D1"))) & (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "D")))) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "D")))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j")))) "holds" (Bool "(" (Bool (Set ($#k13_integra1 :::"indx"::: ) "(" (Set (Var "D1")) "," (Set (Var "D")) "," (Set (Var "i")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k13_integra1 :::"indx"::: ) "(" (Set (Var "D1")) "," (Set (Var "D")) "," (Set (Var "j")) ")" )) & (Bool (Set ($#k13_integra1 :::"indx"::: ) "(" (Set (Var "D1")) "," (Set (Var "D")) "," (Set (Var "i")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "D1")))) ")" )))) ; theorem :: INTEGRA3:8 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_measure5 :::"closed_interval"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "D")) "," (Set (Var "D1")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "D")) ($#r1_integra1 :::"<="::: ) (Set (Var "D1"))) & (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "D")))) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "D")))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j")))) "holds" (Bool (Set ($#k13_integra1 :::"indx"::: ) "(" (Set (Var "D1")) "," (Set (Var "D")) "," (Set (Var "i")) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k13_integra1 :::"indx"::: ) "(" (Set (Var "D1")) "," (Set (Var "D")) "," (Set (Var "j")) ")" ))))) ; theorem :: INTEGRA3:9 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_measure5 :::"closed_interval"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "D")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) "holds" (Bool (Set ($#k1_integra3 :::"delta"::: ) (Set (Var "D"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: INTEGRA3:10 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_measure5 :::"closed_interval"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "D1")) "," (Set (Var "D2")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_integra1 :::"divset"::: ) "(" (Set (Var "D1")) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "D1")) ")" ) ")" )) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "D1"))) ($#r1_xxreal_0 :::">="::: ) (Num 2)) & (Bool (Set (Var "D1")) ($#r1_integra1 :::"<="::: ) (Set (Var "D2"))) & (Bool (Set ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "D2"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "D1")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k1_seq_4 :::"{"::: ) (Set (Var "x")) ($#k1_seq_4 :::"}"::: ) ))) & (Bool (Set (Set (Var "g")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) "is" ($#v1_comseq_2 :::"bounded"::: ) )) "holds" (Bool (Set (Set "(" ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k5_integra1 :::"lower_volume"::: ) "(" (Set (Var "g")) "," (Set (Var "D2")) ")" ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k5_integra1 :::"lower_volume"::: ) "(" (Set (Var "g")) "," (Set (Var "D1")) ")" ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set "(" ($#k4_seq_4 :::"upper_bound"::: ) (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "g")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k5_seq_4 :::"lower_bound"::: ) (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "g")) ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k1_integra3 :::"delta"::: ) (Set (Var "D1")) ")" ))))))) ; theorem :: INTEGRA3:11 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_measure5 :::"closed_interval"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "D1")) "," (Set (Var "D2")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_integra1 :::"divset"::: ) "(" (Set (Var "D1")) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "D1")) ")" ) ")" )) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "D1"))) ($#r1_xxreal_0 :::">="::: ) (Num 2)) & (Bool (Set (Var "D1")) ($#r1_integra1 :::"<="::: ) (Set (Var "D2"))) & (Bool (Set ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "D2"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "D1")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k1_seq_4 :::"{"::: ) (Set (Var "x")) ($#k1_seq_4 :::"}"::: ) ))) & (Bool (Set (Set (Var "g")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) "is" ($#v1_comseq_2 :::"bounded"::: ) )) "holds" (Bool (Set (Set "(" ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k4_integra1 :::"upper_volume"::: ) "(" (Set (Var "g")) "," (Set (Var "D1")) ")" ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k4_integra1 :::"upper_volume"::: ) "(" (Set (Var "g")) "," (Set (Var "D2")) ")" ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set "(" ($#k4_seq_4 :::"upper_bound"::: ) (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "g")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k5_seq_4 :::"lower_bound"::: ) (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "g")) ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k1_integra3 :::"delta"::: ) (Set (Var "D1")) ")" ))))))) ; theorem :: INTEGRA3:12 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_measure5 :::"closed_interval"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "D")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "D")))) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "D")))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" ($#k3_finseq_6 :::"mid"::: ) "(" (Set (Var "D")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Num 1)))) "holds" (Bool "ex" (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_measure5 :::"closed_interval"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set ($#k5_seq_4 :::"lower_bound"::: ) (Set (Var "B")))) & (Bool (Set ($#k4_seq_4 :::"upper_bound"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_finseq_6 :::"mid"::: ) "(" (Set (Var "D")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k3_finseq_6 :::"mid"::: ) "(" (Set (Var "D")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) ")" ))) & (Bool (Set ($#k3_finseq_6 :::"mid"::: ) "(" (Set (Var "D")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ) "is" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "B"))) ")" )))))) ; theorem :: INTEGRA3:13 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_measure5 :::"closed_interval"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "D1")) "," (Set (Var "D2")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_integra1 :::"divset"::: ) "(" (Set (Var "D1")) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "D1")) ")" ) ")" )) & (Bool (Set ($#k3_integra1 :::"vol"::: ) (Set (Var "A"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "D1")) ($#r1_integra1 :::"<="::: ) (Set (Var "D2"))) & (Bool (Set ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "D2"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "D1")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k1_seq_4 :::"{"::: ) (Set (Var "x")) ($#k1_seq_4 :::"}"::: ) ))) & (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) "is" ($#v1_comseq_2 :::"bounded"::: ) ) & (Bool (Set (Var "x")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k5_seq_4 :::"lower_bound"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Set "(" ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k5_integra1 :::"lower_volume"::: ) "(" (Set (Var "f")) "," (Set (Var "D2")) ")" ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k5_integra1 :::"lower_volume"::: ) "(" (Set (Var "f")) "," (Set (Var "D1")) ")" ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set "(" ($#k4_seq_4 :::"upper_bound"::: ) (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "f")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k5_seq_4 :::"lower_bound"::: ) (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "f")) ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k1_integra3 :::"delta"::: ) (Set (Var "D1")) ")" ))))))) ; theorem :: INTEGRA3:14 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_measure5 :::"closed_interval"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "D1")) "," (Set (Var "D2")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_integra1 :::"divset"::: ) "(" (Set (Var "D1")) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "D1")) ")" ) ")" )) & (Bool (Set ($#k3_integra1 :::"vol"::: ) (Set (Var "A"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "D1")) ($#r1_integra1 :::"<="::: ) (Set (Var "D2"))) & (Bool (Set ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "D2"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "D1")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k1_seq_4 :::"{"::: ) (Set (Var "x")) ($#k1_seq_4 :::"}"::: ) ))) & (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) "is" ($#v1_comseq_2 :::"bounded"::: ) ) & (Bool (Set (Var "x")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k5_seq_4 :::"lower_bound"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Set "(" ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k4_integra1 :::"upper_volume"::: ) "(" (Set (Var "f")) "," (Set (Var "D1")) ")" ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k4_integra1 :::"upper_volume"::: ) "(" (Set (Var "f")) "," (Set (Var "D2")) ")" ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set "(" ($#k4_seq_4 :::"upper_bound"::: ) (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "f")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k5_seq_4 :::"lower_bound"::: ) (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "f")) ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k1_integra3 :::"delta"::: ) (Set (Var "D1")) ")" ))))))) ; theorem :: INTEGRA3:15 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_measure5 :::"closed_interval"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "D1")) "," (Set (Var "D2")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "D1")))) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "D1")))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "D1")) ($#r1_integra1 :::"<="::: ) (Set (Var "D2"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" ($#k3_finseq_6 :::"mid"::: ) "(" (Set (Var "D2")) "," (Set "(" ($#k13_integra1 :::"indx"::: ) "(" (Set (Var "D2")) "," (Set (Var "D1")) "," (Set (Var "i")) ")" ")" ) "," (Set "(" ($#k13_integra1 :::"indx"::: ) "(" (Set (Var "D2")) "," (Set (Var "D1")) "," (Set (Var "j")) ")" ")" ) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Num 1)))) "holds" (Bool "ex" (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_measure5 :::"closed_interval"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) )(Bool "ex" (Set (Var "MD1")) "," (Set (Var "MD2")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "B")) "st" (Bool "(" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set ($#k5_seq_4 :::"lower_bound"::: ) (Set (Var "B")))) & (Bool (Set ($#k4_seq_4 :::"upper_bound"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "MD2")) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "MD2")) ")" ))) & (Bool (Set ($#k4_seq_4 :::"upper_bound"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "MD1")) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "MD1")) ")" ))) & (Bool (Set (Var "MD1")) ($#r1_integra1 :::"<="::: ) (Set (Var "MD2"))) & (Bool (Set (Var "MD1")) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_6 :::"mid"::: ) "(" (Set (Var "D1")) "," (Set (Var "i")) "," (Set (Var "j")) ")" )) & (Bool (Set (Var "MD2")) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_6 :::"mid"::: ) "(" (Set (Var "D2")) "," (Set "(" ($#k13_integra1 :::"indx"::: ) "(" (Set (Var "D2")) "," (Set (Var "D1")) "," (Set (Var "i")) ")" ")" ) "," (Set "(" ($#k13_integra1 :::"indx"::: ) "(" (Set (Var "D2")) "," (Set (Var "D1")) "," (Set (Var "j")) ")" ")" ) ")" )) ")" ))))))) ; theorem :: INTEGRA3:16 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_measure5 :::"closed_interval"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "D")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "D"))))) "holds" (Bool "(" (Bool (Set (Set (Var "D")) ($#k1_seq_1 :::"."::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "x"))) & (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "D")) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "D")) ")" ))) ")" )))) ; theorem :: INTEGRA3:17 (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "p")) "is" ($#v5_valued_0 :::"increasing"::: ) ) & (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Set (Var "k")))) & (Bool (Set (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Set (Var "j"))))) "holds" (Bool (Set (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_rvsum_1 :::"rng"::: ) (Set "(" ($#k3_finseq_6 :::"mid"::: ) "(" (Set (Var "p")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ")" ))))) ; theorem :: INTEGRA3:18 (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_measure5 :::"closed_interval"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "D")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) "is" ($#v1_comseq_2 :::"bounded"::: ) ) & (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "D"))))) "holds" (Bool (Set ($#k5_seq_4 :::"lower_bound"::: ) (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k2_integra1 :::"divset"::: ) "(" (Set (Var "D")) "," (Set (Var "i")) ")" ")" ) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k4_seq_4 :::"upper_bound"::: ) (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "f")) ")" ))))))) ; theorem :: INTEGRA3:19 (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_measure5 :::"closed_interval"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "D")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) "is" ($#v1_comseq_2 :::"bounded"::: ) ) & (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "D"))))) "holds" (Bool (Set ($#k4_seq_4 :::"upper_bound"::: ) (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k2_integra1 :::"divset"::: ) "(" (Set (Var "D")) "," (Set (Var "i")) ")" ")" ) ")" ) ")" )) ($#r1_xxreal_0 :::">="::: ) (Set ($#k5_seq_4 :::"lower_bound"::: ) (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "f")) ")" ))))))) ; begin theorem :: INTEGRA3:20 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_measure5 :::"closed_interval"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"DivSequence":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) "is" ($#v1_comseq_2 :::"bounded"::: ) ) & (Bool (Set ($#k2_integra3 :::"delta"::: ) (Set (Var "T"))) "is" (Set ($#k6_numbers :::"0"::: ) ) ($#v1_fdiff_1 :::"-convergent"::: ) ) & (Bool (Set ($#k2_integra3 :::"delta"::: ) (Set (Var "T"))) "is" ($#v2_relat_1 :::"non-zero"::: ) ) & (Bool (Set ($#k3_integra1 :::"vol"::: ) (Set (Var "A"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k4_integra2 :::"lower_sum"::: ) "(" (Set (Var "f")) "," (Set (Var "T")) ")" ) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set "(" ($#k4_integra2 :::"lower_sum"::: ) "(" (Set (Var "f")) "," (Set (Var "T")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k11_integra1 :::"lower_integral"::: ) (Set (Var "f")))) ")" )))) ; theorem :: INTEGRA3:21 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_measure5 :::"closed_interval"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"DivSequence":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) "is" ($#v1_comseq_2 :::"bounded"::: ) ) & (Bool (Set ($#k2_integra3 :::"delta"::: ) (Set (Var "T"))) "is" (Set ($#k6_numbers :::"0"::: ) ) ($#v1_fdiff_1 :::"-convergent"::: ) ) & (Bool (Set ($#k2_integra3 :::"delta"::: ) (Set (Var "T"))) "is" ($#v2_relat_1 :::"non-zero"::: ) ) & (Bool (Set ($#k3_integra1 :::"vol"::: ) (Set (Var "A"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k3_integra2 :::"upper_sum"::: ) "(" (Set (Var "f")) "," (Set (Var "T")) ")" ) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set "(" ($#k3_integra2 :::"upper_sum"::: ) "(" (Set (Var "f")) "," (Set (Var "T")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k10_integra1 :::"upper_integral"::: ) (Set (Var "f")))) ")" )))) ;