# 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 = 1259$
Assertion 1259lem5 $⊢ 2 34 − 1 gcd N = 1$

### Proof

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