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

Theorem dvradcnv 25796
Description: The radius of convergence of the (formal) derivative 𝐻 of the power series 𝐺 is at least as large as the radius of convergence of 𝐺. (In fact they are equal, but we don't have as much use for the negative side of this claim.) (Contributed by Mario Carneiro, 31-Mar-2015.)
Hypotheses
Ref Expression
dvradcnv.g 𝐺 = (π‘₯ ∈ β„‚ ↦ (𝑛 ∈ β„•0 ↦ ((π΄β€˜π‘›) Β· (π‘₯↑𝑛))))
dvradcnv.r 𝑅 = sup({π‘Ÿ ∈ ℝ ∣ seq0( + , (πΊβ€˜π‘Ÿ)) ∈ dom ⇝ }, ℝ*, < )
dvradcnv.h 𝐻 = (𝑛 ∈ β„•0 ↦ (((𝑛 + 1) Β· (π΄β€˜(𝑛 + 1))) Β· (𝑋↑𝑛)))
dvradcnv.a (πœ‘ β†’ 𝐴:β„•0βŸΆβ„‚)
dvradcnv.x (πœ‘ β†’ 𝑋 ∈ β„‚)
dvradcnv.l (πœ‘ β†’ (absβ€˜π‘‹) < 𝑅)
Assertion
Ref Expression
dvradcnv (πœ‘ β†’ seq0( + , 𝐻) ∈ dom ⇝ )
Distinct variable groups:   π‘₯,𝑛,𝐴   𝐺,π‘Ÿ   𝑛,π‘Ÿ,𝑋,π‘₯
Allowed substitution hints:   πœ‘(π‘₯,𝑛,π‘Ÿ)   𝐴(π‘Ÿ)   𝑅(π‘₯,𝑛,π‘Ÿ)   𝐺(π‘₯,𝑛)   𝐻(π‘₯,𝑛,π‘Ÿ)

Proof of Theorem dvradcnv
Dummy variables π‘˜ 𝑖 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nn0uz 12810 . 2 β„•0 = (β„€β‰₯β€˜0)
2 1nn0 12434 . . 3 1 ∈ β„•0
32a1i 11 . 2 (πœ‘ β†’ 1 ∈ β„•0)
4 ax-1cn 11114 . . . . 5 1 ∈ β„‚
5 nn0cn 12428 . . . . . 6 (π‘˜ ∈ β„•0 β†’ π‘˜ ∈ β„‚)
65adantl 483 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ π‘˜ ∈ β„‚)
7 nn0ex 12424 . . . . . . 7 β„•0 ∈ V
87mptex 7174 . . . . . 6 (𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)))) ∈ V
98shftval4 14968 . . . . 5 ((1 ∈ β„‚ ∧ π‘˜ ∈ β„‚) β†’ (((𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)))) shift -1)β€˜π‘˜) = ((𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–))))β€˜(1 + π‘˜)))
104, 6, 9sylancr 588 . . . 4 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (((𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)))) shift -1)β€˜π‘˜) = ((𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–))))β€˜(1 + π‘˜)))
11 addcom 11346 . . . . . 6 ((1 ∈ β„‚ ∧ π‘˜ ∈ β„‚) β†’ (1 + π‘˜) = (π‘˜ + 1))
124, 6, 11sylancr 588 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (1 + π‘˜) = (π‘˜ + 1))
1312fveq2d 6847 . . . 4 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–))))β€˜(1 + π‘˜)) = ((𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–))))β€˜(π‘˜ + 1)))
14 peano2nn0 12458 . . . . . . 7 (π‘˜ ∈ β„•0 β†’ (π‘˜ + 1) ∈ β„•0)
1514adantl 483 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (π‘˜ + 1) ∈ β„•0)
16 id 22 . . . . . . . 8 (𝑖 = (π‘˜ + 1) β†’ 𝑖 = (π‘˜ + 1))
17 2fveq3 6848 . . . . . . . 8 (𝑖 = (π‘˜ + 1) β†’ (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)) = (absβ€˜((πΊβ€˜π‘‹)β€˜(π‘˜ + 1))))
1816, 17oveq12d 7376 . . . . . . 7 (𝑖 = (π‘˜ + 1) β†’ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–))) = ((π‘˜ + 1) Β· (absβ€˜((πΊβ€˜π‘‹)β€˜(π‘˜ + 1)))))
19 eqid 2733 . . . . . . 7 (𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)))) = (𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–))))
20 ovex 7391 . . . . . . 7 ((π‘˜ + 1) Β· (absβ€˜((πΊβ€˜π‘‹)β€˜(π‘˜ + 1)))) ∈ V
2118, 19, 20fvmpt 6949 . . . . . 6 ((π‘˜ + 1) ∈ β„•0 β†’ ((𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–))))β€˜(π‘˜ + 1)) = ((π‘˜ + 1) Β· (absβ€˜((πΊβ€˜π‘‹)β€˜(π‘˜ + 1)))))
2215, 21syl 17 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–))))β€˜(π‘˜ + 1)) = ((π‘˜ + 1) Β· (absβ€˜((πΊβ€˜π‘‹)β€˜(π‘˜ + 1)))))
23 dvradcnv.x . . . . . . . 8 (πœ‘ β†’ 𝑋 ∈ β„‚)
24 dvradcnv.g . . . . . . . . 9 𝐺 = (π‘₯ ∈ β„‚ ↦ (𝑛 ∈ β„•0 ↦ ((π΄β€˜π‘›) Β· (π‘₯↑𝑛))))
2524pserval2 25786 . . . . . . . 8 ((𝑋 ∈ β„‚ ∧ (π‘˜ + 1) ∈ β„•0) β†’ ((πΊβ€˜π‘‹)β€˜(π‘˜ + 1)) = ((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1))))
2623, 14, 25syl2an 597 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((πΊβ€˜π‘‹)β€˜(π‘˜ + 1)) = ((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1))))
2726fveq2d 6847 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (absβ€˜((πΊβ€˜π‘‹)β€˜(π‘˜ + 1))) = (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1)))))
2827oveq2d 7374 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((π‘˜ + 1) Β· (absβ€˜((πΊβ€˜π‘‹)β€˜(π‘˜ + 1)))) = ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1))))))
2922, 28eqtrd 2773 . . . 4 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–))))β€˜(π‘˜ + 1)) = ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1))))))
3010, 13, 293eqtrd 2777 . . 3 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (((𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)))) shift -1)β€˜π‘˜) = ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1))))))
3115nn0red 12479 . . . 4 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (π‘˜ + 1) ∈ ℝ)
32 dvradcnv.a . . . . . . 7 (πœ‘ β†’ 𝐴:β„•0βŸΆβ„‚)
33 ffvelcdm 7033 . . . . . . 7 ((𝐴:β„•0βŸΆβ„‚ ∧ (π‘˜ + 1) ∈ β„•0) β†’ (π΄β€˜(π‘˜ + 1)) ∈ β„‚)
3432, 14, 33syl2an 597 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (π΄β€˜(π‘˜ + 1)) ∈ β„‚)
35 expcl 13991 . . . . . . 7 ((𝑋 ∈ β„‚ ∧ (π‘˜ + 1) ∈ β„•0) β†’ (𝑋↑(π‘˜ + 1)) ∈ β„‚)
3623, 14, 35syl2an 597 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (𝑋↑(π‘˜ + 1)) ∈ β„‚)
3734, 36mulcld 11180 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1))) ∈ β„‚)
3837abscld 15327 . . . 4 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1)))) ∈ ℝ)
3931, 38remulcld 11190 . . 3 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1))))) ∈ ℝ)
4030, 39eqeltrd 2834 . 2 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (((𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)))) shift -1)β€˜π‘˜) ∈ ℝ)
41 oveq1 7365 . . . . . . 7 (𝑛 = π‘˜ β†’ (𝑛 + 1) = (π‘˜ + 1))
4241fveq2d 6847 . . . . . . 7 (𝑛 = π‘˜ β†’ (π΄β€˜(𝑛 + 1)) = (π΄β€˜(π‘˜ + 1)))
4341, 42oveq12d 7376 . . . . . 6 (𝑛 = π‘˜ β†’ ((𝑛 + 1) Β· (π΄β€˜(𝑛 + 1))) = ((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))))
44 oveq2 7366 . . . . . 6 (𝑛 = π‘˜ β†’ (𝑋↑𝑛) = (π‘‹β†‘π‘˜))
4543, 44oveq12d 7376 . . . . 5 (𝑛 = π‘˜ β†’ (((𝑛 + 1) Β· (π΄β€˜(𝑛 + 1))) Β· (𝑋↑𝑛)) = (((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) Β· (π‘‹β†‘π‘˜)))
46 dvradcnv.h . . . . 5 𝐻 = (𝑛 ∈ β„•0 ↦ (((𝑛 + 1) Β· (π΄β€˜(𝑛 + 1))) Β· (𝑋↑𝑛)))
47 ovex 7391 . . . . 5 (((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) Β· (π‘‹β†‘π‘˜)) ∈ V
4845, 46, 47fvmpt 6949 . . . 4 (π‘˜ ∈ β„•0 β†’ (π»β€˜π‘˜) = (((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) Β· (π‘‹β†‘π‘˜)))
4948adantl 483 . . 3 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (π»β€˜π‘˜) = (((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) Β· (π‘‹β†‘π‘˜)))
5015nn0cnd 12480 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (π‘˜ + 1) ∈ β„‚)
5150, 34mulcld 11180 . . . 4 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) ∈ β„‚)
52 expcl 13991 . . . . 5 ((𝑋 ∈ β„‚ ∧ π‘˜ ∈ β„•0) β†’ (π‘‹β†‘π‘˜) ∈ β„‚)
5323, 52sylan 581 . . . 4 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (π‘‹β†‘π‘˜) ∈ β„‚)
5451, 53mulcld 11180 . . 3 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) Β· (π‘‹β†‘π‘˜)) ∈ β„‚)
5549, 54eqeltrd 2834 . 2 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (π»β€˜π‘˜) ∈ β„‚)
56 dvradcnv.r . . . . . . . 8 𝑅 = sup({π‘Ÿ ∈ ℝ ∣ seq0( + , (πΊβ€˜π‘Ÿ)) ∈ dom ⇝ }, ℝ*, < )
57 dvradcnv.l . . . . . . . 8 (πœ‘ β†’ (absβ€˜π‘‹) < 𝑅)
58 id 22 . . . . . . . . . 10 (𝑖 = π‘˜ β†’ 𝑖 = π‘˜)
59 2fveq3 6848 . . . . . . . . . 10 (𝑖 = π‘˜ β†’ (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)) = (absβ€˜((πΊβ€˜π‘‹)β€˜π‘˜)))
6058, 59oveq12d 7376 . . . . . . . . 9 (𝑖 = π‘˜ β†’ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–))) = (π‘˜ Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘˜))))
6160cbvmptv 5219 . . . . . . . 8 (𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)))) = (π‘˜ ∈ β„•0 ↦ (π‘˜ Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘˜))))
6224, 32, 56, 23, 57, 61radcnvlt1 25793 . . . . . . 7 (πœ‘ β†’ (seq0( + , (𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–))))) ∈ dom ⇝ ∧ seq0( + , (abs ∘ (πΊβ€˜π‘‹))) ∈ dom ⇝ ))
6362simpld 496 . . . . . 6 (πœ‘ β†’ seq0( + , (𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–))))) ∈ dom ⇝ )
64 climdm 15442 . . . . . 6 (seq0( + , (𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–))))) ∈ dom ⇝ ↔ seq0( + , (𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–))))) ⇝ ( ⇝ β€˜seq0( + , (𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)))))))
6563, 64sylib 217 . . . . 5 (πœ‘ β†’ seq0( + , (𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–))))) ⇝ ( ⇝ β€˜seq0( + , (𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)))))))
66 0z 12515 . . . . . 6 0 ∈ β„€
67 neg1z 12544 . . . . . 6 -1 ∈ β„€
688isershft 15554 . . . . . 6 ((0 ∈ β„€ ∧ -1 ∈ β„€) β†’ (seq0( + , (𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–))))) ⇝ ( ⇝ β€˜seq0( + , (𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)))))) ↔ seq(0 + -1)( + , ((𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)))) shift -1)) ⇝ ( ⇝ β€˜seq0( + , (𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–))))))))
6966, 67, 68mp2an 691 . . . . 5 (seq0( + , (𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–))))) ⇝ ( ⇝ β€˜seq0( + , (𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)))))) ↔ seq(0 + -1)( + , ((𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)))) shift -1)) ⇝ ( ⇝ β€˜seq0( + , (𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)))))))
7065, 69sylib 217 . . . 4 (πœ‘ β†’ seq(0 + -1)( + , ((𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)))) shift -1)) ⇝ ( ⇝ β€˜seq0( + , (𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)))))))
71 seqex 13914 . . . . 5 seq(0 + -1)( + , ((𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)))) shift -1)) ∈ V
72 fvex 6856 . . . . 5 ( ⇝ β€˜seq0( + , (𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)))))) ∈ V
7371, 72breldm 5865 . . . 4 (seq(0 + -1)( + , ((𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)))) shift -1)) ⇝ ( ⇝ β€˜seq0( + , (𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)))))) β†’ seq(0 + -1)( + , ((𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)))) shift -1)) ∈ dom ⇝ )
7470, 73syl 17 . . 3 (πœ‘ β†’ seq(0 + -1)( + , ((𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)))) shift -1)) ∈ dom ⇝ )
75 eqid 2733 . . . 4 (β„€β‰₯β€˜(0 + -1)) = (β„€β‰₯β€˜(0 + -1))
76 neg1cn 12272 . . . . . . . 8 -1 ∈ β„‚
7776addid2i 11348 . . . . . . 7 (0 + -1) = -1
78 0le1 11683 . . . . . . . 8 0 ≀ 1
79 1re 11160 . . . . . . . . 9 1 ∈ ℝ
80 le0neg2 11669 . . . . . . . . 9 (1 ∈ ℝ β†’ (0 ≀ 1 ↔ -1 ≀ 0))
8179, 80ax-mp 5 . . . . . . . 8 (0 ≀ 1 ↔ -1 ≀ 0)
8278, 81mpbi 229 . . . . . . 7 -1 ≀ 0
8377, 82eqbrtri 5127 . . . . . 6 (0 + -1) ≀ 0
8477, 67eqeltri 2830 . . . . . . 7 (0 + -1) ∈ β„€
8584eluz1i 12776 . . . . . 6 (0 ∈ (β„€β‰₯β€˜(0 + -1)) ↔ (0 ∈ β„€ ∧ (0 + -1) ≀ 0))
8666, 83, 85mpbir2an 710 . . . . 5 0 ∈ (β„€β‰₯β€˜(0 + -1))
8786a1i 11 . . . 4 (πœ‘ β†’ 0 ∈ (β„€β‰₯β€˜(0 + -1)))
88 eluzelcn 12780 . . . . . . 7 (π‘˜ ∈ (β„€β‰₯β€˜(0 + -1)) β†’ π‘˜ ∈ β„‚)
8988adantl 483 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ (β„€β‰₯β€˜(0 + -1))) β†’ π‘˜ ∈ β„‚)
904, 89, 9sylancr 588 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ (β„€β‰₯β€˜(0 + -1))) β†’ (((𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)))) shift -1)β€˜π‘˜) = ((𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–))))β€˜(1 + π‘˜)))
91 nn0re 12427 . . . . . . . . . 10 (𝑖 ∈ β„•0 β†’ 𝑖 ∈ ℝ)
9291adantl 483 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ β„•0) β†’ 𝑖 ∈ ℝ)
9324, 32, 23psergf 25787 . . . . . . . . . . 11 (πœ‘ β†’ (πΊβ€˜π‘‹):β„•0βŸΆβ„‚)
9493ffvelcdmda 7036 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ β„•0) β†’ ((πΊβ€˜π‘‹)β€˜π‘–) ∈ β„‚)
9594abscld 15327 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ β„•0) β†’ (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)) ∈ ℝ)
9692, 95remulcld 11190 . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ β„•0) β†’ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–))) ∈ ℝ)
9796recnd 11188 . . . . . . 7 ((πœ‘ ∧ 𝑖 ∈ β„•0) β†’ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–))) ∈ β„‚)
9897fmpttd 7064 . . . . . 6 (πœ‘ β†’ (𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)))):β„•0βŸΆβ„‚)
994, 88, 11sylancr 588 . . . . . . 7 (π‘˜ ∈ (β„€β‰₯β€˜(0 + -1)) β†’ (1 + π‘˜) = (π‘˜ + 1))
100 eluzp1p1 12796 . . . . . . . 8 (π‘˜ ∈ (β„€β‰₯β€˜(0 + -1)) β†’ (π‘˜ + 1) ∈ (β„€β‰₯β€˜((0 + -1) + 1)))
10177oveq1i 7368 . . . . . . . . . . 11 ((0 + -1) + 1) = (-1 + 1)
102 1pneg1e0 12277 . . . . . . . . . . . 12 (1 + -1) = 0
1034, 76, 102addcomli 11352 . . . . . . . . . . 11 (-1 + 1) = 0
104101, 103eqtri 2761 . . . . . . . . . 10 ((0 + -1) + 1) = 0
105104fveq2i 6846 . . . . . . . . 9 (β„€β‰₯β€˜((0 + -1) + 1)) = (β„€β‰₯β€˜0)
1061, 105eqtr4i 2764 . . . . . . . 8 β„•0 = (β„€β‰₯β€˜((0 + -1) + 1))
107100, 106eleqtrrdi 2845 . . . . . . 7 (π‘˜ ∈ (β„€β‰₯β€˜(0 + -1)) β†’ (π‘˜ + 1) ∈ β„•0)
10899, 107eqeltrd 2834 . . . . . 6 (π‘˜ ∈ (β„€β‰₯β€˜(0 + -1)) β†’ (1 + π‘˜) ∈ β„•0)
109 ffvelcdm 7033 . . . . . 6 (((𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)))):β„•0βŸΆβ„‚ ∧ (1 + π‘˜) ∈ β„•0) β†’ ((𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–))))β€˜(1 + π‘˜)) ∈ β„‚)
11098, 108, 109syl2an 597 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ (β„€β‰₯β€˜(0 + -1))) β†’ ((𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–))))β€˜(1 + π‘˜)) ∈ β„‚)
11190, 110eqeltrd 2834 . . . 4 ((πœ‘ ∧ π‘˜ ∈ (β„€β‰₯β€˜(0 + -1))) β†’ (((𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)))) shift -1)β€˜π‘˜) ∈ β„‚)
11275, 87, 111iserex 15547 . . 3 (πœ‘ β†’ (seq(0 + -1)( + , ((𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)))) shift -1)) ∈ dom ⇝ ↔ seq0( + , ((𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)))) shift -1)) ∈ dom ⇝ ))
11374, 112mpbid 231 . 2 (πœ‘ β†’ seq0( + , ((𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)))) shift -1)) ∈ dom ⇝ )
114 1red 11161 . . 3 ((πœ‘ ∧ 𝑋 = 0) β†’ 1 ∈ ℝ)
115 neqne 2948 . . . . 5 (Β¬ 𝑋 = 0 β†’ 𝑋 β‰  0)
116 absrpcl 15179 . . . . 5 ((𝑋 ∈ β„‚ ∧ 𝑋 β‰  0) β†’ (absβ€˜π‘‹) ∈ ℝ+)
11723, 115, 116syl2an 597 . . . 4 ((πœ‘ ∧ Β¬ 𝑋 = 0) β†’ (absβ€˜π‘‹) ∈ ℝ+)
118117rprecred 12973 . . 3 ((πœ‘ ∧ Β¬ 𝑋 = 0) β†’ (1 / (absβ€˜π‘‹)) ∈ ℝ)
119114, 118ifclda 4522 . 2 (πœ‘ β†’ if(𝑋 = 0, 1, (1 / (absβ€˜π‘‹))) ∈ ℝ)
120 oveq1 7365 . . . . 5 (1 = if(𝑋 = 0, 1, (1 / (absβ€˜π‘‹))) β†’ (1 Β· ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1)))))) = (if(𝑋 = 0, 1, (1 / (absβ€˜π‘‹))) Β· ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1)))))))
121120breq2d 5118 . . . 4 (1 = if(𝑋 = 0, 1, (1 / (absβ€˜π‘‹))) β†’ ((absβ€˜(((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) Β· (π‘‹β†‘π‘˜))) ≀ (1 Β· ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1)))))) ↔ (absβ€˜(((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) Β· (π‘‹β†‘π‘˜))) ≀ (if(𝑋 = 0, 1, (1 / (absβ€˜π‘‹))) Β· ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1))))))))
122 oveq1 7365 . . . . 5 ((1 / (absβ€˜π‘‹)) = if(𝑋 = 0, 1, (1 / (absβ€˜π‘‹))) β†’ ((1 / (absβ€˜π‘‹)) Β· ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1)))))) = (if(𝑋 = 0, 1, (1 / (absβ€˜π‘‹))) Β· ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1)))))))
123122breq2d 5118 . . . 4 ((1 / (absβ€˜π‘‹)) = if(𝑋 = 0, 1, (1 / (absβ€˜π‘‹))) β†’ ((absβ€˜(((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) Β· (π‘‹β†‘π‘˜))) ≀ ((1 / (absβ€˜π‘‹)) Β· ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1)))))) ↔ (absβ€˜(((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) Β· (π‘‹β†‘π‘˜))) ≀ (if(𝑋 = 0, 1, (1 / (absβ€˜π‘‹))) Β· ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1))))))))
124 elnnuz 12812 . . . . . . . 8 (π‘˜ ∈ β„• ↔ π‘˜ ∈ (β„€β‰₯β€˜1))
125 nnnn0 12425 . . . . . . . 8 (π‘˜ ∈ β„• β†’ π‘˜ ∈ β„•0)
126124, 125sylbir 234 . . . . . . 7 (π‘˜ ∈ (β„€β‰₯β€˜1) β†’ π‘˜ ∈ β„•0)
12715nn0ge0d 12481 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ 0 ≀ (π‘˜ + 1))
12837absge0d 15335 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ 0 ≀ (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1)))))
12931, 38, 127, 128mulge0d 11737 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ 0 ≀ ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1))))))
130126, 129sylan2 594 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ (β„€β‰₯β€˜1)) β†’ 0 ≀ ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1))))))
131130adantr 482 . . . . 5 (((πœ‘ ∧ π‘˜ ∈ (β„€β‰₯β€˜1)) ∧ 𝑋 = 0) β†’ 0 ≀ ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1))))))
132 oveq1 7365 . . . . . . . . 9 (𝑋 = 0 β†’ (π‘‹β†‘π‘˜) = (0β†‘π‘˜))
133 simpr 486 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ (β„€β‰₯β€˜1)) β†’ π‘˜ ∈ (β„€β‰₯β€˜1))
134133, 124sylibr 233 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ (β„€β‰₯β€˜1)) β†’ π‘˜ ∈ β„•)
1351340expd 14050 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ (β„€β‰₯β€˜1)) β†’ (0β†‘π‘˜) = 0)
136132, 135sylan9eqr 2795 . . . . . . . 8 (((πœ‘ ∧ π‘˜ ∈ (β„€β‰₯β€˜1)) ∧ 𝑋 = 0) β†’ (π‘‹β†‘π‘˜) = 0)
137136oveq2d 7374 . . . . . . 7 (((πœ‘ ∧ π‘˜ ∈ (β„€β‰₯β€˜1)) ∧ 𝑋 = 0) β†’ (((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) Β· (π‘‹β†‘π‘˜)) = (((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) Β· 0))
13851mul01d 11359 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) Β· 0) = 0)
139126, 138sylan2 594 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ (β„€β‰₯β€˜1)) β†’ (((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) Β· 0) = 0)
140139adantr 482 . . . . . . 7 (((πœ‘ ∧ π‘˜ ∈ (β„€β‰₯β€˜1)) ∧ 𝑋 = 0) β†’ (((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) Β· 0) = 0)
141137, 140eqtrd 2773 . . . . . 6 (((πœ‘ ∧ π‘˜ ∈ (β„€β‰₯β€˜1)) ∧ 𝑋 = 0) β†’ (((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) Β· (π‘‹β†‘π‘˜)) = 0)
142141abs00bd 15182 . . . . 5 (((πœ‘ ∧ π‘˜ ∈ (β„€β‰₯β€˜1)) ∧ 𝑋 = 0) β†’ (absβ€˜(((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) Β· (π‘‹β†‘π‘˜))) = 0)
14339recnd 11188 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1))))) ∈ β„‚)
144143mulid2d 11178 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (1 Β· ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1)))))) = ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1))))))
145126, 144sylan2 594 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ (β„€β‰₯β€˜1)) β†’ (1 Β· ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1)))))) = ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1))))))
146145adantr 482 . . . . 5 (((πœ‘ ∧ π‘˜ ∈ (β„€β‰₯β€˜1)) ∧ 𝑋 = 0) β†’ (1 Β· ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1)))))) = ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1))))))
147131, 142, 1463brtr4d 5138 . . . 4 (((πœ‘ ∧ π‘˜ ∈ (β„€β‰₯β€˜1)) ∧ 𝑋 = 0) β†’ (absβ€˜(((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) Β· (π‘‹β†‘π‘˜))) ≀ (1 Β· ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1)))))))
148 df-ne 2941 . . . . 5 (𝑋 β‰  0 ↔ Β¬ 𝑋 = 0)
14954abscld 15327 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (absβ€˜(((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) Β· (π‘‹β†‘π‘˜))) ∈ ℝ)
15050, 34, 53mulassd 11183 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) Β· (π‘‹β†‘π‘˜)) = ((π‘˜ + 1) Β· ((π΄β€˜(π‘˜ + 1)) Β· (π‘‹β†‘π‘˜))))
151150fveq2d 6847 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (absβ€˜(((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) Β· (π‘‹β†‘π‘˜))) = (absβ€˜((π‘˜ + 1) Β· ((π΄β€˜(π‘˜ + 1)) Β· (π‘‹β†‘π‘˜)))))
15234, 53mulcld 11180 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((π΄β€˜(π‘˜ + 1)) Β· (π‘‹β†‘π‘˜)) ∈ β„‚)
15350, 152absmuld 15345 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (absβ€˜((π‘˜ + 1) Β· ((π΄β€˜(π‘˜ + 1)) Β· (π‘‹β†‘π‘˜)))) = ((absβ€˜(π‘˜ + 1)) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (π‘‹β†‘π‘˜)))))
15431, 127absidd 15313 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (absβ€˜(π‘˜ + 1)) = (π‘˜ + 1))
155154oveq1d 7373 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((absβ€˜(π‘˜ + 1)) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (π‘‹β†‘π‘˜)))) = ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (π‘‹β†‘π‘˜)))))
156151, 153, 1553eqtrd 2777 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (absβ€˜(((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) Β· (π‘‹β†‘π‘˜))) = ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (π‘‹β†‘π‘˜)))))
157149, 156eqled 11263 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (absβ€˜(((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) Β· (π‘‹β†‘π‘˜))) ≀ ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (π‘‹β†‘π‘˜)))))
158157adantr 482 . . . . . . 7 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ (absβ€˜(((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) Β· (π‘‹β†‘π‘˜))) ≀ ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (π‘‹β†‘π‘˜)))))
15923adantr 482 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ 𝑋 ∈ β„‚)
160116rpreccld 12972 . . . . . . . . . . 11 ((𝑋 ∈ β„‚ ∧ 𝑋 β‰  0) β†’ (1 / (absβ€˜π‘‹)) ∈ ℝ+)
161159, 160sylan 581 . . . . . . . . . 10 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ (1 / (absβ€˜π‘‹)) ∈ ℝ+)
162161rpcnd 12964 . . . . . . . . 9 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ (1 / (absβ€˜π‘‹)) ∈ β„‚)
16350adantr 482 . . . . . . . . 9 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ (π‘˜ + 1) ∈ β„‚)
16438adantr 482 . . . . . . . . . 10 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1)))) ∈ ℝ)
165164recnd 11188 . . . . . . . . 9 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1)))) ∈ β„‚)
166162, 163, 165mul12d 11369 . . . . . . . 8 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ ((1 / (absβ€˜π‘‹)) Β· ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1)))))) = ((π‘˜ + 1) Β· ((1 / (absβ€˜π‘‹)) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1)))))))
16737adantr 482 . . . . . . . . . . 11 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ ((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1))) ∈ β„‚)
16823ad2antrr 725 . . . . . . . . . . 11 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ 𝑋 ∈ β„‚)
169 simpr 486 . . . . . . . . . . 11 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ 𝑋 β‰  0)
170167, 168, 169absdivd 15346 . . . . . . . . . 10 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ (absβ€˜(((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1))) / 𝑋)) = ((absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1)))) / (absβ€˜π‘‹)))
17134adantr 482 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ (π΄β€˜(π‘˜ + 1)) ∈ β„‚)
17236adantr 482 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ (𝑋↑(π‘˜ + 1)) ∈ β„‚)
173171, 172, 168, 169divassd 11971 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ (((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1))) / 𝑋) = ((π΄β€˜(π‘˜ + 1)) Β· ((𝑋↑(π‘˜ + 1)) / 𝑋)))
1746adantr 482 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ π‘˜ ∈ β„‚)
175 pncan 11412 . . . . . . . . . . . . . . . 16 ((π‘˜ ∈ β„‚ ∧ 1 ∈ β„‚) β†’ ((π‘˜ + 1) βˆ’ 1) = π‘˜)
176174, 4, 175sylancl 587 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ ((π‘˜ + 1) βˆ’ 1) = π‘˜)
177176oveq2d 7374 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ (𝑋↑((π‘˜ + 1) βˆ’ 1)) = (π‘‹β†‘π‘˜))
17815nn0zd 12530 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (π‘˜ + 1) ∈ β„€)
179178adantr 482 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ (π‘˜ + 1) ∈ β„€)
180168, 169, 179expm1d 14067 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ (𝑋↑((π‘˜ + 1) βˆ’ 1)) = ((𝑋↑(π‘˜ + 1)) / 𝑋))
181177, 180eqtr3d 2775 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ (π‘‹β†‘π‘˜) = ((𝑋↑(π‘˜ + 1)) / 𝑋))
182181oveq2d 7374 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ ((π΄β€˜(π‘˜ + 1)) Β· (π‘‹β†‘π‘˜)) = ((π΄β€˜(π‘˜ + 1)) Β· ((𝑋↑(π‘˜ + 1)) / 𝑋)))
183173, 182eqtr4d 2776 . . . . . . . . . . 11 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ (((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1))) / 𝑋) = ((π΄β€˜(π‘˜ + 1)) Β· (π‘‹β†‘π‘˜)))
184183fveq2d 6847 . . . . . . . . . 10 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ (absβ€˜(((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1))) / 𝑋)) = (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (π‘‹β†‘π‘˜))))
18523abscld 15327 . . . . . . . . . . . . 13 (πœ‘ β†’ (absβ€˜π‘‹) ∈ ℝ)
186185ad2antrr 725 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ (absβ€˜π‘‹) ∈ ℝ)
187186recnd 11188 . . . . . . . . . . 11 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ (absβ€˜π‘‹) ∈ β„‚)
188159, 116sylan 581 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ (absβ€˜π‘‹) ∈ ℝ+)
189188rpne0d 12967 . . . . . . . . . . 11 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ (absβ€˜π‘‹) β‰  0)
190165, 187, 189divrec2d 11940 . . . . . . . . . 10 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ ((absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1)))) / (absβ€˜π‘‹)) = ((1 / (absβ€˜π‘‹)) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1))))))
191170, 184, 1903eqtr3rd 2782 . . . . . . . . 9 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ ((1 / (absβ€˜π‘‹)) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1))))) = (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (π‘‹β†‘π‘˜))))
192191oveq2d 7374 . . . . . . . 8 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ ((π‘˜ + 1) Β· ((1 / (absβ€˜π‘‹)) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1)))))) = ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (π‘‹β†‘π‘˜)))))
193166, 192eqtrd 2773 . . . . . . 7 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ ((1 / (absβ€˜π‘‹)) Β· ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1)))))) = ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (π‘‹β†‘π‘˜)))))
194158, 193breqtrrd 5134 . . . . . 6 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ (absβ€˜(((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) Β· (π‘‹β†‘π‘˜))) ≀ ((1 / (absβ€˜π‘‹)) Β· ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1)))))))
195126, 194sylanl2 680 . . . . 5 (((πœ‘ ∧ π‘˜ ∈ (β„€β‰₯β€˜1)) ∧ 𝑋 β‰  0) β†’ (absβ€˜(((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) Β· (π‘‹β†‘π‘˜))) ≀ ((1 / (absβ€˜π‘‹)) Β· ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1)))))))
196148, 195sylan2br 596 . . . 4 (((πœ‘ ∧ π‘˜ ∈ (β„€β‰₯β€˜1)) ∧ Β¬ 𝑋 = 0) β†’ (absβ€˜(((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) Β· (π‘‹β†‘π‘˜))) ≀ ((1 / (absβ€˜π‘‹)) Β· ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1)))))))
197121, 123, 147, 196ifbothda 4525 . . 3 ((πœ‘ ∧ π‘˜ ∈ (β„€β‰₯β€˜1)) β†’ (absβ€˜(((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) Β· (π‘‹β†‘π‘˜))) ≀ (if(𝑋 = 0, 1, (1 / (absβ€˜π‘‹))) Β· ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1)))))))
19849fveq2d 6847 . . . 4 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (absβ€˜(π»β€˜π‘˜)) = (absβ€˜(((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) Β· (π‘‹β†‘π‘˜))))
199126, 198sylan2 594 . . 3 ((πœ‘ ∧ π‘˜ ∈ (β„€β‰₯β€˜1)) β†’ (absβ€˜(π»β€˜π‘˜)) = (absβ€˜(((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) Β· (π‘‹β†‘π‘˜))))
20030oveq2d 7374 . . . 4 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (if(𝑋 = 0, 1, (1 / (absβ€˜π‘‹))) Β· (((𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)))) shift -1)β€˜π‘˜)) = (if(𝑋 = 0, 1, (1 / (absβ€˜π‘‹))) Β· ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1)))))))
201126, 200sylan2 594 . . 3 ((πœ‘ ∧ π‘˜ ∈ (β„€β‰₯β€˜1)) β†’ (if(𝑋 = 0, 1, (1 / (absβ€˜π‘‹))) Β· (((𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)))) shift -1)β€˜π‘˜)) = (if(𝑋 = 0, 1, (1 / (absβ€˜π‘‹))) Β· ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1)))))))
202197, 199, 2013brtr4d 5138 . 2 ((πœ‘ ∧ π‘˜ ∈ (β„€β‰₯β€˜1)) β†’ (absβ€˜(π»β€˜π‘˜)) ≀ (if(𝑋 = 0, 1, (1 / (absβ€˜π‘‹))) Β· (((𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)))) shift -1)β€˜π‘˜)))
2031, 3, 40, 55, 113, 119, 202cvgcmpce 15708 1 (πœ‘ β†’ seq0( + , 𝐻) ∈ dom ⇝ )
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107   β‰  wne 2940  {crab 3406  ifcif 4487   class class class wbr 5106   ↦ cmpt 5189  dom cdm 5634   ∘ ccom 5638  βŸΆwf 6493  β€˜cfv 6497  (class class class)co 7358  supcsup 9381  β„‚cc 11054  β„cr 11055  0cc0 11056  1c1 11057   + caddc 11059   Β· cmul 11061  β„*cxr 11193   < clt 11194   ≀ cle 11195   βˆ’ cmin 11390  -cneg 11391   / cdiv 11817  β„•cn 12158  β„•0cn0 12418  β„€cz 12504  β„€β‰₯cuz 12768  β„+crp 12920  seqcseq 13912  β†‘cexp 13973   shift cshi 14957  abscabs 15125   ⇝ cli 15372
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 2704  ax-rep 5243  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673  ax-inf2 9582  ax-cnex 11112  ax-resscn 11113  ax-1cn 11114  ax-icn 11115  ax-addcl 11116  ax-addrcl 11117  ax-mulcl 11118  ax-mulrcl 11119  ax-mulcom 11120  ax-addass 11121  ax-mulass 11122  ax-distr 11123  ax-i2m1 11124  ax-1ne0 11125  ax-1rid 11126  ax-rnegex 11127  ax-rrecex 11128  ax-cnre 11129  ax-pre-lttri 11130  ax-pre-lttrn 11131  ax-pre-ltadd 11132  ax-pre-mulgt0 11133  ax-pre-sup 11134
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 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3930  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-int 4909  df-iun 4957  df-br 5107  df-opab 5169  df-mpt 5190  df-tr 5224  df-id 5532  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5589  df-se 5590  df-we 5591  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6254  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-isom 6506  df-riota 7314  df-ov 7361  df-oprab 7362  df-mpo 7363  df-om 7804  df-1st 7922  df-2nd 7923  df-frecs 8213  df-wrecs 8244  df-recs 8318  df-rdg 8357  df-1o 8413  df-er 8651  df-pm 8771  df-en 8887  df-dom 8888  df-sdom 8889  df-fin 8890  df-sup 9383  df-inf 9384  df-oi 9451  df-card 9880  df-pnf 11196  df-mnf 11197  df-xr 11198  df-ltxr 11199  df-le 11200  df-sub 11392  df-neg 11393  df-div 11818  df-nn 12159  df-2 12221  df-3 12222  df-n0 12419  df-z 12505  df-uz 12769  df-rp 12921  df-ico 13276  df-icc 13277  df-fz 13431  df-fzo 13574  df-fl 13703  df-seq 13913  df-exp 13974  df-hash 14237  df-shft 14958  df-cj 14990  df-re 14991  df-im 14992  df-sqrt 15126  df-abs 15127  df-limsup 15359  df-clim 15376  df-rlim 15377  df-sum 15577
This theorem is referenced by:  pserdvlem2  25803  dvradcnv2  42715
  Copyright terms: Public domain W3C validator