abelthlem5 - Metamath Proof Explorer

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

Theorem abelthlem5 26375

Description: Lemma for abelth 26381. (Contributed by Mario Carneiro, 1-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)

**Assertion**
Ref	Expression
abelthlem5	⊢ ((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) → seq0( + , (𝑘 ∈ ℕ₀ ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))) ∈ dom ⇝ )

Distinct variable groups: 𝑘,𝑛,𝑥,𝑧,𝑀 𝑘,𝑋,𝑛,𝑥,𝑧 𝐴,𝑘,𝑛,𝑥,𝑧 𝜑,𝑘,𝑛,𝑥 𝑆,𝑘,𝑛,𝑥 Allowed substitution hints: 𝜑(𝑧) 𝑆(𝑧) 𝐹(𝑥,𝑧,𝑘,𝑛)

Proof of Theorem abelthlem5 Dummy variables 𝑖 𝑗 𝑚 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nn0uz 12778	. . . 4 ⊢ ℕ₀ = (ℤ_≥‘0)
2		0zd 12489	. . . 4 ⊢ (𝜑 → 0 ∈ ℤ)
3		1rp 12898	. . . . 5 ⊢ 1 ∈ ℝ⁺
4	3	a1i 11	. . . 4 ⊢ (𝜑 → 1 ∈ ℝ⁺)
5		eqidd 2734	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ₀) → (seq0( + , 𝐴)‘𝑚) = (seq0( + , 𝐴)‘𝑚))
6		abelth.7	. . . 4 ⊢ (𝜑 → seq0( + , 𝐴) ⇝ 0)
7	1, 2, 4, 5, 6	climi0 15423	. . 3 ⊢ (𝜑 → ∃𝑗 ∈ ℕ₀ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)
8	7	adantr 480	. 2 ⊢ ((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) → ∃𝑗 ∈ ℕ₀ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)
9		simprl 770	. . 3 ⊢ (((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) → 𝑗 ∈ ℕ₀)
10		oveq2 7362	. . . . . 6 ⊢ (𝑛 = 𝑖 → ((abs‘𝑋)↑𝑛) = ((abs‘𝑋)↑𝑖))
11		eqid 2733	. . . . . 6 ⊢ (𝑛 ∈ ℕ₀ ↦ ((abs‘𝑋)↑𝑛)) = (𝑛 ∈ ℕ₀ ↦ ((abs‘𝑋)↑𝑛))
12		ovex 7387	. . . . . 6 ⊢ ((abs‘𝑋)↑𝑖) ∈ V
13	10, 11, 12	fvmpt 6937	. . . . 5 ⊢ (𝑖 ∈ ℕ₀ → ((𝑛 ∈ ℕ₀ ↦ ((abs‘𝑋)↑𝑛))‘𝑖) = ((abs‘𝑋)↑𝑖))
14	13	adantl 481	. . . 4 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ ℕ₀) → ((𝑛 ∈ ℕ₀ ↦ ((abs‘𝑋)↑𝑛))‘𝑖) = ((abs‘𝑋)↑𝑖))
15		cnxmet 24690	. . . . . . . 8 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
16		0cn 11113	. . . . . . . 8 ⊢ 0 ∈ ℂ
17		1xr 11180	. . . . . . . 8 ⊢ 1 ∈ ℝ^*
18		blssm 24336	. . . . . . . 8 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ ∧ 1 ∈ ℝ^*) → (0(ball‘(abs ∘ − ))1) ⊆ ℂ)
19	15, 16, 17, 18	mp3an 1463	. . . . . . 7 ⊢ (0(ball‘(abs ∘ − ))1) ⊆ ℂ
20		simplr 768	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) → 𝑋 ∈ (0(ball‘(abs ∘ − ))1))
21	19, 20	sselid 3928	. . . . . 6 ⊢ (((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) → 𝑋 ∈ ℂ)
22	21	abscld 15350	. . . . 5 ⊢ (((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) → (abs‘𝑋) ∈ ℝ)
23		reexpcl 13989	. . . . 5 ⊢ (((abs‘𝑋) ∈ ℝ ∧ 𝑖 ∈ ℕ₀) → ((abs‘𝑋)↑𝑖) ∈ ℝ)
24	22, 23	sylan 580	. . . 4 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ ℕ₀) → ((abs‘𝑋)↑𝑖) ∈ ℝ)
25	14, 24	eqeltrd 2833	. . 3 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ ℕ₀) → ((𝑛 ∈ ℕ₀ ↦ ((abs‘𝑋)↑𝑛))‘𝑖) ∈ ℝ)
26		fveq2 6830	. . . . . . 7 ⊢ (𝑘 = 𝑖 → (seq0( + , 𝐴)‘𝑘) = (seq0( + , 𝐴)‘𝑖))
27		oveq2 7362	. . . . . . 7 ⊢ (𝑘 = 𝑖 → (𝑋↑𝑘) = (𝑋↑𝑖))
28	26, 27	oveq12d 7372	. . . . . 6 ⊢ (𝑘 = 𝑖 → ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)) = ((seq0( + , 𝐴)‘𝑖) · (𝑋↑𝑖)))
29		eqid 2733	. . . . . 6 ⊢ (𝑘 ∈ ℕ₀ ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘))) = (𝑘 ∈ ℕ₀ ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))
30		ovex 7387	. . . . . 6 ⊢ ((seq0( + , 𝐴)‘𝑖) · (𝑋↑𝑖)) ∈ V
31	28, 29, 30	fvmpt 6937	. . . . 5 ⊢ (𝑖 ∈ ℕ₀ → ((𝑘 ∈ ℕ₀ ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))‘𝑖) = ((seq0( + , 𝐴)‘𝑖) · (𝑋↑𝑖)))
32	31	adantl 481	. . . 4 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ ℕ₀) → ((𝑘 ∈ ℕ₀ ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))‘𝑖) = ((seq0( + , 𝐴)‘𝑖) · (𝑋↑𝑖)))
33		abelth.1	. . . . . . . . 9 ⊢ (𝜑 → 𝐴:ℕ₀⟶ℂ)
34	33	ffvelcdmda 7025	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ₀) → (𝐴‘𝑥) ∈ ℂ)
35	1, 2, 34	serf 13941	. . . . . . 7 ⊢ (𝜑 → seq0( + , 𝐴):ℕ₀⟶ℂ)
36	35	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) → seq0( + , 𝐴):ℕ₀⟶ℂ)
37	36	ffvelcdmda 7025	. . . . 5 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ ℕ₀) → (seq0( + , 𝐴)‘𝑖) ∈ ℂ)
38		expcl 13990	. . . . . 6 ⊢ ((𝑋 ∈ ℂ ∧ 𝑖 ∈ ℕ₀) → (𝑋↑𝑖) ∈ ℂ)
39	21, 38	sylan 580	. . . . 5 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ ℕ₀) → (𝑋↑𝑖) ∈ ℂ)
40	37, 39	mulcld 11141	. . . 4 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ ℕ₀) → ((seq0( + , 𝐴)‘𝑖) · (𝑋↑𝑖)) ∈ ℂ)
41	32, 40	eqeltrd 2833	. . 3 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ ℕ₀) → ((𝑘 ∈ ℕ₀ ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))‘𝑖) ∈ ℂ)
42	22	recnd 11149	. . . . 5 ⊢ (((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) → (abs‘𝑋) ∈ ℂ)
43		absidm 15235	. . . . . . 7 ⊢ (𝑋 ∈ ℂ → (abs‘(abs‘𝑋)) = (abs‘𝑋))
44	21, 43	syl 17	. . . . . 6 ⊢ (((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) → (abs‘(abs‘𝑋)) = (abs‘𝑋))
45		eqid 2733	. . . . . . . . . 10 ⊢ (abs ∘ − ) = (abs ∘ − )
46	45	cnmetdval 24688	. . . . . . . . 9 ⊢ ((𝑋 ∈ ℂ ∧ 0 ∈ ℂ) → (𝑋(abs ∘ − )0) = (abs‘(𝑋 − 0)))
47	21, 16, 46	sylancl 586	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) → (𝑋(abs ∘ − )0) = (abs‘(𝑋 − 0)))
48	21	subid1d 11470	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) → (𝑋 − 0) = 𝑋)
49	48	fveq2d 6834	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) → (abs‘(𝑋 − 0)) = (abs‘𝑋))
50	47, 49	eqtrd 2768	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) → (𝑋(abs ∘ − )0) = (abs‘𝑋))
51		elbl3 24310	. . . . . . . . . 10 ⊢ ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈ ℝ^*) ∧ (0 ∈ ℂ ∧ 𝑋 ∈ ℂ)) → (𝑋 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝑋(abs ∘ − )0) < 1))
52	15, 17, 51	mpanl12 702	. . . . . . . . 9 ⊢ ((0 ∈ ℂ ∧ 𝑋 ∈ ℂ) → (𝑋 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝑋(abs ∘ − )0) < 1))
53	16, 21, 52	sylancr 587	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) → (𝑋 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝑋(abs ∘ − )0) < 1))
54	20, 53	mpbid 232	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) → (𝑋(abs ∘ − )0) < 1)
55	50, 54	eqbrtrrd 5119	. . . . . 6 ⊢ (((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) → (abs‘𝑋) < 1)
56	44, 55	eqbrtrd 5117	. . . . 5 ⊢ (((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) → (abs‘(abs‘𝑋)) < 1)
57	42, 56, 14	geolim 15781	. . . 4 ⊢ (((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) → seq0( + , (𝑛 ∈ ℕ₀ ↦ ((abs‘𝑋)↑𝑛))) ⇝ (1 / (1 − (abs‘𝑋))))
58		climrel 15403	. . . . 5 ⊢ Rel ⇝
59	58	releldmi 5894	. . . 4 ⊢ (seq0( + , (𝑛 ∈ ℕ₀ ↦ ((abs‘𝑋)↑𝑛))) ⇝ (1 / (1 − (abs‘𝑋))) → seq0( + , (𝑛 ∈ ℕ₀ ↦ ((abs‘𝑋)↑𝑛))) ∈ dom ⇝ )
60	57, 59	syl 17	. . 3 ⊢ (((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) → seq0( + , (𝑛 ∈ ℕ₀ ↦ ((abs‘𝑋)↑𝑛))) ∈ dom ⇝ )
61		1red 11122	. . 3 ⊢ (((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) → 1 ∈ ℝ)
62	36	adantr 480	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ_≥‘𝑗)) → seq0( + , 𝐴):ℕ₀⟶ℂ)
63		eluznn0 12819	. . . . . . . . 9 ⊢ ((𝑗 ∈ ℕ₀ ∧ 𝑖 ∈ (ℤ_≥‘𝑗)) → 𝑖 ∈ ℕ₀)
64	9, 63	sylan 580	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ_≥‘𝑗)) → 𝑖 ∈ ℕ₀)
65	62, 64	ffvelcdmd 7026	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ_≥‘𝑗)) → (seq0( + , 𝐴)‘𝑖) ∈ ℂ)
66	64, 39	syldan 591	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ_≥‘𝑗)) → (𝑋↑𝑖) ∈ ℂ)
67	65, 66	absmuld 15368	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ_≥‘𝑗)) → (abs‘((seq0( + , 𝐴)‘𝑖) · (𝑋↑𝑖))) = ((abs‘(seq0( + , 𝐴)‘𝑖)) · (abs‘(𝑋↑𝑖))))
68	21	adantr 480	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ_≥‘𝑗)) → 𝑋 ∈ ℂ)
69	68, 64	absexpd 15366	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ_≥‘𝑗)) → (abs‘(𝑋↑𝑖)) = ((abs‘𝑋)↑𝑖))
70	69	oveq2d 7370	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ_≥‘𝑗)) → ((abs‘(seq0( + , 𝐴)‘𝑖)) · (abs‘(𝑋↑𝑖))) = ((abs‘(seq0( + , 𝐴)‘𝑖)) · ((abs‘𝑋)↑𝑖)))
71	67, 70	eqtrd 2768	. . . . 5 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ_≥‘𝑗)) → (abs‘((seq0( + , 𝐴)‘𝑖) · (𝑋↑𝑖))) = ((abs‘(seq0( + , 𝐴)‘𝑖)) · ((abs‘𝑋)↑𝑖)))
72	65	abscld 15350	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ_≥‘𝑗)) → (abs‘(seq0( + , 𝐴)‘𝑖)) ∈ ℝ)
73		1red 11122	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ_≥‘𝑗)) → 1 ∈ ℝ)
74	64, 24	syldan 591	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ_≥‘𝑗)) → ((abs‘𝑋)↑𝑖) ∈ ℝ)
75	66	absge0d 15358	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ_≥‘𝑗)) → 0 ≤ (abs‘(𝑋↑𝑖)))
76	75, 69	breqtrd 5121	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ_≥‘𝑗)) → 0 ≤ ((abs‘𝑋)↑𝑖))
77		simprr 772	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) → ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)
78		2fveq3 6835	. . . . . . . . . 10 ⊢ (𝑚 = 𝑖 → (abs‘(seq0( + , 𝐴)‘𝑚)) = (abs‘(seq0( + , 𝐴)‘𝑖)))
79	78	breq1d 5105	. . . . . . . . 9 ⊢ (𝑚 = 𝑖 → ((abs‘(seq0( + , 𝐴)‘𝑚)) < 1 ↔ (abs‘(seq0( + , 𝐴)‘𝑖)) < 1))
80	79	rspccva 3572	. . . . . . . 8 ⊢ ((∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1 ∧ 𝑖 ∈ (ℤ_≥‘𝑗)) → (abs‘(seq0( + , 𝐴)‘𝑖)) < 1)
81	77, 80	sylan 580	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ_≥‘𝑗)) → (abs‘(seq0( + , 𝐴)‘𝑖)) < 1)
82		1re 11121	. . . . . . . 8 ⊢ 1 ∈ ℝ
83		ltle 11210	. . . . . . . 8 ⊢ (((abs‘(seq0( + , 𝐴)‘𝑖)) ∈ ℝ ∧ 1 ∈ ℝ) → ((abs‘(seq0( + , 𝐴)‘𝑖)) < 1 → (abs‘(seq0( + , 𝐴)‘𝑖)) ≤ 1))
84	72, 82, 83	sylancl 586	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ_≥‘𝑗)) → ((abs‘(seq0( + , 𝐴)‘𝑖)) < 1 → (abs‘(seq0( + , 𝐴)‘𝑖)) ≤ 1))
85	81, 84	mpd 15	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ_≥‘𝑗)) → (abs‘(seq0( + , 𝐴)‘𝑖)) ≤ 1)
86	72, 73, 74, 76, 85	lemul1ad 12070	. . . . 5 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ_≥‘𝑗)) → ((abs‘(seq0( + , 𝐴)‘𝑖)) · ((abs‘𝑋)↑𝑖)) ≤ (1 · ((abs‘𝑋)↑𝑖)))
87	71, 86	eqbrtrd 5117	. . . 4 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ_≥‘𝑗)) → (abs‘((seq0( + , 𝐴)‘𝑖) · (𝑋↑𝑖))) ≤ (1 · ((abs‘𝑋)↑𝑖)))
88	64, 31	syl 17	. . . . 5 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ_≥‘𝑗)) → ((𝑘 ∈ ℕ₀ ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))‘𝑖) = ((seq0( + , 𝐴)‘𝑖) · (𝑋↑𝑖)))
89	88	fveq2d 6834	. . . 4 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ_≥‘𝑗)) → (abs‘((𝑘 ∈ ℕ₀ ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))‘𝑖)) = (abs‘((seq0( + , 𝐴)‘𝑖) · (𝑋↑𝑖))))
90	64, 13	syl 17	. . . . 5 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ_≥‘𝑗)) → ((𝑛 ∈ ℕ₀ ↦ ((abs‘𝑋)↑𝑛))‘𝑖) = ((abs‘𝑋)↑𝑖))
91	90	oveq2d 7370	. . . 4 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ_≥‘𝑗)) → (1 · ((𝑛 ∈ ℕ₀ ↦ ((abs‘𝑋)↑𝑛))‘𝑖)) = (1 · ((abs‘𝑋)↑𝑖)))
92	87, 89, 91	3brtr4d 5127	. . 3 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ_≥‘𝑗)) → (abs‘((𝑘 ∈ ℕ₀ ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))‘𝑖)) ≤ (1 · ((𝑛 ∈ ℕ₀ ↦ ((abs‘𝑋)↑𝑛))‘𝑖)))
93	1, 9, 25, 41, 60, 61, 92	cvgcmpce 15729	. 2 ⊢ (((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) → seq0( + , (𝑘 ∈ ℕ₀ ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))) ∈ dom ⇝ )
94	8, 93	rexlimddv 3140	1 ⊢ ((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) → seq0( + , (𝑘 ∈ ℕ₀ ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))) ∈ dom ⇝ )

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1541 ∈ wcel 2113 ∀wral 3048 ∃wrex 3057 {crab 3396 ⊆ wss 3898 class class class wbr 5095 ↦ cmpt 5176 dom cdm 5621 ∘ ccom 5625 ⟶wf 6484 ‘cfv 6488 (class class class)co 7354 ℂcc 11013 ℝcr 11014 0cc0 11015 1c1 11016 + caddc 11018 · cmul 11020 ℝ^*cxr 11154 < clt 11155 ≤ cle 11156 − cmin 11353 / cdiv 11783 ℕ₀cn0 12390 ℤ_≥cuz 12740 ℝ⁺crp 12894 seqcseq 13912 ↑cexp 13972 abscabs 15145 ⇝ cli 15395 Σcsu 15597 ∞Metcxmet 21280 ballcbl 21282

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 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2182 ax-ext 2705 ax-rep 5221 ax-sep 5238 ax-nul 5248 ax-pow 5307 ax-pr 5374 ax-un 7676 ax-inf2 9540 ax-cnex 11071 ax-resscn 11072 ax-1cn 11073 ax-icn 11074 ax-addcl 11075 ax-addrcl 11076 ax-mulcl 11077 ax-mulrcl 11078 ax-mulcom 11079 ax-addass 11080 ax-mulass 11081 ax-distr 11082 ax-i2m1 11083 ax-1ne0 11084 ax-1rid 11085 ax-rnegex 11086 ax-rrecex 11087 ax-cnre 11088 ax-pre-lttri 11089 ax-pre-lttrn 11090 ax-pre-ltadd 11091 ax-pre-mulgt0 11092 ax-pre-sup 11093

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2725 df-clel 2808 df-nfc 2882 df-ne 2930 df-nel 3034 df-ral 3049 df-rex 3058 df-rmo 3347 df-reu 3348 df-rab 3397 df-v 3439 df-sbc 3738 df-csb 3847 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-pss 3918 df-nul 4283 df-if 4477 df-pw 4553 df-sn 4578 df-pr 4580 df-op 4584 df-uni 4861 df-int 4900 df-iun 4945 df-br 5096 df-opab 5158 df-mpt 5177 df-tr 5203 df-id 5516 df-eprel 5521 df-po 5529 df-so 5530 df-fr 5574 df-se 5575 df-we 5576 df-xp 5627 df-rel 5628 df-cnv 5629 df-co 5630 df-dm 5631 df-rn 5632 df-res 5633 df-ima 5634 df-pred 6255 df-ord 6316 df-on 6317 df-lim 6318 df-suc 6319 df-iota 6444 df-fun 6490 df-fn 6491 df-f 6492 df-f1 6493 df-fo 6494 df-f1o 6495 df-fv 6496 df-isom 6497 df-riota 7311 df-ov 7357 df-oprab 7358 df-mpo 7359 df-om 7805 df-1st 7929 df-2nd 7930 df-frecs 8219 df-wrecs 8250 df-recs 8299 df-rdg 8337 df-1o 8393 df-er 8630 df-map 8760 df-pm 8761 df-en 8878 df-dom 8879 df-sdom 8880 df-fin 8881 df-sup 9335 df-inf 9336 df-oi 9405 df-card 9841 df-pnf 11157 df-mnf 11158 df-xr 11159 df-ltxr 11160 df-le 11161 df-sub 11355 df-neg 11356 df-div 11784 df-nn 12135 df-2 12197 df-3 12198 df-n0 12391 df-z 12478 df-uz 12741 df-rp 12895 df-xadd 13016 df-ico 13255 df-fz 13412 df-fzo 13559 df-fl 13700 df-seq 13913 df-exp 13973 df-hash 14242 df-cj 15010 df-re 15011 df-im 15012 df-sqrt 15146 df-abs 15147 df-limsup 15382 df-clim 15399 df-rlim 15400 df-sum 15598 df-psmet 21287 df-xmet 21288 df-met 21289 df-bl 21290

This theorem is referenced by: abelthlem6 26376 abelthlem7 26378

W3C validator