Metamath Proof Explorer

Theorem 4001lem3

Description: Lemma for 4001prm . Calculate a power mod. In decimal, we calculate 2 ^ 1 0 0 0 = 2 ^ 8 0 0 x. 2 ^ 2 0 0 == 2 3 1 1 x. 9 0 2 = 5 2 1 N + 1 and finally 2 ^ ( N - 1 ) = ( 2 ^ 1 0 0 0 ) ^ 4 == 1 ^ 4 = 1 . (Contributed by Mario Carneiro, 3-Mar-2014) (Revised by Mario Carneiro, 20-Apr-2015) (Proof shortened by AV, 16-Sep-2021)

Ref Expression
Hypothesis 4001prm.1 
|- N = ; ; ; 4 0 0 1
Assertion 4001lem3 
|- ( ( 2 ^ ( N - 1 ) ) mod N ) = ( 1 mod N )

Proof

Step Hyp Ref Expression
1 4001prm.1 
 |-  N = ; ; ; 4 0 0 1
2 4nn0 
 |-  4 e. NN0
3 0nn0 
 |-  0 e. NN0
4 2 3 deccl 
 |-  ; 4 0 e. NN0
5 4 3 deccl 
 |-  ; ; 4 0 0 e. NN0
6 1nn 
 |-  1 e. NN
7 5 6 decnncl 
 |-  ; ; ; 4 0 0 1 e. NN
8 1 7 eqeltri 
 |-  N e. NN
9 2nn 
 |-  2 e. NN
10 2nn0 
 |-  2 e. NN0
11 10 3 deccl 
 |-  ; 2 0 e. NN0
12 11 3 deccl 
 |-  ; ; 2 0 0 e. NN0
13 12 3 deccl 
 |-  ; ; ; 2 0 0 0 e. NN0
14 0z 
 |-  0 e. ZZ
15 1nn0 
 |-  1 e. NN0
16 10nn0 
 |-  ; 1 0 e. NN0
17 16 3 deccl 
 |-  ; ; 1 0 0 e. NN0
18 17 3 deccl 
 |-  ; ; ; 1 0 0 0 e. NN0
19 8nn0 
 |-  8 e. NN0
20 19 3 deccl 
 |-  ; 8 0 e. NN0
21 20 3 deccl 
 |-  ; ; 8 0 0 e. NN0
22 5nn0 
 |-  5 e. NN0
23 22 10 deccl 
 |-  ; 5 2 e. NN0
24 23 15 deccl 
 |-  ; ; 5 2 1 e. NN0
25 24 nn0zi 
 |-  ; ; 5 2 1 e. ZZ
26 3nn0 
 |-  3 e. NN0
27 10 26 deccl 
 |-  ; 2 3 e. NN0
28 27 15 deccl 
 |-  ; ; 2 3 1 e. NN0
29 28 15 deccl 
 |-  ; ; ; 2 3 1 1 e. NN0
30 9nn0 
 |-  9 e. NN0
31 30 3 deccl 
 |-  ; 9 0 e. NN0
32 31 10 deccl 
 |-  ; ; 9 0 2 e. NN0
33 1 4001lem2 
 |-  ( ( 2 ^ ; ; 8 0 0 ) mod N ) = ( ; ; ; 2 3 1 1 mod N )
34 1 4001lem1 
 |-  ( ( 2 ^ ; ; 2 0 0 ) mod N ) = ( ; ; 9 0 2 mod N )
35 eqid 
 |-  ; ; 8 0 0 = ; ; 8 0 0
36 eqid 
 |-  ; ; 2 0 0 = ; ; 2 0 0
37 eqid 
 |-  ; 8 0 = ; 8 0
38 eqid 
 |-  ; 2 0 = ; 2 0
39 8p2e10 
 |-  ( 8 + 2 ) = ; 1 0
40 00id 
 |-  ( 0 + 0 ) = 0
41 19 3 10 3 37 38 39 40 decadd 
 |-  ( ; 8 0 + ; 2 0 ) = ; ; 1 0 0
42 20 3 11 3 35 36 41 40 decadd 
 |-  ( ; ; 8 0 0 + ; ; 2 0 0 ) = ; ; ; 1 0 0 0
43 15 dec0h 
 |-  1 = ; 0 1
