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 ⊢ 𝑁 = 1 2 5 9
Assertion 1259lem5 ( ( ( 2 ↑ 3 4 ) − 1 ) gcd 𝑁 ) = 1

Proof

Step Hyp Ref Expression
1 1259prm.1 ⊢ 𝑁 = 1 2 5 9
2 2nn ⊢ 2 ∈ ℕ
3 3nn0 ⊢ 3 ∈ ℕ0
4 4nn0 ⊢ 4 ∈ ℕ0
5 3 4 deccl ⊢ 3 4 ∈ ℕ0
6 nnexpcl ⊢ ( ( 2 ∈ ℕ ∧ 3 4 ∈ ℕ0 ) → ( 2 ↑ 3 4 ) ∈ ℕ )
7 2 5 6 mp2an ⊢ ( 2 ↑ 3 4 ) ∈ ℕ
8 nnm1nn0 ⊢ ( ( 2 ↑ 3 4 ) ∈ ℕ → ( ( 2 ↑ 3 4 ) − 1 ) ∈ ℕ0 )
9 7 8 ax-mp ⊢ ( ( 2 ↑ 3 4 ) − 1 ) ∈ ℕ0
10 8nn0 ⊢ 8 ∈ ℕ0
11 6nn0 ⊢ 6 ∈ ℕ0
12 10 11 deccl ⊢ 8 6 ∈ ℕ0
13 9nn0 ⊢ 9 ∈ ℕ0
14 12 13 deccl ⊢ 8 6 9 ∈ ℕ0
15 1nn0 ⊢ 1 ∈ ℕ0
16 2nn0 ⊢ 2 ∈ ℕ0
17 15 16 deccl ⊢ 1 2 ∈ ℕ0
18 5nn0 ⊢ 5 ∈ ℕ0
19 17 18 deccl ⊢ 1 2 5 ∈ ℕ0
20 9nn ⊢ 9 ∈ ℕ
21 19 20 decnncl ⊢ 1 2 5 9 ∈ ℕ
22 1 21 eqeltri ⊢ 𝑁 ∈ ℕ
23 1 1259lem2 ⊢ ( ( 2 ↑ 3 4 ) mod 𝑁 ) = ( 8 7 0 mod 𝑁 )
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 𝑁 ) = ( 8 6 9 mod 𝑁 )
30 3 13 deccl ⊢ 3 9 ∈ ℕ0
31 0nn0 ⊢ 0 ∈ ℕ0
32 30 31 deccl ⊢ 3 9 0 ∈ ℕ0
33 10 13 deccl ⊢ 8 9 ∈ ℕ0
34 16 15 deccl ⊢ 2 1 ∈ ℕ0
35 15 3 deccl ⊢ 1 3 ∈ ℕ0
36 34 nn0zi ⊢ 2 1 ∈ ℤ
37 35 nn0zi ⊢ 1 3 ∈ ℤ
38 gcdcom ⊢ ( ( 2 1 ∈ ℤ ∧ 1 3 ∈ ℤ ) → ( 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 ∈ ℕ
41 15 40 decnncl ⊢ 1 3 ∈ ℕ
42 8nn ⊢ 8 ∈ ℕ
43 eqid ⊢ 1 3 = 1 3
44 10 dec0h ⊢ 8 = 0 8
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 ) = 1 1
56 54 51 55 addcomli ⊢ ( 3 + 8 ) = 1 1
57 53 56 eqtri ⊢ ( ( 3 · 1 ) + 8 ) = 1 1
58 15 3 31 10 43 44 15 15 15 50 57 decmac ⊢ ( ( 1 3 · 1 ) + 8 ) = 2 1
59 1nn ⊢ 1 ∈ ℕ
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 ∈ ℙ
64 coprm ⊢ ( ( 1 3 ∈ ℙ ∧ 2 1 ∈ ℤ ) → ( ¬ 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 ∈ ℂ
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 = 0 4
79 75 77 78 3eqtri ⊢ ( ( 1 · 1 ) + 3 ) = 0 4
80 16 15 15 3 68 43 15 4 31 74 79 decma2c ⊢ ( ( 1 · 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 · 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 = 0 9
95 92 93 94 3eqtri ⊢ ( ( 2 · 4 ) + 1 ) = 0 9
96 3 4 16 15 82 68 16 13 31 88 95 decma2c ⊢ ( ( 2 · 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 · 8 ) + ( 3 + 4 ) ) = ( ( 4 · 8 ) + 7 )
102 7nn0 ⊢ 7 ∈ ℕ0
103 8t4e32 ⊢ ( 8 · 4 ) = 3 2
104 54 89 103 mulcomli ⊢ ( 4 · 8 ) = 3 2
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 ) = 3 9
109 101 108 eqtri ⊢ ( ( 4 · 8 ) + ( 3 + 4 ) ) = 3 9
110 9cn ⊢ 9 ∈ ℂ
111 9t4e36 ⊢ ( 9 · 4 ) = 3 6
112 110 89 111 mulcomli ⊢ ( 4 · 9 ) = 3 6
113 6p4e10 ⊢ ( 6 + 4 ) = 1 0
114 3 11 4 112 76 113 decaddci2 ⊢ ( ( 4 · 9 ) + 4 ) = 4 0
115 10 13 3 4 98 82 4 31 4 109 114 decma2c ⊢ ( ( 4 · 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 addridi ⊢ ( 8 + 0 ) = 8
120 119 44 eqtri ⊢ ( 8 + 0 ) = 0 8
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 ) = 1 8
125 110 69 124 mulcomli ⊢ ( 2 · 9 ) = 1 8
126 8p8e16 ⊢ ( 8 + 8 ) = 1 6
127 15 10 10 125 49 11 126 decaddci ⊢ ( ( 2 · 9 ) + 8 ) = 2 6
128 3 13 31 10 118 120 16 11 16 123 127 decma2c ⊢ ( ( 2 · 3 9 ) + ( 8 + 0 ) ) = 8 6
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 ) = 0 9
133 30 31 10 13 117 98 16 13 31 128 132 decma2c ⊢ ( ( 2 · 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 ∈ ℂ
136 135 addridi ⊢ ( 3 9 + 0 ) = 3 9
137 54 mullidi ⊢ ( 1 · 8 ) = 8
138 137 76 oveq12i ⊢ ( ( 1 · 8 ) + ( 3 + 1 ) ) = ( 8 + 4 )
139 8p4e12 ⊢ ( 8 + 4 ) = 1 2
140 138 139 eqtri ⊢ ( ( 1 · 8 ) + ( 3 + 1 ) ) = 1 2
141 6cn ⊢ 6 ∈ ℂ
142 141 mullidi ⊢ ( 1 · 6 ) = 6
143 142 oveq1i ⊢ ( ( 1 · 6 ) + 9 ) = ( 6 + 9 )
144 9p6e15 ⊢ ( 9 + 6 ) = 1 5
145 110 141 144 addcomli ⊢ ( 6 + 9 ) = 1 5
146 143 145 eqtri ⊢ ( ( 1 · 6 ) + 9 ) = 1 5
147 10 11 3 13 25 136 15 18 15 140 146 decma2c ⊢ ( ( 1 · 8 6 ) + ( 3 9 + 0 ) ) = 1 2 5
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 ) = 0 9
152 12 13 30 31 27 117 15 13 31 147 151 decma2c ⊢ ( ( 1 · 8 6 9 ) + 3 9 0 ) = 1 2 5 9
153 152 1 eqtr4i ⊢ ( ( 1 · 8 6 9 ) + 3 9 0 ) = 𝑁
154 15 32 14 134 153 gcdi ⊢ ( 𝑁 gcd 8 6 9 ) = 1
155 9 14 22 29 154 gcdmodi ⊢ ( ( ( 2 ↑ 3 4 ) − 1 ) gcd 𝑁 ) = 1