| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | lgamgulm.r | . . . . 5
⊢ (𝜑 → 𝑅 ∈ ℕ) | 
| 2 |  | lgamgulm.u | . . . . 5
⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)))} | 
| 3 |  | lgamgulm.g | . . . . 5
⊢ 𝐺 = (𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))))) | 
| 4 | 1, 2, 3 | lgamgulm2 27080 | . . . 4
⊢ (𝜑 → (∀𝑧 ∈ 𝑈 (log Γ‘𝑧) ∈ ℂ ∧ seq1(
∘f + , 𝐺)(⇝𝑢‘𝑈)(𝑧 ∈ 𝑈 ↦ ((log Γ‘𝑧) + (log‘𝑧))))) | 
| 5 | 4 | simprd 495 | . . 3
⊢ (𝜑 → seq1( ∘f
+ , 𝐺)(⇝𝑢‘𝑈)(𝑧 ∈ 𝑈 ↦ ((log Γ‘𝑧) + (log‘𝑧)))) | 
| 6 |  | eqid 2736 | . . . . 5
⊢ (𝑚 ∈ ℕ ↦ if((2
· 𝑅) ≤ 𝑚, (𝑅 · ((2 · (𝑅 + 1)) / (𝑚↑2))), ((𝑅 · (log‘((𝑚 + 1) / 𝑚))) + ((log‘((𝑅 + 1) · 𝑚)) + π)))) = (𝑚 ∈ ℕ ↦ if((2 · 𝑅) ≤ 𝑚, (𝑅 · ((2 · (𝑅 + 1)) / (𝑚↑2))), ((𝑅 · (log‘((𝑚 + 1) / 𝑚))) + ((log‘((𝑅 + 1) · 𝑚)) + π)))) | 
| 7 | 1, 2, 3, 6 | lgamgulmlem6 27078 | . . . 4
⊢ (𝜑 → (seq1( ∘f
+ , 𝐺) ∈ dom
(⇝𝑢‘𝑈) ∧ (seq1( ∘f + , 𝐺)(⇝𝑢‘𝑈)(𝑧 ∈ 𝑈 ↦ ((log Γ‘𝑧) + (log‘𝑧))) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝑈 (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦))) | 
| 8 | 7 | simprd 495 | . . 3
⊢ (𝜑 → (seq1( ∘f
+ , 𝐺)(⇝𝑢‘𝑈)(𝑧 ∈ 𝑈 ↦ ((log Γ‘𝑧) + (log‘𝑧))) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝑈 (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦)) | 
| 9 | 5, 8 | mpd 15 | . 2
⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝑈 (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦) | 
| 10 | 1 | nnrpd 13076 | . . . . . . . 8
⊢ (𝜑 → 𝑅 ∈
ℝ+) | 
| 11 | 10 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑅 ∈
ℝ+) | 
| 12 | 11 | relogcld 26666 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (log‘𝑅) ∈
ℝ) | 
| 13 |  | pire 26501 | . . . . . . 7
⊢ π
∈ ℝ | 
| 14 | 13 | a1i 11 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → π ∈
ℝ) | 
| 15 | 12, 14 | readdcld 11291 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((log‘𝑅) + π) ∈
ℝ) | 
| 16 |  | simpr 484 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ) | 
| 17 | 15, 16 | readdcld 11291 | . . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (((log‘𝑅) + π) + 𝑦) ∈ ℝ) | 
| 18 | 17 | adantrr 717 | . . 3
⊢ ((𝜑 ∧ (𝑦 ∈ ℝ ∧ ∀𝑧 ∈ 𝑈 (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦)) → (((log‘𝑅) + π) + 𝑦) ∈ ℝ) | 
| 19 | 4 | simpld 494 | . . . . . . . . . . 11
⊢ (𝜑 → ∀𝑧 ∈ 𝑈 (log Γ‘𝑧) ∈ ℂ) | 
| 20 | 19 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ∀𝑧 ∈ 𝑈 (log Γ‘𝑧) ∈ ℂ) | 
| 21 | 20 | r19.21bi 3250 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (log Γ‘𝑧) ∈
ℂ) | 
| 22 | 21 | abscld 15476 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (abs‘(log Γ‘𝑧)) ∈
ℝ) | 
| 23 | 22 | adantr 480 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) ∧ (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦) → (abs‘(log Γ‘𝑧)) ∈
ℝ) | 
| 24 | 11 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → 𝑅 ∈
ℝ+) | 
| 25 | 24 | relogcld 26666 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (log‘𝑅) ∈ ℝ) | 
| 26 | 13 | a1i 11 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → π ∈
ℝ) | 
| 27 | 25, 26 | readdcld 11291 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → ((log‘𝑅) + π) ∈ ℝ) | 
| 28 | 1, 2 | lgamgulmlem1 27073 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑈 ⊆ (ℂ ∖ (ℤ ∖
ℕ))) | 
| 29 | 28 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑈 ⊆ (ℂ ∖ (ℤ ∖
ℕ))) | 
| 30 | 29 | sselda 3982 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → 𝑧 ∈ (ℂ ∖ (ℤ ∖
ℕ))) | 
| 31 | 30 | eldifad 3962 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → 𝑧 ∈ ℂ) | 
| 32 | 30 | dmgmn0 27070 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → 𝑧 ≠ 0) | 
| 33 | 31, 32 | logcld 26613 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (log‘𝑧) ∈ ℂ) | 
| 34 | 21, 33 | addcld 11281 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → ((log Γ‘𝑧) + (log‘𝑧)) ∈
ℂ) | 
| 35 | 34 | abscld 15476 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (abs‘((log
Γ‘𝑧) +
(log‘𝑧))) ∈
ℝ) | 
| 36 | 27, 35 | readdcld 11291 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (((log‘𝑅) + π) + (abs‘((log
Γ‘𝑧) +
(log‘𝑧)))) ∈
ℝ) | 
| 37 | 36 | adantr 480 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) ∧ (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦) → (((log‘𝑅) + π) + (abs‘((log
Γ‘𝑧) +
(log‘𝑧)))) ∈
ℝ) | 
| 38 | 17 | ad2antrr 726 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) ∧ (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦) → (((log‘𝑅) + π) + 𝑦) ∈ ℝ) | 
| 39 | 33 | abscld 15476 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (abs‘(log‘𝑧)) ∈
ℝ) | 
| 40 | 39, 35 | readdcld 11291 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → ((abs‘(log‘𝑧)) + (abs‘((log
Γ‘𝑧) +
(log‘𝑧)))) ∈
ℝ) | 
| 41 | 33 | negcld 11608 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → -(log‘𝑧) ∈ ℂ) | 
| 42 | 21, 41 | abs2difd 15497 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → ((abs‘(log
Γ‘𝑧)) −
(abs‘-(log‘𝑧)))
≤ (abs‘((log Γ‘𝑧) − -(log‘𝑧)))) | 
| 43 | 33 | absnegd 15489 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (abs‘-(log‘𝑧)) = (abs‘(log‘𝑧))) | 
| 44 | 43 | oveq2d 7448 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → ((abs‘(log
Γ‘𝑧)) −
(abs‘-(log‘𝑧)))
= ((abs‘(log Γ‘𝑧)) − (abs‘(log‘𝑧)))) | 
| 45 | 21, 33 | subnegd 11628 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → ((log Γ‘𝑧) − -(log‘𝑧)) = ((log Γ‘𝑧) + (log‘𝑧))) | 
| 46 | 45 | fveq2d 6909 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (abs‘((log
Γ‘𝑧) −
-(log‘𝑧))) =
(abs‘((log Γ‘𝑧) + (log‘𝑧)))) | 
| 47 | 42, 44, 46 | 3brtr3d 5173 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → ((abs‘(log
Γ‘𝑧)) −
(abs‘(log‘𝑧)))
≤ (abs‘((log Γ‘𝑧) + (log‘𝑧)))) | 
| 48 | 22, 39, 35 | lesubadd2d 11863 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (((abs‘(log
Γ‘𝑧)) −
(abs‘(log‘𝑧)))
≤ (abs‘((log Γ‘𝑧) + (log‘𝑧))) ↔ (abs‘(log
Γ‘𝑧)) ≤
((abs‘(log‘𝑧))
+ (abs‘((log Γ‘𝑧) + (log‘𝑧)))))) | 
| 49 | 47, 48 | mpbid 232 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (abs‘(log Γ‘𝑧)) ≤
((abs‘(log‘𝑧))
+ (abs‘((log Γ‘𝑧) + (log‘𝑧))))) | 
| 50 | 31, 32 | absrpcld 15488 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (abs‘𝑧) ∈
ℝ+) | 
| 51 | 50 | relogcld 26666 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (log‘(abs‘𝑧)) ∈
ℝ) | 
| 52 | 51 | recnd 11290 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (log‘(abs‘𝑧)) ∈
ℂ) | 
| 53 | 52 | abscld 15476 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) →
(abs‘(log‘(abs‘𝑧))) ∈ ℝ) | 
| 54 | 53, 26 | readdcld 11291 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) →
((abs‘(log‘(abs‘𝑧))) + π) ∈ ℝ) | 
| 55 |  | abslogle 26661 | . . . . . . . . . . . 12
⊢ ((𝑧 ∈ ℂ ∧ 𝑧 ≠ 0) →
(abs‘(log‘𝑧))
≤ ((abs‘(log‘(abs‘𝑧))) + π)) | 
| 56 | 31, 32, 55 | syl2anc 584 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (abs‘(log‘𝑧)) ≤
((abs‘(log‘(abs‘𝑧))) + π)) | 
| 57 |  | df-neg 11496 | . . . . . . . . . . . . . . . 16
⊢
-(log‘𝑅) = (0
− (log‘𝑅)) | 
| 58 |  | log1 26628 | . . . . . . . . . . . . . . . . 17
⊢
(log‘1) = 0 | 
| 59 | 58 | oveq1i 7442 | . . . . . . . . . . . . . . . 16
⊢
((log‘1) − (log‘𝑅)) = (0 − (log‘𝑅)) | 
| 60 | 57, 59 | eqtr4i 2767 | . . . . . . . . . . . . . . 15
⊢
-(log‘𝑅) =
((log‘1) − (log‘𝑅)) | 
| 61 |  | 1rp 13039 | . . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℝ+ | 
| 62 |  | relogdiv 26636 | . . . . . . . . . . . . . . . 16
⊢ ((1
∈ ℝ+ ∧ 𝑅 ∈ ℝ+) →
(log‘(1 / 𝑅)) =
((log‘1) − (log‘𝑅))) | 
| 63 | 61, 24, 62 | sylancr 587 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (log‘(1 / 𝑅)) = ((log‘1) − (log‘𝑅))) | 
| 64 | 60, 63 | eqtr4id 2795 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → -(log‘𝑅) = (log‘(1 / 𝑅))) | 
| 65 |  | oveq2 7440 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 0 → (𝑧 + 𝑘) = (𝑧 + 0)) | 
| 66 | 65 | fveq2d 6909 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 0 → (abs‘(𝑧 + 𝑘)) = (abs‘(𝑧 + 0))) | 
| 67 | 66 | breq2d 5154 | . . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 0 → ((1 / 𝑅) ≤ (abs‘(𝑧 + 𝑘)) ↔ (1 / 𝑅) ≤ (abs‘(𝑧 + 0)))) | 
| 68 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑧 → (abs‘𝑥) = (abs‘𝑧)) | 
| 69 | 68 | breq1d 5152 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑧 → ((abs‘𝑥) ≤ 𝑅 ↔ (abs‘𝑧) ≤ 𝑅)) | 
| 70 |  | fvoveq1 7455 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = 𝑧 → (abs‘(𝑥 + 𝑘)) = (abs‘(𝑧 + 𝑘))) | 
| 71 | 70 | breq2d 5154 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑧 → ((1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)) ↔ (1 / 𝑅) ≤ (abs‘(𝑧 + 𝑘)))) | 
| 72 | 71 | ralbidv 3177 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑧 → (∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)) ↔ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑧 + 𝑘)))) | 
| 73 | 69, 72 | anbi12d 632 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑧 → (((abs‘𝑥) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘))) ↔ ((abs‘𝑧) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑧 + 𝑘))))) | 
| 74 | 73, 2 | elrab2 3694 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ 𝑈 ↔ (𝑧 ∈ ℂ ∧ ((abs‘𝑧) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑧 + 𝑘))))) | 
| 75 | 74 | simprbi 496 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ 𝑈 → ((abs‘𝑧) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑧 + 𝑘)))) | 
| 76 | 75 | adantl 481 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → ((abs‘𝑧) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑧 + 𝑘)))) | 
| 77 | 76 | simprd 495 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑧 + 𝑘))) | 
| 78 |  | 0nn0 12543 | . . . . . . . . . . . . . . . . . 18
⊢ 0 ∈
ℕ0 | 
| 79 | 78 | a1i 11 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → 0 ∈
ℕ0) | 
| 80 | 67, 77, 79 | rspcdva 3622 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (1 / 𝑅) ≤ (abs‘(𝑧 + 0))) | 
| 81 | 31 | addridd 11462 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (𝑧 + 0) = 𝑧) | 
| 82 | 81 | fveq2d 6909 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (abs‘(𝑧 + 0)) = (abs‘𝑧)) | 
| 83 | 80, 82 | breqtrd 5168 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (1 / 𝑅) ≤ (abs‘𝑧)) | 
| 84 | 24 | rpreccld 13088 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (1 / 𝑅) ∈
ℝ+) | 
| 85 | 84, 50 | logled 26670 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → ((1 / 𝑅) ≤ (abs‘𝑧) ↔ (log‘(1 / 𝑅)) ≤ (log‘(abs‘𝑧)))) | 
| 86 | 83, 85 | mpbid 232 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (log‘(1 / 𝑅)) ≤ (log‘(abs‘𝑧))) | 
| 87 | 64, 86 | eqbrtrd 5164 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → -(log‘𝑅) ≤ (log‘(abs‘𝑧))) | 
| 88 | 76 | simpld 494 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (abs‘𝑧) ≤ 𝑅) | 
| 89 | 50, 24 | logled 26670 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → ((abs‘𝑧) ≤ 𝑅 ↔ (log‘(abs‘𝑧)) ≤ (log‘𝑅))) | 
| 90 | 88, 89 | mpbid 232 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (log‘(abs‘𝑧)) ≤ (log‘𝑅)) | 
| 91 | 51, 25 | absled 15470 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) →
((abs‘(log‘(abs‘𝑧))) ≤ (log‘𝑅) ↔ (-(log‘𝑅) ≤ (log‘(abs‘𝑧)) ∧
(log‘(abs‘𝑧))
≤ (log‘𝑅)))) | 
| 92 | 87, 90, 91 | mpbir2and 713 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) →
(abs‘(log‘(abs‘𝑧))) ≤ (log‘𝑅)) | 
| 93 | 53, 25, 26, 92 | leadd1dd 11878 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) →
((abs‘(log‘(abs‘𝑧))) + π) ≤ ((log‘𝑅) + π)) | 
| 94 | 39, 54, 27, 56, 93 | letrd 11419 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (abs‘(log‘𝑧)) ≤ ((log‘𝑅) + π)) | 
| 95 | 39, 27, 35, 94 | leadd1dd 11878 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → ((abs‘(log‘𝑧)) + (abs‘((log
Γ‘𝑧) +
(log‘𝑧)))) ≤
(((log‘𝑅) + π) +
(abs‘((log Γ‘𝑧) + (log‘𝑧))))) | 
| 96 | 22, 40, 36, 49, 95 | letrd 11419 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (abs‘(log Γ‘𝑧)) ≤ (((log‘𝑅) + π) + (abs‘((log
Γ‘𝑧) +
(log‘𝑧))))) | 
| 97 | 96 | adantr 480 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) ∧ (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦) → (abs‘(log Γ‘𝑧)) ≤ (((log‘𝑅) + π) + (abs‘((log
Γ‘𝑧) +
(log‘𝑧))))) | 
| 98 | 35 | adantr 480 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) ∧ (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦) → (abs‘((log Γ‘𝑧) + (log‘𝑧))) ∈
ℝ) | 
| 99 |  | simpllr 775 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) ∧ (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦) → 𝑦 ∈ ℝ) | 
| 100 | 27 | adantr 480 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) ∧ (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦) → ((log‘𝑅) + π) ∈ ℝ) | 
| 101 |  | simpr 484 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) ∧ (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦) → (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦) | 
| 102 | 98, 99, 100, 101 | leadd2dd 11879 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) ∧ (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦) → (((log‘𝑅) + π) + (abs‘((log
Γ‘𝑧) +
(log‘𝑧)))) ≤
(((log‘𝑅) + π) +
𝑦)) | 
| 103 | 23, 37, 38, 97, 102 | letrd 11419 | . . . . . 6
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) ∧ (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦) → (abs‘(log Γ‘𝑧)) ≤ (((log‘𝑅) + π) + 𝑦)) | 
| 104 | 103 | ex 412 | . . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → ((abs‘((log
Γ‘𝑧) +
(log‘𝑧))) ≤ 𝑦 → (abs‘(log
Γ‘𝑧)) ≤
(((log‘𝑅) + π) +
𝑦))) | 
| 105 | 104 | ralimdva 3166 | . . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (∀𝑧 ∈ 𝑈 (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦 → ∀𝑧 ∈ 𝑈 (abs‘(log Γ‘𝑧)) ≤ (((log‘𝑅) + π) + 𝑦))) | 
| 106 | 105 | impr 454 | . . 3
⊢ ((𝜑 ∧ (𝑦 ∈ ℝ ∧ ∀𝑧 ∈ 𝑈 (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦)) → ∀𝑧 ∈ 𝑈 (abs‘(log Γ‘𝑧)) ≤ (((log‘𝑅) + π) + 𝑦)) | 
| 107 |  | brralrspcev 5202 | . . 3
⊢
(((((log‘𝑅) +
π) + 𝑦) ∈ ℝ
∧ ∀𝑧 ∈
𝑈 (abs‘(log
Γ‘𝑧)) ≤
(((log‘𝑅) + π) +
𝑦)) → ∃𝑟 ∈ ℝ ∀𝑧 ∈ 𝑈 (abs‘(log Γ‘𝑧)) ≤ 𝑟) | 
| 108 | 18, 106, 107 | syl2anc 584 | . 2
⊢ ((𝜑 ∧ (𝑦 ∈ ℝ ∧ ∀𝑧 ∈ 𝑈 (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦)) → ∃𝑟 ∈ ℝ ∀𝑧 ∈ 𝑈 (abs‘(log Γ‘𝑧)) ≤ 𝑟) | 
| 109 | 9, 108 | rexlimddv 3160 | 1
⊢ (𝜑 → ∃𝑟 ∈ ℝ ∀𝑧 ∈ 𝑈 (abs‘(log Γ‘𝑧)) ≤ 𝑟) |