44 eqid 
 |-  ; ; 4 0 0 = ; ; 4 0 0
45 23 nn0cni 
 |-  ; 5 2 e. CC
46 45 addlidi 
 |-  ( 0 + ; 5 2 ) = ; 5 2
47 eqid 
 |-  ; 4 0 = ; 4 0
48 5cn 
 |-  5 e. CC
49 48 addridi 
 |-  ( 5 + 0 ) = 5
50 22 dec0h 
 |-  5 = ; 0 5
51 49 50 eqtri 
 |-  ( 5 + 0 ) = ; 0 5
52 40 3 eqeltri 
 |-  ( 0 + 0 ) e. NN0
53 eqid 
 |-  ; ; 5 2 1 = ; ; 5 2 1
54 eqid 
 |-  ; 5 2 = ; 5 2
55 5t4e20 
 |-  ( 5 x. 4 ) = ; 2 0
56 4cn 
 |-  4 e. CC
57 2cn 
 |-  2 e. CC
58 4t2e8 
 |-  ( 4 x. 2 ) = 8
59 56 57 58 mulcomli 
 |-  ( 2 x. 4 ) = 8
60 2 22 10 54 55 59 decmul1 
 |-  ( ; 5 2 x. 4 ) = ; ; 2 0 8
61 56 mullidi 
 |-  ( 1 x. 4 ) = 4
62 61 40 oveq12i 
 |-  ( ( 1 x. 4 ) + ( 0 + 0 ) ) = ( 4 + 0 )
63 56 addridi 
 |-  ( 4 + 0 ) = 4
64 62 63 eqtri 
 |-  ( ( 1 x. 4 ) + ( 0 + 0 ) ) = 4
65 23 15 52 53 2 60 64 decrmanc 
 |-  ( ( ; ; 5 2 1 x. 4 ) + ( 0 + 0 ) ) = ; ; ; 2 0 8 4
66 24 nn0cni 
 |-  ; ; 5 2 1 e. CC
67 66 mul01i 
 |-  ( ; ; 5 2 1 x. 0 ) = 0
68 67 oveq1i 
 |-  ( ( ; ; 5 2 1 x. 0 ) + 5 ) = ( 0 + 5 )
69 48 addlidi 
 |-  ( 0 + 5 ) = 5
70 68 69 50 3eqtri 
 |-  ( ( ; ; 5 2 1 x. 0 ) + 5 ) = ; 0 5
71 2 3 3 22 47 51 24 22 3 65 70 decma2c 
 |-  ( ( ; ; 5 2 1 x. ; 4 0 ) + ( 5 + 0 ) ) = ; ; ; ; 2 0 8 4 5
72 67 oveq1i 
 |-  ( ( ; ; 5 2 1 x. 0 ) + 2 ) = ( 0 + 2 )
73 57 addlidi 
 |-  ( 0 + 2 ) = 2
74 10 dec0h 
 |-  2 = ; 0 2
75 72 73 74 3eqtri 
 |-  ( ( ; ; 5 2 1 x. 0 ) + 2 ) = ; 0 2
76 4 3 22 10 44 46 24 10 3 71 75 decma2c 
 |-  ( ( ; ; 5 2 1 x. ; ; 4 0 0 ) + ( 0 + ; 5 2 ) ) = ; ; ; ; ; 2 0 8 4 5 2
77 45 mulridi 
 |-  ( ; 5 2 x. 1 ) = ; 5 2
78 ax-1cn 
 |-  1 e. CC
79 78 mullidi 
 |-  ( 1 x. 1 ) = 1
80 79 oveq1i 
 |-  ( ( 1 x. 1 ) + 1 ) = ( 1 + 1 )
81 1p1e2 
 |-  ( 1 + 1 ) = 2
82 80 81 eqtri 
 |-  ( ( 1 x. 1 ) + 1 ) = 2
83 23 15 15 53 15 77 82 decrmanc 
 |-  ( ( ; ; 5 2 1 x. 1 ) + 1 ) = ; ; 5 2 2
84 5 15 3 15 1 43 24 10 23 76 83 decma2c 
 |-  ( ( ; ; 5 2 1 x. N ) + 1 ) = ; ; ; ; ; ; 2 0 8 4 5 2 2
