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$$

Proof

Step	Hyp	Ref	Expression
1		1re	$$⊢1\in ℝ$$
2		ax-1ne0	$$⊢1\ne 0$$
3		msqgt0	$$⊢\left(1\in ℝ\wedge 1\ne 0\right)\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$$