Users' Mathboxes Mathbox for Steve Rodriguez < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  radcnvrat Structured version   Visualization version   GIF version

Theorem radcnvrat 40801
Description: Let 𝐿 be the limit, if one exists, of the ratio (abs‘((𝐴‘(𝑘 + 1)) / (𝐴𝑘))) (as in the ratio test cvgdvgrat 40800) as 𝑘 increases. Then the radius of convergence of power series Σ𝑛 ∈ ℕ0((𝐴𝑛) · (𝑥𝑛)) is (1 / 𝐿) if 𝐿 is nonzero. Proof "The limit involved in the ratio test..." in https://en.wikipedia.org/wiki/Radius_of_convergence 40800 —a few lines that evidently hide quite an involved process to confirm. (Contributed by Steve Rodriguez, 8-Mar-2020.)
Hypotheses
Ref Expression
radcnvrat.g 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑥𝑛))))
radcnvrat.a (𝜑𝐴:ℕ0⟶ℂ)
radcnvrat.r 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ }, ℝ*, < )
radcnvrat.rat 𝐷 = (𝑘 ∈ ℕ0 ↦ (abs‘((𝐴‘(𝑘 + 1)) / (𝐴𝑘))))
radcnvrat.z 𝑍 = (ℤ𝑀)
radcnvrat.m (𝜑𝑀 ∈ ℕ0)
radcnvrat.n0 ((𝜑𝑘𝑍) → (𝐴𝑘) ≠ 0)
radcnvrat.l (𝜑𝐷𝐿)
radcnvrat.ln0 (𝜑𝐿 ≠ 0)
Assertion
Ref Expression
radcnvrat (𝜑𝑅 = (1 / 𝐿))
Distinct variable groups:   𝑘,𝑛,𝑥,𝜑   𝐴,𝑛,𝑥   𝑘,𝐺,𝑛,𝑥   𝑘,𝑟,𝑥,𝐺   𝑘,𝐿,𝑥   𝑘,𝑍,𝑛   𝐷,𝑘   𝑘,𝑀
Allowed substitution hints:   𝜑(𝑟)   𝐴(𝑘,𝑟)   𝐷(𝑥,𝑛,𝑟)   𝑅(𝑥,𝑘,𝑛,𝑟)   𝐿(𝑛,𝑟)   𝑀(𝑥,𝑛,𝑟)   𝑍(𝑥,𝑟)

