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 41901

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

(It also demonstrates how to use climi2 15218 and absltd 15139 to transform a limit to an inequality cf. https://math.stackexchange.com/q/2215191 15139, and how to use r19.29a 3220 in a similar fashion to Mario Carneiro's proof sketch with rexlimdva 3215 at https://groups.google.com/g/metamath/c/2RPikOiXLMo 3215.) (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 13108	. . . . . . . . . 10 ⊢ (𝑟 ∈ (𝐿(,)1) → 𝑟 ∈ ℝ)
4	3	ad3antlr 728	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑘)))) → 𝑟 ∈ ℝ)
5		cvgdvgrat.n	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑁 ∈ 𝑍)
6		cvgdvgrat.z	. . . . . . . . . . . . . . . . 17 ⊢ 𝑍 = (ℤ_≥‘𝑀)
7	5, 6	eleqtrdi 2851	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘𝑀))
8		eluzelz 12591	. . . . . . . . . . . . . . . 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 12641	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ 𝑊 → (𝑘 + 1) ∈ 𝑊)
14		ovex 7304	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 + 1) ∈ V
15		eleq1 2828	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 = (𝑘 + 1) → (𝑖 ∈ 𝑊 ↔ (𝑘 + 1) ∈ 𝑊))
16	15	anbi2d 629	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = (𝑘 + 1) → ((𝜑 ∧ 𝑖 ∈ 𝑊) ↔ (𝜑 ∧ (𝑘 + 1) ∈ 𝑊)))
17		fveq2 6771	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 = (𝑘 + 1) → (𝐹‘𝑖) = (𝐹‘(𝑘 + 1)))
18	17	eleq1d 2825	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = (𝑘 + 1) → ((𝐹‘𝑖) ∈ ℂ ↔ (𝐹‘(𝑘 + 1)) ∈ ℂ))
19	16, 18	imbi12d 345	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = (𝑘 + 1) → (((𝜑 ∧ 𝑖 ∈ 𝑊) → (𝐹‘𝑖) ∈ ℂ) ↔ ((𝜑 ∧ (𝑘 + 1) ∈ 𝑊) → (𝐹‘(𝑘 + 1)) ∈ ℂ)))
20		eleq1 2828	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = 𝑖 → (𝑘 ∈ 𝑊 ↔ 𝑖 ∈ 𝑊))
21	20	anbi2d 629	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = 𝑖 → ((𝜑 ∧ 𝑘 ∈ 𝑊) ↔ (𝜑 ∧ 𝑖 ∈ 𝑊)))
22		fveq2 6771	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = 𝑖 → (𝐹‘𝑘) = (𝐹‘𝑖))
23	22	eleq1d 2825	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = 𝑖 → ((𝐹‘𝑘) ∈ ℂ ↔ (𝐹‘𝑖) ∈ ℂ))
24	21, 23	imbi12d 345	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = 𝑖 → (((𝜑 ∧ 𝑘 ∈ 𝑊) → (𝐹‘𝑘) ∈ ℂ) ↔ ((𝜑 ∧ 𝑖 ∈ 𝑊) → (𝐹‘𝑖) ∈ ℂ)))
25	1	eleq2i 2832	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 ∈ 𝑊 ↔ 𝑘 ∈ (ℤ_≥‘𝑁))
26	6	uztrn2 12600	. . . . . . . . . . . . . . . . . . . . . . . . 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 2006	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑊) → (𝐹‘𝑖) ∈ ℂ)
32	14, 19, 31	vtocl 3497	. . . . . . . . . . . . . . . . . . . 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 15146	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) ∈ ℝ)
37	12, 36	fvmpt2d 6885	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → (𝑅‘𝑘) = (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))))
38	37, 36	eqeltrd 2841	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → (𝑅‘𝑘) ∈ ℝ)
39	1, 9, 10, 38	climrecl 15290	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐿 ∈ ℝ)
40	39	rexrd 11026	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐿 ∈ ℝ^*)
41		1xr 11035	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℝ^*
42		elioo2 13119	. . . . . . . . . . . . 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 7294	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑖 → (𝐹‘(𝑘 + 1)) = (𝐹‘(𝑖 + 1)))
52	51	fveq2d 6775	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑖 → (abs‘(𝐹‘(𝑘 + 1))) = (abs‘(𝐹‘(𝑖 + 1))))
53	22	fveq2d 6775	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑖 → (abs‘(𝐹‘𝑘)) = (abs‘(𝐹‘𝑖)))
54	53	oveq2d 7287	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑖 → (𝑟 · (abs‘(𝐹‘𝑘))) = (𝑟 · (abs‘(𝐹‘𝑖))))
55	52, 54	breq12d 5092	. . . . . . . . . . 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 15593	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑘)))) → seq𝑁( + , 𝐹) ∈ dom ⇝ )
59	9	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) → 𝑁 ∈ ℤ)
60	44	simp2d 1142	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) → 𝐿 < 𝑟)
61		difrp 12767	. . . . . . . . . . . 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 15218	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) → ∃𝑛 ∈ 𝑊 ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿))
67	1	uztrn2 12600	. . . . . . . . . . . . . . . . . 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 15146	. . . . . . . . . . . . 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 15146	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (abs‘(𝐹‘𝑘)) ∈ ℝ)
79	73, 78	remulcld 11006	. . . . . . . . . . . . 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 15165	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) = ((abs‘(𝐹‘(𝑘 + 1))) / (abs‘(𝐹‘𝑘))))
85	70, 76, 82	divcld 11751	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → ((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘)) ∈ ℂ)
86	85	abscld 15146	. . . . . . . . . . . . . . . . . . . 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 15139	. . . . . . . . . . . . . . . . . 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 15146	. . . . . . . . . . . . . . . . . 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 5103	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → ((abs‘(𝐹‘(𝑘 + 1))) / (abs‘(𝐹‘𝑘))) < 𝑟)
99	77, 83	absrpcld 15158	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (abs‘(𝐹‘𝑘)) ∈ ℝ⁺)
100	72, 73, 99	ltdivmuld 12822	. . . . . . . . . . . . . . 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 12773	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (abs‘(𝐹‘𝑘)) ∈ ℂ)
103	73	recnd 11004	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → 𝑟 ∈ ℂ)
104	102, 103	mulcomd 10997	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → ((abs‘(𝐹‘𝑘)) · 𝑟) = (𝑟 · (abs‘(𝐹‘𝑘))))
105	101, 104	breqtrd 5105	. . . . . . . . . . . . 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 3105	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) → (∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿) → ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑘)))))
109	108	reximdva 3205	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) → (∃𝑛 ∈ 𝑊 ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿) → ∃𝑛 ∈ 𝑊 ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑘)))))
110	66, 109	mpd 15	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) → ∃𝑛 ∈ 𝑊 ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑘))))
111	58, 110	r19.29a 3220	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) → seq𝑁( + , 𝐹) ∈ dom ⇝ )
112	111	ralrimiva 3110	. . . . . 6 ⊢ (𝜑 → ∀𝑟 ∈ (𝐿(,)1)seq𝑁( + , 𝐹) ∈ dom ⇝ )
113	112	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝐿 < 1) → ∀𝑟 ∈ (𝐿(,)1)seq𝑁( + , 𝐹) ∈ dom ⇝ )
114		ioon0 13104	. . . . . . . 8 ⊢ ((𝐿 ∈ ℝ^* ∧ 1 ∈ ℝ^*) → ((𝐿(,)1) ≠ ∅ ↔ 𝐿 < 1))
115	40, 41, 114	sylancl 586	. . . . . . 7 ⊢ (𝜑 → ((𝐿(,)1) ≠ ∅ ↔ 𝐿 < 1))
116	115	biimpar 478	. . . . . 6 ⊢ ((𝜑 ∧ 𝐿 < 1) → (𝐿(,)1) ≠ ∅)
117		r19.3rzv 4435	. . . . . 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 15366	. . . . 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 10977	. . . . . . 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 12600	. . . . . . . . . . . 12 ⊢ ((𝑛 ∈ 𝑊 ∧ 𝑖 ∈ (ℤ_≥‘𝑛)) → 𝑖 ∈ 𝑊)
135	22	neeq1d 3005	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑖 → ((𝐹‘𝑘) ≠ 0 ↔ (𝐹‘𝑖) ≠ 0))
136	21, 135	imbi12d 345	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑖 → (((𝜑 ∧ 𝑘 ∈ 𝑊) → (𝐹‘𝑘) ≠ 0) ↔ ((𝜑 ∧ 𝑖 ∈ 𝑊) → (𝐹‘𝑖) ≠ 0)))
137	136, 34	chvarvv 2006	. . . . . . . . . . . 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 5092	. . . . . . . . . 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 41900	. . . . . . 7 ⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))) → seq𝑁( + , 𝐹) ∉ dom ⇝ )
146	9	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 1 < 𝐿) → 𝑁 ∈ ℤ)
147		1re 10976	. . . . . . . . . . 11 ⊢ 1 ∈ ℝ
148		difrp 12767	. . . . . . . . . . 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 15218	. . . . . . . 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 15146	. . . . . . . . . . . 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 15146	. . . . . . . . . . . 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 15158	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (abs‘(𝐹‘𝑘)) ∈ ℝ⁺)
163	162	rpcnd 12773	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (abs‘(𝐹‘𝑘)) ∈ ℂ)
164	163	mulid2d 10994	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (1 · (abs‘(𝐹‘𝑘))) = (abs‘(𝐹‘𝑘)))
165	39	ad4antr 729	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → 𝐿 ∈ ℝ)
166	165	recnd 11004	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → 𝐿 ∈ ℂ)
167		1cnd 10971	. . . . . . . . . . . . . . . . . 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 15146	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) ∈ ℝ)
171	39	ad3antrrr 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → 𝐿 ∈ ℝ)
172	170, 171	resubcld 11403	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿) ∈ ℝ)
173		1red 10977	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → 1 ∈ ℝ)
174	171, 173	resubcld 11403	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → (𝐿 − 1) ∈ ℝ)
175	172, 174	absltd 15139	. . . . . . . . . . . . . . . . . 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 5103	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (1 − 𝐿) < ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿))
178		1red 10977	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → 1 ∈ ℝ)
179	158, 155, 161	divcld 11751	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → ((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘)) ∈ ℂ)
180	179	abscld 15146	. . . . . . . . . . . . . . . . 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 15165	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) = ((abs‘(𝐹‘(𝑘 + 1))) / (abs‘(𝐹‘𝑘))))
184	182, 183	breqtrd 5105	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → 1 < ((abs‘(𝐹‘(𝑘 + 1))) / (abs‘(𝐹‘𝑘))))
185	178, 159, 162	ltmuldivd 12818	. . . . . . . . . . . . . 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 5103	. . . . . . . . . . . 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 3105	. . . . . . . . 9 ⊢ (((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) → (∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1) → ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))))
191	190	reximdva 3205	. . . . . . . 8 ⊢ ((𝜑 ∧ 1 < 𝐿) → (∃𝑛 ∈ 𝑊 ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1) → ∃𝑛 ∈ 𝑊 ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))))
192	153, 191	mpd 15	. . . . . . 7 ⊢ ((𝜑 ∧ 1 < 𝐿) → ∃𝑛 ∈ 𝑊 ∀𝑘 ∈ (ℤ_≥‘𝑛)(abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1))))
193	145, 192	r19.29a 3220	. . . . . 6 ⊢ ((𝜑 ∧ 1 < 𝐿) → seq𝑁( + , 𝐹) ∉ dom ⇝ )
194		df-nel 3052	. . . . . 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 1542 ∈ wcel 2110 ≠ wne 2945 ∉ wnel 3051 ∀wral 3066 ∃wrex 3067 ∅c0 4262 class class class wbr 5079 ↦ cmpt 5162 dom cdm 5590 ‘cfv 6432 (class class class)co 7271 ℂcc 10870 ℝcr 10871 0cc0 10872 1c1 10873 + caddc 10875 · cmul 10877 ℝ^*cxr 11009 < clt 11010 ≤ cle 11011 − cmin 11205 -cneg 11206 / cdiv 11632 ℤcz 12319 ℤ_≥cuz 12581 ℝ⁺crp 12729 (,)cioo 13078 seqcseq 13719 abscabs 14943 ⇝ cli 15191

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2015 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2158 ax-12 2175 ax-ext 2711 ax-rep 5214 ax-sep 5227 ax-nul 5234 ax-pow 5292 ax-pr 5356 ax-un 7582 ax-inf2 9377 ax-cnex 10928 ax-resscn 10929 ax-1cn 10930 ax-icn 10931 ax-addcl 10932 ax-addrcl 10933 ax-mulcl 10934 ax-mulrcl 10935 ax-mulcom 10936 ax-addass 10937 ax-mulass 10938 ax-distr 10939 ax-i2m1 10940 ax-1ne0 10941 ax-1rid 10942 ax-rnegex 10943 ax-rrecex 10944 ax-cnre 10945 ax-pre-lttri 10946 ax-pre-lttrn 10947 ax-pre-ltadd 10948 ax-pre-mulgt0 10949 ax-pre-sup 10950

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2072 df-mo 2542 df-eu 2571 df-clab 2718 df-cleq 2732 df-clel 2818 df-nfc 2891 df-ne 2946 df-nel 3052 df-ral 3071 df-rex 3072 df-reu 3073 df-rmo 3074 df-rab 3075 df-v 3433 df-sbc 3721 df-csb 3838 df-dif 3895 df-un 3897 df-in 3899 df-ss 3909 df-pss 3911 df-nul 4263 df-if 4466 df-pw 4541 df-sn 4568 df-pr 4570 df-op 4574 df-uni 4846 df-int 4886 df-iun 4932 df-br 5080 df-opab 5142 df-mpt 5163 df-tr 5197 df-id 5490 df-eprel 5496 df-po 5504 df-so 5505 df-fr 5545 df-se 5546 df-we 5547 df-xp 5596 df-rel 5597 df-cnv 5598 df-co 5599 df-dm 5600 df-rn 5601 df-res 5602 df-ima 5603 df-pred 6201 df-ord 6268 df-on 6269 df-lim 6270 df-suc 6271 df-iota 6390 df-fun 6434 df-fn 6435 df-f 6436 df-f1 6437 df-fo 6438 df-f1o 6439 df-fv 6440 df-isom 6441 df-riota 7228 df-ov 7274 df-oprab 7275 df-mpo 7276 df-om 7707 df-1st 7824 df-2nd 7825 df-frecs 8088 df-wrecs 8119 df-recs 8193 df-rdg 8232 df-1o 8288 df-er 8481 df-pm 8601 df-en 8717 df-dom 8718 df-sdom 8719 df-fin 8720 df-sup 9179 df-inf 9180 df-oi 9247 df-card 9698 df-pnf 11012 df-mnf 11013 df-xr 11014 df-ltxr 11015 df-le 11016 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 12582 df-q 12688 df-rp 12730 df-ioo 13082 df-ico 13084 df-fz 13239 df-fzo 13382 df-fl 13510 df-seq 13720 df-exp 13781 df-hash 14043 df-shft 14776 df-cj 14808 df-re 14809 df-im 14810 df-sqrt 14944 df-abs 14945 df-limsup 15178 df-clim 15195 df-rlim 15196 df-sum 15396

This theorem is referenced by: radcnvrat 41902

W3C validator