cvgdvgrat - Mathbox for Steve Rodriguez

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

Theorem cvgdvgrat 44282

Description: Ratio test for convergence and divergence of a complex infinite series. If the ratio 𝑅 of the absolute values of successive terms in an infinite sequence 𝐹 converges to less than one, then the infinite sum of the terms of 𝐹 converges to a complex number; and if 𝑅 converges greater then the sum diverges. This combined form of cvgrat 15931 and dvgrat 44281 directly uses the limit of the ratio.

(It also demonstrates how to use climi2 15557 and absltd 15478 to transform a limit to an inequality cf. https://math.stackexchange.com/q/2215191 15478, and how to use r19.29a 3168 in a similar fashion to Mario Carneiro's proof sketch with rexlimdva 3161 at https://groups.google.com/g/metamath/c/2RPikOiXLMo 3161.) (Contributed by Steve Rodriguez, 28-Feb-2020.)

**Hypotheses**
Ref	Expression
cvgdvgrat.z	⊢ 𝑍 = (ℤ_≥‘𝑀)
cvgdvgrat.w	⊢ 𝑊 = (ℤ_≥‘𝑁)
cvgdvgrat.n	⊢ (𝜑 → 𝑁 ∈ 𝑍)
cvgdvgrat.f	⊢ (𝜑 → 𝐹 ∈ 𝑉)
cvgdvgrat.c	⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)
cvgdvgrat.n0	⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → (𝐹‘𝑘) ≠ 0)
cvgdvgrat.r	⊢ 𝑅 = (𝑘 ∈ 𝑊 ↦ (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))))
cvgdvgrat.cvg	⊢ (𝜑 → 𝑅 ⇝ 𝐿)
cvgdvgrat.n1	⊢ (𝜑 → 𝐿 ≠ 1)

**Assertion**
Ref	Expression
cvgdvgrat	⊢ (𝜑 → (𝐿 < 1 ↔ seq𝑀( + , 𝐹) ∈ dom ⇝ ))

Distinct variable groups: 𝜑,𝑘 𝑘,𝐹 𝑘,𝐿 𝑘,𝑁 𝑘,𝑊 𝑅,𝑘 𝑘,𝑀 𝑘,𝑍 Allowed substitution hint: 𝑉(𝑘)

