Theorem radcnvrat 44303

Description: Let 𝐿 be the limit, if one exists, of the ratio (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))) (as in the ratio test cvgdvgrat 44302) 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 44302 —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 13101	. . . 4 ⊢ < Or ℝ*
3	2	a1i 11	. . 3 ⊢ (𝜑 → < Or ℝ*)
4		radcnvrat.z	. . . . . 6 ⊢ 𝑍 = (ℤ≥‘𝑀)
5		radcnvrat.m	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ ℕ0)
6	5	nn0zd 12555	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℤ)
7	4	reseq2i 5947	. . . . . . 7 ⊢ (𝐷 ↾ 𝑍) = (𝐷 ↾ (ℤ≥‘𝑀))
8		radcnvrat.l	. . . . . . . 8 ⊢ (𝜑 → 𝐷 ⇝ 𝐿)
9		radcnvrat.rat	. . . . . . . . . 10 ⊢ 𝐷 = (𝑘 ∈ ℕ0 ↦ (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))))
10		nn0ex 12448	. . . . . . . . . . 11 ⊢ ℕ0 ∈ V
11	10	mptex 7197	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ0 ↦ (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)))) ∈ V
12	9, 11	eqeltri 2824	. . . . . . . . 9 ⊢ 𝐷 ∈ V
13		climres 15541	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝐷 ∈ V) → ((𝐷 ↾ (ℤ≥‘𝑀)) ⇝ 𝐿 ↔ 𝐷 ⇝ 𝐿))
14	6, 12, 13	sylancl 586	. . . . . . . 8 ⊢ (𝜑 → ((𝐷 ↾ (ℤ≥‘𝑀)) ⇝ 𝐿 ↔ 𝐷 ⇝ 𝐿))
15	8, 14	mpbird 257	. . . . . . 7 ⊢ (𝜑 → (𝐷 ↾ (ℤ≥‘𝑀)) ⇝ 𝐿)
16	7, 15	eqbrtrid 5142	. . . . . 6 ⊢ (𝜑 → (𝐷 ↾ 𝑍) ⇝ 𝐿)
17	9	reseq1i 5946	. . . . . . . . 9 ⊢ (𝐷 ↾ 𝑍) = ((𝑘 ∈ ℕ0 ↦ (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)))) ↾ 𝑍)
18		eluznn0 12876	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → 𝑘 ∈ ℕ0)
19	5, 18	sylan 580	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → 𝑘 ∈ ℕ0)
20	19	ex 412	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑘 ∈ (ℤ≥‘𝑀) → 𝑘 ∈ ℕ0))
21	20	ssrdv 3952	. . . . . . . . . . 11 ⊢ (𝜑 → (ℤ≥‘𝑀) ⊆ ℕ0)
22	4, 21	eqsstrid 3985	. . . . . . . . . 10 ⊢ (𝜑 → 𝑍 ⊆ ℕ0)
23	22	resmptd 6011	. . . . . . . . 9 ⊢ (𝜑 → ((𝑘 ∈ ℕ0 ↦ (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)))) ↾ 𝑍) = (𝑘 ∈ 𝑍 ↦ (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)))))
24	17, 23	eqtrid 2776	. . . . . . . 8 ⊢ (𝜑 → (𝐷 ↾ 𝑍) = (𝑘 ∈ 𝑍 ↦ (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)))))
25		fvexd 6873	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))) ∈ V)
26	24, 25	fvmpt2d 6981	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝐷 ↾ 𝑍)‘𝑘) = (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))))
27	4	peano2uzs 12861	. . . . . . . . . 10 ⊢ (𝑘 ∈ 𝑍 → (𝑘 + 1) ∈ 𝑍)
28	22	sselda 3946	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ 𝑍) → (𝑘 + 1) ∈ ℕ0)
29		radcnvrat.a	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)
30	29	ffvelcdmda 7056	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ ℕ0) → (𝐴‘(𝑘 + 1)) ∈ ℂ)
31	28, 30	syldan 591	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ 𝑍) → (𝐴‘(𝑘 + 1)) ∈ ℂ)
32	27, 31	sylan2 593	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐴‘(𝑘 + 1)) ∈ ℂ)
33	22	sselda 3946	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ ℕ0)
34	29	ffvelcdmda 7056	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐴‘𝑘) ∈ ℂ)
35	33, 34	syldan 591	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐴‘𝑘) ∈ ℂ)
36		radcnvrat.n0	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐴‘𝑘) ≠ 0)
37	32, 35, 36	divcld 11958	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)) ∈ ℂ)
38	37	abscld 15405	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))) ∈ ℝ)
39	26, 38	eqeltrd 2828	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝐷 ↾ 𝑍)‘𝑘) ∈ ℝ)
40	4, 6, 16, 39	climrecl 15549	. . . . 5 ⊢ (𝜑 → 𝐿 ∈ ℝ)
41		radcnvrat.ln0	. . . . 5 ⊢ (𝜑 → 𝐿 ≠ 0)
42	40, 41	rereccld 12009	. . . 4 ⊢ (𝜑 → (1 / 𝐿) ∈ ℝ)
43	42	rexrd 11224	. . 3 ⊢ (𝜑 → (1 / 𝐿) ∈ ℝ*)
44		simpr 484	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }) → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ })
45		elrabi 3654	. . . . 5 ⊢ (𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ } → 𝑥 ∈ ℝ)
46	42	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (1 / 𝐿) ∈ ℝ)
47		recn 11158	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
48	47	abscld 15405	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → (abs‘𝑥) ∈ ℝ)
49	48	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (abs‘𝑥) ∈ ℝ)
50	46, 49	ltlend 11319	. . . . . . . . . 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 11320	. . . . . . . . . . . . . 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 11169	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 1 ∈ ℂ)
59	49	recnd 11202	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (abs‘𝑥) ∈ ℂ)
60	40	recnd 11202	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐿 ∈ ℂ)
61	60	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐿 ∈ ℂ)
62	41	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐿 ≠ 0)
63	58, 59, 61, 62	divmul3d 11992	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((1 / 𝐿) = (abs‘𝑥) ↔ 1 = ((abs‘𝑥) · 𝐿)))
64		eqcom 2736	. . . . . . . . . . . . . . . . 17 ⊢ ((1 / 𝐿) = (abs‘𝑥) ↔ (abs‘𝑥) = (1 / 𝐿))
65		eqcom 2736	. . . . . . . . . . . . . . . . 17 ⊢ (1 = ((abs‘𝑥) · 𝐿) ↔ ((abs‘𝑥) · 𝐿) = 1)
66	63, 64, 65	3bitr3g 313	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((abs‘𝑥) = (1 / 𝐿) ↔ ((abs‘𝑥) · 𝐿) = 1))
67	66	necon3bid 2969	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((abs‘𝑥) ≠ (1 / 𝐿) ↔ ((abs‘𝑥) · 𝐿) ≠ 1))
68	67	biimpa 476	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (abs‘𝑥) ≠ (1 / 𝐿)) → ((abs‘𝑥) · 𝐿) ≠ 1)
69		1red 11175	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 1 ∈ ℝ)
70		fvres 6877	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 ∈ 𝑍 → ((𝐷 ↾ 𝑍)‘𝑘) = (𝐷‘𝑘))
71	70	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝐷 ↾ 𝑍)‘𝑘) = (𝐷‘𝑘))
72	71, 39	eqeltrrd 2829	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐷‘𝑘) ∈ ℝ)
73	37	absge0d 15413	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 0 ≤ (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))))
74	73, 26	breqtrrd 5135	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 0 ≤ ((𝐷 ↾ 𝑍)‘𝑘))
75	74, 71	breqtrd 5133	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 0 ≤ (𝐷‘𝑘))
76	4, 6, 8, 72, 75	climge0 15550	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 0 ≤ 𝐿)
77	40, 76, 41	ne0gt0d 11311	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 0 < 𝐿)
78	40, 77	elrpd 12992	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐿 ∈ ℝ+)
79	78	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐿 ∈ ℝ+)
80	49, 69, 79	ltmuldivd 13042	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((abs‘𝑥) · 𝐿) < 1 ↔ (abs‘𝑥) < (1 / 𝐿)))
81	80	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) → (((abs‘𝑥) · 𝐿) < 1 ↔ (abs‘𝑥) < (1 / 𝐿)))
82		elun 4116	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ((ℝ ∩ {0}) ∪ (ℝ ∖ {0})) ↔ (𝑥 ∈ (ℝ ∩ {0}) ∨ 𝑥 ∈ (ℝ ∖ {0})))
83		inundif 4442	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℝ ∩ {0}) ∪ (ℝ ∖ {0})) = ℝ
84	83	eleq2i 2820	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ((ℝ ∩ {0}) ∪ (ℝ ∖ {0})) ↔ 𝑥 ∈ ℝ)
85	82, 84	bitr3i 277	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ (ℝ ∩ {0}) ∨ 𝑥 ∈ (ℝ ∖ {0})) ↔ 𝑥 ∈ ℝ)
86		elin 3930	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ (ℝ ∩ {0}) ↔ (𝑥 ∈ ℝ ∧ 𝑥 ∈ {0}))
87	86	simprbi 496	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (ℝ ∩ {0}) → 𝑥 ∈ {0})
88		elsni 4606	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ {0} → 𝑥 = 0)
89	87, 88	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (ℝ ∩ {0}) → 𝑥 = 0)
90		fveq2 6858	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = 0 → (abs‘𝑥) = (abs‘0))
91		abs0 15251	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (abs‘0) = 0
92	90, 91	eqtrdi 2780	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 0 → (abs‘𝑥) = 0)
93	92	oveq1d 7402	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 0 → ((abs‘𝑥) · 𝐿) = (0 · 𝐿))
94	60	mul02d 11372	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (0 · 𝐿) = 0)
95	93, 94	sylan9eqr 2786	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 = 0) → ((abs‘𝑥) · 𝐿) = 0)
96		0lt1 11700	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 < 1
97	95, 96	eqbrtrdi 5146	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 = 0) → ((abs‘𝑥) · 𝐿) < 1)
98		radcnvrat.g	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))))
99	98, 29	radcnv0 26325	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 0 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ })
100		eleq1 2816	. . . . . . . . . . . . . . . . . . . . . . 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 593	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∩ {0})) → (((abs‘𝑥) · 𝐿) < 1 ↔ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
105	104	adantlr 715	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ((abs‘𝑥) · 𝐿) ≠ 1) ∧ 𝑥 ∈ (ℝ ∩ {0})) → (((abs‘𝑥) · 𝐿) < 1 ↔ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
106		ax-resscn 11125	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ℝ ⊆ ℂ
107		ssdif 4107	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℝ ⊆ ℂ → (ℝ ∖ {0}) ⊆ (ℂ ∖ {0}))
108	106, 107	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (ℝ ∖ {0}) ⊆ (ℂ ∖ {0})
109	108	sseli 3942	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (ℝ ∖ {0}) → 𝑥 ∈ (ℂ ∖ {0}))
110		nn0uz 12835	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ℕ0 = (ℤ≥‘0)
111	5	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) → 𝑀 ∈ ℕ0)
112		fvexd 6873	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) → (𝐺‘𝑥) ∈ V)
113		eldifi 4094	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 ∈ (ℂ ∖ {0}) → 𝑥 ∈ ℂ)
114	98	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))))
115	10	mptex 7197	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))) ∈ V
116	115	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))) ∈ V)
117	114, 116	fvmpt2d 6981	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (𝐺‘𝑥) = (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))))
118	117	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑥) = (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))))
119		fveq2 6858	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑛 = 𝑘 → (𝐴‘𝑛) = (𝐴‘𝑘))
120		oveq2 7395	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑛 = 𝑘 → (𝑥↑𝑛) = (𝑥↑𝑘))
121	119, 120	oveq12d 7405	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑛 = 𝑘 → ((𝐴‘𝑛) · (𝑥↑𝑛)) = ((𝐴‘𝑘) · (𝑥↑𝑘)))
122	121	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) ∧ 𝑛 = 𝑘) → ((𝐴‘𝑛) · (𝑥↑𝑛)) = ((𝐴‘𝑘) · (𝑥↑𝑘)))
123		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ ℕ0)
124		ovexd 7422	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → ((𝐴‘𝑘) · (𝑥↑𝑘)) ∈ V)
125	118, 122, 123, 124	fvmptd 6975	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → ((𝐺‘𝑥)‘𝑘) = ((𝐴‘𝑘) · (𝑥↑𝑘)))
126	34	adantlr 715	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (𝐴‘𝑘) ∈ ℂ)
127		simplr 768	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → 𝑥 ∈ ℂ)
128	127, 123	expcld 14111	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (𝑥↑𝑘) ∈ ℂ)
129	126, 128	mulcld 11194	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → ((𝐴‘𝑘) · (𝑥↑𝑘)) ∈ ℂ)
130	125, 129	eqeltrd 2828	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → ((𝐺‘𝑥)‘𝑘) ∈ ℂ)
131	113, 130	sylanl2 681	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ ℕ0) → ((𝐺‘𝑥)‘𝑘) ∈ ℂ)
132	131	adantlr 715	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) ∧ 𝑘 ∈ ℕ0) → ((𝐺‘𝑥)‘𝑘) ∈ ℂ)
133	33	adantlr 715	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ ℕ0)
134	133, 125	syldan 591	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) → ((𝐺‘𝑥)‘𝑘) = ((𝐴‘𝑘) · (𝑥↑𝑘)))
135	113, 134	sylanl2 681	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → ((𝐺‘𝑥)‘𝑘) = ((𝐴‘𝑘) · (𝑥↑𝑘)))
136	35	adantlr 715	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝐴‘𝑘) ∈ ℂ)
137	113	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → 𝑥 ∈ ℂ)
138	137	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → 𝑥 ∈ ℂ)
139	33	adantlr 715	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ ℕ0)
140	138, 139	expcld 14111	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝑥↑𝑘) ∈ ℂ)
141	36	adantlr 715	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝐴‘𝑘) ≠ 0)
142		eldifsni 4754	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 ∈ (ℂ ∖ {0}) → 𝑥 ≠ 0)
143	142	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → 𝑥 ≠ 0)
144	139	nn0zd 12555	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ ℤ)
145	138, 143, 144	expne0d 14117	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝑥↑𝑘) ≠ 0)
146	136, 140, 141, 145	mulne0d 11830	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → ((𝐴‘𝑘) · (𝑥↑𝑘)) ≠ 0)
147	135, 146	eqnetrd 2992	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → ((𝐺‘𝑥)‘𝑘) ≠ 0)
148	147	adantlr 715	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) ∧ 𝑘 ∈ 𝑍) → ((𝐺‘𝑥)‘𝑘) ≠ 0)
149		fvoveq1 7410	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 = 𝑘 → ((𝐺‘𝑥)‘(𝑛 + 1)) = ((𝐺‘𝑥)‘(𝑘 + 1)))
150		fveq2 6858	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 = 𝑘 → ((𝐺‘𝑥)‘𝑛) = ((𝐺‘𝑥)‘𝑘))
151	149, 150	oveq12d 7405	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 𝑘 → (((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)) = (((𝐺‘𝑥)‘(𝑘 + 1)) / ((𝐺‘𝑥)‘𝑘)))
152	151	fveq2d 6862	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑘 → (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛))) = (abs‘(((𝐺‘𝑥)‘(𝑘 + 1)) / ((𝐺‘𝑥)‘𝑘))))
153	152	cbvmptv 5211	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ 𝑍 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) = (𝑘 ∈ 𝑍 ↦ (abs‘(((𝐺‘𝑥)‘(𝑘 + 1)) / ((𝐺‘𝑥)‘𝑘))))
154	4	reseq2i 5947	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ↾ 𝑍) = ((𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ↾ (ℤ≥‘𝑀))
155	22	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → 𝑍 ⊆ ℕ0)
156	155	resmptd 6011	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → ((𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ↾ 𝑍) = (𝑛 ∈ 𝑍 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))))
157	154, 156	eqtr3id 2778	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → ((𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ↾ (ℤ≥‘𝑀)) = (𝑛 ∈ 𝑍 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))))
158	6	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → 𝑀 ∈ ℤ)
159	8	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → 𝐷 ⇝ 𝐿)
160	137	abscld 15405	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (abs‘𝑥) ∈ ℝ)
161	160	recnd 11202	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (abs‘𝑥) ∈ ℂ)
162	10	mptex 7197	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ∈ V
163	162	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ∈ V)
164	72	recnd 11202	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐷‘𝑘) ∈ ℂ)
165	164	adantlr 715	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝐷‘𝑘) ∈ ℂ)
166		eqidd 2730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) = (𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))))
167	152	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) ∧ 𝑛 = 𝑘) → (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛))) = (abs‘(((𝐺‘𝑥)‘(𝑘 + 1)) / ((𝐺‘𝑥)‘𝑘))))
168		fvexd 6873	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (abs‘(((𝐺‘𝑥)‘(𝑘 + 1)) / ((𝐺‘𝑥)‘𝑘))) ∈ V)
169	166, 167, 139, 168	fvmptd 6975	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → ((𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛))))‘𝑘) = (abs‘(((𝐺‘𝑥)‘(𝑘 + 1)) / ((𝐺‘𝑥)‘𝑘))))
170	117	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑥) = (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))))
171		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) ∧ 𝑛 = (𝑘 + 1)) → 𝑛 = (𝑘 + 1))
172	171	fveq2d 6862	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) ∧ 𝑛 = (𝑘 + 1)) → (𝐴‘𝑛) = (𝐴‘(𝑘 + 1)))
173	171	oveq2d 7403	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) ∧ 𝑛 = (𝑘 + 1)) → (𝑥↑𝑛) = (𝑥↑(𝑘 + 1)))
174	172, 173	oveq12d 7405	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) ∧ 𝑛 = (𝑘 + 1)) → ((𝐴‘𝑛) · (𝑥↑𝑛)) = ((𝐴‘(𝑘 + 1)) · (𝑥↑(𝑘 + 1))))
175		1nn0 12458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ 1 ∈ ℕ0
176	175	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) → 1 ∈ ℕ0)
177	133, 176	nn0addcld 12507	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) → (𝑘 + 1) ∈ ℕ0)
178		ovexd 7422	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) → ((𝐴‘(𝑘 + 1)) · (𝑥↑(𝑘 + 1))) ∈ V)
179	170, 174, 177, 178	fvmptd 6975	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) → ((𝐺‘𝑥)‘(𝑘 + 1)) = ((𝐴‘(𝑘 + 1)) · (𝑥↑(𝑘 + 1))))
180	121	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) ∧ 𝑛 = 𝑘) → ((𝐴‘𝑛) · (𝑥↑𝑛)) = ((𝐴‘𝑘) · (𝑥↑𝑘)))
181		ovexd 7422	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) → ((𝐴‘𝑘) · (𝑥↑𝑘)) ∈ V)
182	170, 180, 133, 181	fvmptd 6975	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) → ((𝐺‘𝑥)‘𝑘) = ((𝐴‘𝑘) · (𝑥↑𝑘)))
183	179, 182	oveq12d 7405	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) → (((𝐺‘𝑥)‘(𝑘 + 1)) / ((𝐺‘𝑥)‘𝑘)) = (((𝐴‘(𝑘 + 1)) · (𝑥↑(𝑘 + 1))) / ((𝐴‘𝑘) · (𝑥↑𝑘))))
184	113, 183	sylanl2 681	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (((𝐺‘𝑥)‘(𝑘 + 1)) / ((𝐺‘𝑥)‘𝑘)) = (((𝐴‘(𝑘 + 1)) · (𝑥↑(𝑘 + 1))) / ((𝐴‘𝑘) · (𝑥↑𝑘))))
185	32	adantlr 715	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝐴‘(𝑘 + 1)) ∈ ℂ)
186	113, 177	sylanl2 681	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝑘 + 1) ∈ ℕ0)
187	138, 186	expcld 14111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝑥↑(𝑘 + 1)) ∈ ℂ)
188	185, 136, 187, 140, 141, 145	divmuldivd 11999	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)) · ((𝑥↑(𝑘 + 1)) / (𝑥↑𝑘))) = (((𝐴‘(𝑘 + 1)) · (𝑥↑(𝑘 + 1))) / ((𝐴‘𝑘) · (𝑥↑𝑘))))
189	139	nn0cnd 12505	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ ℂ)
190		1cnd 11169	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → 1 ∈ ℂ)
191	189, 190	pncan2d 11535	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → ((𝑘 + 1) − 𝑘) = 1)
192	191	oveq2d 7403	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝑥↑((𝑘 + 1) − 𝑘)) = (𝑥↑1))
193	186	nn0zd 12555	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝑘 + 1) ∈ ℤ)
194	138, 143, 144, 193	expsubd 14122	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝑥↑((𝑘 + 1) − 𝑘)) = ((𝑥↑(𝑘 + 1)) / (𝑥↑𝑘)))
195	138	exp1d 14106	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝑥↑1) = 𝑥)
196	192, 194, 195	3eqtr3d 2772	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → ((𝑥↑(𝑘 + 1)) / (𝑥↑𝑘)) = 𝑥)
197	196	oveq2d 7403	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)) · ((𝑥↑(𝑘 + 1)) / (𝑥↑𝑘))) = (((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)) · 𝑥))
198	184, 188, 197	3eqtr2d 2770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (((𝐺‘𝑥)‘(𝑘 + 1)) / ((𝐺‘𝑥)‘𝑘)) = (((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)) · 𝑥))
199	198	fveq2d 6862	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (abs‘(((𝐺‘𝑥)‘(𝑘 + 1)) / ((𝐺‘𝑥)‘𝑘))) = (abs‘(((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)) · 𝑥)))
200	37	adantlr 715	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → ((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)) ∈ ℂ)
201	200, 138	absmuld 15423	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (abs‘(((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)) · 𝑥)) = ((abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))) · (abs‘𝑥)))
202	169, 199, 201	3eqtrd 2768	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → ((𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛))))‘𝑘) = ((abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))) · (abs‘𝑥)))
203	71, 26	eqtr3d 2766	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐷‘𝑘) = (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))))
204	203	adantlr 715	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝐷‘𝑘) = (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))))
205	204	eqcomd 2735	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))) = (𝐷‘𝑘))
206	205	oveq1d 7402	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → ((abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))) · (abs‘𝑥)) = ((𝐷‘𝑘) · (abs‘𝑥)))
207	161	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (abs‘𝑥) ∈ ℂ)
208	165, 207	mulcomd 11195	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → ((𝐷‘𝑘) · (abs‘𝑥)) = ((abs‘𝑥) · (𝐷‘𝑘)))
209	202, 206, 208	3eqtrd 2768	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → ((𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛))))‘𝑘) = ((abs‘𝑥) · (𝐷‘𝑘)))
210	4, 158, 159, 161, 163, 165, 209	climmulc2 15603	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ⇝ ((abs‘𝑥) · 𝐿))
211		climres 15541	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑀 ∈ ℤ ∧ (𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ∈ V) → (((𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ↾ (ℤ≥‘𝑀)) ⇝ ((abs‘𝑥) · 𝐿) ↔ (𝑛 ∈ ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ⇝ ((abs‘𝑥) · 𝐿)))
212	158, 162, 211	sylancl 586	. . . . . . . . . . . . . . . . . . . . . . . . 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 5131	. . . . . . . . . . . . . . . . . . . . . . 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 44302	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) → (((abs‘𝑥) · 𝐿) < 1 ↔ seq0( + , (𝐺‘𝑥)) ∈ dom ⇝ ))
218	109, 217	sylanl2 681	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℝ ∖ {0})) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) → (((abs‘𝑥) · 𝐿) < 1 ↔ seq0( + , (𝐺‘𝑥)) ∈ dom ⇝ ))
219		eldifi 4094	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ (ℝ ∖ {0}) → 𝑥 ∈ ℝ)
220		fveq2 6858	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑟 = 𝑥 → (𝐺‘𝑟) = (𝐺‘𝑥))
221	220	seqeq3d 13974	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑟 = 𝑥 → seq0( + , (𝐺‘𝑟)) = seq0( + , (𝐺‘𝑥)))
222	221	eleq1d 2813	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑟 = 𝑥 → (seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ ↔ seq0( + , (𝐺‘𝑥)) ∈ dom ⇝ ))
223	222	elrab3 3660	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ℝ → (𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ } ↔ seq0( + , (𝐺‘𝑥)) ∈ dom ⇝ ))
224	219, 223	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (ℝ ∖ {0}) → (𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ } ↔ seq0( + , (𝐺‘𝑥)) ∈ dom ⇝ ))
225	224	ad2antlr 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℝ ∖ {0})) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) → (𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ } ↔ seq0( + , (𝐺‘𝑥)) ∈ dom ⇝ ))
226	218, 225	bitr4d 282	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℝ ∖ {0})) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) → (((abs‘𝑥) · 𝐿) < 1 ↔ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
227	226	an32s 652	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ((abs‘𝑥) · 𝐿) ≠ 1) ∧ 𝑥 ∈ (ℝ ∖ {0})) → (((abs‘𝑥) · 𝐿) < 1 ↔ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
228	105, 227	jaodan 959	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ((abs‘𝑥) · 𝐿) ≠ 1) ∧ (𝑥 ∈ (ℝ ∩ {0}) ∨ 𝑥 ∈ (ℝ ∖ {0}))) → (((abs‘𝑥) · 𝐿) < 1 ↔ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
229	85, 228	sylan2br 595	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ((abs‘𝑥) · 𝐿) ≠ 1) ∧ 𝑥 ∈ ℝ) → (((abs‘𝑥) · 𝐿) < 1 ↔ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
230	229	an32s 652	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) → (((abs‘𝑥) · 𝐿) < 1 ↔ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
231	81, 230	bitr3d 281	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) → ((abs‘𝑥) < (1 / 𝐿) ↔ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
232	68, 231	syldan 591	. . . . . . . . . . . . 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 768	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (1 / 𝐿) < 𝑥) → 𝑥 ∈ ℝ)
242	49	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (1 / 𝐿) < 𝑥) → (abs‘𝑥) ∈ ℝ)
243		simpr 484	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (1 / 𝐿) < 𝑥) → (1 / 𝐿) < 𝑥)
244	241	leabsd 15381	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (1 / 𝐿) < 𝑥) → 𝑥 ≤ (abs‘𝑥))
245	240, 241, 242, 243, 244	ltletrd 11334	. . . . . . 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 593	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }) → (𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ } → ¬ (1 / 𝐿) < 𝑥))
249	44, 248	mpd 15	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }) → ¬ (1 / 𝐿) < 𝑥)
250	42	renegcld 11605	. . . . . . . . 9 ⊢ (𝜑 → -(1 / 𝐿) ∈ ℝ)
251	250	rexrd 11224	. . . . . . . 8 ⊢ (𝜑 → -(1 / 𝐿) ∈ ℝ*)
252		iooss1 13341	. . . . . . . 8 ⊢ ((-(1 / 𝐿) ∈ ℝ* ∧ -(1 / 𝐿) ≤ 𝑥) → (𝑥(,)(1 / 𝐿)) ⊆ (-(1 / 𝐿)(,)(1 / 𝐿)))
253	251, 252	sylan 580	. . . . . . 7 ⊢ ((𝜑 ∧ -(1 / 𝐿) ≤ 𝑥) → (𝑥(,)(1 / 𝐿)) ⊆ (-(1 / 𝐿)(,)(1 / 𝐿)))
254	253	adantlr 715	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑥 < (1 / 𝐿))) ∧ -(1 / 𝐿) ≤ 𝑥) → (𝑥(,)(1 / 𝐿)) ⊆ (-(1 / 𝐿)(,)(1 / 𝐿)))
255		eliooord 13366	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (𝑥(,)(1 / 𝐿)) → (𝑥 < 𝑘 ∧ 𝑘 < (1 / 𝐿)))
256	255	simpld 494	. . . . . . . . . 10 ⊢ (𝑘 ∈ (𝑥(,)(1 / 𝐿)) → 𝑥 < 𝑘)
257	256	rgen 3046	. . . . . . . . 9 ⊢ ∀𝑘 ∈ (𝑥(,)(1 / 𝐿))𝑥 < 𝑘
258		ioon0 13332	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ* ∧ (1 / 𝐿) ∈ ℝ*) → ((𝑥(,)(1 / 𝐿)) ≠ ∅ ↔ 𝑥 < (1 / 𝐿)))
259	43, 258	sylan2 593	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ* ∧ 𝜑) → ((𝑥(,)(1 / 𝐿)) ≠ ∅ ↔ 𝑥 < (1 / 𝐿)))
260	259	ancoms 458	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ*) → ((𝑥(,)(1 / 𝐿)) ≠ ∅ ↔ 𝑥 < (1 / 𝐿)))
261	260	biimpar 477	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ 𝑥 < (1 / 𝐿)) → (𝑥(,)(1 / 𝐿)) ≠ ∅)
262		r19.2zb 4459	. . . . . . . . . 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 4016	. . . . . 6 ⊢ ((𝑥(,)(1 / 𝐿)) ⊆ (-(1 / 𝐿)(,)(1 / 𝐿)) → (∃𝑘 ∈ (𝑥(,)(1 / 𝐿))𝑥 < 𝑘 → ∃𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘))
268	254, 266, 267	sylc 65	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑥 < (1 / 𝐿))) ∧ -(1 / 𝐿) ≤ 𝑥) → ∃𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘)
269		simplr 768	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ ¬ -(1 / 𝐿) ≤ 𝑥) → 𝑥 ∈ ℝ*)
270		xrltnle 11241	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ* ∧ -(1 / 𝐿) ∈ ℝ*) → (𝑥 < -(1 / 𝐿) ↔ ¬ -(1 / 𝐿) ≤ 𝑥))
271		xrltle 13109	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ* ∧ -(1 / 𝐿) ∈ ℝ*) → (𝑥 < -(1 / 𝐿) → 𝑥 ≤ -(1 / 𝐿)))
272	270, 271	sylbird 260	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ* ∧ -(1 / 𝐿) ∈ ℝ*) → (¬ -(1 / 𝐿) ≤ 𝑥 → 𝑥 ≤ -(1 / 𝐿)))
273	251, 272	sylan2 593	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ* ∧ 𝜑) → (¬ -(1 / 𝐿) ≤ 𝑥 → 𝑥 ≤ -(1 / 𝐿)))
274	273	ancoms 458	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ*) → (¬ -(1 / 𝐿) ≤ 𝑥 → 𝑥 ≤ -(1 / 𝐿)))
275	274	imp 406	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ ¬ -(1 / 𝐿) ≤ 𝑥) → 𝑥 ≤ -(1 / 𝐿))
276		iooss1 13341	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ* ∧ 𝑥 ≤ -(1 / 𝐿)) → (-(1 / 𝐿)(,)(1 / 𝐿)) ⊆ (𝑥(,)(1 / 𝐿)))
277	269, 275, 276	syl2anc 584	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ ¬ -(1 / 𝐿) ≤ 𝑥) → (-(1 / 𝐿)(,)(1 / 𝐿)) ⊆ (𝑥(,)(1 / 𝐿)))
278	277	sselda 3946	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ ¬ -(1 / 𝐿) ≤ 𝑥) ∧ 𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))) → 𝑘 ∈ (𝑥(,)(1 / 𝐿)))
279	278, 256	syl 17	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ ¬ -(1 / 𝐿) ≤ 𝑥) ∧ 𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))) → 𝑥 < 𝑘)
280	279	ralrimiva 3125	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ ¬ -(1 / 𝐿) ≤ 𝑥) → ∀𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘)
281	40, 77	recgt0d 12117	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 < (1 / 𝐿))
282	42, 42, 281, 281	addgt0d 11753	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 < ((1 / 𝐿) + (1 / 𝐿)))
283	42	recnd 11202	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1 / 𝐿) ∈ ℂ)
284	283, 283	subnegd 11540	. . . . . . . . . . . 12 ⊢ (𝜑 → ((1 / 𝐿) − -(1 / 𝐿)) = ((1 / 𝐿) + (1 / 𝐿)))
285	282, 284	breqtrrd 5135	. . . . . . . . . . 11 ⊢ (𝜑 → 0 < ((1 / 𝐿) − -(1 / 𝐿)))
286	250, 42	posdifd 11765	. . . . . . . . . . 11 ⊢ (𝜑 → (-(1 / 𝐿) < (1 / 𝐿) ↔ 0 < ((1 / 𝐿) − -(1 / 𝐿))))
287	285, 286	mpbird 257	. . . . . . . . . 10 ⊢ (𝜑 → -(1 / 𝐿) < (1 / 𝐿))
288		ioon0 13332	. . . . . . . . . . 11 ⊢ ((-(1 / 𝐿) ∈ ℝ* ∧ (1 / 𝐿) ∈ ℝ*) → ((-(1 / 𝐿)(,)(1 / 𝐿)) ≠ ∅ ↔ -(1 / 𝐿) < (1 / 𝐿)))
289	251, 43, 288	syl2anc 584	. . . . . . . . . 10 ⊢ (𝜑 → ((-(1 / 𝐿)(,)(1 / 𝐿)) ≠ ∅ ↔ -(1 / 𝐿) < (1 / 𝐿)))
290	287, 289	mpbird 257	. . . . . . . . 9 ⊢ (𝜑 → (-(1 / 𝐿)(,)(1 / 𝐿)) ≠ ∅)
291		r19.2zb 4459	. . . . . . . . 9 ⊢ ((-(1 / 𝐿)(,)(1 / 𝐿)) ≠ ∅ ↔ (∀𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘 → ∃𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘))
292	290, 291	sylib 218	. . . . . . . 8 ⊢ (𝜑 → (∀𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘 → ∃𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘))
293	292	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ ¬ -(1 / 𝐿) ≤ 𝑥) → (∀𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘 → ∃𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘))
294	280, 293	mpd 15	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ ¬ -(1 / 𝐿) ≤ 𝑥) → ∃𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘)
295	294	adantlrr 721	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑥 < (1 / 𝐿))) ∧ ¬ -(1 / 𝐿) ≤ 𝑥) → ∃𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘)
296	268, 295	pm2.61dan 812	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑥 < (1 / 𝐿))) → ∃𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘)
297		elioo2 13347	. . . . . . . . . . 11 ⊢ ((-(1 / 𝐿) ∈ ℝ* ∧ (1 / 𝐿) ∈ ℝ*) → (𝑥 ∈ (-(1 / 𝐿)(,)(1 / 𝐿)) ↔ (𝑥 ∈ ℝ ∧ -(1 / 𝐿) < 𝑥 ∧ 𝑥 < (1 / 𝐿))))
298	251, 43, 297	syl2anc 584	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ (-(1 / 𝐿)(,)(1 / 𝐿)) ↔ (𝑥 ∈ ℝ ∧ -(1 / 𝐿) < 𝑥 ∧ 𝑥 < (1 / 𝐿))))
299	298	biimpa 476	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))) → (𝑥 ∈ ℝ ∧ -(1 / 𝐿) < 𝑥 ∧ 𝑥 < (1 / 𝐿)))
300		simpr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
301	300, 46	absltd 15398	. . . . . . . . . . . . . 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 11310	. . . . . . . . . . . . . . . 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 1114	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ ∧ -(1 / 𝐿) < 𝑥 ∧ 𝑥 < (1 / 𝐿)) → (𝜑 → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
313	312	impcom 407	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ -(1 / 𝐿) < 𝑥 ∧ 𝑥 < (1 / 𝐿))) → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ })
314	299, 313	syldan 591	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))) → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ })
315	314	ex 412	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (-(1 / 𝐿)(,)(1 / 𝐿)) → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }))
316	315	ssrdv 3952	. . . . . 6 ⊢ (𝜑 → (-(1 / 𝐿)(,)(1 / 𝐿)) ⊆ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ })
317		ssrexv 4016	. . . . . 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 9408	. 2 ⊢ (𝜑 → sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) = (1 / 𝐿))
322	1, 321	eqtrid 2776	1 ⊢ (𝜑 → 𝑅 = (1 / 𝐿))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109   ≠ wne 2925  ∀wral 3044  ∃wrex 3053  {crab 3405  Vcvv 3447   ∖ cdif 3911   ∪ cun 3912   ∩ cin 3913   ⊆ wss 3914  ∅c0 4296  {csn 4589   class class class wbr 5107   ↦ cmpt 5188   Or wor 5545  dom cdm 5638   ↾ cres 5640  ⟶wf 6507  ‘cfv 6511  (class class class)co 7387  supcsup 9391  ℂcc 11066  ℝcr 11067  0cc0 11068  1c1 11069   + caddc 11071   · cmul 11073  ℝ^*cxr 11207   < clt 11208   ≤ cle 11209   − cmin 11405  -cneg 11406   / cdiv 11835  ℕ₀cn0 12442  ℤcz 12529  ℤ_≥cuz 12793  ℝ⁺crp 12951  (,)cioo 13306  seqcseq 13966  ↑cexp 14026  abscabs 15200   ⇝ cli 15450

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5234  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711  ax-inf2 9594  ax-cnex 11124  ax-resscn 11125  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-mulcom 11132  ax-addass 11133  ax-mulass 11134  ax-distr 11135  ax-i2m1 11136  ax-1ne0 11137  ax-1rid 11138  ax-rnegex 11139  ax-rrecex 11140  ax-cnre 11141  ax-pre-lttri 11142  ax-pre-lttrn 11143  ax-pre-ltadd 11144  ax-pre-mulgt0 11145  ax-pre-sup 11146

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rmo 3354  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-int 4911  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-se 5592  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-isom 6520  df-riota 7344  df-ov 7390  df-oprab 7391  df-mpo 7392  df-om 7843  df-1st 7968  df-2nd 7969  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-1o 8434  df-er 8671  df-pm 8802  df-en 8919  df-dom 8920  df-sdom 8921  df-fin 8922  df-sup 9393  df-inf 9394  df-oi 9463  df-card 9892  df-pnf 11210  df-mnf 11211  df-xr 11212  df-ltxr 11213  df-le 11214  df-sub 11407  df-neg 11408  df-div 11836  df-nn 12187  df-2 12249  df-3 12250  df-n0 12443  df-z 12530  df-uz 12794  df-q 12908  df-rp 12952  df-ioo 13310  df-ico 13312  df-fz 13469  df-fzo 13616  df-fl 13754  df-seq 13967  df-exp 14027  df-hash 14296  df-shft 15033  df-cj 15065  df-re 15066  df-im 15067  df-sqrt 15201  df-abs 15202  df-limsup 15437  df-clim 15454  df-rlim 15455  df-sum 15653

This theorem is referenced by:  binomcxplemradcnv  44341