85 eqid 
 |-  ; ; 9 0 2 = ; ; 9 0 2
86 6nn0 
 |-  6 e. NN0
87 2 86 deccl 
 |-  ; 4 6 e. NN0
88 87 10 deccl 
 |-  ; ; 4 6 2 e. NN0
89 eqid 
 |-  ; 9 0 = ; 9 0
90 eqid 
 |-  ; ; 4 6 2 = ; ; 4 6 2
91 eqid 
 |-  ; ; ; 2 3 1 1 = ; ; ; 2 3 1 1
92 87 nn0cni 
 |-  ; 4 6 e. CC
93 92 addridi 
 |-  ( ; 4 6 + 0 ) = ; 4 6
94 4p1e5 
 |-  ( 4 + 1 ) = 5
95 94 22 eqeltri 
 |-  ( 4 + 1 ) e. NN0
96 eqid 
 |-  ; ; 2 3 1 = ; ; 2 3 1
97 eqid 
 |-  ; 2 3 = ; 2 3
98 9cn 
 |-  9 e. CC
99 9t2e18 
 |-  ( 9 x. 2 ) = ; 1 8
100 98 57 99 mulcomli 
 |-  ( 2 x. 9 ) = ; 1 8
101 15 19 10 100 81 39 decaddci2 
 |-  ( ( 2 x. 9 ) + 2 ) = ; 2 0
102 7nn0 
 |-  7 e. NN0
103 7p1e8 
 |-  ( 7 + 1 ) = 8
104 3cn 
 |-  3 e. CC
105 9t3e27 
 |-  ( 9 x. 3 ) = ; 2 7
106 98 104 105 mulcomli 
 |-  ( 3 x. 9 ) = ; 2 7
107 10 102 103 106 decsuc 
 |-  ( ( 3 x. 9 ) + 1 ) = ; 2 8
108 10 26 15 97 30 19 10 101 107 decrmac 
 |-  ( ( ; 2 3 x. 9 ) + 1 ) = ; ; 2 0 8
109 98 mullidi 
 |-  ( 1 x. 9 ) = 9
110 109 94 oveq12i 
 |-  ( ( 1 x. 9 ) + ( 4 + 1 ) ) = ( 9 + 5 )
111 9p5e14 
 |-  ( 9 + 5 ) = ; 1 4
112 110 111 eqtri 
 |-  ( ( 1 x. 9 ) + ( 4 + 1 ) ) = ; 1 4
113 27 15 95 96 30 2 15 108 112 decrmac 
 |-  ( ( ; ; 2 3 1 x. 9 ) + ( 4 + 1 ) ) = ; ; ; 2 0 8 4
114 109 oveq1i 
 |-  ( ( 1 x. 9 ) + 6 ) = ( 9 + 6 )
115 9p6e15 
 |-  ( 9 + 6 ) = ; 1 5
116 114 115 eqtri 
 |-  ( ( 1 x. 9 ) + 6 ) = ; 1 5
117 28 15 2 86 91 93 30 22 15 113 116 decmac 
 |-  ( ( ; ; ; 2 3 1 1 x. 9 ) + ( ; 4 6 + 0 ) ) = ; ; ; ; 2 0 8 4 5
118 29 nn0cni 
 |-  ; ; ; 2 3 1 1 e. CC
119 118 mul01i 
 |-  ( ; ; ; 2 3 1 1 x. 0 ) = 0
120 119 oveq1i 
 |-  ( ( ; ; ; 2 3 1 1 x. 0 ) + 2 ) = ( 0 + 2 )
121 120 73 74 3eqtri 
 |-  ( ( ; ; ; 2 3 1 1 x. 0 ) + 2 ) = ; 0 2
122 30 3 87 10 89 90 29 10 3 117 121 decma2c 
 |-  ( ( ; ; ; 2 3 1 1 x. ; 9 0 ) + ; ; 4 6 2 ) = ; ; ; ; ; 2 0 8 4 5 2
123 2t2e4 
 |-  ( 2 x. 2 ) = 4
124 3t2e6 
 |-  ( 3 x. 2 ) = 6
125 10 10 26 97 123 124 decmul1 
 |-  ( ; 2 3 x. 2 ) = ; 4 6
126 57 mullidi 
 |-  ( 1 x. 2 ) = 2
