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

Theorem 2503lem3 15684
 Description: Lemma for 2503prm 15685. 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 11062 . . . 4 2 ∈ ℕ
2 1nn0 11185 . . . . 5 1 ∈ ℕ0
3 8nn0 11192 . . . . 5 8 ∈ ℕ0
42, 3deccl 11388 . . . 4 18 ∈ ℕ0
5 nnexpcl 12735 . . . 4 ((2 ∈ ℕ ∧ 18 ∈ ℕ0) → (2↑18) ∈ ℕ)
61, 4, 5mp2an 704 . . 3 (2↑18) ∈ ℕ
7 nnm1nn0 11211 . . 3 ((2↑18) ∈ ℕ → ((2↑18) − 1) ∈ ℕ0)
86, 7ax-mp 5 . 2 ((2↑18) − 1) ∈ ℕ0
9 3nn0 11187 . . . 4 3 ∈ ℕ0
104, 9deccl 11388 . . 3 183 ∈ ℕ0
1110, 2deccl 11388 . 2 1831 ∈ ℕ0
12 2503prm.1 . . 3 𝑁 = 2503
13 2nn0 11186 . . . . . 6 2 ∈ ℕ0
14 5nn0 11189 . . . . . 6 5 ∈ ℕ0
1513, 14deccl 11388 . . . . 5 25 ∈ ℕ0
16 0nn0 11184 . . . . 5 0 ∈ ℕ0
1715, 16deccl 11388 . . . 4 250 ∈ ℕ0
18 3nn 11063 . . . 4 3 ∈ ℕ
1917, 18decnncl 11394 . . 3 2503 ∈ ℕ
2012, 19eqeltri 2684 . 2 𝑁 ∈ ℕ
21122503lem1 15682 . . 3 ((2↑18) mod 𝑁) = (1832 mod 𝑁)
22 1p1e2 11011 . . . 4 (1 + 1) = 2
23 eqid 2610 . . . 4 1831 = 1831
2410, 2, 22, 23decsuc 11411 . . 3 (1831 + 1) = 1832
2520, 6, 2, 11, 21, 24modsubi 15614 . 2 (((2↑18) − 1) mod 𝑁) = (1831 mod 𝑁)
26 6nn0 11190 . . . . 5 6 ∈ ℕ0
27 7nn0 11191 . . . . 5 7 ∈ ℕ0
2826, 27deccl 11388 . . . 4 67 ∈ ℕ0
2928, 13deccl 11388 . . 3 672 ∈ ℕ0
30 4nn0 11188 . . . . . 6 4 ∈ ℕ0
3130, 3deccl 11388 . . . . 5 48 ∈ ℕ0
3231, 27deccl 11388 . . . 4 487 ∈ ℕ0
334, 14deccl 11388 . . . . 5 185 ∈ ℕ0
342, 2deccl 11388 . . . . . . 7 11 ∈ ℕ0
3534, 27deccl 11388 . . . . . 6 117 ∈ ℕ0
3626, 3deccl 11388 . . . . . . 7 68 ∈ ℕ0
37 9nn0 11193 . . . . . . . . 9 9 ∈ ℕ0
3830, 37deccl 11388 . . . . . . . 8 49 ∈ ℕ0
392, 37deccl 11388 . . . . . . . . 9 19 ∈ ℕ0
4038nn0zi 11279 . . . . . . . . . . 11 49 ∈ ℤ
4139nn0zi 11279 . . . . . . . . . . 11 19 ∈ ℤ
42 gcdcom 15073 . . . . . . . . . . 11 ((49 ∈ ℤ ∧ 19 ∈ ℤ) → (49 gcd 19) = (19 gcd 49))
4340, 41, 42mp2an 704 . . . . . . . . . 10 (49 gcd 19) = (19 gcd 49)
44 9nn 11069 . . . . . . . . . . . . 13 9 ∈ ℕ
452, 44decnncl 11394 . . . . . . . . . . . 12 19 ∈ ℕ
46 1nn 10908 . . . . . . . . . . . . 13 1 ∈ ℕ
472, 46decnncl 11394 . . . . . . . . . . . 12 11 ∈ ℕ
48 eqid 2610 . . . . . . . . . . . . 13 19 = 19
49 eqid 2610 . . . . . . . . . . . . 13 11 = 11
50 2cn 10968 . . . . . . . . . . . . . . . 16 2 ∈ ℂ
5150mulid2i 9922 . . . . . . . . . . . . . . 15 (1 · 2) = 2
5251, 22oveq12i 6561 . . . . . . . . . . . . . 14 ((1 · 2) + (1 + 1)) = (2 + 2)
53 2p2e4 11021 . . . . . . . . . . . . . 14 (2 + 2) = 4
5452, 53eqtri 2632 . . . . . . . . . . . . 13 ((1 · 2) + (1 + 1)) = 4
55 8p1e9 11035 . . . . . . . . . . . . . 14 (8 + 1) = 9
56 9t2e18 11539 . . . . . . . . . . . . . 14 (9 · 2) = 18
572, 3, 55, 56decsuc 11411 . . . . . . . . . . . . 13 ((9 · 2) + 1) = 19
582, 37, 2, 2, 48, 49, 13, 37, 2, 54, 57decmac 11442 . . . . . . . . . . . 12 ((19 · 2) + 11) = 49
59 1lt9 11106 . . . . . . . . . . . . 13 1 < 9
602, 2, 44, 59declt 11406 . . . . . . . . . . . 12 11 < 19
6145, 13, 47, 58, 60ndvdsi 14974 . . . . . . . . . . 11 ¬ 19 ∥ 49
62 19prm 15663 . . . . . . . . . . . 12 19 ∈ ℙ
63 coprm 15261 . . . . . . . . . . . 12 ((19 ∈ ℙ ∧ 49 ∈ ℤ) → (¬ 19 ∥ 49 ↔ (19 gcd 49) = 1))
6462, 40, 63mp2an 704 . . . . . . . . . . 11 19 ∥ 49 ↔ (19 gcd 49) = 1)
6561, 64mpbi 219 . . . . . . . . . 10 (19 gcd 49) = 1
6643, 65eqtri 2632 . . . . . . . . 9 (49 gcd 19) = 1
67 eqid 2610 . . . . . . . . . 10 49 = 49
68 4cn 10975 . . . . . . . . . . . . 13 4 ∈ ℂ
6968mulid2i 9922 . . . . . . . . . . . 12 (1 · 4) = 4
7069, 22oveq12i 6561 . . . . . . . . . . 11 ((1 · 4) + (1 + 1)) = (4 + 2)
71 4p2e6 11039 . . . . . . . . . . 11 (4 + 2) = 6
7270, 71eqtri 2632 . . . . . . . . . 10 ((1 · 4) + (1 + 1)) = 6
73 9cn 10985 . . . . . . . . . . . . 13 9 ∈ ℂ
7473mulid2i 9922 . . . . . . . . . . . 12 (1 · 9) = 9
7574oveq1i 6559 . . . . . . . . . . 11 ((1 · 9) + 9) = (9 + 9)
76 9p9e18 11503 . . . . . . . . . . 11 (9 + 9) = 18
7775, 76eqtri 2632 . . . . . . . . . 10 ((1 · 9) + 9) = 18
7830, 37, 2, 37, 67, 48, 2, 3, 2, 72, 77decma2c 11444 . . . . . . . . 9 ((1 · 49) + 19) = 68
792, 39, 38, 66, 78gcdi 15615 . . . . . . . 8 (68 gcd 49) = 1
80 eqid 2610 . . . . . . . . 9 68 = 68
81 6cn 10979 . . . . . . . . . . . 12 6 ∈ ℂ
8281mulid2i 9922 . . . . . . . . . . 11 (1 · 6) = 6
83 4p1e5 11031 . . . . . . . . . . 11 (4 + 1) = 5
8482, 83oveq12i 6561 . . . . . . . . . 10 ((1 · 6) + (4 + 1)) = (6 + 5)
85 6p5e11 11476 . . . . . . . . . 10 (6 + 5) = 11
8684, 85eqtri 2632 . . . . . . . . 9 ((1 · 6) + (4 + 1)) = 11
87 8cn 10983 . . . . . . . . . . . 12 8 ∈ ℂ
8887mulid2i 9922 . . . . . . . . . . 11 (1 · 8) = 8
8988oveq1i 6559 . . . . . . . . . 10 ((1 · 8) + 9) = (8 + 9)
90 9p8e17 11502 . . . . . . . . . . 11 (9 + 8) = 17
9173, 87, 90addcomli 10107 . . . . . . . . . 10 (8 + 9) = 17
9289, 91eqtri 2632 . . . . . . . . 9 ((1 · 8) + 9) = 17
9326, 3, 30, 37, 80, 67, 2, 27, 2, 86, 92decma2c 11444 . . . . . . . 8 ((1 · 68) + 49) = 117
942, 38, 36, 79, 93gcdi 15615 . . . . . . 7 (117 gcd 68) = 1
95 eqid 2610 . . . . . . . 8 117 = 117
96 6p1e7 11033 . . . . . . . . . 10 (6 + 1) = 7
9727dec0h 11398 . . . . . . . . . 10 7 = 07
9896, 97eqtri 2632 . . . . . . . . 9 (6 + 1) = 07
99 1t1e1 11052 . . . . . . . . . . 11 (1 · 1) = 1
100 00id 10090 . . . . . . . . . . 11 (0 + 0) = 0
10199, 100oveq12i 6561 . . . . . . . . . 10 ((1 · 1) + (0 + 0)) = (1 + 0)
102 ax-1cn 9873 . . . . . . . . . . 11 1 ∈ ℂ
103102addid1i 10102 . . . . . . . . . 10 (1 + 0) = 1
104101, 103eqtri 2632 . . . . . . . . 9 ((1 · 1) + (0 + 0)) = 1
10599oveq1i 6559 . . . . . . . . . 10 ((1 · 1) + 7) = (1 + 7)
106 7cn 10981 . . . . . . . . . . 11 7 ∈ ℂ
107 7p1e8 11034 . . . . . . . . . . 11 (7 + 1) = 8
108106, 102, 107addcomli 10107 . . . . . . . . . 10 (1 + 7) = 8
1093dec0h 11398 . . . . . . . . . 10 8 = 08
110105, 108, 1093eqtri 2636 . . . . . . . . 9 ((1 · 1) + 7) = 08
1112, 2, 16, 27, 49, 98, 2, 3, 16, 104, 110decma2c 11444 . . . . . . . 8 ((1 · 11) + (6 + 1)) = 18
112106mulid2i 9922 . . . . . . . . . 10 (1 · 7) = 7
113112oveq1i 6559 . . . . . . . . 9 ((1 · 7) + 8) = (7 + 8)
114 8p7e15 11493 . . . . . . . . . 10 (8 + 7) = 15
11587, 106, 114addcomli 10107 . . . . . . . . 9 (7 + 8) = 15
116113, 115eqtri 2632 . . . . . . . 8 ((1 · 7) + 8) = 15
11734, 27, 26, 3, 95, 80, 2, 14, 2, 111, 116decma2c 11444 . . . . . . 7 ((1 · 117) + 68) = 185
1182, 36, 35, 94, 117gcdi 15615 . . . . . 6 (185 gcd 117) = 1
119 eqid 2610 . . . . . . 7 185 = 185
120 eqid 2610 . . . . . . . 8 18 = 18
1212, 2, 22, 49decsuc 11411 . . . . . . . 8 (11 + 1) = 12
122 2t1e2 11053 . . . . . . . . . 10 (2 · 1) = 2
123122, 22oveq12i 6561 . . . . . . . . 9 ((2 · 1) + (1 + 1)) = (2 + 2)
124123, 53eqtri 2632 . . . . . . . 8 ((2 · 1) + (1 + 1)) = 4
125 8t2e16 11530 . . . . . . . . . 10 (8 · 2) = 16
12687, 50, 125mulcomli 9926 . . . . . . . . 9 (2 · 8) = 16
127 6p2e8 11046 . . . . . . . . 9 (6 + 2) = 8
1282, 26, 13, 126, 127decaddi 11455 . . . . . . . 8 ((2 · 8) + 2) = 18
1292, 3, 2, 13, 120, 121, 13, 3, 2, 124, 128decma2c 11444 . . . . . . 7 ((2 · 18) + (11 + 1)) = 48
130 5cn 10977 . . . . . . . . 9 5 ∈ ℂ
131 5t2e10 11510 . . . . . . . . 9 (5 · 2) = 10
132130, 50, 131mulcomli 9926 . . . . . . . 8 (2 · 5) = 10
133106addid2i 10103 . . . . . . . 8 (0 + 7) = 7
1342, 16, 27, 132, 133decaddi 11455 . . . . . . 7 ((2 · 5) + 7) = 17
1354, 14, 34, 27, 119, 95, 13, 27, 2, 129, 134decma2c 11444 . . . . . 6 ((2 · 185) + 117) = 487
13613, 35, 33, 118, 135gcdi 15615 . . . . 5 (487 gcd 185) = 1
137 eqid 2610 . . . . . 6 487 = 487
138 eqid 2610 . . . . . . 7 48 = 48
1392, 3, 55, 120decsuc 11411 . . . . . . 7 (18 + 1) = 19
14030, 3, 2, 37, 138, 139, 2, 27, 2, 72, 92decma2c 11444 . . . . . 6 ((1 · 48) + (18 + 1)) = 67
141112oveq1i 6559 . . . . . . 7 ((1 · 7) + 5) = (7 + 5)
142 7p5e12 11483 . . . . . . 7 (7 + 5) = 12
143141, 142eqtri 2632 . . . . . 6 ((1 · 7) + 5) = 12
14431, 27, 4, 14, 137, 119, 2, 13, 2, 140, 143decma2c 11444 . . . . 5 ((1 · 487) + 185) = 672
1452, 33, 32, 136, 144gcdi 15615 . . . 4 (672 gcd 487) = 1
146 eqid 2610 . . . . 5 672 = 672
147 eqid 2610 . . . . . 6 67 = 67
14830, 3, 55, 138decsuc 11411 . . . . . 6 (48 + 1) = 49
14971oveq2i 6560 . . . . . . 7 ((2 · 6) + (4 + 2)) = ((2 · 6) + 6)
150 6t2e12 11517 . . . . . . . . 9 (6 · 2) = 12
15181, 50, 150mulcomli 9926 . . . . . . . 8 (2 · 6) = 12
15281, 50, 127addcomli 10107 . . . . . . . 8 (2 + 6) = 8
1532, 13, 26, 151, 152decaddi 11455 . . . . . . 7 ((2 · 6) + 6) = 18
154149, 153eqtri 2632 . . . . . 6 ((2 · 6) + (4 + 2)) = 18
155 7t2e14 11524 . . . . . . . 8 (7 · 2) = 14
156106, 50, 155mulcomli 9926 . . . . . . 7 (2 · 7) = 14
157 9p4e13 11498 . . . . . . . 8 (9 + 4) = 13
15873, 68, 157addcomli 10107 . . . . . . 7 (4 + 9) = 13
1592, 30, 37, 156, 22, 9, 158decaddci 11456 . . . . . 6 ((2 · 7) + 9) = 23
16026, 27, 30, 37, 147, 148, 13, 9, 13, 154, 159decma2c 11444 . . . . 5 ((2 · 67) + (48 + 1)) = 183
161 2t2e4 11054 . . . . . . 7 (2 · 2) = 4
162161oveq1i 6559 . . . . . 6 ((2 · 2) + 7) = (4 + 7)
163 7p4e11 11481 . . . . . . 7 (7 + 4) = 11
164106, 68, 163addcomli 10107 . . . . . 6 (4 + 7) = 11
165162, 164eqtri 2632 . . . . 5 ((2 · 2) + 7) = 11
16628, 13, 31, 27, 146, 137, 13, 2, 2, 160, 165decma2c 11444 . . . 4 ((2 · 672) + 487) = 1831
16713, 32, 29, 145, 166gcdi 15615 . . 3 (1831 gcd 672) = 1
168 eqid 2610 . . . . . 6 183 = 183
16928nn0cni 11181 . . . . . . 7 67 ∈ ℂ
170169addid1i 10102 . . . . . 6 (67 + 0) = 67
171102addid2i 10103 . . . . . . . . 9 (0 + 1) = 1
17299, 171oveq12i 6561 . . . . . . . 8 ((1 · 1) + (0 + 1)) = (1 + 1)
173172, 22eqtri 2632 . . . . . . 7 ((1 · 1) + (0 + 1)) = 2
17488oveq1i 6559 . . . . . . . 8 ((1 · 8) + 7) = (8 + 7)
175174, 114eqtri 2632 . . . . . . 7 ((1 · 8) + 7) = 15
1762, 3, 16, 27, 120, 98, 2, 14, 2, 173, 175decma2c 11444 . . . . . 6 ((1 · 18) + (6 + 1)) = 25
177 3cn 10972 . . . . . . . . 9 3 ∈ ℂ
178177mulid2i 9922 . . . . . . . 8 (1 · 3) = 3
179178oveq1i 6559 . . . . . . 7 ((1 · 3) + 7) = (3 + 7)
180 7p3e10 11479 . . . . . . . 8 (7 + 3) = 10
181106, 177, 180addcomli 10107 . . . . . . 7 (3 + 7) = 10
182179, 181eqtri 2632 . . . . . 6 ((1 · 3) + 7) = 10
1834, 9, 26, 27, 168, 170, 2, 16, 2, 176, 182decma2c 11444 . . . . 5 ((1 · 183) + (67 + 0)) = 250
18499oveq1i 6559 . . . . . 6 ((1 · 1) + 2) = (1 + 2)
185 1p2e3 11029 . . . . . 6 (1 + 2) = 3
1869dec0h 11398 . . . . . 6 3 = 03
187184, 185, 1863eqtri 2636 . . . . 5 ((1 · 1) + 2) = 03
18810, 2, 28, 13, 23, 146, 2, 9, 16, 183, 187decma2c 11444 . . . 4 ((1 · 1831) + 672) = 2503
189188, 12eqtr4i 2635 . . 3 ((1 · 1831) + 672) = 𝑁
1902, 29, 11, 167, 189gcdi 15615 . 2 (𝑁 gcd 1831) = 1
1918, 11, 20, 25, 190gcdmodi 15616 1 (((2↑18) − 1) gcd 𝑁) = 1
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ↔ wb 195   = wceq 1475   ∈ wcel 1977   class class class wbr 4583  (class class class)co 6549  0cc0 9815  1c1 9816   + caddc 9818   · cmul 9820   − cmin 10145  ℕcn 10897  2c2 10947  3c3 10948  4c4 10949  5c5 10950  6c6 10951  7c7 10952  8c8 10953  9c9 10954  ℕ0cn0 11169  ℤcz 11254  ;cdc 11369  ↑cexp 12722   ∥ cdvds 14821   gcd cgcd 15054  ℙcprime 15223 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-2o 7448  df-oadd 7451  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-sup 8231  df-inf 8232  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-4 10958  df-5 10959  df-6 10960  df-7 10961  df-8 10962  df-9 10963  df-n0 11170  df-z 11255  df-dec 11370  df-uz 11564  df-rp 11709  df-fz 12198  df-fl 12455  df-mod 12531  df-seq 12664  df-exp 12723  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-dvds 14822  df-gcd 15055  df-prm 15224 This theorem is referenced by:  2503prm  15685
 Copyright terms: Public domain W3C validator