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