MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dvradcnv Structured version   Visualization version   GIF version
Theorem dvradcnv 25940
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 12866 . 2 β„•0 = (β„€β‰₯β€˜0)
2 1nn0 12490 . . 3 1 ∈ β„•0
32a1i 11 . 2 (πœ‘ β†’ 1 ∈ β„•0)
4 ax-1cn 11170 . . . . 5 1 ∈ β„‚
5 nn0cn 12484 . . . . . 6 (π‘˜ ∈ β„•0 β†’ π‘˜ ∈ β„‚)
65adantl 482 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ π‘˜ ∈ β„‚)
7 nn0ex 12480 . . . . . . 7 β„•0 ∈ V
87mptex 7227 . . . . . 6 (𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)))) ∈ V
98shftval4 15026 . . . . 5 ((1 ∈ β„‚ ∧ π‘˜ ∈ β„‚) β†’ (((𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)))) shift -1)β€˜π‘˜) = ((𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–))))β€˜(1 + π‘˜)))
104, 6, 9sylancr 587 . . . 4 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (((𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)))) shift -1)β€˜π‘˜) = ((𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–))))β€˜(1 + π‘˜)))
11 addcom 11402 . . . . . 6 ((1 ∈ β„‚ ∧ π‘˜ ∈ β„‚) β†’ (1 + π‘˜) = (π‘˜ + 1))
124, 6, 11sylancr 587 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (1 + π‘˜) = (π‘˜ + 1))
1312fveq2d 6895 . . . 4 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–))))β€˜(1 + π‘˜)) = ((𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–))))β€˜(π‘˜ + 1)))
14 peano2nn0 12514 . . . . . . 7 (π‘˜ ∈ β„•0 β†’ (π‘˜ + 1) ∈ β„•0)
1514adantl 482 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (π‘˜ + 1) ∈ β„•0)
16 id 22 . . . . . . . 8 (𝑖 = (π‘˜ + 1) β†’ 𝑖 = (π‘˜ + 1))
17 2fveq3 6896 . . . . . . . 8 (𝑖 = (π‘˜ + 1) β†’ (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)) = (absβ€˜((πΊβ€˜π‘‹)β€˜(π‘˜ + 1))))
1816, 17oveq12d 7429 . . . . . . 7 (𝑖 = (π‘˜ + 1) β†’ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–))) = ((π‘˜ + 1) Β· (absβ€˜((πΊβ€˜π‘‹)β€˜(π‘˜ + 1)))))
19 eqid 2732 . . . . . . 7 (𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)))) = (𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–))))
20 ovex 7444 . . . . . . 7 ((π‘˜ + 1) Β· (absβ€˜((πΊβ€˜π‘‹)β€˜(π‘˜ + 1)))) ∈ V
2118, 19, 20fvmpt 6998 . . . . . 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 25930 . . . . . . . 8 ((𝑋 ∈ β„‚ ∧ (π‘˜ + 1) ∈ β„•0) β†’ ((πΊβ€˜π‘‹)β€˜(π‘˜ + 1)) = ((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1))))
2623, 14, 25syl2an 596 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((πΊβ€˜π‘‹)β€˜(π‘˜ + 1)) = ((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1))))
2726fveq2d 6895 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (absβ€˜((πΊβ€˜π‘‹)β€˜(π‘˜ + 1))) = (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1)))))
2827oveq2d 7427 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((π‘˜ + 1) Β· (absβ€˜((πΊβ€˜π‘‹)β€˜(π‘˜ + 1)))) = ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1))))))
2922, 28eqtrd 2772 . . . 4 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–))))β€˜(π‘˜ + 1)) = ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1))))))
3010, 13, 293eqtrd 2776 . . 3 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (((𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)))) shift -1)β€˜π‘˜) = ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1))))))
3115nn0red 12535 . . . 4 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (π‘˜ + 1) ∈ ℝ)
32 dvradcnv.a . . . . . . 7 (πœ‘ β†’ 𝐴:β„•0βŸΆβ„‚)
33 ffvelcdm 7083 . . . . . . 7 ((𝐴:β„•0βŸΆβ„‚ ∧ (π‘˜ + 1) ∈ β„•0) β†’ (π΄β€˜(π‘˜ + 1)) ∈ β„‚)
3432, 14, 33syl2an 596 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (π΄β€˜(π‘˜ + 1)) ∈ β„‚)
35 expcl 14047 . . . . . . 7 ((𝑋 ∈ β„‚ ∧ (π‘˜ + 1) ∈ β„•0) β†’ (𝑋↑(π‘˜ + 1)) ∈ β„‚)
3623, 14, 35syl2an 596 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (𝑋↑(π‘˜ + 1)) ∈ β„‚)
3734, 36mulcld 11236 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1))) ∈ β„‚)
3837abscld 15385 . . . 4 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1)))) ∈ ℝ)
3931, 38remulcld 11246 . . 3 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1))))) ∈ ℝ)
4030, 39eqeltrd 2833 . 2 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (((𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)))) shift -1)β€˜π‘˜) ∈ ℝ)
41 oveq1 7418 . . . . . . 7 (𝑛 = π‘˜ β†’ (𝑛 + 1) = (π‘˜ + 1))
4241fveq2d 6895 . . . . . . 7 (𝑛 = π‘˜ β†’ (π΄β€˜(𝑛 + 1)) = (π΄β€˜(π‘˜ + 1)))
4341, 42oveq12d 7429 . . . . . 6 (𝑛 = π‘˜ β†’ ((𝑛 + 1) Β· (π΄β€˜(𝑛 + 1))) = ((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))))
44 oveq2 7419 . . . . . 6 (𝑛 = π‘˜ β†’ (𝑋↑𝑛) = (π‘‹β†‘π‘˜))
4543, 44oveq12d 7429 . . . . 5 (𝑛 = π‘˜ β†’ (((𝑛 + 1) Β· (π΄β€˜(𝑛 + 1))) Β· (𝑋↑𝑛)) = (((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) Β· (π‘‹β†‘π‘˜)))
46 dvradcnv.h . . . . 5 𝐻 = (𝑛 ∈ β„•0 ↦ (((𝑛 + 1) Β· (π΄β€˜(𝑛 + 1))) Β· (𝑋↑𝑛)))
47 ovex 7444 . . . . 5 (((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) Β· (π‘‹β†‘π‘˜)) ∈ V
4845, 46, 47fvmpt 6998 . . . 4 (π‘˜ ∈ β„•0 β†’ (π»β€˜π‘˜) = (((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) Β· (π‘‹β†‘π‘˜)))
4948adantl 482 . . 3 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (π»β€˜π‘˜) = (((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) Β· (π‘‹β†‘π‘˜)))
5015nn0cnd 12536 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (π‘˜ + 1) ∈ β„‚)
5150, 34mulcld 11236 . . . 4 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) ∈ β„‚)
52 expcl 14047 . . . . 5 ((𝑋 ∈ β„‚ ∧ π‘˜ ∈ β„•0) β†’ (π‘‹β†‘π‘˜) ∈ β„‚)
5323, 52sylan 580 . . . 4 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (π‘‹β†‘π‘˜) ∈ β„‚)
5451, 53mulcld 11236 . . 3 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) Β· (π‘‹β†‘π‘˜)) ∈ β„‚)
5549, 54eqeltrd 2833 . 2 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (π»β€˜π‘˜) ∈ β„‚)
56 dvradcnv.r . . . . . . . 8 𝑅 = sup({π‘Ÿ ∈ ℝ ∣ seq0( + , (πΊβ€˜π‘Ÿ)) ∈ dom ⇝ }, ℝ*, < )
57 dvradcnv.l . . . . . . . 8 (πœ‘ β†’ (absβ€˜π‘‹) < 𝑅)
58 id 22 . . . . . . . . . 10 (𝑖 = π‘˜ β†’ 𝑖 = π‘˜)
59 2fveq3 6896 . . . . . . . . . 10 (𝑖 = π‘˜ β†’ (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)) = (absβ€˜((πΊβ€˜π‘‹)β€˜π‘˜)))
6058, 59oveq12d 7429 . . . . . . . . 9 (𝑖 = π‘˜ β†’ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–))) = (π‘˜ Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘˜))))
6160cbvmptv 5261 . . . . . . . 8 (𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)))) = (π‘˜ ∈ β„•0 ↦ (π‘˜ Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘˜))))
6224, 32, 56, 23, 57, 61radcnvlt1 25937 . . . . . . 7 (πœ‘ β†’ (seq0( + , (𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–))))) ∈ dom ⇝ ∧ seq0( + , (abs ∘ (πΊβ€˜π‘‹))) ∈ dom ⇝ ))
6362simpld 495 . . . . . 6 (πœ‘ β†’ seq0( + , (𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–))))) ∈ dom ⇝ )
64 climdm 15500 . . . . . 6 (seq0( + , (𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–))))) ∈ dom ⇝ ↔ seq0( + , (𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–))))) ⇝ ( ⇝ β€˜seq0( + , (𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)))))))
6563, 64sylib 217 . . . . 5 (πœ‘ β†’ seq0( + , (𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–))))) ⇝ ( ⇝ β€˜seq0( + , (𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)))))))
66 0z 12571 . . . . . 6 0 ∈ β„€
67 neg1z 12600 . . . . . 6 -1 ∈ β„€
688isershft 15612 . . . . . 6 ((0 ∈ β„€ ∧ -1 ∈ β„€) β†’ (seq0( + , (𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–))))) ⇝ ( ⇝ β€˜seq0( + , (𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)))))) ↔ seq(0 + -1)( + , ((𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)))) shift -1)) ⇝ ( ⇝ β€˜seq0( + , (𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–))))))))
6966, 67, 68mp2an 690 . . . . 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 13970 . . . . 5 seq(0 + -1)( + , ((𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)))) shift -1)) ∈ V
72 fvex 6904 . . . . 5 ( ⇝ β€˜seq0( + , (𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)))))) ∈ V
7371, 72breldm 5908 . . . 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 2732 . . . 4 (β„€β‰₯β€˜(0 + -1)) = (β„€β‰₯β€˜(0 + -1))
76 neg1cn 12328 . . . . . . . 8 -1 ∈ β„‚
7776addlidi 11404 . . . . . . 7 (0 + -1) = -1
78 0le1 11739 . . . . . . . 8 0 ≀ 1
79 1re 11216 . . . . . . . . 9 1 ∈ ℝ
80 le0neg2 11725 . . . . . . . . 9 (1 ∈ ℝ β†’ (0 ≀ 1 ↔ -1 ≀ 0))
8179, 80ax-mp 5 . . . . . . . 8 (0 ≀ 1 ↔ -1 ≀ 0)
8278, 81mpbi 229 . . . . . . 7 -1 ≀ 0
8377, 82eqbrtri 5169 . . . . . 6 (0 + -1) ≀ 0
8477, 67eqeltri 2829 . . . . . . 7 (0 + -1) ∈ β„€
8584eluz1i 12832 . . . . . 6 (0 ∈ (β„€β‰₯β€˜(0 + -1)) ↔ (0 ∈ β„€ ∧ (0 + -1) ≀ 0))
8666, 83, 85mpbir2an 709 . . . . 5 0 ∈ (β„€β‰₯β€˜(0 + -1))
8786a1i 11 . . . 4 (πœ‘ β†’ 0 ∈ (β„€β‰₯β€˜(0 + -1)))
88 eluzelcn 12836 . . . . . . 7 (π‘˜ ∈ (β„€β‰₯β€˜(0 + -1)) β†’ π‘˜ ∈ β„‚)
8988adantl 482 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ (β„€β‰₯β€˜(0 + -1))) β†’ π‘˜ ∈ β„‚)
904, 89, 9sylancr 587 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ (β„€β‰₯β€˜(0 + -1))) β†’ (((𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)))) shift -1)β€˜π‘˜) = ((𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–))))β€˜(1 + π‘˜)))
91 nn0re 12483 . . . . . . . . . 10 (𝑖 ∈ β„•0 β†’ 𝑖 ∈ ℝ)
9291adantl 482 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ β„•0) β†’ 𝑖 ∈ ℝ)
9324, 32, 23psergf 25931 . . . . . . . . . . 11 (πœ‘ β†’ (πΊβ€˜π‘‹):β„•0βŸΆβ„‚)
9493ffvelcdmda 7086 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ β„•0) β†’ ((πΊβ€˜π‘‹)β€˜π‘–) ∈ β„‚)
9594abscld 15385 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ β„•0) β†’ (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)) ∈ ℝ)
9692, 95remulcld 11246 . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ β„•0) β†’ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–))) ∈ ℝ)
9796recnd 11244 . . . . . . 7 ((πœ‘ ∧ 𝑖 ∈ β„•0) β†’ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–))) ∈ β„‚)
9897fmpttd 7116 . . . . . 6 (πœ‘ β†’ (𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)))):β„•0βŸΆβ„‚)
994, 88, 11sylancr 587 . . . . . . 7 (π‘˜ ∈ (β„€β‰₯β€˜(0 + -1)) β†’ (1 + π‘˜) = (π‘˜ + 1))
100 eluzp1p1 12852 . . . . . . . 8 (π‘˜ ∈ (β„€β‰₯β€˜(0 + -1)) β†’ (π‘˜ + 1) ∈ (β„€β‰₯β€˜((0 + -1) + 1)))
10177oveq1i 7421 . . . . . . . . . . 11 ((0 + -1) + 1) = (-1 + 1)
102 1pneg1e0 12333 . . . . . . . . . . . 12 (1 + -1) = 0
1034, 76, 102addcomli 11408 . . . . . . . . . . 11 (-1 + 1) = 0
104101, 103eqtri 2760 . . . . . . . . . 10 ((0 + -1) + 1) = 0
105104fveq2i 6894 . . . . . . . . 9 (β„€β‰₯β€˜((0 + -1) + 1)) = (β„€β‰₯β€˜0)
1061, 105eqtr4i 2763 . . . . . . . 8 β„•0 = (β„€β‰₯β€˜((0 + -1) + 1))
107100, 106eleqtrrdi 2844 . . . . . . 7 (π‘˜ ∈ (β„€β‰₯β€˜(0 + -1)) β†’ (π‘˜ + 1) ∈ β„•0)
10899, 107eqeltrd 2833 . . . . . 6 (π‘˜ ∈ (β„€β‰₯β€˜(0 + -1)) β†’ (1 + π‘˜) ∈ β„•0)
109 ffvelcdm 7083 . . . . . 6 (((𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)))):β„•0βŸΆβ„‚ ∧ (1 + π‘˜) ∈ β„•0) β†’ ((𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–))))β€˜(1 + π‘˜)) ∈ β„‚)
11098, 108, 109syl2an 596 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ (β„€β‰₯β€˜(0 + -1))) β†’ ((𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–))))β€˜(1 + π‘˜)) ∈ β„‚)
11190, 110eqeltrd 2833 . . . 4 ((πœ‘ ∧ π‘˜ ∈ (β„€β‰₯β€˜(0 + -1))) β†’ (((𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)))) shift -1)β€˜π‘˜) ∈ β„‚)
11275, 87, 111iserex 15605 . . 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 11217 . . 3 ((πœ‘ ∧ 𝑋 = 0) β†’ 1 ∈ ℝ)
115 neqne 2948 . . . . 5 (Β¬ 𝑋 = 0 β†’ 𝑋 β‰  0)
116 absrpcl 15237 . . . . 5 ((𝑋 ∈ β„‚ ∧ 𝑋 β‰  0) β†’ (absβ€˜π‘‹) ∈ ℝ+)
11723, 115, 116syl2an 596 . . . 4 ((πœ‘ ∧ Β¬ 𝑋 = 0) β†’ (absβ€˜π‘‹) ∈ ℝ+)
118117rprecred 13029 . . 3 ((πœ‘ ∧ Β¬ 𝑋 = 0) β†’ (1 / (absβ€˜π‘‹)) ∈ ℝ)
119114, 118ifclda 4563 . 2 (πœ‘ β†’ if(𝑋 = 0, 1, (1 / (absβ€˜π‘‹))) ∈ ℝ)
120 oveq1 7418 . . . . 5 (1 = if(𝑋 = 0, 1, (1 / (absβ€˜π‘‹))) β†’ (1 Β· ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1)))))) = (if(𝑋 = 0, 1, (1 / (absβ€˜π‘‹))) Β· ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1)))))))
121120breq2d 5160 . . . 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 7418 . . . . 5 ((1 / (absβ€˜π‘‹)) = if(𝑋 = 0, 1, (1 / (absβ€˜π‘‹))) β†’ ((1 / (absβ€˜π‘‹)) Β· ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1)))))) = (if(𝑋 = 0, 1, (1 / (absβ€˜π‘‹))) Β· ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1)))))))
123122breq2d 5160 . . . 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 12868 . . . . . . . 8 (π‘˜ ∈ β„• ↔ π‘˜ ∈ (β„€β‰₯β€˜1))
125 nnnn0 12481 . . . . . . . 8 (π‘˜ ∈ β„• β†’ π‘˜ ∈ β„•0)
126124, 125sylbir 234 . . . . . . 7 (π‘˜ ∈ (β„€β‰₯β€˜1) β†’ π‘˜ ∈ β„•0)
12715nn0ge0d 12537 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ 0 ≀ (π‘˜ + 1))
12837absge0d 15393 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ 0 ≀ (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1)))))
12931, 38, 127, 128mulge0d 11793 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ 0 ≀ ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1))))))
130126, 129sylan2 593 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ (β„€β‰₯β€˜1)) β†’ 0 ≀ ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1))))))
131130adantr 481 . . . . 5 (((πœ‘ ∧ π‘˜ ∈ (β„€β‰₯β€˜1)) ∧ 𝑋 = 0) β†’ 0 ≀ ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1))))))
132 oveq1 7418 . . . . . . . . 9 (𝑋 = 0 β†’ (π‘‹β†‘π‘˜) = (0β†‘π‘˜))
133 simpr 485 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ (β„€β‰₯β€˜1)) β†’ π‘˜ ∈ (β„€β‰₯β€˜1))
134133, 124sylibr 233 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ (β„€β‰₯β€˜1)) β†’ π‘˜ ∈ β„•)
1351340expd 14106 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ (β„€β‰₯β€˜1)) β†’ (0β†‘π‘˜) = 0)
136132, 135sylan9eqr 2794 . . . . . . . 8 (((πœ‘ ∧ π‘˜ ∈ (β„€β‰₯β€˜1)) ∧ 𝑋 = 0) β†’ (π‘‹β†‘π‘˜) = 0)
137136oveq2d 7427 . . . . . . 7 (((πœ‘ ∧ π‘˜ ∈ (β„€β‰₯β€˜1)) ∧ 𝑋 = 0) β†’ (((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) Β· (π‘‹β†‘π‘˜)) = (((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) Β· 0))
13851mul01d 11415 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) Β· 0) = 0)
139126, 138sylan2 593 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ (β„€β‰₯β€˜1)) β†’ (((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) Β· 0) = 0)
140139adantr 481 . . . . . . 7 (((πœ‘ ∧ π‘˜ ∈ (β„€β‰₯β€˜1)) ∧ 𝑋 = 0) β†’ (((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) Β· 0) = 0)
141137, 140eqtrd 2772 . . . . . 6 (((πœ‘ ∧ π‘˜ ∈ (β„€β‰₯β€˜1)) ∧ 𝑋 = 0) β†’ (((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) Β· (π‘‹β†‘π‘˜)) = 0)
142141abs00bd 15240 . . . . 5 (((πœ‘ ∧ π‘˜ ∈ (β„€β‰₯β€˜1)) ∧ 𝑋 = 0) β†’ (absβ€˜(((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) Β· (π‘‹β†‘π‘˜))) = 0)
14339recnd 11244 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1))))) ∈ β„‚)
144143mullidd 11234 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (1 Β· ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1)))))) = ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1))))))
145126, 144sylan2 593 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ (β„€β‰₯β€˜1)) β†’ (1 Β· ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1)))))) = ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1))))))
146145adantr 481 . . . . 5 (((πœ‘ ∧ π‘˜ ∈ (β„€β‰₯β€˜1)) ∧ 𝑋 = 0) β†’ (1 Β· ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1)))))) = ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1))))))
147131, 142, 1463brtr4d 5180 . . . 4 (((πœ‘ ∧ π‘˜ ∈ (β„€β‰₯β€˜1)) ∧ 𝑋 = 0) β†’ (absβ€˜(((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) Β· (π‘‹β†‘π‘˜))) ≀ (1 Β· ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1)))))))
148 df-ne 2941 . . . . 5 (𝑋 β‰  0 ↔ Β¬ 𝑋 = 0)
14954abscld 15385 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (absβ€˜(((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) Β· (π‘‹β†‘π‘˜))) ∈ ℝ)
15050, 34, 53mulassd 11239 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) Β· (π‘‹β†‘π‘˜)) = ((π‘˜ + 1) Β· ((π΄β€˜(π‘˜ + 1)) Β· (π‘‹β†‘π‘˜))))
151150fveq2d 6895 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (absβ€˜(((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) Β· (π‘‹β†‘π‘˜))) = (absβ€˜((π‘˜ + 1) Β· ((π΄β€˜(π‘˜ + 1)) Β· (π‘‹β†‘π‘˜)))))
15234, 53mulcld 11236 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((π΄β€˜(π‘˜ + 1)) Β· (π‘‹β†‘π‘˜)) ∈ β„‚)
15350, 152absmuld 15403 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (absβ€˜((π‘˜ + 1) Β· ((π΄β€˜(π‘˜ + 1)) Β· (π‘‹β†‘π‘˜)))) = ((absβ€˜(π‘˜ + 1)) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (π‘‹β†‘π‘˜)))))
15431, 127absidd 15371 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (absβ€˜(π‘˜ + 1)) = (π‘˜ + 1))
155154oveq1d 7426 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((absβ€˜(π‘˜ + 1)) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (π‘‹β†‘π‘˜)))) = ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (π‘‹β†‘π‘˜)))))
156151, 153, 1553eqtrd 2776 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (absβ€˜(((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) Β· (π‘‹β†‘π‘˜))) = ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (π‘‹β†‘π‘˜)))))
157149, 156eqled 11319 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (absβ€˜(((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) Β· (π‘‹β†‘π‘˜))) ≀ ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (π‘‹β†‘π‘˜)))))
158157adantr 481 . . . . . . 7 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ (absβ€˜(((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) Β· (π‘‹β†‘π‘˜))) ≀ ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (π‘‹β†‘π‘˜)))))
15923adantr 481 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ 𝑋 ∈ β„‚)
160116rpreccld 13028 . . . . . . . . . . 11 ((𝑋 ∈ β„‚ ∧ 𝑋 β‰  0) β†’ (1 / (absβ€˜π‘‹)) ∈ ℝ+)
161159, 160sylan 580 . . . . . . . . . 10 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ (1 / (absβ€˜π‘‹)) ∈ ℝ+)
162161rpcnd 13020 . . . . . . . . 9 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ (1 / (absβ€˜π‘‹)) ∈ β„‚)
16350adantr 481 . . . . . . . . 9 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ (π‘˜ + 1) ∈ β„‚)
16438adantr 481 . . . . . . . . . 10 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1)))) ∈ ℝ)
165164recnd 11244 . . . . . . . . 9 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1)))) ∈ β„‚)
166162, 163, 165mul12d 11425 . . . . . . . 8 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ ((1 / (absβ€˜π‘‹)) Β· ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1)))))) = ((π‘˜ + 1) Β· ((1 / (absβ€˜π‘‹)) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1)))))))
16737adantr 481 . . . . . . . . . . 11 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ ((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1))) ∈ β„‚)
16823ad2antrr 724 . . . . . . . . . . 11 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ 𝑋 ∈ β„‚)
169 simpr 485 . . . . . . . . . . 11 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ 𝑋 β‰  0)
170167, 168, 169absdivd 15404 . . . . . . . . . 10 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ (absβ€˜(((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1))) / 𝑋)) = ((absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1)))) / (absβ€˜π‘‹)))
17134adantr 481 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ (π΄β€˜(π‘˜ + 1)) ∈ β„‚)
17236adantr 481 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ (𝑋↑(π‘˜ + 1)) ∈ β„‚)
173171, 172, 168, 169divassd 12027 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ (((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1))) / 𝑋) = ((π΄β€˜(π‘˜ + 1)) Β· ((𝑋↑(π‘˜ + 1)) / 𝑋)))
1746adantr 481 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ π‘˜ ∈ β„‚)
175 pncan 11468 . . . . . . . . . . . . . . . 16 ((π‘˜ ∈ β„‚ ∧ 1 ∈ β„‚) β†’ ((π‘˜ + 1) βˆ’ 1) = π‘˜)
176174, 4, 175sylancl 586 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ ((π‘˜ + 1) βˆ’ 1) = π‘˜)
177176oveq2d 7427 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ (𝑋↑((π‘˜ + 1) βˆ’ 1)) = (π‘‹β†‘π‘˜))
17815nn0zd 12586 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (π‘˜ + 1) ∈ β„€)
179178adantr 481 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ (π‘˜ + 1) ∈ β„€)
180168, 169, 179expm1d 14123 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ (𝑋↑((π‘˜ + 1) βˆ’ 1)) = ((𝑋↑(π‘˜ + 1)) / 𝑋))
181177, 180eqtr3d 2774 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ (π‘‹β†‘π‘˜) = ((𝑋↑(π‘˜ + 1)) / 𝑋))
182181oveq2d 7427 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ ((π΄β€˜(π‘˜ + 1)) Β· (π‘‹β†‘π‘˜)) = ((π΄β€˜(π‘˜ + 1)) Β· ((𝑋↑(π‘˜ + 1)) / 𝑋)))
183173, 182eqtr4d 2775 . . . . . . . . . . 11 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ (((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1))) / 𝑋) = ((π΄β€˜(π‘˜ + 1)) Β· (π‘‹β†‘π‘˜)))
184183fveq2d 6895 . . . . . . . . . 10 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ (absβ€˜(((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1))) / 𝑋)) = (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (π‘‹β†‘π‘˜))))
18523abscld 15385 . . . . . . . . . . . . 13 (πœ‘ β†’ (absβ€˜π‘‹) ∈ ℝ)
186185ad2antrr 724 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ (absβ€˜π‘‹) ∈ ℝ)
187186recnd 11244 . . . . . . . . . . 11 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ (absβ€˜π‘‹) ∈ β„‚)
188159, 116sylan 580 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ (absβ€˜π‘‹) ∈ ℝ+)
189188rpne0d 13023 . . . . . . . . . . 11 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ (absβ€˜π‘‹) β‰  0)
190165, 187, 189divrec2d 11996 . . . . . . . . . 10 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ ((absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1)))) / (absβ€˜π‘‹)) = ((1 / (absβ€˜π‘‹)) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1))))))
191170, 184, 1903eqtr3rd 2781 . . . . . . . . 9 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ ((1 / (absβ€˜π‘‹)) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1))))) = (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (π‘‹β†‘π‘˜))))
192191oveq2d 7427 . . . . . . . 8 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ ((π‘˜ + 1) Β· ((1 / (absβ€˜π‘‹)) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1)))))) = ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (π‘‹β†‘π‘˜)))))
193166, 192eqtrd 2772 . . . . . . 7 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ ((1 / (absβ€˜π‘‹)) Β· ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1)))))) = ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (π‘‹β†‘π‘˜)))))
194158, 193breqtrrd 5176 . . . . . 6 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ (absβ€˜(((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) Β· (π‘‹β†‘π‘˜))) ≀ ((1 / (absβ€˜π‘‹)) Β· ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1)))))))
195126, 194sylanl2 679 . . . . 5 (((πœ‘ ∧ π‘˜ ∈ (β„€β‰₯β€˜1)) ∧ 𝑋 β‰  0) β†’ (absβ€˜(((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) Β· (π‘‹β†‘π‘˜))) ≀ ((1 / (absβ€˜π‘‹)) Β· ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1)))))))
196148, 195sylan2br 595 . . . 4 (((πœ‘ ∧ π‘˜ ∈ (β„€β‰₯β€˜1)) ∧ Β¬ 𝑋 = 0) β†’ (absβ€˜(((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) Β· (π‘‹β†‘π‘˜))) ≀ ((1 / (absβ€˜π‘‹)) Β· ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1)))))))
197121, 123, 147, 196ifbothda 4566 . . 3 ((πœ‘ ∧ π‘˜ ∈ (β„€β‰₯β€˜1)) β†’ (absβ€˜(((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) Β· (π‘‹β†‘π‘˜))) ≀ (if(𝑋 = 0, 1, (1 / (absβ€˜π‘‹))) Β· ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1)))))))
19849fveq2d 6895 . . . 4 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (absβ€˜(π»β€˜π‘˜)) = (absβ€˜(((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) Β· (π‘‹β†‘π‘˜))))
199126, 198sylan2 593 . . 3 ((πœ‘ ∧ π‘˜ ∈ (β„€β‰₯β€˜1)) β†’ (absβ€˜(π»β€˜π‘˜)) = (absβ€˜(((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) Β· (π‘‹β†‘π‘˜))))
20030oveq2d 7427 . . . 4 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (if(𝑋 = 0, 1, (1 / (absβ€˜π‘‹))) Β· (((𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)))) shift -1)β€˜π‘˜)) = (if(𝑋 = 0, 1, (1 / (absβ€˜π‘‹))) Β· ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1)))))))
201126, 200sylan2 593 . . 3 ((πœ‘ ∧ π‘˜ ∈ (β„€β‰₯β€˜1)) β†’ (if(𝑋 = 0, 1, (1 / (absβ€˜π‘‹))) Β· (((𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)))) shift -1)β€˜π‘˜)) = (if(𝑋 = 0, 1, (1 / (absβ€˜π‘‹))) Β· ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1)))))))
202197, 199, 2013brtr4d 5180 . 2 ((πœ‘ ∧ π‘˜ ∈ (β„€β‰₯β€˜1)) β†’ (absβ€˜(π»β€˜π‘˜)) ≀ (if(𝑋 = 0, 1, (1 / (absβ€˜π‘‹))) Β· (((𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)))) shift -1)β€˜π‘˜)))
2031, 3, 40, 55, 113, 119, 202cvgcmpce 15766 1 (πœ‘ β†’ seq0( + , 𝐻) ∈ dom ⇝ )
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541   ∈ wcel 2106   β‰  wne 2940  {crab 3432  ifcif 4528   class class class wbr 5148   ↦ cmpt 5231  dom cdm 5676   ∘ ccom 5680  βŸΆwf 6539  β€˜cfv 6543  (class class class)co 7411  supcsup 9437  β„‚cc 11110  β„cr 11111  0cc0 11112  1c1 11113   + caddc 11115   Β· cmul 11117  β„*cxr 11249   < clt 11250   ≀ cle 11251   βˆ’ cmin 11446  -cneg 11447   / cdiv 11873  β„•cn 12214  β„•0cn0 12474  β„€cz 12560  β„€β‰₯cuz 12824  β„+crp 12976  seqcseq 13968  β†‘cexp 14029   shift cshi 15015  abscabs 15183   ⇝ cli 15430
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727  ax-inf2 9638  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189  ax-pre-sup 11190
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-er 8705  df-pm 8825  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-sup 9439  df-inf 9440  df-oi 9507  df-card 9936  df-pnf 11252  df-mnf 11253  df-xr 11254  df-ltxr 11255  df-le 11256  df-sub 11448  df-neg 11449  df-div 11874  df-nn 12215  df-2 12277  df-3 12278  df-n0 12475  df-z 12561  df-uz 12825  df-rp 12977  df-ico 13332  df-icc 13333  df-fz 13487  df-fzo 13630  df-fl 13759  df-seq 13969  df-exp 14030  df-hash 14293  df-shft 15016  df-cj 15048  df-re 15049  df-im 15050  df-sqrt 15184  df-abs 15185  df-limsup 15417  df-clim 15434  df-rlim 15435  df-sum 15635
This theorem is referenced by:  pserdvlem2  25947  dvradcnv2  43188
  Copyright terms: Public domain W3C validator