Metamath Proof Explorer

Theorem 1259lem5

Description: Lemma for 1259prm . Calculate the GCD of 2 ^ 3 4 - 1 == 8 6 9 with N = 1 2 5 9 . (Contributed by Mario Carneiro, 22-Feb-2014) (Revised by Mario Carneiro, 20-Apr-2015)

Ref Expression
Hypothesis 1259prm.1 
|- N = ; ; ; 1 2 5 9
Assertion 1259lem5 
|- ( ( ( 2 ^ ; 3 4 ) - 1 ) gcd N ) = 1

Proof

Step Hyp Ref Expression
1 1259prm.1 
 |-  N = ; ; ; 1 2 5 9
2 2nn 
 |-  2 e. NN
3 3nn0 
 |-  3 e. NN0
4 4nn0 
 |-  4 e. NN0
5 3 4 deccl 
 |-  ; 3 4 e. NN0
6 nnexpcl 
 |-  ( ( 2 e. NN /\ ; 3 4 e. NN0 ) -> ( 2 ^ ; 3 4 ) e. NN )
7 2 5 6 mp2an 
 |-  ( 2 ^ ; 3 4 ) e. NN
8 nnm1nn0 
 |-  ( ( 2 ^ ; 3 4 ) e. NN -> ( ( 2 ^ ; 3 4 ) - 1 ) e. NN0 )
9 7 8 ax-mp 
 |-  ( ( 2 ^ ; 3 4 ) - 1 ) e. NN0
10 8nn0 
 |-  8 e. NN0
11 6nn0 
 |-  6 e. NN0
12 10 11 deccl 
 |-  ; 8 6 e. NN0
13 9nn0 
 |-  9 e. NN0
14 12 13 deccl 
 |-  ; ; 8 6 9 e. NN0
15 1nn0 
 |-  1 e. NN0
16 2nn0 
 |-  2 e. NN0
17 15 16 deccl 
 |-  ; 1 2 e. NN0
18 5nn0 
 |-  5 e. NN0
19 17 18 deccl 
 |-  ; ; 1 2 5 e. NN0
20 9nn 
 |-  9 e. NN
21 19 20 decnncl 
 |-  ; ; ; 1 2 5 9 e. NN
22 1 21 eqeltri 
 |-  N e. NN
23 1 1259lem2 
 |-  ( ( 2 ^ ; 3 4 ) mod N ) = ( ; ; 8 7 0 mod N )
24 6p1e7 
 |-  ( 6 + 1 ) = 7
25 eqid 
 |-  ; 8 6 = ; 8 6
26 10 11 24 25 decsuc 
 |-  ( ; 8 6 + 1 ) = ; 8 7
27 eqid 
 |-  ; ; 8 6 9 = ; ; 8 6 9
28 12 26 27 decsucc 
 |-  ( ; ; 8 6 9 + 1 ) = ; ; 8 7 0
29 22 7 15 14 23 28 modsubi 
 |-  ( ( ( 2 ^ ; 3 4 ) - 1 ) mod N ) = ( ; ; 8 6 9 mod N )
30 3 13 deccl 
 |-  ; 3 9 e. NN0
31 0nn0 
 |-  0 e. NN0
32 30 31 deccl 
 |-  ; ; 3 9 0 e. NN0
33 10 13 deccl 
 |-  ; 8 9 e. NN0
34 16 15 deccl 
 |-  ; 2 1 e. NN0
35 15 3 deccl 
 |-  ; 1 3 e. NN0
36 34 nn0zi 
 |-  ; 2 1 e. ZZ
37 35 nn0zi 
 |-  ; 1 3 e. ZZ
38 gcdcom 
 |-  ( ( ; 2 1 e. ZZ /\ ; 1 3 e. ZZ ) -> ( ; 2 1 gcd ; 1 3 ) = ( ; 1 3 gcd ; 2 1 ) )
