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