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 10
2 3nn0 30
3 1 2 deccl 130
4 9nn 9
5 3 4 decnncl 139
6 8nn0 80
7 4nn0 40
8 9nn0 90
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 42=8
18 df-9 9=8+1
19 3 7 17 18 dec2dvds ¬2139
20 3ndvds4 ¬34
21 1 2 3dvdsdec 31331+3
22 3cn 3
23 ax-1cn 1
24 3p1e4 3+1=4
25 22 23 24 addcomli 1+3=4
26 25 breq2i 31+334
27 21 26 bitri 31334
28 20 27 mtbir ¬313
29 1 2 8 3dvds2dec 313931+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 31+3+9313
37 29 36 bitri 3139313
38 28 37 mtbir ¬3139
39 4nn 4
40 4lt5 4<5
41 5p4e9 5+4=9
42 3 39 40 41 dec5dvds2 ¬5139
43 7nn 7
44 1 8 deccl 190
45 6nn 6
46 0nn0 00
47 6nn0 60
48 eqid 19=19
49 47 dec0h 6=06
50 7nn0 70
51 7cn 7
52 51 mulridi 71=7
53 6cn 6
54 53 addlidi 0+6=6
55 52 54 oveq12i 71+0+6=7+6
56 7p6e13 7+6=13
57 55 56 eqtri 71+0+6=13
58 9t7e63 97=63
59 31 51 58 mulcomli 79=63
60 6p3e9 6+3=9
61 53 22 60 addcomli 3+6=9
62 47 2 47 59 61 decaddi 79+6=69
63 1 8 46 47 48 49 50 8 47 57 62 decma2c 719+6=139
64 6lt7 6<7
65 43 44 45 63 64 ndvdsi ¬7139
66 1nn 1
67 1 66 decnncl 11
68 2nn0 20
69 1 68 deccl 120
70 eqid 12=12
71 50 dec0h 7=07
72 1 1 deccl 110
73 2cn 2
74 73 addlidi 0+2=2
75 74 oveq2i 111+0+2=111+2
76 67 nncni 11
77 76 mulridi 111=11
78 1p2e3 1+2=3
79 1 1 68 77 78 decaddi 111+2=13
80 75 79 eqtri 111+0+2=13
81 eqid 11=11
82 73 mullidi 12=2
83 00id 0+0=0
84 82 83 oveq12i 12+0+0=2+0
85 73 addridi 2+0=2
86 84 85 eqtri 12+0+0=2
87 82 oveq1i 12+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 12+7=09
92 1 1 46 50 81 71 68 8 46 86 91 decmac 112+7=29
93 1 68 46 50 70 71 72 8 68 80 92 decma2c 1112+7=139
94 7lt10 7<10
95 66 1 50 94 declti 7<11
96 67 69 43 93 95 ndvdsi ¬11139
97 1 46 deccl 100
98 eqid 10=10
99 3 nn0cni 13
100 99 mulridi 131=13
101 100 83 oveq12i 131+0+0=13+0
102 99 addridi 13+0=13
103 101 102 eqtri 131+0+0=13
104 99 mul01i 130=0
105 104 oveq1i 130+9=0+9
106 31 addlidi 0+9=9
107 105 106 90 3eqtri 130+9=09
108 1 46 46 8 98 90 3 8 46 103 107 decma2c 1310+9=139
109 66 2 8 11 declti 9<13
110 14 97 4 108 109 ndvdsi ¬13139
111 1 43 decnncl 17
112 eqid 17=17
113 2 dec0h 3=03
114 5nn0 50
115 8cn 8
116 115 mullidi 18=8
117 5cn 5
118 117 addlidi 0+5=5
119 116 118 oveq12i 18+0+5=8+5
120 8p5e13 8+5=13
121 119 120 eqtri 18+0+5=13
122 8t7e56 87=56
123 115 51 122 mulcomli 78=56
124 114 47 2 123 60 decaddi 78+3=59
125 1 50 46 2 112 113 6 8 114 121 124 decmac 178+3=139
126 66 50 2 10 declti 3<17
127 111 6 13 125 126 ndvdsi ¬17139
128 1 4 decnncl 19
129 51 mullidi 17=7
130 129 54 oveq12i 17+0+6=7+6
131 130 56 eqtri 17+0+6=13
132 47 2 47 58 61 decaddi 97+6=69
133 1 8 46 47 48 49 50 8 47 131 132 decmac 197+6=139
134 6lt10 6<10
135 66 8 47 134 declti 6<19
136 128 50 45 133 135 ndvdsi ¬19139
137 68 13 decnncl 23
138 eqid 23=23
139 2p1e3 2+1=3
140 6t2e12 62=12
141 53 73 140 mulcomli 26=12
142 1 68 139 141 decsuc 26+1=13
143 8p1e9 8+1=9
144 6t3e18 63=18
145 53 22 144 mulcomli 36=18
146 1 6 143 145 decsuc 36+1=19
147 68 2 1 138 47 8 1 142 146 decrmac 236+1=139
148 2nn 2
149 148 2 1 15 declti 1<23
150 137 47 66 147 149 ndvdsi ¬23139
151 5 12 16 19 38 42 65 96 110 127 136 150 prmlem2 139