| Step | Hyp | Ref
| Expression |
| 1 | | rpssre 13042 |
. . . . 5
⊢
ℝ+ ⊆ ℝ |
| 2 | 1 | a1i 11 |
. . . 4
⊢ (⊤
→ ℝ+ ⊆ ℝ) |
| 3 | | 1red 11262 |
. . . 4
⊢ (⊤
→ 1 ∈ ℝ) |
| 4 | | simpr 484 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → 𝑥 ∈ ℝ+) |
| 5 | 4 | rpred 13077 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → 𝑥 ∈ ℝ) |
| 6 | | chpcl 27167 |
. . . . . 6
⊢ (𝑥 ∈ ℝ →
(ψ‘𝑥) ∈
ℝ) |
| 7 | 5, 6 | syl 17 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (ψ‘𝑥) ∈ ℝ) |
| 8 | 7, 4 | rerpdivcld 13108 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((ψ‘𝑥) / 𝑥) ∈ ℝ) |
| 9 | | chpo1ub 27524 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
↦ ((ψ‘𝑥) /
𝑥)) ∈
𝑂(1) |
| 10 | 9 | a1i 11 |
. . . . 5
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ∈ 𝑂(1)) |
| 11 | 8, 10 | o1lo1d 15575 |
. . . 4
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ∈ ≤𝑂(1)) |
| 12 | | chpcl 27167 |
. . . . . 6
⊢ (𝑦 ∈ ℝ →
(ψ‘𝑦) ∈
ℝ) |
| 13 | 12 | ad2antrl 728 |
. . . . 5
⊢
((⊤ ∧ (𝑦
∈ ℝ ∧ 1 ≤ 𝑦)) → (ψ‘𝑦) ∈ ℝ) |
| 14 | 13 | rehalfcld 12513 |
. . . 4
⊢
((⊤ ∧ (𝑦
∈ ℝ ∧ 1 ≤ 𝑦)) → ((ψ‘𝑦) / 2) ∈ ℝ) |
| 15 | 5 | adantr 480 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 𝑥 ∈ ℝ) |
| 16 | | chpeq0 27252 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ →
((ψ‘𝑥) = 0 ↔
𝑥 < 2)) |
| 17 | 15, 16 | syl 17 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → ((ψ‘𝑥) = 0 ↔ 𝑥 < 2)) |
| 18 | 17 | biimpar 477 |
. . . . . . 7
⊢
((((⊤ ∧ 𝑥
∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑥 < 2) → (ψ‘𝑥) = 0) |
| 19 | 18 | oveq1d 7446 |
. . . . . 6
⊢
((((⊤ ∧ 𝑥
∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑥 < 2) → ((ψ‘𝑥) / 𝑥) = (0 / 𝑥)) |
| 20 | 4 | adantr 480 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 𝑥 ∈ ℝ+) |
| 21 | 20 | rpcnd 13079 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 𝑥 ∈ ℂ) |
| 22 | 20 | rpne0d 13082 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 𝑥 ≠ 0) |
| 23 | 21, 22 | div0d 12042 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (0 / 𝑥) = 0) |
| 24 | 13 | ad2ant2r 747 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (ψ‘𝑦) ∈ ℝ) |
| 25 | | 2rp 13039 |
. . . . . . . . . 10
⊢ 2 ∈
ℝ+ |
| 26 | 25 | a1i 11 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 2 ∈
ℝ+) |
| 27 | | simprll 779 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 𝑦 ∈ ℝ) |
| 28 | | chpge0 27169 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℝ → 0 ≤
(ψ‘𝑦)) |
| 29 | 27, 28 | syl 17 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 0 ≤ (ψ‘𝑦)) |
| 30 | 24, 26, 29 | divge0d 13117 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 0 ≤ ((ψ‘𝑦) / 2)) |
| 31 | 23, 30 | eqbrtrd 5165 |
. . . . . . 7
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (0 / 𝑥) ≤ ((ψ‘𝑦) / 2)) |
| 32 | 31 | adantr 480 |
. . . . . 6
⊢
((((⊤ ∧ 𝑥
∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑥 < 2) → (0 / 𝑥) ≤ ((ψ‘𝑦) / 2)) |
| 33 | 19, 32 | eqbrtrd 5165 |
. . . . 5
⊢
((((⊤ ∧ 𝑥
∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑥 < 2) → ((ψ‘𝑥) / 𝑥) ≤ ((ψ‘𝑦) / 2)) |
| 34 | 7 | ad2antrr 726 |
. . . . . 6
⊢
((((⊤ ∧ 𝑥
∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 2 ≤ 𝑥) → (ψ‘𝑥) ∈ ℝ) |
| 35 | 24 | adantr 480 |
. . . . . 6
⊢
((((⊤ ∧ 𝑥
∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 2 ≤ 𝑥) → (ψ‘𝑦) ∈ ℝ) |
| 36 | 25 | a1i 11 |
. . . . . 6
⊢
((((⊤ ∧ 𝑥
∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 2 ≤ 𝑥) → 2 ∈
ℝ+) |
| 37 | 15 | adantr 480 |
. . . . . 6
⊢
((((⊤ ∧ 𝑥
∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 2 ≤ 𝑥) → 𝑥 ∈ ℝ) |
| 38 | | chpge0 27169 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ → 0 ≤
(ψ‘𝑥)) |
| 39 | 37, 38 | syl 17 |
. . . . . 6
⊢
((((⊤ ∧ 𝑥
∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 2 ≤ 𝑥) → 0 ≤ (ψ‘𝑥)) |
| 40 | 27 | adantr 480 |
. . . . . . 7
⊢
((((⊤ ∧ 𝑥
∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 2 ≤ 𝑥) → 𝑦 ∈ ℝ) |
| 41 | | simprr 773 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 𝑥 < 𝑦) |
| 42 | 15, 27, 41 | ltled 11409 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 𝑥 ≤ 𝑦) |
| 43 | 42 | adantr 480 |
. . . . . . 7
⊢
((((⊤ ∧ 𝑥
∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 2 ≤ 𝑥) → 𝑥 ≤ 𝑦) |
| 44 | | chpwordi 27200 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 ≤ 𝑦) → (ψ‘𝑥) ≤ (ψ‘𝑦)) |
| 45 | 37, 40, 43, 44 | syl3anc 1373 |
. . . . . 6
⊢
((((⊤ ∧ 𝑥
∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 2 ≤ 𝑥) → (ψ‘𝑥) ≤ (ψ‘𝑦)) |
| 46 | | simpr 484 |
. . . . . 6
⊢
((((⊤ ∧ 𝑥
∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 2 ≤ 𝑥) → 2 ≤ 𝑥) |
| 47 | 34, 35, 36, 37, 39, 45, 46 | lediv12ad 13136 |
. . . . 5
⊢
((((⊤ ∧ 𝑥
∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 2 ≤ 𝑥) → ((ψ‘𝑥) / 𝑥) ≤ ((ψ‘𝑦) / 2)) |
| 48 | | 2re 12340 |
. . . . . 6
⊢ 2 ∈
ℝ |
| 49 | 48 | a1i 11 |
. . . . 5
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 2 ∈ ℝ) |
| 50 | 33, 47, 15, 49 | ltlecasei 11369 |
. . . 4
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → ((ψ‘𝑥) / 𝑥) ≤ ((ψ‘𝑦) / 2)) |
| 51 | 2, 3, 8, 11, 14, 50 | lo1bddrp 15561 |
. . 3
⊢ (⊤
→ ∃𝑐 ∈
ℝ+ ∀𝑥 ∈ ℝ+
((ψ‘𝑥) / 𝑥) ≤ 𝑐) |
| 52 | 51 | mptru 1547 |
. 2
⊢
∃𝑐 ∈
ℝ+ ∀𝑥 ∈ ℝ+
((ψ‘𝑥) / 𝑥) ≤ 𝑐 |
| 53 | | simpr 484 |
. . . . . . 7
⊢ ((𝑐 ∈ ℝ+
∧ 𝑥 ∈
ℝ+) → 𝑥 ∈ ℝ+) |
| 54 | 53 | rpred 13077 |
. . . . . 6
⊢ ((𝑐 ∈ ℝ+
∧ 𝑥 ∈
ℝ+) → 𝑥 ∈ ℝ) |
| 55 | 54, 6 | syl 17 |
. . . . 5
⊢ ((𝑐 ∈ ℝ+
∧ 𝑥 ∈
ℝ+) → (ψ‘𝑥) ∈ ℝ) |
| 56 | | simpl 482 |
. . . . . 6
⊢ ((𝑐 ∈ ℝ+
∧ 𝑥 ∈
ℝ+) → 𝑐 ∈ ℝ+) |
| 57 | 56 | rpred 13077 |
. . . . 5
⊢ ((𝑐 ∈ ℝ+
∧ 𝑥 ∈
ℝ+) → 𝑐 ∈ ℝ) |
| 58 | 55, 57, 53 | ledivmul2d 13131 |
. . . 4
⊢ ((𝑐 ∈ ℝ+
∧ 𝑥 ∈
ℝ+) → (((ψ‘𝑥) / 𝑥) ≤ 𝑐 ↔ (ψ‘𝑥) ≤ (𝑐 · 𝑥))) |
| 59 | 58 | ralbidva 3176 |
. . 3
⊢ (𝑐 ∈ ℝ+
→ (∀𝑥 ∈
ℝ+ ((ψ‘𝑥) / 𝑥) ≤ 𝑐 ↔ ∀𝑥 ∈ ℝ+
(ψ‘𝑥) ≤ (𝑐 · 𝑥))) |
| 60 | 59 | rexbiia 3092 |
. 2
⊢
(∃𝑐 ∈
ℝ+ ∀𝑥 ∈ ℝ+
((ψ‘𝑥) / 𝑥) ≤ 𝑐 ↔ ∃𝑐 ∈ ℝ+ ∀𝑥 ∈ ℝ+
(ψ‘𝑥) ≤ (𝑐 · 𝑥)) |
| 61 | 52, 60 | mpbi 230 |
1
⊢
∃𝑐 ∈
ℝ+ ∀𝑥 ∈ ℝ+
(ψ‘𝑥) ≤ (𝑐 · 𝑥) |