nominpos

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

		Ref	Expression
	Assertion	nominpos	$⊢ \neg \exists x \in ℝ (0 < x \land \neg \exists y \in ℝ (0 < y \land y < x))$

Step	Hyp	Ref	Expression
1		rehalfcl	$⊢ x \in ℝ \to \frac{x}{2} \in ℝ$
2		2re	$⊢ 2 \in ℝ$
3		2pos	$⊢ 0 < 2$
4		divgt0	$⊢ ((x \in ℝ \land 0 < x) \land (2 \in ℝ \land 0 < 2)) \to 0 < \frac{x}{2}$
5	2 3 4	mpanr12	$⊢ (x \in ℝ \land 0 < x) \to 0 < \frac{x}{2}$
6	5	ex	$⊢ x \in ℝ \to (0 < x \to 0 < \frac{x}{2})$
7		halfpos	$⊢ x \in ℝ \to (0 < x \leftrightarrow \frac{x}{2} < x)$
8	7	biimpd	$⊢ x \in ℝ \to (0 < x \to \frac{x}{2} < x)$
9	6 8	jcad	$⊢ x \in ℝ \to (0 < x \to (0 < \frac{x}{2} \land \frac{x}{2} < x))$
10		breq2	$⊢ y = \frac{x}{2} \to (0 < y \leftrightarrow 0 < \frac{x}{2})$
11		breq1	$⊢ y = \frac{x}{2} \to (y < x \leftrightarrow \frac{x}{2} < x)$
12	10 11	anbi12d	$⊢ y = \frac{x}{2} \to ((0 < y \land y < x) \leftrightarrow (0 < \frac{x}{2} \land \frac{x}{2} < x))$
13	12	rspcev	$⊢ (\frac{x}{2} \in ℝ \land (0 < \frac{x}{2} \land \frac{x}{2} < x)) \to \exists y \in ℝ (0 < y \land y < x)$
14	1 9 13	syl6an	$⊢ x \in ℝ \to (0 < x \to \exists y \in ℝ (0 < y \land y < x))$
15		iman	$⊢ (0 < x \to \exists y \in ℝ (0 < y \land y < x)) \leftrightarrow \neg (0 < x \land \neg \exists y \in ℝ (0 < y \land y < x))$
16	14 15	sylib	$⊢ x \in ℝ \to \neg (0 < x \land \neg \exists y \in ℝ (0 < y \land y < x))$
17	16	nrex	$⊢ \neg \exists x \in ℝ (0 < x \land \neg \exists y \in ℝ (0 < y \land y < x))$

Metamath Proof Explorer