Proof of Theorem cvgdvgrat Dummy variables 𝑖 𝑛 𝑟 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		cvgdvgrat.w	. . . . . . . . 9 ⊢ 𝑊 = (ℤ_≥‘𝑁)
2		eqid 2740	. . . . . . . . 9 ⊢ (ℤ_≥‘𝑛) = (ℤ_≥‘𝑛)
3		elioore 13437	. . . . . . . . . 10 ⊢ (𝑟 ∈ (𝐿(,)1) → 𝑟 ∈ ℝ)
4	3	ad3antlr 730	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑘)))) → 𝑟 ∈ ℝ)
5		cvgdvgrat.n	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑁 ∈ 𝑍)
6		cvgdvgrat.z	. . . . . . . . . . . . . . . . 17 ⊢ 𝑍 = (ℤ_≥‘𝑀)
7	5, 6	eleqtrdi 2854	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘𝑀))
8		eluzelz 12913	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → 𝑁 ∈ ℤ)
9	7, 8	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑁 ∈ ℤ)
10		cvgdvgrat.cvg	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑅 ⇝ 𝐿)
11		cvgdvgrat.r	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑅 = (𝑘 ∈ 𝑊 ↦ (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))))
12	11	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑅 = (𝑘 ∈ 𝑊 ↦ (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘)))))
13	1	peano2uzs 12967	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ 𝑊 → (𝑘 + 1) ∈ 𝑊)
14		ovex 7481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 + 1) ∈ V
15		eleq1 2832	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 = (𝑘 + 1) → (𝑖 ∈ 𝑊 ↔ (𝑘 + 1) ∈ 𝑊))
16	15	anbi2d 629	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = (𝑘 + 1) → ((𝜑 ∧ 𝑖 ∈ 𝑊) ↔ (𝜑 ∧ (𝑘 + 1) ∈ 𝑊)))
17		fveq2 6920	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 = (𝑘 + 1) → (𝐹‘𝑖) = (𝐹‘(𝑘 + 1)))
18	17	eleq1d 2829	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = (𝑘 + 1) → ((𝐹‘𝑖) ∈ ℂ ↔ (𝐹‘(𝑘 + 1)) ∈ ℂ))
19	16, 18	imbi12d 344	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = (𝑘 + 1) → (((𝜑 ∧ 𝑖 ∈ 𝑊) → (𝐹‘𝑖) ∈ ℂ) ↔ ((𝜑 ∧ (𝑘 + 1) ∈ 𝑊) → (𝐹‘(𝑘 + 1)) ∈ ℂ)))
20		eleq1 2832	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = 𝑖 → (𝑘 ∈ 𝑊 ↔ 𝑖 ∈ 𝑊))
21	20	anbi2d 629	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = 𝑖 → ((𝜑 ∧ 𝑘 ∈ 𝑊) ↔ (𝜑 ∧ 𝑖 ∈ 𝑊)))
22		fveq2 6920	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = 𝑖 → (𝐹‘𝑘) = (𝐹‘𝑖))
23	22	eleq1d 2829	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = 𝑖 → ((𝐹‘𝑘) ∈ ℂ ↔ (𝐹‘𝑖) ∈ ℂ))
24	21, 23	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = 𝑖 → (((𝜑 ∧ 𝑘 ∈ 𝑊) → (𝐹‘𝑘) ∈ ℂ) ↔ ((𝜑 ∧ 𝑖 ∈ 𝑊) → (𝐹‘𝑖) ∈ ℂ)))
25	1	eleq2i 2836	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 ∈ 𝑊 ↔ 𝑘 ∈ (ℤ_≥‘𝑁))
26	6	uztrn2 12922	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑁 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) → 𝑘 ∈ 𝑍)
27	5, 26	sylan 579	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) → 𝑘 ∈ 𝑍)
28	25, 27	sylan2b 593	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → 𝑘 ∈ 𝑍)
29		cvgdvgrat.c	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)
30	28, 29	syldan 590	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → (𝐹‘𝑘) ∈ ℂ)
31	24, 30	chvarvv 1998	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑊) → (𝐹‘𝑖) ∈ ℂ)
32	14, 19, 31	vtocl 3570	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ 𝑊) → (𝐹‘(𝑘 + 1)) ∈ ℂ)
33	13, 32	sylan2 592	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → (𝐹‘(𝑘 + 1)) ∈ ℂ)
34		cvgdvgrat.n0	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → (𝐹‘𝑘) ≠ 0)
35	33, 30, 34	divcld 12070	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → ((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘)) ∈ ℂ)
36	35	abscld 15485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) ∈ ℝ)
37	12, 36	fvmpt2d 7042	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → (𝑅‘𝑘) = (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))))
38	37, 36	eqeltrd 2844	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → (𝑅‘𝑘) ∈ ℝ)
39	1, 9, 10, 38	climrecl 15629	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐿 ∈ ℝ)
40	39	rexrd 11340	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐿 ∈ ℝ^*)
41		1xr 11349	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℝ^*
42		elioo2 13448	. . . . . . . . . . . . 13 ⊢ ((𝐿 ∈ ℝ^* ∧ 1 ∈ ℝ^*) → (𝑟 ∈ (𝐿(,)1) ↔ (𝑟 ∈ ℝ ∧ 𝐿 < 𝑟 ∧ 𝑟 < 1)))
43	40, 41, 42	sylancl 585	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑟 ∈ (𝐿(,)1) ↔ (𝑟 ∈ ℝ ∧ 𝐿 < 𝑟 ∧ 𝑟 < 1)))
44	43	biimpa 476	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) → (𝑟 ∈ ℝ ∧ 𝐿 < 𝑟 ∧ 𝑟 < 1))
45	44	simp3d 1144	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) → 𝑟 < 1)
46	45	ad2antrr 725	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑘)))) → 𝑟 < 1)
47		simplr 768	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑘)))) → 𝑛 ∈ 𝑊)
48	31	ex 412	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑖 ∈ 𝑊 → (𝐹‘𝑖) ∈ ℂ))
49	48	ad3antrrr 729	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑘)))) → (𝑖 ∈ 𝑊 → (𝐹‘𝑖) ∈ ℂ))
50	49	imp 406	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑘)))) ∧ 𝑖 ∈ 𝑊) → (𝐹‘𝑖) ∈ ℂ)
51		fvoveq1 7471	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑖 → (𝐹‘(𝑘 + 1)) = (𝐹‘(𝑖 + 1)))
52	51	fveq2d 6924	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑖 → (abs‘(𝐹‘(𝑘 + 1))) = (abs‘(𝐹‘(𝑖 + 1))))
53	22	fveq2d 6924	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑖 → (abs‘(𝐹‘𝑘)) = (abs‘(𝐹‘𝑖)))
54	53	oveq2d 7464	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑖 → (𝑟 · (abs‘(𝐹‘𝑘))) = (𝑟 · (abs‘(𝐹‘𝑖))))
55	52, 54	breq12d 5179	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑖 → ((abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑘))) ↔ (abs‘(𝐹‘(𝑖 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑖)))))
56	55	rspccva 3634	. . . . . . . . . 10 ⊢ ((∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑘))) ∧ 𝑖 ∈ (ℤ_≥‘𝑛)) → (abs‘(𝐹‘(𝑖 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑖))))
57	56	adantll 713	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑘)))) ∧ 𝑖 ∈ (ℤ_≥‘𝑛)) → (abs‘(𝐹‘(𝑖 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑖))))
58	1, 2, 4, 46, 47, 50, 57	cvgrat 15931	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑘)))) → seq𝑁( + , 𝐹) ∈ dom ⇝ )
59	9	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) → 𝑁 ∈ ℤ)
60	44	simp2d 1143	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) → 𝐿 < 𝑟)
61		difrp 13095	. . . . . . . . . . . 12 ⊢ ((𝐿 ∈ ℝ ∧ 𝑟 ∈ ℝ) → (𝐿 < 𝑟 ↔ (𝑟 − 𝐿) ∈ ℝ⁺))
62	39, 3, 61	syl2an 595	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) → (𝐿 < 𝑟 ↔ (𝑟 − 𝐿) ∈ ℝ⁺))
63	60, 62	mpbid 232	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) → (𝑟 − 𝐿) ∈ ℝ⁺)
64	37	adantlr 714	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑘 ∈ 𝑊) → (𝑅‘𝑘) = (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))))
65	10	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) → 𝑅 ⇝ 𝐿)
66	1, 59, 63, 64, 65	climi2 15557	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) → ∃𝑛 ∈ 𝑊 ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿))
67	1	uztrn2 12922	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ 𝑊 ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → 𝑘 ∈ 𝑊)
68	67, 33	sylan2 592	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑛 ∈ 𝑊 ∧ 𝑘 ∈ (ℤ_≥‘𝑛))) → (𝐹‘(𝑘 + 1)) ∈ ℂ)
69	68	anassrs 467	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → (𝐹‘(𝑘 + 1)) ∈ ℂ)
70	69	adantllr 718	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → (𝐹‘(𝑘 + 1)) ∈ ℂ)
71	70	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (𝐹‘(𝑘 + 1)) ∈ ℂ)
72	71	abscld 15485	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (abs‘(𝐹‘(𝑘 + 1))) ∈ ℝ)
73	3	ad4antlr 732	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → 𝑟 ∈ ℝ)
74	67, 30	sylan2 592	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑛 ∈ 𝑊 ∧ 𝑘 ∈ (ℤ_≥‘𝑛))) → (𝐹‘𝑘) ∈ ℂ)
75	74	anassrs 467	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → (𝐹‘𝑘) ∈ ℂ)
76	75	adantllr 718	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → (𝐹‘𝑘) ∈ ℂ)
77	76	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (𝐹‘𝑘) ∈ ℂ)
78	77	abscld 15485	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (abs‘(𝐹‘𝑘)) ∈ ℝ)
79	73, 78	remulcld 11320	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (𝑟 · (abs‘(𝐹‘𝑘))) ∈ ℝ)
80	67, 34	sylan2 592	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑛 ∈ 𝑊 ∧ 𝑘 ∈ (ℤ_≥‘𝑛))) → (𝐹‘𝑘) ≠ 0)
81	80	anassrs 467	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → (𝐹‘𝑘) ≠ 0)
82	81	adantllr 718	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → (𝐹‘𝑘) ≠ 0)
83	82	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (𝐹‘𝑘) ≠ 0)
84	71, 77, 83	absdivd 15504	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) = ((abs‘(𝐹‘(𝑘 + 1))) / (abs‘(𝐹‘𝑘))))
85	70, 76, 82	divcld 12070	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → ((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘)) ∈ ℂ)
86	85	abscld 15485	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) ∈ ℝ)
87	39	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → 𝐿 ∈ ℝ)
88	86, 87	resubcld 11718	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿) ∈ ℝ)
89	3	ad3antlr 730	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → 𝑟 ∈ ℝ)
90	89, 87	resubcld 11718	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → (𝑟 − 𝐿) ∈ ℝ)
91	88, 90	absltd 15478	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → ((abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿) ↔ (-(𝑟 − 𝐿) < ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿) ∧ ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿) < (𝑟 − 𝐿))))
92	91	simplbda 499	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿) < (𝑟 − 𝐿))
93	71, 77, 83	divcld 12070	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → ((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘)) ∈ ℂ)
94	93	abscld 15485	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) ∈ ℝ)
95	39	ad4antr 731	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → 𝐿 ∈ ℝ)
96	94, 73, 95	ltsub1d 11899	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) < 𝑟 ↔ ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿) < (𝑟 − 𝐿)))
97	92, 96	mpbird 257	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) < 𝑟)
98	84, 97	eqbrtrrd 5190	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → ((abs‘(𝐹‘(𝑘 + 1))) / (abs‘(𝐹‘𝑘))) < 𝑟)
99	77, 83	absrpcld 15497	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (abs‘(𝐹‘𝑘)) ∈ ℝ⁺)
100	72, 73, 99	ltdivmuld 13150	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (((abs‘(𝐹‘(𝑘 + 1))) / (abs‘(𝐹‘𝑘))) < 𝑟 ↔ (abs‘(𝐹‘(𝑘 + 1))) < ((abs‘(𝐹‘𝑘)) · 𝑟)))
101	98, 100	mpbid 232	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (abs‘(𝐹‘(𝑘 + 1))) < ((abs‘(𝐹‘𝑘)) · 𝑟))
102	99	rpcnd 13101	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (abs‘(𝐹‘𝑘)) ∈ ℂ)
103	73	recnd 11318	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → 𝑟 ∈ ℂ)
104	102, 103	mulcomd 11311	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → ((abs‘(𝐹‘𝑘)) · 𝑟) = (𝑟 · (abs‘(𝐹‘𝑘))))
105	101, 104	breqtrd 5192	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (abs‘(𝐹‘(𝑘 + 1))) < (𝑟 · (abs‘(𝐹‘𝑘))))
106	72, 79, 105	ltled 11438	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑘))))
107	106	ex 412	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → ((abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿) → (abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑘)))))
108	107	ralimdva 3173	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) → (∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿) → ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑘)))))
109	108	reximdva 3174	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) → (∃𝑛 ∈ 𝑊 ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿) → ∃𝑛 ∈ 𝑊 ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑘)))))
110	66, 109	mpd 15	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) → ∃𝑛 ∈ 𝑊 ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑘))))
111	58, 110	r19.29a 3168	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) → seq𝑁( + , 𝐹) ∈ dom ⇝ )
112	111	ralrimiva 3152	. . . . . 6 ⊢ (𝜑 → ∀𝑟 ∈ (𝐿(,)1)seq𝑁( + , 𝐹) ∈ dom ⇝ )
113	112	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝐿 < 1) → ∀𝑟 ∈ (𝐿(,)1)seq𝑁( + , 𝐹) ∈ dom ⇝ )
114		ioon0 13433	. . . . . . . 8 ⊢ ((𝐿 ∈ ℝ^* ∧ 1 ∈ ℝ^*) → ((𝐿(,)1) ≠ ∅ ↔ 𝐿 < 1))
115	40, 41, 114	sylancl 585	. . . . . . 7 ⊢ (𝜑 → ((𝐿(,)1) ≠ ∅ ↔ 𝐿 < 1))
116	115	biimpar 477	. . . . . 6 ⊢ ((𝜑 ∧ 𝐿 < 1) → (𝐿(,)1) ≠ ∅)
117		r19.3rzv 4522	. . . . . 6 ⊢ ((𝐿(,)1) ≠ ∅ → (seq𝑁( + , 𝐹) ∈ dom ⇝ ↔ ∀𝑟 ∈ (𝐿(,)1)seq𝑁( + , 𝐹) ∈ dom ⇝ ))
118	116, 117	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝐿 < 1) → (seq𝑁( + , 𝐹) ∈ dom ⇝ ↔ ∀𝑟 ∈ (𝐿(,)1)seq𝑁( + , 𝐹) ∈ dom ⇝ ))
119	113, 118	mpbird 257	. . . 4 ⊢ ((𝜑 ∧ 𝐿 < 1) → seq𝑁( + , 𝐹) ∈ dom ⇝ )
120	6, 5, 29	iserex 15705	. . . . 5 ⊢ (𝜑 → (seq𝑀( + , 𝐹) ∈ dom ⇝ ↔ seq𝑁( + , 𝐹) ∈ dom ⇝ ))
121	120	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝐿 < 1) → (seq𝑀( + , 𝐹) ∈ dom ⇝ ↔ seq𝑁( + , 𝐹) ∈ dom ⇝ ))
122	119, 121	mpbird 257	. . 3 ⊢ ((𝜑 ∧ 𝐿 < 1) → seq𝑀( + , 𝐹) ∈ dom ⇝ )
123	122	ex 412	. 2 ⊢ (𝜑 → (𝐿 < 1 → seq𝑀( + , 𝐹) ∈ dom ⇝ ))
124		cvgdvgrat.n1	. . . . . 6 ⊢ (𝜑 → 𝐿 ≠ 1)
125		1red 11291	. . . . . . 7 ⊢ (𝜑 → 1 ∈ ℝ)
126	39, 125	lttri2d 11429	. . . . . 6 ⊢ (𝜑 → (𝐿 ≠ 1 ↔ (𝐿 < 1 ∨ 1 < 𝐿)))
127	124, 126	mpbid 232	. . . . 5 ⊢ (𝜑 → (𝐿 < 1 ∨ 1 < 𝐿))
128	127	orcanai 1003	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝐿 < 1) → 1 < 𝐿)
129		simplr 768	. . . . . . . 8 ⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))) → 𝑛 ∈ 𝑊)
130		cvgdvgrat.f	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 ∈ 𝑉)
131	130	ad3antrrr 729	. . . . . . . 8 ⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))) → 𝐹 ∈ 𝑉)
132	48	ad3antrrr 729	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))) → (𝑖 ∈ 𝑊 → (𝐹‘𝑖) ∈ ℂ))
133	132	imp 406	. . . . . . . 8 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))) ∧ 𝑖 ∈ 𝑊) → (𝐹‘𝑖) ∈ ℂ)
134	1	uztrn2 12922	. . . . . . . . . . . 12 ⊢ ((𝑛 ∈ 𝑊 ∧ 𝑖 ∈ (ℤ_≥‘𝑛)) → 𝑖 ∈ 𝑊)
135	22	neeq1d 3006	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑖 → ((𝐹‘𝑘) ≠ 0 ↔ (𝐹‘𝑖) ≠ 0))
136	21, 135	imbi12d 344	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑖 → (((𝜑 ∧ 𝑘 ∈ 𝑊) → (𝐹‘𝑘) ≠ 0) ↔ ((𝜑 ∧ 𝑖 ∈ 𝑊) → (𝐹‘𝑖) ≠ 0)))
137	136, 34	chvarvv 1998	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑊) → (𝐹‘𝑖) ≠ 0)
138	134, 137	sylan2 592	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑛 ∈ 𝑊 ∧ 𝑖 ∈ (ℤ_≥‘𝑛))) → (𝐹‘𝑖) ≠ 0)
139	138	anassrs 467	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑊) ∧ 𝑖 ∈ (ℤ_≥‘𝑛)) → (𝐹‘𝑖) ≠ 0)
140	139	adantllr 718	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑖 ∈ (ℤ_≥‘𝑛)) → (𝐹‘𝑖) ≠ 0)
141	140	adantlr 714	. . . . . . . 8 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))) ∧ 𝑖 ∈ (ℤ_≥‘𝑛)) → (𝐹‘𝑖) ≠ 0)
142	53, 52	breq12d 5179	. . . . . . . . . 10 ⊢ (𝑘 = 𝑖 → ((abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1))) ↔ (abs‘(𝐹‘𝑖)) ≤ (abs‘(𝐹‘(𝑖 + 1)))))
143	142	rspccva 3634	. . . . . . . . 9 ⊢ ((∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1))) ∧ 𝑖 ∈ (ℤ_≥‘𝑛)) → (abs‘(𝐹‘𝑖)) ≤ (abs‘(𝐹‘(𝑖 + 1))))
144	143	adantll 713	. . . . . . . 8 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))) ∧ 𝑖 ∈ (ℤ_≥‘𝑛)) → (abs‘(𝐹‘𝑖)) ≤ (abs‘(𝐹‘(𝑖 + 1))))
145	1, 2, 129, 131, 133, 141, 144	dvgrat 44281	. . . . . . 7 ⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))) → seq𝑁( + , 𝐹) ∉ dom ⇝ )
146	9	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 1 < 𝐿) → 𝑁 ∈ ℤ)
147		1re 11290	. . . . . . . . . . 11 ⊢ 1 ∈ ℝ
148		difrp 13095	. . . . . . . . . . 11 ⊢ ((1 ∈ ℝ ∧ 𝐿 ∈ ℝ) → (1 < 𝐿 ↔ (𝐿 − 1) ∈ ℝ⁺))
149	147, 39, 148	sylancr 586	. . . . . . . . . 10 ⊢ (𝜑 → (1 < 𝐿 ↔ (𝐿 − 1) ∈ ℝ⁺))
150	149	biimpa 476	. . . . . . . . 9 ⊢ ((𝜑 ∧ 1 < 𝐿) → (𝐿 − 1) ∈ ℝ⁺)
151	37	adantlr 714	. . . . . . . . 9 ⊢ (((𝜑 ∧ 1 < 𝐿) ∧ 𝑘 ∈ 𝑊) → (𝑅‘𝑘) = (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))))
152	10	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 1 < 𝐿) → 𝑅 ⇝ 𝐿)
153	1, 146, 150, 151, 152	climi2 15557	. . . . . . . 8 ⊢ ((𝜑 ∧ 1 < 𝐿) → ∃𝑛 ∈ 𝑊 ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1))
154	75	adantllr 718	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → (𝐹‘𝑘) ∈ ℂ)
155	154	adantr 480	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (𝐹‘𝑘) ∈ ℂ)
156	155	abscld 15485	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (abs‘(𝐹‘𝑘)) ∈ ℝ)
157	69	adantllr 718	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → (𝐹‘(𝑘 + 1)) ∈ ℂ)
158	157	adantr 480	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (𝐹‘(𝑘 + 1)) ∈ ℂ)
159	158	abscld 15485	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (abs‘(𝐹‘(𝑘 + 1))) ∈ ℝ)
160	81	adantllr 718	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → (𝐹‘𝑘) ≠ 0)
161	160	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (𝐹‘𝑘) ≠ 0)
162	155, 161	absrpcld 15497	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (abs‘(𝐹‘𝑘)) ∈ ℝ⁺)
163	162	rpcnd 13101	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (abs‘(𝐹‘𝑘)) ∈ ℂ)
164	163	mullidd 11308	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (1 · (abs‘(𝐹‘𝑘))) = (abs‘(𝐹‘𝑘)))
165	39	ad4antr 731	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → 𝐿 ∈ ℝ)
166	165	recnd 11318	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → 𝐿 ∈ ℂ)
167		1cnd 11285	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → 1 ∈ ℂ)
168	166, 167	negsubdi2d 11663	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → -(𝐿 − 1) = (1 − 𝐿))
169	157, 154, 160	divcld 12070	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → ((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘)) ∈ ℂ)
170	169	abscld 15485	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) ∈ ℝ)
171	39	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → 𝐿 ∈ ℝ)
172	170, 171	resubcld 11718	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿) ∈ ℝ)
173		1red 11291	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → 1 ∈ ℝ)
174	171, 173	resubcld 11718	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → (𝐿 − 1) ∈ ℝ)
175	172, 174	absltd 15478	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → ((abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1) ↔ (-(𝐿 − 1) < ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿) ∧ ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿) < (𝐿 − 1))))
176	175	simprbda 498	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → -(𝐿 − 1) < ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿))
177	168, 176	eqbrtrrd 5190	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (1 − 𝐿) < ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿))
178		1red 11291	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → 1 ∈ ℝ)
179	158, 155, 161	divcld 12070	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → ((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘)) ∈ ℂ)
180	179	abscld 15485	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) ∈ ℝ)
181	178, 180, 165	ltsub1d 11899	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (1 < (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) ↔ (1 − 𝐿) < ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)))
182	177, 181	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → 1 < (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))))
183	158, 155, 161	absdivd 15504	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) = ((abs‘(𝐹‘(𝑘 + 1))) / (abs‘(𝐹‘𝑘))))
184	182, 183	breqtrd 5192	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → 1 < ((abs‘(𝐹‘(𝑘 + 1))) / (abs‘(𝐹‘𝑘))))
185	178, 159, 162	ltmuldivd 13146	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → ((1 · (abs‘(𝐹‘𝑘))) < (abs‘(𝐹‘(𝑘 + 1))) ↔ 1 < ((abs‘(𝐹‘(𝑘 + 1))) / (abs‘(𝐹‘𝑘)))))
186	184, 185	mpbird 257	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (1 · (abs‘(𝐹‘𝑘))) < (abs‘(𝐹‘(𝑘 + 1))))
187	164, 186	eqbrtrrd 5190	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (abs‘(𝐹‘𝑘)) < (abs‘(𝐹‘(𝑘 + 1))))
188	156, 159, 187	ltled 11438	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1))))
189	188	ex 412	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → ((abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1) → (abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))))
190	189	ralimdva 3173	. . . . . . . . 9 ⊢ (((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) → (∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1) → ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))))
191	190	reximdva 3174	. . . . . . . 8 ⊢ ((𝜑 ∧ 1 < 𝐿) → (∃𝑛 ∈ 𝑊 ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1) → ∃𝑛 ∈ 𝑊 ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))))
192	153, 191	mpd 15	. . . . . . 7 ⊢ ((𝜑 ∧ 1 < 𝐿) → ∃𝑛 ∈ 𝑊 ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1))))
193	145, 192	r19.29a 3168	. . . . . 6 ⊢ ((𝜑 ∧ 1 < 𝐿) → seq𝑁( + , 𝐹) ∉ dom ⇝ )
194		df-nel 3053	. . . . . 6 ⊢ (seq𝑁( + , 𝐹) ∉ dom ⇝ ↔ ¬ seq𝑁( + , 𝐹) ∈ dom ⇝ )
195	193, 194	sylib 218	. . . . 5 ⊢ ((𝜑 ∧ 1 < 𝐿) → ¬ seq𝑁( + , 𝐹) ∈ dom ⇝ )
196	120	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 1 < 𝐿) → (seq𝑀( + , 𝐹) ∈ dom ⇝ ↔ seq𝑁( + , 𝐹) ∈ dom ⇝ ))
197	195, 196	mtbird 325	. . . 4 ⊢ ((𝜑 ∧ 1 < 𝐿) → ¬ seq𝑀( + , 𝐹) ∈ dom ⇝ )
198	128, 197	syldan 590	. . 3 ⊢ ((𝜑 ∧ ¬ 𝐿 < 1) → ¬ seq𝑀( + , 𝐹) ∈ dom ⇝ )
199	198	ex 412	. 2 ⊢ (𝜑 → (¬ 𝐿 < 1 → ¬ seq𝑀( + , 𝐹) ∈ dom ⇝ ))
200	123, 199	impcon4bid 227	1 ⊢ (𝜑 → (𝐿 < 1 ↔ seq𝑀( + , 𝐹) ∈ dom ⇝ ))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 846 ∧ w3a 1087 = wceq 1537 ∈ wcel 2108 ≠ wne 2946 ∉ wnel 3052 ∀wral 3067 ∃wrex 3076 ∅c0 4352 class class class wbr 5166 ↦ cmpt 5249 dom cdm 5700 ‘cfv 6573 (class class class)co 7448 ℂcc 11182 ℝcr 11183 0cc0 11184 1c1 11185 + caddc 11187 · cmul 11189 ℝ^*cxr 11323 < clt 11324 ≤ cle 11325 − cmin 11520 -cneg 11521 / cdiv 11947 ℤcz 12639 ℤ_≥cuz 12903 ℝ⁺crp 13057 (,)cioo 13407 seqcseq 14052 abscabs 15283 ⇝ cli 15530

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2158 ax-12 2178 ax-ext 2711 ax-rep 5303 ax-sep 5317 ax-nul 5324 ax-pow 5383 ax-pr 5447 ax-un 7770 ax-inf2 9710 ax-cnex 11240 ax-resscn 11241 ax-1cn 11242 ax-icn 11243 ax-addcl 11244 ax-addrcl 11245 ax-mulcl 11246 ax-mulrcl 11247 ax-mulcom 11248 ax-addass 11249 ax-mulass 11250 ax-distr 11251 ax-i2m1 11252 ax-1ne0 11253 ax-1rid 11254 ax-rnegex 11255 ax-rrecex 11256 ax-cnre 11257 ax-pre-lttri 11258 ax-pre-lttrn 11259 ax-pre-ltadd 11260 ax-pre-mulgt0 11261 ax-pre-sup 11262

