Step |
Hyp |
Ref |
Expression |
1 |
|
rehalfcl |
⊢ ( 𝑥 ∈ ℝ → ( 𝑥 / 2 ) ∈ ℝ ) |
2 |
|
2re |
⊢ 2 ∈ ℝ |
3 |
|
2pos |
⊢ 0 < 2 |
4 |
|
divgt0 |
⊢ ( ( ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ) ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → 0 < ( 𝑥 / 2 ) ) |
5 |
2 3 4
|
mpanr12 |
⊢ ( ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ) → 0 < ( 𝑥 / 2 ) ) |
6 |
5
|
ex |
⊢ ( 𝑥 ∈ ℝ → ( 0 < 𝑥 → 0 < ( 𝑥 / 2 ) ) ) |
7 |
|
halfpos |
⊢ ( 𝑥 ∈ ℝ → ( 0 < 𝑥 ↔ ( 𝑥 / 2 ) < 𝑥 ) ) |
8 |
7
|
biimpd |
⊢ ( 𝑥 ∈ ℝ → ( 0 < 𝑥 → ( 𝑥 / 2 ) < 𝑥 ) ) |
9 |
6 8
|
jcad |
⊢ ( 𝑥 ∈ ℝ → ( 0 < 𝑥 → ( 0 < ( 𝑥 / 2 ) ∧ ( 𝑥 / 2 ) < 𝑥 ) ) ) |
10 |
|
breq2 |
⊢ ( 𝑦 = ( 𝑥 / 2 ) → ( 0 < 𝑦 ↔ 0 < ( 𝑥 / 2 ) ) ) |
11 |
|
breq1 |
⊢ ( 𝑦 = ( 𝑥 / 2 ) → ( 𝑦 < 𝑥 ↔ ( 𝑥 / 2 ) < 𝑥 ) ) |
12 |
10 11
|
anbi12d |
⊢ ( 𝑦 = ( 𝑥 / 2 ) → ( ( 0 < 𝑦 ∧ 𝑦 < 𝑥 ) ↔ ( 0 < ( 𝑥 / 2 ) ∧ ( 𝑥 / 2 ) < 𝑥 ) ) ) |
13 |
12
|
rspcev |
⊢ ( ( ( 𝑥 / 2 ) ∈ ℝ ∧ ( 0 < ( 𝑥 / 2 ) ∧ ( 𝑥 / 2 ) < 𝑥 ) ) → ∃ 𝑦 ∈ ℝ ( 0 < 𝑦 ∧ 𝑦 < 𝑥 ) ) |
14 |
1 9 13
|
syl6an |
⊢ ( 𝑥 ∈ ℝ → ( 0 < 𝑥 → ∃ 𝑦 ∈ ℝ ( 0 < 𝑦 ∧ 𝑦 < 𝑥 ) ) ) |
15 |
|
iman |
⊢ ( ( 0 < 𝑥 → ∃ 𝑦 ∈ ℝ ( 0 < 𝑦 ∧ 𝑦 < 𝑥 ) ) ↔ ¬ ( 0 < 𝑥 ∧ ¬ ∃ 𝑦 ∈ ℝ ( 0 < 𝑦 ∧ 𝑦 < 𝑥 ) ) ) |
16 |
14 15
|
sylib |
⊢ ( 𝑥 ∈ ℝ → ¬ ( 0 < 𝑥 ∧ ¬ ∃ 𝑦 ∈ ℝ ( 0 < 𝑦 ∧ 𝑦 < 𝑥 ) ) ) |
17 |
16
|
nrex |
⊢ ¬ ∃ 𝑥 ∈ ℝ ( 0 < 𝑥 ∧ ¬ ∃ 𝑦 ∈ ℝ ( 0 < 𝑦 ∧ 𝑦 < 𝑥 ) ) |