39 36 37 38 mp2an 
 |-  ( ; 2 1 gcd ; 1 3 ) = ( ; 1 3 gcd ; 2 1 )
40 3nn 
 |-  3 e. NN
41 15 40 decnncl 
 |-  ; 1 3 e. NN
42 8nn 
 |-  8 e. NN
43 eqid 
 |-  ; 1 3 = ; 1 3
44 10 dec0h 
 |-  8 = ; 0 8
45 ax-1cn 
 |-  1 e. CC
46 45 mulid1i 
 |-  ( 1 x. 1 ) = 1
47 45 addid2i 
 |-  ( 0 + 1 ) = 1
48 46 47 oveq12i 
 |-  ( ( 1 x. 1 ) + ( 0 + 1 ) ) = ( 1 + 1 )
49 1p1e2 
 |-  ( 1 + 1 ) = 2
50 48 49 eqtri 
 |-  ( ( 1 x. 1 ) + ( 0 + 1 ) ) = 2
51 3cn 
 |-  3 e. CC
52 51 mulid1i 
 |-  ( 3 x. 1 ) = 3
53 52 oveq1i 
 |-  ( ( 3 x. 1 ) + 8 ) = ( 3 + 8 )
54 8cn 
 |-  8 e. CC
55 8p3e11 
 |-  ( 8 + 3 ) = ; 1 1
56 54 51 55 addcomli 
 |-  ( 3 + 8 ) = ; 1 1
57 53 56 eqtri 
 |-  ( ( 3 x. 1 ) + 8 ) = ; 1 1
58 15 3 31 10 43 44 15 15 15 50 57 decmac 
 |-  ( ( ; 1 3 x. 1 ) + 8 ) = ; 2 1
59 1nn 
 |-  1 e. NN
60 8lt10 
 |-  8 < ; 1 0
61 59 3 10 60 declti 
 |-  8 < ; 1 3
62 41 15 42 58 61 ndvdsi 
 |-  -. ; 1 3 || ; 2 1
63 13prm 
 |-  ; 1 3 e. Prime
64 coprm 
 |-  ( ( ; 1 3 e. Prime /\ ; 2 1 e. ZZ ) -> ( -. ; 1 3 || ; 2 1 <-> ( ; 1 3 gcd ; 2 1 ) = 1 ) )
65 63 36 64 mp2an 
 |-  ( -. ; 1 3 || ; 2 1 <-> ( ; 1 3 gcd ; 2 1 ) = 1 )
66 62 65 mpbi 
 |-  ( ; 1 3 gcd ; 2 1 ) = 1
67 39 66 eqtri 
 |-  ( ; 2 1 gcd ; 1 3 ) = 1
68 eqid 
 |-  ; 2 1 = ; 2 1
69 2cn 
 |-  2 e. CC
70 69 mulid2i 
 |-  ( 1 x. 2 ) = 2
71 45 addid1i 
 |-  ( 1 + 0 ) = 1
72 70 71 oveq12i 
 |-  ( ( 1 x. 2 ) + ( 1 + 0 ) ) = ( 2 + 1 )
73 2p1e3 
 |-  ( 2 + 1 ) = 3
74 72 73 eqtri 
 |-  ( ( 1 x. 2 ) + ( 1 + 0 ) ) = 3
75 46 oveq1i 
 |-  ( ( 1 x. 1 ) + 3 ) = ( 1 + 3 )
76 3p1e4 
 |-  ( 3 + 1 ) = 4
77 51 45 76 addcomli 
 |-  ( 1 + 3 ) = 4
78 4 dec0h 
 |-  4 = ; 0 4
79 75 77 78 3eqtri 
 |-  ( ( 1 x. 1 ) + 3 ) = ; 0 4
80 16 15 15 3 68 43 15 4 31 74 79 decma2c 
 |-  ( ( 1 x. ; 2 1 ) + ; 1 3 ) = ; 3 4
