radcnvrat

Description: Let L be the limit, if one exists, of the ratio ( abs( ( A( k + 1 ) ) / ( Ak ) ) ) (as in the ratio test cvgdvgrat ) as k increases. Then the radius of convergence of power series sum_ n e. NN0 ( ( An ) x. ( x ^ n ) ) is ( 1 / L ) if L is nonzero. Proof "The limit involved in the ratio test..." in https://en.wikipedia.org/wiki/Radius_of_convergence —a few lines that evidently hide quite an involved process to confirm. (Contributed by Steve Rodriguez, 8-Mar-2020)

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

Proof

Step	Hyp	Ref	Expression
1		radcnvrat.g	⊢ 𝐺 = ( 𝑥 ∈ ℂ ↦ ( 𝑛 ∈ ℕ₀ ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) )
2		radcnvrat.a	⊢ ( 𝜑 → 𝐴 : ℕ₀ ⟶ ℂ )
3		radcnvrat.r	⊢ 𝑅 = sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ^* , < )
4		radcnvrat.rat	⊢ 𝐷 = ( 𝑘 ∈ ℕ₀ ↦ ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) / ( 𝐴 ‘ 𝑘 ) ) ) )
5		radcnvrat.z	⊢ 𝑍 = ( ℤ_≥ ‘ 𝑀 )
6		radcnvrat.m	⊢ ( 𝜑 → 𝑀 ∈ ℕ₀ )
7		radcnvrat.n0	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐴 ‘ 𝑘 ) ≠ 0 )
8		radcnvrat.l	⊢ ( 𝜑 → 𝐷 ⇝ 𝐿 )
9		radcnvrat.ln0	⊢ ( 𝜑 → 𝐿 ≠ 0 )
10		xrltso	⊢ < Or ℝ^*
11	10	a1i	⊢ ( 𝜑 → < Or ℝ^* )
12	6	nn0zd	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
13	5	reseq2i	⊢ ( 𝐷 ↾ 𝑍 ) = ( 𝐷 ↾ ( ℤ_≥ ‘ 𝑀 ) )
14		nn0ex	⊢ ℕ₀ ∈ V
15	14	mptex	⊢ ( 𝑘 ∈ ℕ₀ ↦ ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) / ( 𝐴 ‘ 𝑘 ) ) ) ) ∈ V
16	4 15	eqeltri	⊢ 𝐷 ∈ V
17		climres	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐷 ∈ V ) → ( ( 𝐷 ↾ ( ℤ_≥ ‘ 𝑀 ) ) ⇝ 𝐿 ↔ 𝐷 ⇝ 𝐿 ) )
18	12 16 17	sylancl	⊢ ( 𝜑 → ( ( 𝐷 ↾ ( ℤ_≥ ‘ 𝑀 ) ) ⇝ 𝐿 ↔ 𝐷 ⇝ 𝐿 ) )
19	8 18	mpbird	⊢ ( 𝜑 → ( 𝐷 ↾ ( ℤ_≥ ‘ 𝑀 ) ) ⇝ 𝐿 )
20	13 19	eqbrtrid	⊢ ( 𝜑 → ( 𝐷 ↾ 𝑍 ) ⇝ 𝐿 )
21	4	reseq1i	⊢ ( 𝐷 ↾ 𝑍 ) = ( ( 𝑘 ∈ ℕ₀ ↦ ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) / ( 𝐴 ‘ 𝑘 ) ) ) ) ↾ 𝑍 )
22		eluznn0	⊢ ( ( 𝑀 ∈ ℕ₀ ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝑀 ) ) → 𝑘 ∈ ℕ₀ )
23	6 22	sylan	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝑀 ) ) → 𝑘 ∈ ℕ₀ )
24	23	ex	⊢ ( 𝜑 → ( 𝑘 ∈ ( ℤ_≥ ‘ 𝑀 ) → 𝑘 ∈ ℕ₀ ) )
25	24	ssrdv	⊢ ( 𝜑 → ( ℤ_≥ ‘ 𝑀 ) ⊆ ℕ₀ )
26	5 25	eqsstrid	⊢ ( 𝜑 → 𝑍 ⊆ ℕ₀ )
27	26	resmptd	⊢ ( 𝜑 → ( ( 𝑘 ∈ ℕ₀ ↦ ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) / ( 𝐴 ‘ 𝑘 ) ) ) ) ↾ 𝑍 ) = ( 𝑘 ∈ 𝑍 ↦ ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) / ( 𝐴 ‘ 𝑘 ) ) ) ) )
28	21 27	syl5eq	⊢ ( 𝜑 → ( 𝐷 ↾ 𝑍 ) = ( 𝑘 ∈ 𝑍 ↦ ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) / ( 𝐴 ‘ 𝑘 ) ) ) ) )
29		fvexd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) / ( 𝐴 ‘ 𝑘 ) ) ) ∈ V )
30	28 29	fvmpt2d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝐷 ↾ 𝑍 ) ‘ 𝑘 ) = ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) / ( 𝐴 ‘ 𝑘 ) ) ) )
31	5	peano2uzs	⊢ ( 𝑘 ∈ 𝑍 → ( 𝑘 + 1 ) ∈ 𝑍 )
32	26	sselda	⊢ ( ( 𝜑 ∧ ( 𝑘 + 1 ) ∈ 𝑍 ) → ( 𝑘 + 1 ) ∈ ℕ₀ )
33	2	ffvelrnda	⊢ ( ( 𝜑 ∧ ( 𝑘 + 1 ) ∈ ℕ₀ ) → ( 𝐴 ‘ ( 𝑘 + 1 ) ) ∈ ℂ )
34	32 33	syldan	⊢ ( ( 𝜑 ∧ ( 𝑘 + 1 ) ∈ 𝑍 ) → ( 𝐴 ‘ ( 𝑘 + 1 ) ) ∈ ℂ )
35	31 34	sylan2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐴 ‘ ( 𝑘 + 1 ) ) ∈ ℂ )
36	26	sselda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝑘 ∈ ℕ₀ )
37	2	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ₀ ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
38	36 37	syldan	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
39	35 38 7	divcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) / ( 𝐴 ‘ 𝑘 ) ) ∈ ℂ )
40	39	abscld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) / ( 𝐴 ‘ 𝑘 ) ) ) ∈ ℝ )
41	30 40	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝐷 ↾ 𝑍 ) ‘ 𝑘 ) ∈ ℝ )
42	5 12 20 41	climrecl	⊢ ( 𝜑 → 𝐿 ∈ ℝ )
43	42 9	rereccld	⊢ ( 𝜑 → ( 1 / 𝐿 ) ∈ ℝ )
44	43	rexrd	⊢ ( 𝜑 → ( 1 / 𝐿 ) ∈ ℝ^* )
45		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } ) → 𝑥 ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } )
46		elrabi	⊢ ( 𝑥 ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } → 𝑥 ∈ ℝ )
47	43	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 1 / 𝐿 ) ∈ ℝ )
48		recn	⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℂ )
49	48	abscld	⊢ ( 𝑥 ∈ ℝ → ( abs ‘ 𝑥 ) ∈ ℝ )
50	49	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( abs ‘ 𝑥 ) ∈ ℝ )
51	47 50	ltlend	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( 1 / 𝐿 ) < ( abs ‘ 𝑥 ) ↔ ( ( 1 / 𝐿 ) ≤ ( abs ‘ 𝑥 ) ∧ ( abs ‘ 𝑥 ) ≠ ( 1 / 𝐿 ) ) ) )
52	51	simplbda	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 1 / 𝐿 ) < ( abs ‘ 𝑥 ) ) → ( abs ‘ 𝑥 ) ≠ ( 1 / 𝐿 ) )
53	51	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( abs ‘ 𝑥 ) ≠ ( 1 / 𝐿 ) ) → ( ( 1 / 𝐿 ) < ( abs ‘ 𝑥 ) ↔ ( ( 1 / 𝐿 ) ≤ ( abs ‘ 𝑥 ) ∧ ( abs ‘ 𝑥 ) ≠ ( 1 / 𝐿 ) ) ) )
54		simpr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( abs ‘ 𝑥 ) ≠ ( 1 / 𝐿 ) ) → ( abs ‘ 𝑥 ) ≠ ( 1 / 𝐿 ) )
55	54	biantrud	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( abs ‘ 𝑥 ) ≠ ( 1 / 𝐿 ) ) → ( ( 1 / 𝐿 ) ≤ ( abs ‘ 𝑥 ) ↔ ( ( 1 / 𝐿 ) ≤ ( abs ‘ 𝑥 ) ∧ ( abs ‘ 𝑥 ) ≠ ( 1 / 𝐿 ) ) ) )
56	47 50	lenltd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( 1 / 𝐿 ) ≤ ( abs ‘ 𝑥 ) ↔ ¬ ( abs ‘ 𝑥 ) < ( 1 / 𝐿 ) ) )
57	56	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( abs ‘ 𝑥 ) ≠ ( 1 / 𝐿 ) ) → ( ( 1 / 𝐿 ) ≤ ( abs ‘ 𝑥 ) ↔ ¬ ( abs ‘ 𝑥 ) < ( 1 / 𝐿 ) ) )
58	53 55 57	3bitr2d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( abs ‘ 𝑥 ) ≠ ( 1 / 𝐿 ) ) → ( ( 1 / 𝐿 ) < ( abs ‘ 𝑥 ) ↔ ¬ ( abs ‘ 𝑥 ) < ( 1 / 𝐿 ) ) )
59		1cnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 1 ∈ ℂ )
60	50	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( abs ‘ 𝑥 ) ∈ ℂ )
61	42	recnd	⊢ ( 𝜑 → 𝐿 ∈ ℂ )
62	61	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝐿 ∈ ℂ )
63	9	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝐿 ≠ 0 )
64	59 60 62 63	divmul3d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( 1 / 𝐿 ) = ( abs ‘ 𝑥 ) ↔ 1 = ( ( abs ‘ 𝑥 ) · 𝐿 ) ) )
65		eqcom	⊢ ( ( 1 / 𝐿 ) = ( abs ‘ 𝑥 ) ↔ ( abs ‘ 𝑥 ) = ( 1 / 𝐿 ) )
66		eqcom	⊢ ( 1 = ( ( abs ‘ 𝑥 ) · 𝐿 ) ↔ ( ( abs ‘ 𝑥 ) · 𝐿 ) = 1 )
67	64 65 66	3bitr3g	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( abs ‘ 𝑥 ) = ( 1 / 𝐿 ) ↔ ( ( abs ‘ 𝑥 ) · 𝐿 ) = 1 ) )
68	67	necon3bid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( abs ‘ 𝑥 ) ≠ ( 1 / 𝐿 ) ↔ ( ( abs ‘ 𝑥 ) · 𝐿 ) ≠ 1 ) )
69	68	biimpa	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( abs ‘ 𝑥 ) ≠ ( 1 / 𝐿 ) ) → ( ( abs ‘ 𝑥 ) · 𝐿 ) ≠ 1 )
70		1red	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 1 ∈ ℝ )
71		fvres	⊢ ( 𝑘 ∈ 𝑍 → ( ( 𝐷 ↾ 𝑍 ) ‘ 𝑘 ) = ( 𝐷 ‘ 𝑘 ) )
72	71	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝐷 ↾ 𝑍 ) ‘ 𝑘 ) = ( 𝐷 ‘ 𝑘 ) )
73	72 41	eqeltrrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐷 ‘ 𝑘 ) ∈ ℝ )
74	39	absge0d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 0 ≤ ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) / ( 𝐴 ‘ 𝑘 ) ) ) )
75	74 30	breqtrrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 0 ≤ ( ( 𝐷 ↾ 𝑍 ) ‘ 𝑘 ) )
76	75 72	breqtrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 0 ≤ ( 𝐷 ‘ 𝑘 ) )
77	5 12 8 73 76	climge0	⊢ ( 𝜑 → 0 ≤ 𝐿 )
78	42 77 9	ne0gt0d	⊢ ( 𝜑 → 0 < 𝐿 )
79	42 78	elrpd	⊢ ( 𝜑 → 𝐿 ∈ ℝ⁺ )
80	79	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝐿 ∈ ℝ⁺ )
81	50 70 80	ltmuldivd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( ( abs ‘ 𝑥 ) · 𝐿 ) < 1 ↔ ( abs ‘ 𝑥 ) < ( 1 / 𝐿 ) ) )
82	81	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( ( abs ‘ 𝑥 ) · 𝐿 ) ≠ 1 ) → ( ( ( abs ‘ 𝑥 ) · 𝐿 ) < 1 ↔ ( abs ‘ 𝑥 ) < ( 1 / 𝐿 ) ) )
83		elun	⊢ ( 𝑥 ∈ ( ( ℝ ∩ { 0 } ) ∪ ( ℝ ∖ { 0 } ) ) ↔ ( 𝑥 ∈ ( ℝ ∩ { 0 } ) ∨ 𝑥 ∈ ( ℝ ∖ { 0 } ) ) )
84		inundif	⊢ ( ( ℝ ∩ { 0 } ) ∪ ( ℝ ∖ { 0 } ) ) = ℝ
85	84	eleq2i	⊢ ( 𝑥 ∈ ( ( ℝ ∩ { 0 } ) ∪ ( ℝ ∖ { 0 } ) ) ↔ 𝑥 ∈ ℝ )
86	83 85	bitr3i	⊢ ( ( 𝑥 ∈ ( ℝ ∩ { 0 } ) ∨ 𝑥 ∈ ( ℝ ∖ { 0 } ) ) ↔ 𝑥 ∈ ℝ )
87		elin	⊢ ( 𝑥 ∈ ( ℝ ∩ { 0 } ) ↔ ( 𝑥 ∈ ℝ ∧ 𝑥 ∈ { 0 } ) )
88	87	simprbi	⊢ ( 𝑥 ∈ ( ℝ ∩ { 0 } ) → 𝑥 ∈ { 0 } )
89		elsni	⊢ ( 𝑥 ∈ { 0 } → 𝑥 = 0 )
90	88 89	syl	⊢ ( 𝑥 ∈ ( ℝ ∩ { 0 } ) → 𝑥 = 0 )
91		fveq2	⊢ ( 𝑥 = 0 → ( abs ‘ 𝑥 ) = ( abs ‘ 0 ) )
92		abs0	⊢ ( abs ‘ 0 ) = 0
93	91 92	eqtrdi	⊢ ( 𝑥 = 0 → ( abs ‘ 𝑥 ) = 0 )
94	93	oveq1d	⊢ ( 𝑥 = 0 → ( ( abs ‘ 𝑥 ) · 𝐿 ) = ( 0 · 𝐿 ) )
95	61	mul02d	⊢ ( 𝜑 → ( 0 · 𝐿 ) = 0 )
96	94 95	sylan9eqr	⊢ ( ( 𝜑 ∧ 𝑥 = 0 ) → ( ( abs ‘ 𝑥 ) · 𝐿 ) = 0 )
97		0lt1	⊢ 0 < 1
98	96 97	eqbrtrdi	⊢ ( ( 𝜑 ∧ 𝑥 = 0 ) → ( ( abs ‘ 𝑥 ) · 𝐿 ) < 1 )
99	1 2	radcnv0	⊢ ( 𝜑 → 0 ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } )
100		eleq1	⊢ ( 𝑥 = 0 → ( 𝑥 ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } ↔ 0 ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } ) )
101	99 100	syl5ibrcom	⊢ ( 𝜑 → ( 𝑥 = 0 → 𝑥 ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } ) )
102	101	imp	⊢ ( ( 𝜑 ∧ 𝑥 = 0 ) → 𝑥 ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } )
103	98 102	2thd	⊢ ( ( 𝜑 ∧ 𝑥 = 0 ) → ( ( ( abs ‘ 𝑥 ) · 𝐿 ) < 1 ↔ 𝑥 ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } ) )
104	90 103	sylan2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∩ { 0 } ) ) → ( ( ( abs ‘ 𝑥 ) · 𝐿 ) < 1 ↔ 𝑥 ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } ) )
105	104	adantlr	⊢ ( ( ( 𝜑 ∧ ( ( abs ‘ 𝑥 ) · 𝐿 ) ≠ 1 ) ∧ 𝑥 ∈ ( ℝ ∩ { 0 } ) ) → ( ( ( abs ‘ 𝑥 ) · 𝐿 ) < 1 ↔ 𝑥 ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } ) )
106		ax-resscn	⊢ ℝ ⊆ ℂ
107		ssdif	⊢ ( ℝ ⊆ ℂ → ( ℝ ∖ { 0 } ) ⊆ ( ℂ ∖ { 0 } ) )
108	106 107	ax-mp	⊢ ( ℝ ∖ { 0 } ) ⊆ ( ℂ ∖ { 0 } )
109	108	sseli	⊢ ( 𝑥 ∈ ( ℝ ∖ { 0 } ) → 𝑥 ∈ ( ℂ ∖ { 0 } ) )
110		nn0uz	⊢ ℕ₀ = ( ℤ_≥ ‘ 0 )
111	6	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( ( abs ‘ 𝑥 ) · 𝐿 ) ≠ 1 ) → 𝑀 ∈ ℕ₀ )
112		fvexd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( ( abs ‘ 𝑥 ) · 𝐿 ) ≠ 1 ) → ( 𝐺 ‘ 𝑥 ) ∈ V )
113		eldifi	⊢ ( 𝑥 ∈ ( ℂ ∖ { 0 } ) → 𝑥 ∈ ℂ )
114	1	a1i	⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ ℂ ↦ ( 𝑛 ∈ ℕ₀ ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) ) )
115	14	mptex	⊢ ( 𝑛 ∈ ℕ₀ ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) ∈ V
116	115	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( 𝑛 ∈ ℕ₀ ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) ∈ V )
117	114 116	fvmpt2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( 𝐺 ‘ 𝑥 ) = ( 𝑛 ∈ ℕ₀ ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) )
118	117	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ℕ₀ ) → ( 𝐺 ‘ 𝑥 ) = ( 𝑛 ∈ ℕ₀ ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) )
119		fveq2	⊢ ( 𝑛 = 𝑘 → ( 𝐴 ‘ 𝑛 ) = ( 𝐴 ‘ 𝑘 ) )
120		oveq2	⊢ ( 𝑛 = 𝑘 → ( 𝑥 ↑ 𝑛 ) = ( 𝑥 ↑ 𝑘 ) )
121	119 120	oveq12d	⊢ ( 𝑛 = 𝑘 → ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) = ( ( 𝐴 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) )
122	121	adantl	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ℕ₀ ) ∧ 𝑛 = 𝑘 ) → ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) = ( ( 𝐴 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) )
123		simpr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ℕ₀ ) → 𝑘 ∈ ℕ₀ )
124		ovexd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ℕ₀ ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) ∈ V )
125	118 122 123 124	fvmptd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ℕ₀ ) → ( ( 𝐺 ‘ 𝑥 ) ‘ 𝑘 ) = ( ( 𝐴 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) )
126	37	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ℕ₀ ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
127		simplr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ℕ₀ ) → 𝑥 ∈ ℂ )
128	127 123	expcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ℕ₀ ) → ( 𝑥 ↑ 𝑘 ) ∈ ℂ )
129	126 128	mulcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ℕ₀ ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) ∈ ℂ )
130	125 129	eqeltrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ℕ₀ ) → ( ( 𝐺 ‘ 𝑥 ) ‘ 𝑘 ) ∈ ℂ )
131	113 130	sylanl2	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑘 ∈ ℕ₀ ) → ( ( 𝐺 ‘ 𝑥 ) ‘ 𝑘 ) ∈ ℂ )
132	131	adantlr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( ( abs ‘ 𝑥 ) · 𝐿 ) ≠ 1 ) ∧ 𝑘 ∈ ℕ₀ ) → ( ( 𝐺 ‘ 𝑥 ) ‘ 𝑘 ) ∈ ℂ )
133	36	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ 𝑍 ) → 𝑘 ∈ ℕ₀ )
134	133 125	syldan	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝐺 ‘ 𝑥 ) ‘ 𝑘 ) = ( ( 𝐴 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) )
135	113 134	sylanl2	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝐺 ‘ 𝑥 ) ‘ 𝑘 ) = ( ( 𝐴 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) )
136	38	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑘 ∈ 𝑍 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
137	113	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → 𝑥 ∈ ℂ )
138	137	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑘 ∈ 𝑍 ) → 𝑥 ∈ ℂ )
139	36	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑘 ∈ 𝑍 ) → 𝑘 ∈ ℕ₀ )
140	138 139	expcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑘 ∈ 𝑍 ) → ( 𝑥 ↑ 𝑘 ) ∈ ℂ )
141	7	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑘 ∈ 𝑍 ) → ( 𝐴 ‘ 𝑘 ) ≠ 0 )
142		eldifsni	⊢ ( 𝑥 ∈ ( ℂ ∖ { 0 } ) → 𝑥 ≠ 0 )
143	142	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑘 ∈ 𝑍 ) → 𝑥 ≠ 0 )
144	139	nn0zd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑘 ∈ 𝑍 ) → 𝑘 ∈ ℤ )
145	138 143 144	expne0d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑘 ∈ 𝑍 ) → ( 𝑥 ↑ 𝑘 ) ≠ 0 )
146	136 140 141 145	mulne0d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) ≠ 0 )
147	135 146	eqnetrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝐺 ‘ 𝑥 ) ‘ 𝑘 ) ≠ 0 )
148	147	adantlr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( ( abs ‘ 𝑥 ) · 𝐿 ) ≠ 1 ) ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝐺 ‘ 𝑥 ) ‘ 𝑘 ) ≠ 0 )
149		fvoveq1	⊢ ( 𝑛 = 𝑘 → ( ( 𝐺 ‘ 𝑥 ) ‘ ( 𝑛 + 1 ) ) = ( ( 𝐺 ‘ 𝑥 ) ‘ ( 𝑘 + 1 ) ) )
150		fveq2	⊢ ( 𝑛 = 𝑘 → ( ( 𝐺 ‘ 𝑥 ) ‘ 𝑛 ) = ( ( 𝐺 ‘ 𝑥 ) ‘ 𝑘 ) )
151	149 150	oveq12d	⊢ ( 𝑛 = 𝑘 → ( ( ( 𝐺 ‘ 𝑥 ) ‘ ( 𝑛 + 1 ) ) / ( ( 𝐺 ‘ 𝑥 ) ‘ 𝑛 ) ) = ( ( ( 𝐺 ‘ 𝑥 ) ‘ ( 𝑘 + 1 ) ) / ( ( 𝐺 ‘ 𝑥 ) ‘ 𝑘 ) ) )
152	151	fveq2d	⊢ ( 𝑛 = 𝑘 → ( abs ‘ ( ( ( 𝐺 ‘ 𝑥 ) ‘ ( 𝑛 + 1 ) ) / ( ( 𝐺 ‘ 𝑥 ) ‘ 𝑛 ) ) ) = ( abs ‘ ( ( ( 𝐺 ‘ 𝑥 ) ‘ ( 𝑘 + 1 ) ) / ( ( 𝐺 ‘ 𝑥 ) ‘ 𝑘 ) ) ) )
153	152	cbvmptv	⊢ ( 𝑛 ∈ 𝑍 ↦ ( abs ‘ ( ( ( 𝐺 ‘ 𝑥 ) ‘ ( 𝑛 + 1 ) ) / ( ( 𝐺 ‘ 𝑥 ) ‘ 𝑛 ) ) ) ) = ( 𝑘 ∈ 𝑍 ↦ ( abs ‘ ( ( ( 𝐺 ‘ 𝑥 ) ‘ ( 𝑘 + 1 ) ) / ( ( 𝐺 ‘ 𝑥 ) ‘ 𝑘 ) ) ) )
154	5	reseq2i	⊢ ( ( 𝑛 ∈ ℕ₀ ↦ ( abs ‘ ( ( ( 𝐺 ‘ 𝑥 ) ‘ ( 𝑛 + 1 ) ) / ( ( 𝐺 ‘ 𝑥 ) ‘ 𝑛 ) ) ) ) ↾ 𝑍 ) = ( ( 𝑛 ∈ ℕ₀ ↦ ( abs ‘ ( ( ( 𝐺 ‘ 𝑥 ) ‘ ( 𝑛 + 1 ) ) / ( ( 𝐺 ‘ 𝑥 ) ‘ 𝑛 ) ) ) ) ↾ ( ℤ_≥ ‘ 𝑀 ) )
155	26	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → 𝑍 ⊆ ℕ₀ )
156	155	resmptd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( ( 𝑛 ∈ ℕ₀ ↦ ( abs ‘ ( ( ( 𝐺 ‘ 𝑥 ) ‘ ( 𝑛 + 1 ) ) / ( ( 𝐺 ‘ 𝑥 ) ‘ 𝑛 ) ) ) ) ↾ 𝑍 ) = ( 𝑛 ∈ 𝑍 ↦ ( abs ‘ ( ( ( 𝐺 ‘ 𝑥 ) ‘ ( 𝑛 + 1 ) ) / ( ( 𝐺 ‘ 𝑥 ) ‘ 𝑛 ) ) ) ) )
157	154 156	eqtr3id	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( ( 𝑛 ∈ ℕ₀ ↦ ( abs ‘ ( ( ( 𝐺 ‘ 𝑥 ) ‘ ( 𝑛 + 1 ) ) / ( ( 𝐺 ‘ 𝑥 ) ‘ 𝑛 ) ) ) ) ↾ ( ℤ_≥ ‘ 𝑀 ) ) = ( 𝑛 ∈ 𝑍 ↦ ( abs ‘ ( ( ( 𝐺 ‘ 𝑥 ) ‘ ( 𝑛 + 1 ) ) / ( ( 𝐺 ‘ 𝑥 ) ‘ 𝑛 ) ) ) ) )
158	12	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → 𝑀 ∈ ℤ )
159	8	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → 𝐷 ⇝ 𝐿 )
160	137	abscld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( abs ‘ 𝑥 ) ∈ ℝ )
161	160	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( abs ‘ 𝑥 ) ∈ ℂ )
162	14	mptex	⊢ ( 𝑛 ∈ ℕ₀ ↦ ( abs ‘ ( ( ( 𝐺 ‘ 𝑥 ) ‘ ( 𝑛 + 1 ) ) / ( ( 𝐺 ‘ 𝑥 ) ‘ 𝑛 ) ) ) ) ∈ V
163	162	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑛 ∈ ℕ₀ ↦ ( abs ‘ ( ( ( 𝐺 ‘ 𝑥 ) ‘ ( 𝑛 + 1 ) ) / ( ( 𝐺 ‘ 𝑥 ) ‘ 𝑛 ) ) ) ) ∈ V )
164	73	recnd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐷 ‘ 𝑘 ) ∈ ℂ )
165	164	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑘 ∈ 𝑍 ) → ( 𝐷 ‘ 𝑘 ) ∈ ℂ )
166		eqidd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑘 ∈ 𝑍 ) → ( 𝑛 ∈ ℕ₀ ↦ ( abs ‘ ( ( ( 𝐺 ‘ 𝑥 ) ‘ ( 𝑛 + 1 ) ) / ( ( 𝐺 ‘ 𝑥 ) ‘ 𝑛 ) ) ) ) = ( 𝑛 ∈ ℕ₀ ↦ ( abs ‘ ( ( ( 𝐺 ‘ 𝑥 ) ‘ ( 𝑛 + 1 ) ) / ( ( 𝐺 ‘ 𝑥 ) ‘ 𝑛 ) ) ) ) )
167	152	adantl	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑛 = 𝑘 ) → ( abs ‘ ( ( ( 𝐺 ‘ 𝑥 ) ‘ ( 𝑛 + 1 ) ) / ( ( 𝐺 ‘ 𝑥 ) ‘ 𝑛 ) ) ) = ( abs ‘ ( ( ( 𝐺 ‘ 𝑥 ) ‘ ( 𝑘 + 1 ) ) / ( ( 𝐺 ‘ 𝑥 ) ‘ 𝑘 ) ) ) )
168		fvexd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑘 ∈ 𝑍 ) → ( abs ‘ ( ( ( 𝐺 ‘ 𝑥 ) ‘ ( 𝑘 + 1 ) ) / ( ( 𝐺 ‘ 𝑥 ) ‘ 𝑘 ) ) ) ∈ V )
169	166 167 139 168	fvmptd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑛 ∈ ℕ₀ ↦ ( abs ‘ ( ( ( 𝐺 ‘ 𝑥 ) ‘ ( 𝑛 + 1 ) ) / ( ( 𝐺 ‘ 𝑥 ) ‘ 𝑛 ) ) ) ) ‘ 𝑘 ) = ( abs ‘ ( ( ( 𝐺 ‘ 𝑥 ) ‘ ( 𝑘 + 1 ) ) / ( ( 𝐺 ‘ 𝑥 ) ‘ 𝑘 ) ) ) )
170	117	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑥 ) = ( 𝑛 ∈ ℕ₀ ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) )
171		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑛 = ( 𝑘 + 1 ) ) → 𝑛 = ( 𝑘 + 1 ) )
172	171	fveq2d	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑛 = ( 𝑘 + 1 ) ) → ( 𝐴 ‘ 𝑛 ) = ( 𝐴 ‘ ( 𝑘 + 1 ) ) )
173	171	oveq2d	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑛 = ( 𝑘 + 1 ) ) → ( 𝑥 ↑ 𝑛 ) = ( 𝑥 ↑ ( 𝑘 + 1 ) ) )
174	172 173	oveq12d	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑛 = ( 𝑘 + 1 ) ) → ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) = ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑥 ↑ ( 𝑘 + 1 ) ) ) )
175		1nn0	⊢ 1 ∈ ℕ₀
176	175	a1i	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ 𝑍 ) → 1 ∈ ℕ₀ )
177	133 176	nn0addcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ 𝑍 ) → ( 𝑘 + 1 ) ∈ ℕ₀ )
178		ovexd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑥 ↑ ( 𝑘 + 1 ) ) ) ∈ V )
179	170 174 177 178	fvmptd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝐺 ‘ 𝑥 ) ‘ ( 𝑘 + 1 ) ) = ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑥 ↑ ( 𝑘 + 1 ) ) ) )
180	121	adantl	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑛 = 𝑘 ) → ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) = ( ( 𝐴 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) )
181		ovexd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) ∈ V )
182	170 180 133 181	fvmptd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝐺 ‘ 𝑥 ) ‘ 𝑘 ) = ( ( 𝐴 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) )
183	179 182	oveq12d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ 𝑍 ) → ( ( ( 𝐺 ‘ 𝑥 ) ‘ ( 𝑘 + 1 ) ) / ( ( 𝐺 ‘ 𝑥 ) ‘ 𝑘 ) ) = ( ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑥 ↑ ( 𝑘 + 1 ) ) ) / ( ( 𝐴 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) ) )
184	113 183	sylanl2	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑘 ∈ 𝑍 ) → ( ( ( 𝐺 ‘ 𝑥 ) ‘ ( 𝑘 + 1 ) ) / ( ( 𝐺 ‘ 𝑥 ) ‘ 𝑘 ) ) = ( ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑥 ↑ ( 𝑘 + 1 ) ) ) / ( ( 𝐴 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) ) )
185	35	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑘 ∈ 𝑍 ) → ( 𝐴 ‘ ( 𝑘 + 1 ) ) ∈ ℂ )
186	113 177	sylanl2	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑘 ∈ 𝑍 ) → ( 𝑘 + 1 ) ∈ ℕ₀ )
187	138 186	expcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑘 ∈ 𝑍 ) → ( 𝑥 ↑ ( 𝑘 + 1 ) ) ∈ ℂ )
188	185 136 187 140 141 145	divmuldivd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑘 ∈ 𝑍 ) → ( ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) / ( 𝐴 ‘ 𝑘 ) ) · ( ( 𝑥 ↑ ( 𝑘 + 1 ) ) / ( 𝑥 ↑ 𝑘 ) ) ) = ( ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑥 ↑ ( 𝑘 + 1 ) ) ) / ( ( 𝐴 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) ) )
189	139	nn0cnd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑘 ∈ 𝑍 ) → 𝑘 ∈ ℂ )
190		1cnd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑘 ∈ 𝑍 ) → 1 ∈ ℂ )
191	189 190	pncan2d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑘 + 1 ) − 𝑘 ) = 1 )
192	191	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑘 ∈ 𝑍 ) → ( 𝑥 ↑ ( ( 𝑘 + 1 ) − 𝑘 ) ) = ( 𝑥 ↑ 1 ) )
193	186	nn0zd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑘 ∈ 𝑍 ) → ( 𝑘 + 1 ) ∈ ℤ )
194	138 143 144 193	expsubd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑘 ∈ 𝑍 ) → ( 𝑥 ↑ ( ( 𝑘 + 1 ) − 𝑘 ) ) = ( ( 𝑥 ↑ ( 𝑘 + 1 ) ) / ( 𝑥 ↑ 𝑘 ) ) )
195	138	exp1d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑘 ∈ 𝑍 ) → ( 𝑥 ↑ 1 ) = 𝑥 )
196	192 194 195	3eqtr3d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑥 ↑ ( 𝑘 + 1 ) ) / ( 𝑥 ↑ 𝑘 ) ) = 𝑥 )
197	196	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑘 ∈ 𝑍 ) → ( ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) / ( 𝐴 ‘ 𝑘 ) ) · ( ( 𝑥 ↑ ( 𝑘 + 1 ) ) / ( 𝑥 ↑ 𝑘 ) ) ) = ( ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) / ( 𝐴 ‘ 𝑘 ) ) · 𝑥 ) )
198	184 188 197	3eqtr2d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑘 ∈ 𝑍 ) → ( ( ( 𝐺 ‘ 𝑥 ) ‘ ( 𝑘 + 1 ) ) / ( ( 𝐺 ‘ 𝑥 ) ‘ 𝑘 ) ) = ( ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) / ( 𝐴 ‘ 𝑘 ) ) · 𝑥 ) )
199	198	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑘 ∈ 𝑍 ) → ( abs ‘ ( ( ( 𝐺 ‘ 𝑥 ) ‘ ( 𝑘 + 1 ) ) / ( ( 𝐺 ‘ 𝑥 ) ‘ 𝑘 ) ) ) = ( abs ‘ ( ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) / ( 𝐴 ‘ 𝑘 ) ) · 𝑥 ) ) )
200	39	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) / ( 𝐴 ‘ 𝑘 ) ) ∈ ℂ )
201	200 138	absmuld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑘 ∈ 𝑍 ) → ( abs ‘ ( ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) / ( 𝐴 ‘ 𝑘 ) ) · 𝑥 ) ) = ( ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) / ( 𝐴 ‘ 𝑘 ) ) ) · ( abs ‘ 𝑥 ) ) )
202	169 199 201	3eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑛 ∈ ℕ₀ ↦ ( abs ‘ ( ( ( 𝐺 ‘ 𝑥 ) ‘ ( 𝑛 + 1 ) ) / ( ( 𝐺 ‘ 𝑥 ) ‘ 𝑛 ) ) ) ) ‘ 𝑘 ) = ( ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) / ( 𝐴 ‘ 𝑘 ) ) ) · ( abs ‘ 𝑥 ) ) )
203	72 30	eqtr3d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐷 ‘ 𝑘 ) = ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) / ( 𝐴 ‘ 𝑘 ) ) ) )
204	203	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑘 ∈ 𝑍 ) → ( 𝐷 ‘ 𝑘 ) = ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) / ( 𝐴 ‘ 𝑘 ) ) ) )
205	204	eqcomd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑘 ∈ 𝑍 ) → ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) / ( 𝐴 ‘ 𝑘 ) ) ) = ( 𝐷 ‘ 𝑘 ) )
206	205	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑘 ∈ 𝑍 ) → ( ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) / ( 𝐴 ‘ 𝑘 ) ) ) · ( abs ‘ 𝑥 ) ) = ( ( 𝐷 ‘ 𝑘 ) · ( abs ‘ 𝑥 ) ) )
207	161	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑘 ∈ 𝑍 ) → ( abs ‘ 𝑥 ) ∈ ℂ )
208	165 207	mulcomd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝐷 ‘ 𝑘 ) · ( abs ‘ 𝑥 ) ) = ( ( abs ‘ 𝑥 ) · ( 𝐷 ‘ 𝑘 ) ) )
209	202 206 208	3eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑛 ∈ ℕ₀ ↦ ( abs ‘ ( ( ( 𝐺 ‘ 𝑥 ) ‘ ( 𝑛 + 1 ) ) / ( ( 𝐺 ‘ 𝑥 ) ‘ 𝑛 ) ) ) ) ‘ 𝑘 ) = ( ( abs ‘ 𝑥 ) · ( 𝐷 ‘ 𝑘 ) ) )
210	5 158 159 161 163 165 209	climmulc2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑛 ∈ ℕ₀ ↦ ( abs ‘ ( ( ( 𝐺 ‘ 𝑥 ) ‘ ( 𝑛 + 1 ) ) / ( ( 𝐺 ‘ 𝑥 ) ‘ 𝑛 ) ) ) ) ⇝ ( ( abs ‘ 𝑥 ) · 𝐿 ) )
211		climres	⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝑛 ∈ ℕ₀ ↦ ( abs ‘ ( ( ( 𝐺 ‘ 𝑥 ) ‘ ( 𝑛 + 1 ) ) / ( ( 𝐺 ‘ 𝑥 ) ‘ 𝑛 ) ) ) ) ∈ V ) → ( ( ( 𝑛 ∈ ℕ₀ ↦ ( abs ‘ ( ( ( 𝐺 ‘ 𝑥 ) ‘ ( 𝑛 + 1 ) ) / ( ( 𝐺 ‘ 𝑥 ) ‘ 𝑛 ) ) ) ) ↾ ( ℤ_≥ ‘ 𝑀 ) ) ⇝ ( ( abs ‘ 𝑥 ) · 𝐿 ) ↔ ( 𝑛 ∈ ℕ₀ ↦ ( abs ‘ ( ( ( 𝐺 ‘ 𝑥 ) ‘ ( 𝑛 + 1 ) ) / ( ( 𝐺 ‘ 𝑥 ) ‘ 𝑛 ) ) ) ) ⇝ ( ( abs ‘ 𝑥 ) · 𝐿 ) ) )
212	158 162 211	sylancl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( ( ( 𝑛 ∈ ℕ₀ ↦ ( abs ‘ ( ( ( 𝐺 ‘ 𝑥 ) ‘ ( 𝑛 + 1 ) ) / ( ( 𝐺 ‘ 𝑥 ) ‘ 𝑛 ) ) ) ) ↾ ( ℤ_≥ ‘ 𝑀 ) ) ⇝ ( ( abs ‘ 𝑥 ) · 𝐿 ) ↔ ( 𝑛 ∈ ℕ₀ ↦ ( abs ‘ ( ( ( 𝐺 ‘ 𝑥 ) ‘ ( 𝑛 + 1 ) ) / ( ( 𝐺 ‘ 𝑥 ) ‘ 𝑛 ) ) ) ) ⇝ ( ( abs ‘ 𝑥 ) · 𝐿 ) ) )
213	210 212	mpbird	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( ( 𝑛 ∈ ℕ₀ ↦ ( abs ‘ ( ( ( 𝐺 ‘ 𝑥 ) ‘ ( 𝑛 + 1 ) ) / ( ( 𝐺 ‘ 𝑥 ) ‘ 𝑛 ) ) ) ) ↾ ( ℤ_≥ ‘ 𝑀 ) ) ⇝ ( ( abs ‘ 𝑥 ) · 𝐿 ) )
214	157 213	eqbrtrrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑛 ∈ 𝑍 ↦ ( abs ‘ ( ( ( 𝐺 ‘ 𝑥 ) ‘ ( 𝑛 + 1 ) ) / ( ( 𝐺 ‘ 𝑥 ) ‘ 𝑛 ) ) ) ) ⇝ ( ( abs ‘ 𝑥 ) · 𝐿 ) )
215	214	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( ( abs ‘ 𝑥 ) · 𝐿 ) ≠ 1 ) → ( 𝑛 ∈ 𝑍 ↦ ( abs ‘ ( ( ( 𝐺 ‘ 𝑥 ) ‘ ( 𝑛 + 1 ) ) / ( ( 𝐺 ‘ 𝑥 ) ‘ 𝑛 ) ) ) ) ⇝ ( ( abs ‘ 𝑥 ) · 𝐿 ) )
216		simpr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( ( abs ‘ 𝑥 ) · 𝐿 ) ≠ 1 ) → ( ( abs ‘ 𝑥 ) · 𝐿 ) ≠ 1 )
217	110 5 111 112 132 148 153 215 216	cvgdvgrat	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( ( abs ‘ 𝑥 ) · 𝐿 ) ≠ 1 ) → ( ( ( abs ‘ 𝑥 ) · 𝐿 ) < 1 ↔ seq 0 ( + , ( 𝐺 ‘ 𝑥 ) ) ∈ dom ⇝ ) )
218	109 217	sylanl2	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ { 0 } ) ) ∧ ( ( abs ‘ 𝑥 ) · 𝐿 ) ≠ 1 ) → ( ( ( abs ‘ 𝑥 ) · 𝐿 ) < 1 ↔ seq 0 ( + , ( 𝐺 ‘ 𝑥 ) ) ∈ dom ⇝ ) )
219		eldifi	⊢ ( 𝑥 ∈ ( ℝ ∖ { 0 } ) → 𝑥 ∈ ℝ )
220		fveq2	⊢ ( 𝑟 = 𝑥 → ( 𝐺 ‘ 𝑟 ) = ( 𝐺 ‘ 𝑥 ) )
221	220	seqeq3d	⊢ ( 𝑟 = 𝑥 → seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) = seq 0 ( + , ( 𝐺 ‘ 𝑥 ) ) )
222	221	eleq1d	⊢ ( 𝑟 = 𝑥 → ( seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ ↔ seq 0 ( + , ( 𝐺 ‘ 𝑥 ) ) ∈ dom ⇝ ) )
223	222	elrab3	⊢ ( 𝑥 ∈ ℝ → ( 𝑥 ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } ↔ seq 0 ( + , ( 𝐺 ‘ 𝑥 ) ) ∈ dom ⇝ ) )
224	219 223	syl	⊢ ( 𝑥 ∈ ( ℝ ∖ { 0 } ) → ( 𝑥 ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } ↔ seq 0 ( + , ( 𝐺 ‘ 𝑥 ) ) ∈ dom ⇝ ) )
225	224	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ { 0 } ) ) ∧ ( ( abs ‘ 𝑥 ) · 𝐿 ) ≠ 1 ) → ( 𝑥 ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } ↔ seq 0 ( + , ( 𝐺 ‘ 𝑥 ) ) ∈ dom ⇝ ) )
226	218 225	bitr4d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ { 0 } ) ) ∧ ( ( abs ‘ 𝑥 ) · 𝐿 ) ≠ 1 ) → ( ( ( abs ‘ 𝑥 ) · 𝐿 ) < 1 ↔ 𝑥 ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } ) )
227	226	an32s	⊢ ( ( ( 𝜑 ∧ ( ( abs ‘ 𝑥 ) · 𝐿 ) ≠ 1 ) ∧ 𝑥 ∈ ( ℝ ∖ { 0 } ) ) → ( ( ( abs ‘ 𝑥 ) · 𝐿 ) < 1 ↔ 𝑥 ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } ) )
228	105 227	jaodan	⊢ ( ( ( 𝜑 ∧ ( ( abs ‘ 𝑥 ) · 𝐿 ) ≠ 1 ) ∧ ( 𝑥 ∈ ( ℝ ∩ { 0 } ) ∨ 𝑥 ∈ ( ℝ ∖ { 0 } ) ) ) → ( ( ( abs ‘ 𝑥 ) · 𝐿 ) < 1 ↔ 𝑥 ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } ) )
229	86 228	sylan2br	⊢ ( ( ( 𝜑 ∧ ( ( abs ‘ 𝑥 ) · 𝐿 ) ≠ 1 ) ∧ 𝑥 ∈ ℝ ) → ( ( ( abs ‘ 𝑥 ) · 𝐿 ) < 1 ↔ 𝑥 ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } ) )
230	229	an32s	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( ( abs ‘ 𝑥 ) · 𝐿 ) ≠ 1 ) → ( ( ( abs ‘ 𝑥 ) · 𝐿 ) < 1 ↔ 𝑥 ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } ) )
231	82 230	bitr3d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( ( abs ‘ 𝑥 ) · 𝐿 ) ≠ 1 ) → ( ( abs ‘ 𝑥 ) < ( 1 / 𝐿 ) ↔ 𝑥 ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } ) )
232	69 231	syldan	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( abs ‘ 𝑥 ) ≠ ( 1 / 𝐿 ) ) → ( ( abs ‘ 𝑥 ) < ( 1 / 𝐿 ) ↔ 𝑥 ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } ) )
233	232	notbid	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( abs ‘ 𝑥 ) ≠ ( 1 / 𝐿 ) ) → ( ¬ ( abs ‘ 𝑥 ) < ( 1 / 𝐿 ) ↔ ¬ 𝑥 ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } ) )
234	58 233	bitrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( abs ‘ 𝑥 ) ≠ ( 1 / 𝐿 ) ) → ( ( 1 / 𝐿 ) < ( abs ‘ 𝑥 ) ↔ ¬ 𝑥 ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } ) )
235	234	biimpd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( abs ‘ 𝑥 ) ≠ ( 1 / 𝐿 ) ) → ( ( 1 / 𝐿 ) < ( abs ‘ 𝑥 ) → ¬ 𝑥 ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } ) )
236	235	impancom	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 1 / 𝐿 ) < ( abs ‘ 𝑥 ) ) → ( ( abs ‘ 𝑥 ) ≠ ( 1 / 𝐿 ) → ¬ 𝑥 ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } ) )
237	52 236	mpd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 1 / 𝐿 ) < ( abs ‘ 𝑥 ) ) → ¬ 𝑥 ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } )
238	237	ex	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( 1 / 𝐿 ) < ( abs ‘ 𝑥 ) → ¬ 𝑥 ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } ) )
239	238	con2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑥 ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } → ¬ ( 1 / 𝐿 ) < ( abs ‘ 𝑥 ) ) )
240	47	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 1 / 𝐿 ) < 𝑥 ) → ( 1 / 𝐿 ) ∈ ℝ )
241		simplr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 1 / 𝐿 ) < 𝑥 ) → 𝑥 ∈ ℝ )
242	50	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 1 / 𝐿 ) < 𝑥 ) → ( abs ‘ 𝑥 ) ∈ ℝ )
243		simpr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 1 / 𝐿 ) < 𝑥 ) → ( 1 / 𝐿 ) < 𝑥 )
244	241	leabsd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 1 / 𝐿 ) < 𝑥 ) → 𝑥 ≤ ( abs ‘ 𝑥 ) )
245	240 241 242 243 244	ltletrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 1 / 𝐿 ) < 𝑥 ) → ( 1 / 𝐿 ) < ( abs ‘ 𝑥 ) )
246	245	ex	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( 1 / 𝐿 ) < 𝑥 → ( 1 / 𝐿 ) < ( abs ‘ 𝑥 ) ) )
247	239 246	nsyld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑥 ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } → ¬ ( 1 / 𝐿 ) < 𝑥 ) )
248	46 247	sylan2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } ) → ( 𝑥 ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } → ¬ ( 1 / 𝐿 ) < 𝑥 ) )
249	45 248	mpd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } ) → ¬ ( 1 / 𝐿 ) < 𝑥 )
250	43	renegcld	⊢ ( 𝜑 → - ( 1 / 𝐿 ) ∈ ℝ )
251	250	rexrd	⊢ ( 𝜑 → - ( 1 / 𝐿 ) ∈ ℝ^* )
252		iooss1	⊢ ( ( - ( 1 / 𝐿 ) ∈ ℝ^* ∧ - ( 1 / 𝐿 ) ≤ 𝑥 ) → ( 𝑥 (,) ( 1 / 𝐿 ) ) ⊆ ( - ( 1 / 𝐿 ) (,) ( 1 / 𝐿 ) ) )
253	251 252	sylan	⊢ ( ( 𝜑 ∧ - ( 1 / 𝐿 ) ≤ 𝑥 ) → ( 𝑥 (,) ( 1 / 𝐿 ) ) ⊆ ( - ( 1 / 𝐿 ) (,) ( 1 / 𝐿 ) ) )
254	253	adantlr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ^* ∧ 𝑥 < ( 1 / 𝐿 ) ) ) ∧ - ( 1 / 𝐿 ) ≤ 𝑥 ) → ( 𝑥 (,) ( 1 / 𝐿 ) ) ⊆ ( - ( 1 / 𝐿 ) (,) ( 1 / 𝐿 ) ) )
255		eliooord	⊢ ( 𝑘 ∈ ( 𝑥 (,) ( 1 / 𝐿 ) ) → ( 𝑥 < 𝑘 ∧ 𝑘 < ( 1 / 𝐿 ) ) )
256	255	simpld	⊢ ( 𝑘 ∈ ( 𝑥 (,) ( 1 / 𝐿 ) ) → 𝑥 < 𝑘 )
257	256	rgen	⊢ ∀ 𝑘 ∈ ( 𝑥 (,) ( 1 / 𝐿 ) ) 𝑥 < 𝑘
258		ioon0	⊢ ( ( 𝑥 ∈ ℝ^* ∧ ( 1 / 𝐿 ) ∈ ℝ^* ) → ( ( 𝑥 (,) ( 1 / 𝐿 ) ) ≠ ∅ ↔ 𝑥 < ( 1 / 𝐿 ) ) )
259	44 258	sylan2	⊢ ( ( 𝑥 ∈ ℝ^* ∧ 𝜑 ) → ( ( 𝑥 (,) ( 1 / 𝐿 ) ) ≠ ∅ ↔ 𝑥 < ( 1 / 𝐿 ) ) )
260	259	ancoms	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ^* ) → ( ( 𝑥 (,) ( 1 / 𝐿 ) ) ≠ ∅ ↔ 𝑥 < ( 1 / 𝐿 ) ) )
261	260	biimpar	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ^* ) ∧ 𝑥 < ( 1 / 𝐿 ) ) → ( 𝑥 (,) ( 1 / 𝐿 ) ) ≠ ∅ )
262		r19.2zb	⊢ ( ( 𝑥 (,) ( 1 / 𝐿 ) ) ≠ ∅ ↔ ( ∀ 𝑘 ∈ ( 𝑥 (,) ( 1 / 𝐿 ) ) 𝑥 < 𝑘 → ∃ 𝑘 ∈ ( 𝑥 (,) ( 1 / 𝐿 ) ) 𝑥 < 𝑘 ) )
263	261 262	sylib	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ^* ) ∧ 𝑥 < ( 1 / 𝐿 ) ) → ( ∀ 𝑘 ∈ ( 𝑥 (,) ( 1 / 𝐿 ) ) 𝑥 < 𝑘 → ∃ 𝑘 ∈ ( 𝑥 (,) ( 1 / 𝐿 ) ) 𝑥 < 𝑘 ) )
264	257 263	mpi	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ^* ) ∧ 𝑥 < ( 1 / 𝐿 ) ) → ∃ 𝑘 ∈ ( 𝑥 (,) ( 1 / 𝐿 ) ) 𝑥 < 𝑘 )
265	264	anasss	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ^* ∧ 𝑥 < ( 1 / 𝐿 ) ) ) → ∃ 𝑘 ∈ ( 𝑥 (,) ( 1 / 𝐿 ) ) 𝑥 < 𝑘 )
266	265	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ^* ∧ 𝑥 < ( 1 / 𝐿 ) ) ) ∧ - ( 1 / 𝐿 ) ≤ 𝑥 ) → ∃ 𝑘 ∈ ( 𝑥 (,) ( 1 / 𝐿 ) ) 𝑥 < 𝑘 )
267		ssrexv	⊢ ( ( 𝑥 (,) ( 1 / 𝐿 ) ) ⊆ ( - ( 1 / 𝐿 ) (,) ( 1 / 𝐿 ) ) → ( ∃ 𝑘 ∈ ( 𝑥 (,) ( 1 / 𝐿 ) ) 𝑥 < 𝑘 → ∃ 𝑘 ∈ ( - ( 1 / 𝐿 ) (,) ( 1 / 𝐿 ) ) 𝑥 < 𝑘 ) )
268	254 266 267	sylc	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ^* ∧ 𝑥 < ( 1 / 𝐿 ) ) ) ∧ - ( 1 / 𝐿 ) ≤ 𝑥 ) → ∃ 𝑘 ∈ ( - ( 1 / 𝐿 ) (,) ( 1 / 𝐿 ) ) 𝑥 < 𝑘 )
269		simplr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ^* ) ∧ ¬ - ( 1 / 𝐿 ) ≤ 𝑥 ) → 𝑥 ∈ ℝ^* )
270		xrltnle	⊢ ( ( 𝑥 ∈ ℝ^* ∧ - ( 1 / 𝐿 ) ∈ ℝ^* ) → ( 𝑥 < - ( 1 / 𝐿 ) ↔ ¬ - ( 1 / 𝐿 ) ≤ 𝑥 ) )
271		xrltle	⊢ ( ( 𝑥 ∈ ℝ^* ∧ - ( 1 / 𝐿 ) ∈ ℝ^* ) → ( 𝑥 < - ( 1 / 𝐿 ) → 𝑥 ≤ - ( 1 / 𝐿 ) ) )
272	270 271	sylbird	⊢ ( ( 𝑥 ∈ ℝ^* ∧ - ( 1 / 𝐿 ) ∈ ℝ^* ) → ( ¬ - ( 1 / 𝐿 ) ≤ 𝑥 → 𝑥 ≤ - ( 1 / 𝐿 ) ) )
273	251 272	sylan2	⊢ ( ( 𝑥 ∈ ℝ^* ∧ 𝜑 ) → ( ¬ - ( 1 / 𝐿 ) ≤ 𝑥 → 𝑥 ≤ - ( 1 / 𝐿 ) ) )
274	273	ancoms	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ^* ) → ( ¬ - ( 1 / 𝐿 ) ≤ 𝑥 → 𝑥 ≤ - ( 1 / 𝐿 ) ) )
275	274	imp	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ^* ) ∧ ¬ - ( 1 / 𝐿 ) ≤ 𝑥 ) → 𝑥 ≤ - ( 1 / 𝐿 ) )
276		iooss1	⊢ ( ( 𝑥 ∈ ℝ^* ∧ 𝑥 ≤ - ( 1 / 𝐿 ) ) → ( - ( 1 / 𝐿 ) (,) ( 1 / 𝐿 ) ) ⊆ ( 𝑥 (,) ( 1 / 𝐿 ) ) )
277	269 275 276	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ^* ) ∧ ¬ - ( 1 / 𝐿 ) ≤ 𝑥 ) → ( - ( 1 / 𝐿 ) (,) ( 1 / 𝐿 ) ) ⊆ ( 𝑥 (,) ( 1 / 𝐿 ) ) )
278	277	sselda	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ^* ) ∧ ¬ - ( 1 / 𝐿 ) ≤ 𝑥 ) ∧ 𝑘 ∈ ( - ( 1 / 𝐿 ) (,) ( 1 / 𝐿 ) ) ) → 𝑘 ∈ ( 𝑥 (,) ( 1 / 𝐿 ) ) )
279	278 256	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ^* ) ∧ ¬ - ( 1 / 𝐿 ) ≤ 𝑥 ) ∧ 𝑘 ∈ ( - ( 1 / 𝐿 ) (,) ( 1 / 𝐿 ) ) ) → 𝑥 < 𝑘 )
280	279	ralrimiva	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ^* ) ∧ ¬ - ( 1 / 𝐿 ) ≤ 𝑥 ) → ∀ 𝑘 ∈ ( - ( 1 / 𝐿 ) (,) ( 1 / 𝐿 ) ) 𝑥 < 𝑘 )
281	42 78	recgt0d	⊢ ( 𝜑 → 0 < ( 1 / 𝐿 ) )
282	43 43 281 281	addgt0d	⊢ ( 𝜑 → 0 < ( ( 1 / 𝐿 ) + ( 1 / 𝐿 ) ) )
283	43	recnd	⊢ ( 𝜑 → ( 1 / 𝐿 ) ∈ ℂ )
284	283 283	subnegd	⊢ ( 𝜑 → ( ( 1 / 𝐿 ) − - ( 1 / 𝐿 ) ) = ( ( 1 / 𝐿 ) + ( 1 / 𝐿 ) ) )
285	282 284	breqtrrd	⊢ ( 𝜑 → 0 < ( ( 1 / 𝐿 ) − - ( 1 / 𝐿 ) ) )
286	250 43	posdifd	⊢ ( 𝜑 → ( - ( 1 / 𝐿 ) < ( 1 / 𝐿 ) ↔ 0 < ( ( 1 / 𝐿 ) − - ( 1 / 𝐿 ) ) ) )
287	285 286	mpbird	⊢ ( 𝜑 → - ( 1 / 𝐿 ) < ( 1 / 𝐿 ) )
288		ioon0	⊢ ( ( - ( 1 / 𝐿 ) ∈ ℝ^* ∧ ( 1 / 𝐿 ) ∈ ℝ^* ) → ( ( - ( 1 / 𝐿 ) (,) ( 1 / 𝐿 ) ) ≠ ∅ ↔ - ( 1 / 𝐿 ) < ( 1 / 𝐿 ) ) )
289	251 44 288	syl2anc	⊢ ( 𝜑 → ( ( - ( 1 / 𝐿 ) (,) ( 1 / 𝐿 ) ) ≠ ∅ ↔ - ( 1 / 𝐿 ) < ( 1 / 𝐿 ) ) )
290	287 289	mpbird	⊢ ( 𝜑 → ( - ( 1 / 𝐿 ) (,) ( 1 / 𝐿 ) ) ≠ ∅ )
291		r19.2zb	⊢ ( ( - ( 1 / 𝐿 ) (,) ( 1 / 𝐿 ) ) ≠ ∅ ↔ ( ∀ 𝑘 ∈ ( - ( 1 / 𝐿 ) (,) ( 1 / 𝐿 ) ) 𝑥 < 𝑘 → ∃ 𝑘 ∈ ( - ( 1 / 𝐿 ) (,) ( 1 / 𝐿 ) ) 𝑥 < 𝑘 ) )
292	290 291	sylib	⊢ ( 𝜑 → ( ∀ 𝑘 ∈ ( - ( 1 / 𝐿 ) (,) ( 1 / 𝐿 ) ) 𝑥 < 𝑘 → ∃ 𝑘 ∈ ( - ( 1 / 𝐿 ) (,) ( 1 / 𝐿 ) ) 𝑥 < 𝑘 ) )
293	292	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ^* ) ∧ ¬ - ( 1 / 𝐿 ) ≤ 𝑥 ) → ( ∀ 𝑘 ∈ ( - ( 1 / 𝐿 ) (,) ( 1 / 𝐿 ) ) 𝑥 < 𝑘 → ∃ 𝑘 ∈ ( - ( 1 / 𝐿 ) (,) ( 1 / 𝐿 ) ) 𝑥 < 𝑘 ) )
294	280 293	mpd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ^* ) ∧ ¬ - ( 1 / 𝐿 ) ≤ 𝑥 ) → ∃ 𝑘 ∈ ( - ( 1 / 𝐿 ) (,) ( 1 / 𝐿 ) ) 𝑥 < 𝑘 )
295	294	adantlrr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ^* ∧ 𝑥 < ( 1 / 𝐿 ) ) ) ∧ ¬ - ( 1 / 𝐿 ) ≤ 𝑥 ) → ∃ 𝑘 ∈ ( - ( 1 / 𝐿 ) (,) ( 1 / 𝐿 ) ) 𝑥 < 𝑘 )
296	268 295	pm2.61dan	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ^* ∧ 𝑥 < ( 1 / 𝐿 ) ) ) → ∃ 𝑘 ∈ ( - ( 1 / 𝐿 ) (,) ( 1 / 𝐿 ) ) 𝑥 < 𝑘 )
297		elioo2	⊢ ( ( - ( 1 / 𝐿 ) ∈ ℝ^* ∧ ( 1 / 𝐿 ) ∈ ℝ^* ) → ( 𝑥 ∈ ( - ( 1 / 𝐿 ) (,) ( 1 / 𝐿 ) ) ↔ ( 𝑥 ∈ ℝ ∧ - ( 1 / 𝐿 ) < 𝑥 ∧ 𝑥 < ( 1 / 𝐿 ) ) ) )
298	251 44 297	syl2anc	⊢ ( 𝜑 → ( 𝑥 ∈ ( - ( 1 / 𝐿 ) (,) ( 1 / 𝐿 ) ) ↔ ( 𝑥 ∈ ℝ ∧ - ( 1 / 𝐿 ) < 𝑥 ∧ 𝑥 < ( 1 / 𝐿 ) ) ) )
299	298	biimpa	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - ( 1 / 𝐿 ) (,) ( 1 / 𝐿 ) ) ) → ( 𝑥 ∈ ℝ ∧ - ( 1 / 𝐿 ) < 𝑥 ∧ 𝑥 < ( 1 / 𝐿 ) ) )
300		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℝ )
301	300 47	absltd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( abs ‘ 𝑥 ) < ( 1 / 𝐿 ) ↔ ( - ( 1 / 𝐿 ) < 𝑥 ∧ 𝑥 < ( 1 / 𝐿 ) ) ) )
302	50	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( abs ‘ 𝑥 ) < ( 1 / 𝐿 ) ) → ( abs ‘ 𝑥 ) ∈ ℝ )
303		simpr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( abs ‘ 𝑥 ) < ( 1 / 𝐿 ) ) → ( abs ‘ 𝑥 ) < ( 1 / 𝐿 ) )
304	302 303	ltned	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( abs ‘ 𝑥 ) < ( 1 / 𝐿 ) ) → ( abs ‘ 𝑥 ) ≠ ( 1 / 𝐿 ) )
305	232	biimpd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( abs ‘ 𝑥 ) ≠ ( 1 / 𝐿 ) ) → ( ( abs ‘ 𝑥 ) < ( 1 / 𝐿 ) → 𝑥 ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } ) )
306	305	impancom	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( abs ‘ 𝑥 ) < ( 1 / 𝐿 ) ) → ( ( abs ‘ 𝑥 ) ≠ ( 1 / 𝐿 ) → 𝑥 ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } ) )
307	304 306	mpd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( abs ‘ 𝑥 ) < ( 1 / 𝐿 ) ) → 𝑥 ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } )
308	307	ex	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( abs ‘ 𝑥 ) < ( 1 / 𝐿 ) → 𝑥 ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } ) )
309	301 308	sylbird	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( - ( 1 / 𝐿 ) < 𝑥 ∧ 𝑥 < ( 1 / 𝐿 ) ) → 𝑥 ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } ) )
310	309	impr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( - ( 1 / 𝐿 ) < 𝑥 ∧ 𝑥 < ( 1 / 𝐿 ) ) ) ) → 𝑥 ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } )
311	310	expcom	⊢ ( ( 𝑥 ∈ ℝ ∧ ( - ( 1 / 𝐿 ) < 𝑥 ∧ 𝑥 < ( 1 / 𝐿 ) ) ) → ( 𝜑 → 𝑥 ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } ) )
312	311	3impb	⊢ ( ( 𝑥 ∈ ℝ ∧ - ( 1 / 𝐿 ) < 𝑥 ∧ 𝑥 < ( 1 / 𝐿 ) ) → ( 𝜑 → 𝑥 ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } ) )
313	312	impcom	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ - ( 1 / 𝐿 ) < 𝑥 ∧ 𝑥 < ( 1 / 𝐿 ) ) ) → 𝑥 ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } )
314	299 313	syldan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - ( 1 / 𝐿 ) (,) ( 1 / 𝐿 ) ) ) → 𝑥 ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } )
315	314	ex	⊢ ( 𝜑 → ( 𝑥 ∈ ( - ( 1 / 𝐿 ) (,) ( 1 / 𝐿 ) ) → 𝑥 ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } ) )
316	315	ssrdv	⊢ ( 𝜑 → ( - ( 1 / 𝐿 ) (,) ( 1 / 𝐿 ) ) ⊆ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } )
317		ssrexv	⊢ ( ( - ( 1 / 𝐿 ) (,) ( 1 / 𝐿 ) ) ⊆ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } → ( ∃ 𝑘 ∈ ( - ( 1 / 𝐿 ) (,) ( 1 / 𝐿 ) ) 𝑥 < 𝑘 → ∃ 𝑘 ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } 𝑥 < 𝑘 ) )
318	316 317	syl	⊢ ( 𝜑 → ( ∃ 𝑘 ∈ ( - ( 1 / 𝐿 ) (,) ( 1 / 𝐿 ) ) 𝑥 < 𝑘 → ∃ 𝑘 ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } 𝑥 < 𝑘 ) )
319	318	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ^* ∧ 𝑥 < ( 1 / 𝐿 ) ) ) → ( ∃ 𝑘 ∈ ( - ( 1 / 𝐿 ) (,) ( 1 / 𝐿 ) ) 𝑥 < 𝑘 → ∃ 𝑘 ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } 𝑥 < 𝑘 ) )
320	296 319	mpd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ^* ∧ 𝑥 < ( 1 / 𝐿 ) ) ) → ∃ 𝑘 ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } 𝑥 < 𝑘 )
321	11 44 249 320	eqsupd	⊢ ( 𝜑 → sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ^* , < ) = ( 1 / 𝐿 ) )
322	3 321	syl5eq	⊢ ( 𝜑 → 𝑅 = ( 1 / 𝐿 ) )

Metamath Proof Explorer

Theorem radcnvrat

Proof