MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  2503lem2 Unicode version

Theorem 2503lem2 13152
Description: Lemma for 2503prm 13154. Calculate a power mod. We calculate  2 ^ 1 9  =  2 ^ 1 8  x.  2  ==  1 8 3 2  x.  2  =  N  +  1 1 6 1,  2 ^ 3 8  =  ( 2 ^ 1 9 ) ^ 2  ==  1
1 6 1 ^ 2  =  5 3 8 N  +  1 3 0 7,  2 ^ 3 9  =  2 ^ 3 8  x.  2  ==  1 3 0 7  x.  2  =  N  +  1 1 1,  2 ^ 7 8  =  ( 2 ^ 3 9 ) ^ 2  ==  1
1 1 ^ 2  =  5 N  - 
1 9 4,  2 ^ 1 5 6  =  ( 2 ^ 7 8 ) ^ 2  ==  1 9 4 ^ 2  =  1 5 N  +  9 1,  2 ^ 3 1 2  =  ( 2 ^ 1 5 6 ) ^ 2  ==  9 1 ^ 2  =  3 N  +  7 7 2,  2 ^ 6 2 4  =  ( 2 ^ 3 1 2 ) ^ 2  ==  7 7 2 ^ 2  =  2 3 8 N  + 
2 7 0,  2 ^ 1 2 4 8  =  ( 2 ^ 6 2 4 ) ^
2  ==  2 7 0 ^ 2  =  2 9 N  + 
3 1 3,  2 ^ 1 2 5 1  =  2 ^ 1 2 4 8  x.  8  ==  3 1 3  x.  8  =  N  +  1 and finally  2 ^ ( N  -  1 )  =  ( 2 ^ 1 2 5 1 ) ^ 2  ==  1 ^ 2  =  1. (Contributed by Mario Carneiro, 3-Mar-2014.) (Revised by Mario Carneiro, 20-Apr-2015.)
Hypothesis
Ref Expression
2503prm.1  |-  N  = ;;; 2 5 0 3
Assertion
Ref Expression
2503lem2  |-  ( ( 2 ^ ( N  -  1 ) )  mod  N )  =  ( 1  mod  N
)

