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 26183 |
. . . 4
⊢ (𝜑 → (∀𝑧 ∈ 𝑈 (log Γ‘𝑧) ∈ ℂ ∧ seq1(
∘f + , 𝐺)(⇝𝑢‘𝑈)(𝑧 ∈ 𝑈 ↦ ((log Γ‘𝑧) + (log‘𝑧))))) |
5 | 4 | simprd 496 |
. . 3
⊢ (𝜑 → seq1( ∘f
+ , 𝐺)(⇝𝑢‘𝑈)(𝑧 ∈ 𝑈 ↦ ((log Γ‘𝑧) + (log‘𝑧)))) |
6 | | eqid 2740 |
. . . . 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 26181 |
. . . 4
⊢ (𝜑 → (seq1( ∘f
+ , 𝐺) ∈ dom
(⇝𝑢‘𝑈) ∧ (seq1( ∘f + , 𝐺)(⇝𝑢‘𝑈)(𝑧 ∈ 𝑈 ↦ ((log Γ‘𝑧) + (log‘𝑧))) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝑈 (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦))) |
8 | 7 | simprd 496 |
. . 3
⊢ (𝜑 → (seq1( ∘f
+ , 𝐺)(⇝𝑢‘𝑈)(𝑧 ∈ 𝑈 ↦ ((log Γ‘𝑧) + (log‘𝑧))) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝑈 (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦)) |
9 | 5, 8 | mpd 15 |
. 2
⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝑈 (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦) |
10 | 1 | nnrpd 12769 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈
ℝ+) |
11 | 10 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑅 ∈
ℝ+) |
12 | 11 | relogcld 25776 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (log‘𝑅) ∈
ℝ) |
13 | | pire 25613 |
. . . . . . 7
⊢ π
∈ ℝ |
14 | 13 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → π ∈
ℝ) |
15 | 12, 14 | readdcld 11005 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((log‘𝑅) + π) ∈
ℝ) |
16 | | simpr 485 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ) |
17 | 15, 16 | readdcld 11005 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (((log‘𝑅) + π) + 𝑦) ∈ ℝ) |
18 | 17 | adantrr 714 |
. . 3
⊢ ((𝜑 ∧ (𝑦 ∈ ℝ ∧ ∀𝑧 ∈ 𝑈 (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦)) → (((log‘𝑅) + π) + 𝑦) ∈ ℝ) |
19 | 4 | simpld 495 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑧 ∈ 𝑈 (log Γ‘𝑧) ∈ ℂ) |
20 | 19 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ∀𝑧 ∈ 𝑈 (log Γ‘𝑧) ∈ ℂ) |
21 | 20 | r19.21bi 3135 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (log Γ‘𝑧) ∈
ℂ) |
22 | 21 | abscld 15146 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (abs‘(log Γ‘𝑧)) ∈
ℝ) |
23 | 22 | adantr 481 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) ∧ (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦) → (abs‘(log Γ‘𝑧)) ∈
ℝ) |
24 | 11 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → 𝑅 ∈
ℝ+) |
25 | 24 | relogcld 25776 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (log‘𝑅) ∈ ℝ) |
26 | 13 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → π ∈
ℝ) |
27 | 25, 26 | readdcld 11005 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → ((log‘𝑅) + π) ∈ ℝ) |
28 | 1, 2 | lgamgulmlem1 26176 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑈 ⊆ (ℂ ∖ (ℤ ∖
ℕ))) |
29 | 28 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑈 ⊆ (ℂ ∖ (ℤ ∖
ℕ))) |
30 | 29 | sselda 3926 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → 𝑧 ∈ (ℂ ∖ (ℤ ∖
ℕ))) |
31 | 30 | eldifad 3904 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → 𝑧 ∈ ℂ) |
32 | 30 | dmgmn0 26173 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → 𝑧 ≠ 0) |
33 | 31, 32 | logcld 25724 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (log‘𝑧) ∈ ℂ) |
34 | 21, 33 | addcld 10995 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → ((log Γ‘𝑧) + (log‘𝑧)) ∈
ℂ) |
35 | 34 | abscld 15146 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (abs‘((log
Γ‘𝑧) +
(log‘𝑧))) ∈
ℝ) |
36 | 27, 35 | readdcld 11005 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (((log‘𝑅) + π) + (abs‘((log
Γ‘𝑧) +
(log‘𝑧)))) ∈
ℝ) |
37 | 36 | adantr 481 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) ∧ (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦) → (((log‘𝑅) + π) + (abs‘((log
Γ‘𝑧) +
(log‘𝑧)))) ∈
ℝ) |
38 | 17 | ad2antrr 723 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) ∧ (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦) → (((log‘𝑅) + π) + 𝑦) ∈ ℝ) |
39 | 33 | abscld 15146 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (abs‘(log‘𝑧)) ∈
ℝ) |
40 | 39, 35 | readdcld 11005 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → ((abs‘(log‘𝑧)) + (abs‘((log
Γ‘𝑧) +
(log‘𝑧)))) ∈
ℝ) |
41 | 33 | negcld 11319 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → -(log‘𝑧) ∈ ℂ) |
42 | 21, 41 | abs2difd 15167 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → ((abs‘(log
Γ‘𝑧)) −
(abs‘-(log‘𝑧)))
≤ (abs‘((log Γ‘𝑧) − -(log‘𝑧)))) |
43 | 33 | absnegd 15159 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (abs‘-(log‘𝑧)) = (abs‘(log‘𝑧))) |
44 | 43 | oveq2d 7287 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → ((abs‘(log
Γ‘𝑧)) −
(abs‘-(log‘𝑧)))
= ((abs‘(log Γ‘𝑧)) − (abs‘(log‘𝑧)))) |
45 | 21, 33 | subnegd 11339 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → ((log Γ‘𝑧) − -(log‘𝑧)) = ((log Γ‘𝑧) + (log‘𝑧))) |
46 | 45 | fveq2d 6775 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (abs‘((log
Γ‘𝑧) −
-(log‘𝑧))) =
(abs‘((log Γ‘𝑧) + (log‘𝑧)))) |
47 | 42, 44, 46 | 3brtr3d 5110 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → ((abs‘(log
Γ‘𝑧)) −
(abs‘(log‘𝑧)))
≤ (abs‘((log Γ‘𝑧) + (log‘𝑧)))) |
48 | 22, 39, 35 | lesubadd2d 11574 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (((abs‘(log
Γ‘𝑧)) −
(abs‘(log‘𝑧)))
≤ (abs‘((log Γ‘𝑧) + (log‘𝑧))) ↔ (abs‘(log
Γ‘𝑧)) ≤
((abs‘(log‘𝑧))
+ (abs‘((log Γ‘𝑧) + (log‘𝑧)))))) |
49 | 47, 48 | mpbid 231 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (abs‘(log Γ‘𝑧)) ≤
((abs‘(log‘𝑧))
+ (abs‘((log Γ‘𝑧) + (log‘𝑧))))) |
50 | 31, 32 | absrpcld 15158 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (abs‘𝑧) ∈
ℝ+) |
51 | 50 | relogcld 25776 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (log‘(abs‘𝑧)) ∈
ℝ) |
52 | 51 | recnd 11004 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (log‘(abs‘𝑧)) ∈
ℂ) |
53 | 52 | abscld 15146 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) →
(abs‘(log‘(abs‘𝑧))) ∈ ℝ) |
54 | 53, 26 | readdcld 11005 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) →
((abs‘(log‘(abs‘𝑧))) + π) ∈ ℝ) |
55 | | abslogle 25771 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ ℂ ∧ 𝑧 ≠ 0) →
(abs‘(log‘𝑧))
≤ ((abs‘(log‘(abs‘𝑧))) + π)) |
56 | 31, 32, 55 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (abs‘(log‘𝑧)) ≤
((abs‘(log‘(abs‘𝑧))) + π)) |
57 | | df-neg 11208 |
. . . . . . . . . . . . . . . 16
⊢
-(log‘𝑅) = (0
− (log‘𝑅)) |
58 | | log1 25739 |
. . . . . . . . . . . . . . . . 17
⊢
(log‘1) = 0 |
59 | 58 | oveq1i 7281 |
. . . . . . . . . . . . . . . 16
⊢
((log‘1) − (log‘𝑅)) = (0 − (log‘𝑅)) |
60 | 57, 59 | eqtr4i 2771 |
. . . . . . . . . . . . . . 15
⊢
-(log‘𝑅) =
((log‘1) − (log‘𝑅)) |
61 | | 1rp 12733 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℝ+ |
62 | | relogdiv 25746 |
. . . . . . . . . . . . . . . 16
⊢ ((1
∈ ℝ+ ∧ 𝑅 ∈ ℝ+) →
(log‘(1 / 𝑅)) =
((log‘1) − (log‘𝑅))) |
63 | 61, 24, 62 | sylancr 587 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (log‘(1 / 𝑅)) = ((log‘1) − (log‘𝑅))) |
64 | 60, 63 | eqtr4id 2799 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → -(log‘𝑅) = (log‘(1 / 𝑅))) |
65 | | oveq2 7279 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 0 → (𝑧 + 𝑘) = (𝑧 + 0)) |
66 | 65 | fveq2d 6775 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 0 → (abs‘(𝑧 + 𝑘)) = (abs‘(𝑧 + 0))) |
67 | 66 | breq2d 5091 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 0 → ((1 / 𝑅) ≤ (abs‘(𝑧 + 𝑘)) ↔ (1 / 𝑅) ≤ (abs‘(𝑧 + 0)))) |
68 | | fveq2 6771 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑧 → (abs‘𝑥) = (abs‘𝑧)) |
69 | 68 | breq1d 5089 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑧 → ((abs‘𝑥) ≤ 𝑅 ↔ (abs‘𝑧) ≤ 𝑅)) |
70 | | fvoveq1 7294 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = 𝑧 → (abs‘(𝑥 + 𝑘)) = (abs‘(𝑧 + 𝑘))) |
71 | 70 | breq2d 5091 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑧 → ((1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)) ↔ (1 / 𝑅) ≤ (abs‘(𝑧 + 𝑘)))) |
72 | 71 | ralbidv 3123 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑧 → (∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)) ↔ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑧 + 𝑘)))) |
73 | 69, 72 | anbi12d 631 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑧 → (((abs‘𝑥) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘))) ↔ ((abs‘𝑧) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑧 + 𝑘))))) |
74 | 73, 2 | elrab2 3629 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ 𝑈 ↔ (𝑧 ∈ ℂ ∧ ((abs‘𝑧) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑧 + 𝑘))))) |
75 | 74 | simprbi 497 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ 𝑈 → ((abs‘𝑧) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑧 + 𝑘)))) |
76 | 75 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → ((abs‘𝑧) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑧 + 𝑘)))) |
77 | 76 | simprd 496 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑧 + 𝑘))) |
78 | | 0nn0 12248 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 ∈
ℕ0 |
79 | 78 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → 0 ∈
ℕ0) |
80 | 67, 77, 79 | rspcdva 3563 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (1 / 𝑅) ≤ (abs‘(𝑧 + 0))) |
81 | 31 | addid1d 11175 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (𝑧 + 0) = 𝑧) |
82 | 81 | fveq2d 6775 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (abs‘(𝑧 + 0)) = (abs‘𝑧)) |
83 | 80, 82 | breqtrd 5105 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (1 / 𝑅) ≤ (abs‘𝑧)) |
84 | 24 | rpreccld 12781 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (1 / 𝑅) ∈
ℝ+) |
85 | 84, 50 | logled 25780 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → ((1 / 𝑅) ≤ (abs‘𝑧) ↔ (log‘(1 / 𝑅)) ≤ (log‘(abs‘𝑧)))) |
86 | 83, 85 | mpbid 231 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (log‘(1 / 𝑅)) ≤ (log‘(abs‘𝑧))) |
87 | 64, 86 | eqbrtrd 5101 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → -(log‘𝑅) ≤ (log‘(abs‘𝑧))) |
88 | 76 | simpld 495 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (abs‘𝑧) ≤ 𝑅) |
89 | 50, 24 | logled 25780 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → ((abs‘𝑧) ≤ 𝑅 ↔ (log‘(abs‘𝑧)) ≤ (log‘𝑅))) |
90 | 88, 89 | mpbid 231 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (log‘(abs‘𝑧)) ≤ (log‘𝑅)) |
91 | 51, 25 | absled 15140 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) →
((abs‘(log‘(abs‘𝑧))) ≤ (log‘𝑅) ↔ (-(log‘𝑅) ≤ (log‘(abs‘𝑧)) ∧
(log‘(abs‘𝑧))
≤ (log‘𝑅)))) |
92 | 87, 90, 91 | mpbir2and 710 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) →
(abs‘(log‘(abs‘𝑧))) ≤ (log‘𝑅)) |
93 | 53, 25, 26, 92 | leadd1dd 11589 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) →
((abs‘(log‘(abs‘𝑧))) + π) ≤ ((log‘𝑅) + π)) |
94 | 39, 54, 27, 56, 93 | letrd 11132 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (abs‘(log‘𝑧)) ≤ ((log‘𝑅) + π)) |
95 | 39, 27, 35, 94 | leadd1dd 11589 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → ((abs‘(log‘𝑧)) + (abs‘((log
Γ‘𝑧) +
(log‘𝑧)))) ≤
(((log‘𝑅) + π) +
(abs‘((log Γ‘𝑧) + (log‘𝑧))))) |
96 | 22, 40, 36, 49, 95 | letrd 11132 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (abs‘(log Γ‘𝑧)) ≤ (((log‘𝑅) + π) + (abs‘((log
Γ‘𝑧) +
(log‘𝑧))))) |
97 | 96 | adantr 481 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) ∧ (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦) → (abs‘(log Γ‘𝑧)) ≤ (((log‘𝑅) + π) + (abs‘((log
Γ‘𝑧) +
(log‘𝑧))))) |
98 | 35 | adantr 481 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) ∧ (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦) → (abs‘((log Γ‘𝑧) + (log‘𝑧))) ∈
ℝ) |
99 | | simpllr 773 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) ∧ (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦) → 𝑦 ∈ ℝ) |
100 | 27 | adantr 481 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) ∧ (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦) → ((log‘𝑅) + π) ∈ ℝ) |
101 | | simpr 485 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) ∧ (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦) → (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦) |
102 | 98, 99, 100, 101 | leadd2dd 11590 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) ∧ (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦) → (((log‘𝑅) + π) + (abs‘((log
Γ‘𝑧) +
(log‘𝑧)))) ≤
(((log‘𝑅) + π) +
𝑦)) |
103 | 23, 37, 38, 97, 102 | letrd 11132 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) ∧ (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦) → (abs‘(log Γ‘𝑧)) ≤ (((log‘𝑅) + π) + 𝑦)) |
104 | 103 | ex 413 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → ((abs‘((log
Γ‘𝑧) +
(log‘𝑧))) ≤ 𝑦 → (abs‘(log
Γ‘𝑧)) ≤
(((log‘𝑅) + π) +
𝑦))) |
105 | 104 | ralimdva 3105 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (∀𝑧 ∈ 𝑈 (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦 → ∀𝑧 ∈ 𝑈 (abs‘(log Γ‘𝑧)) ≤ (((log‘𝑅) + π) + 𝑦))) |
106 | 105 | impr 455 |
. . 3
⊢ ((𝜑 ∧ (𝑦 ∈ ℝ ∧ ∀𝑧 ∈ 𝑈 (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦)) → ∀𝑧 ∈ 𝑈 (abs‘(log Γ‘𝑧)) ≤ (((log‘𝑅) + π) + 𝑦)) |
107 | | brralrspcev 5139 |
. . 3
⊢
(((((log‘𝑅) +
π) + 𝑦) ∈ ℝ
∧ ∀𝑧 ∈
𝑈 (abs‘(log
Γ‘𝑧)) ≤
(((log‘𝑅) + π) +
𝑦)) → ∃𝑟 ∈ ℝ ∀𝑧 ∈ 𝑈 (abs‘(log Γ‘𝑧)) ≤ 𝑟) |
108 | 18, 106, 107 | syl2anc 584 |
. 2
⊢ ((𝜑 ∧ (𝑦 ∈ ℝ ∧ ∀𝑧 ∈ 𝑈 (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦)) → ∃𝑟 ∈ ℝ ∀𝑧 ∈ 𝑈 (abs‘(log Γ‘𝑧)) ≤ 𝑟) |
109 | 9, 108 | rexlimddv 3222 |
1
⊢ (𝜑 → ∃𝑟 ∈ ℝ ∀𝑧 ∈ 𝑈 (abs‘(log Γ‘𝑧)) ≤ 𝑟) |