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

Theorem abelthlem7 24629
Description: Lemma for abelth 24632. (Contributed by Mario Carneiro, 2-Apr-2015.)
Hypotheses
Ref Expression
abelth.1 (𝜑𝐴:ℕ0⟶ℂ)
abelth.2 (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ )
abelth.3 (𝜑𝑀 ∈ ℝ)
abelth.4 (𝜑 → 0 ≤ 𝑀)
abelth.5 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))}
abelth.6 𝐹 = (𝑥𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · (𝑥𝑛)))
abelth.7 (𝜑 → seq0( + , 𝐴) ⇝ 0)
abelthlem6.1 (𝜑𝑋 ∈ (𝑆 ∖ {1}))
abelthlem7.2 (𝜑𝑅 ∈ ℝ+)
abelthlem7.3 (𝜑𝑁 ∈ ℕ0)
abelthlem7.4 (𝜑 → ∀𝑘 ∈ (ℤ𝑁)(abs‘(seq0( + , 𝐴)‘𝑘)) < 𝑅)
abelthlem7.5 (𝜑 → (abs‘(1 − 𝑋)) < (𝑅 / (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1)))
Assertion
Ref Expression
abelthlem7 (𝜑 → (abs‘(𝐹𝑋)) < ((𝑀 + 1) · 𝑅))
Distinct variable groups:   𝑘,𝑛,𝑥,𝑧,𝑀   𝑅,𝑘,𝑛,𝑥,𝑧   𝑘,𝑋,𝑛,𝑥,𝑧   𝐴,𝑘,𝑛,𝑥,𝑧   𝑘,𝑁,𝑛   𝜑,𝑘,𝑛,𝑥   𝑆,𝑘,𝑛,𝑥
Allowed substitution hints:   𝜑(𝑧)   𝑆(𝑧)   𝐹(𝑥,𝑧,𝑘,𝑛)   𝑁(𝑥,𝑧)

