Theorem radcnvrat 44699

Description: Let 𝐿 be the limit, if one exists, of the ratio (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))) (as in the ratio test cvgdvgrat 44698) 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 44698 —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 13069	. . . 4 ⊢ < Or ℝ*
3	2	a1i 11	. . 3 ⊢ (𝜑 → < Or ℝ*)
4		radcnvrat.z	. . . . . 6 ⊢ 𝑍 = (ℤ≥‘𝑀)
5		radcnvrat.m	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ ℕ0)
6	5	nn0zd 12527	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℤ)
7	4	reseq2i 5945	. . . . . . 7 ⊢ (𝐷 ↾ 𝑍) = (𝐷 ↾ (ℤ≥‘𝑀))
8		radcnvrat.l	. . . . . . . 8 ⊢ (𝜑 → 𝐷 ⇝ 𝐿)
9		radcnvrat.rat	. . . . . . . . . 10 ⊢ 𝐷 = (𝑘 ∈ ℕ0 ↦ (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))))
10		nn0ex 12421	. . . . . . . . . . 11 ⊢ ℕ0 ∈ V
11	10	mptex 7181	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ0 ↦ (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)))) ∈ V
12	9, 11	eqeltri 2833	. . . . . . . . 9 ⊢ 𝐷 ∈ V
13		climres 15512	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝐷 ∈ V) → ((𝐷 ↾ (ℤ≥‘𝑀)) ⇝ 𝐿 ↔ 𝐷 ⇝ 𝐿))
14	6, 12, 13	sylancl 587	. . . . . . . 8 ⊢ (𝜑 → ((𝐷 ↾ (ℤ≥‘𝑀)) ⇝ 𝐿 ↔ 𝐷 ⇝ 𝐿))
15	8, 14	mpbird 257	. . . . . . 7 ⊢ (𝜑 → (𝐷 ↾ (ℤ≥‘𝑀)) ⇝ 𝐿)
16	7, 15	eqbrtrid 5135	. . . . . 6 ⊢ (𝜑 → (𝐷 ↾ 𝑍) ⇝ 𝐿)
17	9	reseq1i 5944	. . . . . . . . 9 ⊢ (𝐷 ↾ 𝑍) = ((𝑘 ∈ ℕ0 ↦ (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)))) ↾ 𝑍)
18		eluznn0 12844	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → 𝑘 ∈ ℕ0)
19	5, 18	sylan 581	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → 𝑘 ∈ ℕ0)
20	19	ex 412	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑘 ∈ (ℤ≥‘𝑀) → 𝑘 ∈ ℕ0))
21	20	ssrdv 3941	. . . . . . . . . . 11 ⊢ (𝜑 → (ℤ≥‘𝑀) ⊆ ℕ0)
22	4, 21	eqsstrid 3974	. . . . . . . . . 10 ⊢ (𝜑 → 𝑍 ⊆ ℕ0)
23	22	resmptd 6009	. . . . . . . . 9 ⊢ (𝜑 → ((𝑘 ∈ ℕ0 ↦ (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)))) ↾ 𝑍) = (𝑘 ∈ 𝑍 ↦ (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)))))
24	17, 23	eqtrid 2784	. . . . . . . 8 ⊢ (𝜑 → (𝐷 ↾ 𝑍) = (𝑘 ∈ 𝑍 ↦ (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)))))
25		fvexd 6859	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))) ∈ V)
26	24, 25	fvmpt2d 6965	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝐷 ↾ 𝑍)‘𝑘) = (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))))
27	4	peano2uzs 12829	. . . . . . . . . 10 ⊢ (𝑘 ∈ 𝑍 → (𝑘 + 1) ∈ 𝑍)
28	22	sselda 3935	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ 𝑍) → (𝑘 + 1) ∈ ℕ0)
29		radcnvrat.a	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)
30	29	ffvelcdmda 7040	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ ℕ0) → (𝐴‘(𝑘 + 1)) ∈ ℂ)
31	28, 30	syldan 592	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ 𝑍) → (𝐴‘(𝑘 + 1)) ∈ ℂ)
32	27, 31	sylan2 594	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐴‘(𝑘 + 1)) ∈ ℂ)
33	22	sselda 3935	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ ℕ0)
34	29	ffvelcdmda 7040	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐴‘𝑘) ∈ ℂ)
35	33, 34	syldan 592	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐴‘𝑘) ∈ ℂ)
36		radcnvrat.n0	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐴‘𝑘) ≠ 0)
37	32, 35, 36	divcld 11931	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)) ∈ ℂ)
38	37	abscld 15376	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))) ∈ ℝ)
39	26, 38	eqeltrd 2837	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝐷 ↾ 𝑍)‘𝑘) ∈ ℝ)
40	4, 6, 16, 39	climrecl 15520	. . . . 5 ⊢ (𝜑 → 𝐿 ∈ ℝ)
41		radcnvrat.ln0	. . . . 5 ⊢ (𝜑 → 𝐿 ≠ 0)
42	40, 41	rereccld 11982	. . . 4 ⊢ (𝜑 → (1 / 𝐿) ∈ ℝ)
43	42	rexrd 11196	. . 3 ⊢ (𝜑 → (1 / 𝐿) ∈ ℝ*)
44		simpr 484	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }) → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ })
45		elrabi 3644	. . . . 5 ⊢ (𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ } → 𝑥 ∈ ℝ)
46	42	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (1 / 𝐿) ∈ ℝ)
47		recn 11130	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
48	47	abscld 15376	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → (abs‘𝑥) ∈ ℝ)
49	48	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (abs‘𝑥) ∈ ℝ)
50	46, 49	ltlend 11292	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((1 / 𝐿) < (abs‘𝑥) ↔ ((1 / 𝐿) ≤ (abs‘𝑥) ∧ (abs‘𝑥) ≠ (1 / 𝐿))))
51	50	simplbda 499	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (1 / 𝐿) < (abs‘𝑥)) → (abs‘𝑥) ≠ (1 / 𝐿))
52	50	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (abs‘𝑥) ≠ (1 / 𝐿)) → ((1 / 𝐿) < (abs‘𝑥) ↔ ((1 / 𝐿) ≤ (abs‘𝑥) ∧ (abs‘𝑥) ≠ (1 / 𝐿))))
53		simpr 484	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (abs‘𝑥) ≠ (1 / 𝐿)) → (abs‘𝑥) ≠ (1 / 𝐿))
54	53	biantrud 531	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (abs‘𝑥) ≠ (1 / 𝐿)) → ((1 / 𝐿) ≤ (abs‘𝑥) ↔ ((1 / 𝐿) ≤ (abs‘𝑥) ∧ (abs‘𝑥) ≠ (1 / 𝐿))))
55	46, 49	lenltd 11293	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((1 / 𝐿) ≤ (abs‘𝑥) ↔ ¬ (abs‘𝑥) < (1 / 𝐿)))
56	55	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (abs‘𝑥) ≠ (1 / 𝐿)) → ((1 / 𝐿) ≤ (abs‘𝑥) ↔ ¬ (abs‘𝑥) < (1 / 𝐿)))
57	52, 54, 56	3bitr2d 307	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (abs‘𝑥) ≠ (1 / 𝐿)) → ((1 / 𝐿) < (abs‘𝑥) ↔ ¬ (abs‘𝑥) < (1 / 𝐿)))
58		1cnd 11141	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 1 ∈ ℂ)
59	49	recnd 11174	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (abs‘𝑥) ∈ ℂ)
60	40	recnd 11174	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐿 ∈ ℂ)
61	60	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐿 ∈ ℂ)
62	41	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐿 ≠ 0)
63	58, 59, 61, 62	divmul3d 11965	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((1 / 𝐿) = (abs‘𝑥) ↔ 1 = ((abs‘𝑥) · 𝐿)))
64		eqcom 2744	. . . . . . . . . . . . . . . . 17 ⊢ ((1 / 𝐿) = (abs‘𝑥) ↔ (abs‘𝑥) = (1 / 𝐿))
65		eqcom 2744	. . . . . . . . . . . . . . . . 17 ⊢ (1 = ((abs‘𝑥) · 𝐿) ↔ ((abs‘𝑥) · 𝐿) = 1)
66	63, 64, 65	3bitr3g 313	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((abs‘𝑥) = (1 / 𝐿) ↔ ((abs‘𝑥) · 𝐿) = 1))
67	66	necon3bid 2977	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((abs‘𝑥) ≠ (1 / 𝐿) ↔ ((abs‘𝑥) · 𝐿) ≠ 1))
68	67	biimpa 476	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (abs‘𝑥) ≠ (1 / 𝐿)) → ((abs‘𝑥) · 𝐿) ≠ 1)
69		1red 11147	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 1 ∈ ℝ)
70		fvres 6863	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 ∈ 𝑍 → ((𝐷 ↾ 𝑍)‘𝑘) = (𝐷‘𝑘))
71	70	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝐷 ↾ 𝑍)‘𝑘) = (𝐷‘𝑘))
72	71, 39	eqeltrrd 2838	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐷‘𝑘) ∈ ℝ)
73	37	absge0d 15384	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 0 ≤ (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))))
74	73, 26	breqtrrd 5128	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 0 ≤ ((𝐷 ↾ 𝑍)‘𝑘))
75	74, 71	breqtrd 5126	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 0 ≤ (𝐷‘𝑘))
76	4, 6, 8, 72, 75	climge0 15521	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 0 ≤ 𝐿)
77	40, 76, 41	ne0gt0d 11284	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 0 < 𝐿)
78	40, 77	elrpd 12960	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐿 ∈ ℝ+)
79	78	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐿 ∈ ℝ+)
80	49, 69, 79	ltmuldivd 13010	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((abs‘𝑥) · 𝐿) < 1 ↔ (abs‘𝑥) < (1 / 𝐿)))
81	80	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) → (((abs‘𝑥) · 𝐿) < 1 ↔ (abs‘𝑥) < (1 / 𝐿)))
82		elun 4107	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ((ℝ ∩ {0}) ∪ (ℝ ∖ {0})) ↔ (𝑥 ∈ (ℝ ∩ {0}) ∨ 𝑥 ∈ (ℝ ∖ {0})))
83		inundif 4433	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℝ ∩ {0}) ∪ (ℝ ∖ {0})) = ℝ
84	83	eleq2i 2829	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ((ℝ ∩ {0}) ∪ (ℝ ∖ {0})) ↔ 𝑥 ∈ ℝ)
85	82, 84	bitr3i 277	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ (ℝ ∩ {0}) ∨ 𝑥 ∈ (ℝ ∖ {0})) ↔ 𝑥 ∈ ℝ)
86		elin 3919	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ (ℝ ∩ {0}) ↔ (𝑥 ∈ ℝ ∧ 𝑥 ∈ {0}))
87	86	simprbi 497	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (ℝ ∩ {0}) → 𝑥 ∈ {0})
88		elsni 4599	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ {0} → 𝑥 = 0)
89	87, 88	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (ℝ ∩ {0}) → 𝑥 = 0)
90		fveq2 6844	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = 0 → (abs‘𝑥) = (abs‘0))
91		abs0 15222	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (abs‘0) = 0
92	90, 91	eqtrdi 2788	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 0 → (abs‘𝑥) = 0)
93	92	oveq1d 7385	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 0 → ((abs‘𝑥) · 𝐿) = (0 · 𝐿))
94	60	mul02d 11345	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (0 · 𝐿) = 0)
95	93, 94	sylan9eqr 2794	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 = 0) → ((abs‘𝑥) · 𝐿) = 0)
96		0lt1 11673	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 < 1
97	95, 96	eqbrtrdi 5139	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 = 0) → ((abs‘𝑥) · 𝐿) < 1)
98		radcnvrat.g	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))))
99	98, 29	radcnv0 26398	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 0 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ })
100		eleq1 2825	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 0 → (𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ } ↔ 0 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
101	99, 100	syl5ibrcom 247	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑥 = 0 → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
102	101	imp 406	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 = 0) → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ })
103	97, 102	2thd 265	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 = 0) → (((abs‘𝑥) · 𝐿) < 1 ↔ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
104	89, 103	sylan2 594	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∩ {0})) → (((abs‘𝑥) · 𝐿) < 1 ↔ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
105	104	adantlr 716	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ((abs‘𝑥) · 𝐿) ≠ 1) ∧ 𝑥 ∈ (ℝ ∩ {0})) → (((abs‘𝑥) · 𝐿) < 1 ↔ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
106		ax-resscn 11097	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ℝ ⊆ ℂ
107		ssdif 4098	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℝ ⊆ ℂ → (ℝ ∖ {0}) ⊆ (ℂ ∖ {0}))
108	106, 107	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (ℝ ∖ {0}) ⊆ (ℂ ∖ {0})
109	108	sseli 3931	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (ℝ ∖ {0}) → 𝑥 ∈ (ℂ ∖ {0}))
110		nn0uz 12803	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ℕ0 = (ℤ≥‘0)
111	5	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) → 𝑀 ∈ ℕ0)
112		fvexd 6859	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) → (𝐺‘𝑥) ∈ V)
113		eldifi 4085	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 ∈ (ℂ ∖ {0}) → 𝑥 ∈ ℂ)
114	98	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))))
115	10	mptex 7181	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))) ∈ V
116	115	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))) ∈ V)
117	114, 116	fvmpt2d 6965	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (𝐺‘𝑥) = (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))))
118	117	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑥) = (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))))
119		fveq2 6844	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑛 = 𝑘 → (𝐴‘𝑛) = (𝐴‘𝑘))
120		oveq2 7378	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑛 = 𝑘 → (𝑥↑𝑛) = (𝑥↑𝑘))
121	119, 120	oveq12d 7388	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑛 = 𝑘 → ((𝐴‘𝑛) · (𝑥↑𝑛)) = ((𝐴‘𝑘) · (𝑥↑𝑘)))
122	121	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) ∧ 𝑛 = 𝑘) → ((𝐴‘𝑛) · (𝑥↑𝑛)) = ((𝐴‘𝑘) · (𝑥↑𝑘)))
123		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ ℕ0)
124		ovexd 7405	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → ((𝐴‘𝑘) · (𝑥↑𝑘)) ∈ V)
125	118, 122, 123, 124	fvmptd 6959	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → ((𝐺‘𝑥)‘𝑘) = ((𝐴‘𝑘) · (𝑥↑𝑘)))
126	34	adantlr 716	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (𝐴‘𝑘) ∈ ℂ)
127		simplr 769	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → 𝑥 ∈ ℂ)
128	127, 123	expcld 14083	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (𝑥↑𝑘) ∈ ℂ)
129	126, 128	mulcld 11166	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → ((𝐴‘𝑘) · (𝑥↑𝑘)) ∈ ℂ)
130	125, 129	eqeltrd 2837	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → ((𝐺‘𝑥)‘𝑘) ∈ ℂ)
131	113, 130	sylanl2 682	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ ℕ0) → ((𝐺‘𝑥)‘𝑘) ∈ ℂ)
132	131	adantlr 716	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) ∧ 𝑘 ∈ ℕ0) → ((𝐺‘𝑥)‘𝑘) ∈ ℂ)
133	33	adantlr 716	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ ℕ0)
134	133, 125	syldan 592	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) → ((𝐺‘𝑥)‘𝑘) = ((𝐴‘𝑘) · (𝑥↑𝑘)))
135	113, 134	sylanl2 682	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → ((𝐺‘𝑥)‘𝑘) = ((𝐴‘𝑘) · (𝑥↑𝑘)))
136	35	adantlr 716	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝐴‘𝑘) ∈ ℂ)
137	113	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → 𝑥 ∈ ℂ)
138	137	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → 𝑥 ∈ ℂ)
139	33	adantlr 716	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ ℕ0)
140	138, 139	expcld 14083	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝑥↑𝑘) ∈ ℂ)
141	36	adantlr 716	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝐴‘𝑘) ≠ 0)
142		eldifsni 4748	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 ∈ (ℂ ∖ {0}) → 𝑥 ≠ 0)
143	142	ad2antlr 728	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → 𝑥 ≠ 0)
144	139	nn0zd 12527	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ ℤ)
145	138, 143, 144	expne0d 14089	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝑥↑𝑘) ≠ 0)
146	136, 140, 141, 145	mulne0d 11803	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → ((𝐴‘𝑘) · (𝑥↑𝑘)) ≠ 0)
147	135, 146	eqnetrd 3000	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → ((𝐺‘𝑥)‘𝑘) ≠ 0)
148	147	adantlr 716	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) ∧ 𝑘 ∈ 𝑍) → ((𝐺‘𝑥)‘𝑘) ≠ 0)
149		fvoveq1 7393	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 = 𝑘 → ((𝐺‘𝑥)‘(𝑛 + 1)) = ((𝐺‘𝑥)‘(𝑘 + 1)))
150		fveq2 6844	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 = 𝑘 → ((𝐺‘𝑥)‘𝑛) = ((𝐺‘𝑥)‘𝑘))
151	149, 150	oveq12d 7388	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 𝑘 → (((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)) = (((𝐺‘𝑥)‘(𝑘 + 1)) / ((𝐺‘𝑥)‘𝑘)))
152	151	fveq2d 6848	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑘 → (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛))) = (abs‘(((𝐺‘𝑥)‘(𝑘 + 1)) / ((𝐺‘𝑥)‘𝑘))))
153	152	cbvmptv 5204	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ 𝑍 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) = (𝑘 ∈ 𝑍 ↦ (abs‘(((𝐺‘𝑥)‘(𝑘 + 1)) / ((𝐺‘𝑥)‘𝑘))))
154	4	reseq2i 5945	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ↾ 𝑍) = ((𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ↾ (ℤ≥‘𝑀))
155	22	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → 𝑍 ⊆ ℕ0)
156	155	resmptd 6009	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → ((𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ↾ 𝑍) = (𝑛 ∈ 𝑍 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))))
157	154, 156	eqtr3id 2786	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → ((𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ↾ (ℤ≥‘𝑀)) = (𝑛 ∈ 𝑍 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))))
158	6	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → 𝑀 ∈ ℤ)
159	8	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → 𝐷 ⇝ 𝐿)
160	137	abscld 15376	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (abs‘𝑥) ∈ ℝ)
161	160	recnd 11174	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (abs‘𝑥) ∈ ℂ)
162	10	mptex 7181	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ∈ V
163	162	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ∈ V)
164	72	recnd 11174	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐷‘𝑘) ∈ ℂ)
165	164	adantlr 716	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝐷‘𝑘) ∈ ℂ)
166		eqidd 2738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) = (𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))))
167	152	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) ∧ 𝑛 = 𝑘) → (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛))) = (abs‘(((𝐺‘𝑥)‘(𝑘 + 1)) / ((𝐺‘𝑥)‘𝑘))))
168		fvexd 6859	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (abs‘(((𝐺‘𝑥)‘(𝑘 + 1)) / ((𝐺‘𝑥)‘𝑘))) ∈ V)
169	166, 167, 139, 168	fvmptd 6959	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → ((𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛))))‘𝑘) = (abs‘(((𝐺‘𝑥)‘(𝑘 + 1)) / ((𝐺‘𝑥)‘𝑘))))
170	117	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑥) = (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))))
171		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) ∧ 𝑛 = (𝑘 + 1)) → 𝑛 = (𝑘 + 1))
172	171	fveq2d 6848	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) ∧ 𝑛 = (𝑘 + 1)) → (𝐴‘𝑛) = (𝐴‘(𝑘 + 1)))
173	171	oveq2d 7386	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) ∧ 𝑛 = (𝑘 + 1)) → (𝑥↑𝑛) = (𝑥↑(𝑘 + 1)))
174	172, 173	oveq12d 7388	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) ∧ 𝑛 = (𝑘 + 1)) → ((𝐴‘𝑛) · (𝑥↑𝑛)) = ((𝐴‘(𝑘 + 1)) · (𝑥↑(𝑘 + 1))))
175		1nn0 12431	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ 1 ∈ ℕ0
176	175	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) → 1 ∈ ℕ0)
177	133, 176	nn0addcld 12480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) → (𝑘 + 1) ∈ ℕ0)
178		ovexd 7405	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) → ((𝐴‘(𝑘 + 1)) · (𝑥↑(𝑘 + 1))) ∈ V)
179	170, 174, 177, 178	fvmptd 6959	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) → ((𝐺‘𝑥)‘(𝑘 + 1)) = ((𝐴‘(𝑘 + 1)) · (𝑥↑(𝑘 + 1))))
180	121	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) ∧ 𝑛 = 𝑘) → ((𝐴‘𝑛) · (𝑥↑𝑛)) = ((𝐴‘𝑘) · (𝑥↑𝑘)))
181		ovexd 7405	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) → ((𝐴‘𝑘) · (𝑥↑𝑘)) ∈ V)
182	170, 180, 133, 181	fvmptd 6959	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) → ((𝐺‘𝑥)‘𝑘) = ((𝐴‘𝑘) · (𝑥↑𝑘)))
183	179, 182	oveq12d 7388	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) → (((𝐺‘𝑥)‘(𝑘 + 1)) / ((𝐺‘𝑥)‘𝑘)) = (((𝐴‘(𝑘 + 1)) · (𝑥↑(𝑘 + 1))) / ((𝐴‘𝑘) · (𝑥↑𝑘))))
184	113, 183	sylanl2 682	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (((𝐺‘𝑥)‘(𝑘 + 1)) / ((𝐺‘𝑥)‘𝑘)) = (((𝐴‘(𝑘 + 1)) · (𝑥↑(𝑘 + 1))) / ((𝐴‘𝑘) · (𝑥↑𝑘))))
185	32	adantlr 716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝐴‘(𝑘 + 1)) ∈ ℂ)
186	113, 177	sylanl2 682	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝑘 + 1) ∈ ℕ0)
187	138, 186	expcld 14083	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝑥↑(𝑘 + 1)) ∈ ℂ)
188	185, 136, 187, 140, 141, 145	divmuldivd 11972	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)) · ((𝑥↑(𝑘 + 1)) / (𝑥↑𝑘))) = (((𝐴‘(𝑘 + 1)) · (𝑥↑(𝑘 + 1))) / ((𝐴‘𝑘) · (𝑥↑𝑘))))
189	139	nn0cnd 12478	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ ℂ)
190		1cnd 11141	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → 1 ∈ ℂ)
191	189, 190	pncan2d 11508	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → ((𝑘 + 1) − 𝑘) = 1)
192	191	oveq2d 7386	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝑥↑((𝑘 + 1) − 𝑘)) = (𝑥↑1))
193	186	nn0zd 12527	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝑘 + 1) ∈ ℤ)
194	138, 143, 144, 193	expsubd 14094	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝑥↑((𝑘 + 1) − 𝑘)) = ((𝑥↑(𝑘 + 1)) / (𝑥↑𝑘)))
195	138	exp1d 14078	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝑥↑1) = 𝑥)
196	192, 194, 195	3eqtr3d 2780	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → ((𝑥↑(𝑘 + 1)) / (𝑥↑𝑘)) = 𝑥)
197	196	oveq2d 7386	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)) · ((𝑥↑(𝑘 + 1)) / (𝑥↑𝑘))) = (((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)) · 𝑥))
198	184, 188, 197	3eqtr2d 2778	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (((𝐺‘𝑥)‘(𝑘 + 1)) / ((𝐺‘𝑥)‘𝑘)) = (((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)) · 𝑥))
199	198	fveq2d 6848	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (abs‘(((𝐺‘𝑥)‘(𝑘 + 1)) / ((𝐺‘𝑥)‘𝑘))) = (abs‘(((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)) · 𝑥)))
200	37	adantlr 716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → ((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)) ∈ ℂ)
201	200, 138	absmuld 15394	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (abs‘(((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)) · 𝑥)) = ((abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))) · (abs‘𝑥)))
202	169, 199, 201	3eqtrd 2776	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → ((𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛))))‘𝑘) = ((abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))) · (abs‘𝑥)))
203	71, 26	eqtr3d 2774	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐷‘𝑘) = (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))))
204	203	adantlr 716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝐷‘𝑘) = (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))))
205	204	eqcomd 2743	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))) = (𝐷‘𝑘))
206	205	oveq1d 7385	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → ((abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))) · (abs‘𝑥)) = ((𝐷‘𝑘) · (abs‘𝑥)))
207	161	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (abs‘𝑥) ∈ ℂ)
208	165, 207	mulcomd 11167	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → ((𝐷‘𝑘) · (abs‘𝑥)) = ((abs‘𝑥) · (𝐷‘𝑘)))
209	202, 206, 208	3eqtrd 2776	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → ((𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛))))‘𝑘) = ((abs‘𝑥) · (𝐷‘𝑘)))
210	4, 158, 159, 161, 163, 165, 209	climmulc2 15574	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ⇝ ((abs‘𝑥) · 𝐿))
211		climres 15512	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑀 ∈ ℤ ∧ (𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ∈ V) → (((𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ↾ (ℤ≥‘𝑀)) ⇝ ((abs‘𝑥) · 𝐿) ↔ (𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ⇝ ((abs‘𝑥) · 𝐿)))
212	158, 162, 211	sylancl 587	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (((𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ↾ (ℤ≥‘𝑀)) ⇝ ((abs‘𝑥) · 𝐿) ↔ (𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ⇝ ((abs‘𝑥) · 𝐿)))
213	210, 212	mpbird 257	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → ((𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ↾ (ℤ≥‘𝑀)) ⇝ ((abs‘𝑥) · 𝐿))
214	157, 213	eqbrtrrd 5124	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (𝑛 ∈ 𝑍 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ⇝ ((abs‘𝑥) · 𝐿))
215	214	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) → (𝑛 ∈ 𝑍 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ⇝ ((abs‘𝑥) · 𝐿))
216		simpr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) → ((abs‘𝑥) · 𝐿) ≠ 1)
217	110, 4, 111, 112, 132, 148, 153, 215, 216	cvgdvgrat 44698	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) → (((abs‘𝑥) · 𝐿) < 1 ↔ seq0( + , (𝐺‘𝑥)) ∈ dom ⇝ ))
218	109, 217	sylanl2 682	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℝ ∖ {0})) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) → (((abs‘𝑥) · 𝐿) < 1 ↔ seq0( + , (𝐺‘𝑥)) ∈ dom ⇝ ))
219		eldifi 4085	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ (ℝ ∖ {0}) → 𝑥 ∈ ℝ)
220		fveq2 6844	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑟 = 𝑥 → (𝐺‘𝑟) = (𝐺‘𝑥))
221	220	seqeq3d 13946	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑟 = 𝑥 → seq0( + , (𝐺‘𝑟)) = seq0( + , (𝐺‘𝑥)))
222	221	eleq1d 2822	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑟 = 𝑥 → (seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ ↔ seq0( + , (𝐺‘𝑥)) ∈ dom ⇝ ))
223	222	elrab3 3649	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ℝ → (𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ } ↔ seq0( + , (𝐺‘𝑥)) ∈ dom ⇝ ))
224	219, 223	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (ℝ ∖ {0}) → (𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ } ↔ seq0( + , (𝐺‘𝑥)) ∈ dom ⇝ ))
225	224	ad2antlr 728	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℝ ∖ {0})) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) → (𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ } ↔ seq0( + , (𝐺‘𝑥)) ∈ dom ⇝ ))
226	218, 225	bitr4d 282	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℝ ∖ {0})) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) → (((abs‘𝑥) · 𝐿) < 1 ↔ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
227	226	an32s 653	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ((abs‘𝑥) · 𝐿) ≠ 1) ∧ 𝑥 ∈ (ℝ ∖ {0})) → (((abs‘𝑥) · 𝐿) < 1 ↔ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
228	105, 227	jaodan 960	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ((abs‘𝑥) · 𝐿) ≠ 1) ∧ (𝑥 ∈ (ℝ ∩ {0}) ∨ 𝑥 ∈ (ℝ ∖ {0}))) → (((abs‘𝑥) · 𝐿) < 1 ↔ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
229	85, 228	sylan2br 596	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ((abs‘𝑥) · 𝐿) ≠ 1) ∧ 𝑥 ∈ ℝ) → (((abs‘𝑥) · 𝐿) < 1 ↔ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
230	229	an32s 653	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) → (((abs‘𝑥) · 𝐿) < 1 ↔ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
231	81, 230	bitr3d 281	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) → ((abs‘𝑥) < (1 / 𝐿) ↔ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
232	68, 231	syldan 592	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (abs‘𝑥) ≠ (1 / 𝐿)) → ((abs‘𝑥) < (1 / 𝐿) ↔ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
233	232	notbid 318	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (abs‘𝑥) ≠ (1 / 𝐿)) → (¬ (abs‘𝑥) < (1 / 𝐿) ↔ ¬ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
234	57, 233	bitrd 279	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (abs‘𝑥) ≠ (1 / 𝐿)) → ((1 / 𝐿) < (abs‘𝑥) ↔ ¬ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
235	234	biimpd 229	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (abs‘𝑥) ≠ (1 / 𝐿)) → ((1 / 𝐿) < (abs‘𝑥) → ¬ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
236	235	impancom 451	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (1 / 𝐿) < (abs‘𝑥)) → ((abs‘𝑥) ≠ (1 / 𝐿) → ¬ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
237	51, 236	mpd 15	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (1 / 𝐿) < (abs‘𝑥)) → ¬ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ })
238	237	ex 412	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((1 / 𝐿) < (abs‘𝑥) → ¬ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
239	238	con2d 134	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ } → ¬ (1 / 𝐿) < (abs‘𝑥)))
240	46	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (1 / 𝐿) < 𝑥) → (1 / 𝐿) ∈ ℝ)
241		simplr 769	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (1 / 𝐿) < 𝑥) → 𝑥 ∈ ℝ)
242	49	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (1 / 𝐿) < 𝑥) → (abs‘𝑥) ∈ ℝ)
243		simpr 484	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (1 / 𝐿) < 𝑥) → (1 / 𝐿) < 𝑥)
244	241	leabsd 15352	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (1 / 𝐿) < 𝑥) → 𝑥 ≤ (abs‘𝑥))
245	240, 241, 242, 243, 244	ltletrd 11307	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (1 / 𝐿) < 𝑥) → (1 / 𝐿) < (abs‘𝑥))
246	245	ex 412	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((1 / 𝐿) < 𝑥 → (1 / 𝐿) < (abs‘𝑥)))
247	239, 246	nsyld 156	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ } → ¬ (1 / 𝐿) < 𝑥))
248	45, 247	sylan2 594	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }) → (𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ } → ¬ (1 / 𝐿) < 𝑥))
249	44, 248	mpd 15	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }) → ¬ (1 / 𝐿) < 𝑥)
250	42	renegcld 11578	. . . . . . . . 9 ⊢ (𝜑 → -(1 / 𝐿) ∈ ℝ)
251	250	rexrd 11196	. . . . . . . 8 ⊢ (𝜑 → -(1 / 𝐿) ∈ ℝ*)
252		iooss1 13310	. . . . . . . 8 ⊢ ((-(1 / 𝐿) ∈ ℝ* ∧ -(1 / 𝐿) ≤ 𝑥) → (𝑥(,)(1 / 𝐿)) ⊆ (-(1 / 𝐿)(,)(1 / 𝐿)))
253	251, 252	sylan 581	. . . . . . 7 ⊢ ((𝜑 ∧ -(1 / 𝐿) ≤ 𝑥) → (𝑥(,)(1 / 𝐿)) ⊆ (-(1 / 𝐿)(,)(1 / 𝐿)))
254	253	adantlr 716	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑥 < (1 / 𝐿))) ∧ -(1 / 𝐿) ≤ 𝑥) → (𝑥(,)(1 / 𝐿)) ⊆ (-(1 / 𝐿)(,)(1 / 𝐿)))
255		eliooord 13335	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (𝑥(,)(1 / 𝐿)) → (𝑥 < 𝑘 ∧ 𝑘 < (1 / 𝐿)))
256	255	simpld 494	. . . . . . . . . 10 ⊢ (𝑘 ∈ (𝑥(,)(1 / 𝐿)) → 𝑥 < 𝑘)
257	256	rgen 3054	. . . . . . . . 9 ⊢ ∀𝑘 ∈ (𝑥(,)(1 / 𝐿))𝑥 < 𝑘
258		ioon0 13301	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ* ∧ (1 / 𝐿) ∈ ℝ*) → ((𝑥(,)(1 / 𝐿)) ≠ ∅ ↔ 𝑥 < (1 / 𝐿)))
259	43, 258	sylan2 594	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ* ∧ 𝜑) → ((𝑥(,)(1 / 𝐿)) ≠ ∅ ↔ 𝑥 < (1 / 𝐿)))
260	259	ancoms 458	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ*) → ((𝑥(,)(1 / 𝐿)) ≠ ∅ ↔ 𝑥 < (1 / 𝐿)))
261	260	biimpar 477	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ 𝑥 < (1 / 𝐿)) → (𝑥(,)(1 / 𝐿)) ≠ ∅)
262		r19.2zb 4455	. . . . . . . . . 10 ⊢ ((𝑥(,)(1 / 𝐿)) ≠ ∅ ↔ (∀𝑘 ∈ (𝑥(,)(1 / 𝐿))𝑥 < 𝑘 → ∃𝑘 ∈ (𝑥(,)(1 / 𝐿))𝑥 < 𝑘))
263	261, 262	sylib 218	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ 𝑥 < (1 / 𝐿)) → (∀𝑘 ∈ (𝑥(,)(1 / 𝐿))𝑥 < 𝑘 → ∃𝑘 ∈ (𝑥(,)(1 / 𝐿))𝑥 < 𝑘))
264	257, 263	mpi 20	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ 𝑥 < (1 / 𝐿)) → ∃𝑘 ∈ (𝑥(,)(1 / 𝐿))𝑥 < 𝑘)
265	264	anasss 466	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑥 < (1 / 𝐿))) → ∃𝑘 ∈ (𝑥(,)(1 / 𝐿))𝑥 < 𝑘)
266	265	adantr 480	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑥 < (1 / 𝐿))) ∧ -(1 / 𝐿) ≤ 𝑥) → ∃𝑘 ∈ (𝑥(,)(1 / 𝐿))𝑥 < 𝑘)
267		ssrexv 4005	. . . . . 6 ⊢ ((𝑥(,)(1 / 𝐿)) ⊆ (-(1 / 𝐿)(,)(1 / 𝐿)) → (∃𝑘 ∈ (𝑥(,)(1 / 𝐿))𝑥 < 𝑘 → ∃𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘))
268	254, 266, 267	sylc 65	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑥 < (1 / 𝐿))) ∧ -(1 / 𝐿) ≤ 𝑥) → ∃𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘)
269		simplr 769	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ ¬ -(1 / 𝐿) ≤ 𝑥) → 𝑥 ∈ ℝ*)
270		xrltnle 11213	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ* ∧ -(1 / 𝐿) ∈ ℝ*) → (𝑥 < -(1 / 𝐿) ↔ ¬ -(1 / 𝐿) ≤ 𝑥))
271		xrltle 13077	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ* ∧ -(1 / 𝐿) ∈ ℝ*) → (𝑥 < -(1 / 𝐿) → 𝑥 ≤ -(1 / 𝐿)))
272	270, 271	sylbird 260	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ* ∧ -(1 / 𝐿) ∈ ℝ*) → (¬ -(1 / 𝐿) ≤ 𝑥 → 𝑥 ≤ -(1 / 𝐿)))
273	251, 272	sylan2 594	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ* ∧ 𝜑) → (¬ -(1 / 𝐿) ≤ 𝑥 → 𝑥 ≤ -(1 / 𝐿)))
274	273	ancoms 458	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ*) → (¬ -(1 / 𝐿) ≤ 𝑥 → 𝑥 ≤ -(1 / 𝐿)))
275	274	imp 406	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ ¬ -(1 / 𝐿) ≤ 𝑥) → 𝑥 ≤ -(1 / 𝐿))
276		iooss1 13310	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ* ∧ 𝑥 ≤ -(1 / 𝐿)) → (-(1 / 𝐿)(,)(1 / 𝐿)) ⊆ (𝑥(,)(1 / 𝐿)))
277	269, 275, 276	syl2anc 585	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ ¬ -(1 / 𝐿) ≤ 𝑥) → (-(1 / 𝐿)(,)(1 / 𝐿)) ⊆ (𝑥(,)(1 / 𝐿)))
278	277	sselda 3935	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ ¬ -(1 / 𝐿) ≤ 𝑥) ∧ 𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))) → 𝑘 ∈ (𝑥(,)(1 / 𝐿)))
279	278, 256	syl 17	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ ¬ -(1 / 𝐿) ≤ 𝑥) ∧ 𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))) → 𝑥 < 𝑘)
280	279	ralrimiva 3130	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ ¬ -(1 / 𝐿) ≤ 𝑥) → ∀𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘)
281	40, 77	recgt0d 12090	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 < (1 / 𝐿))
282	42, 42, 281, 281	addgt0d 11726	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 < ((1 / 𝐿) + (1 / 𝐿)))
283	42	recnd 11174	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1 / 𝐿) ∈ ℂ)
284	283, 283	subnegd 11513	. . . . . . . . . . . 12 ⊢ (𝜑 → ((1 / 𝐿) − -(1 / 𝐿)) = ((1 / 𝐿) + (1 / 𝐿)))
285	282, 284	breqtrrd 5128	. . . . . . . . . . 11 ⊢ (𝜑 → 0 < ((1 / 𝐿) − -(1 / 𝐿)))
286	250, 42	posdifd 11738	. . . . . . . . . . 11 ⊢ (𝜑 → (-(1 / 𝐿) < (1 / 𝐿) ↔ 0 < ((1 / 𝐿) − -(1 / 𝐿))))
287	285, 286	mpbird 257	. . . . . . . . . 10 ⊢ (𝜑 → -(1 / 𝐿) < (1 / 𝐿))
288		ioon0 13301	. . . . . . . . . . 11 ⊢ ((-(1 / 𝐿) ∈ ℝ* ∧ (1 / 𝐿) ∈ ℝ*) → ((-(1 / 𝐿)(,)(1 / 𝐿)) ≠ ∅ ↔ -(1 / 𝐿) < (1 / 𝐿)))
289	251, 43, 288	syl2anc 585	. . . . . . . . . 10 ⊢ (𝜑 → ((-(1 / 𝐿)(,)(1 / 𝐿)) ≠ ∅ ↔ -(1 / 𝐿) < (1 / 𝐿)))
290	287, 289	mpbird 257	. . . . . . . . 9 ⊢ (𝜑 → (-(1 / 𝐿)(,)(1 / 𝐿)) ≠ ∅)
291		r19.2zb 4455	. . . . . . . . 9 ⊢ ((-(1 / 𝐿)(,)(1 / 𝐿)) ≠ ∅ ↔ (∀𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘 → ∃𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘))
292	290, 291	sylib 218	. . . . . . . 8 ⊢ (𝜑 → (∀𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘 → ∃𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘))
293	292	ad2antrr 727	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ ¬ -(1 / 𝐿) ≤ 𝑥) → (∀𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘 → ∃𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘))
294	280, 293	mpd 15	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ ¬ -(1 / 𝐿) ≤ 𝑥) → ∃𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘)
295	294	adantlrr 722	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑥 < (1 / 𝐿))) ∧ ¬ -(1 / 𝐿) ≤ 𝑥) → ∃𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘)
296	268, 295	pm2.61dan 813	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑥 < (1 / 𝐿))) → ∃𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘)
297		elioo2 13316	. . . . . . . . . . 11 ⊢ ((-(1 / 𝐿) ∈ ℝ* ∧ (1 / 𝐿) ∈ ℝ*) → (𝑥 ∈ (-(1 / 𝐿)(,)(1 / 𝐿)) ↔ (𝑥 ∈ ℝ ∧ -(1 / 𝐿) < 𝑥 ∧ 𝑥 < (1 / 𝐿))))
298	251, 43, 297	syl2anc 585	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ (-(1 / 𝐿)(,)(1 / 𝐿)) ↔ (𝑥 ∈ ℝ ∧ -(1 / 𝐿) < 𝑥 ∧ 𝑥 < (1 / 𝐿))))
299	298	biimpa 476	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))) → (𝑥 ∈ ℝ ∧ -(1 / 𝐿) < 𝑥 ∧ 𝑥 < (1 / 𝐿)))
300		simpr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
301	300, 46	absltd 15369	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((abs‘𝑥) < (1 / 𝐿) ↔ (-(1 / 𝐿) < 𝑥 ∧ 𝑥 < (1 / 𝐿))))
302	49	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (abs‘𝑥) < (1 / 𝐿)) → (abs‘𝑥) ∈ ℝ)
303		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (abs‘𝑥) < (1 / 𝐿)) → (abs‘𝑥) < (1 / 𝐿))
304	302, 303	ltned 11283	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (abs‘𝑥) < (1 / 𝐿)) → (abs‘𝑥) ≠ (1 / 𝐿))
305	232	biimpd 229	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (abs‘𝑥) ≠ (1 / 𝐿)) → ((abs‘𝑥) < (1 / 𝐿) → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
306	305	impancom 451	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (abs‘𝑥) < (1 / 𝐿)) → ((abs‘𝑥) ≠ (1 / 𝐿) → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
307	304, 306	mpd 15	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (abs‘𝑥) < (1 / 𝐿)) → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ })
308	307	ex 412	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((abs‘𝑥) < (1 / 𝐿) → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
309	301, 308	sylbird 260	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((-(1 / 𝐿) < 𝑥 ∧ 𝑥 < (1 / 𝐿)) → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
310	309	impr 454	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ (-(1 / 𝐿) < 𝑥 ∧ 𝑥 < (1 / 𝐿)))) → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ })
311	310	expcom 413	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ ∧ (-(1 / 𝐿) < 𝑥 ∧ 𝑥 < (1 / 𝐿))) → (𝜑 → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
312	311	3impb 1115	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ ∧ -(1 / 𝐿) < 𝑥 ∧ 𝑥 < (1 / 𝐿)) → (𝜑 → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
313	312	impcom 407	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ -(1 / 𝐿) < 𝑥 ∧ 𝑥 < (1 / 𝐿))) → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ })
314	299, 313	syldan 592	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))) → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ })
315	314	ex 412	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (-(1 / 𝐿)(,)(1 / 𝐿)) → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
316	315	ssrdv 3941	. . . . . 6 ⊢ (𝜑 → (-(1 / 𝐿)(,)(1 / 𝐿)) ⊆ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ })
317		ssrexv 4005	. . . . . 6 ⊢ ((-(1 / 𝐿)(,)(1 / 𝐿)) ⊆ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ } → (∃𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘 → ∃𝑘 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }𝑥 < 𝑘))
318	316, 317	syl 17	. . . . 5 ⊢ (𝜑 → (∃𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘 → ∃𝑘 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }𝑥 < 𝑘))
319	318	adantr 480	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑥 < (1 / 𝐿))) → (∃𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘 → ∃𝑘 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }𝑥 < 𝑘))
320	296, 319	mpd 15	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑥 < (1 / 𝐿))) → ∃𝑘 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }𝑥 < 𝑘)
321	3, 43, 249, 320	eqsupd 9374	. 2 ⊢ (𝜑 → sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) = (1 / 𝐿))
322	1, 321	eqtrid 2784	1 ⊢ (𝜑 → 𝑅 = (1 / 𝐿))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 848   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114   ≠ wne 2933  ∀wral 3052  ∃wrex 3062  {crab 3401  Vcvv 3442   ∖ cdif 3900   ∪ cun 3901   ∩ cin 3902   ⊆ wss 3903  ∅c0 4287  {csn 4582   class class class wbr 5100   ↦ cmpt 5181   Or wor 5541  dom cdm 5634   ↾ cres 5636  ⟶wf 6498  ‘cfv 6502  (class class class)co 7370  supcsup 9357  ℂcc 11038  ℝcr 11039  0cc0 11040  1c1 11041   + caddc 11043   · cmul 11045  ℝ^*cxr 11179   < clt 11180   ≤ cle 11181   − cmin 11378  -cneg 11379   / cdiv 11808  ℕ₀cn0 12415  ℤcz 12502  ℤ_≥cuz 12765  ℝ⁺crp 12919  (,)cioo 13275  seqcseq 13938  ↑cexp 13998  abscabs 15171   ⇝ cli 15421

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5226  ax-sep 5245  ax-nul 5255  ax-pow 5314  ax-pr 5381  ax-un 7692  ax-inf2 9564  ax-cnex 11096  ax-resscn 11097  ax-1cn 11098  ax-icn 11099  ax-addcl 11100  ax-addrcl 11101  ax-mulcl 11102  ax-mulrcl 11103  ax-mulcom 11104  ax-addass 11105  ax-mulass 11106  ax-distr 11107  ax-i2m1 11108  ax-1ne0 11109  ax-1rid 11110  ax-rnegex 11111  ax-rrecex 11112  ax-cnre 11113  ax-pre-lttri 11114  ax-pre-lttrn 11115  ax-pre-ltadd 11116  ax-pre-mulgt0 11117  ax-pre-sup 11118

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rmo 3352  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-int 4905  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5529  df-eprel 5534  df-po 5542  df-so 5543  df-fr 5587  df-se 5588  df-we 5589  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6269  df-ord 6330  df-on 6331  df-lim 6332  df-suc 6333  df-iota 6458  df-fun 6504  df-fn 6505  df-f 6506  df-f1 6507  df-fo 6508  df-f1o 6509  df-fv 6510  df-isom 6511  df-riota 7327  df-ov 7373  df-oprab 7374  df-mpo 7375  df-om 7821  df-1st 7945  df-2nd 7946  df-frecs 8235  df-wrecs 8266  df-recs 8315  df-rdg 8353  df-1o 8409  df-er 8647  df-pm 8780  df-en 8898  df-dom 8899  df-sdom 8900  df-fin 8901  df-sup 9359  df-inf 9360  df-oi 9429  df-card 9865  df-pnf 11182  df-mnf 11183  df-xr 11184  df-ltxr 11185  df-le 11186  df-sub 11380  df-neg 11381  df-div 11809  df-nn 12160  df-2 12222  df-3 12223  df-n0 12416  df-z 12503  df-uz 12766  df-q 12876  df-rp 12920  df-ioo 13279  df-ico 13281  df-fz 13438  df-fzo 13585  df-fl 13726  df-seq 13939  df-exp 13999  df-hash 14268  df-shft 15004  df-cj 15036  df-re 15037  df-im 15038  df-sqrt 15172  df-abs 15173  df-limsup 15408  df-clim 15425  df-rlim 15426  df-sum 15624

This theorem is referenced by:  binomcxplemradcnv  44737