MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dvradcnv Structured version   Visualization version   GIF version
Theorem dvradcnv 26157
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 12868 . 2 β„•0 = (β„€β‰₯β€˜0)
2 1nn0 12492 . . 3 1 ∈ β„•0
32a1i 11 . 2 (πœ‘ β†’ 1 ∈ β„•0)
4 ax-1cn 11170 . . . . 5 1 ∈ β„‚
5 nn0cn 12486 . . . . . 6 (π‘˜ ∈ β„•0 β†’ π‘˜ ∈ β„‚)
65adantl 482 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ π‘˜ ∈ β„‚)
7 nn0ex 12482 . . . . . . 7 β„•0 ∈ V
87mptex 7227 . . . . . 6 (𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)))) ∈ V
98shftval4 15028 . . . . 5 ((1 ∈ β„‚ ∧ π‘˜ ∈ β„‚) β†’ (((𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)))) shift -1)β€˜π‘˜) = ((𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–))))β€˜(1 + π‘˜)))
104, 6, 9sylancr 587 . . . 4 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (((𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)))) shift -1)β€˜π‘˜) = ((𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–))))β€˜(1 + π‘˜)))
11 addcom 11404 . . . . . 6 ((1 ∈ β„‚ ∧ π‘˜ ∈ β„‚) β†’ (1 + π‘˜) = (π‘˜ + 1))
124, 6, 11sylancr 587 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (1 + π‘˜) = (π‘˜ + 1))
1312fveq2d 6895 . . . 4 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–))))β€˜(1 + π‘˜)) = ((𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–))))β€˜(π‘˜ + 1)))
14 peano2nn0 12516 . . . . . . 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 26147 . . . . . . . 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 12537 . . . 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 14049 . . . . . . 7 ((𝑋 ∈ β„‚ ∧ (π‘˜ + 1) ∈ β„•0) β†’ (𝑋↑(π‘˜ + 1)) ∈ β„‚)
3623, 14, 35syl2an 596 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (𝑋↑(π‘˜ + 1)) ∈ β„‚)
3734, 36mulcld 11238 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1))) ∈ β„‚)
3837abscld 15387 . . . 4 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1)))) ∈ ℝ)
3931, 38remulcld 11248 . . 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 12538 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (π‘˜ + 1) ∈ β„‚)
5150, 34mulcld 11238 . . . 4 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) ∈ β„‚)
52 expcl 14049 . . . . 5 ((𝑋 ∈ β„‚ ∧ π‘˜ ∈ β„•0) β†’ (π‘‹β†‘π‘˜) ∈ β„‚)
5323, 52sylan 580 . . . 4 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (π‘‹β†‘π‘˜) ∈ β„‚)
5451, 53mulcld 11238 . . 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 26154 . . . . . . 7 (πœ‘ β†’ (seq0( + , (𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–))))) ∈ dom ⇝ ∧ seq0( + , (abs ∘ (πΊβ€˜π‘‹))) ∈ dom ⇝ ))
6362simpld 495 . . . . . 6 (πœ‘ β†’ seq0( + , (𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–))))) ∈ dom ⇝ )
64 climdm 15502 . . . . . 6 (seq0( + , (𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–))))) ∈ dom ⇝ ↔ seq0( + , (𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–))))) ⇝ ( ⇝ β€˜seq0( + , (𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)))))))
6563, 64sylib 217 . . . . 5 (πœ‘ β†’ seq0( + , (𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–))))) ⇝ ( ⇝ β€˜seq0( + , (𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)))))))
66 0z 12573 . . . . . 6 0 ∈ β„€
67 neg1z 12602 . . . . . 6 -1 ∈ β„€
688isershft 15614 . . . . . 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 13972 . . . . 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 12330 . . . . . . . 8 -1 ∈ β„‚
7776addlidi 11406 . . . . . . 7 (0 + -1) = -1
78 0le1 11741 . . . . . . . 8 0 ≀ 1
79 1re 11218 . . . . . . . . 9 1 ∈ ℝ
80 le0neg2 11727 . . . . . . . . 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 12834 . . . . . 6 (0 ∈ (β„€β‰₯β€˜(0 + -1)) ↔ (0 ∈ β„€ ∧ (0 + -1) ≀ 0))
8666, 83, 85mpbir2an 709 . . . . 5 0 ∈ (β„€β‰₯β€˜(0 + -1))
8786a1i 11 . . . 4 (πœ‘ β†’ 0 ∈ (β„€β‰₯β€˜(0 + -1)))
88 eluzelcn 12838 . . . . . . 7 (π‘˜ ∈ (β„€β‰₯β€˜(0 + -1)) β†’ π‘˜ ∈ β„‚)
8988adantl 482 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ (β„€β‰₯β€˜(0 + -1))) β†’ π‘˜ ∈ β„‚)
904, 89, 9sylancr 587 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ (β„€β‰₯β€˜(0 + -1))) β†’ (((𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)))) shift -1)β€˜π‘˜) = ((𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–))))β€˜(1 + π‘˜)))
91 nn0re 12485 . . . . . . . . . 10 (𝑖 ∈ β„•0 β†’ 𝑖 ∈ ℝ)
9291adantl 482 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ β„•0) β†’ 𝑖 ∈ ℝ)
9324, 32, 23psergf 26148 . . . . . . . . . . 11 (πœ‘ β†’ (πΊβ€˜π‘‹):β„•0βŸΆβ„‚)
9493ffvelcdmda 7086 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ β„•0) β†’ ((πΊβ€˜π‘‹)β€˜π‘–) ∈ β„‚)
9594abscld 15387 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ β„•0) β†’ (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)) ∈ ℝ)
9692, 95remulcld 11248 . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ β„•0) β†’ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–))) ∈ ℝ)
9796recnd 11246 . . . . . . 7 ((πœ‘ ∧ 𝑖 ∈ β„•0) β†’ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–))) ∈ β„‚)
9897fmpttd 7116 . . . . . 6 (πœ‘ β†’ (𝑖 ∈ β„•0 ↦ (𝑖 Β· (absβ€˜((πΊβ€˜π‘‹)β€˜π‘–)))):β„•0βŸΆβ„‚)
994, 88, 11sylancr 587 . . . . . . 7 (π‘˜ ∈ (β„€β‰₯β€˜(0 + -1)) β†’ (1 + π‘˜) = (π‘˜ + 1))
100 eluzp1p1 12854 . . . . . . . 8 (π‘˜ ∈ (β„€β‰₯β€˜(0 + -1)) β†’ (π‘˜ + 1) ∈ (β„€β‰₯β€˜((0 + -1) + 1)))
10177oveq1i 7421 . . . . . . . . . . 11 ((0 + -1) + 1) = (-1 + 1)
102 1pneg1e0 12335 . . . . . . . . . . . 12 (1 + -1) = 0
1034, 76, 102addcomli 11410 . . . . . . . . . . 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 15607 . . 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 11219 . . 3 ((πœ‘ ∧ 𝑋 = 0) β†’ 1 ∈ ℝ)
115 neqne 2948 . . . . 5 (Β¬ 𝑋 = 0 β†’ 𝑋 β‰  0)
116 absrpcl 15239 . . . . 5 ((𝑋 ∈ β„‚ ∧ 𝑋 β‰  0) β†’ (absβ€˜π‘‹) ∈ ℝ+)
11723, 115, 116syl2an 596 . . . 4 ((πœ‘ ∧ Β¬ 𝑋 = 0) β†’ (absβ€˜π‘‹) ∈ ℝ+)
118117rprecred 13031 . . 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 12870 . . . . . . . 8 (π‘˜ ∈ β„• ↔ π‘˜ ∈ (β„€β‰₯β€˜1))
125 nnnn0 12483 . . . . . . . 8 (π‘˜ ∈ β„• β†’ π‘˜ ∈ β„•0)
126124, 125sylbir 234 . . . . . . 7 (π‘˜ ∈ (β„€β‰₯β€˜1) β†’ π‘˜ ∈ β„•0)
12715nn0ge0d 12539 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ 0 ≀ (π‘˜ + 1))
12837absge0d 15395 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ 0 ≀ (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1)))))
12931, 38, 127, 128mulge0d 11795 . . . . . . 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 14108 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ (β„€β‰₯β€˜1)) β†’ (0β†‘π‘˜) = 0)
136132, 135sylan9eqr 2794 . . . . . . . 8 (((πœ‘ ∧ π‘˜ ∈ (β„€β‰₯β€˜1)) ∧ 𝑋 = 0) β†’ (π‘‹β†‘π‘˜) = 0)
137136oveq2d 7427 . . . . . . 7 (((πœ‘ ∧ π‘˜ ∈ (β„€β‰₯β€˜1)) ∧ 𝑋 = 0) β†’ (((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) Β· (π‘‹β†‘π‘˜)) = (((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) Β· 0))
13851mul01d 11417 . . . . . . . . 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 15242 . . . . 5 (((πœ‘ ∧ π‘˜ ∈ (β„€β‰₯β€˜1)) ∧ 𝑋 = 0) β†’ (absβ€˜(((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) Β· (π‘‹β†‘π‘˜))) = 0)
14339recnd 11246 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1))))) ∈ β„‚)
144143mullidd 11236 . . . . . . 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 15387 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (absβ€˜(((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) Β· (π‘‹β†‘π‘˜))) ∈ ℝ)
15050, 34, 53mulassd 11241 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) Β· (π‘‹β†‘π‘˜)) = ((π‘˜ + 1) Β· ((π΄β€˜(π‘˜ + 1)) Β· (π‘‹β†‘π‘˜))))
151150fveq2d 6895 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (absβ€˜(((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) Β· (π‘‹β†‘π‘˜))) = (absβ€˜((π‘˜ + 1) Β· ((π΄β€˜(π‘˜ + 1)) Β· (π‘‹β†‘π‘˜)))))
15234, 53mulcld 11238 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((π΄β€˜(π‘˜ + 1)) Β· (π‘‹β†‘π‘˜)) ∈ β„‚)
15350, 152absmuld 15405 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (absβ€˜((π‘˜ + 1) Β· ((π΄β€˜(π‘˜ + 1)) Β· (π‘‹β†‘π‘˜)))) = ((absβ€˜(π‘˜ + 1)) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (π‘‹β†‘π‘˜)))))
15431, 127absidd 15373 . . . . . . . . . . 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 11321 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (absβ€˜(((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) Β· (π‘‹β†‘π‘˜))) ≀ ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (π‘‹β†‘π‘˜)))))
158157adantr 481 . . . . . . 7 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ (absβ€˜(((π‘˜ + 1) Β· (π΄β€˜(π‘˜ + 1))) Β· (π‘‹β†‘π‘˜))) ≀ ((π‘˜ + 1) Β· (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (π‘‹β†‘π‘˜)))))
15923adantr 481 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ 𝑋 ∈ β„‚)
160116rpreccld 13030 . . . . . . . . . . 11 ((𝑋 ∈ β„‚ ∧ 𝑋 β‰  0) β†’ (1 / (absβ€˜π‘‹)) ∈ ℝ+)
161159, 160sylan 580 . . . . . . . . . 10 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ (1 / (absβ€˜π‘‹)) ∈ ℝ+)
162161rpcnd 13022 . . . . . . . . 9 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ (1 / (absβ€˜π‘‹)) ∈ β„‚)
16350adantr 481 . . . . . . . . 9 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ (π‘˜ + 1) ∈ β„‚)
16438adantr 481 . . . . . . . . . 10 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1)))) ∈ ℝ)
165164recnd 11246 . . . . . . . . 9 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ (absβ€˜((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1)))) ∈ β„‚)
166162, 163, 165mul12d 11427 . . . . . . . 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 15406 . . . . . . . . . 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 12029 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ (((π΄β€˜(π‘˜ + 1)) Β· (𝑋↑(π‘˜ + 1))) / 𝑋) = ((π΄β€˜(π‘˜ + 1)) Β· ((𝑋↑(π‘˜ + 1)) / 𝑋)))
1746adantr 481 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ π‘˜ ∈ β„‚)
175 pncan 11470 . . . . . . . . . . . . . . . 16 ((π‘˜ ∈ β„‚ ∧ 1 ∈ β„‚) β†’ ((π‘˜ + 1) βˆ’ 1) = π‘˜)
176174, 4, 175sylancl 586 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ ((π‘˜ + 1) βˆ’ 1) = π‘˜)
177176oveq2d 7427 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ (𝑋↑((π‘˜ + 1) βˆ’ 1)) = (π‘‹β†‘π‘˜))
17815nn0zd 12588 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (π‘˜ + 1) ∈ β„€)
179178adantr 481 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ (π‘˜ + 1) ∈ β„€)
180168, 169, 179expm1d 14125 . . . . . . . . . . . . . 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 15387 . . . . . . . . . . . . 13 (πœ‘ β†’ (absβ€˜π‘‹) ∈ ℝ)
186185ad2antrr 724 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ (absβ€˜π‘‹) ∈ ℝ)
187186recnd 11246 . . . . . . . . . . 11 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ (absβ€˜π‘‹) ∈ β„‚)
188159, 116sylan 580 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ (absβ€˜π‘‹) ∈ ℝ+)
189188rpne0d 13025 . . . . . . . . . . 11 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑋 β‰  0) β†’ (absβ€˜π‘‹) β‰  0)
190165, 187, 189divrec2d 11998 . . . . . . . . . 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 15768 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 11251   < clt 11252   ≀ cle 11253   βˆ’ cmin 11448  -cneg 11449   / cdiv 11875  β„•cn 12216  β„•0cn0 12476  β„€cz 12562  β„€β‰₯cuz 12826  β„+crp 12978  seqcseq 13970  β†‘cexp 14031   shift cshi 15017  abscabs 15185   ⇝ cli 15432
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 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-div 11876  df-nn 12217  df-2 12279  df-3 12280  df-n0 12477  df-z 12563  df-uz 12827  df-rp 12979  df-ico 13334  df-icc 13335  df-fz 13489  df-fzo 13632  df-fl 13761  df-seq 13971  df-exp 14032  df-hash 14295  df-shft 15018  df-cj 15050  df-re 15051  df-im 15052  df-sqrt 15186  df-abs 15187  df-limsup 15419  df-clim 15436  df-rlim 15437  df-sum 15637
This theorem is referenced by:  pserdvlem2  26164  dvradcnv2  43408
  Copyright terms: Public domain W3C validator