lgamgulmlem6

Description: The series G is uniformly convergent on the compact region U , which describes a circle of radius R with holes of size 1 / R around the poles of the gamma function. (Contributed by Mario Carneiro, 9-Jul-2017)

	Ref	Expression
Hypotheses	lgamgulm.r	⊢ ( 𝜑 → 𝑅 ∈ ℕ )
	lgamgulm.u	⊢ 𝑈 = { 𝑥 ∈ ℂ ∣ ( ( abs ‘ 𝑥 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ₀ ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ) }
	lgamgulm.g	⊢ 𝐺 = ( 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ 𝑈 ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ) )
	lgamgulm.t	⊢ 𝑇 = ( 𝑚 ∈ ℕ ↦ if ( ( 2 · 𝑅 ) ≤ 𝑚 , ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑚 ↑ 2 ) ) ) , ( ( 𝑅 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) + ( ( log ‘ ( ( 𝑅 + 1 ) · 𝑚 ) ) + π ) ) ) )
Assertion	lgamgulmlem6	⊢ ( 𝜑 → ( seq 1 ( ∘_f + , 𝐺 ) ∈ dom ( ⇝_𝑢 ‘ 𝑈 ) ∧ ( seq 1 ( ∘_f + , 𝐺 ) ( ⇝_𝑢 ‘ 𝑈 ) ( 𝑧 ∈ 𝑈 ↦ 𝑂 ) → ∃ 𝑟 ∈ ℝ ∀ 𝑧 ∈ 𝑈 ( abs ‘ 𝑂 ) ≤ 𝑟 ) ) )

Proof

