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

Theorem 2503lem3 17054
Description: Lemma for 2503prm 17055. 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 12267 . . . 4 2 ∈ ℕ
2 1nn0 12470 . . . . 5 1 ∈ ℕ0
3 8nn0 12477 . . . . 5 8 ∈ ℕ0
42, 3deccl 12674 . . . 4 18 ∈ ℕ0
5 nnexpcl 14022 . . . 4 ((2 ∈ ℕ ∧ 18 ∈ ℕ0) → (2↑18) ∈ ℕ)
61, 4, 5mp2an 690 . . 3 (2↑18) ∈ ℕ
7 nnm1nn0 12495 . . 3 ((2↑18) ∈ ℕ → ((2↑18) − 1) ∈ ℕ0)
86, 7ax-mp 5 . 2 ((2↑18) − 1) ∈ ℕ0
9 3nn0 12472 . . . 4 3 ∈ ℕ0
104, 9deccl 12674 . . 3 183 ∈ ℕ0
1110, 2deccl 12674 . 2 1831 ∈ ℕ0
12 2503prm.1 . . 3 𝑁 = 2503
13 2nn0 12471 . . . . . 6 2 ∈ ℕ0
14 5nn0 12474 . . . . . 6 5 ∈ ℕ0
1513, 14deccl 12674 . . . . 5 25 ∈ ℕ0
16 0nn0 12469 . . . . 5 0 ∈ ℕ0
1715, 16deccl 12674 . . . 4 250 ∈ ℕ0
18 3nn 12273 . . . 4 3 ∈ ℕ
1917, 18decnncl 12679 . . 3 2503 ∈ ℕ
2012, 19eqeltri 2828 . 2 𝑁 ∈ ℕ
21122503lem1 17052 . . 3 ((2↑18) mod 𝑁) = (1832 mod 𝑁)
22 1p1e2 12319 . . . 4 (1 + 1) = 2
23 eqid 2731 . . . 4 1831 = 1831
2410, 2, 22, 23decsuc 12690 . . 3 (1831 + 1) = 1832
2520, 6, 2, 11, 21, 24modsubi 16987 . 2 (((2↑18) − 1) mod 𝑁) = (1831 mod 𝑁)
26 6nn0 12475 . . . . 5 6 ∈ ℕ0
27 7nn0 12476 . . . . 5 7 ∈ ℕ0
2826, 27deccl 12674 . . . 4 67 ∈ ℕ0
2928, 13deccl 12674 . . 3 672 ∈ ℕ0
30 4nn0 12473 . . . . . 6 4 ∈ ℕ0
3130, 3deccl 12674 . . . . 5 48 ∈ ℕ0
3231, 27deccl 12674 . . . 4 487 ∈ ℕ0
334, 14deccl 12674 . . . . 5 185 ∈ ℕ0
342, 2deccl 12674 . . . . . . 7 11 ∈ ℕ0
3534, 27deccl 12674 . . . . . 6 117 ∈ ℕ0
3626, 3deccl 12674 . . . . . . 7 68 ∈ ℕ0
37 9nn0 12478 . . . . . . . . 9 9 ∈ ℕ0
3830, 37deccl 12674 . . . . . . . 8 49 ∈ ℕ0
392, 37deccl 12674 . . . . . . . . 9 19 ∈ ℕ0
4038nn0zi 12569 . . . . . . . . . . 11 49 ∈ ℤ
4139nn0zi 12569 . . . . . . . . . . 11 19 ∈ ℤ
42 gcdcom 16436 . . . . . . . . . . 11 ((49 ∈ ℤ ∧ 19 ∈ ℤ) → (49 gcd 19) = (19 gcd 49))
4340, 41, 42mp2an 690 . . . . . . . . . 10 (49 gcd 19) = (19 gcd 49)
44 9nn 12292 . . . . . . . . . . . . 13 9 ∈ ℕ
452, 44decnncl 12679 . . . . . . . . . . . 12 19 ∈ ℕ
46 1nn 12205 . . . . . . . . . . . . 13 1 ∈ ℕ
472, 46decnncl 12679 . . . . . . . . . . . 12 11 ∈ ℕ
48 eqid 2731 . . . . . . . . . . . . 13 19 = 19
49 eqid 2731 . . . . . . . . . . . . 13 11 = 11
50 2cn 12269 . . . . . . . . . . . . . . . 16 2 ∈ ℂ
5150mullidi 11201 . . . . . . . . . . . . . . 15 (1 · 2) = 2
5251, 22oveq12i 7405 . . . . . . . . . . . . . 14 ((1 · 2) + (1 + 1)) = (2 + 2)
53 2p2e4 12329 . . . . . . . . . . . . . 14 (2 + 2) = 4
5452, 53eqtri 2759 . . . . . . . . . . . . 13 ((1 · 2) + (1 + 1)) = 4
55 8p1e9 12344 . . . . . . . . . . . . . 14 (8 + 1) = 9
56 9t2e18 12781 . . . . . . . . . . . . . 14 (9 · 2) = 18
572, 3, 55, 56decsuc 12690 . . . . . . . . . . . . 13 ((9 · 2) + 1) = 19
582, 37, 2, 2, 48, 49, 13, 37, 2, 54, 57decmac 12711 . . . . . . . . . . . 12 ((19 · 2) + 11) = 49
59 1lt9 12400 . . . . . . . . . . . . 13 1 < 9
602, 2, 44, 59declt 12687 . . . . . . . . . . . 12 11 < 19
6145, 13, 47, 58, 60ndvdsi 16337 . . . . . . . . . . 11 ¬ 19 ∥ 49
62 19prm 17033 . . . . . . . . . . . 12 19 ∈ ℙ
63 coprm 16630 . . . . . . . . . . . 12 ((19 ∈ ℙ ∧ 49 ∈ ℤ) → (¬ 19 ∥ 49 ↔ (19 gcd 49) = 1))
6462, 40, 63mp2an 690 . . . . . . . . . . 11 19 ∥ 49 ↔ (19 gcd 49) = 1)
6561, 64mpbi 229 . . . . . . . . . 10 (19 gcd 49) = 1
6643, 65eqtri 2759 . . . . . . . . 9 (49 gcd 19) = 1
67 eqid 2731 . . . . . . . . . 10 49 = 49
68 4cn 12279 . . . . . . . . . . . . 13 4 ∈ ℂ
6968mullidi 11201 . . . . . . . . . . . 12 (1 · 4) = 4
7069, 22oveq12i 7405 . . . . . . . . . . 11 ((1 · 4) + (1 + 1)) = (4 + 2)
71 4p2e6 12347 . . . . . . . . . . 11 (4 + 2) = 6
7270, 71eqtri 2759 . . . . . . . . . 10 ((1 · 4) + (1 + 1)) = 6
73 9cn 12294 . . . . . . . . . . . . 13 9 ∈ ℂ
7473mullidi 11201 . . . . . . . . . . . 12 (1 · 9) = 9
7574oveq1i 7403 . . . . . . . . . . 11 ((1 · 9) + 9) = (9 + 9)
76 9p9e18 12753 . . . . . . . . . . 11 (9 + 9) = 18
7775, 76eqtri 2759 . . . . . . . . . 10 ((1 · 9) + 9) = 18
7830, 37, 2, 37, 67, 48, 2, 3, 2, 72, 77decma2c 12712 . . . . . . . . 9 ((1 · 49) + 19) = 68
792, 39, 38, 66, 78gcdi 16988 . . . . . . . 8 (68 gcd 49) = 1
80 eqid 2731 . . . . . . . . 9 68 = 68
81 6cn 12285 . . . . . . . . . . . 12 6 ∈ ℂ
8281mullidi 11201 . . . . . . . . . . 11 (1 · 6) = 6
83 4p1e5 12340 . . . . . . . . . . 11 (4 + 1) = 5
8482, 83oveq12i 7405 . . . . . . . . . 10 ((1 · 6) + (4 + 1)) = (6 + 5)
85 6p5e11 12732 . . . . . . . . . 10 (6 + 5) = 11
8684, 85eqtri 2759 . . . . . . . . 9 ((1 · 6) + (4 + 1)) = 11
87 8cn 12291 . . . . . . . . . . . 12 8 ∈ ℂ
8887mullidi 11201 . . . . . . . . . . 11 (1 · 8) = 8
8988oveq1i 7403 . . . . . . . . . 10 ((1 · 8) + 9) = (8 + 9)
90 9p8e17 12752 . . . . . . . . . . 11 (9 + 8) = 17
9173, 87, 90addcomli 11388 . . . . . . . . . 10 (8 + 9) = 17
9289, 91eqtri 2759 . . . . . . . . 9 ((1 · 8) + 9) = 17
9326, 3, 30, 37, 80, 67, 2, 27, 2, 86, 92decma2c 12712 . . . . . . . 8 ((1 · 68) + 49) = 117
942, 38, 36, 79, 93gcdi 16988 . . . . . . 7 (117 gcd 68) = 1
95 eqid 2731 . . . . . . . 8 117 = 117
96 6p1e7 12342 . . . . . . . . . 10 (6 + 1) = 7
9727dec0h 12681 . . . . . . . . . 10 7 = 07
9896, 97eqtri 2759 . . . . . . . . 9 (6 + 1) = 07
99 1t1e1 12356 . . . . . . . . . . 11 (1 · 1) = 1
100 00id 11371 . . . . . . . . . . 11 (0 + 0) = 0
10199, 100oveq12i 7405 . . . . . . . . . 10 ((1 · 1) + (0 + 0)) = (1 + 0)
102 ax-1cn 11150 . . . . . . . . . . 11 1 ∈ ℂ
103102addridi 11383 . . . . . . . . . 10 (1 + 0) = 1
104101, 103eqtri 2759 . . . . . . . . 9 ((1 · 1) + (0 + 0)) = 1
10599oveq1i 7403 . . . . . . . . . 10 ((1 · 1) + 7) = (1 + 7)
106 7cn 12288 . . . . . . . . . . 11 7 ∈ ℂ
107 7p1e8 12343 . . . . . . . . . . 11 (7 + 1) = 8
108106, 102, 107addcomli 11388 . . . . . . . . . 10 (1 + 7) = 8
1093dec0h 12681 . . . . . . . . . 10 8 = 08
110105, 108, 1093eqtri 2763 . . . . . . . . 9 ((1 · 1) + 7) = 08
1112, 2, 16, 27, 49, 98, 2, 3, 16, 104, 110decma2c 12712 . . . . . . . 8 ((1 · 11) + (6 + 1)) = 18
112106mullidi 11201 . . . . . . . . . 10 (1 · 7) = 7
113112oveq1i 7403 . . . . . . . . 9 ((1 · 7) + 8) = (7 + 8)
114 8p7e15 12744 . . . . . . . . . 10 (8 + 7) = 15
11587, 106, 114addcomli 11388 . . . . . . . . 9 (7 + 8) = 15
116113, 115eqtri 2759 . . . . . . . 8 ((1 · 7) + 8) = 15
11734, 27, 26, 3, 95, 80, 2, 14, 2, 111, 116decma2c 12712 . . . . . . 7 ((1 · 117) + 68) = 185
1182, 36, 35, 94, 117gcdi 16988 . . . . . 6 (185 gcd 117) = 1
119 eqid 2731 . . . . . . 7 185 = 185
120 eqid 2731 . . . . . . . 8 18 = 18
1212, 2, 22, 49decsuc 12690 . . . . . . . 8 (11 + 1) = 12
122 2t1e2 12357 . . . . . . . . . 10 (2 · 1) = 2
123122, 22oveq12i 7405 . . . . . . . . 9 ((2 · 1) + (1 + 1)) = (2 + 2)
124123, 53eqtri 2759 . . . . . . . 8 ((2 · 1) + (1 + 1)) = 4
125 8t2e16 12774 . . . . . . . . . 10 (8 · 2) = 16
12687, 50, 125mulcomli 11205 . . . . . . . . 9 (2 · 8) = 16
127 6p2e8 12353 . . . . . . . . 9 (6 + 2) = 8
1282, 26, 13, 126, 127decaddi 12719 . . . . . . . 8 ((2 · 8) + 2) = 18
1292, 3, 2, 13, 120, 121, 13, 3, 2, 124, 128decma2c 12712 . . . . . . 7 ((2 · 18) + (11 + 1)) = 48
130 5cn 12282 . . . . . . . . 9 5 ∈ ℂ
131 5t2e10 12759 . . . . . . . . 9 (5 · 2) = 10
132130, 50, 131mulcomli 11205 . . . . . . . 8 (2 · 5) = 10
133106addlidi 11384 . . . . . . . 8 (0 + 7) = 7
1342, 16, 27, 132, 133decaddi 12719 . . . . . . 7 ((2 · 5) + 7) = 17
1354, 14, 34, 27, 119, 95, 13, 27, 2, 129, 134decma2c 12712 . . . . . 6 ((2 · 185) + 117) = 487
13613, 35, 33, 118, 135gcdi 16988 . . . . 5 (487 gcd 185) = 1
137 eqid 2731 . . . . . 6 487 = 487
138 eqid 2731 . . . . . . 7 48 = 48
1392, 3, 55, 120decsuc 12690 . . . . . . 7 (18 + 1) = 19
14030, 3, 2, 37, 138, 139, 2, 27, 2, 72, 92decma2c 12712 . . . . . 6 ((1 · 48) + (18 + 1)) = 67
141112oveq1i 7403 . . . . . . 7 ((1 · 7) + 5) = (7 + 5)
142 7p5e12 12736 . . . . . . 7 (7 + 5) = 12
143141, 142eqtri 2759 . . . . . 6 ((1 · 7) + 5) = 12
14431, 27, 4, 14, 137, 119, 2, 13, 2, 140, 143decma2c 12712 . . . . 5 ((1 · 487) + 185) = 672
1452, 33, 32, 136, 144gcdi 16988 . . . 4 (672 gcd 487) = 1
146 eqid 2731 . . . . 5 672 = 672
147 eqid 2731 . . . . . 6 67 = 67
14830, 3, 55, 138decsuc 12690 . . . . . 6 (48 + 1) = 49
14971oveq2i 7404 . . . . . . 7 ((2 · 6) + (4 + 2)) = ((2 · 6) + 6)
150 6t2e12 12763 . . . . . . . . 9 (6 · 2) = 12
15181, 50, 150mulcomli 11205 . . . . . . . 8 (2 · 6) = 12
15281, 50, 127addcomli 11388 . . . . . . . 8 (2 + 6) = 8
1532, 13, 26, 151, 152decaddi 12719 . . . . . . 7 ((2 · 6) + 6) = 18
154149, 153eqtri 2759 . . . . . 6 ((2 · 6) + (4 + 2)) = 18
155 7t2e14 12768 . . . . . . . 8 (7 · 2) = 14
156106, 50, 155mulcomli 11205 . . . . . . 7 (2 · 7) = 14
157 9p4e13 12748 . . . . . . . 8 (9 + 4) = 13
15873, 68, 157addcomli 11388 . . . . . . 7 (4 + 9) = 13
1592, 30, 37, 156, 22, 9, 158decaddci 12720 . . . . . 6 ((2 · 7) + 9) = 23
16026, 27, 30, 37, 147, 148, 13, 9, 13, 154, 159decma2c 12712 . . . . 5 ((2 · 67) + (48 + 1)) = 183
161 2t2e4 12358 . . . . . . 7 (2 · 2) = 4
162161oveq1i 7403 . . . . . 6 ((2 · 2) + 7) = (4 + 7)
163 7p4e11 12735 . . . . . . 7 (7 + 4) = 11
164106, 68, 163addcomli 11388 . . . . . 6 (4 + 7) = 11
165162, 164eqtri 2759 . . . . 5 ((2 · 2) + 7) = 11
16628, 13, 31, 27, 146, 137, 13, 2, 2, 160, 165decma2c 12712 . . . 4 ((2 · 672) + 487) = 1831
16713, 32, 29, 145, 166gcdi 16988 . . 3 (1831 gcd 672) = 1
168 eqid 2731 . . . . . 6 183 = 183
16928nn0cni 12466 . . . . . . 7 67 ∈ ℂ
170169addridi 11383 . . . . . 6 (67 + 0) = 67
171102addlidi 11384 . . . . . . . . 9 (0 + 1) = 1
17299, 171oveq12i 7405 . . . . . . . 8 ((1 · 1) + (0 + 1)) = (1 + 1)
173172, 22eqtri 2759 . . . . . . 7 ((1 · 1) + (0 + 1)) = 2
17488oveq1i 7403 . . . . . . . 8 ((1 · 8) + 7) = (8 + 7)
175174, 114eqtri 2759 . . . . . . 7 ((1 · 8) + 7) = 15
1762, 3, 16, 27, 120, 98, 2, 14, 2, 173, 175decma2c 12712 . . . . . 6 ((1 · 18) + (6 + 1)) = 25
177 3cn 12275 . . . . . . . . 9 3 ∈ ℂ
178177mullidi 11201 . . . . . . . 8 (1 · 3) = 3
179178oveq1i 7403 . . . . . . 7 ((1 · 3) + 7) = (3 + 7)
180 7p3e10 12734 . . . . . . . 8 (7 + 3) = 10
181106, 177, 180addcomli 11388 . . . . . . 7 (3 + 7) = 10
182179, 181eqtri 2759 . . . . . 6 ((1 · 3) + 7) = 10
1834, 9, 26, 27, 168, 170, 2, 16, 2, 176, 182decma2c 12712 . . . . 5 ((1 · 183) + (67 + 0)) = 250
18499oveq1i 7403 . . . . . 6 ((1 · 1) + 2) = (1 + 2)
185 1p2e3 12337 . . . . . 6 (1 + 2) = 3
1869dec0h 12681 . . . . . 6 3 = 03
187184, 185, 1863eqtri 2763 . . . . 5 ((1 · 1) + 2) = 03
18810, 2, 28, 13, 23, 146, 2, 9, 16, 183, 187decma2c 12712 . . . 4 ((1 · 1831) + 672) = 2503
189188, 12eqtr4i 2762 . . 3 ((1 · 1831) + 672) = 𝑁
1902, 29, 11, 167, 189gcdi 16988 . 2 (𝑁 gcd 1831) = 1
1918, 11, 20, 25, 190gcdmodi 16989 1 (((2↑18) − 1) gcd 𝑁) = 1
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 205   = wceq 1541  wcel 2106   class class class wbr 5141  (class class class)co 7393  0cc0 11092  1c1 11093   + caddc 11095   · cmul 11097  cmin 11426  cn 12194  2c2 12249  3c3 12250  4c4 12251  5c5 12252  6c6 12253  7c7 12254  8c8 12255  9c9 12256  0cn0 12454  cz 12540  cdc 12659  cexp 14009  cdvds 16179   gcd cgcd 16417  cprime 16590
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7708  ax-cnex 11148  ax-resscn 11149  ax-1cn 11150  ax-icn 11151  ax-addcl 11152  ax-addrcl 11153  ax-mulcl 11154  ax-mulrcl 11155  ax-mulcom 11156  ax-addass 11157  ax-mulass 11158  ax-distr 11159  ax-i2m1 11160  ax-1ne0 11161  ax-1rid 11162  ax-rnegex 11163  ax-rrecex 11164  ax-cnre 11165  ax-pre-lttri 11166  ax-pre-lttrn 11167  ax-pre-ltadd 11168  ax-pre-mulgt0 11169  ax-pre-sup 11170
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4523  df-pw 4598  df-sn 4623  df-pr 4625  df-op 4629  df-uni 4902  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6289  df-ord 6356  df-on 6357  df-lim 6358  df-suc 6359  df-iota 6484  df-fun 6534  df-fn 6535  df-f 6536  df-f1 6537  df-fo 6538  df-f1o 6539  df-fv 6540  df-riota 7349  df-ov 7396  df-oprab 7397  df-mpo 7398  df-om 7839  df-1st 7957  df-2nd 7958  df-frecs 8248  df-wrecs 8279  df-recs 8353  df-rdg 8392  df-1o 8448  df-2o 8449  df-er 8686  df-en 8923  df-dom 8924  df-sdom 8925  df-fin 8926  df-sup 9419  df-inf 9420  df-pnf 11232  df-mnf 11233  df-xr 11234  df-ltxr 11235  df-le 11236  df-sub 11428  df-neg 11429  df-div 11854  df-nn 12195  df-2 12257  df-3 12258  df-4 12259  df-5 12260  df-6 12261  df-7 12262  df-8 12263  df-9 12264  df-n0 12455  df-z 12541  df-dec 12660  df-uz 12805  df-rp 12957  df-fz 13467  df-fl 13739  df-mod 13817  df-seq 13949  df-exp 14010  df-cj 15028  df-re 15029  df-im 15030  df-sqrt 15164  df-abs 15165  df-dvds 16180  df-gcd 16418  df-prm 16591
This theorem is referenced by:  2503prm  17055
  Copyright terms: Public domain W3C validator