Theorem 4001lem2 15101

Description: Lemma for 4001prm 15104. 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 10889	. . . . . 6 |- 4 e. NN0
3		0nn0 10885	. . . . . 6 |- 0 e. NN0
4	2, 3	deccl 11066	. . . . 5 |- ; 4 0 e. NN0
5	4, 3	deccl 11066	. . . 4 |- ;; 4 0 0 e. NN0
6		1nn 10621	. . . 4 |- 1 e. NN
7	5, 6	decnncl 11065	. . 3 |- ;;; 4 0 0 1 e. NN
8	1, 7	eqeltri 2506	. 2 |- N e. NN
9		2nn 10768	. 2 |- 2 e. NN
10		9nn0 10894	. . . . 5 |- 9 e. NN0
11	2, 10	deccl 11066	. . . 4 |- ; 4 9 e. NN0
12	11, 3	deccl 11066	. . 3 |- ;; 4 9 0 e. NN0
13	12	nn0zi 10963	. 2 |- ;; 4 9 0 e. ZZ
14		1nn0 10886	. . . . 5 |- 1 e. NN0
15	14, 2	deccl 11066	. . . 4 |- ; 1 4 e. NN0
16	15, 3	deccl 11066	. . 3 |- ;; 1 4 0 e. NN0
17	16, 14	deccl 11066	. 2 |- ;;; 1 4 0 1 e. NN0
18		2nn0 10887	. . . . 5 |- 2 e. NN0
19		3nn0 10888	. . . . 5 |- 3 e. NN0
20	18, 19	deccl 11066	. . . 4 |- ; 2 3 e. NN0
21	20, 14	deccl 11066	. . 3 |- ;; 2 3 1 e. NN0
22	21, 14	deccl 11066	. 2 |- ;;; 2 3 1 1 e. NN0
23	18, 3	deccl 11066	. . . 4 |- ; 2 0 e. NN0
24	23, 3	deccl 11066	. . 3 |- ;; 2 0 0 e. NN0
25	23, 19	deccl 11066	. . . 4 |- ;; 2 0 3 e. NN0
26	25	nn0zi 10963	. . 3 |- ;; 2 0 3 e. ZZ
27	10, 3	deccl 11066	. . . 4 |- ; 9 0 e. NN0
28	27, 18	deccl 11066	. . 3 |- ;; 9 0 2 e. NN0
29	1	4001lem1 15100	. . 3 |- ( ( 2 ^;; 2 0 0 ) mod N ) = (;; 9 0 2 mod N )
30		eqid 2422	. . . 4 |- ;; 2 0 0 = ;; 2 0 0
31		eqid 2422	. . . . . . 7 |- ; 2 0 = ; 2 0
32		2t2e4 10760	. . . . . . . . 9 |- ( 2 x. 2 ) = 4
33	32	oveq1i 6312	. . . . . . . 8 |- ( ( 2 x. 2 ) + 0 ) = ( 4 + 0 )
34		4cn 10688	. . . . . . . . 9 |- 4 e. CC
35	34	addid1i 9821	. . . . . . . 8 |- ( 4 + 0 ) = 4
36	33, 35	eqtri 2451	. . . . . . 7 |- ( ( 2 x. 2 ) + 0 ) = 4
37		2cn 10681	. . . . . . . . 9 |- 2 e. CC
38	37	mul01i 9824	. . . . . . . 8 |- ( 2 x. 0 ) = 0
39	3	dec0h 11068	. . . . . . . 8 |- 0 = ; 0 0
40	38, 39	eqtri 2451	. . . . . . 7 |- ( 2 x. 0 ) = ; 0 0
41	18, 18, 3, 31, 3, 3, 36, 40	decmul2c 11100	. . . . . 6 |- ( 2 x. ; 2 0 ) = ; 4 0
42	41	oveq1i 6312	. . . . 5 |- ( ( 2 x. ; 2 0 ) + 0 ) = (; 4 0 + 0 )
43	4	nn0cni 10882	. . . . . 6 |- ; 4 0 e. CC
44	43	addid1i 9821	. . . . 5 |- (; 4 0 + 0 ) = ; 4 0
45	42, 44	eqtri 2451	. . . 4 |- ( ( 2 x. ; 2 0 ) + 0 ) = ; 4 0
46	18, 23, 3, 30, 3, 3, 45, 40	decmul2c 11100	. . 3 |- ( 2 x. ;; 2 0 0 ) = ;; 4 0 0
47		eqid 2422	. . . . 5 |- ;;; 1 4 0 1 = ;;; 1 4 0 1
48		6nn0 10891	. . . . . . 7 |- 6 e. NN0
49	14, 48	deccl 11066	. . . . . 6 |- ; 1 6 e. NN0
50		eqid 2422	. . . . . 6 |- ;; 4 0 0 = ;; 4 0 0
51		eqid 2422	. . . . . . 7 |- ;; 1 4 0 = ;; 1 4 0
52		eqid 2422	. . . . . . . 8 |- ; 1 4 = ; 1 4
53		4p2e6 10745	. . . . . . . 8 |- ( 4 + 2 ) = 6
54	14, 2, 18, 52, 53	decaddi 11096	. . . . . . 7 |- (; 1 4 + 2 ) = ; 1 6
55		00id 9809	. . . . . . 7 |- ( 0 + 0 ) = 0
56	15, 3, 18, 3, 51, 31, 54, 55	decadd 11093	. . . . . 6 |- (;; 1 4 0 + ; 2 0 ) = ;; 1 6 0
57		eqid 2422	. . . . . . 7 |- ; 4 0 = ; 4 0
58	49	nn0cni 10882	. . . . . . . 8 |- ; 1 6 e. CC
59	58	addid1i 9821	. . . . . . 7 |- (; 1 6 + 0 ) = ; 1 6
60		eqid 2422	. . . . . . . 8 |- ;; 2 0 3 = ;; 2 0 3
61		ax-1cn 9598	. . . . . . . . . 10 |- 1 e. CC
62	61	addid1i 9821	. . . . . . . . 9 |- ( 1 + 0 ) = 1
63	14	dec0h 11068	. . . . . . . . 9 |- 1 = ; 0 1
64	62, 63	eqtri 2451	. . . . . . . 8 |- ( 1 + 0 ) = ; 0 1
65	61	addid2i 9822	. . . . . . . . . 10 |- ( 0 + 1 ) = 1
66	65, 63	eqtri 2451	. . . . . . . . 9 |- ( 0 + 1 ) = ; 0 1
67		4t2e8 10764	. . . . . . . . . . . 12 |- ( 4 x. 2 ) = 8
68	34, 37, 67	mulcomli 9651	. . . . . . . . . . 11 |- ( 2 x. 4 ) = 8
69	68, 55	oveq12i 6314	. . . . . . . . . 10 |- ( ( 2 x. 4 ) + ( 0 + 0 ) ) = ( 8 + 0 )
70		8cn 10696	. . . . . . . . . . 11 |- 8 e. CC
71	70	addid1i 9821	. . . . . . . . . 10 |- ( 8 + 0 ) = 8
72	69, 71	eqtri 2451	. . . . . . . . 9 |- ( ( 2 x. 4 ) + ( 0 + 0 ) ) = 8
73	34	mul02i 9823	. . . . . . . . . . 11 |- ( 0 x. 4 ) = 0
74	73	oveq1i 6312	. . . . . . . . . 10 |- ( ( 0 x. 4 ) + 1 ) = ( 0 + 1 )
75	74, 65, 63	3eqtri 2455	. . . . . . . . 9 |- ( ( 0 x. 4 ) + 1 ) = ; 0 1
76	18, 3, 3, 14, 31, 66, 2, 14, 3, 72, 75	decmac 11091	. . . . . . . 8 |- ( (; 2 0 x. 4 ) + ( 0 + 1 ) ) = ; 8 1
77		2p1e3 10734	. . . . . . . . 9 |- ( 2 + 1 ) = 3
78		3cn 10685	. . . . . . . . . 10 |- 3 e. CC
79		4t3e12 11124	. . . . . . . . . 10 |- ( 4 x. 3 ) = ; 1 2
80	34, 78, 79	mulcomli 9651	. . . . . . . . 9 |- ( 3 x. 4 ) = ; 1 2
81	14, 18, 77, 80	decsuc 11075	. . . . . . . 8 |- ( ( 3 x. 4 ) + 1 ) = ; 1 3
82	23, 19, 3, 14, 60, 64, 2, 19, 14, 76, 81	decmac 11091	. . . . . . 7 |- ( (;; 2 0 3 x. 4 ) + ( 1 + 0 ) ) = ;; 8 1 3
83	25	nn0cni 10882	. . . . . . . . . 10 |- ;; 2 0 3 e. CC
84	83	mul01i 9824	. . . . . . . . 9 |- (;; 2 0 3 x. 0 ) = 0
85	84	oveq1i 6312	. . . . . . . 8 |- ( (;; 2 0 3 x. 0 ) + 6 ) = ( 0 + 6 )
86		6cn 10692	. . . . . . . . 9 |- 6 e. CC
87	86	addid2i 9822	. . . . . . . 8 |- ( 0 + 6 ) = 6
88	48	dec0h 11068	. . . . . . . 8 |- 6 = ; 0 6
89	85, 87, 88	3eqtri 2455	. . . . . . 7 |- ( (;; 2 0 3 x. 0 ) + 6 ) = ; 0 6
90	2, 3, 14, 48, 57, 59, 25, 48, 3, 82, 89	decma2c 11092	. . . . . 6 |- ( (;; 2 0 3 x. ; 4 0 ) + (; 1 6 + 0 ) ) = ;;; 8 1 3 6
91	84	oveq1i 6312	. . . . . . 7 |- ( (;; 2 0 3 x. 0 ) + 0 ) = ( 0 + 0 )
92	91, 55, 39	3eqtri 2455	. . . . . 6 |- ( (;; 2 0 3 x. 0 ) + 0 ) = ; 0 0
93	4, 3, 49, 3, 50, 56, 25, 3, 3, 90, 92	decma2c 11092	. . . . 5 |- ( (;; 2 0 3 x. ;; 4 0 0 ) + (;; 1 4 0 + ; 2 0 ) ) = ;;;; 8 1 3 6 0
94	55, 39	eqtri 2451	. . . . . . 7 |- ( 0 + 0 ) = ; 0 0
95	37	mulid1i 9646	. . . . . . . . 9 |- ( 2 x. 1 ) = 2
96	95, 55	oveq12i 6314	. . . . . . . 8 |- ( ( 2 x. 1 ) + ( 0 + 0 ) ) = ( 2 + 0 )
97	37	addid1i 9821	. . . . . . . 8 |- ( 2 + 0 ) = 2
98	96, 97	eqtri 2451	. . . . . . 7 |- ( ( 2 x. 1 ) + ( 0 + 0 ) ) = 2
99	61	mul02i 9823	. . . . . . . . 9 |- ( 0 x. 1 ) = 0
100	99	oveq1i 6312	. . . . . . . 8 |- ( ( 0 x. 1 ) + 0 ) = ( 0 + 0 )
101	100, 55, 39	3eqtri 2455	. . . . . . 7 |- ( ( 0 x. 1 ) + 0 ) = ; 0 0
102	18, 3, 3, 3, 31, 94, 14, 3, 3, 98, 101	decmac 11091	. . . . . 6 |- ( (; 2 0 x. 1 ) + ( 0 + 0 ) ) = ; 2 0
103	78	mulid1i 9646	. . . . . . . 8 |- ( 3 x. 1 ) = 3
104	103	oveq1i 6312	. . . . . . 7 |- ( ( 3 x. 1 ) + 1 ) = ( 3 + 1 )
105		3p1e4 10736	. . . . . . 7 |- ( 3 + 1 ) = 4
106	2	dec0h 11068	. . . . . . 7 |- 4 = ; 0 4
107	104, 105, 106	3eqtri 2455	. . . . . 6 |- ( ( 3 x. 1 ) + 1 ) = ; 0 4
108	23, 19, 3, 14, 60, 63, 14, 2, 3, 102, 107	decmac 11091	. . . . 5 |- ( (;; 2 0 3 x. 1 ) + 1 ) = ;; 2 0 4
109	5, 14, 16, 14, 1, 47, 25, 2, 23, 93, 108	decma2c 11092	. . . 4 |- ( (;; 2 0 3 x. N ) + ;;; 1 4 0 1 ) = ;;;;; 8 1 3 6 0 4
110		eqid 2422	. . . . 5 |- ;; 9 0 2 = ;; 9 0 2
111		8nn0 10893	. . . . . . 7 |- 8 e. NN0
112	14, 111	deccl 11066	. . . . . 6 |- ; 1 8 e. NN0
113	112, 3	deccl 11066	. . . . 5 |- ;; 1 8 0 e. NN0
114		eqid 2422	. . . . . 6 |- ; 9 0 = ; 9 0
115		eqid 2422	. . . . . 6 |- ;; 1 8 0 = ;; 1 8 0
116	112	nn0cni 10882	. . . . . . . 8 |- ; 1 8 e. CC
117	116	addid1i 9821	. . . . . . 7 |- (; 1 8 + 0 ) = ; 1 8
118		1p2e3 10735	. . . . . . . . 9 |- ( 1 + 2 ) = 3
119	19	dec0h 11068	. . . . . . . . 9 |- 3 = ; 0 3
120	118, 119	eqtri 2451	. . . . . . . 8 |- ( 1 + 2 ) = ; 0 3
121		9t9e81 11154	. . . . . . . . . 10 |- ( 9 x. 9 ) = ; 8 1
122	121	oveq1i 6312	. . . . . . . . 9 |- ( ( 9 x. 9 ) + 0 ) = (; 8 1 + 0 )
123	111, 14	deccl 11066	. . . . . . . . . . 11 |- ; 8 1 e. NN0
124	123	nn0cni 10882	. . . . . . . . . 10 |- ; 8 1 e. CC
125	124	addid1i 9821	. . . . . . . . 9 |- (; 8 1 + 0 ) = ; 8 1
126	122, 125	eqtri 2451	. . . . . . . 8 |- ( ( 9 x. 9 ) + 0 ) = ; 8 1
127		9cn 10698	. . . . . . . . . . 11 |- 9 e. CC
128	127	mul02i 9823	. . . . . . . . . 10 |- ( 0 x. 9 ) = 0
129	128	oveq1i 6312	. . . . . . . . 9 |- ( ( 0 x. 9 ) + 3 ) = ( 0 + 3 )
130	78	addid2i 9822	. . . . . . . . 9 |- ( 0 + 3 ) = 3
131	129, 130	eqtri 2451	. . . . . . . 8 |- ( ( 0 x. 9 ) + 3 ) = 3
132	10, 3, 3, 19, 114, 120, 10, 126, 131	decma 11090	. . . . . . 7 |- ( (; 9 0 x. 9 ) + ( 1 + 2 ) ) = ;; 8 1 3
133		9t2e18 11147	. . . . . . . . 9 |- ( 9 x. 2 ) = ; 1 8
134	127, 37, 133	mulcomli 9651	. . . . . . . 8 |- ( 2 x. 9 ) = ; 1 8
135		1p1e2 10724	. . . . . . . 8 |- ( 1 + 1 ) = 2
136		8p8e16 11113	. . . . . . . 8 |- ( 8 + 8 ) = ; 1 6
137	14, 111, 111, 134, 135, 48, 136	decaddci 11097	. . . . . . 7 |- ( ( 2 x. 9 ) + 8 ) = ; 2 6
138	27, 18, 14, 111, 110, 117, 10, 48, 18, 132, 137	decmac 11091	. . . . . 6 |- ( (;; 9 0 2 x. 9 ) + (; 1 8 + 0 ) ) = ;;; 8 1 3 6
139	28	nn0cni 10882	. . . . . . . . 9 |- ;; 9 0 2 e. CC
140	139	mul01i 9824	. . . . . . . 8 |- (;; 9 0 2 x. 0 ) = 0
141	140	oveq1i 6312	. . . . . . 7 |- ( (;; 9 0 2 x. 0 ) + 0 ) = ( 0 + 0 )
142	141, 55, 39	3eqtri 2455	. . . . . 6 |- ( (;; 9 0 2 x. 0 ) + 0 ) = ; 0 0
143	10, 3, 112, 3, 114, 115, 28, 3, 3, 138, 142	decma2c 11092	. . . . 5 |- ( (;; 9 0 2 x. ; 9 0 ) + ;; 1 8 0 ) = ;;;; 8 1 3 6 0
144	133	oveq1i 6312	. . . . . . . . . 10 |- ( ( 9 x. 2 ) + 0 ) = (; 1 8 + 0 )
145	144, 117	eqtri 2451	. . . . . . . . 9 |- ( ( 9 x. 2 ) + 0 ) = ; 1 8
146	37	mul02i 9823	. . . . . . . . . 10 |- ( 0 x. 2 ) = 0
147	146, 39	eqtri 2451	. . . . . . . . 9 |- ( 0 x. 2 ) = ; 0 0
148	18, 10, 3, 114, 3, 3, 145, 147	decmul1c 11099	. . . . . . . 8 |- (; 9 0 x. 2 ) = ;; 1 8 0
149	148	oveq1i 6312	. . . . . . 7 |- ( (; 9 0 x. 2 ) + 0 ) = (;; 1 8 0 + 0 )
150	113	nn0cni 10882	. . . . . . . 8 |- ;; 1 8 0 e. CC
151	150	addid1i 9821	. . . . . . 7 |- (;; 1 8 0 + 0 ) = ;; 1 8 0
152	149, 151	eqtri 2451	. . . . . 6 |- ( (; 9 0 x. 2 ) + 0 ) = ;; 1 8 0
153	32, 106	eqtri 2451	. . . . . 6 |- ( 2 x. 2 ) = ; 0 4
154	18, 27, 18, 110, 2, 3, 152, 153	decmul1c 11099	. . . . 5 |- (;; 9 0 2 x. 2 ) = ;;; 1 8 0 4
155	28, 27, 18, 110, 2, 113, 143, 154	decmul2c 11100	. . . 4 |- (;; 9 0 2 x. ;; 9 0 2 ) = ;;;;; 8 1 3 6 0 4
156	109, 155	eqtr4i 2454	. . 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 15029	. 2 |- ( ( 2 ^;; 4 0 0 ) mod N ) = (;;; 1 4 0 1 mod N )
158	68	oveq1i 6312	. . . . . . 7 |- ( ( 2 x. 4 ) + 0 ) = ( 8 + 0 )
159	158, 71	eqtri 2451	. . . . . 6 |- ( ( 2 x. 4 ) + 0 ) = 8
160	18, 2, 3, 57, 3, 3, 159, 40	decmul2c 11100	. . . . 5 |- ( 2 x. ; 4 0 ) = ; 8 0
161	160	oveq1i 6312	. . . 4 |- ( ( 2 x. ; 4 0 ) + 0 ) = (; 8 0 + 0 )
162	111, 3	deccl 11066	. . . . . 6 |- ; 8 0 e. NN0
163	162	nn0cni 10882	. . . . 5 |- ; 8 0 e. CC
164	163	addid1i 9821	. . . 4 |- (; 8 0 + 0 ) = ; 8 0
165	161, 164	eqtri 2451	. . 3 |- ( ( 2 x. ; 4 0 ) + 0 ) = ; 8 0
166	18, 4, 3, 50, 3, 3, 165, 40	decmul2c 11100	. 2 |- ( 2 x. ;; 4 0 0 ) = ;; 8 0 0
167		eqid 2422	. . . 4 |- ;;; 2 3 1 1 = ;;; 2 3 1 1
168	18, 111	deccl 11066	. . . . 5 |- ; 2 8 e. NN0
169		eqid 2422	. . . . . 6 |- ;; 2 3 1 = ;; 2 3 1
170		eqid 2422	. . . . . 6 |- ; 4 9 = ; 4 9
171		7nn0 10892	. . . . . . 7 |- 7 e. NN0
172		7p1e8 10740	. . . . . . 7 |- ( 7 + 1 ) = 8
173		eqid 2422	. . . . . . . 8 |- ; 2 3 = ; 2 3
174		4p3e7 10746	. . . . . . . . 9 |- ( 4 + 3 ) = 7
175	34, 78, 174	addcomli 9826	. . . . . . . 8 |- ( 3 + 4 ) = 7
176	18, 19, 2, 173, 175	decaddi 11096	. . . . . . 7 |- (; 2 3 + 4 ) = ; 2 7
177	18, 171, 172, 176	decsuc 11075	. . . . . 6 |- ( (; 2 3 + 4 ) + 1 ) = ; 2 8
178		9p1e10 10742	. . . . . . 7 |- ( 9 + 1 ) = 10
179	127, 61, 178	addcomli 9826	. . . . . 6 |- ( 1 + 9 ) = 10
180	20, 14, 2, 10, 169, 170, 177, 179	decaddc2 11095	. . . . 5 |- (;; 2 3 1 + ; 4 9 ) = ;; 2 8 0
181	168	nn0cni 10882	. . . . . . 7 |- ; 2 8 e. CC
182	181	addid1i 9821	. . . . . 6 |- (; 2 8 + 0 ) = ; 2 8
183		eqid 2422	. . . . . . 7 |- ;; 4 9 0 = ;; 4 9 0
184	18	dec0h 11068	. . . . . . . 8 |- 2 = ; 0 2
185	97, 184	eqtri 2451	. . . . . . 7 |- ( 2 + 0 ) = ; 0 2
186	130	oveq2i 6313	. . . . . . . . 9 |- ( ( 4 x. 4 ) + ( 0 + 3 ) ) = ( ( 4 x. 4 ) + 3 )
187		4t4e16 11125	. . . . . . . . . 10 |- ( 4 x. 4 ) = ; 1 6
188		6p3e9 10753	. . . . . . . . . 10 |- ( 6 + 3 ) = 9
189	14, 48, 19, 187, 188	decaddi 11096	. . . . . . . . 9 |- ( ( 4 x. 4 ) + 3 ) = ; 1 9
190	186, 189	eqtri 2451	. . . . . . . 8 |- ( ( 4 x. 4 ) + ( 0 + 3 ) ) = ; 1 9
191		9t4e36 11149	. . . . . . . . . 10 |- ( 9 x. 4 ) = ; 3 6
192	191	oveq1i 6312	. . . . . . . . 9 |- ( ( 9 x. 4 ) + 0 ) = (; 3 6 + 0 )
193	19, 48	deccl 11066	. . . . . . . . . . 11 |- ; 3 6 e. NN0
194	193	nn0cni 10882	. . . . . . . . . 10 |- ; 3 6 e. CC
195	194	addid1i 9821	. . . . . . . . 9 |- (; 3 6 + 0 ) = ; 3 6
196	192, 195	eqtri 2451	. . . . . . . 8 |- ( ( 9 x. 4 ) + 0 ) = ; 3 6
197	2, 10, 3, 3, 170, 94, 2, 48, 19, 190, 196	decmac 11091	. . . . . . 7 |- ( (; 4 9 x. 4 ) + ( 0 + 0 ) ) = ;; 1 9 6
198	73	oveq1i 6312	. . . . . . . 8 |- ( ( 0 x. 4 ) + 2 ) = ( 0 + 2 )
199	37	addid2i 9822	. . . . . . . 8 |- ( 0 + 2 ) = 2
200	198, 199, 184	3eqtri 2455	. . . . . . 7 |- ( ( 0 x. 4 ) + 2 ) = ; 0 2
201	11, 3, 3, 18, 183, 185, 2, 18, 3, 197, 200	decmac 11091	. . . . . 6 |- ( (;; 4 9 0 x. 4 ) + ( 2 + 0 ) ) = ;;; 1 9 6 2
202	12	nn0cni 10882	. . . . . . . . 9 |- ;; 4 9 0 e. CC
203	202	mul01i 9824	. . . . . . . 8 |- (;; 4 9 0 x. 0 ) = 0
204	203	oveq1i 6312	. . . . . . 7 |- ( (;; 4 9 0 x. 0 ) + 8 ) = ( 0 + 8 )
205	70	addid2i 9822	. . . . . . 7 |- ( 0 + 8 ) = 8
206	111	dec0h 11068	. . . . . . 7 |- 8 = ; 0 8
207	204, 205, 206	3eqtri 2455	. . . . . 6 |- ( (;; 4 9 0 x. 0 ) + 8 ) = ; 0 8
208	2, 3, 18, 111, 57, 182, 12, 111, 3, 201, 207	decma2c 11092	. . . . 5 |- ( (;; 4 9 0 x. ; 4 0 ) + (; 2 8 + 0 ) ) = ;;;; 1 9 6 2 8
209	203	oveq1i 6312	. . . . . 6 |- ( (;; 4 9 0 x. 0 ) + 0 ) = ( 0 + 0 )
210	209, 55, 39	3eqtri 2455	. . . . 5 |- ( (;; 4 9 0 x. 0 ) + 0 ) = ; 0 0
211	4, 3, 168, 3, 50, 180, 12, 3, 3, 208, 210	decma2c 11092	. . . 4 |- ( (;; 4 9 0 x. ;; 4 0 0 ) + (;; 2 3 1 + ; 4 9 ) ) = ;;;;; 1 9 6 2 8 0
212	34	mulid1i 9646	. . . . . . . 8 |- ( 4 x. 1 ) = 4
213	212, 55	oveq12i 6314	. . . . . . 7 |- ( ( 4 x. 1 ) + ( 0 + 0 ) ) = ( 4 + 0 )
214	213, 35	eqtri 2451	. . . . . 6 |- ( ( 4 x. 1 ) + ( 0 + 0 ) ) = 4
215	127	mulid1i 9646	. . . . . . . 8 |- ( 9 x. 1 ) = 9
216	215	oveq1i 6312	. . . . . . 7 |- ( ( 9 x. 1 ) + 0 ) = ( 9 + 0 )
217	127	addid1i 9821	. . . . . . 7 |- ( 9 + 0 ) = 9
218	10	dec0h 11068	. . . . . . 7 |- 9 = ; 0 9
219	216, 217, 218	3eqtri 2455	. . . . . 6 |- ( ( 9 x. 1 ) + 0 ) = ; 0 9
220	2, 10, 3, 3, 170, 94, 14, 10, 3, 214, 219	decmac 11091	. . . . 5 |- ( (; 4 9 x. 1 ) + ( 0 + 0 ) ) = ; 4 9
221	99	oveq1i 6312	. . . . . 6 |- ( ( 0 x. 1 ) + 1 ) = ( 0 + 1 )
222	221, 65, 63	3eqtri 2455	. . . . 5 |- ( ( 0 x. 1 ) + 1 ) = ; 0 1
223	11, 3, 3, 14, 183, 63, 14, 14, 3, 220, 222	decmac 11091	. . . 4 |- ( (;; 4 9 0 x. 1 ) + 1 ) = ;; 4 9 1
224	5, 14, 21, 14, 1, 167, 12, 14, 11, 211, 223	decma2c 11092	. . 3 |- ( (;; 4 9 0 x. N ) + ;;; 2 3 1 1 ) = ;;;;;; 1 9 6 2 8 0 1
225	15	nn0cni 10882	. . . . . . 7 |- ; 1 4 e. CC
226	225	addid1i 9821	. . . . . 6 |- (; 1 4 + 0 ) = ; 1 4
227		5nn0 10890	. . . . . . . 8 |- 5 e. NN0
228	227, 48	deccl 11066	. . . . . . 7 |- ; 5 6 e. NN0
229	228, 3	deccl 11066	. . . . . 6 |- ;; 5 6 0 e. NN0
230		eqid 2422	. . . . . . . 8 |- ;; 5 6 0 = ;; 5 6 0
231	228	nn0cni 10882	. . . . . . . . 9 |- ; 5 6 e. CC
232	231	addid2i 9822	. . . . . . . 8 |- ( 0 + ; 5 6 ) = ; 5 6
233	3, 14, 228, 3, 63, 230, 232, 62	decadd 11093	. . . . . . 7 |- ( 1 + ;; 5 6 0 ) = ;; 5 6 1
234	231	addid1i 9821	. . . . . . . 8 |- (; 5 6 + 0 ) = ; 5 6
235		5cn 10690	. . . . . . . . . . 11 |- 5 e. CC
236	235	addid1i 9821	. . . . . . . . . 10 |- ( 5 + 0 ) = 5
237	227	dec0h 11068	. . . . . . . . . 10 |- 5 = ; 0 5
238	236, 237	eqtri 2451	. . . . . . . . 9 |- ( 5 + 0 ) = ; 0 5
239	61	mulid1i 9646	. . . . . . . . . . 11 |- ( 1 x. 1 ) = 1
240	239, 55	oveq12i 6314	. . . . . . . . . 10 |- ( ( 1 x. 1 ) + ( 0 + 0 ) ) = ( 1 + 0 )
241	240, 62	eqtri 2451	. . . . . . . . 9 |- ( ( 1 x. 1 ) + ( 0 + 0 ) ) = 1
242	212	oveq1i 6312	. . . . . . . . . 10 |- ( ( 4 x. 1 ) + 5 ) = ( 4 + 5 )
243		5p4e9 10750	. . . . . . . . . . 11 |- ( 5 + 4 ) = 9
244	235, 34, 243	addcomli 9826	. . . . . . . . . 10 |- ( 4 + 5 ) = 9
245	242, 244, 218	3eqtri 2455	. . . . . . . . 9 |- ( ( 4 x. 1 ) + 5 ) = ; 0 9
246	14, 2, 3, 227, 52, 238, 14, 10, 3, 241, 245	decmac 11091	. . . . . . . 8 |- ( (; 1 4 x. 1 ) + ( 5 + 0 ) ) = ; 1 9
247	99	oveq1i 6312	. . . . . . . . 9 |- ( ( 0 x. 1 ) + 6 ) = ( 0 + 6 )
248	247, 87, 88	3eqtri 2455	. . . . . . . 8 |- ( ( 0 x. 1 ) + 6 ) = ; 0 6
249	15, 3, 227, 48, 51, 234, 14, 48, 3, 246, 248	decmac 11091	. . . . . . 7 |- ( (;; 1 4 0 x. 1 ) + (; 5 6 + 0 ) ) = ;; 1 9 6
250	239	oveq1i 6312	. . . . . . . 8 |- ( ( 1 x. 1 ) + 1 ) = ( 1 + 1 )
251	250, 135, 184	3eqtri 2455	. . . . . . 7 |- ( ( 1 x. 1 ) + 1 ) = ; 0 2
252	16, 14, 228, 14, 47, 233, 14, 18, 3, 249, 251	decmac 11091	. . . . . 6 |- ( (;;; 1 4 0 1 x. 1 ) + ( 1 + ;; 5 6 0 ) ) = ;;; 1 9 6 2
253	34	mulid2i 9647	. . . . . . . . . . 11 |- ( 1 x. 4 ) = 4
254	253, 65	oveq12i 6314	. . . . . . . . . 10 |- ( ( 1 x. 4 ) + ( 0 + 1 ) ) = ( 4 + 1 )
255		4p1e5 10737	. . . . . . . . . 10 |- ( 4 + 1 ) = 5
256	254, 255	eqtri 2451	. . . . . . . . 9 |- ( ( 1 x. 4 ) + ( 0 + 1 ) ) = 5
257	187	oveq1i 6312	. . . . . . . . . 10 |- ( ( 4 x. 4 ) + 0 ) = (; 1 6 + 0 )
258	257, 59	eqtri 2451	. . . . . . . . 9 |- ( ( 4 x. 4 ) + 0 ) = ; 1 6
259	14, 2, 3, 3, 52, 94, 2, 48, 14, 256, 258	decmac 11091	. . . . . . . 8 |- ( (; 1 4 x. 4 ) + ( 0 + 0 ) ) = ; 5 6
260	73	oveq1i 6312	. . . . . . . . 9 |- ( ( 0 x. 4 ) + 0 ) = ( 0 + 0 )
261	260, 55, 39	3eqtri 2455	. . . . . . . 8 |- ( ( 0 x. 4 ) + 0 ) = ; 0 0
262	15, 3, 3, 3, 51, 94, 2, 3, 3, 259, 261	decmac 11091	. . . . . . 7 |- ( (;; 1 4 0 x. 4 ) + ( 0 + 0 ) ) = ;; 5 6 0
263	253	oveq1i 6312	. . . . . . . 8 |- ( ( 1 x. 4 ) + 4 ) = ( 4 + 4 )
264		4p4e8 10747	. . . . . . . 8 |- ( 4 + 4 ) = 8
265	263, 264, 206	3eqtri 2455	. . . . . . 7 |- ( ( 1 x. 4 ) + 4 ) = ; 0 8
266	16, 14, 3, 2, 47, 106, 2, 111, 3, 262, 265	decmac 11091	. . . . . 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 11092	. . . . 5 |- ( (;;; 1 4 0 1 x. ; 1 4 ) + (; 1 4 + 0 ) ) = ;;;; 1 9 6 2 8
268	17	nn0cni 10882	. . . . . . . 8 |- ;;; 1 4 0 1 e. CC
269	268	mul01i 9824	. . . . . . 7 |- (;;; 1 4 0 1 x. 0 ) = 0
270	269	oveq1i 6312	. . . . . 6 |- ( (;;; 1 4 0 1 x. 0 ) + 0 ) = ( 0 + 0 )
271	270, 55, 39	3eqtri 2455	. . . . 5 |- ( (;;; 1 4 0 1 x. 0 ) + 0 ) = ; 0 0
272	15, 3, 15, 3, 51, 51, 17, 3, 3, 267, 271	decma2c 11092	. . . 4 |- ( (;;; 1 4 0 1 x. ;; 1 4 0 ) + ;; 1 4 0 ) = ;;;;; 1 9 6 2 8 0
273	268	mulid1i 9646	. . . 4 |- (;;; 1 4 0 1 x. 1 ) = ;;; 1 4 0 1
274	17, 16, 14, 47, 14, 16, 272, 273	decmul2c 11100	. . 3 |- (;;; 1 4 0 1 x. ;;; 1 4 0 1 ) = ;;;;;; 1 9 6 2 8 0 1
275	224, 274	eqtr4i 2454	. 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 15029	1 |- ( ( 2 ^;; 8 0 0 ) mod N ) = (;;; 2 3 1 1 mod N )

