Step | Hyp | Ref
| Expression |
1 | | halfre 12187 |
. . . . . . . . 9
⊢ (1 / 2)
∈ ℝ |
2 | | 1re 10976 |
. . . . . . . . . 10
⊢ 1 ∈
ℝ |
3 | | rpre 12737 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ∈
ℝ) |
4 | | resubcl 11285 |
. . . . . . . . . 10
⊢ ((1
∈ ℝ ∧ 𝑦
∈ ℝ) → (1 − 𝑦) ∈ ℝ) |
5 | 2, 3, 4 | sylancr 587 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ+
→ (1 − 𝑦) ∈
ℝ) |
6 | | ifcl 4510 |
. . . . . . . . 9
⊢ (((1 / 2)
∈ ℝ ∧ (1 − 𝑦) ∈ ℝ) → if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1
− 𝑦)) ∈
ℝ) |
7 | 1, 5, 6 | sylancr 587 |
. . . . . . . 8
⊢ (𝑦 ∈ ℝ+
→ if((1 − 𝑦)
≤ (1 / 2), (1 / 2), (1 − 𝑦)) ∈ ℝ) |
8 | | 0red 10979 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ+
→ 0 ∈ ℝ) |
9 | 1 | a1i 11 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ+
→ (1 / 2) ∈ ℝ) |
10 | | halfgt0 12189 |
. . . . . . . . . 10
⊢ 0 < (1
/ 2) |
11 | 10 | a1i 11 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ+
→ 0 < (1 / 2)) |
12 | | max2 12920 |
. . . . . . . . . 10
⊢ (((1
− 𝑦) ∈ ℝ
∧ (1 / 2) ∈ ℝ) → (1 / 2) ≤ if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1
− 𝑦))) |
13 | 5, 1, 12 | sylancl 586 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ+
→ (1 / 2) ≤ if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦))) |
14 | 8, 9, 7, 11, 13 | ltletrd 11135 |
. . . . . . . 8
⊢ (𝑦 ∈ ℝ+
→ 0 < if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦))) |
15 | 7, 14 | elrpd 12768 |
. . . . . . 7
⊢ (𝑦 ∈ ℝ+
→ if((1 − 𝑦)
≤ (1 / 2), (1 / 2), (1 − 𝑦)) ∈
ℝ+) |
16 | 15 | rpsqrtcld 15121 |
. . . . . 6
⊢ (𝑦 ∈ ℝ+
→ (√‘if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦))) ∈
ℝ+) |
17 | | halflt1 12191 |
. . . . . . . . 9
⊢ (1 / 2)
< 1 |
18 | | ltsubrp 12765 |
. . . . . . . . . 10
⊢ ((1
∈ ℝ ∧ 𝑦
∈ ℝ+) → (1 − 𝑦) < 1) |
19 | 2, 18 | mpan 687 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ+
→ (1 − 𝑦) <
1) |
20 | | breq1 5082 |
. . . . . . . . . 10
⊢ ((1 / 2)
= if((1 − 𝑦) ≤ (1
/ 2), (1 / 2), (1 − 𝑦)) → ((1 / 2) < 1 ↔ if((1
− 𝑦) ≤ (1 / 2), (1
/ 2), (1 − 𝑦)) <
1)) |
21 | | breq1 5082 |
. . . . . . . . . 10
⊢ ((1
− 𝑦) = if((1 −
𝑦) ≤ (1 / 2), (1 / 2),
(1 − 𝑦)) → ((1
− 𝑦) < 1 ↔
if((1 − 𝑦) ≤ (1 /
2), (1 / 2), (1 − 𝑦))
< 1)) |
22 | 20, 21 | ifboth 4504 |
. . . . . . . . 9
⊢ (((1 / 2)
< 1 ∧ (1 − 𝑦)
< 1) → if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦)) < 1) |
23 | 17, 19, 22 | sylancr 587 |
. . . . . . . 8
⊢ (𝑦 ∈ ℝ+
→ if((1 − 𝑦)
≤ (1 / 2), (1 / 2), (1 − 𝑦)) < 1) |
24 | 15 | rpge0d 12775 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ+
→ 0 ≤ if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦))) |
25 | 2 | a1i 11 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ+
→ 1 ∈ ℝ) |
26 | | 0le1 11498 |
. . . . . . . . . 10
⊢ 0 ≤
1 |
27 | 26 | a1i 11 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ+
→ 0 ≤ 1) |
28 | 7, 24, 25, 27 | sqrtltd 15137 |
. . . . . . . 8
⊢ (𝑦 ∈ ℝ+
→ (if((1 − 𝑦)
≤ (1 / 2), (1 / 2), (1 − 𝑦)) < 1 ↔ (√‘if((1 −
𝑦) ≤ (1 / 2), (1 / 2),
(1 − 𝑦))) <
(√‘1))) |
29 | 23, 28 | mpbid 231 |
. . . . . . 7
⊢ (𝑦 ∈ ℝ+
→ (√‘if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦))) <
(√‘1)) |
30 | | sqrt1 14981 |
. . . . . . 7
⊢
(√‘1) = 1 |
31 | 29, 30 | breqtrdi 5120 |
. . . . . 6
⊢ (𝑦 ∈ ℝ+
→ (√‘if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦))) < 1) |
32 | 16, 31 | chtppilimlem2 26620 |
. . . . 5
⊢ (𝑦 ∈ ℝ+
→ ∃𝑧 ∈
ℝ ∀𝑥 ∈
(2[,)+∞)(𝑧 ≤ 𝑥 → (((√‘if((1
− 𝑦) ≤ (1 / 2), (1
/ 2), (1 − 𝑦)))↑2) ·
((π‘𝑥)
· (log‘𝑥)))
< (θ‘𝑥))) |
33 | 5 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℝ+
∧ 𝑥 ∈
(2[,)+∞)) → (1 − 𝑦) ∈ ℝ) |
34 | | max1 12918 |
. . . . . . . . . . 11
⊢ (((1
− 𝑦) ∈ ℝ
∧ (1 / 2) ∈ ℝ) → (1 − 𝑦) ≤ if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦))) |
35 | 33, 1, 34 | sylancl 586 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℝ+
∧ 𝑥 ∈
(2[,)+∞)) → (1 − 𝑦) ≤ if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦))) |
36 | 7 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℝ+
∧ 𝑥 ∈
(2[,)+∞)) → if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦)) ∈
ℝ) |
37 | | 2re 12047 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℝ |
38 | | elicopnf 13176 |
. . . . . . . . . . . . . . . 16
⊢ (2 ∈
ℝ → (𝑥 ∈
(2[,)+∞) ↔ (𝑥
∈ ℝ ∧ 2 ≤ 𝑥))) |
39 | 37, 38 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (2[,)+∞) ↔
(𝑥 ∈ ℝ ∧ 2
≤ 𝑥)) |
40 | 39 | simplbi 498 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (2[,)+∞) →
𝑥 ∈
ℝ) |
41 | | chtcl 26256 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℝ →
(θ‘𝑥) ∈
ℝ) |
42 | 40, 41 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (2[,)+∞) →
(θ‘𝑥) ∈
ℝ) |
43 | | ppinncl 26321 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℝ ∧ 2 ≤
𝑥) →
(π‘𝑥)
∈ ℕ) |
44 | 39, 43 | sylbi 216 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (2[,)+∞) →
(π‘𝑥)
∈ ℕ) |
45 | 44 | nnrpd 12769 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (2[,)+∞) →
(π‘𝑥)
∈ ℝ+) |
46 | 2 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (2[,)+∞) → 1
∈ ℝ) |
47 | 37 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (2[,)+∞) → 2
∈ ℝ) |
48 | | 1lt2 12144 |
. . . . . . . . . . . . . . . . 17
⊢ 1 <
2 |
49 | 48 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (2[,)+∞) → 1
< 2) |
50 | 39 | simprbi 497 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (2[,)+∞) → 2
≤ 𝑥) |
51 | 46, 47, 40, 49, 50 | ltletrd 11135 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (2[,)+∞) → 1
< 𝑥) |
52 | 40, 51 | rplogcld 25782 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (2[,)+∞) →
(log‘𝑥) ∈
ℝ+) |
53 | 45, 52 | rpmulcld 12787 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (2[,)+∞) →
((π‘𝑥)
· (log‘𝑥))
∈ ℝ+) |
54 | 42, 53 | rerpdivcld 12802 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (2[,)+∞) →
((θ‘𝑥) /
((π‘𝑥)
· (log‘𝑥)))
∈ ℝ) |
55 | 54 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℝ+
∧ 𝑥 ∈
(2[,)+∞)) → ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))) ∈ ℝ) |
56 | | lelttr 11066 |
. . . . . . . . . . 11
⊢ (((1
− 𝑦) ∈ ℝ
∧ if((1 − 𝑦) ≤
(1 / 2), (1 / 2), (1 − 𝑦)) ∈ ℝ ∧ ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))) ∈ ℝ) → (((1
− 𝑦) ≤ if((1
− 𝑦) ≤ (1 / 2), (1
/ 2), (1 − 𝑦)) ∧
if((1 − 𝑦) ≤ (1 /
2), (1 / 2), (1 − 𝑦))
< ((θ‘𝑥) /
((π‘𝑥)
· (log‘𝑥))))
→ (1 − 𝑦) <
((θ‘𝑥) /
((π‘𝑥)
· (log‘𝑥))))) |
57 | 33, 36, 55, 56 | syl3anc 1370 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℝ+
∧ 𝑥 ∈
(2[,)+∞)) → (((1 − 𝑦) ≤ if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦)) ∧ if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1
− 𝑦)) <
((θ‘𝑥) /
((π‘𝑥)
· (log‘𝑥))))
→ (1 − 𝑦) <
((θ‘𝑥) /
((π‘𝑥)
· (log‘𝑥))))) |
58 | 35, 57 | mpand 692 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℝ+
∧ 𝑥 ∈
(2[,)+∞)) → (if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦)) < ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))) → (1 − 𝑦) < ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))))) |
59 | 7 | recnd 11004 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℝ+
→ if((1 − 𝑦)
≤ (1 / 2), (1 / 2), (1 − 𝑦)) ∈ ℂ) |
60 | 59 | sqsqrtd 15149 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℝ+
→ ((√‘if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦)))↑2) = if((1 −
𝑦) ≤ (1 / 2), (1 / 2),
(1 − 𝑦))) |
61 | 60 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℝ+
∧ 𝑥 ∈
(2[,)+∞)) → ((√‘if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦)))↑2) = if((1 −
𝑦) ≤ (1 / 2), (1 / 2),
(1 − 𝑦))) |
62 | 61 | oveq1d 7286 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℝ+
∧ 𝑥 ∈
(2[,)+∞)) → (((√‘if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦)))↑2) ·
((π‘𝑥)
· (log‘𝑥))) =
(if((1 − 𝑦) ≤ (1 /
2), (1 / 2), (1 − 𝑦))
· ((π‘𝑥) · (log‘𝑥)))) |
63 | 62 | breq1d 5089 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℝ+
∧ 𝑥 ∈
(2[,)+∞)) → ((((√‘if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦)))↑2) ·
((π‘𝑥)
· (log‘𝑥)))
< (θ‘𝑥)
↔ (if((1 − 𝑦)
≤ (1 / 2), (1 / 2), (1 − 𝑦)) · ((π‘𝑥) · (log‘𝑥))) < (θ‘𝑥))) |
64 | 42 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℝ+
∧ 𝑥 ∈
(2[,)+∞)) → (θ‘𝑥) ∈ ℝ) |
65 | 53 | rpregt0d 12777 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (2[,)+∞) →
(((π‘𝑥)
· (log‘𝑥))
∈ ℝ ∧ 0 < ((π‘𝑥) · (log‘𝑥)))) |
66 | 65 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℝ+
∧ 𝑥 ∈
(2[,)+∞)) → (((π‘𝑥) · (log‘𝑥)) ∈ ℝ ∧ 0 <
((π‘𝑥)
· (log‘𝑥)))) |
67 | | ltmuldiv 11848 |
. . . . . . . . . . 11
⊢ ((if((1
− 𝑦) ≤ (1 / 2), (1
/ 2), (1 − 𝑦)) ∈
ℝ ∧ (θ‘𝑥) ∈ ℝ ∧
(((π‘𝑥)
· (log‘𝑥))
∈ ℝ ∧ 0 < ((π‘𝑥) · (log‘𝑥)))) → ((if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1
− 𝑦)) ·
((π‘𝑥)
· (log‘𝑥)))
< (θ‘𝑥)
↔ if((1 − 𝑦)
≤ (1 / 2), (1 / 2), (1 − 𝑦)) < ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))))) |
68 | 36, 64, 66, 67 | syl3anc 1370 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℝ+
∧ 𝑥 ∈
(2[,)+∞)) → ((if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦)) ·
((π‘𝑥)
· (log‘𝑥)))
< (θ‘𝑥)
↔ if((1 − 𝑦)
≤ (1 / 2), (1 / 2), (1 − 𝑦)) < ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))))) |
69 | 63, 68 | bitrd 278 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℝ+
∧ 𝑥 ∈
(2[,)+∞)) → ((((√‘if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦)))↑2) ·
((π‘𝑥)
· (log‘𝑥)))
< (θ‘𝑥)
↔ if((1 − 𝑦)
≤ (1 / 2), (1 / 2), (1 − 𝑦)) < ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))))) |
70 | | 0red 10979 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (2[,)+∞) → 0
∈ ℝ) |
71 | | 2pos 12076 |
. . . . . . . . . . . . . . . . . . 19
⊢ 0 <
2 |
72 | 71 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (2[,)+∞) → 0
< 2) |
73 | 70, 47, 40, 72, 50 | ltletrd 11135 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (2[,)+∞) → 0
< 𝑥) |
74 | 40, 73 | elrpd 12768 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (2[,)+∞) →
𝑥 ∈
ℝ+) |
75 | | chtleppi 26356 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℝ+
→ (θ‘𝑥)
≤ ((π‘𝑥)
· (log‘𝑥))) |
76 | 74, 75 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (2[,)+∞) →
(θ‘𝑥) ≤
((π‘𝑥)
· (log‘𝑥))) |
77 | 53 | rpcnd 12773 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (2[,)+∞) →
((π‘𝑥)
· (log‘𝑥))
∈ ℂ) |
78 | 77 | mulid1d 10993 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (2[,)+∞) →
(((π‘𝑥)
· (log‘𝑥))
· 1) = ((π‘𝑥) · (log‘𝑥))) |
79 | 76, 78 | breqtrrd 5107 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (2[,)+∞) →
(θ‘𝑥) ≤
(((π‘𝑥)
· (log‘𝑥))
· 1)) |
80 | 42, 46, 53 | ledivmuld 12824 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (2[,)+∞) →
(((θ‘𝑥) /
((π‘𝑥)
· (log‘𝑥)))
≤ 1 ↔ (θ‘𝑥) ≤ (((π‘𝑥) · (log‘𝑥)) ·
1))) |
81 | 79, 80 | mpbird 256 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (2[,)+∞) →
((θ‘𝑥) /
((π‘𝑥)
· (log‘𝑥)))
≤ 1) |
82 | 54, 46, 81 | abssuble0d 15142 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (2[,)+∞) →
(abs‘(((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))) − 1)) = (1 −
((θ‘𝑥) /
((π‘𝑥)
· (log‘𝑥))))) |
83 | 82 | breq1d 5089 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (2[,)+∞) →
((abs‘(((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))) − 1)) < 𝑦 ↔ (1 − ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥)))) < 𝑦)) |
84 | 83 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℝ+
∧ 𝑥 ∈
(2[,)+∞)) → ((abs‘(((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))) − 1)) < 𝑦 ↔ (1 − ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥)))) < 𝑦)) |
85 | 2 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℝ+
∧ 𝑥 ∈
(2[,)+∞)) → 1 ∈ ℝ) |
86 | 3 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℝ+
∧ 𝑥 ∈
(2[,)+∞)) → 𝑦
∈ ℝ) |
87 | | ltsub23 11455 |
. . . . . . . . . . 11
⊢ ((1
∈ ℝ ∧ ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))) ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((1 −
((θ‘𝑥) /
((π‘𝑥)
· (log‘𝑥))))
< 𝑦 ↔ (1 −
𝑦) <
((θ‘𝑥) /
((π‘𝑥)
· (log‘𝑥))))) |
88 | 85, 55, 86, 87 | syl3anc 1370 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℝ+
∧ 𝑥 ∈
(2[,)+∞)) → ((1 − ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥)))) < 𝑦 ↔ (1 − 𝑦) < ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))))) |
89 | 84, 88 | bitrd 278 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℝ+
∧ 𝑥 ∈
(2[,)+∞)) → ((abs‘(((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))) − 1)) < 𝑦 ↔ (1 − 𝑦) < ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))))) |
90 | 58, 69, 89 | 3imtr4d 294 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℝ+
∧ 𝑥 ∈
(2[,)+∞)) → ((((√‘if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦)))↑2) ·
((π‘𝑥)
· (log‘𝑥)))
< (θ‘𝑥)
→ (abs‘(((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))) − 1)) < 𝑦)) |
91 | 90 | imim2d 57 |
. . . . . . 7
⊢ ((𝑦 ∈ ℝ+
∧ 𝑥 ∈
(2[,)+∞)) → ((𝑧
≤ 𝑥 →
(((√‘if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦)))↑2) ·
((π‘𝑥)
· (log‘𝑥)))
< (θ‘𝑥))
→ (𝑧 ≤ 𝑥 →
(abs‘(((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))) − 1)) < 𝑦))) |
92 | 91 | ralimdva 3105 |
. . . . . 6
⊢ (𝑦 ∈ ℝ+
→ (∀𝑥 ∈
(2[,)+∞)(𝑧 ≤ 𝑥 → (((√‘if((1
− 𝑦) ≤ (1 / 2), (1
/ 2), (1 − 𝑦)))↑2) ·
((π‘𝑥)
· (log‘𝑥)))
< (θ‘𝑥))
→ ∀𝑥 ∈
(2[,)+∞)(𝑧 ≤ 𝑥 →
(abs‘(((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))) − 1)) < 𝑦))) |
93 | 92 | reximdv 3204 |
. . . . 5
⊢ (𝑦 ∈ ℝ+
→ (∃𝑧 ∈
ℝ ∀𝑥 ∈
(2[,)+∞)(𝑧 ≤ 𝑥 → (((√‘if((1
− 𝑦) ≤ (1 / 2), (1
/ 2), (1 − 𝑦)))↑2) ·
((π‘𝑥)
· (log‘𝑥)))
< (θ‘𝑥))
→ ∃𝑧 ∈
ℝ ∀𝑥 ∈
(2[,)+∞)(𝑧 ≤ 𝑥 →
(abs‘(((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))) − 1)) < 𝑦))) |
94 | 32, 93 | mpd 15 |
. . . 4
⊢ (𝑦 ∈ ℝ+
→ ∃𝑧 ∈
ℝ ∀𝑥 ∈
(2[,)+∞)(𝑧 ≤ 𝑥 →
(abs‘(((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))) − 1)) < 𝑦)) |
95 | 94 | rgen 3076 |
. . 3
⊢
∀𝑦 ∈
ℝ+ ∃𝑧 ∈ ℝ ∀𝑥 ∈ (2[,)+∞)(𝑧 ≤ 𝑥 → (abs‘(((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))) − 1)) < 𝑦) |
96 | 54 | recnd 11004 |
. . . . . 6
⊢ (𝑥 ∈ (2[,)+∞) →
((θ‘𝑥) /
((π‘𝑥)
· (log‘𝑥)))
∈ ℂ) |
97 | 96 | adantl 482 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))) ∈ ℂ) |
98 | 97 | ralrimiva 3110 |
. . . 4
⊢ (⊤
→ ∀𝑥 ∈
(2[,)+∞)((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))) ∈ ℂ) |
99 | 40 | ssriv 3930 |
. . . . 5
⊢
(2[,)+∞) ⊆ ℝ |
100 | 99 | a1i 11 |
. . . 4
⊢ (⊤
→ (2[,)+∞) ⊆ ℝ) |
101 | | 1cnd 10971 |
. . . 4
⊢ (⊤
→ 1 ∈ ℂ) |
102 | 98, 100, 101 | rlim2 15203 |
. . 3
⊢ (⊤
→ ((𝑥 ∈
(2[,)+∞) ↦ ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥)))) ⇝𝑟 1 ↔
∀𝑦 ∈
ℝ+ ∃𝑧 ∈ ℝ ∀𝑥 ∈ (2[,)+∞)(𝑧 ≤ 𝑥 → (abs‘(((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))) − 1)) < 𝑦))) |
103 | 95, 102 | mpbiri 257 |
. 2
⊢ (⊤
→ (𝑥 ∈
(2[,)+∞) ↦ ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥)))) ⇝𝑟
1) |
104 | 103 | mptru 1549 |
1
⊢ (𝑥 ∈ (2[,)+∞) ↦
((θ‘𝑥) /
((π‘𝑥)
· (log‘𝑥))))
⇝𝑟 1 |