Metamath Proof Explorer

Theorem 5prm

Description: 5 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014) (Revised by Mario Carneiro, 20-Apr-2015)

Ref Expression
Assertion 5prm 
|- 5 e. Prime

Proof

Step Hyp Ref Expression
1 5nn 
 |-  5 e. NN
2 1lt5 
 |-  1 < 5
3 2nn 
 |-  2 e. NN
4 2nn0 
 |-  2 e. NN0
5 1nn 
 |-  1 e. NN
6 2t2e4 
 |-  ( 2 x. 2 ) = 4
7 6 oveq1i 
 |-  ( ( 2 x. 2 ) + 1 ) = ( 4 + 1 )
8 df-5 
 |-  5 = ( 4 + 1 )
9 7 8 eqtr4i 
 |-  ( ( 2 x. 2 ) + 1 ) = 5
10 1lt2 
 |-  1 < 2
11 3 4 5 9 10 ndvdsi 
 |-  -. 2 || 5
12 3nn 
 |-  3 e. NN
13 1nn0 
 |-  1 e. NN0
14 3t1e3 
 |-  ( 3 x. 1 ) = 3
15 14 oveq1i 
 |-  ( ( 3 x. 1 ) + 2 ) = ( 3 + 2 )
16 3p2e5 
 |-  ( 3 + 2 ) = 5
17 15 16 eqtri 
 |-  ( ( 3 x. 1 ) + 2 ) = 5
18 2lt3 
 |-  2 < 3
19 12 13 3 17 18 ndvdsi 
 |-  -. 3 || 5
20 5nn0 
 |-  5 e. NN0
21 5lt10 
 |-  5 < ; 1 0
22 3 20 20 21 declti 
 |-  5 < ; 2 5
23 1 2 11 19 22 prmlem1 
 |-  5 e. Prime