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

Theorem 2503lem3 16054
Description: Lemma for 2503prm 16055. 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 11388 . . . 4 2 ∈ ℕ
2 1nn0 11511 . . . . 5 1 ∈ ℕ0
3 8nn0 11518 . . . . 5 8 ∈ ℕ0
42, 3deccl 11715 . . . 4 18 ∈ ℕ0
5 nnexpcl 13081 . . . 4 ((2 ∈ ℕ ∧ 18 ∈ ℕ0) → (2↑18) ∈ ℕ)
61, 4, 5mp2an 666 . . 3 (2↑18) ∈ ℕ
7 nnm1nn0 11537 . . 3 ((2↑18) ∈ ℕ → ((2↑18) − 1) ∈ ℕ0)
86, 7ax-mp 5 . 2 ((2↑18) − 1) ∈ ℕ0
9 3nn0 11513 . . . 4 3 ∈ ℕ0
104, 9deccl 11715 . . 3 183 ∈ ℕ0
1110, 2deccl 11715 . 2 1831 ∈ ℕ0
12 2503prm.1 . . 3 𝑁 = 2503
13 2nn0 11512 . . . . . 6 2 ∈ ℕ0
14 5nn0 11515 . . . . . 6 5 ∈ ℕ0
1513, 14deccl 11715 . . . . 5 25 ∈ ℕ0
16 0nn0 11510 . . . . 5 0 ∈ ℕ0
1715, 16deccl 11715 . . . 4 250 ∈ ℕ0
18 3nn 11389 . . . 4 3 ∈ ℕ
1917, 18decnncl 11721 . . 3 2503 ∈ ℕ
2012, 19eqeltri 2846 . 2 𝑁 ∈ ℕ
21122503lem1 16052 . . 3 ((2↑18) mod 𝑁) = (1832 mod 𝑁)
22 1p1e2 11337 . . . 4 (1 + 1) = 2
23 eqid 2771 . . . 4 1831 = 1831
2410, 2, 22, 23decsuc 11738 . . 3 (1831 + 1) = 1832
2520, 6, 2, 11, 21, 24modsubi 15984 . 2 (((2↑18) − 1) mod 𝑁) = (1831 mod 𝑁)
26 6nn0 11516 . . . . 5 6 ∈ ℕ0
27 7nn0 11517 . . . . 5 7 ∈ ℕ0
2826, 27deccl 11715 . . . 4 67 ∈ ℕ0
2928, 13deccl 11715 . . 3 672 ∈ ℕ0
30 4nn0 11514 . . . . . 6 4 ∈ ℕ0
3130, 3deccl 11715 . . . . 5 48 ∈ ℕ0
3231, 27deccl 11715 . . . 4 487 ∈ ℕ0
334, 14deccl 11715 . . . . 5 185 ∈ ℕ0
342, 2deccl 11715 . . . . . . 7 11 ∈ ℕ0
3534, 27deccl 11715 . . . . . 6 117 ∈ ℕ0
3626, 3deccl 11715 . . . . . . 7 68 ∈ ℕ0
37 9nn0 11519 . . . . . . . . 9 9 ∈ ℕ0
3830, 37deccl 11715 . . . . . . . 8 49 ∈ ℕ0
392, 37deccl 11715 . . . . . . . . 9 19 ∈ ℕ0
4038nn0zi 11605 . . . . . . . . . . 11 49 ∈ ℤ
4139nn0zi 11605 . . . . . . . . . . 11 19 ∈ ℤ
42 gcdcom 15444 . . . . . . . . . . 11 ((49 ∈ ℤ ∧ 19 ∈ ℤ) → (49 gcd 19) = (19 gcd 49))
4340, 41, 42mp2an 666 . . . . . . . . . 10 (49 gcd 19) = (19 gcd 49)
44 9nn 11395 . . . . . . . . . . . . 13 9 ∈ ℕ
452, 44decnncl 11721 . . . . . . . . . . . 12 19 ∈ ℕ
46 1nn 11234 . . . . . . . . . . . . 13 1 ∈ ℕ
472, 46decnncl 11721 . . . . . . . . . . . 12 11 ∈ ℕ
48 eqid 2771 . . . . . . . . . . . . 13 19 = 19
49 eqid 2771 . . . . . . . . . . . . 13 11 = 11
50 2cn 11294 . . . . . . . . . . . . . . . 16 2 ∈ ℂ
5150mulid2i 10246 . . . . . . . . . . . . . . 15 (1 · 2) = 2
5251, 22oveq12i 6806 . . . . . . . . . . . . . 14 ((1 · 2) + (1 + 1)) = (2 + 2)
53 2p2e4 11347 . . . . . . . . . . . . . 14 (2 + 2) = 4
5452, 53eqtri 2793 . . . . . . . . . . . . 13 ((1 · 2) + (1 + 1)) = 4
55 8p1e9 11361 . . . . . . . . . . . . . 14 (8 + 1) = 9
56 9t2e18 11865 . . . . . . . . . . . . . 14 (9 · 2) = 18
572, 3, 55, 56decsuc 11738 . . . . . . . . . . . . 13 ((9 · 2) + 1) = 19
582, 37, 2, 2, 48, 49, 13, 37, 2, 54, 57decmac 11768 . . . . . . . . . . . 12 ((19 · 2) + 11) = 49
59 1lt9 11432 . . . . . . . . . . . . 13 1 < 9
602, 2, 44, 59declt 11733 . . . . . . . . . . . 12 11 < 19
6145, 13, 47, 58, 60ndvdsi 15345 . . . . . . . . . . 11 ¬ 19 ∥ 49
62 19prm 16033 . . . . . . . . . . . 12 19 ∈ ℙ
63 coprm 15631 . . . . . . . . . . . 12 ((19 ∈ ℙ ∧ 49 ∈ ℤ) → (¬ 19 ∥ 49 ↔ (19 gcd 49) = 1))
6462, 40, 63mp2an 666 . . . . . . . . . . 11 19 ∥ 49 ↔ (19 gcd 49) = 1)
6561, 64mpbi 220 . . . . . . . . . 10 (19 gcd 49) = 1
6643, 65eqtri 2793 . . . . . . . . 9 (49 gcd 19) = 1
67 eqid 2771 . . . . . . . . . 10 49 = 49
68 4cn 11301 . . . . . . . . . . . . 13 4 ∈ ℂ
6968mulid2i 10246 . . . . . . . . . . . 12 (1 · 4) = 4
7069, 22oveq12i 6806 . . . . . . . . . . 11 ((1 · 4) + (1 + 1)) = (4 + 2)
71 4p2e6 11365 . . . . . . . . . . 11 (4 + 2) = 6
7270, 71eqtri 2793 . . . . . . . . . 10 ((1 · 4) + (1 + 1)) = 6
73 9cn 11311 . . . . . . . . . . . . 13 9 ∈ ℂ
7473mulid2i 10246 . . . . . . . . . . . 12 (1 · 9) = 9
7574oveq1i 6804 . . . . . . . . . . 11 ((1 · 9) + 9) = (9 + 9)
76 9p9e18 11829 . . . . . . . . . . 11 (9 + 9) = 18
7775, 76eqtri 2793 . . . . . . . . . 10 ((1 · 9) + 9) = 18
7830, 37, 2, 37, 67, 48, 2, 3, 2, 72, 77decma2c 11770 . . . . . . . . 9 ((1 · 49) + 19) = 68
792, 39, 38, 66, 78gcdi 15985 . . . . . . . 8 (68 gcd 49) = 1
80 eqid 2771 . . . . . . . . 9 68 = 68
81 6cn 11305 . . . . . . . . . . . 12 6 ∈ ℂ
8281mulid2i 10246 . . . . . . . . . . 11 (1 · 6) = 6
83 4p1e5 11357 . . . . . . . . . . 11 (4 + 1) = 5
8482, 83oveq12i 6806 . . . . . . . . . 10 ((1 · 6) + (4 + 1)) = (6 + 5)
85 6p5e11 11802 . . . . . . . . . 10 (6 + 5) = 11
8684, 85eqtri 2793 . . . . . . . . 9 ((1 · 6) + (4 + 1)) = 11
87 8cn 11309 . . . . . . . . . . . 12 8 ∈ ℂ
8887mulid2i 10246 . . . . . . . . . . 11 (1 · 8) = 8
8988oveq1i 6804 . . . . . . . . . 10 ((1 · 8) + 9) = (8 + 9)
90 9p8e17 11828 . . . . . . . . . . 11 (9 + 8) = 17
9173, 87, 90addcomli 10431 . . . . . . . . . 10 (8 + 9) = 17
9289, 91eqtri 2793 . . . . . . . . 9 ((1 · 8) + 9) = 17
9326, 3, 30, 37, 80, 67, 2, 27, 2, 86, 92decma2c 11770 . . . . . . . 8 ((1 · 68) + 49) = 117
942, 38, 36, 79, 93gcdi 15985 . . . . . . 7 (117 gcd 68) = 1
95 eqid 2771 . . . . . . . 8 117 = 117
96 6p1e7 11359 . . . . . . . . . 10 (6 + 1) = 7
9727dec0h 11725 . . . . . . . . . 10 7 = 07
9896, 97eqtri 2793 . . . . . . . . 9 (6 + 1) = 07
99 1t1e1 11378 . . . . . . . . . . 11 (1 · 1) = 1
100 00id 10414 . . . . . . . . . . 11 (0 + 0) = 0
10199, 100oveq12i 6806 . . . . . . . . . 10 ((1 · 1) + (0 + 0)) = (1 + 0)
102 ax-1cn 10197 . . . . . . . . . . 11 1 ∈ ℂ
103102addid1i 10426 . . . . . . . . . 10 (1 + 0) = 1
104101, 103eqtri 2793 . . . . . . . . 9 ((1 · 1) + (0 + 0)) = 1
10599oveq1i 6804 . . . . . . . . . 10 ((1 · 1) + 7) = (1 + 7)
106 7cn 11307 . . . . . . . . . . 11 7 ∈ ℂ
107 7p1e8 11360 . . . . . . . . . . 11 (7 + 1) = 8
108106, 102, 107addcomli 10431 . . . . . . . . . 10 (1 + 7) = 8
1093dec0h 11725 . . . . . . . . . 10 8 = 08
110105, 108, 1093eqtri 2797 . . . . . . . . 9 ((1 · 1) + 7) = 08
1112, 2, 16, 27, 49, 98, 2, 3, 16, 104, 110decma2c 11770 . . . . . . . 8 ((1 · 11) + (6 + 1)) = 18
112106mulid2i 10246 . . . . . . . . . 10 (1 · 7) = 7
113112oveq1i 6804 . . . . . . . . 9 ((1 · 7) + 8) = (7 + 8)
114 8p7e15 11819 . . . . . . . . . 10 (8 + 7) = 15
11587, 106, 114addcomli 10431 . . . . . . . . 9 (7 + 8) = 15
116113, 115eqtri 2793 . . . . . . . 8 ((1 · 7) + 8) = 15
11734, 27, 26, 3, 95, 80, 2, 14, 2, 111, 116decma2c 11770 . . . . . . 7 ((1 · 117) + 68) = 185
1182, 36, 35, 94, 117gcdi 15985 . . . . . 6 (185 gcd 117) = 1
119 eqid 2771 . . . . . . 7 185 = 185
120 eqid 2771 . . . . . . . 8 18 = 18
1212, 2, 22, 49decsuc 11738 . . . . . . . 8 (11 + 1) = 12
122 2t1e2 11379 . . . . . . . . . 10 (2 · 1) = 2
123122, 22oveq12i 6806 . . . . . . . . 9 ((2 · 1) + (1 + 1)) = (2 + 2)
124123, 53eqtri 2793 . . . . . . . 8 ((2 · 1) + (1 + 1)) = 4
125 8t2e16 11856 . . . . . . . . . 10 (8 · 2) = 16
12687, 50, 125mulcomli 10250 . . . . . . . . 9 (2 · 8) = 16
127 6p2e8 11372 . . . . . . . . 9 (6 + 2) = 8
1282, 26, 13, 126, 127decaddi 11781 . . . . . . . 8 ((2 · 8) + 2) = 18
1292, 3, 2, 13, 120, 121, 13, 3, 2, 124, 128decma2c 11770 . . . . . . 7 ((2 · 18) + (11 + 1)) = 48
130 5cn 11303 . . . . . . . . 9 5 ∈ ℂ
131 5t2e10 11836 . . . . . . . . 9 (5 · 2) = 10
132130, 50, 131mulcomli 10250 . . . . . . . 8 (2 · 5) = 10
133106addid2i 10427 . . . . . . . 8 (0 + 7) = 7
1342, 16, 27, 132, 133decaddi 11781 . . . . . . 7 ((2 · 5) + 7) = 17
1354, 14, 34, 27, 119, 95, 13, 27, 2, 129, 134decma2c 11770 . . . . . 6 ((2 · 185) + 117) = 487
13613, 35, 33, 118, 135gcdi 15985 . . . . 5 (487 gcd 185) = 1
137 eqid 2771 . . . . . 6 487 = 487
138 eqid 2771 . . . . . . 7 48 = 48
1392, 3, 55, 120decsuc 11738 . . . . . . 7 (18 + 1) = 19
14030, 3, 2, 37, 138, 139, 2, 27, 2, 72, 92decma2c 11770 . . . . . 6 ((1 · 48) + (18 + 1)) = 67
141112oveq1i 6804 . . . . . . 7 ((1 · 7) + 5) = (7 + 5)
142 7p5e12 11809 . . . . . . 7 (7 + 5) = 12
143141, 142eqtri 2793 . . . . . 6 ((1 · 7) + 5) = 12
14431, 27, 4, 14, 137, 119, 2, 13, 2, 140, 143decma2c 11770 . . . . 5 ((1 · 487) + 185) = 672
1452, 33, 32, 136, 144gcdi 15985 . . . 4 (672 gcd 487) = 1
146 eqid 2771 . . . . 5 672 = 672
147 eqid 2771 . . . . . 6 67 = 67
14830, 3, 55, 138decsuc 11738 . . . . . 6 (48 + 1) = 49
14971oveq2i 6805 . . . . . . 7 ((2 · 6) + (4 + 2)) = ((2 · 6) + 6)
150 6t2e12 11843 . . . . . . . . 9 (6 · 2) = 12
15181, 50, 150mulcomli 10250 . . . . . . . 8 (2 · 6) = 12
15281, 50, 127addcomli 10431 . . . . . . . 8 (2 + 6) = 8
1532, 13, 26, 151, 152decaddi 11781 . . . . . . 7 ((2 · 6) + 6) = 18
154149, 153eqtri 2793 . . . . . 6 ((2 · 6) + (4 + 2)) = 18
155 7t2e14 11850 . . . . . . . 8 (7 · 2) = 14
156106, 50, 155mulcomli 10250 . . . . . . 7 (2 · 7) = 14
157 9p4e13 11824 . . . . . . . 8 (9 + 4) = 13
15873, 68, 157addcomli 10431 . . . . . . 7 (4 + 9) = 13
1592, 30, 37, 156, 22, 9, 158decaddci 11782 . . . . . 6 ((2 · 7) + 9) = 23
16026, 27, 30, 37, 147, 148, 13, 9, 13, 154, 159decma2c 11770 . . . . 5 ((2 · 67) + (48 + 1)) = 183
161 2t2e4 11380 . . . . . . 7 (2 · 2) = 4
162161oveq1i 6804 . . . . . 6 ((2 · 2) + 7) = (4 + 7)
163 7p4e11 11807 . . . . . . 7 (7 + 4) = 11
164106, 68, 163addcomli 10431 . . . . . 6 (4 + 7) = 11
165162, 164eqtri 2793 . . . . 5 ((2 · 2) + 7) = 11
16628, 13, 31, 27, 146, 137, 13, 2, 2, 160, 165decma2c 11770 . . . 4 ((2 · 672) + 487) = 1831
16713, 32, 29, 145, 166gcdi 15985 . . 3 (1831 gcd 672) = 1
168 eqid 2771 . . . . . 6 183 = 183
16928nn0cni 11507 . . . . . . 7 67 ∈ ℂ
170169addid1i 10426 . . . . . 6 (67 + 0) = 67
171102addid2i 10427 . . . . . . . . 9 (0 + 1) = 1
17299, 171oveq12i 6806 . . . . . . . 8 ((1 · 1) + (0 + 1)) = (1 + 1)
173172, 22eqtri 2793 . . . . . . 7 ((1 · 1) + (0 + 1)) = 2
17488oveq1i 6804 . . . . . . . 8 ((1 · 8) + 7) = (8 + 7)
175174, 114eqtri 2793 . . . . . . 7 ((1 · 8) + 7) = 15
1762, 3, 16, 27, 120, 98, 2, 14, 2, 173, 175decma2c 11770 . . . . . 6 ((1 · 18) + (6 + 1)) = 25
177 3cn 11298 . . . . . . . . 9 3 ∈ ℂ
178177mulid2i 10246 . . . . . . . 8 (1 · 3) = 3
179178oveq1i 6804 . . . . . . 7 ((1 · 3) + 7) = (3 + 7)
180 7p3e10 11805 . . . . . . . 8 (7 + 3) = 10
181106, 177, 180addcomli 10431 . . . . . . 7 (3 + 7) = 10
182179, 181eqtri 2793 . . . . . 6 ((1 · 3) + 7) = 10
1834, 9, 26, 27, 168, 170, 2, 16, 2, 176, 182decma2c 11770 . . . . 5 ((1 · 183) + (67 + 0)) = 250
18499oveq1i 6804 . . . . . 6 ((1 · 1) + 2) = (1 + 2)
185 1p2e3 11355 . . . . . 6 (1 + 2) = 3
1869dec0h 11725 . . . . . 6 3 = 03
187184, 185, 1863eqtri 2797 . . . . 5 ((1 · 1) + 2) = 03
18810, 2, 28, 13, 23, 146, 2, 9, 16, 183, 187decma2c 11770 . . . 4 ((1 · 1831) + 672) = 2503
189188, 12eqtr4i 2796 . . 3 ((1 · 1831) + 672) = 𝑁
1902, 29, 11, 167, 189gcdi 15985 . 2 (𝑁 gcd 1831) = 1
1918, 11, 20, 25, 190gcdmodi 15986 1 (((2↑18) − 1) gcd 𝑁) = 1
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196   = wceq 1631  wcel 2145   class class class wbr 4787  (class class class)co 6794  0cc0 10139  1c1 10140   + caddc 10142   · cmul 10144  cmin 10469  cn 11223  2c2 11273  3c3 11274  4c4 11275  5c5 11276  6c6 11277  7c7 11278  8c8 11279  9c9 11280  0cn0 11495  cz 11580  cdc 11696  cexp 13068  cdvds 15190   gcd cgcd 15425  cprime 15593
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4916  ax-nul 4924  ax-pow 4975  ax-pr 5035  ax-un 7097  ax-cnex 10195  ax-resscn 10196  ax-1cn 10197  ax-icn 10198  ax-addcl 10199  ax-addrcl 10200  ax-mulcl 10201  ax-mulrcl 10202  ax-mulcom 10203  ax-addass 10204  ax-mulass 10205  ax-distr 10206  ax-i2m1 10207  ax-1ne0 10208  ax-1rid 10209  ax-rnegex 10210  ax-rrecex 10211  ax-cnre 10212  ax-pre-lttri 10213  ax-pre-lttrn 10214  ax-pre-ltadd 10215  ax-pre-mulgt0 10216  ax-pre-sup 10217
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3589  df-csb 3684  df-dif 3727  df-un 3729  df-in 3731  df-ss 3738  df-pss 3740  df-nul 4065  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-tp 4322  df-op 4324  df-uni 4576  df-iun 4657  df-br 4788  df-opab 4848  df-mpt 4865  df-tr 4888  df-id 5158  df-eprel 5163  df-po 5171  df-so 5172  df-fr 5209  df-we 5211  df-xp 5256  df-rel 5257  df-cnv 5258  df-co 5259  df-dm 5260  df-rn 5261  df-res 5262  df-ima 5263  df-pred 5824  df-ord 5870  df-on 5871  df-lim 5872  df-suc 5873  df-iota 5995  df-fun 6034  df-fn 6035  df-f 6036  df-f1 6037  df-fo 6038  df-f1o 6039  df-fv 6040  df-riota 6755  df-ov 6797  df-oprab 6798  df-mpt2 6799  df-om 7214  df-1st 7316  df-2nd 7317  df-wrecs 7560  df-recs 7622  df-rdg 7660  df-1o 7714  df-2o 7715  df-er 7897  df-en 8111  df-dom 8112  df-sdom 8113  df-fin 8114  df-sup 8505  df-inf 8506  df-pnf 10279  df-mnf 10280  df-xr 10281  df-ltxr 10282  df-le 10283  df-sub 10471  df-neg 10472  df-div 10888  df-nn 11224  df-2 11282  df-3 11283  df-4 11284  df-5 11285  df-6 11286  df-7 11287  df-8 11288  df-9 11289  df-n0 11496  df-z 11581  df-dec 11697  df-uz 11890  df-rp 12037  df-fz 12535  df-fl 12802  df-mod 12878  df-seq 13010  df-exp 13069  df-cj 14048  df-re 14049  df-im 14050  df-sqrt 14184  df-abs 14185  df-dvds 15191  df-gcd 15426  df-prm 15594
This theorem is referenced by:  2503prm  16055
  Copyright terms: Public domain W3C validator