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