Metamath Proof Explorer

Theorem lgambdd

Description: The log-Gamma function is bounded on the region U . (Contributed by Mario Carneiro, 9-Jul-2017)

Ref Expression
Hypotheses lgamgulm.r ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
lgamgulm.u ⊢ 𝑈 = { 𝑥 ∈ ℂ ∣ ( ( abs ‘ 𝑥 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ) }
lgamgulm.g ⊢ 𝐺 = ( 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ 𝑈 ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ) )
Assertion lgambdd ( 𝜑 → ∃ 𝑟 ∈ ℝ ∀ 𝑧 ∈ 𝑈 ( abs ‘ ( log Γ ‘ 𝑧 ) ) ≤ 𝑟 )

Proof

Step Hyp Ref Expression
1 lgamgulm.r ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
2 lgamgulm.u ⊢ 𝑈 = { 𝑥 ∈ ℂ ∣ ( ( abs ‘ 𝑥 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ) }
3 lgamgulm.g ⊢ 𝐺 = ( 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ 𝑈 ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ) )
4 1 2 3 lgamgulm2 ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ 𝑈 ( log Γ ‘ 𝑧 ) ∈ ℂ ∧ seq 1 ( ∘f + , 𝐺 ) ( ⇝𝑢 ‘ 𝑈 ) ( 𝑧 ∈ 𝑈 ↦ ( ( log Γ ‘ 𝑧 ) + ( log ‘ 𝑧 ) ) ) ) )
5 4 simprd ⊢ ( 𝜑 → seq 1 ( ∘f + , 𝐺 ) ( ⇝𝑢 ‘ 𝑈 ) ( 𝑧 ∈ 𝑈 ↦ ( ( log Γ ‘ 𝑧 ) + ( log ‘ 𝑧 ) ) ) )
6 eqid ⊢ ( 𝑚 ∈ ℕ ↦ if ( ( 2 · 𝑅 ) ≤ 𝑚 , ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑚 ↑ 2 ) ) ) , ( ( 𝑅 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) + ( ( log ‘ ( ( 𝑅 + 1 ) · 𝑚 ) ) + π ) ) ) ) = ( 𝑚 ∈ ℕ ↦ if ( ( 2 · 𝑅 ) ≤ 𝑚 , ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑚 ↑ 2 ) ) ) , ( ( 𝑅 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) + ( ( log ‘ ( ( 𝑅 + 1 ) · 𝑚 ) ) + π ) ) ) )
7 1 2 3 6 lgamgulmlem6 ⊢ ( 𝜑 → ( seq 1 ( ∘f + , 𝐺 ) ∈ dom ( ⇝𝑢 ‘ 𝑈 ) ∧ ( seq 1 ( ∘f + , 𝐺 ) ( ⇝𝑢 ‘ 𝑈 ) ( 𝑧 ∈ 𝑈 ↦ ( ( log Γ ‘ 𝑧 ) + ( log ‘ 𝑧 ) ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝑈 ( abs ‘ ( ( log Γ ‘ 𝑧 ) + ( log ‘ 𝑧 ) ) ) ≤ 𝑦 ) ) )
8 7 simprd ⊢ ( 𝜑 → ( seq 1 ( ∘f + , 𝐺 ) ( ⇝𝑢 ‘ 𝑈 ) ( 𝑧 ∈ 𝑈 ↦ ( ( log Γ ‘ 𝑧 ) + ( log ‘ 𝑧 ) ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝑈 ( abs ‘ ( ( log Γ ‘ 𝑧 ) + ( log ‘ 𝑧 ) ) ) ≤ 𝑦 ) )
9 5 8 mpd ⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝑈 ( abs ‘ ( ( log Γ ‘ 𝑧 ) + ( log ‘ 𝑧 ) ) ) ≤ 𝑦 )
10 1 nnrpd ⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
11 10 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝑅 ∈ ℝ+ )
12 11 relogcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( log ‘ 𝑅 ) ∈ ℝ )
13 pire ⊢ π ∈ ℝ
14 13 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → π ∈ ℝ )
15 12 14 readdcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ( log ‘ 𝑅 ) + π ) ∈ ℝ )
16 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℝ )
17 15 16 readdcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ( ( log ‘ 𝑅 ) + π ) + 𝑦 ) ∈ ℝ )
18 17 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑈 ( abs ‘ ( ( log Γ ‘ 𝑧 ) + ( log ‘ 𝑧 ) ) ) ≤ 𝑦 ) ) → ( ( ( log ‘ 𝑅 ) + π ) + 𝑦 ) ∈ ℝ )
19 4 simpld ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝑈 ( log Γ ‘ 𝑧 ) ∈ ℂ )
20 19 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ∀ 𝑧 ∈ 𝑈 ( log Γ ‘ 𝑧 ) ∈ ℂ )
21 20 r19.21bi ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝑈 ) → ( log Γ ‘ 𝑧 ) ∈ ℂ )
22 21 abscld ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝑈 ) → ( abs ‘ ( log Γ ‘ 𝑧 ) ) ∈ ℝ )
23 22 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝑈 ) ∧ ( abs ‘ ( ( log Γ ‘ 𝑧 ) + ( log ‘ 𝑧 ) ) ) ≤ 𝑦 ) → ( abs ‘ ( log Γ ‘ 𝑧 ) ) ∈ ℝ )
24 11 adantr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝑈 ) → 𝑅 ∈ ℝ+ )
25 24 relogcld ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝑈 ) → ( log ‘ 𝑅 ) ∈ ℝ )
26 13 a1i ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝑈 ) → π ∈ ℝ )
27 25 26 readdcld ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝑈 ) → ( ( log ‘ 𝑅 ) + π ) ∈ ℝ )
28 1 2 lgamgulmlem1 ⊢ ( 𝜑 → 𝑈 ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )
29 28 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝑈 ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )
30 29 sselda ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝑈 ) → 𝑧 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )
31 30 eldifad ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝑈 ) → 𝑧 ∈ ℂ )
32 30 dmgmn0 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝑈 ) → 𝑧 ≠ 0 )
33 31 32 logcld ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝑈 ) → ( log ‘ 𝑧 ) ∈ ℂ )
34 21 33 addcld ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝑈 ) → ( ( log Γ ‘ 𝑧 ) + ( log ‘ 𝑧 ) ) ∈ ℂ )
35 34 abscld ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝑈 ) → ( abs ‘ ( ( log Γ ‘ 𝑧 ) + ( log ‘ 𝑧 ) ) ) ∈ ℝ )
36 27 35 readdcld ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝑈 ) → ( ( ( log ‘ 𝑅 ) + π ) + ( abs ‘ ( ( log Γ ‘ 𝑧 ) + ( log ‘ 𝑧 ) ) ) ) ∈ ℝ )
37 36 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝑈 ) ∧ ( abs ‘ ( ( log Γ ‘ 𝑧 ) + ( log ‘ 𝑧 ) ) ) ≤ 𝑦 ) → ( ( ( log ‘ 𝑅 ) + π ) + ( abs ‘ ( ( log Γ ‘ 𝑧 ) + ( log ‘ 𝑧 ) ) ) ) ∈ ℝ )
38 17 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝑈 ) ∧ ( abs ‘ ( ( log Γ ‘ 𝑧 ) + ( log ‘ 𝑧 ) ) ) ≤ 𝑦 ) → ( ( ( log ‘ 𝑅 ) + π ) + 𝑦 ) ∈ ℝ )
39 33 abscld ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝑈 ) → ( abs ‘ ( log ‘ 𝑧 ) ) ∈ ℝ )
40 39 35 readdcld ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝑈 ) → ( ( abs ‘ ( log ‘ 𝑧 ) ) + ( abs ‘ ( ( log Γ ‘ 𝑧 ) + ( log ‘ 𝑧 ) ) ) ) ∈ ℝ )
41 33 negcld ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝑈 ) → - ( log ‘ 𝑧 ) ∈ ℂ )
42 21 41 abs2difd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝑈 ) → ( ( abs ‘ ( log Γ ‘ 𝑧 ) ) − ( abs ‘ - ( log ‘ 𝑧 ) ) ) ≤ ( abs ‘ ( ( log Γ ‘ 𝑧 ) − - ( log ‘ 𝑧 ) ) ) )
43 33 absnegd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝑈 ) → ( abs ‘ - ( log ‘ 𝑧 ) ) = ( abs ‘ ( log ‘ 𝑧 ) ) )
44 43 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝑈 ) → ( ( abs ‘ ( log Γ ‘ 𝑧 ) ) − ( abs ‘ - ( log ‘ 𝑧 ) ) ) = ( ( abs ‘ ( log Γ ‘ 𝑧 ) ) − ( abs ‘ ( log ‘ 𝑧 ) ) ) )
45 21 33 subnegd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝑈 ) → ( ( log Γ ‘ 𝑧 ) − - ( log ‘ 𝑧 ) ) = ( ( log Γ ‘ 𝑧 ) + ( log ‘ 𝑧 ) ) )
46 45 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝑈 ) → ( abs ‘ ( ( log Γ ‘ 𝑧 ) − - ( log ‘ 𝑧 ) ) ) = ( abs ‘ ( ( log Γ ‘ 𝑧 ) + ( log ‘ 𝑧 ) ) ) )
47 42 44 46 3brtr3d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝑈 ) → ( ( abs ‘ ( log Γ ‘ 𝑧 ) ) − ( abs ‘ ( log ‘ 𝑧 ) ) ) ≤ ( abs ‘ ( ( log Γ ‘ 𝑧 ) + ( log ‘ 𝑧 ) ) ) )
48 22 39 35 lesubadd2d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝑈 ) → ( ( ( abs ‘ ( log Γ ‘ 𝑧 ) ) − ( abs ‘ ( log ‘ 𝑧 ) ) ) ≤ ( abs ‘ ( ( log Γ ‘ 𝑧 ) + ( log ‘ 𝑧 ) ) ) ↔ ( abs ‘ ( log Γ ‘ 𝑧 ) ) ≤ ( ( abs ‘ ( log ‘ 𝑧 ) ) + ( abs ‘ ( ( log Γ ‘ 𝑧 ) + ( log ‘ 𝑧 ) ) ) ) ) )
49 47 48 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝑈 ) → ( abs ‘ ( log Γ ‘ 𝑧 ) ) ≤ ( ( abs ‘ ( log ‘ 𝑧 ) ) + ( abs ‘ ( ( log Γ ‘ 𝑧 ) + ( log ‘ 𝑧 ) ) ) ) )
50 31 32 absrpcld ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝑈 ) → ( abs ‘ 𝑧 ) ∈ ℝ+ )
51 50 relogcld ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝑈 ) → ( log ‘ ( abs ‘ 𝑧 ) ) ∈ ℝ )
52 51 recnd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝑈 ) → ( log ‘ ( abs ‘ 𝑧 ) ) ∈ ℂ )
53 52 abscld ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝑈 ) → ( abs ‘ ( log ‘ ( abs ‘ 𝑧 ) ) ) ∈ ℝ )
54 53 26 readdcld ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝑈 ) → ( ( abs ‘ ( log ‘ ( abs ‘ 𝑧 ) ) ) + π ) ∈ ℝ )
55 abslogle ⊢ ( ( 𝑧 ∈ ℂ ∧ 𝑧 ≠ 0 ) → ( abs ‘ ( log ‘ 𝑧 ) ) ≤ ( ( abs ‘ ( log ‘ ( abs ‘ 𝑧 ) ) ) + π ) )
56 31 32 55 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝑈 ) → ( abs ‘ ( log ‘ 𝑧 ) ) ≤ ( ( abs ‘ ( log ‘ ( abs ‘ 𝑧 ) ) ) + π ) )
57 df-neg ⊢ - ( log ‘ 𝑅 ) = ( 0 − ( log ‘ 𝑅 ) )
58 log1 ⊢ ( log ‘ 1 ) = 0
59 58 oveq1i ⊢ ( ( log ‘ 1 ) − ( log ‘ 𝑅 ) ) = ( 0 − ( log ‘ 𝑅 ) )
60 57 59 eqtr4i ⊢ - ( log ‘ 𝑅 ) = ( ( log ‘ 1 ) − ( log ‘ 𝑅 ) )
61 1rp ⊢ 1 ∈ ℝ+
62 relogdiv ⊢ ( ( 1 ∈ ℝ+ ∧ 𝑅 ∈ ℝ+ ) → ( log ‘ ( 1 / 𝑅 ) ) = ( ( log ‘ 1 ) − ( log ‘ 𝑅 ) ) )
63 61 24 62 sylancr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝑈 ) → ( log ‘ ( 1 / 𝑅 ) ) = ( ( log ‘ 1 ) − ( log ‘ 𝑅 ) ) )
64 60 63 eqtr4id ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝑈 ) → - ( log ‘ 𝑅 ) = ( log ‘ ( 1 / 𝑅 ) ) )
65 oveq2 ⊢ ( 𝑘 = 0 → ( 𝑧 + 𝑘 ) = ( 𝑧 + 0 ) )
66 65 fveq2d ⊢ ( 𝑘 = 0 → ( abs ‘ ( 𝑧 + 𝑘 ) ) = ( abs ‘ ( 𝑧 + 0 ) ) )
67 66 breq2d ⊢ ( 𝑘 = 0 → ( ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑧 + 𝑘 ) ) ↔ ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑧 + 0 ) ) ) )
68 fveq2 ⊢ ( 𝑥 = 𝑧 → ( abs ‘ 𝑥 ) = ( abs ‘ 𝑧 ) )
69 68 breq1d ⊢ ( 𝑥 = 𝑧 → ( ( abs ‘ 𝑥 ) ≤ 𝑅 ↔ ( abs ‘ 𝑧 ) ≤ 𝑅 ) )
70 fvoveq1 ⊢ ( 𝑥 = 𝑧 → ( abs ‘ ( 𝑥 + 𝑘 ) ) = ( abs ‘ ( 𝑧 + 𝑘 ) ) )
71 70 breq2d ⊢ ( 𝑥 = 𝑧 → ( ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ↔ ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑧 + 𝑘 ) ) ) )
72 71 ralbidv ⊢ ( 𝑥 = 𝑧 → ( ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ↔ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑧 + 𝑘 ) ) ) )
73 69 72 anbi12d ⊢ ( 𝑥 = 𝑧 → ( ( ( abs ‘ 𝑥 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ) ↔ ( ( abs ‘ 𝑧 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑧 + 𝑘 ) ) ) ) )
74 73 2 elrab2 ⊢ ( 𝑧 ∈ 𝑈 ↔ ( 𝑧 ∈ ℂ ∧ ( ( abs ‘ 𝑧 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑧 + 𝑘 ) ) ) ) )
75 74 simprbi ⊢ ( 𝑧 ∈ 𝑈 → ( ( abs ‘ 𝑧 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑧 + 𝑘 ) ) ) )
76 75 adantl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝑈 ) → ( ( abs ‘ 𝑧 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑧 + 𝑘 ) ) ) )
77 76 simprd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝑈 ) → ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑧 + 𝑘 ) ) )
78 0nn0 ⊢ 0 ∈ ℕ0
79 78 a1i ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝑈 ) → 0 ∈ ℕ0 )
80 67 77 79 rspcdva ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝑈 ) → ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑧 + 0 ) ) )
81 31 addridd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝑈 ) → ( 𝑧 + 0 ) = 𝑧 )
82 81 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝑈 ) → ( abs ‘ ( 𝑧 + 0 ) ) = ( abs ‘ 𝑧 ) )
83 80 82 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝑈 ) → ( 1 / 𝑅 ) ≤ ( abs ‘ 𝑧 ) )
84 24 rpreccld ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝑈 ) → ( 1 / 𝑅 ) ∈ ℝ+ )
85 84 50 logled ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝑈 ) → ( ( 1 / 𝑅 ) ≤ ( abs ‘ 𝑧 ) ↔ ( log ‘ ( 1 / 𝑅 ) ) ≤ ( log ‘ ( abs ‘ 𝑧 ) ) ) )
86 83 85 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝑈 ) → ( log ‘ ( 1 / 𝑅 ) ) ≤ ( log ‘ ( abs ‘ 𝑧 ) ) )
87 64 86 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝑈 ) → - ( log ‘ 𝑅 ) ≤ ( log ‘ ( abs ‘ 𝑧 ) ) )
88 76 simpld ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝑈 ) → ( abs ‘ 𝑧 ) ≤ 𝑅 )
89 50 24 logled ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝑈 ) → ( ( abs ‘ 𝑧 ) ≤ 𝑅 ↔ ( log ‘ ( abs ‘ 𝑧 ) ) ≤ ( log ‘ 𝑅 ) ) )
90 88 89 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝑈 ) → ( log ‘ ( abs ‘ 𝑧 ) ) ≤ ( log ‘ 𝑅 ) )
91 51 25 absled ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝑈 ) → ( ( abs ‘ ( log ‘ ( abs ‘ 𝑧 ) ) ) ≤ ( log ‘ 𝑅 ) ↔ ( - ( log ‘ 𝑅 ) ≤ ( log ‘ ( abs ‘ 𝑧 ) ) ∧ ( log ‘ ( abs ‘ 𝑧 ) ) ≤ ( log ‘ 𝑅 ) ) ) )
92 87 90 91 mpbir2and ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝑈 ) → ( abs ‘ ( log ‘ ( abs ‘ 𝑧 ) ) ) ≤ ( log ‘ 𝑅 ) )
93 53 25 26 92 leadd1dd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝑈 ) → ( ( abs ‘ ( log ‘ ( abs ‘ 𝑧 ) ) ) + π ) ≤ ( ( log ‘ 𝑅 ) + π ) )
94 39 54 27 56 93 letrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝑈 ) → ( abs ‘ ( log ‘ 𝑧 ) ) ≤ ( ( log ‘ 𝑅 ) + π ) )
95 39 27 35 94 leadd1dd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝑈 ) → ( ( abs ‘ ( log ‘ 𝑧 ) ) + ( abs ‘ ( ( log Γ ‘ 𝑧 ) + ( log ‘ 𝑧 ) ) ) ) ≤ ( ( ( log ‘ 𝑅 ) + π ) + ( abs ‘ ( ( log Γ ‘ 𝑧 ) + ( log ‘ 𝑧 ) ) ) ) )
96 22 40 36 49 95 letrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝑈 ) → ( abs ‘ ( log Γ ‘ 𝑧 ) ) ≤ ( ( ( log ‘ 𝑅 ) + π ) + ( abs ‘ ( ( log Γ ‘ 𝑧 ) + ( log ‘ 𝑧 ) ) ) ) )
97 96 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝑈 ) ∧ ( abs ‘ ( ( log Γ ‘ 𝑧 ) + ( log ‘ 𝑧 ) ) ) ≤ 𝑦 ) → ( abs ‘ ( log Γ ‘ 𝑧 ) ) ≤ ( ( ( log ‘ 𝑅 ) + π ) + ( abs ‘ ( ( log Γ ‘ 𝑧 ) + ( log ‘ 𝑧 ) ) ) ) )
98 35 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝑈 ) ∧ ( abs ‘ ( ( log Γ ‘ 𝑧 ) + ( log ‘ 𝑧 ) ) ) ≤ 𝑦 ) → ( abs ‘ ( ( log Γ ‘ 𝑧 ) + ( log ‘ 𝑧 ) ) ) ∈ ℝ )
99 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝑈 ) ∧ ( abs ‘ ( ( log Γ ‘ 𝑧 ) + ( log ‘ 𝑧 ) ) ) ≤ 𝑦 ) → 𝑦 ∈ ℝ )
100 27 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝑈 ) ∧ ( abs ‘ ( ( log Γ ‘ 𝑧 ) + ( log ‘ 𝑧 ) ) ) ≤ 𝑦 ) → ( ( log ‘ 𝑅 ) + π ) ∈ ℝ )
101 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝑈 ) ∧ ( abs ‘ ( ( log Γ ‘ 𝑧 ) + ( log ‘ 𝑧 ) ) ) ≤ 𝑦 ) → ( abs ‘ ( ( log Γ ‘ 𝑧 ) + ( log ‘ 𝑧 ) ) ) ≤ 𝑦 )
102 98 99 100 101 leadd2dd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝑈 ) ∧ ( abs ‘ ( ( log Γ ‘ 𝑧 ) + ( log ‘ 𝑧 ) ) ) ≤ 𝑦 ) → ( ( ( log ‘ 𝑅 ) + π ) + ( abs ‘ ( ( log Γ ‘ 𝑧 ) + ( log ‘ 𝑧 ) ) ) ) ≤ ( ( ( log ‘ 𝑅 ) + π ) + 𝑦 ) )
103 23 37 38 97 102 letrd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝑈 ) ∧ ( abs ‘ ( ( log Γ ‘ 𝑧 ) + ( log ‘ 𝑧 ) ) ) ≤ 𝑦 ) → ( abs ‘ ( log Γ ‘ 𝑧 ) ) ≤ ( ( ( log ‘ 𝑅 ) + π ) + 𝑦 ) )
104 103 ex ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝑈 ) → ( ( abs ‘ ( ( log Γ ‘ 𝑧 ) + ( log ‘ 𝑧 ) ) ) ≤ 𝑦 → ( abs ‘ ( log Γ ‘ 𝑧 ) ) ≤ ( ( ( log ‘ 𝑅 ) + π ) + 𝑦 ) ) )
105 104 ralimdva ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ∀ 𝑧 ∈ 𝑈 ( abs ‘ ( ( log Γ ‘ 𝑧 ) + ( log ‘ 𝑧 ) ) ) ≤ 𝑦 → ∀ 𝑧 ∈ 𝑈 ( abs ‘ ( log Γ ‘ 𝑧 ) ) ≤ ( ( ( log ‘ 𝑅 ) + π ) + 𝑦 ) ) )
106 105 impr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑈 ( abs ‘ ( ( log Γ ‘ 𝑧 ) + ( log ‘ 𝑧 ) ) ) ≤ 𝑦 ) ) → ∀ 𝑧 ∈ 𝑈 ( abs ‘ ( log Γ ‘ 𝑧 ) ) ≤ ( ( ( log ‘ 𝑅 ) + π ) + 𝑦 ) )
107 brralrspcev ⊢ ( ( ( ( ( log ‘ 𝑅 ) + π ) + 𝑦 ) ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑈 ( abs ‘ ( log Γ ‘ 𝑧 ) ) ≤ ( ( ( log ‘ 𝑅 ) + π ) + 𝑦 ) ) → ∃ 𝑟 ∈ ℝ ∀ 𝑧 ∈ 𝑈 ( abs ‘ ( log Γ ‘ 𝑧 ) ) ≤ 𝑟 )
108 18 106 107 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑈 ( abs ‘ ( ( log Γ ‘ 𝑧 ) + ( log ‘ 𝑧 ) ) ) ≤ 𝑦 ) ) → ∃ 𝑟 ∈ ℝ ∀ 𝑧 ∈ 𝑈 ( abs ‘ ( log Γ ‘ 𝑧 ) ) ≤ 𝑟 )
109 9 108 rexlimddv ⊢ ( 𝜑 → ∃ 𝑟 ∈ ℝ ∀ 𝑧 ∈ 𝑈 ( abs ‘ ( log Γ ‘ 𝑧 ) ) ≤ 𝑟 )