:: FDIFF_1 semantic presentation begin theorem :: FDIFF_1:1 (Bool "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) "iff" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) ")" ) ")" ) "iff" (Bool (Set (Var "Y")) ($#r1_hidden :::"="::: ) (Set ($#k1_numbers :::"REAL"::: ) )) ")" )) ; definitionlet "x" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; let "IT" be ($#m1_subset_1 :::"Real_Sequence":::); attr "IT" is "x" :::"-convergent"::: means :: FDIFF_1:def 1 (Bool "(" (Bool "IT" "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) "IT") ($#r1_hidden :::"="::: ) "x") ")" ); end; :: deftheorem defines :::"-convergent"::: FDIFF_1:def 1 : (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" (Set (Var "x")) ($#v1_fdiff_1 :::"-convergent"::: ) ) "iff" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set (Var "IT"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" ) ")" ))); registration cluster bbbadV1_RELAT_1() ($#v2_relat_1 :::"non-zero"::: ) bbbadV4_RELAT_1((Set ($#k5_numbers :::"NAT"::: ) )) bbbadV5_RELAT_1((Set ($#k1_numbers :::"REAL"::: ) )) bbbadV1_FUNCT_1() ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_partfun1 :::"total"::: ) ($#v1_funct_2 :::"quasi_total"::: ) ($#v1_valued_0 :::"complex-valued"::: ) ($#v2_valued_0 :::"ext-real-valued"::: ) ($#v3_valued_0 :::"real-valued"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#v1_fdiff_1 :::"-convergent"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ))))); end; registrationlet "f" be (Set ($#k6_numbers :::"0"::: ) ) ($#v1_fdiff_1 :::"-convergent"::: ) ($#m1_subset_1 :::"Real_Sequence":::); cluster (Set ($#k1_seq_2 :::"lim"::: ) "f") -> ($#v1_xboole_0 :::"empty"::: ) ; end; registration cluster bbbadV1_FUNCT_1() ($#v1_funct_2 :::"quasi_total"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#v1_fdiff_1 :::"-convergent"::: ) -> ($#v2_comseq_2 :::"convergent"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ))))); end; definitionlet "IT" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); attr "IT" is :::"RestFunc-like"::: means :: FDIFF_1:def 2 (Bool "(" (Bool "IT" "is" ($#v1_partfun1 :::"total"::: ) ) & (Bool "(" "for" (Set (Var "h")) "being" ($#v2_relat_1 :::"non-zero"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#v1_fdiff_1 :::"-convergent"::: ) ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "h")) ($#k37_valued_1 :::"""::: ) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set "(" "IT" ($#k8_funct_2 :::"/*"::: ) (Set (Var "h")) ")" )) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set "(" (Set "(" (Set (Var "h")) ($#k37_valued_1 :::"""::: ) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set "(" "IT" ($#k8_funct_2 :::"/*"::: ) (Set (Var "h")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" ) ")" ); end; :: deftheorem defines :::"RestFunc-like"::: FDIFF_1:def 2 : (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_fdiff_1 :::"RestFunc-like"::: ) ) "iff" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_partfun1 :::"total"::: ) ) & (Bool "(" "for" (Set (Var "h")) "being" ($#v2_relat_1 :::"non-zero"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#v1_fdiff_1 :::"-convergent"::: ) ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "h")) ($#k37_valued_1 :::"""::: ) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set "(" (Set (Var "IT")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "h")) ")" )) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set "(" (Set "(" (Set (Var "h")) ($#k37_valued_1 :::"""::: ) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set "(" (Set (Var "IT")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "h")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" ) ")" ) ")" )); registration cluster bbbadV1_RELAT_1() bbbadV4_RELAT_1((Set ($#k1_numbers :::"REAL"::: ) )) bbbadV5_RELAT_1((Set ($#k1_numbers :::"REAL"::: ) )) bbbadV1_FUNCT_1() ($#v1_valued_0 :::"complex-valued"::: ) ($#v2_valued_0 :::"ext-real-valued"::: ) ($#v3_valued_0 :::"real-valued"::: ) ($#v2_fdiff_1 :::"RestFunc-like"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ))))); end; definitionmode RestFunc is ($#v2_fdiff_1 :::"RestFunc-like"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); end; definitionlet "IT" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); attr "IT" is :::"linear"::: means :: FDIFF_1:def 3 (Bool "(" (Bool "IT" "is" ($#v1_partfun1 :::"total"::: ) ) & (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set "IT" ($#k1_seq_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set (Var "p")))))) ")" ); end; :: deftheorem defines :::"linear"::: FDIFF_1:def 3 : (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v3_fdiff_1 :::"linear"::: ) ) "iff" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_partfun1 :::"total"::: ) ) & (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set (Var "IT")) ($#k1_seq_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set (Var "p")))))) ")" ) ")" )); registration cluster bbbadV1_RELAT_1() bbbadV4_RELAT_1((Set ($#k1_numbers :::"REAL"::: ) )) bbbadV5_RELAT_1((Set ($#k1_numbers :::"REAL"::: ) )) bbbadV1_FUNCT_1() ($#v1_valued_0 :::"complex-valued"::: ) ($#v2_valued_0 :::"ext-real-valued"::: ) ($#v3_valued_0 :::"real-valued"::: ) ($#v3_fdiff_1 :::"linear"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ))))); end; definitionmode LinearFunc is ($#v3_fdiff_1 :::"linear"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); end; theorem :: FDIFF_1:2 (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m1_subset_1 :::"LinearFunc":::) "holds" (Bool "(" (Bool (Set (Set (Var "L1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "L2"))) "is" ($#m1_subset_1 :::"LinearFunc":::)) & (Bool (Set (Set (Var "L1")) ($#k47_valued_1 :::"-"::: ) (Set (Var "L2"))) "is" ($#m1_subset_1 :::"LinearFunc":::)) ")" )) ; theorem :: FDIFF_1:3 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"LinearFunc":::) "holds" (Bool (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "L"))) "is" ($#m1_subset_1 :::"LinearFunc":::)))) ; theorem :: FDIFF_1:4 (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#m1_subset_1 :::"RestFunc":::) "holds" (Bool "(" (Bool (Set (Set (Var "R1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "R2"))) "is" ($#m1_subset_1 :::"RestFunc":::)) & (Bool (Set (Set (Var "R1")) ($#k47_valued_1 :::"-"::: ) (Set (Var "R2"))) "is" ($#m1_subset_1 :::"RestFunc":::)) & (Bool (Set (Set (Var "R1")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "R2"))) "is" ($#m1_subset_1 :::"RestFunc":::)) ")" )) ; theorem :: FDIFF_1:5 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"RestFunc":::) "holds" (Bool (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "R"))) "is" ($#m1_subset_1 :::"RestFunc":::)))) ; theorem :: FDIFF_1:6 (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m1_subset_1 :::"LinearFunc":::) "holds" (Bool (Set (Set (Var "L1")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "L2"))) "is" ($#v2_fdiff_1 :::"RestFunc-like"::: ) )) ; theorem :: FDIFF_1:7 (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"RestFunc":::) (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"LinearFunc":::) "holds" (Bool "(" (Bool (Set (Set (Var "R")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "L"))) "is" ($#m1_subset_1 :::"RestFunc":::)) & (Bool (Set (Set (Var "L")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "R"))) "is" ($#m1_subset_1 :::"RestFunc":::)) ")" ))) ; definitionlet "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "x0" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; pred "f" :::"is_differentiable_in"::: "x0" means :: FDIFF_1:def 4 (Bool "ex" (Set (Var "N")) "being" ($#m1_rcomp_1 :::"Neighbourhood"::: ) "of" "x0" "st" (Bool "(" (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) "f")) & (Bool "ex" (Set (Var "L")) "being" ($#m1_subset_1 :::"LinearFunc":::)(Bool "ex" (Set (Var "R")) "being" ($#m1_subset_1 :::"RestFunc":::) "st" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "N")))) "holds" (Bool (Set (Set "(" "f" ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" "f" ($#k1_seq_1 :::"."::: ) "x0" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "L")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) "x0" ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "R")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) "x0" ")" ) ")" )))))) ")" )); end; :: deftheorem defines :::"is_differentiable_in"::: FDIFF_1:def 4 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "x0")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "x0"))) "iff" (Bool "ex" (Set (Var "N")) "being" ($#m1_rcomp_1 :::"Neighbourhood"::: ) "of" (Set (Var "x0")) "st" (Bool "(" (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool "ex" (Set (Var "L")) "being" ($#m1_subset_1 :::"LinearFunc":::)(Bool "ex" (Set (Var "R")) "being" ($#m1_subset_1 :::"RestFunc":::) "st" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "N")))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x0")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "L")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set (Var "x0")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "R")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set (Var "x0")) ")" ) ")" )))))) ")" )) ")" ))); definitionlet "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "x0" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; assume (Bool (Set (Const "f")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Const "x0"))) ; func :::"diff"::: "(" "f" "," "x0" ")" -> ($#m1_subset_1 :::"Real":::) means :: FDIFF_1:def 5 (Bool "ex" (Set (Var "N")) "being" ($#m1_rcomp_1 :::"Neighbourhood"::: ) "of" "x0" "st" (Bool "(" (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) "f")) & (Bool "ex" (Set (Var "L")) "being" ($#m1_subset_1 :::"LinearFunc":::)(Bool "ex" (Set (Var "R")) "being" ($#m1_subset_1 :::"RestFunc":::) "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "L")) ($#k1_seq_1 :::"."::: ) (Num 1))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "N")))) "holds" (Bool (Set (Set "(" "f" ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" "f" ($#k1_seq_1 :::"."::: ) "x0" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "L")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) "x0" ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "R")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) "x0" ")" ) ")" ))) ")" ) ")" ))) ")" )); end; :: deftheorem defines :::"diff"::: FDIFF_1:def 5 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "x0")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "f")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "x0")))) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f")) "," (Set (Var "x0")) ")" )) "iff" (Bool "ex" (Set (Var "N")) "being" ($#m1_rcomp_1 :::"Neighbourhood"::: ) "of" (Set (Var "x0")) "st" (Bool "(" (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool "ex" (Set (Var "L")) "being" ($#m1_subset_1 :::"LinearFunc":::)(Bool "ex" (Set (Var "R")) "being" ($#m1_subset_1 :::"RestFunc":::) "st" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "L")) ($#k1_seq_1 :::"."::: ) (Num 1))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "N")))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x0")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "L")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set (Var "x0")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "R")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set (Var "x0")) ")" ) ")" ))) ")" ) ")" ))) ")" )) ")" )))); definitionlet "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "X" be ($#m1_hidden :::"set"::: ) ; pred "f" :::"is_differentiable_on"::: "X" means :: FDIFF_1:def 6 (Bool "(" (Bool "X" ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) "f")) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "X")) "holds" (Bool (Set "f" ($#k2_partfun1 :::"|"::: ) "X") ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "x"))) ")" ) ")" ); end; :: deftheorem defines :::"is_differentiable_on"::: FDIFF_1:def 6 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "X"))) "iff" (Bool "(" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "x"))) ")" ) ")" ) ")" ))); theorem :: FDIFF_1:8 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "X")) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) )))) ; theorem :: FDIFF_1:9 (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) "iff" (Bool "(" (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Var "f")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "x"))) ")" ) ")" ) ")" ))) ; theorem :: FDIFF_1:10 (Bool "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Y")))) "holds" (Bool (Set (Var "Y")) "is" ($#v3_rcomp_1 :::"open"::: ) ))) ; definitionlet "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "X" be ($#m1_hidden :::"set"::: ) ; assume (Bool (Set (Const "f")) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Const "X"))) ; func "f" :::"`|"::: "X" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: FDIFF_1:def 7 (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) "X") & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "X")) "holds" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_fdiff_1 :::"diff"::: ) "(" "f" "," (Set (Var "x")) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"`|"::: FDIFF_1:def 7 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "f")) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "X")))) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "X")))) "iff" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set (Var "X"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) ")" )) ")" ) ")" ) ")" )))); theorem :: FDIFF_1:11 (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "r")) ($#k1_tarski :::"}"::: ) )))) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" ))) ; registrationlet "h" be ($#v2_relat_1 :::"non-zero"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#v1_fdiff_1 :::"-convergent"::: ) ($#m1_subset_1 :::"Real_Sequence":::); let "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set "h" ($#k9_nat_1 :::"^\"::: ) "n") -> ($#v2_relat_1 :::"non-zero"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#v1_fdiff_1 :::"-convergent"::: ) for ($#m1_subset_1 :::"Real_Sequence":::); end; theorem :: FDIFF_1:12 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "x0")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "N")) "being" ($#m1_rcomp_1 :::"Neighbourhood"::: ) "of" (Set (Var "x0")) "st" (Bool (Bool (Set (Var "f")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "x0"))) & (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool "for" (Set (Var "h")) "being" ($#v2_relat_1 :::"non-zero"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#v1_fdiff_1 :::"-convergent"::: ) ($#m1_subset_1 :::"Real_Sequence":::) (Bool "for" (Set (Var "c")) "being" bbbadV3_FUNCT_1() ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x0")) ($#k1_tarski :::"}"::: ) )) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set (Var "h")) ($#k3_valued_1 :::"+"::: ) (Set (Var "c")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "N")))) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "h")) ($#k37_valued_1 :::"""::: ) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k8_funct_2 :::"/*"::: ) (Set "(" (Set (Var "h")) ($#k3_valued_1 :::"+"::: ) (Set (Var "c")) ")" ) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "c")) ")" ) ")" )) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f")) "," (Set (Var "x0")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_seq_2 :::"lim"::: ) (Set "(" (Set "(" (Set (Var "h")) ($#k37_valued_1 :::"""::: ) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k8_funct_2 :::"/*"::: ) (Set "(" (Set (Var "h")) ($#k3_valued_1 :::"+"::: ) (Set (Var "c")) ")" ) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "c")) ")" ) ")" ) ")" ))) ")" )))))) ; theorem :: FDIFF_1:13 (Bool "for" (Set (Var "x0")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f1")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "x0"))) & (Bool (Set (Var "f2")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "x0")))) "holds" (Bool "(" (Bool (Set (Set (Var "f1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "f2"))) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "x0"))) & (Bool (Set ($#k1_fdiff_1 :::"diff"::: ) "(" (Set "(" (Set (Var "f1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "f2")) ")" ) "," (Set (Var "x0")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f1")) "," (Set (Var "x0")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f2")) "," (Set (Var "x0")) ")" ")" ))) ")" ))) ; theorem :: FDIFF_1:14 (Bool "for" (Set (Var "x0")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f1")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "x0"))) & (Bool (Set (Var "f2")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "x0")))) "holds" (Bool "(" (Bool (Set (Set (Var "f1")) ($#k47_valued_1 :::"-"::: ) (Set (Var "f2"))) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "x0"))) & (Bool (Set ($#k1_fdiff_1 :::"diff"::: ) "(" (Set "(" (Set (Var "f1")) ($#k47_valued_1 :::"-"::: ) (Set (Var "f2")) ")" ) "," (Set (Var "x0")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f1")) "," (Set (Var "x0")) ")" ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f2")) "," (Set (Var "x0")) ")" ")" ))) ")" ))) ; theorem :: FDIFF_1:15 (Bool "for" (Set (Var "x0")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "x0")))) "holds" (Bool "(" (Bool (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f"))) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "x0"))) & (Bool (Set ($#k1_fdiff_1 :::"diff"::: ) "(" (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f")) ")" ) "," (Set (Var "x0")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f")) "," (Set (Var "x0")) ")" ")" ))) ")" ))) ; theorem :: FDIFF_1:16 (Bool "for" (Set (Var "x0")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f1")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "x0"))) & (Bool (Set (Var "f2")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "x0")))) "holds" (Bool "(" (Bool (Set (Set (Var "f1")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "f2"))) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "x0"))) & (Bool (Set ($#k1_fdiff_1 :::"diff"::: ) "(" (Set "(" (Set (Var "f1")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "f2")) ")" ) "," (Set (Var "x0")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "f2")) ($#k1_seq_1 :::"."::: ) (Set (Var "x0")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f1")) "," (Set (Var "x0")) ")" ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "x0")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f2")) "," (Set (Var "x0")) ")" ")" ) ")" ))) ")" ))) ; theorem :: FDIFF_1:17 (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Z"))) ($#r2_relset_1 :::"="::: ) (Set ($#k1_partfun2 :::"id"::: ) (Set (Var "Z"))))) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 1)) ")" ) ")" ))) ; theorem :: FDIFF_1:18 (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "f2")) ")" ))) & (Bool (Set (Var "f1")) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool (Set (Var "f2")) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z")))) "holds" (Bool "(" (Bool (Set (Set (Var "f1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "f2"))) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "f1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "f2")) ")" ) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f1")) "," (Set (Var "x")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f2")) "," (Set (Var "x")) ")" ")" ))) ")" ) ")" ))) ; theorem :: FDIFF_1:19 (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f1")) ($#k47_valued_1 :::"-"::: ) (Set (Var "f2")) ")" ))) & (Bool (Set (Var "f1")) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool (Set (Var "f2")) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z")))) "holds" (Bool "(" (Bool (Set (Set (Var "f1")) ($#k47_valued_1 :::"-"::: ) (Set (Var "f2"))) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "f1")) ($#k47_valued_1 :::"-"::: ) (Set (Var "f2")) ")" ) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f1")) "," (Set (Var "x")) ")" ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f2")) "," (Set (Var "x")) ")" ")" ))) ")" ) ")" ))) ; theorem :: FDIFF_1:20 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f")) ")" ))) & (Bool (Set (Var "f")) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z")))) "holds" (Bool "(" (Bool (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f"))) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f")) ")" ) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) ")" ")" ))) ")" ) ")" )))) ; theorem :: FDIFF_1:21 (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f1")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "f2")) ")" ))) & (Bool (Set (Var "f1")) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool (Set (Var "f2")) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z")))) "holds" (Bool "(" (Bool (Set (Set (Var "f1")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "f2"))) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "f1")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "f2")) ")" ) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "f2")) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f1")) "," (Set (Var "x")) ")" ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f2")) "," (Set (Var "x")) ")" ")" ) ")" ))) ")" ) ")" ))) ; theorem :: FDIFF_1:22 (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Z"))) "is" bbbadV3_FUNCT_1())) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" ))) ; theorem :: FDIFF_1:23 (Bool "for" (Set (Var "r")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k7_real_1 :::"+"::: ) (Set (Var "p")))) ")" )) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "r"))) ")" ) ")" )))) ; theorem :: FDIFF_1:24 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "x0")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "f")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "x0")))) "holds" (Bool (Set (Var "f")) ($#r1_fcont_1 :::"is_continuous_in"::: ) (Set (Var "x0"))))) ; theorem :: FDIFF_1:25 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) "is" ($#v1_fcont_1 :::"continuous"::: ) ))) ; theorem :: FDIFF_1:26 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "X"))) & (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "f")) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z")))))) ; theorem :: FDIFF_1:27 (Bool "ex" (Set (Var "R")) "being" ($#m1_subset_1 :::"RestFunc":::) "st" (Bool "(" (Bool (Set (Set (Var "R")) ($#k1_seq_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "R")) ($#r1_fcont_1 :::"is_continuous_in"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ; definitionlet "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); attr "f" is :::"differentiable"::: means :: FDIFF_1:def 8 (Bool "f" ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "f")); end; :: deftheorem defines :::"differentiable"::: FDIFF_1:def 8 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v4_fdiff_1 :::"differentiable"::: ) ) "iff" (Bool (Set (Var "f")) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) ")" )); registration cluster bbbadV1_RELAT_1() bbbadV4_RELAT_1((Set ($#k1_numbers :::"REAL"::: ) )) bbbadV5_RELAT_1((Set ($#k1_numbers :::"REAL"::: ) )) bbbadV1_FUNCT_1() ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_partfun1 :::"total"::: ) ($#v1_funct_2 :::"quasi_total"::: ) ($#v1_valued_0 :::"complex-valued"::: ) ($#v2_valued_0 :::"ext-real-valued"::: ) ($#v3_valued_0 :::"real-valued"::: ) ($#v4_fdiff_1 :::"differentiable"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ))))); end; theorem :: FDIFF_1:28 (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#v4_fdiff_1 :::"differentiable"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Var "f")) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))))) ;