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 26768

Description: Lemma for abelth 26774. (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 13007	. . . 4 ⊢ ℕ₀ = (ℤ_≥‘0)
2		0zd 12709	. . . 4 ⊢ (𝜑 → 0 ∈ ℤ)
3		1rp 13128	. . . . 5 ⊢ 1 ∈ ℝ⁺
4	3	a1i 11	. . . 4 ⊢ (𝜑 → 1 ∈ ℝ⁺)
5		eqidd 2761	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ₀) → (seq0( + , 𝐴)‘𝑚) = (seq0( + , 𝐴)‘𝑚))
6		abelth.7	. . . 4 ⊢ (𝜑 → seq0( + , 𝐴) ⇝ 0)
7	1, 2, 4, 5, 6	climi0 15685	. . 3 ⊢ (𝜑 → ∃𝑗 ∈ ℕ₀ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)
8	7	adantr 486	. 2 ⊢ ((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) → ∃𝑗 ∈ ℕ₀ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)
9		simprl 783	. . 3 ⊢ (((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) → 𝑗 ∈ ℕ₀)
10		oveq2 7429	. . . . . 6 ⊢ (𝑛 = 𝑖 → ((abs‘𝑋)↑𝑛) = ((abs‘𝑋)↑𝑖))
11		eqid 2760	. . . . . 6 ⊢ (𝑛 ∈ ℕ₀ ↦ ((abs‘𝑋)↑𝑛)) = (𝑛 ∈ ℕ₀ ↦ ((abs‘𝑋)↑𝑛))
12		ovex 7454	. . . . . 6 ⊢ ((abs‘𝑋)↑𝑖) ∈ V
13	10, 11, 12	fvmpt 6994	. . . . 5 ⊢ (𝑖 ∈ ℕ₀ → ((𝑛 ∈ ℕ₀ ↦ ((abs‘𝑋)↑𝑛))‘𝑖) = ((abs‘𝑋)↑𝑖))
14	13	adantl 487	. . . 4 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ ℕ₀) → ((𝑛 ∈ ℕ₀ ↦ ((abs‘𝑋)↑𝑛))‘𝑖) = ((abs‘𝑋)↑𝑖))
15		cnxmet 25097	. . . . . . . 8 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
16		0cn 11302	. . . . . . . 8 ⊢ 0 ∈ ℂ
17		1xr 11372	. . . . . . . 8 ⊢ 1 ∈ ℝ^*
18		blssm 24743	. . . . . . . 8 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ ∧ 1 ∈ ℝ^*) → (0(ball‘(abs ∘ − ))1) ⊆ ℂ)
19	15, 16, 17, 18	mp3an 1490	. . . . . . 7 ⊢ (0(ball‘(abs ∘ − ))1) ⊆ ℂ
20		simplr 781	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) → 𝑋 ∈ (0(ball‘(abs ∘ − ))1))
21	19, 20	sselid 3906	. . . . . 6 ⊢ (((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) → 𝑋 ∈ ℂ)
22	21	abscld 15612	. . . . 5 ⊢ (((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) → (abs‘𝑋) ∈ ℝ)
23		reexpcl 14225	. . . . 5 ⊢ (((abs‘𝑋) ∈ ℝ ∧ 𝑖 ∈ ℕ₀) → ((abs‘𝑋)↑𝑖) ∈ ℝ)
24	22, 23	sylan 592	. . . 4 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ ℕ₀) → ((abs‘𝑋)↑𝑖) ∈ ℝ)
25	14, 24	eqeltrd 2860	. . 3 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ ℕ₀) → ((𝑛 ∈ ℕ₀ ↦ ((abs‘𝑋)↑𝑛))‘𝑖) ∈ ℝ)
26		fveq2 6886	. . . . . . 7 ⊢ (𝑘 = 𝑖 → (seq0( + , 𝐴)‘𝑘) = (seq0( + , 𝐴)‘𝑖))
27		oveq2 7429	. . . . . . 7 ⊢ (𝑘 = 𝑖 → (𝑋↑𝑘) = (𝑋↑𝑖))
28	26, 27	oveq12d 7439	. . . . . 6 ⊢ (𝑘 = 𝑖 → ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)) = ((seq0( + , 𝐴)‘𝑖) · (𝑋↑𝑖)))
29		eqid 2760	. . . . . 6 ⊢ (𝑘 ∈ ℕ₀ ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘))) = (𝑘 ∈ ℕ₀ ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))
30		ovex 7454	. . . . . 6 ⊢ ((seq0( + , 𝐴)‘𝑖) · (𝑋↑𝑖)) ∈ V
31	28, 29, 30	fvmpt 6994	. . . . 5 ⊢ (𝑖 ∈ ℕ₀ → ((𝑘 ∈ ℕ₀ ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))‘𝑖) = ((seq0( + , 𝐴)‘𝑖) · (𝑋↑𝑖)))
32	31	adantl 487	. . . 4 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ ℕ₀) → ((𝑘 ∈ ℕ₀ ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))‘𝑖) = ((seq0( + , 𝐴)‘𝑖) · (𝑋↑𝑖)))
33		abelth.1	. . . . . . . . 9 ⊢ (𝜑 → 𝐴:ℕ₀⟶ℂ)
34	33	ffvelcdmda 7085	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ₀) → (𝐴‘𝑥) ∈ ℂ)
35	1, 2, 34	serf 14177	. . . . . . 7 ⊢ (𝜑 → seq0( + , 𝐴):ℕ₀⟶ℂ)
36	35	ad2antrr 739	. . . . . 6 ⊢ (((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) → seq0( + , 𝐴):ℕ₀⟶ℂ)
37	36	ffvelcdmda 7085	. . . . 5 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ ℕ₀) → (seq0( + , 𝐴)‘𝑖) ∈ ℂ)
38		expcl 14226	. . . . . 6 ⊢ ((𝑋 ∈ ℂ ∧ 𝑖 ∈ ℕ₀) → (𝑋↑𝑖) ∈ ℂ)
39	21, 38	sylan 592	. . . . 5 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ ℕ₀) → (𝑋↑𝑖) ∈ ℂ)
40	37, 39	mulcld 11333	. . . 4 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ ℕ₀) → ((seq0( + , 𝐴)‘𝑖) · (𝑋↑𝑖)) ∈ ℂ)
41	32, 40	eqeltrd 2860	. . 3 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ ℕ₀) → ((𝑘 ∈ ℕ₀ ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))‘𝑖) ∈ ℂ)
42	22	recnd 11341	. . . . 5 ⊢ (((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) → (abs‘𝑋) ∈ ℂ)
43		absidm 15497	. . . . . . 7 ⊢ (𝑋 ∈ ℂ → (abs‘(abs‘𝑋)) = (abs‘𝑋))
44	21, 43	syl 18	. . . . . 6 ⊢ (((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) → (abs‘(abs‘𝑋)) = (abs‘𝑋))
45		eqid 2760	. . . . . . . . . 10 ⊢ (abs ∘ − ) = (abs ∘ − )
46	45	cnmetdval 25095	. . . . . . . . 9 ⊢ ((𝑋 ∈ ℂ ∧ 0 ∈ ℂ) → (𝑋(abs ∘ − )0) = (abs‘(𝑋 − 0)))
47	21, 16, 46	sylancl 598	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) → (𝑋(abs ∘ − )0) = (abs‘(𝑋 − 0)))
48	21	subid1d 11662	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) → (𝑋 − 0) = 𝑋)
49	48	fveq2d 6890	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) → (abs‘(𝑋 − 0)) = (abs‘𝑋))
50	47, 49	eqtrd 2795	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) → (𝑋(abs ∘ − )0) = (abs‘𝑋))
51		elbl3 24717	. . . . . . . . . 10 ⊢ ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈ ℝ^*) ∧ (0 ∈ ℂ ∧ 𝑋 ∈ ℂ)) → (𝑋 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝑋(abs ∘ − )0) < 1))
52	15, 17, 51	mpanl12 715	. . . . . . . . 9 ⊢ ((0 ∈ ℂ ∧ 𝑋 ∈ ℂ) → (𝑋 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝑋(abs ∘ − )0) < 1))
53	16, 21, 52	sylancr 599	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) → (𝑋 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝑋(abs ∘ − )0) < 1))
54	20, 53	mpbid 235	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) → (𝑋(abs ∘ − )0) < 1)
55	50, 54	eqbrtrrd 5128	. . . . . 6 ⊢ (((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) → (abs‘𝑋) < 1)
56	44, 55	eqbrtrd 5126	. . . . 5 ⊢ (((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) → (abs‘(abs‘𝑋)) < 1)
57	42, 56, 14	geolim 16045	. . . 4 ⊢ (((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) → seq0( + , (𝑛 ∈ ℕ₀ ↦ ((abs‘𝑋)↑𝑛))) ⇝ (1 / (1 − (abs‘𝑋))))
58		climrel 15665	. . . . 5 ⊢ Rel ⇝
59	58	releldmi 5929	. . . 4 ⊢ (seq0( + , (𝑛 ∈ ℕ₀ ↦ ((abs‘𝑋)↑𝑛))) ⇝ (1 / (1 − (abs‘𝑋))) → seq0( + , (𝑛 ∈ ℕ₀ ↦ ((abs‘𝑋)↑𝑛))) ∈ dom ⇝ )
60	57, 59	syl 18	. . 3 ⊢ (((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) → seq0( + , (𝑛 ∈ ℕ₀ ↦ ((abs‘𝑋)↑𝑛))) ∈ dom ⇝ )
61		1red 11313	. . 3 ⊢ (((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) → 1 ∈ ℝ)
62	36	adantr 486	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ_≥‘𝑗)) → seq0( + , 𝐴):ℕ₀⟶ℂ)
63		eluznn0 13048	. . . . . . . . 9 ⊢ ((𝑗 ∈ ℕ₀ ∧ 𝑖 ∈ (ℤ_≥‘𝑗)) → 𝑖 ∈ ℕ₀)
64	9, 63	sylan 592	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ_≥‘𝑗)) → 𝑖 ∈ ℕ₀)
65	62, 64	ffvelcdmd 7086	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ_≥‘𝑗)) → (seq0( + , 𝐴)‘𝑖) ∈ ℂ)
66	64, 39	syldan 603	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ_≥‘𝑗)) → (𝑋↑𝑖) ∈ ℂ)
67	65, 66	absmuld 15630	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ_≥‘𝑗)) → (abs‘((seq0( + , 𝐴)‘𝑖) · (𝑋↑𝑖))) = ((abs‘(seq0( + , 𝐴)‘𝑖)) · (abs‘(𝑋↑𝑖))))
68	21	adantr 486	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ_≥‘𝑗)) → 𝑋 ∈ ℂ)
69	68, 64	absexpd 15628	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ_≥‘𝑗)) → (abs‘(𝑋↑𝑖)) = ((abs‘𝑋)↑𝑖))
70	69	oveq2d 7437	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ_≥‘𝑗)) → ((abs‘(seq0( + , 𝐴)‘𝑖)) · (abs‘(𝑋↑𝑖))) = ((abs‘(seq0( + , 𝐴)‘𝑖)) · ((abs‘𝑋)↑𝑖)))
71	67, 70	eqtrd 2795	. . . . 5 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ_≥‘𝑗)) → (abs‘((seq0( + , 𝐴)‘𝑖) · (𝑋↑𝑖))) = ((abs‘(seq0( + , 𝐴)‘𝑖)) · ((abs‘𝑋)↑𝑖)))
72	65	abscld 15612	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ_≥‘𝑗)) → (abs‘(seq0( + , 𝐴)‘𝑖)) ∈ ℝ)
73		1red 11313	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ_≥‘𝑗)) → 1 ∈ ℝ)
74	64, 24	syldan 603	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ_≥‘𝑗)) → ((abs‘𝑋)↑𝑖) ∈ ℝ)
75	66	absge0d 15620	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ_≥‘𝑗)) → 0 ≤ (abs‘(𝑋↑𝑖)))
76	75, 69	breqtrd 5130	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ_≥‘𝑗)) → 0 ≤ ((abs‘𝑋)↑𝑖))
77		simprr 785	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) → ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)
78		2fveq3 6891	. . . . . . . . . 10 ⊢ (𝑚 = 𝑖 → (abs‘(seq0( + , 𝐴)‘𝑚)) = (abs‘(seq0( + , 𝐴)‘𝑖)))
79	78	breq1d 5112	. . . . . . . . 9 ⊢ (𝑚 = 𝑖 → ((abs‘(seq0( + , 𝐴)‘𝑚)) < 1 ↔ (abs‘(seq0( + , 𝐴)‘𝑖)) < 1))
80	79	rspccva 3575	. . . . . . . 8 ⊢ ((∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1 ∧ 𝑖 ∈ (ℤ_≥‘𝑗)) → (abs‘(seq0( + , 𝐴)‘𝑖)) < 1)
81	77, 80	sylan 592	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ_≥‘𝑗)) → (abs‘(seq0( + , 𝐴)‘𝑖)) < 1)
82		1re 11312	. . . . . . . 8 ⊢ 1 ∈ ℝ
83		ltle 11402	. . . . . . . 8 ⊢ (((abs‘(seq0( + , 𝐴)‘𝑖)) ∈ ℝ ∧ 1 ∈ ℝ) → ((abs‘(seq0( + , 𝐴)‘𝑖)) < 1 → (abs‘(seq0( + , 𝐴)‘𝑖)) ≤ 1))
84	72, 82, 83	sylancl 598	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ_≥‘𝑗)) → ((abs‘(seq0( + , 𝐴)‘𝑖)) < 1 → (abs‘(seq0( + , 𝐴)‘𝑖)) ≤ 1))
85	81, 84	mpd 16	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ_≥‘𝑗)) → (abs‘(seq0( + , 𝐴)‘𝑖)) ≤ 1)
86	72, 73, 74, 76, 85	lemul1ad 12260	. . . . 5 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ_≥‘𝑗)) → ((abs‘(seq0( + , 𝐴)‘𝑖)) · ((abs‘𝑋)↑𝑖)) ≤ (1 · ((abs‘𝑋)↑𝑖)))
87	71, 86	eqbrtrd 5126	. . . 4 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ_≥‘𝑗)) → (abs‘((seq0( + , 𝐴)‘𝑖) · (𝑋↑𝑖))) ≤ (1 · ((abs‘𝑋)↑𝑖)))
88	64, 31	syl 18	. . . . 5 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ_≥‘𝑗)) → ((𝑘 ∈ ℕ₀ ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))‘𝑖) = ((seq0( + , 𝐴)‘𝑖) · (𝑋↑𝑖)))
89	88	fveq2d 6890	. . . 4 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ_≥‘𝑗)) → (abs‘((𝑘 ∈ ℕ₀ ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))‘𝑖)) = (abs‘((seq0( + , 𝐴)‘𝑖) · (𝑋↑𝑖))))
90	64, 13	syl 18	. . . . 5 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ_≥‘𝑗)) → ((𝑛 ∈ ℕ₀ ↦ ((abs‘𝑋)↑𝑛))‘𝑖) = ((abs‘𝑋)↑𝑖))
91	90	oveq2d 7437	. . . 4 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ_≥‘𝑗)) → (1 · ((𝑛 ∈ ℕ₀ ↦ ((abs‘𝑋)↑𝑛))‘𝑖)) = (1 · ((abs‘𝑋)↑𝑖)))
92	87, 89, 91	3brtr4d 5136	. . 3 ⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ_≥‘𝑗)) → (abs‘((𝑘 ∈ ℕ₀ ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))‘𝑖)) ≤ (1 · ((𝑛 ∈ ℕ₀ ↦ ((abs‘𝑋)↑𝑛))‘𝑖)))
93	1, 9, 25, 41, 60, 61, 92	cvgcmpce 15991	. 2 ⊢ (((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) ∧ (𝑗 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) → seq0( + , (𝑘 ∈ ℕ₀ ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))) ∈ dom ⇝ )
94	8, 93	rexlimddv 3169	1 ⊢ ((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) → seq0( + , (𝑘 ∈ ℕ₀ ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))) ∈ dom ⇝ )

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1569 ∈ wcel 2144 ∀wral 3076 ∃wrex 3086 {crab 3412 ⊆ wss 3895 class class class wbr 5102 ↦ cmpt 5185 dom cdm 5650 ∘ ccom 5654 ⟶wf 6535 ‘cfv 6539 (class class class)co 7421 ℂcc 11202 ℝcr 11203 0cc0 11204 1c1 11205 + caddc 11207 · cmul 11209 ℝ^*cxr 11346 < clt 11347 ≤ cle 11348 − cmin 11545 / cdiv 11977 ℕ₀cn0 12610 ℤ_≥cuz 12969 ℝ⁺crp 13124 seqcseq 14148 ↑cexp 14208 abscabs 15407 ⇝ cli 15657 Σcsu 15859 ∞Metcxmet 21669 ballcbl 21671

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7752 ax-inf2 9646 ax-cnex 11260 ax-resscn 11261 ax-1cn 11262 ax-icn 11263 ax-addcl 11264 ax-addrcl 11265 ax-mulcl 11266 ax-mulrcl 11267 ax-mulcom 11268 ax-addass 11269 ax-mulass 11270 ax-distr 11271 ax-i2m1 11272 ax-1ne0 11273 ax-1rid 11274 ax-rnegex 11275 ax-rrecex 11276 ax-cnre 11277 ax-pre-lttri 11278 ax-pre-lttrn 11279 ax-pre-ltadd 11280 ax-pre-mulgt0 11281 ax-pre-sup 11282

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-op 4835 df-uni 4867 df-int 4907 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-se 5604 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6541 df-fn 6542 df-f 6543 df-f1 6544 df-fo 6545 df-f1o 6546 df-fv 6547 df-isom 6548 df-riota 7378 df-ov 7424 df-oprab 7425 df-mpo 7426 df-om 7879 df-1st 8002 df-2nd 8003 df-frecs 8303 df-wrecs 8334 df-recs 8383 df-rdg 8422 df-1o 8480 df-er 8721 df-map 8853 df-pm 8854 df-en 8978 df-dom 8979 df-sdom 8980 df-fin 8981 df-sup 9438 df-inf 9439 df-oi 9508 df-card 10024 df-pnf 11349 df-mnf 11350 df-xr 11351 df-ltxr 11352 df-le 11353 df-sub 11547 df-neg 11548 df-div 11978 df-nn 12340 df-2 12409 df-3 12410 df-n0 12611 df-z 12698 df-uz 12970 df-rp 13125 df-xadd 13246 df-ico 13486 df-fz 13644 df-fzo 13793 df-fl 13936 df-seq 14149 df-exp 14209 df-hash 14479 df-cj 15272 df-re 15273 df-im 15274 df-sqrt 15408 df-abs 15409 df-limsup 15644 df-clim 15661 df-rlim 15662 df-sum 15860 df-psmet 21676 df-xmet 21677 df-met 21678 df-bl 21679

This theorem is used by: abelthlem6 26769 abelthlem7 26771

W3C validator