Metamath Proof Explorer

Theorem 5eluz3

Description: 5 is an integer greater than or equal to 3. (Contributed by AV, 7-Sep-2025)

Ref Expression
Assertion 5eluz3 
|- 5 e. ( ZZ>= ` 3 )

Proof

Step Hyp Ref Expression
1 3z 
 |-  3 e. ZZ
2 5nn 
 |-  5 e. NN
3 2 nnzi 
 |-  5 e. ZZ
4 3re 
 |-  3 e. RR
5 5re 
 |-  5 e. RR
6 3lt5 
 |-  3 < 5
7 4 5 6 ltleii 
 |-  3 <_ 5
8 eluz2 
 |-  ( 5 e. ( ZZ>= ` 3 ) <-> ( 3 e. ZZ /\ 5 e. ZZ /\ 3 <_ 5 ) )
9 1 3 7 8 mpbir3an 
 |-  5 e. ( ZZ>= ` 3 )