abelthlem7 - Metamath Proof Explorer

	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	⊢ (𝜑 → 𝐴:ℕ₀⟶ℂ)
abelth.2	⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ )
abelth.3	⊢ (𝜑 → 𝑀 ∈ ℝ)
abelth.4	⊢ (𝜑 → 0 ≤ 𝑀)
abelth.5	⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))}
abelth.6	⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ Σ𝑛 ∈ ℕ₀ ((𝐴‘𝑛) · (𝑥↑𝑛)))
abelth.7	⊢ (𝜑 → seq0( + , 𝐴) ⇝ 0)
abelthlem6.1	⊢ (𝜑 → 𝑋 ∈ (𝑆 ∖ {1}))
abelthlem7.2	⊢ (𝜑 → 𝑅 ∈ ℝ⁺)
abelthlem7.3	⊢ (𝜑 → 𝑁 ∈ ℕ₀)
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**
Step	Hyp	Ref	Expression
1		abelth.1	. . . . 5 ⊢ (𝜑 → 𝐴:ℕ₀⟶ℂ)
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 ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ Σ𝑛 ∈ ℕ₀ ((𝐴‘𝑛) · (𝑥↑𝑛)))
7	1, 2, 3, 4, 5, 6	abelthlem4 24625	. . . 4 ⊢ (𝜑 → 𝐹:𝑆⟶ℂ)
8		abelthlem6.1	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ (𝑆 ∖ {1}))
9	8	eldifad 3804	. . . 4 ⊢ (𝜑 → 𝑋 ∈ 𝑆)
10	7, 9	ffvelrnd 6624	. . 3 ⊢ (𝜑 → (𝐹‘𝑋) ∈ ℂ)
11	10	abscld 14583	. 2 ⊢ (𝜑 → (abs‘(𝐹‘𝑋)) ∈ ℝ)
12		ax-1cn 10330	. . . . . 6 ⊢ 1 ∈ ℂ
13		abelth.7	. . . . . . . 8 ⊢ (𝜑 → seq0( + , 𝐴) ⇝ 0)
14	1, 2, 3, 4, 5, 6, 13, 8	abelthlem7a 24628	. . . . . . 7 ⊢ (𝜑 → (𝑋 ∈ ℂ ∧ (abs‘(1 − 𝑋)) ≤ (𝑀 · (1 − (abs‘𝑋)))))
15	14	simpld 490	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ ℂ)
16		subcl 10621	. . . . . 6 ⊢ ((1 ∈ ℂ ∧ 𝑋 ∈ ℂ) → (1 − 𝑋) ∈ ℂ)
17	12, 15, 16	sylancr 581	. . . . 5 ⊢ (𝜑 → (1 − 𝑋) ∈ ℂ)
18		fzfid 13091	. . . . . 6 ⊢ (𝜑 → (0...(𝑁 − 1)) ∈ Fin)
19		elfznn0 12751	. . . . . . 7 ⊢ (𝑛 ∈ (0...(𝑁 − 1)) → 𝑛 ∈ ℕ₀)
20		nn0uz 12028	. . . . . . . . . 10 ⊢ ℕ₀ = (ℤ_≥‘0)
21		0zd 11740	. . . . . . . . . 10 ⊢ (𝜑 → 0 ∈ ℤ)
22	1	ffvelrnda 6623	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝐴‘𝑛) ∈ ℂ)
23	20, 21, 22	serf 13147	. . . . . . . . 9 ⊢ (𝜑 → seq0( + , 𝐴):ℕ₀⟶ℂ)
24	23	ffvelrnda 6623	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (seq0( + , 𝐴)‘𝑛) ∈ ℂ)
25		expcl 13196	. . . . . . . . 9 ⊢ ((𝑋 ∈ ℂ ∧ 𝑛 ∈ ℕ₀) → (𝑋↑𝑛) ∈ ℂ)
26	15, 25	sylan 575	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝑋↑𝑛) ∈ ℂ)
27	24, 26	mulcld 10397	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)) ∈ ℂ)
28	19, 27	sylan2 586	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...(𝑁 − 1))) → ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)) ∈ ℂ)
29	18, 28	fsumcl 14871	. . . . 5 ⊢ (𝜑 → Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)) ∈ ℂ)
30	17, 29	mulcld 10397	. . . 4 ⊢ (𝜑 → ((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ∈ ℂ)
31	30	abscld 14583	. . 3 ⊢ (𝜑 → (abs‘((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) ∈ ℝ)
32		eqid 2778	. . . . . 6 ⊢ (ℤ_≥‘𝑁) = (ℤ_≥‘𝑁)
33		abelthlem7.3	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
34	33	nn0zd 11832	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ ℤ)
35		eluznn0 12064	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → 𝑛 ∈ ℕ₀)
36	33, 35	sylan 575	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → 𝑛 ∈ ℕ₀)
37		fveq2 6446	. . . . . . . . 9 ⊢ (𝑘 = 𝑛 → (seq0( + , 𝐴)‘𝑘) = (seq0( + , 𝐴)‘𝑛))
38		oveq2 6930	. . . . . . . . 9 ⊢ (𝑘 = 𝑛 → (𝑋↑𝑘) = (𝑋↑𝑛))
39	37, 38	oveq12d 6940	. . . . . . . 8 ⊢ (𝑘 = 𝑛 → ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)) = ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))
40		eqid 2778	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ₀ ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘))) = (𝑘 ∈ ℕ₀ ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))
41		ovex 6954	. . . . . . . 8 ⊢ ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)) ∈ V
42	39, 40, 41	fvmpt 6542	. . . . . . 7 ⊢ (𝑛 ∈ ℕ₀ → ((𝑘 ∈ ℕ₀ ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))‘𝑛) = ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))
43	36, 42	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → ((𝑘 ∈ ℕ₀ ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))‘𝑛) = ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))
44	36, 27	syldan 585	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)) ∈ ℂ)
45	1, 2, 3, 4, 5	abelthlem2 24623	. . . . . . . . . 10 ⊢ (𝜑 → (1 ∈ 𝑆 ∧ (𝑆 ∖ {1}) ⊆ (0(ball‘(abs ∘ − ))1)))
46	45	simprd 491	. . . . . . . . 9 ⊢ (𝜑 → (𝑆 ∖ {1}) ⊆ (0(ball‘(abs ∘ − ))1))
47	46, 8	sseldd 3822	. . . . . . . 8 ⊢ (𝜑 → 𝑋 ∈ (0(ball‘(abs ∘ − ))1))
48	1, 2, 3, 4, 5, 6, 13	abelthlem5 24626	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) → seq0( + , (𝑘 ∈ ℕ₀ ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))) ∈ dom ⇝ )
49	47, 48	mpdan 677	. . . . . . 7 ⊢ (𝜑 → seq0( + , (𝑘 ∈ ℕ₀ ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))) ∈ dom ⇝ )
50	42	adantl 475	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → ((𝑘 ∈ ℕ₀ ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))‘𝑛) = ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))
51	50, 27	eqeltrd 2859	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → ((𝑘 ∈ ℕ₀ ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))‘𝑛) ∈ ℂ)
52	20, 33, 51	iserex 14795	. . . . . . 7 ⊢ (𝜑 → (seq0( + , (𝑘 ∈ ℕ₀ ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))) ∈ dom ⇝ ↔ seq𝑁( + , (𝑘 ∈ ℕ₀ ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))) ∈ dom ⇝ ))
53	49, 52	mpbid 224	. . . . . 6 ⊢ (𝜑 → seq𝑁( + , (𝑘 ∈ ℕ₀ ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))) ∈ dom ⇝ )
54	32, 34, 43, 44, 53	isumcl 14897	. . . . 5 ⊢ (𝜑 → Σ𝑛 ∈ (ℤ_≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)) ∈ ℂ)
55	17, 54	mulcld 10397	. . . 4 ⊢ (𝜑 → ((1 − 𝑋) · Σ𝑛 ∈ (ℤ_≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ∈ ℂ)
56	55	abscld 14583	. . 3 ⊢ (𝜑 → (abs‘((1 − 𝑋) · Σ𝑛 ∈ (ℤ_≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) ∈ ℝ)
57	31, 56	readdcld 10406	. 2 ⊢ (𝜑 → ((abs‘((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) + (abs‘((1 − 𝑋) · Σ𝑛 ∈ (ℤ_≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))))) ∈ ℝ)
58		peano2re 10549	. . . 4 ⊢ (𝑀 ∈ ℝ → (𝑀 + 1) ∈ ℝ)
59	3, 58	syl 17	. . 3 ⊢ (𝜑 → (𝑀 + 1) ∈ ℝ)
60		abelthlem7.2	. . . 4 ⊢ (𝜑 → 𝑅 ∈ ℝ⁺)
61	60	rpred 12181	. . 3 ⊢ (𝜑 → 𝑅 ∈ ℝ)
62	59, 61	remulcld 10407	. 2 ⊢ (𝜑 → ((𝑀 + 1) · 𝑅) ∈ ℝ)
63	1, 2, 3, 4, 5, 6, 13, 8	abelthlem6 24627	. . . . 5 ⊢ (𝜑 → (𝐹‘𝑋) = ((1 − 𝑋) · Σ𝑛 ∈ ℕ₀ ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))))
64	20, 32, 33, 50, 27, 49	isumsplit 14976	. . . . . 6 ⊢ (𝜑 → Σ𝑛 ∈ ℕ₀ ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)) = (Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)) + Σ𝑛 ∈ (ℤ_≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))))
65	64	oveq2d 6938	. . . . 5 ⊢ (𝜑 → ((1 − 𝑋) · Σ𝑛 ∈ ℕ₀ ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) = ((1 − 𝑋) · (Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)) + Σ𝑛 ∈ (ℤ_≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))))
66	17, 29, 54	adddid 10401	. . . . 5 ⊢ (𝜑 → ((1 − 𝑋) · (Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)) + Σ𝑛 ∈ (ℤ_≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) = (((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) + ((1 − 𝑋) · Σ𝑛 ∈ (ℤ_≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))))
67	63, 65, 66	3eqtrd 2818	. . . 4 ⊢ (𝜑 → (𝐹‘𝑋) = (((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) + ((1 − 𝑋) · Σ𝑛 ∈ (ℤ_≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))))
68	67	fveq2d 6450	. . 3 ⊢ (𝜑 → (abs‘(𝐹‘𝑋)) = (abs‘(((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) + ((1 − 𝑋) · Σ𝑛 ∈ (ℤ_≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))))))
69	30, 55	abstrid 14603	. . 3 ⊢ (𝜑 → (abs‘(((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) + ((1 − 𝑋) · Σ𝑛 ∈ (ℤ_≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))))) ≤ ((abs‘((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) + (abs‘((1 − 𝑋) · Σ𝑛 ∈ (ℤ_≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))))))
70	68, 69	eqbrtrd 4908	. 2 ⊢ (𝜑 → (abs‘(𝐹‘𝑋)) ≤ ((abs‘((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) + (abs‘((1 − 𝑋) · Σ𝑛 ∈ (ℤ_≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))))))
71	3, 61	remulcld 10407	. . . 4 ⊢ (𝜑 → (𝑀 · 𝑅) ∈ ℝ)
72	17	abscld 14583	. . . . . 6 ⊢ (𝜑 → (abs‘(1 − 𝑋)) ∈ ℝ)
73	24	abscld 14583	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (abs‘(seq0( + , 𝐴)‘𝑛)) ∈ ℝ)
74	19, 73	sylan2 586	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (abs‘(seq0( + , 𝐴)‘𝑛)) ∈ ℝ)
75	18, 74	fsumrecl 14872	. . . . . . 7 ⊢ (𝜑 → Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) ∈ ℝ)
76		peano2re 10549	. . . . . . 7 ⊢ (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) ∈ ℝ → (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1) ∈ ℝ)
77	75, 76	syl 17	. . . . . 6 ⊢ (𝜑 → (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1) ∈ ℝ)
78	72, 77	remulcld 10407	. . . . 5 ⊢ (𝜑 → ((abs‘(1 − 𝑋)) · (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1)) ∈ ℝ)
79	17, 29	absmuld 14601	. . . . . 6 ⊢ (𝜑 → (abs‘((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) = ((abs‘(1 − 𝑋)) · (abs‘Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))))
80	29	abscld 14583	. . . . . . 7 ⊢ (𝜑 → (abs‘Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ∈ ℝ)
81	17	absge0d 14591	. . . . . . 7 ⊢ (𝜑 → 0 ≤ (abs‘(1 − 𝑋)))
82	27	abscld 14583	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ∈ ℝ)
83	19, 82	sylan2 586	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ∈ ℝ)
84	18, 83	fsumrecl 14872	. . . . . . . . . 10 ⊢ (𝜑 → Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ∈ ℝ)
85	18, 28	fsumabs 14937	. . . . . . . . . 10 ⊢ (𝜑 → (abs‘Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ≤ Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))))
86	15	abscld 14583	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (abs‘𝑋) ∈ ℝ)
87		reexpcl 13195	. . . . . . . . . . . . . . 15 ⊢ (((abs‘𝑋) ∈ ℝ ∧ 𝑛 ∈ ℕ₀) → ((abs‘𝑋)↑𝑛) ∈ ℝ)
88	86, 87	sylan 575	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → ((abs‘𝑋)↑𝑛) ∈ ℝ)
89		1red 10377	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → 1 ∈ ℝ)
90	24	absge0d 14591	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → 0 ≤ (abs‘(seq0( + , 𝐴)‘𝑛)))
91	86	adantr 474	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (abs‘𝑋) ∈ ℝ)
92	15	absge0d 14591	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 0 ≤ (abs‘𝑋))
93	92	adantr 474	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → 0 ≤ (abs‘𝑋))
94		0cn 10368	. . . . . . . . . . . . . . . . . . . 20 ⊢ 0 ∈ ℂ
95		eqid 2778	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (abs ∘ − ) = (abs ∘ − )
96	95	cnmetdval 22982	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑋 ∈ ℂ ∧ 0 ∈ ℂ) → (𝑋(abs ∘ − )0) = (abs‘(𝑋 − 0)))
97	15, 94, 96	sylancl 580	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑋(abs ∘ − )0) = (abs‘(𝑋 − 0)))
98	15	subid1d 10723	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑋 − 0) = 𝑋)
99	98	fveq2d 6450	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (abs‘(𝑋 − 0)) = (abs‘𝑋))
100	97, 99	eqtrd 2814	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑋(abs ∘ − )0) = (abs‘𝑋))
101		cnxmet 22984	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
102		1rp 12141	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ∈ ℝ⁺
103		rpxr 12148	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1 ∈ ℝ⁺ → 1 ∈ ℝ^*)
104	102, 103	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 1 ∈ ℝ^*
105		elbl3 22605	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈ ℝ^*) ∧ (0 ∈ ℂ ∧ 𝑋 ∈ ℂ)) → (𝑋 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝑋(abs ∘ − )0) < 1))
106	101, 104, 105	mpanl12 692	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((0 ∈ ℂ ∧ 𝑋 ∈ ℂ) → (𝑋 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝑋(abs ∘ − )0) < 1))
107	94, 15, 106	sylancr 581	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑋 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝑋(abs ∘ − )0) < 1))
108	47, 107	mpbid 224	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑋(abs ∘ − )0) < 1)
109	100, 108	eqbrtrrd 4910	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (abs‘𝑋) < 1)
110		1re 10376	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ ℝ
111		ltle 10465	. . . . . . . . . . . . . . . . . 18 ⊢ (((abs‘𝑋) ∈ ℝ ∧ 1 ∈ ℝ) → ((abs‘𝑋) < 1 → (abs‘𝑋) ≤ 1))
112	86, 110, 111	sylancl 580	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((abs‘𝑋) < 1 → (abs‘𝑋) ≤ 1))
113	109, 112	mpd 15	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (abs‘𝑋) ≤ 1)
114	113	adantr 474	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (abs‘𝑋) ≤ 1)
115		simpr 479	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → 𝑛 ∈ ℕ₀)
116		exple1 13238	. . . . . . . . . . . . . . 15 ⊢ ((((abs‘𝑋) ∈ ℝ ∧ 0 ≤ (abs‘𝑋) ∧ (abs‘𝑋) ≤ 1) ∧ 𝑛 ∈ ℕ₀) → ((abs‘𝑋)↑𝑛) ≤ 1)
117	91, 93, 114, 115, 116	syl31anc 1441	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → ((abs‘𝑋)↑𝑛) ≤ 1)
118	88, 89, 73, 90, 117	lemul2ad 11318	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → ((abs‘(seq0( + , 𝐴)‘𝑛)) · ((abs‘𝑋)↑𝑛)) ≤ ((abs‘(seq0( + , 𝐴)‘𝑛)) · 1))
119	24, 26	absmuld 14601	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) = ((abs‘(seq0( + , 𝐴)‘𝑛)) · (abs‘(𝑋↑𝑛))))
120		absexp 14451	. . . . . . . . . . . . . . . 16 ⊢ ((𝑋 ∈ ℂ ∧ 𝑛 ∈ ℕ₀) → (abs‘(𝑋↑𝑛)) = ((abs‘𝑋)↑𝑛))
121	15, 120	sylan 575	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (abs‘(𝑋↑𝑛)) = ((abs‘𝑋)↑𝑛))
122	121	oveq2d 6938	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → ((abs‘(seq0( + , 𝐴)‘𝑛)) · (abs‘(𝑋↑𝑛))) = ((abs‘(seq0( + , 𝐴)‘𝑛)) · ((abs‘𝑋)↑𝑛)))
123	119, 122	eqtr2d 2815	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → ((abs‘(seq0( + , 𝐴)‘𝑛)) · ((abs‘𝑋)↑𝑛)) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))))
124	73	recnd 10405	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (abs‘(seq0( + , 𝐴)‘𝑛)) ∈ ℂ)
125	124	mulid1d 10394	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → ((abs‘(seq0( + , 𝐴)‘𝑛)) · 1) = (abs‘(seq0( + , 𝐴)‘𝑛)))
126	118, 123, 125	3brtr3d 4917	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ≤ (abs‘(seq0( + , 𝐴)‘𝑛)))
127	19, 126	sylan2 586	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ≤ (abs‘(seq0( + , 𝐴)‘𝑛)))
128	18, 83, 74, 127	fsumle 14935	. . . . . . . . . 10 ⊢ (𝜑 → Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ≤ Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)))
129	80, 84, 75, 85, 128	letrd 10533	. . . . . . . . 9 ⊢ (𝜑 → (abs‘Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ≤ Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)))
130	75	ltp1d 11308	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) < (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1))
131	80, 75, 77, 129, 130	lelttrd 10534	. . . . . . . 8 ⊢ (𝜑 → (abs‘Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) < (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1))
132	80, 77, 131	ltled 10524	. . . . . . 7 ⊢ (𝜑 → (abs‘Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ≤ (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1))
133	80, 77, 72, 81, 132	lemul2ad 11318	. . . . . 6 ⊢ (𝜑 → ((abs‘(1 − 𝑋)) · (abs‘Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) ≤ ((abs‘(1 − 𝑋)) · (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1)))
134	79, 133	eqbrtrd 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 ∈ ℝ)
137	19, 90	sylan2 586	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...(𝑁 − 1))) → 0 ≤ (abs‘(seq0( + , 𝐴)‘𝑛)))
138	18, 74, 137	fsumge0 14931	. . . . . . . 8 ⊢ (𝜑 → 0 ≤ Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)))
139	136, 75, 77, 138, 130	lelttrd 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))))
141	72, 61, 77, 139, 140	syl112anc 1442	. . . . . 6 ⊢ (𝜑 → (((abs‘(1 − 𝑋)) · (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1)) < 𝑅 ↔ (abs‘(1 − 𝑋)) < (𝑅 / (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1))))
142	135, 141	mpbird 249	. . . . 5 ⊢ (𝜑 → ((abs‘(1 − 𝑋)) · (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1)) < 𝑅)
143	31, 78, 61, 134, 142	lelttrd 10534	. . . 4 ⊢ (𝜑 → (abs‘((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) < 𝑅)
144	17, 54	absmuld 14601	. . . . 5 ⊢ (𝜑 → (abs‘((1 − 𝑋) · Σ𝑛 ∈ (ℤ_≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) = ((abs‘(1 − 𝑋)) · (abs‘Σ𝑛 ∈ (ℤ_≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))))
145	54	abscld 14583	. . . . . . 7 ⊢ (𝜑 → (abs‘Σ𝑛 ∈ (ℤ_≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ∈ ℝ)
146	39	fveq2d 6450	. . . . . . . . . 10 ⊢ (𝑘 = 𝑛 → (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘))) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))))
147		eqid 2778	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ₀ ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))) = (𝑘 ∈ ℕ₀ ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘))))
148		fvex 6459	. . . . . . . . . 10 ⊢ (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ∈ V
149	146, 147, 148	fvmpt 6542	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ₀ → ((𝑘 ∈ ℕ₀ ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘))))‘𝑛) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))))
150	36, 149	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → ((𝑘 ∈ ℕ₀ ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘))))‘𝑛) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))))
151	44	abscld 14583	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ∈ ℝ)
152		uzid 12007	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ (ℤ_≥‘𝑁))
153	34, 152	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘𝑁))
154		oveq2 6930	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑛 → ((abs‘𝑋)↑𝑘) = ((abs‘𝑋)↑𝑛))
155		eqid 2778	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ₀ ↦ ((abs‘𝑋)↑𝑘)) = (𝑘 ∈ ℕ₀ ↦ ((abs‘𝑋)↑𝑘))
156		ovex 6954	. . . . . . . . . . . 12 ⊢ ((abs‘𝑋)↑𝑛) ∈ V
157	154, 155, 156	fvmpt 6542	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ₀ → ((𝑘 ∈ ℕ₀ ↦ ((abs‘𝑋)↑𝑘))‘𝑛) = ((abs‘𝑋)↑𝑛))
158	36, 157	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → ((𝑘 ∈ ℕ₀ ↦ ((abs‘𝑋)↑𝑘))‘𝑛) = ((abs‘𝑋)↑𝑛))
159	36, 88	syldan 585	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → ((abs‘𝑋)↑𝑛) ∈ ℝ)
160	158, 159	eqeltrd 2859	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → ((𝑘 ∈ ℕ₀ ↦ ((abs‘𝑋)↑𝑘))‘𝑛) ∈ ℝ)
161	151	recnd 10405	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ∈ ℂ)
162	150, 161	eqeltrd 2859	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → ((𝑘 ∈ ℕ₀ ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘))))‘𝑛) ∈ ℂ)
163	86	recnd 10405	. . . . . . . . . . 11 ⊢ (𝜑 → (abs‘𝑋) ∈ ℂ)
164		absidm 14470	. . . . . . . . . . . . 13 ⊢ (𝑋 ∈ ℂ → (abs‘(abs‘𝑋)) = (abs‘𝑋))
165	15, 164	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (abs‘(abs‘𝑋)) = (abs‘𝑋))
166	165, 109	eqbrtrd 4908	. . . . . . . . . . 11 ⊢ (𝜑 → (abs‘(abs‘𝑋)) < 1)
167	163, 166, 33, 158	geolim2 15006	. . . . . . . . . 10 ⊢ (𝜑 → seq𝑁( + , (𝑘 ∈ ℕ₀ ↦ ((abs‘𝑋)↑𝑘))) ⇝ (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋))))
168		seqex 13121	. . . . . . . . . . 11 ⊢ seq𝑁( + , (𝑘 ∈ ℕ₀ ↦ ((abs‘𝑋)↑𝑘))) ∈ V
169		ovex 6954	. . . . . . . . . . 11 ⊢ (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋))) ∈ V
170	168, 169	breldm 5574	. . . . . . . . . 10 ⊢ (seq𝑁( + , (𝑘 ∈ ℕ₀ ↦ ((abs‘𝑋)↑𝑘))) ⇝ (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋))) → seq𝑁( + , (𝑘 ∈ ℕ₀ ↦ ((abs‘𝑋)↑𝑘))) ∈ dom ⇝ )
171	167, 170	syl 17	. . . . . . . . 9 ⊢ (𝜑 → seq𝑁( + , (𝑘 ∈ ℕ₀ ↦ ((abs‘𝑋)↑𝑘))) ∈ dom ⇝ )
172	119, 122	eqtrd 2814	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) = ((abs‘(seq0( + , 𝐴)‘𝑛)) · ((abs‘𝑋)↑𝑛)))
173	36, 172	syldan 585	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) = ((abs‘(seq0( + , 𝐴)‘𝑛)) · ((abs‘𝑋)↑𝑛)))
174	36, 73	syldan 585	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (abs‘(seq0( + , 𝐴)‘𝑛)) ∈ ℝ)
175	61	adantr 474	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → 𝑅 ∈ ℝ)
176	86	adantr 474	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (abs‘𝑋) ∈ ℝ)
177	92	adantr 474	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → 0 ≤ (abs‘𝑋))
178	176, 36, 177	expge0d 13345	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → 0 ≤ ((abs‘𝑋)↑𝑛))
179		abelthlem7.4	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑘 ∈ (ℤ_≥‘𝑁)(abs‘(seq0( + , 𝐴)‘𝑘)) < 𝑅)
180	37	fveq2d 6450	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑛 → (abs‘(seq0( + , 𝐴)‘𝑘)) = (abs‘(seq0( + , 𝐴)‘𝑛)))
181	180	breq1d 4896	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑛 → ((abs‘(seq0( + , 𝐴)‘𝑘)) < 𝑅 ↔ (abs‘(seq0( + , 𝐴)‘𝑛)) < 𝑅))
182	181	rspccva 3510	. . . . . . . . . . . . . 14 ⊢ ((∀𝑘 ∈ (ℤ_≥‘𝑁)(abs‘(seq0( + , 𝐴)‘𝑘)) < 𝑅 ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (abs‘(seq0( + , 𝐴)‘𝑛)) < 𝑅)
183	179, 182	sylan 575	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (abs‘(seq0( + , 𝐴)‘𝑛)) < 𝑅)
184	174, 175, 183	ltled 10524	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (abs‘(seq0( + , 𝐴)‘𝑛)) ≤ 𝑅)
185	174, 175, 159, 178, 184	lemul1ad 11317	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → ((abs‘(seq0( + , 𝐴)‘𝑛)) · ((abs‘𝑋)↑𝑛)) ≤ (𝑅 · ((abs‘𝑋)↑𝑛)))
186	173, 185	eqbrtrd 4908	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ≤ (𝑅 · ((abs‘𝑋)↑𝑛)))
187	150	fveq2d 6450	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (abs‘((𝑘 ∈ ℕ₀ ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘))))‘𝑛)) = (abs‘(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))))
188		absidm 14470	. . . . . . . . . . . 12 ⊢ (((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)) ∈ ℂ → (abs‘(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))))
189	44, 188	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (abs‘(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))))
190	187, 189	eqtrd 2814	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (abs‘((𝑘 ∈ ℕ₀ ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘))))‘𝑛)) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))))
191	158	oveq2d 6938	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝑅 · ((𝑘 ∈ ℕ₀ ↦ ((abs‘𝑋)↑𝑘))‘𝑛)) = (𝑅 · ((abs‘𝑋)↑𝑛)))
192	186, 190, 191	3brtr4d 4918	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (abs‘((𝑘 ∈ ℕ₀ ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘))))‘𝑛)) ≤ (𝑅 · ((𝑘 ∈ ℕ₀ ↦ ((abs‘𝑋)↑𝑘))‘𝑛)))
193	32, 153, 160, 162, 171, 61, 192	cvgcmpce 14954	. . . . . . . 8 ⊢ (𝜑 → seq𝑁( + , (𝑘 ∈ ℕ₀ ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘))))) ∈ dom ⇝ )
194	32, 34, 150, 151, 193	isumrecl 14901	. . . . . . 7 ⊢ (𝜑 → Σ𝑛 ∈ (ℤ_≥‘𝑁)(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ∈ ℝ)
195		eldifsni 4553	. . . . . . . . . . . 12 ⊢ (𝑋 ∈ (𝑆 ∖ {1}) → 𝑋 ≠ 1)
196	8, 195	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ≠ 1)
197	196	necomd 3024	. . . . . . . . . 10 ⊢ (𝜑 → 1 ≠ 𝑋)
198		subeq0 10649	. . . . . . . . . . . 12 ⊢ ((1 ∈ ℂ ∧ 𝑋 ∈ ℂ) → ((1 − 𝑋) = 0 ↔ 1 = 𝑋))
199	198	necon3bid 3013	. . . . . . . . . . 11 ⊢ ((1 ∈ ℂ ∧ 𝑋 ∈ ℂ) → ((1 − 𝑋) ≠ 0 ↔ 1 ≠ 𝑋))
200	12, 15, 199	sylancr 581	. . . . . . . . . 10 ⊢ (𝜑 → ((1 − 𝑋) ≠ 0 ↔ 1 ≠ 𝑋))
201	197, 200	mpbird 249	. . . . . . . . 9 ⊢ (𝜑 → (1 − 𝑋) ≠ 0)
202	17, 201	absrpcld 14595	. . . . . . . 8 ⊢ (𝜑 → (abs‘(1 − 𝑋)) ∈ ℝ⁺)
203	71, 202	rerpdivcld 12212	. . . . . . 7 ⊢ (𝜑 → ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))) ∈ ℝ)
204	32, 34, 43, 44, 53	isumclim2 14894	. . . . . . . 8 ⊢ (𝜑 → seq𝑁( + , (𝑘 ∈ ℕ₀ ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))) ⇝ Σ𝑛 ∈ (ℤ_≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))
205	32, 34, 150, 161, 193	isumclim2 14894	. . . . . . . 8 ⊢ (𝜑 → seq𝑁( + , (𝑘 ∈ ℕ₀ ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘))))) ⇝ Σ𝑛 ∈ (ℤ_≥‘𝑁)(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))))
206	36, 51	syldan 585	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → ((𝑘 ∈ ℕ₀ ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))‘𝑛) ∈ ℂ)
207	43	fveq2d 6450	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (abs‘((𝑘 ∈ ℕ₀ ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))‘𝑛)) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))))
208	150, 207	eqtr4d 2817	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → ((𝑘 ∈ ℕ₀ ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘))))‘𝑛) = (abs‘((𝑘 ∈ ℕ₀ ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))‘𝑛)))
209	32, 204, 205, 34, 206, 208	iserabs 14951	. . . . . . 7 ⊢ (𝜑 → (abs‘Σ𝑛 ∈ (ℤ_≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ≤ Σ𝑛 ∈ (ℤ_≥‘𝑁)(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))))
210	86, 33	reexpcld 13344	. . . . . . . . . 10 ⊢ (𝜑 → ((abs‘𝑋)↑𝑁) ∈ ℝ)
211		difrp 12177	. . . . . . . . . . . 12 ⊢ (((abs‘𝑋) ∈ ℝ ∧ 1 ∈ ℝ) → ((abs‘𝑋) < 1 ↔ (1 − (abs‘𝑋)) ∈ ℝ⁺))
212	86, 110, 211	sylancl 580	. . . . . . . . . . 11 ⊢ (𝜑 → ((abs‘𝑋) < 1 ↔ (1 − (abs‘𝑋)) ∈ ℝ⁺))
213	109, 212	mpbid 224	. . . . . . . . . 10 ⊢ (𝜑 → (1 − (abs‘𝑋)) ∈ ℝ⁺)
214	210, 213	rerpdivcld 12212	. . . . . . . . 9 ⊢ (𝜑 → (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋))) ∈ ℝ)
215	61, 214	remulcld 10407	. . . . . . . 8 ⊢ (𝜑 → (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))) ∈ ℝ)
216	154	oveq2d 6938	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑛 → (𝑅 · ((abs‘𝑋)↑𝑘)) = (𝑅 · ((abs‘𝑋)↑𝑛)))
217		eqid 2778	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ₀ ↦ (𝑅 · ((abs‘𝑋)↑𝑘))) = (𝑘 ∈ ℕ₀ ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))
218		ovex 6954	. . . . . . . . . . . 12 ⊢ (𝑅 · ((abs‘𝑋)↑𝑛)) ∈ V
219	216, 217, 218	fvmpt 6542	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ₀ → ((𝑘 ∈ ℕ₀ ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))‘𝑛) = (𝑅 · ((abs‘𝑋)↑𝑛)))
220	36, 219	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → ((𝑘 ∈ ℕ₀ ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))‘𝑛) = (𝑅 · ((abs‘𝑋)↑𝑛)))
221	175, 159	remulcld 10407	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝑅 · ((abs‘𝑋)↑𝑛)) ∈ ℝ)
222	60	rpcnd 12183	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑅 ∈ ℂ)
223	160	recnd 10405	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → ((𝑘 ∈ ℕ₀ ↦ ((abs‘𝑋)↑𝑘))‘𝑛) ∈ ℂ)
224	220, 191	eqtr4d 2817	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → ((𝑘 ∈ ℕ₀ ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))‘𝑛) = (𝑅 · ((𝑘 ∈ ℕ₀ ↦ ((abs‘𝑋)↑𝑘))‘𝑛)))
225	32, 34, 222, 167, 223, 224	isermulc2 14796	. . . . . . . . . . 11 ⊢ (𝜑 → seq𝑁( + , (𝑘 ∈ ℕ₀ ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))) ⇝ (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))))
226		seqex 13121	. . . . . . . . . . . 12 ⊢ seq𝑁( + , (𝑘 ∈ ℕ₀ ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))) ∈ V
227		ovex 6954	. . . . . . . . . . . 12 ⊢ (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))) ∈ V
228	226, 227	breldm 5574	. . . . . . . . . . 11 ⊢ (seq𝑁( + , (𝑘 ∈ ℕ₀ ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))) ⇝ (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))) → seq𝑁( + , (𝑘 ∈ ℕ₀ ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))) ∈ dom ⇝ )
229	225, 228	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → seq𝑁( + , (𝑘 ∈ ℕ₀ ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))) ∈ dom ⇝ )
230	32, 34, 150, 151, 220, 221, 186, 193, 229	isumle 14980	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑛 ∈ (ℤ_≥‘𝑁)(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ≤ Σ𝑛 ∈ (ℤ_≥‘𝑁)(𝑅 · ((abs‘𝑋)↑𝑛)))
231	221	recnd 10405	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝑅 · ((abs‘𝑋)↑𝑛)) ∈ ℂ)
232	32, 34, 220, 231, 225	isumclim 14893	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑛 ∈ (ℤ_≥‘𝑁)(𝑅 · ((abs‘𝑋)↑𝑛)) = (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))))
233	230, 232	breqtrd 4912	. . . . . . . 8 ⊢ (𝜑 → Σ𝑛 ∈ (ℤ_≥‘𝑁)(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ≤ (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))))
234	60, 213	rpdivcld 12198	. . . . . . . . . 10 ⊢ (𝜑 → (𝑅 / (1 − (abs‘𝑋))) ∈ ℝ⁺)
235	234	rpred 12181	. . . . . . . . 9 ⊢ (𝜑 → (𝑅 / (1 − (abs‘𝑋))) ∈ ℝ)
236	210	recnd 10405	. . . . . . . . . . 11 ⊢ (𝜑 → ((abs‘𝑋)↑𝑁) ∈ ℂ)
237	213	rpcnd 12183	. . . . . . . . . . 11 ⊢ (𝜑 → (1 − (abs‘𝑋)) ∈ ℂ)
238	213	rpne0d 12186	. . . . . . . . . . 11 ⊢ (𝜑 → (1 − (abs‘𝑋)) ≠ 0)
239	222, 236, 237, 238	div12d 11187	. . . . . . . . . 10 ⊢ (𝜑 → (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))) = (((abs‘𝑋)↑𝑁) · (𝑅 / (1 − (abs‘𝑋)))))
240		1red 10377	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ∈ ℝ)
241	234	rpge0d 12185	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ≤ (𝑅 / (1 − (abs‘𝑋))))
242		exple1 13238	. . . . . . . . . . . . 13 ⊢ ((((abs‘𝑋) ∈ ℝ ∧ 0 ≤ (abs‘𝑋) ∧ (abs‘𝑋) ≤ 1) ∧ 𝑁 ∈ ℕ₀) → ((abs‘𝑋)↑𝑁) ≤ 1)
243	86, 92, 113, 33, 242	syl31anc 1441	. . . . . . . . . . . 12 ⊢ (𝜑 → ((abs‘𝑋)↑𝑁) ≤ 1)
244	210, 240, 235, 241, 243	lemul1ad 11317	. . . . . . . . . . 11 ⊢ (𝜑 → (((abs‘𝑋)↑𝑁) · (𝑅 / (1 − (abs‘𝑋)))) ≤ (1 · (𝑅 / (1 − (abs‘𝑋)))))
245	234	rpcnd 12183	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑅 / (1 − (abs‘𝑋))) ∈ ℂ)
246	245	mulid2d 10395	. . . . . . . . . . 11 ⊢ (𝜑 → (1 · (𝑅 / (1 − (abs‘𝑋)))) = (𝑅 / (1 − (abs‘𝑋))))
247	244, 246	breqtrd 4912	. . . . . . . . . 10 ⊢ (𝜑 → (((abs‘𝑋)↑𝑁) · (𝑅 / (1 − (abs‘𝑋)))) ≤ (𝑅 / (1 − (abs‘𝑋))))
248	239, 247	eqbrtrd 4908	. . . . . . . . 9 ⊢ (𝜑 → (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))) ≤ (𝑅 / (1 − (abs‘𝑋))))
249	14	simprd 491	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (abs‘(1 − 𝑋)) ≤ (𝑀 · (1 − (abs‘𝑋))))
250		resubcl 10687	. . . . . . . . . . . . . . . . 17 ⊢ ((1 ∈ ℝ ∧ (abs‘𝑋) ∈ ℝ) → (1 − (abs‘𝑋)) ∈ ℝ)
251	110, 86, 250	sylancr 581	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1 − (abs‘𝑋)) ∈ ℝ)
252	3, 251	remulcld 10407	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀 · (1 − (abs‘𝑋))) ∈ ℝ)
253	72, 252, 60	lemul2d 12225	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((abs‘(1 − 𝑋)) ≤ (𝑀 · (1 − (abs‘𝑋))) ↔ (𝑅 · (abs‘(1 − 𝑋))) ≤ (𝑅 · (𝑀 · (1 − (abs‘𝑋))))))
254	249, 253	mpbid 224	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑅 · (abs‘(1 − 𝑋))) ≤ (𝑅 · (𝑀 · (1 − (abs‘𝑋)))))
255	3	recnd 10405	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 ∈ ℂ)
256	222, 255, 237	mul12d 10585	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑅 · (𝑀 · (1 − (abs‘𝑋)))) = (𝑀 · (𝑅 · (1 − (abs‘𝑋)))))
257	222, 237	mulcomd 10398	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑅 · (1 − (abs‘𝑋))) = ((1 − (abs‘𝑋)) · 𝑅))
258	257	oveq2d 6938	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑀 · (𝑅 · (1 − (abs‘𝑋)))) = (𝑀 · ((1 − (abs‘𝑋)) · 𝑅)))
259	255, 237, 222	mul12d 10585	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑀 · ((1 − (abs‘𝑋)) · 𝑅)) = ((1 − (abs‘𝑋)) · (𝑀 · 𝑅)))
260	256, 258, 259	3eqtrd 2818	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑅 · (𝑀 · (1 − (abs‘𝑋)))) = ((1 − (abs‘𝑋)) · (𝑀 · 𝑅)))
261	254, 260	breqtrd 4912	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑅 · (abs‘(1 − 𝑋))) ≤ ((1 − (abs‘𝑋)) · (𝑀 · 𝑅)))
262	251, 71	remulcld 10407	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((1 − (abs‘𝑋)) · (𝑀 · 𝑅)) ∈ ℝ)
263	61, 262, 202	lemuldivd 12230	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑅 · (abs‘(1 − 𝑋))) ≤ ((1 − (abs‘𝑋)) · (𝑀 · 𝑅)) ↔ 𝑅 ≤ (((1 − (abs‘𝑋)) · (𝑀 · 𝑅)) / (abs‘(1 − 𝑋)))))
264	261, 263	mpbid 224	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑅 ≤ (((1 − (abs‘𝑋)) · (𝑀 · 𝑅)) / (abs‘(1 − 𝑋))))
265	71	recnd 10405	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑀 · 𝑅) ∈ ℂ)
266	72	recnd 10405	. . . . . . . . . . . 12 ⊢ (𝜑 → (abs‘(1 − 𝑋)) ∈ ℂ)
267	202	rpne0d 12186	. . . . . . . . . . . 12 ⊢ (𝜑 → (abs‘(1 − 𝑋)) ≠ 0)
268	237, 265, 266, 267	divassd 11186	. . . . . . . . . . 11 ⊢ (𝜑 → (((1 − (abs‘𝑋)) · (𝑀 · 𝑅)) / (abs‘(1 − 𝑋))) = ((1 − (abs‘𝑋)) · ((𝑀 · 𝑅) / (abs‘(1 − 𝑋)))))
269	264, 268	breqtrd 4912	. . . . . . . . . 10 ⊢ (𝜑 → 𝑅 ≤ ((1 − (abs‘𝑋)) · ((𝑀 · 𝑅) / (abs‘(1 − 𝑋)))))
270		posdif 10868	. . . . . . . . . . . . 13 ⊢ (((abs‘𝑋) ∈ ℝ ∧ 1 ∈ ℝ) → ((abs‘𝑋) < 1 ↔ 0 < (1 − (abs‘𝑋))))
271	86, 110, 270	sylancl 580	. . . . . . . . . . . 12 ⊢ (𝜑 → ((abs‘𝑋) < 1 ↔ 0 < (1 − (abs‘𝑋))))
272	109, 271	mpbid 224	. . . . . . . . . . 11 ⊢ (𝜑 → 0 < (1 − (abs‘𝑋)))
273		ledivmul 11253	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ ℝ ∧ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))) ∈ ℝ ∧ ((1 − (abs‘𝑋)) ∈ ℝ ∧ 0 < (1 − (abs‘𝑋)))) → ((𝑅 / (1 − (abs‘𝑋))) ≤ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))) ↔ 𝑅 ≤ ((1 − (abs‘𝑋)) · ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))))))
274	61, 203, 251, 272, 273	syl112anc 1442	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑅 / (1 − (abs‘𝑋))) ≤ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))) ↔ 𝑅 ≤ ((1 − (abs‘𝑋)) · ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))))))
275	269, 274	mpbird 249	. . . . . . . . 9 ⊢ (𝜑 → (𝑅 / (1 − (abs‘𝑋))) ≤ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))))
276	215, 235, 203, 248, 275	letrd 10533	. . . . . . . 8 ⊢ (𝜑 → (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))) ≤ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))))
277	194, 215, 203, 233, 276	letrd 10533	. . . . . . 7 ⊢ (𝜑 → Σ𝑛 ∈ (ℤ_≥‘𝑁)(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ≤ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))))
278	145, 194, 203, 209, 277	letrd 10533	. . . . . 6 ⊢ (𝜑 → (abs‘Σ𝑛 ∈ (ℤ_≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ≤ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))))
279	145, 71, 202	lemuldiv2d 12231	. . . . . 6 ⊢ (𝜑 → (((abs‘(1 − 𝑋)) · (abs‘Σ𝑛 ∈ (ℤ_≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) ≤ (𝑀 · 𝑅) ↔ (abs‘Σ𝑛 ∈ (ℤ_≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ≤ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋)))))
280	278, 279	mpbird 249	. . . . 5 ⊢ (𝜑 → ((abs‘(1 − 𝑋)) · (abs‘Σ𝑛 ∈ (ℤ_≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) ≤ (𝑀 · 𝑅))
281	144, 280	eqbrtrd 4908	. . . 4 ⊢ (𝜑 → (abs‘((1 − 𝑋) · Σ𝑛 ∈ (ℤ_≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) ≤ (𝑀 · 𝑅))
282	31, 56, 61, 71, 143, 281	ltleaddd 10996	. . 3 ⊢ (𝜑 → ((abs‘((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) + (abs‘((1 − 𝑋) · Σ𝑛 ∈ (ℤ_≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))))) < (𝑅 + (𝑀 · 𝑅)))
283		1cnd 10371	. . . . 5 ⊢ (𝜑 → 1 ∈ ℂ)
284	255, 283, 222	adddird 10402	. . . 4 ⊢ (𝜑 → ((𝑀 + 1) · 𝑅) = ((𝑀 · 𝑅) + (1 · 𝑅)))
285	222	mulid2d 10395	. . . . 5 ⊢ (𝜑 → (1 · 𝑅) = 𝑅)
286	285	oveq2d 6938	. . . 4 ⊢ (𝜑 → ((𝑀 · 𝑅) + (1 · 𝑅)) = ((𝑀 · 𝑅) + 𝑅))
287	265, 222	addcomd 10578	. . . 4 ⊢ (𝜑 → ((𝑀 · 𝑅) + 𝑅) = (𝑅 + (𝑀 · 𝑅)))
288	284, 286, 287	3eqtrd 2818	. . 3 ⊢ (𝜑 → ((𝑀 + 1) · 𝑅) = (𝑅 + (𝑀 · 𝑅)))
289	282, 288	breqtrrd 4914	. 2 ⊢ (𝜑 → ((abs‘((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) + (abs‘((1 − 𝑋) · Σ𝑛 ∈ (ℤ_≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))))) < ((𝑀 + 1) · 𝑅))
290	11, 57, 62, 70, 289	lelttrd 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 ℕ₀cn0 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

W3C validator