Metamath Proof Explorer

Theorem 2503lem3

Description: Lemma for 2503prm . Calculate the GCD of 2 ^ 1 8 - 1 == 1 8 3 1 with N = 2 5 0 3 . (Contributed by Mario Carneiro, 3-Mar-2014) (Revised by Mario Carneiro, 20-Apr-2015) (Proof shortened by AV, 15-Sep-2021)

Ref Expression
Hypothesis 2503prm.1 
|- N = ; ; ; 2 5 0 3
Assertion 2503lem3 
|- ( ( ( 2 ^ ; 1 8 ) - 1 ) gcd N ) = 1

Proof

Step Hyp Ref Expression
1 2503prm.1 
 |-  N = ; ; ; 2 5 0 3
2 2nn 
 |-  2 e. NN
3 1nn0 
 |-  1 e. NN0
4 8nn0 
 |-  8 e. NN0
5 3 4 deccl 
 |-  ; 1 8 e. NN0
6 nnexpcl 
 |-  ( ( 2 e. NN /\ ; 1 8 e. NN0 ) -> ( 2 ^ ; 1 8 ) e. NN )
7 2 5 6 mp2an 
 |-  ( 2 ^ ; 1 8 ) e. NN
8 nnm1nn0 
 |-  ( ( 2 ^ ; 1 8 ) e. NN -> ( ( 2 ^ ; 1 8 ) - 1 ) e. NN0 )
9 7 8 ax-mp 
 |-  ( ( 2 ^ ; 1 8 ) - 1 ) e. NN0
10 3nn0 
 |-  3 e. NN0
11 5 10 deccl 
 |-  ; ; 1 8 3 e. NN0
12 11 3 deccl 
 |-  ; ; ; 1 8 3 1 e. NN0
13 2nn0 
 |-  2 e. NN0
14 5nn0 
 |-  5 e. NN0
15 13 14 deccl 
 |-  ; 2 5 e. NN0
16 0nn0 
 |-  0 e. NN0
17 15 16 deccl 
 |-  ; ; 2 5 0 e. NN0
18 3nn 
 |-  3 e. NN
19 17 18 decnncl 
 |-  ; ; ; 2 5 0 3 e. NN
20 1 19 eqeltri 
 |-  N e. NN
21 1 2503lem1 
 |-  ( ( 2 ^ ; 1 8 ) mod N ) = ( ; ; ; 1 8 3 2 mod N )
22 1p1e2 
 |-  ( 1 + 1 ) = 2
23 eqid 
 |-  ; ; ; 1 8 3 1 = ; ; ; 1 8 3 1
24 11 3 22 23 decsuc 
 |-  ( ; ; ; 1 8 3 1 + 1 ) = ; ; ; 1 8 3 2
25 20 7 3 12 21 24 modsubi 
 |-  ( ( ( 2 ^ ; 1 8 ) - 1 ) mod N ) = ( ; ; ; 1 8 3 1 mod N )
26 6nn0 
 |-  6 e. NN0
27 7nn0 
 |-  7 e. NN0
28 26 27 deccl 
 |-  ; 6 7 e. NN0
29 28 13 deccl 
 |-  ; ; 6 7 2 e. NN0
30 4nn0 
 |-  4 e. NN0
31 30 4 deccl 
 |-  ; 4 8 e. NN0
32 31 27 deccl 
 |-  ; ; 4 8 7 e. NN0
33 5 14 deccl 
 |-  ; ; 1 8 5 e. NN0
34 3 3 deccl 
 |-  ; 1 1 e. NN0
35 34 27 deccl 
 |-  ; ; 1 1 7 e. NN0
36 26 4 deccl 
 |-  ; 6 8 e. NN0
37 9nn0 
 |-  9 e. NN0
38 30 37 deccl 
 |-  ; 4 9 e. NN0
39 3 37 deccl 
 |-  ; 1 9 e. NN0
40 38 nn0zi 
 |-  ; 4 9 e. ZZ
