Step | Hyp | Ref
| Expression |
1 | | rpssre 11719 |
. . . . 5
⊢
ℝ+ ⊆ ℝ |
2 | 1 | a1i 11 |
. . . 4
⊢ (⊤
→ ℝ+ ⊆ ℝ) |
3 | | 1red 9934 |
. . . 4
⊢ (⊤
→ 1 ∈ ℝ) |
4 | | simpr 476 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → 𝑥 ∈ ℝ+) |
5 | 4 | rpred 11748 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → 𝑥 ∈ ℝ) |
6 | | chpcl 24650 |
. . . . . 6
⊢ (𝑥 ∈ ℝ →
(ψ‘𝑥) ∈
ℝ) |
7 | 5, 6 | syl 17 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (ψ‘𝑥) ∈ ℝ) |
8 | 7, 4 | rerpdivcld 11779 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((ψ‘𝑥) / 𝑥) ∈ ℝ) |
9 | | chpo1ub 24969 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
↦ ((ψ‘𝑥) /
𝑥)) ∈
𝑂(1) |
10 | 9 | a1i 11 |
. . . . 5
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ∈ 𝑂(1)) |
11 | 8, 10 | o1lo1d 14118 |
. . . 4
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ∈ ≤𝑂(1)) |
12 | | chpcl 24650 |
. . . . . 6
⊢ (𝑦 ∈ ℝ →
(ψ‘𝑦) ∈
ℝ) |
13 | 12 | ad2antrl 760 |
. . . . 5
⊢
((⊤ ∧ (𝑦
∈ ℝ ∧ 1 ≤ 𝑦)) → (ψ‘𝑦) ∈ ℝ) |
14 | 13 | rehalfcld 11156 |
. . . 4
⊢
((⊤ ∧ (𝑦
∈ ℝ ∧ 1 ≤ 𝑦)) → ((ψ‘𝑦) / 2) ∈ ℝ) |
15 | 5 | adantr 480 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 𝑥 ∈ ℝ) |
16 | | chpeq0 24733 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ →
((ψ‘𝑥) = 0 ↔
𝑥 < 2)) |
17 | 15, 16 | syl 17 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → ((ψ‘𝑥) = 0 ↔ 𝑥 < 2)) |
18 | 17 | biimpar 501 |
. . . . . . 7
⊢
((((⊤ ∧ 𝑥
∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑥 < 2) → (ψ‘𝑥) = 0) |
19 | 18 | oveq1d 6564 |
. . . . . 6
⊢
((((⊤ ∧ 𝑥
∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑥 < 2) → ((ψ‘𝑥) / 𝑥) = (0 / 𝑥)) |
20 | 4 | adantr 480 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 𝑥 ∈ ℝ+) |
21 | 20 | rpcnd 11750 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 𝑥 ∈ ℂ) |
22 | 20 | rpne0d 11753 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 𝑥 ≠ 0) |
23 | 21, 22 | div0d 10679 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (0 / 𝑥) = 0) |
24 | 13 | ad2ant2r 779 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (ψ‘𝑦) ∈ ℝ) |
25 | | 2rp 11713 |
. . . . . . . . . 10
⊢ 2 ∈
ℝ+ |
26 | 25 | a1i 11 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 2 ∈
ℝ+) |
27 | | simprll 798 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 𝑦 ∈ ℝ) |
28 | | chpge0 24652 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℝ → 0 ≤
(ψ‘𝑦)) |
29 | 27, 28 | syl 17 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 0 ≤ (ψ‘𝑦)) |
30 | 24, 26, 29 | divge0d 11788 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 0 ≤ ((ψ‘𝑦) / 2)) |
31 | 23, 30 | eqbrtrd 4605 |
. . . . . . 7
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (0 / 𝑥) ≤ ((ψ‘𝑦) / 2)) |
32 | 31 | adantr 480 |
. . . . . 6
⊢
((((⊤ ∧ 𝑥
∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑥 < 2) → (0 / 𝑥) ≤ ((ψ‘𝑦) / 2)) |
33 | 19, 32 | eqbrtrd 4605 |
. . . . 5
⊢
((((⊤ ∧ 𝑥
∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑥 < 2) → ((ψ‘𝑥) / 𝑥) ≤ ((ψ‘𝑦) / 2)) |
34 | 7 | ad2antrr 758 |
. . . . . 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 24652 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ → 0 ≤
(ψ‘𝑥)) |
39 | 37, 38 | syl 17 |
. . . . . 6
⊢
((((⊤ ∧ 𝑥
∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 2 ≤ 𝑥) → 0 ≤ (ψ‘𝑥)) |
40 | 27 | adantr 480 |
. . . . . . 7
⊢
((((⊤ ∧ 𝑥
∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 2 ≤ 𝑥) → 𝑦 ∈ ℝ) |
41 | | simprr 792 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 𝑥 < 𝑦) |
42 | 15, 27, 41 | ltled 10064 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 𝑥 ≤ 𝑦) |
43 | 42 | adantr 480 |
. . . . . . 7
⊢
((((⊤ ∧ 𝑥
∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 2 ≤ 𝑥) → 𝑥 ≤ 𝑦) |
44 | | chpwordi 24683 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 ≤ 𝑦) → (ψ‘𝑥) ≤ (ψ‘𝑦)) |
45 | 37, 40, 43, 44 | syl3anc 1318 |
. . . . . 6
⊢
((((⊤ ∧ 𝑥
∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 2 ≤ 𝑥) → (ψ‘𝑥) ≤ (ψ‘𝑦)) |
46 | | simpr 476 |
. . . . . 6
⊢
((((⊤ ∧ 𝑥
∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 2 ≤ 𝑥) → 2 ≤ 𝑥) |
47 | 34, 35, 36, 37, 39, 45, 46 | lediv12ad 11807 |
. . . . 5
⊢
((((⊤ ∧ 𝑥
∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 2 ≤ 𝑥) → ((ψ‘𝑥) / 𝑥) ≤ ((ψ‘𝑦) / 2)) |
48 | | 2re 10967 |
. . . . . 6
⊢ 2 ∈
ℝ |
49 | 48 | a1i 11 |
. . . . 5
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 2 ∈ ℝ) |
50 | 33, 47, 15, 49 | ltlecasei 10024 |
. . . 4
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → ((ψ‘𝑥) / 𝑥) ≤ ((ψ‘𝑦) / 2)) |
51 | 2, 3, 8, 11, 14, 50 | lo1bddrp 14104 |
. . 3
⊢ (⊤
→ ∃𝑐 ∈
ℝ+ ∀𝑥 ∈ ℝ+
((ψ‘𝑥) / 𝑥) ≤ 𝑐) |
52 | 51 | trud 1484 |
. 2
⊢
∃𝑐 ∈
ℝ+ ∀𝑥 ∈ ℝ+
((ψ‘𝑥) / 𝑥) ≤ 𝑐 |
53 | | simpr 476 |
. . . . . . 7
⊢ ((𝑐 ∈ ℝ+
∧ 𝑥 ∈
ℝ+) → 𝑥 ∈ ℝ+) |
54 | 53 | rpred 11748 |
. . . . . 6
⊢ ((𝑐 ∈ ℝ+
∧ 𝑥 ∈
ℝ+) → 𝑥 ∈ ℝ) |
55 | 54, 6 | syl 17 |
. . . . 5
⊢ ((𝑐 ∈ ℝ+
∧ 𝑥 ∈
ℝ+) → (ψ‘𝑥) ∈ ℝ) |
56 | | simpl 472 |
. . . . . 6
⊢ ((𝑐 ∈ ℝ+
∧ 𝑥 ∈
ℝ+) → 𝑐 ∈ ℝ+) |
57 | 56 | rpred 11748 |
. . . . 5
⊢ ((𝑐 ∈ ℝ+
∧ 𝑥 ∈
ℝ+) → 𝑐 ∈ ℝ) |
58 | 55, 57, 53 | ledivmul2d 11802 |
. . . 4
⊢ ((𝑐 ∈ ℝ+
∧ 𝑥 ∈
ℝ+) → (((ψ‘𝑥) / 𝑥) ≤ 𝑐 ↔ (ψ‘𝑥) ≤ (𝑐 · 𝑥))) |
59 | 58 | ralbidva 2968 |
. . 3
⊢ (𝑐 ∈ ℝ+
→ (∀𝑥 ∈
ℝ+ ((ψ‘𝑥) / 𝑥) ≤ 𝑐 ↔ ∀𝑥 ∈ ℝ+
(ψ‘𝑥) ≤ (𝑐 · 𝑥))) |
60 | 59 | rexbiia 3022 |
. 2
⊢
(∃𝑐 ∈
ℝ+ ∀𝑥 ∈ ℝ+
((ψ‘𝑥) / 𝑥) ≤ 𝑐 ↔ ∃𝑐 ∈ ℝ+ ∀𝑥 ∈ ℝ+
(ψ‘𝑥) ≤ (𝑐 · 𝑥)) |
61 | 52, 60 | mpbi 219 |
1
⊢
∃𝑐 ∈
ℝ+ ∀𝑥 ∈ ℝ+
(ψ‘𝑥) ≤ (𝑐 · 𝑥) |