81 15 35 34 67 80 gcdi 
 |-  ( ; 3 4 gcd ; 2 1 ) = 1
82 eqid 
 |-  ; 3 4 = ; 3 4
83 3t2e6 
 |-  ( 3 x. 2 ) = 6
84 51 69 83 mulcomli 
 |-  ( 2 x. 3 ) = 6
85 69 addid1i 
 |-  ( 2 + 0 ) = 2
86 84 85 oveq12i 
 |-  ( ( 2 x. 3 ) + ( 2 + 0 ) ) = ( 6 + 2 )
87 6p2e8 
 |-  ( 6 + 2 ) = 8
88 86 87 eqtri 
 |-  ( ( 2 x. 3 ) + ( 2 + 0 ) ) = 8
89 4cn 
 |-  4 e. CC
90 4t2e8 
 |-  ( 4 x. 2 ) = 8
91 89 69 90 mulcomli 
 |-  ( 2 x. 4 ) = 8
92 91 oveq1i 
 |-  ( ( 2 x. 4 ) + 1 ) = ( 8 + 1 )
93 8p1e9 
 |-  ( 8 + 1 ) = 9
94 13 dec0h 
 |-  9 = ; 0 9
95 92 93 94 3eqtri 
 |-  ( ( 2 x. 4 ) + 1 ) = ; 0 9
96 3 4 16 15 82 68 16 13 31 88 95 decma2c 
 |-  ( ( 2 x. ; 3 4 ) + ; 2 1 ) = ; 8 9
97 16 34 5 81 96 gcdi 
 |-  ( ; 8 9 gcd ; 3 4 ) = 1
98 eqid 
 |-  ; 8 9 = ; 8 9
99 4p3e7 
 |-  ( 4 + 3 ) = 7
100 89 51 99 addcomli 
 |-  ( 3 + 4 ) = 7
101 100 oveq2i 
 |-  ( ( 4 x. 8 ) + ( 3 + 4 ) ) = ( ( 4 x. 8 ) + 7 )
102 7nn0 
 |-  7 e. NN0
103 8t4e32 
 |-  ( 8 x. 4 ) = ; 3 2
104 54 89 103 mulcomli 
 |-  ( 4 x. 8 ) = ; 3 2
105 7cn 
 |-  7 e. CC
106 7p2e9 
 |-  ( 7 + 2 ) = 9
107 105 69 106 addcomli 
 |-  ( 2 + 7 ) = 9
108 3 16 102 104 107 decaddi 
 |-  ( ( 4 x. 8 ) + 7 ) = ; 3 9
109 101 108 eqtri 
 |-  ( ( 4 x. 8 ) + ( 3 + 4 ) ) = ; 3 9
110 9cn 
 |-  9 e. CC
111 9t4e36 
 |-  ( 9 x. 4 ) = ; 3 6
112 110 89 111 mulcomli 
 |-  ( 4 x. 9 ) = ; 3 6
113 6p4e10 
 |-  ( 6 + 4 ) = ; 1 0
114 3 11 4 112 76 113 decaddci2 
 |-  ( ( 4 x. 9 ) + 4 ) = ; 4 0
115 10 13 3 4 98 82 4 31 4 109 114 decma2c 
 |-  ( ( 4 x. ; 8 9 ) + ; 3 4 ) = ; ; 3 9 0
116 4 5 33 97 115 gcdi 
 |-  ( ; ; 3 9 0 gcd ; 8 9 ) = 1
117 eqid 
 |-  ; ; 3 9 0 = ; ; 3 9 0
118 eqid 
 |-  ; 3 9 = ; 3 9
119 54 addid1i 
 |-  ( 8 + 0 ) = 8
120 119 44 eqtri 
 |-  ( 8 + 0 ) = ; 0 8
121 69 addid2i 
 |-  ( 0 + 2 ) = 2
