Metamath Proof Explorer

Theorem 139prmALT

Description: 139 is a prime number. In contrast to 139prm , the proof of this theorem uses 3dvds2dec for checking the divisibility by 3. Although the proof using 3dvds2dec is longer (regarding size: 1849 characters compared with 1809 for 139prm ), the number of essential steps is smaller (301 compared with 327 for 139prm ). (Contributed by Mario Carneiro, 19-Feb-2014) (Revised by AV, 18-Aug-2021) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion 139prmALT 1 3 9 ∈ ℙ

Proof

Step Hyp Ref Expression
1 1nn0 ⊢ 1 ∈ ℕ0
2 3nn0 ⊢ 3 ∈ ℕ0
3 1 2 deccl ⊢ 1 3 ∈ ℕ0
4 9nn ⊢ 9 ∈ ℕ
5 3 4 decnncl ⊢ 1 3 9 ∈ ℕ
6 8nn0 ⊢ 8 ∈ ℕ0
7 4nn0 ⊢ 4 ∈ ℕ0
8 9nn0 ⊢ 9 ∈ ℕ0
9 1lt8 ⊢ 1 < 8
10 3lt10 ⊢ 3 < 1 0
11 9lt10 ⊢ 9 < 1 0
12 1 6 2 7 8 1 9 10 11 3decltc ⊢ 1 3 9 < 8 4 1
13 3nn ⊢ 3 ∈ ℕ
14 1 13 decnncl ⊢ 1 3 ∈ ℕ
15 1lt10 ⊢ 1 < 1 0
16 14 8 1 15 declti ⊢ 1 < 1 3 9
17 4t2e8 ⊢ ( 4 · 2 ) = 8
18 df-9 ⊢ 9 = ( 8 + 1 )
19 3 7 17 18 dec2dvds ⊢ ¬ 2 ∥ 1 3 9
20 3ndvds4 ⊢ ¬ 3 ∥ 4
21 1 2 3dvdsdec ⊢ ( 3 ∥ 1 3 ↔ 3 ∥ ( 1 + 3 ) )
22 3cn ⊢ 3 ∈ ℂ
23 ax-1cn ⊢ 1 ∈ ℂ
24 3p1e4 ⊢ ( 3 + 1 ) = 4
25 22 23 24 addcomli ⊢ ( 1 + 3 ) = 4
26 25 breq2i ⊢ ( 3 ∥ ( 1 + 3 ) ↔ 3 ∥ 4 )
27 21 26 bitri ⊢ ( 3 ∥ 1 3 ↔ 3 ∥ 4 )
28 20 27 mtbir ⊢ ¬ 3 ∥ 1 3
29 1 2 8 3dvds2dec ⊢ ( 3 ∥ 1 3 9 ↔ 3 ∥ ( ( 1 + 3 ) + 9 ) )
30 25 oveq1i ⊢ ( ( 1 + 3 ) + 9 ) = ( 4 + 9 )
31 9cn ⊢ 9 ∈ ℂ
32 4cn ⊢ 4 ∈ ℂ
33 9p4e13 ⊢ ( 9 + 4 ) = 1 3
34 31 32 33 addcomli ⊢ ( 4 + 9 ) = 1 3
35 30 34 eqtri ⊢ ( ( 1 + 3 ) + 9 ) = 1 3
36 35 breq2i ⊢ ( 3 ∥ ( ( 1 + 3 ) + 9 ) ↔ 3 ∥ 1 3 )
37 29 36 bitri ⊢ ( 3 ∥ 1 3 9 ↔ 3 ∥ 1 3 )
38 28 37 mtbir ⊢ ¬ 3 ∥ 1 3 9
39 4nn ⊢ 4 ∈ ℕ
40 4lt5 ⊢ 4 < 5
41 5p4e9 ⊢ ( 5 + 4 ) = 9
42 3 39 40 41 dec5dvds2 ⊢ ¬ 5 ∥ 1 3 9
43 7nn ⊢ 7 ∈ ℕ
44 1 8 deccl ⊢ 1 9 ∈ ℕ0
45 6nn ⊢ 6 ∈ ℕ
46 0nn0 ⊢ 0 ∈ ℕ0
47 6nn0 ⊢ 6 ∈ ℕ0
48 eqid ⊢ 1 9 = 1 9
49 47 dec0h ⊢ 6 = 0 6
50 7nn0 ⊢ 7 ∈ ℕ0
51 7cn ⊢ 7 ∈ ℂ
52 51 mulridi ⊢ ( 7 · 1 ) = 7
53 6cn ⊢ 6 ∈ ℂ
54 53 addlidi ⊢ ( 0 + 6 ) = 6
55 52 54 oveq12i ⊢ ( ( 7 · 1 ) + ( 0 + 6 ) ) = ( 7 + 6 )
56 7p6e13 ⊢ ( 7 + 6 ) = 1 3
57 55 56 eqtri ⊢ ( ( 7 · 1 ) + ( 0 + 6 ) ) = 1 3
58 9t7e63 ⊢ ( 9 · 7 ) = 6 3
59 31 51 58 mulcomli ⊢ ( 7 · 9 ) = 6 3
60 6p3e9 ⊢ ( 6 + 3 ) = 9
61 53 22 60 addcomli ⊢ ( 3 + 6 ) = 9
62 47 2 47 59 61 decaddi ⊢ ( ( 7 · 9 ) + 6 ) = 6 9
63 1 8 46 47 48 49 50 8 47 57 62 decma2c ⊢ ( ( 7 · 1 9 ) + 6 ) = 1 3 9
64 6lt7 ⊢ 6 < 7
65 43 44 45 63 64 ndvdsi ⊢ ¬ 7 ∥ 1 3 9
66 1nn ⊢ 1 ∈ ℕ
67 1 66 decnncl ⊢ 1 1 ∈ ℕ
68 2nn0 ⊢ 2 ∈ ℕ0
69 1 68 deccl ⊢ 1 2 ∈ ℕ0
70 eqid ⊢ 1 2 = 1 2
71 50 dec0h ⊢ 7 = 0 7
72 1 1 deccl ⊢ 1 1 ∈ ℕ0
73 2cn ⊢ 2 ∈ ℂ
74 73 addlidi ⊢ ( 0 + 2 ) = 2
75 74 oveq2i ⊢ ( ( 1 1 · 1 ) + ( 0 + 2 ) ) = ( ( 1 1 · 1 ) + 2 )
76 67 nncni ⊢ 1 1 ∈ ℂ
77 76 mulridi ⊢ ( 1 1 · 1 ) = 1 1
78 1p2e3 ⊢ ( 1 + 2 ) = 3
79 1 1 68 77 78 decaddi ⊢ ( ( 1 1 · 1 ) + 2 ) = 1 3
80 75 79 eqtri ⊢ ( ( 1 1 · 1 ) + ( 0 + 2 ) ) = 1 3
81 eqid ⊢ 1 1 = 1 1
82 73 mullidi ⊢ ( 1 · 2 ) = 2
83 00id ⊢ ( 0 + 0 ) = 0
84 82 83 oveq12i ⊢ ( ( 1 · 2 ) + ( 0 + 0 ) ) = ( 2 + 0 )
85 73 addridi ⊢ ( 2 + 0 ) = 2
86 84 85 eqtri ⊢ ( ( 1 · 2 ) + ( 0 + 0 ) ) = 2
87 82 oveq1i ⊢ ( ( 1 · 2 ) + 7 ) = ( 2 + 7 )
88 7p2e9 ⊢ ( 7 + 2 ) = 9
89 51 73 88 addcomli ⊢ ( 2 + 7 ) = 9
90 8 dec0h ⊢ 9 = 0 9
91 87 89 90 3eqtri ⊢ ( ( 1 · 2 ) + 7 ) = 0 9
92 1 1 46 50 81 71 68 8 46 86 91 decmac ⊢ ( ( 1 1 · 2 ) + 7 ) = 2 9
93 1 68 46 50 70 71 72 8 68 80 92 decma2c ⊢ ( ( 1 1 · 1 2 ) + 7 ) = 1 3 9
94 7lt10 ⊢ 7 < 1 0
95 66 1 50 94 declti ⊢ 7 < 1 1
96 67 69 43 93 95 ndvdsi ⊢ ¬ 1 1 ∥ 1 3 9
97 1 46 deccl ⊢ 1 0 ∈ ℕ0
98 eqid ⊢ 1 0 = 1 0
99 3 nn0cni ⊢ 1 3 ∈ ℂ
100 99 mulridi ⊢ ( 1 3 · 1 ) = 1 3
101 100 83 oveq12i ⊢ ( ( 1 3 · 1 ) + ( 0 + 0 ) ) = ( 1 3 + 0 )
102 99 addridi ⊢ ( 1 3 + 0 ) = 1 3
103 101 102 eqtri ⊢ ( ( 1 3 · 1 ) + ( 0 + 0 ) ) = 1 3
104 99 mul01i ⊢ ( 1 3 · 0 ) = 0
105 104 oveq1i ⊢ ( ( 1 3 · 0 ) + 9 ) = ( 0 + 9 )
106 31 addlidi ⊢ ( 0 + 9 ) = 9
107 105 106 90 3eqtri ⊢ ( ( 1 3 · 0 ) + 9 ) = 0 9
108 1 46 46 8 98 90 3 8 46 103 107 decma2c ⊢ ( ( 1 3 · 1 0 ) + 9 ) = 1 3 9
109 66 2 8 11 declti ⊢ 9 < 1 3
110 14 97 4 108 109 ndvdsi ⊢ ¬ 1 3 ∥ 1 3 9
111 1 43 decnncl ⊢ 1 7 ∈ ℕ
112 eqid ⊢ 1 7 = 1 7
113 2 dec0h ⊢ 3 = 0 3
114 5nn0 ⊢ 5 ∈ ℕ0
115 8cn ⊢ 8 ∈ ℂ
116 115 mullidi ⊢ ( 1 · 8 ) = 8
117 5cn ⊢ 5 ∈ ℂ
118 117 addlidi ⊢ ( 0 + 5 ) = 5
119 116 118 oveq12i ⊢ ( ( 1 · 8 ) + ( 0 + 5 ) ) = ( 8 + 5 )
120 8p5e13 ⊢ ( 8 + 5 ) = 1 3
121 119 120 eqtri ⊢ ( ( 1 · 8 ) + ( 0 + 5 ) ) = 1 3
122 8t7e56 ⊢ ( 8 · 7 ) = 5 6
123 115 51 122 mulcomli ⊢ ( 7 · 8 ) = 5 6
124 114 47 2 123 60 decaddi ⊢ ( ( 7 · 8 ) + 3 ) = 5 9
125 1 50 46 2 112 113 6 8 114 121 124 decmac ⊢ ( ( 1 7 · 8 ) + 3 ) = 1 3 9
126 66 50 2 10 declti ⊢ 3 < 1 7
127 111 6 13 125 126 ndvdsi ⊢ ¬ 1 7 ∥ 1 3 9
128 1 4 decnncl ⊢ 1 9 ∈ ℕ
129 51 mullidi ⊢ ( 1 · 7 ) = 7
130 129 54 oveq12i ⊢ ( ( 1 · 7 ) + ( 0 + 6 ) ) = ( 7 + 6 )
131 130 56 eqtri ⊢ ( ( 1 · 7 ) + ( 0 + 6 ) ) = 1 3
132 47 2 47 58 61 decaddi ⊢ ( ( 9 · 7 ) + 6 ) = 6 9
133 1 8 46 47 48 49 50 8 47 131 132 decmac ⊢ ( ( 1 9 · 7 ) + 6 ) = 1 3 9
134 6lt10 ⊢ 6 < 1 0
135 66 8 47 134 declti ⊢ 6 < 1 9
136 128 50 45 133 135 ndvdsi ⊢ ¬ 1 9 ∥ 1 3 9
137 68 13 decnncl ⊢ 2 3 ∈ ℕ
138 eqid ⊢ 2 3 = 2 3
139 2p1e3 ⊢ ( 2 + 1 ) = 3
140 6t2e12 ⊢ ( 6 · 2 ) = 1 2
141 53 73 140 mulcomli ⊢ ( 2 · 6 ) = 1 2
142 1 68 139 141 decsuc ⊢ ( ( 2 · 6 ) + 1 ) = 1 3
143 8p1e9 ⊢ ( 8 + 1 ) = 9
144 6t3e18 ⊢ ( 6 · 3 ) = 1 8
145 53 22 144 mulcomli ⊢ ( 3 · 6 ) = 1 8
146 1 6 143 145 decsuc ⊢ ( ( 3 · 6 ) + 1 ) = 1 9
147 68 2 1 138 47 8 1 142 146 decrmac ⊢ ( ( 2 3 · 6 ) + 1 ) = 1 3 9
148 2nn ⊢ 2 ∈ ℕ
149 148 2 1 15 declti ⊢ 1 < 2 3
150 137 47 66 147 149 ndvdsi ⊢ ¬ 2 3 ∥ 1 3 9
151 5 12 16 19 38 42 65 96 110 127 136 150 prmlem2 ⊢ 1 3 9 ∈ ℙ