This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 mulridi ⊢ 1 ⋅ 1 = 1
47 45 addlidi ⊢ 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 mulridi ⊢ 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 mullidi ⊢ 1 ⋅ 2 = 2
71 45 addridi ⊢ 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 addridi ⊢ 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 addridi ⊢ 8 + 0 = 8
120 119 44 eqtri ⊢ 8 + 0 = 08
121 69 addlidi ⊢ 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 addlidi ⊢ 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 addridi ⊢ 39 + 0 = 39
137 54 mullidi ⊢ 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 mullidi ⊢ 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 mullidi ⊢ 1 ⋅ 9 = 9
149 148 oveq1i ⊢ 1 ⋅ 9 + 0 = 9 + 0
150 110 addridi ⊢ 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