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

Theorem 4001lem1 15105
Description: Lemma for 4001prm 15109. Calculate a power mod. In decimal, we calculate  2 ^ 1 2  =  4 0 9 6  =  N  +  9 5,  2 ^ 2 4  =  ( 2 ^ 1 2 ) ^ 2  ==  9
5 ^ 2  =  2 N  +  1 0 2 3,  2 ^ 2 5  =  2 ^ 2 4  x.  2  ==  1 0 2 3  x.  2  =  2 0 4 6,  2 ^ 5 0  =  ( 2 ^ 2 5 ) ^ 2  ==  2
0 4 6 ^ 2  =  1 0 4 6 N  + 
1 0 7 0,  2 ^ 1 0 0  =  ( 2 ^ 5 0 ) ^ 2  ==  1 0 7 0 ^ 2  =  2 8 6 N  + 
6 1 4 and  2 ^ 2 0 0  =  ( 2 ^ 1 0 0 ) ^ 2  ==  6 1 4 ^ 2  =  9 4 N  +  9 0 2  ==  9 0 2. (Contributed by Mario Carneiro, 3-Mar-2014.) (Revised by Mario Carneiro, 20-Apr-2015.)
Hypothesis
Ref Expression
4001prm.1  |-  N  = ;;; 4 0 0 1
Assertion
Ref Expression
4001lem1  |-  ( ( 2 ^;; 2 0 0 )  mod 
N )  =  (;; 9 0 2  mod 
N )