Proof of Theorem radcnvrat
StepHypRef Expression
1 radcnvrat.r . 2 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ }, ℝ*, < )
2 xrltso 12513 . . . 4 < Or ℝ*
32a1i 11 . . 3 (𝜑 → < Or ℝ*)
4 radcnvrat.z . . . . . 6 𝑍 = (ℤ𝑀)
5 radcnvrat.m . . . . . . 7 (𝜑𝑀 ∈ ℕ0)
65nn0zd 12064 . . . . . 6 (𝜑𝑀 ∈ ℤ)
74reseq2i 5826 . . . . . . 7 (𝐷𝑍) = (𝐷 ↾ (ℤ𝑀))
8 radcnvrat.l . . . . . . . 8 (𝜑𝐷𝐿)
9 radcnvrat.rat . . . . . . . . . 10 𝐷 = (𝑘 ∈ ℕ0 ↦ (abs‘((𝐴‘(𝑘 + 1)) / (𝐴𝑘))))
10 nn0ex 11882 . . . . . . . . . . 11 0 ∈ V
1110mptex 6962 . . . . . . . . . 10 (𝑘 ∈ ℕ0 ↦ (abs‘((𝐴‘(𝑘 + 1)) / (𝐴𝑘)))) ∈ V
129, 11eqeltri 2907 . . . . . . . . 9 𝐷 ∈ V
13 climres 14912 . . . . . . . . 9 ((𝑀 ∈ ℤ ∧ 𝐷 ∈ V) → ((𝐷 ↾ (ℤ𝑀)) ⇝ 𝐿𝐷𝐿))
146, 12, 13sylancl 588 . . . . . . . 8 (𝜑 → ((𝐷 ↾ (ℤ𝑀)) ⇝ 𝐿𝐷𝐿))
158, 14mpbird 259 . . . . . . 7 (𝜑 → (𝐷 ↾ (ℤ𝑀)) ⇝ 𝐿)
167, 15eqbrtrid 5077 . . . . . 6 (𝜑 → (𝐷𝑍) ⇝ 𝐿)
179reseq1i 5825 . . . . . . . . 9 (𝐷𝑍) = ((𝑘 ∈ ℕ0 ↦ (abs‘((𝐴‘(𝑘 + 1)) / (𝐴𝑘)))) ↾ 𝑍)
18 eluznn0 12296 . . . . . . . . . . . . . 14 ((𝑀 ∈ ℕ0𝑘 ∈ (ℤ𝑀)) → 𝑘 ∈ ℕ0)
195, 18sylan 582 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (ℤ𝑀)) → 𝑘 ∈ ℕ0)
2019ex 415 . . . . . . . . . . . 12 (𝜑 → (𝑘 ∈ (ℤ𝑀) → 𝑘 ∈ ℕ0))
2120ssrdv 3952 . . . . . . . . . . 11 (𝜑 → (ℤ𝑀) ⊆ ℕ0)
224, 21eqsstrid 3994 . . . . . . . . . 10 (𝜑𝑍 ⊆ ℕ0)
2322resmptd 5884 . . . . . . . . 9 (𝜑 → ((𝑘 ∈ ℕ0 ↦ (abs‘((𝐴‘(𝑘 + 1)) / (𝐴𝑘)))) ↾ 𝑍) = (𝑘𝑍 ↦ (abs‘((𝐴‘(𝑘 + 1)) / (𝐴𝑘)))))
2417, 23syl5eq 2867 . . . . . . . 8 (𝜑 → (𝐷𝑍) = (𝑘𝑍 ↦ (abs‘((𝐴‘(𝑘 + 1)) / (𝐴𝑘)))))
25 fvexd 6661 . . . . . . . 8 ((𝜑𝑘𝑍) → (abs‘((𝐴‘(𝑘 + 1)) / (𝐴𝑘))) ∈ V)
2624, 25fvmpt2d 6757 . . . . . . 7 ((𝜑𝑘𝑍) → ((𝐷𝑍)‘𝑘) = (abs‘((𝐴‘(𝑘 + 1)) / (𝐴𝑘))))
274peano2uzs 12281 . . . . . . . . . 10 (𝑘𝑍 → (𝑘 + 1) ∈ 𝑍)
2822sselda 3946 . . . . . . . . . . 11 ((𝜑 ∧ (𝑘 + 1) ∈ 𝑍) → (𝑘 + 1) ∈ ℕ0)
29 radcnvrat.a . . . . . . . . . . . 12 (𝜑𝐴:ℕ0⟶ℂ)
3029ffvelrnda 6827 . . . . . . . . . . 11 ((𝜑 ∧ (𝑘 + 1) ∈ ℕ0) → (𝐴‘(𝑘 + 1)) ∈ ℂ)
3128, 30syldan 593 . . . . . . . . . 10 ((𝜑 ∧ (𝑘 + 1) ∈ 𝑍) → (𝐴‘(𝑘 + 1)) ∈ ℂ)
3227, 31sylan2 594 . . . . . . . . 9 ((𝜑𝑘𝑍) → (𝐴‘(𝑘 + 1)) ∈ ℂ)
3322sselda 3946 . . . . . . . . . 10 ((𝜑𝑘𝑍) → 𝑘 ∈ ℕ0)
3429ffvelrnda 6827 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ0) → (𝐴𝑘) ∈ ℂ)
3533, 34syldan 593 . . . . . . . . 9 ((𝜑𝑘𝑍) → (𝐴𝑘) ∈ ℂ)
36 radcnvrat.n0 . . . . . . . . 9 ((𝜑𝑘𝑍) → (𝐴𝑘) ≠ 0)
3732, 35, 36divcld 11394 . . . . . . . 8 ((𝜑𝑘𝑍) → ((𝐴‘(𝑘 + 1)) / (𝐴𝑘)) ∈ ℂ)
3837abscld 14776 . . . . . . 7 ((𝜑𝑘𝑍) → (abs‘((𝐴‘(𝑘 + 1)) / (𝐴𝑘))) ∈ ℝ)
3926, 38eqeltrd 2911 . . . . . 6 ((𝜑𝑘𝑍) → ((𝐷𝑍)‘𝑘) ∈ ℝ)
404, 6, 16, 39climrecl 14920 . . . . 5 (𝜑𝐿 ∈ ℝ)
41 radcnvrat.ln0 . . . . 5 (𝜑𝐿 ≠ 0)
4240, 41rereccld 11445 . . . 4 (𝜑 → (1 / 𝐿) ∈ ℝ)
4342rexrd 10669 . . 3 (𝜑 → (1 / 𝐿) ∈ ℝ*)
44 simpr 487 . . . 4 ((𝜑𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ }) → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ })
45 elrabi 3655 . . . . 5 (𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ } → 𝑥 ∈ ℝ)
4642adantr 483 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ℝ) → (1 / 𝐿) ∈ ℝ)
47 recn 10605 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
4847abscld 14776 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → (abs‘𝑥) ∈ ℝ)
4948adantl 484 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ℝ) → (abs‘𝑥) ∈ ℝ)
5046, 49ltlend 10763 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℝ) → ((1 / 𝐿) < (abs‘𝑥) ↔ ((1 / 𝐿) ≤ (abs‘𝑥) ∧ (abs‘𝑥) ≠ (1 / 𝐿))))
5150simplbda 502 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ) ∧ (1 / 𝐿) < (abs‘𝑥)) → (abs‘𝑥) ≠ (1 / 𝐿))
5250adantr 483 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ ℝ) ∧ (abs‘𝑥) ≠ (1 / 𝐿)) → ((1 / 𝐿) < (abs‘𝑥) ↔ ((1 / 𝐿) ≤ (abs‘𝑥) ∧ (abs‘𝑥) ≠ (1 / 𝐿))))
53 simpr 487 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ ℝ) ∧ (abs‘𝑥) ≠ (1 / 𝐿)) → (abs‘𝑥) ≠ (1 / 𝐿))
5453biantrud 534 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ ℝ) ∧ (abs‘𝑥) ≠ (1 / 𝐿)) → ((1 / 𝐿) ≤ (abs‘𝑥) ↔ ((1 / 𝐿) ≤ (abs‘𝑥) ∧ (abs‘𝑥) ≠ (1 / 𝐿))))
5546, 49lenltd 10764 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ℝ) → ((1 / 𝐿) ≤ (abs‘𝑥) ↔ ¬ (abs‘𝑥) < (1 / 𝐿)))
5655adantr 483 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ ℝ) ∧ (abs‘𝑥) ≠ (1 / 𝐿)) → ((1 / 𝐿) ≤ (abs‘𝑥) ↔ ¬ (abs‘𝑥) < (1 / 𝐿)))
5752, 54, 563bitr2d 309 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℝ) ∧ (abs‘𝑥) ≠ (1 / 𝐿)) → ((1 / 𝐿) < (abs‘𝑥) ↔ ¬ (abs‘𝑥) < (1 / 𝐿)))
58 1cnd 10614 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ ℝ) → 1 ∈ ℂ)
5949recnd 10647 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ ℝ) → (abs‘𝑥) ∈ ℂ)
6040recnd 10647 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐿 ∈ ℂ)
6160adantr 483 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ ℝ) → 𝐿 ∈ ℂ)
6241adantr 483 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ ℝ) → 𝐿 ≠ 0)
6358, 59, 61, 62divmul3d 11428 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ℝ) → ((1 / 𝐿) = (abs‘𝑥) ↔ 1 = ((abs‘𝑥) · 𝐿)))
64 eqcom 2827 . . . . . . . . . . . . . . . . 17 ((1 / 𝐿) = (abs‘𝑥) ↔ (abs‘𝑥) = (1 / 𝐿))
65 eqcom 2827 . . . . . . . . . . . . . . . . 17 (1 = ((abs‘𝑥) · 𝐿) ↔ ((abs‘𝑥) · 𝐿) = 1)
6663, 64, 653bitr3g 315 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ℝ) → ((abs‘𝑥) = (1 / 𝐿) ↔ ((abs‘𝑥) · 𝐿) = 1))
6766necon3bid 3050 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ ℝ) → ((abs‘𝑥) ≠ (1 / 𝐿) ↔ ((abs‘𝑥) · 𝐿) ≠ 1))
6867biimpa 479 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ ℝ) ∧ (abs‘𝑥) ≠ (1 / 𝐿)) → ((abs‘𝑥) · 𝐿) ≠ 1)
69 1red 10620 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ℝ) → 1 ∈ ℝ)
70 fvres 6665 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘𝑍 → ((𝐷𝑍)‘𝑘) = (𝐷𝑘))
7170adantl 484 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘𝑍) → ((𝐷𝑍)‘𝑘) = (𝐷𝑘))
7271, 39eqeltrrd 2912 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘𝑍) → (𝐷𝑘) ∈ ℝ)
7337absge0d 14784 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑘𝑍) → 0 ≤ (abs‘((𝐴‘(𝑘 + 1)) / (𝐴𝑘))))
7473, 26breqtrrd 5070 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘𝑍) → 0 ≤ ((𝐷𝑍)‘𝑘))
7574, 71breqtrd 5068 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘𝑍) → 0 ≤ (𝐷𝑘))
764, 6, 8, 72, 75climge0 14921 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → 0 ≤ 𝐿)
7740, 76, 41ne0gt0d 10755 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 0 < 𝐿)
7840, 77elrpd 12407 . . . . . . . . . . . . . . . . . 18 (𝜑𝐿 ∈ ℝ+)
7978adantr 483 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ℝ) → 𝐿 ∈ ℝ+)
8049, 69, 79ltmuldivd 12457 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ℝ) → (((abs‘𝑥) · 𝐿) < 1 ↔ (abs‘𝑥) < (1 / 𝐿)))
8180adantr 483 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ ℝ) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) → (((abs‘𝑥) · 𝐿) < 1 ↔ (abs‘𝑥) < (1 / 𝐿)))
82 elun 4104 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ((ℝ ∩ {0}) ∪ (ℝ ∖ {0})) ↔ (𝑥 ∈ (ℝ ∩ {0}) ∨ 𝑥 ∈ (ℝ ∖ {0})))
83 inundif 4403 . . . . . . . . . . . . . . . . . . 19 ((ℝ ∩ {0}) ∪ (ℝ ∖ {0})) = ℝ
8483eleq2i 2902 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ((ℝ ∩ {0}) ∪ (ℝ ∖ {0})) ↔ 𝑥 ∈ ℝ)
8582, 84bitr3i 279 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (ℝ ∩ {0}) ∨ 𝑥 ∈ (ℝ ∖ {0})) ↔ 𝑥 ∈ ℝ)
86 elin 3929 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (ℝ ∩ {0}) ↔ (𝑥 ∈ ℝ ∧ 𝑥 ∈ {0}))
8786simprbi 499 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (ℝ ∩ {0}) → 𝑥 ∈ {0})
88 elsni 4560 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ {0} → 𝑥 = 0)
8987, 88syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (ℝ ∩ {0}) → 𝑥 = 0)
90 fveq2 6646 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 0 → (abs‘𝑥) = (abs‘0))
91 abs0 14625 . . . . . . . . . . . . . . . . . . . . . . . . 25 (abs‘0) = 0
9290, 91syl6eq 2871 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 0 → (abs‘𝑥) = 0)
9392oveq1d 7148 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 0 → ((abs‘𝑥) · 𝐿) = (0 · 𝐿))
9460mul02d 10816 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (0 · 𝐿) = 0)
9593, 94sylan9eqr 2877 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 = 0) → ((abs‘𝑥) · 𝐿) = 0)
96 0lt1 11140 . . . . . . . . . . . . . . . . . . . . . 22 0 < 1
9795, 96eqbrtrdi 5081 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 = 0) → ((abs‘𝑥) · 𝐿) < 1)
98 radcnvrat.g . . . . . . . . . . . . . . . . . . . . . . . 24 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑥𝑛))))
9998, 29radcnv0 24990 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → 0 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ })
100 eleq1 2898 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 0 → (𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ } ↔ 0 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ }))
10199, 100syl5ibrcom 249 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑥 = 0 → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ }))
102101imp 409 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 = 0) → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ })
10397, 1022thd 267 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 = 0) → (((abs‘𝑥) · 𝐿) < 1 ↔ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ }))
10489, 103sylan2 594 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (ℝ ∩ {0})) → (((abs‘𝑥) · 𝐿) < 1 ↔ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ }))
105104adantlr 713 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ((abs‘𝑥) · 𝐿) ≠ 1) ∧ 𝑥 ∈ (ℝ ∩ {0})) → (((abs‘𝑥) · 𝐿) < 1 ↔ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ }))
106 ax-resscn 10572 . . . . . . . . . . . . . . . . . . . . . . 23 ℝ ⊆ ℂ
107 ssdif 4095 . . . . . . . . . . . . . . . . . . . . . . 23 (ℝ ⊆ ℂ → (ℝ ∖ {0}) ⊆ (ℂ ∖ {0}))
108106, 107ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 (ℝ ∖ {0}) ⊆ (ℂ ∖ {0})
109108sseli 3942 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (ℝ ∖ {0}) → 𝑥 ∈ (ℂ ∖ {0}))
110 nn0uz 12259 . . . . . . . . . . . . . . . . . . . . . 22 0 = (ℤ‘0)
1115ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑥 ∈ (ℂ ∖ {0})) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) → 𝑀 ∈ ℕ0)
112 fvexd 6661 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑥 ∈ (ℂ ∖ {0})) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) → (𝐺𝑥) ∈ V)
113 eldifi 4082 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 ∈ (ℂ ∖ {0}) → 𝑥 ∈ ℂ)
11498a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑥𝑛)))))
11510mptex 6962 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑥𝑛))) ∈ V
116115a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑥 ∈ ℂ) → (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑥𝑛))) ∈ V)
117114, 116fvmpt2d 6757 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑥 ∈ ℂ) → (𝐺𝑥) = (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑥𝑛))))
118117adantr 483 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (𝐺𝑥) = (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑥𝑛))))
119 fveq2 6646 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 = 𝑘 → (𝐴𝑛) = (𝐴𝑘))
120 oveq2 7141 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 = 𝑘 → (𝑥𝑛) = (𝑥𝑘))
121119, 120oveq12d 7151 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 = 𝑘 → ((𝐴𝑛) · (𝑥𝑛)) = ((𝐴𝑘) · (𝑥𝑘)))
122121adantl 484 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) ∧ 𝑛 = 𝑘) → ((𝐴𝑛) · (𝑥𝑛)) = ((𝐴𝑘) · (𝑥𝑘)))
123 simpr 487 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ ℕ0)
124 ovexd 7168 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → ((𝐴𝑘) · (𝑥𝑘)) ∈ V)
125118, 122, 123, 124fvmptd 6751 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → ((𝐺𝑥)‘𝑘) = ((𝐴𝑘) · (𝑥𝑘)))
12634adantlr 713 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (𝐴𝑘) ∈ ℂ)
127 simplr 767 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → 𝑥 ∈ ℂ)
128127, 123expcld 13495 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (𝑥𝑘) ∈ ℂ)
129126, 128mulcld 10639 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → ((𝐴𝑘) · (𝑥𝑘)) ∈ ℂ)
130125, 129eqeltrd 2911 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → ((𝐺𝑥)‘𝑘) ∈ ℂ)
131113, 130sylanl2 679 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ ℕ0) → ((𝐺𝑥)‘𝑘) ∈ ℂ)
132131adantlr 713 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑥 ∈ (ℂ ∖ {0})) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) ∧ 𝑘 ∈ ℕ0) → ((𝐺𝑥)‘𝑘) ∈ ℂ)
13333adantlr 713 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘𝑍) → 𝑘 ∈ ℕ0)
134133, 125syldan 593 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘𝑍) → ((𝐺𝑥)‘𝑘) = ((𝐴𝑘) · (𝑥𝑘)))
135113, 134sylanl2 679 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘𝑍) → ((𝐺𝑥)‘𝑘) = ((𝐴𝑘) · (𝑥𝑘)))
13635adantlr 713 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘𝑍) → (𝐴𝑘) ∈ ℂ)
137113adantl 484 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑥 ∈ (ℂ ∖ {0})) → 𝑥 ∈ ℂ)
138137adantr 483 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘𝑍) → 𝑥 ∈ ℂ)
13933adantlr 713 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘𝑍) → 𝑘 ∈ ℕ0)
140138, 139expcld 13495 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘𝑍) → (𝑥𝑘) ∈ ℂ)
14136adantlr 713 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘𝑍) → (𝐴𝑘) ≠ 0)
142 eldifsni 4698 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 ∈ (ℂ ∖ {0}) → 𝑥 ≠ 0)
143142ad2antlr 725 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘𝑍) → 𝑥 ≠ 0)
144139nn0zd 12064 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘𝑍) → 𝑘 ∈ ℤ)
145138, 143, 144expne0d 13501 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘𝑍) → (𝑥𝑘) ≠ 0)
146136, 140, 141, 145mulne0d 11270 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘𝑍) → ((𝐴𝑘) · (𝑥𝑘)) ≠ 0)
147135, 146eqnetrd 3073 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘𝑍) → ((𝐺𝑥)‘𝑘) ≠ 0)
148147adantlr 713 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑥 ∈ (ℂ ∖ {0})) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) ∧ 𝑘𝑍) → ((𝐺𝑥)‘𝑘) ≠ 0)
149 fvoveq1 7156 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = 𝑘 → ((𝐺𝑥)‘(𝑛 + 1)) = ((𝐺𝑥)‘(𝑘 + 1)))
150 fveq2 6646 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = 𝑘 → ((𝐺𝑥)‘𝑛) = ((𝐺𝑥)‘𝑘))
151149, 150oveq12d 7151 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = 𝑘 → (((𝐺𝑥)‘(𝑛 + 1)) / ((𝐺𝑥)‘𝑛)) = (((𝐺𝑥)‘(𝑘 + 1)) / ((𝐺𝑥)‘𝑘)))
152151fveq2d 6650 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝑘 → (abs‘(((𝐺𝑥)‘(𝑛 + 1)) / ((𝐺𝑥)‘𝑛))) = (abs‘(((𝐺𝑥)‘(𝑘 + 1)) / ((𝐺𝑥)‘𝑘))))
153152cbvmptv 5145 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛𝑍 ↦ (abs‘(((𝐺𝑥)‘(𝑛 + 1)) / ((𝐺𝑥)‘𝑛)))) = (𝑘𝑍 ↦ (abs‘(((𝐺𝑥)‘(𝑘 + 1)) / ((𝐺𝑥)‘𝑘))))
1544reseq2i 5826 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺𝑥)‘(𝑛 + 1)) / ((𝐺𝑥)‘𝑛)))) ↾ 𝑍) = ((𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺𝑥)‘(𝑛 + 1)) / ((𝐺𝑥)‘𝑛)))) ↾ (ℤ𝑀))
15522adantr 483 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑥 ∈ (ℂ ∖ {0})) → 𝑍 ⊆ ℕ0)
156155resmptd 5884 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑥 ∈ (ℂ ∖ {0})) → ((𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺𝑥)‘(𝑛 + 1)) / ((𝐺𝑥)‘𝑛)))) ↾ 𝑍) = (𝑛𝑍 ↦ (abs‘(((𝐺𝑥)‘(𝑛 + 1)) / ((𝐺𝑥)‘𝑛)))))
157154, 156syl5eqr 2869 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑥 ∈ (ℂ ∖ {0})) → ((𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺𝑥)‘(𝑛 + 1)) / ((𝐺𝑥)‘𝑛)))) ↾ (ℤ𝑀)) = (𝑛𝑍 ↦ (abs‘(((𝐺𝑥)‘(𝑛 + 1)) / ((𝐺𝑥)‘𝑛)))))
1586adantr 483 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑥 ∈ (ℂ ∖ {0})) → 𝑀 ∈ ℤ)
1598adantr 483 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑥 ∈ (ℂ ∖ {0})) → 𝐷𝐿)
160137abscld 14776 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑥 ∈ (ℂ ∖ {0})) → (abs‘𝑥) ∈ ℝ)
161160recnd 10647 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑥 ∈ (ℂ ∖ {0})) → (abs‘𝑥) ∈ ℂ)
16210mptex 6962 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺𝑥)‘(𝑛 + 1)) / ((𝐺𝑥)‘𝑛)))) ∈ V
163162a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑥 ∈ (ℂ ∖ {0})) → (𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺𝑥)‘(𝑛 + 1)) / ((𝐺𝑥)‘𝑛)))) ∈ V)
16472recnd 10647 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑘𝑍) → (𝐷𝑘) ∈ ℂ)
165164adantlr 713 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘𝑍) → (𝐷𝑘) ∈ ℂ)
166 eqidd 2821 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘𝑍) → (𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺𝑥)‘(𝑛 + 1)) / ((𝐺𝑥)‘𝑛)))) = (𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺𝑥)‘(𝑛 + 1)) / ((𝐺𝑥)‘𝑛)))))
167152adantl 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘𝑍) ∧ 𝑛 = 𝑘) → (abs‘(((𝐺𝑥)‘(𝑛 + 1)) / ((𝐺𝑥)‘𝑛))) = (abs‘(((𝐺𝑥)‘(𝑘 + 1)) / ((𝐺𝑥)‘𝑘))))
168 fvexd 6661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘𝑍) → (abs‘(((𝐺𝑥)‘(𝑘 + 1)) / ((𝐺𝑥)‘𝑘))) ∈ V)
169166, 167, 139, 168fvmptd 6751 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘𝑍) → ((𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺𝑥)‘(𝑛 + 1)) / ((𝐺𝑥)‘𝑛))))‘𝑘) = (abs‘(((𝐺𝑥)‘(𝑘 + 1)) / ((𝐺𝑥)‘𝑘))))
170117adantr 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘𝑍) → (𝐺𝑥) = (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑥𝑛))))
171 simpr 487 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝜑𝑥 ∈ ℂ) ∧ 𝑘𝑍) ∧ 𝑛 = (𝑘 + 1)) → 𝑛 = (𝑘 + 1))
172171fveq2d 6650 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑𝑥 ∈ ℂ) ∧ 𝑘𝑍) ∧ 𝑛 = (𝑘 + 1)) → (𝐴𝑛) = (𝐴‘(𝑘 + 1)))
173171oveq2d 7149 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑𝑥 ∈ ℂ) ∧ 𝑘𝑍) ∧ 𝑛 = (𝑘 + 1)) → (𝑥𝑛) = (𝑥↑(𝑘 + 1)))
174172, 173oveq12d 7151 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑𝑥 ∈ ℂ) ∧ 𝑘𝑍) ∧ 𝑛 = (𝑘 + 1)) → ((𝐴𝑛) · (𝑥𝑛)) = ((𝐴‘(𝑘 + 1)) · (𝑥↑(𝑘 + 1))))
175 1nn0 11892 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 1 ∈ ℕ0
176175a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘𝑍) → 1 ∈ ℕ0)
177133, 176nn0addcld 11938 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘𝑍) → (𝑘 + 1) ∈ ℕ0)
178 ovexd 7168 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘𝑍) → ((𝐴‘(𝑘 + 1)) · (𝑥↑(𝑘 + 1))) ∈ V)
179170, 174, 177, 178fvmptd 6751 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘𝑍) → ((𝐺𝑥)‘(𝑘 + 1)) = ((𝐴‘(𝑘 + 1)) · (𝑥↑(𝑘 + 1))))
180121adantl 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑𝑥 ∈ ℂ) ∧ 𝑘𝑍) ∧ 𝑛 = 𝑘) → ((𝐴𝑛) · (𝑥𝑛)) = ((𝐴𝑘) · (𝑥𝑘)))
181 ovexd 7168 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘𝑍) → ((𝐴𝑘) · (𝑥𝑘)) ∈ V)
182170, 180, 133, 181fvmptd 6751 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘𝑍) → ((𝐺𝑥)‘𝑘) = ((𝐴𝑘) · (𝑥𝑘)))
183179, 182oveq12d 7151 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘𝑍) → (((𝐺𝑥)‘(𝑘 + 1)) / ((𝐺𝑥)‘𝑘)) = (((𝐴‘(𝑘 + 1)) · (𝑥↑(𝑘 + 1))) / ((𝐴𝑘) · (𝑥𝑘))))
184113, 183sylanl2 679 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘𝑍) → (((𝐺𝑥)‘(𝑘 + 1)) / ((𝐺𝑥)‘𝑘)) = (((𝐴‘(𝑘 + 1)) · (𝑥↑(𝑘 + 1))) / ((𝐴𝑘) · (𝑥𝑘))))
18532adantlr 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘𝑍) → (𝐴‘(𝑘 + 1)) ∈ ℂ)
186113, 177sylanl2 679 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘𝑍) → (𝑘 + 1) ∈ ℕ0)
187138, 186expcld 13495 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘𝑍) → (𝑥↑(𝑘 + 1)) ∈ ℂ)
188185, 136, 187, 140, 141, 145divmuldivd 11435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘𝑍) → (((𝐴‘(𝑘 + 1)) / (𝐴𝑘)) · ((𝑥↑(𝑘 + 1)) / (𝑥𝑘))) = (((𝐴‘(𝑘 + 1)) · (𝑥↑(𝑘 + 1))) / ((𝐴𝑘) · (𝑥𝑘))))
189139nn0cnd 11936 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘𝑍) → 𝑘 ∈ ℂ)
190 1cnd 10614 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘𝑍) → 1 ∈ ℂ)
191189, 190pncan2d 10977 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘𝑍) → ((𝑘 + 1) − 𝑘) = 1)
192191oveq2d 7149 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘𝑍) → (𝑥↑((𝑘 + 1) − 𝑘)) = (𝑥↑1))
193186nn0zd 12064 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘𝑍) → (𝑘 + 1) ∈ ℤ)
194138, 143, 144, 193expsubd 13506 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘𝑍) → (𝑥↑((𝑘 + 1) − 𝑘)) = ((𝑥↑(𝑘 + 1)) / (𝑥𝑘)))
195138exp1d 13490 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘𝑍) → (𝑥↑1) = 𝑥)
196192, 194, 1953eqtr3d 2863 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘𝑍) → ((𝑥↑(𝑘 + 1)) / (𝑥𝑘)) = 𝑥)
197196oveq2d 7149 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘𝑍) → (((𝐴‘(𝑘 + 1)) / (𝐴𝑘)) · ((𝑥↑(𝑘 + 1)) / (𝑥𝑘))) = (((𝐴‘(𝑘 + 1)) / (𝐴𝑘)) · 𝑥))
198184, 188, 1973eqtr2d 2861 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘𝑍) → (((𝐺𝑥)‘(𝑘 + 1)) / ((𝐺𝑥)‘𝑘)) = (((𝐴‘(𝑘 + 1)) / (𝐴𝑘)) · 𝑥))
199198fveq2d 6650 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘𝑍) → (abs‘(((𝐺𝑥)‘(𝑘 + 1)) / ((𝐺𝑥)‘𝑘))) = (abs‘(((𝐴‘(𝑘 + 1)) / (𝐴𝑘)) · 𝑥)))
20037adantlr 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘𝑍) → ((𝐴‘(𝑘 + 1)) / (𝐴𝑘)) ∈ ℂ)
201200, 138absmuld 14794 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘𝑍) → (abs‘(((𝐴‘(𝑘 + 1)) / (𝐴𝑘)) · 𝑥)) = ((abs‘((𝐴‘(𝑘 + 1)) / (𝐴𝑘))) · (abs‘𝑥)))
202169, 199, 2013eqtrd 2859 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘𝑍) → ((𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺𝑥)‘(𝑛 + 1)) / ((𝐺𝑥)‘𝑛))))‘𝑘) = ((abs‘((𝐴‘(𝑘 + 1)) / (𝐴𝑘))) · (abs‘𝑥)))
20371, 26eqtr3d 2857 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑘𝑍) → (𝐷𝑘) = (abs‘((𝐴‘(𝑘 + 1)) / (𝐴𝑘))))
204203adantlr 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘𝑍) → (𝐷𝑘) = (abs‘((𝐴‘(𝑘 + 1)) / (𝐴𝑘))))
205204eqcomd 2826 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘𝑍) → (abs‘((𝐴‘(𝑘 + 1)) / (𝐴𝑘))) = (𝐷𝑘))
206205oveq1d 7148 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘𝑍) → ((abs‘((𝐴‘(𝑘 + 1)) / (𝐴𝑘))) · (abs‘𝑥)) = ((𝐷𝑘) · (abs‘𝑥)))
207161adantr 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘𝑍) → (abs‘𝑥) ∈ ℂ)
208165, 207mulcomd 10640 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘𝑍) → ((𝐷𝑘) · (abs‘𝑥)) = ((abs‘𝑥) · (𝐷𝑘)))
209202, 206, 2083eqtrd 2859 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘𝑍) → ((𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺𝑥)‘(𝑛 + 1)) / ((𝐺𝑥)‘𝑛))))‘𝑘) = ((abs‘𝑥) · (𝐷𝑘)))
2104, 158, 159, 161, 163, 165, 209climmulc2 14973 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑥 ∈ (ℂ ∖ {0})) → (𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺𝑥)‘(𝑛 + 1)) / ((𝐺𝑥)‘𝑛)))) ⇝ ((abs‘𝑥) · 𝐿))
211 climres 14912 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑀 ∈ ℤ ∧ (𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺𝑥)‘(𝑛 + 1)) / ((𝐺𝑥)‘𝑛)))) ∈ V) → (((𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺𝑥)‘(𝑛 + 1)) / ((𝐺𝑥)‘𝑛)))) ↾ (ℤ𝑀)) ⇝ ((abs‘𝑥) · 𝐿) ↔ (𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺𝑥)‘(𝑛 + 1)) / ((𝐺𝑥)‘𝑛)))) ⇝ ((abs‘𝑥) · 𝐿)))
212158, 162, 211sylancl 588 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑥 ∈ (ℂ ∖ {0})) → (((𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺𝑥)‘(𝑛 + 1)) / ((𝐺𝑥)‘𝑛)))) ↾ (ℤ𝑀)) ⇝ ((abs‘𝑥) · 𝐿) ↔ (𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺𝑥)‘(𝑛 + 1)) / ((𝐺𝑥)‘𝑛)))) ⇝ ((abs‘𝑥) · 𝐿)))
213210, 212mpbird 259 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑥 ∈ (ℂ ∖ {0})) → ((𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺𝑥)‘(𝑛 + 1)) / ((𝐺𝑥)‘𝑛)))) ↾ (ℤ𝑀)) ⇝ ((abs‘𝑥) · 𝐿))
214157, 213eqbrtrrd 5066 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥 ∈ (ℂ ∖ {0})) → (𝑛𝑍 ↦ (abs‘(((𝐺𝑥)‘(𝑛 + 1)) / ((𝐺𝑥)‘𝑛)))) ⇝ ((abs‘𝑥) · 𝐿))
215214adantr 483 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑥 ∈ (ℂ ∖ {0})) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) → (𝑛𝑍 ↦ (abs‘(((𝐺𝑥)‘(𝑛 + 1)) / ((𝐺𝑥)‘𝑛)))) ⇝ ((abs‘𝑥) · 𝐿))
216 simpr 487 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑥 ∈ (ℂ ∖ {0})) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) → ((abs‘𝑥) · 𝐿) ≠ 1)
217110, 4, 111, 112, 132, 148, 153, 215, 216cvgdvgrat 40800 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥 ∈ (ℂ ∖ {0})) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) → (((abs‘𝑥) · 𝐿) < 1 ↔ seq0( + , (𝐺𝑥)) ∈ dom ⇝ ))
218109, 217sylanl2 679 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ (ℝ ∖ {0})) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) → (((abs‘𝑥) · 𝐿) < 1 ↔ seq0( + , (𝐺𝑥)) ∈ dom ⇝ ))
219 eldifi 4082 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (ℝ ∖ {0}) → 𝑥 ∈ ℝ)
220 fveq2 6646 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑟 = 𝑥 → (𝐺𝑟) = (𝐺𝑥))
221220seqeq3d 13361 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑟 = 𝑥 → seq0( + , (𝐺𝑟)) = seq0( + , (𝐺𝑥)))
222221eleq1d 2895 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑟 = 𝑥 → (seq0( + , (𝐺𝑟)) ∈ dom ⇝ ↔ seq0( + , (𝐺𝑥)) ∈ dom ⇝ ))
223222elrab3 3661 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℝ → (𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ } ↔ seq0( + , (𝐺𝑥)) ∈ dom ⇝ ))
224219, 223syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (ℝ ∖ {0}) → (𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ } ↔ seq0( + , (𝐺𝑥)) ∈ dom ⇝ ))
225224ad2antlr 725 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ (ℝ ∖ {0})) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) → (𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ } ↔ seq0( + , (𝐺𝑥)) ∈ dom ⇝ ))
226218, 225bitr4d 284 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (ℝ ∖ {0})) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) → (((abs‘𝑥) · 𝐿) < 1 ↔ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ }))
227226an32s 650 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ((abs‘𝑥) · 𝐿) ≠ 1) ∧ 𝑥 ∈ (ℝ ∖ {0})) → (((abs‘𝑥) · 𝐿) < 1 ↔ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ }))
228105, 227jaodan 954 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ((abs‘𝑥) · 𝐿) ≠ 1) ∧ (𝑥 ∈ (ℝ ∩ {0}) ∨ 𝑥 ∈ (ℝ ∖ {0}))) → (((abs‘𝑥) · 𝐿) < 1 ↔ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ }))
22985, 228sylan2br 596 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ((abs‘𝑥) · 𝐿) ≠ 1) ∧ 𝑥 ∈ ℝ) → (((abs‘𝑥) · 𝐿) < 1 ↔ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ }))
230229an32s 650 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ ℝ) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) → (((abs‘𝑥) · 𝐿) < 1 ↔ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ }))
23181, 230bitr3d 283 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ ℝ) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) → ((abs‘𝑥) < (1 / 𝐿) ↔ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ }))
23268, 231syldan 593 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ ℝ) ∧ (abs‘𝑥) ≠ (1 / 𝐿)) → ((abs‘𝑥) < (1 / 𝐿) ↔ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ }))
233232notbid 320 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℝ) ∧ (abs‘𝑥) ≠ (1 / 𝐿)) → (¬ (abs‘𝑥) < (1 / 𝐿) ↔ ¬ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ }))
23457, 233bitrd 281 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ) ∧ (abs‘𝑥) ≠ (1 / 𝐿)) → ((1 / 𝐿) < (abs‘𝑥) ↔ ¬ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ }))
235234biimpd 231 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ) ∧ (abs‘𝑥) ≠ (1 / 𝐿)) → ((1 / 𝐿) < (abs‘𝑥) → ¬ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ }))
236235impancom 454 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ) ∧ (1 / 𝐿) < (abs‘𝑥)) → ((abs‘𝑥) ≠ (1 / 𝐿) → ¬ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ }))
23751, 236mpd 15 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ) ∧ (1 / 𝐿) < (abs‘𝑥)) → ¬ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ })
238237ex 415 . . . . . . 7 ((𝜑𝑥 ∈ ℝ) → ((1 / 𝐿) < (abs‘𝑥) → ¬ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ }))
239238con2d 136 . . . . . 6 ((𝜑𝑥 ∈ ℝ) → (𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ } → ¬ (1 / 𝐿) < (abs‘𝑥)))
24046adantr 483 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ) ∧ (1 / 𝐿) < 𝑥) → (1 / 𝐿) ∈ ℝ)
241 simplr 767 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ) ∧ (1 / 𝐿) < 𝑥) → 𝑥 ∈ ℝ)
24249adantr 483 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ) ∧ (1 / 𝐿) < 𝑥) → (abs‘𝑥) ∈ ℝ)
243 simpr 487 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ) ∧ (1 / 𝐿) < 𝑥) → (1 / 𝐿) < 𝑥)
244241leabsd 14754 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ) ∧ (1 / 𝐿) < 𝑥) → 𝑥 ≤ (abs‘𝑥))
245240, 241, 242, 243, 244ltletrd 10778 . . . . . . 7 (((𝜑𝑥 ∈ ℝ) ∧ (1 / 𝐿) < 𝑥) → (1 / 𝐿) < (abs‘𝑥))
246245ex 415 . . . . . 6 ((𝜑𝑥 ∈ ℝ) → ((1 / 𝐿) < 𝑥 → (1 / 𝐿) < (abs‘𝑥)))
247239, 246nsyld 159 . . . . 5 ((𝜑𝑥 ∈ ℝ) → (𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ } → ¬ (1 / 𝐿) < 𝑥))
24845, 247sylan2 594 . . . 4 ((𝜑𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ }) → (𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ } → ¬ (1 / 𝐿) < 𝑥))
24944, 248mpd 15 . . 3 ((𝜑𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ }) → ¬ (1 / 𝐿) < 𝑥)
25042renegcld 11045 . . . . . . . . 9 (𝜑 → -(1 / 𝐿) ∈ ℝ)
251250rexrd 10669 . . . . . . . 8 (𝜑 → -(1 / 𝐿) ∈ ℝ*)
252 iooss1 12752 . . . . . . . 8 ((-(1 / 𝐿) ∈ ℝ* ∧ -(1 / 𝐿) ≤ 𝑥) → (𝑥(,)(1 / 𝐿)) ⊆ (-(1 / 𝐿)(,)(1 / 𝐿)))
253251, 252sylan 582 . . . . . . 7 ((𝜑 ∧ -(1 / 𝐿) ≤ 𝑥) → (𝑥(,)(1 / 𝐿)) ⊆ (-(1 / 𝐿)(,)(1 / 𝐿)))
254253adantlr 713 . . . . . 6 (((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < (1 / 𝐿))) ∧ -(1 / 𝐿) ≤ 𝑥) → (𝑥(,)(1 / 𝐿)) ⊆ (-(1 / 𝐿)(,)(1 / 𝐿)))
255 eliooord 12775 . . . . . . . . . . 11 (𝑘 ∈ (𝑥(,)(1 / 𝐿)) → (𝑥 < 𝑘𝑘 < (1 / 𝐿)))
256255simpld 497 . . . . . . . . . 10 (𝑘 ∈ (𝑥(,)(1 / 𝐿)) → 𝑥 < 𝑘)
257256rgen 3135 . . . . . . . . 9 𝑘 ∈ (𝑥(,)(1 / 𝐿))𝑥 < 𝑘
258 ioon0 12743 . . . . . . . . . . . . 13 ((𝑥 ∈ ℝ* ∧ (1 / 𝐿) ∈ ℝ*) → ((𝑥(,)(1 / 𝐿)) ≠ ∅ ↔ 𝑥 < (1 / 𝐿)))
25943, 258sylan2 594 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ*𝜑) → ((𝑥(,)(1 / 𝐿)) ≠ ∅ ↔ 𝑥 < (1 / 𝐿)))
260259ancoms 461 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ℝ*) → ((𝑥(,)(1 / 𝐿)) ≠ ∅ ↔ 𝑥 < (1 / 𝐿)))
261260biimpar 480 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ*) ∧ 𝑥 < (1 / 𝐿)) → (𝑥(,)(1 / 𝐿)) ≠ ∅)
262 r19.2zb 4417 . . . . . . . . . 10 ((𝑥(,)(1 / 𝐿)) ≠ ∅ ↔ (∀𝑘 ∈ (𝑥(,)(1 / 𝐿))𝑥 < 𝑘 → ∃𝑘 ∈ (𝑥(,)(1 / 𝐿))𝑥 < 𝑘))
263261, 262sylib 220 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ*) ∧ 𝑥 < (1 / 𝐿)) → (∀𝑘 ∈ (𝑥(,)(1 / 𝐿))𝑥 < 𝑘 → ∃𝑘 ∈ (𝑥(,)(1 / 𝐿))𝑥 < 𝑘))
264257, 263mpi 20 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ*) ∧ 𝑥 < (1 / 𝐿)) → ∃𝑘 ∈ (𝑥(,)(1 / 𝐿))𝑥 < 𝑘)
265264anasss 469 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < (1 / 𝐿))) → ∃𝑘 ∈ (𝑥(,)(1 / 𝐿))𝑥 < 𝑘)
266265adantr 483 . . . . . 6 (((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < (1 / 𝐿))) ∧ -(1 / 𝐿) ≤ 𝑥) → ∃𝑘 ∈ (𝑥(,)(1 / 𝐿))𝑥 < 𝑘)
267 ssrexv 4013 . . . . . 6 ((𝑥(,)(1 / 𝐿)) ⊆ (-(1 / 𝐿)(,)(1 / 𝐿)) → (∃𝑘 ∈ (𝑥(,)(1 / 𝐿))𝑥 < 𝑘 → ∃𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘))
268254, 266, 267sylc 65 . . . . 5 (((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < (1 / 𝐿))) ∧ -(1 / 𝐿) ≤ 𝑥) → ∃𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘)
269 simplr 767 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ*) ∧ ¬ -(1 / 𝐿) ≤ 𝑥) → 𝑥 ∈ ℝ*)
270 xrltnle 10686 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℝ* ∧ -(1 / 𝐿) ∈ ℝ*) → (𝑥 < -(1 / 𝐿) ↔ ¬ -(1 / 𝐿) ≤ 𝑥))
271 xrltle 12521 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℝ* ∧ -(1 / 𝐿) ∈ ℝ*) → (𝑥 < -(1 / 𝐿) → 𝑥 ≤ -(1 / 𝐿)))
272270, 271sylbird 262 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℝ* ∧ -(1 / 𝐿) ∈ ℝ*) → (¬ -(1 / 𝐿) ≤ 𝑥𝑥 ≤ -(1 / 𝐿)))
273251, 272sylan2 594 . . . . . . . . . . . . 13 ((𝑥 ∈ ℝ*𝜑) → (¬ -(1 / 𝐿) ≤ 𝑥𝑥 ≤ -(1 / 𝐿)))
274273ancoms 461 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ℝ*) → (¬ -(1 / 𝐿) ≤ 𝑥𝑥 ≤ -(1 / 𝐿)))
275274imp 409 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ*) ∧ ¬ -(1 / 𝐿) ≤ 𝑥) → 𝑥 ≤ -(1 / 𝐿))
276 iooss1 12752 . . . . . . . . . . 11 ((𝑥 ∈ ℝ*𝑥 ≤ -(1 / 𝐿)) → (-(1 / 𝐿)(,)(1 / 𝐿)) ⊆ (𝑥(,)(1 / 𝐿)))
277269, 275, 276syl2anc 586 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ*) ∧ ¬ -(1 / 𝐿) ≤ 𝑥) → (-(1 / 𝐿)(,)(1 / 𝐿)) ⊆ (𝑥(,)(1 / 𝐿)))
278277sselda 3946 . . . . . . . . 9 ((((𝜑𝑥 ∈ ℝ*) ∧ ¬ -(1 / 𝐿) ≤ 𝑥) ∧ 𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))) → 𝑘 ∈ (𝑥(,)(1 / 𝐿)))
279278, 256syl 17 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ*) ∧ ¬ -(1 / 𝐿) ≤ 𝑥) ∧ 𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))) → 𝑥 < 𝑘)
280279ralrimiva 3169 . . . . . . 7 (((𝜑𝑥 ∈ ℝ*) ∧ ¬ -(1 / 𝐿) ≤ 𝑥) → ∀𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘)
28140, 77recgt0d 11552 . . . . . . . . . . . . 13 (𝜑 → 0 < (1 / 𝐿))
28242, 42, 281, 281addgt0d 11193 . . . . . . . . . . . 12 (𝜑 → 0 < ((1 / 𝐿) + (1 / 𝐿)))
28342recnd 10647 . . . . . . . . . . . . 13 (𝜑 → (1 / 𝐿) ∈ ℂ)
284283, 283subnegd 10982 . . . . . . . . . . . 12 (𝜑 → ((1 / 𝐿) − -(1 / 𝐿)) = ((1 / 𝐿) + (1 / 𝐿)))
285282, 284breqtrrd 5070 . . . . . . . . . . 11 (𝜑 → 0 < ((1 / 𝐿) − -(1 / 𝐿)))
286250, 42posdifd 11205 . . . . . . . . . . 11 (𝜑 → (-(1 / 𝐿) < (1 / 𝐿) ↔ 0 < ((1 / 𝐿) − -(1 / 𝐿))))
287285, 286mpbird 259 . . . . . . . . . 10 (𝜑 → -(1 / 𝐿) < (1 / 𝐿))
288 ioon0 12743 . . . . . . . . . . 11 ((-(1 / 𝐿) ∈ ℝ* ∧ (1 / 𝐿) ∈ ℝ*) → ((-(1 / 𝐿)(,)(1 / 𝐿)) ≠ ∅ ↔ -(1 / 𝐿) < (1 / 𝐿)))
289251, 43, 288syl2anc 586 . . . . . . . . . 10 (𝜑 → ((-(1 / 𝐿)(,)(1 / 𝐿)) ≠ ∅ ↔ -(1 / 𝐿) < (1 / 𝐿)))
290287, 289mpbird 259 . . . . . . . . 9 (𝜑 → (-(1 / 𝐿)(,)(1 / 𝐿)) ≠ ∅)
291 r19.2zb 4417 . . . . . . . . 9 ((-(1 / 𝐿)(,)(1 / 𝐿)) ≠ ∅ ↔ (∀𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘 → ∃𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘))
292290, 291sylib 220 . . . . . . . 8 (𝜑 → (∀𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘 → ∃𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘))
293292ad2antrr 724 . . . . . . 7 (((𝜑𝑥 ∈ ℝ*) ∧ ¬ -(1 / 𝐿) ≤ 𝑥) → (∀𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘 → ∃𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘))
294280, 293mpd 15 . . . . . 6 (((𝜑𝑥 ∈ ℝ*) ∧ ¬ -(1 / 𝐿) ≤ 𝑥) → ∃𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘)
295294adantlrr 719 . . . . 5 (((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < (1 / 𝐿))) ∧ ¬ -(1 / 𝐿) ≤ 𝑥) → ∃𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘)
296268, 295pm2.61dan 811 . . . 4 ((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < (1 / 𝐿))) → ∃𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘)
297 elioo2 12758 . . . . . . . . . . 11 ((-(1 / 𝐿) ∈ ℝ* ∧ (1 / 𝐿) ∈ ℝ*) → (𝑥 ∈ (-(1 / 𝐿)(,)(1 / 𝐿)) ↔ (𝑥 ∈ ℝ ∧ -(1 / 𝐿) < 𝑥𝑥 < (1 / 𝐿))))
298251, 43, 297syl2anc 586 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ (-(1 / 𝐿)(,)(1 / 𝐿)) ↔ (𝑥 ∈ ℝ ∧ -(1 / 𝐿) < 𝑥𝑥 < (1 / 𝐿))))
299298biimpa 479 . . . . . . . . 9 ((𝜑𝑥 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))) → (𝑥 ∈ ℝ ∧ -(1 / 𝐿) < 𝑥𝑥 < (1 / 𝐿)))
300 simpr 487 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
301300, 46absltd 14769 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ℝ) → ((abs‘𝑥) < (1 / 𝐿) ↔ (-(1 / 𝐿) < 𝑥𝑥 < (1 / 𝐿))))
30249adantr 483 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ ℝ) ∧ (abs‘𝑥) < (1 / 𝐿)) → (abs‘𝑥) ∈ ℝ)
303 simpr 487 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ ℝ) ∧ (abs‘𝑥) < (1 / 𝐿)) → (abs‘𝑥) < (1 / 𝐿))
304302, 303ltned 10754 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ ℝ) ∧ (abs‘𝑥) < (1 / 𝐿)) → (abs‘𝑥) ≠ (1 / 𝐿))
305232biimpd 231 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ ℝ) ∧ (abs‘𝑥) ≠ (1 / 𝐿)) → ((abs‘𝑥) < (1 / 𝐿) → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ }))
306305impancom 454 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ ℝ) ∧ (abs‘𝑥) < (1 / 𝐿)) → ((abs‘𝑥) ≠ (1 / 𝐿) → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ }))
307304, 306mpd 15 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ ℝ) ∧ (abs‘𝑥) < (1 / 𝐿)) → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ })
308307ex 415 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ℝ) → ((abs‘𝑥) < (1 / 𝐿) → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ }))
309301, 308sylbird 262 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ℝ) → ((-(1 / 𝐿) < 𝑥𝑥 < (1 / 𝐿)) → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ }))
310309impr 457 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ ℝ ∧ (-(1 / 𝐿) < 𝑥𝑥 < (1 / 𝐿)))) → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ })
311310expcom 416 . . . . . . . . . . 11 ((𝑥 ∈ ℝ ∧ (-(1 / 𝐿) < 𝑥𝑥 < (1 / 𝐿))) → (𝜑𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ }))
3123113impb 1111 . . . . . . . . . 10 ((𝑥 ∈ ℝ ∧ -(1 / 𝐿) < 𝑥𝑥 < (1 / 𝐿)) → (𝜑𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ }))
313312impcom 410 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ℝ ∧ -(1 / 𝐿) < 𝑥𝑥 < (1 / 𝐿))) → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ })
314299, 313syldan 593 . . . . . . . 8 ((𝜑𝑥 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))) → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ })
315314ex 415 . . . . . . 7 (𝜑 → (𝑥 ∈ (-(1 / 𝐿)(,)(1 / 𝐿)) → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ }))
316315ssrdv 3952 . . . . . 6 (𝜑 → (-(1 / 𝐿)(,)(1 / 𝐿)) ⊆ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ })
317 ssrexv 4013 . . . . . 6 ((-(1 / 𝐿)(,)(1 / 𝐿)) ⊆ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ } → (∃𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘 → ∃𝑘 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ }𝑥 < 𝑘))
318316, 317syl 17 . . . . 5 (𝜑 → (∃𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘 → ∃𝑘 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ }𝑥 < 𝑘))
319318adantr 483 . . . 4 ((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < (1 / 𝐿))) → (∃𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘 → ∃𝑘 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ }𝑥 < 𝑘))
320296, 319mpd 15 . . 3 ((𝜑 ∧ (𝑥 ∈ ℝ*𝑥 < (1 / 𝐿))) → ∃𝑘 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ }𝑥 < 𝑘)
3213, 43, 249, 320eqsupd 8899 . 2 (𝜑 → sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ }, ℝ*, < ) = (1 / 𝐿))
3221, 321syl5eq 2867 1 (𝜑𝑅 = (1 / 𝐿))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 208  wa 398  wo 843  w3a 1083   = wceq 1537  wcel 2114  wne 3006  wral 3125  wrex 3126  {crab 3129  Vcvv 3473  cdif 3910  cun 3911  cin 3912  wss 3913  c0 4269  {csn 4543   class class class wbr 5042  cmpt 5122   Or wor 5449  dom cdm 5531  cres 5533  wf 6327  cfv 6331  (class class class)co 7133  supcsup 8882  cc 10513  cr 10514  0cc0 10515  1c1 10516   + caddc 10518   · cmul 10520  *cxr 10652   < clt 10653  cle 10654  cmin 10848  -cneg 10849   / cdiv 11275  0cn0 11876  cz 11960  cuz 12222  +crp 12368  (,)cioo 12717  seqcseq 13353  cexp 13414  abscabs 14573  cli 14821
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792  ax-rep 5166  ax-sep 5179  ax-nul 5186  ax-pow 5242  ax-pr 5306  ax-un 7439  ax-inf2 9082  ax-cnex 10571  ax-resscn 10572  ax-1cn 10573  ax-icn 10574  ax-addcl 10575  ax-addrcl 10576  ax-mulcl 10577  ax-mulrcl 10578  ax-mulcom 10579  ax-addass 10580  ax-mulass 10581  ax-distr 10582  ax-i2m1 10583  ax-1ne0 10584  ax-1rid 10585  ax-rnegex 10586  ax-rrecex 10587  ax-cnre 10588  ax-pre-lttri 10589  ax-pre-lttrn 10590  ax-pre-ltadd 10591  ax-pre-mulgt0 10592  ax-pre-sup 10593  ax-addf 10594  ax-mulf 10595
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-fal 1550  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ne 3007  df-nel 3111  df-ral 3130  df-rex 3131  df-reu 3132  df-rmo 3133  df-rab 3134  df-v 3475  df-sbc 3753  df-csb 3861  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3932  df-nul 4270  df-if 4444  df-pw 4517  df-sn 4544  df-pr 4546  df-tp 4548  df-op 4550  df-uni 4815  df-int 4853  df-iun 4897  df-br 5043  df-opab 5105  df-mpt 5123  df-tr 5149  df-id 5436  df-eprel 5441  df-po 5450  df-so 5451  df-fr 5490  df-se 5491  df-we 5492  df-xp 5537  df-rel 5538  df-cnv 5539  df-co 5540  df-dm 5541  df-rn 5542  df-res 5543  df-ima 5544  df-pred 6124  df-ord 6170  df-on 6171  df-lim 6172  df-suc 6173  df-iota 6290  df-fun 6333  df-fn 6334  df-f 6335  df-f1 6336  df-fo 6337  df-f1o 6338  df-fv 6339  df-isom 6340  df-riota 7091  df-ov 7136  df-oprab 7137  df-mpo 7138  df-om 7559  df-1st 7667  df-2nd 7668  df-wrecs 7925  df-recs 7986  df-rdg 8024  df-1o 8080  df-oadd 8084  df-er 8267  df-pm 8387  df-en 8488  df-dom 8489  df-sdom 8490  df-fin 8491  df-sup 8884  df-inf 8885  df-oi 8952  df-card 9346  df-pnf 10655  df-mnf 10656  df-xr 10657  df-ltxr 10658  df-le 10659  df-sub 10850  df-neg 10851  df-div 11276  df-nn 11617  df-2 11679  df-3 11680  df-n0 11877  df-z 11961  df-uz 12223  df-q 12328  df-rp 12369  df-ioo 12721  df-ico 12723  df-fz 12877  df-fzo 13018  df-fl 13146  df-seq 13354  df-exp 13415  df-hash 13676  df-shft 14406  df-cj 14438  df-re 14439  df-im 14440  df-sqrt 14574  df-abs 14575  df-limsup 14808  df-clim 14825  df-rlim 14826  df-sum 15023
This theorem is referenced by:  binomcxplemradcnv  40839
  Copyright terms: Public domain W3C validator