This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

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