Proof of Theorem 4001lem1
StepHypRef Expression
1 4001prm.1 . . 3  |-  N  = ;;; 4 0 0 1
2 4nn0 10890 . . . . . 6  |-  4  e.  NN0
3 0nn0 10886 . . . . . 6  |-  0  e.  NN0
42, 3deccl 11067 . . . . 5  |- ; 4 0  e.  NN0
54, 3deccl 11067 . . . 4  |- ;; 4 0 0  e.  NN0
6 1nn 10622 . . . 4  |-  1  e.  NN
75, 6decnncl 11066 . . 3  |- ;;; 4 0 0 1  e.  NN
81, 7eqeltri 2507 . 2  |-  N  e.  NN
9 2nn 10769 . 2  |-  2  e.  NN
10 10nn0 10896 . . 3  |-  10  e.  NN0
1110, 3deccl 11067 . 2  |- ; 10 0  e.  NN0
12 9nn0 10895 . . . 4  |-  9  e.  NN0
1312, 2deccl 11067 . . 3  |- ; 9 4  e.  NN0
1413nn0zi 10964 . 2  |- ; 9 4  e.  ZZ
15 6nn0 10892 . . . 4  |-  6  e.  NN0
16 1nn0 10887 . . . 4  |-  1  e.  NN0
1715, 16deccl 11067 . . 3  |- ; 6 1  e.  NN0
1817, 2deccl 11067 . 2  |- ;; 6 1 4  e.  NN0
1912, 3deccl 11067 . . 3  |- ; 9 0  e.  NN0
20 2nn0 10888 . . 3  |-  2  e.  NN0
2119, 20deccl 11067 . 2  |- ;; 9 0 2  e.  NN0
22 5nn0 10891 . . . 4  |-  5  e.  NN0
2322, 3deccl 11067 . . 3  |- ; 5 0  e.  NN0
24 8nn0 10894 . . . . . 6  |-  8  e.  NN0
2520, 24deccl 11067 . . . . 5  |- ; 2 8  e.  NN0
2625, 15deccl 11067 . . . 4  |- ;; 2 8 6  e.  NN0
2726nn0zi 10964 . . 3  |- ;; 2 8 6  e.  ZZ
28 7nn0 10893 . . . . 5  |-  7  e.  NN0
2910, 28deccl 11067 . . . 4  |- ; 10 7  e.  NN0
3029, 3deccl 11067 . . 3  |- ;; 10 7 0  e.  NN0
3120, 22deccl 11067 . . . 4  |- ; 2 5  e.  NN0
3210, 2deccl 11067 . . . . . 6  |- ; 10 4  e.  NN0
3332, 15deccl 11067 . . . . 5  |- ;; 10 4 6  e.  NN0
3433nn0zi 10964 . . . 4  |- ;; 10 4 6  e.  ZZ
3520, 3deccl 11067 . . . . . 6  |- ; 2 0  e.  NN0
3635, 2deccl 11067 . . . . 5  |- ;; 2 0 4  e.  NN0
3736, 15deccl 11067 . . . 4  |- ;;; 2 0 4 6  e.  NN0
3820, 2deccl 11067 . . . . 5  |- ; 2 4  e.  NN0
39 0z 10950 . . . . 5  |-  0  e.  ZZ
4010, 20deccl 11067 . . . . . 6  |- ; 10 2  e.  NN0
41 3nn0 10889 . . . . . 6  |-  3  e.  NN0
4240, 41deccl 11067 . . . . 5  |- ;; 10 2 3  e.  NN0
4316, 20deccl 11067 . . . . . 6  |- ; 1 2  e.  NN0
44 2z 10971 . . . . . 6  |-  2  e.  ZZ
4512, 22deccl 11067 . . . . . 6  |- ; 9 5  e.  NN0
46 1z 10969 . . . . . . 7  |-  1  e.  ZZ
4715, 2deccl 11067 . . . . . . 7  |- ; 6 4  e.  NN0
48 2exp6 15051 . . . . . . . 8  |-  ( 2 ^ 6 )  = ; 6
4
4948oveq1i 6313 . . . . . . 7  |-  ( ( 2 ^ 6 )  mod  N )  =  (; 6 4  mod  N
)
50 6cn 10693 . . . . . . . 8  |-  6  e.  CC
51 2cn 10682 . . . . . . . 8  |-  2  e.  CC
52 6t2e12 11130 . . . . . . . 8  |-  ( 6  x.  2 )  = ; 1
2
5350, 51, 52mulcomli 9652 . . . . . . 7  |-  ( 2  x.  6 )  = ; 1
2
54 eqid 2423 . . . . . . . . 9  |- ; 9 5  = ; 9 5
55 eqid 2423 . . . . . . . . . 10  |- ;; 4 0 0  = ;; 4 0 0
56 9cn 10699 . . . . . . . . . . . 12  |-  9  e.  CC
5756addid1i 9822 . . . . . . . . . . 11  |-  ( 9  +  0 )  =  9
5812dec0h 11069 . . . . . . . . . . 11  |-  9  = ; 0 9
5957, 58eqtri 2452 . . . . . . . . . 10  |-  ( 9  +  0 )  = ; 0
9
60 eqid 2423 . . . . . . . . . . 11  |- ; 4 0  = ; 4 0
61 00id 9810 . . . . . . . . . . . 12  |-  ( 0  +  0 )  =  0
623dec0h 11069 . . . . . . . . . . . 12  |-  0  = ; 0 0
6361, 62eqtri 2452 . . . . . . . . . . 11  |-  ( 0  +  0 )  = ; 0
0
64 4cn 10689 . . . . . . . . . . . . . 14  |-  4  e.  CC
6564mulid2i 9648 . . . . . . . . . . . . 13  |-  ( 1  x.  4 )  =  4
6665, 61oveq12i 6315 . . . . . . . . . . . 12  |-  ( ( 1  x.  4 )  +  ( 0  +  0 ) )  =  ( 4  +  0 )
6764addid1i 9822 . . . . . . . . . . . 12  |-  ( 4  +  0 )  =  4
6866, 67eqtri 2452 . . . . . . . . . . 11  |-  ( ( 1  x.  4 )  +  ( 0  +  0 ) )  =  4
69 ax-1cn 9599 . . . . . . . . . . . . . 14  |-  1  e.  CC
7069mul01i 9825 . . . . . . . . . . . . 13  |-  ( 1  x.  0 )  =  0
7170oveq1i 6313 . . . . . . . . . . . 12  |-  ( ( 1  x.  0 )  +  0 )  =  ( 0  +  0 )
7271, 63eqtri 2452 . . . . . . . . . . 11  |-  ( ( 1  x.  0 )  +  0 )  = ; 0
0
732, 3, 3, 3, 60, 63, 16, 3, 3, 68, 72decma2c 11093 . . . . . . . . . 10  |-  ( ( 1  x. ; 4 0 )  +  ( 0  +  0 ) )  = ; 4 0
7470oveq1i 6313 . . . . . . . . . . 11  |-  ( ( 1  x.  0 )  +  9 )  =  ( 0  +  9 )
7556addid2i 9823 . . . . . . . . . . . 12  |-  ( 0  +  9 )  =  9
7675, 58eqtri 2452 . . . . . . . . . . 11  |-  ( 0  +  9 )  = ; 0
9
7774, 76eqtri 2452 . . . . . . . . . 10  |-  ( ( 1  x.  0 )  +  9 )  = ; 0
9
784, 3, 3, 12, 55, 59, 16, 12, 3, 73, 77decma2c 11093 . . . . . . . . 9  |-  ( ( 1  x. ;; 4 0 0 )  +  ( 9  +  0 ) )  = ;; 4 0 9
7969mulid1i 9647 . . . . . . . . . . 11  |-  ( 1  x.  1 )  =  1
8079oveq1i 6313 . . . . . . . . . 10  |-  ( ( 1  x.  1 )  +  5 )  =  ( 1  +  5 )
81 5cn 10691 . . . . . . . . . . . 12  |-  5  e.  CC
82 5p1e6 10739 . . . . . . . . . . . 12  |-  ( 5  +  1 )  =  6
8381, 69, 82addcomli 9827 . . . . . . . . . . 11  |-  ( 1  +  5 )  =  6
8415dec0h 11069 . . . . . . . . . . 11  |-  6  = ; 0 6
8583, 84eqtri 2452 . . . . . . . . . 10  |-  ( 1  +  5 )  = ; 0
6
8680, 85eqtri 2452 . . . . . . . . 9  |-  ( ( 1  x.  1 )  +  5 )  = ; 0
6
875, 16, 12, 22, 1, 54, 16, 15, 3, 78, 86decma2c 11093 . . . . . . . 8  |-  ( ( 1  x.  N )  + ; 9 5 )  = ;;; 4 0 9 6
88 eqid 2423 . . . . . . . . 9  |- ; 6 4  = ; 6 4
89 eqid 2423 . . . . . . . . . 10  |- ; 2 5  = ; 2 5
90 2p2e4 10729 . . . . . . . . . . . 12  |-  ( 2  +  2 )  =  4
9190oveq2i 6314 . . . . . . . . . . 11  |-  ( ( 6  x.  6 )  +  ( 2  +  2 ) )  =  ( ( 6  x.  6 )  +  4 )
92 6t6e36 11134 . . . . . . . . . . . 12  |-  ( 6  x.  6 )  = ; 3
6
93 3p1e4 10737 . . . . . . . . . . . 12  |-  ( 3  +  1 )  =  4
94 6p4e10 10755 . . . . . . . . . . . 12  |-  ( 6  +  4 )  =  10
9541, 15, 2, 92, 93, 94decaddci2 11099 . . . . . . . . . . 11  |-  ( ( 6  x.  6 )  +  4 )  = ; 4
0
9691, 95eqtri 2452 . . . . . . . . . 10  |-  ( ( 6  x.  6 )  +  ( 2  +  2 ) )  = ; 4
0
97 6t4e24 11132 . . . . . . . . . . . 12  |-  ( 6  x.  4 )  = ; 2
4
9850, 64, 97mulcomli 9652 . . . . . . . . . . 11  |-  ( 4  x.  6 )  = ; 2
4
99 5p4e9 10751 . . . . . . . . . . . 12  |-  ( 5  +  4 )  =  9
10081, 64, 99addcomli 9827 . . . . . . . . . . 11  |-  ( 4  +  5 )  =  9
10120, 2, 22, 98, 100decaddi 11097 . . . . . . . . . 10  |-  ( ( 4  x.  6 )  +  5 )  = ; 2
9
10215, 2, 20, 22, 88, 89, 15, 12, 20, 96, 101decmac 11092 . . . . . . . . 9  |-  ( (; 6
4  x.  6 )  + ; 2 5 )  = ;; 4 0 9
103 4p1e5 10738 . . . . . . . . . . 11  |-  ( 4  +  1 )  =  5
10420, 2, 103, 97decsuc 11076 . . . . . . . . . 10  |-  ( ( 6  x.  4 )  +  1 )  = ; 2
5
105 4t4e16 11126 . . . . . . . . . 10  |-  ( 4  x.  4 )  = ; 1
6
1062, 15, 2, 88, 15, 16, 104, 105decmul1c 11100 . . . . . . . . 9  |-  (; 6 4  x.  4 )  = ;; 2 5 6
10747, 15, 2, 88, 15, 31, 102, 106decmul2c 11101 . . . . . . . 8  |-  (; 6 4  x. ; 6 4 )  = ;;; 4 0 9 6
10887, 107eqtr4i 2455 . . . . . . 7  |-  ( ( 1  x.  N )  + ; 9 5 )  =  (; 6 4  x. ; 6 4 )
1098, 9, 15, 46, 47, 45, 49, 53, 108mod2xi 15034 . . . . . 6  |-  ( ( 2 ^; 1 2 )  mod 
N )  =  (; 9
5  mod  N )
110 eqid 2423 . . . . . . 7  |- ; 1 2  = ; 1 2
11151mulid1i 9647 . . . . . . . . 9  |-  ( 2  x.  1 )  =  2
112111oveq1i 6313 . . . . . . . 8  |-  ( ( 2  x.  1 )  +  0 )  =  ( 2  +  0 )
11351addid1i 9822 . . . . . . . 8  |-  ( 2  +  0 )  =  2
114112, 113eqtri 2452 . . . . . . 7  |-  ( ( 2  x.  1 )  +  0 )  =  2
115 2t2e4 10761 . . . . . . . 8  |-  ( 2  x.  2 )  =  4
1162dec0h 11069 . . . . . . . 8  |-  4  = ; 0 4
117115, 116eqtri 2452 . . . . . . 7  |-  ( 2  x.  2 )  = ; 0
4
11820, 16, 20, 110, 2, 3, 114, 117decmul2c 11101 . . . . . 6  |-  ( 2  x. ; 1 2 )  = ; 2
4
119 eqid 2423 . . . . . . . 8  |- ;; 10 2 3  = ;; 10 2 3
12040nn0cni 10883 . . . . . . . . . 10  |- ; 10 2  e.  CC
121120addid1i 9822 . . . . . . . . 9  |-  (; 10 2  +  0 )  = ; 10 2
122 dec10p 11082 . . . . . . . . . 10  |-  ( 10  +  0 )  = ; 1
0
123 4t2e8 10765 . . . . . . . . . . . . 13  |-  ( 4  x.  2 )  =  8
12464, 51, 123mulcomli 9652 . . . . . . . . . . . 12  |-  ( 2  x.  4 )  =  8
12569addid1i 9822 . . . . . . . . . . . 12  |-  ( 1  +  0 )  =  1
126124, 125oveq12i 6315 . . . . . . . . . . 11  |-  ( ( 2  x.  4 )  +  ( 1  +  0 ) )  =  ( 8  +  1 )
127 8p1e9 10742 . . . . . . . . . . 11  |-  ( 8  +  1 )  =  9
128126, 127eqtri 2452 . . . . . . . . . 10  |-  ( ( 2  x.  4 )  +  ( 1  +  0 ) )  =  9
12951mul01i 9825 . . . . . . . . . . . 12  |-  ( 2  x.  0 )  =  0
130129oveq1i 6313 . . . . . . . . . . 11  |-  ( ( 2  x.  0 )  +  0 )  =  ( 0  +  0 )
131130, 63eqtri 2452 . . . . . . . . . 10  |-  ( ( 2  x.  0 )  +  0 )  = ; 0
0
1322, 3, 16, 3, 60, 122, 20, 3, 3, 128, 131decma2c 11093 . . . . . . . . 9  |-  ( ( 2  x. ; 4 0 )  +  ( 10  +  0 ) )  = ; 9 0
133129oveq1i 6313 . . . . . . . . . 10  |-  ( ( 2  x.  0 )  +  2 )  =  ( 0  +  2 )
13451addid2i 9823 . . . . . . . . . . 11  |-  ( 0  +  2 )  =  2
13520dec0h 11069 . . . . . . . . . . 11  |-  2  = ; 0 2
136134, 135eqtri 2452 . . . . . . . . . 10  |-  ( 0  +  2 )  = ; 0
2
137133, 136eqtri 2452 . . . . . . . . 9  |-  ( ( 2  x.  0 )  +  2 )  = ; 0
2
1384, 3, 10, 20, 55, 121, 20, 20, 3, 132, 137decma2c 11093 . . . . . . . 8  |-  ( ( 2  x. ;; 4 0 0 )  +  (; 10 2  +  0
) )  = ;; 9 0 2
139111oveq1i 6313 . . . . . . . . 9  |-  ( ( 2  x.  1 )  +  3 )  =  ( 2  +  3 )
140 3cn 10686 . . . . . . . . . . 11  |-  3  e.  CC
141 3p2e5 10744 . . . . . . . . . . 11  |-  ( 3  +  2 )  =  5
142140, 51, 141addcomli 9827 . . . . . . . . . 10  |-  ( 2  +  3 )  =  5
14322dec0h 11069 . . . . . . . . . 10  |-  5  = ; 0 5
144142, 143eqtri 2452 . . . . . . . . 9  |-  ( 2  +  3 )  = ; 0
5
145139, 144eqtri 2452 . . . . . . . 8  |-  ( ( 2  x.  1 )  +  3 )  = ; 0
5
1465, 16, 40, 41, 1, 119, 20, 22, 3, 138, 145decma2c 11093 . . . . . . 7  |-  ( ( 2  x.  N )  + ;; 10 2 3 )  = ;;; 9 0 2 5
1472, 28deccl 11067 . . . . . . . 8  |- ; 4 7  e.  NN0
148 eqid 2423 . . . . . . . . 9  |- ; 4 7  = ; 4 7
149100oveq2i 6314 . . . . . . . . . 10  |-  ( ( 9  x.  9 )  +  ( 4  +  5 ) )  =  ( ( 9  x.  9 )  +  9 )
150 9t9e81 11155 . . . . . . . . . . 11  |-  ( 9  x.  9 )  = ; 8
1
151 9p1e10 10743 . . . . . . . . . . . 12  |-  ( 9  +  1 )  =  10
15256, 69, 151addcomli 9827 . . . . . . . . . . 11  |-  ( 1  +  9 )  =  10
15324, 16, 12, 150, 127, 152decaddci2 11099 . . . . . . . . . 10  |-  ( ( 9  x.  9 )  +  9 )  = ; 9
0
154149, 153eqtri 2452 . . . . . . . . 9  |-  ( ( 9  x.  9 )  +  ( 4  +  5 ) )  = ; 9
0
155 9t5e45 11151 . . . . . . . . . . 11  |-  ( 9  x.  5 )  = ; 4
5
15656, 81, 155mulcomli 9652 . . . . . . . . . 10  |-  ( 5  x.  9 )  = ; 4
5
157 7cn 10695 . . . . . . . . . . 11  |-  7  e.  CC
158 7p5e12 11106 . . . . . . . . . . 11  |-  ( 7  +  5 )  = ; 1
2
159157, 81, 158addcomli 9827 . . . . . . . . . 10  |-  ( 5  +  7 )  = ; 1
2
1602, 22, 28, 156, 103, 20, 159decaddci 11098 . . . . . . . . 9  |-  ( ( 5  x.  9 )  +  7 )  = ; 5
2
16112, 22, 2, 28, 54, 148, 12, 20, 22, 154, 160decmac 11092 . . . . . . . 8  |-  ( (; 9
5  x.  9 )  + ; 4 7 )  = ;; 9 0 2
162 5p2e7 10749 . . . . . . . . . 10  |-  ( 5  +  2 )  =  7
1632, 22, 20, 155, 162decaddi 11097 . . . . . . . . 9  |-  ( ( 9  x.  5 )  +  2 )  = ; 4
7
164 5t5e25 11129 . . . . . . . . 9  |-  ( 5  x.  5 )  = ; 2
5
16522, 12, 22, 54, 22, 20, 163, 164decmul1c 11100 . . . . . . . 8  |-  (; 9 5  x.  5 )  = ;; 4 7 5
16645, 12, 22, 54, 22, 147, 161, 165decmul2c 11101 . . . . . . 7  |-  (; 9 5  x. ; 9 5 )  = ;;; 9 0 2 5
167146, 166eqtr4i 2455 . . . . . 6  |-  ( ( 2  x.  N )  + ;; 10 2 3 )  =  (; 9
5  x. ; 9 5 )
1688, 9, 43, 44, 45, 42, 109, 118, 167mod2xi 15034 . . . . 5  |-  ( ( 2 ^; 2 4 )  mod 
N )  =  (;; 10 2 3  mod 
N )
169 eqid 2423 . . . . . 6  |- ; 2 4  = ; 2 4
17020, 2, 103, 169decsuc 11076 . . . . 5  |-  (; 2 4  +  1 )  = ; 2 5
17137nn0cni 10883 . . . . . . 7  |- ;;; 2 0 4 6  e.  CC
172171addid2i 9823 . . . . . 6  |-  ( 0  + ;;; 2 0 4 6 )  = ;;; 2 0 4 6
1738nncni 10621 . . . . . . . 8  |-  N  e.  CC
174173mul02i 9824 . . . . . . 7  |-  ( 0  x.  N )  =  0
175174oveq1i 6313 . . . . . 6  |-  ( ( 0  x.  N )  + ;;; 2 0 4 6 )  =  ( 0  + ;;; 2 0 4 6 )
176 eqid 2423 . . . . . . . . . 10  |- ; 10 2  = ; 10 2
17720dec0u 11068 . . . . . . . . . . . 12  |-  ( 10  x.  2 )  = ; 2
0
178177oveq1i 6313 . . . . . . . . . . 11  |-  ( ( 10  x.  2 )  +  0 )  =  (; 2 0  +  0 )
17935nn0cni 10883 . . . . . . . . . . . 12  |- ; 2 0  e.  CC
180179addid1i 9822 . . . . . . . . . . 11  |-  (; 2 0  +  0 )  = ; 2 0
181178, 180eqtri 2452 . . . . . . . . . 10  |-  ( ( 10  x.  2 )  +  0 )  = ; 2
0
18220, 10, 20, 176, 2, 3, 181, 117decmul1c 11100 . . . . . . . . 9  |-  (; 10 2  x.  2 )  = ;; 2 0 4
183182oveq1i 6313 . . . . . . . 8  |-  ( (; 10 2  x.  2 )  +  0 )  =  (;; 2 0 4  +  0 )
18436nn0cni 10883 . . . . . . . . 9  |- ;; 2 0 4  e.  CC
185184addid1i 9822 . . . . . . . 8  |-  (;; 2 0 4  +  0 )  = ;; 2 0 4
186183, 185eqtri 2452 . . . . . . 7  |-  ( (; 10 2  x.  2 )  +  0 )  = ;; 2 0 4
187 3t2e6 10763 . . . . . . . 8  |-  ( 3  x.  2 )  =  6
188187, 84eqtri 2452 . . . . . . 7  |-  ( 3  x.  2 )  = ; 0
6
18920, 40, 41, 119, 15, 3, 186, 188decmul1c 11100 . . . . . 6  |-  (;; 10 2 3  x.  2 )  = ;;; 2 0 4 6
190172, 175, 1893eqtr4i 2462 . . . . 5  |-  ( ( 0  x.  N )  + ;;; 2 0 4 6 )  =  (;; 10 2 3  x.  2 )
1918, 9, 38, 39, 42, 37, 168, 170, 190modxp1i 15035 . . . 4  |-  ( ( 2 ^; 2 5 )  mod 
N )  =  (;;; 2 0 4 6  mod 
N )
192115oveq1i 6313 . . . . . 6  |-  ( ( 2  x.  2 )  +  1 )  =  ( 4  +  1 )
193192, 103eqtri 2452 . . . . 5  |-  ( ( 2  x.  2 )  +  1 )  =  5
194 5t2e10 10766 . . . . . . 7  |-  ( 5  x.  2 )  =  10
19581, 51, 194mulcomli 9652 . . . . . 6  |-  ( 2  x.  5 )  =  10
196 dec10 11083 . . . . . 6  |-  10  = ; 1 0
197195, 196eqtri 2452 . . . . 5  |-  ( 2  x.  5 )  = ; 1
0
19820, 20, 22, 89, 3, 16, 193, 197decmul2c 11101 . . . 4  |-  ( 2  x. ; 2 5 )  = ; 5
0
199 eqid 2423 . . . . . 6  |- ;; 10 7 0  = ;; 10 7 0
20020, 16deccl 11067 . . . . . . 7  |- ; 2 1  e.  NN0
201 eqid 2423 . . . . . . . 8  |- ; 10 7  = ; 10 7
202 eqid 2423 . . . . . . . 8  |- ; 10 4  = ; 10 4
203 0p1e1 10723 . . . . . . . . 9  |-  ( 0  +  1 )  =  1
204 10p10e20 11123 . . . . . . . . 9  |-  ( 10  +  10 )  = ; 2
0
20520, 3, 203, 204decsuc 11076 . . . . . . . 8  |-  ( ( 10  +  10 )  +  1 )  = ; 2
1
206 7p4e11 11105 . . . . . . . 8  |-  ( 7  +  4 )  = ; 1
1
20710, 28, 10, 2, 201, 202, 205, 16, 206decaddc 11095 . . . . . . 7  |-  (; 10 7  + ; 10 4 )  = ;; 2 1 1
208200nn0cni 10883 . . . . . . . . 9  |- ; 2 1  e.  CC
209208addid1i 9822 . . . . . . . 8  |-  (; 2 1  +  0 )  = ; 2 1
210 eqid 2423 . . . . . . . . 9  |- ;; 10 4 6  = ;; 10 4 6
211113, 135eqtri 2452 . . . . . . . . 9  |-  ( 2  +  0 )  = ; 0
2
21216dec0h 11069 . . . . . . . . . . . 12  |-  1  = ; 0 1
213203, 212eqtri 2452 . . . . . . . . . . 11  |-  ( 0  +  1 )  = ; 0
1
21464mul02i 9824 . . . . . . . . . . . . 13  |-  ( 0  x.  4 )  =  0
215214oveq1i 6313 . . . . . . . . . . . 12  |-  ( ( 0  x.  4 )  +  1 )  =  ( 0  +  1 )
216215, 213eqtri 2452 . . . . . . . . . . 11  |-  ( ( 0  x.  4 )  +  1 )  = ; 0
1
21716, 3, 3, 16, 196, 213, 2, 16, 3, 68, 216decmac 11092 . . . . . . . . . 10  |-  ( ( 10  x.  4 )  +  ( 0  +  1 ) )  = ; 4
1
218 6p2e8 10753 . . . . . . . . . . 11  |-  ( 6  +  2 )  =  8
21916, 15, 20, 105, 218decaddi 11097 . . . . . . . . . 10  |-  ( ( 4  x.  4 )  +  2 )  = ; 1
8
22010, 2, 3, 20, 202, 136, 2, 24, 16, 217, 219decmac 11092 . . . . . . . . 9  |-  ( (; 10 4  x.  4 )  +  ( 0  +  2 ) )  = ;; 4 1 8
221 4p2e6 10746 . . . . . . . . . 10  |-  ( 4  +  2 )  =  6
22220, 2, 20, 97, 221decaddi 11097 . . . . . . . . 9  |-  ( ( 6  x.  4 )  +  2 )  = ; 2
6
22332, 15, 3, 20, 210, 211, 2, 15, 20, 220, 222decmac 11092 . . . . . . . 8  |-  ( (;; 10 4 6  x.  4 )  +  ( 2  +  0 ) )  = ;;; 4 1 8 6
22433nn0cni 10883 . . . . . . . . . . 11  |- ;; 10 4 6  e.  CC
225224mul01i 9825 . . . . . . . . . 10  |-  (;; 10 4 6  x.  0 )  =  0
226225oveq1i 6313 . . . . . . . . 9  |-  ( (;; 10 4 6  x.  0 )  +  1 )  =  ( 0  +  1 )
227226, 213eqtri 2452 . . . . . . . 8  |-  ( (;; 10 4 6  x.  0 )  +  1 )  = ; 0 1
2282, 3, 20, 16, 60, 209, 33, 16, 3, 223, 227decma2c 11093 . . . . . . 7  |-  ( (;; 10 4 6  x. ; 4
0 )  +  (; 2
1  +  0 ) )  = ;;;; 4 1 8 6 1
2294, 3, 200, 16, 55, 207, 33, 16, 3, 228, 227decma2c 11093 . . . . . 6  |-  ( (;; 10 4 6  x. ;; 4 0 0 )  +  (; 10 7  + ; 10 4 ) )  = ;;;;; 4 1 8 6 1 1
230224mulid1i 9647 . . . . . . . 8  |-  (;; 10 4 6  x.  1 )  = ;; 10 4 6
231230oveq1i 6313 . . . . . . 7  |-  ( (;; 10 4 6  x.  1 )  +  0 )  =  (;; 10 4 6  +  0 )
232224addid1i 9822 . . . . . . 7  |-  (;; 10 4 6  +  0 )  = ;; 10 4 6
233231, 232eqtri 2452 . . . . . 6  |-  ( (;; 10 4 6  x.  1 )  +  0 )  = ;; 10 4 6
2345, 16, 29, 3, 1, 199, 33, 15, 32, 229, 233decma2c 11093 . . . . 5  |-  ( (;; 10 4 6  x.  N )  + ;; 10 7 0 )  = ;;;;;; 4 1 8 6 1 1 6
235 eqid 2423 . . . . . 6  |- ;;; 2 0 4 6  = ;;; 2 0 4 6
23643, 20deccl 11067 . . . . . . 7  |- ;; 1 2 2  e.  NN0
237236, 28deccl 11067 . . . . . 6  |- ;;; 1 2 2 7  e.  NN0
238 eqid 2423 . . . . . . 7  |- ;; 2 0 4  = ;; 2 0 4
239 eqid 2423 . . . . . . 7  |- ;;; 1 2 2 7  = ;;; 1 2 2 7
24024, 16deccl 11067 . . . . . . . 8  |- ; 8 1  e.  NN0
241240, 12deccl 11067 . . . . . . 7  |- ;; 8 1 9  e.  NN0
242 eqid 2423 . . . . . . . 8  |- ; 2 0  = ; 2 0
243 eqid 2423 . . . . . . . . 9  |- ;; 1 2 2  = ;; 1 2 2
244 eqid 2423 . . . . . . . . 9  |- ;; 8 1 9  = ;; 8 1 9
245 eqid 2423 . . . . . . . . . . 11  |- ; 8 1  = ; 8 1
246 8cn 10697 . . . . . . . . . . . 12  |-  8  e.  CC
247246, 69, 127addcomli 9827 . . . . . . . . . . 11  |-  ( 1  +  8 )  =  9
248 2p1e3 10735 . . . . . . . . . . 11  |-  ( 2  +  1 )  =  3
24916, 20, 24, 16, 110, 245, 247, 248decadd 11094 . . . . . . . . . 10  |-  (; 1 2  + ; 8 1 )  = ; 9
3
25012, 41, 93, 249decsuc 11076 . . . . . . . . 9  |-  ( (; 1
2  + ; 8 1 )  +  1 )  = ; 9 4
251 9p2e11 11115 . . . . . . . . . 10  |-  ( 9  +  2 )  = ; 1
1
25256, 51, 251addcomli 9827 . . . . . . . . 9  |-  ( 2  +  9 )  = ; 1
1
25343, 20, 240, 12, 243, 244, 250, 16, 252decaddc 11095 . . . . . . . 8  |-  (;; 1 2 2  + ;; 8 1 9 )  = ;; 9 4 1
25413nn0cni 10883 . . . . . . . . . 10  |- ; 9 4  e.  CC
255254addid1i 9822 . . . . . . . . 9  |-  (; 9 4  +  0 )  = ; 9 4
256151, 196eqtri 2452 . . . . . . . . . 10  |-  ( 9  +  1 )  = ; 1
0
257125, 212eqtri 2452 . . . . . . . . . . 11  |-  ( 1  +  0 )  = ; 0
1
258115, 61oveq12i 6315 . . . . . . . . . . . 12  |-  ( ( 2  x.  2 )  +  ( 0  +  0 ) )  =  ( 4  +  0 )
259258, 67eqtri 2452 . . . . . . . . . . 11  |-  ( ( 2  x.  2 )  +  ( 0  +  0 ) )  =  4
26051mul02i 9824 . . . . . . . . . . . . 13  |-  ( 0  x.  2 )  =  0
261260oveq1i 6313 . . . . . . . . . . . 12  |-  ( ( 0  x.  2 )  +  1 )  =  ( 0  +  1 )
262261, 213eqtri 2452 . . . . . . . . . . 11  |-  ( ( 0  x.  2 )  +  1 )  = ; 0
1
26320, 3, 3, 16, 242, 257, 20, 16, 3, 259, 262decmac 11092 . . . . . . . . . 10  |-  ( (; 2
0  x.  2 )  +  ( 1  +  0 ) )  = ; 4
1
264123oveq1i 6313 . . . . . . . . . . 11  |-  ( ( 4  x.  2 )  +  0 )  =  ( 8  +  0 )
265246addid1i 9822 . . . . . . . . . . . 12  |-  ( 8  +  0 )  =  8
26624dec0h 11069 . . . . . . . . . . . 12  |-  8  = ; 0 8
267265, 266eqtri 2452 . . . . . . . . . . 11  |-  ( 8  +  0 )  = ; 0
8
268264, 267eqtri 2452 . . . . . . . . . 10  |-  ( ( 4  x.  2 )  +  0 )  = ; 0
8
26935, 2, 16, 3, 238, 256, 20, 24, 3, 263, 268decmac 11092 . . . . . . . . 9  |-  ( (;; 2 0 4  x.  2 )  +  ( 9  +  1 ) )  = ;; 4 1 8
27064, 51, 221addcomli 9827 . . . . . . . . . 10  |-  ( 2  +  4 )  =  6
27116, 20, 2, 52, 270decaddi 11097 . . . . . . . . 9  |-  ( ( 6  x.  2 )  +  4 )  = ; 1
6
27236, 15, 12, 2, 235, 255, 20, 15, 16, 269, 271decmac 11092 . . . . . . . 8  |-  ( (;;; 2 0 4 6  x.  2 )  +  (; 9
4  +  0 ) )  = ;;; 4 1 8 6
273171mul01i 9825 . . . . . . . . . 10  |-  (;;; 2 0 4 6  x.  0 )  =  0
274273oveq1i 6313 . . . . . . . . 9  |-  ( (;;; 2 0 4 6  x.  0 )  +  1 )  =  ( 0  +  1 )
275274, 213eqtri 2452 . . . . . . . 8  |-  ( (;;; 2 0 4 6  x.  0 )  +  1 )  = ; 0 1
27620, 3, 13, 16, 242, 253, 37, 16, 3, 272, 275decma2c 11093 . . . . . . 7  |-  ( (;;; 2 0 4 6  x. ; 2
0 )  +  (;; 1 2 2  + ;; 8 1 9 ) )  = ;;;; 4 1 8 6 1
27728dec0h 11069 . . . . . . . 8  |-  7  = ; 0 7
278140addid2i 9823 . . . . . . . . . 10  |-  ( 0  +  3 )  =  3
27941dec0h 11069 . . . . . . . . . 10  |-  3  = ; 0 3
280278, 279eqtri 2452 . . . . . . . . 9  |-  ( 0  +  3 )  = ; 0
3
281124, 61oveq12i 6315 . . . . . . . . . . 11  |-  ( ( 2  x.  4 )  +  ( 0  +  0 ) )  =  ( 8  +  0 )
282281, 265eqtri 2452 . . . . . . . . . 10  |-  ( ( 2  x.  4 )  +  ( 0  +  0 ) )  =  8
28320, 3, 3, 16, 242, 213, 2, 16, 3, 282, 216decmac 11092 . . . . . . . . 9  |-  ( (; 2
0  x.  4 )  +  ( 0  +  1 ) )  = ; 8
1
284 6p3e9 10754 . . . . . . . . . 10  |-  ( 6  +  3 )  =  9
28516, 15, 41, 105, 284decaddi 11097 . . . . . . . . 9  |-  ( ( 4  x.  4 )  +  3 )  = ; 1
9
28635, 2, 3, 41, 238, 280, 2, 12, 16, 283, 285decmac 11092 . . . . . . . 8  |-  ( (;; 2 0 4  x.  4 )  +  ( 0  +  3 ) )  = ;; 8 1 9
287157, 64, 206addcomli 9827 . . . . . . . . 9  |-  ( 4  +  7 )  = ; 1
1
28820, 2, 28, 97, 248, 16, 287decaddci 11098 . . . . . . . 8  |-  ( ( 6  x.  4 )  +  7 )  = ; 3
1
28936, 15, 3, 28, 235, 277, 2, 16, 41, 286, 288decmac 11092 . . . . . . 7  |-  ( (;;; 2 0 4 6  x.  4 )  +  7 )  = ;;; 8 1 9 1
29035, 2, 236, 28, 238, 239, 37, 16, 241, 276, 289decma2c 11093 . . . . . 6  |-  ( (;;; 2 0 4 6  x. ;; 2 0 4 )  + ;;; 1 2 2 7 )  = ;;;;; 4 1 8 6 1 1
29153oveq1i 6313 . . . . . . . . . 10  |-  ( ( 2  x.  6 )  +  0 )  =  (; 1 2  +  0 )
29243nn0cni 10883 . . . . . . . . . . 11  |- ; 1 2  e.  CC
293292addid1i 9822 . . . . . . . . . 10  |-  (; 1 2  +  0 )  = ; 1 2
294291, 293eqtri 2452 . . . . . . . . 9  |-  ( ( 2  x.  6 )  +  0 )  = ; 1
2
29550mul02i 9824 . . . . . . . . . . 11  |-  ( 0  x.  6 )  =  0
296295oveq1i 6313 . . . . . . . . . 10  |-  ( ( 0  x.  6 )  +  2 )  =  ( 0  +  2 )
297296, 134eqtri 2452 . . . . . . . . 9  |-  ( ( 0  x.  6 )  +  2 )  =  2
29820, 3, 3, 20, 242, 136, 15, 294, 297decma 11091 . . . . . . . 8  |-  ( (; 2
0  x.  6 )  +  ( 0  +  2 ) )  = ;; 1 2 2
299 4p3e7 10747 . . . . . . . . 9  |-  ( 4  +  3 )  =  7
30020, 2, 41, 98, 299decaddi 11097 . . . . . . . 8  |-  ( ( 4  x.  6 )  +  3 )  = ; 2
7
30135, 2, 3, 41, 238, 279, 15, 28, 20, 298, 300decmac 11092 . . . . . . 7  |-  ( (;; 2 0 4  x.  6 )  +  3 )  = ;;; 1 2 2 7
30215, 36, 15, 235, 15, 41, 301, 92decmul1c 11100 . . . . . 6  |-  (;;; 2 0 4 6  x.  6 )  = ;;;; 1 2 2 7 6
30337, 36, 15, 235, 15, 237, 290, 302decmul2c 11101 . . . . 5  |-  (;;; 2 0 4 6  x. ;;; 2 0 4 6 )  = ;;;;;; 4 1 8 6 1 1 6
304234, 303eqtr4i 2455 . . . 4  |-  ( (;; 10 4 6  x.  N )  + ;; 10 7 0 )  =  (;;; 2 0 4 6  x. ;;; 2 0 4 6 )
3058, 9, 31, 34, 37, 30, 191, 198, 304mod2xi 15034 . . 3  |-  ( ( 2 ^; 5 0 )  mod 
N )  =  (;; 10 7 0  mod 
N )
306 eqid 2423 . . . 4  |- ; 5 0  = ; 5 0
307195oveq1i 6313 . . . . 5  |-  ( ( 2  x.  5 )  +  0 )  =  ( 10  +  0 )
308 10nn 10777 . . . . . . 7  |-  10  e.  NN
309308nncni 10621 . . . . . 6  |-  10  e.  CC
310309addid1i 9822 . . . . 5  |-  ( 10  +  0 )  =  10
311307, 310eqtri 2452 . . . 4  |-  ( ( 2  x.  5 )  +  0 )  =  10
312129, 62eqtri 2452 . . . 4  |-  ( 2  x.  0 )  = ; 0
0
31320, 22, 3, 306, 3, 3, 311, 312decmul2c 11101 . . 3  |-  ( 2  x. ; 5 0 )  = ; 10 0
314 eqid 2423 . . . . 5  |- ;; 6 1 4  = ;; 6 1 4
31520, 12deccl 11067 . . . . 5  |- ; 2 9  e.  NN0
316 eqid 2423 . . . . . . 7  |- ; 6 1  = ; 6 1
317 eqid 2423 . . . . . . 7  |- ; 2 9  = ; 2 9
318218oveq1i 6313 . . . . . . . 8  |-  ( ( 6  +  2 )  +  1 )  =  ( 8  +  1 )
319318, 127eqtri 2452 . . . . . . 7  |-  ( ( 6  +  2 )  +  1 )  =  9
32015, 16, 20, 12, 316, 317, 319, 152decaddc2 11096 . . . . . 6  |-  (; 6 1  + ; 2 9 )  = ; 9
0
321 eqid 2423 . . . . . . . 8  |- ;; 2 8 6  = ;; 2 8 6
322 eqid 2423 . . . . . . . . 9  |- ; 2 8  = ; 2 8
323124, 278oveq12i 6315 . . . . . . . . . 10  |-  ( ( 2  x.  4 )  +  ( 0  +  3 ) )  =  ( 8  +  3 )
324 8p3e11 11109 . . . . . . . . . 10  |-  ( 8  +  3 )  = ; 1
1
325323, 324eqtri 2452 . . . . . . . . 9  |-  ( ( 2  x.  4 )  +  ( 0  +  3 ) )  = ; 1
1
326 8t4e32 11143 . . . . . . . . . 10  |-  ( 8  x.  4 )  = ; 3
2
32741, 20, 20, 326, 90decaddi 11097 . . . . . . . . 9  |-  ( ( 8  x.  4 )  +  2 )  = ; 3
4
32820, 24, 3, 20, 322, 136, 2, 2, 41, 325, 327decmac 11092 . . . . . . . 8  |-  ( (; 2
8  x.  4 )  +  ( 0  +  2 ) )  = ;; 1 1 4
32997oveq1i 6313 . . . . . . . . 9  |-  ( ( 6  x.  4 )  +  0 )  =  (; 2 4  +  0 )
33038nn0cni 10883 . . . . . . . . . 10  |- ; 2 4  e.  CC
331330addid1i 9822 . . . . . . . . 9  |-  (; 2 4  +  0 )  = ; 2 4
332329, 331eqtri 2452 . . . . . . . 8  |-  ( ( 6  x.  4 )  +  0 )  = ; 2
4
33325, 15, 3, 3, 321, 63, 2, 2, 20, 328, 332decmac 11092 . . . . . . 7  |-  ( (;; 2 8 6  x.  4 )  +  ( 0  +  0 ) )  = ;;; 1 1 4 4
33426nn0cni 10883 . . . . . . . . . 10  |- ;; 2 8 6  e.  CC
335334mul01i 9825 . . . . . . . . 9  |-  (;; 2 8 6  x.  0 )  =  0
336335oveq1i 6313 . . . . . . . 8  |-  ( (;; 2 8 6  x.  0 )  +  9 )  =  ( 0  +  9 )
337336, 76eqtri 2452 . . . . . . 7  |-  ( (;; 2 8 6  x.  0 )  +  9 )  = ; 0 9
3382, 3, 3, 12, 60, 59, 26, 12, 3, 333, 337decma2c 11093 . . . . . 6  |-  ( (;; 2 8 6  x. ; 4
0 )  +  ( 9  +  0 ) )  = ;;;; 1 1 4 4 9
339335oveq1i 6313 . . . . . . 7  |-  ( (;; 2 8 6  x.  0 )  +  0 )  =  ( 0  +  0 )
340339, 63eqtri 2452 . . . . . 6  |-  ( (;; 2 8 6  x.  0 )  +  0 )  = ; 0 0
3414, 3, 12, 3, 55, 320, 26, 3, 3, 338, 340decma2c 11093 . . . . 5  |-  ( (;; 2 8 6  x. ;; 4 0 0 )  +  (; 6 1  + ; 2 9 ) )  = ;;;;; 1 1 4 4 9 0
342111, 61oveq12i 6315 . . . . . . . 8  |-  ( ( 2  x.  1 )  +  ( 0  +  0 ) )  =  ( 2  +  0 )
343342, 113eqtri 2452 . . . . . . 7  |-  ( ( 2  x.  1 )  +  ( 0  +  0 ) )  =  2
344246mulid1i 9647 . . . . . . . . 9  |-  ( 8  x.  1 )  =  8
345344oveq1i 6313 . . . . . . . 8  |-  ( ( 8  x.  1 )  +  1 )  =  ( 8  +  1 )
346127, 58eqtri 2452 . . . . . . . 8  |-  ( 8  +  1 )  = ; 0
9
347345, 346eqtri 2452 . . . . . . 7  |-  ( ( 8  x.  1 )  +  1 )  = ; 0
9
34820, 24, 3, 16, 322, 213, 16, 12, 3, 343, 347decmac 11092 . . . . . 6  |-  ( (; 2
8  x.  1 )  +  ( 0  +  1 ) )  = ; 2
9
34950mulid1i 9647 . . . . . . . 8  |-  ( 6  x.  1 )  =  6
350349oveq1i 6313 . . . . . . 7  |-  ( ( 6  x.  1 )  +  4 )  =  ( 6  +  4 )
35194, 196eqtri 2452 . . . . . . 7  |-  ( 6  +  4 )  = ; 1
0
352350, 351eqtri 2452 . . . . . 6  |-  ( ( 6  x.  1 )  +  4 )  = ; 1
0
35325, 15, 3, 2, 321, 116, 16, 3, 16, 348, 352decmac 11092 . . . . 5  |-  ( (;; 2 8 6  x.  1 )  +  4 )  = ;; 2 9 0
3545, 16, 17, 2, 1, 314, 26, 3, 315, 341, 353decma2c 11093 . . . 4  |-  ( (;; 2 8 6  x.  N )  + ;; 6 1 4 )  = ;;;;;; 1 1 4 4 9 0 0
35516, 16deccl 11067 . . . . . . . . 9  |- ; 1 1  e.  NN0
356355, 2deccl 11067 . . . . . . . 8  |- ;; 1 1 4  e.  NN0
357356, 2deccl 11067 . . . . . . 7  |- ;;; 1 1 4 4  e.  NN0
358357, 12deccl 11067 . . . . . 6  |- ;;;; 1 1 4 4 9  e.  NN0
35928, 2deccl 11067 . . . . . . . 8  |- ; 7 4  e.  NN0
360359, 12deccl 11067 . . . . . . 7  |- ;; 7 4 9  e.  NN0
361 eqid 2423 . . . . . . . 8  |- ;; 7 4 9  = ;; 7 4 9
362359nn0cni 10883 . . . . . . . . . 10  |- ; 7 4  e.  CC
363362addid1i 9822 . . . . . . . . 9  |-  (; 7 4  +  0 )  = ; 7 4
364157addid1i 9822 . . . . . . . . . . 11  |-  ( 7  +  0 )  =  7
365364, 277eqtri 2452 . . . . . . . . . 10  |-  ( 7  +  0 )  = ; 0
7
36679, 61oveq12i 6315 . . . . . . . . . . . 12  |-  ( ( 1  x.  1 )  +  ( 0  +  0 ) )  =  ( 1  +  0 )
367366, 125eqtri 2452 . . . . . . . . . . 11  |-  ( ( 1  x.  1 )  +  ( 0  +  0 ) )  =  1
36869mul02i 9824 . . . . . . . . . . . . 13  |-  ( 0  x.  1 )  =  0
369368oveq1i 6313 . . . . . . . . . . . 12  |-  ( ( 0  x.  1 )  +  1 )  =  ( 0  +  1 )
370369, 213eqtri 2452 . . . . . . . . . . 11  |-  ( ( 0  x.  1 )  +  1 )  = ; 0
1
37116, 3, 3, 16, 196, 213, 16, 16, 3, 367, 370decmac 11092 . . . . . . . . . 10  |-  ( ( 10  x.  1 )  +  ( 0  +  1 ) )  = ; 1
1
372157mulid1i 9647 . . . . . . . . . . . 12  |-  ( 7  x.  1 )  =  7
373372oveq1i 6313 . . . . . . . . . . 11  |-  ( ( 7  x.  1 )  +  7 )  =  ( 7  +  7 )
374 7p7e14 11108 . . . . . . . . . . 11  |-  ( 7  +  7 )  = ; 1
4
375373, 374eqtri 2452 . . . . . . . . . 10  |-  ( ( 7  x.  1 )  +  7 )  = ; 1
4
37610, 28, 3, 28, 201, 365, 16, 2, 16, 371, 375decmac 11092 . . . . . . . . 9  |-  ( (; 10 7  x.  1 )  +  ( 7  +  0 ) )  = ;; 1 1 4
377368oveq1i 6313 . . . . . . . . . 10  |-  ( ( 0  x.  1 )  +  4 )  =  ( 0  +  4 )
37864addid2i 9823 . . . . . . . . . . 11  |-  ( 0  +  4 )  =  4
379378, 116eqtri 2452 . . . . . . . . . 10  |-  ( 0  +  4 )  = ; 0
4
380377, 379eqtri 2452 . . . . . . . . 9  |-  ( ( 0  x.  1 )  +  4 )  = ; 0
4
38129, 3, 28, 2, 199, 363, 16, 2, 3, 376, 380decmac 11092 . . . . . . . 8  |-  ( (;; 10 7 0  x.  1 )  +  (; 7
4  +  0 ) )  = ;;; 1 1 4 4
38230nn0cni 10883 . . . . . . . . . . 11  |- ;; 10 7 0  e.  CC
383382mul01i 9825 . . . . . . . . . 10  |-  (;; 10 7 0  x.  0 )  =  0
384383oveq1i 6313 . . . . . . . . 9  |-  ( (;; 10 7 0  x.  0 )  +  9 )  =  ( 0  +  9 )
385384, 76eqtri 2452 . . . . . . . 8  |-  ( (;; 10 7 0  x.  0 )  +  9 )  = ; 0 9
38616, 3, 359, 12, 196, 361, 30, 12, 3, 381, 385decma2c 11093 . . . . . . 7  |-  ( (;; 10 7 0  x.  10 )  + ;; 7 4 9 )  = ;;;; 1 1 4 4 9
387157mulid2i 9648 . . . . . . . . . . . . . 14  |-  ( 1  x.  7 )  =  7
388387, 61oveq12i 6315 . . . . . . . . . . . . 13  |-  ( ( 1  x.  7 )  +  ( 0  +  0 ) )  =  ( 7  +  0 )
389388, 364eqtri 2452 . . . . . . . . . . . 12  |-  ( ( 1  x.  7 )  +  ( 0  +  0 ) )  =  7
390157mul02i 9824 . . . . . . . . . . . . . 14  |-  ( 0  x.  7 )  =  0
391390oveq1i 6313 . . . . . . . . . . . . 13  |-  ( ( 0  x.  7 )  +  4 )  =  ( 0  +  4 )
392391, 379eqtri 2452 . . . . . . . . . . . 12  |-  ( ( 0  x.  7 )  +  4 )  = ; 0
4
39316, 3, 3, 2, 196, 116, 28, 2, 3, 389, 392decmac 11092 . . . . . . . . . . 11  |-  ( ( 10  x.  7 )  +  4 )  = ; 7
4
394 7t7e49 11140 . . . . . . . . . . 11  |-  ( 7  x.  7 )  = ; 4
9
39528, 10, 28, 201, 12, 2, 393, 394decmul1c 11100 . . . . . . . . . 10  |-  (; 10 7  x.  7 )  = ;; 7 4 9
396395oveq1i 6313 . . . . . . . . 9  |-  ( (; 10 7  x.  7 )  +  0 )  =  (;; 7 4 9  +  0 )
397360nn0cni 10883 . . . . . . . . . 10  |- ;; 7 4 9  e.  CC
398397addid1i 9822 . . . . . . . . 9  |-  (;; 7 4 9  +  0 )  = ;; 7 4 9
399396, 398eqtri 2452 . . . . . . . 8  |-  ( (; 10 7  x.  7 )  +  0 )  = ;; 7 4 9
400390, 62eqtri 2452 . . . . . . . 8  |-  ( 0  x.  7 )  = ; 0
0
40128, 29, 3, 199, 3, 3, 399, 400decmul1c 11100 . . . . . . 7  |-  (;; 10 7 0  x.  7 )  = ;;; 7 4 9 0
40230, 10, 28, 201, 3, 360, 386, 401decmul2c 11101 . . . . . 6  |-  (;; 10 7 0  x. ; 10 7 )  = ;;;;; 1 1 4 4 9 0
403358, 3, 3, 402, 61decaddi 11097 . . . . 5  |-  ( (;; 10 7 0  x. ; 10 7 )  +  0 )  = ;;;;; 1 1 4 4 9 0
404383, 62eqtri 2452 . . . . 5  |-  (;; 10 7 0  x.  0 )  = ; 0 0
40530, 29, 3, 199, 3, 3, 403, 404decmul2c 11101 . . . 4  |-  (;; 10 7 0  x. ;; 10 7 0 )  = ;;;;;; 1 1 4 4 9 0 0
406354, 405eqtr4i 2455 . . 3  |-  ( (;; 2 8 6  x.  N )  + ;; 6 1 4 )  =  (;; 10 7 0  x. ;; 10 7 0 )
4078, 9, 23, 27, 30, 18, 305, 313, 406mod2xi 15034 . 2  |-  ( ( 2 ^; 10 0 )  mod 
N )  =  (;; 6 1 4  mod 
N )
408 eqid 2423 . . 3  |- ; 10 0  = ; 10 0
40920, 16, 3, 196, 3, 3, 114, 312decmul2c 11101 . . . . 5  |-  ( 2  x.  10 )  = ; 2
0
410409oveq1i 6313 . . . 4  |-  ( ( 2  x.  10 )  +  0 )  =  (; 2 0  +  0 )
411410, 180eqtri 2452 . . 3  |-  ( ( 2  x.  10 )  +  0 )  = ; 2
0
41220, 10, 3, 408, 3, 3, 411, 312decmul2c 11101 . 2  |-  ( 2  x. ; 10 0 )  = ;; 2 0 0
413 eqid 2423 . . . 4  |- ;; 9 0 2  = ;; 9 0 2
414 eqid 2423 . . . . . 6  |- ; 9 0  = ; 9 0
41512, 3, 12, 414, 75decaddi 11097 . . . . 5  |-  (; 9 0  +  9 )  = ; 9 9
416 eqid 2423 . . . . . . 7  |- ; 9 4  = ; 9 4
417203oveq2i 6314 . . . . . . . 8  |-  ( ( 9  x.  4 )  +  ( 0  +  1 ) )  =  ( ( 9  x.  4 )  +  1 )
418 6p1e7 10740 . . . . . . . . 9  |-  ( 6  +  1 )  =  7
419 9t4e36 11150 . . . . . . . . 9  |-  ( 9  x.  4 )  = ; 3
6
42041, 15, 418, 419decsuc 11076 . . . . . . . 8  |-  ( ( 9  x.  4 )  +  1 )  = ; 3
7
421417, 420eqtri 2452 . . . . . . 7  |-  ( ( 9  x.  4 )  +  ( 0  +  1 ) )  = ; 3
7
422105oveq1i 6313 . . . . . . . 8  |-  ( ( 4  x.  4 )  +  0 )  =  (; 1 6  +  0 )
42316, 15deccl 11067 . . . . . . . . . 10  |- ; 1 6  e.  NN0
424423nn0cni 10883 . . . . . . . . 9  |- ; 1 6  e.  CC
425424addid1i 9822 . . . . . . . 8  |-  (; 1 6  +  0 )  = ; 1 6
426422, 425eqtri 2452 . . . . . . 7  |-  ( ( 4  x.  4 )  +  0 )  = ; 1
6
42712, 2, 3, 3, 416, 63, 2, 15, 16, 421, 426decmac 11092 . . . . . 6  |-  ( (; 9
4  x.  4 )  +  ( 0  +  0 ) )  = ;; 3 7 6
428254mul01i 9825 . . . . . . . 8  |-  (; 9 4  x.  0 )  =  0
429428oveq1i 6313 . . . . . . 7  |-  ( (; 9
4  x.  0 )  +  9 )  =  ( 0  +  9 )
430429, 76eqtri 2452 . . . . . 6  |-  ( (; 9
4  x.  0 )  +  9 )  = ; 0
9
4312, 3, 3, 12, 60, 59, 13, 12, 3, 427, 430decma2c 11093 . . . . 5  |-  ( (; 9
4  x. ; 4 0 )  +  ( 9  +  0 ) )  = ;;; 3 7 6 9
4324, 3, 12, 12, 55, 415, 13, 12, 3, 431, 430decma2c 11093 . . . 4  |-  ( (; 9
4  x. ;; 4 0 0 )  +  (; 9 0  +  9 ) )  = ;;;; 3 7 6 9 9
43356mulid1i 9647 . . . . . . 7  |-  ( 9  x.  1 )  =  9
434433, 61oveq12i 6315 . . . . . 6  |-  ( ( 9  x.  1 )  +  ( 0  +  0 ) )  =  ( 9  +  0 )
435434, 57eqtri 2452 . . . . 5  |-  ( ( 9  x.  1 )  +  ( 0  +  0 ) )  =  9
43664mulid1i 9647 . . . . . . 7  |-  ( 4  x.  1 )  =  4
437436oveq1i 6313 . . . . . 6  |-  ( ( 4  x.  1 )  +  2 )  =  ( 4  +  2 )
438221, 84eqtri 2452 . . . . . 6  |-  ( 4  +  2 )  = ; 0
6
439437, 438eqtri 2452 . . . . 5  |-  ( ( 4  x.  1 )  +  2 )  = ; 0
6
44012, 2, 3, 20, 416, 135, 16, 15, 3, 435, 439decmac 11092 . . . 4  |-  ( (; 9
4  x.  1 )  +  2 )  = ; 9
6
4415, 16, 19, 20, 1, 413, 13, 15, 12, 432, 440decma2c 11093 . . 3  |-  ( (; 9
4  x.  N )  + ;; 9 0 2 )  = ;;;;; 3 7 6 9 9 6
44238, 22deccl 11067 . . . 4  |- ;; 2 4 5  e.  NN0
443 eqid 2423 . . . . 5  |- ;; 2 4 5  = ;; 2 4 5
44450, 51, 218addcomli 9827 . . . . . . 7  |-  ( 2  +  6 )  =  8
44520, 2, 15, 16, 169, 316, 444, 103decadd 11094 . . . . . 6  |-  (; 2 4  + ; 6 1 )  = ; 8
5
446 8p2e10 10758 . . . . . . . 8  |-  ( 8  +  2 )  =  10
447446, 196eqtri 2452 . . . . . . 7  |-  ( 8  +  2 )  = ; 1
0
44841, 15, 418, 92decsuc 11076 . . . . . . 7  |-  ( ( 6  x.  6 )  +  1 )  = ; 3
7
44950mulid2i 9648 . . . . . . . . 9  |-  ( 1  x.  6 )  =  6
450449oveq1i 6313 . . . . . . . 8  |-  ( ( 1  x.  6 )  +  0 )  =  ( 6  +  0 )
45150addid1i 9822 . . . . . . . 8  |-  ( 6  +  0 )  =  6
452450, 451eqtri 2452 . . . . . . 7  |-  ( ( 1  x.  6 )  +  0 )  =  6
45315, 16, 16, 3, 316, 447, 15, 448, 452decma 11091 . . . . . 6  |-  ( (; 6
1  x.  6 )  +  ( 8  +  2 ) )  = ;; 3 7 6
45417, 2, 24, 22, 314, 445, 15, 12, 20, 453, 101decmac 11092 . . . . 5  |-  ( (;; 6 1 4  x.  6 )  +  (; 2
4  + ; 6 1 ) )  = ;;; 3 7 6 9
455349, 61oveq12i 6315 . . . . . . . 8  |-  ( ( 6  x.  1 )  +  ( 0  +  0 ) )  =  ( 6  +  0 )
456455, 451eqtri 2452 . . . . . . 7  |-  ( ( 6  x.  1 )  +  ( 0  +  0 ) )  =  6
45779oveq1i 6313 . . . . . . . 8  |-  ( ( 1  x.  1 )  +  0 )  =  ( 1  +  0 )
458457, 257eqtri 2452 . . . . . . 7  |-  ( ( 1  x.  1 )  +  0 )  = ; 0
1
45915, 16, 3, 3, 316, 63, 16, 16, 3, 456, 458decmac 11092 . . . . . 6  |-  ( (; 6
1  x.  1 )  +  ( 0  +  0 ) )  = ; 6
1
460436oveq1i 6313 . . . . . . 7  |-  ( ( 4  x.  1 )  +  5 )  =  ( 4  +  5 )
461100, 58eqtri 2452 . . . . . . 7  |-  ( 4  +  5 )  = ; 0
9
462460, 461eqtri 2452 . . . . . 6  |-  ( ( 4  x.  1 )  +  5 )  = ; 0
9
46317, 2, 3, 22, 314, 143, 16, 12, 3, 459, 462decmac 11092 . . . . 5  |-  ( (;; 6 1 4  x.  1 )  +  5 )  = ;; 6 1 9
46415, 16, 38, 22, 316, 443, 18, 12, 17, 454, 463decma2c 11093 . . . 4  |-  ( (;; 6 1 4  x. ; 6
1 )  + ;; 2 4 5 )  = ;;;; 3 7 6 9 9
46565oveq1i 6313 . . . . . . 7  |-  ( ( 1  x.  4 )  +  1 )  =  ( 4  +  1 )
466465, 103eqtri 2452 . . . . . 6  |-  ( ( 1  x.  4 )  +  1 )  =  5
46715, 16, 3, 16, 316, 212, 2, 332, 466decma 11091 . . . . 5  |-  ( (; 6
1  x.  4 )  +  1 )  = ;; 2 4 5
4682, 17, 2, 314, 15, 16, 467, 105decmul1c 11100 . . . 4  |-  (;; 6 1 4  x.  4 )  = ;;; 2 4 5 6
46918, 17, 2, 314, 15, 442, 464, 468decmul2c 11101 . . 3  |-  (;; 6 1 4  x. ;; 6 1 4 )  = ;;;;; 3 7 6 9 9 6
470441, 469eqtr4i 2455 . 2  |-  ( (; 9
4  x.  N )  + ;; 9 0 2 )  =  (;; 6 1 4  x. ;; 6 1 4 )
4718, 9, 11, 14, 18, 21, 407, 412, 470mod2xi 15034 1  |-  ( ( 2 ^;; 2 0 0 )  mod 
N )  =  (;; 9 0 2  mod 
N )
Colors of variables: wff setvar class
Syntax hints:    = wceq 1438  (class class class)co 6303   0cc0 9541   1c1 9542    + caddc 9544    x. cmul 9546   NNcn 10611   2c2 10661   3c3 10662   4c4 10663   5c5 10664   6c6 10665   7c7 10666   8c8 10667   9c9 10668   10c10 10669  ;cdc 11053    mod cmo 12097   ^cexp 12273
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-8 1871  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-sep 4544  ax-nul 4553  ax-pow 4600  ax-pr 4658  ax-un 6595  ax-cnex 9597  ax-resscn 9598  ax-1cn 9599  ax-icn 9600  ax-addcl 9601  ax-addrcl 9602  ax-mulcl 9603  ax-mulrcl 9604  ax-mulcom 9605  ax-addass 9606  ax-mulass 9607  ax-distr 9608  ax-i2m1 9609  ax-1ne0 9610  ax-1rid 9611  ax-rnegex 9612  ax-rrecex 9613  ax-cnre 9614  ax-pre-lttri 9615  ax-pre-lttrn 9616  ax-pre-ltadd 9617  ax-pre-mulgt0 9618  ax-pre-sup 9619
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 984  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-eu 2270  df-mo 2271  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-nel 2622  df-ral 2781  df-rex 2782  df-reu 2783  df-rmo 2784  df-rab 2785  df-v 3084  df-sbc 3301  df-csb 3397  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-pss 3453  df-nul 3763  df-if 3911  df-pw 3982  df-sn 3998  df-pr 4000  df-tp 4002  df-op 4004  df-uni 4218  df-iun 4299  df-br 4422  df-opab 4481  df-mpt 4482  df-tr 4517  df-eprel 4762  df-id 4766  df-po 4772  df-so 4773  df-fr 4810  df-we 4812  df-xp 4857  df-rel 4858  df-cnv 4859  df-co 4860  df-dm 4861  df-rn 4862  df-res 4863  df-ima 4864  df-pred 5397  df-ord 5443  df-on 5444  df-lim 5445  df-suc 5446  df-iota 5563  df-fun 5601  df-fn 5602  df-f 5603  df-f1 5604  df-fo 5605  df-f1o 5606  df-fv 5607  df-riota 6265  df-ov 6306  df-oprab 6307  df-mpt2 6308  df-om 6705  df-2nd 6806  df-wrecs 7034  df-recs 7096  df-rdg 7134  df-er 7369  df-en 7576  df-dom 7577  df-sdom 7578  df-sup 7960  df-inf 7961  df-pnf 9679  df-mnf 9680  df-xr 9681  df-ltxr 9682  df-le 9683  df-sub 9864  df-neg 9865  df-div 10272  df-nn 10612  df-2 10670  df-3 10671  df-4 10672  df-5 10673  df-6 10674  df-7 10675  df-8 10676  df-9 10677  df-10 10678  df-n0 10872  df-z 10940  df-dec 11054  df-uz 11162  df-rp 11305  df-fl 12029  df-mod 12098  df-seq 12215  df-exp 12274
This theorem is referenced by:  4001lem2  15106  4001lem3  15107
  Copyright terms: Public domain W3C validator