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

Proof

Step Hyp Ref Expression
1 1re 
 |-  1 e. RR
2 ax-1ne0 
 |-  1 =/= 0
3 msqgt0 
 |-  ( ( 1 e. RR /\ 1 =/= 0 ) -> 0 < ( 1 x. 1 ) )
4 1 2 3 mp2an 
 |-  0 < ( 1 x. 1 )
5 ax-1cn 
 |-  1 e. CC
6 5 mulid1i 
 |-  ( 1 x. 1 ) = 1
7 4 6 breqtri 
 |-  0 < 1