Metamath Proof Explorer

Theorem 17prm

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

Ref Expression
Assertion 17prm 
|- ; 1 7 e. Prime

Proof

Step Hyp Ref Expression
1 1nn0 
 |-  1 e. NN0
2 7nn 
 |-  7 e. NN
3 1 2 decnncl 
 |-  ; 1 7 e. NN
4 1nn 
 |-  1 e. NN
5 7nn0 
 |-  7 e. NN0
6 1lt10 
 |-  1 < ; 1 0
7 4 5 1 6 declti 
 |-  1 < ; 1 7
8 3nn0 
 |-  3 e. NN0
9 3t2e6 
 |-  ( 3 x. 2 ) = 6
10 df-7 
 |-  7 = ( 6 + 1 )
11 1 8 9 10 dec2dvds 
 |-  -. 2 || ; 1 7
12 3nn 
 |-  3 e. NN
13 5nn0 
 |-  5 e. NN0
14 2nn 
 |-  2 e. NN
15 2nn0 
 |-  2 e. NN0
16 5cn 
 |-  5 e. CC
17 3cn 
 |-  3 e. CC
18 5t3e15 
 |-  ( 5 x. 3 ) = ; 1 5
19 16 17 18 mulcomli 
 |-  ( 3 x. 5 ) = ; 1 5
20 5p2e7 
 |-  ( 5 + 2 ) = 7
21 1 13 15 19 20 decaddi 
 |-  ( ( 3 x. 5 ) + 2 ) = ; 1 7
22 2lt3 
 |-  2 < 3
23 12 13 14 21 22 ndvdsi 
 |-  -. 3 || ; 1 7
24 7lt10 
 |-  7 < ; 1 0
25 1lt2 
 |-  1 < 2
26 1 15 5 13 24 25 decltc 
 |-  ; 1 7 < ; 2 5
27 3 7 11 23 26 prmlem1 
 |-  ; 1 7 e. Prime