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 25305 |
. . . 4
⊢ (𝜑 → (∀𝑧 ∈ 𝑈 (log Γ‘𝑧) ∈ ℂ ∧ seq1(
∘𝑓 + , 𝐺)(⇝𝑢‘𝑈)(𝑧 ∈ 𝑈 ↦ ((log Γ‘𝑧) + (log‘𝑧))))) |
5 | 4 | simprd 488 |
. . 3
⊢ (𝜑 → seq1(
∘𝑓 + , 𝐺)(⇝𝑢‘𝑈)(𝑧 ∈ 𝑈 ↦ ((log Γ‘𝑧) + (log‘𝑧)))) |
6 | | eqid 2772 |
. . . . 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 25303 |
. . . 4
⊢ (𝜑 → (seq1(
∘𝑓 + , 𝐺) ∈ dom
(⇝𝑢‘𝑈) ∧ (seq1( ∘𝑓 +
, 𝐺)(⇝𝑢‘𝑈)(𝑧 ∈ 𝑈 ↦ ((log Γ‘𝑧) + (log‘𝑧))) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝑈 (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦))) |
8 | 7 | simprd 488 |
. . 3
⊢ (𝜑 → (seq1(
∘𝑓 + , 𝐺)(⇝𝑢‘𝑈)(𝑧 ∈ 𝑈 ↦ ((log Γ‘𝑧) + (log‘𝑧))) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝑈 (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦)) |
9 | 5, 8 | mpd 15 |
. 2
⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝑈 (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦) |
10 | 1 | nnrpd 12239 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈
ℝ+) |
11 | 10 | adantr 473 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑅 ∈
ℝ+) |
12 | 11 | relogcld 24897 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (log‘𝑅) ∈
ℝ) |
13 | | pire 24737 |
. . . . . . 7
⊢ π
∈ ℝ |
14 | 13 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → π ∈
ℝ) |
15 | 12, 14 | readdcld 10461 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((log‘𝑅) + π) ∈
ℝ) |
16 | | simpr 477 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ) |
17 | 15, 16 | readdcld 10461 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (((log‘𝑅) + π) + 𝑦) ∈ ℝ) |
18 | 17 | adantrr 704 |
. . 3
⊢ ((𝜑 ∧ (𝑦 ∈ ℝ ∧ ∀𝑧 ∈ 𝑈 (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦)) → (((log‘𝑅) + π) + 𝑦) ∈ ℝ) |
19 | 4 | simpld 487 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑧 ∈ 𝑈 (log Γ‘𝑧) ∈ ℂ) |
20 | 19 | adantr 473 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ∀𝑧 ∈ 𝑈 (log Γ‘𝑧) ∈ ℂ) |
21 | 20 | r19.21bi 3152 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (log Γ‘𝑧) ∈
ℂ) |
22 | 21 | abscld 14647 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (abs‘(log Γ‘𝑧)) ∈
ℝ) |
23 | 22 | adantr 473 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) ∧ (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦) → (abs‘(log Γ‘𝑧)) ∈
ℝ) |
24 | 11 | adantr 473 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → 𝑅 ∈
ℝ+) |
25 | 24 | relogcld 24897 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (log‘𝑅) ∈ ℝ) |
26 | 13 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → π ∈
ℝ) |
27 | 25, 26 | readdcld 10461 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → ((log‘𝑅) + π) ∈ ℝ) |
28 | 1, 2 | lgamgulmlem1 25298 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑈 ⊆ (ℂ ∖ (ℤ ∖
ℕ))) |
29 | 28 | adantr 473 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑈 ⊆ (ℂ ∖ (ℤ ∖
ℕ))) |
30 | 29 | sselda 3854 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → 𝑧 ∈ (ℂ ∖ (ℤ ∖
ℕ))) |
31 | 30 | eldifad 3837 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → 𝑧 ∈ ℂ) |
32 | 30 | dmgmn0 25295 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → 𝑧 ≠ 0) |
33 | 31, 32 | logcld 24845 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (log‘𝑧) ∈ ℂ) |
34 | 21, 33 | addcld 10451 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → ((log Γ‘𝑧) + (log‘𝑧)) ∈
ℂ) |
35 | 34 | abscld 14647 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (abs‘((log
Γ‘𝑧) +
(log‘𝑧))) ∈
ℝ) |
36 | 27, 35 | readdcld 10461 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (((log‘𝑅) + π) + (abs‘((log
Γ‘𝑧) +
(log‘𝑧)))) ∈
ℝ) |
37 | 36 | adantr 473 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) ∧ (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦) → (((log‘𝑅) + π) + (abs‘((log
Γ‘𝑧) +
(log‘𝑧)))) ∈
ℝ) |
38 | 17 | ad2antrr 713 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) ∧ (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦) → (((log‘𝑅) + π) + 𝑦) ∈ ℝ) |
39 | 33 | abscld 14647 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (abs‘(log‘𝑧)) ∈
ℝ) |
40 | 39, 35 | readdcld 10461 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → ((abs‘(log‘𝑧)) + (abs‘((log
Γ‘𝑧) +
(log‘𝑧)))) ∈
ℝ) |
41 | 33 | negcld 10777 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → -(log‘𝑧) ∈ ℂ) |
42 | 21, 41 | abs2difd 14668 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → ((abs‘(log
Γ‘𝑧)) −
(abs‘-(log‘𝑧)))
≤ (abs‘((log Γ‘𝑧) − -(log‘𝑧)))) |
43 | 33 | absnegd 14660 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (abs‘-(log‘𝑧)) = (abs‘(log‘𝑧))) |
44 | 43 | oveq2d 6986 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → ((abs‘(log
Γ‘𝑧)) −
(abs‘-(log‘𝑧)))
= ((abs‘(log Γ‘𝑧)) − (abs‘(log‘𝑧)))) |
45 | 21, 33 | subnegd 10797 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → ((log Γ‘𝑧) − -(log‘𝑧)) = ((log Γ‘𝑧) + (log‘𝑧))) |
46 | 45 | fveq2d 6497 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (abs‘((log
Γ‘𝑧) −
-(log‘𝑧))) =
(abs‘((log Γ‘𝑧) + (log‘𝑧)))) |
47 | 42, 44, 46 | 3brtr3d 4954 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → ((abs‘(log
Γ‘𝑧)) −
(abs‘(log‘𝑧)))
≤ (abs‘((log Γ‘𝑧) + (log‘𝑧)))) |
48 | 22, 39, 35 | lesubadd2d 11032 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (((abs‘(log
Γ‘𝑧)) −
(abs‘(log‘𝑧)))
≤ (abs‘((log Γ‘𝑧) + (log‘𝑧))) ↔ (abs‘(log
Γ‘𝑧)) ≤
((abs‘(log‘𝑧))
+ (abs‘((log Γ‘𝑧) + (log‘𝑧)))))) |
49 | 47, 48 | mpbid 224 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (abs‘(log Γ‘𝑧)) ≤
((abs‘(log‘𝑧))
+ (abs‘((log Γ‘𝑧) + (log‘𝑧))))) |
50 | 31, 32 | absrpcld 14659 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (abs‘𝑧) ∈
ℝ+) |
51 | 50 | relogcld 24897 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (log‘(abs‘𝑧)) ∈
ℝ) |
52 | 51 | recnd 10460 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (log‘(abs‘𝑧)) ∈
ℂ) |
53 | 52 | abscld 14647 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) →
(abs‘(log‘(abs‘𝑧))) ∈ ℝ) |
54 | 53, 26 | readdcld 10461 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) →
((abs‘(log‘(abs‘𝑧))) + π) ∈ ℝ) |
55 | | abslogle 24892 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ ℂ ∧ 𝑧 ≠ 0) →
(abs‘(log‘𝑧))
≤ ((abs‘(log‘(abs‘𝑧))) + π)) |
56 | 31, 32, 55 | syl2anc 576 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (abs‘(log‘𝑧)) ≤
((abs‘(log‘(abs‘𝑧))) + π)) |
57 | | 1rp 12201 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℝ+ |
58 | | relogdiv 24867 |
. . . . . . . . . . . . . . . 16
⊢ ((1
∈ ℝ+ ∧ 𝑅 ∈ ℝ+) →
(log‘(1 / 𝑅)) =
((log‘1) − (log‘𝑅))) |
59 | 57, 24, 58 | sylancr 578 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (log‘(1 / 𝑅)) = ((log‘1) − (log‘𝑅))) |
60 | | df-neg 10665 |
. . . . . . . . . . . . . . . 16
⊢
-(log‘𝑅) = (0
− (log‘𝑅)) |
61 | | log1 24860 |
. . . . . . . . . . . . . . . . 17
⊢
(log‘1) = 0 |
62 | 61 | oveq1i 6980 |
. . . . . . . . . . . . . . . 16
⊢
((log‘1) − (log‘𝑅)) = (0 − (log‘𝑅)) |
63 | 60, 62 | eqtr4i 2799 |
. . . . . . . . . . . . . . 15
⊢
-(log‘𝑅) =
((log‘1) − (log‘𝑅)) |
64 | 59, 63 | syl6reqr 2827 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → -(log‘𝑅) = (log‘(1 / 𝑅))) |
65 | | oveq2 6978 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 0 → (𝑧 + 𝑘) = (𝑧 + 0)) |
66 | 65 | fveq2d 6497 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 0 → (abs‘(𝑧 + 𝑘)) = (abs‘(𝑧 + 0))) |
67 | 66 | breq2d 4935 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 0 → ((1 / 𝑅) ≤ (abs‘(𝑧 + 𝑘)) ↔ (1 / 𝑅) ≤ (abs‘(𝑧 + 0)))) |
68 | | fveq2 6493 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑧 → (abs‘𝑥) = (abs‘𝑧)) |
69 | 68 | breq1d 4933 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑧 → ((abs‘𝑥) ≤ 𝑅 ↔ (abs‘𝑧) ≤ 𝑅)) |
70 | | fvoveq1 6993 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = 𝑧 → (abs‘(𝑥 + 𝑘)) = (abs‘(𝑧 + 𝑘))) |
71 | 70 | breq2d 4935 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑧 → ((1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)) ↔ (1 / 𝑅) ≤ (abs‘(𝑧 + 𝑘)))) |
72 | 71 | ralbidv 3141 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑧 → (∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)) ↔ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑧 + 𝑘)))) |
73 | 69, 72 | anbi12d 621 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑧 → (((abs‘𝑥) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘))) ↔ ((abs‘𝑧) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑧 + 𝑘))))) |
74 | 73, 2 | elrab2 3593 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ 𝑈 ↔ (𝑧 ∈ ℂ ∧ ((abs‘𝑧) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑧 + 𝑘))))) |
75 | 74 | simprbi 489 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ 𝑈 → ((abs‘𝑧) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑧 + 𝑘)))) |
76 | 75 | adantl 474 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → ((abs‘𝑧) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑧 + 𝑘)))) |
77 | 76 | simprd 488 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑧 + 𝑘))) |
78 | | 0nn0 11717 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 ∈
ℕ0 |
79 | 78 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → 0 ∈
ℕ0) |
80 | 67, 77, 79 | rspcdva 3535 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (1 / 𝑅) ≤ (abs‘(𝑧 + 0))) |
81 | 31 | addid1d 10632 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (𝑧 + 0) = 𝑧) |
82 | 81 | fveq2d 6497 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (abs‘(𝑧 + 0)) = (abs‘𝑧)) |
83 | 80, 82 | breqtrd 4949 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (1 / 𝑅) ≤ (abs‘𝑧)) |
84 | 24 | rpreccld 12251 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (1 / 𝑅) ∈
ℝ+) |
85 | 84, 50 | logled 24901 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → ((1 / 𝑅) ≤ (abs‘𝑧) ↔ (log‘(1 / 𝑅)) ≤ (log‘(abs‘𝑧)))) |
86 | 83, 85 | mpbid 224 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (log‘(1 / 𝑅)) ≤ (log‘(abs‘𝑧))) |
87 | 64, 86 | eqbrtrd 4945 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → -(log‘𝑅) ≤ (log‘(abs‘𝑧))) |
88 | 76 | simpld 487 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (abs‘𝑧) ≤ 𝑅) |
89 | 50, 24 | logled 24901 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → ((abs‘𝑧) ≤ 𝑅 ↔ (log‘(abs‘𝑧)) ≤ (log‘𝑅))) |
90 | 88, 89 | mpbid 224 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (log‘(abs‘𝑧)) ≤ (log‘𝑅)) |
91 | 51, 25 | absled 14641 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) →
((abs‘(log‘(abs‘𝑧))) ≤ (log‘𝑅) ↔ (-(log‘𝑅) ≤ (log‘(abs‘𝑧)) ∧
(log‘(abs‘𝑧))
≤ (log‘𝑅)))) |
92 | 87, 90, 91 | mpbir2and 700 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) →
(abs‘(log‘(abs‘𝑧))) ≤ (log‘𝑅)) |
93 | 53, 25, 26, 92 | leadd1dd 11047 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) →
((abs‘(log‘(abs‘𝑧))) + π) ≤ ((log‘𝑅) + π)) |
94 | 39, 54, 27, 56, 93 | letrd 10589 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (abs‘(log‘𝑧)) ≤ ((log‘𝑅) + π)) |
95 | 39, 27, 35, 94 | leadd1dd 11047 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → ((abs‘(log‘𝑧)) + (abs‘((log
Γ‘𝑧) +
(log‘𝑧)))) ≤
(((log‘𝑅) + π) +
(abs‘((log Γ‘𝑧) + (log‘𝑧))))) |
96 | 22, 40, 36, 49, 95 | letrd 10589 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → (abs‘(log Γ‘𝑧)) ≤ (((log‘𝑅) + π) + (abs‘((log
Γ‘𝑧) +
(log‘𝑧))))) |
97 | 96 | adantr 473 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) ∧ (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦) → (abs‘(log Γ‘𝑧)) ≤ (((log‘𝑅) + π) + (abs‘((log
Γ‘𝑧) +
(log‘𝑧))))) |
98 | 35 | adantr 473 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) ∧ (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦) → (abs‘((log Γ‘𝑧) + (log‘𝑧))) ∈
ℝ) |
99 | | simpllr 763 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) ∧ (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦) → 𝑦 ∈ ℝ) |
100 | 27 | adantr 473 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) ∧ (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦) → ((log‘𝑅) + π) ∈ ℝ) |
101 | | simpr 477 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) ∧ (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦) → (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦) |
102 | 98, 99, 100, 101 | leadd2dd 11048 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) ∧ (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦) → (((log‘𝑅) + π) + (abs‘((log
Γ‘𝑧) +
(log‘𝑧)))) ≤
(((log‘𝑅) + π) +
𝑦)) |
103 | 23, 37, 38, 97, 102 | letrd 10589 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) ∧ (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦) → (abs‘(log Γ‘𝑧)) ≤ (((log‘𝑅) + π) + 𝑦)) |
104 | 103 | ex 405 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝑈) → ((abs‘((log
Γ‘𝑧) +
(log‘𝑧))) ≤ 𝑦 → (abs‘(log
Γ‘𝑧)) ≤
(((log‘𝑅) + π) +
𝑦))) |
105 | 104 | ralimdva 3121 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (∀𝑧 ∈ 𝑈 (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦 → ∀𝑧 ∈ 𝑈 (abs‘(log Γ‘𝑧)) ≤ (((log‘𝑅) + π) + 𝑦))) |
106 | 105 | impr 447 |
. . 3
⊢ ((𝜑 ∧ (𝑦 ∈ ℝ ∧ ∀𝑧 ∈ 𝑈 (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦)) → ∀𝑧 ∈ 𝑈 (abs‘(log Γ‘𝑧)) ≤ (((log‘𝑅) + π) + 𝑦)) |
107 | | brralrspcev 4983 |
. . 3
⊢
(((((log‘𝑅) +
π) + 𝑦) ∈ ℝ
∧ ∀𝑧 ∈
𝑈 (abs‘(log
Γ‘𝑧)) ≤
(((log‘𝑅) + π) +
𝑦)) → ∃𝑟 ∈ ℝ ∀𝑧 ∈ 𝑈 (abs‘(log Γ‘𝑧)) ≤ 𝑟) |
108 | 18, 106, 107 | syl2anc 576 |
. 2
⊢ ((𝜑 ∧ (𝑦 ∈ ℝ ∧ ∀𝑧 ∈ 𝑈 (abs‘((log Γ‘𝑧) + (log‘𝑧))) ≤ 𝑦)) → ∃𝑟 ∈ ℝ ∀𝑧 ∈ 𝑈 (abs‘(log Γ‘𝑧)) ≤ 𝑟) |
109 | 9, 108 | rexlimddv 3230 |
1
⊢ (𝜑 → ∃𝑟 ∈ ℝ ∀𝑧 ∈ 𝑈 (abs‘(log Γ‘𝑧)) ≤ 𝑟) |