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

Metamath Proof Explorer

Theorem 0lt1

Description: 0 is less than 1. Theorem I.21 of Apostol p. 20. (Contributed by NM, 17-Jan-1997)

		Ref	Expression
	Assertion	0lt1	$⊢ 0 < 1$

Step	Hyp	Ref	Expression
1		1re	$⊢ 1 \in ℝ$
2		ax-1ne0	$⊢ 1 \neq 0$
3		msqgt0	$⊢ (1 \in ℝ \land 1 \neq 0) \to 0 < 1 \cdot 1$
4	1 2 3	mp2an	$⊢ 0 < 1 \cdot 1$
5		ax-1cn	$⊢ 1 \in ℂ$
6	5	mulridi	$⊢ 1 \cdot 1 = 1$
7	4 6	breqtri	$⊢ 0 < 1$