# 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 ${⊢}43\in ℙ$

### Proof

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