Proof of Theorem abelthlem7
StepHypRef Expression
1 abelth.1 . . . . 5 (𝜑𝐴:ℕ0⟶ℂ)
2 abelth.2 . . . . 5 (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ )
3 abelth.3 . . . . 5 (𝜑𝑀 ∈ ℝ)
4 abelth.4 . . . . 5 (𝜑 → 0 ≤ 𝑀)
5 abelth.5 . . . . 5 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))}
6 abelth.6 . . . . 5 𝐹 = (𝑥𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · (𝑥𝑛)))
71, 2, 3, 4, 5, 6abelthlem4 24625 . . . 4 (𝜑𝐹:𝑆⟶ℂ)
8 abelthlem6.1 . . . . 5 (𝜑𝑋 ∈ (𝑆 ∖ {1}))
98eldifad 3804 . . . 4 (𝜑𝑋𝑆)
107, 9ffvelrnd 6624 . . 3 (𝜑 → (𝐹𝑋) ∈ ℂ)
1110abscld 14583 . 2 (𝜑 → (abs‘(𝐹𝑋)) ∈ ℝ)
12 ax-1cn 10330 . . . . . 6 1 ∈ ℂ
13 abelth.7 . . . . . . . 8 (𝜑 → seq0( + , 𝐴) ⇝ 0)
141, 2, 3, 4, 5, 6, 13, 8abelthlem7a 24628 . . . . . . 7 (𝜑 → (𝑋 ∈ ℂ ∧ (abs‘(1 − 𝑋)) ≤ (𝑀 · (1 − (abs‘𝑋)))))
1514simpld 490 . . . . . 6 (𝜑𝑋 ∈ ℂ)
16 subcl 10621 . . . . . 6 ((1 ∈ ℂ ∧ 𝑋 ∈ ℂ) → (1 − 𝑋) ∈ ℂ)
1712, 15, 16sylancr 581 . . . . 5 (𝜑 → (1 − 𝑋) ∈ ℂ)
18 fzfid 13091 . . . . . 6 (𝜑 → (0...(𝑁 − 1)) ∈ Fin)
19 elfznn0 12751 . . . . . . 7 (𝑛 ∈ (0...(𝑁 − 1)) → 𝑛 ∈ ℕ0)
20 nn0uz 12028 . . . . . . . . . 10 0 = (ℤ‘0)
21 0zd 11740 . . . . . . . . . 10 (𝜑 → 0 ∈ ℤ)
221ffvelrnda 6623 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ0) → (𝐴𝑛) ∈ ℂ)
2320, 21, 22serf 13147 . . . . . . . . 9 (𝜑 → seq0( + , 𝐴):ℕ0⟶ℂ)
2423ffvelrnda 6623 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ0) → (seq0( + , 𝐴)‘𝑛) ∈ ℂ)
25 expcl 13196 . . . . . . . . 9 ((𝑋 ∈ ℂ ∧ 𝑛 ∈ ℕ0) → (𝑋𝑛) ∈ ℂ)
2615, 25sylan 575 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ0) → (𝑋𝑛) ∈ ℂ)
2724, 26mulcld 10397 . . . . . . 7 ((𝜑𝑛 ∈ ℕ0) → ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) ∈ ℂ)
2819, 27sylan2 586 . . . . . 6 ((𝜑𝑛 ∈ (0...(𝑁 − 1))) → ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) ∈ ℂ)
2918, 28fsumcl 14871 . . . . 5 (𝜑 → Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) ∈ ℂ)
3017, 29mulcld 10397 . . . 4 (𝜑 → ((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ∈ ℂ)
3130abscld 14583 . . 3 (𝜑 → (abs‘((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) ∈ ℝ)
32 eqid 2778 . . . . . 6 (ℤ𝑁) = (ℤ𝑁)
33 abelthlem7.3 . . . . . . 7 (𝜑𝑁 ∈ ℕ0)
3433nn0zd 11832 . . . . . 6 (𝜑𝑁 ∈ ℤ)
35 eluznn0 12064 . . . . . . . 8 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → 𝑛 ∈ ℕ0)
3633, 35sylan 575 . . . . . . 7 ((𝜑𝑛 ∈ (ℤ𝑁)) → 𝑛 ∈ ℕ0)
37 fveq2 6446 . . . . . . . . 9 (𝑘 = 𝑛 → (seq0( + , 𝐴)‘𝑘) = (seq0( + , 𝐴)‘𝑛))
38 oveq2 6930 . . . . . . . . 9 (𝑘 = 𝑛 → (𝑋𝑘) = (𝑋𝑛))
3937, 38oveq12d 6940 . . . . . . . 8 (𝑘 = 𝑛 → ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)) = ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))
40 eqid 2778 . . . . . . . 8 (𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))) = (𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))
41 ovex 6954 . . . . . . . 8 ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) ∈ V
4239, 40, 41fvmpt 6542 . . . . . . 7 (𝑛 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))‘𝑛) = ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))
4336, 42syl 17 . . . . . 6 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))‘𝑛) = ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))
4436, 27syldan 585 . . . . . 6 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) ∈ ℂ)
451, 2, 3, 4, 5abelthlem2 24623 . . . . . . . . . 10 (𝜑 → (1 ∈ 𝑆 ∧ (𝑆 ∖ {1}) ⊆ (0(ball‘(abs ∘ − ))1)))
4645simprd 491 . . . . . . . . 9 (𝜑 → (𝑆 ∖ {1}) ⊆ (0(ball‘(abs ∘ − ))1))
4746, 8sseldd 3822 . . . . . . . 8 (𝜑𝑋 ∈ (0(ball‘(abs ∘ − ))1))
481, 2, 3, 4, 5, 6, 13abelthlem5 24626 . . . . . . . 8 ((𝜑𝑋 ∈ (0(ball‘(abs ∘ − ))1)) → seq0( + , (𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))) ∈ dom ⇝ )
4947, 48mpdan 677 . . . . . . 7 (𝜑 → seq0( + , (𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))) ∈ dom ⇝ )
5042adantl 475 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))‘𝑛) = ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))
5150, 27eqeltrd 2859 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))‘𝑛) ∈ ℂ)
5220, 33, 51iserex 14795 . . . . . . 7 (𝜑 → (seq0( + , (𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))) ∈ dom ⇝ ↔ seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))) ∈ dom ⇝ ))
5349, 52mpbid 224 . . . . . 6 (𝜑 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))) ∈ dom ⇝ )
5432, 34, 43, 44, 53isumcl 14897 . . . . 5 (𝜑 → Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) ∈ ℂ)
5517, 54mulcld 10397 . . . 4 (𝜑 → ((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ∈ ℂ)
5655abscld 14583 . . 3 (𝜑 → (abs‘((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) ∈ ℝ)
5731, 56readdcld 10406 . 2 (𝜑 → ((abs‘((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) + (abs‘((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))) ∈ ℝ)
58 peano2re 10549 . . . 4 (𝑀 ∈ ℝ → (𝑀 + 1) ∈ ℝ)
593, 58syl 17 . . 3 (𝜑 → (𝑀 + 1) ∈ ℝ)
60 abelthlem7.2 . . . 4 (𝜑𝑅 ∈ ℝ+)
6160rpred 12181 . . 3 (𝜑𝑅 ∈ ℝ)
6259, 61remulcld 10407 . 2 (𝜑 → ((𝑀 + 1) · 𝑅) ∈ ℝ)
631, 2, 3, 4, 5, 6, 13, 8abelthlem6 24627 . . . . 5 (𝜑 → (𝐹𝑋) = ((1 − 𝑋) · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
6420, 32, 33, 50, 27, 49isumsplit 14976 . . . . . 6 (𝜑 → Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) = (Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) + Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
6564oveq2d 6938 . . . . 5 (𝜑 → ((1 − 𝑋) · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) = ((1 − 𝑋) · (Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) + Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))))
6617, 29, 54adddid 10401 . . . . 5 (𝜑 → ((1 − 𝑋) · (Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) + Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) = (((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) + ((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))))
6763, 65, 663eqtrd 2818 . . . 4 (𝜑 → (𝐹𝑋) = (((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) + ((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))))
6867fveq2d 6450 . . 3 (𝜑 → (abs‘(𝐹𝑋)) = (abs‘(((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) + ((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))))
6930, 55abstrid 14603 . . 3 (𝜑 → (abs‘(((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) + ((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))) ≤ ((abs‘((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) + (abs‘((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))))
7068, 69eqbrtrd 4908 . 2 (𝜑 → (abs‘(𝐹𝑋)) ≤ ((abs‘((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) + (abs‘((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))))
713, 61remulcld 10407 . . . 4 (𝜑 → (𝑀 · 𝑅) ∈ ℝ)
7217abscld 14583 . . . . . 6 (𝜑 → (abs‘(1 − 𝑋)) ∈ ℝ)
7324abscld 14583 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ0) → (abs‘(seq0( + , 𝐴)‘𝑛)) ∈ ℝ)
7419, 73sylan2 586 . . . . . . . 8 ((𝜑𝑛 ∈ (0...(𝑁 − 1))) → (abs‘(seq0( + , 𝐴)‘𝑛)) ∈ ℝ)
7518, 74fsumrecl 14872 . . . . . . 7 (𝜑 → Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) ∈ ℝ)
76 peano2re 10549 . . . . . . 7 𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) ∈ ℝ → (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1) ∈ ℝ)
7775, 76syl 17 . . . . . 6 (𝜑 → (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1) ∈ ℝ)
7872, 77remulcld 10407 . . . . 5 (𝜑 → ((abs‘(1 − 𝑋)) · (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1)) ∈ ℝ)
7917, 29absmuld 14601 . . . . . 6 (𝜑 → (abs‘((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) = ((abs‘(1 − 𝑋)) · (abs‘Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))))
8029abscld 14583 . . . . . . 7 (𝜑 → (abs‘Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ∈ ℝ)
8117absge0d 14591 . . . . . . 7 (𝜑 → 0 ≤ (abs‘(1 − 𝑋)))
8227abscld 14583 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ0) → (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ∈ ℝ)
8319, 82sylan2 586 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (0...(𝑁 − 1))) → (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ∈ ℝ)
8418, 83fsumrecl 14872 . . . . . . . . . 10 (𝜑 → Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ∈ ℝ)
8518, 28fsumabs 14937 . . . . . . . . . 10 (𝜑 → (abs‘Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
8615abscld 14583 . . . . . . . . . . . . . . 15 (𝜑 → (abs‘𝑋) ∈ ℝ)
87 reexpcl 13195 . . . . . . . . . . . . . . 15 (((abs‘𝑋) ∈ ℝ ∧ 𝑛 ∈ ℕ0) → ((abs‘𝑋)↑𝑛) ∈ ℝ)
8886, 87sylan 575 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ0) → ((abs‘𝑋)↑𝑛) ∈ ℝ)
89 1red 10377 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ0) → 1 ∈ ℝ)
9024absge0d 14591 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ0) → 0 ≤ (abs‘(seq0( + , 𝐴)‘𝑛)))
9186adantr 474 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ0) → (abs‘𝑋) ∈ ℝ)
9215absge0d 14591 . . . . . . . . . . . . . . . 16 (𝜑 → 0 ≤ (abs‘𝑋))
9392adantr 474 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ0) → 0 ≤ (abs‘𝑋))
94 0cn 10368 . . . . . . . . . . . . . . . . . . . 20 0 ∈ ℂ
95 eqid 2778 . . . . . . . . . . . . . . . . . . . . 21 (abs ∘ − ) = (abs ∘ − )
9695cnmetdval 22982 . . . . . . . . . . . . . . . . . . . 20 ((𝑋 ∈ ℂ ∧ 0 ∈ ℂ) → (𝑋(abs ∘ − )0) = (abs‘(𝑋 − 0)))
9715, 94, 96sylancl 580 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑋(abs ∘ − )0) = (abs‘(𝑋 − 0)))
9815subid1d 10723 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑋 − 0) = 𝑋)
9998fveq2d 6450 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (abs‘(𝑋 − 0)) = (abs‘𝑋))
10097, 99eqtrd 2814 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑋(abs ∘ − )0) = (abs‘𝑋))
101 cnxmet 22984 . . . . . . . . . . . . . . . . . . . . 21 (abs ∘ − ) ∈ (∞Met‘ℂ)
102 1rp 12141 . . . . . . . . . . . . . . . . . . . . . 22 1 ∈ ℝ+
103 rpxr 12148 . . . . . . . . . . . . . . . . . . . . . 22 (1 ∈ ℝ+ → 1 ∈ ℝ*)
104102, 103ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 1 ∈ ℝ*
105 elbl3 22605 . . . . . . . . . . . . . . . . . . . . 21 ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈ ℝ*) ∧ (0 ∈ ℂ ∧ 𝑋 ∈ ℂ)) → (𝑋 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝑋(abs ∘ − )0) < 1))
106101, 104, 105mpanl12 692 . . . . . . . . . . . . . . . . . . . 20 ((0 ∈ ℂ ∧ 𝑋 ∈ ℂ) → (𝑋 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝑋(abs ∘ − )0) < 1))
10794, 15, 106sylancr 581 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑋 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝑋(abs ∘ − )0) < 1))
10847, 107mpbid 224 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑋(abs ∘ − )0) < 1)
109100, 108eqbrtrrd 4910 . . . . . . . . . . . . . . . . 17 (𝜑 → (abs‘𝑋) < 1)
110 1re 10376 . . . . . . . . . . . . . . . . . 18 1 ∈ ℝ
111 ltle 10465 . . . . . . . . . . . . . . . . . 18 (((abs‘𝑋) ∈ ℝ ∧ 1 ∈ ℝ) → ((abs‘𝑋) < 1 → (abs‘𝑋) ≤ 1))
11286, 110, 111sylancl 580 . . . . . . . . . . . . . . . . 17 (𝜑 → ((abs‘𝑋) < 1 → (abs‘𝑋) ≤ 1))
113109, 112mpd 15 . . . . . . . . . . . . . . . 16 (𝜑 → (abs‘𝑋) ≤ 1)
114113adantr 474 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ0) → (abs‘𝑋) ≤ 1)
115 simpr 479 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ0) → 𝑛 ∈ ℕ0)
116 exple1 13238 . . . . . . . . . . . . . . 15 ((((abs‘𝑋) ∈ ℝ ∧ 0 ≤ (abs‘𝑋) ∧ (abs‘𝑋) ≤ 1) ∧ 𝑛 ∈ ℕ0) → ((abs‘𝑋)↑𝑛) ≤ 1)
11791, 93, 114, 115, 116syl31anc 1441 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ0) → ((abs‘𝑋)↑𝑛) ≤ 1)
11888, 89, 73, 90, 117lemul2ad 11318 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ0) → ((abs‘(seq0( + , 𝐴)‘𝑛)) · ((abs‘𝑋)↑𝑛)) ≤ ((abs‘(seq0( + , 𝐴)‘𝑛)) · 1))
11924, 26absmuld 14601 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ0) → (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) = ((abs‘(seq0( + , 𝐴)‘𝑛)) · (abs‘(𝑋𝑛))))
120 absexp 14451 . . . . . . . . . . . . . . . 16 ((𝑋 ∈ ℂ ∧ 𝑛 ∈ ℕ0) → (abs‘(𝑋𝑛)) = ((abs‘𝑋)↑𝑛))
12115, 120sylan 575 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ0) → (abs‘(𝑋𝑛)) = ((abs‘𝑋)↑𝑛))
122121oveq2d 6938 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ0) → ((abs‘(seq0( + , 𝐴)‘𝑛)) · (abs‘(𝑋𝑛))) = ((abs‘(seq0( + , 𝐴)‘𝑛)) · ((abs‘𝑋)↑𝑛)))
123119, 122eqtr2d 2815 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ0) → ((abs‘(seq0( + , 𝐴)‘𝑛)) · ((abs‘𝑋)↑𝑛)) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
12473recnd 10405 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ0) → (abs‘(seq0( + , 𝐴)‘𝑛)) ∈ ℂ)
125124mulid1d 10394 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ0) → ((abs‘(seq0( + , 𝐴)‘𝑛)) · 1) = (abs‘(seq0( + , 𝐴)‘𝑛)))
126118, 123, 1253brtr3d 4917 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ0) → (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ (abs‘(seq0( + , 𝐴)‘𝑛)))
12719, 126sylan2 586 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (0...(𝑁 − 1))) → (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ (abs‘(seq0( + , 𝐴)‘𝑛)))
12818, 83, 74, 127fsumle 14935 . . . . . . . . . 10 (𝜑 → Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)))
12980, 84, 75, 85, 128letrd 10533 . . . . . . . . 9 (𝜑 → (abs‘Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)))
13075ltp1d 11308 . . . . . . . . 9 (𝜑 → Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) < (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1))
13180, 75, 77, 129, 130lelttrd 10534 . . . . . . . 8 (𝜑 → (abs‘Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) < (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1))
13280, 77, 131ltled 10524 . . . . . . 7 (𝜑 → (abs‘Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1))
13380, 77, 72, 81, 132lemul2ad 11318 . . . . . 6 (𝜑 → ((abs‘(1 − 𝑋)) · (abs‘Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) ≤ ((abs‘(1 − 𝑋)) · (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1)))
13479, 133eqbrtrd 4908 . . . . 5 (𝜑 → (abs‘((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) ≤ ((abs‘(1 − 𝑋)) · (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1)))
135 abelthlem7.5 . . . . . 6 (𝜑 → (abs‘(1 − 𝑋)) < (𝑅 / (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1)))
136 0red 10380 . . . . . . . 8 (𝜑 → 0 ∈ ℝ)
13719, 90sylan2 586 . . . . . . . . 9 ((𝜑𝑛 ∈ (0...(𝑁 − 1))) → 0 ≤ (abs‘(seq0( + , 𝐴)‘𝑛)))
13818, 74, 137fsumge0 14931 . . . . . . . 8 (𝜑 → 0 ≤ Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)))
139136, 75, 77, 138, 130lelttrd 10534 . . . . . . 7 (𝜑 → 0 < (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1))
140 ltmuldiv 11250 . . . . . . 7 (((abs‘(1 − 𝑋)) ∈ ℝ ∧ 𝑅 ∈ ℝ ∧ ((Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1) ∈ ℝ ∧ 0 < (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1))) → (((abs‘(1 − 𝑋)) · (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1)) < 𝑅 ↔ (abs‘(1 − 𝑋)) < (𝑅 / (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1))))
14172, 61, 77, 139, 140syl112anc 1442 . . . . . 6 (𝜑 → (((abs‘(1 − 𝑋)) · (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1)) < 𝑅 ↔ (abs‘(1 − 𝑋)) < (𝑅 / (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1))))
142135, 141mpbird 249 . . . . 5 (𝜑 → ((abs‘(1 − 𝑋)) · (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1)) < 𝑅)
14331, 78, 61, 134, 142lelttrd 10534 . . . 4 (𝜑 → (abs‘((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) < 𝑅)
14417, 54absmuld 14601 . . . . 5 (𝜑 → (abs‘((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) = ((abs‘(1 − 𝑋)) · (abs‘Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))))
14554abscld 14583 . . . . . . 7 (𝜑 → (abs‘Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ∈ ℝ)
14639fveq2d 6450 . . . . . . . . . 10 (𝑘 = 𝑛 → (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
147 eqid 2778 . . . . . . . . . 10 (𝑘 ∈ ℕ0 ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))) = (𝑘 ∈ ℕ0 ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))))
148 fvex 6459 . . . . . . . . . 10 (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ∈ V
149146, 147, 148fvmpt 6542 . . . . . . . . 9 (𝑛 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))))‘𝑛) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
15036, 149syl 17 . . . . . . . 8 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((𝑘 ∈ ℕ0 ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))))‘𝑛) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
15144abscld 14583 . . . . . . . 8 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ∈ ℝ)
152 uzid 12007 . . . . . . . . . 10 (𝑁 ∈ ℤ → 𝑁 ∈ (ℤ𝑁))
15334, 152syl 17 . . . . . . . . 9 (𝜑𝑁 ∈ (ℤ𝑁))
154 oveq2 6930 . . . . . . . . . . . 12 (𝑘 = 𝑛 → ((abs‘𝑋)↑𝑘) = ((abs‘𝑋)↑𝑛))
155 eqid 2778 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘)) = (𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))
156 ovex 6954 . . . . . . . . . . . 12 ((abs‘𝑋)↑𝑛) ∈ V
157154, 155, 156fvmpt 6542 . . . . . . . . . . 11 (𝑛 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))‘𝑛) = ((abs‘𝑋)↑𝑛))
15836, 157syl 17 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))‘𝑛) = ((abs‘𝑋)↑𝑛))
15936, 88syldan 585 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((abs‘𝑋)↑𝑛) ∈ ℝ)
160158, 159eqeltrd 2859 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))‘𝑛) ∈ ℝ)
161151recnd 10405 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ∈ ℂ)
162150, 161eqeltrd 2859 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((𝑘 ∈ ℕ0 ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))))‘𝑛) ∈ ℂ)
16386recnd 10405 . . . . . . . . . . 11 (𝜑 → (abs‘𝑋) ∈ ℂ)
164 absidm 14470 . . . . . . . . . . . . 13 (𝑋 ∈ ℂ → (abs‘(abs‘𝑋)) = (abs‘𝑋))
16515, 164syl 17 . . . . . . . . . . . 12 (𝜑 → (abs‘(abs‘𝑋)) = (abs‘𝑋))
166165, 109eqbrtrd 4908 . . . . . . . . . . 11 (𝜑 → (abs‘(abs‘𝑋)) < 1)
167163, 166, 33, 158geolim2 15006 . . . . . . . . . 10 (𝜑 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))) ⇝ (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋))))
168 seqex 13121 . . . . . . . . . . 11 seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))) ∈ V
169 ovex 6954 . . . . . . . . . . 11 (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋))) ∈ V
170168, 169breldm 5574 . . . . . . . . . 10 (seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))) ⇝ (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋))) → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))) ∈ dom ⇝ )
171167, 170syl 17 . . . . . . . . 9 (𝜑 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))) ∈ dom ⇝ )
172119, 122eqtrd 2814 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ0) → (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) = ((abs‘(seq0( + , 𝐴)‘𝑛)) · ((abs‘𝑋)↑𝑛)))
17336, 172syldan 585 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) = ((abs‘(seq0( + , 𝐴)‘𝑛)) · ((abs‘𝑋)↑𝑛)))
17436, 73syldan 585 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘(seq0( + , 𝐴)‘𝑛)) ∈ ℝ)
17561adantr 474 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (ℤ𝑁)) → 𝑅 ∈ ℝ)
17686adantr 474 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘𝑋) ∈ ℝ)
17792adantr 474 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (ℤ𝑁)) → 0 ≤ (abs‘𝑋))
178176, 36, 177expge0d 13345 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (ℤ𝑁)) → 0 ≤ ((abs‘𝑋)↑𝑛))
179 abelthlem7.4 . . . . . . . . . . . . . 14 (𝜑 → ∀𝑘 ∈ (ℤ𝑁)(abs‘(seq0( + , 𝐴)‘𝑘)) < 𝑅)
18037fveq2d 6450 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑛 → (abs‘(seq0( + , 𝐴)‘𝑘)) = (abs‘(seq0( + , 𝐴)‘𝑛)))
181180breq1d 4896 . . . . . . . . . . . . . . 15 (𝑘 = 𝑛 → ((abs‘(seq0( + , 𝐴)‘𝑘)) < 𝑅 ↔ (abs‘(seq0( + , 𝐴)‘𝑛)) < 𝑅))
182181rspccva 3510 . . . . . . . . . . . . . 14 ((∀𝑘 ∈ (ℤ𝑁)(abs‘(seq0( + , 𝐴)‘𝑘)) < 𝑅𝑛 ∈ (ℤ𝑁)) → (abs‘(seq0( + , 𝐴)‘𝑛)) < 𝑅)
183179, 182sylan 575 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘(seq0( + , 𝐴)‘𝑛)) < 𝑅)
184174, 175, 183ltled 10524 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘(seq0( + , 𝐴)‘𝑛)) ≤ 𝑅)
185174, 175, 159, 178, 184lemul1ad 11317 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((abs‘(seq0( + , 𝐴)‘𝑛)) · ((abs‘𝑋)↑𝑛)) ≤ (𝑅 · ((abs‘𝑋)↑𝑛)))
186173, 185eqbrtrd 4908 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ (𝑅 · ((abs‘𝑋)↑𝑛)))
187150fveq2d 6450 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘((𝑘 ∈ ℕ0 ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))))‘𝑛)) = (abs‘(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))))
188 absidm 14470 . . . . . . . . . . . 12 (((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) ∈ ℂ → (abs‘(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
18944, 188syl 17 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
190187, 189eqtrd 2814 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘((𝑘 ∈ ℕ0 ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))))‘𝑛)) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
191158oveq2d 6938 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℤ𝑁)) → (𝑅 · ((𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))‘𝑛)) = (𝑅 · ((abs‘𝑋)↑𝑛)))
192186, 190, 1913brtr4d 4918 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘((𝑘 ∈ ℕ0 ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))))‘𝑛)) ≤ (𝑅 · ((𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))‘𝑛)))
19332, 153, 160, 162, 171, 61, 192cvgcmpce 14954 . . . . . . . 8 (𝜑 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))))) ∈ dom ⇝ )
19432, 34, 150, 151, 193isumrecl 14901 . . . . . . 7 (𝜑 → Σ𝑛 ∈ (ℤ𝑁)(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ∈ ℝ)
195 eldifsni 4553 . . . . . . . . . . . 12 (𝑋 ∈ (𝑆 ∖ {1}) → 𝑋 ≠ 1)
1968, 195syl 17 . . . . . . . . . . 11 (𝜑𝑋 ≠ 1)
197196necomd 3024 . . . . . . . . . 10 (𝜑 → 1 ≠ 𝑋)
198 subeq0 10649 . . . . . . . . . . . 12 ((1 ∈ ℂ ∧ 𝑋 ∈ ℂ) → ((1 − 𝑋) = 0 ↔ 1 = 𝑋))
199198necon3bid 3013 . . . . . . . . . . 11 ((1 ∈ ℂ ∧ 𝑋 ∈ ℂ) → ((1 − 𝑋) ≠ 0 ↔ 1 ≠ 𝑋))
20012, 15, 199sylancr 581 . . . . . . . . . 10 (𝜑 → ((1 − 𝑋) ≠ 0 ↔ 1 ≠ 𝑋))
201197, 200mpbird 249 . . . . . . . . 9 (𝜑 → (1 − 𝑋) ≠ 0)
20217, 201absrpcld 14595 . . . . . . . 8 (𝜑 → (abs‘(1 − 𝑋)) ∈ ℝ+)
20371, 202rerpdivcld 12212 . . . . . . 7 (𝜑 → ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))) ∈ ℝ)
20432, 34, 43, 44, 53isumclim2 14894 . . . . . . . 8 (𝜑 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))) ⇝ Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))
20532, 34, 150, 161, 193isumclim2 14894 . . . . . . . 8 (𝜑 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))))) ⇝ Σ𝑛 ∈ (ℤ𝑁)(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
20636, 51syldan 585 . . . . . . . 8 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))‘𝑛) ∈ ℂ)
20743fveq2d 6450 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘((𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))‘𝑛)) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
208150, 207eqtr4d 2817 . . . . . . . 8 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((𝑘 ∈ ℕ0 ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))))‘𝑛) = (abs‘((𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))‘𝑛)))
20932, 204, 205, 34, 206, 208iserabs 14951 . . . . . . 7 (𝜑 → (abs‘Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ Σ𝑛 ∈ (ℤ𝑁)(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
21086, 33reexpcld 13344 . . . . . . . . . 10 (𝜑 → ((abs‘𝑋)↑𝑁) ∈ ℝ)
211 difrp 12177 . . . . . . . . . . . 12 (((abs‘𝑋) ∈ ℝ ∧ 1 ∈ ℝ) → ((abs‘𝑋) < 1 ↔ (1 − (abs‘𝑋)) ∈ ℝ+))
21286, 110, 211sylancl 580 . . . . . . . . . . 11 (𝜑 → ((abs‘𝑋) < 1 ↔ (1 − (abs‘𝑋)) ∈ ℝ+))
213109, 212mpbid 224 . . . . . . . . . 10 (𝜑 → (1 − (abs‘𝑋)) ∈ ℝ+)
214210, 213rerpdivcld 12212 . . . . . . . . 9 (𝜑 → (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋))) ∈ ℝ)
21561, 214remulcld 10407 . . . . . . . 8 (𝜑 → (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))) ∈ ℝ)
216154oveq2d 6938 . . . . . . . . . . . 12 (𝑘 = 𝑛 → (𝑅 · ((abs‘𝑋)↑𝑘)) = (𝑅 · ((abs‘𝑋)↑𝑛)))
217 eqid 2778 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 ↦ (𝑅 · ((abs‘𝑋)↑𝑘))) = (𝑘 ∈ ℕ0 ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))
218 ovex 6954 . . . . . . . . . . . 12 (𝑅 · ((abs‘𝑋)↑𝑛)) ∈ V
219216, 217, 218fvmpt 6542 . . . . . . . . . . 11 (𝑛 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))‘𝑛) = (𝑅 · ((abs‘𝑋)↑𝑛)))
22036, 219syl 17 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((𝑘 ∈ ℕ0 ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))‘𝑛) = (𝑅 · ((abs‘𝑋)↑𝑛)))
221175, 159remulcld 10407 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℤ𝑁)) → (𝑅 · ((abs‘𝑋)↑𝑛)) ∈ ℝ)
22260rpcnd 12183 . . . . . . . . . . . 12 (𝜑𝑅 ∈ ℂ)
223160recnd 10405 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))‘𝑛) ∈ ℂ)
224220, 191eqtr4d 2817 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((𝑘 ∈ ℕ0 ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))‘𝑛) = (𝑅 · ((𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))‘𝑛)))
22532, 34, 222, 167, 223, 224isermulc2 14796 . . . . . . . . . . 11 (𝜑 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))) ⇝ (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))))
226 seqex 13121 . . . . . . . . . . . 12 seq𝑁( + , (𝑘 ∈ ℕ0 ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))) ∈ V
227 ovex 6954 . . . . . . . . . . . 12 (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))) ∈ V
228226, 227breldm 5574 . . . . . . . . . . 11 (seq𝑁( + , (𝑘 ∈ ℕ0 ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))) ⇝ (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))) → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))) ∈ dom ⇝ )
229225, 228syl 17 . . . . . . . . . 10 (𝜑 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))) ∈ dom ⇝ )
23032, 34, 150, 151, 220, 221, 186, 193, 229isumle 14980 . . . . . . . . 9 (𝜑 → Σ𝑛 ∈ (ℤ𝑁)(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ Σ𝑛 ∈ (ℤ𝑁)(𝑅 · ((abs‘𝑋)↑𝑛)))
231221recnd 10405 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℤ𝑁)) → (𝑅 · ((abs‘𝑋)↑𝑛)) ∈ ℂ)
23232, 34, 220, 231, 225isumclim 14893 . . . . . . . . 9 (𝜑 → Σ𝑛 ∈ (ℤ𝑁)(𝑅 · ((abs‘𝑋)↑𝑛)) = (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))))
233230, 232breqtrd 4912 . . . . . . . 8 (𝜑 → Σ𝑛 ∈ (ℤ𝑁)(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))))
23460, 213rpdivcld 12198 . . . . . . . . . 10 (𝜑 → (𝑅 / (1 − (abs‘𝑋))) ∈ ℝ+)
235234rpred 12181 . . . . . . . . 9 (𝜑 → (𝑅 / (1 − (abs‘𝑋))) ∈ ℝ)
236210recnd 10405 . . . . . . . . . . 11 (𝜑 → ((abs‘𝑋)↑𝑁) ∈ ℂ)
237213rpcnd 12183 . . . . . . . . . . 11 (𝜑 → (1 − (abs‘𝑋)) ∈ ℂ)
238213rpne0d 12186 . . . . . . . . . . 11 (𝜑 → (1 − (abs‘𝑋)) ≠ 0)
239222, 236, 237, 238div12d 11187 . . . . . . . . . 10 (𝜑 → (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))) = (((abs‘𝑋)↑𝑁) · (𝑅 / (1 − (abs‘𝑋)))))
240 1red 10377 . . . . . . . . . . . 12 (𝜑 → 1 ∈ ℝ)
241234rpge0d 12185 . . . . . . . . . . . 12 (𝜑 → 0 ≤ (𝑅 / (1 − (abs‘𝑋))))
242 exple1 13238 . . . . . . . . . . . . 13 ((((abs‘𝑋) ∈ ℝ ∧ 0 ≤ (abs‘𝑋) ∧ (abs‘𝑋) ≤ 1) ∧ 𝑁 ∈ ℕ0) → ((abs‘𝑋)↑𝑁) ≤ 1)
24386, 92, 113, 33, 242syl31anc 1441 . . . . . . . . . . . 12 (𝜑 → ((abs‘𝑋)↑𝑁) ≤ 1)
244210, 240, 235, 241, 243lemul1ad 11317 . . . . . . . . . . 11 (𝜑 → (((abs‘𝑋)↑𝑁) · (𝑅 / (1 − (abs‘𝑋)))) ≤ (1 · (𝑅 / (1 − (abs‘𝑋)))))
245234rpcnd 12183 . . . . . . . . . . . 12 (𝜑 → (𝑅 / (1 − (abs‘𝑋))) ∈ ℂ)
246245mulid2d 10395 . . . . . . . . . . 11 (𝜑 → (1 · (𝑅 / (1 − (abs‘𝑋)))) = (𝑅 / (1 − (abs‘𝑋))))
247244, 246breqtrd 4912 . . . . . . . . . 10 (𝜑 → (((abs‘𝑋)↑𝑁) · (𝑅 / (1 − (abs‘𝑋)))) ≤ (𝑅 / (1 − (abs‘𝑋))))
248239, 247eqbrtrd 4908 . . . . . . . . 9 (𝜑 → (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))) ≤ (𝑅 / (1 − (abs‘𝑋))))
24914simprd 491 . . . . . . . . . . . . . 14 (𝜑 → (abs‘(1 − 𝑋)) ≤ (𝑀 · (1 − (abs‘𝑋))))
250 resubcl 10687 . . . . . . . . . . . . . . . . 17 ((1 ∈ ℝ ∧ (abs‘𝑋) ∈ ℝ) → (1 − (abs‘𝑋)) ∈ ℝ)
251110, 86, 250sylancr 581 . . . . . . . . . . . . . . . 16 (𝜑 → (1 − (abs‘𝑋)) ∈ ℝ)
2523, 251remulcld 10407 . . . . . . . . . . . . . . 15 (𝜑 → (𝑀 · (1 − (abs‘𝑋))) ∈ ℝ)
25372, 252, 60lemul2d 12225 . . . . . . . . . . . . . 14 (𝜑 → ((abs‘(1 − 𝑋)) ≤ (𝑀 · (1 − (abs‘𝑋))) ↔ (𝑅 · (abs‘(1 − 𝑋))) ≤ (𝑅 · (𝑀 · (1 − (abs‘𝑋))))))
254249, 253mpbid 224 . . . . . . . . . . . . 13 (𝜑 → (𝑅 · (abs‘(1 − 𝑋))) ≤ (𝑅 · (𝑀 · (1 − (abs‘𝑋)))))
2553recnd 10405 . . . . . . . . . . . . . . 15 (𝜑𝑀 ∈ ℂ)
256222, 255, 237mul12d 10585 . . . . . . . . . . . . . 14 (𝜑 → (𝑅 · (𝑀 · (1 − (abs‘𝑋)))) = (𝑀 · (𝑅 · (1 − (abs‘𝑋)))))
257222, 237mulcomd 10398 . . . . . . . . . . . . . . 15 (𝜑 → (𝑅 · (1 − (abs‘𝑋))) = ((1 − (abs‘𝑋)) · 𝑅))
258257oveq2d 6938 . . . . . . . . . . . . . 14 (𝜑 → (𝑀 · (𝑅 · (1 − (abs‘𝑋)))) = (𝑀 · ((1 − (abs‘𝑋)) · 𝑅)))
259255, 237, 222mul12d 10585 . . . . . . . . . . . . . 14 (𝜑 → (𝑀 · ((1 − (abs‘𝑋)) · 𝑅)) = ((1 − (abs‘𝑋)) · (𝑀 · 𝑅)))
260256, 258, 2593eqtrd 2818 . . . . . . . . . . . . 13 (𝜑 → (𝑅 · (𝑀 · (1 − (abs‘𝑋)))) = ((1 − (abs‘𝑋)) · (𝑀 · 𝑅)))
261254, 260breqtrd 4912 . . . . . . . . . . . 12 (𝜑 → (𝑅 · (abs‘(1 − 𝑋))) ≤ ((1 − (abs‘𝑋)) · (𝑀 · 𝑅)))
262251, 71remulcld 10407 . . . . . . . . . . . . 13 (𝜑 → ((1 − (abs‘𝑋)) · (𝑀 · 𝑅)) ∈ ℝ)
26361, 262, 202lemuldivd 12230 . . . . . . . . . . . 12 (𝜑 → ((𝑅 · (abs‘(1 − 𝑋))) ≤ ((1 − (abs‘𝑋)) · (𝑀 · 𝑅)) ↔ 𝑅 ≤ (((1 − (abs‘𝑋)) · (𝑀 · 𝑅)) / (abs‘(1 − 𝑋)))))
264261, 263mpbid 224 . . . . . . . . . . 11 (𝜑𝑅 ≤ (((1 − (abs‘𝑋)) · (𝑀 · 𝑅)) / (abs‘(1 − 𝑋))))
26571recnd 10405 . . . . . . . . . . . 12 (𝜑 → (𝑀 · 𝑅) ∈ ℂ)
26672recnd 10405 . . . . . . . . . . . 12 (𝜑 → (abs‘(1 − 𝑋)) ∈ ℂ)
267202rpne0d 12186 . . . . . . . . . . . 12 (𝜑 → (abs‘(1 − 𝑋)) ≠ 0)
268237, 265, 266, 267divassd 11186 . . . . . . . . . . 11 (𝜑 → (((1 − (abs‘𝑋)) · (𝑀 · 𝑅)) / (abs‘(1 − 𝑋))) = ((1 − (abs‘𝑋)) · ((𝑀 · 𝑅) / (abs‘(1 − 𝑋)))))
269264, 268breqtrd 4912 . . . . . . . . . 10 (𝜑𝑅 ≤ ((1 − (abs‘𝑋)) · ((𝑀 · 𝑅) / (abs‘(1 − 𝑋)))))
270 posdif 10868 . . . . . . . . . . . . 13 (((abs‘𝑋) ∈ ℝ ∧ 1 ∈ ℝ) → ((abs‘𝑋) < 1 ↔ 0 < (1 − (abs‘𝑋))))
27186, 110, 270sylancl 580 . . . . . . . . . . . 12 (𝜑 → ((abs‘𝑋) < 1 ↔ 0 < (1 − (abs‘𝑋))))
272109, 271mpbid 224 . . . . . . . . . . 11 (𝜑 → 0 < (1 − (abs‘𝑋)))
273 ledivmul 11253 . . . . . . . . . . 11 ((𝑅 ∈ ℝ ∧ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))) ∈ ℝ ∧ ((1 − (abs‘𝑋)) ∈ ℝ ∧ 0 < (1 − (abs‘𝑋)))) → ((𝑅 / (1 − (abs‘𝑋))) ≤ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))) ↔ 𝑅 ≤ ((1 − (abs‘𝑋)) · ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))))))
27461, 203, 251, 272, 273syl112anc 1442 . . . . . . . . . 10 (𝜑 → ((𝑅 / (1 − (abs‘𝑋))) ≤ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))) ↔ 𝑅 ≤ ((1 − (abs‘𝑋)) · ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))))))
275269, 274mpbird 249 . . . . . . . . 9 (𝜑 → (𝑅 / (1 − (abs‘𝑋))) ≤ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))))
276215, 235, 203, 248, 275letrd 10533 . . . . . . . 8 (𝜑 → (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))) ≤ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))))
277194, 215, 203, 233, 276letrd 10533 . . . . . . 7 (𝜑 → Σ𝑛 ∈ (ℤ𝑁)(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))))
278145, 194, 203, 209, 277letrd 10533 . . . . . 6 (𝜑 → (abs‘Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))))
279145, 71, 202lemuldiv2d 12231 . . . . . 6 (𝜑 → (((abs‘(1 − 𝑋)) · (abs‘Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) ≤ (𝑀 · 𝑅) ↔ (abs‘Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋)))))
280278, 279mpbird 249 . . . . 5 (𝜑 → ((abs‘(1 − 𝑋)) · (abs‘Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) ≤ (𝑀 · 𝑅))
281144, 280eqbrtrd 4908 . . . 4 (𝜑 → (abs‘((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) ≤ (𝑀 · 𝑅))
28231, 56, 61, 71, 143, 281ltleaddd 10996 . . 3 (𝜑 → ((abs‘((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) + (abs‘((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))) < (𝑅 + (𝑀 · 𝑅)))
283 1cnd 10371 . . . . 5 (𝜑 → 1 ∈ ℂ)
284255, 283, 222adddird 10402 . . . 4 (𝜑 → ((𝑀 + 1) · 𝑅) = ((𝑀 · 𝑅) + (1 · 𝑅)))
285222mulid2d 10395 . . . . 5 (𝜑 → (1 · 𝑅) = 𝑅)
286285oveq2d 6938 . . . 4 (𝜑 → ((𝑀 · 𝑅) + (1 · 𝑅)) = ((𝑀 · 𝑅) + 𝑅))
287265, 222addcomd 10578 . . . 4 (𝜑 → ((𝑀 · 𝑅) + 𝑅) = (𝑅 + (𝑀 · 𝑅)))
288284, 286, 2873eqtrd 2818 . . 3 (𝜑 → ((𝑀 + 1) · 𝑅) = (𝑅 + (𝑀 · 𝑅)))
289282, 288breqtrrd 4914 . 2 (𝜑 → ((abs‘((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) + (abs‘((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))) < ((𝑀 + 1) · 𝑅))
29011, 57, 62, 70, 289lelttrd 10534 1 (𝜑 → (abs‘(𝐹𝑋)) < ((𝑀 + 1) · 𝑅))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 386   = wceq 1601  wcel 2107  wne 2969  wral 3090  {crab 3094  cdif 3789  wss 3792  {csn 4398   class class class wbr 4886  cmpt 4965  dom cdm 5355  ccom 5359  wf 6131  cfv 6135  (class class class)co 6922  cc 10270  cr 10271  0cc0 10272  1c1 10273   + caddc 10275   · cmul 10277  *cxr 10410   < clt 10411  cle 10412  cmin 10606   / cdiv 11032  0cn0 11642  cz 11728  cuz 11992  +crp 12137  ...cfz 12643  seqcseq 13119  cexp 13178  abscabs 14381  cli 14623  Σcsu 14824  ∞Metcxmet 20127  ballcbl 20129
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-rep 5006  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226  ax-inf2 8835  ax-cnex 10328  ax-resscn 10329  ax-1cn 10330  ax-icn 10331  ax-addcl 10332  ax-addrcl 10333  ax-mulcl 10334  ax-mulrcl 10335  ax-mulcom 10336  ax-addass 10337  ax-mulass 10338  ax-distr 10339  ax-i2m1 10340  ax-1ne0 10341  ax-1rid 10342  ax-rnegex 10343  ax-rrecex 10344  ax-cnre 10345  ax-pre-lttri 10346  ax-pre-lttrn 10347  ax-pre-ltadd 10348  ax-pre-mulgt0 10349  ax-pre-sup 10350  ax-addf 10351  ax-mulf 10352
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-fal 1615  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-nel 3076  df-ral 3095  df-rex 3096  df-reu 3097  df-rmo 3098  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4672  df-int 4711  df-iun 4755  df-br 4887  df-opab 4949  df-mpt 4966  df-tr 4988  df-id 5261  df-eprel 5266  df-po 5274  df-so 5275  df-fr 5314  df-se 5315  df-we 5316  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-pred 5933  df-ord 5979  df-on 5980  df-lim 5981  df-suc 5982  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-isom 6144  df-riota 6883  df-ov 6925  df-oprab 6926  df-mpt2 6927  df-om 7344  df-1st 7445  df-2nd 7446  df-wrecs 7689  df-recs 7751  df-rdg 7789  df-1o 7843  df-oadd 7847  df-er 8026  df-map 8142  df-pm 8143  df-en 8242  df-dom 8243  df-sdom 8244  df-fin 8245  df-sup 8636  df-inf 8637  df-oi 8704  df-card 9098  df-pnf 10413  df-mnf 10414  df-xr 10415  df-ltxr 10416  df-le 10417  df-sub 10608  df-neg 10609  df-div 11033  df-nn 11375  df-2 11438  df-3 11439  df-n0 11643  df-z 11729  df-uz 11993  df-rp 12138  df-xadd 12258  df-ico 12493  df-icc 12494  df-fz 12644  df-fzo 12785  df-fl 12912  df-seq 13120  df-exp 13179  df-hash 13436  df-shft 14214  df-cj 14246  df-re 14247  df-im 14248  df-sqrt 14382  df-abs 14383  df-limsup 14610  df-clim 14627  df-rlim 14628  df-sum 14825  df-psmet 20134  df-xmet 20135  df-met 20136  df-bl 20137
This theorem is referenced by:  abelthlem8  24630
  Copyright terms: Public domain W3C validator