:: HOLDER_1 semantic presentation begin registrationlet "x" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k2_limfunc1 :::"right_closed_halfline"::: ) "x") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: HOLDER_1:1 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "p"))) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "q")))) "holds" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "a")))) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k4_power :::"to_power"::: ) (Set (Var "p")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k4_power :::"to_power"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k4_power :::"to_power"::: ) (Set "(" (Set (Var "p")) ($#k7_real_1 :::"+"::: ) (Set (Var "q")) ")" ))))) ; theorem :: HOLDER_1:2 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "p"))) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "q")))) "holds" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "a")))) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k4_power :::"to_power"::: ) (Set (Var "p")) ")" ) ($#k4_power :::"to_power"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k4_power :::"to_power"::: ) (Set "(" (Set (Var "p")) ($#k8_real_1 :::"*"::: ) (Set (Var "q")) ")" ))))) ; theorem :: HOLDER_1:3 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "p")))) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "a"))) & (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b")))) "holds" (Bool (Set (Set (Var "a")) ($#k4_power :::"to_power"::: ) (Set (Var "p"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "b")) ($#k4_power :::"to_power"::: ) (Set (Var "p")))))) ; theorem :: HOLDER_1:4 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "p"))) & (Bool (Set (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "p")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "a"))) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "b")))) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k8_real_1 :::"*"::: ) (Set (Var "b"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set "(" (Set (Var "a")) ($#k10_prepower :::"#R"::: ) (Set (Var "p")) ")" ) ($#k10_real_1 :::"/"::: ) (Set (Var "p")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "b")) ($#k10_prepower :::"#R"::: ) (Set (Var "q")) ")" ) ($#k10_real_1 :::"/"::: ) (Set (Var "q")) ")" ))) & "(" (Bool (Bool (Set (Set (Var "a")) ($#k8_real_1 :::"*"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "a")) ($#k10_prepower :::"#R"::: ) (Set (Var "p")) ")" ) ($#k10_real_1 :::"/"::: ) (Set (Var "p")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "b")) ($#k10_prepower :::"#R"::: ) (Set (Var "q")) ")" ) ($#k10_real_1 :::"/"::: ) (Set (Var "q")) ")" )))) "implies" (Bool (Set (Set (Var "a")) ($#k10_prepower :::"#R"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k10_prepower :::"#R"::: ) (Set (Var "q")))) ")" & "(" (Bool (Bool (Set (Set (Var "a")) ($#k10_prepower :::"#R"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k10_prepower :::"#R"::: ) (Set (Var "q"))))) "implies" (Bool (Set (Set (Var "a")) ($#k8_real_1 :::"*"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "a")) ($#k10_prepower :::"#R"::: ) (Set (Var "p")) ")" ) ($#k10_real_1 :::"/"::: ) (Set (Var "p")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "b")) ($#k10_prepower :::"#R"::: ) (Set (Var "q")) ")" ) ($#k10_real_1 :::"/"::: ) (Set (Var "q")) ")" ))) ")" ")" )) ; theorem :: HOLDER_1:5 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "p"))) & (Bool (Set (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "p")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "a"))) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b")))) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k8_real_1 :::"*"::: ) (Set (Var "b"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set "(" (Set (Var "a")) ($#k4_power :::"to_power"::: ) (Set (Var "p")) ")" ) ($#k10_real_1 :::"/"::: ) (Set (Var "p")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "b")) ($#k4_power :::"to_power"::: ) (Set (Var "q")) ")" ) ($#k10_real_1 :::"/"::: ) (Set (Var "q")) ")" ))) & "(" (Bool (Bool (Set (Set (Var "a")) ($#k8_real_1 :::"*"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "a")) ($#k4_power :::"to_power"::: ) (Set (Var "p")) ")" ) ($#k10_real_1 :::"/"::: ) (Set (Var "p")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "b")) ($#k4_power :::"to_power"::: ) (Set (Var "q")) ")" ) ($#k10_real_1 :::"/"::: ) (Set (Var "q")) ")" )))) "implies" (Bool (Set (Set (Var "a")) ($#k4_power :::"to_power"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k4_power :::"to_power"::: ) (Set (Var "q")))) ")" & "(" (Bool (Bool (Set (Set (Var "a")) ($#k4_power :::"to_power"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k4_power :::"to_power"::: ) (Set (Var "q"))))) "implies" (Bool (Set (Set (Var "a")) ($#k8_real_1 :::"*"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "a")) ($#k4_power :::"to_power"::: ) (Set (Var "p")) ")" ) ($#k10_real_1 :::"/"::: ) (Set (Var "p")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "b")) ($#k4_power :::"to_power"::: ) (Set (Var "q")) ")" ) ($#k10_real_1 :::"/"::: ) (Set (Var "q")) ")" ))) ")" ")" )) ; begin theorem :: HOLDER_1:6 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "p"))) & (Bool (Set (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "p")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "ap")) "," (Set (Var "bq")) "," (Set (Var "ab")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "ap")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k18_complex1 :::"abs"::: ) (Set "(" (Set (Var "a")) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" ) ")" ) ($#k4_power :::"to_power"::: ) (Set (Var "p")))) & (Bool (Set (Set (Var "bq")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k18_complex1 :::"abs"::: ) (Set "(" (Set (Var "b")) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" ) ")" ) ($#k4_power :::"to_power"::: ) (Set (Var "q")))) & (Bool (Set (Set (Var "ab")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" ) ")" ))) ")" ) ")" )) "holds" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set (Var "ab")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set (Var "ap")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k4_power :::"to_power"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "p")) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set (Var "bq")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k4_power :::"to_power"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "q")) ")" ) ")" )))))) ; theorem :: HOLDER_1:7 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "p")))) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "ab")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "ap")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k18_complex1 :::"abs"::: ) (Set "(" (Set (Var "a")) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" ) ")" ) ($#k4_power :::"to_power"::: ) (Set (Var "p")))) & (Bool (Set (Set (Var "bp")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k18_complex1 :::"abs"::: ) (Set "(" (Set (Var "b")) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" ) ")" ) ($#k4_power :::"to_power"::: ) (Set (Var "p")))) & (Bool (Set (Set (Var "ab")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" ) ")" ) ")" ) ($#k4_power :::"to_power"::: ) (Set (Var "p")))) ")" ) ")" )) "holds" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set (Var "ab")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k4_power :::"to_power"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "p")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set (Var "ap")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k4_power :::"to_power"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "p")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set (Var "bp")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k4_power :::"to_power"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "p")) ")" ) ")" )))))) ; theorem :: HOLDER_1:8 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "a")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "b")) ($#k1_seq_1 :::"."::: ) (Set (Var "n")))) ")" ) & (Bool (Set (Var "b")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set (Var "a")) "is" bbbadV7_VALUED_0())) "holds" (Bool "(" (Bool (Set (Var "a")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k2_seq_2 :::"lim"::: ) (Set (Var "b")))) ")" )) ; theorem :: HOLDER_1:9 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "a")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set (Var "b")) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "c")) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" ))) ")" ) & (Bool (Set (Var "b")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set (Var "c")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set (Var "a")) "is" bbbadV7_VALUED_0())) "holds" (Bool "(" (Bool (Set (Var "a")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k2_seq_2 :::"lim"::: ) (Set (Var "b")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k2_seq_2 :::"lim"::: ) (Set (Var "c")) ")" ))) ")" )) ; theorem :: HOLDER_1:10 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "p")))) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "ap")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "a")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "a")) ($#k1_seq_1 :::"."::: ) (Set (Var "n")))) ")" ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "ap")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k4_power :::"to_power"::: ) (Set (Var "p")))) ")" )) "holds" (Bool "(" (Bool (Set (Var "ap")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set (Var "ap"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_seq_2 :::"lim"::: ) (Set (Var "a")) ")" ) ($#k4_power :::"to_power"::: ) (Set (Var "p")))) ")" ))) ; theorem :: HOLDER_1:11 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "p")))) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "ap")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "a")) "is" ($#v1_series_1 :::"summable"::: ) ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "a")) ($#k1_seq_1 :::"."::: ) (Set (Var "n")))) ")" ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "ap")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set (Var "a")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k4_power :::"to_power"::: ) (Set (Var "p")))) ")" )) "holds" (Bool "(" (Bool (Set (Var "ap")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set (Var "ap"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_series_1 :::"Sum"::: ) (Set (Var "a")) ")" ) ($#k4_power :::"to_power"::: ) (Set (Var "p")))) & (Bool (Set (Var "ap")) "is" bbbadV7_VALUED_0()) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "ap")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k4_series_1 :::"Sum"::: ) (Set (Var "a")) ")" ) ($#k4_power :::"to_power"::: ) (Set (Var "p")))) ")" ) ")" ))) ; theorem :: HOLDER_1:12 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "p"))) & (Bool (Set (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "p")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "ap")) "," (Set (Var "bq")) "," (Set (Var "ab")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "ap")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k18_complex1 :::"abs"::: ) (Set "(" (Set (Var "a")) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" ) ")" ) ($#k4_power :::"to_power"::: ) (Set (Var "p")))) & (Bool (Set (Set (Var "bq")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k18_complex1 :::"abs"::: ) (Set "(" (Set (Var "b")) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" ) ")" ) ($#k4_power :::"to_power"::: ) (Set (Var "q")))) & (Bool (Set (Set (Var "ab")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" ) ")" ))) ")" ) ")" ) & (Bool (Set (Var "ap")) "is" ($#v1_series_1 :::"summable"::: ) ) & (Bool (Set (Var "bq")) "is" ($#v1_series_1 :::"summable"::: ) )) "holds" (Bool "(" (Bool (Set (Var "ab")) "is" ($#v1_series_1 :::"summable"::: ) ) & (Bool (Set ($#k4_series_1 :::"Sum"::: ) (Set (Var "ab"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set "(" ($#k4_series_1 :::"Sum"::: ) (Set (Var "ap")) ")" ) ($#k4_power :::"to_power"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "p")) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k4_series_1 :::"Sum"::: ) (Set (Var "bq")) ")" ) ($#k4_power :::"to_power"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "q")) ")" ) ")" ))) ")" ))) ; theorem :: HOLDER_1:13 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "p")))) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "ab")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "ap")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k18_complex1 :::"abs"::: ) (Set "(" (Set (Var "a")) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" ) ")" ) ($#k4_power :::"to_power"::: ) (Set (Var "p")))) & (Bool (Set (Set (Var "bp")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k18_complex1 :::"abs"::: ) (Set "(" (Set (Var "b")) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" ) ")" ) ($#k4_power :::"to_power"::: ) (Set (Var "p")))) & (Bool (Set (Set (Var "ab")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" ) ")" ) ")" ) ($#k4_power :::"to_power"::: ) (Set (Var "p")))) ")" ) ")" ) & (Bool (Set (Var "ap")) "is" ($#v1_series_1 :::"summable"::: ) ) & (Bool (Set (Var "bp")) "is" ($#v1_series_1 :::"summable"::: ) )) "holds" (Bool "(" (Bool (Set (Var "ab")) "is" ($#v1_series_1 :::"summable"::: ) ) & (Bool (Set (Set "(" ($#k4_series_1 :::"Sum"::: ) (Set (Var "ab")) ")" ) ($#k4_power :::"to_power"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "p")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set "(" ($#k4_series_1 :::"Sum"::: ) (Set (Var "ap")) ")" ) ($#k4_power :::"to_power"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "p")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k4_series_1 :::"Sum"::: ) (Set (Var "bp")) ")" ) ($#k4_power :::"to_power"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "p")) ")" ) ")" ))) ")" ))) ;