Theorem radcnvrat 45298

Description: Let 𝐿 be the limit, if one exists, of the ratio (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))) (as in the ratio test cvgdvgrat 45297) as 𝑘 increases. Then the radius of convergence of power series Σ𝑛 ∈ ℕ₀((𝐴‘𝑛) · (𝑥↑𝑛)) is (1 / 𝐿) if 𝐿 is nonzero. Proof "The limit involved in the ratio test..." in https://en.wikipedia.org/wiki/Radius_of_convergence 45297 —a few lines that evidently hide quite an involved process to confirm. (Contributed by Steve Rodriguez, 8-Mar-2020.)

Hypotheses

Ref	Expression
radcnvrat.g	⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))))
radcnvrat.a	⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)
radcnvrat.r	⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < )
radcnvrat.rat	⊢ 𝐷 = (𝑘 ∈ ℕ0 ↦ (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))))
radcnvrat.z	⊢ 𝑍 = (ℤ≥‘𝑀)
radcnvrat.m	⊢ (𝜑 → 𝑀 ∈ ℕ0)
radcnvrat.n0	⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐴‘𝑘) ≠ 0)
radcnvrat.l	⊢ (𝜑 → 𝐷 ⇝ 𝐿)
radcnvrat.ln0	⊢ (𝜑 → 𝐿 ≠ 0)

Assertion

Ref	Expression
radcnvrat	⊢ (𝜑 → 𝑅 = (1 / 𝐿))

Distinct variable groups:   𝑘,𝑛,𝑥,𝜑   𝐴,𝑛,𝑥   𝑘,𝐺,𝑛,𝑥   𝑘,𝑟,𝑥,𝐺   𝑘,𝐿,𝑥   𝑘,𝑍,𝑛   𝐷,𝑘   𝑘,𝑀

Allowed substitution hints:   𝜑(𝑟)   𝐴(𝑘, 𝑟)   𝐷(𝑥, 𝑛, 𝑟)   𝑅(𝑥, 𝑘, 𝑛, 𝑟)   𝐿(𝑛, 𝑟)   𝑀(𝑥, 𝑛, 𝑟)   𝑍(𝑥, 𝑟)

Proof of Theorem radcnvrat

