Theorem radcnvrat 45052

Description: Let 𝐿 be the limit, if one exists, of the ratio (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))) (as in the ratio test cvgdvgrat 45051) 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 45051 —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 13172	. . . 4 ⊢ < Or ℝ*
3	2	a1i 11	. . 3 ⊢ (𝜑 → < Or ℝ*)
4		radcnvrat.z	. . . . . 6 ⊢ 𝑍 = (ℤ≥‘𝑀)
5		radcnvrat.m	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ ℕ0)
6	5	nn0zd 12622	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℤ)
7	4	reseq2i 5974	. . . . . . 7 ⊢ (𝐷 ↾ 𝑍) = (𝐷 ↾ (ℤ≥‘𝑀))
8		radcnvrat.l	. . . . . . . 8 ⊢ (𝜑 → 𝐷 ⇝ 𝐿)
9		radcnvrat.rat	. . . . . . . . . 10 ⊢ 𝐷 = (𝑘 ∈ ℕ0 ↦ (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))))
10		nn0ex 12516	. . . . . . . . . . 11 ⊢ ℕ0 ∈ V
11	10	mptex 7221	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ0 ↦ (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)))) ∈ V
12	9, 11	eqeltri 2858	. . . . . . . . 9 ⊢ 𝐷 ∈ V
13		climres 15633	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝐷 ∈ V) → ((𝐷 ↾ (ℤ≥‘𝑀)) ⇝ 𝐿 ↔ 𝐷 ⇝ 𝐿))
14	6, 12, 13	sylancl 597	. . . . . . . 8 ⊢ (𝜑 → ((𝐷 ↾ (ℤ≥‘𝑀)) ⇝ 𝐿 ↔ 𝐷 ⇝ 𝐿))
15	8, 14	mpbird 260	. . . . . . 7 ⊢ (𝜑 → (𝐷 ↾ (ℤ≥‘𝑀)) ⇝ 𝐿)
16	7, 15	eqbrtrid 5145	. . . . . 6 ⊢ (𝜑 → (𝐷 ↾ 𝑍) ⇝ 𝐿)
17	9	reseq1i 5973	. . . . . . . . 9 ⊢ (𝐷 ↾ 𝑍) = ((𝑘 ∈ ℕ0 ↦ (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)))) ↾ 𝑍)
18		eluznn0 12947	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → 𝑘 ∈ ℕ0)
19	5, 18	sylan 591	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → 𝑘 ∈ ℕ0)
20	19	ex 417	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑘 ∈ (ℤ≥‘𝑀) → 𝑘 ∈ ℕ0))
21	20	ssrdv 3942	. . . . . . . . . . 11 ⊢ (𝜑 → (ℤ≥‘𝑀) ⊆ ℕ0)
22	4, 21	eqsstrid 3974	. . . . . . . . . 10 ⊢ (𝜑 → 𝑍 ⊆ ℕ0)
23	22	resmptd 6041	. . . . . . . . 9 ⊢ (𝜑 → ((𝑘 ∈ ℕ0 ↦ (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)))) ↾ 𝑍) = (𝑘 ∈ 𝑍 ↦ (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)))))
24	17, 23	eqtrid 2809	. . . . . . . 8 ⊢ (𝜑 → (𝐷 ↾ 𝑍) = (𝑘 ∈ 𝑍 ↦ (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)))))
25		fvexd 6896	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))) ∈ V)
26	24, 25	fvmpt2d 7003	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝐷 ↾ 𝑍)‘𝑘) = (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))))
27	4	peano2uzs 12932	. . . . . . . . . 10 ⊢ (𝑘 ∈ 𝑍 → (𝑘 + 1) ∈ 𝑍)
28	22	sselda 3936	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ 𝑍) → (𝑘 + 1) ∈ ℕ0)
29		radcnvrat.a	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)
30	29	ffvelcdmda 7079	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ ℕ0) → (𝐴‘(𝑘 + 1)) ∈ ℂ)
31	28, 30	syldan 602	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ 𝑍) → (𝐴‘(𝑘 + 1)) ∈ ℂ)
32	27, 31	sylan2 604	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐴‘(𝑘 + 1)) ∈ ℂ)
33	22	sselda 3936	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ ℕ0)
34	29	ffvelcdmda 7079	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐴‘𝑘) ∈ ℂ)
35	33, 34	syldan 602	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐴‘𝑘) ∈ ℂ)
36		radcnvrat.n0	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐴‘𝑘) ≠ 0)
37	32, 35, 36	divcld 11997	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)) ∈ ℂ)
38	37	abscld 15497	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))) ∈ ℝ)
39	26, 38	eqeltrd 2862	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝐷 ↾ 𝑍)‘𝑘) ∈ ℝ)
40	4, 6, 16, 39	climrecl 15641	. . . . 5 ⊢ (𝜑 → 𝐿 ∈ ℝ)
41		radcnvrat.ln0	. . . . 5 ⊢ (𝜑 → 𝐿 ≠ 0)
42	40, 41	rereccld 12048	. . . 4 ⊢ (𝜑 → (1 / 𝐿) ∈ ℝ)
43	42	rexrd 11265	. . 3 ⊢ (𝜑 → (1 / 𝐿) ∈ ℝ*)
44		simpr 489	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }) → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ })
45		elrabi 3645	. . . . 5 ⊢ (𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ } → 𝑥 ∈ ℝ)
46	42	adantr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (1 / 𝐿) ∈ ℝ)
47		recn 11196	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
48	47	abscld 15497	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → (abs‘𝑥) ∈ ℝ)
49	48	adantl 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (abs‘𝑥) ∈ ℝ)
50	46, 49	ltlend 11361	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((1 / 𝐿) < (abs‘𝑥) ↔ ((1 / 𝐿) ≤ (abs‘𝑥) ∧ (abs‘𝑥) ≠ (1 / 𝐿))))
51	50	simplbda 504	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (1 / 𝐿) < (abs‘𝑥)) → (abs‘𝑥) ≠ (1 / 𝐿))
52	50	adantr 485	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (abs‘𝑥) ≠ (1 / 𝐿)) → ((1 / 𝐿) < (abs‘𝑥) ↔ ((1 / 𝐿) ≤ (abs‘𝑥) ∧ (abs‘𝑥) ≠ (1 / 𝐿))))
53		simpr 489	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (abs‘𝑥) ≠ (1 / 𝐿)) → (abs‘𝑥) ≠ (1 / 𝐿))
54	53	biantrud 540	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (abs‘𝑥) ≠ (1 / 𝐿)) → ((1 / 𝐿) ≤ (abs‘𝑥) ↔ ((1 / 𝐿) ≤ (abs‘𝑥) ∧ (abs‘𝑥) ≠ (1 / 𝐿))))
55	46, 49	lenltd 11362	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((1 / 𝐿) ≤ (abs‘𝑥) ↔ ¬ (abs‘𝑥) < (1 / 𝐿)))
56	55	adantr 485	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (abs‘𝑥) ≠ (1 / 𝐿)) → ((1 / 𝐿) ≤ (abs‘𝑥) ↔ ¬ (abs‘𝑥) < (1 / 𝐿)))
57	52, 54, 56	3bitr2d 310	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (abs‘𝑥) ≠ (1 / 𝐿)) → ((1 / 𝐿) < (abs‘𝑥) ↔ ¬ (abs‘𝑥) < (1 / 𝐿)))
58		1cnd 11208	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 1 ∈ ℂ)
59	49	recnd 11243	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (abs‘𝑥) ∈ ℂ)
60	40	recnd 11243	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐿 ∈ ℂ)
61	60	adantr 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐿 ∈ ℂ)
62	41	adantr 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐿 ≠ 0)
63	58, 59, 61, 62	divmul3d 12031	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((1 / 𝐿) = (abs‘𝑥) ↔ 1 = ((abs‘𝑥) · 𝐿)))
64		eqcom 2769	. . . . . . . . . . . . . . . . 17 ⊢ ((1 / 𝐿) = (abs‘𝑥) ↔ (abs‘𝑥) = (1 / 𝐿))
65		eqcom 2769	. . . . . . . . . . . . . . . . 17 ⊢ (1 = ((abs‘𝑥) · 𝐿) ↔ ((abs‘𝑥) · 𝐿) = 1)
66	63, 64, 65	3bitr3g 316	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((abs‘𝑥) = (1 / 𝐿) ↔ ((abs‘𝑥) · 𝐿) = 1))
67	66	necon3bid 3001	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((abs‘𝑥) ≠ (1 / 𝐿) ↔ ((abs‘𝑥) · 𝐿) ≠ 1))
68	67	biimpa 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (abs‘𝑥) ≠ (1 / 𝐿)) → ((abs‘𝑥) · 𝐿) ≠ 1)
69		1red 11215	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 1 ∈ ℝ)
70		fvres 6900	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 ∈ 𝑍 → ((𝐷 ↾ 𝑍)‘𝑘) = (𝐷‘𝑘))
71	70	adantl 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝐷 ↾ 𝑍)‘𝑘) = (𝐷‘𝑘))
72	71, 39	eqeltrrd 2863	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐷‘𝑘) ∈ ℝ)
73	37	absge0d 15505	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 0 ≤ (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))))
74	73, 26	breqtrrd 5138	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 0 ≤ ((𝐷 ↾ 𝑍)‘𝑘))
75	74, 71	breqtrd 5136	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 0 ≤ (𝐷‘𝑘))
76	4, 6, 8, 72, 75	climge0 15642	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 0 ≤ 𝐿)
77	40, 76, 41	ne0gt0d 11353	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 0 < 𝐿)
78	40, 77	elrpd 13063	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐿 ∈ ℝ+)
79	78	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐿 ∈ ℝ+)
80	49, 69, 79	ltmuldivd 13113	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((abs‘𝑥) · 𝐿) < 1 ↔ (abs‘𝑥) < (1 / 𝐿)))
81	80	adantr 485	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) → (((abs‘𝑥) · 𝐿) < 1 ↔ (abs‘𝑥) < (1 / 𝐿)))
82		elun 4106	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ((ℝ ∩ {0}) ∪ (ℝ ∖ {0})) ↔ (𝑥 ∈ (ℝ ∩ {0}) ∨ 𝑥 ∈ (ℝ ∖ {0})))
83		inundif 4439	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℝ ∩ {0}) ∪ (ℝ ∖ {0})) = ℝ
84	83	eleq2i 2854	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ((ℝ ∩ {0}) ∪ (ℝ ∖ {0})) ↔ 𝑥 ∈ ℝ)
85	82, 84	bitr3i 280	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ (ℝ ∩ {0}) ∨ 𝑥 ∈ (ℝ ∖ {0})) ↔ 𝑥 ∈ ℝ)
86		elin 3920	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ (ℝ ∩ {0}) ↔ (𝑥 ∈ ℝ ∧ 𝑥 ∈ {0}))
87	86	simprbi 502	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (ℝ ∩ {0}) → 𝑥 ∈ {0})
88		elsni 4605	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ {0} → 𝑥 = 0)
89	87, 88	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (ℝ ∩ {0}) → 𝑥 = 0)
90		fveq2 6881	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = 0 → (abs‘𝑥) = (abs‘0))
91		abs0 15343	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (abs‘0) = 0
92	90, 91	eqtrdi 2813	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 0 → (abs‘𝑥) = 0)
93	92	oveq1d 7427	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 0 → ((abs‘𝑥) · 𝐿) = (0 · 𝐿))
94	60	mul02d 11414	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (0 · 𝐿) = 0)
95	93, 94	sylan9eqr 2819	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 = 0) → ((abs‘𝑥) · 𝐿) = 0)
96		0lt1 11742	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 < 1
97	95, 96	eqbrtrdi 5149	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 = 0) → ((abs‘𝑥) · 𝐿) < 1)
98		radcnvrat.g	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))))
99	98, 29	radcnv0 26590	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 0 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ })
100		eleq1 2850	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 0 → (𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ } ↔ 0 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
101	99, 100	syl5ibrcom 250	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑥 = 0 → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
102	101	imp 411	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 = 0) → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ })
103	97, 102	2thd 268	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 = 0) → (((abs‘𝑥) · 𝐿) < 1 ↔ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
104	89, 103	sylan2 604	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∩ {0})) → (((abs‘𝑥) · 𝐿) < 1 ↔ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
105	104	adantlr 727	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ((abs‘𝑥) · 𝐿) ≠ 1) ∧ 𝑥 ∈ (ℝ ∩ {0})) → (((abs‘𝑥) · 𝐿) < 1 ↔ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
106		ax-resscn 11163	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ℝ ⊆ ℂ
107		ssdif 4097	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℝ ⊆ ℂ → (ℝ ∖ {0}) ⊆ (ℂ ∖ {0}))
108	106, 107	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (ℝ ∖ {0}) ⊆ (ℂ ∖ {0})
109	108	sseli 3932	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (ℝ ∖ {0}) → 𝑥 ∈ (ℂ ∖ {0}))
110		nn0uz 12906	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ℕ0 = (ℤ≥‘0)
111	5	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) → 𝑀 ∈ ℕ0)
112		fvexd 6896	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) → (𝐺‘𝑥) ∈ V)
113		eldifi 4084	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 ∈ (ℂ ∖ {0}) → 𝑥 ∈ ℂ)
114	98	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))))
115	10	mptex 7221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))) ∈ V
116	115	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))) ∈ V)
117	114, 116	fvmpt2d 7003	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (𝐺‘𝑥) = (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))))
118	117	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑥) = (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))))
119		fveq2 6881	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑛 = 𝑘 → (𝐴‘𝑛) = (𝐴‘𝑘))
120		oveq2 7420	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑛 = 𝑘 → (𝑥↑𝑛) = (𝑥↑𝑘))
121	119, 120	oveq12d 7430	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑛 = 𝑘 → ((𝐴‘𝑛) · (𝑥↑𝑛)) = ((𝐴‘𝑘) · (𝑥↑𝑘)))
122	121	adantl 486	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) ∧ 𝑛 = 𝑘) → ((𝐴‘𝑛) · (𝑥↑𝑛)) = ((𝐴‘𝑘) · (𝑥↑𝑘)))
123		simpr 489	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ ℕ0)
124		ovexd 7447	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → ((𝐴‘𝑘) · (𝑥↑𝑘)) ∈ V)
125	118, 122, 123, 124	fvmptd 6997	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → ((𝐺‘𝑥)‘𝑘) = ((𝐴‘𝑘) · (𝑥↑𝑘)))
126	34	adantlr 727	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (𝐴‘𝑘) ∈ ℂ)
127		simplr 780	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → 𝑥 ∈ ℂ)
128	127, 123	expcld 14189	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (𝑥↑𝑘) ∈ ℂ)
129	126, 128	mulcld 11235	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → ((𝐴‘𝑘) · (𝑥↑𝑘)) ∈ ℂ)
130	125, 129	eqeltrd 2862	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → ((𝐺‘𝑥)‘𝑘) ∈ ℂ)
131	113, 130	sylanl2 693	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ ℕ0) → ((𝐺‘𝑥)‘𝑘) ∈ ℂ)
132	131	adantlr 727	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) ∧ 𝑘 ∈ ℕ0) → ((𝐺‘𝑥)‘𝑘) ∈ ℂ)
133	33	adantlr 727	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ ℕ0)
134	133, 125	syldan 602	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) → ((𝐺‘𝑥)‘𝑘) = ((𝐴‘𝑘) · (𝑥↑𝑘)))
135	113, 134	sylanl2 693	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → ((𝐺‘𝑥)‘𝑘) = ((𝐴‘𝑘) · (𝑥↑𝑘)))
136	35	adantlr 727	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝐴‘𝑘) ∈ ℂ)
137	113	adantl 486	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → 𝑥 ∈ ℂ)
138	137	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → 𝑥 ∈ ℂ)
139	33	adantlr 727	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ ℕ0)
140	138, 139	expcld 14189	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝑥↑𝑘) ∈ ℂ)
141	36	adantlr 727	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝐴‘𝑘) ≠ 0)
142		eldifsni 4757	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 ∈ (ℂ ∖ {0}) → 𝑥 ≠ 0)
143	142	ad2antlr 739	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → 𝑥 ≠ 0)
144	139	nn0zd 12622	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ ℤ)
145	138, 143, 144	expne0d 14195	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝑥↑𝑘) ≠ 0)
146	136, 140, 141, 145	mulne0d 11872	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → ((𝐴‘𝑘) · (𝑥↑𝑘)) ≠ 0)
147	135, 146	eqnetrd 3024	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → ((𝐺‘𝑥)‘𝑘) ≠ 0)
148	147	adantlr 727	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) ∧ 𝑘 ∈ 𝑍) → ((𝐺‘𝑥)‘𝑘) ≠ 0)
149		fvoveq1 7435	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 = 𝑘 → ((𝐺‘𝑥)‘(𝑛 + 1)) = ((𝐺‘𝑥)‘(𝑘 + 1)))
150		fveq2 6881	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 = 𝑘 → ((𝐺‘𝑥)‘𝑛) = ((𝐺‘𝑥)‘𝑘))
151	149, 150	oveq12d 7430	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 𝑘 → (((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)) = (((𝐺‘𝑥)‘(𝑘 + 1)) / ((𝐺‘𝑥)‘𝑘)))
152	151	fveq2d 6885	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑘 → (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛))) = (abs‘(((𝐺‘𝑥)‘(𝑘 + 1)) / ((𝐺‘𝑥)‘𝑘))))
153	152	cbvmptv 5214	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ 𝑍 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) = (𝑘 ∈ 𝑍 ↦ (abs‘(((𝐺‘𝑥)‘(𝑘 + 1)) / ((𝐺‘𝑥)‘𝑘))))
154	4	reseq2i 5974	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ↾ 𝑍) = ((𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ↾ (ℤ≥‘𝑀))
155	22	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → 𝑍 ⊆ ℕ0)
156	155	resmptd 6041	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → ((𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ↾ 𝑍) = (𝑛 ∈ 𝑍 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))))
157	154, 156	eqtr3id 2811	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → ((𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ↾ (ℤ≥‘𝑀)) = (𝑛 ∈ 𝑍 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))))
158	6	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → 𝑀 ∈ ℤ)
159	8	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → 𝐷 ⇝ 𝐿)
160	137	abscld 15497	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (abs‘𝑥) ∈ ℝ)
161	160	recnd 11243	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (abs‘𝑥) ∈ ℂ)
162	10	mptex 7221	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ∈ V
163	162	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ∈ V)
164	72	recnd 11243	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐷‘𝑘) ∈ ℂ)
165	164	adantlr 727	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝐷‘𝑘) ∈ ℂ)
166		eqidd 2763	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) = (𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))))
167	152	adantl 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) ∧ 𝑛 = 𝑘) → (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛))) = (abs‘(((𝐺‘𝑥)‘(𝑘 + 1)) / ((𝐺‘𝑥)‘𝑘))))
168		fvexd 6896	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (abs‘(((𝐺‘𝑥)‘(𝑘 + 1)) / ((𝐺‘𝑥)‘𝑘))) ∈ V)
169	166, 167, 139, 168	fvmptd 6997	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → ((𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛))))‘𝑘) = (abs‘(((𝐺‘𝑥)‘(𝑘 + 1)) / ((𝐺‘𝑥)‘𝑘))))
170	117	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑥) = (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))))
171		simpr 489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) ∧ 𝑛 = (𝑘 + 1)) → 𝑛 = (𝑘 + 1))
172	171	fveq2d 6885	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) ∧ 𝑛 = (𝑘 + 1)) → (𝐴‘𝑛) = (𝐴‘(𝑘 + 1)))
173	171	oveq2d 7428	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) ∧ 𝑛 = (𝑘 + 1)) → (𝑥↑𝑛) = (𝑥↑(𝑘 + 1)))
174	172, 173	oveq12d 7430	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) ∧ 𝑛 = (𝑘 + 1)) → ((𝐴‘𝑛) · (𝑥↑𝑛)) = ((𝐴‘(𝑘 + 1)) · (𝑥↑(𝑘 + 1))))
175		1nn0 12526	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ 1 ∈ ℕ0
176	175	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) → 1 ∈ ℕ0)
177	133, 176	nn0addcld 12575	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) → (𝑘 + 1) ∈ ℕ0)
178		ovexd 7447	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) → ((𝐴‘(𝑘 + 1)) · (𝑥↑(𝑘 + 1))) ∈ V)
179	170, 174, 177, 178	fvmptd 6997	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) → ((𝐺‘𝑥)‘(𝑘 + 1)) = ((𝐴‘(𝑘 + 1)) · (𝑥↑(𝑘 + 1))))
180	121	adantl 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) ∧ 𝑛 = 𝑘) → ((𝐴‘𝑛) · (𝑥↑𝑛)) = ((𝐴‘𝑘) · (𝑥↑𝑘)))
181		ovexd 7447	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) → ((𝐴‘𝑘) · (𝑥↑𝑘)) ∈ V)
182	170, 180, 133, 181	fvmptd 6997	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) → ((𝐺‘𝑥)‘𝑘) = ((𝐴‘𝑘) · (𝑥↑𝑘)))
183	179, 182	oveq12d 7430	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) → (((𝐺‘𝑥)‘(𝑘 + 1)) / ((𝐺‘𝑥)‘𝑘)) = (((𝐴‘(𝑘 + 1)) · (𝑥↑(𝑘 + 1))) / ((𝐴‘𝑘) · (𝑥↑𝑘))))
184	113, 183	sylanl2 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (((𝐺‘𝑥)‘(𝑘 + 1)) / ((𝐺‘𝑥)‘𝑘)) = (((𝐴‘(𝑘 + 1)) · (𝑥↑(𝑘 + 1))) / ((𝐴‘𝑘) · (𝑥↑𝑘))))
185	32	adantlr 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝐴‘(𝑘 + 1)) ∈ ℂ)
186	113, 177	sylanl2 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝑘 + 1) ∈ ℕ0)
187	138, 186	expcld 14189	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝑥↑(𝑘 + 1)) ∈ ℂ)
188	185, 136, 187, 140, 141, 145	divmuldivd 12038	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)) · ((𝑥↑(𝑘 + 1)) / (𝑥↑𝑘))) = (((𝐴‘(𝑘 + 1)) · (𝑥↑(𝑘 + 1))) / ((𝐴‘𝑘) · (𝑥↑𝑘))))
189	139	nn0cnd 12573	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ ℂ)
190		1cnd 11208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → 1 ∈ ℂ)
191	189, 190	pncan2d 11577	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → ((𝑘 + 1) − 𝑘) = 1)
192	191	oveq2d 7428	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝑥↑((𝑘 + 1) − 𝑘)) = (𝑥↑1))
193	186	nn0zd 12622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝑘 + 1) ∈ ℤ)
194	138, 143, 144, 193	expsubd 14200	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝑥↑((𝑘 + 1) − 𝑘)) = ((𝑥↑(𝑘 + 1)) / (𝑥↑𝑘)))
195	138	exp1d 14184	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝑥↑1) = 𝑥)
196	192, 194, 195	3eqtr3d 2805	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → ((𝑥↑(𝑘 + 1)) / (𝑥↑𝑘)) = 𝑥)
197	196	oveq2d 7428	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)) · ((𝑥↑(𝑘 + 1)) / (𝑥↑𝑘))) = (((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)) · 𝑥))
198	184, 188, 197	3eqtr2d 2803	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (((𝐺‘𝑥)‘(𝑘 + 1)) / ((𝐺‘𝑥)‘𝑘)) = (((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)) · 𝑥))
199	198	fveq2d 6885	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (abs‘(((𝐺‘𝑥)‘(𝑘 + 1)) / ((𝐺‘𝑥)‘𝑘))) = (abs‘(((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)) · 𝑥)))
200	37	adantlr 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → ((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)) ∈ ℂ)
201	200, 138	absmuld 15515	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (abs‘(((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)) · 𝑥)) = ((abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))) · (abs‘𝑥)))
202	169, 199, 201	3eqtrd 2801	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → ((𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛))))‘𝑘) = ((abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))) · (abs‘𝑥)))
203	71, 26	eqtr3d 2799	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐷‘𝑘) = (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))))
204	203	adantlr 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝐷‘𝑘) = (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))))
205	204	eqcomd 2768	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))) = (𝐷‘𝑘))
206	205	oveq1d 7427	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → ((abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))) · (abs‘𝑥)) = ((𝐷‘𝑘) · (abs‘𝑥)))
207	161	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (abs‘𝑥) ∈ ℂ)
208	165, 207	mulcomd 11236	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → ((𝐷‘𝑘) · (abs‘𝑥)) = ((abs‘𝑥) · (𝐷‘𝑘)))
209	202, 206, 208	3eqtrd 2801	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → ((𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛))))‘𝑘) = ((abs‘𝑥) · (𝐷‘𝑘)))
210	4, 158, 159, 161, 163, 165, 209	climmulc2 15695	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ⇝ ((abs‘𝑥) · 𝐿))
211		climres 15633	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑀 ∈ ℤ ∧ (𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ∈ V) → (((𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ↾ (ℤ≥‘𝑀)) ⇝ ((abs‘𝑥) · 𝐿) ↔ (𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ⇝ ((abs‘𝑥) · 𝐿)))
212	158, 162, 211	sylancl 597	. . . . . . . . . . . . . . . . . . . . . . . . 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 5134	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (𝑛 ∈ 𝑍 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ⇝ ((abs‘𝑥) · 𝐿))
215	214	adantr 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) → (𝑛 ∈ 𝑍 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ⇝ ((abs‘𝑥) · 𝐿))
216		simpr 489	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) → ((abs‘𝑥) · 𝐿) ≠ 1)
217	110, 4, 111, 112, 132, 148, 153, 215, 216	cvgdvgrat 45051	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) → (((abs‘𝑥) · 𝐿) < 1 ↔ seq0( + , (𝐺‘𝑥)) ∈ dom ⇝ ))
218	109, 217	sylanl2 693	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℝ ∖ {0})) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) → (((abs‘𝑥) · 𝐿) < 1 ↔ seq0( + , (𝐺‘𝑥)) ∈ dom ⇝ ))
219		eldifi 4084	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ (ℝ ∖ {0}) → 𝑥 ∈ ℝ)
220		fveq2 6881	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑟 = 𝑥 → (𝐺‘𝑟) = (𝐺‘𝑥))
221	220	seqeq3d 14052	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑟 = 𝑥 → seq0( + , (𝐺‘𝑟)) = seq0( + , (𝐺‘𝑥)))
222	221	eleq1d 2847	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑟 = 𝑥 → (seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ ↔ seq0( + , (𝐺‘𝑥)) ∈ dom ⇝ ))
223	222	elrab3 3650	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ℝ → (𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ } ↔ seq0( + , (𝐺‘𝑥)) ∈ dom ⇝ ))
224	219, 223	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (ℝ ∖ {0}) → (𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ } ↔ seq0( + , (𝐺‘𝑥)) ∈ dom ⇝ ))
225	224	ad2antlr 739	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℝ ∖ {0})) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) → (𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ } ↔ seq0( + , (𝐺‘𝑥)) ∈ dom ⇝ ))
226	218, 225	bitr4d 285	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℝ ∖ {0})) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) → (((abs‘𝑥) · 𝐿) < 1 ↔ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
227	226	an32s 664	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ((abs‘𝑥) · 𝐿) ≠ 1) ∧ 𝑥 ∈ (ℝ ∖ {0})) → (((abs‘𝑥) · 𝐿) < 1 ↔ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
228	105, 227	jaodan 971	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ((abs‘𝑥) · 𝐿) ≠ 1) ∧ (𝑥 ∈ (ℝ ∩ {0}) ∨ 𝑥 ∈ (ℝ ∖ {0}))) → (((abs‘𝑥) · 𝐿) < 1 ↔ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
229	85, 228	sylan2br 606	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ((abs‘𝑥) · 𝐿) ≠ 1) ∧ 𝑥 ∈ ℝ) → (((abs‘𝑥) · 𝐿) < 1 ↔ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
230	229	an32s 664	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) → (((abs‘𝑥) · 𝐿) < 1 ↔ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
231	81, 230	bitr3d 284	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) → ((abs‘𝑥) < (1 / 𝐿) ↔ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
232	68, 231	syldan 602	. . . . . . . . . . . . 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 456	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (1 / 𝐿) < (abs‘𝑥)) → ((abs‘𝑥) ≠ (1 / 𝐿) → ¬ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
237	51, 236	mpd 16	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (1 / 𝐿) < (abs‘𝑥)) → ¬ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ })
238	237	ex 417	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((1 / 𝐿) < (abs‘𝑥) → ¬ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
239	238	con2d 135	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ } → ¬ (1 / 𝐿) < (abs‘𝑥)))
240	46	adantr 485	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (1 / 𝐿) < 𝑥) → (1 / 𝐿) ∈ ℝ)
241		simplr 780	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (1 / 𝐿) < 𝑥) → 𝑥 ∈ ℝ)
242	49	adantr 485	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (1 / 𝐿) < 𝑥) → (abs‘𝑥) ∈ ℝ)
243		simpr 489	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (1 / 𝐿) < 𝑥) → (1 / 𝐿) < 𝑥)
244	241	leabsd 15473	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (1 / 𝐿) < 𝑥) → 𝑥 ≤ (abs‘𝑥))
245	240, 241, 242, 243, 244	ltletrd 11376	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (1 / 𝐿) < 𝑥) → (1 / 𝐿) < (abs‘𝑥))
246	245	ex 417	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((1 / 𝐿) < 𝑥 → (1 / 𝐿) < (abs‘𝑥)))
247	239, 246	nsyld 157	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ } → ¬ (1 / 𝐿) < 𝑥))
248	45, 247	sylan2 604	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }) → (𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ } → ¬ (1 / 𝐿) < 𝑥))
249	44, 248	mpd 16	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }) → ¬ (1 / 𝐿) < 𝑥)
250	42	renegcld 11647	. . . . . . . . 9 ⊢ (𝜑 → -(1 / 𝐿) ∈ ℝ)
251	250	rexrd 11265	. . . . . . . 8 ⊢ (𝜑 → -(1 / 𝐿) ∈ ℝ*)
252		iooss1 13413	. . . . . . . 8 ⊢ ((-(1 / 𝐿) ∈ ℝ* ∧ -(1 / 𝐿) ≤ 𝑥) → (𝑥(,)(1 / 𝐿)) ⊆ (-(1 / 𝐿)(,)(1 / 𝐿)))
253	251, 252	sylan 591	. . . . . . 7 ⊢ ((𝜑 ∧ -(1 / 𝐿) ≤ 𝑥) → (𝑥(,)(1 / 𝐿)) ⊆ (-(1 / 𝐿)(,)(1 / 𝐿)))
254	253	adantlr 727	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑥 < (1 / 𝐿))) ∧ -(1 / 𝐿) ≤ 𝑥) → (𝑥(,)(1 / 𝐿)) ⊆ (-(1 / 𝐿)(,)(1 / 𝐿)))
255		eliooord 13438	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (𝑥(,)(1 / 𝐿)) → (𝑥 < 𝑘 ∧ 𝑘 < (1 / 𝐿)))
256	255	simpld 499	. . . . . . . . . 10 ⊢ (𝑘 ∈ (𝑥(,)(1 / 𝐿)) → 𝑥 < 𝑘)
257	256	rgen 3080	. . . . . . . . 9 ⊢ ∀𝑘 ∈ (𝑥(,)(1 / 𝐿))𝑥 < 𝑘
258		ioon0 13404	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ* ∧ (1 / 𝐿) ∈ ℝ*) → ((𝑥(,)(1 / 𝐿)) ≠ ∅ ↔ 𝑥 < (1 / 𝐿)))
259	43, 258	sylan2 604	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ* ∧ 𝜑) → ((𝑥(,)(1 / 𝐿)) ≠ ∅ ↔ 𝑥 < (1 / 𝐿)))
260	259	ancoms 463	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ*) → ((𝑥(,)(1 / 𝐿)) ≠ ∅ ↔ 𝑥 < (1 / 𝐿)))
261	260	biimpar 482	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ 𝑥 < (1 / 𝐿)) → (𝑥(,)(1 / 𝐿)) ≠ ∅)
262		r19.2zb 4460	. . . . . . . . . 10 ⊢ ((𝑥(,)(1 / 𝐿)) ≠ ∅ ↔ (∀𝑘 ∈ (𝑥(,)(1 / 𝐿))𝑥 < 𝑘 → ∃𝑘 ∈ (𝑥(,)(1 / 𝐿))𝑥 < 𝑘))
263	261, 262	sylib 221	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ 𝑥 < (1 / 𝐿)) → (∀𝑘 ∈ (𝑥(,)(1 / 𝐿))𝑥 < 𝑘 → ∃𝑘 ∈ (𝑥(,)(1 / 𝐿))𝑥 < 𝑘))
264	257, 263	mpi 21	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ 𝑥 < (1 / 𝐿)) → ∃𝑘 ∈ (𝑥(,)(1 / 𝐿))𝑥 < 𝑘)
265	264	anasss 471	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑥 < (1 / 𝐿))) → ∃𝑘 ∈ (𝑥(,)(1 / 𝐿))𝑥 < 𝑘)
266	265	adantr 485	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑥 < (1 / 𝐿))) ∧ -(1 / 𝐿) ≤ 𝑥) → ∃𝑘 ∈ (𝑥(,)(1 / 𝐿))𝑥 < 𝑘)
267		ssrexv 4006	. . . . . 6 ⊢ ((𝑥(,)(1 / 𝐿)) ⊆ (-(1 / 𝐿)(,)(1 / 𝐿)) → (∃𝑘 ∈ (𝑥(,)(1 / 𝐿))𝑥 < 𝑘 → ∃𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘))
268	254, 266, 267	sylc 66	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑥 < (1 / 𝐿))) ∧ -(1 / 𝐿) ≤ 𝑥) → ∃𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘)
269		simplr 780	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ ¬ -(1 / 𝐿) ≤ 𝑥) → 𝑥 ∈ ℝ*)
270		xrltnle 11282	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ* ∧ -(1 / 𝐿) ∈ ℝ*) → (𝑥 < -(1 / 𝐿) ↔ ¬ -(1 / 𝐿) ≤ 𝑥))
271		xrltle 13180	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ* ∧ -(1 / 𝐿) ∈ ℝ*) → (𝑥 < -(1 / 𝐿) → 𝑥 ≤ -(1 / 𝐿)))
272	270, 271	sylbird 263	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ* ∧ -(1 / 𝐿) ∈ ℝ*) → (¬ -(1 / 𝐿) ≤ 𝑥 → 𝑥 ≤ -(1 / 𝐿)))
273	251, 272	sylan2 604	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ* ∧ 𝜑) → (¬ -(1 / 𝐿) ≤ 𝑥 → 𝑥 ≤ -(1 / 𝐿)))
274	273	ancoms 463	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ*) → (¬ -(1 / 𝐿) ≤ 𝑥 → 𝑥 ≤ -(1 / 𝐿)))
275	274	imp 411	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ ¬ -(1 / 𝐿) ≤ 𝑥) → 𝑥 ≤ -(1 / 𝐿))
276		iooss1 13413	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ* ∧ 𝑥 ≤ -(1 / 𝐿)) → (-(1 / 𝐿)(,)(1 / 𝐿)) ⊆ (𝑥(,)(1 / 𝐿)))
277	269, 275, 276	syl2anc 595	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ ¬ -(1 / 𝐿) ≤ 𝑥) → (-(1 / 𝐿)(,)(1 / 𝐿)) ⊆ (𝑥(,)(1 / 𝐿)))
278	277	sselda 3936	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ ¬ -(1 / 𝐿) ≤ 𝑥) ∧ 𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))) → 𝑘 ∈ (𝑥(,)(1 / 𝐿)))
279	278, 256	syl 18	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ ¬ -(1 / 𝐿) ≤ 𝑥) ∧ 𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))) → 𝑥 < 𝑘)
280	279	ralrimiva 3156	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ ¬ -(1 / 𝐿) ≤ 𝑥) → ∀𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘)
281	40, 77	recgt0d 12155	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 < (1 / 𝐿))
282	42, 42, 281, 281	addgt0d 11795	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 < ((1 / 𝐿) + (1 / 𝐿)))
283	42	recnd 11243	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1 / 𝐿) ∈ ℂ)
284	283, 283	subnegd 11582	. . . . . . . . . . . 12 ⊢ (𝜑 → ((1 / 𝐿) − -(1 / 𝐿)) = ((1 / 𝐿) + (1 / 𝐿)))
285	282, 284	breqtrrd 5138	. . . . . . . . . . 11 ⊢ (𝜑 → 0 < ((1 / 𝐿) − -(1 / 𝐿)))
286	250, 42	posdifd 11807	. . . . . . . . . . 11 ⊢ (𝜑 → (-(1 / 𝐿) < (1 / 𝐿) ↔ 0 < ((1 / 𝐿) − -(1 / 𝐿))))
287	285, 286	mpbird 260	. . . . . . . . . 10 ⊢ (𝜑 → -(1 / 𝐿) < (1 / 𝐿))
288		ioon0 13404	. . . . . . . . . . 11 ⊢ ((-(1 / 𝐿) ∈ ℝ* ∧ (1 / 𝐿) ∈ ℝ*) → ((-(1 / 𝐿)(,)(1 / 𝐿)) ≠ ∅ ↔ -(1 / 𝐿) < (1 / 𝐿)))
289	251, 43, 288	syl2anc 595	. . . . . . . . . 10 ⊢ (𝜑 → ((-(1 / 𝐿)(,)(1 / 𝐿)) ≠ ∅ ↔ -(1 / 𝐿) < (1 / 𝐿)))
290	287, 289	mpbird 260	. . . . . . . . 9 ⊢ (𝜑 → (-(1 / 𝐿)(,)(1 / 𝐿)) ≠ ∅)
291		r19.2zb 4460	. . . . . . . . 9 ⊢ ((-(1 / 𝐿)(,)(1 / 𝐿)) ≠ ∅ ↔ (∀𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘 → ∃𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘))
292	290, 291	sylib 221	. . . . . . . 8 ⊢ (𝜑 → (∀𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘 → ∃𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘))
293	292	ad2antrr 738	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ ¬ -(1 / 𝐿) ≤ 𝑥) → (∀𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘 → ∃𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘))
294	280, 293	mpd 16	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ ¬ -(1 / 𝐿) ≤ 𝑥) → ∃𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘)
295	294	adantlrr 733	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑥 < (1 / 𝐿))) ∧ ¬ -(1 / 𝐿) ≤ 𝑥) → ∃𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘)
296	268, 295	pm2.61dan 824	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑥 < (1 / 𝐿))) → ∃𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘)
297		elioo2 13419	. . . . . . . . . . 11 ⊢ ((-(1 / 𝐿) ∈ ℝ* ∧ (1 / 𝐿) ∈ ℝ*) → (𝑥 ∈ (-(1 / 𝐿)(,)(1 / 𝐿)) ↔ (𝑥 ∈ ℝ ∧ -(1 / 𝐿) < 𝑥 ∧ 𝑥 < (1 / 𝐿))))
298	251, 43, 297	syl2anc 595	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ (-(1 / 𝐿)(,)(1 / 𝐿)) ↔ (𝑥 ∈ ℝ ∧ -(1 / 𝐿) < 𝑥 ∧ 𝑥 < (1 / 𝐿))))
299	298	biimpa 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))) → (𝑥 ∈ ℝ ∧ -(1 / 𝐿) < 𝑥 ∧ 𝑥 < (1 / 𝐿)))
300		simpr 489	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
301	300, 46	absltd 15490	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((abs‘𝑥) < (1 / 𝐿) ↔ (-(1 / 𝐿) < 𝑥 ∧ 𝑥 < (1 / 𝐿))))
302	49	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (abs‘𝑥) < (1 / 𝐿)) → (abs‘𝑥) ∈ ℝ)
303		simpr 489	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (abs‘𝑥) < (1 / 𝐿)) → (abs‘𝑥) < (1 / 𝐿))
304	302, 303	ltned 11352	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (abs‘𝑥) < (1 / 𝐿)) → (abs‘𝑥) ≠ (1 / 𝐿))
305	232	biimpd 232	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (abs‘𝑥) ≠ (1 / 𝐿)) → ((abs‘𝑥) < (1 / 𝐿) → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
306	305	impancom 456	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (abs‘𝑥) < (1 / 𝐿)) → ((abs‘𝑥) ≠ (1 / 𝐿) → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
307	304, 306	mpd 16	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (abs‘𝑥) < (1 / 𝐿)) → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ })
308	307	ex 417	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((abs‘𝑥) < (1 / 𝐿) → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
309	301, 308	sylbird 263	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((-(1 / 𝐿) < 𝑥 ∧ 𝑥 < (1 / 𝐿)) → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
310	309	impr 459	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ (-(1 / 𝐿) < 𝑥 ∧ 𝑥 < (1 / 𝐿)))) → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ })
311	310	expcom 418	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ ∧ (-(1 / 𝐿) < 𝑥 ∧ 𝑥 < (1 / 𝐿))) → (𝜑 → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
312	311	3impb 1131	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ ∧ -(1 / 𝐿) < 𝑥 ∧ 𝑥 < (1 / 𝐿)) → (𝜑 → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
313	312	impcom 412	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ -(1 / 𝐿) < 𝑥 ∧ 𝑥 < (1 / 𝐿))) → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ })
314	299, 313	syldan 602	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))) → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ })
315	314	ex 417	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (-(1 / 𝐿)(,)(1 / 𝐿)) → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
316	315	ssrdv 3942	. . . . . 6 ⊢ (𝜑 → (-(1 / 𝐿)(,)(1 / 𝐿)) ⊆ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ })
317		ssrexv 4006	. . . . . 6 ⊢ ((-(1 / 𝐿)(,)(1 / 𝐿)) ⊆ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ } → (∃𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘 → ∃𝑘 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }𝑥 < 𝑘))
318	316, 317	syl 18	. . . . 5 ⊢ (𝜑 → (∃𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘 → ∃𝑘 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }𝑥 < 𝑘))
319	318	adantr 485	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑥 < (1 / 𝐿))) → (∃𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘 → ∃𝑘 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }𝑥 < 𝑘))
320	296, 319	mpd 16	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑥 < (1 / 𝐿))) → ∃𝑘 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }𝑥 < 𝑘)
321	3, 43, 249, 320	eqsupd 9415	. 2 ⊢ (𝜑 → sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) = (1 / 𝐿))
322	1, 321	eqtrid 2809	1 ⊢ (𝜑 → 𝑅 = (1 / 𝐿))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∨ wo 860   ∧ w3a 1102   = wceq 1569   ∈ wcel 2142   ≠ wne 2957  ∀wral 3078  ∃wrex 3088  {crab 3415  Vcvv 3454   ∖ cdif 3901   ∪ cun 3902   ∩ cin 3903   ⊆ wss 3904  ∅c0 4285  {csn 4588   class class class wbr 5108   ↦ cmpt 5191   Or wor 5567  dom cdm 5660   ↾ cres 5662  ⟶wf 6532  ‘cfv 6536  (class class class)co 7412  supcsup 9398  ℂcc 11104  ℝcr 11105  0cc0 11106  1c1 11107   + caddc 11109   · cmul 11111  ℝ^*cxr 11248   < clt 11249   ≤ cle 11250   − cmin 11447  -cneg 11448   / cdiv 11877  ℕ₀cn0 12510  ℤcz 12597  ℤ_≥cuz 12868  ℝ⁺crp 13022  (,)cioo 13378  seqcseq 14044  ↑cexp 14104  abscabs 15292   ⇝ cli 15542

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-rep 5237  ax-sep 5256  ax-nul 5268  ax-pow 5335  ax-pr 5403  ax-un 7734  ax-inf2 9608  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183  ax-pre-sup 11184

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1103  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-nf 1813  df-sb 2096  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-rmo 3368  df-reu 3369  df-rab 3416  df-v 3456  df-sbc 3744  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4487  df-pw 4563  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-int 4912  df-iun 4957  df-br 5109  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5555  df-eprel 5560  df-po 5568  df-so 5569  df-fr 5613  df-se 5614  df-we 5615  df-xp 5666  df-rel 5667  df-cnv 5668  df-co 5669  df-dm 5670  df-rn 5671  df-res 5672  df-ima 5673  df-pred 6302  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-isom 6545  df-riota 7369  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7861  df-1st 7984  df-2nd 7985  df-frecs 8276  df-wrecs 8307  df-recs 8356  df-rdg 8395  df-1o 8451  df-er 8692  df-pm 8825  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-sup 9400  df-inf 9401  df-oi 9470  df-card 9932  df-pnf 11251  df-mnf 11252  df-xr 11253  df-ltxr 11254  df-le 11255  df-sub 11449  df-neg 11450  df-div 11878  df-nn 12240  df-2 12309  df-3 12310  df-n0 12511  df-z 12598  df-uz 12869  df-q 12979  df-rp 13023  df-ioo 13382  df-ico 13384  df-fz 13542  df-fzo 13690  df-fl 13832  df-seq 14045  df-exp 14105  df-hash 14374  df-shft 15111  df-cj 15157  df-re 15158  df-im 15159  df-sqrt 15293  df-abs 15294  df-limsup 15529  df-clim 15546  df-rlim 15547  df-sum 15745

This theorem is used by:  binomcxplemradcnv  45090