Metamath Proof Explorer

Theorem nnle1eq1

Description: A positive integer is less than or equal to one iff it is equal to one. (Contributed by NM, 3-Apr-2005)

Ref Expression
Assertion nnle1eq1 
|- ( A e. NN -> ( A <_ 1 <-> A = 1 ) )

Proof

Step Hyp Ref Expression
1 nnge1 
 |-  ( A e. NN -> 1 <_ A )
2 1 biantrud 
 |-  ( A e. NN -> ( A <_ 1 <-> ( A <_ 1 /\ 1 <_ A ) ) )
3 nnre 
 |-  ( A e. NN -> A e. RR )
4 1re 
 |-  1 e. RR
5 letri3 
 |-  ( ( A e. RR /\ 1 e. RR ) -> ( A = 1 <-> ( A <_ 1 /\ 1 <_ A ) ) )
6 3 4 5 sylancl 
 |-  ( A e. NN -> ( A = 1 <-> ( A <_ 1 /\ 1 <_ A ) ) )
7 2 6 bitr4d 
 |-  ( A e. NN -> ( A <_ 1 <-> A = 1 ) )