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 mulridi 
 |-  ( 1 x. 1 ) = 1
47 45 addlidi 
 |-  ( 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 mulridi 
 |-  ( 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 mullidi 
 |-  ( 1 x. 2 ) = 2
71 45 addridi 
 |-  ( 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 2t3e6 
 |-  ( 2 x. 3 ) = 6
84 69 addridi 
 |-  ( 2 + 0 ) = 2
85 83 84 oveq12i 
 |-  ( ( 2 x. 3 ) + ( 2 + 0 ) ) = ( 6 + 2 )
86 6p2e8 
 |-  ( 6 + 2 ) = 8
87 85 86 eqtri 
 |-  ( ( 2 x. 3 ) + ( 2 + 0 ) ) = 8
88 4cn 
 |-  4 e. CC
89 4t2e8 
 |-  ( 4 x. 2 ) = 8
90 88 69 89 mulcomli 
 |-  ( 2 x. 4 ) = 8
91 90 oveq1i 
 |-  ( ( 2 x. 4 ) + 1 ) = ( 8 + 1 )
92 8p1e9 
 |-  ( 8 + 1 ) = 9
93 13 dec0h 
 |-  9 = ; 0 9
94 91 92 93 3eqtri 
 |-  ( ( 2 x. 4 ) + 1 ) = ; 0 9
95 3 4 16 15 82 68 16 13 31 87 94 decma2c 
 |-  ( ( 2 x. ; 3 4 ) + ; 2 1 ) = ; 8 9
96 16 34 5 81 95 gcdi 
 |-  ( ; 8 9 gcd ; 3 4 ) = 1
97 eqid 
 |-  ; 8 9 = ; 8 9
98 4p3e7 
 |-  ( 4 + 3 ) = 7
99 88 51 98 addcomli 
 |-  ( 3 + 4 ) = 7
100 99 oveq2i 
 |-  ( ( 4 x. 8 ) + ( 3 + 4 ) ) = ( ( 4 x. 8 ) + 7 )
101 7nn0 
 |-  7 e. NN0
102 8t4e32 
 |-  ( 8 x. 4 ) = ; 3 2
103 54 88 102 mulcomli 
 |-  ( 4 x. 8 ) = ; 3 2
104 7cn 
 |-  7 e. CC
105 7p2e9 
 |-  ( 7 + 2 ) = 9
106 104 69 105 addcomli 
 |-  ( 2 + 7 ) = 9
107 3 16 101 103 106 decaddi 
 |-  ( ( 4 x. 8 ) + 7 ) = ; 3 9
108 100 107 eqtri 
 |-  ( ( 4 x. 8 ) + ( 3 + 4 ) ) = ; 3 9
109 9cn 
 |-  9 e. CC
110 9t4e36 
 |-  ( 9 x. 4 ) = ; 3 6
111 109 88 110 mulcomli 
 |-  ( 4 x. 9 ) = ; 3 6
112 6p4e10 
 |-  ( 6 + 4 ) = ; 1 0
113 3 11 4 111 76 112 decaddci2 
 |-  ( ( 4 x. 9 ) + 4 ) = ; 4 0
114 10 13 3 4 97 82 4 31 4 108 113 decma2c 
 |-  ( ( 4 x. ; 8 9 ) + ; 3 4 ) = ; ; 3 9 0
115 4 5 33 96 114 gcdi 
 |-  ( ; ; 3 9 0 gcd ; 8 9 ) = 1
116 eqid 
 |-  ; ; 3 9 0 = ; ; 3 9 0
117 eqid 
 |-  ; 3 9 = ; 3 9
118 54 addridi 
 |-  ( 8 + 0 ) = 8
119 118 44 eqtri 
 |-  ( 8 + 0 ) = ; 0 8
120 69 addlidi 
 |-  ( 0 + 2 ) = 2
121 83 120 oveq12i 
 |-  ( ( 2 x. 3 ) + ( 0 + 2 ) ) = ( 6 + 2 )
122 121 86 eqtri 
 |-  ( ( 2 x. 3 ) + ( 0 + 2 ) ) = 8
123 9t2e18 
 |-  ( 9 x. 2 ) = ; 1 8
124 109 69 123 mulcomli 
 |-  ( 2 x. 9 ) = ; 1 8
125 8p8e16 
 |-  ( 8 + 8 ) = ; 1 6
126 15 10 10 124 49 11 125 decaddci 
 |-  ( ( 2 x. 9 ) + 8 ) = ; 2 6
127 3 13 31 10 117 119 16 11 16 122 126 decma2c 
 |-  ( ( 2 x. ; 3 9 ) + ( 8 + 0 ) ) = ; 8 6
128 2t0e0 
 |-  ( 2 x. 0 ) = 0
129 128 oveq1i 
 |-  ( ( 2 x. 0 ) + 9 ) = ( 0 + 9 )
130 109 addlidi 
 |-  ( 0 + 9 ) = 9
131 129 130 93 3eqtri 
 |-  ( ( 2 x. 0 ) + 9 ) = ; 0 9
132 30 31 10 13 116 97 16 13 31 127 131 decma2c 
 |-  ( ( 2 x. ; ; 3 9 0 ) + ; 8 9 ) = ; ; 8 6 9
133 16 33 32 115 132 gcdi 
 |-  ( ; ; 8 6 9 gcd ; ; 3 9 0 ) = 1
134 30 nn0cni 
 |-  ; 3 9 e. CC
135 134 addridi 
 |-  ( ; 3 9 + 0 ) = ; 3 9
136 54 mullidi 
 |-  ( 1 x. 8 ) = 8
137 136 76 oveq12i 
 |-  ( ( 1 x. 8 ) + ( 3 + 1 ) ) = ( 8 + 4 )
138 8p4e12 
 |-  ( 8 + 4 ) = ; 1 2
139 137 138 eqtri 
 |-  ( ( 1 x. 8 ) + ( 3 + 1 ) ) = ; 1 2
140 6cn 
 |-  6 e. CC
141 140 mullidi 
 |-  ( 1 x. 6 ) = 6
142 141 oveq1i 
 |-  ( ( 1 x. 6 ) + 9 ) = ( 6 + 9 )
143 9p6e15 
 |-  ( 9 + 6 ) = ; 1 5
144 109 140 143 addcomli 
 |-  ( 6 + 9 ) = ; 1 5
145 142 144 eqtri 
 |-  ( ( 1 x. 6 ) + 9 ) = ; 1 5
146 10 11 3 13 25 135 15 18 15 139 145 decma2c 
 |-  ( ( 1 x. ; 8 6 ) + ( ; 3 9 + 0 ) ) = ; ; 1 2 5
147 109 mullidi 
 |-  ( 1 x. 9 ) = 9
148 147 oveq1i 
 |-  ( ( 1 x. 9 ) + 0 ) = ( 9 + 0 )
149 109 addridi 
 |-  ( 9 + 0 ) = 9
150 148 149 93 3eqtri 
 |-  ( ( 1 x. 9 ) + 0 ) = ; 0 9
151 12 13 30 31 27 116 15 13 31 146 150 decma2c 
 |-  ( ( 1 x. ; ; 8 6 9 ) + ; ; 3 9 0 ) = ; ; ; 1 2 5 9
152 151 1 eqtr4i 
 |-  ( ( 1 x. ; ; 8 6 9 ) + ; ; 3 9 0 ) = N
153 15 32 14 133 152 gcdi 
 |-  ( N gcd ; ; 8 6 9 ) = 1
154 9 14 22 29 153 gcdmodi 
 |-  ( ( ( 2 ^ ; 3 4 ) - 1 ) gcd N ) = 1