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

Theorem 2503lem2 14154
Description: Lemma for 2503prm 14156. 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 10588 . . . . . 6  |-  2  e.  NN0
3 5nn0 10591 . . . . . 6  |-  5  e.  NN0
42, 3deccl 10761 . . . . 5  |- ; 2 5  e.  NN0
5 0nn0 10586 . . . . 5  |-  0  e.  NN0
64, 5deccl 10761 . . . 4  |- ;; 2 5 0  e.  NN0
7 3nn 10472 . . . 4  |-  3  e.  NN
86, 7decnncl 10760 . . 3  |- ;;; 2 5 0 3  e.  NN
91, 8eqeltri 2508 . 2  |-  N  e.  NN
10 2nn 10471 . 2  |-  2  e.  NN
11 1nn0 10587 . . . . 5  |-  1  e.  NN0
1211, 2deccl 10761 . . . 4  |- ; 1 2  e.  NN0
1312, 3deccl 10761 . . 3  |- ;; 1 2 5  e.  NN0
1413, 11deccl 10761 . 2  |- ;;; 1 2 5 1  e.  NN0
15 0z 10649 . 2  |-  0  e.  ZZ
16 4nn0 10590 . . . . 5  |-  4  e.  NN0
1712, 16deccl 10761 . . . 4  |- ;; 1 2 4  e.  NN0
18 8nn0 10594 . . . 4  |-  8  e.  NN0
1917, 18deccl 10761 . . 3  |- ;;; 1 2 4 8  e.  NN0
20 1z 10668 . . 3  |-  1  e.  ZZ
21 3nn0 10589 . . . . 5  |-  3  e.  NN0
2221, 11deccl 10761 . . . 4  |- ; 3 1  e.  NN0
2322, 21deccl 10761 . . 3  |- ;; 3 1 3  e.  NN0
24 6nn0 10592 . . . . . 6  |-  6  e.  NN0
2524, 2deccl 10761 . . . . 5  |- ; 6 2  e.  NN0
2625, 16deccl 10761 . . . 4  |- ;; 6 2 4  e.  NN0
27 9nn0 10595 . . . . . 6  |-  9  e.  NN0
282, 27deccl 10761 . . . . 5  |- ; 2 9  e.  NN0
2928nn0zi 10663 . . . 4  |- ; 2 9  e.  ZZ
30 7nn0 10593 . . . . . 6  |-  7  e.  NN0
312, 30deccl 10761 . . . . 5  |- ; 2 7  e.  NN0
3231, 5deccl 10761 . . . 4  |- ;; 2 7 0  e.  NN0
3322, 2deccl 10761 . . . . 5  |- ;; 3 1 2  e.  NN0
342, 21deccl 10761 . . . . . . 7  |- ; 2 3  e.  NN0
3534, 18deccl 10761 . . . . . 6  |- ;; 2 3 8  e.  NN0
3635nn0zi 10663 . . . . 5  |- ;; 2 3 8  e.  ZZ
3730, 30deccl 10761 . . . . . 6  |- ; 7 7  e.  NN0
3837, 2deccl 10761 . . . . 5  |- ;; 7 7 2  e.  NN0
3911, 3deccl 10761 . . . . . . 7  |- ; 1 5  e.  NN0
4039, 24deccl 10761 . . . . . 6  |- ;; 1 5 6  e.  NN0
4121nn0zi 10663 . . . . . 6  |-  3  e.  ZZ
4227, 11deccl 10761 . . . . . 6  |- ; 9 1  e.  NN0
4330, 18deccl 10761 . . . . . . 7  |- ; 7 8  e.  NN0
4439nn0zi 10663 . . . . . . 7  |- ; 1 5  e.  ZZ
4511, 27deccl 10761 . . . . . . . 8  |- ; 1 9  e.  NN0
46 4nn 10473 . . . . . . . 8  |-  4  e.  NN
4745, 46decnncl 10760 . . . . . . 7  |- ;; 1 9 4  e.  NN
4834, 5deccl 10761 . . . . . . . 8  |- ;; 2 3 0  e.  NN0
4948, 27deccl 10761 . . . . . . 7  |- ;;; 2 3 0 9  e.  NN0
5021, 27deccl 10761 . . . . . . . 8  |- ; 3 9  e.  NN0
5116nn0zi 10663 . . . . . . . 8  |-  4  e.  ZZ
5211, 11deccl 10761 . . . . . . . . 9  |- ; 1 1  e.  NN0
5352, 11deccl 10761 . . . . . . . 8  |- ;; 1 1 1  e.  NN0
5421, 18deccl 10761 . . . . . . . . 9  |- ; 3 8  e.  NN0
5511, 21deccl 10761 . . . . . . . . . . 11  |- ; 1 3  e.  NN0
5655, 5deccl 10761 . . . . . . . . . 10  |- ;; 1 3 0  e.  NN0
5756, 30deccl 10761 . . . . . . . . 9  |- ;;; 1 3 0 7  e.  NN0
583, 21deccl 10761 . . . . . . . . . . . 12  |- ; 5 3  e.  NN0
5958, 18deccl 10761 . . . . . . . . . . 11  |- ;; 5 3 8  e.  NN0
6059nn0zi 10663 . . . . . . . . . 10  |- ;; 5 3 8  e.  ZZ
6152, 24deccl 10761 . . . . . . . . . . 11  |- ;; 1 1 6  e.  NN0
6261, 11deccl 10761 . . . . . . . . . 10  |- ;;; 1 1 6 1  e.  NN0
6311, 18deccl 10761 . . . . . . . . . . 11  |- ; 1 8  e.  NN0
6463, 21deccl 10761 . . . . . . . . . . . 12  |- ;; 1 8 3  e.  NN0
6564, 2deccl 10761 . . . . . . . . . . 11  |- ;;; 1 8 3 2  e.  NN0
6612503lem1 14153 . . . . . . . . . . 11  |-  ( ( 2 ^; 1 8 )  mod 
N )  =  (;;; 1 8 3 2  mod 
N )
67 8p1e9 10444 . . . . . . . . . . . 12  |-  ( 8  +  1 )  =  9
68 eqid 2438 . . . . . . . . . . . 12  |- ; 1 8  = ; 1 8
6911, 18, 67, 68decsuc 10770 . . . . . . . . . . 11  |-  (; 1 8  +  1 )  = ; 1 9
70 eqid 2438 . . . . . . . . . . . . 13  |- ;;; 1 1 6 1  = ;;; 1 1 6 1
71 eqid 2438 . . . . . . . . . . . . . 14  |- ;; 2 5 0  = ;; 2 5 0
7261nn0cni 10583 . . . . . . . . . . . . . . 15  |- ;; 1 1 6  e.  CC
7372addid1i 9548 . . . . . . . . . . . . . 14  |-  (;; 1 1 6  +  0 )  = ;; 1 1 6
74 eqid 2438 . . . . . . . . . . . . . . 15  |- ; 2 5  = ; 2 5
7552nn0cni 10583 . . . . . . . . . . . . . . . 16  |- ; 1 1  e.  CC
7675addid1i 9548 . . . . . . . . . . . . . . 15  |-  (; 1 1  +  0 )  = ; 1 1
77 2cn 10384 . . . . . . . . . . . . . . . . . 18  |-  2  e.  CC
7877mulid2i 9381 . . . . . . . . . . . . . . . . 17  |-  ( 1  x.  2 )  =  2
79 1p0e1 10426 . . . . . . . . . . . . . . . . 17  |-  ( 1  +  0 )  =  1
8078, 79oveq12i 6098 . . . . . . . . . . . . . . . 16  |-  ( ( 1  x.  2 )  +  ( 1  +  0 ) )  =  ( 2  +  1 )
81 2p1e3 10437 . . . . . . . . . . . . . . . 16  |-  ( 2  +  1 )  =  3
8280, 81eqtri 2458 . . . . . . . . . . . . . . 15  |-  ( ( 1  x.  2 )  +  ( 1  +  0 ) )  =  3
83 5cn 10393 . . . . . . . . . . . . . . . . . 18  |-  5  e.  CC
8483mulid2i 9381 . . . . . . . . . . . . . . . . 17  |-  ( 1  x.  5 )  =  5
8584oveq1i 6096 . . . . . . . . . . . . . . . 16  |-  ( ( 1  x.  5 )  +  1 )  =  ( 5  +  1 )
86 5p1e6 10441 . . . . . . . . . . . . . . . 16  |-  ( 5  +  1 )  =  6
8724dec0h 10763 . . . . . . . . . . . . . . . 16  |-  6  = ; 0 6
8885, 86, 873eqtri 2462 . . . . . . . . . . . . . . 15  |-  ( ( 1  x.  5 )  +  1 )  = ; 0
6
892, 3, 11, 11, 74, 76, 11, 24, 5, 82, 88decma2c 10787 . . . . . . . . . . . . . 14  |-  ( ( 1  x. ; 2 5 )  +  (; 1 1  +  0 ) )  = ; 3 6
90 ax-1cn 9332 . . . . . . . . . . . . . . . . 17  |-  1  e.  CC
9190mul01i 9551 . . . . . . . . . . . . . . . 16  |-  ( 1  x.  0 )  =  0
9291oveq1i 6096 . . . . . . . . . . . . . . 15  |-  ( ( 1  x.  0 )  +  6 )  =  ( 0  +  6 )
93 6cn 10395 . . . . . . . . . . . . . . . 16  |-  6  e.  CC
9493addid2i 9549 . . . . . . . . . . . . . . 15  |-  ( 0  +  6 )  =  6
9592, 94, 873eqtri 2462 . . . . . . . . . . . . . 14  |-  ( ( 1  x.  0 )  +  6 )  = ; 0
6
964, 5, 52, 24, 71, 73, 11, 24, 5, 89, 95decma2c 10787 . . . . . . . . . . . . 13  |-  ( ( 1  x. ;; 2 5 0 )  +  (;; 1 1 6  +  0 ) )  = ;; 3 6 6
97 3cn 10388 . . . . . . . . . . . . . . . 16  |-  3  e.  CC
9897mulid2i 9381 . . . . . . . . . . . . . . 15  |-  ( 1  x.  3 )  =  3
9998oveq1i 6096 . . . . . . . . . . . . . 14  |-  ( ( 1  x.  3 )  +  1 )  =  ( 3  +  1 )
100 3p1e4 10439 . . . . . . . . . . . . . 14  |-  ( 3  +  1 )  =  4
10116dec0h 10763 . . . . . . . . . . . . . 14  |-  4  = ; 0 4
10299, 100, 1013eqtri 2462 . . . . . . . . . . . . 13  |-  ( ( 1  x.  3 )  +  1 )  = ; 0
4
1036, 21, 61, 11, 1, 70, 11, 16, 5, 96, 102decma2c 10787 . . . . . . . . . . . 12  |-  ( ( 1  x.  N )  + ;;; 1 1 6 1 )  = ;;; 3 6 6 4
104 eqid 2438 . . . . . . . . . . . . 13  |- ;;; 1 8 3 2  = ;;; 1 8 3 2
105 eqid 2438 . . . . . . . . . . . . . . . 16  |- ;; 1 8 3  = ;; 1 8 3
10678oveq1i 6096 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 1  x.  2 )  +  1 )  =  ( 2  +  1 )
107106, 81eqtri 2458 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 1  x.  2 )  +  1 )  =  3
108 8t2e16 10835 . . . . . . . . . . . . . . . . . . 19  |-  ( 8  x.  2 )  = ; 1
6
1092, 11, 18, 68, 24, 11, 107, 108decmul1c 10794 . . . . . . . . . . . . . . . . . 18  |-  (; 1 8  x.  2 )  = ; 3 6
110109oveq1i 6096 . . . . . . . . . . . . . . . . 17  |-  ( (; 1
8  x.  2 )  +  0 )  =  (; 3 6  +  0 )
11121, 24deccl 10761 . . . . . . . . . . . . . . . . . . 19  |- ; 3 6  e.  NN0
112111nn0cni 10583 . . . . . . . . . . . . . . . . . 18  |- ; 3 6  e.  CC
113112addid1i 9548 . . . . . . . . . . . . . . . . 17  |-  (; 3 6  +  0 )  = ; 3 6
114110, 113eqtri 2458 . . . . . . . . . . . . . . . 16  |-  ( (; 1
8  x.  2 )  +  0 )  = ; 3
6
115 3t2e6 10465 . . . . . . . . . . . . . . . . 17  |-  ( 3  x.  2 )  =  6
116115, 87eqtri 2458 . . . . . . . . . . . . . . . 16  |-  ( 3  x.  2 )  = ; 0
6
1172, 63, 21, 105, 24, 5, 114, 116decmul1c 10794 . . . . . . . . . . . . . . 15  |-  (;; 1 8 3  x.  2 )  = ;; 3 6 6
118117oveq1i 6096 . . . . . . . . . . . . . 14  |-  ( (;; 1 8 3  x.  2 )  +  0 )  =  (;; 3 6 6  +  0 )
119111, 24deccl 10761 . . . . . . . . . . . . . . . 16  |- ;; 3 6 6  e.  NN0
120119nn0cni 10583 . . . . . . . . . . . . . . 15  |- ;; 3 6 6  e.  CC
121120addid1i 9548 . . . . . . . . . . . . . 14  |-  (;; 3 6 6  +  0 )  = ;; 3 6 6
122118, 121eqtri 2458 . . . . . . . . . . . . 13  |-  ( (;; 1 8 3  x.  2 )  +  0 )  = ;; 3 6 6
123 2t2e4 10463 . . . . . . . . . . . . . 14  |-  ( 2  x.  2 )  =  4
124123, 101eqtri 2458 . . . . . . . . . . . . 13  |-  ( 2  x.  2 )  = ; 0
4
1252, 64, 2, 104, 16, 5, 122, 124decmul1c 10794 . . . . . . . . . . . 12  |-  (;;; 1 8 3 2  x.  2 )  = ;;; 3 6 6 4
126103, 125eqtr4i 2461 . . . . . . . . . . 11  |-  ( ( 1  x.  N )  + ;;; 1 1 6 1 )  =  (;;; 1 8 3 2  x.  2 )
1279, 10, 63, 20, 65, 62, 66, 69, 126modxp1i 14091 . . . . . . . . . 10  |-  ( ( 2 ^; 1 9 )  mod 
N )  =  (;;; 1 1 6 1  mod 
N )
128 eqid 2438 . . . . . . . . . . 11  |- ; 1 9  = ; 1 9
129 2t1e2 10462 . . . . . . . . . . . . 13  |-  ( 2  x.  1 )  =  2
130129oveq1i 6096 . . . . . . . . . . . 12  |-  ( ( 2  x.  1 )  +  1 )  =  ( 2  +  1 )
131130, 81eqtri 2458 . . . . . . . . . . 11  |-  ( ( 2  x.  1 )  +  1 )  =  3
132 9cn 10401 . . . . . . . . . . . 12  |-  9  e.  CC
133 9t2e18 10842 . . . . . . . . . . . 12  |-  ( 9  x.  2 )  = ; 1
8
134132, 77, 133mulcomli 9385 . . . . . . . . . . 11  |-  ( 2  x.  9 )  = ; 1
8
1352, 11, 27, 128, 18, 11, 131, 134decmul2c 10795 . . . . . . . . . 10  |-  ( 2  x. ; 1 9 )  = ; 3
8
136 eqid 2438 . . . . . . . . . . . 12  |- ;;; 1 3 0 7  = ;;; 1 3 0 7
13711, 24deccl 10761 . . . . . . . . . . . . 13  |- ; 1 6  e.  NN0
138137, 2deccl 10761 . . . . . . . . . . . 12  |- ;; 1 6 2  e.  NN0
139 eqid 2438 . . . . . . . . . . . . . 14  |- ;; 1 3 0  = ;; 1 3 0
140 eqid 2438 . . . . . . . . . . . . . 14  |- ;; 1 6 2  = ;; 1 6 2
141 eqid 2438 . . . . . . . . . . . . . . 15  |- ; 1 3  = ; 1 3
142 eqid 2438 . . . . . . . . . . . . . . 15  |- ; 1 6  = ; 1 6
143 1p1e2 10427 . . . . . . . . . . . . . . 15  |-  ( 1  +  1 )  =  2
144 6p3e9 10456 . . . . . . . . . . . . . . . 16  |-  ( 6  +  3 )  =  9
14593, 97, 144addcomli 9553 . . . . . . . . . . . . . . 15  |-  ( 3  +  6 )  =  9
14611, 21, 11, 24, 141, 142, 143, 145decadd 10788 . . . . . . . . . . . . . 14  |-  (; 1 3  + ; 1 6 )  = ; 2
9
14777addid2i 9549 . . . . . . . . . . . . . 14  |-  ( 0  +  2 )  =  2
14855, 5, 137, 2, 139, 140, 146, 147decadd 10788 . . . . . . . . . . . . 13  |-  (;; 1 3 0  + ;; 1 6 2 )  = ;; 2 9 2
14928nn0cni 10583 . . . . . . . . . . . . . . 15  |- ; 2 9  e.  CC
150149addid1i 9548 . . . . . . . . . . . . . 14  |-  (; 2 9  +  0 )  = ; 2 9
1512, 24deccl 10761 . . . . . . . . . . . . . . 15  |- ; 2 6  e.  NN0
152151, 27deccl 10761 . . . . . . . . . . . . . 14  |- ;; 2 6 9  e.  NN0
153 eqid 2438 . . . . . . . . . . . . . . 15  |- ;; 5 3 8  = ;; 5 3 8
1542dec0h 10763 . . . . . . . . . . . . . . . 16  |-  2  = ; 0 2
155 eqid 2438 . . . . . . . . . . . . . . . 16  |- ;; 2 6 9  = ;; 2 6 9
156 6p1e7 10442 . . . . . . . . . . . . . . . . 17  |-  ( 6  +  1 )  =  7
157151nn0cni 10583 . . . . . . . . . . . . . . . . . 18  |- ; 2 6  e.  CC
158157addid2i 9549 . . . . . . . . . . . . . . . . 17  |-  ( 0  + ; 2 6 )  = ; 2
6
1592, 24, 156, 158decsuc 10770 . . . . . . . . . . . . . . . 16  |-  ( ( 0  + ; 2 6 )  +  1 )  = ; 2 7
160 9p2e11 10809 . . . . . . . . . . . . . . . . 17  |-  ( 9  +  2 )  = ; 1
1
161132, 77, 160addcomli 9553 . . . . . . . . . . . . . . . 16  |-  ( 2  +  9 )  = ; 1
1
1625, 2, 151, 27, 154, 155, 159, 11, 161decaddc 10789 . . . . . . . . . . . . . . 15  |-  ( 2  + ;; 2 6 9 )  = ;; 2 7 1
163 eqid 2438 . . . . . . . . . . . . . . . 16  |- ; 5 3  = ; 5 3
164 7p1e8 10443 . . . . . . . . . . . . . . . . 17  |-  ( 7  +  1 )  =  8
165 eqid 2438 . . . . . . . . . . . . . . . . 17  |- ; 2 7  = ; 2 7
1662, 30, 164, 165decsuc 10770 . . . . . . . . . . . . . . . 16  |-  (; 2 7  +  1 )  = ; 2 8
16781oveq2i 6097 . . . . . . . . . . . . . . . . 17  |-  ( ( 5  x.  2 )  +  ( 2  +  1 ) )  =  ( ( 5  x.  2 )  +  3 )
168 5t2e10 10468 . . . . . . . . . . . . . . . . . . 19  |-  ( 5  x.  2 )  =  10
169 dec10 10777 . . . . . . . . . . . . . . . . . . 19  |-  10  = ; 1 0
170168, 169eqtri 2458 . . . . . . . . . . . . . . . . . 18  |-  ( 5  x.  2 )  = ; 1
0
17197addid2i 9549 . . . . . . . . . . . . . . . . . 18  |-  ( 0  +  3 )  =  3
17211, 5, 21, 170, 171decaddi 10791 . . . . . . . . . . . . . . . . 17  |-  ( ( 5  x.  2 )  +  3 )  = ; 1
3
173167, 172eqtri 2458 . . . . . . . . . . . . . . . 16  |-  ( ( 5  x.  2 )  +  ( 2  +  1 ) )  = ; 1
3
174115oveq1i 6096 . . . . . . . . . . . . . . . . 17  |-  ( ( 3  x.  2 )  +  8 )  =  ( 6  +  8 )
175 8cn 10399 . . . . . . . . . . . . . . . . . 18  |-  8  e.  CC
176 8p6e14 10806 . . . . . . . . . . . . . . . . . 18  |-  ( 8  +  6 )  = ; 1
4
177175, 93, 176addcomli 9553 . . . . . . . . . . . . . . . . 17  |-  ( 6  +  8 )  = ; 1
4
178174, 177eqtri 2458 . . . . . . . . . . . . . . . 16  |-  ( ( 3  x.  2 )  +  8 )  = ; 1
4
1793, 21, 2, 18, 163, 166, 2, 16, 11, 173, 178decmac 10786 . . . . . . . . . . . . . . 15  |-  ( (; 5
3  x.  2 )  +  (; 2 7  +  1 ) )  = ;; 1 3 4
18011, 24, 156, 108decsuc 10770 . . . . . . . . . . . . . . 15  |-  ( ( 8  x.  2 )  +  1 )  = ; 1
7
18158, 18, 31, 11, 153, 162, 2, 30, 11, 179, 180decmac 10786 . . . . . . . . . . . . . 14  |-  ( (;; 5 3 8  x.  2 )  +  ( 2  + ;; 2 6 9 ) )  = ;;; 1 3 4 7
18227dec0h 10763 . . . . . . . . . . . . . . 15  |-  9  = ; 0 9
183 4cn 10391 . . . . . . . . . . . . . . . . . 18  |-  4  e.  CC
184183addid2i 9549 . . . . . . . . . . . . . . . . 17  |-  ( 0  +  4 )  =  4
185184, 101eqtri 2458 . . . . . . . . . . . . . . . 16  |-  ( 0  +  4 )  = ; 0
4
186 0p1e1 10425 . . . . . . . . . . . . . . . . . 18  |-  ( 0  +  1 )  =  1
187186oveq2i 6097 . . . . . . . . . . . . . . . . 17  |-  ( ( 5  x.  5 )  +  ( 0  +  1 ) )  =  ( ( 5  x.  5 )  +  1 )
188 5t5e25 10823 . . . . . . . . . . . . . . . . . 18  |-  ( 5  x.  5 )  = ; 2
5
1892, 3, 86, 188decsuc 10770 . . . . . . . . . . . . . . . . 17  |-  ( ( 5  x.  5 )  +  1 )  = ; 2
6
190187, 189eqtri 2458 . . . . . . . . . . . . . . . 16  |-  ( ( 5  x.  5 )  +  ( 0  +  1 ) )  = ; 2
6
191 5t3e15 10821 . . . . . . . . . . . . . . . . . 18  |-  ( 5  x.  3 )  = ; 1
5
19283, 97, 191mulcomli 9385 . . . . . . . . . . . . . . . . 17  |-  ( 3  x.  5 )  = ; 1
5
193 5p4e9 10453 . . . . . . . . . . . . . . . . 17  |-  ( 5  +  4 )  =  9
19411, 3, 16, 192, 193decaddi 10791 . . . . . . . . . . . . . . . 16  |-  ( ( 3  x.  5 )  +  4 )  = ; 1
9
1953, 21, 5, 16, 163, 185, 3, 27, 11, 190, 194decmac 10786 . . . . . . . . . . . . . . 15  |-  ( (; 5
3  x.  5 )  +  ( 0  +  4 ) )  = ;; 2 6 9
196 8t5e40 10838 . . . . . . . . . . . . . . . 16  |-  ( 8  x.  5 )  = ; 4
0
197132addid2i 9549 . . . . . . . . . . . . . . . 16  |-  ( 0  +  9 )  =  9
19816, 5, 27, 196, 197decaddi 10791 . . . . . . . . . . . . . . 15  |-  ( ( 8  x.  5 )  +  9 )  = ; 4
9
19958, 18, 5, 27, 153, 182, 3, 27, 16, 195, 198decmac 10786 . . . . . . . . . . . . . 14  |-  ( (;; 5 3 8  x.  5 )  +  9 )  = ;;; 2 6 9 9
2002, 3, 2, 27, 74, 150, 59, 27, 152, 181, 199decma2c 10787 . . . . . . . . . . . . 13  |-  ( (;; 5 3 8  x. ; 2
5 )  +  (; 2
9  +  0 ) )  = ;;;; 1 3 4 7 9
20159nn0cni 10583 . . . . . . . . . . . . . . . 16  |- ;; 5 3 8  e.  CC
202201mul01i 9551 . . . . . . . . . . . . . . 15  |-  (;; 5 3 8  x.  0 )  =  0
203202oveq1i 6096 . . . . . . . . . . . . . 14  |-  ( (;; 5 3 8  x.  0 )  +  2 )  =  ( 0  +  2 )
204203, 147, 1543eqtri 2462 . . . . . . . . . . . . 13  |-  ( (;; 5 3 8  x.  0 )  +  2 )  = ; 0 2
2054, 5, 28, 2, 71, 148, 59, 2, 5, 200, 204decma2c 10787 . . . . . . . . . . . 12  |-  ( (;; 5 3 8  x. ;; 2 5 0 )  +  (;; 1 3 0  + ;; 1 6 2 ) )  = ;;;;; 1 3 4 7 9 2
20630dec0h 10763 . . . . . . . . . . . . 13  |-  7  = ; 0 7
20721dec0h 10763 . . . . . . . . . . . . . . 15  |-  3  = ; 0 3
208171, 207eqtri 2458 . . . . . . . . . . . . . 14  |-  ( 0  +  3 )  = ; 0
3
209186oveq2i 6097 . . . . . . . . . . . . . . 15  |-  ( ( 5  x.  3 )  +  ( 0  +  1 ) )  =  ( ( 5  x.  3 )  +  1 )
21011, 3, 86, 191decsuc 10770 . . . . . . . . . . . . . . 15  |-  ( ( 5  x.  3 )  +  1 )  = ; 1
6
211209, 210eqtri 2458 . . . . . . . . . . . . . 14  |-  ( ( 5  x.  3 )  +  ( 0  +  1 ) )  = ; 1
6
212 3t3e9 10466 . . . . . . . . . . . . . . . 16  |-  ( 3  x.  3 )  =  9
213212oveq1i 6096 . . . . . . . . . . . . . . 15  |-  ( ( 3  x.  3 )  +  3 )  =  ( 9  +  3 )
214 9p3e12 10810 . . . . . . . . . . . . . . 15  |-  ( 9  +  3 )  = ; 1
2
215213, 214eqtri 2458 . . . . . . . . . . . . . 14  |-  ( ( 3  x.  3 )  +  3 )  = ; 1
2
2163, 21, 5, 21, 163, 208, 21, 2, 11, 211, 215decmac 10786 . . . . . . . . . . . . 13  |-  ( (; 5
3  x.  3 )  +  ( 0  +  3 ) )  = ;; 1 6 2
217 8t3e24 10836 . . . . . . . . . . . . . 14  |-  ( 8  x.  3 )  = ; 2
4
218 7cn 10397 . . . . . . . . . . . . . . 15  |-  7  e.  CC
219 7p4e11 10799 . . . . . . . . . . . . . . 15  |-  ( 7  +  4 )  = ; 1
1
220218, 183, 219addcomli 9553 . . . . . . . . . . . . . 14  |-  ( 4  +  7 )  = ; 1
1
2212, 16, 30, 217, 81, 11, 220decaddci 10792 . . . . . . . . . . . . 13  |-  ( ( 8  x.  3 )  +  7 )  = ; 3
1
22258, 18, 5, 30, 153, 206, 21, 11, 21, 216, 221decmac 10786 . . . . . . . . . . . 12  |-  ( (;; 5 3 8  x.  3 )  +  7 )  = ;;; 1 6 2 1
2236, 21, 56, 30, 1, 136, 59, 11, 138, 205, 222decma2c 10787 . . . . . . . . . . 11  |-  ( (;; 5 3 8  x.  N )  + ;;; 1 3 0 7 )  = ;;;;;; 1 3 4 7 9 2 1
224 eqid 2438 . . . . . . . . . . . . 13  |- ;; 1 1 6  = ;; 1 1 6
22524, 27deccl 10761 . . . . . . . . . . . . . 14  |- ; 6 9  e.  NN0
226225, 30deccl 10761 . . . . . . . . . . . . 13  |- ;; 6 9 7  e.  NN0
22730, 5deccl 10761 . . . . . . . . . . . . . 14  |- ; 7 0  e.  NN0
228 eqid 2438 . . . . . . . . . . . . . 14  |- ; 1 1  = ; 1 1
229 eqid 2438 . . . . . . . . . . . . . . 15  |- ;; 6 9 7  = ;; 6 9 7
23011dec0h 10763 . . . . . . . . . . . . . . . 16  |-  1  = ; 0 1
231 eqid 2438 . . . . . . . . . . . . . . . 16  |- ; 6 9  = ; 6 9
23294oveq1i 6096 . . . . . . . . . . . . . . . . 17  |-  ( ( 0  +  6 )  +  1 )  =  ( 6  +  1 )
233232, 156eqtri 2458 . . . . . . . . . . . . . . . 16  |-  ( ( 0  +  6 )  +  1 )  =  7
234 9p1e10 10445 . . . . . . . . . . . . . . . . 17  |-  ( 9  +  1 )  =  10
235132, 90, 234addcomli 9553 . . . . . . . . . . . . . . . 16  |-  ( 1  +  9 )  =  10
2365, 11, 24, 27, 230, 231, 233, 235decaddc2 10790 . . . . . . . . . . . . . . 15  |-  ( 1  + ; 6 9 )  = ; 7
0
237218, 90, 164addcomli 9553 . . . . . . . . . . . . . . 15  |-  ( 1  +  7 )  =  8
23811, 11, 225, 30, 228, 229, 236, 237decadd 10788 . . . . . . . . . . . . . 14  |-  (; 1 1  + ;; 6 9 7 )  = ;; 7 0 8
239 eqid 2438 . . . . . . . . . . . . . . . 16  |- ; 7 0  = ; 7 0
2405, 30, 11, 11, 206, 228, 186, 164decadd 10788 . . . . . . . . . . . . . . . 16  |-  ( 7  + ; 1 1 )  = ; 1
8
24130, 5, 52, 24, 239, 224, 240, 94decadd 10788 . . . . . . . . . . . . . . 15  |-  (; 7 0  + ;; 1 1 6 )  = ;; 1 8 6
24263nn0cni 10583 . . . . . . . . . . . . . . . . 17  |- ; 1 8  e.  CC
243242addid1i 9548 . . . . . . . . . . . . . . . 16  |-  (; 1 8  +  0 )  = ; 1 8
244143, 154eqtri 2458 . . . . . . . . . . . . . . . . 17  |-  ( 1  +  1 )  = ; 0
2
245 1t1e1 10461 . . . . . . . . . . . . . . . . . . 19  |-  ( 1  x.  1 )  =  1
246 00id 9536 . . . . . . . . . . . . . . . . . . 19  |-  ( 0  +  0 )  =  0
247245, 246oveq12i 6098 . . . . . . . . . . . . . . . . . 18  |-  ( ( 1  x.  1 )  +  ( 0  +  0 ) )  =  ( 1  +  0 )
248247, 79eqtri 2458 . . . . . . . . . . . . . . . . 17  |-  ( ( 1  x.  1 )  +  ( 0  +  0 ) )  =  1
249245oveq1i 6096 . . . . . . . . . . . . . . . . . 18  |-  ( ( 1  x.  1 )  +  2 )  =  ( 1  +  2 )
250 1p2e3 10438 . . . . . . . . . . . . . . . . . 18  |-  ( 1  +  2 )  =  3
251249, 250, 2073eqtri 2462 . . . . . . . . . . . . . . . . 17  |-  ( ( 1  x.  1 )  +  2 )  = ; 0
3
25211, 11, 5, 2, 228, 244, 11, 21, 5, 248, 251decmac 10786 . . . . . . . . . . . . . . . 16  |-  ( (; 1
1  x.  1 )  +  ( 1  +  1 ) )  = ; 1
3
25393mulid1i 9380 . . . . . . . . . . . . . . . . . 18  |-  ( 6  x.  1 )  =  6
254253oveq1i 6096 . . . . . . . . . . . . . . . . 17  |-  ( ( 6  x.  1 )  +  8 )  =  ( 6  +  8 )
255254, 177eqtri 2458 . . . . . . . . . . . . . . . 16  |-  ( ( 6  x.  1 )  +  8 )  = ; 1
4
25652, 24, 11, 18, 224, 243, 11, 16, 11, 252, 255decmac 10786 . . . . . . . . . . . . . . 15  |-  ( (;; 1 1 6  x.  1 )  +  (; 1
8  +  0 ) )  = ;; 1 3 4
257245oveq1i 6096 . . . . . . . . . . . . . . . 16  |-  ( ( 1  x.  1 )  +  6 )  =  ( 1  +  6 )
25893, 90, 156addcomli 9553 . . . . . . . . . . . . . . . 16  |-  ( 1  +  6 )  =  7
259257, 258, 2063eqtri 2462 . . . . . . . . . . . . . . 15  |-  ( ( 1  x.  1 )  +  6 )  = ; 0
7
26061, 11, 63, 24, 70, 241, 11, 30, 5, 256, 259decmac 10786 . . . . . . . . . . . . . 14  |-  ( (;;; 1 1 6 1  x.  1 )  +  (; 7
0  + ;; 1 1 6 ) )  = ;;; 1 3 4 7
26118dec0h 10763 . . . . . . . . . . . . . . 15  |-  8  = ; 0 8
2625dec0h 10763 . . . . . . . . . . . . . . . . 17  |-  0  = ; 0 0
263246, 262eqtri 2458 . . . . . . . . . . . . . . . 16  |-  ( 0  +  0 )  = ; 0
0
264245oveq1i 6096 . . . . . . . . . . . . . . . . . 18  |-  ( ( 1  x.  1 )  +  0 )  =  ( 1  +  0 )
265264, 79eqtri 2458 . . . . . . . . . . . . . . . . 17  |-  ( ( 1  x.  1 )  +  0 )  =  1
26611, 11, 5, 5, 228, 263, 11, 265, 265decma 10785 . . . . . . . . . . . . . . . 16  |-  ( (; 1
1  x.  1 )  +  ( 0  +  0 ) )  = ; 1
1
267253oveq1i 6096 . . . . . . . . . . . . . . . . 17  |-  ( ( 6  x.  1 )  +  0 )  =  ( 6  +  0 )
26893addid1i 9548 . . . . . . . . . . . . . . . . 17  |-  ( 6  +  0 )  =  6
269267, 268, 873eqtri 2462 . . . . . . . . . . . . . . . 16  |-  ( ( 6  x.  1 )  +  0 )  = ; 0
6
27052, 24, 5, 5, 224, 263, 11, 24, 5, 266, 269decmac 10786 . . . . . . . . . . . . . . 15  |-  ( (;; 1 1 6  x.  1 )  +  ( 0  +  0 ) )  = ;; 1 1 6
271245oveq1i 6096 . . . . . . . . . . . . . . . 16  |-  ( ( 1  x.  1 )  +  8 )  =  ( 1  +  8 )
272175, 90, 67addcomli 9553 . . . . . . . . . . . . . . . 16  |-  ( 1  +  8 )  =  9
273271, 272, 1823eqtri 2462 . . . . . . . . . . . . . . 15  |-  ( ( 1  x.  1 )  +  8 )  = ; 0
9
27461, 11, 5, 18, 70, 261, 11, 27, 5, 270, 273decmac 10786 . . . . . . . . . . . . . 14  |-  ( (;;; 1 1 6 1  x.  1 )  +  8 )  = ;;; 1 1 6 9
27511, 11, 227, 18, 228, 238, 62, 27, 61, 260, 274decma2c 10787 . . . . . . . . . . . . 13  |-  ( (;;; 1 1 6 1  x. ; 1
1 )  +  (; 1
1  + ;; 6 9 7 ) )  = ;;;; 1 3 4 7 9
276186, 230eqtri 2458 . . . . . . . . . . . . . . 15  |-  ( 0  +  1 )  = ; 0
1
27793mulid2i 9381 . . . . . . . . . . . . . . . . . 18  |-  ( 1  x.  6 )  =  6
278277, 246oveq12i 6098 . . . . . . . . . . . . . . . . 17  |-  ( ( 1  x.  6 )  +  ( 0  +  0 ) )  =  ( 6  +  0 )
279278, 268eqtri 2458 . . . . . . . . . . . . . . . 16  |-  ( ( 1  x.  6 )  +  ( 0  +  0 ) )  =  6
280277oveq1i 6096 . . . . . . . . . . . . . . . . 17  |-  ( ( 1  x.  6 )  +  3 )  =  ( 6  +  3 )
281280, 144, 1823eqtri 2462 . . . . . . . . . . . . . . . 16  |-  ( ( 1  x.  6 )  +  3 )  = ; 0
9
28211, 11, 5, 21, 228, 208, 24, 27, 5, 279, 281decmac 10786 . . . . . . . . . . . . . . 15  |-  ( (; 1
1  x.  6 )  +  ( 0  +  3 ) )  = ; 6
9
283 6t6e36 10828 . . . . . . . . . . . . . . . 16  |-  ( 6  x.  6 )  = ; 3
6
28421, 24, 156, 283decsuc 10770 . . . . . . . . . . . . . . 15  |-  ( ( 6  x.  6 )  +  1 )  = ; 3
7
28552, 24, 5, 11, 224, 276, 24, 30, 21, 282, 284decmac 10786 . . . . . . . . . . . . . 14  |-  ( (;; 1 1 6  x.  6 )  +  ( 0  +  1 ) )  = ;; 6 9 7
286277oveq1i 6096 . . . . . . . . . . . . . . 15  |-  ( ( 1  x.  6 )  +  6 )  =  ( 6  +  6 )
287 6p6e12 10798 . . . . . . . . . . . . . . 15  |-  ( 6  +  6 )  = ; 1
2
288286, 287eqtri 2458 . . . . . . . . . . . . . 14  |-  ( ( 1  x.  6 )  +  6 )  = ; 1
2
28961, 11, 5, 24, 70, 87, 24, 2, 11, 285, 288decmac 10786 . . . . . . . . . . . . 13  |-  ( (;;; 1 1 6 1  x.  6 )  +  6 )  = ;;; 6 9 7 2
29052, 24, 52, 24, 224, 224, 62, 2, 226, 275, 289decma2c 10787 . . . . . . . . . . . 12  |-  ( (;;; 1 1 6 1  x. ;; 1 1 6 )  + ;; 1 1 6 )  = ;;;;; 1 3 4 7 9 2
29162nn0cni 10583 . . . . . . . . . . . . 13  |- ;;; 1 1 6 1  e.  CC
292291mulid1i 9380 . . . . . . . . . . . 12  |-  (;;; 1 1 6 1  x.  1 )  = ;;; 1 1 6 1
29362, 61, 11, 70, 11, 61, 290, 292decmul2c 10795 . . . . . . . . . . 11  |-  (;;; 1 1 6 1  x. ;;; 1 1 6 1 )  = ;;;;;; 1 3 4 7 9 2 1
294223, 293eqtr4i 2461 . . . . . . . . . 10  |-  ( (;; 5 3 8  x.  N )  + ;;; 1 3 0 7 )  =  (;;; 1 1 6 1  x. ;;; 1 1 6 1 )
2959, 10, 45, 60, 62, 57, 127, 135, 294mod2xi 14090 . . . . . . . . 9  |-  ( ( 2 ^; 3 8 )  mod 
N )  =  (;;; 1 3 0 7  mod 
N )
296 eqid 2438 . . . . . . . . . 10  |- ; 3 8  = ; 3 8
29721, 18, 67, 296decsuc 10770 . . . . . . . . 9  |-  (; 3 8  +  1 )  = ; 3 9
298 eqid 2438 . . . . . . . . . . 11  |- ;; 1 1 1  = ;; 1 1 1
29979, 230eqtri 2458 . . . . . . . . . . . . 13  |-  ( 1  +  0 )  = ; 0
1
30078, 246oveq12i 6098 . . . . . . . . . . . . . 14  |-  ( ( 1  x.  2 )  +  ( 0  +  0 ) )  =  ( 2  +  0 )
30177addid1i 9548 . . . . . . . . . . . . . 14  |-  ( 2  +  0 )  =  2
302300, 301eqtri 2458 . . . . . . . . . . . . 13  |-  ( ( 1  x.  2 )  +  ( 0  +  0 ) )  =  2
3032, 3, 5, 11, 74, 299, 11, 24, 5, 302, 88decma2c 10787 . . . . . . . . . . . 12  |-  ( ( 1  x. ; 2 5 )  +  ( 1  +  0 ) )  = ; 2 6
30491oveq1i 6096 . . . . . . . . . . . . 13  |-  ( ( 1  x.  0 )  +  1 )  =  ( 0  +  1 )
305304, 186, 2303eqtri 2462 . . . . . . . . . . . 12  |-  ( ( 1  x.  0 )  +  1 )  = ; 0
1
3064, 5, 11, 11, 71, 76, 11, 11, 5, 303, 305decma2c 10787 . . . . . . . . . . 11  |-  ( ( 1  x. ;; 2 5 0 )  +  (; 1 1  +  0 ) )  = ;; 2 6 1
3076, 21, 52, 11, 1, 298, 11, 16, 5, 306, 102decma2c 10787 . . . . . . . . . 10  |-  ( ( 1  x.  N )  + ;; 1 1 1 )  = ;;; 2 6 1 4
308115oveq1i 6096 . . . . . . . . . . . . . 14  |-  ( ( 3  x.  2 )  +  0 )  =  ( 6  +  0 )
309308, 268, 873eqtri 2462 . . . . . . . . . . . . 13  |-  ( ( 3  x.  2 )  +  0 )  = ; 0
6
31011, 21, 5, 5, 141, 263, 2, 24, 5, 302, 309decmac 10786 . . . . . . . . . . . 12  |-  ( (; 1
3  x.  2 )  +  ( 0  +  0 ) )  = ; 2
6
31177mul02i 9550 . . . . . . . . . . . . . 14  |-  ( 0  x.  2 )  =  0
312311oveq1i 6096 . . . . . . . . . . . . 13  |-  ( ( 0  x.  2 )  +  1 )  =  ( 0  +  1 )
313312, 186, 2303eqtri 2462 . . . . . . . . . . . 12  |-  ( ( 0  x.  2 )  +  1 )  = ; 0
1
31455, 5, 5, 11, 139, 230, 2, 11, 5, 310, 313decmac 10786 . . . . . . . . . . 11  |-  ( (;; 1 3 0  x.  2 )  +  1 )  = ;; 2 6 1
315 7t2e14 10829 . . . . . . . . . . 11  |-  ( 7  x.  2 )  = ; 1
4
3162, 56, 30, 136, 16, 11, 314, 315decmul1c 10794 . . . . . . . . . 10  |-  (;;; 1 3 0 7  x.  2 )  = ;;; 2 6 1 4
317307, 316eqtr4i 2461 . . . . . . . . 9  |-  ( ( 1  x.  N )  + ;; 1 1 1 )  =  (;;; 1 3 0 7  x.  2 )
3189, 10, 54, 20, 57, 53, 295, 297, 317modxp1i 14091 . . . . . . . 8  |-  ( ( 2 ^; 3 9 )  mod 
N )  =  (;; 1 1 1  mod 
N )
319 eqid 2438 . . . . . . . . 9  |- ; 3 9  = ; 3 9
32097, 77, 115mulcomli 9385 . . . . . . . . . . 11  |-  ( 2  x.  3 )  =  6
321320oveq1i 6096 . . . . . . . . . 10  |-  ( ( 2  x.  3 )  +  1 )  =  ( 6  +  1 )
322321, 156eqtri 2458 . . . . . . . . 9  |-  ( ( 2  x.  3 )  +  1 )  =  7
3232, 21, 27, 319, 18, 11, 322, 134decmul2c 10795 . . . . . . . 8  |-  ( 2  x. ; 3 9 )  = ; 7
8
324 eqid 2438 . . . . . . . . . 10  |- ;;; 2 3 0 9  = ;;; 2 3 0 9
325 eqid 2438 . . . . . . . . . . . 12  |- ;; 2 3 0  = ;; 2 3 0
32634, 5, 2, 325, 147decaddi 10791 . . . . . . . . . . 11  |-  (;; 2 3 0  +  2 )  = ;; 2 3 2
32734nn0cni 10583 . . . . . . . . . . . . 13  |- ; 2 3  e.  CC
328327addid1i 9548 . . . . . . . . . . . 12  |-  (; 2 3  +  0 )  = ; 2 3
329 4t2e8 10467 . . . . . . . . . . . . . 14  |-  ( 4  x.  2 )  =  8
330 2p2e4 10431 . . . . . . . . . . . . . 14  |-  ( 2  +  2 )  =  4
331329, 330oveq12i 6098 . . . . . . . . . . . . 13  |-  ( ( 4  x.  2 )  +  ( 2  +  2 ) )  =  ( 8  +  4 )
332 8p4e12 10804 . . . . . . . . . . . . 13  |-  ( 8  +  4 )  = ; 1
2
333331, 332eqtri 2458 . . . . . . . . . . . 12  |-  ( ( 4  x.  2 )  +  ( 2  +  2 ) )  = ; 1
2
334 5t4e20 10822 . . . . . . . . . . . . . 14  |-  ( 5  x.  4 )  = ; 2
0
33583, 183, 334mulcomli 9385 . . . . . . . . . . . . 13  |-  ( 4  x.  5 )  = ; 2
0
3362, 5, 21, 335, 171decaddi 10791 . . . . . . . . . . . 12  |-  ( ( 4  x.  5 )  +  3 )  = ; 2
3
3372, 3, 2, 21, 74, 328, 16, 21, 2, 333, 336decma2c 10787 . . . . . . . . . . 11  |-  ( ( 4  x. ; 2 5 )  +  (; 2 3  +  0 ) )  = ;; 1 2 3
338183mul01i 9551 . . . . . . . . . . . . 13  |-  ( 4  x.  0 )  =  0
339338oveq1i 6096 . . . . . . . . . . . 12  |-  ( ( 4  x.  0 )  +  2 )  =  ( 0  +  2 )
340339, 147, 1543eqtri 2462 . . . . . . . . . . 11  |-  ( ( 4  x.  0 )  +  2 )  = ; 0
2
3414, 5, 34, 2, 71, 326, 16, 2, 5, 337, 340decma2c 10787 . . . . . . . . . 10  |-  ( ( 4  x. ;; 2 5 0 )  +  (;; 2 3 0  +  2 ) )  = ;;; 1 2 3 2
342 4t3e12 10819 . . . . . . . . . . 11  |-  ( 4  x.  3 )  = ; 1
2
34311, 2, 27, 342, 143, 11, 161decaddci 10792 . . . . . . . . . 10  |-  ( ( 4  x.  3 )  +  9 )  = ; 2
1
3446, 21, 48, 27, 1, 324, 16, 11, 2, 341, 343decma2c 10787 . . . . . . . . 9  |-  ( ( 4  x.  N )  + ;;; 2 3 0 9 )  = ;;;; 1 2 3 2 1
3455, 11, 11, 11, 230, 228, 186, 143decadd 10788 . . . . . . . . . . . 12  |-  ( 1  + ; 1 1 )  = ; 1
2
346245oveq1i 6096 . . . . . . . . . . . . . 14  |-  ( ( 1  x.  1 )  +  1 )  =  ( 1  +  1 )
347346, 143, 1543eqtri 2462 . . . . . . . . . . . . 13  |-  ( ( 1  x.  1 )  +  1 )  = ; 0
2
34811, 11, 5, 11, 228, 299, 11, 2, 5, 248, 347decmac 10786 . . . . . . . . . . . 12  |-  ( (; 1
1  x.  1 )  +  ( 1  +  0 ) )  = ; 1
2
34952, 11, 11, 2, 298, 345, 11, 21, 5, 348, 251decmac 10786 . . . . . . . . . . 11  |-  ( (;; 1 1 1  x.  1 )  +  ( 1  + ; 1 1 ) )  = ;; 1 2 3
35052, 11, 5, 11, 298, 230, 11, 2, 5, 266, 347decmac 10786 . . . . . . . . . . 11  |-  ( (;; 1 1 1  x.  1 )  +  1 )  = ;; 1 1 2
35111, 11, 11, 11, 228, 228, 53, 2, 52, 349, 350decma2c 10787 . . . . . . . . . 10  |-  ( (;; 1 1 1  x. ; 1
1 )  + ; 1 1 )  = ;;; 1 2 3 2
35253nn0cni 10583 . . . . . . . . . . 11  |- ;; 1 1 1  e.  CC
353352mulid1i 9380 . . . . . . . . . 10  |-  (;; 1 1 1  x.  1 )  = ;; 1 1 1
35453, 52, 11, 298, 11, 52, 351, 353decmul2c 10795 . . . . . . . . 9  |-  (;; 1 1 1  x. ;; 1 1 1 )  = ;;;; 1 2 3 2 1
355344, 354eqtr4i 2461 . . . . . . . 8  |-  ( ( 4  x.  N )  + ;;; 2 3 0 9 )  =  (;; 1 1 1  x. ;; 1 1 1 )
3569, 10, 50, 51, 53, 49, 318, 323, 355mod2xi 14090 . . . . . . 7  |-  ( ( 2 ^; 7 8 )  mod 
N )  =  (;;; 2 3 0 9  mod 
N )
357 eqid 2438 . . . . . . . 8  |- ; 7 8  = ; 7 8
358 4p1e5 10440 . . . . . . . . 9  |-  ( 4  +  1 )  =  5
359218, 77, 315mulcomli 9385 . . . . . . . . 9  |-  ( 2  x.  7 )  = ; 1
4
36011, 16, 358, 359decsuc 10770 . . . . . . . 8  |-  ( ( 2  x.  7 )  +  1 )  = ; 1
5
361175, 77, 108mulcomli 9385 . . . . . . . 8  |-  ( 2  x.  8 )  = ; 1
6
3622, 30, 18, 357, 24, 11, 360, 361decmul2c 10795 . . . . . . 7  |-  ( 2  x. ; 7 8 )  = ;; 1 5 6
363 eqid 2438 . . . . . . . . 9  |- ;; 1 9 4  = ;; 1 9 4
3642, 16deccl 10761 . . . . . . . . . 10  |- ; 2 4  e.  NN0
365 eqid 2438 . . . . . . . . . . 11  |- ; 2 4  = ; 2 4
3662, 16, 358, 365decsuc 10770 . . . . . . . . . 10  |-  (; 2 4  +  1 )  = ; 2 5
367 eqid 2438 . . . . . . . . . . . 12  |- ; 2 3  = ; 2 3
3682, 21, 100, 367decsuc 10770 . . . . . . . . . . 11  |-  (; 2 3  +  1 )  = ; 2 4
36934, 5, 11, 27, 325, 128, 368, 197decadd 10788 . . . . . . . . . 10  |-  (;; 2 3 0  + ; 1 9 )  = ;; 2 4 9
370364, 366, 369decsucc 10774 . . . . . . . . 9  |-  ( (;; 2 3 0  + ; 1
9 )  +  1 )  = ;; 2 5 0
371 9p4e13 10811 . . . . . . . . 9  |-  ( 9  +  4 )  = ; 1
3
37248, 27, 45, 16, 324, 363, 370, 21, 371decaddc 10789 . . . . . . . 8  |-  (;;; 2 3 0 9  + ;; 1 9 4 )  = ;;; 2 5 0 3
373372, 1eqtr4i 2461 . . . . . . 7  |-  (;;; 2 3 0 9  + ;; 1 9 4 )  =  N
374 eqid 2438 . . . . . . . . 9  |- ; 9 1  = ; 9 1
375 eqid 2438 . . . . . . . . . . . 12  |- ; 1 5  = ; 1 5
376218addid2i 9549 . . . . . . . . . . . . 13  |-  ( 0  +  7 )  =  7
377376, 206eqtri 2458 . . . . . . . . . . . 12  |-  ( 0  +  7 )  = ; 0
7
37878, 186oveq12i 6098 . . . . . . . . . . . . 13  |-  ( ( 1  x.  2 )  +  ( 0  +  1 ) )  =  ( 2  +  1 )
379378, 81eqtri 2458 . . . . . . . . . . . 12  |-  ( ( 1  x.  2 )  +  ( 0  +  1 ) )  =  3
38011, 5, 30, 170, 376decaddi 10791 . . . . . . . . . . . 12  |-  ( ( 5  x.  2 )  +  7 )  = ; 1
7
38111, 3, 5, 30, 375, 377, 2, 30, 11, 379, 380decmac 10786 . . . . . . . . . . 11  |-  ( (; 1
5  x.  2 )  +  ( 0  +  7 ) )  = ; 3
7
38284, 147oveq12i 6098 . . . . . . . . . . . . 13  |-  ( ( 1  x.  5 )  +  ( 0  +  2 ) )  =  ( 5  +  2 )
383 5p2e7 10451 . . . . . . . . . . . . 13  |-  ( 5  +  2 )  =  7
384382, 383eqtri 2458 . . . . . . . . . . . 12  |-  ( ( 1  x.  5 )  +  ( 0  +  2 ) )  =  7
38511, 3, 5, 11, 375, 230, 3, 24, 2, 384, 189decmac 10786 . . . . . . . . . . 11  |-  ( (; 1
5  x.  5 )  +  1 )  = ; 7
6
3862, 3, 5, 11, 74, 299, 39, 24, 30, 381, 385decma2c 10787 . . . . . . . . . 10  |-  ( (; 1
5  x. ; 2 5 )  +  ( 1  +  0 ) )  = ;; 3 7 6
38739nn0cni 10583 . . . . . . . . . . . . 13  |- ; 1 5  e.  CC
388387mul01i 9551 . . . . . . . . . . . 12  |-  (; 1 5  x.  0 )  =  0
389388oveq1i 6096 . . . . . . . . . . 11  |-  ( (; 1
5  x.  0 )  +  3 )  =  ( 0  +  3 )
390389, 171, 2073eqtri 2462 . . . . . . . . . 10  |-  ( (; 1
5  x.  0 )  +  3 )  = ; 0
3
3914, 5, 11, 21, 71, 371, 39, 21, 5, 386, 390decma2c 10787 . . . . . . . . 9  |-  ( (; 1
5  x. ;; 2 5 0 )  +  ( 9  +  4 ) )  = ;;; 3 7 6 3
39298, 186oveq12i 6098 . . . . . . . . . . 11  |-  ( ( 1  x.  3 )  +  ( 0  +  1 ) )  =  ( 3  +  1 )
393392, 100eqtri 2458 . . . . . . . . . 10  |-  ( ( 1  x.  3 )  +  ( 0  +  1 ) )  =  4
39411, 3, 5, 11, 375, 230, 21, 24, 11, 393, 210decmac 10786 . . . . . . . . 9  |-  ( (; 1
5  x.  3 )  +  1 )  = ; 4
6
3956, 21, 27, 11, 1, 374, 39, 24, 16, 391, 394decma2c 10787 . . . . . . . 8  |-  ( (; 1
5  x.  N )  + ; 9 1 )  = ;;;; 3 7 6 3 6
39645, 16deccl 10761 . . . . . . . . 9  |- ;; 1 9 4  e.  NN0
397 eqid 2438 . . . . . . . . . 10  |- ; 7 7  = ; 7 7
39811, 30deccl 10761 . . . . . . . . . . 11  |- ; 1 7  e.  NN0
399398, 3deccl 10761 . . . . . . . . . 10  |- ;; 1 7 5  e.  NN0
400 eqid 2438 . . . . . . . . . . . 12  |- ;; 1 7 5  = ;; 1 7 5
401398nn0cni 10583 . . . . . . . . . . . . . 14  |- ; 1 7  e.  CC
402401addid2i 9549 . . . . . . . . . . . . 13  |-  ( 0  + ; 1 7 )  = ; 1
7
40311, 30, 164, 402decsuc 10770 . . . . . . . . . . . 12  |-  ( ( 0  + ; 1 7 )  +  1 )  = ; 1 8
404 7p5e12 10800 . . . . . . . . . . . 12  |-  ( 7  +  5 )  = ; 1
2
4055, 30, 398, 3, 206, 400, 403, 2, 404decaddc 10789 . . . . . . . . . . 11  |-  ( 7  + ;; 1 7 5 )  = ;; 1 8 2
406245, 143oveq12i 6098 . . . . . . . . . . . . 13  |-  ( ( 1  x.  1 )  +  ( 1  +  1 ) )  =  ( 1  +  2 )
407406, 250eqtri 2458 . . . . . . . . . . . 12  |-  ( ( 1  x.  1 )  +  ( 1  +  1 ) )  =  3
408132mulid1i 9380 . . . . . . . . . . . . . 14  |-  ( 9  x.  1 )  =  9
409408oveq1i 6096 . . . . . . . . . . . . 13  |-  ( ( 9  x.  1 )  +  8 )  =  ( 9  +  8 )
410 9p8e17 10815 . . . . . . . . . . . . 13  |-  ( 9  +  8 )  = ; 1
7
411409, 410eqtri 2458 . . . . . . . . . . . 12  |-  ( ( 9  x.  1 )  +  8 )  = ; 1
7
41211, 27, 11, 18, 128, 243, 11, 30, 11, 407, 411decmac 10786 . . . . . . . . . . 11  |-  ( (; 1
9  x.  1 )  +  (; 1 8  +  0 ) )  = ; 3 7
413183mulid1i 9380 . . . . . . . . . . . . 13  |-  ( 4  x.  1 )  =  4
414413oveq1i 6096 . . . . . . . . . . . 12  |-  ( ( 4  x.  1 )  +  2 )  =  ( 4  +  2 )
415 4p2e6 10448 . . . . . . . . . . . 12  |-  ( 4  +  2 )  =  6
416414, 415, 873eqtri 2462 . . . . . . . . . . 11  |-  ( ( 4  x.  1 )  +  2 )  = ; 0
6
41745, 16, 63, 2, 363, 405, 11, 24, 5, 412, 416decmac 10786 . . . . . . . . . 10  |-  ( (;; 1 9 4  x.  1 )  +  ( 7  + ;; 1 7 5 ) )  = ;; 3 7 6
418132mulid2i 9381 . . . . . . . . . . . . . 14  |-  ( 1  x.  9 )  =  9
419175addid2i 9549 . . . . . . . . . . . . . 14  |-  ( 0  +  8 )  =  8
420418, 419oveq12i 6098 . . . . . . . . . . . . 13  |-  ( ( 1  x.  9 )  +  ( 0  +  8 ) )  =  ( 9  +  8 )
421420, 410eqtri 2458 . . . . . . . . . . . 12  |-  ( ( 1  x.  9 )  +  ( 0  +  8 ) )  = ; 1
7
422 9t9e81 10849 . . . . . . . . . . . . 13  |-  ( 9  x.  9 )  = ; 8
1
423183, 90, 358addcomli 9553 . . . . . . . . . . . . 13  |-  ( 1  +  4 )  =  5
42418, 11, 16, 422, 423decaddi 10791 . . . . . . . . . . . 12  |-  ( ( 9  x.  9 )  +  4 )  = ; 8
5
42511, 27, 5, 16, 128, 185, 27, 3, 18, 421, 424decmac 10786 . . . . . . . . . . 11  |-  ( (; 1
9  x.  9 )  +  ( 0  +  4 ) )  = ;; 1 7 5
426 9t4e36 10844 . . . . . . . . . . . . 13  |-  ( 9  x.  4 )  = ; 3
6
427132, 183, 426mulcomli 9385 . . . . . . . . . . . 12  |-  ( 4  x.  9 )  = ; 3
6
428 7p6e13 10801 . . . . . . . . . . . . 13  |-  ( 7  +  6 )  = ; 1
3
429218, 93, 428addcomli 9553 . . . . . . . . . . . 12  |-  ( 6  +  7 )  = ; 1
3
43021, 24, 30, 427, 100, 21, 429decaddci 10792 . . . . . . . . . . 11  |-  ( ( 4  x.  9 )  +  7 )  = ; 4
3
43145, 16, 5, 30, 363, 206, 27, 21, 16, 425, 430decmac 10786 . . . . . . . . . 10  |-  ( (;; 1 9 4  x.  9 )  +  7 )  = ;;; 1 7 5 3
43211, 27, 30, 30, 128, 397, 396, 21, 399, 417, 431decma2c 10787 . . . . . . . . 9  |-  ( (;; 1 9 4  x. ; 1
9 )  + ; 7 7 )  = ;;; 3 7 6 3
433183mulid2i 9381 . . . . . . . . . . . . 13  |-  ( 1  x.  4 )  =  4
434433, 171oveq12i 6098 . . . . . . . . . . . 12  |-  ( ( 1  x.  4 )  +  ( 0  +  3 ) )  =  ( 4  +  3 )
435 4p3e7 10449 . . . . . . . . . . . 12  |-  ( 4  +  3 )  =  7
436434, 435eqtri 2458 . . . . . . . . . . 11  |-  ( ( 1  x.  4 )  +  ( 0  +  3 ) )  =  7
43721, 24, 156, 426decsuc 10770 . . . . . . . . . . 11  |-  ( ( 9  x.  4 )  +  1 )  = ; 3
7
43811, 27, 5, 11, 128, 230, 16, 30, 21, 436, 437decmac 10786 . . . . . . . . . 10  |-  ( (; 1
9  x.  4 )  +  1 )  = ; 7
7
439 4t4e16 10820 . . . . . . . . . 10  |-  ( 4  x.  4 )  = ; 1
6
44016, 45, 16, 363, 24, 11, 438, 439decmul1c 10794 . . . . . . . . 9  |-  (;; 1 9 4  x.  4 )  = ;; 7 7 6
441396, 45, 16, 363, 24, 37, 432, 440decmul2c 10795 . . . . . . . 8  |-  (;; 1 9 4  x. ;; 1 9 4 )  = ;;;; 3 7 6 3 6
442395, 441eqtr4i 2461 . . . . . . 7  |-  ( (; 1
5  x.  N )  + ; 9 1 )  =  (;; 1 9 4  x. ;; 1 9 4 )
44310, 43, 44, 47, 42, 49, 356, 362, 373, 442mod2xnegi 14092 . . . . . 6  |-  ( ( 2 ^;; 1 5 6 )  mod 
N )  =  (; 9
1  mod  N )
444 eqid 2438 . . . . . . 7  |- ;; 1 5 6  = ;; 1 5 6
445129, 186oveq12i 6098 . . . . . . . . 9  |-  ( ( 2  x.  1 )  +  ( 0  +  1 ) )  =  ( 2  +  1 )
446445, 81eqtri 2458 . . . . . . . 8  |-  ( ( 2  x.  1 )  +  ( 0  +  1 ) )  =  3
44783, 77, 168mulcomli 9385 . . . . . . . . . 10  |-  ( 2  x.  5 )  =  10
448447, 169eqtri 2458 . . . . . . . . 9  |-  ( 2  x.  5 )  = ; 1
0
44911, 5, 186, 448decsuc 10770 . . . . . . . 8  |-  ( ( 2  x.  5 )  +  1 )  = ; 1
1
45011, 3, 5, 11, 375, 230, 2, 11, 11, 446, 449decma2c 10787 . . . . . . 7  |-  ( ( 2  x. ; 1 5 )  +  1 )  = ; 3 1
451 6t2e12 10824 . . . . . . . 8  |-  ( 6  x.  2 )  = ; 1
2
45293, 77, 451mulcomli 9385 . . . . . . 7  |-  ( 2  x.  6 )  = ; 1
2
4532, 39, 24, 444, 2, 11, 450, 452decmul2c 10795 . . . . . 6  |-  ( 2  x. ;; 1 5 6 )  = ;; 3 1 2
454 eqid 2438 . . . . . . . 8  |- ;; 7 7 2  = ;; 7 7 2
45530, 30, 164, 397decsuc 10770 . . . . . . . . 9  |-  (; 7 7  +  1 )  = ; 7 8
456218addid1i 9548 . . . . . . . . . . 11  |-  ( 7  +  0 )  =  7
457456, 206eqtri 2458 . . . . . . . . . 10  |-  ( 7  +  0 )  = ; 0
7
458115, 147oveq12i 6098 . . . . . . . . . . 11  |-  ( ( 3  x.  2 )  +  ( 0  +  2 ) )  =  ( 6  +  2 )
459 6p2e8 10455 . . . . . . . . . . 11  |-  ( 6  +  2 )  =  8
460458, 459eqtri 2458 . . . . . . . . . 10  |-  ( ( 3  x.  2 )  +  ( 0  +  2 ) )  =  8
461218, 83, 404addcomli 9553 . . . . . . . . . . 11  |-  ( 5  +  7 )  = ; 1
2
46211, 3, 30, 192, 143, 2, 461decaddci 10792 . . . . . . . . . 10  |-  ( ( 3  x.  5 )  +  7 )  = ; 2
2
4632, 3, 5, 30, 74, 457, 21, 2, 2, 460, 462decma2c 10787 . . . . . . . . 9  |-  ( ( 3  x. ; 2 5 )  +  ( 7  +  0 ) )  = ; 8 2
46497mul01i 9551 . . . . . . . . . . 11  |-  ( 3  x.  0 )  =  0
465464oveq1i 6096 . . . . . . . . . 10  |-  ( ( 3  x.  0 )  +  8 )  =  ( 0  +  8 )
466465, 419, 2613eqtri 2462 . . . . . . . . 9  |-  ( ( 3  x.  0 )  +  8 )  = ; 0
8
4674, 5, 30, 18, 71, 455, 21, 18, 5, 463, 466decma2c 10787 . . . . . . . 8  |-  ( ( 3  x. ;; 2 5 0 )  +  (; 7 7  +  1 ) )  = ;; 8 2 8
468212oveq1i 6096 . . . . . . . . 9  |-  ( ( 3  x.  3 )  +  2 )  =  ( 9  +  2 )
469468, 160eqtri 2458 . . . . . . . 8  |-  ( ( 3  x.  3 )  +  2 )  = ; 1
1
4706, 21, 37, 2, 1, 454, 21, 11, 11, 467, 469decma2c 10787 . . . . . . 7  |-  ( ( 3  x.  N )  + ;; 7 7 2 )  = ;;; 8 2 8 1
471186oveq2i 6097 . . . . . . . . . 10  |-  ( ( 9  x.  9 )  +  ( 0  +  1 ) )  =  ( ( 9  x.  9 )  +  1 )
47218, 11, 143, 422decsuc 10770 . . . . . . . . . 10  |-  ( ( 9  x.  9 )  +  1 )  = ; 8
2
473471, 472eqtri 2458 . . . . . . . . 9  |-  ( ( 9  x.  9 )  +  ( 0  +  1 ) )  = ; 8
2
474418oveq1i 6096 . . . . . . . . . 10  |-  ( ( 1  x.  9 )  +  9 )  =  ( 9  +  9 )
475 9p9e18 10816 . . . . . . . . . 10  |-  ( 9  +  9 )  = ; 1
8
476474, 475eqtri 2458 . . . . . . . . 9  |-  ( ( 1  x.  9 )  +  9 )  = ; 1
8
47727, 11, 5, 27, 374, 182, 27, 18, 11, 473, 476decmac 10786 . . . . . . . 8  |-  ( (; 9
1  x.  9 )  +  9 )  = ;; 8 2 8
47842nn0cni 10583 . . . . . . . . 9  |- ; 9 1  e.  CC
479478mulid1i 9380 . . . . . . . 8  |-  (; 9 1  x.  1 )  = ; 9 1
48042, 27, 11, 374, 11, 27, 477, 479decmul2c 10795 . . . . . . 7  |-  (; 9 1  x. ; 9 1 )  = ;;; 8 2 8 1
481470, 480eqtr4i 2461 . . . . . 6  |-  ( ( 3  x.  N )  + ;; 7 7 2 )  =  (; 9
1  x. ; 9 1 )
4829, 10, 40, 41, 42, 38, 443, 453, 481mod2xi 14090 . . . . 5  |-  ( ( 2 ^;; 3 1 2 )  mod 
N )  =  (;; 7 7 2  mod 
N )
483 eqid 2438 . . . . . 6  |- ;; 3 1 2  = ;; 3 1 2
484 eqid 2438 . . . . . . . . 9  |- ; 3 1  = ; 3 1
485320oveq1i 6096 . . . . . . . . . 10  |-  ( ( 2  x.  3 )  +  0 )  =  ( 6  +  0 )
486485, 268eqtri 2458 . . . . . . . . 9  |-  ( ( 2  x.  3 )  +  0 )  =  6
487129, 154eqtri 2458 . . . . . . . . 9  |-  ( 2  x.  1 )  = ; 0
2
4882, 21, 11, 484, 2, 5, 486, 487decmul2c 10795 . . . . . . . 8  |-  ( 2  x. ; 3 1 )  = ; 6
2
489488oveq1i 6096 . . . . . . 7  |-  ( ( 2  x. ; 3 1 )  +  0 )  =  (; 6
2  +  0 )
49025nn0cni 10583 . . . . . . . 8  |- ; 6 2  e.  CC
491490addid1i 9548 . . . . . . 7  |-  (; 6 2  +  0 )  = ; 6 2
492489, 491eqtri 2458 . . . . . 6  |-  ( ( 2  x. ; 3 1 )  +  0 )  = ; 6 2
4932, 22, 2, 483, 16, 5, 492, 124decmul2c 10795 . . . . 5  |-  ( 2  x. ;; 3 1 2 )  = ;; 6 2 4
494 eqid 2438 . . . . . . 7  |- ;; 2 7 0  = ;; 2 7 0
49530, 11deccl 10761 . . . . . . 7  |- ; 7 1  e.  NN0
496 eqid 2438 . . . . . . . . 9  |- ; 7 1  = ; 7 1
497 7p2e9 10458 . . . . . . . . . 10  |-  ( 7  +  2 )  =  9
498218, 77, 497addcomli 9553 . . . . . . . . 9  |-  ( 2  +  7 )  =  9
4992, 30, 30, 11, 165, 496, 498, 164decadd 10788 . . . . . . . 8  |-  (; 2 7  + ; 7 1 )  = ; 9
8
500132addid1i 9548 . . . . . . . . . 10  |-  ( 9  +  0 )  =  9
501500, 182eqtri 2458 . . . . . . . . 9  |-  ( 9  +  0 )  = ; 0
9
50252, 27deccl 10761 . . . . . . . . 9  |- ;; 1 1 9  e.  NN0
503 eqid 2438 . . . . . . . . . 10  |- ;; 2 3 8  = ;; 2 3 8
504502nn0cni 10583 . . . . . . . . . . 11  |- ;; 1 1 9  e.  CC
505504addid2i 9549 . . . . . . . . . 10  |-  ( 0  + ;; 1 1 9 )  = ;; 1 1 9
50611, 11, 2, 228, 250decaddi 10791 . . . . . . . . . . 11  |-  (; 1 1  +  2 )  = ; 1 3
507123, 79oveq12i 6098 . . . . . . . . . . . 12  |-  ( ( 2  x.  2 )  +  ( 1  +  0 ) )  =  ( 4  +  1 )
508507, 358eqtri 2458 . . . . . . . . . . 11  |-  ( ( 2  x.  2 )  +  ( 1  +  0 ) )  =  5
509115oveq1i 6096 . . . . . . . . . . . 12  |-  ( ( 3  x.  2 )  +  3 )  =  ( 6  +  3 )
510509, 144, 1823eqtri 2462 . . . . . . . . . . 11  |-  ( ( 3  x.  2 )  +  3 )  = ; 0
9
5112, 21, 11, 21, 367, 506, 2, 27, 5, 508, 510decmac 10786 . . . . . . . . . 10  |-  ( (; 2
3  x.  2 )  +  (; 1 1  +  2 ) )  = ; 5 9
512 9p6e15 10813 . . . . . . . . . . . 12  |-  ( 9  +  6 )  = ; 1
5
513132, 93, 512addcomli 9553 . . . . . . . . . . 11  |-  ( 6  +  9 )  = ; 1
5
51411, 24, 27, 108, 143, 3, 513decaddci 10792 . . . . . . . . . 10  |-  ( ( 8  x.  2 )  +  9 )  = ; 2
5
51534, 18, 52, 27, 503, 505, 2, 3, 2, 511, 514decmac 10786 . . . . . . . . 9  |-  ( (;; 2 3 8  x.  2 )  +  ( 0  + ;; 1 1 9 ) )  = ;; 5 9 5
516186oveq2i 6097 . . . . . . . . . . . 12  |-  ( ( 2  x.  5 )  +  ( 0  +  1 ) )  =  ( ( 2  x.  5 )  +  1 )
517516, 449eqtri 2458 . . . . . . . . . . 11  |-  ( ( 2  x.  5 )  +  ( 0  +  1 ) )  = ; 1
1
5182, 21, 5, 16, 367, 185, 3, 27, 11, 517, 194decmac 10786 . . . . . . . . . 10  |-  ( (; 2
3  x.  5 )  +  ( 0  +  4 ) )  = ;; 1 1 9
51934, 18, 5, 27, 503, 182, 3, 27, 16, 518, 198decmac 10786 . . . . . . . . 9  |-  ( (;; 2 3 8  x.  5 )  +  9 )  = ;;; 1 1 9 9
5202, 3, 5, 27, 74, 501, 35, 27, 502, 515, 519decma2c 10787 . . . . . . . 8  |-  ( (;; 2 3 8  x. ; 2
5 )  +  ( 9  +  0 ) )  = ;;; 5 9 5 9
52135nn0cni 10583 . . . . . . . . . . 11  |- ;; 2 3 8  e.  CC
522521mul01i 9551 . . . . . . . . . 10  |-  (;; 2 3 8  x.  0 )  =  0
523522oveq1i 6096 . . . . . . . . 9  |-  ( (;; 2 3 8  x.  0 )  +  8 )  =  ( 0  +  8 )
524523, 419, 2613eqtri 2462 . . . . . . . 8  |-  ( (;; 2 3 8  x.  0 )  +  8 )  = ; 0 8
5254, 5, 27, 18, 71, 499, 35, 18, 5, 520, 524decma2c 10787 . . . . . . 7  |-  ( (;; 2 3 8  x. ;; 2 5 0 )  +  (; 2 7  + ; 7 1 ) )  = ;;;; 5 9 5 9 8
526320, 186oveq12i 6098 . . . . . . . . . . . 12  |-  ( ( 2  x.  3 )  +  ( 0  +  1 ) )  =  ( 6  +  1 )
527526, 156eqtri 2458 . . . . . . . . . . 11  |-  ( ( 2  x.  3 )  +  ( 0  +  1 ) )  =  7
5282, 21, 5, 2, 367, 154, 21, 11, 11, 527, 469decmac 10786 . . . . . . . . . 10  |-  ( (; 2
3  x.  3 )  +  2 )  = ; 7
1
52921, 34, 18, 503, 16, 2, 528, 217decmul1c 10794 . . . . . . . . 9  |-  (;; 2 3 8  x.  3 )  = ;; 7 1 4
530529oveq1i 6096 . . . . . . . 8  |-  ( (;; 2 3 8  x.  3 )  +  0 )  =  (;; 7 1 4  +  0 )
531495, 16deccl 10761 . . . . . . . . . 10  |- ;; 7 1 4  e.  NN0
532531nn0cni 10583 . . . . . . . . 9  |- ;; 7 1 4  e.  CC
533532addid1i 9548 . . . . . . . 8  |-  (;; 7 1 4  +  0 )  = ;; 7 1 4
534530, 533eqtri 2458 . . . . . . 7  |-  ( (;; 2 3 8  x.  3 )  +  0 )  = ;; 7 1 4
5356, 21, 31, 5, 1, 494, 35, 16, 495, 525, 534decma2c 10787 . . . . . 6  |-  ( (;; 2 3 8  x.  N )  + ;; 2 7 0 )  = ;;;;; 5 9 5 9 8 4
53639, 16deccl 10761 . . . . . . 7  |- ;; 1 5 4  e.  NN0
537 eqid 2438 . . . . . . . 8  |- ;; 1 5 4  = ;; 1 5 4
5383, 16deccl 10761 . . . . . . . . 9  |- ; 5 4  e.  NN0
539538, 5deccl 10761 . . . . . . . 8  |- ;; 5 4 0  e.  NN0
5403, 3deccl 10761 . . . . . . . . 9  |- ; 5 5  e.  NN0
541 eqid 2438 . . . . . . . . . 10  |- ;; 5 4 0  = ;; 5 4 0
542 eqid 2438 . . . . . . . . . . 11  |- ; 5 4  = ; 5 4
54383addid2i 9549 . . . . . . . . . . 11  |-  ( 0  +  5 )  =  5
5445, 11, 3, 16, 230, 542, 543, 423decadd 10788 . . . . . . . . . 10  |-  ( 1  + ; 5 4 )  = ; 5
5
54583addid1i 9548 . . . . . . . . . 10  |-  ( 5  +  0 )  =  5
54611, 3, 538, 5, 375, 541, 544, 545decadd 10788 . . . . . . . . 9  |-  (; 1 5  + ;; 5 4 0 )  = ;; 5 5 5
547 eqid 2438 . . . . . . . . . . 11  |- ; 5 5  = ; 5 5
5483, 3, 86, 547decsuc 10770 . . . . . . . . . 10  |-  (; 5 5  +  1 )  = ; 5 6
549 7t7e49 10834 . . . . . . . . . . 11  |-  ( 7  x.  7 )  = ; 4
9
550 5p5e10 10454 . . . . . . . . . . . 12  |-  ( 5  +  5 )  =  10
551550, 169eqtri 2458 . . . . . . . . . . 11  |-  ( 5  +  5 )  = ; 1
0
55216, 27, 11, 5, 549, 551, 358, 500decadd 10788 . . . . . . . . . 10  |-  ( ( 7  x.  7 )  +  ( 5  +  5 ) )  = ; 5
9
55316, 27, 24, 549, 358, 3, 512decaddci 10792 . . . . . . . . . 10  |-  ( ( 7  x.  7 )  +  6 )  = ; 5
5
55430, 30, 3, 24, 397, 548, 30, 3, 3, 552, 553decmac 10786 . . . . . . . . 9  |-  ( (; 7
7  x.  7 )  +  (; 5 5  +  1 ) )  = ;; 5 9 5
55583, 183, 193addcomli 9553 . . . . . . . . . 10  |-  ( 4  +  5 )  =  9
55611, 16, 3, 359, 555decaddi 10791 . . . . . . . . 9  |-  ( ( 2  x.  7 )  +  5 )  = ; 1
9
55737, 2, 540, 3, 454, 546, 30, 27, 11, 554, 556decmac 10786 . . . . . . . 8  |-  ( (;; 7 7 2  x.  7 )  +  (; 1
5  + ;; 5 4 0 ) )  = ;;; 5 9 5 9
558543oveq2i 6097 . . . . . . . . . . 11  |-  ( ( 7  x.  7 )  +  ( 0  +  5 ) )  =  ( ( 7  x.  7 )  +  5 )
559 9p5e14 10812 . . . . . . . . . . . 12  |-  ( 9  +  5 )  = ; 1
4
56016, 27, 3, 549, 358, 16, 559decaddci 10792 . . . . . . . . . . 11  |-  ( ( 7  x.  7 )  +  5 )  = ; 5
4
561558, 560eqtri 2458 . . . . . . . . . 10  |-  ( ( 7  x.  7 )  +  ( 0  +  5 ) )  = ; 5
4
56216, 358, 549decsucc 10774 . . . . . . . . . 10  |-  ( ( 7  x.  7 )  +  1 )  = ; 5
0
56330, 30, 5, 11, 397, 276, 30, 5, 3, 561, 562decmac 10786 . . . . . . . . 9  |-  ( (; 7
7  x.  7 )  +  ( 0  +  1 ) )  = ;; 5 4 0
564 4p4e8 10450 . . . . . . . . . 10  |-  ( 4  +  4 )  =  8
56511, 16, 16, 359, 564decaddi 10791 . . . . . . . . 9  |-  ( ( 2  x.  7 )  +  4 )  = ; 1
8
56637, 2, 5, 16, 454, 101, 30, 18, 11, 563, 565decmac 10786 . . . . . . . 8  |-  ( (;; 7 7 2  x.  7 )  +  4 )  = ;;; 5 4 0 8
56730, 30, 39, 16, 397, 537, 38, 18, 539, 557, 566decma2c 10787 . . . . . . 7  |-  ( (;; 7 7 2  x. ; 7
7 )  + ;; 1 5 4 )  = ;;;; 5 9 5 9 8
56811, 16, 358, 315decsuc 10770 . . . . . . . . . . 11  |-  ( ( 7  x.  2 )  +  1 )  = ; 1
5
5692, 30, 30, 397, 16, 11, 568, 315decmul1c 10794 . . . . . . . . . 10  |-  (; 7 7  x.  2 )  = ;; 1 5 4
570569oveq1i 6096 . . . . . . . . 9  |-  ( (; 7
7  x.  2 )  +  0 )  =  (;; 1 5 4  +  0 )
571536nn0cni 10583 . . . . . . . . . 10  |- ;; 1 5 4  e.  CC
572571addid1i 9548 . . . . . . . . 9  |-  (;; 1 5 4  +  0 )  = ;; 1 5 4
573570, 572eqtri 2458 . . . . . . . 8  |-  ( (; 7
7  x.  2 )  +  0 )  = ;; 1 5 4
5742, 37, 2, 454, 16, 5, 573, 124decmul1c 10794 . . . . . . 7  |-  (;; 7 7 2  x.  2 )  = ;;; 1 5 4 4
57538, 37, 2, 454, 16, 536, 567, 574decmul2c 10795 . . . . . 6  |-  (;; 7 7 2  x. ;; 7 7 2 )  = ;;;;; 5 9 5 9 8 4
576535, 575eqtr4i 2461 . . . . 5  |-  ( (;; 2 3 8  x.  N )  + ;; 2 7 0 )  =  (;; 7 7 2  x. ;; 7 7 2 )
5779, 10, 33, 36, 38, 32, 482, 493, 576mod2xi 14090 . . . 4  |-  ( ( 2 ^;; 6 2 4 )  mod 
N )  =  (;; 2 7 0  mod 
N )
578 eqid 2438 . . . . 5  |- ;; 6 2 4  = ;; 6 2 4
579 eqid 2438 . . . . . . . 8  |- ; 6 2  = ; 6 2
580452oveq1i 6096 . . . . . . . . 9  |-  ( ( 2  x.  6 )  +  0 )  =  (; 1 2  +  0 )
58112nn0cni 10583 . . . . . . . . . 10  |- ; 1 2  e.  CC
582581addid1i 9548 . . . . . . . . 9  |-  (; 1 2  +  0 )  = ; 1 2
583580, 582eqtri 2458 . . . . . . . 8  |-  ( ( 2  x.  6 )  +  0 )  = ; 1
2
5842, 24, 2, 579, 16, 5, 583, 124decmul2c 10795 . . . . . . 7  |-  ( 2  x. ; 6 2 )  = ;; 1 2 4
585584oveq1i 6096 . . . . . 6  |-  ( ( 2  x. ; 6 2 )  +  0 )  =  (;; 1 2 4  +  0 )
58617nn0cni 10583 . . . . . . 7  |- ;; 1 2 4  e.  CC
587586addid1i 9548 . . . . . 6  |-  (;; 1 2 4  +  0 )  = ;; 1 2 4
588585, 587eqtri 2458 . . . . 5  |-  ( ( 2  x. ; 6 2 )  +  0 )  = ;; 1 2 4
589183, 77, 329mulcomli 9385 . . . . . 6  |-  ( 2  x.  4 )  =  8
590589, 261eqtri 2458 . . . . 5  |-  ( 2  x.  4 )  = ; 0
8
5912, 25, 16, 578, 18, 5, 588, 590decmul2c 10795 . . . 4  |-  ( 2  x. ;; 6 2 4 )  = ;;; 1 2 4 8
592 eqid 2438 . . . . . 6  |- ;; 3 1 3  = ;; 3 1 3
59321, 11, 27, 484, 100, 235decaddci2 10793 . . . . . . 7  |-  (; 3 1  +  9 )  = ; 4 0
594183addid1i 9548 . . . . . . . . 9  |-  ( 4  +  0 )  =  4
595594, 101eqtri 2458 . . . . . . . 8  |-  ( 4  +  0 )  = ; 0
4
59611, 16deccl 10761 . . . . . . . 8  |- ; 1 4  e.  NN0
597 eqid 2438 . . . . . . . . 9  |- ; 2 9  = ; 2 9
598596nn0cni 10583 . . . . . . . . . 10  |- ; 1 4  e.  CC
599598addid2i 9549 . . . . . . . . 9  |-  ( 0  + ; 1 4 )  = ; 1
4
600123, 250oveq12i 6098 . . . . . . . . . 10  |-  ( ( 2  x.  2 )  +  ( 1  +  2 ) )  =  ( 4  +  3 )
601600, 435eqtri 2458 . . . . . . . . 9  |-  ( ( 2  x.  2 )  +  ( 1  +  2 ) )  =  7
60211, 18, 16, 133, 143, 2, 332decaddci 10792 . . . . . . . . 9  |-  ( ( 9  x.  2 )  +  4 )  = ; 2
2
6032, 27, 11, 16, 597, 599, 2, 2, 2, 601, 602decmac 10786 . . . . . . . 8  |-  ( (; 2
9  x.  2 )  +  ( 0  + ; 1
4 ) )  = ; 7
2
604184oveq2i 6097 . . . . . . . . . 10  |-  ( ( 2  x.  5 )  +  ( 0  +  4 ) )  =  ( ( 2  x.  5 )  +  4 )
60511, 5, 16, 448, 184decaddi 10791 . . . . . . . . . 10  |-  ( ( 2  x.  5 )  +  4 )  = ; 1
4
606604, 605eqtri 2458 . . . . . . . . 9  |-  ( ( 2  x.  5 )  +  ( 0  +  4 ) )  = ; 1
4
607 9t5e45 10845 . . . . . . . . . 10  |-  ( 9  x.  5 )  = ; 4
5
60816, 3, 16, 607, 193decaddi 10791 . . . . . . . . 9  |-  ( ( 9  x.  5 )  +  4 )  = ; 4
9
6092, 27, 5, 16, 597, 101, 3, 27, 16, 606, 608decmac 10786 . . . . . . . 8  |-  ( (; 2
9  x.  5 )  +  4 )  = ;; 1 4 9
6102, 3, 5, 16, 74, 595, 28, 27, 596, 603, 609decma2c 10787 . . . . . . 7  |-  ( (; 2
9  x. ; 2 5 )  +  ( 4  +  0 ) )  = ;; 7 2 9
611149mul01i 9551 . . . . . . . . 9  |-  (; 2 9  x.  0 )  =  0
612611oveq1i 6096 . . . . . . . 8  |-  ( (; 2
9  x.  0 )  +  0 )  =  ( 0  +  0 )
613612, 246, 2623eqtri 2462 . . . . . . 7  |-  ( (; 2
9  x.  0 )  +  0 )  = ; 0
0
6144, 5, 16, 5, 71, 593, 28, 5, 5, 610, 613decma2c 10787 . . . . . 6  |-  ( (; 2
9  x. ;; 2 5 0 )  +  (; 3 1  +  9 ) )  = ;;; 7 2 9 0
615320, 171oveq12i 6098 . . . . . . . 8  |-  ( ( 2  x.  3 )  +  ( 0  +  3 ) )  =  ( 6  +  3 )
616615, 144eqtri 2458 . . . . . . 7  |-  ( ( 2  x.  3 )  +  ( 0  +  3 ) )  =  9
617 9t3e27 10843 . . . . . . . 8  |-  ( 9  x.  3 )  = ; 2
7
618 7p3e10 10459 . . . . . . . 8  |-  ( 7  +  3 )  =  10
6192, 30, 21, 617, 81, 618decaddci2 10793 . . . . . . 7  |-  ( ( 9  x.  3 )  +  3 )  = ; 3
0
6202, 27, 5, 21, 597, 207, 21, 5, 21, 616, 619decmac 10786 . . . . . 6  |-  ( (; 2
9  x.  3 )  +  3 )  = ; 9
0
6216, 21, 22, 21, 1, 592, 28, 5, 27, 614, 620decma2c 10787 . . . . 5  |-  ( (; 2
9  x.  N )  + ;; 3 1 3 )  = ;;;; 7 2 9 0 0
62263, 27deccl 10761 . . . . . . . . 9  |- ;; 1 8 9  e.  NN0
623 eqid 2438 . . . . . . . . . 10  |- ;; 1 8 9  = ;; 1 8 9
624175, 183, 332addcomli 9553 . . . . . . . . . . . 12  |-  ( 4  +  8 )  = ; 1
2
62511, 16, 18, 315, 143, 2, 624decaddci 10792 . . . . . . . . . . 11  |-  ( ( 7  x.  2 )  +  8 )  = ; 2
2
6262, 30, 11, 18, 165, 243, 2, 2, 2, 601, 625decmac 10786 . . . . . . . . . 10  |-  ( (; 2
7  x.  2 )  +  (; 1 8  +  0 ) )  = ; 7 2
627311oveq1i 6096 . . . . . . . . . . 11  |-  ( ( 0  x.  2 )  +  9 )  =  ( 0  +  9 )
628627, 197, 1823eqtri 2462 . . . . . . . . . 10  |-  ( ( 0  x.  2 )  +  9 )  = ; 0
9
62931, 5, 63, 27, 494, 623, 2, 27, 5, 626, 628decmac 10786 . . . . . . . . 9  |-  ( (;; 2 7 0  x.  2 )  + ;; 1 8 9 )  = ;; 7 2 9
63030, 2, 30, 165, 27, 16, 565, 549decmul1c 10794 . . . . . . . . . . . 12  |-  (; 2 7  x.  7 )  = ;; 1 8 9
631630oveq1i 6096 . . . . . . . . . . 11  |-  ( (; 2
7  x.  7 )  +  0 )  =  (;; 1 8 9  +  0 )
632622nn0cni 10583 . . . . . . . . . . . 12  |- ;; 1 8 9  e.  CC
633632addid1i 9548 . . . . . . . . . . 11  |-  (;; 1 8 9  +  0 )  = ;; 1 8 9
634631, 633eqtri 2458 . . . . . . . . . 10  |-  ( (; 2
7  x.  7 )  +  0 )  = ;; 1 8 9
635218mul02i 9550 . . . . . . . . . . 11  |-  ( 0  x.  7 )  =  0
636635, 262eqtri 2458 . . . . . . . . . 10  |-  ( 0  x.  7 )  = ; 0
0
63730, 31, 5, 494, 5, 5, 634, 636decmul1c 10794 . . . . . . . . 9  |-  (;; 2 7 0  x.  7 )  = ;;; 1 8 9 0
63832, 2, 30, 165, 5, 622, 629, 637decmul2c 10795 . . . . . . . 8  |-  (;; 2 7 0  x. ; 2 7 )  = ;;; 7 2 9 0
639638oveq1i 6096 . . . . . . 7  |-  ( (;; 2 7 0  x. ; 2
7 )  +  0 )  =  (;;; 7 2 9 0  +  0 )
64030, 2deccl 10761 . . . . . . . . . . 11  |- ; 7 2  e.  NN0
641640, 27deccl 10761 . . . . . . . . . 10  |- ;; 7 2 9  e.  NN0
642641, 5deccl 10761 . . . . . . . . 9  |- ;;; 7 2 9 0  e.  NN0
643642nn0cni 10583 . . . . . . . 8  |- ;;; 7 2 9 0  e.  CC
644643addid1i 9548 . . . . . . 7  |-  (;;; 7 2 9 0  +  0 )  = ;;; 7 2 9 0
645639, 644eqtri 2458 . . . . . 6  |-  ( (;; 2 7 0  x. ; 2
7 )  +  0 )  = ;;; 7 2 9 0
64632nn0cni 10583 . . . . . . . 8  |- ;; 2 7 0  e.  CC
647646mul01i 9551 . . . . . . 7  |-  (;; 2 7 0  x.  0 )  =  0
648647, 262eqtri 2458 . . . . . 6  |-  (;; 2 7 0  x.  0 )  = ; 0 0
64932, 31, 5, 494, 5, 5, 645, 648decmul2c 10795 . . . . 5  |-  (;; 2 7 0  x. ;; 2 7 0 )  = ;;;; 7 2 9 0 0
650621, 649eqtr4i 2461 . . . 4  |-  ( (; 2
9  x.  N )  + ;; 3 1 3 )  =  (;; 2 7 0  x. ;; 2 7 0 )
6519, 10, 26, 29, 32, 23, 577, 591, 650mod2xi 14090 . . 3  |-  ( ( 2 ^;;; 1 2 4 8 )  mod  N )  =  (;; 3 1 3  mod  N
)
652 cu2 11956 . . . 4  |-  ( 2 ^ 3 )  =  8
653652oveq1i 6096 . . 3  |-  ( ( 2 ^ 3 )  mod  N )  =  ( 8  mod  N
)
654 eqid 2438 . . . 4  |- ;;; 1 2 4 8  = ;;; 1 2 4 8
655 eqid 2438 . . . . 5  |- ;; 1 2 4  = ;; 1 2 4
65612, 16, 358, 655decsuc 10770 . . . 4  |-  (;; 1 2 4  +  1 )  = ;; 1 2 5
657 8p3e11 10803 . . . 4  |-  ( 8  +  3 )  = ; 1
1
65817, 18, 21, 654, 656, 11, 657decaddci 10792 . . 3  |-  (;;; 1 2 4 8  +  3 )  = ;;; 1 2 5 1
6599nncni 10324 . . . . . . 7  |-  N  e.  CC
660659mulid2i 9381 . . . . . 6  |-  ( 1  x.  N )  =  N
661660, 1eqtri 2458 . . . . 5  |-  ( 1  x.  N )  = ;;; 2 5 0 3
6626, 21, 100, 661decsuc 10770 . . . 4  |-  ( ( 1  x.  N )  +  1 )  = ;;; 2 5 0 4
663186oveq2i 6097 . . . . . . 7  |-  ( ( 3  x.  8 )  +  ( 0  +  1 ) )  =  ( ( 3  x.  8 )  +  1 )
664175, 97, 217mulcomli 9385 . . . . . . . 8  |-  ( 3  x.  8 )  = ; 2
4
6652, 16, 358, 664decsuc 10770 . . . . . . 7  |-  ( ( 3  x.  8 )  +  1 )  = ; 2
5
666663, 665eqtri 2458 . . . . . 6  |-  ( ( 3  x.  8 )  +  ( 0  +  1 ) )  = ; 2
5
667175mulid2i 9381 . . . . . . . 8  |-  ( 1  x.  8 )  =  8
668667oveq1i 6096 . . . . . . 7  |-  ( ( 1  x.  8 )  +  2 )  =  ( 8  +  2 )
669 8p2e10 10460 . . . . . . 7  |-  ( 8  +  2 )  =  10
670668, 669, 1693eqtri 2462 . . . . . 6  |-  ( ( 1  x.  8 )  +  2 )  = ; 1
0
67121, 11, 5, 2, 484, 154, 18, 5, 11, 666, 670decmac 10786 . . . . 5  |-  ( (; 3
1  x.  8 )  +  2 )  = ;; 2 5 0
67218, 22, 21, 592, 16, 2, 671, 664decmul1c 10794 . . . 4  |-  (;; 3 1 3  x.  8 )  = ;;; 2 5 0 4
673662, 672eqtr4i 2461 . . 3  |-  ( ( 1  x.  N )  +  1 )  =  (;; 3 1 3  x.  8 )
6749, 10, 19, 20, 23, 11, 21, 18, 651, 653, 658, 673modxai 14089 . 2  |-  ( ( 2 ^;;; 1 2 5 1 )  mod  N )  =  ( 1  mod 
N )
675 eqid 2438 . . . 4  |- ;;; 1 2 5 1  = ;;; 1 2 5 1
676 eqid 2438 . . . . . 6  |- ;; 1 2 5  = ;; 1 2 5
677 eqid 2438 . . . . . . 7  |- ; 1 2  = ; 1 2
678129, 246oveq12i 6098 . . . . . . . 8  |-  ( ( 2  x.  1 )  +  ( 0  +  0 ) )  =  ( 2  +  0 )
679678, 301eqtri 2458 . . . . . . 7  |-  ( ( 2  x.  1 )  +  ( 0  +  0 ) )  =  2
680123oveq1i 6096 . . . . . . . 8  |-  ( ( 2  x.  2 )  +  1 )  =  ( 4  +  1 )
6813dec0h 10763 . . . . . . . 8  |-  5  = ; 0 5
682680, 358, 6813eqtri 2462 . . . . . . 7  |-  ( ( 2  x.  2 )  +  1 )  = ; 0
5
68311, 2, 5, 11, 677, 230, 2, 3, 5, 679, 682decma2c 10787 . . . . . 6  |-  ( ( 2  x. ; 1 2 )  +  1 )  = ; 2 5
6842, 12, 3, 676, 5, 11, 683, 448decmul2c 10795 . . . . 5  |-  ( 2  x. ;; 1 2 5 )  = ;; 2 5 0
6854, 5, 5, 684, 246decaddi 10791 . . . 4  |-  ( ( 2  x. ;; 1 2 5 )  +  0 )  = ;; 2 5 0
6862, 13, 11, 675, 2, 5, 685, 487decmul2c 10795 . . 3  |-  ( 2  x. ;;; 1 2 5 1 )  = ;;; 2 5 0 2
687 eqid 2438 . . . . . . 7  |- ;;; 2 5 0 2  = ;;; 2 5 0 2
6886, 2, 81, 687decsuc 10770 . . . . . 6  |-  (;;; 2 5 0 2  +  1 )  = ;;; 2 5 0 3
6891, 688eqtr4i 2461 . . . . 5  |-  N  =  (;;; 2 5 0 2  +  1 )
690689oveq1i 6096 . . . 4  |-  ( N  -  1 )  =  ( (;;; 2 5 0 2  +  1 )  - 
1 )
6916, 2deccl 10761 . . . . . 6  |- ;;; 2 5 0 2  e.  NN0
692691nn0cni 10583 . . . . 5  |- ;;; 2 5 0 2  e.  CC
693 pncan 9608 . . . . 5  |-  ( (;;; 2 5 0 2  e.  CC  /\  1  e.  CC )  ->  (
(;;; 2 5 0 2  +  1 )  - 
1 )  = ;;; 2 5 0 2 )
694692, 90, 693mp2an 672 . . . 4  |-  ( (;;; 2 5 0 2  +  1 )  -  1 )  = ;;; 2 5 0 2
695690, 694eqtri 2458 . . 3  |-  ( N  -  1 )  = ;;; 2 5 0 2
696686, 695eqtr4i 2461 . 2  |-  ( 2  x. ;;; 1 2 5 1 )  =  ( N  -  1 )
697659mul02i 9550 . . . 4  |-  ( 0  x.  N )  =  0
698697oveq1i 6096 . . 3  |-  ( ( 0  x.  N )  +  1 )  =  ( 0  +  1 )
699245, 186eqtr4i 2461 . . 3  |-  ( 1  x.  1 )  =  ( 0  +  1 )
700698, 699eqtr4i 2461 . 2  |-  ( ( 0  x.  N )  +  1 )  =  ( 1  x.  1 )
7019, 10, 14, 15, 11, 11, 674, 696, 700mod2xi 14090 1  |-  ( ( 2 ^ ( N  -  1 ) )  mod  N )  =  ( 1  mod  N
)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1369    e. wcel 1756  (class class class)co 6086   CCcc 9272   0cc0 9274   1c1 9275    + caddc 9277    x. cmul 9279    - cmin 9587   NNcn 10314   2c2 10363   3c3 10364   4c4 10365   5c5 10366   6c6 10367   7c7 10368   8c8 10369   9c9 10370   10c10 10371  ;cdc 10747    mod cmo 11700   ^cexp 11857
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pow 4465  ax-pr 4526  ax-un 6367  ax-cnex 9330  ax-resscn 9331  ax-1cn 9332  ax-icn 9333  ax-addcl 9334  ax-addrcl 9335  ax-mulcl 9336  ax-mulrcl 9337  ax-mulcom 9338  ax-addass 9339  ax-mulass 9340  ax-distr 9341  ax-i2m1 9342  ax-1ne0 9343  ax-1rid 9344  ax-rnegex 9345  ax-rrecex 9346  ax-cnre 9347  ax-pre-lttri 9348  ax-pre-lttrn 9349  ax-pre-ltadd 9350  ax-pre-mulgt0 9351  ax-pre-sup 9352
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2715  df-rex 2716  df-reu 2717  df-rmo 2718  df-rab 2719  df-v 2969  df-sbc 3182  df-csb 3284  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-pss 3339  df-nul 3633  df-if 3787  df-pw 3857  df-sn 3873  df-pr 3875  df-tp 3877  df-op 3879  df-uni 4087  df-iun 4168  df-br 4288  df-opab 4346  df-mpt 4347  df-tr 4381  df-eprel 4627  df-id 4631  df-po 4636  df-so 4637  df-fr 4674  df-we 4676  df-ord 4717  df-on 4718  df-lim 4719  df-suc 4720  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5376  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-riota 6047  df-ov 6089  df-oprab 6090  df-mpt2 6091  df-om 6472  df-2nd 6573  df-recs 6824  df-rdg 6858  df-er 7093  df-en 7303  df-dom 7304  df-sdom 7305  df-sup 7683  df-pnf 9412  df-mnf 9413  df-xr 9414  df-ltxr 9415  df-le 9416  df-sub 9589  df-neg 9590  df-div 9986  df-nn 10315  df-2 10372  df-3 10373  df-4 10374  df-5 10375  df-6 10376  df-7 10377  df-8 10378  df-9 10379  df-10 10380  df-n0 10572  df-z 10639  df-dec 10748  df-uz 10854  df-rp 10984  df-fl 11634  df-mod 11701  df-seq 11799  df-exp 11858
This theorem is referenced by:  2503prm  14156
  Copyright terms: Public domain W3C validator