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 3cn 
 |-  3 e. CC
7 2cn 
 |-  2 e. CC
8 3t2e6 
 |-  ( 3 x. 2 ) = 6
9 6 7 8 mulcomli 
 |-  ( 2 x. 3 ) = 6
10 9 oveq1i 
 |-  ( ( 2 x. 3 ) + 1 ) = ( 6 + 1 )
11 df-7 
 |-  7 = ( 6 + 1 )
12 10 11 eqtr4i 
 |-  ( ( 2 x. 3 ) + 1 ) = 7
13 1lt2 
 |-  1 < 2
14 3 4 5 12 13 ndvdsi 
 |-  -. 2 || 7
15 3nn 
 |-  3 e. NN
16 2nn0 
 |-  2 e. NN0
17 8 oveq1i 
 |-  ( ( 3 x. 2 ) + 1 ) = ( 6 + 1 )
18 17 11 eqtr4i 
 |-  ( ( 3 x. 2 ) + 1 ) = 7
19 1lt3 
 |-  1 < 3
20 15 16 5 18 19 ndvdsi 
 |-  -. 3 || 7
21 5nn0 
 |-  5 e. NN0
22 7nn0 
 |-  7 e. NN0
23 7lt10 
 |-  7 < ; 1 0
24 3 21 22 23 declti 
 |-  7 < ; 2 5
25 1 2 14 20 24 prmlem1 
 |-  7 e. Prime