Metamath Proof Explorer

Theorem 37prm

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

Ref Expression
Assertion 37prm 
|- ; 3 7 e. Prime

Proof

Step Hyp Ref Expression
1 3nn0 
 |-  3 e. NN0
2 7nn 
 |-  7 e. NN
3 1 2 decnncl 
 |-  ; 3 7 e. NN
4 8nn0 
 |-  8 e. NN0
5 4nn0 
 |-  4 e. NN0
6 4 5 deccl 
 |-  ; 8 4 e. NN0
7 7nn0 
 |-  7 e. NN0
8 1nn0 
 |-  1 e. NN0
9 7lt10 
 |-  7 < ; 1 0
10 8nn 
 |-  8 e. NN
11 3lt10 
 |-  3 < ; 1 0
12 10 5 1 11 declti 
 |-  3 < ; 8 4
13 1 6 7 8 9 12 decltc 
 |-  ; 3 7 < ; ; 8 4 1
14 3nn 
 |-  3 e. NN
15 1lt10 
 |-  1 < ; 1 0
16 14 7 8 15 declti 
 |-  1 < ; 3 7
17 3t2e6 
 |-  ( 3 x. 2 ) = 6
18 df-7 
 |-  7 = ( 6 + 1 )
19 1 1 17 18 dec2dvds 
 |-  -. 2 || ; 3 7
20 2nn0 
 |-  2 e. NN0
21 8 20 deccl 
 |-  ; 1 2 e. NN0
22 1nn 
 |-  1 e. NN
23 6nn0 
 |-  6 e. NN0
24 6p1e7 
 |-  ( 6 + 1 ) = 7
25 eqid 
 |-  ; 1 2 = ; 1 2
26 0nn0 
 |-  0 e. NN0
27 3cn 
 |-  3 e. CC
28 27 mulid1i 
 |-  ( 3 x. 1 ) = 3
29 28 oveq1i 
 |-  ( ( 3 x. 1 ) + 0 ) = ( 3 + 0 )
30 27 addid1i 
 |-  ( 3 + 0 ) = 3
31 29 30 eqtri 
 |-  ( ( 3 x. 1 ) + 0 ) = 3
32 23 dec0h 
 |-  6 = ; 0 6
33 17 32 eqtri 
 |-  ( 3 x. 2 ) = ; 0 6
34 1 8 20 25 23 26 31 33 decmul2c 
 |-  ( 3 x. ; 1 2 ) = ; 3 6
35 1 23 24 34 decsuc 
 |-  ( ( 3 x. ; 1 2 ) + 1 ) = ; 3 7
36 1lt3 
 |-  1 < 3
37 14 21 22 35 36 ndvdsi 
 |-  -. 3 || ; 3 7
38 2nn 
 |-  2 e. NN
39 2lt5 
 |-  2 < 5
40 5p2e7 
 |-  ( 5 + 2 ) = 7
41 1 38 39 40 dec5dvds2 
 |-  -. 5 || ; 3 7
42 5nn0 
 |-  5 e. NN0
43 7t5e35 
 |-  ( 7 x. 5 ) = ; 3 5
44 1 42 20 43 40 decaddi 
 |-  ( ( 7 x. 5 ) + 2 ) = ; 3 7
45 2lt7 
 |-  2 < 7
46 2 42 38 44 45 ndvdsi 
 |-  -. 7 || ; 3 7
47 8 22 decnncl 
 |-  ; 1 1 e. NN
48 4nn 
 |-  4 e. NN
49 eqid 
 |-  ; 1 1 = ; 1 1
50 27 mulid2i 
 |-  ( 1 x. 3 ) = 3
51 50 oveq1i 
 |-  ( ( 1 x. 3 ) + 4 ) = ( 3 + 4 )
52 48 nncni 
 |-  4 e. CC
53 4p3e7 
 |-  ( 4 + 3 ) = 7
54 52 27 53 addcomli 
 |-  ( 3 + 4 ) = 7
55 51 54 eqtri 
 |-  ( ( 1 x. 3 ) + 4 ) = 7
56 8 8 5 49 1 50 55 decrmanc 
 |-  ( ( ; 1 1 x. 3 ) + 4 ) = ; 3 7
