Metamath Proof Explorer

Theorem 13prm

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

Ref Expression
Assertion 13prm 
|- ; 1 3 e. Prime

Proof

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