127 10 27 15 96 125 126 decmul1 
 |-  ( ; ; 2 3 1 x. 2 ) = ; ; 4 6 2
128 10 28 15 91 127 126 decmul1 
 |-  ( ; ; ; 2 3 1 1 x. 2 ) = ; ; ; 4 6 2 2
129 29 31 10 85 10 88 122 128 decmul2c 
 |-  ( ; ; ; 2 3 1 1 x. ; ; 9 0 2 ) = ; ; ; ; ; ; 2 0 8 4 5 2 2
130 84 129 eqtr4i 
 |-  ( ( ; ; 5 2 1 x. N ) + 1 ) = ( ; ; ; 2 3 1 1 x. ; ; 9 0 2 )
131 8 9 21 25 29 15 12 32 33 34 42 130 modxai 
 |-  ( ( 2 ^ ; ; ; 1 0 0 0 ) mod N ) = ( 1 mod N )
132 18 nn0cni 
 |-  ; ; ; 1 0 0 0 e. CC
133 eqid 
 |-  ; ; ; 1 0 0 0 = ; ; ; 1 0 0 0
134 eqid 
 |-  ; ; 1 0 0 = ; ; 1 0 0
135 10 dec0u 
 |-  ( ; 1 0 x. 2 ) = ; 2 0
136 57 mul02i 
 |-  ( 0 x. 2 ) = 0
137 10 16 3 134 135 136 decmul1 
 |-  ( ; ; 1 0 0 x. 2 ) = ; ; 2 0 0
138 10 17 3 133 137 136 decmul1 
 |-  ( ; ; ; 1 0 0 0 x. 2 ) = ; ; ; 2 0 0 0
139 132 57 138 mulcomli 
 |-  ( 2 x. ; ; ; 1 0 0 0 ) = ; ; ; 2 0 0 0
140 8 nncni 
 |-  N e. CC
141 140 mul02i 
 |-  ( 0 x. N ) = 0
142 141 oveq1i 
 |-  ( ( 0 x. N ) + 1 ) = ( 0 + 1 )
143 78 addlidi 
 |-  ( 0 + 1 ) = 1
144 79 143 eqtr4i 
 |-  ( 1 x. 1 ) = ( 0 + 1 )
145 142 144 eqtr4i 
 |-  ( ( 0 x. N ) + 1 ) = ( 1 x. 1 )
146 8 9 18 14 15 15 131 139 145 mod2xi 
 |-  ( ( 2 ^ ; ; ; 2 0 0 0 ) mod N ) = ( 1 mod N )
147 13 nn0cni 
 |-  ; ; ; 2 0 0 0 e. CC
148 eqid 
 |-  ; ; ; 2 0 0 0 = ; ; ; 2 0 0 0
149 10 10 3 38 123 136 decmul1 
 |-  ( ; 2 0 x. 2 ) = ; 4 0
150 10 11 3 36 149 136 decmul1 
 |-  ( ; ; 2 0 0 x. 2 ) = ; ; 4 0 0
151 10 12 3 148 150 136 decmul1 
 |-  ( ; ; ; 2 0 0 0 x. 2 ) = ; ; ; 4 0 0 0
152 147 57 151 mulcomli 
 |-  ( 2 x. ; ; ; 2 0 0 0 ) = ; ; ; 4 0 0 0
153 5 3 deccl 
 |-  ; ; ; 4 0 0 0 e. NN0
154 153 nn0cni 
 |-  ; ; ; 4 0 0 0 e. CC
155 eqid 
 |-  ; ; ; 4 0 0 0 = ; ; ; 4 0 0 0
156 5 3 143 155 decsuc 
 |-  ( ; ; ; 4 0 0 0 + 1 ) = ; ; ; 4 0 0 1
157 1 156 eqtr4i 
 |-  N = ( ; ; ; 4 0 0 0 + 1 )
158 154 78 157 mvrraddi 
 |-  ( N - 1 ) = ; ; ; 4 0 0 0
159 152 158 eqtr4i 
 |-  ( 2 x. ; ; ; 2 0 0 0 ) = ( N - 1 )
160 8 9 13 14 15 15 146 159 145 mod2xi 
 |-  ( ( 2 ^ ( N - 1 ) ) mod N ) = ( 1 mod N )