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 45083

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

(It also demonstrates how to use climi2 15588 and absltd 15509 to transform a limit to an inequality cf. https://math.stackexchange.com/q/2215191 15509, and how to use r19.29a 3175 in a similar fashion to Mario Carneiro's proof sketch with rexlimdva 3168 at https://groups.google.com/g/metamath/c/2RPikOiXLMo 3168.) (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 2765	. . . . . . . . 9 ⊢ (ℤ_≥‘𝑛) = (ℤ_≥‘𝑛)
3		elioore 13420	. . . . . . . . . 10 ⊢ (𝑟 ∈ (𝐿(,)1) → 𝑟 ∈ ℝ)
4	3	ad3antlr 744	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑘)))) → 𝑟 ∈ ℝ)
5		cvgdvgrat.n	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑁 ∈ 𝑍)
6		cvgdvgrat.z	. . . . . . . . . . . . . . . . 17 ⊢ 𝑍 = (ℤ_≥‘𝑀)
7	5, 6	eleqtrdi 2875	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘𝑀))
8		eluzelz 12890	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → 𝑁 ∈ ℤ)
9	7, 8	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑁 ∈ ℤ)
10		cvgdvgrat.cvg	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑅 ⇝ 𝐿)
11		cvgdvgrat.r	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑅 = (𝑘 ∈ 𝑊 ↦ (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))))
12	11	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑅 = (𝑘 ∈ 𝑊 ↦ (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘)))))
13	1	peano2uzs 12944	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ 𝑊 → (𝑘 + 1) ∈ 𝑊)
14		ovex 7452	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 + 1) ∈ V
15		eleq1 2853	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 = (𝑘 + 1) → (𝑖 ∈ 𝑊 ↔ (𝑘 + 1) ∈ 𝑊))
16	15	anbi2d 642	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = (𝑘 + 1) → ((𝜑 ∧ 𝑖 ∈ 𝑊) ↔ (𝜑 ∧ (𝑘 + 1) ∈ 𝑊)))
17		fveq2 6885	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 = (𝑘 + 1) → (𝐹‘𝑖) = (𝐹‘(𝑘 + 1)))
18	17	eleq1d 2850	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = (𝑘 + 1) → ((𝐹‘𝑖) ∈ ℂ ↔ (𝐹‘(𝑘 + 1)) ∈ ℂ))
19	16, 18	imbi12d 347	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = (𝑘 + 1) → (((𝜑 ∧ 𝑖 ∈ 𝑊) → (𝐹‘𝑖) ∈ ℂ) ↔ ((𝜑 ∧ (𝑘 + 1) ∈ 𝑊) → (𝐹‘(𝑘 + 1)) ∈ ℂ)))
20		eleq1 2853	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = 𝑖 → (𝑘 ∈ 𝑊 ↔ 𝑖 ∈ 𝑊))
21	20	anbi2d 642	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = 𝑖 → ((𝜑 ∧ 𝑘 ∈ 𝑊) ↔ (𝜑 ∧ 𝑖 ∈ 𝑊)))
22		fveq2 6885	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = 𝑖 → (𝐹‘𝑘) = (𝐹‘𝑖))
23	22	eleq1d 2850	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = 𝑖 → ((𝐹‘𝑘) ∈ ℂ ↔ (𝐹‘𝑖) ∈ ℂ))
24	21, 23	imbi12d 347	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = 𝑖 → (((𝜑 ∧ 𝑘 ∈ 𝑊) → (𝐹‘𝑘) ∈ ℂ) ↔ ((𝜑 ∧ 𝑖 ∈ 𝑊) → (𝐹‘𝑖) ∈ ℂ)))
25	1	eleq2i 2857	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 ∈ 𝑊 ↔ 𝑘 ∈ (ℤ_≥‘𝑁))
26	6	uztrn2 12899	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑁 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) → 𝑘 ∈ 𝑍)
27	5, 26	sylan 592	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) → 𝑘 ∈ 𝑍)
28	25, 27	sylan2b 606	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → 𝑘 ∈ 𝑍)
29		cvgdvgrat.c	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)
30	28, 29	syldan 603	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → (𝐹‘𝑘) ∈ ℂ)
31	24, 30	chvarvv 2022	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑊) → (𝐹‘𝑖) ∈ ℂ)
32	14, 19, 31	vtocl 3527	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ 𝑊) → (𝐹‘(𝑘 + 1)) ∈ ℂ)
33	13, 32	sylan2 605	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → (𝐹‘(𝑘 + 1)) ∈ ℂ)
34		cvgdvgrat.n0	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → (𝐹‘𝑘) ≠ 0)
35	33, 30, 34	divcld 12008	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → ((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘)) ∈ ℂ)
36	35	abscld 15516	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) ∈ ℝ)
37	12, 36	fvmpt2d 7007	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → (𝑅‘𝑘) = (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))))
38	37, 36	eqeltrd 2865	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → (𝑅‘𝑘) ∈ ℝ)
39	1, 9, 10, 38	climrecl 15660	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐿 ∈ ℝ)
40	39	rexrd 11276	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐿 ∈ ℝ^*)
41		1xr 11285	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℝ^*
42		elioo2 13431	. . . . . . . . . . . . 13 ⊢ ((𝐿 ∈ ℝ^* ∧ 1 ∈ ℝ^*) → (𝑟 ∈ (𝐿(,)1) ↔ (𝑟 ∈ ℝ ∧ 𝐿 < 𝑟 ∧ 𝑟 < 1)))
43	40, 41, 42	sylancl 598	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑟 ∈ (𝐿(,)1) ↔ (𝑟 ∈ ℝ ∧ 𝐿 < 𝑟 ∧ 𝑟 < 1)))
44	43	biimpa 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) → (𝑟 ∈ ℝ ∧ 𝐿 < 𝑟 ∧ 𝑟 < 1))
45	44	simp3d 1162	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) → 𝑟 < 1)
46	45	ad2antrr 739	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑘)))) → 𝑟 < 1)
47		simplr 781	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑘)))) → 𝑛 ∈ 𝑊)
48	31	ex 418	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑖 ∈ 𝑊 → (𝐹‘𝑖) ∈ ℂ))
49	48	ad3antrrr 743	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑘)))) → (𝑖 ∈ 𝑊 → (𝐹‘𝑖) ∈ ℂ))
50	49	imp 412	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑘)))) ∧ 𝑖 ∈ 𝑊) → (𝐹‘𝑖) ∈ ℂ)
51		fvoveq1 7442	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑖 → (𝐹‘(𝑘 + 1)) = (𝐹‘(𝑖 + 1)))
52	51	fveq2d 6889	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑖 → (abs‘(𝐹‘(𝑘 + 1))) = (abs‘(𝐹‘(𝑖 + 1))))
53	22	fveq2d 6889	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑖 → (abs‘(𝐹‘𝑘)) = (abs‘(𝐹‘𝑖)))
54	53	oveq2d 7435	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑖 → (𝑟 · (abs‘(𝐹‘𝑘))) = (𝑟 · (abs‘(𝐹‘𝑖))))
55	52, 54	breq12d 5124	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑖 → ((abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑘))) ↔ (abs‘(𝐹‘(𝑖 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑖)))))
56	55	rspccva 3582	. . . . . . . . . 10 ⊢ ((∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑘))) ∧ 𝑖 ∈ (ℤ_≥‘𝑛)) → (abs‘(𝐹‘(𝑖 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑖))))
57	56	adantll 727	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑘)))) ∧ 𝑖 ∈ (ℤ_≥‘𝑛)) → (abs‘(𝐹‘(𝑖 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑖))))
58	1, 2, 4, 46, 47, 50, 57	cvgrat 15962	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑘)))) → seq𝑁( + , 𝐹) ∈ dom ⇝ )
59	9	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) → 𝑁 ∈ ℤ)
60	44	simp2d 1161	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) → 𝐿 < 𝑟)
61		difrp 13074	. . . . . . . . . . . 12 ⊢ ((𝐿 ∈ ℝ ∧ 𝑟 ∈ ℝ) → (𝐿 < 𝑟 ↔ (𝑟 − 𝐿) ∈ ℝ⁺))
62	39, 3, 61	syl2an 608	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) → (𝐿 < 𝑟 ↔ (𝑟 − 𝐿) ∈ ℝ⁺))
63	60, 62	mpbid 235	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) → (𝑟 − 𝐿) ∈ ℝ⁺)
64	37	adantlr 728	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑘 ∈ 𝑊) → (𝑅‘𝑘) = (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))))
65	10	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) → 𝑅 ⇝ 𝐿)
66	1, 59, 63, 64, 65	climi2 15588	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) → ∃𝑛 ∈ 𝑊 ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿))
67	1	uztrn2 12899	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ 𝑊 ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → 𝑘 ∈ 𝑊)
68	67, 33	sylan2 605	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑛 ∈ 𝑊 ∧ 𝑘 ∈ (ℤ_≥‘𝑛))) → (𝐹‘(𝑘 + 1)) ∈ ℂ)
69	68	anassrs 473	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → (𝐹‘(𝑘 + 1)) ∈ ℂ)
70	69	adantllr 732	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → (𝐹‘(𝑘 + 1)) ∈ ℂ)
71	70	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (𝐹‘(𝑘 + 1)) ∈ ℂ)
72	71	abscld 15516	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (abs‘(𝐹‘(𝑘 + 1))) ∈ ℝ)
73	3	ad4antlr 746	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → 𝑟 ∈ ℝ)
74	67, 30	sylan2 605	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑛 ∈ 𝑊 ∧ 𝑘 ∈ (ℤ_≥‘𝑛))) → (𝐹‘𝑘) ∈ ℂ)
75	74	anassrs 473	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → (𝐹‘𝑘) ∈ ℂ)
76	75	adantllr 732	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → (𝐹‘𝑘) ∈ ℂ)
77	76	adantr 486	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (𝐹‘𝑘) ∈ ℂ)
78	77	abscld 15516	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (abs‘(𝐹‘𝑘)) ∈ ℝ)
79	73, 78	remulcld 11256	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (𝑟 · (abs‘(𝐹‘𝑘))) ∈ ℝ)
80	67, 34	sylan2 605	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑛 ∈ 𝑊 ∧ 𝑘 ∈ (ℤ_≥‘𝑛))) → (𝐹‘𝑘) ≠ 0)
81	80	anassrs 473	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → (𝐹‘𝑘) ≠ 0)
82	81	adantllr 732	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → (𝐹‘𝑘) ≠ 0)
83	82	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (𝐹‘𝑘) ≠ 0)
84	71, 77, 83	absdivd 15535	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) = ((abs‘(𝐹‘(𝑘 + 1))) / (abs‘(𝐹‘𝑘))))
85	70, 76, 82	divcld 12008	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → ((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘)) ∈ ℂ)
86	85	abscld 15516	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) ∈ ℝ)
87	39	ad3antrrr 743	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → 𝐿 ∈ ℝ)
88	86, 87	resubcld 11659	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿) ∈ ℝ)
89	3	ad3antlr 744	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → 𝑟 ∈ ℝ)
90	89, 87	resubcld 11659	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → (𝑟 − 𝐿) ∈ ℝ)
91	88, 90	absltd 15509	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → ((abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿) ↔ (-(𝑟 − 𝐿) < ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿) ∧ ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿) < (𝑟 − 𝐿))))
92	91	simplbda 505	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿) < (𝑟 − 𝐿))
93	71, 77, 83	divcld 12008	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → ((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘)) ∈ ℂ)
94	93	abscld 15516	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) ∈ ℝ)
95	39	ad4antr 745	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → 𝐿 ∈ ℝ)
96	94, 73, 95	ltsub1d 11840	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) < 𝑟 ↔ ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿) < (𝑟 − 𝐿)))
97	92, 96	mpbird 260	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) < 𝑟)
98	84, 97	eqbrtrrd 5137	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → ((abs‘(𝐹‘(𝑘 + 1))) / (abs‘(𝐹‘𝑘))) < 𝑟)
99	77, 83	absrpcld 15528	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (abs‘(𝐹‘𝑘)) ∈ ℝ⁺)
100	72, 73, 99	ltdivmuld 13129	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (((abs‘(𝐹‘(𝑘 + 1))) / (abs‘(𝐹‘𝑘))) < 𝑟 ↔ (abs‘(𝐹‘(𝑘 + 1))) < ((abs‘(𝐹‘𝑘)) · 𝑟)))
101	98, 100	mpbid 235	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (abs‘(𝐹‘(𝑘 + 1))) < ((abs‘(𝐹‘𝑘)) · 𝑟))
102	99	rpcnd 13080	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (abs‘(𝐹‘𝑘)) ∈ ℂ)
103	73	recnd 11254	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → 𝑟 ∈ ℂ)
104	102, 103	mulcomd 11247	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → ((abs‘(𝐹‘𝑘)) · 𝑟) = (𝑟 · (abs‘(𝐹‘𝑘))))
105	101, 104	breqtrd 5139	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (abs‘(𝐹‘(𝑘 + 1))) < (𝑟 · (abs‘(𝐹‘𝑘))))
106	72, 79, 105	ltled 11375	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑘))))
107	106	ex 418	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → ((abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿) → (abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑘)))))
108	107	ralimdva 3179	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) → (∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿) → ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑘)))))
109	108	reximdva 3180	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) → (∃𝑛 ∈ 𝑊 ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿) → ∃𝑛 ∈ 𝑊 ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑘)))))
110	66, 109	mpd 16	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) → ∃𝑛 ∈ 𝑊 ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑘))))
111	58, 110	r19.29a 3175	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) → seq𝑁( + , 𝐹) ∈ dom ⇝ )
112	111	ralrimiva 3159	. . . . . 6 ⊢ (𝜑 → ∀𝑟 ∈ (𝐿(,)1)seq𝑁( + , 𝐹) ∈ dom ⇝ )
113	112	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝐿 < 1) → ∀𝑟 ∈ (𝐿(,)1)seq𝑁( + , 𝐹) ∈ dom ⇝ )
114		ioon0 13416	. . . . . . . 8 ⊢ ((𝐿 ∈ ℝ^* ∧ 1 ∈ ℝ^*) → ((𝐿(,)1) ≠ ∅ ↔ 𝐿 < 1))
115	40, 41, 114	sylancl 598	. . . . . . 7 ⊢ (𝜑 → ((𝐿(,)1) ≠ ∅ ↔ 𝐿 < 1))
116	115	biimpar 483	. . . . . 6 ⊢ ((𝜑 ∧ 𝐿 < 1) → (𝐿(,)1) ≠ ∅)
117		r19.3rzv 4466	. . . . . 6 ⊢ ((𝐿(,)1) ≠ ∅ → (seq𝑁( + , 𝐹) ∈ dom ⇝ ↔ ∀𝑟 ∈ (𝐿(,)1)seq𝑁( + , 𝐹) ∈ dom ⇝ ))
118	116, 117	syl 18	. . . . 5 ⊢ ((𝜑 ∧ 𝐿 < 1) → (seq𝑁( + , 𝐹) ∈ dom ⇝ ↔ ∀𝑟 ∈ (𝐿(,)1)seq𝑁( + , 𝐹) ∈ dom ⇝ ))
119	113, 118	mpbird 260	. . . 4 ⊢ ((𝜑 ∧ 𝐿 < 1) → seq𝑁( + , 𝐹) ∈ dom ⇝ )
120	6, 5, 29	iserex 15734	. . . . 5 ⊢ (𝜑 → (seq𝑀( + , 𝐹) ∈ dom ⇝ ↔ seq𝑁( + , 𝐹) ∈ dom ⇝ ))
121	120	adantr 486	. . . 4 ⊢ ((𝜑 ∧ 𝐿 < 1) → (seq𝑀( + , 𝐹) ∈ dom ⇝ ↔ seq𝑁( + , 𝐹) ∈ dom ⇝ ))
122	119, 121	mpbird 260	. . 3 ⊢ ((𝜑 ∧ 𝐿 < 1) → seq𝑀( + , 𝐹) ∈ dom ⇝ )
123	122	ex 418	. 2 ⊢ (𝜑 → (𝐿 < 1 → seq𝑀( + , 𝐹) ∈ dom ⇝ ))
124		cvgdvgrat.n1	. . . . . 6 ⊢ (𝜑 → 𝐿 ≠ 1)
125		1red 11226	. . . . . . 7 ⊢ (𝜑 → 1 ∈ ℝ)
126	39, 125	lttri2d 11366	. . . . . 6 ⊢ (𝜑 → (𝐿 ≠ 1 ↔ (𝐿 < 1 ∨ 1 < 𝐿)))
127	124, 126	mpbid 235	. . . . 5 ⊢ (𝜑 → (𝐿 < 1 ∨ 1 < 𝐿))
128	127	orcanai 1018	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝐿 < 1) → 1 < 𝐿)
129		simplr 781	. . . . . . . 8 ⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))) → 𝑛 ∈ 𝑊)
130		cvgdvgrat.f	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 ∈ 𝑉)
131	130	ad3antrrr 743	. . . . . . . 8 ⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))) → 𝐹 ∈ 𝑉)
132	48	ad3antrrr 743	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))) → (𝑖 ∈ 𝑊 → (𝐹‘𝑖) ∈ ℂ))
133	132	imp 412	. . . . . . . 8 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))) ∧ 𝑖 ∈ 𝑊) → (𝐹‘𝑖) ∈ ℂ)
134	1	uztrn2 12899	. . . . . . . . . . . 12 ⊢ ((𝑛 ∈ 𝑊 ∧ 𝑖 ∈ (ℤ_≥‘𝑛)) → 𝑖 ∈ 𝑊)
135	22	neeq1d 3019	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑖 → ((𝐹‘𝑘) ≠ 0 ↔ (𝐹‘𝑖) ≠ 0))
136	21, 135	imbi12d 347	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑖 → (((𝜑 ∧ 𝑘 ∈ 𝑊) → (𝐹‘𝑘) ≠ 0) ↔ ((𝜑 ∧ 𝑖 ∈ 𝑊) → (𝐹‘𝑖) ≠ 0)))
137	136, 34	chvarvv 2022	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑊) → (𝐹‘𝑖) ≠ 0)
138	134, 137	sylan2 605	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑛 ∈ 𝑊 ∧ 𝑖 ∈ (ℤ_≥‘𝑛))) → (𝐹‘𝑖) ≠ 0)
139	138	anassrs 473	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑊) ∧ 𝑖 ∈ (ℤ_≥‘𝑛)) → (𝐹‘𝑖) ≠ 0)
140	139	adantllr 732	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑖 ∈ (ℤ_≥‘𝑛)) → (𝐹‘𝑖) ≠ 0)
141	140	adantlr 728	. . . . . . . 8 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))) ∧ 𝑖 ∈ (ℤ_≥‘𝑛)) → (𝐹‘𝑖) ≠ 0)
142	53, 52	breq12d 5124	. . . . . . . . . 10 ⊢ (𝑘 = 𝑖 → ((abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1))) ↔ (abs‘(𝐹‘𝑖)) ≤ (abs‘(𝐹‘(𝑖 + 1)))))
143	142	rspccva 3582	. . . . . . . . 9 ⊢ ((∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1))) ∧ 𝑖 ∈ (ℤ_≥‘𝑛)) → (abs‘(𝐹‘𝑖)) ≤ (abs‘(𝐹‘(𝑖 + 1))))
144	143	adantll 727	. . . . . . . 8 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))) ∧ 𝑖 ∈ (ℤ_≥‘𝑛)) → (abs‘(𝐹‘𝑖)) ≤ (abs‘(𝐹‘(𝑖 + 1))))
145	1, 2, 129, 131, 133, 141, 144	dvgrat 45082	. . . . . . 7 ⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))) → seq𝑁( + , 𝐹) ∉ dom ⇝ )
146	9	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 1 < 𝐿) → 𝑁 ∈ ℤ)
147		1re 11225	. . . . . . . . . . 11 ⊢ 1 ∈ ℝ
148		difrp 13074	. . . . . . . . . . 11 ⊢ ((1 ∈ ℝ ∧ 𝐿 ∈ ℝ) → (1 < 𝐿 ↔ (𝐿 − 1) ∈ ℝ⁺))
149	147, 39, 148	sylancr 599	. . . . . . . . . 10 ⊢ (𝜑 → (1 < 𝐿 ↔ (𝐿 − 1) ∈ ℝ⁺))
150	149	biimpa 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 1 < 𝐿) → (𝐿 − 1) ∈ ℝ⁺)
151	37	adantlr 728	. . . . . . . . 9 ⊢ (((𝜑 ∧ 1 < 𝐿) ∧ 𝑘 ∈ 𝑊) → (𝑅‘𝑘) = (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))))
152	10	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 1 < 𝐿) → 𝑅 ⇝ 𝐿)
153	1, 146, 150, 151, 152	climi2 15588	. . . . . . . 8 ⊢ ((𝜑 ∧ 1 < 𝐿) → ∃𝑛 ∈ 𝑊 ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1))
154	75	adantllr 732	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → (𝐹‘𝑘) ∈ ℂ)
155	154	adantr 486	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (𝐹‘𝑘) ∈ ℂ)
156	155	abscld 15516	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (abs‘(𝐹‘𝑘)) ∈ ℝ)
157	69	adantllr 732	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → (𝐹‘(𝑘 + 1)) ∈ ℂ)
158	157	adantr 486	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (𝐹‘(𝑘 + 1)) ∈ ℂ)
159	158	abscld 15516	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (abs‘(𝐹‘(𝑘 + 1))) ∈ ℝ)
160	81	adantllr 732	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → (𝐹‘𝑘) ≠ 0)
161	160	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (𝐹‘𝑘) ≠ 0)
162	155, 161	absrpcld 15528	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (abs‘(𝐹‘𝑘)) ∈ ℝ⁺)
163	162	rpcnd 13080	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (abs‘(𝐹‘𝑘)) ∈ ℂ)
164	163	mullidd 11244	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (1 · (abs‘(𝐹‘𝑘))) = (abs‘(𝐹‘𝑘)))
165	39	ad4antr 745	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → 𝐿 ∈ ℝ)
166	165	recnd 11254	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → 𝐿 ∈ ℂ)
167		1cnd 11219	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → 1 ∈ ℂ)
168	166, 167	negsubdi2d 11602	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → -(𝐿 − 1) = (1 − 𝐿))
169	157, 154, 160	divcld 12008	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → ((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘)) ∈ ℂ)
170	169	abscld 15516	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) ∈ ℝ)
171	39	ad3antrrr 743	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → 𝐿 ∈ ℝ)
172	170, 171	resubcld 11659	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿) ∈ ℝ)
173		1red 11226	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → 1 ∈ ℝ)
174	171, 173	resubcld 11659	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → (𝐿 − 1) ∈ ℝ)
175	172, 174	absltd 15509	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → ((abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1) ↔ (-(𝐿 − 1) < ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿) ∧ ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿) < (𝐿 − 1))))
176	175	simprbda 504	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → -(𝐿 − 1) < ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿))
177	168, 176	eqbrtrrd 5137	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (1 − 𝐿) < ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿))
178		1red 11226	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → 1 ∈ ℝ)
179	158, 155, 161	divcld 12008	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → ((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘)) ∈ ℂ)
180	179	abscld 15516	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) ∈ ℝ)
181	178, 180, 165	ltsub1d 11840	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (1 < (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) ↔ (1 − 𝐿) < ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)))
182	177, 181	mpbird 260	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → 1 < (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))))
183	158, 155, 161	absdivd 15535	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) = ((abs‘(𝐹‘(𝑘 + 1))) / (abs‘(𝐹‘𝑘))))
184	182, 183	breqtrd 5139	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → 1 < ((abs‘(𝐹‘(𝑘 + 1))) / (abs‘(𝐹‘𝑘))))
185	178, 159, 162	ltmuldivd 13125	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → ((1 · (abs‘(𝐹‘𝑘))) < (abs‘(𝐹‘(𝑘 + 1))) ↔ 1 < ((abs‘(𝐹‘(𝑘 + 1))) / (abs‘(𝐹‘𝑘)))))
186	184, 185	mpbird 260	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (1 · (abs‘(𝐹‘𝑘))) < (abs‘(𝐹‘(𝑘 + 1))))
187	164, 186	eqbrtrrd 5137	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (abs‘(𝐹‘𝑘)) < (abs‘(𝐹‘(𝑘 + 1))))
188	156, 159, 187	ltled 11375	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1))))
189	188	ex 418	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → ((abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1) → (abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))))
190	189	ralimdva 3179	. . . . . . . . 9 ⊢ (((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) → (∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1) → ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))))
191	190	reximdva 3180	. . . . . . . 8 ⊢ ((𝜑 ∧ 1 < 𝐿) → (∃𝑛 ∈ 𝑊 ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1) → ∃𝑛 ∈ 𝑊 ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))))
192	153, 191	mpd 16	. . . . . . 7 ⊢ ((𝜑 ∧ 1 < 𝐿) → ∃𝑛 ∈ 𝑊 ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1))))
193	145, 192	r19.29a 3175	. . . . . 6 ⊢ ((𝜑 ∧ 1 < 𝐿) → seq𝑁( + , 𝐹) ∉ dom ⇝ )
194		df-nel 3067	. . . . . 6 ⊢ (seq𝑁( + , 𝐹) ∉ dom ⇝ ↔ ¬ seq𝑁( + , 𝐹) ∈ dom ⇝ )
195	193, 194	sylib 221	. . . . 5 ⊢ ((𝜑 ∧ 1 < 𝐿) → ¬ seq𝑁( + , 𝐹) ∈ dom ⇝ )
196	120	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 1 < 𝐿) → (seq𝑀( + , 𝐹) ∈ dom ⇝ ↔ seq𝑁( + , 𝐹) ∈ dom ⇝ ))
197	195, 196	mtbird 328	. . . 4 ⊢ ((𝜑 ∧ 1 < 𝐿) → ¬ seq𝑀( + , 𝐹) ∈ dom ⇝ )
198	128, 197	syldan 603	. . 3 ⊢ ((𝜑 ∧ ¬ 𝐿 < 1) → ¬ seq𝑀( + , 𝐹) ∈ dom ⇝ )
199	198	ex 418	. 2 ⊢ (𝜑 → (¬ 𝐿 < 1 → ¬ seq𝑀( + , 𝐹) ∈ dom ⇝ ))
200	123, 199	impcon4bid 230	1 ⊢ (𝜑 → (𝐿 < 1 ↔ seq𝑀( + , 𝐹) ∈ dom ⇝ ))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 ∧ w3a 1103 = wceq 1570 ∈ wcel 2146 ≠ wne 2960 ∉ wnel 3066 ∀wral 3081 ∃wrex 3091 ∅c0 4286 class class class wbr 5111 ↦ cmpt 5194 dom cdm 5663 ‘cfv 6540 (class class class)co 7419 ℂcc 11115 ℝcr 11116 0cc0 11117 1c1 11118 + caddc 11120 · cmul 11122 ℝ^*cxr 11259 < clt 11260 ≤ cle 11261 − cmin 11458 -cneg 11459 / cdiv 11888 ℤcz 12608 ℤ_≥cuz 12880 ℝ⁺crp 13034 (,)cioo 13390 seqcseq 14057 abscabs 15311 ⇝ cli 15561

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-rep 5240 ax-sep 5259 ax-nul 5271 ax-pow 5338 ax-pr 5406 ax-un 7742 ax-inf2 9617 ax-cnex 11173 ax-resscn 11174 ax-1cn 11175 ax-icn 11176 ax-addcl 11177 ax-addrcl 11178 ax-mulcl 11179 ax-mulrcl 11180 ax-mulcom 11181 ax-addass 11182 ax-mulass 11183 ax-distr 11184 ax-i2m1 11185 ax-1ne0 11186 ax-1rid 11187 ax-rnegex 11188 ax-rrecex 11189 ax-cnre 11190 ax-pre-lttri 11191 ax-pre-lttrn 11192 ax-pre-ltadd 11193 ax-pre-mulgt0 11194 ax-pre-sup 11195

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3067 df-ral 3082 df-rex 3092 df-rmo 3371 df-reu 3372 df-rab 3419 df-v 3459 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4287 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4875 df-int 4915 df-iun 4960 df-br 5112 df-opab 5176 df-mpt 5195 df-tr 5221 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-se 5617 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6306 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6496 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-isom 6549 df-riota 7376 df-ov 7422 df-oprab 7423 df-mpo 7424 df-om 7869 df-1st 7992 df-2nd 7993 df-frecs 8284 df-wrecs 8315 df-recs 8364 df-rdg 8403 df-1o 8459 df-er 8700 df-pm 8833 df-en 8950 df-dom 8951 df-sdom 8952 df-fin 8953 df-sup 9409 df-inf 9410 df-oi 9479 df-card 9941 df-pnf 11262 df-mnf 11263 df-xr 11264 df-ltxr 11265 df-le 11266 df-sub 11460 df-neg 11461 df-div 11889 df-nn 12251 df-2 12320 df-3 12321 df-n0 12522 df-z 12609 df-uz 12881 df-q 12991 df-rp 13035 df-ioo 13394 df-ico 13396 df-fz 13554 df-fzo 13702 df-fl 13845 df-seq 14058 df-exp 14118 df-hash 14387 df-shft 15130 df-cj 15176 df-re 15177 df-im 15178 df-sqrt 15312 df-abs 15313 df-limsup 15548 df-clim 15565 df-rlim 15566 df-sum 15764

This theorem is used by: radcnvrat 45084

W3C validator