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 ∈ ℙ

Proof

Step Hyp Ref Expression
1 3nn0 ⊢ 3 ∈ ℕ0
2 7nn ⊢ 7 ∈ ℕ
3 1 2 decnncl ⊢ 3 7 ∈ ℕ
4 8nn0 ⊢ 8 ∈ ℕ0
5 4nn0 ⊢ 4 ∈ ℕ0
6 4 5 deccl ⊢ 8 4 ∈ ℕ0
7 7nn0 ⊢ 7 ∈ ℕ0
8 1nn0 ⊢ 1 ∈ ℕ0
9 7lt10 ⊢ 7 < 1 0
10 8nn ⊢ 8 ∈ ℕ
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 ∈ ℕ
15 1lt10 ⊢ 1 < 1 0
16 14 7 8 15 declti ⊢ 1 < 3 7
17 3t2e6 ⊢ ( 3 · 2 ) = 6
18 df-7 ⊢ 7 = ( 6 + 1 )
19 1 1 17 18 dec2dvds ⊢ ¬ 2 ∥ 3 7
20 2nn0 ⊢ 2 ∈ ℕ0
21 8 20 deccl ⊢ 1 2 ∈ ℕ0
22 1nn ⊢ 1 ∈ ℕ
23 6nn0 ⊢ 6 ∈ ℕ0
24 6p1e7 ⊢ ( 6 + 1 ) = 7
25 eqid ⊢ 1 2 = 1 2
26 0nn0 ⊢ 0 ∈ ℕ0
27 3cn ⊢ 3 ∈ ℂ
28 27 mulid1i ⊢ ( 3 · 1 ) = 3
29 28 oveq1i ⊢ ( ( 3 · 1 ) + 0 ) = ( 3 + 0 )
30 27 addid1i ⊢ ( 3 + 0 ) = 3
31 29 30 eqtri ⊢ ( ( 3 · 1 ) + 0 ) = 3
32 23 dec0h ⊢ 6 = 0 6
33 17 32 eqtri ⊢ ( 3 · 2 ) = 0 6
34 1 8 20 25 23 26 31 33 decmul2c ⊢ ( 3 · 1 2 ) = 3 6
35 1 23 24 34 decsuc ⊢ ( ( 3 · 1 2 ) + 1 ) = 3 7
36 1lt3 ⊢ 1 < 3
37 14 21 22 35 36 ndvdsi ⊢ ¬ 3 ∥ 3 7
38 2nn ⊢ 2 ∈ ℕ
39 2lt5 ⊢ 2 < 5
40 5p2e7 ⊢ ( 5 + 2 ) = 7
41 1 38 39 40 dec5dvds2 ⊢ ¬ 5 ∥ 3 7
42 5nn0 ⊢ 5 ∈ ℕ0
43 7t5e35 ⊢ ( 7 · 5 ) = 3 5
44 1 42 20 43 40 decaddi ⊢ ( ( 7 · 5 ) + 2 ) = 3 7
45 2lt7 ⊢ 2 < 7
46 2 42 38 44 45 ndvdsi ⊢ ¬ 7 ∥ 3 7
47 8 22 decnncl ⊢ 1 1 ∈ ℕ
48 4nn ⊢ 4 ∈ ℕ
49 eqid ⊢ 1 1 = 1 1
50 27 mulid2i ⊢ ( 1 · 3 ) = 3
51 50 oveq1i ⊢ ( ( 1 · 3 ) + 4 ) = ( 3 + 4 )
52 48 nncni ⊢ 4 ∈ ℂ
53 4p3e7 ⊢ ( 4 + 3 ) = 7
54 52 27 53 addcomli ⊢ ( 3 + 4 ) = 7
55 51 54 eqtri ⊢ ( ( 1 · 3 ) + 4 ) = 7
56 8 8 5 49 1 50 55 decrmanc ⊢ ( ( 1 1 · 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 ∈ ℕ
61 eqid ⊢ 1 3 = 1 3
62 2cn ⊢ 2 ∈ ℂ
63 62 mulid2i ⊢ ( 1 · 2 ) = 2
64 20 8 1 61 63 17 decmul1 ⊢ ( 1 3 · 2 ) = 2 6
65 2p1e3 ⊢ ( 2 + 1 ) = 3
66 20 23 8 8 64 49 65 24 decadd ⊢ ( ( 1 3 · 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 ∈ ℕ
70 eqid ⊢ 1 7 = 1 7
71 1 dec0h ⊢ 3 = 0 3
72 0p1e1 ⊢ ( 0 + 1 ) = 1
73 63 72 oveq12i ⊢ ( ( 1 · 2 ) + ( 0 + 1 ) ) = ( 2 + 1 )
74 73 65 eqtri ⊢ ( ( 1 · 2 ) + ( 0 + 1 ) ) = 3
75 7t2e14 ⊢ ( 7 · 2 ) = 1 4
76 8 5 1 75 53 decaddi ⊢ ( ( 7 · 2 ) + 3 ) = 1 7
77 8 7 26 1 70 71 20 7 8 74 76 decmac ⊢ ( ( 1 7 · 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 ∈ ℕ
81 8 80 decnncl ⊢ 1 9 ∈ ℕ
82 8 10 decnncl ⊢ 1 8 ∈ ℕ
83 9nn0 ⊢ 9 ∈ ℕ0
84 81 nncni ⊢ 1 9 ∈ ℂ
85 84 mulid1i ⊢ ( 1 9 · 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 · 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 ∈ ℕ
96 8 48 decnncl ⊢ 1 4 ∈ ℕ
97 95 nncni ⊢ 2 3 ∈ ℂ
98 97 mulid1i ⊢ ( 2 3 · 1 ) = 2 3
99 eqid ⊢ 1 4 = 1 4
100 20 1 8 5 98 99 65 54 decadd ⊢ ( ( 2 3 · 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 ∈ ℙ