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 mulid1i ( 7 · 1 ) = 7
53 6cn 6 ∈ ℂ
54 53 addid2i ( 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 addid2i ( 0 + 2 ) = 2
75 74 oveq2i ( ( 1 1 · 1 ) + ( 0 + 2 ) ) = ( ( 1 1 · 1 ) + 2 )
76 67 nncni 1 1 ∈ ℂ
77 76 mulid1i ( 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 mulid2i ( 1 · 2 ) = 2
83 00id ( 0 + 0 ) = 0
84 82 83 oveq12i ( ( 1 · 2 ) + ( 0 + 0 ) ) = ( 2 + 0 )
85 73 addid1i ( 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 mulid1i ( 1 3 · 1 ) = 1 3
101 100 83 oveq12i ( ( 1 3 · 1 ) + ( 0 + 0 ) ) = ( 1 3 + 0 )
102 99 addid1i ( 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 addid2i ( 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 mulid2i ( 1 · 8 ) = 8
117 5cn 5 ∈ ℂ
118 117 addid2i ( 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 mulid2i ( 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 ∈ ℙ