Step	Hyp	Ref	Expression
1		radcnvrat.r	. 2 ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < )
2		xrltso 13270	. . . 4 ⊢ < Or ℝ*
3	2	a1i 11	. . 3 ⊢ (𝜑 → < Or ℝ*)
4		radcnvrat.z	. . . . . 6 ⊢ 𝑍 = (ℤ≥‘𝑀)
5		radcnvrat.m	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ ℕ0)
6	5	nn0zd 12718	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℤ)
7	4	reseq2i 5966	. . . . . . 7 ⊢ (𝐷 ↾ 𝑍) = (𝐷 ↾ (ℤ≥‘𝑀))
8		radcnvrat.l	. . . . . . . 8 ⊢ (𝜑 → 𝐷 ⇝ 𝐿)
9		radcnvrat.rat	. . . . . . . . . 10 ⊢ 𝐷 = (𝑘 ∈ ℕ0 ↦ (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))))
10		nn0ex 12612	. . . . . . . . . . 11 ⊢ ℕ0 ∈ V
11	10	mptex 7229	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ0 ↦ (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)))) ∈ V
12	9, 11	eqeltri 2856	. . . . . . . . 9 ⊢ 𝐷 ∈ V
13		climres 15742	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝐷 ∈ V) → ((𝐷 ↾ (ℤ≥‘𝑀)) ⇝ 𝐿 ↔ 𝐷 ⇝ 𝐿))
14	6, 12, 13	sylancl 598	. . . . . . . 8 ⊢ (𝜑 → ((𝐷 ↾ (ℤ≥‘𝑀)) ⇝ 𝐿 ↔ 𝐷 ⇝ 𝐿))
15	8, 14	mpbird 260	. . . . . . 7 ⊢ (𝜑 → (𝐷 ↾ (ℤ≥‘𝑀)) ⇝ 𝐿)
16	7, 15	eqbrtrid 5139	. . . . . 6 ⊢ (𝜑 → (𝐷 ↾ 𝑍) ⇝ 𝐿)
17	9	reseq1i 5965	. . . . . . . . 9 ⊢ (𝐷 ↾ 𝑍) = ((𝑘 ∈ ℕ0 ↦ (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)))) ↾ 𝑍)
18		eluznn0 13044	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → 𝑘 ∈ ℕ0)
19	5, 18	sylan 592	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → 𝑘 ∈ ℕ0)
20	19	ex 418	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑘 ∈ (ℤ≥‘𝑀) → 𝑘 ∈ ℕ0))
21	20	ssrdv 3914	. . . . . . . . . . 11 ⊢ (𝜑 → (ℤ≥‘𝑀) ⊆ ℕ0)
22	4, 21	eqsstrid 3946	. . . . . . . . . 10 ⊢ (𝜑 → 𝑍 ⊆ ℕ0)
23	22	resmptd 6031	. . . . . . . . 9 ⊢ (𝜑 → ((𝑘 ∈ ℕ0 ↦ (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)))) ↾ 𝑍) = (𝑘 ∈ 𝑍 ↦ (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)))))
24	17, 23	eqtrid 2807	. . . . . . . 8 ⊢ (𝜑 → (𝐷 ↾ 𝑍) = (𝑘 ∈ 𝑍 ↦ (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)))))
25		fvexd 6900	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))) ∈ V)
26	24, 25	fvmpt2d 7007	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝐷 ↾ 𝑍)‘𝑘) = (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))))
27	4	peano2uzs 13029	. . . . . . . . . 10 ⊢ (𝑘 ∈ 𝑍 → (𝑘 + 1) ∈ 𝑍)
28	22	sselda 3908	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ 𝑍) → (𝑘 + 1) ∈ ℕ0)
29		radcnvrat.a	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)
30	29	ffvelcdmda 7084	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ ℕ0) → (𝐴‘(𝑘 + 1)) ∈ ℂ)
31	28, 30	syldan 603	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ 𝑍) → (𝐴‘(𝑘 + 1)) ∈ ℂ)
32	27, 31	sylan2 605	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐴‘(𝑘 + 1)) ∈ ℂ)
33	22	sselda 3908	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ ℕ0)
34	29	ffvelcdmda 7084	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐴‘𝑘) ∈ ℂ)
35	33, 34	syldan 603	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐴‘𝑘) ∈ ℂ)
36		radcnvrat.n0	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐴‘𝑘) ≠ 0)
37	32, 35, 36	divcld 12093	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)) ∈ ℂ)
38	37	abscld 15606	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))) ∈ ℝ)
39	26, 38	eqeltrd 2860	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝐷 ↾ 𝑍)‘𝑘) ∈ ℝ)
40	4, 6, 16, 39	climrecl 15750	. . . . 5 ⊢ (𝜑 → 𝐿 ∈ ℝ)
41		radcnvrat.ln0	. . . . 5 ⊢ (𝜑 → 𝐿 ≠ 0)
42	40, 41	rereccld 12144	. . . 4 ⊢ (𝜑 → (1 / 𝐿) ∈ ℝ)
43	42	rexrd 11359	. . 3 ⊢ (𝜑 → (1 / 𝐿) ∈ ℝ*)
44		simpr 490	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }) → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ })
45		elrabi 3640	. . . . 5 ⊢ (𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ } → 𝑥 ∈ ℝ)
46	42	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (1 / 𝐿) ∈ ℝ)
47		recn 11290	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
48	47	abscld 15606	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → (abs‘𝑥) ∈ ℝ)
49	48	adantl 487	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (abs‘𝑥) ∈ ℝ)
50	46, 49	ltlend 11455	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((1 / 𝐿) < (abs‘𝑥) ↔ ((1 / 𝐿) ≤ (abs‘𝑥) ∧ (abs‘𝑥) ≠ (1 / 𝐿))))
51	50	simplbda 505	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (1 / 𝐿) < (abs‘𝑥)) → (abs‘𝑥) ≠ (1 / 𝐿))
52	50	adantr 486	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (abs‘𝑥) ≠ (1 / 𝐿)) → ((1 / 𝐿) < (abs‘𝑥) ↔ ((1 / 𝐿) ≤ (abs‘𝑥) ∧ (abs‘𝑥) ≠ (1 / 𝐿))))
53		simpr 490	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (abs‘𝑥) ≠ (1 / 𝐿)) → (abs‘𝑥) ≠ (1 / 𝐿))
54	53	biantrud 541	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (abs‘𝑥) ≠ (1 / 𝐿)) → ((1 / 𝐿) ≤ (abs‘𝑥) ↔ ((1 / 𝐿) ≤ (abs‘𝑥) ∧ (abs‘𝑥) ≠ (1 / 𝐿))))
55	46, 49	lenltd 11456	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((1 / 𝐿) ≤ (abs‘𝑥) ↔ ¬ (abs‘𝑥) < (1 / 𝐿)))
56	55	adantr 486	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (abs‘𝑥) ≠ (1 / 𝐿)) → ((1 / 𝐿) ≤ (abs‘𝑥) ↔ ¬ (abs‘𝑥) < (1 / 𝐿)))
57	52, 54, 56	3bitr2d 310	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (abs‘𝑥) ≠ (1 / 𝐿)) → ((1 / 𝐿) < (abs‘𝑥) ↔ ¬ (abs‘𝑥) < (1 / 𝐿)))
58		1cnd 11302	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 1 ∈ ℂ)
59	49	recnd 11337	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (abs‘𝑥) ∈ ℂ)
60	40	recnd 11337	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐿 ∈ ℂ)
61	60	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐿 ∈ ℂ)
62	41	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐿 ≠ 0)
63	58, 59, 61, 62	divmul3d 12127	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((1 / 𝐿) = (abs‘𝑥) ↔ 1 = ((abs‘𝑥) · 𝐿)))
64		eqcom 2767	. . . . . . . . . . . . . . . . 17 ⊢ ((1 / 𝐿) = (abs‘𝑥) ↔ (abs‘𝑥) = (1 / 𝐿))
65		eqcom 2767	. . . . . . . . . . . . . . . . 17 ⊢ (1 = ((abs‘𝑥) · 𝐿) ↔ ((abs‘𝑥) · 𝐿) = 1)
66	63, 64, 65	3bitr3g 316	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((abs‘𝑥) = (1 / 𝐿) ↔ ((abs‘𝑥) · 𝐿) = 1))
67	66	necon3bid 2999	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((abs‘𝑥) ≠ (1 / 𝐿) ↔ ((abs‘𝑥) · 𝐿) ≠ 1))
68	67	biimpa 482	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (abs‘𝑥) ≠ (1 / 𝐿)) → ((abs‘𝑥) · 𝐿) ≠ 1)
69		1red 11309	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 1 ∈ ℝ)
70		fvres 6904	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 ∈ 𝑍 → ((𝐷 ↾ 𝑍)‘𝑘) = (𝐷‘𝑘))
71	70	adantl 487	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝐷 ↾ 𝑍)‘𝑘) = (𝐷‘𝑘))
72	71, 39	eqeltrrd 2861	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐷‘𝑘) ∈ ℝ)
73	37	absge0d 15614	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 0 ≤ (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))))
74	73, 26	breqtrrd 5132	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 0 ≤ ((𝐷 ↾ 𝑍)‘𝑘))
75	74, 71	breqtrd 5130	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 0 ≤ (𝐷‘𝑘))
76	4, 6, 8, 72, 75	climge0 15751	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 0 ≤ 𝐿)
77	40, 76, 41	ne0gt0d 11447	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 0 < 𝐿)
78	40, 77	elrpd 13161	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐿 ∈ ℝ+)
79	78	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐿 ∈ ℝ+)
80	49, 69, 79	ltmuldivd 13211	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((abs‘𝑥) · 𝐿) < 1 ↔ (abs‘𝑥) < (1 / 𝐿)))
81	80	adantr 486	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) → (((abs‘𝑥) · 𝐿) < 1 ↔ (abs‘𝑥) < (1 / 𝐿)))
82		elun 4152	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ((ℝ ∩ {0}) ∪ (ℝ ∖ {0})) ↔ (𝑥 ∈ (ℝ ∩ {0}) ∨ 𝑥 ∈ (ℝ ∖ {0})))
83		inundif 4434	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℝ ∩ {0}) ∪ (ℝ ∖ {0})) = ℝ
84	83	eleq2i 2852	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ((ℝ ∩ {0}) ∪ (ℝ ∖ {0})) ↔ 𝑥 ∈ ℝ)
85	82, 84	bitr3i 280	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ (ℝ ∩ {0}) ∨ 𝑥 ∈ (ℝ ∖ {0})) ↔ 𝑥 ∈ ℝ)
86		elin 4093	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ (ℝ ∩ {0}) ↔ (𝑥 ∈ ℝ ∧ 𝑥 ∈ {0}))
87	86	simprbi 503	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (ℝ ∩ {0}) → 𝑥 ∈ {0})
88		elsni 4600	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ {0} → 𝑥 = 0)
89	87, 88	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (ℝ ∩ {0}) → 𝑥 = 0)
90		fveq2 6885	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = 0 → (abs‘𝑥) = (abs‘0))
91		abs0 15452	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (abs‘0) = 0
92	90, 91	eqtrdi 2811	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 0 → (abs‘𝑥) = 0)
93	92	oveq1d 7435	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 0 → ((abs‘𝑥) · 𝐿) = (0 · 𝐿))
94	60	mul02d 11508	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (0 · 𝐿) = 0)
95	93, 94	sylan9eqr 2817	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 = 0) → ((abs‘𝑥) · 𝐿) = 0)
96		0lt1 11838	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 < 1
97	95, 96	eqbrtrdi 5143	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 = 0) → ((abs‘𝑥) · 𝐿) < 1)
98		radcnvrat.g	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))))
99	98, 29	radcnv0 26743	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 0 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ })
100		eleq1 2848	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 0 → (𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ } ↔ 0 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
101	99, 100	syl5ibrcom 250	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑥 = 0 → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
102	101	imp 412	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 = 0) → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ })
103	97, 102	2thd 268	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 = 0) → (((abs‘𝑥) · 𝐿) < 1 ↔ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
104	89, 103	sylan2 605	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∩ {0})) → (((abs‘𝑥) · 𝐿) < 1 ↔ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
105	104	adantlr 728	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ((abs‘𝑥) · 𝐿) ≠ 1) ∧ 𝑥 ∈ (ℝ ∩ {0})) → (((abs‘𝑥) · 𝐿) < 1 ↔ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
106		ax-resscn 11257	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ℝ ⊆ ℂ
107		ssdif 4080	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℝ ⊆ ℂ → (ℝ ∖ {0}) ⊆ (ℂ ∖ {0}))
108	106, 107	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (ℝ ∖ {0}) ⊆ (ℂ ∖ {0})
109	108	sseli 3904	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (ℝ ∖ {0}) → 𝑥 ∈ (ℂ ∖ {0}))
110		nn0uz 13003	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ℕ0 = (ℤ≥‘0)
111	5	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) → 𝑀 ∈ ℕ0)
112		fvexd 6900	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) → (𝐺‘𝑥) ∈ V)
113		eldifi 4067	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 ∈ (ℂ ∖ {0}) → 𝑥 ∈ ℂ)
114	98	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))))
115	10	mptex 7229	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))) ∈ V
116	115	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))) ∈ V)
117	114, 116	fvmpt2d 7007	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (𝐺‘𝑥) = (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))))
118	117	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑥) = (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))))
119		fveq2 6885	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑛 = 𝑘 → (𝐴‘𝑛) = (𝐴‘𝑘))
120		oveq2 7428	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑛 = 𝑘 → (𝑥↑𝑛) = (𝑥↑𝑘))
121	119, 120	oveq12d 7438	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑛 = 𝑘 → ((𝐴‘𝑛) · (𝑥↑𝑛)) = ((𝐴‘𝑘) · (𝑥↑𝑘)))
122	121	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) ∧ 𝑛 = 𝑘) → ((𝐴‘𝑛) · (𝑥↑𝑛)) = ((𝐴‘𝑘) · (𝑥↑𝑘)))
123		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ ℕ0)
124		ovexd 7455	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → ((𝐴‘𝑘) · (𝑥↑𝑘)) ∈ V)
125	118, 122, 123, 124	fvmptd 7001	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → ((𝐺‘𝑥)‘𝑘) = ((𝐴‘𝑘) · (𝑥↑𝑘)))
126	34	adantlr 728	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (𝐴‘𝑘) ∈ ℂ)
127		simplr 781	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → 𝑥 ∈ ℂ)
128	127, 123	expcld 14289	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (𝑥↑𝑘) ∈ ℂ)
129	126, 128	mulcld 11329	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → ((𝐴‘𝑘) · (𝑥↑𝑘)) ∈ ℂ)
130	125, 129	eqeltrd 2860	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → ((𝐺‘𝑥)‘𝑘) ∈ ℂ)
131	113, 130	sylanl2 694	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ ℕ0) → ((𝐺‘𝑥)‘𝑘) ∈ ℂ)
132	131	adantlr 728	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) ∧ 𝑘 ∈ ℕ0) → ((𝐺‘𝑥)‘𝑘) ∈ ℂ)
133	33	adantlr 728	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ ℕ0)
134	133, 125	syldan 603	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) → ((𝐺‘𝑥)‘𝑘) = ((𝐴‘𝑘) · (𝑥↑𝑘)))
135	113, 134	sylanl2 694	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → ((𝐺‘𝑥)‘𝑘) = ((𝐴‘𝑘) · (𝑥↑𝑘)))
136	35	adantlr 728	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝐴‘𝑘) ∈ ℂ)
137	113	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → 𝑥 ∈ ℂ)
138	137	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → 𝑥 ∈ ℂ)
139	33	adantlr 728	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ ℕ0)
140	138, 139	expcld 14289	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝑥↑𝑘) ∈ ℂ)
141	36	adantlr 728	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝐴‘𝑘) ≠ 0)
142		eldifsni 4752	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 ∈ (ℂ ∖ {0}) → 𝑥 ≠ 0)
143	142	ad2antlr 740	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → 𝑥 ≠ 0)
144	139	nn0zd 12718	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ ℤ)
145	138, 143, 144	expne0d 14295	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝑥↑𝑘) ≠ 0)
146	136, 140, 141, 145	mulne0d 11968	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → ((𝐴‘𝑘) · (𝑥↑𝑘)) ≠ 0)
147	135, 146	eqnetrd 3022	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → ((𝐺‘𝑥)‘𝑘) ≠ 0)
148	147	adantlr 728	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) ∧ 𝑘 ∈ 𝑍) → ((𝐺‘𝑥)‘𝑘) ≠ 0)
149		fvoveq1 7443	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 = 𝑘 → ((𝐺‘𝑥)‘(𝑛 + 1)) = ((𝐺‘𝑥)‘(𝑘 + 1)))
150		fveq2 6885	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 = 𝑘 → ((𝐺‘𝑥)‘𝑛) = ((𝐺‘𝑥)‘𝑘))
151	149, 150	oveq12d 7438	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 𝑘 → (((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)) = (((𝐺‘𝑥)‘(𝑘 + 1)) / ((𝐺‘𝑥)‘𝑘)))
152	151	fveq2d 6889	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑘 → (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛))) = (abs‘(((𝐺‘𝑥)‘(𝑘 + 1)) / ((𝐺‘𝑥)‘𝑘))))
153	152	cbvmptv 5208	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ 𝑍 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) = (𝑘 ∈ 𝑍 ↦ (abs‘(((𝐺‘𝑥)‘(𝑘 + 1)) / ((𝐺‘𝑥)‘𝑘))))
154	4	reseq2i 5966	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ↾ 𝑍) = ((𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ↾ (ℤ≥‘𝑀))
155	22	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → 𝑍 ⊆ ℕ0)
156	155	resmptd 6031	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → ((𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ↾ 𝑍) = (𝑛 ∈ 𝑍 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))))
157	154, 156	eqtr3id 2809	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → ((𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ↾ (ℤ≥‘𝑀)) = (𝑛 ∈ 𝑍 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))))
158	6	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → 𝑀 ∈ ℤ)
159	8	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → 𝐷 ⇝ 𝐿)
160	137	abscld 15606	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (abs‘𝑥) ∈ ℝ)
161	160	recnd 11337	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (abs‘𝑥) ∈ ℂ)
162	10	mptex 7229	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ∈ V
163	162	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ∈ V)
164	72	recnd 11337	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐷‘𝑘) ∈ ℂ)
165	164	adantlr 728	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝐷‘𝑘) ∈ ℂ)
166		eqidd 2761	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) = (𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))))
167	152	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) ∧ 𝑛 = 𝑘) → (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛))) = (abs‘(((𝐺‘𝑥)‘(𝑘 + 1)) / ((𝐺‘𝑥)‘𝑘))))
168		fvexd 6900	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (abs‘(((𝐺‘𝑥)‘(𝑘 + 1)) / ((𝐺‘𝑥)‘𝑘))) ∈ V)
169	166, 167, 139, 168	fvmptd 7001	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → ((𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛))))‘𝑘) = (abs‘(((𝐺‘𝑥)‘(𝑘 + 1)) / ((𝐺‘𝑥)‘𝑘))))
170	117	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑥) = (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))))
171		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) ∧ 𝑛 = (𝑘 + 1)) → 𝑛 = (𝑘 + 1))
172	171	fveq2d 6889	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) ∧ 𝑛 = (𝑘 + 1)) → (𝐴‘𝑛) = (𝐴‘(𝑘 + 1)))
173	171	oveq2d 7436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) ∧ 𝑛 = (𝑘 + 1)) → (𝑥↑𝑛) = (𝑥↑(𝑘 + 1)))
174	172, 173	oveq12d 7438	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) ∧ 𝑛 = (𝑘 + 1)) → ((𝐴‘𝑛) · (𝑥↑𝑛)) = ((𝐴‘(𝑘 + 1)) · (𝑥↑(𝑘 + 1))))
175		1nn0 12622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ 1 ∈ ℕ0
176	175	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) → 1 ∈ ℕ0)
177	133, 176	nn0addcld 12671	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) → (𝑘 + 1) ∈ ℕ0)
178		ovexd 7455	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) → ((𝐴‘(𝑘 + 1)) · (𝑥↑(𝑘 + 1))) ∈ V)
179	170, 174, 177, 178	fvmptd 7001	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) → ((𝐺‘𝑥)‘(𝑘 + 1)) = ((𝐴‘(𝑘 + 1)) · (𝑥↑(𝑘 + 1))))
180	121	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) ∧ 𝑛 = 𝑘) → ((𝐴‘𝑛) · (𝑥↑𝑛)) = ((𝐴‘𝑘) · (𝑥↑𝑘)))
181		ovexd 7455	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) → ((𝐴‘𝑘) · (𝑥↑𝑘)) ∈ V)
182	170, 180, 133, 181	fvmptd 7001	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) → ((𝐺‘𝑥)‘𝑘) = ((𝐴‘𝑘) · (𝑥↑𝑘)))
183	179, 182	oveq12d 7438	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) → (((𝐺‘𝑥)‘(𝑘 + 1)) / ((𝐺‘𝑥)‘𝑘)) = (((𝐴‘(𝑘 + 1)) · (𝑥↑(𝑘 + 1))) / ((𝐴‘𝑘) · (𝑥↑𝑘))))
184	113, 183	sylanl2 694	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (((𝐺‘𝑥)‘(𝑘 + 1)) / ((𝐺‘𝑥)‘𝑘)) = (((𝐴‘(𝑘 + 1)) · (𝑥↑(𝑘 + 1))) / ((𝐴‘𝑘) · (𝑥↑𝑘))))
185	32	adantlr 728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝐴‘(𝑘 + 1)) ∈ ℂ)
186	113, 177	sylanl2 694	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝑘 + 1) ∈ ℕ0)
187	138, 186	expcld 14289	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝑥↑(𝑘 + 1)) ∈ ℂ)
188	185, 136, 187, 140, 141, 145	divmuldivd 12134	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)) · ((𝑥↑(𝑘 + 1)) / (𝑥↑𝑘))) = (((𝐴‘(𝑘 + 1)) · (𝑥↑(𝑘 + 1))) / ((𝐴‘𝑘) · (𝑥↑𝑘))))
189	139	nn0cnd 12669	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ ℂ)
190		1cnd 11302	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → 1 ∈ ℂ)
191	189, 190	pncan2d 11671	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → ((𝑘 + 1) − 𝑘) = 1)
192	191	oveq2d 7436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝑥↑((𝑘 + 1) − 𝑘)) = (𝑥↑1))
193	186	nn0zd 12718	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝑘 + 1) ∈ ℤ)
194	138, 143, 144, 193	expsubd 14300	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝑥↑((𝑘 + 1) − 𝑘)) = ((𝑥↑(𝑘 + 1)) / (𝑥↑𝑘)))
195	138	exp1d 14284	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝑥↑1) = 𝑥)
196	192, 194, 195	3eqtr3d 2803	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → ((𝑥↑(𝑘 + 1)) / (𝑥↑𝑘)) = 𝑥)
197	196	oveq2d 7436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)) · ((𝑥↑(𝑘 + 1)) / (𝑥↑𝑘))) = (((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)) · 𝑥))
198	184, 188, 197	3eqtr2d 2801	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (((𝐺‘𝑥)‘(𝑘 + 1)) / ((𝐺‘𝑥)‘𝑘)) = (((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)) · 𝑥))
199	198	fveq2d 6889	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (abs‘(((𝐺‘𝑥)‘(𝑘 + 1)) / ((𝐺‘𝑥)‘𝑘))) = (abs‘(((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)) · 𝑥)))
200	37	adantlr 728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → ((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)) ∈ ℂ)
201	200, 138	absmuld 15624	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (abs‘(((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)) · 𝑥)) = ((abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))) · (abs‘𝑥)))
202	169, 199, 201	3eqtrd 2799	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → ((𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛))))‘𝑘) = ((abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))) · (abs‘𝑥)))
203	71, 26	eqtr3d 2797	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐷‘𝑘) = (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))))
204	203	adantlr 728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝐷‘𝑘) = (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))))
205	204	eqcomd 2766	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))) = (𝐷‘𝑘))
206	205	oveq1d 7435	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → ((abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))) · (abs‘𝑥)) = ((𝐷‘𝑘) · (abs‘𝑥)))
207	161	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (abs‘𝑥) ∈ ℂ)
208	165, 207	mulcomd 11330	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → ((𝐷‘𝑘) · (abs‘𝑥)) = ((abs‘𝑥) · (𝐷‘𝑘)))
209	202, 206, 208	3eqtrd 2799	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → ((𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛))))‘𝑘) = ((abs‘𝑥) · (𝐷‘𝑘)))
210	4, 158, 159, 161, 163, 165, 209	climmulc2 15804	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ⇝ ((abs‘𝑥) · 𝐿))
211		climres 15742	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑀 ∈ ℤ ∧ (𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ∈ V) → (((𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ↾ (ℤ≥‘𝑀)) ⇝ ((abs‘𝑥) · 𝐿) ↔ (𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ⇝ ((abs‘𝑥) · 𝐿)))
212	158, 162, 211	sylancl 598	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (((𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ↾ (ℤ≥‘𝑀)) ⇝ ((abs‘𝑥) · 𝐿) ↔ (𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ⇝ ((abs‘𝑥) · 𝐿)))
213	210, 212	mpbird 260	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → ((𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ↾ (ℤ≥‘𝑀)) ⇝ ((abs‘𝑥) · 𝐿))
214	157, 213	eqbrtrrd 5128	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (𝑛 ∈ 𝑍 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ⇝ ((abs‘𝑥) · 𝐿))
215	214	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) → (𝑛 ∈ 𝑍 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ⇝ ((abs‘𝑥) · 𝐿))
216		simpr 490	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) → ((abs‘𝑥) · 𝐿) ≠ 1)
217	110, 4, 111, 112, 132, 148, 153, 215, 216	cvgdvgrat 45297	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) → (((abs‘𝑥) · 𝐿) < 1 ↔ seq0( + , (𝐺‘𝑥)) ∈ dom ⇝ ))
218	109, 217	sylanl2 694	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℝ ∖ {0})) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) → (((abs‘𝑥) · 𝐿) < 1 ↔ seq0( + , (𝐺‘𝑥)) ∈ dom ⇝ ))
219		eldifi 4067	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ (ℝ ∖ {0}) → 𝑥 ∈ ℝ)
220		fveq2 6885	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑟 = 𝑥 → (𝐺‘𝑟) = (𝐺‘𝑥))
221	220	seqeq3d 14152	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑟 = 𝑥 → seq0( + , (𝐺‘𝑟)) = seq0( + , (𝐺‘𝑥)))
222	221	eleq1d 2845	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑟 = 𝑥 → (seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ ↔ seq0( + , (𝐺‘𝑥)) ∈ dom ⇝ ))
223	222	elrab3 3645	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ℝ → (𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ } ↔ seq0( + , (𝐺‘𝑥)) ∈ dom ⇝ ))
224	219, 223	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (ℝ ∖ {0}) → (𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ } ↔ seq0( + , (𝐺‘𝑥)) ∈ dom ⇝ ))
225	224	ad2antlr 740	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℝ ∖ {0})) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) → (𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ } ↔ seq0( + , (𝐺‘𝑥)) ∈ dom ⇝ ))
226	218, 225	bitr4d 285	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℝ ∖ {0})) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) → (((abs‘𝑥) · 𝐿) < 1 ↔ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
227	226	an32s 665	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ((abs‘𝑥) · 𝐿) ≠ 1) ∧ 𝑥 ∈ (ℝ ∖ {0})) → (((abs‘𝑥) · 𝐿) < 1 ↔ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
228	105, 227	jaodan 972	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ((abs‘𝑥) · 𝐿) ≠ 1) ∧ (𝑥 ∈ (ℝ ∩ {0}) ∨ 𝑥 ∈ (ℝ ∖ {0}))) → (((abs‘𝑥) · 𝐿) < 1 ↔ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
229	85, 228	sylan2br 607	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ((abs‘𝑥) · 𝐿) ≠ 1) ∧ 𝑥 ∈ ℝ) → (((abs‘𝑥) · 𝐿) < 1 ↔ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
230	229	an32s 665	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) → (((abs‘𝑥) · 𝐿) < 1 ↔ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
231	81, 230	bitr3d 284	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) → ((abs‘𝑥) < (1 / 𝐿) ↔ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
232	68, 231	syldan 603	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (abs‘𝑥) ≠ (1 / 𝐿)) → ((abs‘𝑥) < (1 / 𝐿) ↔ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
233	232	notbid 321	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (abs‘𝑥) ≠ (1 / 𝐿)) → (¬ (abs‘𝑥) < (1 / 𝐿) ↔ ¬ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
234	57, 233	bitrd 282	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (abs‘𝑥) ≠ (1 / 𝐿)) → ((1 / 𝐿) < (abs‘𝑥) ↔ ¬ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
235	234	biimpd 232	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (abs‘𝑥) ≠ (1 / 𝐿)) → ((1 / 𝐿) < (abs‘𝑥) → ¬ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
236	235	impancom 457	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (1 / 𝐿) < (abs‘𝑥)) → ((abs‘𝑥) ≠ (1 / 𝐿) → ¬ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
237	51, 236	mpd 16	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (1 / 𝐿) < (abs‘𝑥)) → ¬ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ })
238	237	ex 418	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((1 / 𝐿) < (abs‘𝑥) → ¬ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
239	238	con2d 135	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ } → ¬ (1 / 𝐿) < (abs‘𝑥)))
240	46	adantr 486	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (1 / 𝐿) < 𝑥) → (1 / 𝐿) ∈ ℝ)
241		simplr 781	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (1 / 𝐿) < 𝑥) → 𝑥 ∈ ℝ)
242	49	adantr 486	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (1 / 𝐿) < 𝑥) → (abs‘𝑥) ∈ ℝ)
243		simpr 490	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (1 / 𝐿) < 𝑥) → (1 / 𝐿) < 𝑥)
244	241	leabsd 15582	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (1 / 𝐿) < 𝑥) → 𝑥 ≤ (abs‘𝑥))
245	240, 241, 242, 243, 244	ltletrd 11470	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (1 / 𝐿) < 𝑥) → (1 / 𝐿) < (abs‘𝑥))
246	245	ex 418	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((1 / 𝐿) < 𝑥 → (1 / 𝐿) < (abs‘𝑥)))
247	239, 246	nsyld 157	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ } → ¬ (1 / 𝐿) < 𝑥))
248	45, 247	sylan2 605	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }) → (𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ } → ¬ (1 / 𝐿) < 𝑥))
249	44, 248	mpd 16	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }) → ¬ (1 / 𝐿) < 𝑥)
250	42	renegcld 11743	. . . . . . . . 9 ⊢ (𝜑 → -(1 / 𝐿) ∈ ℝ)
251	250	rexrd 11359	. . . . . . . 8 ⊢ (𝜑 → -(1 / 𝐿) ∈ ℝ*)
252		iooss1 13511	. . . . . . . 8 ⊢ (( -(1 / 𝐿) ∈ ℝ* ∧ -(1 / 𝐿) ≤ 𝑥) → (𝑥(,)(1 / 𝐿)) ⊆ ( -(1 / 𝐿)(,)(1 / 𝐿)))
253	251, 252	sylan 592	. . . . . . 7 ⊢ ((𝜑 ∧ -(1 / 𝐿) ≤ 𝑥) → (𝑥(,)(1 / 𝐿)) ⊆ ( -(1 / 𝐿)(,)(1 / 𝐿)))
254	253	adantlr 728	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑥 < (1 / 𝐿))) ∧ -(1 / 𝐿) ≤ 𝑥) → (𝑥(,)(1 / 𝐿)) ⊆ ( -(1 / 𝐿)(,)(1 / 𝐿)))
255		eliooord 13536	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (𝑥(,)(1 / 𝐿)) → (𝑥 < 𝑘 ∧ 𝑘 < (1 / 𝐿)))
256	255	simpld 500	. . . . . . . . . 10 ⊢ (𝑘 ∈ (𝑥(,)(1 / 𝐿)) → 𝑥 < 𝑘)
257	256	rgen 3078	. . . . . . . . 9 ⊢ ∀𝑘 ∈ (𝑥(,)(1 / 𝐿))𝑥 < 𝑘
258		ioon0 13502	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ* ∧ (1 / 𝐿) ∈ ℝ*) → ((𝑥(,)(1 / 𝐿)) ≠ ∅ ↔ 𝑥 < (1 / 𝐿)))
259	43, 258	sylan2 605	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ* ∧ 𝜑) → ((𝑥(,)(1 / 𝐿)) ≠ ∅ ↔ 𝑥 < (1 / 𝐿)))
260	259	ancoms 464	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ*) → ((𝑥(,)(1 / 𝐿)) ≠ ∅ ↔ 𝑥 < (1 / 𝐿)))
261	260	biimpar 483	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ 𝑥 < (1 / 𝐿)) → (𝑥(,)(1 / 𝐿)) ≠ ∅)
262		r19.2zb 4455	. . . . . . . . . 10 ⊢ ((𝑥(,)(1 / 𝐿)) ≠ ∅ ↔ (∀𝑘 ∈ (𝑥(,)(1 / 𝐿))𝑥 < 𝑘 → ∃𝑘 ∈ (𝑥(,)(1 / 𝐿))𝑥 < 𝑘))
263	261, 262	sylib 221	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ 𝑥 < (1 / 𝐿)) → (∀𝑘 ∈ (𝑥(,)(1 / 𝐿))𝑥 < 𝑘 → ∃𝑘 ∈ (𝑥(,)(1 / 𝐿))𝑥 < 𝑘))
264	257, 263	mpi 21	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ 𝑥 < (1 / 𝐿)) → ∃𝑘 ∈ (𝑥(,)(1 / 𝐿))𝑥 < 𝑘)
265	264	anasss 472	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑥 < (1 / 𝐿))) → ∃𝑘 ∈ (𝑥(,)(1 / 𝐿))𝑥 < 𝑘)
266	265	adantr 486	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑥 < (1 / 𝐿))) ∧ -(1 / 𝐿) ≤ 𝑥) → ∃𝑘 ∈ (𝑥(,)(1 / 𝐿))𝑥 < 𝑘)
267		ssrexv 3978	. . . . . 6 ⊢ ((𝑥(,)(1 / 𝐿)) ⊆ ( -(1 / 𝐿)(,)(1 / 𝐿)) → (∃𝑘 ∈ (𝑥(,)(1 / 𝐿))𝑥 < 𝑘 → ∃𝑘 ∈ ( -(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘))
268	254, 266, 267	sylc 66	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑥 < (1 / 𝐿))) ∧ -(1 / 𝐿) ≤ 𝑥) → ∃𝑘 ∈ ( -(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘)
269		simplr 781	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ ¬ -(1 / 𝐿) ≤ 𝑥) → 𝑥 ∈ ℝ*)
270		xrltnle 11376	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ* ∧ -(1 / 𝐿) ∈ ℝ*) → (𝑥 < -(1 / 𝐿) ↔ ¬ -(1 / 𝐿) ≤ 𝑥))
271		xrltle 13278	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ* ∧ -(1 / 𝐿) ∈ ℝ*) → (𝑥 < -(1 / 𝐿) → 𝑥 ≤ -(1 / 𝐿)))
272	270, 271	sylbird 263	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ* ∧ -(1 / 𝐿) ∈ ℝ*) → (¬ -(1 / 𝐿) ≤ 𝑥 → 𝑥 ≤ -(1 / 𝐿)))
273	251, 272	sylan2 605	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ* ∧ 𝜑) → (¬ -(1 / 𝐿) ≤ 𝑥 → 𝑥 ≤ -(1 / 𝐿)))
274	273	ancoms 464	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ*) → (¬ -(1 / 𝐿) ≤ 𝑥 → 𝑥 ≤ -(1 / 𝐿)))
275	274	imp 412	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ ¬ -(1 / 𝐿) ≤ 𝑥) → 𝑥 ≤ -(1 / 𝐿))
276		iooss1 13511	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ* ∧ 𝑥 ≤ -(1 / 𝐿)) → ( -(1 / 𝐿)(,)(1 / 𝐿)) ⊆ (𝑥(,)(1 / 𝐿)))
277	269, 275, 276	syl2anc 596	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ ¬ -(1 / 𝐿) ≤ 𝑥) → ( -(1 / 𝐿)(,)(1 / 𝐿)) ⊆ (𝑥(,)(1 / 𝐿)))
278	277	sselda 3908	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ ¬ -(1 / 𝐿) ≤ 𝑥) ∧ 𝑘 ∈ ( -(1 / 𝐿)(,)(1 / 𝐿))) → 𝑘 ∈ (𝑥(,)(1 / 𝐿)))
279	278, 256	syl 18	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ ¬ -(1 / 𝐿) ≤ 𝑥) ∧ 𝑘 ∈ ( -(1 / 𝐿)(,)(1 / 𝐿))) → 𝑥 < 𝑘)
280	279	ralrimiva 3154	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ ¬ -(1 / 𝐿) ≤ 𝑥) → ∀𝑘 ∈ ( -(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘)
281	40, 77	recgt0d 12251	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 < (1 / 𝐿))
282	42, 42, 281, 281	addgt0d 11891	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 < ((1 / 𝐿) + (1 / 𝐿)))
283	42	recnd 11337	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1 / 𝐿) ∈ ℂ)
284	283, 283	subnegd 11676	. . . . . . . . . . . 12 ⊢ (𝜑 → ((1 / 𝐿) − -(1 / 𝐿)) = ((1 / 𝐿) + (1 / 𝐿)))
285	282, 284	breqtrrd 5132	. . . . . . . . . . 11 ⊢ (𝜑 → 0 < ((1 / 𝐿) − -(1 / 𝐿)))
286	250, 42	posdifd 11903	. . . . . . . . . . 11 ⊢ (𝜑 → ( -(1 / 𝐿) < (1 / 𝐿) ↔ 0 < ((1 / 𝐿) − -(1 / 𝐿))))
287	285, 286	mpbird 260	. . . . . . . . . 10 ⊢ (𝜑 → -(1 / 𝐿) < (1 / 𝐿))
288		ioon0 13502	. . . . . . . . . . 11 ⊢ (( -(1 / 𝐿) ∈ ℝ* ∧ (1 / 𝐿) ∈ ℝ*) → (( -(1 / 𝐿)(,)(1 / 𝐿)) ≠ ∅ ↔ -(1 / 𝐿) < (1 / 𝐿)))
289	251, 43, 288	syl2anc 596	. . . . . . . . . 10 ⊢ (𝜑 → (( -(1 / 𝐿)(,)(1 / 𝐿)) ≠ ∅ ↔ -(1 / 𝐿) < (1 / 𝐿)))
290	287, 289	mpbird 260	. . . . . . . . 9 ⊢ (𝜑 → ( -(1 / 𝐿)(,)(1 / 𝐿)) ≠ ∅)
291		r19.2zb 4455	. . . . . . . . 9 ⊢ (( -(1 / 𝐿)(,)(1 / 𝐿)) ≠ ∅ ↔ (∀𝑘 ∈ ( -(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘 → ∃𝑘 ∈ ( -(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘))
292	290, 291	sylib 221	. . . . . . . 8 ⊢ (𝜑 → (∀𝑘 ∈ ( -(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘 → ∃𝑘 ∈ ( -(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘))
293	292	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ ¬ -(1 / 𝐿) ≤ 𝑥) → (∀𝑘 ∈ ( -(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘 → ∃𝑘 ∈ ( -(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘))
294	280, 293	mpd 16	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ ¬ -(1 / 𝐿) ≤ 𝑥) → ∃𝑘 ∈ ( -(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘)
295	294	adantlrr 734	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑥 < (1 / 𝐿))) ∧ ¬ -(1 / 𝐿) ≤ 𝑥) → ∃𝑘 ∈ ( -(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘)
296	268, 295	pm2.61dan 825	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑥 < (1 / 𝐿))) → ∃𝑘 ∈ ( -(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘)
297		elioo2 13517	. . . . . . . . . . 11 ⊢ (( -(1 / 𝐿) ∈ ℝ* ∧ (1 / 𝐿) ∈ ℝ*) → (𝑥 ∈ ( -(1 / 𝐿)(,)(1 / 𝐿)) ↔ (𝑥 ∈ ℝ ∧ -(1 / 𝐿) < 𝑥 ∧ 𝑥 < (1 / 𝐿))))
298	251, 43, 297	syl2anc 596	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ ( -(1 / 𝐿)(,)(1 / 𝐿)) ↔ (𝑥 ∈ ℝ ∧ -(1 / 𝐿) < 𝑥 ∧ 𝑥 < (1 / 𝐿))))
299	298	biimpa 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ( -(1 / 𝐿)(,)(1 / 𝐿))) → (𝑥 ∈ ℝ ∧ -(1 / 𝐿) < 𝑥 ∧ 𝑥 < (1 / 𝐿)))
300		simpr 490	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
301	300, 46	absltd 15599	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((abs‘𝑥) < (1 / 𝐿) ↔ ( -(1 / 𝐿) < 𝑥 ∧ 𝑥 < (1 / 𝐿))))
302	49	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (abs‘𝑥) < (1 / 𝐿)) → (abs‘𝑥) ∈ ℝ)
303		simpr 490	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (abs‘𝑥) < (1 / 𝐿)) → (abs‘𝑥) < (1 / 𝐿))
304	302, 303	ltned 11446	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (abs‘𝑥) < (1 / 𝐿)) → (abs‘𝑥) ≠ (1 / 𝐿))
305	232	biimpd 232	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (abs‘𝑥) ≠ (1 / 𝐿)) → ((abs‘𝑥) < (1 / 𝐿) → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
306	305	impancom 457	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (abs‘𝑥) < (1 / 𝐿)) → ((abs‘𝑥) ≠ (1 / 𝐿) → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
307	304, 306	mpd 16	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (abs‘𝑥) < (1 / 𝐿)) → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ })
308	307	ex 418	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((abs‘𝑥) < (1 / 𝐿) → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
309	301, 308	sylbird 263	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (( -(1 / 𝐿) < 𝑥 ∧ 𝑥 < (1 / 𝐿)) → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
310	309	impr 460	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ ( -(1 / 𝐿) < 𝑥 ∧ 𝑥 < (1 / 𝐿)))) → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ })
311	310	expcom 419	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ ∧ ( -(1 / 𝐿) < 𝑥 ∧ 𝑥 < (1 / 𝐿))) → (𝜑 → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
312	311	3impb 1132	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ ∧ -(1 / 𝐿) < 𝑥 ∧ 𝑥 < (1 / 𝐿)) → (𝜑 → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
313	312	impcom 413	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ -(1 / 𝐿) < 𝑥 ∧ 𝑥 < (1 / 𝐿))) → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ })
314	299, 313	syldan 603	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ( -(1 / 𝐿)(,)(1 / 𝐿))) → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ })
315	314	ex 418	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ ( -(1 / 𝐿)(,)(1 / 𝐿)) → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
316	315	ssrdv 3914	. . . . . 6 ⊢ (𝜑 → ( -(1 / 𝐿)(,)(1 / 𝐿)) ⊆ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ })
317		ssrexv 3978	. . . . . 6 ⊢ (( -(1 / 𝐿)(,)(1 / 𝐿)) ⊆ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ } → (∃𝑘 ∈ ( -(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘 → ∃𝑘 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }𝑥 < 𝑘))
318	316, 317	syl 18	. . . . 5 ⊢ (𝜑 → (∃𝑘 ∈ ( -(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘 → ∃𝑘 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }𝑥 < 𝑘))
319	318	adantr 486	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑥 < (1 / 𝐿))) → (∃𝑘 ∈ ( -(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘 → ∃𝑘 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }𝑥 < 𝑘))
320	296, 319	mpd 16	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑥 < (1 / 𝐿))) → ∃𝑘 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }𝑥 < 𝑘)
321	3, 43, 249, 320	eqsupd 9449	. 2 ⊢ (𝜑 → sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) = (1 / 𝐿))
322	1, 321	eqtrid 2807	1 ⊢ (𝜑 → 𝑅 = (1 / 𝐿))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   ∧ w3a 1103   = wceq 1569   ∈ wcel 2144   ≠ wne 2955  ∀wral 3076  ∃wrex 3086  {crab 3412  Vcvv 3450   ⊆ wss 3895   ∖ cdif 4045   ∩ cin 4089   ∪ cun 4149  ∅c0 4278  {csn 4583   class class class wbr 5102   ↦ cmpt 5185   Or wor 5557  dom cdm 5650   ↾ cres 5652  ⟶wf 6534  ‘cfv 6538  (class class class)co 7420  supcsup 9432  ℂcc 11198  ℝcr 11199  0cc0 11200  1c1 11201   + caddc 11203   · cmul 11205  ℝ^*cxr 11342   < clt 11343   ≤ cle 11344   − cmin 11541   -cneg 11542   / cdiv 11973  ℕ₀cn0 12606  ℤcz 12693  ℤ_≥cuz 12965  ℝ⁺crp 13120  (,)cioo 13476  seqcseq 14144  ↑cexp 14204  abscabs 15401   ⇝ cli 15651

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

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-int 4907  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-se 5604  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-isom 6547  df-riota 7377  df-ov 7423  df-oprab 7424  df-mpo 7425  df-om 7878  df-1st 8001  df-2nd 8002  df-frecs 8299  df-wrecs 8330  df-recs 8379  df-rdg 8418  df-1o 8476  df-er 8717  df-pm 8850  df-en 8974  df-dom 8975  df-sdom 8976  df-fin 8977  df-sup 9434  df-inf 9435  df-oi 9504  df-card 10020  df-pnf 11345  df-mnf 11346  df-xr 11347  df-ltxr 11348  df-le 11349  df-sub 11543  df-neg 11544  df-div 11974  df-nn 12336  df-2 12405  df-3 12406  df-n0 12607  df-z 12694  df-uz 12966  df-q 13076  df-rp 13121  df-ioo 13480  df-ico 13482  df-fz 13640  df-fzo 13789  df-fl 13932  df-seq 14145  df-exp 14205  df-hash 14475  df-shft 15220  df-cj 15266  df-re 15267  df-im 15268  df-sqrt 15402  df-abs 15403  df-limsup 15638  df-clim 15655  df-rlim 15656  df-sum 15854

This theorem is used by:  binomcxplemradcnv  45336