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

Theorem 2503lem3 17117
Description: Lemma for 2503prm 17118. 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 12325 . . . 4 2 ∈ ℕ
2 1nn0 12528 . . . . 5 1 ∈ ℕ0
3 8nn0 12535 . . . . 5 8 ∈ ℕ0
42, 3deccl 12732 . . . 4 18 ∈ ℕ0
5 nnexpcl 14081 . . . 4 ((2 ∈ ℕ ∧ 18 ∈ ℕ0) → (2↑18) ∈ ℕ)
61, 4, 5mp2an 690 . . 3 (2↑18) ∈ ℕ
7 nnm1nn0 12553 . . 3 ((2↑18) ∈ ℕ → ((2↑18) − 1) ∈ ℕ0)
86, 7ax-mp 5 . 2 ((2↑18) − 1) ∈ ℕ0
9 3nn0 12530 . . . 4 3 ∈ ℕ0
104, 9deccl 12732 . . 3 183 ∈ ℕ0
1110, 2deccl 12732 . 2 1831 ∈ ℕ0
12 2503prm.1 . . 3 𝑁 = 2503
13 2nn0 12529 . . . . . 6 2 ∈ ℕ0
14 5nn0 12532 . . . . . 6 5 ∈ ℕ0
1513, 14deccl 12732 . . . . 5 25 ∈ ℕ0
16 0nn0 12527 . . . . 5 0 ∈ ℕ0
1715, 16deccl 12732 . . . 4 250 ∈ ℕ0
18 3nn 12331 . . . 4 3 ∈ ℕ
1917, 18decnncl 12737 . . 3 2503 ∈ ℕ
2012, 19eqeltri 2825 . 2 𝑁 ∈ ℕ
21122503lem1 17115 . . 3 ((2↑18) mod 𝑁) = (1832 mod 𝑁)
22 1p1e2 12377 . . . 4 (1 + 1) = 2
23 eqid 2728 . . . 4 1831 = 1831
2410, 2, 22, 23decsuc 12748 . . 3 (1831 + 1) = 1832
2520, 6, 2, 11, 21, 24modsubi 17050 . 2 (((2↑18) − 1) mod 𝑁) = (1831 mod 𝑁)
26 6nn0 12533 . . . . 5 6 ∈ ℕ0
27 7nn0 12534 . . . . 5 7 ∈ ℕ0
2826, 27deccl 12732 . . . 4 67 ∈ ℕ0
2928, 13deccl 12732 . . 3 672 ∈ ℕ0
30 4nn0 12531 . . . . . 6 4 ∈ ℕ0
3130, 3deccl 12732 . . . . 5 48 ∈ ℕ0
3231, 27deccl 12732 . . . 4 487 ∈ ℕ0
334, 14deccl 12732 . . . . 5 185 ∈ ℕ0
342, 2deccl 12732 . . . . . . 7 11 ∈ ℕ0
3534, 27deccl 12732 . . . . . 6 117 ∈ ℕ0
3626, 3deccl 12732 . . . . . . 7 68 ∈ ℕ0
37 9nn0 12536 . . . . . . . . 9 9 ∈ ℕ0
3830, 37deccl 12732 . . . . . . . 8 49 ∈ ℕ0
392, 37deccl 12732 . . . . . . . . 9 19 ∈ ℕ0
4038nn0zi 12627 . . . . . . . . . . 11 49 ∈ ℤ
4139nn0zi 12627 . . . . . . . . . . 11 19 ∈ ℤ
42 gcdcom 16497 . . . . . . . . . . 11 ((49 ∈ ℤ ∧ 19 ∈ ℤ) → (49 gcd 19) = (19 gcd 49))
4340, 41, 42mp2an 690 . . . . . . . . . 10 (49 gcd 19) = (19 gcd 49)
44 9nn 12350 . . . . . . . . . . . . 13 9 ∈ ℕ
452, 44decnncl 12737 . . . . . . . . . . . 12 19 ∈ ℕ
46 1nn 12263 . . . . . . . . . . . . 13 1 ∈ ℕ
472, 46decnncl 12737 . . . . . . . . . . . 12 11 ∈ ℕ
48 eqid 2728 . . . . . . . . . . . . 13 19 = 19
49 eqid 2728 . . . . . . . . . . . . 13 11 = 11
50 2cn 12327 . . . . . . . . . . . . . . . 16 2 ∈ ℂ
5150mullidi 11259 . . . . . . . . . . . . . . 15 (1 · 2) = 2
5251, 22oveq12i 7438 . . . . . . . . . . . . . 14 ((1 · 2) + (1 + 1)) = (2 + 2)
53 2p2e4 12387 . . . . . . . . . . . . . 14 (2 + 2) = 4
5452, 53eqtri 2756 . . . . . . . . . . . . 13 ((1 · 2) + (1 + 1)) = 4
55 8p1e9 12402 . . . . . . . . . . . . . 14 (8 + 1) = 9
56 9t2e18 12839 . . . . . . . . . . . . . 14 (9 · 2) = 18
572, 3, 55, 56decsuc 12748 . . . . . . . . . . . . 13 ((9 · 2) + 1) = 19
582, 37, 2, 2, 48, 49, 13, 37, 2, 54, 57decmac 12769 . . . . . . . . . . . 12 ((19 · 2) + 11) = 49
59 1lt9 12458 . . . . . . . . . . . . 13 1 < 9
602, 2, 44, 59declt 12745 . . . . . . . . . . . 12 11 < 19
6145, 13, 47, 58, 60ndvdsi 16398 . . . . . . . . . . 11 ¬ 19 ∥ 49
62 19prm 17096 . . . . . . . . . . . 12 19 ∈ ℙ
63 coprm 16691 . . . . . . . . . . . 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 2756 . . . . . . . . 9 (49 gcd 19) = 1
67 eqid 2728 . . . . . . . . . 10 49 = 49
68 4cn 12337 . . . . . . . . . . . . 13 4 ∈ ℂ
6968mullidi 11259 . . . . . . . . . . . 12 (1 · 4) = 4
7069, 22oveq12i 7438 . . . . . . . . . . 11 ((1 · 4) + (1 + 1)) = (4 + 2)
71 4p2e6 12405 . . . . . . . . . . 11 (4 + 2) = 6
7270, 71eqtri 2756 . . . . . . . . . 10 ((1 · 4) + (1 + 1)) = 6
73 9cn 12352 . . . . . . . . . . . . 13 9 ∈ ℂ
7473mullidi 11259 . . . . . . . . . . . 12 (1 · 9) = 9
7574oveq1i 7436 . . . . . . . . . . 11 ((1 · 9) + 9) = (9 + 9)
76 9p9e18 12811 . . . . . . . . . . 11 (9 + 9) = 18
7775, 76eqtri 2756 . . . . . . . . . 10 ((1 · 9) + 9) = 18
7830, 37, 2, 37, 67, 48, 2, 3, 2, 72, 77decma2c 12770 . . . . . . . . 9 ((1 · 49) + 19) = 68
792, 39, 38, 66, 78gcdi 17051 . . . . . . . 8 (68 gcd 49) = 1
80 eqid 2728 . . . . . . . . 9 68 = 68
81 6cn 12343 . . . . . . . . . . . 12 6 ∈ ℂ
8281mullidi 11259 . . . . . . . . . . 11 (1 · 6) = 6
83 4p1e5 12398 . . . . . . . . . . 11 (4 + 1) = 5
8482, 83oveq12i 7438 . . . . . . . . . 10 ((1 · 6) + (4 + 1)) = (6 + 5)
85 6p5e11 12790 . . . . . . . . . 10 (6 + 5) = 11
8684, 85eqtri 2756 . . . . . . . . 9 ((1 · 6) + (4 + 1)) = 11
87 8cn 12349 . . . . . . . . . . . 12 8 ∈ ℂ
8887mullidi 11259 . . . . . . . . . . 11 (1 · 8) = 8
8988oveq1i 7436 . . . . . . . . . 10 ((1 · 8) + 9) = (8 + 9)
90 9p8e17 12810 . . . . . . . . . . 11 (9 + 8) = 17
9173, 87, 90addcomli 11446 . . . . . . . . . 10 (8 + 9) = 17
9289, 91eqtri 2756 . . . . . . . . 9 ((1 · 8) + 9) = 17
9326, 3, 30, 37, 80, 67, 2, 27, 2, 86, 92decma2c 12770 . . . . . . . 8 ((1 · 68) + 49) = 117
942, 38, 36, 79, 93gcdi 17051 . . . . . . 7 (117 gcd 68) = 1
95 eqid 2728 . . . . . . . 8 117 = 117
96 6p1e7 12400 . . . . . . . . . 10 (6 + 1) = 7
9727dec0h 12739 . . . . . . . . . 10 7 = 07
9896, 97eqtri 2756 . . . . . . . . 9 (6 + 1) = 07
99 1t1e1 12414 . . . . . . . . . . 11 (1 · 1) = 1
100 00id 11429 . . . . . . . . . . 11 (0 + 0) = 0
10199, 100oveq12i 7438 . . . . . . . . . 10 ((1 · 1) + (0 + 0)) = (1 + 0)
102 ax-1cn 11206 . . . . . . . . . . 11 1 ∈ ℂ
103102addridi 11441 . . . . . . . . . 10 (1 + 0) = 1
104101, 103eqtri 2756 . . . . . . . . 9 ((1 · 1) + (0 + 0)) = 1
10599oveq1i 7436 . . . . . . . . . 10 ((1 · 1) + 7) = (1 + 7)
106 7cn 12346 . . . . . . . . . . 11 7 ∈ ℂ
107 7p1e8 12401 . . . . . . . . . . 11 (7 + 1) = 8
108106, 102, 107addcomli 11446 . . . . . . . . . 10 (1 + 7) = 8
1093dec0h 12739 . . . . . . . . . 10 8 = 08
110105, 108, 1093eqtri 2760 . . . . . . . . 9 ((1 · 1) + 7) = 08
1112, 2, 16, 27, 49, 98, 2, 3, 16, 104, 110decma2c 12770 . . . . . . . 8 ((1 · 11) + (6 + 1)) = 18
112106mullidi 11259 . . . . . . . . . 10 (1 · 7) = 7
113112oveq1i 7436 . . . . . . . . 9 ((1 · 7) + 8) = (7 + 8)
114 8p7e15 12802 . . . . . . . . . 10 (8 + 7) = 15
11587, 106, 114addcomli 11446 . . . . . . . . 9 (7 + 8) = 15
116113, 115eqtri 2756 . . . . . . . 8 ((1 · 7) + 8) = 15
11734, 27, 26, 3, 95, 80, 2, 14, 2, 111, 116decma2c 12770 . . . . . . 7 ((1 · 117) + 68) = 185
1182, 36, 35, 94, 117gcdi 17051 . . . . . 6 (185 gcd 117) = 1
119 eqid 2728 . . . . . . 7 185 = 185
120 eqid 2728 . . . . . . . 8 18 = 18
1212, 2, 22, 49decsuc 12748 . . . . . . . 8 (11 + 1) = 12
122 2t1e2 12415 . . . . . . . . . 10 (2 · 1) = 2
123122, 22oveq12i 7438 . . . . . . . . 9 ((2 · 1) + (1 + 1)) = (2 + 2)
124123, 53eqtri 2756 . . . . . . . 8 ((2 · 1) + (1 + 1)) = 4
125 8t2e16 12832 . . . . . . . . . 10 (8 · 2) = 16
12687, 50, 125mulcomli 11263 . . . . . . . . 9 (2 · 8) = 16
127 6p2e8 12411 . . . . . . . . 9 (6 + 2) = 8
1282, 26, 13, 126, 127decaddi 12777 . . . . . . . 8 ((2 · 8) + 2) = 18
1292, 3, 2, 13, 120, 121, 13, 3, 2, 124, 128decma2c 12770 . . . . . . 7 ((2 · 18) + (11 + 1)) = 48
130 5cn 12340 . . . . . . . . 9 5 ∈ ℂ
131 5t2e10 12817 . . . . . . . . 9 (5 · 2) = 10
132130, 50, 131mulcomli 11263 . . . . . . . 8 (2 · 5) = 10
133106addlidi 11442 . . . . . . . 8 (0 + 7) = 7
1342, 16, 27, 132, 133decaddi 12777 . . . . . . 7 ((2 · 5) + 7) = 17
1354, 14, 34, 27, 119, 95, 13, 27, 2, 129, 134decma2c 12770 . . . . . 6 ((2 · 185) + 117) = 487
13613, 35, 33, 118, 135gcdi 17051 . . . . 5 (487 gcd 185) = 1
137 eqid 2728 . . . . . 6 487 = 487
138 eqid 2728 . . . . . . 7 48 = 48
1392, 3, 55, 120decsuc 12748 . . . . . . 7 (18 + 1) = 19
14030, 3, 2, 37, 138, 139, 2, 27, 2, 72, 92decma2c 12770 . . . . . 6 ((1 · 48) + (18 + 1)) = 67
141112oveq1i 7436 . . . . . . 7 ((1 · 7) + 5) = (7 + 5)
142 7p5e12 12794 . . . . . . 7 (7 + 5) = 12
143141, 142eqtri 2756 . . . . . 6 ((1 · 7) + 5) = 12
14431, 27, 4, 14, 137, 119, 2, 13, 2, 140, 143decma2c 12770 . . . . 5 ((1 · 487) + 185) = 672
1452, 33, 32, 136, 144gcdi 17051 . . . 4 (672 gcd 487) = 1
146 eqid 2728 . . . . 5 672 = 672
147 eqid 2728 . . . . . 6 67 = 67
14830, 3, 55, 138decsuc 12748 . . . . . 6 (48 + 1) = 49
14971oveq2i 7437 . . . . . . 7 ((2 · 6) + (4 + 2)) = ((2 · 6) + 6)
150 6t2e12 12821 . . . . . . . . 9 (6 · 2) = 12
15181, 50, 150mulcomli 11263 . . . . . . . 8 (2 · 6) = 12
15281, 50, 127addcomli 11446 . . . . . . . 8 (2 + 6) = 8
1532, 13, 26, 151, 152decaddi 12777 . . . . . . 7 ((2 · 6) + 6) = 18
154149, 153eqtri 2756 . . . . . 6 ((2 · 6) + (4 + 2)) = 18
155 7t2e14 12826 . . . . . . . 8 (7 · 2) = 14
156106, 50, 155mulcomli 11263 . . . . . . 7 (2 · 7) = 14
157 9p4e13 12806 . . . . . . . 8 (9 + 4) = 13
15873, 68, 157addcomli 11446 . . . . . . 7 (4 + 9) = 13
1592, 30, 37, 156, 22, 9, 158decaddci 12778 . . . . . 6 ((2 · 7) + 9) = 23
16026, 27, 30, 37, 147, 148, 13, 9, 13, 154, 159decma2c 12770 . . . . 5 ((2 · 67) + (48 + 1)) = 183
161 2t2e4 12416 . . . . . . 7 (2 · 2) = 4
162161oveq1i 7436 . . . . . 6 ((2 · 2) + 7) = (4 + 7)
163 7p4e11 12793 . . . . . . 7 (7 + 4) = 11
164106, 68, 163addcomli 11446 . . . . . 6 (4 + 7) = 11
165162, 164eqtri 2756 . . . . 5 ((2 · 2) + 7) = 11
16628, 13, 31, 27, 146, 137, 13, 2, 2, 160, 165decma2c 12770 . . . 4 ((2 · 672) + 487) = 1831
16713, 32, 29, 145, 166gcdi 17051 . . 3 (1831 gcd 672) = 1
168 eqid 2728 . . . . . 6 183 = 183
16928nn0cni 12524 . . . . . . 7 67 ∈ ℂ
170169addridi 11441 . . . . . 6 (67 + 0) = 67
171102addlidi 11442 . . . . . . . . 9 (0 + 1) = 1
17299, 171oveq12i 7438 . . . . . . . 8 ((1 · 1) + (0 + 1)) = (1 + 1)
173172, 22eqtri 2756 . . . . . . 7 ((1 · 1) + (0 + 1)) = 2
17488oveq1i 7436 . . . . . . . 8 ((1 · 8) + 7) = (8 + 7)
175174, 114eqtri 2756 . . . . . . 7 ((1 · 8) + 7) = 15
1762, 3, 16, 27, 120, 98, 2, 14, 2, 173, 175decma2c 12770 . . . . . 6 ((1 · 18) + (6 + 1)) = 25
177 3cn 12333 . . . . . . . . 9 3 ∈ ℂ
178177mullidi 11259 . . . . . . . 8 (1 · 3) = 3
179178oveq1i 7436 . . . . . . 7 ((1 · 3) + 7) = (3 + 7)
180 7p3e10 12792 . . . . . . . 8 (7 + 3) = 10
181106, 177, 180addcomli 11446 . . . . . . 7 (3 + 7) = 10
182179, 181eqtri 2756 . . . . . 6 ((1 · 3) + 7) = 10
1834, 9, 26, 27, 168, 170, 2, 16, 2, 176, 182decma2c 12770 . . . . 5 ((1 · 183) + (67 + 0)) = 250
18499oveq1i 7436 . . . . . 6 ((1 · 1) + 2) = (1 + 2)
185 1p2e3 12395 . . . . . 6 (1 + 2) = 3
1869dec0h 12739 . . . . . 6 3 = 03
187184, 185, 1863eqtri 2760 . . . . 5 ((1 · 1) + 2) = 03
18810, 2, 28, 13, 23, 146, 2, 9, 16, 183, 187decma2c 12770 . . . 4 ((1 · 1831) + 672) = 2503
189188, 12eqtr4i 2759 . . 3 ((1 · 1831) + 672) = 𝑁
1902, 29, 11, 167, 189gcdi 17051 . 2 (𝑁 gcd 1831) = 1
1918, 11, 20, 25, 190gcdmodi 17052 1 (((2↑18) − 1) gcd 𝑁) = 1
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 205   = wceq 1533  wcel 2098   class class class wbr 5152  (class class class)co 7426  0cc0 11148  1c1 11149   + caddc 11151   · cmul 11153  cmin 11484  cn 12252  2c2 12307  3c3 12308  4c4 12309  5c5 12310  6c6 12311  7c7 12312  8c8 12313  9c9 12314  0cn0 12512  cz 12598  cdc 12717  cexp 14068  cdvds 16240   gcd cgcd 16478  cprime 16651
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2699  ax-sep 5303  ax-nul 5310  ax-pow 5369  ax-pr 5433  ax-un 7748  ax-cnex 11204  ax-resscn 11205  ax-1cn 11206  ax-icn 11207  ax-addcl 11208  ax-addrcl 11209  ax-mulcl 11210  ax-mulrcl 11211  ax-mulcom 11212  ax-addass 11213  ax-mulass 11214  ax-distr 11215  ax-i2m1 11216  ax-1ne0 11217  ax-1rid 11218  ax-rnegex 11219  ax-rrecex 11220  ax-cnre 11221  ax-pre-lttri 11222  ax-pre-lttrn 11223  ax-pre-ltadd 11224  ax-pre-mulgt0 11225  ax-pre-sup 11226
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-iun 5002  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6310  df-ord 6377  df-on 6378  df-lim 6379  df-suc 6380  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-riota 7382  df-ov 7429  df-oprab 7430  df-mpo 7431  df-om 7879  df-1st 8001  df-2nd 8002  df-frecs 8295  df-wrecs 8326  df-recs 8400  df-rdg 8439  df-1o 8495  df-2o 8496  df-er 8733  df-en 8973  df-dom 8974  df-sdom 8975  df-fin 8976  df-sup 9475  df-inf 9476  df-pnf 11290  df-mnf 11291  df-xr 11292  df-ltxr 11293  df-le 11294  df-sub 11486  df-neg 11487  df-div 11912  df-nn 12253  df-2 12315  df-3 12316  df-4 12317  df-5 12318  df-6 12319  df-7 12320  df-8 12321  df-9 12322  df-n0 12513  df-z 12599  df-dec 12718  df-uz 12863  df-rp 13017  df-fz 13527  df-fl 13799  df-mod 13877  df-seq 14009  df-exp 14069  df-cj 15088  df-re 15089  df-im 15090  df-sqrt 15224  df-abs 15225  df-dvds 16241  df-gcd 16479  df-prm 16652
This theorem is referenced by:  2503prm  17118
  Copyright terms: Public domain W3C validator