41 39 nn0zi 
 |-  ; 1 9 e. ZZ
42 gcdcom 
 |-  ( ( ; 4 9 e. ZZ /\ ; 1 9 e. ZZ ) -> ( ; 4 9 gcd ; 1 9 ) = ( ; 1 9 gcd ; 4 9 ) )
43 40 41 42 mp2an 
 |-  ( ; 4 9 gcd ; 1 9 ) = ( ; 1 9 gcd ; 4 9 )
44 9nn 
 |-  9 e. NN
45 3 44 decnncl 
 |-  ; 1 9 e. NN
46 1nn 
 |-  1 e. NN
47 3 46 decnncl 
 |-  ; 1 1 e. NN
48 eqid 
 |-  ; 1 9 = ; 1 9
49 eqid 
 |-  ; 1 1 = ; 1 1
50 2cn 
 |-  2 e. CC
51 50 mullidi 
 |-  ( 1 x. 2 ) = 2
52 51 22 oveq12i 
 |-  ( ( 1 x. 2 ) + ( 1 + 1 ) ) = ( 2 + 2 )
53 2p2e4 
 |-  ( 2 + 2 ) = 4
54 52 53 eqtri 
 |-  ( ( 1 x. 2 ) + ( 1 + 1 ) ) = 4
55 8p1e9 
 |-  ( 8 + 1 ) = 9
56 9t2e18 
 |-  ( 9 x. 2 ) = ; 1 8
57 3 4 55 56 decsuc 
 |-  ( ( 9 x. 2 ) + 1 ) = ; 1 9
58 3 37 3 3 48 49 13 37 3 54 57 decmac 
 |-  ( ( ; 1 9 x. 2 ) + ; 1 1 ) = ; 4 9
59 1lt9 
 |-  1 < 9
60 3 3 44 59 declt 
 |-  ; 1 1 < ; 1 9
61 45 13 47 58 60 ndvdsi 
 |-  -. ; 1 9 || ; 4 9
62 19prm 
 |-  ; 1 9 e. Prime
63 coprm 
 |-  ( ( ; 1 9 e. Prime /\ ; 4 9 e. ZZ ) -> ( -. ; 1 9 || ; 4 9 <-> ( ; 1 9 gcd ; 4 9 ) = 1 ) )
64 62 40 63 mp2an 
 |-  ( -. ; 1 9 || ; 4 9 <-> ( ; 1 9 gcd ; 4 9 ) = 1 )
65 61 64 mpbi 
 |-  ( ; 1 9 gcd ; 4 9 ) = 1
66 43 65 eqtri 
 |-  ( ; 4 9 gcd ; 1 9 ) = 1
67 eqid 
 |-  ; 4 9 = ; 4 9
68 4cn 
 |-  4 e. CC
69 68 mullidi 
 |-  ( 1 x. 4 ) = 4
70 69 22 oveq12i 
 |-  ( ( 1 x. 4 ) + ( 1 + 1 ) ) = ( 4 + 2 )
71 4p2e6 
 |-  ( 4 + 2 ) = 6
72 70 71 eqtri 
 |-  ( ( 1 x. 4 ) + ( 1 + 1 ) ) = 6
73 9cn 
 |-  9 e. CC
74 73 mullidi 
 |-  ( 1 x. 9 ) = 9
75 74 oveq1i 
 |-  ( ( 1 x. 9 ) + 9 ) = ( 9 + 9 )
76 9p9e18 
 |-  ( 9 + 9 ) = ; 1 8
77 75 76 eqtri 
 |-  ( ( 1 x. 9 ) + 9 ) = ; 1 8
78 30 37 3 37 67 48 3 4 3 72 77 decma2c 
 |-  ( ( 1 x. ; 4 9 ) + ; 1 9 ) = ; 6 8
79 3 39 38 66 78 gcdi 
 |-  ( ; 6 8 gcd ; 4 9 ) = 1
80 eqid 
 |-  ; 6 8 = ; 6 8
81 6cn 
 |-  6 e. CC
