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 24562 |
. . . 4
⊢ (𝜑 → (∀𝑧 ∈ 𝑈 (log Γ‘𝑧) ∈ ℂ ∧ seq1(
∘𝑓 + , 𝐺)(⇝𝑢‘𝑈)(𝑧 ∈ 𝑈 ↦ ((log Γ‘𝑧) + (log‘𝑧))))) |
5 | 4 | simprd 478 |
. . 3
⊢ (𝜑 → seq1(
∘𝑓 + , 𝐺)(⇝𝑢‘𝑈)(𝑧 ∈ 𝑈 ↦ ((log Γ‘𝑧) + (log‘𝑧)))) |
6 | | eqid 2610 |
. . . . 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 24560 |
. . . 4
⊢ (𝜑 → (seq1(
∘𝑓 + , 𝐺) ∈ dom
(⇝𝑢‘𝑈) ∧ (seq1( ∘𝑓 +
, 𝐺)(⇝𝑢‘𝑈)(𝑧 ∈ 𝑈 ↦ ((log Γ‘𝑧) + (log‘𝑧))) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝑈 (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦))) |
8 | 7 | simprd 478 |
. . 3
⊢ (𝜑 → (seq1(
∘𝑓 + , 𝐺)(⇝𝑢‘𝑈)(𝑧 ∈ 𝑈 ↦ ((log Γ‘𝑧) + (log‘𝑧))) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝑈 (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦)) |
9 | 5, 8 | mpd 15 |
. 2
⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝑈 (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦) |
10 | 1 | nnrpd 11746 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈
ℝ+) |
11 | 10 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑅 ∈
ℝ+) |
12 | 11 | relogcld 24173 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (log‘𝑅) ∈
ℝ) |
13 | | pire 24014 |
. . . . . . 7
⊢ π
∈ ℝ |
14 | 13 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → π ∈
ℝ) |
15 | 12, 14 | readdcld 9948 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((log‘𝑅) + π) ∈
ℝ) |
16 | | simpr 476 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ) |
17 | 15, 16 | readdcld 9948 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (((log‘𝑅) + π) + 𝑦) ∈ ℝ) |
18 | 17 | adantrr 749 |
. . 3
⊢ ((𝜑 ∧ (𝑦 ∈ ℝ ∧ ∀𝑧 ∈ 𝑈 (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦)) → (((log‘𝑅) + π) + 𝑦) ∈ ℝ) |
19 | 4 | simpld 474 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑧 ∈ 𝑈 (log Γ‘𝑧) ∈ ℂ) |
20 | 19 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ∀𝑧 ∈ 𝑈 (log Γ‘𝑧) ∈ ℂ) |
21 | 20 | r19.21bi 2916 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (log Γ‘𝑧) ∈
ℂ) |
22 | 21 | abscld 14023 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (abs‘(log Γ‘𝑧)) ∈
ℝ) |
23 | 22 | adantr 480 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) ∧ (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦) → (abs‘(log Γ‘𝑧)) ∈
ℝ) |
24 | 11 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → 𝑅 ∈
ℝ+) |
25 | 24 | relogcld 24173 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (log‘𝑅) ∈ ℝ) |
26 | 13 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → π ∈
ℝ) |
27 | 25, 26 | readdcld 9948 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → ((log‘𝑅) + π) ∈ ℝ) |
28 | 1, 2 | lgamgulmlem1 24555 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑈 ⊆ (ℂ ∖ (ℤ ∖
ℕ))) |
29 | 28 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑈 ⊆ (ℂ ∖ (ℤ ∖
ℕ))) |
30 | 29 | sselda 3568 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → 𝑧 ∈ (ℂ ∖ (ℤ ∖
ℕ))) |
31 | 30 | eldifad 3552 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → 𝑧 ∈ ℂ) |
32 | 30 | dmgmn0 24552 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → 𝑧 ≠ 0) |
33 | 31, 32 | logcld 24121 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (log‘𝑧) ∈ ℂ) |
34 | 21, 33 | addcld 9938 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → ((log Γ‘𝑧) + (log‘𝑧)) ∈
ℂ) |
35 | 34 | abscld 14023 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (abs‘((log
Γ‘𝑧) +
(log‘𝑧))) ∈
ℝ) |
36 | 27, 35 | readdcld 9948 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (((log‘𝑅) + π) + (abs‘((log
Γ‘𝑧) +
(log‘𝑧)))) ∈
ℝ) |
37 | 36 | adantr 480 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) ∧ (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦) → (((log‘𝑅) + π) + (abs‘((log
Γ‘𝑧) +
(log‘𝑧)))) ∈
ℝ) |
38 | 17 | ad2antrr 758 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) ∧ (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦) → (((log‘𝑅) + π) + 𝑦) ∈ ℝ) |
39 | 33 | abscld 14023 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (abs‘(log‘𝑧)) ∈
ℝ) |
40 | 39, 35 | readdcld 9948 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → ((abs‘(log‘𝑧)) + (abs‘((log
Γ‘𝑧) +
(log‘𝑧)))) ∈
ℝ) |
41 | 33 | negcld 10258 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → -(log‘𝑧) ∈ ℂ) |
42 | 21, 41 | abs2difd 14044 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → ((abs‘(log
Γ‘𝑧)) −
(abs‘-(log‘𝑧)))
≤ (abs‘((log Γ‘𝑧) − -(log‘𝑧)))) |
43 | 33 | absnegd 14036 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (abs‘-(log‘𝑧)) = (abs‘(log‘𝑧))) |
44 | 43 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → ((abs‘(log
Γ‘𝑧)) −
(abs‘-(log‘𝑧)))
= ((abs‘(log Γ‘𝑧)) − (abs‘(log‘𝑧)))) |
45 | 21, 33 | subnegd 10278 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → ((log Γ‘𝑧) − -(log‘𝑧)) = ((log Γ‘𝑧) + (log‘𝑧))) |
46 | 45 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (abs‘((log
Γ‘𝑧) −
-(log‘𝑧))) =
(abs‘((log Γ‘𝑧) + (log‘𝑧)))) |
47 | 42, 44, 46 | 3brtr3d 4614 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → ((abs‘(log
Γ‘𝑧)) −
(abs‘(log‘𝑧)))
≤ (abs‘((log Γ‘𝑧) + (log‘𝑧)))) |
48 | 22, 39, 35 | lesubadd2d 10505 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (((abs‘(log
Γ‘𝑧)) −
(abs‘(log‘𝑧)))
≤ (abs‘((log Γ‘𝑧) + (log‘𝑧))) ↔ (abs‘(log
Γ‘𝑧)) ≤
((abs‘(log‘𝑧))
+ (abs‘((log Γ‘𝑧) + (log‘𝑧)))))) |
49 | 47, 48 | mpbid 221 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (abs‘(log Γ‘𝑧)) ≤
((abs‘(log‘𝑧))
+ (abs‘((log Γ‘𝑧) + (log‘𝑧))))) |
50 | 31, 32 | absrpcld 14035 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (abs‘𝑧) ∈
ℝ+) |
51 | 50 | relogcld 24173 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (log‘(abs‘𝑧)) ∈
ℝ) |
52 | 51 | recnd 9947 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (log‘(abs‘𝑧)) ∈
ℂ) |
53 | 52 | abscld 14023 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) →
(abs‘(log‘(abs‘𝑧))) ∈ ℝ) |
54 | 53, 26 | readdcld 9948 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) →
((abs‘(log‘(abs‘𝑧))) + π) ∈ ℝ) |
55 | | abslogle 24168 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ ℂ ∧ 𝑧 ≠ 0) →
(abs‘(log‘𝑧))
≤ ((abs‘(log‘(abs‘𝑧))) + π)) |
56 | 31, 32, 55 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (abs‘(log‘𝑧)) ≤
((abs‘(log‘(abs‘𝑧))) + π)) |
57 | | 1rp 11712 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℝ+ |
58 | | relogdiv 24143 |
. . . . . . . . . . . . . . . 16
⊢ ((1
∈ ℝ+ ∧ 𝑅 ∈ ℝ+) →
(log‘(1 / 𝑅)) =
((log‘1) − (log‘𝑅))) |
59 | 57, 24, 58 | sylancr 694 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (log‘(1 / 𝑅)) = ((log‘1) − (log‘𝑅))) |
60 | | df-neg 10148 |
. . . . . . . . . . . . . . . 16
⊢
-(log‘𝑅) = (0
− (log‘𝑅)) |
61 | | log1 24136 |
. . . . . . . . . . . . . . . . 17
⊢
(log‘1) = 0 |
62 | 61 | oveq1i 6559 |
. . . . . . . . . . . . . . . 16
⊢
((log‘1) − (log‘𝑅)) = (0 − (log‘𝑅)) |
63 | 60, 62 | eqtr4i 2635 |
. . . . . . . . . . . . . . 15
⊢
-(log‘𝑅) =
((log‘1) − (log‘𝑅)) |
64 | 59, 63 | syl6reqr 2663 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → -(log‘𝑅) = (log‘(1 / 𝑅))) |
65 | | 0nn0 11184 |
. . . . . . . . . . . . . . . . 17
⊢ 0 ∈
ℕ0 |
66 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑧 → (abs‘𝑥) = (abs‘𝑧)) |
67 | 66 | breq1d 4593 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑧 → ((abs‘𝑥) ≤ 𝑅 ↔ (abs‘𝑧) ≤ 𝑅)) |
68 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = 𝑧 → (𝑥 + 𝑘) = (𝑧 + 𝑘)) |
69 | 68 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = 𝑧 → (abs‘(𝑥 + 𝑘)) = (abs‘(𝑧 + 𝑘))) |
70 | 69 | breq2d 4595 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑧 → ((1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)) ↔ (1 / 𝑅) ≤ (abs‘(𝑧 + 𝑘)))) |
71 | 70 | ralbidv 2969 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑧 → (∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)) ↔ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑧 + 𝑘)))) |
72 | 67, 71 | anbi12d 743 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑧 → (((abs‘𝑥) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘))) ↔ ((abs‘𝑧) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑧 + 𝑘))))) |
73 | 72, 2 | elrab2 3333 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ 𝑈 ↔ (𝑧 ∈ ℂ ∧ ((abs‘𝑧) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑧 + 𝑘))))) |
74 | 73 | simprbi 479 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ 𝑈 → ((abs‘𝑧) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑧 + 𝑘)))) |
75 | 74 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → ((abs‘𝑧) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑧 + 𝑘)))) |
76 | 75 | simprd 478 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑧 + 𝑘))) |
77 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 0 → (𝑧 + 𝑘) = (𝑧 + 0)) |
78 | 77 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 0 → (abs‘(𝑧 + 𝑘)) = (abs‘(𝑧 + 0))) |
79 | 78 | breq2d 4595 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 0 → ((1 / 𝑅) ≤ (abs‘(𝑧 + 𝑘)) ↔ (1 / 𝑅) ≤ (abs‘(𝑧 + 0)))) |
80 | 79 | rspcv 3278 |
. . . . . . . . . . . . . . . . 17
⊢ (0 ∈
ℕ0 → (∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑧 + 𝑘)) → (1 / 𝑅) ≤ (abs‘(𝑧 + 0)))) |
81 | 65, 76, 80 | mpsyl 66 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (1 / 𝑅) ≤ (abs‘(𝑧 + 0))) |
82 | 31 | addid1d 10115 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (𝑧 + 0) = 𝑧) |
83 | 82 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (abs‘(𝑧 + 0)) = (abs‘𝑧)) |
84 | 81, 83 | breqtrd 4609 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (1 / 𝑅) ≤ (abs‘𝑧)) |
85 | 24 | rpreccld 11758 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (1 / 𝑅) ∈
ℝ+) |
86 | 85, 50 | logled 24177 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → ((1 / 𝑅) ≤ (abs‘𝑧) ↔ (log‘(1 / 𝑅)) ≤ (log‘(abs‘𝑧)))) |
87 | 84, 86 | mpbid 221 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (log‘(1 / 𝑅)) ≤ (log‘(abs‘𝑧))) |
88 | 64, 87 | eqbrtrd 4605 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → -(log‘𝑅) ≤ (log‘(abs‘𝑧))) |
89 | 75 | simpld 474 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (abs‘𝑧) ≤ 𝑅) |
90 | 50, 24 | logled 24177 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → ((abs‘𝑧) ≤ 𝑅 ↔ (log‘(abs‘𝑧)) ≤ (log‘𝑅))) |
91 | 89, 90 | mpbid 221 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (log‘(abs‘𝑧)) ≤ (log‘𝑅)) |
92 | 51, 25 | absled 14017 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) →
((abs‘(log‘(abs‘𝑧))) ≤ (log‘𝑅) ↔ (-(log‘𝑅) ≤ (log‘(abs‘𝑧)) ∧
(log‘(abs‘𝑧))
≤ (log‘𝑅)))) |
93 | 88, 91, 92 | mpbir2and 959 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) →
(abs‘(log‘(abs‘𝑧))) ≤ (log‘𝑅)) |
94 | 53, 25, 26, 93 | leadd1dd 10520 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) →
((abs‘(log‘(abs‘𝑧))) + π) ≤ ((log‘𝑅) + π)) |
95 | 39, 54, 27, 56, 94 | letrd 10073 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (abs‘(log‘𝑧)) ≤ ((log‘𝑅) + π)) |
96 | 39, 27, 35, 95 | leadd1dd 10520 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → ((abs‘(log‘𝑧)) + (abs‘((log
Γ‘𝑧) +
(log‘𝑧)))) ≤
(((log‘𝑅) + π) +
(abs‘((log Γ‘𝑧) + (log‘𝑧))))) |
97 | 22, 40, 36, 49, 96 | letrd 10073 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (abs‘(log Γ‘𝑧)) ≤ (((log‘𝑅) + π) + (abs‘((log
Γ‘𝑧) +
(log‘𝑧))))) |
98 | 97 | adantr 480 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) ∧ (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦) → (abs‘(log Γ‘𝑧)) ≤ (((log‘𝑅) + π) + (abs‘((log
Γ‘𝑧) +
(log‘𝑧))))) |
99 | 35 | adantr 480 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) ∧ (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦) → (abs‘((log Γ‘𝑧) + (log‘𝑧))) ∈
ℝ) |
100 | | simpllr 795 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) ∧ (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦) → 𝑦 ∈ ℝ) |
101 | 27 | adantr 480 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) ∧ (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦) → ((log‘𝑅) + π) ∈ ℝ) |
102 | | simpr 476 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) ∧ (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦) → (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦) |
103 | 99, 100, 101, 102 | leadd2dd 10521 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) ∧ (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦) → (((log‘𝑅) + π) + (abs‘((log
Γ‘𝑧) +
(log‘𝑧)))) ≤
(((log‘𝑅) + π) +
𝑦)) |
104 | 23, 37, 38, 98, 103 | letrd 10073 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) ∧ (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦) → (abs‘(log Γ‘𝑧)) ≤ (((log‘𝑅) + π) + 𝑦)) |
105 | 104 | ex 449 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → ((abs‘((log
Γ‘𝑧) +
(log‘𝑧))) ≤ 𝑦 → (abs‘(log
Γ‘𝑧)) ≤
(((log‘𝑅) + π) +
𝑦))) |
106 | 105 | ralimdva 2945 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (∀𝑧 ∈ 𝑈 (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦 → ∀𝑧 ∈ 𝑈 (abs‘(log Γ‘𝑧)) ≤ (((log‘𝑅) + π) + 𝑦))) |
107 | 106 | impr 647 |
. . 3
⊢ ((𝜑 ∧ (𝑦 ∈ ℝ ∧ ∀𝑧 ∈ 𝑈 (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦)) → ∀𝑧 ∈ 𝑈 (abs‘(log Γ‘𝑧)) ≤ (((log‘𝑅) + π) + 𝑦)) |
108 | | breq2 4587 |
. . . . 5
⊢ (𝑟 = (((log‘𝑅) + π) + 𝑦) → ((abs‘(log Γ‘𝑧)) ≤ 𝑟 ↔ (abs‘(log Γ‘𝑧)) ≤ (((log‘𝑅) + π) + 𝑦))) |
109 | 108 | ralbidv 2969 |
. . . 4
⊢ (𝑟 = (((log‘𝑅) + π) + 𝑦) → (∀𝑧 ∈ 𝑈 (abs‘(log Γ‘𝑧)) ≤ 𝑟 ↔ ∀𝑧 ∈ 𝑈 (abs‘(log Γ‘𝑧)) ≤ (((log‘𝑅) + π) + 𝑦))) |
110 | 109 | rspcev 3282 |
. . 3
⊢
(((((log‘𝑅) +
π) + 𝑦) ∈ ℝ
∧ ∀𝑧 ∈
𝑈 (abs‘(log
Γ‘𝑧)) ≤
(((log‘𝑅) + π) +
𝑦)) → ∃𝑟 ∈ ℝ ∀𝑧 ∈ 𝑈 (abs‘(log Γ‘𝑧)) ≤ 𝑟) |
111 | 18, 107, 110 | syl2anc 691 |
. 2
⊢ ((𝜑 ∧ (𝑦 ∈ ℝ ∧ ∀𝑧 ∈ 𝑈 (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦)) → ∃𝑟 ∈ ℝ ∀𝑧 ∈ 𝑈 (abs‘(log Γ‘𝑧)) ≤ 𝑟) |
112 | 9, 111 | rexlimddv 3017 |
1
⊢ (𝜑 → ∃𝑟 ∈ ℝ ∀𝑧 ∈ 𝑈 (abs‘(log Γ‘𝑧)) ≤ 𝑟) |