MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  2503lem3 Structured version   Visualization version   GIF version

Theorem 2503lem3 16057
Description: Lemma for 2503prm 16058. Calculate the GCD of 2↑18 − 1≡1831 with 𝑁 = 2503. (Contributed by Mario Carneiro, 3-Mar-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) (Proof shortened by AV, 15-Sep-2021.)
Hypothesis
Ref Expression
2503prm.1 𝑁 = 2503
Assertion
Ref Expression
2503lem3 (((2↑18) − 1) gcd 𝑁) = 1

Proof of Theorem 2503lem3
StepHypRef Expression
1 2nn 11462 . . . 4 2 ∈ ℕ
2 1nn0 11575 . . . . 5 1 ∈ ℕ0
3 8nn0 11582 . . . . 5 8 ∈ ℕ0
42, 3deccl 11774 . . . 4 18 ∈ ℕ0
5 nnexpcl 13096 . . . 4 ((2 ∈ ℕ ∧ 18 ∈ ℕ0) → (2↑18) ∈ ℕ)
61, 4, 5mp2an 675 . . 3 (2↑18) ∈ ℕ
7 nnm1nn0 11600 . . 3 ((2↑18) ∈ ℕ → ((2↑18) − 1) ∈ ℕ0)
86, 7ax-mp 5 . 2 ((2↑18) − 1) ∈ ℕ0
9 3nn0 11577 . . . 4 3 ∈ ℕ0
104, 9deccl 11774 . . 3 183 ∈ ℕ0
1110, 2deccl 11774 . 2 1831 ∈ ℕ0
12 2503prm.1 . . 3 𝑁 = 2503
13 2nn0 11576 . . . . . 6 2 ∈ ℕ0
14 5nn0 11579 . . . . . 6 5 ∈ ℕ0
1513, 14deccl 11774 . . . . 5 25 ∈ ℕ0
16 0nn0 11574 . . . . 5 0 ∈ ℕ0
1715, 16deccl 11774 . . . 4 250 ∈ ℕ0
18 3nn 11463 . . . 4 3 ∈ ℕ
1917, 18decnncl 11779 . . 3 2503 ∈ ℕ
2012, 19eqeltri 2881 . 2 𝑁 ∈ ℕ
21122503lem1 16055 . . 3 ((2↑18) mod 𝑁) = (1832 mod 𝑁)
22 1p1e2 11417 . . . 4 (1 + 1) = 2
23 eqid 2806 . . . 4 1831 = 1831
2410, 2, 22, 23decsuc 11790 . . 3 (1831 + 1) = 1832
2520, 6, 2, 11, 21, 24modsubi 15993 . 2 (((2↑18) − 1) mod 𝑁) = (1831 mod 𝑁)
26 6nn0 11580 . . . . 5 6 ∈ ℕ0
27 7nn0 11581 . . . . 5 7 ∈ ℕ0
2826, 27deccl 11774 . . . 4 67 ∈ ℕ0
2928, 13deccl 11774 . . 3 672 ∈ ℕ0
30 4nn0 11578 . . . . . 6 4 ∈ ℕ0
3130, 3deccl 11774 . . . . 5 48 ∈ ℕ0
3231, 27deccl 11774 . . . 4 487 ∈ ℕ0
334, 14deccl 11774 . . . . 5 185 ∈ ℕ0
342, 2deccl 11774 . . . . . . 7 11 ∈ ℕ0
3534, 27deccl 11774 . . . . . 6 117 ∈ ℕ0
3626, 3deccl 11774 . . . . . . 7 68 ∈ ℕ0
37 9nn0 11583 . . . . . . . . 9 9 ∈ ℕ0
3830, 37deccl 11774 . . . . . . . 8 49 ∈ ℕ0
392, 37deccl 11774 . . . . . . . . 9 19 ∈ ℕ0
4038nn0zi 11668 . . . . . . . . . . 11 49 ∈ ℤ
4139nn0zi 11668 . . . . . . . . . . 11 19 ∈ ℤ
42 gcdcom 15454 . . . . . . . . . . 11 ((49 ∈ ℤ ∧ 19 ∈ ℤ) → (49 gcd 19) = (19 gcd 49))
4340, 41, 42mp2an 675 . . . . . . . . . 10 (49 gcd 19) = (19 gcd 49)
44 9nn 11469 . . . . . . . . . . . . 13 9 ∈ ℕ
452, 44decnncl 11779 . . . . . . . . . . . 12 19 ∈ ℕ
46 1nn 11316 . . . . . . . . . . . . 13 1 ∈ ℕ
472, 46decnncl 11779 . . . . . . . . . . . 12 11 ∈ ℕ
48 eqid 2806 . . . . . . . . . . . . 13 19 = 19
49 eqid 2806 . . . . . . . . . . . . 13 11 = 11
50 2cn 11375 . . . . . . . . . . . . . . . 16 2 ∈ ℂ
5150mulid2i 10330 . . . . . . . . . . . . . . 15 (1 · 2) = 2
5251, 22oveq12i 6886 . . . . . . . . . . . . . 14 ((1 · 2) + (1 + 1)) = (2 + 2)
53 2p2e4 11427 . . . . . . . . . . . . . 14 (2 + 2) = 4
5452, 53eqtri 2828 . . . . . . . . . . . . 13 ((1 · 2) + (1 + 1)) = 4
55 8p1e9 11441 . . . . . . . . . . . . . 14 (8 + 1) = 9
56 9t2e18 11881 . . . . . . . . . . . . . 14 (9 · 2) = 18
572, 3, 55, 56decsuc 11790 . . . . . . . . . . . . 13 ((9 · 2) + 1) = 19
582, 37, 2, 2, 48, 49, 13, 37, 2, 54, 57decmac 11811 . . . . . . . . . . . 12 ((19 · 2) + 11) = 49
59 1lt9 11505 . . . . . . . . . . . . 13 1 < 9
602, 2, 44, 59declt 11787 . . . . . . . . . . . 12 11 < 19
6145, 13, 47, 58, 60ndvdsi 15355 . . . . . . . . . . 11 ¬ 19 ∥ 49
62 19prm 16036 . . . . . . . . . . . 12 19 ∈ ℙ
63 coprm 15640 . . . . . . . . . . . 12 ((19 ∈ ℙ ∧ 49 ∈ ℤ) → (¬ 19 ∥ 49 ↔ (19 gcd 49) = 1))
6462, 40, 63mp2an 675 . . . . . . . . . . 11 19 ∥ 49 ↔ (19 gcd 49) = 1)
6561, 64mpbi 221 . . . . . . . . . 10 (19 gcd 49) = 1
6643, 65eqtri 2828 . . . . . . . . 9 (49 gcd 19) = 1
67 eqid 2806 . . . . . . . . . 10 49 = 49
68 4cn 11382 . . . . . . . . . . . . 13 4 ∈ ℂ
6968mulid2i 10330 . . . . . . . . . . . 12 (1 · 4) = 4
7069, 22oveq12i 6886 . . . . . . . . . . 11 ((1 · 4) + (1 + 1)) = (4 + 2)
71 4p2e6 11444 . . . . . . . . . . 11 (4 + 2) = 6
7270, 71eqtri 2828 . . . . . . . . . 10 ((1 · 4) + (1 + 1)) = 6
73 9cn 11392 . . . . . . . . . . . . 13 9 ∈ ℂ
7473mulid2i 10330 . . . . . . . . . . . 12 (1 · 9) = 9
7574oveq1i 6884 . . . . . . . . . . 11 ((1 · 9) + 9) = (9 + 9)
76 9p9e18 11853 . . . . . . . . . . 11 (9 + 9) = 18
7775, 76eqtri 2828 . . . . . . . . . 10 ((1 · 9) + 9) = 18
7830, 37, 2, 37, 67, 48, 2, 3, 2, 72, 77decma2c 11812 . . . . . . . . 9 ((1 · 49) + 19) = 68
792, 39, 38, 66, 78gcdi 15994 . . . . . . . 8 (68 gcd 49) = 1
80 eqid 2806 . . . . . . . . 9 68 = 68
81 6cn 11386 . . . . . . . . . . . 12 6 ∈ ℂ
8281mulid2i 10330 . . . . . . . . . . 11 (1 · 6) = 6
83 4p1e5 11437 . . . . . . . . . . 11 (4 + 1) = 5
8482, 83oveq12i 6886 . . . . . . . . . 10 ((1 · 6) + (4 + 1)) = (6 + 5)
85 6p5e11 11832 . . . . . . . . . 10 (6 + 5) = 11
8684, 85eqtri 2828 . . . . . . . . 9 ((1 · 6) + (4 + 1)) = 11
87 8cn 11390 . . . . . . . . . . . 12 8 ∈ ℂ
8887mulid2i 10330 . . . . . . . . . . 11 (1 · 8) = 8
8988oveq1i 6884 . . . . . . . . . 10 ((1 · 8) + 9) = (8 + 9)
90 9p8e17 11852 . . . . . . . . . . 11 (9 + 8) = 17
9173, 87, 90addcomli 10513 . . . . . . . . . 10 (8 + 9) = 17
9289, 91eqtri 2828 . . . . . . . . 9 ((1 · 8) + 9) = 17
9326, 3, 30, 37, 80, 67, 2, 27, 2, 86, 92decma2c 11812 . . . . . . . 8 ((1 · 68) + 49) = 117
942, 38, 36, 79, 93gcdi 15994 . . . . . . 7 (117 gcd 68) = 1
95 eqid 2806 . . . . . . . 8 117 = 117
96 6p1e7 11439 . . . . . . . . . 10 (6 + 1) = 7
9727dec0h 11781 . . . . . . . . . 10 7 = 07
9896, 97eqtri 2828 . . . . . . . . 9 (6 + 1) = 07
99 1t1e1 11453 . . . . . . . . . . 11 (1 · 1) = 1
100 00id 10496 . . . . . . . . . . 11 (0 + 0) = 0
10199, 100oveq12i 6886 . . . . . . . . . 10 ((1 · 1) + (0 + 0)) = (1 + 0)
102 ax-1cn 10279 . . . . . . . . . . 11 1 ∈ ℂ
103102addid1i 10508 . . . . . . . . . 10 (1 + 0) = 1
104101, 103eqtri 2828 . . . . . . . . 9 ((1 · 1) + (0 + 0)) = 1
10599oveq1i 6884 . . . . . . . . . 10 ((1 · 1) + 7) = (1 + 7)
106 7cn 11388 . . . . . . . . . . 11 7 ∈ ℂ
107 7p1e8 11440 . . . . . . . . . . 11 (7 + 1) = 8
108106, 102, 107addcomli 10513 . . . . . . . . . 10 (1 + 7) = 8
1093dec0h 11781 . . . . . . . . . 10 8 = 08
110105, 108, 1093eqtri 2832 . . . . . . . . 9 ((1 · 1) + 7) = 08
1112, 2, 16, 27, 49, 98, 2, 3, 16, 104, 110decma2c 11812 . . . . . . . 8 ((1 · 11) + (6 + 1)) = 18
112106mulid2i 10330 . . . . . . . . . 10 (1 · 7) = 7
113112oveq1i 6884 . . . . . . . . 9 ((1 · 7) + 8) = (7 + 8)
114 8p7e15 11844 . . . . . . . . . 10 (8 + 7) = 15
11587, 106, 114addcomli 10513 . . . . . . . . 9 (7 + 8) = 15
116113, 115eqtri 2828 . . . . . . . 8 ((1 · 7) + 8) = 15
11734, 27, 26, 3, 95, 80, 2, 14, 2, 111, 116decma2c 11812 . . . . . . 7 ((1 · 117) + 68) = 185
1182, 36, 35, 94, 117gcdi 15994 . . . . . 6 (185 gcd 117) = 1
119 eqid 2806 . . . . . . 7 185 = 185
120 eqid 2806 . . . . . . . 8 18 = 18
1212, 2, 22, 49decsuc 11790 . . . . . . . 8 (11 + 1) = 12
122 2t1e2 11454 . . . . . . . . . 10 (2 · 1) = 2
123122, 22oveq12i 6886 . . . . . . . . 9 ((2 · 1) + (1 + 1)) = (2 + 2)
124123, 53eqtri 2828 . . . . . . . 8 ((2 · 1) + (1 + 1)) = 4
125 8t2e16 11874 . . . . . . . . . 10 (8 · 2) = 16
12687, 50, 125mulcomli 10334 . . . . . . . . 9 (2 · 8) = 16
127 6p2e8 11450 . . . . . . . . 9 (6 + 2) = 8
1282, 26, 13, 126, 127decaddi 11819 . . . . . . . 8 ((2 · 8) + 2) = 18
1292, 3, 2, 13, 120, 121, 13, 3, 2, 124, 128decma2c 11812 . . . . . . 7 ((2 · 18) + (11 + 1)) = 48
130 5cn 11384 . . . . . . . . 9 5 ∈ ℂ
131 5t2e10 11859 . . . . . . . . 9 (5 · 2) = 10
132130, 50, 131mulcomli 10334 . . . . . . . 8 (2 · 5) = 10
133106addid2i 10509 . . . . . . . 8 (0 + 7) = 7
1342, 16, 27, 132, 133decaddi 11819 . . . . . . 7 ((2 · 5) + 7) = 17
1354, 14, 34, 27, 119, 95, 13, 27, 2, 129, 134decma2c 11812 . . . . . 6 ((2 · 185) + 117) = 487
13613, 35, 33, 118, 135gcdi 15994 . . . . 5 (487 gcd 185) = 1
137 eqid 2806 . . . . . 6 487 = 487
138 eqid 2806 . . . . . . 7 48 = 48
1392, 3, 55, 120decsuc 11790 . . . . . . 7 (18 + 1) = 19
14030, 3, 2, 37, 138, 139, 2, 27, 2, 72, 92decma2c 11812 . . . . . 6 ((1 · 48) + (18 + 1)) = 67
141112oveq1i 6884 . . . . . . 7 ((1 · 7) + 5) = (7 + 5)
142 7p5e12 11836 . . . . . . 7 (7 + 5) = 12
143141, 142eqtri 2828 . . . . . 6 ((1 · 7) + 5) = 12
14431, 27, 4, 14, 137, 119, 2, 13, 2, 140, 143decma2c 11812 . . . . 5 ((1 · 487) + 185) = 672
1452, 33, 32, 136, 144gcdi 15994 . . . 4 (672 gcd 487) = 1
146 eqid 2806 . . . . 5 672 = 672
147 eqid 2806 . . . . . 6 67 = 67
14830, 3, 55, 138decsuc 11790 . . . . . 6 (48 + 1) = 49
14971oveq2i 6885 . . . . . . 7 ((2 · 6) + (4 + 2)) = ((2 · 6) + 6)
150 6t2e12 11863 . . . . . . . . 9 (6 · 2) = 12
15181, 50, 150mulcomli 10334 . . . . . . . 8 (2 · 6) = 12
15281, 50, 127addcomli 10513 . . . . . . . 8 (2 + 6) = 8
1532, 13, 26, 151, 152decaddi 11819 . . . . . . 7 ((2 · 6) + 6) = 18
154149, 153eqtri 2828 . . . . . 6 ((2 · 6) + (4 + 2)) = 18
155 7t2e14 11868 . . . . . . . 8 (7 · 2) = 14
156106, 50, 155mulcomli 10334 . . . . . . 7 (2 · 7) = 14
157 9p4e13 11848 . . . . . . . 8 (9 + 4) = 13
15873, 68, 157addcomli 10513 . . . . . . 7 (4 + 9) = 13
1592, 30, 37, 156, 22, 9, 158decaddci 11820 . . . . . 6 ((2 · 7) + 9) = 23
16026, 27, 30, 37, 147, 148, 13, 9, 13, 154, 159decma2c 11812 . . . . 5 ((2 · 67) + (48 + 1)) = 183
161 2t2e4 11455 . . . . . . 7 (2 · 2) = 4
162161oveq1i 6884 . . . . . 6 ((2 · 2) + 7) = (4 + 7)
163 7p4e11 11835 . . . . . . 7 (7 + 4) = 11
164106, 68, 163addcomli 10513 . . . . . 6 (4 + 7) = 11
165162, 164eqtri 2828 . . . . 5 ((2 · 2) + 7) = 11
16628, 13, 31, 27, 146, 137, 13, 2, 2, 160, 165decma2c 11812 . . . 4 ((2 · 672) + 487) = 1831
16713, 32, 29, 145, 166gcdi 15994 . . 3 (1831 gcd 672) = 1
168 eqid 2806 . . . . . 6 183 = 183
16928nn0cni 11571 . . . . . . 7 67 ∈ ℂ
170169addid1i 10508 . . . . . 6 (67 + 0) = 67
171102addid2i 10509 . . . . . . . . 9 (0 + 1) = 1
17299, 171oveq12i 6886 . . . . . . . 8 ((1 · 1) + (0 + 1)) = (1 + 1)
173172, 22eqtri 2828 . . . . . . 7 ((1 · 1) + (0 + 1)) = 2
17488oveq1i 6884 . . . . . . . 8 ((1 · 8) + 7) = (8 + 7)
175174, 114eqtri 2828 . . . . . . 7 ((1 · 8) + 7) = 15
1762, 3, 16, 27, 120, 98, 2, 14, 2, 173, 175decma2c 11812 . . . . . 6 ((1 · 18) + (6 + 1)) = 25
177 3cn 11379 . . . . . . . . 9 3 ∈ ℂ
178177mulid2i 10330 . . . . . . . 8 (1 · 3) = 3
179178oveq1i 6884 . . . . . . 7 ((1 · 3) + 7) = (3 + 7)
180 7p3e10 11834 . . . . . . . 8 (7 + 3) = 10
181106, 177, 180addcomli 10513 . . . . . . 7 (3 + 7) = 10
182179, 181eqtri 2828 . . . . . 6 ((1 · 3) + 7) = 10
1834, 9, 26, 27, 168, 170, 2, 16, 2, 176, 182decma2c 11812 . . . . 5 ((1 · 183) + (67 + 0)) = 250
18499oveq1i 6884 . . . . . 6 ((1 · 1) + 2) = (1 + 2)
185 1p2e3 11435 . . . . . 6 (1 + 2) = 3
1869dec0h 11781 . . . . . 6 3 = 03
187184, 185, 1863eqtri 2832 . . . . 5 ((1 · 1) + 2) = 03
18810, 2, 28, 13, 23, 146, 2, 9, 16, 183, 187decma2c 11812 . . . 4 ((1 · 1831) + 672) = 2503
189188, 12eqtr4i 2831 . . 3 ((1 · 1831) + 672) = 𝑁
1902, 29, 11, 167, 189gcdi 15994 . 2 (𝑁 gcd 1831) = 1
1918, 11, 20, 25, 190gcdmodi 15995 1 (((2↑18) − 1) gcd 𝑁) = 1
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 197   = wceq 1637  wcel 2156   class class class wbr 4844  (class class class)co 6874  0cc0 10221  1c1 10222   + caddc 10224   · cmul 10226  cmin 10551  cn 11305  2c2 11356  3c3 11357  4c4 11358  5c5 11359  6c6 11360  7c7 11361  8c8 11362  9c9 11363  0cn0 11559  cz 11643  cdc 11759  cexp 13083  cdvds 15203   gcd cgcd 15435  cprime 15603
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7179  ax-cnex 10277  ax-resscn 10278  ax-1cn 10279  ax-icn 10280  ax-addcl 10281  ax-addrcl 10282  ax-mulcl 10283  ax-mulrcl 10284  ax-mulcom 10285  ax-addass 10286  ax-mulass 10287  ax-distr 10288  ax-i2m1 10289  ax-1ne0 10290  ax-1rid 10291  ax-rnegex 10292  ax-rrecex 10293  ax-cnre 10294  ax-pre-lttri 10295  ax-pre-lttrn 10296  ax-pre-ltadd 10297  ax-pre-mulgt0 10298  ax-pre-sup 10299
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-nel 3082  df-ral 3101  df-rex 3102  df-reu 3103  df-rmo 3104  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-tp 4375  df-op 4377  df-uni 4631  df-iun 4714  df-br 4845  df-opab 4907  df-mpt 4924  df-tr 4947  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5893  df-ord 5939  df-on 5940  df-lim 5941  df-suc 5942  df-iota 6064  df-fun 6103  df-fn 6104  df-f 6105  df-f1 6106  df-fo 6107  df-f1o 6108  df-fv 6109  df-riota 6835  df-ov 6877  df-oprab 6878  df-mpt2 6879  df-om 7296  df-1st 7398  df-2nd 7399  df-wrecs 7642  df-recs 7704  df-rdg 7742  df-1o 7796  df-2o 7797  df-er 7979  df-en 8193  df-dom 8194  df-sdom 8195  df-fin 8196  df-sup 8587  df-inf 8588  df-pnf 10361  df-mnf 10362  df-xr 10363  df-ltxr 10364  df-le 10365  df-sub 10553  df-neg 10554  df-div 10970  df-nn 11306  df-2 11364  df-3 11365  df-4 11366  df-5 11367  df-6 11368  df-7 11369  df-8 11370  df-9 11371  df-n0 11560  df-z 11644  df-dec 11760  df-uz 11905  df-rp 12047  df-fz 12550  df-fl 12817  df-mod 12893  df-seq 13025  df-exp 13084  df-cj 14062  df-re 14063  df-im 14064  df-sqrt 14198  df-abs 14199  df-dvds 15204  df-gcd 15436  df-prm 15604
This theorem is referenced by:  2503prm  16058
  Copyright terms: Public domain W3C validator