82 81 mullidi 
 |-  ( 1 x. 6 ) = 6
83 4p1e5 
 |-  ( 4 + 1 ) = 5
84 82 83 oveq12i 
 |-  ( ( 1 x. 6 ) + ( 4 + 1 ) ) = ( 6 + 5 )
85 6p5e11 
 |-  ( 6 + 5 ) = ; 1 1
86 84 85 eqtri 
 |-  ( ( 1 x. 6 ) + ( 4 + 1 ) ) = ; 1 1
87 8cn 
 |-  8 e. CC
88 87 mullidi 
 |-  ( 1 x. 8 ) = 8
89 88 oveq1i 
 |-  ( ( 1 x. 8 ) + 9 ) = ( 8 + 9 )
90 9p8e17 
 |-  ( 9 + 8 ) = ; 1 7
91 73 87 90 addcomli 
 |-  ( 8 + 9 ) = ; 1 7
92 89 91 eqtri 
 |-  ( ( 1 x. 8 ) + 9 ) = ; 1 7
93 26 4 30 37 80 67 3 27 3 86 92 decma2c 
 |-  ( ( 1 x. ; 6 8 ) + ; 4 9 ) = ; ; 1 1 7
94 3 38 36 79 93 gcdi 
 |-  ( ; ; 1 1 7 gcd ; 6 8 ) = 1
95 eqid 
 |-  ; ; 1 1 7 = ; ; 1 1 7
96 6p1e7 
 |-  ( 6 + 1 ) = 7
97 27 dec0h 
 |-  7 = ; 0 7
98 96 97 eqtri 
 |-  ( 6 + 1 ) = ; 0 7
99 1t1e1 
 |-  ( 1 x. 1 ) = 1
100 00id 
 |-  ( 0 + 0 ) = 0
101 99 100 oveq12i 
 |-  ( ( 1 x. 1 ) + ( 0 + 0 ) ) = ( 1 + 0 )
102 ax-1cn 
 |-  1 e. CC
103 102 addridi 
 |-  ( 1 + 0 ) = 1
104 101 103 eqtri 
 |-  ( ( 1 x. 1 ) + ( 0 + 0 ) ) = 1
105 99 oveq1i 
 |-  ( ( 1 x. 1 ) + 7 ) = ( 1 + 7 )
106 7cn 
 |-  7 e. CC
107 7p1e8 
 |-  ( 7 + 1 ) = 8
108 106 102 107 addcomli 
 |-  ( 1 + 7 ) = 8
109 4 dec0h 
 |-  8 = ; 0 8
110 105 108 109 3eqtri 
 |-  ( ( 1 x. 1 ) + 7 ) = ; 0 8
111 3 3 16 27 49 98 3 4 16 104 110 decma2c 
 |-  ( ( 1 x. ; 1 1 ) + ( 6 + 1 ) ) = ; 1 8
112 106 mullidi 
 |-  ( 1 x. 7 ) = 7
113 112 oveq1i 
 |-  ( ( 1 x. 7 ) + 8 ) = ( 7 + 8 )
114 8p7e15 
 |-  ( 8 + 7 ) = ; 1 5
115 87 106 114 addcomli 
 |-  ( 7 + 8 ) = ; 1 5
116 113 115 eqtri 
 |-  ( ( 1 x. 7 ) + 8 ) = ; 1 5
117 34 27 26 4 95 80 3 14 3 111 116 decma2c 
 |-  ( ( 1 x. ; ; 1 1 7 ) + ; 6 8 ) = ; ; 1 8 5
118 3 36 35 94 117 gcdi 
 |-  ( ; ; 1 8 5 gcd ; ; 1 1 7 ) = 1
119 eqid 
 |-  ; ; 1 8 5 = ; ; 1 8 5
120 eqid 
 |-  ; 1 8 = ; 1 8
121 3 3 22 49 decsuc 
 |-  ( ; 1 1 + 1 ) = ; 1 2
122 2t1e2 
 |-  ( 2 x. 1 ) = 2