Step	Hyp	Ref	Expression
1		lgamgulm.r	⊢ ( 𝜑 → 𝑅 ∈ ℕ )
2		lgamgulm.u	⊢ 𝑈 = { 𝑥 ∈ ℂ ∣ ( ( abs ‘ 𝑥 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ₀ ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ) }
3		lgamgulm.g	⊢ 𝐺 = ( 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ 𝑈 ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ) )
4		lgamgulm.t	⊢ 𝑇 = ( 𝑚 ∈ ℕ ↦ if ( ( 2 · 𝑅 ) ≤ 𝑚 , ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑚 ↑ 2 ) ) ) , ( ( 𝑅 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) + ( ( log ‘ ( ( 𝑅 + 1 ) · 𝑚 ) ) + π ) ) ) )
5		nnuz	⊢ ℕ = ( ℤ_≥ ‘ 1 )
6		1zzd	⊢ ( 𝜑 → 1 ∈ ℤ )
7		cnex	⊢ ℂ ∈ V
8	2 7	rabex2	⊢ 𝑈 ∈ V
9	8	a1i	⊢ ( 𝜑 → 𝑈 ∈ V )
10	1 2	lgamgulmlem1	⊢ ( 𝜑 → 𝑈 ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )
11	10	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑧 ∈ 𝑈 ) → 𝑈 ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )
12		simpr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑧 ∈ 𝑈 ) → 𝑧 ∈ 𝑈 )
13	11 12	sseldd	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑧 ∈ 𝑈 ) → 𝑧 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )
14	13	eldifad	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑧 ∈ 𝑈 ) → 𝑧 ∈ ℂ )
15		simplr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑧 ∈ 𝑈 ) → 𝑚 ∈ ℕ )
16	15	peano2nnd	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑧 ∈ 𝑈 ) → ( 𝑚 + 1 ) ∈ ℕ )
17	16	nnrpd	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑧 ∈ 𝑈 ) → ( 𝑚 + 1 ) ∈ ℝ⁺ )
18	15	nnrpd	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑧 ∈ 𝑈 ) → 𝑚 ∈ ℝ⁺ )
19	17 18	rpdivcld	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑧 ∈ 𝑈 ) → ( ( 𝑚 + 1 ) / 𝑚 ) ∈ ℝ⁺ )
20	19	relogcld	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑧 ∈ 𝑈 ) → ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ∈ ℝ )
21	20	recnd	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑧 ∈ 𝑈 ) → ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ∈ ℂ )
22	14 21	mulcld	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑧 ∈ 𝑈 ) → ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) ∈ ℂ )
23	15	nncnd	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑧 ∈ 𝑈 ) → 𝑚 ∈ ℂ )
24	15	nnne0d	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑧 ∈ 𝑈 ) → 𝑚 ≠ 0 )
25	14 23 24	divcld	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑧 ∈ 𝑈 ) → ( 𝑧 / 𝑚 ) ∈ ℂ )
26		1cnd	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑧 ∈ 𝑈 ) → 1 ∈ ℂ )
27	25 26	addcld	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑧 ∈ 𝑈 ) → ( ( 𝑧 / 𝑚 ) + 1 ) ∈ ℂ )
28	13 15	dmgmdivn0	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑧 ∈ 𝑈 ) → ( ( 𝑧 / 𝑚 ) + 1 ) ≠ 0 )
29	27 28	logcld	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑧 ∈ 𝑈 ) → ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ∈ ℂ )
30	22 29	subcld	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑧 ∈ 𝑈 ) → ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ∈ ℂ )
31	30	fmpttd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝑧 ∈ 𝑈 ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ) : 𝑈 ⟶ ℂ )
32	7 8	elmap	⊢ ( ( 𝑧 ∈ 𝑈 ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ) ∈ ( ℂ ↑_m 𝑈 ) ↔ ( 𝑧 ∈ 𝑈 ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ) : 𝑈 ⟶ ℂ )
33	31 32	sylibr	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝑧 ∈ 𝑈 ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ) ∈ ( ℂ ↑_m 𝑈 ) )
34	33 3	fmptd	⊢ ( 𝜑 → 𝐺 : ℕ ⟶ ( ℂ ↑_m 𝑈 ) )
35		nnex	⊢ ℕ ∈ V
36	35	mptex	⊢ ( 𝑚 ∈ ℕ ↦ if ( ( 2 · 𝑅 ) ≤ 𝑚 , ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑚 ↑ 2 ) ) ) , ( ( 𝑅 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) + ( ( log ‘ ( ( 𝑅 + 1 ) · 𝑚 ) ) + π ) ) ) ) ∈ V
37	4 36	eqeltri	⊢ 𝑇 ∈ V
38	37	a1i	⊢ ( 𝜑 → 𝑇 ∈ V )
39	1	adantr	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝑅 ∈ ℕ )
40	39	nnred	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝑅 ∈ ℝ )
41		2re	⊢ 2 ∈ ℝ
42	41	a1i	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 2 ∈ ℝ )
43		1red	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 1 ∈ ℝ )
44	40 43	readdcld	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝑅 + 1 ) ∈ ℝ )
45	42 44	remulcld	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 2 · ( 𝑅 + 1 ) ) ∈ ℝ )
46		simpr	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝑚 ∈ ℕ )
47	46	nnsqcld	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝑚 ↑ 2 ) ∈ ℕ )
48	45 47	nndivred	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑚 ↑ 2 ) ) ∈ ℝ )
49	40 48	remulcld	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑚 ↑ 2 ) ) ) ∈ ℝ )
50	46	peano2nnd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝑚 + 1 ) ∈ ℕ )
51	50	nnrpd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝑚 + 1 ) ∈ ℝ⁺ )
52	46	nnrpd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝑚 ∈ ℝ⁺ )
53	51 52	rpdivcld	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 𝑚 + 1 ) / 𝑚 ) ∈ ℝ⁺ )
54	53	relogcld	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ∈ ℝ )
55	40 54	remulcld	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝑅 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) ∈ ℝ )
56	39	peano2nnd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝑅 + 1 ) ∈ ℕ )
57	56	nnrpd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝑅 + 1 ) ∈ ℝ⁺ )
58	57 52	rpmulcld	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 𝑅 + 1 ) · 𝑚 ) ∈ ℝ⁺ )
59	58	relogcld	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( log ‘ ( ( 𝑅 + 1 ) · 𝑚 ) ) ∈ ℝ )
60		pire	⊢ π ∈ ℝ
61	60	a1i	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → π ∈ ℝ )
62	59 61	readdcld	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( log ‘ ( ( 𝑅 + 1 ) · 𝑚 ) ) + π ) ∈ ℝ )
63	55 62	readdcld	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 𝑅 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) + ( ( log ‘ ( ( 𝑅 + 1 ) · 𝑚 ) ) + π ) ) ∈ ℝ )
64	49 63	ifcld	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → if ( ( 2 · 𝑅 ) ≤ 𝑚 , ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑚 ↑ 2 ) ) ) , ( ( 𝑅 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) + ( ( log ‘ ( ( 𝑅 + 1 ) · 𝑚 ) ) + π ) ) ) ∈ ℝ )
65	64 4	fmptd	⊢ ( 𝜑 → 𝑇 : ℕ ⟶ ℝ )
66	65	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑇 ‘ 𝑛 ) ∈ ℝ )
67	1 2 3 4	lgamgulmlem5	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑛 ) ‘ 𝑦 ) ) ≤ ( 𝑇 ‘ 𝑛 ) )
68	1 2 3 4	lgamgulmlem4	⊢ ( 𝜑 → seq 1 ( + , 𝑇 ) ∈ dom ⇝ )
69	5 6 9 34 38 66 67 68	mtest	⊢ ( 𝜑 → seq 1 ( ∘_f + , 𝐺 ) ∈ dom ( ⇝_𝑢 ‘ 𝑈 ) )
70		1zzd	⊢ ( ( 𝜑 ∧ seq 1 ( ∘_f + , 𝐺 ) ( ⇝_𝑢 ‘ 𝑈 ) ( 𝑧 ∈ 𝑈 ↦ 𝑂 ) ) → 1 ∈ ℤ )
71	8	a1i	⊢ ( ( 𝜑 ∧ seq 1 ( ∘_f + , 𝐺 ) ( ⇝_𝑢 ‘ 𝑈 ) ( 𝑧 ∈ 𝑈 ↦ 𝑂 ) ) → 𝑈 ∈ V )
72	34	adantr	⊢ ( ( 𝜑 ∧ seq 1 ( ∘_f + , 𝐺 ) ( ⇝_𝑢 ‘ 𝑈 ) ( 𝑧 ∈ 𝑈 ↦ 𝑂 ) ) → 𝐺 : ℕ ⟶ ( ℂ ↑_m 𝑈 ) )
73	37	a1i	⊢ ( ( 𝜑 ∧ seq 1 ( ∘_f + , 𝐺 ) ( ⇝_𝑢 ‘ 𝑈 ) ( 𝑧 ∈ 𝑈 ↦ 𝑂 ) ) → 𝑇 ∈ V )
74	66	adantlr	⊢ ( ( ( 𝜑 ∧ seq 1 ( ∘_f + , 𝐺 ) ( ⇝_𝑢 ‘ 𝑈 ) ( 𝑧 ∈ 𝑈 ↦ 𝑂 ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑇 ‘ 𝑛 ) ∈ ℝ )
75	67	adantlr	⊢ ( ( ( 𝜑 ∧ seq 1 ( ∘_f + , 𝐺 ) ( ⇝_𝑢 ‘ 𝑈 ) ( 𝑧 ∈ 𝑈 ↦ 𝑂 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑛 ) ‘ 𝑦 ) ) ≤ ( 𝑇 ‘ 𝑛 ) )
76	68	adantr	⊢ ( ( 𝜑 ∧ seq 1 ( ∘_f + , 𝐺 ) ( ⇝_𝑢 ‘ 𝑈 ) ( 𝑧 ∈ 𝑈 ↦ 𝑂 ) ) → seq 1 ( + , 𝑇 ) ∈ dom ⇝ )
77		simpr	⊢ ( ( 𝜑 ∧ seq 1 ( ∘_f + , 𝐺 ) ( ⇝_𝑢 ‘ 𝑈 ) ( 𝑧 ∈ 𝑈 ↦ 𝑂 ) ) → seq 1 ( ∘_f + , 𝐺 ) ( ⇝_𝑢 ‘ 𝑈 ) ( 𝑧 ∈ 𝑈 ↦ 𝑂 ) )
78	5 70 71 72 73 74 75 76 77	mtestbdd	⊢ ( ( 𝜑 ∧ seq 1 ( ∘_f + , 𝐺 ) ( ⇝_𝑢 ‘ 𝑈 ) ( 𝑧 ∈ 𝑈 ↦ 𝑂 ) ) → ∃ 𝑟 ∈ ℝ ∀ 𝑦 ∈ 𝑈 ( abs ‘ ( ( 𝑧 ∈ 𝑈 ↦ 𝑂 ) ‘ 𝑦 ) ) ≤ 𝑟 )
79		nfcv	⊢ Ⅎ 𝑧 abs
80		nffvmpt1	⊢ Ⅎ 𝑧 ( ( 𝑧 ∈ 𝑈 ↦ 𝑂 ) ‘ 𝑦 )
81	79 80	nffv	⊢ Ⅎ 𝑧 ( abs ‘ ( ( 𝑧 ∈ 𝑈 ↦ 𝑂 ) ‘ 𝑦 ) )
82		nfcv	⊢ Ⅎ 𝑧 ≤
83		nfcv	⊢ Ⅎ 𝑧 𝑟
84	81 82 83	nfbr	⊢ Ⅎ 𝑧 ( abs ‘ ( ( 𝑧 ∈ 𝑈 ↦ 𝑂 ) ‘ 𝑦 ) ) ≤ 𝑟
85		nfv	⊢ Ⅎ 𝑦 ( abs ‘ ( ( 𝑧 ∈ 𝑈 ↦ 𝑂 ) ‘ 𝑧 ) ) ≤ 𝑟
86		2fveq3	⊢ ( 𝑦 = 𝑧 → ( abs ‘ ( ( 𝑧 ∈ 𝑈 ↦ 𝑂 ) ‘ 𝑦 ) ) = ( abs ‘ ( ( 𝑧 ∈ 𝑈 ↦ 𝑂 ) ‘ 𝑧 ) ) )
87	86	breq1d	⊢ ( 𝑦 = 𝑧 → ( ( abs ‘ ( ( 𝑧 ∈ 𝑈 ↦ 𝑂 ) ‘ 𝑦 ) ) ≤ 𝑟 ↔ ( abs ‘ ( ( 𝑧 ∈ 𝑈 ↦ 𝑂 ) ‘ 𝑧 ) ) ≤ 𝑟 ) )
88	84 85 87	cbvralw	⊢ ( ∀ 𝑦 ∈ 𝑈 ( abs ‘ ( ( 𝑧 ∈ 𝑈 ↦ 𝑂 ) ‘ 𝑦 ) ) ≤ 𝑟 ↔ ∀ 𝑧 ∈ 𝑈 ( abs ‘ ( ( 𝑧 ∈ 𝑈 ↦ 𝑂 ) ‘ 𝑧 ) ) ≤ 𝑟 )
89		ulmcl	⊢ ( seq 1 ( ∘_f + , 𝐺 ) ( ⇝_𝑢 ‘ 𝑈 ) ( 𝑧 ∈ 𝑈 ↦ 𝑂 ) → ( 𝑧 ∈ 𝑈 ↦ 𝑂 ) : 𝑈 ⟶ ℂ )
90	89	adantl	⊢ ( ( 𝜑 ∧ seq 1 ( ∘_f + , 𝐺 ) ( ⇝_𝑢 ‘ 𝑈 ) ( 𝑧 ∈ 𝑈 ↦ 𝑂 ) ) → ( 𝑧 ∈ 𝑈 ↦ 𝑂 ) : 𝑈 ⟶ ℂ )
91		eqid	⊢ ( 𝑧 ∈ 𝑈 ↦ 𝑂 ) = ( 𝑧 ∈ 𝑈 ↦ 𝑂 )
92	91	fmpt	⊢ ( ∀ 𝑧 ∈ 𝑈 𝑂 ∈ ℂ ↔ ( 𝑧 ∈ 𝑈 ↦ 𝑂 ) : 𝑈 ⟶ ℂ )
93	90 92	sylibr	⊢ ( ( 𝜑 ∧ seq 1 ( ∘_f + , 𝐺 ) ( ⇝_𝑢 ‘ 𝑈 ) ( 𝑧 ∈ 𝑈 ↦ 𝑂 ) ) → ∀ 𝑧 ∈ 𝑈 𝑂 ∈ ℂ )
94	91	fvmpt2	⊢ ( ( 𝑧 ∈ 𝑈 ∧ 𝑂 ∈ ℂ ) → ( ( 𝑧 ∈ 𝑈 ↦ 𝑂 ) ‘ 𝑧 ) = 𝑂 )
95	94	fveq2d	⊢ ( ( 𝑧 ∈ 𝑈 ∧ 𝑂 ∈ ℂ ) → ( abs ‘ ( ( 𝑧 ∈ 𝑈 ↦ 𝑂 ) ‘ 𝑧 ) ) = ( abs ‘ 𝑂 ) )
96	95	breq1d	⊢ ( ( 𝑧 ∈ 𝑈 ∧ 𝑂 ∈ ℂ ) → ( ( abs ‘ ( ( 𝑧 ∈ 𝑈 ↦ 𝑂 ) ‘ 𝑧 ) ) ≤ 𝑟 ↔ ( abs ‘ 𝑂 ) ≤ 𝑟 ) )
97	96	ralimiaa	⊢ ( ∀ 𝑧 ∈ 𝑈 𝑂 ∈ ℂ → ∀ 𝑧 ∈ 𝑈 ( ( abs ‘ ( ( 𝑧 ∈ 𝑈 ↦ 𝑂 ) ‘ 𝑧 ) ) ≤ 𝑟 ↔ ( abs ‘ 𝑂 ) ≤ 𝑟 ) )
98		ralbi	⊢ ( ∀ 𝑧 ∈ 𝑈 ( ( abs ‘ ( ( 𝑧 ∈ 𝑈 ↦ 𝑂 ) ‘ 𝑧 ) ) ≤ 𝑟 ↔ ( abs ‘ 𝑂 ) ≤ 𝑟 ) → ( ∀ 𝑧 ∈ 𝑈 ( abs ‘ ( ( 𝑧 ∈ 𝑈 ↦ 𝑂 ) ‘ 𝑧 ) ) ≤ 𝑟 ↔ ∀ 𝑧 ∈ 𝑈 ( abs ‘ 𝑂 ) ≤ 𝑟 ) )
99	93 97 98	3syl	⊢ ( ( 𝜑 ∧ seq 1 ( ∘_f + , 𝐺 ) ( ⇝_𝑢 ‘ 𝑈 ) ( 𝑧 ∈ 𝑈 ↦ 𝑂 ) ) → ( ∀ 𝑧 ∈ 𝑈 ( abs ‘ ( ( 𝑧 ∈ 𝑈 ↦ 𝑂 ) ‘ 𝑧 ) ) ≤ 𝑟 ↔ ∀ 𝑧 ∈ 𝑈 ( abs ‘ 𝑂 ) ≤ 𝑟 ) )
100	88 99	syl5bb	⊢ ( ( 𝜑 ∧ seq 1 ( ∘_f + , 𝐺 ) ( ⇝_𝑢 ‘ 𝑈 ) ( 𝑧 ∈ 𝑈 ↦ 𝑂 ) ) → ( ∀ 𝑦 ∈ 𝑈 ( abs ‘ ( ( 𝑧 ∈ 𝑈 ↦ 𝑂 ) ‘ 𝑦 ) ) ≤ 𝑟 ↔ ∀ 𝑧 ∈ 𝑈 ( abs ‘ 𝑂 ) ≤ 𝑟 ) )
101	100	rexbidv	⊢ ( ( 𝜑 ∧ seq 1 ( ∘_f + , 𝐺 ) ( ⇝_𝑢 ‘ 𝑈 ) ( 𝑧 ∈ 𝑈 ↦ 𝑂 ) ) → ( ∃ 𝑟 ∈ ℝ ∀ 𝑦 ∈ 𝑈 ( abs ‘ ( ( 𝑧 ∈ 𝑈 ↦ 𝑂 ) ‘ 𝑦 ) ) ≤ 𝑟 ↔ ∃ 𝑟 ∈ ℝ ∀ 𝑧 ∈ 𝑈 ( abs ‘ 𝑂 ) ≤ 𝑟 ) )
102	78 101	mpbid	⊢ ( ( 𝜑 ∧ seq 1 ( ∘_f + , 𝐺 ) ( ⇝_𝑢 ‘ 𝑈 ) ( 𝑧 ∈ 𝑈 ↦ 𝑂 ) ) → ∃ 𝑟 ∈ ℝ ∀ 𝑧 ∈ 𝑈 ( abs ‘ 𝑂 ) ≤ 𝑟 )
103	102	ex	⊢ ( 𝜑 → ( seq 1 ( ∘_f + , 𝐺 ) ( ⇝_𝑢 ‘ 𝑈 ) ( 𝑧 ∈ 𝑈 ↦ 𝑂 ) → ∃ 𝑟 ∈ ℝ ∀ 𝑧 ∈ 𝑈 ( abs ‘ 𝑂 ) ≤ 𝑟 ) )
104	69 103	jca	⊢ ( 𝜑 → ( seq 1 ( ∘_f + , 𝐺 ) ∈ dom ( ⇝_𝑢 ‘ 𝑈 ) ∧ ( seq 1 ( ∘_f + , 𝐺 ) ( ⇝_𝑢 ‘ 𝑈 ) ( 𝑧 ∈ 𝑈 ↦ 𝑂 ) → ∃ 𝑟 ∈ ℝ ∀ 𝑧 ∈ 𝑈 ( abs ‘ 𝑂 ) ≤ 𝑟 ) ) )

Metamath Proof Explorer

Theorem lgamgulmlem6

Proof