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 41931

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 15595 and dvgrat 41930 directly uses the limit of the ratio.

(It also demonstrates how to use climi2 15220 and absltd 15141 to transform a limit to an inequality cf. https://math.stackexchange.com/q/2215191 15141, and how to use r19.29a 3218 in a similar fashion to Mario Carneiro's proof sketch with rexlimdva 3213 at https://groups.google.com/g/metamath/c/2RPikOiXLMo 3213.) (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 2738	. . . . . . . . 9 ⊢ (ℤ_≥‘𝑛) = (ℤ_≥‘𝑛)
3		elioore 13109	. . . . . . . . . 10 ⊢ (𝑟 ∈ (𝐿(,)1) → 𝑟 ∈ ℝ)
4	3	ad3antlr 728	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑘)))) → 𝑟 ∈ ℝ)
5		cvgdvgrat.n	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑁 ∈ 𝑍)
6		cvgdvgrat.z	. . . . . . . . . . . . . . . . 17 ⊢ 𝑍 = (ℤ_≥‘𝑀)
7	5, 6	eleqtrdi 2849	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘𝑀))
8		eluzelz 12592	. . . . . . . . . . . . . . . 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 12642	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ 𝑊 → (𝑘 + 1) ∈ 𝑊)
14		ovex 7308	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 + 1) ∈ V
15		eleq1 2826	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 = (𝑘 + 1) → (𝑖 ∈ 𝑊 ↔ (𝑘 + 1) ∈ 𝑊))
16	15	anbi2d 629	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = (𝑘 + 1) → ((𝜑 ∧ 𝑖 ∈ 𝑊) ↔ (𝜑 ∧ (𝑘 + 1) ∈ 𝑊)))
17		fveq2 6774	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 = (𝑘 + 1) → (𝐹‘𝑖) = (𝐹‘(𝑘 + 1)))
18	17	eleq1d 2823	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = (𝑘 + 1) → ((𝐹‘𝑖) ∈ ℂ ↔ (𝐹‘(𝑘 + 1)) ∈ ℂ))
19	16, 18	imbi12d 345	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = (𝑘 + 1) → (((𝜑 ∧ 𝑖 ∈ 𝑊) → (𝐹‘𝑖) ∈ ℂ) ↔ ((𝜑 ∧ (𝑘 + 1) ∈ 𝑊) → (𝐹‘(𝑘 + 1)) ∈ ℂ)))
20		eleq1 2826	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = 𝑖 → (𝑘 ∈ 𝑊 ↔ 𝑖 ∈ 𝑊))
21	20	anbi2d 629	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = 𝑖 → ((𝜑 ∧ 𝑘 ∈ 𝑊) ↔ (𝜑 ∧ 𝑖 ∈ 𝑊)))
22		fveq2 6774	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = 𝑖 → (𝐹‘𝑘) = (𝐹‘𝑖))
23	22	eleq1d 2823	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = 𝑖 → ((𝐹‘𝑘) ∈ ℂ ↔ (𝐹‘𝑖) ∈ ℂ))
24	21, 23	imbi12d 345	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = 𝑖 → (((𝜑 ∧ 𝑘 ∈ 𝑊) → (𝐹‘𝑘) ∈ ℂ) ↔ ((𝜑 ∧ 𝑖 ∈ 𝑊) → (𝐹‘𝑖) ∈ ℂ)))
25	1	eleq2i 2830	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 ∈ 𝑊 ↔ 𝑘 ∈ (ℤ_≥‘𝑁))
26	6	uztrn2 12601	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑁 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) → 𝑘 ∈ 𝑍)
27	5, 26	sylan 580	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) → 𝑘 ∈ 𝑍)
28	25, 27	sylan2b 594	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → 𝑘 ∈ 𝑍)
29		cvgdvgrat.c	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)
30	28, 29	syldan 591	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → (𝐹‘𝑘) ∈ ℂ)
31	24, 30	chvarvv 2002	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑊) → (𝐹‘𝑖) ∈ ℂ)
32	14, 19, 31	vtocl 3498	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ 𝑊) → (𝐹‘(𝑘 + 1)) ∈ ℂ)
33	13, 32	sylan2 593	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → (𝐹‘(𝑘 + 1)) ∈ ℂ)
34		cvgdvgrat.n0	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → (𝐹‘𝑘) ≠ 0)
35	33, 30, 34	divcld 11751	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → ((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘)) ∈ ℂ)
36	35	abscld 15148	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) ∈ ℝ)
37	12, 36	fvmpt2d 6888	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → (𝑅‘𝑘) = (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))))
38	37, 36	eqeltrd 2839	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → (𝑅‘𝑘) ∈ ℝ)
39	1, 9, 10, 38	climrecl 15292	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐿 ∈ ℝ)
40	39	rexrd 11025	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐿 ∈ ℝ^*)
41		1xr 11034	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℝ^*
42		elioo2 13120	. . . . . . . . . . . . 13 ⊢ ((𝐿 ∈ ℝ^* ∧ 1 ∈ ℝ^*) → (𝑟 ∈ (𝐿(,)1) ↔ (𝑟 ∈ ℝ ∧ 𝐿 < 𝑟 ∧ 𝑟 < 1)))
43	40, 41, 42	sylancl 586	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑟 ∈ (𝐿(,)1) ↔ (𝑟 ∈ ℝ ∧ 𝐿 < 𝑟 ∧ 𝑟 < 1)))
44	43	biimpa 477	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) → (𝑟 ∈ ℝ ∧ 𝐿 < 𝑟 ∧ 𝑟 < 1))
45	44	simp3d 1143	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) → 𝑟 < 1)
46	45	ad2antrr 723	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑘)))) → 𝑟 < 1)
47		simplr 766	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑘)))) → 𝑛 ∈ 𝑊)
48	31	ex 413	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑖 ∈ 𝑊 → (𝐹‘𝑖) ∈ ℂ))
49	48	ad3antrrr 727	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑘)))) → (𝑖 ∈ 𝑊 → (𝐹‘𝑖) ∈ ℂ))
50	49	imp 407	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑘)))) ∧ 𝑖 ∈ 𝑊) → (𝐹‘𝑖) ∈ ℂ)
51		fvoveq1 7298	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑖 → (𝐹‘(𝑘 + 1)) = (𝐹‘(𝑖 + 1)))
52	51	fveq2d 6778	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑖 → (abs‘(𝐹‘(𝑘 + 1))) = (abs‘(𝐹‘(𝑖 + 1))))
53	22	fveq2d 6778	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑖 → (abs‘(𝐹‘𝑘)) = (abs‘(𝐹‘𝑖)))
54	53	oveq2d 7291	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑖 → (𝑟 · (abs‘(𝐹‘𝑘))) = (𝑟 · (abs‘(𝐹‘𝑖))))
55	52, 54	breq12d 5087	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑖 → ((abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑘))) ↔ (abs‘(𝐹‘(𝑖 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑖)))))
56	55	rspccva 3560	. . . . . . . . . 10 ⊢ ((∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑘))) ∧ 𝑖 ∈ (ℤ_≥‘𝑛)) → (abs‘(𝐹‘(𝑖 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑖))))
57	56	adantll 711	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑘)))) ∧ 𝑖 ∈ (ℤ_≥‘𝑛)) → (abs‘(𝐹‘(𝑖 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑖))))
58	1, 2, 4, 46, 47, 50, 57	cvgrat 15595	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑘)))) → seq𝑁( + , 𝐹) ∈ dom ⇝ )
59	9	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) → 𝑁 ∈ ℤ)
60	44	simp2d 1142	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) → 𝐿 < 𝑟)
61		difrp 12768	. . . . . . . . . . . 12 ⊢ ((𝐿 ∈ ℝ ∧ 𝑟 ∈ ℝ) → (𝐿 < 𝑟 ↔ (𝑟 − 𝐿) ∈ ℝ⁺))
62	39, 3, 61	syl2an 596	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) → (𝐿 < 𝑟 ↔ (𝑟 − 𝐿) ∈ ℝ⁺))
63	60, 62	mpbid 231	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) → (𝑟 − 𝐿) ∈ ℝ⁺)
64	37	adantlr 712	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑘 ∈ 𝑊) → (𝑅‘𝑘) = (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))))
65	10	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) → 𝑅 ⇝ 𝐿)
66	1, 59, 63, 64, 65	climi2 15220	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) → ∃𝑛 ∈ 𝑊 ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿))
67	1	uztrn2 12601	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ 𝑊 ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → 𝑘 ∈ 𝑊)
68	67, 33	sylan2 593	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑛 ∈ 𝑊 ∧ 𝑘 ∈ (ℤ_≥‘𝑛))) → (𝐹‘(𝑘 + 1)) ∈ ℂ)
69	68	anassrs 468	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → (𝐹‘(𝑘 + 1)) ∈ ℂ)
70	69	adantllr 716	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → (𝐹‘(𝑘 + 1)) ∈ ℂ)
71	70	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (𝐹‘(𝑘 + 1)) ∈ ℂ)
72	71	abscld 15148	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (abs‘(𝐹‘(𝑘 + 1))) ∈ ℝ)
73	3	ad4antlr 730	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → 𝑟 ∈ ℝ)
74	67, 30	sylan2 593	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑛 ∈ 𝑊 ∧ 𝑘 ∈ (ℤ_≥‘𝑛))) → (𝐹‘𝑘) ∈ ℂ)
75	74	anassrs 468	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → (𝐹‘𝑘) ∈ ℂ)
76	75	adantllr 716	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → (𝐹‘𝑘) ∈ ℂ)
77	76	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (𝐹‘𝑘) ∈ ℂ)
78	77	abscld 15148	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (abs‘(𝐹‘𝑘)) ∈ ℝ)
79	73, 78	remulcld 11005	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (𝑟 · (abs‘(𝐹‘𝑘))) ∈ ℝ)
80	67, 34	sylan2 593	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑛 ∈ 𝑊 ∧ 𝑘 ∈ (ℤ_≥‘𝑛))) → (𝐹‘𝑘) ≠ 0)
81	80	anassrs 468	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → (𝐹‘𝑘) ≠ 0)
82	81	adantllr 716	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → (𝐹‘𝑘) ≠ 0)
83	82	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (𝐹‘𝑘) ≠ 0)
84	71, 77, 83	absdivd 15167	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) = ((abs‘(𝐹‘(𝑘 + 1))) / (abs‘(𝐹‘𝑘))))
85	70, 76, 82	divcld 11751	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → ((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘)) ∈ ℂ)
86	85	abscld 15148	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) ∈ ℝ)
87	39	ad3antrrr 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → 𝐿 ∈ ℝ)
88	86, 87	resubcld 11403	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿) ∈ ℝ)
89	3	ad3antlr 728	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → 𝑟 ∈ ℝ)
90	89, 87	resubcld 11403	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → (𝑟 − 𝐿) ∈ ℝ)
91	88, 90	absltd 15141	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → ((abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿) ↔ (-(𝑟 − 𝐿) < ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿) ∧ ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿) < (𝑟 − 𝐿))))
92	91	simplbda 500	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿) < (𝑟 − 𝐿))
93	71, 77, 83	divcld 11751	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → ((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘)) ∈ ℂ)
94	93	abscld 15148	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) ∈ ℝ)
95	39	ad4antr 729	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → 𝐿 ∈ ℝ)
96	94, 73, 95	ltsub1d 11584	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) < 𝑟 ↔ ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿) < (𝑟 − 𝐿)))
97	92, 96	mpbird 256	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) < 𝑟)
98	84, 97	eqbrtrrd 5098	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → ((abs‘(𝐹‘(𝑘 + 1))) / (abs‘(𝐹‘𝑘))) < 𝑟)
99	77, 83	absrpcld 15160	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (abs‘(𝐹‘𝑘)) ∈ ℝ⁺)
100	72, 73, 99	ltdivmuld 12823	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (((abs‘(𝐹‘(𝑘 + 1))) / (abs‘(𝐹‘𝑘))) < 𝑟 ↔ (abs‘(𝐹‘(𝑘 + 1))) < ((abs‘(𝐹‘𝑘)) · 𝑟)))
101	98, 100	mpbid 231	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (abs‘(𝐹‘(𝑘 + 1))) < ((abs‘(𝐹‘𝑘)) · 𝑟))
102	99	rpcnd 12774	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (abs‘(𝐹‘𝑘)) ∈ ℂ)
103	73	recnd 11003	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → 𝑟 ∈ ℂ)
104	102, 103	mulcomd 10996	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → ((abs‘(𝐹‘𝑘)) · 𝑟) = (𝑟 · (abs‘(𝐹‘𝑘))))
105	101, 104	breqtrd 5100	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (abs‘(𝐹‘(𝑘 + 1))) < (𝑟 · (abs‘(𝐹‘𝑘))))
106	72, 79, 105	ltled 11123	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑘))))
107	106	ex 413	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → ((abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿) → (abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑘)))))
108	107	ralimdva 3108	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) → (∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿) → ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑘)))))
109	108	reximdva 3203	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) → (∃𝑛 ∈ 𝑊 ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿) → ∃𝑛 ∈ 𝑊 ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑘)))))
110	66, 109	mpd 15	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) → ∃𝑛 ∈ 𝑊 ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑘))))
111	58, 110	r19.29a 3218	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) → seq𝑁( + , 𝐹) ∈ dom ⇝ )
112	111	ralrimiva 3103	. . . . . 6 ⊢ (𝜑 → ∀𝑟 ∈ (𝐿(,)1)seq𝑁( + , 𝐹) ∈ dom ⇝ )
113	112	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝐿 < 1) → ∀𝑟 ∈ (𝐿(,)1)seq𝑁( + , 𝐹) ∈ dom ⇝ )
114		ioon0 13105	. . . . . . . 8 ⊢ ((𝐿 ∈ ℝ^* ∧ 1 ∈ ℝ^*) → ((𝐿(,)1) ≠ ∅ ↔ 𝐿 < 1))
115	40, 41, 114	sylancl 586	. . . . . . 7 ⊢ (𝜑 → ((𝐿(,)1) ≠ ∅ ↔ 𝐿 < 1))
116	115	biimpar 478	. . . . . 6 ⊢ ((𝜑 ∧ 𝐿 < 1) → (𝐿(,)1) ≠ ∅)
117		r19.3rzv 4429	. . . . . 6 ⊢ ((𝐿(,)1) ≠ ∅ → (seq𝑁( + , 𝐹) ∈ dom ⇝ ↔ ∀𝑟 ∈ (𝐿(,)1)seq𝑁( + , 𝐹) ∈ dom ⇝ ))
118	116, 117	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝐿 < 1) → (seq𝑁( + , 𝐹) ∈ dom ⇝ ↔ ∀𝑟 ∈ (𝐿(,)1)seq𝑁( + , 𝐹) ∈ dom ⇝ ))
119	113, 118	mpbird 256	. . . 4 ⊢ ((𝜑 ∧ 𝐿 < 1) → seq𝑁( + , 𝐹) ∈ dom ⇝ )
120	6, 5, 29	iserex 15368	. . . . 5 ⊢ (𝜑 → (seq𝑀( + , 𝐹) ∈ dom ⇝ ↔ seq𝑁( + , 𝐹) ∈ dom ⇝ ))
121	120	adantr 481	. . . 4 ⊢ ((𝜑 ∧ 𝐿 < 1) → (seq𝑀( + , 𝐹) ∈ dom ⇝ ↔ seq𝑁( + , 𝐹) ∈ dom ⇝ ))
122	119, 121	mpbird 256	. . 3 ⊢ ((𝜑 ∧ 𝐿 < 1) → seq𝑀( + , 𝐹) ∈ dom ⇝ )
123	122	ex 413	. 2 ⊢ (𝜑 → (𝐿 < 1 → seq𝑀( + , 𝐹) ∈ dom ⇝ ))
124		cvgdvgrat.n1	. . . . . 6 ⊢ (𝜑 → 𝐿 ≠ 1)
125		1red 10976	. . . . . . 7 ⊢ (𝜑 → 1 ∈ ℝ)
126	39, 125	lttri2d 11114	. . . . . 6 ⊢ (𝜑 → (𝐿 ≠ 1 ↔ (𝐿 < 1 ∨ 1 < 𝐿)))
127	124, 126	mpbid 231	. . . . 5 ⊢ (𝜑 → (𝐿 < 1 ∨ 1 < 𝐿))
128	127	orcanai 1000	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝐿 < 1) → 1 < 𝐿)
129		simplr 766	. . . . . . . 8 ⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))) → 𝑛 ∈ 𝑊)
130		cvgdvgrat.f	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 ∈ 𝑉)
131	130	ad3antrrr 727	. . . . . . . 8 ⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))) → 𝐹 ∈ 𝑉)
132	48	ad3antrrr 727	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))) → (𝑖 ∈ 𝑊 → (𝐹‘𝑖) ∈ ℂ))
133	132	imp 407	. . . . . . . 8 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))) ∧ 𝑖 ∈ 𝑊) → (𝐹‘𝑖) ∈ ℂ)
134	1	uztrn2 12601	. . . . . . . . . . . 12 ⊢ ((𝑛 ∈ 𝑊 ∧ 𝑖 ∈ (ℤ_≥‘𝑛)) → 𝑖 ∈ 𝑊)
135	22	neeq1d 3003	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑖 → ((𝐹‘𝑘) ≠ 0 ↔ (𝐹‘𝑖) ≠ 0))
136	21, 135	imbi12d 345	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑖 → (((𝜑 ∧ 𝑘 ∈ 𝑊) → (𝐹‘𝑘) ≠ 0) ↔ ((𝜑 ∧ 𝑖 ∈ 𝑊) → (𝐹‘𝑖) ≠ 0)))
137	136, 34	chvarvv 2002	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑊) → (𝐹‘𝑖) ≠ 0)
138	134, 137	sylan2 593	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑛 ∈ 𝑊 ∧ 𝑖 ∈ (ℤ_≥‘𝑛))) → (𝐹‘𝑖) ≠ 0)
139	138	anassrs 468	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑊) ∧ 𝑖 ∈ (ℤ_≥‘𝑛)) → (𝐹‘𝑖) ≠ 0)
140	139	adantllr 716	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑖 ∈ (ℤ_≥‘𝑛)) → (𝐹‘𝑖) ≠ 0)
141	140	adantlr 712	. . . . . . . 8 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))) ∧ 𝑖 ∈ (ℤ_≥‘𝑛)) → (𝐹‘𝑖) ≠ 0)
142	53, 52	breq12d 5087	. . . . . . . . . 10 ⊢ (𝑘 = 𝑖 → ((abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1))) ↔ (abs‘(𝐹‘𝑖)) ≤ (abs‘(𝐹‘(𝑖 + 1)))))
143	142	rspccva 3560	. . . . . . . . 9 ⊢ ((∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1))) ∧ 𝑖 ∈ (ℤ_≥‘𝑛)) → (abs‘(𝐹‘𝑖)) ≤ (abs‘(𝐹‘(𝑖 + 1))))
144	143	adantll 711	. . . . . . . 8 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))) ∧ 𝑖 ∈ (ℤ_≥‘𝑛)) → (abs‘(𝐹‘𝑖)) ≤ (abs‘(𝐹‘(𝑖 + 1))))
145	1, 2, 129, 131, 133, 141, 144	dvgrat 41930	. . . . . . 7 ⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))) → seq𝑁( + , 𝐹) ∉ dom ⇝ )
146	9	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 1 < 𝐿) → 𝑁 ∈ ℤ)
147		1re 10975	. . . . . . . . . . 11 ⊢ 1 ∈ ℝ
148		difrp 12768	. . . . . . . . . . 11 ⊢ ((1 ∈ ℝ ∧ 𝐿 ∈ ℝ) → (1 < 𝐿 ↔ (𝐿 − 1) ∈ ℝ⁺))
149	147, 39, 148	sylancr 587	. . . . . . . . . 10 ⊢ (𝜑 → (1 < 𝐿 ↔ (𝐿 − 1) ∈ ℝ⁺))
150	149	biimpa 477	. . . . . . . . 9 ⊢ ((𝜑 ∧ 1 < 𝐿) → (𝐿 − 1) ∈ ℝ⁺)
151	37	adantlr 712	. . . . . . . . 9 ⊢ (((𝜑 ∧ 1 < 𝐿) ∧ 𝑘 ∈ 𝑊) → (𝑅‘𝑘) = (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))))
152	10	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 1 < 𝐿) → 𝑅 ⇝ 𝐿)
153	1, 146, 150, 151, 152	climi2 15220	. . . . . . . 8 ⊢ ((𝜑 ∧ 1 < 𝐿) → ∃𝑛 ∈ 𝑊 ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1))
154	75	adantllr 716	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → (𝐹‘𝑘) ∈ ℂ)
155	154	adantr 481	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (𝐹‘𝑘) ∈ ℂ)
156	155	abscld 15148	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (abs‘(𝐹‘𝑘)) ∈ ℝ)
157	69	adantllr 716	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → (𝐹‘(𝑘 + 1)) ∈ ℂ)
158	157	adantr 481	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (𝐹‘(𝑘 + 1)) ∈ ℂ)
159	158	abscld 15148	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (abs‘(𝐹‘(𝑘 + 1))) ∈ ℝ)
160	81	adantllr 716	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → (𝐹‘𝑘) ≠ 0)
161	160	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (𝐹‘𝑘) ≠ 0)
162	155, 161	absrpcld 15160	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (abs‘(𝐹‘𝑘)) ∈ ℝ⁺)
163	162	rpcnd 12774	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (abs‘(𝐹‘𝑘)) ∈ ℂ)
164	163	mulid2d 10993	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (1 · (abs‘(𝐹‘𝑘))) = (abs‘(𝐹‘𝑘)))
165	39	ad4antr 729	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → 𝐿 ∈ ℝ)
166	165	recnd 11003	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → 𝐿 ∈ ℂ)
167		1cnd 10970	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → 1 ∈ ℂ)
168	166, 167	negsubdi2d 11348	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → -(𝐿 − 1) = (1 − 𝐿))
169	157, 154, 160	divcld 11751	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → ((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘)) ∈ ℂ)
170	169	abscld 15148	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) ∈ ℝ)
171	39	ad3antrrr 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → 𝐿 ∈ ℝ)
172	170, 171	resubcld 11403	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿) ∈ ℝ)
173		1red 10976	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → 1 ∈ ℝ)
174	171, 173	resubcld 11403	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → (𝐿 − 1) ∈ ℝ)
175	172, 174	absltd 15141	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → ((abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1) ↔ (-(𝐿 − 1) < ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿) ∧ ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿) < (𝐿 − 1))))
176	175	simprbda 499	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → -(𝐿 − 1) < ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿))
177	168, 176	eqbrtrrd 5098	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (1 − 𝐿) < ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿))
178		1red 10976	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → 1 ∈ ℝ)
179	158, 155, 161	divcld 11751	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → ((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘)) ∈ ℂ)
180	179	abscld 15148	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) ∈ ℝ)
181	178, 180, 165	ltsub1d 11584	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (1 < (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) ↔ (1 − 𝐿) < ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)))
182	177, 181	mpbird 256	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → 1 < (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))))
183	158, 155, 161	absdivd 15167	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) = ((abs‘(𝐹‘(𝑘 + 1))) / (abs‘(𝐹‘𝑘))))
184	182, 183	breqtrd 5100	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → 1 < ((abs‘(𝐹‘(𝑘 + 1))) / (abs‘(𝐹‘𝑘))))
185	178, 159, 162	ltmuldivd 12819	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → ((1 · (abs‘(𝐹‘𝑘))) < (abs‘(𝐹‘(𝑘 + 1))) ↔ 1 < ((abs‘(𝐹‘(𝑘 + 1))) / (abs‘(𝐹‘𝑘)))))
186	184, 185	mpbird 256	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (1 · (abs‘(𝐹‘𝑘))) < (abs‘(𝐹‘(𝑘 + 1))))
187	164, 186	eqbrtrrd 5098	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (abs‘(𝐹‘𝑘)) < (abs‘(𝐹‘(𝑘 + 1))))
188	156, 159, 187	ltled 11123	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1))))
189	188	ex 413	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → ((abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1) → (abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))))
190	189	ralimdva 3108	. . . . . . . . 9 ⊢ (((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) → (∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1) → ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))))
191	190	reximdva 3203	. . . . . . . 8 ⊢ ((𝜑 ∧ 1 < 𝐿) → (∃𝑛 ∈ 𝑊 ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1) → ∃𝑛 ∈ 𝑊 ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))))
192	153, 191	mpd 15	. . . . . . 7 ⊢ ((𝜑 ∧ 1 < 𝐿) → ∃𝑛 ∈ 𝑊 ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1))))
193	145, 192	r19.29a 3218	. . . . . 6 ⊢ ((𝜑 ∧ 1 < 𝐿) → seq𝑁( + , 𝐹) ∉ dom ⇝ )
194		df-nel 3050	. . . . . 6 ⊢ (seq𝑁( + , 𝐹) ∉ dom ⇝ ↔ ¬ seq𝑁( + , 𝐹) ∈ dom ⇝ )
195	193, 194	sylib 217	. . . . 5 ⊢ ((𝜑 ∧ 1 < 𝐿) → ¬ seq𝑁( + , 𝐹) ∈ dom ⇝ )
196	120	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 1 < 𝐿) → (seq𝑀( + , 𝐹) ∈ dom ⇝ ↔ seq𝑁( + , 𝐹) ∈ dom ⇝ ))
197	195, 196	mtbird 325	. . . 4 ⊢ ((𝜑 ∧ 1 < 𝐿) → ¬ seq𝑀( + , 𝐹) ∈ dom ⇝ )
198	128, 197	syldan 591	. . 3 ⊢ ((𝜑 ∧ ¬ 𝐿 < 1) → ¬ seq𝑀( + , 𝐹) ∈ dom ⇝ )
199	198	ex 413	. 2 ⊢ (𝜑 → (¬ 𝐿 < 1 → ¬ seq𝑀( + , 𝐹) ∈ dom ⇝ ))
200	123, 199	impcon4bid 226	1 ⊢ (𝜑 → (𝐿 < 1 ↔ seq𝑀( + , 𝐹) ∈ dom ⇝ ))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∨ wo 844 ∧ w3a 1086 = wceq 1539 ∈ wcel 2106 ≠ wne 2943 ∉ wnel 3049 ∀wral 3064 ∃wrex 3065 ∅c0 4256 class class class wbr 5074 ↦ cmpt 5157 dom cdm 5589 ‘cfv 6433 (class class class)co 7275 ℂcc 10869 ℝcr 10870 0cc0 10871 1c1 10872 + caddc 10874 · cmul 10876 ℝ^*cxr 11008 < clt 11009 ≤ cle 11010 − cmin 11205 -cneg 11206 / cdiv 11632 ℤcz 12319 ℤ_≥cuz 12582 ℝ⁺crp 12730 (,)cioo 13079 seqcseq 13721 abscabs 14945 ⇝ cli 15193

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-rep 5209 ax-sep 5223 ax-nul 5230 ax-pow 5288 ax-pr 5352 ax-un 7588 ax-inf2 9399 ax-cnex 10927 ax-resscn 10928 ax-1cn 10929 ax-icn 10930 ax-addcl 10931 ax-addrcl 10932 ax-mulcl 10933 ax-mulrcl 10934 ax-mulcom 10935 ax-addass 10936 ax-mulass 10937 ax-distr 10938 ax-i2m1 10939 ax-1ne0 10940 ax-1rid 10941 ax-rnegex 10942 ax-rrecex 10943 ax-cnre 10944 ax-pre-lttri 10945 ax-pre-lttrn 10946 ax-pre-ltadd 10947 ax-pre-mulgt0 10948 ax-pre-sup 10949

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-rmo 3071 df-reu 3072 df-rab 3073 df-v 3434 df-sbc 3717 df-csb 3833 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-pss 3906 df-nul 4257 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-int 4880 df-iun 4926 df-br 5075 df-opab 5137 df-mpt 5158 df-tr 5192 df-id 5489 df-eprel 5495 df-po 5503 df-so 5504 df-fr 5544 df-se 5545 df-we 5546 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-rn 5600 df-res 5601 df-ima 5602 df-pred 6202 df-ord 6269 df-on 6270 df-lim 6271 df-suc 6272 df-iota 6391 df-fun 6435 df-fn 6436 df-f 6437 df-f1 6438 df-fo 6439 df-f1o 6440 df-fv 6441 df-isom 6442 df-riota 7232 df-ov 7278 df-oprab 7279 df-mpo 7280 df-om 7713 df-1st 7831 df-2nd 7832 df-frecs 8097 df-wrecs 8128 df-recs 8202 df-rdg 8241 df-1o 8297 df-er 8498 df-pm 8618 df-en 8734 df-dom 8735 df-sdom 8736 df-fin 8737 df-sup 9201 df-inf 9202 df-oi 9269 df-card 9697 df-pnf 11011 df-mnf 11012 df-xr 11013 df-ltxr 11014 df-le 11015 df-sub 11207 df-neg 11208 df-div 11633 df-nn 11974 df-2 12036 df-3 12037 df-n0 12234 df-z 12320 df-uz 12583 df-q 12689 df-rp 12731 df-ioo 13083 df-ico 13085 df-fz 13240 df-fzo 13383 df-fl 13512 df-seq 13722 df-exp 13783 df-hash 14045 df-shft 14778 df-cj 14810 df-re 14811 df-im 14812 df-sqrt 14946 df-abs 14947 df-limsup 15180 df-clim 15197 df-rlim 15198 df-sum 15398

This theorem is referenced by: radcnvrat 41932

W3C validator