Syntax hints:   = wceq 1437  (class class class)co 6302   0cc0 9540   1c1 9541   + caddc 9543   x. cmul 9545   NNcn 10610   2c2 10660   3c3 10661   4c4 10662   5c5 10663   6c6 10664   7c7 10665   8c8 10666   9c9 10667   10c10 10668  ;cdc 11052   mod cmo 12096   ^cexp 12272

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4552  ax-pow 4599  ax-pr 4657  ax-un 6594  ax-cnex 9596  ax-resscn 9597  ax-1cn 9598  ax-icn 9599  ax-addcl 9600  ax-addrcl 9601  ax-mulcl 9602  ax-mulrcl 9603  ax-mulcom 9604  ax-addass 9605  ax-mulass 9606  ax-distr 9607  ax-i2m1 9608  ax-1ne0 9609  ax-1rid 9610  ax-rnegex 9611  ax-rrecex 9612  ax-cnre 9613  ax-pre-lttri 9614  ax-pre-lttrn 9615  ax-pre-ltadd 9616  ax-pre-mulgt0 9617  ax-pre-sup 9618

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-nel 2621  df-ral 2780  df-rex 2781  df-reu 2782  df-rmo 2783  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-tp 4001  df-op 4003  df-uni 4217  df-iun 4298  df-br 4421  df-opab 4480  df-mpt 4481  df-tr 4516  df-eprel 4761  df-id 4765  df-po 4771  df-so 4772  df-fr 4809  df-we 4811  df-xp 4856  df-rel 4857  df-cnv 4858  df-co 4859  df-dm 4860  df-rn 4861  df-res 4862  df-ima 4863  df-pred 5396  df-ord 5442  df-on 5443  df-lim 5444  df-suc 5445  df-iota 5562  df-fun 5600  df-fn 5601  df-f 5602  df-f1 5603  df-fo 5604  df-f1o 5605  df-fv 5606  df-riota 6264  df-ov 6305  df-oprab 6306  df-mpt2 6307  df-om 6704  df-2nd 6805  df-wrecs 7033  df-recs 7095  df-rdg 7133  df-er 7368  df-en 7575  df-dom 7576  df-sdom 7577  df-sup 7959  df-inf 7960  df-pnf 9678  df-mnf 9679  df-xr 9680  df-ltxr 9681  df-le 9682  df-sub 9863  df-neg 9864  df-div 10271  df-nn 10611  df-2 10669  df-3 10670  df-4 10671  df-5 10672  df-6 10673  df-7 10674  df-8 10675  df-9 10676  df-10 10677  df-n0 10871  df-z 10939  df-dec 11053  df-uz 11161  df-rp 11304  df-fl 12028  df-mod 12097  df-seq 12214  df-exp 12273

This theorem is referenced by:  4001lem3  15102  4001lem4  15103