123 122 22 oveq12i 
 |-  ( ( 2 x. 1 ) + ( 1 + 1 ) ) = ( 2 + 2 )
124 123 53 eqtri 
 |-  ( ( 2 x. 1 ) + ( 1 + 1 ) ) = 4
125 8t2e16 
 |-  ( 8 x. 2 ) = ; 1 6
126 87 50 125 mulcomli 
 |-  ( 2 x. 8 ) = ; 1 6
127 6p2e8 
 |-  ( 6 + 2 ) = 8
128 3 26 13 126 127 decaddi 
 |-  ( ( 2 x. 8 ) + 2 ) = ; 1 8
129 3 4 3 13 120 121 13 4 3 124 128 decma2c 
 |-  ( ( 2 x. ; 1 8 ) + ( ; 1 1 + 1 ) ) = ; 4 8
130 5cn 
 |-  5 e. CC
131 5t2e10 
 |-  ( 5 x. 2 ) = ; 1 0
132 130 50 131 mulcomli 
 |-  ( 2 x. 5 ) = ; 1 0
133 106 addlidi 
 |-  ( 0 + 7 ) = 7
134 3 16 27 132 133 decaddi 
 |-  ( ( 2 x. 5 ) + 7 ) = ; 1 7
135 5 14 34 27 119 95 13 27 3 129 134 decma2c 
 |-  ( ( 2 x. ; ; 1 8 5 ) + ; ; 1 1 7 ) = ; ; 4 8 7
136 13 35 33 118 135 gcdi 
 |-  ( ; ; 4 8 7 gcd ; ; 1 8 5 ) = 1
137 eqid 
 |-  ; ; 4 8 7 = ; ; 4 8 7
138 eqid 
 |-  ; 4 8 = ; 4 8
139 3 4 55 120 decsuc 
 |-  ( ; 1 8 + 1 ) = ; 1 9
140 30 4 3 37 138 139 3 27 3 72 92 decma2c 
 |-  ( ( 1 x. ; 4 8 ) + ( ; 1 8 + 1 ) ) = ; 6 7
141 112 oveq1i 
 |-  ( ( 1 x. 7 ) + 5 ) = ( 7 + 5 )
142 7p5e12 
 |-  ( 7 + 5 ) = ; 1 2
143 141 142 eqtri 
 |-  ( ( 1 x. 7 ) + 5 ) = ; 1 2
144 31 27 5 14 137 119 3 13 3 140 143 decma2c 
 |-  ( ( 1 x. ; ; 4 8 7 ) + ; ; 1 8 5 ) = ; ; 6 7 2
145 3 33 32 136 144 gcdi 
 |-  ( ; ; 6 7 2 gcd ; ; 4 8 7 ) = 1
146 eqid 
 |-  ; ; 6 7 2 = ; ; 6 7 2
147 eqid 
 |-  ; 6 7 = ; 6 7
148 30 4 55 138 decsuc 
 |-  ( ; 4 8 + 1 ) = ; 4 9
149 71 oveq2i 
 |-  ( ( 2 x. 6 ) + ( 4 + 2 ) ) = ( ( 2 x. 6 ) + 6 )
150 6t2e12 
 |-  ( 6 x. 2 ) = ; 1 2
151 81 50 150 mulcomli 
 |-  ( 2 x. 6 ) = ; 1 2
152 81 50 127 addcomli 
 |-  ( 2 + 6 ) = 8
153 3 13 26 151 152 decaddi 
 |-  ( ( 2 x. 6 ) + 6 ) = ; 1 8
154 149 153 eqtri 
 |-  ( ( 2 x. 6 ) + ( 4 + 2 ) ) = ; 1 8
155 7t2e14 
 |-  ( 7 x. 2 ) = ; 1 4
156 106 50 155 mulcomli 
 |-  ( 2 x. 7 ) = ; 1 4
157 9p4e13 
 |-  ( 9 + 4 ) = ; 1 3
158 73 68 157 addcomli 
 |-  ( 4 + 9 ) = ; 1 3
