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