57 4lt10 
 |-  4 < ; 1 0
58 22 8 5 57 declti 
 |-  4 < ; 1 1
59 47 1 48 56 58 ndvdsi 
 |-  -. ; 1 1 || ; 3 7
60 8 14 decnncl 
 |-  ; 1 3 e. NN
61 eqid 
 |-  ; 1 3 = ; 1 3
62 2cn 
 |-  2 e. CC
63 62 mulid2i 
 |-  ( 1 x. 2 ) = 2
64 20 8 1 61 63 17 decmul1 
 |-  ( ; 1 3 x. 2 ) = ; 2 6
65 2p1e3 
 |-  ( 2 + 1 ) = 3
66 20 23 8 8 64 49 65 24 decadd 
 |-  ( ( ; 1 3 x. 2 ) + ; 1 1 ) = ; 3 7
67 8 8 14 36 declt 
 |-  ; 1 1 < ; 1 3
68 60 20 47 66 67 ndvdsi 
 |-  -. ; 1 3 || ; 3 7
69 8 2 decnncl 
 |-  ; 1 7 e. NN
70 eqid 
 |-  ; 1 7 = ; 1 7
71 1 dec0h 
 |-  3 = ; 0 3
72 0p1e1 
 |-  ( 0 + 1 ) = 1
73 63 72 oveq12i 
 |-  ( ( 1 x. 2 ) + ( 0 + 1 ) ) = ( 2 + 1 )
74 73 65 eqtri 
 |-  ( ( 1 x. 2 ) + ( 0 + 1 ) ) = 3
75 7t2e14 
 |-  ( 7 x. 2 ) = ; 1 4
76 8 5 1 75 53 decaddi 
 |-  ( ( 7 x. 2 ) + 3 ) = ; 1 7
77 8 7 26 1 70 71 20 7 8 74 76 decmac 
 |-  ( ( ; 1 7 x. 2 ) + 3 ) = ; 3 7
78 22 7 1 11 declti 
 |-  3 < ; 1 7
79 69 20 14 77 78 ndvdsi 
 |-  -. ; 1 7 || ; 3 7
80 9nn 
 |-  9 e. NN
81 8 80 decnncl 
 |-  ; 1 9 e. NN
82 8 10 decnncl 
 |-  ; 1 8 e. NN
83 9nn0 
 |-  9 e. NN0
84 81 nncni 
 |-  ; 1 9 e. CC
85 84 mulid1i 
 |-  ( ; 1 9 x. 1 ) = ; 1 9
86 eqid 
 |-  ; 1 8 = ; 1 8
87 1p1e2 
 |-  ( 1 + 1 ) = 2
88 87 oveq1i 
 |-  ( ( 1 + 1 ) + 1 ) = ( 2 + 1 )
89 88 65 eqtri 
 |-  ( ( 1 + 1 ) + 1 ) = 3
90 9p8e17 
 |-  ( 9 + 8 ) = ; 1 7
91 8 83 8 4 85 86 89 7 90 decaddc 
 |-  ( ( ; 1 9 x. 1 ) + ; 1 8 ) = ; 3 7
92 8lt9 
 |-  8 < 9
93 8 4 80 92 declt 
 |-  ; 1 8 < ; 1 9
94 81 8 82 91 93 ndvdsi 
 |-  -. ; 1 9 || ; 3 7
95 20 14 decnncl 
 |-  ; 2 3 e. NN
96 8 48 decnncl 
 |-  ; 1 4 e. NN
97 95 nncni 
 |-  ; 2 3 e. CC
98 97 mulid1i 
 |-  ( ; 2 3 x. 1 ) = ; 2 3
99 eqid 
 |-  ; 1 4 = ; 1 4
100 20 1 8 5 98 99 65 54 decadd 
 |-  ( ( ; 2 3 x. 1 ) + ; 1 4 ) = ; 3 7
101 1lt2 
 |-  1 < 2
102 8 20 5 1 57 101 decltc 
 |-  ; 1 4 < ; 2 3
103 95 8 96 100 102 ndvdsi 
 |-  -. ; 2 3 || ; 3 7
104 3 13 16 19 37 41 46 59 68 79 94 103 prmlem2 
 |-  ; 3 7 e. Prime