This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nominpos

Description: There is no smallest positive real number. (Contributed by NM, 28-Oct-2004)

Ref Expression
Assertion nominpos ¬ ∃ 𝑥 ∈ ℝ ( 0 < 𝑥 ∧ ¬ ∃ 𝑦 ∈ ℝ ( 0 < 𝑦 ∧ 𝑦 < 𝑥 ) )

Proof

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 < 𝑦 ∧ 𝑦 < 𝑥 ) )