Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  139prmALT Structured version   Visualization version   GIF version

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

Proof of Theorem 139prmALT
StepHypRef Expression
1 1nn0 11346 . . . 4 1 ∈ ℕ0
2 3nn0 11348 . . . 4 3 ∈ ℕ0
31, 2deccl 11550 . . 3 13 ∈ ℕ0
4 9nn 11230 . . 3 9 ∈ ℕ
53, 4decnncl 11556 . 2 139 ∈ ℕ
6 8nn0 11353 . . 3 8 ∈ ℕ0
7 4nn0 11349 . . 3 4 ∈ ℕ0
8 9nn0 11354 . . 3 9 ∈ ℕ0
9 1lt8 11259 . . 3 1 < 8
10 3lt10 11717 . . 3 3 < 10
11 9lt10 11711 . . 3 9 < 10
121, 6, 2, 7, 8, 1, 9, 10, 113decltc 11576 . 2 139 < 841
13 3nn 11224 . . . 4 3 ∈ ℕ
141, 13decnncl 11556 . . 3 13 ∈ ℕ
15 1lt10 11719 . . 3 1 < 10
1614, 8, 1, 15declti 11584 . 2 1 < 139
17 4t2e8 11219 . . 3 (4 · 2) = 8
18 df-9 11124 . . 3 9 = (8 + 1)
193, 7, 17, 18dec2dvds 15814 . 2 ¬ 2 ∥ 139
20 3ndvds4 41835 . . . 4 ¬ 3 ∥ 4
211, 23dvdsdec 15101 . . . . 5 (3 ∥ 13 ↔ 3 ∥ (1 + 3))
22 3cn 11133 . . . . . . 7 3 ∈ ℂ
23 ax-1cn 10032 . . . . . . 7 1 ∈ ℂ
24 3p1e4 11191 . . . . . . 7 (3 + 1) = 4
2522, 23, 24addcomli 10266 . . . . . 6 (1 + 3) = 4
2625breq2i 4693 . . . . 5 (3 ∥ (1 + 3) ↔ 3 ∥ 4)
2721, 26bitri 264 . . . 4 (3 ∥ 13 ↔ 3 ∥ 4)
2820, 27mtbir 312 . . 3 ¬ 3 ∥ 13
291, 2, 83dvds2dec 15103 . . . 4 (3 ∥ 139 ↔ 3 ∥ ((1 + 3) + 9))
3025oveq1i 6700 . . . . . 6 ((1 + 3) + 9) = (4 + 9)
31 9cn 11146 . . . . . . 7 9 ∈ ℂ
32 4cn 11136 . . . . . . 7 4 ∈ ℂ
33 9p4e13 11660 . . . . . . 7 (9 + 4) = 13
3431, 32, 33addcomli 10266 . . . . . 6 (4 + 9) = 13
3530, 34eqtri 2673 . . . . 5 ((1 + 3) + 9) = 13
3635breq2i 4693 . . . 4 (3 ∥ ((1 + 3) + 9) ↔ 3 ∥ 13)
3729, 36bitri 264 . . 3 (3 ∥ 139 ↔ 3 ∥ 13)
3828, 37mtbir 312 . 2 ¬ 3 ∥ 139
39 4nn 11225 . . 3 4 ∈ ℕ
40 4lt5 11238 . . 3 4 < 5
41 5p4e9 11205 . . 3 (5 + 4) = 9
423, 39, 40, 41dec5dvds2 15816 . 2 ¬ 5 ∥ 139
43 7nn 11228 . . 3 7 ∈ ℕ
441, 8deccl 11550 . . 3 19 ∈ ℕ0
45 6nn 11227 . . 3 6 ∈ ℕ
46 0nn0 11345 . . . 4 0 ∈ ℕ0
47 6nn0 11351 . . . 4 6 ∈ ℕ0
48 eqid 2651 . . . 4 19 = 19
4947dec0h 11560 . . . 4 6 = 06
50 7nn0 11352 . . . 4 7 ∈ ℕ0
51 7cn 11142 . . . . . . 7 7 ∈ ℂ
5251mulid1i 10080 . . . . . 6 (7 · 1) = 7
53 6cn 11140 . . . . . . 7 6 ∈ ℂ
5453addid2i 10262 . . . . . 6 (0 + 6) = 6
5552, 54oveq12i 6702 . . . . 5 ((7 · 1) + (0 + 6)) = (7 + 6)
56 7p6e13 11646 . . . . 5 (7 + 6) = 13
5755, 56eqtri 2673 . . . 4 ((7 · 1) + (0 + 6)) = 13
58 9t7e63 11706 . . . . . 6 (9 · 7) = 63
5931, 51, 58mulcomli 10085 . . . . 5 (7 · 9) = 63
60 6p3e9 11208 . . . . . 6 (6 + 3) = 9
6153, 22, 60addcomli 10266 . . . . 5 (3 + 6) = 9
6247, 2, 47, 59, 61decaddi 11617 . . . 4 ((7 · 9) + 6) = 69
631, 8, 46, 47, 48, 49, 50, 8, 47, 57, 62decma2c 11606 . . 3 ((7 · 19) + 6) = 139
64 6lt7 11247 . . 3 6 < 7
6543, 44, 45, 63, 64ndvdsi 15183 . 2 ¬ 7 ∥ 139
66 1nn 11069 . . . 4 1 ∈ ℕ
671, 66decnncl 11556 . . 3 11 ∈ ℕ
68 2nn0 11347 . . . 4 2 ∈ ℕ0
691, 68deccl 11550 . . 3 12 ∈ ℕ0
70 eqid 2651 . . . 4 12 = 12
7150dec0h 11560 . . . 4 7 = 07
721, 1deccl 11550 . . . 4 11 ∈ ℕ0
73 2cn 11129 . . . . . . 7 2 ∈ ℂ
7473addid2i 10262 . . . . . 6 (0 + 2) = 2
7574oveq2i 6701 . . . . 5 ((11 · 1) + (0 + 2)) = ((11 · 1) + 2)
7667nncni 11068 . . . . . . 7 11 ∈ ℂ
7776mulid1i 10080 . . . . . 6 (11 · 1) = 11
78 1p2e3 11190 . . . . . 6 (1 + 2) = 3
791, 1, 68, 77, 78decaddi 11617 . . . . 5 ((11 · 1) + 2) = 13
8075, 79eqtri 2673 . . . 4 ((11 · 1) + (0 + 2)) = 13
81 eqid 2651 . . . . 5 11 = 11
8273mulid2i 10081 . . . . . . 7 (1 · 2) = 2
83 00id 10249 . . . . . . 7 (0 + 0) = 0
8482, 83oveq12i 6702 . . . . . 6 ((1 · 2) + (0 + 0)) = (2 + 0)
8573addid1i 10261 . . . . . 6 (2 + 0) = 2
8684, 85eqtri 2673 . . . . 5 ((1 · 2) + (0 + 0)) = 2
8782oveq1i 6700 . . . . . 6 ((1 · 2) + 7) = (2 + 7)
88 7p2e9 11210 . . . . . . 7 (7 + 2) = 9
8951, 73, 88addcomli 10266 . . . . . 6 (2 + 7) = 9
908dec0h 11560 . . . . . 6 9 = 09
9187, 89, 903eqtri 2677 . . . . 5 ((1 · 2) + 7) = 09
921, 1, 46, 50, 81, 71, 68, 8, 46, 86, 91decmac 11604 . . . 4 ((11 · 2) + 7) = 29
931, 68, 46, 50, 70, 71, 72, 8, 68, 80, 92decma2c 11606 . . 3 ((11 · 12) + 7) = 139
94 7lt10 11713 . . . 4 7 < 10
9566, 1, 50, 94declti 11584 . . 3 7 < 11
9667, 69, 43, 93, 95ndvdsi 15183 . 2 ¬ 11 ∥ 139
971, 46deccl 11550 . . 3 10 ∈ ℕ0
98 eqid 2651 . . . 4 10 = 10
993nn0cni 11342 . . . . . . 7 13 ∈ ℂ
10099mulid1i 10080 . . . . . 6 (13 · 1) = 13
101100, 83oveq12i 6702 . . . . 5 ((13 · 1) + (0 + 0)) = (13 + 0)
10299addid1i 10261 . . . . 5 (13 + 0) = 13
103101, 102eqtri 2673 . . . 4 ((13 · 1) + (0 + 0)) = 13
10499mul01i 10264 . . . . . 6 (13 · 0) = 0
105104oveq1i 6700 . . . . 5 ((13 · 0) + 9) = (0 + 9)
10631addid2i 10262 . . . . 5 (0 + 9) = 9
107105, 106, 903eqtri 2677 . . . 4 ((13 · 0) + 9) = 09
1081, 46, 46, 8, 98, 90, 3, 8, 46, 103, 107decma2c 11606 . . 3 ((13 · 10) + 9) = 139
10966, 2, 8, 11declti 11584 . . 3 9 < 13
11014, 97, 4, 108, 109ndvdsi 15183 . 2 ¬ 13 ∥ 139
1111, 43decnncl 11556 . . 3 17 ∈ ℕ
112 eqid 2651 . . . 4 17 = 17
1132dec0h 11560 . . . 4 3 = 03
114 5nn0 11350 . . . 4 5 ∈ ℕ0
115 8cn 11144 . . . . . . 7 8 ∈ ℂ
116115mulid2i 10081 . . . . . 6 (1 · 8) = 8
117 5cn 11138 . . . . . . 7 5 ∈ ℂ
118117addid2i 10262 . . . . . 6 (0 + 5) = 5
119116, 118oveq12i 6702 . . . . 5 ((1 · 8) + (0 + 5)) = (8 + 5)
120 8p5e13 11653 . . . . 5 (8 + 5) = 13
121119, 120eqtri 2673 . . . 4 ((1 · 8) + (0 + 5)) = 13
122 8t7e56 11699 . . . . . 6 (8 · 7) = 56
123115, 51, 122mulcomli 10085 . . . . 5 (7 · 8) = 56
124114, 47, 2, 123, 60decaddi 11617 . . . 4 ((7 · 8) + 3) = 59
1251, 50, 46, 2, 112, 113, 6, 8, 114, 121, 124decmac 11604 . . 3 ((17 · 8) + 3) = 139
12666, 50, 2, 10declti 11584 . . 3 3 < 17
127111, 6, 13, 125, 126ndvdsi 15183 . 2 ¬ 17 ∥ 139
1281, 4decnncl 11556 . . 3 19 ∈ ℕ
12951mulid2i 10081 . . . . . 6 (1 · 7) = 7
130129, 54oveq12i 6702 . . . . 5 ((1 · 7) + (0 + 6)) = (7 + 6)
131130, 56eqtri 2673 . . . 4 ((1 · 7) + (0 + 6)) = 13
13247, 2, 47, 58, 61decaddi 11617 . . . 4 ((9 · 7) + 6) = 69
1331, 8, 46, 47, 48, 49, 50, 8, 47, 131, 132decmac 11604 . . 3 ((19 · 7) + 6) = 139
134 6lt10 11714 . . . 4 6 < 10
13566, 8, 47, 134declti 11584 . . 3 6 < 19
136128, 50, 45, 133, 135ndvdsi 15183 . 2 ¬ 19 ∥ 139
13768, 13decnncl 11556 . . 3 23 ∈ ℕ
138 eqid 2651 . . . 4 23 = 23
139 2p1e3 11189 . . . . 5 (2 + 1) = 3
140 6t2e12 11679 . . . . . 6 (6 · 2) = 12
14153, 73, 140mulcomli 10085 . . . . 5 (2 · 6) = 12
1421, 68, 139, 141decsuc 11573 . . . 4 ((2 · 6) + 1) = 13
143 8p1e9 11196 . . . . 5 (8 + 1) = 9
144 6t3e18 11680 . . . . . 6 (6 · 3) = 18
14553, 22, 144mulcomli 10085 . . . . 5 (3 · 6) = 18
1461, 6, 143, 145decsuc 11573 . . . 4 ((3 · 6) + 1) = 19
14768, 2, 1, 138, 47, 8, 1, 142, 146decrmac 11615 . . 3 ((23 · 6) + 1) = 139
148 2nn 11223 . . . 4 2 ∈ ℕ
149148, 2, 1, 15declti 11584 . . 3 1 < 23
150137, 47, 66, 147, 149ndvdsi 15183 . 2 ¬ 23 ∥ 139
1515, 12, 16, 19, 38, 42, 65, 96, 110, 127, 136, 150prmlem2 15874 1 139 ∈ ℙ
Colors of variables: wff setvar class
Syntax hints:  wcel 2030   class class class wbr 4685  (class class class)co 6690  0cc0 9974  1c1 9975   + caddc 9977   · cmul 9979  2c2 11108  3c3 11109  4c4 11110  5c5 11111  6c6 11112  7c7 11113  8c8 11114  9c9 11115  cdc 11531  cdvds 15027  cprime 15432
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-sup 8389  df-inf 8390  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-4 11119  df-5 11120  df-6 11121  df-7 11122  df-8 11123  df-9 11124  df-n0 11331  df-z 11416  df-dec 11532  df-uz 11726  df-rp 11871  df-fz 12365  df-seq 12842  df-exp 12901  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-dvds 15028  df-prm 15433
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator