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 139

Proof

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