Theorem 4001lem2 14605

Description: Lemma for 4001prm 14608. Calculate a power mod. In decimal, we calculate 2 ^ 4 0 0 = ( 2 ^ 2 0 0 ) ^ 2 == 9 0 2 ^ 2 = 2 0 3 N + 1 4 0 1 and 2 ^ 8 0 0 = ( 2 ^ 4 0 0 ) ^ 2 == 1 4 0 1 ^ 2 = 4 9 0 N + 2 3 1 1 == 2 3 1 1. (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
4001lem2	|- ( ( 2 ^;; 8 0 0 ) mod N ) = (;;; 2 3 1 1 mod N )

Proof of Theorem 4001lem2

Step	Hyp	Ref	Expression
1		4001prm.1	. . 3 |- N = ;;; 4 0 0 1
2		4nn0 10821	. . . . . 6 |- 4 e. NN0
3		0nn0 10817	. . . . . 6 |- 0 e. NN0
4	2, 3	deccl 10999	. . . . 5 |- ; 4 0 e. NN0
5	4, 3	deccl 10999	. . . 4 |- ;; 4 0 0 e. NN0
6		1nn 10554	. . . 4 |- 1 e. NN
7	5, 6	decnncl 10998	. . 3 |- ;;; 4 0 0 1 e. NN
8	1, 7	eqeltri 2527	. 2 |- N e. NN
9		2nn 10700	. 2 |- 2 e. NN
10		9nn0 10826	. . . . 5 |- 9 e. NN0
11	2, 10	deccl 10999	. . . 4 |- ; 4 9 e. NN0
12	11, 3	deccl 10999	. . 3 |- ;; 4 9 0 e. NN0
13	12	nn0zi 10896	. 2 |- ;; 4 9 0 e. ZZ
14		1nn0 10818	. . . . 5 |- 1 e. NN0
15	14, 2	deccl 10999	. . . 4 |- ; 1 4 e. NN0
16	15, 3	deccl 10999	. . 3 |- ;; 1 4 0 e. NN0
17	16, 14	deccl 10999	. 2 |- ;;; 1 4 0 1 e. NN0
18		2nn0 10819	. . . . 5 |- 2 e. NN0
19		3nn0 10820	. . . . 5 |- 3 e. NN0
20	18, 19	deccl 10999	. . . 4 |- ; 2 3 e. NN0
21	20, 14	deccl 10999	. . 3 |- ;; 2 3 1 e. NN0
22	21, 14	deccl 10999	. 2 |- ;;; 2 3 1 1 e. NN0
23	18, 3	deccl 10999	. . . 4 |- ; 2 0 e. NN0
24	23, 3	deccl 10999	. . 3 |- ;; 2 0 0 e. NN0
25	23, 19	deccl 10999	. . . 4 |- ;; 2 0 3 e. NN0
26	25	nn0zi 10896	. . 3 |- ;; 2 0 3 e. ZZ
27	10, 3	deccl 10999	. . . 4 |- ; 9 0 e. NN0
28	27, 18	deccl 10999	. . 3 |- ;; 9 0 2 e. NN0
29	1	4001lem1 14604	. . 3 |- ( ( 2 ^;; 2 0 0 ) mod N ) = (;; 9 0 2 mod N )
30		eqid 2443	. . . 4 |- ;; 2 0 0 = ;; 2 0 0
31		eqid 2443	. . . . . . 7 |- ; 2 0 = ; 2 0
32		2t2e4 10692	. . . . . . . . 9 |- ( 2 x. 2 ) = 4
33	32	oveq1i 6291	. . . . . . . 8 |- ( ( 2 x. 2 ) + 0 ) = ( 4 + 0 )
34		4cn 10620	. . . . . . . . 9 |- 4 e. CC
35	34	addid1i 9770	. . . . . . . 8 |- ( 4 + 0 ) = 4
36	33, 35	eqtri 2472	. . . . . . 7 |- ( ( 2 x. 2 ) + 0 ) = 4
37		2cn 10613	. . . . . . . . 9 |- 2 e. CC
38	37	mul01i 9773	. . . . . . . 8 |- ( 2 x. 0 ) = 0
39	3	dec0h 11001	. . . . . . . 8 |- 0 = ; 0 0
40	38, 39	eqtri 2472	. . . . . . 7 |- ( 2 x. 0 ) = ; 0 0
41	18, 18, 3, 31, 3, 3, 36, 40	decmul2c 11033	. . . . . 6 |- ( 2 x. ; 2 0 ) = ; 4 0
42	41	oveq1i 6291	. . . . 5 |- ( ( 2 x. ; 2 0 ) + 0 ) = (; 4 0 + 0 )
43	4	nn0cni 10814	. . . . . 6 |- ; 4 0 e. CC
44	43	addid1i 9770	. . . . 5 |- (; 4 0 + 0 ) = ; 4 0
45	42, 44	eqtri 2472	. . . 4 |- ( ( 2 x. ; 2 0 ) + 0 ) = ; 4 0
46	18, 23, 3, 30, 3, 3, 45, 40	decmul2c 11033	. . 3 |- ( 2 x. ;; 2 0 0 ) = ;; 4 0 0
47		eqid 2443	. . . . 5 |- ;;; 1 4 0 1 = ;;; 1 4 0 1
48		6nn0 10823	. . . . . . 7 |- 6 e. NN0
49	14, 48	deccl 10999	. . . . . 6 |- ; 1 6 e. NN0
50		eqid 2443	. . . . . 6 |- ;; 4 0 0 = ;; 4 0 0
51		eqid 2443	. . . . . . 7 |- ;; 1 4 0 = ;; 1 4 0
52		eqid 2443	. . . . . . . 8 |- ; 1 4 = ; 1 4
53		4p2e6 10677	. . . . . . . 8 |- ( 4 + 2 ) = 6
54	14, 2, 18, 52, 53	decaddi 11029	. . . . . . 7 |- (; 1 4 + 2 ) = ; 1 6
55		00id 9758	. . . . . . 7 |- ( 0 + 0 ) = 0
56	15, 3, 18, 3, 51, 31, 54, 55	decadd 11026	. . . . . 6 |- (;; 1 4 0 + ; 2 0 ) = ;; 1 6 0
57		eqid 2443	. . . . . . 7 |- ; 4 0 = ; 4 0
58	49	nn0cni 10814	. . . . . . . 8 |- ; 1 6 e. CC
59	58	addid1i 9770	. . . . . . 7 |- (; 1 6 + 0 ) = ; 1 6
60		eqid 2443	. . . . . . . 8 |- ;; 2 0 3 = ;; 2 0 3
61		ax-1cn 9553	. . . . . . . . . 10 |- 1 e. CC
62	61	addid1i 9770	. . . . . . . . 9 |- ( 1 + 0 ) = 1
63	14	dec0h 11001	. . . . . . . . 9 |- 1 = ; 0 1
64	62, 63	eqtri 2472	. . . . . . . 8 |- ( 1 + 0 ) = ; 0 1
65	61	addid2i 9771	. . . . . . . . . 10 |- ( 0 + 1 ) = 1
66	65, 63	eqtri 2472	. . . . . . . . 9 |- ( 0 + 1 ) = ; 0 1
67		4t2e8 10696	. . . . . . . . . . . 12 |- ( 4 x. 2 ) = 8
68	34, 37, 67	mulcomli 9606	. . . . . . . . . . 11 |- ( 2 x. 4 ) = 8
69	68, 55	oveq12i 6293	. . . . . . . . . 10 |- ( ( 2 x. 4 ) + ( 0 + 0 ) ) = ( 8 + 0 )
70		8cn 10628	. . . . . . . . . . 11 |- 8 e. CC
71	70	addid1i 9770	. . . . . . . . . 10 |- ( 8 + 0 ) = 8
72	69, 71	eqtri 2472	. . . . . . . . 9 |- ( ( 2 x. 4 ) + ( 0 + 0 ) ) = 8
73	34	mul02i 9772	. . . . . . . . . . 11 |- ( 0 x. 4 ) = 0
74	73	oveq1i 6291	. . . . . . . . . 10 |- ( ( 0 x. 4 ) + 1 ) = ( 0 + 1 )
75	74, 65, 63	3eqtri 2476	. . . . . . . . 9 |- ( ( 0 x. 4 ) + 1 ) = ; 0 1
76	18, 3, 3, 14, 31, 66, 2, 14, 3, 72, 75	decmac 11024	. . . . . . . 8 |- ( (; 2 0 x. 4 ) + ( 0 + 1 ) ) = ; 8 1
77		2p1e3 10666	. . . . . . . . 9 |- ( 2 + 1 ) = 3
78		3cn 10617	. . . . . . . . . 10 |- 3 e. CC
79		4t3e12 11057	. . . . . . . . . 10 |- ( 4 x. 3 ) = ; 1 2
80	34, 78, 79	mulcomli 9606	. . . . . . . . 9 |- ( 3 x. 4 ) = ; 1 2
81	14, 18, 77, 80	decsuc 11008	. . . . . . . 8 |- ( ( 3 x. 4 ) + 1 ) = ; 1 3
82	23, 19, 3, 14, 60, 64, 2, 19, 14, 76, 81	decmac 11024	. . . . . . 7 |- ( (;; 2 0 3 x. 4 ) + ( 1 + 0 ) ) = ;; 8 1 3
83	25	nn0cni 10814	. . . . . . . . . 10 |- ;; 2 0 3 e. CC
84	83	mul01i 9773	. . . . . . . . 9 |- (;; 2 0 3 x. 0 ) = 0
85	84	oveq1i 6291	. . . . . . . 8 |- ( (;; 2 0 3 x. 0 ) + 6 ) = ( 0 + 6 )
86		6cn 10624	. . . . . . . . 9 |- 6 e. CC
87	86	addid2i 9771	. . . . . . . 8 |- ( 0 + 6 ) = 6
88	48	dec0h 11001	. . . . . . . 8 |- 6 = ; 0 6
89	85, 87, 88	3eqtri 2476	. . . . . . 7 |- ( (;; 2 0 3 x. 0 ) + 6 ) = ; 0 6
90	2, 3, 14, 48, 57, 59, 25, 48, 3, 82, 89	decma2c 11025	. . . . . 6 |- ( (;; 2 0 3 x. ; 4 0 ) + (; 1 6 + 0 ) ) = ;;; 8 1 3 6
91	84	oveq1i 6291	. . . . . . 7 |- ( (;; 2 0 3 x. 0 ) + 0 ) = ( 0 + 0 )
92	91, 55, 39	3eqtri 2476	. . . . . 6 |- ( (;; 2 0 3 x. 0 ) + 0 ) = ; 0 0
93	4, 3, 49, 3, 50, 56, 25, 3, 3, 90, 92	decma2c 11025	. . . . 5 |- ( (;; 2 0 3 x. ;; 4 0 0 ) + (;; 1 4 0 + ; 2 0 ) ) = ;;;; 8 1 3 6 0
94	55, 39	eqtri 2472	. . . . . . 7 |- ( 0 + 0 ) = ; 0 0
95	37	mulid1i 9601	. . . . . . . . 9 |- ( 2 x. 1 ) = 2
96	95, 55	oveq12i 6293	. . . . . . . 8 |- ( ( 2 x. 1 ) + ( 0 + 0 ) ) = ( 2 + 0 )
97	37	addid1i 9770	. . . . . . . 8 |- ( 2 + 0 ) = 2
98	96, 97	eqtri 2472	. . . . . . 7 |- ( ( 2 x. 1 ) + ( 0 + 0 ) ) = 2
99	61	mul02i 9772	. . . . . . . . 9 |- ( 0 x. 1 ) = 0
100	99	oveq1i 6291	. . . . . . . 8 |- ( ( 0 x. 1 ) + 0 ) = ( 0 + 0 )
101	100, 55, 39	3eqtri 2476	. . . . . . 7 |- ( ( 0 x. 1 ) + 0 ) = ; 0 0
102	18, 3, 3, 3, 31, 94, 14, 3, 3, 98, 101	decmac 11024	. . . . . 6 |- ( (; 2 0 x. 1 ) + ( 0 + 0 ) ) = ; 2 0
103	78	mulid1i 9601	. . . . . . . 8 |- ( 3 x. 1 ) = 3
104	103	oveq1i 6291	. . . . . . 7 |- ( ( 3 x. 1 ) + 1 ) = ( 3 + 1 )
105		3p1e4 10668	. . . . . . 7 |- ( 3 + 1 ) = 4
106	2	dec0h 11001	. . . . . . 7 |- 4 = ; 0 4
107	104, 105, 106	3eqtri 2476	. . . . . 6 |- ( ( 3 x. 1 ) + 1 ) = ; 0 4
108	23, 19, 3, 14, 60, 63, 14, 2, 3, 102, 107	decmac 11024	. . . . 5 |- ( (;; 2 0 3 x. 1 ) + 1 ) = ;; 2 0 4
109	5, 14, 16, 14, 1, 47, 25, 2, 23, 93, 108	decma2c 11025	. . . 4 |- ( (;; 2 0 3 x. N ) + ;;; 1 4 0 1 ) = ;;;;; 8 1 3 6 0 4
110		eqid 2443	. . . . 5 |- ;; 9 0 2 = ;; 9 0 2
111		8nn0 10825	. . . . . . 7 |- 8 e. NN0
112	14, 111	deccl 10999	. . . . . 6 |- ; 1 8 e. NN0
113	112, 3	deccl 10999	. . . . 5 |- ;; 1 8 0 e. NN0
114		eqid 2443	. . . . . 6 |- ; 9 0 = ; 9 0
115		eqid 2443	. . . . . 6 |- ;; 1 8 0 = ;; 1 8 0
116	112	nn0cni 10814	. . . . . . . 8 |- ; 1 8 e. CC
117	116	addid1i 9770	. . . . . . 7 |- (; 1 8 + 0 ) = ; 1 8
118		1p2e3 10667	. . . . . . . . 9 |- ( 1 + 2 ) = 3
119	19	dec0h 11001	. . . . . . . . 9 |- 3 = ; 0 3
120	118, 119	eqtri 2472	. . . . . . . 8 |- ( 1 + 2 ) = ; 0 3
121		9t9e81 11087	. . . . . . . . . 10 |- ( 9 x. 9 ) = ; 8 1
122	121	oveq1i 6291	. . . . . . . . 9 |- ( ( 9 x. 9 ) + 0 ) = (; 8 1 + 0 )
123	111, 14	deccl 10999	. . . . . . . . . . 11 |- ; 8 1 e. NN0
124	123	nn0cni 10814	. . . . . . . . . 10 |- ; 8 1 e. CC
125	124	addid1i 9770	. . . . . . . . 9 |- (; 8 1 + 0 ) = ; 8 1
126	122, 125	eqtri 2472	. . . . . . . 8 |- ( ( 9 x. 9 ) + 0 ) = ; 8 1
127		9cn 10630	. . . . . . . . . . 11 |- 9 e. CC
128	127	mul02i 9772	. . . . . . . . . 10 |- ( 0 x. 9 ) = 0
129	128	oveq1i 6291	. . . . . . . . 9 |- ( ( 0 x. 9 ) + 3 ) = ( 0 + 3 )
130	78	addid2i 9771	. . . . . . . . 9 |- ( 0 + 3 ) = 3
131	129, 130	eqtri 2472	. . . . . . . 8 |- ( ( 0 x. 9 ) + 3 ) = 3
132	10, 3, 3, 19, 114, 120, 10, 126, 131	decma 11023	. . . . . . 7 |- ( (; 9 0 x. 9 ) + ( 1 + 2 ) ) = ;; 8 1 3
133		9t2e18 11080	. . . . . . . . 9 |- ( 9 x. 2 ) = ; 1 8
134	127, 37, 133	mulcomli 9606	. . . . . . . 8 |- ( 2 x. 9 ) = ; 1 8
135		1p1e2 10656	. . . . . . . 8 |- ( 1 + 1 ) = 2
136		8p8e16 11046	. . . . . . . 8 |- ( 8 + 8 ) = ; 1 6
137	14, 111, 111, 134, 135, 48, 136	decaddci 11030	. . . . . . 7 |- ( ( 2 x. 9 ) + 8 ) = ; 2 6
138	27, 18, 14, 111, 110, 117, 10, 48, 18, 132, 137	decmac 11024	. . . . . 6 |- ( (;; 9 0 2 x. 9 ) + (; 1 8 + 0 ) ) = ;;; 8 1 3 6
139	28	nn0cni 10814	. . . . . . . . 9 |- ;; 9 0 2 e. CC
140	139	mul01i 9773	. . . . . . . 8 |- (;; 9 0 2 x. 0 ) = 0
141	140	oveq1i 6291	. . . . . . 7 |- ( (;; 9 0 2 x. 0 ) + 0 ) = ( 0 + 0 )
142	141, 55, 39	3eqtri 2476	. . . . . 6 |- ( (;; 9 0 2 x. 0 ) + 0 ) = ; 0 0
143	10, 3, 112, 3, 114, 115, 28, 3, 3, 138, 142	decma2c 11025	. . . . 5 |- ( (;; 9 0 2 x. ; 9 0 ) + ;; 1 8 0 ) = ;;;; 8 1 3 6 0
144	133	oveq1i 6291	. . . . . . . . . 10 |- ( ( 9 x. 2 ) + 0 ) = (; 1 8 + 0 )
145	144, 117	eqtri 2472	. . . . . . . . 9 |- ( ( 9 x. 2 ) + 0 ) = ; 1 8
146	37	mul02i 9772	. . . . . . . . . 10 |- ( 0 x. 2 ) = 0
147	146, 39	eqtri 2472	. . . . . . . . 9 |- ( 0 x. 2 ) = ; 0 0
148	18, 10, 3, 114, 3, 3, 145, 147	decmul1c 11032	. . . . . . . 8 |- (; 9 0 x. 2 ) = ;; 1 8 0
149	148	oveq1i 6291	. . . . . . 7 |- ( (; 9 0 x. 2 ) + 0 ) = (;; 1 8 0 + 0 )
150	113	nn0cni 10814	. . . . . . . 8 |- ;; 1 8 0 e. CC
151	150	addid1i 9770	. . . . . . 7 |- (;; 1 8 0 + 0 ) = ;; 1 8 0
152	149, 151	eqtri 2472	. . . . . 6 |- ( (; 9 0 x. 2 ) + 0 ) = ;; 1 8 0
153	32, 106	eqtri 2472	. . . . . 6 |- ( 2 x. 2 ) = ; 0 4
154	18, 27, 18, 110, 2, 3, 152, 153	decmul1c 11032	. . . . 5 |- (;; 9 0 2 x. 2 ) = ;;; 1 8 0 4
155	28, 27, 18, 110, 2, 113, 143, 154	decmul2c 11033	. . . 4 |- (;; 9 0 2 x. ;; 9 0 2 ) = ;;;;; 8 1 3 6 0 4
156	109, 155	eqtr4i 2475	. . 3 |- ( (;; 2 0 3 x. N ) + ;;; 1 4 0 1 ) = (;; 9 0 2 x. ;; 9 0 2 )
157	8, 9, 24, 26, 28, 17, 29, 46, 156	mod2xi 14536	. 2 |- ( ( 2 ^;; 4 0 0 ) mod N ) = (;;; 1 4 0 1 mod N )
158	68	oveq1i 6291	. . . . . . 7 |- ( ( 2 x. 4 ) + 0 ) = ( 8 + 0 )
159	158, 71	eqtri 2472	. . . . . 6 |- ( ( 2 x. 4 ) + 0 ) = 8
160	18, 2, 3, 57, 3, 3, 159, 40	decmul2c 11033	. . . . 5 |- ( 2 x. ; 4 0 ) = ; 8 0
161	160	oveq1i 6291	. . . 4 |- ( ( 2 x. ; 4 0 ) + 0 ) = (; 8 0 + 0 )
162	111, 3	deccl 10999	. . . . . 6 |- ; 8 0 e. NN0
163	162	nn0cni 10814	. . . . 5 |- ; 8 0 e. CC
164	163	addid1i 9770	. . . 4 |- (; 8 0 + 0 ) = ; 8 0
165	161, 164	eqtri 2472	. . 3 |- ( ( 2 x. ; 4 0 ) + 0 ) = ; 8 0
166	18, 4, 3, 50, 3, 3, 165, 40	decmul2c 11033	. 2 |- ( 2 x. ;; 4 0 0 ) = ;; 8 0 0
167		eqid 2443	. . . 4 |- ;;; 2 3 1 1 = ;;; 2 3 1 1
168	18, 111	deccl 10999	. . . . 5 |- ; 2 8 e. NN0
169		eqid 2443	. . . . . 6 |- ;; 2 3 1 = ;; 2 3 1
170		eqid 2443	. . . . . 6 |- ; 4 9 = ; 4 9
171		7nn0 10824	. . . . . . 7 |- 7 e. NN0
172		7p1e8 10672	. . . . . . 7 |- ( 7 + 1 ) = 8
173		eqid 2443	. . . . . . . 8 |- ; 2 3 = ; 2 3
174		4p3e7 10678	. . . . . . . . 9 |- ( 4 + 3 ) = 7
175	34, 78, 174	addcomli 9775	. . . . . . . 8 |- ( 3 + 4 ) = 7
176	18, 19, 2, 173, 175	decaddi 11029	. . . . . . 7 |- (; 2 3 + 4 ) = ; 2 7
177	18, 171, 172, 176	decsuc 11008	. . . . . 6 |- ( (; 2 3 + 4 ) + 1 ) = ; 2 8
178		9p1e10 10674	. . . . . . 7 |- ( 9 + 1 ) = 10
179	127, 61, 178	addcomli 9775	. . . . . 6 |- ( 1 + 9 ) = 10
180	20, 14, 2, 10, 169, 170, 177, 179	decaddc2 11028	. . . . 5 |- (;; 2 3 1 + ; 4 9 ) = ;; 2 8 0
181	168	nn0cni 10814	. . . . . . 7 |- ; 2 8 e. CC
182	181	addid1i 9770	. . . . . 6 |- (; 2 8 + 0 ) = ; 2 8
183		eqid 2443	. . . . . . 7 |- ;; 4 9 0 = ;; 4 9 0
184	18	dec0h 11001	. . . . . . . 8 |- 2 = ; 0 2
185	97, 184	eqtri 2472	. . . . . . 7 |- ( 2 + 0 ) = ; 0 2
186	130	oveq2i 6292	. . . . . . . . 9 |- ( ( 4 x. 4 ) + ( 0 + 3 ) ) = ( ( 4 x. 4 ) + 3 )
187		4t4e16 11058	. . . . . . . . . 10 |- ( 4 x. 4 ) = ; 1 6
188		6p3e9 10685	. . . . . . . . . 10 |- ( 6 + 3 ) = 9
189	14, 48, 19, 187, 188	decaddi 11029	. . . . . . . . 9 |- ( ( 4 x. 4 ) + 3 ) = ; 1 9
190	186, 189	eqtri 2472	. . . . . . . 8 |- ( ( 4 x. 4 ) + ( 0 + 3 ) ) = ; 1 9
191		9t4e36 11082	. . . . . . . . . 10 |- ( 9 x. 4 ) = ; 3 6
192	191	oveq1i 6291	. . . . . . . . 9 |- ( ( 9 x. 4 ) + 0 ) = (; 3 6 + 0 )
193	19, 48	deccl 10999	. . . . . . . . . . 11 |- ; 3 6 e. NN0
194	193	nn0cni 10814	. . . . . . . . . 10 |- ; 3 6 e. CC
195	194	addid1i 9770	. . . . . . . . 9 |- (; 3 6 + 0 ) = ; 3 6
196	192, 195	eqtri 2472	. . . . . . . 8 |- ( ( 9 x. 4 ) + 0 ) = ; 3 6
197	2, 10, 3, 3, 170, 94, 2, 48, 19, 190, 196	decmac 11024	. . . . . . 7 |- ( (; 4 9 x. 4 ) + ( 0 + 0 ) ) = ;; 1 9 6
198	73	oveq1i 6291	. . . . . . . 8 |- ( ( 0 x. 4 ) + 2 ) = ( 0 + 2 )
199	37	addid2i 9771	. . . . . . . 8 |- ( 0 + 2 ) = 2
200	198, 199, 184	3eqtri 2476	. . . . . . 7 |- ( ( 0 x. 4 ) + 2 ) = ; 0 2
201	11, 3, 3, 18, 183, 185, 2, 18, 3, 197, 200	decmac 11024	. . . . . 6 |- ( (;; 4 9 0 x. 4 ) + ( 2 + 0 ) ) = ;;; 1 9 6 2
202	12	nn0cni 10814	. . . . . . . . 9 |- ;; 4 9 0 e. CC
203	202	mul01i 9773	. . . . . . . 8 |- (;; 4 9 0 x. 0 ) = 0
204	203	oveq1i 6291	. . . . . . 7 |- ( (;; 4 9 0 x. 0 ) + 8 ) = ( 0 + 8 )
205	70	addid2i 9771	. . . . . . 7 |- ( 0 + 8 ) = 8
206	111	dec0h 11001	. . . . . . 7 |- 8 = ; 0 8
207	204, 205, 206	3eqtri 2476	. . . . . 6 |- ( (;; 4 9 0 x. 0 ) + 8 ) = ; 0 8
208	2, 3, 18, 111, 57, 182, 12, 111, 3, 201, 207	decma2c 11025	. . . . 5 |- ( (;; 4 9 0 x. ; 4 0 ) + (; 2 8 + 0 ) ) = ;;;; 1 9 6 2 8
209	203	oveq1i 6291	. . . . . 6 |- ( (;; 4 9 0 x. 0 ) + 0 ) = ( 0 + 0 )
210	209, 55, 39	3eqtri 2476	. . . . 5 |- ( (;; 4 9 0 x. 0 ) + 0 ) = ; 0 0
211	4, 3, 168, 3, 50, 180, 12, 3, 3, 208, 210	decma2c 11025	. . . 4 |- ( (;; 4 9 0 x. ;; 4 0 0 ) + (;; 2 3 1 + ; 4 9 ) ) = ;;;;; 1 9 6 2 8 0
212	34	mulid1i 9601	. . . . . . . 8 |- ( 4 x. 1 ) = 4
213	212, 55	oveq12i 6293	. . . . . . 7 |- ( ( 4 x. 1 ) + ( 0 + 0 ) ) = ( 4 + 0 )
214	213, 35	eqtri 2472	. . . . . 6 |- ( ( 4 x. 1 ) + ( 0 + 0 ) ) = 4
215	127	mulid1i 9601	. . . . . . . 8 |- ( 9 x. 1 ) = 9
216	215	oveq1i 6291	. . . . . . 7 |- ( ( 9 x. 1 ) + 0 ) = ( 9 + 0 )
217	127	addid1i 9770	. . . . . . 7 |- ( 9 + 0 ) = 9
218	10	dec0h 11001	. . . . . . 7 |- 9 = ; 0 9
219	216, 217, 218	3eqtri 2476	. . . . . 6 |- ( ( 9 x. 1 ) + 0 ) = ; 0 9
220	2, 10, 3, 3, 170, 94, 14, 10, 3, 214, 219	decmac 11024	. . . . 5 |- ( (; 4 9 x. 1 ) + ( 0 + 0 ) ) = ; 4 9
221	99	oveq1i 6291	. . . . . 6 |- ( ( 0 x. 1 ) + 1 ) = ( 0 + 1 )
222	221, 65, 63	3eqtri 2476	. . . . 5 |- ( ( 0 x. 1 ) + 1 ) = ; 0 1
223	11, 3, 3, 14, 183, 63, 14, 14, 3, 220, 222	decmac 11024	. . . 4 |- ( (;; 4 9 0 x. 1 ) + 1 ) = ;; 4 9 1
224	5, 14, 21, 14, 1, 167, 12, 14, 11, 211, 223	decma2c 11025	. . 3 |- ( (;; 4 9 0 x. N ) + ;;; 2 3 1 1 ) = ;;;;;; 1 9 6 2 8 0 1
225	15	nn0cni 10814	. . . . . . 7 |- ; 1 4 e. CC
226	225	addid1i 9770	. . . . . 6 |- (; 1 4 + 0 ) = ; 1 4
227		5nn0 10822	. . . . . . . 8 |- 5 e. NN0
228	227, 48	deccl 10999	. . . . . . 7 |- ; 5 6 e. NN0
229	228, 3	deccl 10999	. . . . . 6 |- ;; 5 6 0 e. NN0
230		eqid 2443	. . . . . . . 8 |- ;; 5 6 0 = ;; 5 6 0
231	228	nn0cni 10814	. . . . . . . . 9 |- ; 5 6 e. CC
232	231	addid2i 9771	. . . . . . . 8 |- ( 0 + ; 5 6 ) = ; 5 6
233	3, 14, 228, 3, 63, 230, 232, 62	decadd 11026	. . . . . . 7 |- ( 1 + ;; 5 6 0 ) = ;; 5 6 1
234	231	addid1i 9770	. . . . . . . 8 |- (; 5 6 + 0 ) = ; 5 6
235		5cn 10622	. . . . . . . . . . 11 |- 5 e. CC
236	235	addid1i 9770	. . . . . . . . . 10 |- ( 5 + 0 ) = 5
237	227	dec0h 11001	. . . . . . . . . 10 |- 5 = ; 0 5
238	236, 237	eqtri 2472	. . . . . . . . 9 |- ( 5 + 0 ) = ; 0 5
239	61	mulid1i 9601	. . . . . . . . . . 11 |- ( 1 x. 1 ) = 1
240	239, 55	oveq12i 6293	. . . . . . . . . 10 |- ( ( 1 x. 1 ) + ( 0 + 0 ) ) = ( 1 + 0 )
241	240, 62	eqtri 2472	. . . . . . . . 9 |- ( ( 1 x. 1 ) + ( 0 + 0 ) ) = 1
242	212	oveq1i 6291	. . . . . . . . . 10 |- ( ( 4 x. 1 ) + 5 ) = ( 4 + 5 )
243		5p4e9 10682	. . . . . . . . . . 11 |- ( 5 + 4 ) = 9
244	235, 34, 243	addcomli 9775	. . . . . . . . . 10 |- ( 4 + 5 ) = 9
245	242, 244, 218	3eqtri 2476	. . . . . . . . 9 |- ( ( 4 x. 1 ) + 5 ) = ; 0 9
246	14, 2, 3, 227, 52, 238, 14, 10, 3, 241, 245	decmac 11024	. . . . . . . 8 |- ( (; 1 4 x. 1 ) + ( 5 + 0 ) ) = ; 1 9
247	99	oveq1i 6291	. . . . . . . . 9 |- ( ( 0 x. 1 ) + 6 ) = ( 0 + 6 )
248	247, 87, 88	3eqtri 2476	. . . . . . . 8 |- ( ( 0 x. 1 ) + 6 ) = ; 0 6
249	15, 3, 227, 48, 51, 234, 14, 48, 3, 246, 248	decmac 11024	. . . . . . 7 |- ( (;; 1 4 0 x. 1 ) + (; 5 6 + 0 ) ) = ;; 1 9 6
250	239	oveq1i 6291	. . . . . . . 8 |- ( ( 1 x. 1 ) + 1 ) = ( 1 + 1 )
251	250, 135, 184	3eqtri 2476	. . . . . . 7 |- ( ( 1 x. 1 ) + 1 ) = ; 0 2
252	16, 14, 228, 14, 47, 233, 14, 18, 3, 249, 251	decmac 11024	. . . . . 6 |- ( (;;; 1 4 0 1 x. 1 ) + ( 1 + ;; 5 6 0 ) ) = ;;; 1 9 6 2
253	34	mulid2i 9602	. . . . . . . . . . 11 |- ( 1 x. 4 ) = 4
254	253, 65	oveq12i 6293	. . . . . . . . . 10 |- ( ( 1 x. 4 ) + ( 0 + 1 ) ) = ( 4 + 1 )
255		4p1e5 10669	. . . . . . . . . 10 |- ( 4 + 1 ) = 5
256	254, 255	eqtri 2472	. . . . . . . . 9 |- ( ( 1 x. 4 ) + ( 0 + 1 ) ) = 5
257	187	oveq1i 6291	. . . . . . . . . 10 |- ( ( 4 x. 4 ) + 0 ) = (; 1 6 + 0 )
258	257, 59	eqtri 2472	. . . . . . . . 9 |- ( ( 4 x. 4 ) + 0 ) = ; 1 6
259	14, 2, 3, 3, 52, 94, 2, 48, 14, 256, 258	decmac 11024	. . . . . . . 8 |- ( (; 1 4 x. 4 ) + ( 0 + 0 ) ) = ; 5 6
260	73	oveq1i 6291	. . . . . . . . 9 |- ( ( 0 x. 4 ) + 0 ) = ( 0 + 0 )
261	260, 55, 39	3eqtri 2476	. . . . . . . 8 |- ( ( 0 x. 4 ) + 0 ) = ; 0 0
262	15, 3, 3, 3, 51, 94, 2, 3, 3, 259, 261	decmac 11024	. . . . . . 7 |- ( (;; 1 4 0 x. 4 ) + ( 0 + 0 ) ) = ;; 5 6 0
263	253	oveq1i 6291	. . . . . . . 8 |- ( ( 1 x. 4 ) + 4 ) = ( 4 + 4 )
264		4p4e8 10679	. . . . . . . 8 |- ( 4 + 4 ) = 8
265	263, 264, 206	3eqtri 2476	. . . . . . 7 |- ( ( 1 x. 4 ) + 4 ) = ; 0 8
266	16, 14, 3, 2, 47, 106, 2, 111, 3, 262, 265	decmac 11024	. . . . . 6 |- ( (;;; 1 4 0 1 x. 4 ) + 4 ) = ;;; 5 6 0 8
267	14, 2, 14, 2, 52, 226, 17, 111, 229, 252, 266	decma2c 11025	. . . . 5 |- ( (;;; 1 4 0 1 x. ; 1 4 ) + (; 1 4 + 0 ) ) = ;;;; 1 9 6 2 8
268	17	nn0cni 10814	. . . . . . . 8 |- ;;; 1 4 0 1 e. CC
269	268	mul01i 9773	. . . . . . 7 |- (;;; 1 4 0 1 x. 0 ) = 0
270	269	oveq1i 6291	. . . . . 6 |- ( (;;; 1 4 0 1 x. 0 ) + 0 ) = ( 0 + 0 )
271	270, 55, 39	3eqtri 2476	. . . . 5 |- ( (;;; 1 4 0 1 x. 0 ) + 0 ) = ; 0 0
272	15, 3, 15, 3, 51, 51, 17, 3, 3, 267, 271	decma2c 11025	. . . 4 |- ( (;;; 1 4 0 1 x. ;; 1 4 0 ) + ;; 1 4 0 ) = ;;;;; 1 9 6 2 8 0
273	268	mulid1i 9601	. . . 4 |- (;;; 1 4 0 1 x. 1 ) = ;;; 1 4 0 1
274	17, 16, 14, 47, 14, 16, 272, 273	decmul2c 11033	. . 3 |- (;;; 1 4 0 1 x. ;;; 1 4 0 1 ) = ;;;;;; 1 9 6 2 8 0 1
275	224, 274	eqtr4i 2475	. 2 |- ( (;; 4 9 0 x. N ) + ;;; 2 3 1 1 ) = (;;; 1 4 0 1 x. ;;; 1 4 0 1 )
276	8, 9, 5, 13, 17, 22, 157, 166, 275	mod2xi 14536	1 |- ( ( 2 ^;; 8 0 0 ) mod N ) = (;;; 2 3 1 1 mod N )

Syntax hints:   = wceq 1383  (class class class)co 6281   0cc0 9495   1c1 9496   + caddc 9498   x. cmul 9500   NNcn 10543   2c2 10592   3c3 10593   4c4 10594   5c5 10595   6c6 10596   7c7 10597   8c8 10598   9c9 10599   10c10 10600  ;cdc 10985   mod cmo 11977   ^cexp 12147

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577  ax-cnex 9551  ax-resscn 9552  ax-1cn 9553  ax-icn 9554  ax-addcl 9555  ax-addrcl 9556  ax-mulcl 9557  ax-mulrcl 9558  ax-mulcom 9559  ax-addass 9560  ax-mulass 9561  ax-distr 9562  ax-i2m1 9563  ax-1ne0 9564  ax-1rid 9565  ax-rnegex 9566  ax-rrecex 9567  ax-cnre 9568  ax-pre-lttri 9569  ax-pre-lttrn 9570  ax-pre-ltadd 9571  ax-pre-mulgt0 9572  ax-pre-sup 9573

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 975  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-nel 2641  df-ral 2798  df-rex 2799  df-reu 2800  df-rmo 2801  df-rab 2802  df-v 3097  df-sbc 3314  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-tp 4019  df-op 4021  df-uni 4235  df-iun 4317  df-br 4438  df-opab 4496  df-mpt 4497  df-tr 4531  df-eprel 4781  df-id 4785  df-po 4790  df-so 4791  df-fr 4828  df-we 4830  df-ord 4871  df-on 4872  df-lim 4873  df-suc 4874  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002  df-iota 5541  df-fun 5580  df-fn 5581  df-f 5582  df-f1 5583  df-fo 5584  df-f1o 5585  df-fv 5586  df-riota 6242  df-ov 6284  df-oprab 6285  df-mpt2 6286  df-om 6686  df-2nd 6786  df-recs 7044  df-rdg 7078  df-er 7313  df-en 7519  df-dom 7520  df-sdom 7521  df-sup 7903  df-pnf 9633  df-mnf 9634  df-xr 9635  df-ltxr 9636  df-le 9637  df-sub 9812  df-neg 9813  df-div 10214  df-nn 10544  df-2 10601  df-3 10602  df-4 10603  df-5 10604  df-6 10605  df-7 10606  df-8 10607  df-9 10608  df-10 10609  df-n0 10803  df-z 10872  df-dec 10986  df-uz 11092  df-rp 11231  df-fl 11910  df-mod 11978  df-seq 12089  df-exp 12148

This theorem is referenced by:  4001lem3  14606  4001lem4  14607