This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3or 1088 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2543 df-eu 2572 df-clab 2718 df-cleq 2732 df-clel 2819 df-nfc 2895 df-ne 2947 df-nel 3053 df-ral 3068 df-rex 3077 df-rmo 3388 df-reu 3389 df-rab 3444 df-v 3490 df-sbc 3805 df-csb 3922 df-dif 3979 df-un 3981 df-in 3983 df-ss 3993 df-pss 3996 df-nul 4353 df-if 4549 df-pw 4624 df-sn 4649 df-pr 4651 df-op 4655 df-uni 4932 df-int 4971 df-iun 5017 df-br 5167 df-opab 5229 df-mpt 5250 df-tr 5284 df-id 5593 df-eprel 5599 df-po 5607 df-so 5608 df-fr 5652 df-se 5653 df-we 5654 df-xp 5706 df-rel 5707 df-cnv 5708 df-co 5709 df-dm 5710 df-rn 5711 df-res 5712 df-ima 5713 df-pred 6332 df-ord 6398 df-on 6399 df-lim 6400 df-suc 6401 df-iota 6525 df-fun 6575 df-fn 6576 df-f 6577 df-f1 6578 df-fo 6579 df-f1o 6580 df-fv 6581 df-isom 6582 df-riota 7404 df-ov 7451 df-oprab 7452 df-mpo 7453 df-om 7904 df-1st 8030 df-2nd 8031 df-frecs 8322 df-wrecs 8353 df-recs 8427 df-rdg 8466 df-1o 8522 df-er 8763 df-pm 8887 df-en 9004 df-dom 9005 df-sdom 9006 df-fin 9007 df-sup 9511 df-inf 9512 df-oi 9579 df-card 10008 df-pnf 11326 df-mnf 11327 df-xr 11328 df-ltxr 11329 df-le 11330 df-sub 11522 df-neg 11523 df-div 11948 df-nn 12294 df-2 12356 df-3 12357 df-n0 12554 df-z 12640 df-uz 12904 df-q 13014 df-rp 13058 df-ioo 13411 df-ico 13413 df-fz 13568 df-fzo 13712 df-fl 13843 df-seq 14053 df-exp 14113 df-hash 14380 df-shft 15116 df-cj 15148 df-re 15149 df-im 15150 df-sqrt 15284 df-abs 15285 df-limsup 15517 df-clim 15534 df-rlim 15535 df-sum 15735

This theorem is referenced by: radcnvrat 44283

W3C validator