Metamath Proof Explorer

Theorem 7prm

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

Ref Expression
Assertion 7prm 
|- 7 e. Prime

Proof

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