Proof of Theorem 2503lem2
StepHypRef Expression
1 2503prm.1 . . 3  |-  N  = ;;; 2 5 0 3
2 2nn0 9998 . . . . . 6  |-  2  e.  NN0
3 5nn0 10001 . . . . . 6  |-  5  e.  NN0
42, 3deccl 10154 . . . . 5  |- ; 2 5  e.  NN0
5 0nn0 9996 . . . . 5  |-  0  e.  NN0
64, 5deccl 10154 . . . 4  |- ;; 2 5 0  e.  NN0
7 3nn 9894 . . . 4  |-  3  e.  NN
86, 7decnncl 10153 . . 3  |- ;;; 2 5 0 3  e.  NN
91, 8eqeltri 2366 . 2  |-  N  e.  NN
10 2nn 9893 . 2  |-  2  e.  NN
11 1nn0 9997 . . . . 5  |-  1  e.  NN0
1211, 2deccl 10154 . . . 4  |- ; 1 2  e.  NN0
1312, 3deccl 10154 . . 3  |- ;; 1 2 5  e.  NN0
1413, 11deccl 10154 . 2  |- ;;; 1 2 5 1  e.  NN0
15 0z 10051 . 2  |-  0  e.  ZZ
16 4nn0 10000 . . . . 5  |-  4  e.  NN0
1712, 16deccl 10154 . . . 4  |- ;; 1 2 4  e.  NN0
18 8nn0 10004 . . . 4  |-  8  e.  NN0
1917, 18deccl 10154 . . 3  |- ;;; 1 2 4 8  e.  NN0
20 1z 10069 . . 3  |-  1  e.  ZZ
21 3nn0 9999 . . . . 5  |-  3  e.  NN0
2221, 11deccl 10154 . . . 4  |- ; 3 1  e.  NN0
2322, 21deccl 10154 . . 3  |- ;; 3 1 3  e.  NN0
24 6nn0 10002 . . . . . 6  |-  6  e.  NN0
2524, 2deccl 10154 . . . . 5  |- ; 6 2  e.  NN0
2625, 16deccl 10154 . . . 4  |- ;; 6 2 4  e.  NN0
27 9nn0 10005 . . . . . 6  |-  9  e.  NN0
282, 27deccl 10154 . . . . 5  |- ; 2 9  e.  NN0
2928nn0zi 10064 . . . 4  |- ; 2 9  e.  ZZ
30 7nn0 10003 . . . . . 6  |-  7  e.  NN0
312, 30deccl 10154 . . . . 5  |- ; 2 7  e.  NN0
3231, 5deccl 10154 . . . 4  |- ;; 2 7 0  e.  NN0
3322, 2deccl 10154 . . . . 5  |- ;; 3 1 2  e.  NN0
342, 21deccl 10154 . . . . . . 7  |- ; 2 3  e.  NN0
3534, 18deccl 10154 . . . . . 6  |- ;; 2 3 8  e.  NN0
3635nn0zi 10064 . . . . 5  |- ;; 2 3 8  e.  ZZ
3730, 30deccl 10154 . . . . . 6  |- ; 7 7  e.  NN0
3837, 2deccl 10154 . . . . 5  |- ;; 7 7 2  e.  NN0
3911, 3deccl 10154 . . . . . . 7  |- ; 1 5  e.  NN0
4039, 24deccl 10154 . . . . . 6  |- ;; 1 5 6  e.  NN0
4121nn0zi 10064 . . . . . 6  |-  3  e.  ZZ
4227, 11deccl 10154 . . . . . 6  |- ; 9 1  e.  NN0
4330, 18deccl 10154 . . . . . . 7  |- ; 7 8  e.  NN0
4439nn0zi 10064 . . . . . . 7  |- ; 1 5  e.  ZZ
4511, 27deccl 10154 . . . . . . . 8  |- ; 1 9  e.  NN0
46 4nn 9895 . . . . . . . 8  |-  4  e.  NN
4745, 46decnncl 10153 . . . . . . 7  |- ;; 1 9 4  e.  NN
4834, 5deccl 10154 . . . . . . . 8  |- ;; 2 3 0  e.  NN0
4948, 27deccl 10154 . . . . . . 7  |- ;;; 2 3 0 9  e.  NN0
5021, 27deccl 10154 . . . . . . . 8  |- ; 3 9  e.  NN0
5116nn0zi 10064 . . . . . . . 8  |-  4  e.  ZZ
5211, 11deccl 10154 . . . . . . . . 9  |- ; 1 1  e.  NN0
5352, 11deccl 10154 . . . . . . . 8  |- ;; 1 1 1  e.  NN0
5421, 18deccl 10154 . . . . . . . . 9  |- ; 3 8  e.  NN0
5511, 21deccl 10154 . . . . . . . . . . 11  |- ; 1 3  e.  NN0
5655, 5deccl 10154 . . . . . . . . . 10  |- ;; 1 3 0  e.  NN0
5756, 30deccl 10154 . . . . . . . . 9  |- ;;; 1 3 0 7  e.  NN0
583, 21deccl 10154 . . . . . . . . . . . 12  |- ; 5 3  e.  NN0
5958, 18deccl 10154 . . . . . . . . . . 11  |- ;; 5 3 8  e.  NN0
6059nn0zi 10064 . . . . . . . . . 10  |- ;; 5 3 8  e.  ZZ
6152, 24deccl 10154 . . . . . . . . . . 11  |- ;; 1 1 6  e.  NN0
6261, 11deccl 10154 . . . . . . . . . 10  |- ;;; 1 1 6 1  e.  NN0
6311, 18deccl 10154 . . . . . . . . . . 11  |- ; 1 8  e.  NN0
6463, 21deccl 10154 . . . . . . . . . . . 12  |- ;; 1 8 3  e.  NN0
6564, 2deccl 10154 . . . . . . . . . . 11  |- ;;; 1 8 3 2  e.  NN0
6612503lem1 13151 . . . . . . . . . . 11  |-  ( ( 2 ^; 1 8 )  mod 
N )  =  (;;; 1 8 3 2  mod 
N )
67 8p1e9 9869 . . . . . . . . . . . 12  |-  ( 8  +  1 )  =  9
68 eqid 2296 . . . . . . . . . . . 12  |- ; 1 8  = ; 1 8
6911, 18, 67, 68decsuc 10163 . . . . . . . . . . 11  |-  (; 1 8  +  1 )  = ; 1 9
70 eqid 2296 . . . . . . . . . . . . 13  |- ;;; 1 1 6 1  = ;;; 1 1 6 1
71 eqid 2296 . . . . . . . . . . . . . 14  |- ;; 2 5 0  = ;; 2 5 0
7261nn0cni 9993 . . . . . . . . . . . . . . 15  |- ;; 1 1 6  e.  CC
7372addid1i 9015 . . . . . . . . . . . . . 14  |-  (;; 1 1 6  +  0 )  = ;; 1 1 6
74 eqid 2296 . . . . . . . . . . . . . . 15  |- ; 2 5  = ; 2 5
7552nn0cni 9993 . . . . . . . . . . . . . . . 16  |- ; 1 1  e.  CC
7675addid1i 9015 . . . . . . . . . . . . . . 15  |-  (; 1 1  +  0 )  = ; 1 1
77 2cn 9832 . . . . . . . . . . . . . . . . . 18  |-  2  e.  CC
7877mulid2i 8856 . . . . . . . . . . . . . . . . 17  |-  ( 1  x.  2 )  =  2
79 ax-1cn 8811 . . . . . . . . . . . . . . . . . 18  |-  1  e.  CC
8079addid1i 9015 . . . . . . . . . . . . . . . . 17  |-  ( 1  +  0 )  =  1
8178, 80oveq12i 5886 . . . . . . . . . . . . . . . 16  |-  ( ( 1  x.  2 )  +  ( 1  +  0 ) )  =  ( 2  +  1 )
82 2p1e3 9863 . . . . . . . . . . . . . . . 16  |-  ( 2  +  1 )  =  3
8381, 82eqtri 2316 . . . . . . . . . . . . . . 15  |-  ( ( 1  x.  2 )  +  ( 1  +  0 ) )  =  3
84 5nn 9896 . . . . . . . . . . . . . . . . . . 19  |-  5  e.  NN
8584nncni 9772 . . . . . . . . . . . . . . . . . 18  |-  5  e.  CC
8685mulid2i 8856 . . . . . . . . . . . . . . . . 17  |-  ( 1  x.  5 )  =  5
8786oveq1i 5884 . . . . . . . . . . . . . . . 16  |-  ( ( 1  x.  5 )  +  1 )  =  ( 5  +  1 )
88 5p1e6 9866 . . . . . . . . . . . . . . . 16  |-  ( 5  +  1 )  =  6
8924dec0h 10156 . . . . . . . . . . . . . . . 16  |-  6  = ; 0 6
9087, 88, 893eqtri 2320 . . . . . . . . . . . . . . 15  |-  ( ( 1  x.  5 )  +  1 )  = ; 0
6
912, 3, 11, 11, 74, 76, 11, 24, 5, 83, 90decma2c 10180 . . . . . . . . . . . . . 14  |-  ( ( 1  x. ; 2 5 )  +  (; 1 1  +  0 ) )  = ; 3 6
9279mul01i 9018 . . . . . . . . . . . . . . . 16  |-  ( 1  x.  0 )  =  0
9392oveq1i 5884 . . . . . . . . . . . . . . 15  |-  ( ( 1  x.  0 )  +  6 )  =  ( 0  +  6 )
94 6nn 9897 . . . . . . . . . . . . . . . . 17  |-  6  e.  NN
9594nncni 9772 . . . . . . . . . . . . . . . 16  |-  6  e.  CC
9695addid2i 9016 . . . . . . . . . . . . . . 15  |-  ( 0  +  6 )  =  6
9793, 96, 893eqtri 2320 . . . . . . . . . . . . . 14  |-  ( ( 1  x.  0 )  +  6 )  = ; 0
6
984, 5, 52, 24, 71, 73, 11, 24, 5, 91, 97decma2c 10180 . . . . . . . . . . . . 13  |-  ( ( 1  x. ;; 2 5 0 )  +  (;; 1 1 6  +  0 ) )  = ;; 3 6 6
99 3cn 9834 . . . . . . . . . . . . . . . 16  |-  3  e.  CC
10099mulid2i 8856 . . . . . . . . . . . . . . 15  |-  ( 1  x.  3 )  =  3
101100oveq1i 5884 . . . . . . . . . . . . . 14  |-  ( ( 1  x.  3 )  +  1 )  =  ( 3  +  1 )
102 3p1e4 9864 . . . . . . . . . . . . . 14  |-  ( 3  +  1 )  =  4
10316dec0h 10156 . . . . . . . . . . . . . 14  |-  4  = ; 0 4
104101, 102, 1033eqtri 2320 . . . . . . . . . . . . 13  |-  ( ( 1  x.  3 )  +  1 )  = ; 0
4
1056, 21, 61, 11, 1, 70, 11, 16, 5, 98, 104decma2c 10180 . . . . . . . . . . . 12  |-  ( ( 1  x.  N )  + ;;; 1 1 6 1 )  = ;;; 3 6 6 4
106 eqid 2296 . . . . . . . . . . . . 13  |- ;;; 1 8 3 2  = ;;; 1 8 3 2
107 eqid 2296 . . . . . . . . . . . . . . . 16  |- ;; 1 8 3  = ;; 1 8 3
10878oveq1i 5884 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 1  x.  2 )  +  1 )  =  ( 2  +  1 )
109108, 82eqtri 2316 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 1  x.  2 )  +  1 )  =  3
110 8t2e16 10228 . . . . . . . . . . . . . . . . . . 19  |-  ( 8  x.  2 )  = ; 1
6
1112, 11, 18, 68, 24, 11, 109, 110decmul1c 10187 . . . . . . . . . . . . . . . . . 18  |-  (; 1 8  x.  2 )  = ; 3 6
112111oveq1i 5884 . . . . . . . . . . . . . . . . 17  |-  ( (; 1
8  x.  2 )  +  0 )  =  (; 3 6  +  0 )
11321, 24deccl 10154 . . . . . . . . . . . . . . . . . . 19  |- ; 3 6  e.  NN0
114113nn0cni 9993 . . . . . . . . . . . . . . . . . 18  |- ; 3 6  e.  CC
115114addid1i 9015 . . . . . . . . . . . . . . . . 17  |-  (; 3 6  +  0 )  = ; 3 6
116112, 115eqtri 2316 . . . . . . . . . . . . . . . 16  |-  ( (; 1
8  x.  2 )  +  0 )  = ; 3
6
117 3t2e6 9888 . . . . . . . . . . . . . . . . 17  |-  ( 3  x.  2 )  =  6
118117, 89eqtri 2316 . . . . . . . . . . . . . . . 16  |-  ( 3  x.  2 )  = ; 0
6
1192, 63, 21, 107, 24, 5, 116, 118decmul1c 10187 . . . . . . . . . . . . . . 15  |-  (;; 1 8 3  x.  2 )  = ;; 3 6 6
120119oveq1i 5884 . . . . . . . . . . . . . 14  |-  ( (;; 1 8 3  x.  2 )  +  0 )  =  (;; 3 6 6  +  0 )
121113, 24deccl 10154 . . . . . . . . . . . . . . . 16  |- ;; 3 6 6  e.  NN0
122121nn0cni 9993 . . . . . . . . . . . . . . 15  |- ;; 3 6 6  e.  CC
123122addid1i 9015 . . . . . . . . . . . . . 14  |-  (;; 3 6 6  +  0 )  = ;; 3 6 6
124120, 123eqtri 2316 . . . . . . . . . . . . 13  |-  ( (;; 1 8 3  x.  2 )  +  0 )  = ;; 3 6 6
125 2t2e4 9887 . . . . . . . . . . . . . 14  |-  ( 2  x.  2 )  =  4
126125, 103eqtri 2316 . . . . . . . . . . . . 13  |-  ( 2  x.  2 )  = ; 0
4
1272, 64, 2, 106, 16, 5, 124, 126decmul1c 10187 . . . . . . . . . . . 12  |-  (;;; 1 8 3 2  x.  2 )  = ;;; 3 6 6 4
128105, 127eqtr4i 2319 . . . . . . . . . . 11  |-  ( ( 1  x.  N )  + ;;; 1 1 6 1 )  =  (;;; 1 8 3 2  x.  2 )
1299, 10, 63, 20, 65, 62, 66, 69, 128modxp1i 13101 . . . . . . . . . 10  |-  ( ( 2 ^; 1 9 )  mod 
N )  =  (;;; 1 1 6 1  mod 
N )
130 eqid 2296 . . . . . . . . . . 11  |- ; 1 9  = ; 1 9
13177mulid1i 8855 . . . . . . . . . . . . 13  |-  ( 2  x.  1 )  =  2
132131oveq1i 5884 . . . . . . . . . . . 12  |-  ( ( 2  x.  1 )  +  1 )  =  ( 2  +  1 )
133132, 82eqtri 2316 . . . . . . . . . . 11  |-  ( ( 2  x.  1 )  +  1 )  =  3
134 9nn 9900 . . . . . . . . . . . . 13  |-  9  e.  NN
135134nncni 9772 . . . . . . . . . . . 12  |-  9  e.  CC
136 9t2e18 10235 . . . . . . . . . . . 12  |-  ( 9  x.  2 )  = ; 1
8
137135, 77, 136mulcomli 8860 . . . . . . . . . . 11  |-  ( 2  x.  9 )  = ; 1
8
1382, 11, 27, 130, 18, 11, 133, 137decmul2c 10188 . . . . . . . . . 10  |-  ( 2  x. ; 1 9 )  = ; 3
8
139 eqid 2296 . . . . . . . . . . . 12  |- ;;; 1 3 0 7  = ;;; 1 3 0 7
14011, 24deccl 10154 . . . . . . . . . . . . 13  |- ; 1 6  e.  NN0
141140, 2deccl 10154 . . . . . . . . . . . 12  |- ;; 1 6 2  e.  NN0
142 eqid 2296 . . . . . . . . . . . . . 14  |- ;; 1 3 0  = ;; 1 3 0
143 eqid 2296 . . . . . . . . . . . . . 14  |- ;; 1 6 2  = ;; 1 6 2
144 eqid 2296 . . . . . . . . . . . . . . 15  |- ; 1 3  = ; 1 3
145 eqid 2296 . . . . . . . . . . . . . . 15  |- ; 1 6  = ; 1 6
146 1p1e2 9856 . . . . . . . . . . . . . . 15  |-  ( 1  +  1 )  =  2
147 6p3e9 9881 . . . . . . . . . . . . . . . 16  |-  ( 6  +  3 )  =  9
14895, 99, 147addcomli 9020 . . . . . . . . . . . . . . 15  |-  ( 3  +  6 )  =  9
14911, 21, 11, 24, 144, 145, 146, 148decadd 10181 . . . . . . . . . . . . . 14  |-  (; 1 3  + ; 1 6 )  = ; 2
9
15077addid2i 9016 . . . . . . . . . . . . . 14  |-  ( 0  +  2 )  =  2
15155, 5, 140, 2, 142, 143, 149, 150decadd 10181 . . . . . . . . . . . . 13  |-  (;; 1 3 0  + ;; 1 6 2 )  = ;; 2 9 2
15228nn0cni 9993 . . . . . . . . . . . . . . 15  |- ; 2 9  e.  CC
153152addid1i 9015 . . . . . . . . . . . . . 14  |-  (; 2 9  +  0 )  = ; 2 9
1542, 24deccl 10154 . . . . . . . . . . . . . . 15  |- ; 2 6  e.  NN0
155154, 27deccl 10154 . . . . . . . . . . . . . 14  |- ;; 2 6 9  e.  NN0
156 eqid 2296 . . . . . . . . . . . . . . 15  |- ;; 5 3 8  = ;; 5 3 8
1572dec0h 10156 . . . . . . . . . . . . . . . 16  |-  2  = ; 0 2
158 eqid 2296 . . . . . . . . . . . . . . . 16  |- ;; 2 6 9  = ;; 2 6 9
159 6p1e7 9867 . . . . . . . . . . . . . . . . 17  |-  ( 6  +  1 )  =  7
160154nn0cni 9993 . . . . . . . . . . . . . . . . . 18  |- ; 2 6  e.  CC
161160addid2i 9016 . . . . . . . . . . . . . . . . 17  |-  ( 0  + ; 2 6 )  = ; 2
6
1622, 24, 159, 161decsuc 10163 . . . . . . . . . . . . . . . 16  |-  ( ( 0  + ; 2 6 )  +  1 )  = ; 2 7
163 9p2e11 10202 . . . . . . . . . . . . . . . . 17  |-  ( 9  +  2 )  = ; 1
1
164135, 77, 163addcomli 9020 . . . . . . . . . . . . . . . 16  |-  ( 2  +  9 )  = ; 1
1
1655, 2, 154, 27, 157, 158, 162, 11, 164decaddc 10182 . . . . . . . . . . . . . . 15  |-  ( 2  + ;; 2 6 9 )  = ;; 2 7 1
166 eqid 2296 . . . . . . . . . . . . . . . 16  |- ; 5 3  = ; 5 3
167 7p1e8 9868 . . . . . . . . . . . . . . . . 17  |-  ( 7  +  1 )  =  8
168 eqid 2296 . . . . . . . . . . . . . . . . 17  |- ; 2 7  = ; 2 7
1692, 30, 167, 168decsuc 10163 . . . . . . . . . . . . . . . 16  |-  (; 2 7  +  1 )  = ; 2 8
17082oveq2i 5885 . . . . . . . . . . . . . . . . 17  |-  ( ( 5  x.  2 )  +  ( 2  +  1 ) )  =  ( ( 5  x.  2 )  +  3 )
171 5t2e10 9891 . . . . . . . . . . . . . . . . . . 19  |-  ( 5  x.  2 )  =  10
172 dec10 10170 . . . . . . . . . . . . . . . . . . 19  |-  10  = ; 1 0
173171, 172eqtri 2316 . . . . . . . . . . . . . . . . . 18  |-  ( 5  x.  2 )  = ; 1
0
17499addid2i 9016 . . . . . . . . . . . . . . . . . 18  |-  ( 0  +  3 )  =  3
17511, 5, 21, 173, 174decaddi 10184 . . . . . . . . . . . . . . . . 17  |-  ( ( 5  x.  2 )  +  3 )  = ; 1
3
176170, 175eqtri 2316 . . . . . . . . . . . . . . . 16  |-  ( ( 5  x.  2 )  +  ( 2  +  1 ) )  = ; 1
3
177117oveq1i 5884 . . . . . . . . . . . . . . . . 17  |-  ( ( 3  x.  2 )  +  8 )  =  ( 6  +  8 )
178 8nn 9899 . . . . . . . . . . . . . . . . . . 19  |-  8  e.  NN
179178nncni 9772 . . . . . . . . . . . . . . . . . 18  |-  8  e.  CC
180 8p6e14 10199 . . . . . . . . . . . . . . . . . 18  |-  ( 8  +  6 )  = ; 1
4
181179, 95, 180addcomli 9020 . . . . . . . . . . . . . . . . 17  |-  ( 6  +  8 )  = ; 1
4
182177, 181eqtri 2316 . . . . . . . . . . . . . . . 16  |-  ( ( 3  x.  2 )  +  8 )  = ; 1
4
1833, 21, 2, 18, 166, 169, 2, 16, 11, 176, 182decmac 10179 . . . . . . . . . . . . . . 15  |-  ( (; 5
3  x.  2 )  +  (; 2 7  +  1 ) )  = ;; 1 3 4
18411, 24, 159, 110decsuc 10163 . . . . . . . . . . . . . . 15  |-  ( ( 8  x.  2 )  +  1 )  = ; 1
7
18558, 18, 31, 11, 156, 165, 2, 30, 11, 183, 184decmac 10179 . . . . . . . . . . . . . 14  |-  ( (;; 5 3 8  x.  2 )  +  ( 2  + ;; 2 6 9 ) )  = ;;; 1 3 4 7
18627dec0h 10156 . . . . . . . . . . . . . . 15  |-  9  = ; 0 9
187 4cn 9836 . . . . . . . . . . . . . . . . . 18  |-  4  e.  CC
188187addid2i 9016 . . . . . . . . . . . . . . . . 17  |-  ( 0  +  4 )  =  4
189188, 103eqtri 2316 . . . . . . . . . . . . . . . 16  |-  ( 0  +  4 )  = ; 0
4
190 0p1e1 9855 . . . . . . . . . . . . . . . . . 18  |-  ( 0  +  1 )  =  1
191190oveq2i 5885 . . . . . . . . . . . . . . . . 17  |-  ( ( 5  x.  5 )  +  ( 0  +  1 ) )  =  ( ( 5  x.  5 )  +  1 )
192 5t5e25 10216 . . . . . . . . . . . . . . . . . 18  |-  ( 5  x.  5 )  = ; 2
5
1932, 3, 88, 192decsuc 10163 . . . . . . . . . . . . . . . . 17  |-  ( ( 5  x.  5 )  +  1 )  = ; 2
6
194191, 193eqtri 2316 . . . . . . . . . . . . . . . 16  |-  ( ( 5  x.  5 )  +  ( 0  +  1 ) )  = ; 2
6
195 5t3e15 10214 . . . . . . . . . . . . . . . . . 18  |-  ( 5  x.  3 )  = ; 1
5
19685, 99, 195mulcomli 8860 . . . . . . . . . . . . . . . . 17  |-  ( 3  x.  5 )  = ; 1
5
197 5p4e9 9878 . . . . . . . . . . . . . . . . 17  |-  ( 5  +  4 )  =  9
19811, 3, 16, 196, 197decaddi 10184 . . . . . . . . . . . . . . . 16  |-  ( ( 3  x.  5 )  +  4 )  = ; 1
9
1993, 21, 5, 16, 166, 189, 3, 27, 11, 194, 198decmac 10179 . . . . . . . . . . . . . . 15  |-  ( (; 5
3  x.  5 )  +  ( 0  +  4 ) )  = ;; 2 6 9
200 8t5e40 10231 . . . . . . . . . . . . . . . 16  |-  ( 8  x.  5 )  = ; 4
0
201135addid2i 9016 . . . . . . . . . . . . . . . 16  |-  ( 0  +  9 )  =  9
20216, 5, 27, 200, 201decaddi 10184 . . . . . . . . . . . . . . 15  |-  ( ( 8  x.  5 )  +  9 )  = ; 4
9
20358, 18, 5, 27, 156, 186, 3, 27, 16, 199, 202decmac 10179 . . . . . . . . . . . . . 14  |-  ( (;; 5 3 8  x.  5 )  +  9 )  = ;;; 2 6 9 9
2042, 3, 2, 27, 74, 153, 59, 27, 155, 185, 203decma2c 10180 . . . . . . . . . . . . 13  |-  ( (;; 5 3 8  x. ; 2
5 )  +  (; 2
9  +  0 ) )  = ;;;; 1 3 4 7 9
20559nn0cni 9993 . . . . . . . . . . . . . . . 16  |- ;; 5 3 8  e.  CC
206205mul01i 9018 . . . . . . . . . . . . . . 15  |-  (;; 5 3 8  x.  0 )  =  0
207206oveq1i 5884 . . . . . . . . . . . . . 14  |-  ( (;; 5 3 8  x.  0 )  +  2 )  =  ( 0  +  2 )
208207, 150, 1573eqtri 2320 . . . . . . . . . . . . 13  |-  ( (;; 5 3 8  x.  0 )  +  2 )  = ; 0 2
2094, 5, 28, 2, 71, 151, 59, 2, 5, 204, 208decma2c 10180 . . . . . . . . . . . 12  |-  ( (;; 5 3 8  x. ;; 2 5 0 )  +  (;; 1 3 0  + ;; 1 6 2 ) )  = ;;;;; 1 3 4 7 9 2
21030dec0h 10156 . . . . . . . . . . . . 13  |-  7  = ; 0 7
21121dec0h 10156 . . . . . . . . . . . . . . 15  |-  3  = ; 0 3
212174, 211eqtri 2316 . . . . . . . . . . . . . 14  |-  ( 0  +  3 )  = ; 0
3
213190oveq2i 5885 . . . . . . . . . . . . . . 15  |-  ( ( 5  x.  3 )  +  ( 0  +  1 ) )  =  ( ( 5  x.  3 )  +  1 )
21411, 3, 88, 195decsuc 10163 . . . . . . . . . . . . . . 15  |-  ( ( 5  x.  3 )  +  1 )  = ; 1
6
215213, 214eqtri 2316 . . . . . . . . . . . . . 14  |-  ( ( 5  x.  3 )  +  ( 0  +  1 ) )  = ; 1
6
216 3t3e9 9889 . . . . . . . . . . . . . . . 16  |-  ( 3  x.  3 )  =  9
217216oveq1i 5884 . . . . . . . . . . . . . . 15  |-  ( ( 3  x.  3 )  +  3 )  =  ( 9  +  3 )
218 9p3e12 10203 . . . . . . . . . . . . . . 15  |-  ( 9  +  3 )  = ; 1
2
219217, 218eqtri 2316 . . . . . . . . . . . . . 14  |-  ( ( 3  x.  3 )  +  3 )  = ; 1
2
2203, 21, 5, 21, 166, 212, 21, 2, 11, 215, 219decmac 10179 . . . . . . . . . . . . 13  |-  ( (; 5
3  x.  3 )  +  ( 0  +  3 ) )  = ;; 1 6 2
221 8t3e24 10229 . . . . . . . . . . . . . 14  |-  ( 8  x.  3 )  = ; 2
4
222 7nn 9898 . . . . . . . . . . . . . . . 16  |-  7  e.  NN
223222nncni 9772 . . . . . . . . . . . . . . 15  |-  7  e.  CC
224 7p4e11 10192 . . . . . . . . . . . . . . 15  |-  ( 7  +  4 )  = ; 1
1
225223, 187, 224addcomli 9020 . . . . . . . . . . . . . 14  |-  ( 4  +  7 )  = ; 1
1
2262, 16, 30, 221, 82, 11, 225decaddci 10185 . . . . . . . . . . . . 13  |-  ( ( 8  x.  3 )  +  7 )  = ; 3
1
22758, 18, 5, 30, 156, 210, 21, 11, 21, 220, 226decmac 10179 . . . . . . . . . . . 12  |-  ( (;; 5 3 8  x.  3 )  +  7 )  = ;;; 1 6 2 1
2286, 21, 56, 30, 1, 139, 59, 11, 141, 209, 227decma2c 10180 . . . . . . . . . . 11  |-  ( (;; 5 3 8  x.  N )  + ;;; 1 3 0 7 )  = ;;;;;; 1 3 4 7 9 2 1
229 eqid 2296 . . . . . . . . . . . . 13  |- ;; 1 1 6  = ;; 1 1 6
23024, 27deccl 10154 . . . . . . . . . . . . . 14  |- ; 6 9  e.  NN0
231230, 30deccl 10154 . . . . . . . . . . . . 13  |- ;; 6 9 7  e.  NN0
23230, 5deccl 10154 . . . . . . . . . . . . . 14  |- ; 7 0  e.  NN0
233 eqid 2296 . . . . . . . . . . . . . 14  |- ; 1 1  = ; 1 1
234 eqid 2296 . . . . . . . . . . . . . . 15  |- ;; 6 9 7  = ;; 6 9 7
23511dec0h 10156 . . . . . . . . . . . . . . . 16  |-  1  = ; 0 1
236 eqid 2296 . . . . . . . . . . . . . . . 16  |- ; 6 9  = ; 6 9
23796oveq1i 5884 . . . . . . . . . . . . . . . . 17  |-  ( ( 0  +  6 )  +  1 )  =  ( 6  +  1 )
238237, 159eqtri 2316 . . . . . . . . . . . . . . . 16  |-  ( ( 0  +  6 )  +  1 )  =  7
239 9p1e10 9870 . . . . . . . . . . . . . . . . 17  |-  ( 9  +  1 )  =  10
240135, 79, 239addcomli 9020 . . . . . . . . . . . . . . . 16  |-  ( 1  +  9 )  =  10
2415, 11, 24, 27, 235, 236, 238, 240decaddc2 10183 . . . . . . . . . . . . . . 15  |-  ( 1  + ; 6 9 )  = ; 7
0
242223, 79, 167addcomli 9020 . . . . . . . . . . . . . . 15  |-  ( 1  +  7 )  =  8
24311, 11, 230, 30, 233, 234, 241, 242decadd 10181 . . . . . . . . . . . . . 14  |-  (; 1 1  + ;; 6 9 7 )  = ;; 7 0 8
244 eqid 2296 . . . . . . . . . . . . . . . 16  |- ; 7 0  = ; 7 0
2455, 30, 11, 11, 210, 233, 190, 167decadd 10181 . . . . . . . . . . . . . . . 16  |-  ( 7  + ; 1 1 )  = ; 1
8
24630, 5, 52, 24, 244, 229, 245, 96decadd 10181 . . . . . . . . . . . . . . 15  |-  (; 7 0  + ;; 1 1 6 )  = ;; 1 8 6
24763nn0cni 9993 . . . . . . . . . . . . . . . . 17  |- ; 1 8  e.  CC
248247addid1i 9015 . . . . . . . . . . . . . . . 16  |-  (; 1 8  +  0 )  = ; 1 8
249146, 157eqtri 2316 . . . . . . . . . . . . . . . . 17  |-  ( 1  +  1 )  = ; 0
2
250 1t1e1 9886 . . . . . . . . . . . . . . . . . . 19  |-  ( 1  x.  1 )  =  1
251 00id 9003 . . . . . . . . . . . . . . . . . . 19  |-  ( 0  +  0 )  =  0
252250, 251oveq12i 5886 . . . . . . . . . . . . . . . . . 18  |-  ( ( 1  x.  1 )  +  ( 0  +  0 ) )  =  ( 1  +  0 )
253252, 80eqtri 2316 . . . . . . . . . . . . . . . . 17  |-  ( ( 1  x.  1 )  +  ( 0  +  0 ) )  =  1
254250oveq1i 5884 . . . . . . . . . . . . . . . . . 18  |-  ( ( 1  x.  1 )  +  2 )  =  ( 1  +  2 )
25577, 79, 82addcomli 9020 . . . . . . . . . . . . . . . . . 18  |-  ( 1  +  2 )  =  3
256254, 255, 2113eqtri 2320 . . . . . . . . . . . . . . . . 17  |-  ( ( 1  x.  1 )  +  2 )  = ; 0
3
25711, 11, 5, 2, 233, 249, 11, 21, 5, 253, 256decmac 10179 . . . . . . . . . . . . . . . 16  |-  ( (; 1
1  x.  1 )  +  ( 1  +  1 ) )  = ; 1
3
25895mulid1i 8855 . . . . . . . . . . . . . . . . . 18  |-  ( 6  x.  1 )  =  6
259258oveq1i 5884 . . . . . . . . . . . . . . . . 17  |-  ( ( 6  x.  1 )  +  8 )  =  ( 6  +  8 )
260259, 181eqtri 2316 . . . . . . . . . . . . . . . 16  |-  ( ( 6  x.  1 )  +  8 )  = ; 1
4
26152, 24, 11, 18, 229, 248, 11, 16, 11, 257, 260decmac 10179 . . . . . . . . . . . . . . 15  |-  ( (;; 1 1 6  x.  1 )  +  (; 1
8  +  0 ) )  = ;; 1 3 4
262250oveq1i 5884 . . . . . . . . . . . . . . . 16  |-  ( ( 1  x.  1 )  +  6 )  =  ( 1  +  6 )
26395, 79, 159addcomli 9020 . . . . . . . . . . . . . . . 16  |-  ( 1  +  6 )  =  7
264262, 263, 2103eqtri 2320 . . . . . . . . . . . . . . 15  |-  ( ( 1  x.  1 )  +  6 )  = ; 0
7
26561, 11, 63, 24, 70, 246, 11, 30, 5, 261, 264decmac 10179 . . . . . . . . . . . . . 14  |-  ( (;;; 1 1 6 1  x.  1 )  +  (; 7
0  + ;; 1 1 6 ) )  = ;;; 1 3 4 7
26618dec0h 10156 . . . . . . . . . . . . . . 15  |-  8  = ; 0 8
2675dec0h 10156 . . . . . . . . . . . . . . . . 17  |-  0  = ; 0 0
268251, 267eqtri 2316 . . . . . . . . . . . . . . . 16  |-  ( 0  +  0 )  = ; 0
0
269250oveq1i 5884 . . . . . . . . . . . . . . . . . 18  |-  ( ( 1  x.  1 )  +  0 )  =  ( 1  +  0 )
270269, 80eqtri 2316 . . . . . . . . . . . . . . . . 17  |-  ( ( 1  x.  1 )  +  0 )  =  1
27111, 11, 5, 5, 233, 268, 11, 270, 270decma 10178 . . . . . . . . . . . . . . . 16  |-  ( (; 1
1  x.  1 )  +  ( 0  +  0 ) )  = ; 1
1
272258oveq1i 5884 . . . . . . . . . . . . . . . . 17  |-  ( ( 6  x.  1 )  +  0 )  =  ( 6  +  0 )
27395addid1i 9015 . . . . . . . . . . . . . . . . 17  |-  ( 6  +  0 )  =  6
274272, 273, 893eqtri 2320 . . . . . . . . . . . . . . . 16  |-  ( ( 6  x.  1 )  +  0 )  = ; 0
6
27552, 24, 5, 5, 229, 268, 11, 24, 5, 271, 274decmac 10179 . . . . . . . . . . . . . . 15  |-  ( (;; 1 1 6  x.  1 )  +  ( 0  +  0 ) )  = ;; 1 1 6
276250oveq1i 5884 . . . . . . . . . . . . . . . 16  |-  ( ( 1  x.  1 )  +  8 )  =  ( 1  +  8 )
277179, 79, 67addcomli 9020 . . . . . . . . . . . . . . . 16  |-  ( 1  +  8 )  =  9
278276, 277, 1863eqtri 2320 . . . . . . . . . . . . . . 15  |-  ( ( 1  x.  1 )  +  8 )  = ; 0
9
27961, 11, 5, 18, 70, 266, 11, 27, 5, 275, 278decmac 10179 . . . . . . . . . . . . . 14  |-  ( (;;; 1 1 6 1  x.  1 )  +  8 )  = ;;; 1 1 6 9
28011, 11, 232, 18, 233, 243, 62, 27, 61, 265, 279decma2c 10180 . . . . . . . . . . . . 13  |-  ( (;;; 1 1 6 1  x. ; 1
1 )  +  (; 1
1  + ;; 6 9 7 ) )  = ;;;; 1 3 4 7 9
281190, 235eqtri 2316 . . . . . . . . . . . . . . 15  |-  ( 0  +  1 )  = ; 0
1
28295mulid2i 8856 . . . . . . . . . . . . . . . . . 18  |-  ( 1  x.  6 )  =  6
283282, 251oveq12i 5886 . . . . . . . . . . . . . . . . 17  |-  ( ( 1  x.  6 )  +  ( 0  +  0 ) )  =  ( 6  +  0 )
284283, 273eqtri 2316 . . . . . . . . . . . . . . . 16  |-  ( ( 1  x.  6 )  +  ( 0  +  0 ) )  =  6
285282oveq1i 5884 . . . . . . . . . . . . . . . . 17  |-  ( ( 1  x.  6 )  +  3 )  =  ( 6  +  3 )
286285, 147, 1863eqtri 2320 . . . . . . . . . . . . . . . 16  |-  ( ( 1  x.  6 )  +  3 )  = ; 0
9
28711, 11, 5, 21, 233, 212, 24, 27, 5, 284, 286decmac 10179 . . . . . . . . . . . . . . 15  |-  ( (; 1
1  x.  6 )  +  ( 0  +  3 ) )  = ; 6
9
288 6t6e36 10221 . . . . . . . . . . . . . . . 16  |-  ( 6  x.  6 )  = ; 3
6
28921, 24, 159, 288decsuc 10163 . . . . . . . . . . . . . . 15  |-  ( ( 6  x.  6 )  +  1 )  = ; 3
7
29052, 24, 5, 11, 229, 281, 24, 30, 21, 287, 289decmac 10179 . . . . . . . . . . . . . 14  |-  ( (;; 1 1 6  x.  6 )  +  ( 0  +  1 ) )  = ;; 6 9 7
291282oveq1i 5884 . . . . . . . . . . . . . . 15  |-  ( ( 1  x.  6 )  +  6 )  =  ( 6  +  6 )
292 6p6e12 10191 . . . . . . . . . . . . . . 15  |-  ( 6  +  6 )  = ; 1
2
293291, 292eqtri 2316 . . . . . . . . . . . . . 14  |-  ( ( 1  x.  6 )  +  6 )  = ; 1
2
29461, 11, 5, 24, 70, 89, 24, 2, 11, 290, 293decmac 10179 . . . . . . . . . . . . 13  |-  ( (;;; 1 1 6 1  x.  6 )  +  6 )  = ;;; 6 9 7 2
29552, 24, 52, 24, 229, 229, 62, 2, 231, 280, 294decma2c 10180 . . . . . . . . . . . 12  |-  ( (;;; 1 1 6 1  x. ;; 1 1 6 )  + ;; 1 1 6 )  = ;;;;; 1 3 4 7 9 2
29662nn0cni 9993 . . . . . . . . . . . . 13  |- ;;; 1 1 6 1  e.  CC
297296mulid1i 8855 . . . . . . . . . . . 12  |-  (;;; 1 1 6 1  x.  1 )  = ;;; 1 1 6 1
29862, 61, 11, 70, 11, 61, 295, 297decmul2c 10188 . . . . . . . . . . 11  |-  (;;; 1 1 6 1  x. ;;; 1 1 6 1 )  = ;;;;;; 1 3 4 7 9 2 1
299228, 298eqtr4i 2319 . . . . . . . . . 10  |-  ( (;; 5 3 8  x.  N )  + ;;; 1 3 0 7 )  =  (;;; 1 1 6 1  x. ;;; 1 1 6 1 )
3009, 10, 45, 60, 62, 57, 129, 138, 299mod2xi 13100 . . . . . . . . 9  |-  ( ( 2 ^; 3 8 )  mod 
N )  =  (;;; 1 3 0 7  mod 
N )
301 eqid 2296 . . . . . . . . . 10  |- ; 3 8  = ; 3 8
30221, 18, 67, 301decsuc 10163 . . . . . . . . 9  |-  (; 3 8  +  1 )  = ; 3 9
303 eqid 2296 . . . . . . . . . . 11  |- ;; 1 1 1  = ;; 1 1 1
30480, 235eqtri 2316 . . . . . . . . . . . . 13  |-  ( 1  +  0 )  = ; 0
1
30578, 251oveq12i 5886 . . . . . . . . . . . . . 14  |-  ( ( 1  x.  2 )  +  ( 0  +  0 ) )  =  ( 2  +  0 )
30677addid1i 9015 . . . . . . . . . . . . . 14  |-  ( 2  +  0 )  =  2
307305, 306eqtri 2316 . . . . . . . . . . . . 13  |-  ( ( 1  x.  2 )  +  ( 0  +  0 ) )  =  2
3082, 3, 5, 11, 74, 304, 11, 24, 5, 307, 90decma2c 10180 . . . . . . . . . . . 12  |-  ( ( 1  x. ; 2 5 )  +  ( 1  +  0 ) )  = ; 2 6
30992oveq1i 5884 . . . . . . . . . . . . 13  |-  ( ( 1  x.  0 )  +  1 )  =  ( 0  +  1 )
310309, 190, 2353eqtri 2320 . . . . . . . . . . . 12  |-  ( ( 1  x.  0 )  +  1 )  = ; 0
1
3114, 5, 11, 11, 71, 76, 11, 11, 5, 308, 310decma2c 10180 . . . . . . . . . . 11  |-  ( ( 1  x. ;; 2 5 0 )  +  (; 1 1  +  0 ) )  = ;; 2 6 1
3126, 21, 52, 11, 1, 303, 11, 16, 5, 311, 104decma2c 10180 . . . . . . . . . 10  |-  ( ( 1  x.  N )  + ;; 1 1 1 )  = ;;; 2 6 1 4
313117oveq1i 5884 . . . . . . . . . . . . . 14  |-  ( ( 3  x.  2 )  +  0 )  =  ( 6  +  0 )
314313, 273, 893eqtri 2320 . . . . . . . . . . . . 13  |-  ( ( 3  x.  2 )  +  0 )  = ; 0
6
31511, 21, 5, 5, 144, 268, 2, 24, 5, 307, 314decmac 10179 . . . . . . . . . . . 12  |-  ( (; 1
3  x.  2 )  +  ( 0  +  0 ) )  = ; 2
6
31677mul02i 9017 . . . . . . . . . . . . . 14  |-  ( 0  x.  2 )  =  0
317316oveq1i 5884 . . . . . . . . . . . . 13  |-  ( ( 0  x.  2 )  +  1 )  =  ( 0  +  1 )
318317, 190, 2353eqtri 2320 . . . . . . . . . . . 12  |-  ( ( 0  x.  2 )  +  1 )  = ; 0
1
31955, 5, 5, 11, 142, 235, 2, 11, 5, 315, 318decmac 10179 . . . . . . . . . . 11  |-  ( (;; 1 3 0  x.  2 )  +  1 )  = ;; 2 6 1
320 7t2e14 10222 . . . . . . . . . . 11  |-  ( 7  x.  2 )  = ; 1
4
3212, 56, 30, 139, 16, 11, 319, 320decmul1c 10187 . . . . . . . . . 10  |-  (;;; 1 3 0 7  x.  2 )  = ;;; 2 6 1 4
322312, 321eqtr4i 2319 . . . . . . . . 9  |-  ( ( 1  x.  N )  + ;; 1 1 1 )  =  (;;; 1 3 0 7  x.  2 )
3239, 10, 54, 20, 57, 53, 300, 302, 322modxp1i 13101 . . . . . . . 8  |-  ( ( 2 ^; 3 9 )  mod 
N )  =  (;; 1 1 1  mod 
N )
324 eqid 2296 . . . . . . . . 9  |- ; 3 9  = ; 3 9
32599, 77, 117mulcomli 8860 . . . . . . . . . . 11  |-  ( 2  x.  3 )  =  6
326325oveq1i 5884 . . . . . . . . . 10  |-  ( ( 2  x.  3 )  +  1 )  =  ( 6  +  1 )
327326, 159eqtri 2316 . . . . . . . . 9  |-  ( ( 2  x.  3 )  +  1 )  =  7
3282, 21, 27, 324, 18, 11, 327, 137decmul2c 10188 . . . . . . . 8  |-  ( 2  x. ; 3 9 )  = ; 7
8
329 eqid 2296 . . . . . . . . . 10  |- ;;; 2 3 0 9  = ;;; 2 3 0 9
330 eqid 2296 . . . . . . . . . . . 12  |- ;; 2 3 0  = ;; 2 3 0
33134, 5, 2, 330, 150decaddi 10184 . . . . . . . . . . 11  |-  (;; 2 3 0  +  2 )  = ;; 2 3 2
33234nn0cni 9993 . . . . . . . . . . . . 13  |- ; 2 3  e.  CC
333332addid1i 9015 . . . . . . . . . . . 12  |-  (; 2 3  +  0 )  = ; 2 3
334 4t2e8 9890 . . . . . . . . . . . . . 14  |-  ( 4  x.  2 )  =  8
335 2p2e4 9858 . . . . . . . . . . . . . 14  |-  ( 2  +  2 )  =  4
336334, 335oveq12i 5886 . . . . . . . . . . . . 13  |-  ( ( 4  x.  2 )  +  ( 2  +  2 ) )  =  ( 8  +  4 )
337 8p4e12 10197 . . . . . . . . . . . . 13  |-  ( 8  +  4 )  = ; 1
2
338336, 337eqtri 2316 . . . . . . . . . . . 12  |-  ( ( 4  x.  2 )  +  ( 2  +  2 ) )  = ; 1
2
339 5t4e20 10215 . . . . . . . . . . . . . 14  |-  ( 5  x.  4 )  = ; 2
0
34085, 187, 339mulcomli 8860 . . . . . . . . . . . . 13  |-  ( 4  x.  5 )  = ; 2
0
3412, 5, 21, 340, 174decaddi 10184 . . . . . . . . . . . 12  |-  ( ( 4  x.  5 )  +  3 )  = ; 2
3
3422, 3, 2, 21, 74, 333, 16, 21, 2, 338, 341decma2c 10180 . . . . . . . . . . 11  |-  ( ( 4  x. ; 2 5 )  +  (; 2 3  +  0 ) )  = ;; 1 2 3
343187mul01i 9018 . . . . . . . . . . . . 13  |-  ( 4  x.  0 )  =  0
344343oveq1i 5884 . . . . . . . . . . . 12  |-  ( ( 4  x.  0 )  +  2 )  =  ( 0  +  2 )
345344, 150, 1573eqtri 2320 . . . . . . . . . . 11  |-  ( ( 4  x.  0 )  +  2 )  = ; 0
2
3464, 5, 34, 2, 71, 331, 16, 2, 5, 342, 345decma2c 10180 . . . . . . . . . 10  |-  ( ( 4  x. ;; 2 5 0 )  +  (;; 2 3 0  +  2 ) )  = ;;; 1 2 3 2
347 4t3e12 10212 . . . . . . . . . . 11  |-  ( 4  x.  3 )  = ; 1
2
34811, 2, 27, 347, 146, 11, 164decaddci 10185 . . . . . . . . . 10  |-  ( ( 4  x.  3 )  +  9 )  = ; 2
1
3496, 21, 48, 27, 1, 329, 16, 11, 2, 346, 348decma2c 10180 . . . . . . . . 9  |-  ( ( 4  x.  N )  + ;;; 2 3 0 9 )  = ;;;; 1 2 3 2 1
3505, 11, 11, 11, 235, 233, 190, 146decadd 10181 . . . . . . . . . . . 12  |-  ( 1  + ; 1 1 )  = ; 1
2
351250oveq1i 5884 . . . . . . . . . . . . . 14  |-  ( ( 1  x.  1 )  +  1 )  =  ( 1  +  1 )
352351, 146, 1573eqtri 2320 . . . . . . . . . . . . 13  |-  ( ( 1  x.  1 )  +  1 )  = ; 0
2
35311, 11, 5, 11, 233, 304, 11, 2, 5, 253, 352decmac 10179 . . . . . . . . . . . 12  |-  ( (; 1
1  x.  1 )  +  ( 1  +  0 ) )  = ; 1
2
35452, 11, 11, 2, 303, 350, 11, 21, 5, 353, 256decmac 10179 . . . . . . . . . . 11  |-  ( (;; 1 1 1  x.  1 )  +  ( 1  + ; 1 1 ) )  = ;; 1 2 3
35552, 11, 5, 11, 303, 235, 11, 2, 5, 271, 352decmac 10179 . . . . . . . . . . 11  |-  ( (;; 1 1 1  x.  1 )  +  1 )  = ;; 1 1 2
35611, 11, 11, 11, 233, 233, 53, 2, 52, 354, 355decma2c 10180 . . . . . . . . . 10  |-  ( (;; 1 1 1  x. ; 1
1 )  + ; 1 1 )  = ;;; 1 2 3 2
35753nn0cni 9993 . . . . . . . . . . 11  |- ;; 1 1 1  e.  CC
358357mulid1i 8855 . . . . . . . . . 10  |-  (;; 1 1 1  x.  1 )  = ;; 1 1 1
35953, 52, 11, 303, 11, 52, 356, 358decmul2c 10188 . . . . . . . . 9  |-  (;; 1 1 1  x. ;; 1 1 1 )  = ;;;; 1 2 3 2 1
360349, 359eqtr4i 2319 . . . . . . . 8  |-  ( ( 4  x.  N )  + ;;; 2 3 0 9 )  =  (;; 1 1 1  x. ;; 1 1 1 )
3619, 10, 50, 51, 53, 49, 323, 328, 360mod2xi 13100 . . . . . . 7  |-  ( ( 2 ^; 7 8 )  mod 
N )  =  (;;; 2 3 0 9  mod 
N )
362 eqid 2296 . . . . . . . 8  |- ; 7 8  = ; 7 8
363 4p1e5 9865 . . . . . . . . 9  |-  ( 4  +  1 )  =  5
364223, 77, 320mulcomli 8860 . . . . . . . . 9  |-  ( 2  x.  7 )  = ; 1
4
36511, 16, 363, 364decsuc 10163 . . . . . . . 8  |-  ( ( 2  x.  7 )  +  1 )  = ; 1
5
366179, 77, 110mulcomli 8860 . . . . . . . 8  |-  ( 2  x.  8 )  = ; 1
6
3672, 30, 18, 362, 24, 11, 365, 366decmul2c 10188 . . . . . . 7  |-  ( 2  x. ; 7 8 )  = ;; 1 5 6
368 eqid 2296 . . . . . . . . 9  |- ;; 1 9 4  = ;; 1 9 4
3692, 16deccl 10154 . . . . . . . . . 10  |- ; 2 4  e.  NN0
370 eqid 2296 . . . . . . . . . . 11  |- ; 2 4  = ; 2 4
3712, 16, 363, 370decsuc 10163 . . . . . . . . . 10  |-  (; 2 4  +  1 )  = ; 2 5
372 eqid 2296 . . . . . . . . . . . 12  |- ; 2 3  = ; 2 3
3732, 21, 102, 372decsuc 10163 . . . . . . . . . . 11  |-  (; 2 3  +  1 )  = ; 2 4
37434, 5, 11, 27, 330, 130, 373, 201decadd 10181 . . . . . . . . . 10  |-  (;; 2 3 0  + ; 1 9 )  = ;; 2 4 9
375369, 371, 374decsucc 10167 . . . . . . . . 9  |-  ( (;; 2 3 0  + ; 1
9 )  +  1 )  = ;; 2 5 0
376 9p4e13 10204 . . . . . . . . 9  |-  ( 9  +  4 )  = ; 1
3
37748, 27, 45, 16, 329, 368, 375, 21, 376decaddc 10182 . . . . . . . 8  |-  (;;; 2 3 0 9  + ;; 1 9 4 )  = ;;; 2 5 0 3
378377, 1eqtr4i 2319 . . . . . . 7  |-  (;;; 2 3 0 9  + ;; 1 9 4 )  =  N
379 eqid 2296 . . . . . . . . 9  |- ; 9 1  = ; 9 1
380 eqid 2296 . . . . . . . . . . . 12  |- ; 1 5  = ; 1 5
381223addid2i 9016 . . . . . . . . . . . . 13  |-  ( 0  +  7 )  =  7
382381, 210eqtri 2316 . . . . . . . . . . . 12  |-  ( 0  +  7 )  = ; 0
7
38378, 190oveq12i 5886 . . . . . . . . . . . . 13  |-  ( ( 1  x.  2 )  +  ( 0  +  1 ) )  =  ( 2  +  1 )
384383, 82eqtri 2316 . . . . . . . . . . . 12  |-  ( ( 1  x.  2 )  +  ( 0  +  1 ) )  =  3
38511, 5, 30, 173, 381decaddi 10184 . . . . . . . . . . . 12  |-  ( ( 5  x.  2 )  +  7 )  = ; 1
7
38611, 3, 5, 30, 380, 382, 2, 30, 11, 384, 385decmac 10179 . . . . . . . . . . 11  |-  ( (; 1
5  x.  2 )  +  ( 0  +  7 ) )  = ; 3
7
38786, 150oveq12i 5886 . . . . . . . . . . . . 13  |-  ( ( 1  x.  5 )  +  ( 0  +  2 ) )  =  ( 5  +  2 )
388 5p2e7 9876 . . . . . . . . . . . . 13  |-  ( 5  +  2 )  =  7
389387, 388eqtri 2316 . . . . . . . . . . . 12  |-  ( ( 1  x.  5 )  +  ( 0  +  2 ) )  =  7
39011, 3, 5, 11, 380, 235, 3, 24, 2, 389, 193decmac 10179 . . . . . . . . . . 11  |-  ( (; 1
5  x.  5 )  +  1 )  = ; 7
6
3912, 3, 5, 11, 74, 304, 39, 24, 30, 386, 390decma2c 10180 . . . . . . . . . 10  |-  ( (; 1
5  x. ; 2 5 )  +  ( 1  +  0 ) )  = ;; 3 7 6
39239nn0cni 9993 . . . . . . . . . . . . 13  |- ; 1 5  e.  CC
393392mul01i 9018 . . . . . . . . . . . 12  |-  (; 1 5  x.  0 )  =  0
394393oveq1i 5884 . . . . . . . . . . 11  |-  ( (; 1
5  x.  0 )  +  3 )  =  ( 0  +  3 )
395394, 174, 2113eqtri 2320 . . . . . . . . . 10  |-  ( (; 1
5  x.  0 )  +  3 )  = ; 0
3
3964, 5, 11, 21, 71, 376, 39, 21, 5, 391, 395decma2c 10180 . . . . . . . . 9  |-  ( (; 1
5  x. ;; 2 5 0 )  +  ( 9  +  4 ) )  = ;;; 3 7 6 3
397100, 190oveq12i 5886 . . . . . . . . . . 11  |-  ( ( 1  x.  3 )  +  ( 0  +  1 ) )  =  ( 3  +  1 )
398397, 102eqtri 2316 . . . . . . . . . 10  |-  ( ( 1  x.  3 )  +  ( 0  +  1 ) )  =  4
39911, 3, 5, 11, 380, 235, 21, 24, 11, 398, 214decmac 10179 . . . . . . . . 9  |-  ( (; 1
5  x.  3 )  +  1 )  = ; 4
6
4006, 21, 27, 11, 1, 379, 39, 24, 16, 396, 399decma2c 10180 . . . . . . . 8  |-  ( (; 1
5  x.  N )  + ; 9 1 )  = ;;;; 3 7 6 3 6
40145, 16deccl 10154 . . . . . . . . 9  |- ;; 1 9 4  e.  NN0
402 eqid 2296 . . . . . . . . . 10  |- ; 7 7  = ; 7 7
40311, 30deccl 10154 . . . . . . . . . . 11  |- ; 1 7  e.  NN0
404403, 3deccl 10154 . . . . . . . . . 10  |- ;; 1 7 5  e.  NN0
405 eqid 2296 . . . . . . . . . . . 12  |- ;; 1 7 5  = ;; 1 7 5
406403nn0cni 9993 . . . . . . . . . . . . . 14  |- ; 1 7  e.  CC
407406addid2i 9016 . . . . . . . . . . . . 13  |-  ( 0  + ; 1 7 )  = ; 1
7
40811, 30, 167, 407decsuc 10163 . . . . . . . . . . . 12  |-  ( ( 0  + ; 1 7 )  +  1 )  = ; 1 8
409 7p5e12 10193 . . . . . . . . . . . 12  |-  ( 7  +  5 )  = ; 1
2
4105, 30, 403, 3, 210, 405, 408, 2, 409decaddc 10182 . . . . . . . . . . 11  |-  ( 7  + ;; 1 7 5 )  = ;; 1 8 2
411250, 146oveq12i 5886 . . . . . . . . . . . . 13  |-  ( ( 1  x.  1 )  +  ( 1  +  1 ) )  =  ( 1  +  2 )
412411, 255eqtri 2316 . . . . . . . . . . . 12  |-  ( ( 1  x.  1 )  +  ( 1  +  1 ) )  =  3
413135mulid1i 8855 . . . . . . . . . . . . . 14  |-  ( 9  x.  1 )  =  9
414413oveq1i 5884 . . . . . . . . . . . . 13  |-  ( ( 9  x.  1 )  +  8 )  =  ( 9  +  8 )
415 9p8e17 10208 . . . . . . . . . . . . 13  |-  ( 9  +  8 )  = ; 1
7
416414, 415eqtri 2316 . . . . . . . . . . . 12  |-  ( ( 9  x.  1 )  +  8 )  = ; 1
7
41711, 27, 11, 18, 130, 248, 11, 30, 11, 412, 416decmac 10179 . . . . . . . . . . 11  |-  ( (; 1
9  x.  1 )  +  (; 1 8  +  0 ) )  = ; 3 7
418187mulid1i 8855 . . . . . . . . . . . . 13  |-  ( 4  x.  1 )  =  4
419418oveq1i 5884 . . . . . . . . . . . 12  |-  ( ( 4  x.  1 )  +  2 )  =  ( 4  +  2 )
420 4p2e6 9873 . . . . . . . . . . . 12  |-  ( 4  +  2 )  =  6
421419, 420, 893eqtri 2320 . . . . . . . . . . 11  |-  ( ( 4  x.  1 )  +  2 )  = ; 0
6
42245, 16, 63, 2, 368, 410, 11, 24, 5, 417, 421decmac 10179 . . . . . . . . . 10  |-  ( (;; 1 9 4  x.  1 )  +  ( 7  + ;; 1 7 5 ) )  = ;; 3 7 6
423135mulid2i 8856 . . . . . . . . . . . . . 14  |-  ( 1  x.  9 )  =  9
424179addid2i 9016 . . . . . . . . . . . . . 14  |-  ( 0  +  8 )  =  8
425423, 424oveq12i 5886 . . . . . . . . . . . . 13  |-  ( ( 1  x.  9 )  +  ( 0  +  8 ) )  =  ( 9  +  8 )
426425, 415eqtri 2316 . . . . . . . . . . . 12  |-  ( ( 1  x.  9 )  +  ( 0  +  8 ) )  = ; 1
7
427 9t9e81 10242 . . . . . . . . . . . . 13  |-  ( 9  x.  9 )  = ; 8
1
428187, 79, 363addcomli 9020 . . . . . . . . . . . . 13  |-  ( 1  +  4 )  =  5
42918, 11, 16, 427, 428decaddi 10184 . . . . . . . . . . . 12  |-  ( ( 9  x.  9 )  +  4 )  = ; 8
5
43011, 27, 5, 16, 130, 189, 27, 3, 18, 426, 429decmac 10179 . . . . . . . . . . 11  |-  ( (; 1
9  x.  9 )  +  ( 0  +  4 ) )  = ;; 1 7 5
431 9t4e36 10237 . . . . . . . . . . . . 13  |-  ( 9  x.  4 )  = ; 3
6
432135, 187, 431mulcomli 8860 . . . . . . . . . . . 12  |-  ( 4  x.  9 )  = ; 3
6
433 7p6e13 10194 . . . . . . . . . . . . 13  |-  ( 7  +  6 )  = ; 1
3
434223, 95, 433addcomli 9020 . . . . . . . . . . . 12  |-  ( 6  +  7 )  = ; 1
3
43521, 24, 30, 432, 102, 21, 434decaddci 10185 . . . . . . . . . . 11  |-  ( ( 4  x.  9 )  +  7 )  = ; 4
3
43645, 16, 5, 30, 368, 210, 27, 21, 16, 430, 435decmac 10179 . . . . . . . . . 10  |-  ( (;; 1 9 4  x.  9 )  +  7 )  = ;;; 1 7 5 3
43711, 27, 30, 30, 130, 402, 401, 21, 404, 422, 436decma2c 10180 . . . . . . . . 9  |-  ( (;; 1 9 4  x. ; 1
9 )  + ; 7 7 )  = ;;; 3 7 6 3
438187mulid2i 8856 . . . . . . . . . . . . 13  |-  ( 1  x.  4 )  =  4
439438, 174oveq12i 5886 . . . . . . . . . . . 12  |-  ( ( 1  x.  4 )  +  ( 0  +  3 ) )  =  ( 4  +  3 )
440 4p3e7 9874 . . . . . . . . . . . 12  |-  ( 4  +  3 )  =  7
441439, 440eqtri 2316 . . . . . . . . . . 11  |-  ( ( 1  x.  4 )  +  ( 0  +  3 ) )  =  7
44221, 24, 159, 431decsuc 10163 . . . . . . . . . . 11  |-  ( ( 9  x.  4 )  +  1 )  = ; 3
7
44311, 27, 5, 11, 130, 235, 16, 30, 21, 441, 442decmac 10179 . . . . . . . . . 10  |-  ( (; 1
9  x.  4 )  +  1 )  = ; 7
7
444 4t4e16 10213 . . . . . . . . . 10  |-  ( 4  x.  4 )  = ; 1
6
44516, 45, 16, 368, 24, 11, 443, 444decmul1c 10187 . . . . . . . . 9  |-  (;; 1 9 4  x.  4 )  = ;; 7 7 6
446401, 45, 16, 368, 24, 37, 437, 445decmul2c 10188 . . . . . . . 8  |-  (;; 1 9 4  x. ;; 1 9 4 )  = ;;;; 3 7 6 3 6
447400, 446eqtr4i 2319 . . . . . . 7  |-  ( (; 1
5  x.  N )  + ; 9 1 )  =  (;; 1 9 4  x. ;; 1 9 4 )
44810, 43, 44, 47, 42, 49, 361, 367, 378, 447mod2xnegi 13102 . . . . . 6  |-  ( ( 2 ^;; 1 5 6 )  mod 
N )  =  (; 9
1  mod  N )
449 eqid 2296 . . . . . . 7  |- ;; 1 5 6  = ;; 1 5 6
450131, 190oveq12i 5886 . . . . . . . . 9  |-  ( ( 2  x.  1 )  +  ( 0  +  1 ) )  =  ( 2  +  1 )
451450, 82eqtri 2316 . . . . . . . 8  |-  ( ( 2  x.  1 )  +  ( 0  +  1 ) )  =  3
45285, 77, 171mulcomli 8860 . . . . . . . . . 10  |-  ( 2  x.  5 )  =  10
453452, 172eqtri 2316 . . . . . . . . 9  |-  ( 2  x.  5 )  = ; 1
0
45411, 5, 190, 453decsuc 10163 . . . . . . . 8  |-  ( ( 2  x.  5 )  +  1 )  = ; 1
1
45511, 3, 5, 11, 380, 235, 2, 11, 11, 451, 454decma2c 10180 . . . . . . 7  |-  ( ( 2  x. ; 1 5 )  +  1 )  = ; 3 1
456 6t2e12 10217 . . . . . . . 8  |-  ( 6  x.  2 )  = ; 1
2
45795, 77, 456mulcomli 8860 . . . . . . 7  |-  ( 2  x.  6 )  = ; 1
2
4582, 39, 24, 449, 2, 11, 455, 457decmul2c 10188 . . . . . 6  |-  ( 2  x. ;; 1 5 6 )  = ;; 3 1 2
459 eqid 2296 . . . . . . . 8  |- ;; 7 7 2  = ;; 7 7 2
46030, 30, 167, 402decsuc 10163 . . . . . . . . 9  |-  (; 7 7  +  1 )  = ; 7 8
461223addid1i 9015 . . . . . . . . . . 11  |-  ( 7  +  0 )  =  7
462461, 210eqtri 2316 . . . . . . . . . 10  |-  ( 7  +  0 )  = ; 0
7
463117, 150oveq12i 5886 . . . . . . . . . . 11  |-  ( ( 3  x.  2 )  +  ( 0  +  2 ) )  =  ( 6  +  2 )
464 6p2e8 9880 . . . . . . . . . . 11  |-  ( 6  +  2 )  =  8
465463, 464eqtri 2316 . . . . . . . . . 10  |-  ( ( 3  x.  2 )  +  ( 0  +  2 ) )  =  8
466223, 85, 409addcomli 9020 . . . . . . . . . . 11  |-  ( 5  +  7 )  = ; 1
2
46711, 3, 30, 196, 146, 2, 466decaddci 10185 . . . . . . . . . 10  |-  ( ( 3  x.  5 )  +  7 )  = ; 2
2
4682, 3, 5, 30, 74, 462, 21, 2, 2, 465, 467decma2c 10180 . . . . . . . . 9  |-  ( ( 3  x. ; 2 5 )  +  ( 7  +  0 ) )  = ; 8 2
46999mul01i 9018 . . . . . . . . . . 11  |-  ( 3  x.  0 )  =  0
470469oveq1i 5884 . . . . . . . . . 10  |-  ( ( 3  x.  0 )  +  8 )  =  ( 0  +  8 )
471470, 424, 2663eqtri 2320 . . . . . . . . 9  |-  ( ( 3  x.  0 )  +  8 )  = ; 0
8
4724, 5, 30, 18, 71, 460, 21, 18, 5, 468, 471decma2c 10180 . . . . . . . 8  |-  ( ( 3  x. ;; 2 5 0 )  +  (; 7 7  +  1 ) )  = ;; 8 2 8
473216oveq1i 5884 . . . . . . . . 9  |-  ( ( 3  x.  3 )  +  2 )  =  ( 9  +  2 )
474473, 163eqtri 2316 . . . . . . . 8  |-  ( ( 3  x.  3 )  +  2 )  = ; 1
1
4756, 21, 37, 2, 1, 459, 21, 11, 11, 472, 474decma2c 10180 . . . . . . 7  |-  ( ( 3  x.  N )  + ;; 7 7 2 )  = ;;; 8 2 8 1
476190oveq2i 5885 . . . . . . . . . 10  |-  ( ( 9  x.  9 )  +  ( 0  +  1 ) )  =  ( ( 9  x.  9 )  +  1 )
47718, 11, 146, 427decsuc 10163 . . . . . . . . . 10  |-  ( ( 9  x.  9 )  +  1 )  = ; 8
2
478476, 477eqtri 2316 . . . . . . . . 9  |-  ( ( 9  x.  9 )  +  ( 0  +  1 ) )  = ; 8
2
479423oveq1i 5884 . . . . . . . . . 10  |-  ( ( 1  x.  9 )  +  9 )  =  ( 9  +  9 )
480 9p9e18 10209 . . . . . . . . . 10  |-  ( 9  +  9 )  = ; 1
8
481479, 480eqtri 2316 . . . . . . . . 9  |-  ( ( 1  x.  9 )  +  9 )  = ; 1
8
48227, 11, 5, 27, 379, 186, 27, 18, 11, 478, 481decmac 10179 . . . . . . . 8  |-  ( (; 9
1  x.  9 )  +  9 )  = ;; 8 2 8
48342nn0cni 9993 . . . . . . . . 9  |- ; 9 1  e.  CC
484483mulid1i 8855 . . . . . . . 8  |-  (; 9 1  x.  1 )  = ; 9 1
48542, 27, 11, 379, 11, 27, 482, 484decmul2c 10188 . . . . . . 7  |-  (; 9 1  x. ; 9 1 )  = ;;; 8 2 8 1
486475, 485eqtr4i 2319 . . . . . 6  |-  ( ( 3  x.  N )  + ;; 7 7 2 )  =  (; 9
1  x. ; 9 1 )
4879, 10, 40, 41, 42, 38, 448, 458, 486mod2xi 13100 . . . . 5  |-  ( ( 2 ^;; 3 1 2 )  mod 
N )  =  (;; 7 7 2  mod 
N )
488 eqid 2296 . . . . . 6  |- ;; 3 1 2  = ;; 3 1 2
489 eqid 2296 . . . . . . . . 9  |- ; 3 1  = ; 3 1
490325oveq1i 5884 . . . . . . . . . 10  |-  ( ( 2  x.  3 )  +  0 )  =  ( 6  +  0 )
491490, 273eqtri 2316 . . . . . . . . 9  |-  ( ( 2  x.  3 )  +  0 )  =  6
492131, 157eqtri 2316 . . . . . . . . 9  |-  ( 2  x.  1 )  = ; 0
2
4932, 21, 11, 489, 2, 5, 491, 492decmul2c 10188 . . . . . . . 8  |-  ( 2  x. ; 3 1 )  = ; 6
2
494493oveq1i 5884 . . . . . . 7  |-  ( ( 2  x. ; 3 1 )  +  0 )  =  (; 6
2  +  0 )
49525nn0cni 9993 . . . . . . . 8  |- ; 6 2  e.  CC
496495addid1i 9015 . . . . . . 7  |-  (; 6 2  +  0 )  = ; 6 2
497494, 496eqtri 2316 . . . . . 6  |-  ( ( 2  x. ; 3 1 )  +  0 )  = ; 6 2
4982, 22, 2, 488, 16, 5, 497, 126decmul2c 10188 . . . . 5  |-  ( 2  x. ;; 3 1 2 )  = ;; 6 2 4
499 eqid 2296 . . . . . . 7  |- ;; 2 7 0  = ;; 2 7 0
50030, 11deccl 10154 . . . . . . 7  |- ; 7 1  e.  NN0
501 eqid 2296 . . . . . . . . 9  |- ; 7 1  = ; 7 1
502 7p2e9 9883 . . . . . . . . . 10  |-  ( 7  +  2 )  =  9
503223, 77, 502addcomli 9020 . . . . . . . . 9  |-  ( 2  +  7 )  =  9
5042, 30, 30, 11, 168, 501, 503, 167decadd 10181 . . . . . . . 8  |-  (; 2 7  + ; 7 1 )  = ; 9
8
505135addid1i 9015 . . . . . . . . . 10  |-  ( 9  +  0 )  =  9
506505, 186eqtri 2316 . . . . . . . . 9  |-  ( 9  +  0 )  = ; 0
9
50752, 27deccl 10154 . . . . . . . . 9  |- ;; 1 1 9  e.  NN0
508 eqid 2296 . . . . . . . . . 10  |- ;; 2 3 8  = ;; 2 3 8
509507nn0cni 9993 . . . . . . . . . . 11  |- ;; 1 1 9  e.  CC
510509addid2i 9016 . . . . . . . . . 10  |-  ( 0  + ;; 1 1 9 )  = ;; 1 1 9
51111, 11, 2, 233, 255decaddi 10184 . . . . . . . . . . 11  |-  (; 1 1  +  2 )  = ; 1 3
512125, 80oveq12i 5886 . . . . . . . . . . . 12  |-  ( ( 2  x.  2 )  +  ( 1  +  0 ) )  =  ( 4  +  1 )
513512, 363eqtri 2316 . . . . . . . . . . 11  |-  ( ( 2  x.  2 )  +  ( 1  +  0 ) )  =  5
514117oveq1i 5884 . . . . . . . . . . . 12  |-  ( ( 3  x.  2 )  +  3 )  =  ( 6  +  3 )
515514, 147, 1863eqtri 2320 . . . . . . . . . . 11  |-  ( ( 3  x.  2 )  +  3 )  = ; 0
9
5162, 21, 11, 21, 372, 511, 2, 27, 5, 513, 515decmac 10179 . . . . . . . . . 10  |-  ( (; 2
3  x.  2 )  +  (; 1 1  +  2 ) )  = ; 5 9
517 9p6e15 10206 . . . . . . . . . . . 12  |-  ( 9  +  6 )  = ; 1
5
518135, 95, 517addcomli 9020 . . . . . . . . . . 11  |-  ( 6  +  9 )  = ; 1
5
51911, 24, 27, 110, 146, 3, 518decaddci 10185 . . . . . . . . . 10  |-  ( ( 8  x.  2 )  +  9 )  = ; 2
5
52034, 18, 52, 27, 508, 510, 2, 3, 2, 516, 519decmac 10179 . . . . . . . . 9  |-  ( (;; 2 3 8  x.  2 )  +  ( 0  + ;; 1 1 9 ) )  = ;; 5 9 5
521190oveq2i 5885 . . . . . . . . . . . 12  |-  ( ( 2  x.  5 )  +  ( 0  +  1 ) )  =  ( ( 2  x.  5 )  +  1 )
522521, 454eqtri 2316 . . . . . . . . . . 11  |-  ( ( 2  x.  5 )  +  ( 0  +  1 ) )  = ; 1
1
5232, 21, 5, 16, 372, 189, 3, 27, 11, 522, 198decmac 10179 . . . . . . . . . 10  |-  ( (; 2
3  x.  5 )  +  ( 0  +  4 ) )  = ;; 1 1 9
52434, 18, 5, 27, 508, 186, 3, 27, 16, 523, 202decmac 10179 . . . . . . . . 9  |-  ( (;; 2 3 8  x.  5 )  +  9 )  = ;;; 1 1 9 9
5252, 3, 5, 27, 74, 506, 35, 27, 507, 520, 524decma2c 10180 . . . . . . . 8  |-  ( (;; 2 3 8  x. ; 2
5 )  +  ( 9  +  0 ) )  = ;;; 5 9 5 9
52635nn0cni 9993 . . . . . . . . . . 11  |- ;; 2 3 8  e.  CC
527526mul01i 9018 . . . . . . . . . 10  |-  (;; 2 3 8  x.  0 )  =  0
528527oveq1i 5884 . . . . . . . . 9  |-  ( (;; 2 3 8  x.  0 )  +  8 )  =  ( 0  +  8 )
529528, 424, 2663eqtri 2320 . . . . . . . 8  |-  ( (;; 2 3 8  x.  0 )  +  8 )  = ; 0 8
5304, 5, 27, 18, 71, 504, 35, 18, 5, 525, 529decma2c 10180 . . . . . . 7  |-  ( (;; 2 3 8  x. ;; 2 5 0 )  +  (; 2 7  + ; 7 1 ) )  = ;;;; 5 9 5 9 8
531325, 190oveq12i 5886 . . . . . . . . . . . 12  |-  ( ( 2  x.  3 )  +  ( 0  +  1 ) )  =  ( 6  +  1 )
532531, 159eqtri 2316 . . . . . . . . . . 11  |-  ( ( 2  x.  3 )  +  ( 0  +  1 ) )  =  7
5332, 21, 5, 2, 372, 157, 21, 11, 11, 532, 474decmac 10179 . . . . . . . . . 10  |-  ( (; 2
3  x.  3 )  +  2 )  = ; 7
1
53421, 34, 18, 508, 16, 2, 533, 221decmul1c 10187 . . . . . . . . 9  |-  (;; 2 3 8  x.  3 )  = ;; 7 1 4
535534oveq1i 5884 . . . . . . . 8  |-  ( (;; 2 3 8  x.  3 )  +  0 )  =  (;; 7 1 4  +  0 )
536500, 16deccl 10154 . . . . . . . . . 10  |- ;; 7 1 4  e.  NN0
537536nn0cni 9993 . . . . . . . . 9  |- ;; 7 1 4  e.  CC
538537addid1i 9015 . . . . . . . 8  |-  (;; 7 1 4  +  0 )  = ;; 7 1 4
539535, 538eqtri 2316 . . . . . . 7  |-  ( (;; 2 3 8  x.  3 )  +  0 )  = ;; 7 1 4
5406, 21, 31, 5, 1, 499, 35, 16, 500, 530, 539decma2c 10180 . . . . . 6  |-  ( (;; 2 3 8  x.  N )  + ;; 2 7 0 )  = ;;;;; 5 9 5 9 8 4
54139, 16deccl 10154 . . . . . . 7  |- ;; 1 5 4  e.  NN0
542 eqid 2296 . . . . . . . 8  |- ;; 1 5 4  = ;; 1 5 4
5433, 16deccl 10154 . . . . . . . . 9  |- ; 5 4  e.  NN0
544543, 5deccl 10154 . . . . . . . 8  |- ;; 5 4 0  e.  NN0
5453, 3deccl 10154 . . . . . . . . 9  |- ; 5 5  e.  NN0
546 eqid 2296 . . . . . . . . . 10  |- ;; 5 4 0  = ;; 5 4 0
547 eqid 2296 . . . . . . . . . . 11  |- ; 5 4  = ; 5 4
54885addid2i 9016 . . . . . . . . . . 11  |-  ( 0  +  5 )  =  5
5495, 11, 3, 16, 235, 547, 548, 428decadd 10181 . . . . . . . . . 10  |-  ( 1  + ; 5 4 )  = ; 5
5
55085addid1i 9015 . . . . . . . . . 10  |-  ( 5  +  0 )  =  5
55111, 3, 543, 5, 380, 546, 549, 550decadd 10181 . . . . . . . . 9  |-  (; 1 5  + ;; 5 4 0 )  = ;; 5 5 5
552 eqid 2296 . . . . . . . . . . 11  |- ; 5 5  = ; 5 5
5533, 3, 88, 552decsuc 10163 . . . . . . . . . 10  |-  (; 5 5  +  1 )  = ; 5 6
554 7t7e49 10227 . . . . . . . . . . 11  |-  ( 7  x.  7 )  = ; 4
9
555 5p5e10 9879 . . . . . . . . . . . 12  |-  ( 5  +  5 )  =  10
556555, 172eqtri 2316 . . . . . . . . . . 11  |-  ( 5  +  5 )  = ; 1
0
55716, 27, 11, 5, 554, 556, 363, 505decadd 10181 . . . . . . . . . 10  |-  ( ( 7  x.  7 )  +  ( 5  +  5 ) )  = ; 5
9
55816, 27, 24, 554, 363, 3, 517decaddci 10185 . . . . . . . . . 10  |-  ( ( 7  x.  7 )  +  6 )  = ; 5
5
55930, 30, 3, 24, 402, 553, 30, 3, 3, 557, 558decmac 10179 . . . . . . . . 9  |-  ( (; 7
7  x.  7 )  +  (; 5 5  +  1 ) )  = ;; 5 9 5
56085, 187, 197addcomli 9020 . . . . . . . . . 10  |-  ( 4  +  5 )  =  9
56111, 16, 3, 364, 560decaddi 10184 . . . . . . . . 9  |-  ( ( 2  x.  7 )  +  5 )  = ; 1
9
56237, 2, 545, 3, 459, 551, 30, 27, 11, 559, 561decmac 10179 . . . . . . . 8  |-  ( (;; 7 7 2  x.  7 )  +  (; 1
5  + ;; 5 4 0 ) )  = ;;; 5 9 5 9
563548oveq2i 5885 . . . . . . . . . . 11  |-  ( ( 7  x.  7 )  +  ( 0  +  5 ) )  =  ( ( 7  x.  7 )  +  5 )
564 9p5e14 10205 . . . . . . . . . . . 12  |-  ( 9  +  5 )  = ; 1
4
56516, 27, 3, 554, 363, 16, 564decaddci 10185 . . . . . . . . . . 11  |-  ( ( 7  x.  7 )  +  5 )  = ; 5
4
566563, 565eqtri 2316 . . . . . . . . . 10  |-  ( ( 7  x.  7 )  +  ( 0  +  5 ) )  = ; 5
4
56716, 363, 554decsucc 10167 . . . . . . . . . 10  |-  ( ( 7  x.  7 )  +  1 )  = ; 5
0
56830, 30, 5, 11, 402, 281, 30, 5, 3, 566, 567decmac 10179 . . . . . . . . 9  |-  ( (; 7
7  x.  7 )  +  ( 0  +  1 ) )  = ;; 5 4 0
569 4p4e8 9875 . . . . . . . . . 10  |-  ( 4  +  4 )  =  8
57011, 16, 16, 364, 569decaddi 10184 . . . . . . . . 9  |-  ( ( 2  x.  7 )  +  4 )  = ; 1
8
57137, 2, 5, 16, 459, 103, 30, 18, 11, 568, 570decmac 10179 . . . . . . . 8  |-  ( (;; 7 7 2  x.  7 )  +  4 )  = ;;; 5 4 0 8
57230, 30, 39, 16, 402, 542, 38, 18, 544, 562, 571decma2c 10180 . . . . . . 7  |-  ( (;; 7 7 2  x. ; 7
7 )  + ;; 1 5 4 )  = ;;;; 5 9 5 9 8
57311, 16, 363, 320decsuc 10163 . . . . . . . . . . 11  |-  ( ( 7  x.  2 )  +  1 )  = ; 1
5
5742, 30, 30, 402, 16, 11, 573, 320decmul1c 10187 . . . . . . . . . 10  |-  (; 7 7  x.  2 )  = ;; 1 5 4
575574oveq1i 5884 . . . . . . . . 9  |-  ( (; 7
7  x.  2 )  +  0 )  =  (;; 1 5 4  +  0 )
576541nn0cni 9993 . . . . . . . . . 10  |- ;; 1 5 4  e.  CC
577576addid1i 9015 . . . . . . . . 9  |-  (;; 1 5 4  +  0 )  = ;; 1 5 4
578575, 577eqtri 2316 . . . . . . . 8  |-  ( (; 7
7  x.  2 )  +  0 )  = ;; 1 5 4
5792, 37, 2, 459, 16, 5, 578, 126decmul1c 10187 . . . . . . 7  |-  (;; 7 7 2  x.  2 )  = ;;; 1 5 4 4
58038, 37, 2, 459, 16, 541, 572, 579decmul2c 10188 . . . . . 6  |-  (;; 7 7 2  x. ;; 7 7 2 )  = ;;;;; 5 9 5 9 8 4
581540, 580eqtr4i 2319 . . . . 5  |-  ( (;; 2 3 8  x.  N )  + ;; 2 7 0 )  =  (;; 7 7 2  x. ;; 7 7 2 )
5829, 10, 33, 36, 38, 32, 487, 498, 581mod2xi 13100 . . . 4  |-  ( ( 2 ^;; 6 2 4 )  mod 
N )  =  (;; 2 7 0  mod 
N )
583 eqid 2296 . . . . 5  |- ;; 6 2 4  = ;; 6 2 4
584 eqid 2296 . . . . . . . 8  |- ; 6 2  = ; 6 2
585457oveq1i 5884 . . . . . . . . 9  |-  ( ( 2  x.  6 )  +  0 )  =  (; 1 2  +  0 )
58612nn0cni 9993 . . . . . . . . . 10  |- ; 1 2  e.  CC
587586addid1i 9015 . . . . . . . . 9  |-  (; 1 2  +  0 )  = ; 1 2
588585, 587eqtri 2316 . . . . . . . 8  |-  ( ( 2  x.  6 )  +  0 )  = ; 1
2
5892, 24, 2, 584, 16, 5, 588, 126decmul2c 10188 . . . . . . 7  |-  ( 2  x. ; 6 2 )  = ;; 1 2 4
590589oveq1i 5884 . . . . . 6  |-  ( ( 2  x. ; 6 2 )  +  0 )  =  (;; 1 2 4  +  0 )
59117nn0cni 9993 . . . . . . 7  |- ;; 1 2 4  e.  CC
592591addid1i 9015 . . . . . 6  |-  (;; 1 2 4  +  0 )  = ;; 1 2 4
593590, 592eqtri 2316 . . . . 5  |-  ( ( 2  x. ; 6 2 )  +  0 )  = ;; 1 2 4
594187, 77, 334mulcomli 8860 . . . . . 6  |-  ( 2  x.  4 )  =  8
595594, 266eqtri 2316 . . . . 5  |-  ( 2  x.  4 )  = ; 0
8
5962, 25, 16, 583, 18, 5, 593, 595decmul2c 10188 . . . 4  |-  ( 2  x. ;; 6 2 4 )  = ;;; 1 2 4 8
597 eqid 2296 . . . . . 6  |- ;; 3 1 3  = ;; 3 1 3
59821, 11, 27, 489, 102, 240decaddci2 10186 . . . . . . 7  |-  (; 3 1  +  9 )  = ; 4 0
599187addid1i 9015 . . . . . . . . 9  |-  ( 4  +  0 )  =  4
600599, 103eqtri 2316 . . . . . . . 8  |-  ( 4  +  0 )  = ; 0
4
60111, 16deccl 10154 . . . . . . . 8  |- ; 1 4  e.  NN0
602 eqid 2296 . . . . . . . . 9  |- ; 2 9  = ; 2 9
603601nn0cni 9993 . . . . . . . . . 10  |- ; 1 4  e.  CC
604603addid2i 9016 . . . . . . . . 9  |-  ( 0  + ; 1 4 )  = ; 1
4
605125, 255oveq12i 5886 . . . . . . . . . 10  |-  ( ( 2  x.  2 )  +  ( 1  +  2 ) )  =  ( 4  +  3 )
606605, 440eqtri 2316 . . . . . . . . 9  |-  ( ( 2  x.  2 )  +  ( 1  +  2 ) )  =  7
60711, 18, 16, 136, 146, 2, 337decaddci 10185 . . . . . . . . 9  |-  ( ( 9  x.  2 )  +  4 )  = ; 2
2
6082, 27, 11, 16, 602, 604, 2, 2, 2, 606, 607decmac 10179 . . . . . . . 8  |-  ( (; 2
9  x.  2 )  +  ( 0  + ; 1
4 ) )  = ; 7
2
609188oveq2i 5885 . . . . . . . . . 10  |-  ( ( 2  x.  5 )  +  ( 0  +  4 ) )  =  ( ( 2  x.  5 )  +  4 )
61011, 5, 16, 453, 188decaddi 10184 . . . . . . . . . 10  |-  ( ( 2  x.  5 )  +  4 )  = ; 1
4
611609, 610eqtri 2316 . . . . . . . . 9  |-  ( ( 2  x.  5 )  +  ( 0  +  4 ) )  = ; 1
4
612 9t5e45 10238 . . . . . . . . . 10  |-  ( 9  x.  5 )  = ; 4
5
61316, 3, 16, 612, 197decaddi 10184 . . . . . . . . 9  |-  ( ( 9  x.  5 )  +  4 )  = ; 4
9
6142, 27, 5, 16, 602, 103, 3, 27, 16, 611, 613decmac 10179 . . . . . . . 8  |-  ( (; 2
9  x.  5 )  +  4 )  = ;; 1 4 9
6152, 3, 5, 16, 74, 600, 28, 27, 601, 608, 614decma2c 10180 . . . . . . 7  |-  ( (; 2
9  x. ; 2 5 )  +  ( 4  +  0 ) )  = ;; 7 2 9
616152mul01i 9018 . . . . . . . . 9  |-  (; 2 9  x.  0 )  =  0
617616oveq1i 5884 . . . . . . . 8  |-  ( (; 2
9  x.  0 )  +  0 )  =  ( 0  +  0 )
618617, 251, 2673eqtri 2320 . . . . . . 7  |-  ( (; 2
9  x.  0 )  +  0 )  = ; 0
0
6194, 5, 16, 5, 71, 598, 28, 5, 5, 615, 618decma2c 10180 . . . . . 6  |-  ( (; 2
9  x. ;; 2 5 0 )  +  (; 3 1  +  9 ) )  = ;;; 7 2 9 0
620325, 174oveq12i 5886 . . . . . . . 8  |-  ( ( 2  x.  3 )  +  ( 0  +  3 ) )  =  ( 6  +  3 )
621620, 147eqtri 2316 . . . . . . 7  |-  ( ( 2  x.  3 )  +  ( 0  +  3 ) )  =  9
622 9t3e27 10236 . . . . . . . 8  |-  ( 9  x.  3 )  = ; 2
7
623 7p3e10 9884 . . . . . . . 8  |-  ( 7  +  3 )  =  10
6242, 30, 21, 622, 82, 623decaddci2 10186 . . . . . . 7  |-  ( ( 9  x.  3 )  +  3 )  = ; 3
0
6252, 27, 5, 21, 602, 211, 21, 5, 21, 621, 624decmac 10179 . . . . . 6  |-  ( (; 2
9  x.  3 )  +  3 )  = ; 9
0
6266, 21, 22, 21, 1, 597, 28, 5, 27, 619, 625decma2c 10180 . . . . 5  |-  ( (; 2
9  x.  N )  + ;; 3 1 3 )  = ;;;; 7 2 9 0 0
62763, 27deccl 10154 . . . . . . . . 9  |- ;; 1 8 9  e.  NN0
628 eqid 2296 . . . . . . . . . 10  |- ;; 1 8 9  = ;; 1 8 9
629179, 187, 337addcomli 9020 . . . . . . . . . . . 12  |-  ( 4  +  8 )  = ; 1
2
63011, 16, 18, 320, 146, 2, 629decaddci 10185 . . . . . . . . . . 11  |-  ( ( 7  x.  2 )  +  8 )  = ; 2
2
6312, 30, 11, 18, 168, 248, 2, 2, 2, 606, 630decmac 10179 . . . . . . . . . 10  |-  ( (; 2
7  x.  2 )  +  (; 1 8  +  0 ) )  = ; 7 2
632316oveq1i 5884 . . . . . . . . . . 11  |-  ( ( 0  x.  2 )  +  9 )  =  ( 0  +  9 )
633632, 201, 1863eqtri 2320 . . . . . . . . . 10  |-  ( ( 0  x.  2 )  +  9 )  = ; 0
9
63431, 5, 63, 27, 499, 628, 2, 27, 5, 631, 633decmac 10179 . . . . . . . . 9  |-  ( (;; 2 7 0  x.  2 )  + ;; 1 8 9 )  = ;; 7 2 9
63530, 2, 30, 168, 27, 16, 570, 554decmul1c 10187 . . . . . . . . . . . 12  |-  (; 2 7  x.  7 )  = ;; 1 8 9
636635oveq1i 5884 . . . . . . . . . . 11  |-  ( (; 2
7  x.  7 )  +  0 )  =  (;; 1 8 9  +  0 )
637627nn0cni 9993 . . . . . . . . . . . 12  |- ;; 1 8 9  e.  CC
638637addid1i 9015 . . . . . . . . . . 11  |-  (;; 1 8 9  +  0 )  = ;; 1 8 9
639636, 638eqtri 2316 . . . . . . . . . 10  |-  ( (; 2
7  x.  7 )  +  0 )  = ;; 1 8 9
640223mul02i 9017 . . . . . . . . . . 11  |-  ( 0  x.  7 )  =  0
641640, 267eqtri 2316 . . . . . . . . . 10  |-  ( 0  x.  7 )  = ; 0
0
64230, 31, 5, 499, 5, 5, 639, 641decmul1c 10187 . . . . . . . . 9  |-  (;; 2 7 0  x.  7 )  = ;;; 1 8 9 0
64332, 2, 30, 168, 5, 627, 634, 642decmul2c 10188 . . . . . . . 8  |-  (;; 2 7 0  x. ; 2 7 )  = ;;; 7 2 9 0
644643oveq1i 5884 . . . . . . 7  |-  ( (;; 2 7 0  x. ; 2
7 )  +  0 )  =  (;;; 7 2 9 0  +  0 )
64530, 2deccl 10154 . . . . . . . . . . 11  |- ; 7 2  e.  NN0
646645, 27deccl 10154 . . . . . . . . . 10  |- ;; 7 2 9  e.  NN0
647646, 5deccl 10154 . . . . . . . . 9  |- ;;; 7 2 9 0  e.  NN0
648647nn0cni 9993 . . . . . . . 8  |- ;;; 7 2 9 0  e.  CC
649648addid1i 9015 . . . . . . 7  |-  (;;; 7 2 9 0  +  0 )  = ;;; 7 2 9 0
650644, 649eqtri 2316 . . . . . 6  |-  ( (;; 2 7 0  x. ; 2
7 )  +  0 )  = ;;; 7 2 9 0
65132nn0cni 9993 . . . . . . . 8  |- ;; 2 7 0  e.  CC
652651mul01i 9018 . . . . . . 7  |-  (;; 2 7 0  x.  0 )  =  0
653652, 267eqtri 2316 . . . . . 6  |-  (;; 2 7 0  x.  0 )  = ; 0 0
65432, 31, 5, 499, 5, 5, 650, 653decmul2c 10188 . . . . 5  |-  (;; 2 7 0  x. ;; 2 7 0 )  = ;;;; 7 2 9 0 0
655626, 654eqtr4i 2319 . . . 4  |-  ( (; 2
9  x.  N )  + ;; 3 1 3 )  =  (;; 2 7 0  x. ;; 2 7 0 )
6569, 10, 26, 29, 32, 23, 582, 596, 655mod2xi 13100 . . 3  |-  ( ( 2 ^;;; 1 2 4 8 )  mod  N )  =  (;; 3 1 3  mod  N
)
657 cu2 11217 . . . 4  |-  ( 2 ^ 3 )  =  8
658657oveq1i 5884 . . 3  |-  ( ( 2 ^ 3 )  mod  N )  =  ( 8  mod  N
)
659 eqid 2296 . . . 4  |- ;;; 1 2 4 8  = ;;; 1 2 4 8
660 eqid 2296 . . . . 5  |- ;; 1 2 4  = ;; 1 2 4
66112, 16, 363, 660decsuc 10163 . . . 4  |-  (;; 1 2 4  +  1 )  = ;; 1 2 5
662 8p3e11 10196 . . . 4  |-  ( 8  +  3 )  = ; 1
1
66317, 18, 21, 659, 661, 11, 662decaddci 10185 . . 3  |-  (;;; 1 2 4 8  +  3 )  = ;;; 1 2 5 1
6649nncni 9772 . . . . . . 7  |-  N  e.  CC
665664mulid2i 8856 . . . . . 6  |-  ( 1  x.  N )  =  N
666665, 1eqtri 2316 . . . . 5  |-  ( 1  x.  N )  = ;;; 2 5 0 3
6676, 21, 102, 666decsuc 10163 . . . 4  |-  ( ( 1  x.  N )  +  1 )  = ;;; 2 5 0 4
668190oveq2i 5885 . . . . . . 7  |-  ( ( 3  x.  8 )  +  ( 0  +  1 ) )  =  ( ( 3  x.  8 )  +  1 )
669179, 99, 221mulcomli 8860 . . . . . . . 8  |-  ( 3  x.  8 )  = ; 2
4
6702, 16, 363, 669decsuc 10163 . . . . . . 7  |-  ( ( 3  x.  8 )  +  1 )  = ; 2
5
671668, 670eqtri 2316 . . . . . 6  |-  ( ( 3  x.  8 )  +  ( 0  +  1 ) )  = ; 2
5
672179mulid2i 8856 . . . . . . . 8  |-  ( 1  x.  8 )  =  8
673672oveq1i 5884 . . . . . . 7  |-  ( ( 1  x.  8 )  +  2 )  =  ( 8  +  2 )
674 8p2e10 9885 . . . . . . 7  |-  ( 8  +  2 )  =  10
675673, 674, 1723eqtri 2320 . . . . . 6  |-  ( ( 1  x.  8 )  +  2 )  = ; 1
0
67621, 11, 5, 2, 489, 157, 18, 5, 11, 671, 675decmac 10179 . . . . 5  |-  ( (; 3
1  x.  8 )  +  2 )  = ;; 2 5 0
67718, 22, 21, 597, 16, 2, 676, 669decmul1c 10187 . . . 4  |-  (;; 3 1 3  x.  8 )  = ;;; 2 5 0 4
678667, 677eqtr4i 2319 . . 3  |-  ( ( 1  x.  N )  +  1 )  =  (;; 3 1 3  x.  8 )
6799, 10, 19, 20, 23, 11, 21, 18, 656, 658, 663, 678modxai 13099 . 2  |-  ( ( 2 ^;;; 1 2 5 1 )  mod  N )  =  ( 1  mod 
N )
680 eqid 2296 . . . 4  |- ;;; 1 2 5 1  = ;;; 1 2 5 1
681 eqid 2296 . . . . . 6  |- ;; 1 2 5  = ;; 1 2 5
682 eqid 2296 . . . . . . 7  |- ; 1 2  = ; 1 2
683131, 251oveq12i 5886 . . . . . . . 8  |-  ( ( 2  x.  1 )  +  ( 0  +  0 ) )  =  ( 2  +  0 )
684683, 306eqtri 2316 . . . . . . 7  |-  ( ( 2  x.  1 )  +  ( 0  +  0 ) )  =  2
685125oveq1i 5884 . . . . . . . 8  |-  ( ( 2  x.  2 )  +  1 )  =  ( 4  +  1 )
6863dec0h 10156 . . . . . . . 8  |-  5  = ; 0 5
687685, 363, 6863eqtri 2320 . . . . . . 7  |-  ( ( 2  x.  2 )  +  1 )  = ; 0
5
68811, 2, 5, 11, 682, 235, 2, 3, 5, 684, 687decma2c 10180 . . . . . 6  |-  ( ( 2  x. ; 1 2 )  +  1 )  = ; 2 5
6892, 12, 3, 681, 5, 11, 688, 453decmul2c 10188 . . . . 5  |-  ( 2  x. ;; 1 2 5 )  = ;; 2 5 0
6904, 5, 5, 689, 251decaddi 10184 . . . 4  |-  ( ( 2  x. ;; 1 2 5 )  +  0 )  = ;; 2 5 0
6912, 13, 11, 680, 2, 5, 690, 492decmul2c 10188 . . 3  |-  ( 2  x. ;;; 1 2 5 1 )  = ;;; 2 5 0 2
692 eqid 2296 . . . . . . 7  |- ;;; 2 5 0 2  = ;;; 2 5 0 2
6936, 2, 82, 692decsuc 10163 . . . . . 6  |-  (;;; 2 5 0 2  +  1 )  = ;;; 2 5 0 3
6941, 693eqtr4i 2319 . . . . 5  |-  N  =  (;;; 2 5 0 2  +  1 )
695694oveq1i 5884 . . . 4  |-  ( N  -  1 )  =  ( (;;; 2 5 0 2  +  1 )  - 
1 )
6966, 2deccl 10154 . . . . . 6  |- ;;; 2 5 0 2  e.  NN0
697696nn0cni 9993 . . . . 5  |- ;;; 2 5 0 2  e.  CC
698 pncan 9073 . . . . 5  |-  ( (;;; 2 5 0 2  e.  CC  /\  1  e.  CC )  ->  (
(;;; 2 5 0 2  +  1 )  - 
1 )  = ;;; 2 5 0 2 )
699697, 79, 698mp2an 653 . . . 4  |-  ( (;;; 2 5 0 2  +  1 )  -  1 )  = ;;; 2 5 0 2
700695, 699eqtri 2316 . . 3  |-  ( N  -  1 )  = ;;; 2 5 0 2
701691, 700eqtr4i 2319 . 2  |-  ( 2  x. ;;; 1 2 5 1 )  =  ( N  -  1 )
702664mul02i 9017 . . . 4  |-  ( 0  x.  N )  =  0
703702oveq1i 5884 . . 3  |-  ( ( 0  x.  N )  +  1 )  =  ( 0  +  1 )
704250, 190eqtr4i 2319 . . 3  |-  ( 1  x.  1 )  =  ( 0  +  1 )
705703, 704eqtr4i 2319 . 2  |-  ( ( 0  x.  N )  +  1 )  =  ( 1  x.  1 )
7069, 10, 14, 15, 11, 11, 679, 701, 705mod2xi 13100 1  |-  ( ( 2 ^ ( N  -  1 ) )  mod  N )  =  ( 1  mod  N
)
Colors of variables: wff set class
Syntax hints:    = wceq 1632    e. wcel 1696  (class class class)co 5874   CCcc 8751   0cc0 8753   1c1 8754    + caddc 8756    x. cmul 8758    - cmin 9053   NNcn 9762   2c2 9811   3c3 9812   4c4 9813   5c5 9814   6c6 9815   7c7 9816   8c8 9817   9c9 9818   10c10 9819  ;cdc 10140    mod cmo 10989   ^cexp 11120
This theorem is referenced by:  2503prm  13154
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-nul 4165  ax-pow 4204  ax-pr 4230  ax-un 4528  ax-cnex 8809  ax-resscn 8810  ax-1cn 8811  ax-icn 8812  ax-addcl 8813  ax-addrcl 8814  ax-mulcl 8815  ax-mulrcl 8816  ax-mulcom 8817  ax-addass 8818  ax-mulass 8819  ax-distr 8820  ax-i2m1 8821  ax-1ne0 8822  ax-1rid 8823  ax-rnegex 8824  ax-rrecex 8825  ax-cnre 8826  ax-pre-lttri 8827  ax-pre-lttrn 8828  ax-pre-ltadd 8829  ax-pre-mulgt0 8830  ax-pre-sup 8831
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-nel 2462  df-ral 2561  df-rex 2562  df-reu 2563  df-rmo 2564  df-rab 2565  df-v 2803  df-sbc 3005  df-csb 3095  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-pss 3181  df-nul 3469  df-if 3579  df-pw 3640  df-sn 3659  df-pr 3660  df-tp 3661  df-op 3662  df-uni 3844  df-iun 3923  df-br 4040  df-opab 4094  df-mpt 4095  df-tr 4130  df-eprel 4321  df-id 4325  df-po 4330  df-so 4331  df-fr 4368  df-we 4370  df-ord 4411  df-on 4412  df-lim 4413  df-suc 4414  df-om 4673  df-xp 4711  df-rel 4712  df-cnv 4713  df-co 4714  df-dm 4715  df-rn 4716  df-res 4717  df-ima 4718  df-iota 5235  df-fun 5273  df-fn 5274  df-f 5275  df-f1 5276  df-fo 5277  df-f1o 5278  df-fv 5279  df-ov 5877  df-oprab 5878  df-mpt2 5879  df-2nd 6139  df-riota 6320  df-recs 6404  df-rdg 6439  df-er 6676  df-en 6880  df-dom 6881  df-sdom 6882  df-sup 7210  df-pnf 8885  df-mnf 8886  df-xr 8887  df-ltxr 8888  df-le 8889  df-sub 9055  df-neg 9056  df-div 9440  df-nn 9763  df-2 9820  df-3 9821  df-4 9822  df-5 9823  df-6 9824  df-7 9825  df-8 9826  df-9 9827  df-10 9828  df-n0 9982  df-z 10041  df-dec 10141  df-uz 10247  df-rp 10371  df-fl 10941  df-mod 10990  df-seq 11063  df-exp 11121
  Copyright terms: Public domain W3C validator