159 3 30 37 156 22 10 158 decaddci 
 |-  ( ( 2 x. 7 ) + 9 ) = ; 2 3
160 26 27 30 37 147 148 13 10 13 154 159 decma2c 
 |-  ( ( 2 x. ; 6 7 ) + ( ; 4 8 + 1 ) ) = ; ; 1 8 3
161 2t2e4 
 |-  ( 2 x. 2 ) = 4
162 161 oveq1i 
 |-  ( ( 2 x. 2 ) + 7 ) = ( 4 + 7 )
163 7p4e11 
 |-  ( 7 + 4 ) = ; 1 1
164 106 68 163 addcomli 
 |-  ( 4 + 7 ) = ; 1 1
165 162 164 eqtri 
 |-  ( ( 2 x. 2 ) + 7 ) = ; 1 1
166 28 13 31 27 146 137 13 3 3 160 165 decma2c 
 |-  ( ( 2 x. ; ; 6 7 2 ) + ; ; 4 8 7 ) = ; ; ; 1 8 3 1
167 13 32 29 145 166 gcdi 
 |-  ( ; ; ; 1 8 3 1 gcd ; ; 6 7 2 ) = 1
168 eqid 
 |-  ; ; 1 8 3 = ; ; 1 8 3
169 28 nn0cni 
 |-  ; 6 7 e. CC
170 169 addridi 
 |-  ( ; 6 7 + 0 ) = ; 6 7
171 102 addlidi 
 |-  ( 0 + 1 ) = 1
172 99 171 oveq12i 
 |-  ( ( 1 x. 1 ) + ( 0 + 1 ) ) = ( 1 + 1 )
173 172 22 eqtri 
 |-  ( ( 1 x. 1 ) + ( 0 + 1 ) ) = 2
174 88 oveq1i 
 |-  ( ( 1 x. 8 ) + 7 ) = ( 8 + 7 )
175 174 114 eqtri 
 |-  ( ( 1 x. 8 ) + 7 ) = ; 1 5
176 3 4 16 27 120 98 3 14 3 173 175 decma2c 
 |-  ( ( 1 x. ; 1 8 ) + ( 6 + 1 ) ) = ; 2 5
177 3cn 
 |-  3 e. CC
178 177 mullidi 
 |-  ( 1 x. 3 ) = 3
179 178 oveq1i 
 |-  ( ( 1 x. 3 ) + 7 ) = ( 3 + 7 )
180 7p3e10 
 |-  ( 7 + 3 ) = ; 1 0
181 106 177 180 addcomli 
 |-  ( 3 + 7 ) = ; 1 0
182 179 181 eqtri 
 |-  ( ( 1 x. 3 ) + 7 ) = ; 1 0
183 5 10 26 27 168 170 3 16 3 176 182 decma2c 
 |-  ( ( 1 x. ; ; 1 8 3 ) + ( ; 6 7 + 0 ) ) = ; ; 2 5 0
184 99 oveq1i 
 |-  ( ( 1 x. 1 ) + 2 ) = ( 1 + 2 )
185 1p2e3 
 |-  ( 1 + 2 ) = 3
186 10 dec0h 
 |-  3 = ; 0 3
187 184 185 186 3eqtri 
 |-  ( ( 1 x. 1 ) + 2 ) = ; 0 3
188 11 3 28 13 23 146 3 10 16 183 187 decma2c 
 |-  ( ( 1 x. ; ; ; 1 8 3 1 ) + ; ; 6 7 2 ) = ; ; ; 2 5 0 3
189 188 1 eqtr4i 
 |-  ( ( 1 x. ; ; ; 1 8 3 1 ) + ; ; 6 7 2 ) = N
190 3 29 12 167 189 gcdi 
 |-  ( N gcd ; ; ; 1 8 3 1 ) = 1
191 9 12 20 25 190 gcdmodi 
 |-  ( ( ( 2 ^ ; 1 8 ) - 1 ) gcd N ) = 1