MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dvntaylp Structured version   Visualization version   GIF version

Theorem dvntaylp 25746
Description: The 𝑀-th derivative of the Taylor polynomial is the Taylor polynomial of the 𝑀-th derivative of the function. (Contributed by Mario Carneiro, 1-Jan-2017.)
Hypotheses
Ref Expression
dvntaylp.s (πœ‘ β†’ 𝑆 ∈ {ℝ, β„‚})
dvntaylp.f (πœ‘ β†’ 𝐹:π΄βŸΆβ„‚)
dvntaylp.a (πœ‘ β†’ 𝐴 βŠ† 𝑆)
dvntaylp.m (πœ‘ β†’ 𝑀 ∈ β„•0)
dvntaylp.n (πœ‘ β†’ 𝑁 ∈ β„•0)
dvntaylp.b (πœ‘ β†’ 𝐡 ∈ dom ((𝑆 D𝑛 𝐹)β€˜(𝑁 + 𝑀)))
Assertion
Ref Expression
dvntaylp (πœ‘ β†’ ((β„‚ D𝑛 ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐡))β€˜π‘€) = (𝑁(𝑆 Tayl ((𝑆 D𝑛 𝐹)β€˜π‘€))𝐡))

Proof of Theorem dvntaylp
Dummy variables π‘š 𝑛 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dvntaylp.m . . . . 5 (πœ‘ β†’ 𝑀 ∈ β„•0)
2 nn0uz 12812 . . . . 5 β„•0 = (β„€β‰₯β€˜0)
31, 2eleqtrdi 2848 . . . 4 (πœ‘ β†’ 𝑀 ∈ (β„€β‰₯β€˜0))
4 eluzfz2b 13457 . . . 4 (𝑀 ∈ (β„€β‰₯β€˜0) ↔ 𝑀 ∈ (0...𝑀))
53, 4sylib 217 . . 3 (πœ‘ β†’ 𝑀 ∈ (0...𝑀))
6 fveq2 6847 . . . . . 6 (π‘š = 0 β†’ ((β„‚ D𝑛 ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐡))β€˜π‘š) = ((β„‚ D𝑛 ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐡))β€˜0))
7 fveq2 6847 . . . . . . . 8 (π‘š = 0 β†’ ((𝑆 D𝑛 𝐹)β€˜π‘š) = ((𝑆 D𝑛 𝐹)β€˜0))
87oveq2d 7378 . . . . . . 7 (π‘š = 0 β†’ (𝑆 Tayl ((𝑆 D𝑛 𝐹)β€˜π‘š)) = (𝑆 Tayl ((𝑆 D𝑛 𝐹)β€˜0)))
9 oveq2 7370 . . . . . . . 8 (π‘š = 0 β†’ (𝑀 βˆ’ π‘š) = (𝑀 βˆ’ 0))
109oveq2d 7378 . . . . . . 7 (π‘š = 0 β†’ (𝑁 + (𝑀 βˆ’ π‘š)) = (𝑁 + (𝑀 βˆ’ 0)))
11 eqidd 2738 . . . . . . 7 (π‘š = 0 β†’ 𝐡 = 𝐡)
128, 10, 11oveq123d 7383 . . . . . 6 (π‘š = 0 β†’ ((𝑁 + (𝑀 βˆ’ π‘š))(𝑆 Tayl ((𝑆 D𝑛 𝐹)β€˜π‘š))𝐡) = ((𝑁 + (𝑀 βˆ’ 0))(𝑆 Tayl ((𝑆 D𝑛 𝐹)β€˜0))𝐡))
136, 12eqeq12d 2753 . . . . 5 (π‘š = 0 β†’ (((β„‚ D𝑛 ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐡))β€˜π‘š) = ((𝑁 + (𝑀 βˆ’ π‘š))(𝑆 Tayl ((𝑆 D𝑛 𝐹)β€˜π‘š))𝐡) ↔ ((β„‚ D𝑛 ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐡))β€˜0) = ((𝑁 + (𝑀 βˆ’ 0))(𝑆 Tayl ((𝑆 D𝑛 𝐹)β€˜0))𝐡)))
1413imbi2d 341 . . . 4 (π‘š = 0 β†’ ((πœ‘ β†’ ((β„‚ D𝑛 ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐡))β€˜π‘š) = ((𝑁 + (𝑀 βˆ’ π‘š))(𝑆 Tayl ((𝑆 D𝑛 𝐹)β€˜π‘š))𝐡)) ↔ (πœ‘ β†’ ((β„‚ D𝑛 ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐡))β€˜0) = ((𝑁 + (𝑀 βˆ’ 0))(𝑆 Tayl ((𝑆 D𝑛 𝐹)β€˜0))𝐡))))
15 fveq2 6847 . . . . . 6 (π‘š = 𝑛 β†’ ((β„‚ D𝑛 ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐡))β€˜π‘š) = ((β„‚ D𝑛 ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐡))β€˜π‘›))
16 fveq2 6847 . . . . . . . 8 (π‘š = 𝑛 β†’ ((𝑆 D𝑛 𝐹)β€˜π‘š) = ((𝑆 D𝑛 𝐹)β€˜π‘›))
1716oveq2d 7378 . . . . . . 7 (π‘š = 𝑛 β†’ (𝑆 Tayl ((𝑆 D𝑛 𝐹)β€˜π‘š)) = (𝑆 Tayl ((𝑆 D𝑛 𝐹)β€˜π‘›)))
18 oveq2 7370 . . . . . . . 8 (π‘š = 𝑛 β†’ (𝑀 βˆ’ π‘š) = (𝑀 βˆ’ 𝑛))
1918oveq2d 7378 . . . . . . 7 (π‘š = 𝑛 β†’ (𝑁 + (𝑀 βˆ’ π‘š)) = (𝑁 + (𝑀 βˆ’ 𝑛)))
20 eqidd 2738 . . . . . . 7 (π‘š = 𝑛 β†’ 𝐡 = 𝐡)
2117, 19, 20oveq123d 7383 . . . . . 6 (π‘š = 𝑛 β†’ ((𝑁 + (𝑀 βˆ’ π‘š))(𝑆 Tayl ((𝑆 D𝑛 𝐹)β€˜π‘š))𝐡) = ((𝑁 + (𝑀 βˆ’ 𝑛))(𝑆 Tayl ((𝑆 D𝑛 𝐹)β€˜π‘›))𝐡))
2215, 21eqeq12d 2753 . . . . 5 (π‘š = 𝑛 β†’ (((β„‚ D𝑛 ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐡))β€˜π‘š) = ((𝑁 + (𝑀 βˆ’ π‘š))(𝑆 Tayl ((𝑆 D𝑛 𝐹)β€˜π‘š))𝐡) ↔ ((β„‚ D𝑛 ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐡))β€˜π‘›) = ((𝑁 + (𝑀 βˆ’ 𝑛))(𝑆 Tayl ((𝑆 D𝑛 𝐹)β€˜π‘›))𝐡)))
2322imbi2d 341 . . . 4 (π‘š = 𝑛 β†’ ((πœ‘ β†’ ((β„‚ D𝑛 ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐡))β€˜π‘š) = ((𝑁 + (𝑀 βˆ’ π‘š))(𝑆 Tayl ((𝑆 D𝑛 𝐹)β€˜π‘š))𝐡)) ↔ (πœ‘ β†’ ((β„‚ D𝑛 ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐡))β€˜π‘›) = ((𝑁 + (𝑀 βˆ’ 𝑛))(𝑆 Tayl ((𝑆 D𝑛 𝐹)β€˜π‘›))𝐡))))
24 fveq2 6847 . . . . . 6 (π‘š = (𝑛 + 1) β†’ ((β„‚ D𝑛 ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐡))β€˜π‘š) = ((β„‚ D𝑛 ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐡))β€˜(𝑛 + 1)))
25 fveq2 6847 . . . . . . . 8 (π‘š = (𝑛 + 1) β†’ ((𝑆 D𝑛 𝐹)β€˜π‘š) = ((𝑆 D𝑛 𝐹)β€˜(𝑛 + 1)))
2625oveq2d 7378 . . . . . . 7 (π‘š = (𝑛 + 1) β†’ (𝑆 Tayl ((𝑆 D𝑛 𝐹)β€˜π‘š)) = (𝑆 Tayl ((𝑆 D𝑛 𝐹)β€˜(𝑛 + 1))))
27 oveq2 7370 . . . . . . . 8 (π‘š = (𝑛 + 1) β†’ (𝑀 βˆ’ π‘š) = (𝑀 βˆ’ (𝑛 + 1)))
2827oveq2d 7378 . . . . . . 7 (π‘š = (𝑛 + 1) β†’ (𝑁 + (𝑀 βˆ’ π‘š)) = (𝑁 + (𝑀 βˆ’ (𝑛 + 1))))
29 eqidd 2738 . . . . . . 7 (π‘š = (𝑛 + 1) β†’ 𝐡 = 𝐡)
3026, 28, 29oveq123d 7383 . . . . . 6 (π‘š = (𝑛 + 1) β†’ ((𝑁 + (𝑀 βˆ’ π‘š))(𝑆 Tayl ((𝑆 D𝑛 𝐹)β€˜π‘š))𝐡) = ((𝑁 + (𝑀 βˆ’ (𝑛 + 1)))(𝑆 Tayl ((𝑆 D𝑛 𝐹)β€˜(𝑛 + 1)))𝐡))
3124, 30eqeq12d 2753 . . . . 5 (π‘š = (𝑛 + 1) β†’ (((β„‚ D𝑛 ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐡))β€˜π‘š) = ((𝑁 + (𝑀 βˆ’ π‘š))(𝑆 Tayl ((𝑆 D𝑛 𝐹)β€˜π‘š))𝐡) ↔ ((β„‚ D𝑛 ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐡))β€˜(𝑛 + 1)) = ((𝑁 + (𝑀 βˆ’ (𝑛 + 1)))(𝑆 Tayl ((𝑆 D𝑛 𝐹)β€˜(𝑛 + 1)))𝐡)))
3231imbi2d 341 . . . 4 (π‘š = (𝑛 + 1) β†’ ((πœ‘ β†’ ((β„‚ D𝑛 ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐡))β€˜π‘š) = ((𝑁 + (𝑀 βˆ’ π‘š))(𝑆 Tayl ((𝑆 D𝑛 𝐹)β€˜π‘š))𝐡)) ↔ (πœ‘ β†’ ((β„‚ D𝑛 ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐡))β€˜(𝑛 + 1)) = ((𝑁 + (𝑀 βˆ’ (𝑛 + 1)))(𝑆 Tayl ((𝑆 D𝑛 𝐹)β€˜(𝑛 + 1)))𝐡))))
33 fveq2 6847 . . . . . 6 (π‘š = 𝑀 β†’ ((β„‚ D𝑛 ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐡))β€˜π‘š) = ((β„‚ D𝑛 ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐡))β€˜π‘€))
34 fveq2 6847 . . . . . . . 8 (π‘š = 𝑀 β†’ ((𝑆 D𝑛 𝐹)β€˜π‘š) = ((𝑆 D𝑛 𝐹)β€˜π‘€))
3534oveq2d 7378 . . . . . . 7 (π‘š = 𝑀 β†’ (𝑆 Tayl ((𝑆 D𝑛 𝐹)β€˜π‘š)) = (𝑆 Tayl ((𝑆 D𝑛 𝐹)β€˜π‘€)))
36 oveq2 7370 . . . . . . . 8 (π‘š = 𝑀 β†’ (𝑀 βˆ’ π‘š) = (𝑀 βˆ’ 𝑀))
3736oveq2d 7378 . . . . . . 7 (π‘š = 𝑀 β†’ (𝑁 + (𝑀 βˆ’ π‘š)) = (𝑁 + (𝑀 βˆ’ 𝑀)))
38 eqidd 2738 . . . . . . 7 (π‘š = 𝑀 β†’ 𝐡 = 𝐡)
3935, 37, 38oveq123d 7383 . . . . . 6 (π‘š = 𝑀 β†’ ((𝑁 + (𝑀 βˆ’ π‘š))(𝑆 Tayl ((𝑆 D𝑛 𝐹)β€˜π‘š))𝐡) = ((𝑁 + (𝑀 βˆ’ 𝑀))(𝑆 Tayl ((𝑆 D𝑛 𝐹)β€˜π‘€))𝐡))
4033, 39eqeq12d 2753 . . . . 5 (π‘š = 𝑀 β†’ (((β„‚ D𝑛 ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐡))β€˜π‘š) = ((𝑁 + (𝑀 βˆ’ π‘š))(𝑆 Tayl ((𝑆 D𝑛 𝐹)β€˜π‘š))𝐡) ↔ ((β„‚ D𝑛 ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐡))β€˜π‘€) = ((𝑁 + (𝑀 βˆ’ 𝑀))(𝑆 Tayl ((𝑆 D𝑛 𝐹)β€˜π‘€))𝐡)))
4140imbi2d 341 . . . 4 (π‘š = 𝑀 β†’ ((πœ‘ β†’ ((β„‚ D𝑛 ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐡))β€˜π‘š) = ((𝑁 + (𝑀 βˆ’ π‘š))(𝑆 Tayl ((𝑆 D𝑛 𝐹)β€˜π‘š))𝐡)) ↔ (πœ‘ β†’ ((β„‚ D𝑛 ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐡))β€˜π‘€) = ((𝑁 + (𝑀 βˆ’ 𝑀))(𝑆 Tayl ((𝑆 D𝑛 𝐹)β€˜π‘€))𝐡))))
42 ssidd 3972 . . . . . . 7 (πœ‘ β†’ β„‚ βŠ† β„‚)
43 mapsspm 8821 . . . . . . . 8 (β„‚ ↑m β„‚) βŠ† (β„‚ ↑pm β„‚)
44 dvntaylp.s . . . . . . . . . 10 (πœ‘ β†’ 𝑆 ∈ {ℝ, β„‚})
45 dvntaylp.f . . . . . . . . . 10 (πœ‘ β†’ 𝐹:π΄βŸΆβ„‚)
46 dvntaylp.a . . . . . . . . . 10 (πœ‘ β†’ 𝐴 βŠ† 𝑆)
47 dvntaylp.n . . . . . . . . . . 11 (πœ‘ β†’ 𝑁 ∈ β„•0)
4847, 1nn0addcld 12484 . . . . . . . . . 10 (πœ‘ β†’ (𝑁 + 𝑀) ∈ β„•0)
49 dvntaylp.b . . . . . . . . . 10 (πœ‘ β†’ 𝐡 ∈ dom ((𝑆 D𝑛 𝐹)β€˜(𝑁 + 𝑀)))
50 eqid 2737 . . . . . . . . . 10 ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐡) = ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐡)
5144, 45, 46, 48, 49, 50taylpf 25741 . . . . . . . . 9 (πœ‘ β†’ ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐡):β„‚βŸΆβ„‚)
52 cnex 11139 . . . . . . . . . 10 β„‚ ∈ V
5352, 52elmap 8816 . . . . . . . . 9 (((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐡) ∈ (β„‚ ↑m β„‚) ↔ ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐡):β„‚βŸΆβ„‚)
5451, 53sylibr 233 . . . . . . . 8 (πœ‘ β†’ ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐡) ∈ (β„‚ ↑m β„‚))
5543, 54sselid 3947 . . . . . . 7 (πœ‘ β†’ ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐡) ∈ (β„‚ ↑pm β„‚))
56 dvn0 25304 . . . . . . 7 ((β„‚ βŠ† β„‚ ∧ ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐡) ∈ (β„‚ ↑pm β„‚)) β†’ ((β„‚ D𝑛 ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐡))β€˜0) = ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐡))
5742, 55, 56syl2anc 585 . . . . . 6 (πœ‘ β†’ ((β„‚ D𝑛 ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐡))β€˜0) = ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐡))
58 recnprss 25284 . . . . . . . . . 10 (𝑆 ∈ {ℝ, β„‚} β†’ 𝑆 βŠ† β„‚)
5944, 58syl 17 . . . . . . . . 9 (πœ‘ β†’ 𝑆 βŠ† β„‚)
6052a1i 11 . . . . . . . . . 10 (πœ‘ β†’ β„‚ ∈ V)
61 elpm2r 8790 . . . . . . . . . 10 (((β„‚ ∈ V ∧ 𝑆 ∈ {ℝ, β„‚}) ∧ (𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆)) β†’ 𝐹 ∈ (β„‚ ↑pm 𝑆))
6260, 44, 45, 46, 61syl22anc 838 . . . . . . . . 9 (πœ‘ β†’ 𝐹 ∈ (β„‚ ↑pm 𝑆))
63 dvn0 25304 . . . . . . . . 9 ((𝑆 βŠ† β„‚ ∧ 𝐹 ∈ (β„‚ ↑pm 𝑆)) β†’ ((𝑆 D𝑛 𝐹)β€˜0) = 𝐹)
6459, 62, 63syl2anc 585 . . . . . . . 8 (πœ‘ β†’ ((𝑆 D𝑛 𝐹)β€˜0) = 𝐹)
6564oveq2d 7378 . . . . . . 7 (πœ‘ β†’ (𝑆 Tayl ((𝑆 D𝑛 𝐹)β€˜0)) = (𝑆 Tayl 𝐹))
661nn0cnd 12482 . . . . . . . . 9 (πœ‘ β†’ 𝑀 ∈ β„‚)
6766subid1d 11508 . . . . . . . 8 (πœ‘ β†’ (𝑀 βˆ’ 0) = 𝑀)
6867oveq2d 7378 . . . . . . 7 (πœ‘ β†’ (𝑁 + (𝑀 βˆ’ 0)) = (𝑁 + 𝑀))
69 eqidd 2738 . . . . . . 7 (πœ‘ β†’ 𝐡 = 𝐡)
7065, 68, 69oveq123d 7383 . . . . . 6 (πœ‘ β†’ ((𝑁 + (𝑀 βˆ’ 0))(𝑆 Tayl ((𝑆 D𝑛 𝐹)β€˜0))𝐡) = ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐡))
7157, 70eqtr4d 2780 . . . . 5 (πœ‘ β†’ ((β„‚ D𝑛 ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐡))β€˜0) = ((𝑁 + (𝑀 βˆ’ 0))(𝑆 Tayl ((𝑆 D𝑛 𝐹)β€˜0))𝐡))
7271a1i 11 . . . 4 (𝑀 ∈ (β„€β‰₯β€˜0) β†’ (πœ‘ β†’ ((β„‚ D𝑛 ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐡))β€˜0) = ((𝑁 + (𝑀 βˆ’ 0))(𝑆 Tayl ((𝑆 D𝑛 𝐹)β€˜0))𝐡)))
73 oveq2 7370 . . . . . . 7 (((β„‚ D𝑛 ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐡))β€˜π‘›) = ((𝑁 + (𝑀 βˆ’ 𝑛))(𝑆 Tayl ((𝑆 D𝑛 𝐹)β€˜π‘›))𝐡) β†’ (β„‚ D ((β„‚ D𝑛 ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐡))β€˜π‘›)) = (β„‚ D ((𝑁 + (𝑀 βˆ’ 𝑛))(𝑆 Tayl ((𝑆 D𝑛 𝐹)β€˜π‘›))𝐡)))
74 ssidd 3972 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (0..^𝑀)) β†’ β„‚ βŠ† β„‚)
7555adantr 482 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (0..^𝑀)) β†’ ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐡) ∈ (β„‚ ↑pm β„‚))
76 elfzouz 13583 . . . . . . . . . . 11 (𝑛 ∈ (0..^𝑀) β†’ 𝑛 ∈ (β„€β‰₯β€˜0))
7776adantl 483 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ (0..^𝑀)) β†’ 𝑛 ∈ (β„€β‰₯β€˜0))
7877, 2eleqtrrdi 2849 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (0..^𝑀)) β†’ 𝑛 ∈ β„•0)
79 dvnp1 25305 . . . . . . . . 9 ((β„‚ βŠ† β„‚ ∧ ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐡) ∈ (β„‚ ↑pm β„‚) ∧ 𝑛 ∈ β„•0) β†’ ((β„‚ D𝑛 ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐡))β€˜(𝑛 + 1)) = (β„‚ D ((β„‚ D𝑛 ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐡))β€˜π‘›)))
8074, 75, 78, 79syl3anc 1372 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (0..^𝑀)) β†’ ((β„‚ D𝑛 ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐡))β€˜(𝑛 + 1)) = (β„‚ D ((β„‚ D𝑛 ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐡))β€˜π‘›)))
8144adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ (0..^𝑀)) β†’ 𝑆 ∈ {ℝ, β„‚})
8262adantr 482 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ (0..^𝑀)) β†’ 𝐹 ∈ (β„‚ ↑pm 𝑆))
83 dvnf 25307 . . . . . . . . . . 11 ((𝑆 ∈ {ℝ, β„‚} ∧ 𝐹 ∈ (β„‚ ↑pm 𝑆) ∧ 𝑛 ∈ β„•0) β†’ ((𝑆 D𝑛 𝐹)β€˜π‘›):dom ((𝑆 D𝑛 𝐹)β€˜π‘›)βŸΆβ„‚)
8481, 82, 78, 83syl3anc 1372 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ (0..^𝑀)) β†’ ((𝑆 D𝑛 𝐹)β€˜π‘›):dom ((𝑆 D𝑛 𝐹)β€˜π‘›)βŸΆβ„‚)
85 dvnbss 25308 . . . . . . . . . . . . 13 ((𝑆 ∈ {ℝ, β„‚} ∧ 𝐹 ∈ (β„‚ ↑pm 𝑆) ∧ 𝑛 ∈ β„•0) β†’ dom ((𝑆 D𝑛 𝐹)β€˜π‘›) βŠ† dom 𝐹)
8681, 82, 78, 85syl3anc 1372 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ (0..^𝑀)) β†’ dom ((𝑆 D𝑛 𝐹)β€˜π‘›) βŠ† dom 𝐹)
8745fdmd 6684 . . . . . . . . . . . . 13 (πœ‘ β†’ dom 𝐹 = 𝐴)
8887adantr 482 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ (0..^𝑀)) β†’ dom 𝐹 = 𝐴)
8986, 88sseqtrd 3989 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ (0..^𝑀)) β†’ dom ((𝑆 D𝑛 𝐹)β€˜π‘›) βŠ† 𝐴)
9046adantr 482 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ (0..^𝑀)) β†’ 𝐴 βŠ† 𝑆)
9189, 90sstrd 3959 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ (0..^𝑀)) β†’ dom ((𝑆 D𝑛 𝐹)β€˜π‘›) βŠ† 𝑆)
9247adantr 482 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ (0..^𝑀)) β†’ 𝑁 ∈ β„•0)
93 fzofzp1 13676 . . . . . . . . . . . . 13 (𝑛 ∈ (0..^𝑀) β†’ (𝑛 + 1) ∈ (0...𝑀))
9493adantl 483 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ (0..^𝑀)) β†’ (𝑛 + 1) ∈ (0...𝑀))
95 fznn0sub 13480 . . . . . . . . . . . 12 ((𝑛 + 1) ∈ (0...𝑀) β†’ (𝑀 βˆ’ (𝑛 + 1)) ∈ β„•0)
9694, 95syl 17 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ (0..^𝑀)) β†’ (𝑀 βˆ’ (𝑛 + 1)) ∈ β„•0)
9792, 96nn0addcld 12484 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ (0..^𝑀)) β†’ (𝑁 + (𝑀 βˆ’ (𝑛 + 1))) ∈ β„•0)
9849adantr 482 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ (0..^𝑀)) β†’ 𝐡 ∈ dom ((𝑆 D𝑛 𝐹)β€˜(𝑁 + 𝑀)))
99 elfzofz 13595 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ (0..^𝑀) β†’ 𝑛 ∈ (0...𝑀))
10099adantl 483 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ (0..^𝑀)) β†’ 𝑛 ∈ (0...𝑀))
101 fznn0sub 13480 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (0...𝑀) β†’ (𝑀 βˆ’ 𝑛) ∈ β„•0)
102100, 101syl 17 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑛 ∈ (0..^𝑀)) β†’ (𝑀 βˆ’ 𝑛) ∈ β„•0)
10392, 102nn0addcld 12484 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑛 ∈ (0..^𝑀)) β†’ (𝑁 + (𝑀 βˆ’ 𝑛)) ∈ β„•0)
104 dvnadd 25309 . . . . . . . . . . . . . 14 (((𝑆 ∈ {ℝ, β„‚} ∧ 𝐹 ∈ (β„‚ ↑pm 𝑆)) ∧ (𝑛 ∈ β„•0 ∧ (𝑁 + (𝑀 βˆ’ 𝑛)) ∈ β„•0)) β†’ ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)β€˜π‘›))β€˜(𝑁 + (𝑀 βˆ’ 𝑛))) = ((𝑆 D𝑛 𝐹)β€˜(𝑛 + (𝑁 + (𝑀 βˆ’ 𝑛)))))
10581, 82, 78, 103, 104syl22anc 838 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ (0..^𝑀)) β†’ ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)β€˜π‘›))β€˜(𝑁 + (𝑀 βˆ’ 𝑛))) = ((𝑆 D𝑛 𝐹)β€˜(𝑛 + (𝑁 + (𝑀 βˆ’ 𝑛)))))
10647nn0cnd 12482 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 𝑁 ∈ β„‚)
107106adantr 482 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ (0..^𝑀)) β†’ 𝑁 ∈ β„‚)
10896nn0cnd 12482 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ (0..^𝑀)) β†’ (𝑀 βˆ’ (𝑛 + 1)) ∈ β„‚)
109 1cnd 11157 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ (0..^𝑀)) β†’ 1 ∈ β„‚)
110107, 108, 109addassd 11184 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑛 ∈ (0..^𝑀)) β†’ ((𝑁 + (𝑀 βˆ’ (𝑛 + 1))) + 1) = (𝑁 + ((𝑀 βˆ’ (𝑛 + 1)) + 1)))
11166adantr 482 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑛 ∈ (0..^𝑀)) β†’ 𝑀 ∈ β„‚)
11278nn0cnd 12482 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑛 ∈ (0..^𝑀)) β†’ 𝑛 ∈ β„‚)
113111, 112, 109nppcan2d 11545 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ (0..^𝑀)) β†’ ((𝑀 βˆ’ (𝑛 + 1)) + 1) = (𝑀 βˆ’ 𝑛))
114113oveq2d 7378 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑛 ∈ (0..^𝑀)) β†’ (𝑁 + ((𝑀 βˆ’ (𝑛 + 1)) + 1)) = (𝑁 + (𝑀 βˆ’ 𝑛)))
115110, 114eqtrd 2777 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑛 ∈ (0..^𝑀)) β†’ ((𝑁 + (𝑀 βˆ’ (𝑛 + 1))) + 1) = (𝑁 + (𝑀 βˆ’ 𝑛)))
116115fveq2d 6851 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ (0..^𝑀)) β†’ ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)β€˜π‘›))β€˜((𝑁 + (𝑀 βˆ’ (𝑛 + 1))) + 1)) = ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)β€˜π‘›))β€˜(𝑁 + (𝑀 βˆ’ 𝑛))))
117112, 111pncan3d 11522 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ (0..^𝑀)) β†’ (𝑛 + (𝑀 βˆ’ 𝑛)) = 𝑀)
118117oveq2d 7378 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑛 ∈ (0..^𝑀)) β†’ (𝑁 + (𝑛 + (𝑀 βˆ’ 𝑛))) = (𝑁 + 𝑀))
119111, 112subcld 11519 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ (0..^𝑀)) β†’ (𝑀 βˆ’ 𝑛) ∈ β„‚)
120107, 112, 119add12d 11388 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑛 ∈ (0..^𝑀)) β†’ (𝑁 + (𝑛 + (𝑀 βˆ’ 𝑛))) = (𝑛 + (𝑁 + (𝑀 βˆ’ 𝑛))))
121118, 120eqtr3d 2779 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑛 ∈ (0..^𝑀)) β†’ (𝑁 + 𝑀) = (𝑛 + (𝑁 + (𝑀 βˆ’ 𝑛))))
122121fveq2d 6851 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ (0..^𝑀)) β†’ ((𝑆 D𝑛 𝐹)β€˜(𝑁 + 𝑀)) = ((𝑆 D𝑛 𝐹)β€˜(𝑛 + (𝑁 + (𝑀 βˆ’ 𝑛)))))
123105, 116, 1223eqtr4d 2787 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ (0..^𝑀)) β†’ ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)β€˜π‘›))β€˜((𝑁 + (𝑀 βˆ’ (𝑛 + 1))) + 1)) = ((𝑆 D𝑛 𝐹)β€˜(𝑁 + 𝑀)))
124123dmeqd 5866 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ (0..^𝑀)) β†’ dom ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)β€˜π‘›))β€˜((𝑁 + (𝑀 βˆ’ (𝑛 + 1))) + 1)) = dom ((𝑆 D𝑛 𝐹)β€˜(𝑁 + 𝑀)))
12598, 124eleqtrrd 2841 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ (0..^𝑀)) β†’ 𝐡 ∈ dom ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)β€˜π‘›))β€˜((𝑁 + (𝑀 βˆ’ (𝑛 + 1))) + 1)))
12681, 84, 91, 97, 125dvtaylp 25745 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (0..^𝑀)) β†’ (β„‚ D (((𝑁 + (𝑀 βˆ’ (𝑛 + 1))) + 1)(𝑆 Tayl ((𝑆 D𝑛 𝐹)β€˜π‘›))𝐡)) = ((𝑁 + (𝑀 βˆ’ (𝑛 + 1)))(𝑆 Tayl (𝑆 D ((𝑆 D𝑛 𝐹)β€˜π‘›)))𝐡))
127115oveq1d 7377 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ (0..^𝑀)) β†’ (((𝑁 + (𝑀 βˆ’ (𝑛 + 1))) + 1)(𝑆 Tayl ((𝑆 D𝑛 𝐹)β€˜π‘›))𝐡) = ((𝑁 + (𝑀 βˆ’ 𝑛))(𝑆 Tayl ((𝑆 D𝑛 𝐹)β€˜π‘›))𝐡))
128127oveq2d 7378 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (0..^𝑀)) β†’ (β„‚ D (((𝑁 + (𝑀 βˆ’ (𝑛 + 1))) + 1)(𝑆 Tayl ((𝑆 D𝑛 𝐹)β€˜π‘›))𝐡)) = (β„‚ D ((𝑁 + (𝑀 βˆ’ 𝑛))(𝑆 Tayl ((𝑆 D𝑛 𝐹)β€˜π‘›))𝐡)))
12959adantr 482 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ (0..^𝑀)) β†’ 𝑆 βŠ† β„‚)
130 dvnp1 25305 . . . . . . . . . . . . 13 ((𝑆 βŠ† β„‚ ∧ 𝐹 ∈ (β„‚ ↑pm 𝑆) ∧ 𝑛 ∈ β„•0) β†’ ((𝑆 D𝑛 𝐹)β€˜(𝑛 + 1)) = (𝑆 D ((𝑆 D𝑛 𝐹)β€˜π‘›)))
131129, 82, 78, 130syl3anc 1372 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ (0..^𝑀)) β†’ ((𝑆 D𝑛 𝐹)β€˜(𝑛 + 1)) = (𝑆 D ((𝑆 D𝑛 𝐹)β€˜π‘›)))
132131oveq2d 7378 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ (0..^𝑀)) β†’ (𝑆 Tayl ((𝑆 D𝑛 𝐹)β€˜(𝑛 + 1))) = (𝑆 Tayl (𝑆 D ((𝑆 D𝑛 𝐹)β€˜π‘›))))
133132eqcomd 2743 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ (0..^𝑀)) β†’ (𝑆 Tayl (𝑆 D ((𝑆 D𝑛 𝐹)β€˜π‘›))) = (𝑆 Tayl ((𝑆 D𝑛 𝐹)β€˜(𝑛 + 1))))
134133oveqd 7379 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (0..^𝑀)) β†’ ((𝑁 + (𝑀 βˆ’ (𝑛 + 1)))(𝑆 Tayl (𝑆 D ((𝑆 D𝑛 𝐹)β€˜π‘›)))𝐡) = ((𝑁 + (𝑀 βˆ’ (𝑛 + 1)))(𝑆 Tayl ((𝑆 D𝑛 𝐹)β€˜(𝑛 + 1)))𝐡))
135126, 128, 1343eqtr3rd 2786 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (0..^𝑀)) β†’ ((𝑁 + (𝑀 βˆ’ (𝑛 + 1)))(𝑆 Tayl ((𝑆 D𝑛 𝐹)β€˜(𝑛 + 1)))𝐡) = (β„‚ D ((𝑁 + (𝑀 βˆ’ 𝑛))(𝑆 Tayl ((𝑆 D𝑛 𝐹)β€˜π‘›))𝐡)))
13680, 135eqeq12d 2753 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ (0..^𝑀)) β†’ (((β„‚ D𝑛 ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐡))β€˜(𝑛 + 1)) = ((𝑁 + (𝑀 βˆ’ (𝑛 + 1)))(𝑆 Tayl ((𝑆 D𝑛 𝐹)β€˜(𝑛 + 1)))𝐡) ↔ (β„‚ D ((β„‚ D𝑛 ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐡))β€˜π‘›)) = (β„‚ D ((𝑁 + (𝑀 βˆ’ 𝑛))(𝑆 Tayl ((𝑆 D𝑛 𝐹)β€˜π‘›))𝐡))))
13773, 136syl5ibr 246 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ (0..^𝑀)) β†’ (((β„‚ D𝑛 ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐡))β€˜π‘›) = ((𝑁 + (𝑀 βˆ’ 𝑛))(𝑆 Tayl ((𝑆 D𝑛 𝐹)β€˜π‘›))𝐡) β†’ ((β„‚ D𝑛 ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐡))β€˜(𝑛 + 1)) = ((𝑁 + (𝑀 βˆ’ (𝑛 + 1)))(𝑆 Tayl ((𝑆 D𝑛 𝐹)β€˜(𝑛 + 1)))𝐡)))
138137expcom 415 . . . . 5 (𝑛 ∈ (0..^𝑀) β†’ (πœ‘ β†’ (((β„‚ D𝑛 ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐡))β€˜π‘›) = ((𝑁 + (𝑀 βˆ’ 𝑛))(𝑆 Tayl ((𝑆 D𝑛 𝐹)β€˜π‘›))𝐡) β†’ ((β„‚ D𝑛 ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐡))β€˜(𝑛 + 1)) = ((𝑁 + (𝑀 βˆ’ (𝑛 + 1)))(𝑆 Tayl ((𝑆 D𝑛 𝐹)β€˜(𝑛 + 1)))𝐡))))
139138a2d 29 . . . 4 (𝑛 ∈ (0..^𝑀) β†’ ((πœ‘ β†’ ((β„‚ D𝑛 ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐡))β€˜π‘›) = ((𝑁 + (𝑀 βˆ’ 𝑛))(𝑆 Tayl ((𝑆 D𝑛 𝐹)β€˜π‘›))𝐡)) β†’ (πœ‘ β†’ ((β„‚ D𝑛 ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐡))β€˜(𝑛 + 1)) = ((𝑁 + (𝑀 βˆ’ (𝑛 + 1)))(𝑆 Tayl ((𝑆 D𝑛 𝐹)β€˜(𝑛 + 1)))𝐡))))
14014, 23, 32, 41, 72, 139fzind2 13697 . . 3 (𝑀 ∈ (0...𝑀) β†’ (πœ‘ β†’ ((β„‚ D𝑛 ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐡))β€˜π‘€) = ((𝑁 + (𝑀 βˆ’ 𝑀))(𝑆 Tayl ((𝑆 D𝑛 𝐹)β€˜π‘€))𝐡)))
1415, 140mpcom 38 . 2 (πœ‘ β†’ ((β„‚ D𝑛 ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐡))β€˜π‘€) = ((𝑁 + (𝑀 βˆ’ 𝑀))(𝑆 Tayl ((𝑆 D𝑛 𝐹)β€˜π‘€))𝐡))
14266subidd 11507 . . . . 5 (πœ‘ β†’ (𝑀 βˆ’ 𝑀) = 0)
143142oveq2d 7378 . . . 4 (πœ‘ β†’ (𝑁 + (𝑀 βˆ’ 𝑀)) = (𝑁 + 0))
144106addid1d 11362 . . . 4 (πœ‘ β†’ (𝑁 + 0) = 𝑁)
145143, 144eqtrd 2777 . . 3 (πœ‘ β†’ (𝑁 + (𝑀 βˆ’ 𝑀)) = 𝑁)
146145oveq1d 7377 . 2 (πœ‘ β†’ ((𝑁 + (𝑀 βˆ’ 𝑀))(𝑆 Tayl ((𝑆 D𝑛 𝐹)β€˜π‘€))𝐡) = (𝑁(𝑆 Tayl ((𝑆 D𝑛 𝐹)β€˜π‘€))𝐡))
147141, 146eqtrd 2777 1 (πœ‘ β†’ ((β„‚ D𝑛 ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐡))β€˜π‘€) = (𝑁(𝑆 Tayl ((𝑆 D𝑛 𝐹)β€˜π‘€))𝐡))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 397   = wceq 1542   ∈ wcel 2107  Vcvv 3448   βŠ† wss 3915  {cpr 4593  dom cdm 5638  βŸΆwf 6497  β€˜cfv 6501  (class class class)co 7362   ↑m cmap 8772   ↑pm cpm 8773  β„‚cc 11056  β„cr 11057  0cc0 11058  1c1 11059   + caddc 11061   βˆ’ cmin 11392  β„•0cn0 12420  β„€β‰₯cuz 12770  ...cfz 13431  ..^cfzo 13574   D cdv 25243   D𝑛 cdvn 25244   Tayl ctayl 25728
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-inf2 9584  ax-cnex 11114  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-mulcom 11122  ax-addass 11123  ax-mulass 11124  ax-distr 11125  ax-i2m1 11126  ax-1ne0 11127  ax-1rid 11128  ax-rnegex 11129  ax-rrecex 11130  ax-cnre 11131  ax-pre-lttri 11132  ax-pre-lttrn 11133  ax-pre-ltadd 11134  ax-pre-mulgt0 11135  ax-pre-sup 11136  ax-addf 11137  ax-mulf 11138
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rmo 3356  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-tp 4596  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-iin 4962  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-se 5594  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-isom 6510  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-of 7622  df-om 7808  df-1st 7926  df-2nd 7927  df-supp 8098  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-2o 8418  df-er 8655  df-map 8774  df-pm 8775  df-ixp 8843  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-fsupp 9313  df-fi 9354  df-sup 9385  df-inf 9386  df-oi 9453  df-card 9882  df-pnf 11198  df-mnf 11199  df-xr 11200  df-ltxr 11201  df-le 11202  df-sub 11394  df-neg 11395  df-div 11820  df-nn 12161  df-2 12223  df-3 12224  df-4 12225  df-5 12226  df-6 12227  df-7 12228  df-8 12229  df-9 12230  df-n0 12421  df-z 12507  df-dec 12626  df-uz 12771  df-q 12881  df-rp 12923  df-xneg 13040  df-xadd 13041  df-xmul 13042  df-icc 13278  df-fz 13432  df-fzo 13575  df-seq 13914  df-exp 13975  df-fac 14181  df-hash 14238  df-cj 14991  df-re 14992  df-im 14993  df-sqrt 15127  df-abs 15128  df-clim 15377  df-sum 15578  df-struct 17026  df-sets 17043  df-slot 17061  df-ndx 17073  df-base 17091  df-ress 17120  df-plusg 17153  df-mulr 17154  df-starv 17155  df-sca 17156  df-vsca 17157  df-ip 17158  df-tset 17159  df-ple 17160  df-ds 17162  df-unif 17163  df-hom 17164  df-cco 17165  df-rest 17311  df-topn 17312  df-0g 17330  df-gsum 17331  df-topgen 17332  df-pt 17333  df-prds 17336  df-xrs 17391  df-qtop 17396  df-imas 17397  df-xps 17399  df-mre 17473  df-mrc 17474  df-acs 17476  df-mgm 18504  df-sgrp 18553  df-mnd 18564  df-submnd 18609  df-grp 18758  df-minusg 18759  df-mulg 18880  df-cntz 19104  df-cmn 19571  df-abl 19572  df-mgp 19904  df-ur 19921  df-ring 19973  df-cring 19974  df-psmet 20804  df-xmet 20805  df-met 20806  df-bl 20807  df-mopn 20808  df-fbas 20809  df-fg 20810  df-cnfld 20813  df-top 22259  df-topon 22276  df-topsp 22298  df-bases 22312  df-cld 22386  df-ntr 22387  df-cls 22388  df-nei 22465  df-lp 22503  df-perf 22504  df-cn 22594  df-cnp 22595  df-haus 22682  df-tx 22929  df-hmeo 23122  df-fil 23213  df-fm 23305  df-flim 23306  df-flf 23307  df-tsms 23494  df-xms 23689  df-ms 23690  df-tms 23691  df-cncf 24257  df-limc 25246  df-dv 25247  df-dvn 25248  df-tayl 25730
This theorem is referenced by:  dvntaylp0  25747  taylthlem1  25748
  Copyright terms: Public domain W3C validator