Metamath Proof Explorer

Theorem 43prm

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

Ref Expression
Assertion 43prm 4 3 ∈ ℙ

Proof

Step Hyp Ref Expression
1 4nn0 ⊢ 4 ∈ ℕ0
2 3nn ⊢ 3 ∈ ℕ
3 1 2 decnncl ⊢ 4 3 ∈ ℕ
4 8nn0 ⊢ 8 ∈ ℕ0
5 4 1 deccl ⊢ 8 4 ∈ ℕ0
6 3nn0 ⊢ 3 ∈ ℕ0
7 1nn0 ⊢ 1 ∈ ℕ0
8 3lt10 ⊢ 3 < 1 0
9 8nn ⊢ 8 ∈ ℕ
10 4lt10 ⊢ 4 < 1 0
11 9 1 1 10 declti ⊢ 4 < 8 4
12 1 5 6 7 8 11 decltc ⊢ 4 3 < 8 4 1
13 4nn ⊢ 4 ∈ ℕ
14 1lt10 ⊢ 1 < 1 0
15 13 6 7 14 declti ⊢ 1 < 4 3
16 2cn ⊢ 2 ∈ ℂ
17 16 mulid2i ⊢ ( 1 · 2 ) = 2
18 df-3 ⊢ 3 = ( 2 + 1 )
19 1 7 17 18 dec2dvds ⊢ ¬ 2 ∥ 4 3
20 7 1 deccl ⊢ 1 4 ∈ ℕ0
21 1nn ⊢ 1 ∈ ℕ
22 0nn0 ⊢ 0 ∈ ℕ0
23 eqid ⊢ 1 4 = 1 4
24 7 dec0h ⊢ 1 = 0 1
25 3cn ⊢ 3 ∈ ℂ
26 25 mulid1i ⊢ ( 3 · 1 ) = 3
27 ax-1cn ⊢ 1 ∈ ℂ
28 27 addid2i ⊢ ( 0 + 1 ) = 1
29 26 28 oveq12i ⊢ ( ( 3 · 1 ) + ( 0 + 1 ) ) = ( 3 + 1 )
30 3p1e4 ⊢ ( 3 + 1 ) = 4
31 29 30 eqtri ⊢ ( ( 3 · 1 ) + ( 0 + 1 ) ) = 4
32 2nn0 ⊢ 2 ∈ ℕ0
33 2p1e3 ⊢ ( 2 + 1 ) = 3
34 4cn ⊢ 4 ∈ ℂ
35 4t3e12 ⊢ ( 4 · 3 ) = 1 2
36 34 25 35 mulcomli ⊢ ( 3 · 4 ) = 1 2
37 7 32 33 36 decsuc ⊢ ( ( 3 · 4 ) + 1 ) = 1 3
38 7 1 22 7 23 24 6 6 7 31 37 decma2c ⊢ ( ( 3 · 1 4 ) + 1 ) = 4 3
39 1lt3 ⊢ 1 < 3
40 2 20 21 38 39 ndvdsi ⊢ ¬ 3 ∥ 4 3
41 3lt5 ⊢ 3 < 5
42 1 2 41 dec5dvds ⊢ ¬ 5 ∥ 4 3
43 7nn ⊢ 7 ∈ ℕ
44 6nn0 ⊢ 6 ∈ ℕ0
45 7t6e42 ⊢ ( 7 · 6 ) = 4 2
46 1 32 33 45 decsuc ⊢ ( ( 7 · 6 ) + 1 ) = 4 3
47 1lt7 ⊢ 1 < 7
48 43 44 21 46 47 ndvdsi ⊢ ¬ 7 ∥ 4 3
49 7 21 decnncl ⊢ 1 1 ∈ ℕ
50 21 decnncl2 ⊢ 1 0 ∈ ℕ
51 eqid ⊢ 1 1 = 1 1
52 eqid ⊢ 1 0 = 1 0
53 25 mulid2i ⊢ ( 1 · 3 ) = 3
54 27 addid1i ⊢ ( 1 + 0 ) = 1
55 53 54 oveq12i ⊢ ( ( 1 · 3 ) + ( 1 + 0 ) ) = ( 3 + 1 )
56 55 30 eqtri ⊢ ( ( 1 · 3 ) + ( 1 + 0 ) ) = 4
57 53 oveq1i ⊢ ( ( 1 · 3 ) + 0 ) = ( 3 + 0 )
58 25 addid1i ⊢ ( 3 + 0 ) = 3
59 6 dec0h ⊢ 3 = 0 3
60 57 58 59 3eqtri ⊢ ( ( 1 · 3 ) + 0 ) = 0 3
61 7 7 7 22 51 52 6 6 22 56 60 decmac ⊢ ( ( 1 1 · 3 ) + 1 0 ) = 4 3
62 0lt1 ⊢ 0 < 1
63 7 22 21 62 declt ⊢ 1 0 < 1 1
64 49 6 50 61 63 ndvdsi ⊢ ¬ 1 1 ∥ 4 3
65 7 2 decnncl ⊢ 1 3 ∈ ℕ
66 eqid ⊢ 1 3 = 1 3
67 1 dec0h ⊢ 4 = 0 4
68 53 28 oveq12i ⊢ ( ( 1 · 3 ) + ( 0 + 1 ) ) = ( 3 + 1 )
69 68 30 eqtri ⊢ ( ( 1 · 3 ) + ( 0 + 1 ) ) = 4
70 3t3e9 ⊢ ( 3 · 3 ) = 9
71 70 oveq1i ⊢ ( ( 3 · 3 ) + 4 ) = ( 9 + 4 )
72 9p4e13 ⊢ ( 9 + 4 ) = 1 3
73 71 72 eqtri ⊢ ( ( 3 · 3 ) + 4 ) = 1 3
74 7 6 22 1 66 67 6 6 7 69 73 decmac ⊢ ( ( 1 3 · 3 ) + 4 ) = 4 3
75 21 6 1 10 declti ⊢ 4 < 1 3
76 65 6 13 74 75 ndvdsi ⊢ ¬ 1 3 ∥ 4 3
77 7 43 decnncl ⊢ 1 7 ∈ ℕ
78 9nn ⊢ 9 ∈ ℕ
79 43 nnnn0i ⊢ 7 ∈ ℕ0
80 78 nnnn0i ⊢ 9 ∈ ℕ0
81 eqid ⊢ 1 7 = 1 7
82 80 dec0h ⊢ 9 = 0 9
83 16 addid2i ⊢ ( 0 + 2 ) = 2
84 17 83 oveq12i ⊢ ( ( 1 · 2 ) + ( 0 + 2 ) ) = ( 2 + 2 )
85 2p2e4 ⊢ ( 2 + 2 ) = 4
86 84 85 eqtri ⊢ ( ( 1 · 2 ) + ( 0 + 2 ) ) = 4
87 7t2e14 ⊢ ( 7 · 2 ) = 1 4
88 1p1e2 ⊢ ( 1 + 1 ) = 2
89 78 nncni ⊢ 9 ∈ ℂ
90 89 34 72 addcomli ⊢ ( 4 + 9 ) = 1 3
91 7 1 80 87 88 6 90 decaddci ⊢ ( ( 7 · 2 ) + 9 ) = 2 3
92 7 79 22 80 81 82 32 6 32 86 91 decmac ⊢ ( ( 1 7 · 2 ) + 9 ) = 4 3
93 9lt10 ⊢ 9 < 1 0
94 21 79 80 93 declti ⊢ 9 < 1 7
95 77 32 78 92 94 ndvdsi ⊢ ¬ 1 7 ∥ 4 3
96 7 78 decnncl ⊢ 1 9 ∈ ℕ
97 5nn ⊢ 5 ∈ ℕ
98 97 nnnn0i ⊢ 5 ∈ ℕ0
99 eqid ⊢ 1 9 = 1 9
100 98 dec0h ⊢ 5 = 0 5
101 9t2e18 ⊢ ( 9 · 2 ) = 1 8
102 8p5e13 ⊢ ( 8 + 5 ) = 1 3
103 7 4 98 101 88 6 102 decaddci ⊢ ( ( 9 · 2 ) + 5 ) = 2 3
104 7 80 22 98 99 100 32 6 32 86 103 decmac ⊢ ( ( 1 9 · 2 ) + 5 ) = 4 3
105 5lt10 ⊢ 5 < 1 0
106 21 80 98 105 declti ⊢ 5 < 1 9
107 96 32 97 104 106 ndvdsi ⊢ ¬ 1 9 ∥ 4 3
108 32 2 decnncl ⊢ 2 3 ∈ ℕ
109 2nn ⊢ 2 ∈ ℕ
110 109 decnncl2 ⊢ 2 0 ∈ ℕ
111 108 nncni ⊢ 2 3 ∈ ℂ
112 111 mulid1i ⊢ ( 2 3 · 1 ) = 2 3
113 eqid ⊢ 2 0 = 2 0
114 32 6 32 22 112 113 85 58 decadd ⊢ ( ( 2 3 · 1 ) + 2 0 ) = 4 3
115 3pos ⊢ 0 < 3
116 32 22 2 115 declt ⊢ 2 0 < 2 3
117 108 7 110 114 116 ndvdsi ⊢ ¬ 2 3 ∥ 4 3
118 3 12 15 19 40 42 48 64 76 95 107 117 prmlem2 ⊢ 4 3 ∈ ℙ