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
|
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 ) = ; 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
|
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 = ; 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
|
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 = ; 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
|
addid1i |
⊢ ( 8 + 0 ) = 8 |
120 |
119 44
|
eqtri |
⊢ ( 8 + 0 ) = ; 0 8 |
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 ) = ; 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
|
addid2i |
⊢ ( 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
|
addid1i |
⊢ ( ; 3 9 + 0 ) = ; 3 9 |
137 |
54
|
mulid2i |
⊢ ( 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
|
mulid2i |
⊢ ( 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
|
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 ) = ; 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 |