122 84 121 oveq12i 
 |-  ( ( 2 x. 3 ) + ( 0 + 2 ) ) = ( 6 + 2 )
123 122 87 eqtri 
 |-  ( ( 2 x. 3 ) + ( 0 + 2 ) ) = 8
124 9t2e18 
 |-  ( 9 x. 2 ) = ; 1 8
125 110 69 124 mulcomli 
 |-  ( 2 x. 9 ) = ; 1 8
126 8p8e16 
 |-  ( 8 + 8 ) = ; 1 6
127 15 10 10 125 49 11 126 decaddci 
 |-  ( ( 2 x. 9 ) + 8 ) = ; 2 6
128 3 13 31 10 118 120 16 11 16 123 127 decma2c 
 |-  ( ( 2 x. ; 3 9 ) + ( 8 + 0 ) ) = ; 8 6
129 2t0e0 
 |-  ( 2 x. 0 ) = 0
130 129 oveq1i 
 |-  ( ( 2 x. 0 ) + 9 ) = ( 0 + 9 )
131 110 addid2i 
 |-  ( 0 + 9 ) = 9
132 130 131 94 3eqtri 
 |-  ( ( 2 x. 0 ) + 9 ) = ; 0 9
133 30 31 10 13 117 98 16 13 31 128 132 decma2c 
 |-  ( ( 2 x. ; ; 3 9 0 ) + ; 8 9 ) = ; ; 8 6 9
134 16 33 32 116 133 gcdi 
 |-  ( ; ; 8 6 9 gcd ; ; 3 9 0 ) = 1
135 30 nn0cni 
 |-  ; 3 9 e. CC
136 135 addid1i 
 |-  ( ; 3 9 + 0 ) = ; 3 9
137 54 mulid2i 
 |-  ( 1 x. 8 ) = 8
138 137 76 oveq12i 
 |-  ( ( 1 x. 8 ) + ( 3 + 1 ) ) = ( 8 + 4 )
139 8p4e12 
 |-  ( 8 + 4 ) = ; 1 2
140 138 139 eqtri 
 |-  ( ( 1 x. 8 ) + ( 3 + 1 ) ) = ; 1 2
141 6cn 
 |-  6 e. CC
142 141 mulid2i 
 |-  ( 1 x. 6 ) = 6
143 142 oveq1i 
 |-  ( ( 1 x. 6 ) + 9 ) = ( 6 + 9 )
144 9p6e15 
 |-  ( 9 + 6 ) = ; 1 5
145 110 141 144 addcomli 
 |-  ( 6 + 9 ) = ; 1 5
146 143 145 eqtri 
 |-  ( ( 1 x. 6 ) + 9 ) = ; 1 5
147 10 11 3 13 25 136 15 18 15 140 146 decma2c 
 |-  ( ( 1 x. ; 8 6 ) + ( ; 3 9 + 0 ) ) = ; ; 1 2 5
148 110 mulid2i 
 |-  ( 1 x. 9 ) = 9
149 148 oveq1i 
 |-  ( ( 1 x. 9 ) + 0 ) = ( 9 + 0 )
150 110 addid1i 
 |-  ( 9 + 0 ) = 9
151 149 150 94 3eqtri 
 |-  ( ( 1 x. 9 ) + 0 ) = ; 0 9
152 12 13 30 31 27 117 15 13 31 147 151 decma2c 
 |-  ( ( 1 x. ; ; 8 6 9 ) + ; ; 3 9 0 ) = ; ; ; 1 2 5 9
153 152 1 eqtr4i 
 |-  ( ( 1 x. ; ; 8 6 9 ) + ; ; 3 9 0 ) = N
154 15 32 14 134 153 gcdi 
 |-  ( N gcd ; ; 8 6 9 ) = 1
155 9 14 22 29 154 gcdmodi 
 |-  ( ( ( 2 ^ ; 3 4 ) - 1 ) gcd N ) = 1