Theorem 4001lem1 14497

Description: Lemma for 4001prm 14501. 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

Step	Hyp	Ref	Expression
1		4001prm.1	. . 3 |- N = ;;; 4 0 0 1
2		4nn0 10817	. . . . . 6 |- 4 e. NN0
3		0nn0 10813	. . . . . 6 |- 0 e. NN0
4	2, 3	deccl 10995	. . . . 5 |- ; 4 0 e. NN0
5	4, 3	deccl 10995	. . . 4 |- ;; 4 0 0 e. NN0
6		1nn 10550	. . . 4 |- 1 e. NN
7	5, 6	decnncl 10994	. . 3 |- ;;; 4 0 0 1 e. NN
8	1, 7	eqeltri 2525	. 2 |- N e. NN
9		2nn 10696	. 2 |- 2 e. NN
10		10nn0 10823	. . 3 |- 10 e. NN0
11	10, 3	deccl 10995	. 2 |- ; 10 0 e. NN0
12		9nn0 10822	. . . 4 |- 9 e. NN0
13	12, 2	deccl 10995	. . 3 |- ; 9 4 e. NN0
14	13	nn0zi 10892	. 2 |- ; 9 4 e. ZZ
15		6nn0 10819	. . . 4 |- 6 e. NN0
16		1nn0 10814	. . . 4 |- 1 e. NN0
17	15, 16	deccl 10995	. . 3 |- ; 6 1 e. NN0
18	17, 2	deccl 10995	. 2 |- ;; 6 1 4 e. NN0
19	12, 3	deccl 10995	. . 3 |- ; 9 0 e. NN0
20		2nn0 10815	. . 3 |- 2 e. NN0
21	19, 20	deccl 10995	. 2 |- ;; 9 0 2 e. NN0
22		5nn0 10818	. . . 4 |- 5 e. NN0
23	22, 3	deccl 10995	. . 3 |- ; 5 0 e. NN0
24		8nn0 10821	. . . . . 6 |- 8 e. NN0
25	20, 24	deccl 10995	. . . . 5 |- ; 2 8 e. NN0
26	25, 15	deccl 10995	. . . 4 |- ;; 2 8 6 e. NN0
27	26	nn0zi 10892	. . 3 |- ;; 2 8 6 e. ZZ
28		7nn0 10820	. . . . 5 |- 7 e. NN0
29	10, 28	deccl 10995	. . . 4 |- ; 10 7 e. NN0
30	29, 3	deccl 10995	. . 3 |- ;; 10 7 0 e. NN0
31	20, 22	deccl 10995	. . . 4 |- ; 2 5 e. NN0
32	10, 2	deccl 10995	. . . . . 6 |- ; 10 4 e. NN0
33	32, 15	deccl 10995	. . . . 5 |- ;; 10 4 6 e. NN0
34	33	nn0zi 10892	. . . 4 |- ;; 10 4 6 e. ZZ
35	20, 3	deccl 10995	. . . . . 6 |- ; 2 0 e. NN0
36	35, 2	deccl 10995	. . . . 5 |- ;; 2 0 4 e. NN0
37	36, 15	deccl 10995	. . . 4 |- ;;; 2 0 4 6 e. NN0
38	20, 2	deccl 10995	. . . . 5 |- ; 2 4 e. NN0
39		0z 10878	. . . . 5 |- 0 e. ZZ
40	10, 20	deccl 10995	. . . . . 6 |- ; 10 2 e. NN0
41		3nn0 10816	. . . . . 6 |- 3 e. NN0
42	40, 41	deccl 10995	. . . . 5 |- ;; 10 2 3 e. NN0
43	16, 20	deccl 10995	. . . . . 6 |- ; 1 2 e. NN0
44		2z 10899	. . . . . 6 |- 2 e. ZZ
45	12, 22	deccl 10995	. . . . . 6 |- ; 9 5 e. NN0
46		1z 10897	. . . . . . 7 |- 1 e. ZZ
47	15, 2	deccl 10995	. . . . . . 7 |- ; 6 4 e. NN0
48		2exp6 14446	. . . . . . . 8 |- ( 2 ^ 6 ) = ; 6 4
49	48	oveq1i 6288	. . . . . . 7 |- ( ( 2 ^ 6 ) mod N ) = (; 6 4 mod N )
50		6cn 10620	. . . . . . . 8 |- 6 e. CC
51		2cn 10609	. . . . . . . 8 |- 2 e. CC
52		6t2e12 11058	. . . . . . . 8 |- ( 6 x. 2 ) = ; 1 2
53	50, 51, 52	mulcomli 9603	. . . . . . 7 |- ( 2 x. 6 ) = ; 1 2
54		eqid 2441	. . . . . . . . 9 |- ; 9 5 = ; 9 5
55		eqid 2441	. . . . . . . . . 10 |- ;; 4 0 0 = ;; 4 0 0
56		9cn 10626	. . . . . . . . . . . 12 |- 9 e. CC
57	56	addid1i 9767	. . . . . . . . . . 11 |- ( 9 + 0 ) = 9
58	12	dec0h 10997	. . . . . . . . . . 11 |- 9 = ; 0 9
59	57, 58	eqtri 2470	. . . . . . . . . 10 |- ( 9 + 0 ) = ; 0 9
60		eqid 2441	. . . . . . . . . . 11 |- ; 4 0 = ; 4 0
61		00id 9755	. . . . . . . . . . . 12 |- ( 0 + 0 ) = 0
62	3	dec0h 10997	. . . . . . . . . . . 12 |- 0 = ; 0 0
63	61, 62	eqtri 2470	. . . . . . . . . . 11 |- ( 0 + 0 ) = ; 0 0
64		4cn 10616	. . . . . . . . . . . . . 14 |- 4 e. CC
65	64	mulid2i 9599	. . . . . . . . . . . . 13 |- ( 1 x. 4 ) = 4
66	65, 61	oveq12i 6290	. . . . . . . . . . . 12 |- ( ( 1 x. 4 ) + ( 0 + 0 ) ) = ( 4 + 0 )
67	64	addid1i 9767	. . . . . . . . . . . 12 |- ( 4 + 0 ) = 4
68	66, 67	eqtri 2470	. . . . . . . . . . 11 |- ( ( 1 x. 4 ) + ( 0 + 0 ) ) = 4
69		ax-1cn 9550	. . . . . . . . . . . . . 14 |- 1 e. CC
70	69	mul01i 9770	. . . . . . . . . . . . 13 |- ( 1 x. 0 ) = 0
71	70	oveq1i 6288	. . . . . . . . . . . 12 |- ( ( 1 x. 0 ) + 0 ) = ( 0 + 0 )
72	71, 63	eqtri 2470	. . . . . . . . . . 11 |- ( ( 1 x. 0 ) + 0 ) = ; 0 0
73	2, 3, 3, 3, 60, 63, 16, 3, 3, 68, 72	decma2c 11021	. . . . . . . . . 10 |- ( ( 1 x. ; 4 0 ) + ( 0 + 0 ) ) = ; 4 0
74	70	oveq1i 6288	. . . . . . . . . . 11 |- ( ( 1 x. 0 ) + 9 ) = ( 0 + 9 )
75	56	addid2i 9768	. . . . . . . . . . . 12 |- ( 0 + 9 ) = 9
76	75, 58	eqtri 2470	. . . . . . . . . . 11 |- ( 0 + 9 ) = ; 0 9
77	74, 76	eqtri 2470	. . . . . . . . . 10 |- ( ( 1 x. 0 ) + 9 ) = ; 0 9
78	4, 3, 3, 12, 55, 59, 16, 12, 3, 73, 77	decma2c 11021	. . . . . . . . 9 |- ( ( 1 x. ;; 4 0 0 ) + ( 9 + 0 ) ) = ;; 4 0 9
79	69	mulid1i 9598	. . . . . . . . . . 11 |- ( 1 x. 1 ) = 1
80	79	oveq1i 6288	. . . . . . . . . 10 |- ( ( 1 x. 1 ) + 5 ) = ( 1 + 5 )
81		5cn 10618	. . . . . . . . . . . 12 |- 5 e. CC
82		5p1e6 10666	. . . . . . . . . . . 12 |- ( 5 + 1 ) = 6
83	81, 69, 82	addcomli 9772	. . . . . . . . . . 11 |- ( 1 + 5 ) = 6
84	15	dec0h 10997	. . . . . . . . . . 11 |- 6 = ; 0 6
85	83, 84	eqtri 2470	. . . . . . . . . 10 |- ( 1 + 5 ) = ; 0 6
86	80, 85	eqtri 2470	. . . . . . . . 9 |- ( ( 1 x. 1 ) + 5 ) = ; 0 6
87	5, 16, 12, 22, 1, 54, 16, 15, 3, 78, 86	decma2c 11021	. . . . . . . 8 |- ( ( 1 x. N ) + ; 9 5 ) = ;;; 4 0 9 6
88		eqid 2441	. . . . . . . . 9 |- ; 6 4 = ; 6 4
89		eqid 2441	. . . . . . . . . 10 |- ; 2 5 = ; 2 5
90		2p2e4 10656	. . . . . . . . . . . 12 |- ( 2 + 2 ) = 4
91	90	oveq2i 6289	. . . . . . . . . . 11 |- ( ( 6 x. 6 ) + ( 2 + 2 ) ) = ( ( 6 x. 6 ) + 4 )
92		6t6e36 11062	. . . . . . . . . . . 12 |- ( 6 x. 6 ) = ; 3 6
93		3p1e4 10664	. . . . . . . . . . . 12 |- ( 3 + 1 ) = 4
94		6p4e10 10682	. . . . . . . . . . . 12 |- ( 6 + 4 ) = 10
95	41, 15, 2, 92, 93, 94	decaddci2 11027	. . . . . . . . . . 11 |- ( ( 6 x. 6 ) + 4 ) = ; 4 0
96	91, 95	eqtri 2470	. . . . . . . . . 10 |- ( ( 6 x. 6 ) + ( 2 + 2 ) ) = ; 4 0
97		6t4e24 11060	. . . . . . . . . . . 12 |- ( 6 x. 4 ) = ; 2 4
98	50, 64, 97	mulcomli 9603	. . . . . . . . . . 11 |- ( 4 x. 6 ) = ; 2 4
99		5p4e9 10678	. . . . . . . . . . . 12 |- ( 5 + 4 ) = 9
100	81, 64, 99	addcomli 9772	. . . . . . . . . . 11 |- ( 4 + 5 ) = 9
101	20, 2, 22, 98, 100	decaddi 11025	. . . . . . . . . 10 |- ( ( 4 x. 6 ) + 5 ) = ; 2 9
102	15, 2, 20, 22, 88, 89, 15, 12, 20, 96, 101	decmac 11020	. . . . . . . . 9 |- ( (; 6 4 x. 6 ) + ; 2 5 ) = ;; 4 0 9
103		4p1e5 10665	. . . . . . . . . . 11 |- ( 4 + 1 ) = 5
104	20, 2, 103, 97	decsuc 11004	. . . . . . . . . 10 |- ( ( 6 x. 4 ) + 1 ) = ; 2 5
105		4t4e16 11054	. . . . . . . . . 10 |- ( 4 x. 4 ) = ; 1 6
106	2, 15, 2, 88, 15, 16, 104, 105	decmul1c 11028	. . . . . . . . 9 |- (; 6 4 x. 4 ) = ;; 2 5 6
107	47, 15, 2, 88, 15, 31, 102, 106	decmul2c 11029	. . . . . . . 8 |- (; 6 4 x. ; 6 4 ) = ;;; 4 0 9 6
108	87, 107	eqtr4i 2473	. . . . . . 7 |- ( ( 1 x. N ) + ; 9 5 ) = (; 6 4 x. ; 6 4 )
109	8, 9, 15, 46, 47, 45, 49, 53, 108	mod2xi 14429	. . . . . 6 |- ( ( 2 ^; 1 2 ) mod N ) = (; 9 5 mod N )
110		eqid 2441	. . . . . . 7 |- ; 1 2 = ; 1 2
111	51	mulid1i 9598	. . . . . . . . 9 |- ( 2 x. 1 ) = 2
112	111	oveq1i 6288	. . . . . . . 8 |- ( ( 2 x. 1 ) + 0 ) = ( 2 + 0 )
113	51	addid1i 9767	. . . . . . . 8 |- ( 2 + 0 ) = 2
114	112, 113	eqtri 2470	. . . . . . 7 |- ( ( 2 x. 1 ) + 0 ) = 2
115		2t2e4 10688	. . . . . . . 8 |- ( 2 x. 2 ) = 4
116	2	dec0h 10997	. . . . . . . 8 |- 4 = ; 0 4
117	115, 116	eqtri 2470	. . . . . . 7 |- ( 2 x. 2 ) = ; 0 4
118	20, 16, 20, 110, 2, 3, 114, 117	decmul2c 11029	. . . . . 6 |- ( 2 x. ; 1 2 ) = ; 2 4
119		eqid 2441	. . . . . . . 8 |- ;; 10 2 3 = ;; 10 2 3
120	40	nn0cni 10810	. . . . . . . . . 10 |- ; 10 2 e. CC
121	120	addid1i 9767	. . . . . . . . 9 |- (; 10 2 + 0 ) = ; 10 2
122		dec10p 11010	. . . . . . . . . 10 |- ( 10 + 0 ) = ; 1 0
123		4t2e8 10692	. . . . . . . . . . . . 13 |- ( 4 x. 2 ) = 8
124	64, 51, 123	mulcomli 9603	. . . . . . . . . . . 12 |- ( 2 x. 4 ) = 8
125	69	addid1i 9767	. . . . . . . . . . . 12 |- ( 1 + 0 ) = 1
126	124, 125	oveq12i 6290	. . . . . . . . . . 11 |- ( ( 2 x. 4 ) + ( 1 + 0 ) ) = ( 8 + 1 )
127		8p1e9 10669	. . . . . . . . . . 11 |- ( 8 + 1 ) = 9
128	126, 127	eqtri 2470	. . . . . . . . . 10 |- ( ( 2 x. 4 ) + ( 1 + 0 ) ) = 9
129	51	mul01i 9770	. . . . . . . . . . . 12 |- ( 2 x. 0 ) = 0
130	129	oveq1i 6288	. . . . . . . . . . 11 |- ( ( 2 x. 0 ) + 0 ) = ( 0 + 0 )
131	130, 63	eqtri 2470	. . . . . . . . . 10 |- ( ( 2 x. 0 ) + 0 ) = ; 0 0
132	2, 3, 16, 3, 60, 122, 20, 3, 3, 128, 131	decma2c 11021	. . . . . . . . 9 |- ( ( 2 x. ; 4 0 ) + ( 10 + 0 ) ) = ; 9 0
133	129	oveq1i 6288	. . . . . . . . . 10 |- ( ( 2 x. 0 ) + 2 ) = ( 0 + 2 )
134	51	addid2i 9768	. . . . . . . . . . 11 |- ( 0 + 2 ) = 2
135	20	dec0h 10997	. . . . . . . . . . 11 |- 2 = ; 0 2
136	134, 135	eqtri 2470	. . . . . . . . . 10 |- ( 0 + 2 ) = ; 0 2
137	133, 136	eqtri 2470	. . . . . . . . 9 |- ( ( 2 x. 0 ) + 2 ) = ; 0 2
138	4, 3, 10, 20, 55, 121, 20, 20, 3, 132, 137	decma2c 11021	. . . . . . . 8 |- ( ( 2 x. ;; 4 0 0 ) + (; 10 2 + 0 ) ) = ;; 9 0 2
139	111	oveq1i 6288	. . . . . . . . 9 |- ( ( 2 x. 1 ) + 3 ) = ( 2 + 3 )
140		3cn 10613	. . . . . . . . . . 11 |- 3 e. CC
141		3p2e5 10671	. . . . . . . . . . 11 |- ( 3 + 2 ) = 5
142	140, 51, 141	addcomli 9772	. . . . . . . . . 10 |- ( 2 + 3 ) = 5
143	22	dec0h 10997	. . . . . . . . . 10 |- 5 = ; 0 5
144	142, 143	eqtri 2470	. . . . . . . . 9 |- ( 2 + 3 ) = ; 0 5
145	139, 144	eqtri 2470	. . . . . . . 8 |- ( ( 2 x. 1 ) + 3 ) = ; 0 5
146	5, 16, 40, 41, 1, 119, 20, 22, 3, 138, 145	decma2c 11021	. . . . . . 7 |- ( ( 2 x. N ) + ;; 10 2 3 ) = ;;; 9 0 2 5
147	2, 28	deccl 10995	. . . . . . . 8 |- ; 4 7 e. NN0
148		eqid 2441	. . . . . . . . 9 |- ; 4 7 = ; 4 7
149	100	oveq2i 6289	. . . . . . . . . 10 |- ( ( 9 x. 9 ) + ( 4 + 5 ) ) = ( ( 9 x. 9 ) + 9 )
150		9t9e81 11083	. . . . . . . . . . 11 |- ( 9 x. 9 ) = ; 8 1
151		9p1e10 10670	. . . . . . . . . . . 12 |- ( 9 + 1 ) = 10
152	56, 69, 151	addcomli 9772	. . . . . . . . . . 11 |- ( 1 + 9 ) = 10
153	24, 16, 12, 150, 127, 152	decaddci2 11027	. . . . . . . . . 10 |- ( ( 9 x. 9 ) + 9 ) = ; 9 0
154	149, 153	eqtri 2470	. . . . . . . . 9 |- ( ( 9 x. 9 ) + ( 4 + 5 ) ) = ; 9 0
155		9t5e45 11079	. . . . . . . . . . 11 |- ( 9 x. 5 ) = ; 4 5
156	56, 81, 155	mulcomli 9603	. . . . . . . . . 10 |- ( 5 x. 9 ) = ; 4 5
157		7cn 10622	. . . . . . . . . . 11 |- 7 e. CC
158		7p5e12 11034	. . . . . . . . . . 11 |- ( 7 + 5 ) = ; 1 2
159	157, 81, 158	addcomli 9772	. . . . . . . . . 10 |- ( 5 + 7 ) = ; 1 2
160	2, 22, 28, 156, 103, 20, 159	decaddci 11026	. . . . . . . . 9 |- ( ( 5 x. 9 ) + 7 ) = ; 5 2
161	12, 22, 2, 28, 54, 148, 12, 20, 22, 154, 160	decmac 11020	. . . . . . . 8 |- ( (; 9 5 x. 9 ) + ; 4 7 ) = ;; 9 0 2
162		5p2e7 10676	. . . . . . . . . 10 |- ( 5 + 2 ) = 7
163	2, 22, 20, 155, 162	decaddi 11025	. . . . . . . . 9 |- ( ( 9 x. 5 ) + 2 ) = ; 4 7
164		5t5e25 11057	. . . . . . . . 9 |- ( 5 x. 5 ) = ; 2 5
165	22, 12, 22, 54, 22, 20, 163, 164	decmul1c 11028	. . . . . . . 8 |- (; 9 5 x. 5 ) = ;; 4 7 5
166	45, 12, 22, 54, 22, 147, 161, 165	decmul2c 11029	. . . . . . 7 |- (; 9 5 x. ; 9 5 ) = ;;; 9 0 2 5
167	146, 166	eqtr4i 2473	. . . . . 6 |- ( ( 2 x. N ) + ;; 10 2 3 ) = (; 9 5 x. ; 9 5 )
168	8, 9, 43, 44, 45, 42, 109, 118, 167	mod2xi 14429	. . . . 5 |- ( ( 2 ^; 2 4 ) mod N ) = (;; 10 2 3 mod N )
169		eqid 2441	. . . . . 6 |- ; 2 4 = ; 2 4
170	20, 2, 103, 169	decsuc 11004	. . . . 5 |- (; 2 4 + 1 ) = ; 2 5
171	37	nn0cni 10810	. . . . . . 7 |- ;;; 2 0 4 6 e. CC
172	171	addid2i 9768	. . . . . 6 |- ( 0 + ;;; 2 0 4 6 ) = ;;; 2 0 4 6
173	8	nncni 10549	. . . . . . . 8 |- N e. CC
174	173	mul02i 9769	. . . . . . 7 |- ( 0 x. N ) = 0
175	174	oveq1i 6288	. . . . . 6 |- ( ( 0 x. N ) + ;;; 2 0 4 6 ) = ( 0 + ;;; 2 0 4 6 )
176		eqid 2441	. . . . . . . . . 10 |- ; 10 2 = ; 10 2
177	20	dec0u 10996	. . . . . . . . . . . 12 |- ( 10 x. 2 ) = ; 2 0
178	177	oveq1i 6288	. . . . . . . . . . 11 |- ( ( 10 x. 2 ) + 0 ) = (; 2 0 + 0 )
179	35	nn0cni 10810	. . . . . . . . . . . 12 |- ; 2 0 e. CC
180	179	addid1i 9767	. . . . . . . . . . 11 |- (; 2 0 + 0 ) = ; 2 0
181	178, 180	eqtri 2470	. . . . . . . . . 10 |- ( ( 10 x. 2 ) + 0 ) = ; 2 0
182	20, 10, 20, 176, 2, 3, 181, 117	decmul1c 11028	. . . . . . . . 9 |- (; 10 2 x. 2 ) = ;; 2 0 4
183	182	oveq1i 6288	. . . . . . . 8 |- ( (; 10 2 x. 2 ) + 0 ) = (;; 2 0 4 + 0 )
184	36	nn0cni 10810	. . . . . . . . 9 |- ;; 2 0 4 e. CC
185	184	addid1i 9767	. . . . . . . 8 |- (;; 2 0 4 + 0 ) = ;; 2 0 4
186	183, 185	eqtri 2470	. . . . . . 7 |- ( (; 10 2 x. 2 ) + 0 ) = ;; 2 0 4
187		3t2e6 10690	. . . . . . . 8 |- ( 3 x. 2 ) = 6
188	187, 84	eqtri 2470	. . . . . . 7 |- ( 3 x. 2 ) = ; 0 6
189	20, 40, 41, 119, 15, 3, 186, 188	decmul1c 11028	. . . . . 6 |- (;; 10 2 3 x. 2 ) = ;;; 2 0 4 6
190	172, 175, 189	3eqtr4i 2480	. . . . 5 |- ( ( 0 x. N ) + ;;; 2 0 4 6 ) = (;; 10 2 3 x. 2 )
191	8, 9, 38, 39, 42, 37, 168, 170, 190	modxp1i 14430	. . . 4 |- ( ( 2 ^; 2 5 ) mod N ) = (;;; 2 0 4 6 mod N )
192	115	oveq1i 6288	. . . . . 6 |- ( ( 2 x. 2 ) + 1 ) = ( 4 + 1 )
193	192, 103	eqtri 2470	. . . . 5 |- ( ( 2 x. 2 ) + 1 ) = 5
194		5t2e10 10693	. . . . . . 7 |- ( 5 x. 2 ) = 10
195	81, 51, 194	mulcomli 9603	. . . . . 6 |- ( 2 x. 5 ) = 10
196		dec10 11011	. . . . . 6 |- 10 = ; 1 0
197	195, 196	eqtri 2470	. . . . 5 |- ( 2 x. 5 ) = ; 1 0
198	20, 20, 22, 89, 3, 16, 193, 197	decmul2c 11029	. . . 4 |- ( 2 x. ; 2 5 ) = ; 5 0
199		eqid 2441	. . . . . 6 |- ;; 10 7 0 = ;; 10 7 0
200	20, 16	deccl 10995	. . . . . . 7 |- ; 2 1 e. NN0
201		eqid 2441	. . . . . . . 8 |- ; 10 7 = ; 10 7
202		eqid 2441	. . . . . . . 8 |- ; 10 4 = ; 10 4
203		0p1e1 10650	. . . . . . . . 9 |- ( 0 + 1 ) = 1
204		10p10e20 11051	. . . . . . . . 9 |- ( 10 + 10 ) = ; 2 0
205	20, 3, 203, 204	decsuc 11004	. . . . . . . 8 |- ( ( 10 + 10 ) + 1 ) = ; 2 1
206		7p4e11 11033	. . . . . . . 8 |- ( 7 + 4 ) = ; 1 1
207	10, 28, 10, 2, 201, 202, 205, 16, 206	decaddc 11023	. . . . . . 7 |- (; 10 7 + ; 10 4 ) = ;; 2 1 1
208	200	nn0cni 10810	. . . . . . . . 9 |- ; 2 1 e. CC
209	208	addid1i 9767	. . . . . . . 8 |- (; 2 1 + 0 ) = ; 2 1
210		eqid 2441	. . . . . . . . 9 |- ;; 10 4 6 = ;; 10 4 6
211	113, 135	eqtri 2470	. . . . . . . . 9 |- ( 2 + 0 ) = ; 0 2
212	16	dec0h 10997	. . . . . . . . . . . 12 |- 1 = ; 0 1
213	203, 212	eqtri 2470	. . . . . . . . . . 11 |- ( 0 + 1 ) = ; 0 1
214	64	mul02i 9769	. . . . . . . . . . . . 13 |- ( 0 x. 4 ) = 0
215	214	oveq1i 6288	. . . . . . . . . . . 12 |- ( ( 0 x. 4 ) + 1 ) = ( 0 + 1 )
216	215, 213	eqtri 2470	. . . . . . . . . . 11 |- ( ( 0 x. 4 ) + 1 ) = ; 0 1
217	16, 3, 3, 16, 196, 213, 2, 16, 3, 68, 216	decmac 11020	. . . . . . . . . 10 |- ( ( 10 x. 4 ) + ( 0 + 1 ) ) = ; 4 1
218		6p2e8 10680	. . . . . . . . . . 11 |- ( 6 + 2 ) = 8
219	16, 15, 20, 105, 218	decaddi 11025	. . . . . . . . . 10 |- ( ( 4 x. 4 ) + 2 ) = ; 1 8
220	10, 2, 3, 20, 202, 136, 2, 24, 16, 217, 219	decmac 11020	. . . . . . . . 9 |- ( (; 10 4 x. 4 ) + ( 0 + 2 ) ) = ;; 4 1 8
221		4p2e6 10673	. . . . . . . . . 10 |- ( 4 + 2 ) = 6
222	20, 2, 20, 97, 221	decaddi 11025	. . . . . . . . 9 |- ( ( 6 x. 4 ) + 2 ) = ; 2 6
223	32, 15, 3, 20, 210, 211, 2, 15, 20, 220, 222	decmac 11020	. . . . . . . 8 |- ( (;; 10 4 6 x. 4 ) + ( 2 + 0 ) ) = ;;; 4 1 8 6
224	33	nn0cni 10810	. . . . . . . . . . 11 |- ;; 10 4 6 e. CC
225	224	mul01i 9770	. . . . . . . . . 10 |- (;; 10 4 6 x. 0 ) = 0
226	225	oveq1i 6288	. . . . . . . . 9 |- ( (;; 10 4 6 x. 0 ) + 1 ) = ( 0 + 1 )
227	226, 213	eqtri 2470	. . . . . . . 8 |- ( (;; 10 4 6 x. 0 ) + 1 ) = ; 0 1
228	2, 3, 20, 16, 60, 209, 33, 16, 3, 223, 227	decma2c 11021	. . . . . . 7 |- ( (;; 10 4 6 x. ; 4 0 ) + (; 2 1 + 0 ) ) = ;;;; 4 1 8 6 1
229	4, 3, 200, 16, 55, 207, 33, 16, 3, 228, 227	decma2c 11021	. . . . . 6 |- ( (;; 10 4 6 x. ;; 4 0 0 ) + (; 10 7 + ; 10 4 ) ) = ;;;;; 4 1 8 6 1 1
230	224	mulid1i 9598	. . . . . . . 8 |- (;; 10 4 6 x. 1 ) = ;; 10 4 6
231	230	oveq1i 6288	. . . . . . 7 |- ( (;; 10 4 6 x. 1 ) + 0 ) = (;; 10 4 6 + 0 )
232	224	addid1i 9767	. . . . . . 7 |- (;; 10 4 6 + 0 ) = ;; 10 4 6
233	231, 232	eqtri 2470	. . . . . 6 |- ( (;; 10 4 6 x. 1 ) + 0 ) = ;; 10 4 6
234	5, 16, 29, 3, 1, 199, 33, 15, 32, 229, 233	decma2c 11021	. . . . 5 |- ( (;; 10 4 6 x. N ) + ;; 10 7 0 ) = ;;;;;; 4 1 8 6 1 1 6
235		eqid 2441	. . . . . 6 |- ;;; 2 0 4 6 = ;;; 2 0 4 6
236	43, 20	deccl 10995	. . . . . . 7 |- ;; 1 2 2 e. NN0
237	236, 28	deccl 10995	. . . . . 6 |- ;;; 1 2 2 7 e. NN0
238		eqid 2441	. . . . . . 7 |- ;; 2 0 4 = ;; 2 0 4
239		eqid 2441	. . . . . . 7 |- ;;; 1 2 2 7 = ;;; 1 2 2 7
240	24, 16	deccl 10995	. . . . . . . 8 |- ; 8 1 e. NN0
241	240, 12	deccl 10995	. . . . . . 7 |- ;; 8 1 9 e. NN0
242		eqid 2441	. . . . . . . 8 |- ; 2 0 = ; 2 0
243		eqid 2441	. . . . . . . . 9 |- ;; 1 2 2 = ;; 1 2 2
244		eqid 2441	. . . . . . . . 9 |- ;; 8 1 9 = ;; 8 1 9
245		eqid 2441	. . . . . . . . . . 11 |- ; 8 1 = ; 8 1
246		8cn 10624	. . . . . . . . . . . 12 |- 8 e. CC
247	246, 69, 127	addcomli 9772	. . . . . . . . . . 11 |- ( 1 + 8 ) = 9
248		2p1e3 10662	. . . . . . . . . . 11 |- ( 2 + 1 ) = 3
249	16, 20, 24, 16, 110, 245, 247, 248	decadd 11022	. . . . . . . . . 10 |- (; 1 2 + ; 8 1 ) = ; 9 3
250	12, 41, 93, 249	decsuc 11004	. . . . . . . . 9 |- ( (; 1 2 + ; 8 1 ) + 1 ) = ; 9 4
251		9p2e11 11043	. . . . . . . . . 10 |- ( 9 + 2 ) = ; 1 1
252	56, 51, 251	addcomli 9772	. . . . . . . . 9 |- ( 2 + 9 ) = ; 1 1
253	43, 20, 240, 12, 243, 244, 250, 16, 252	decaddc 11023	. . . . . . . 8 |- (;; 1 2 2 + ;; 8 1 9 ) = ;; 9 4 1
254	13	nn0cni 10810	. . . . . . . . . 10 |- ; 9 4 e. CC
255	254	addid1i 9767	. . . . . . . . 9 |- (; 9 4 + 0 ) = ; 9 4
256	151, 196	eqtri 2470	. . . . . . . . . 10 |- ( 9 + 1 ) = ; 1 0
257	125, 212	eqtri 2470	. . . . . . . . . . 11 |- ( 1 + 0 ) = ; 0 1
258	115, 61	oveq12i 6290	. . . . . . . . . . . 12 |- ( ( 2 x. 2 ) + ( 0 + 0 ) ) = ( 4 + 0 )
259	258, 67	eqtri 2470	. . . . . . . . . . 11 |- ( ( 2 x. 2 ) + ( 0 + 0 ) ) = 4
260	51	mul02i 9769	. . . . . . . . . . . . 13 |- ( 0 x. 2 ) = 0
261	260	oveq1i 6288	. . . . . . . . . . . 12 |- ( ( 0 x. 2 ) + 1 ) = ( 0 + 1 )
262	261, 213	eqtri 2470	. . . . . . . . . . 11 |- ( ( 0 x. 2 ) + 1 ) = ; 0 1
263	20, 3, 3, 16, 242, 257, 20, 16, 3, 259, 262	decmac 11020	. . . . . . . . . 10 |- ( (; 2 0 x. 2 ) + ( 1 + 0 ) ) = ; 4 1
264	123	oveq1i 6288	. . . . . . . . . . 11 |- ( ( 4 x. 2 ) + 0 ) = ( 8 + 0 )
265	246	addid1i 9767	. . . . . . . . . . . 12 |- ( 8 + 0 ) = 8
266	24	dec0h 10997	. . . . . . . . . . . 12 |- 8 = ; 0 8
267	265, 266	eqtri 2470	. . . . . . . . . . 11 |- ( 8 + 0 ) = ; 0 8
268	264, 267	eqtri 2470	. . . . . . . . . 10 |- ( ( 4 x. 2 ) + 0 ) = ; 0 8
269	35, 2, 16, 3, 238, 256, 20, 24, 3, 263, 268	decmac 11020	. . . . . . . . 9 |- ( (;; 2 0 4 x. 2 ) + ( 9 + 1 ) ) = ;; 4 1 8
270	64, 51, 221	addcomli 9772	. . . . . . . . . 10 |- ( 2 + 4 ) = 6
271	16, 20, 2, 52, 270	decaddi 11025	. . . . . . . . 9 |- ( ( 6 x. 2 ) + 4 ) = ; 1 6
272	36, 15, 12, 2, 235, 255, 20, 15, 16, 269, 271	decmac 11020	. . . . . . . 8 |- ( (;;; 2 0 4 6 x. 2 ) + (; 9 4 + 0 ) ) = ;;; 4 1 8 6
273	171	mul01i 9770	. . . . . . . . . 10 |- (;;; 2 0 4 6 x. 0 ) = 0
274	273	oveq1i 6288	. . . . . . . . 9 |- ( (;;; 2 0 4 6 x. 0 ) + 1 ) = ( 0 + 1 )
275	274, 213	eqtri 2470	. . . . . . . 8 |- ( (;;; 2 0 4 6 x. 0 ) + 1 ) = ; 0 1
276	20, 3, 13, 16, 242, 253, 37, 16, 3, 272, 275	decma2c 11021	. . . . . . 7 |- ( (;;; 2 0 4 6 x. ; 2 0 ) + (;; 1 2 2 + ;; 8 1 9 ) ) = ;;;; 4 1 8 6 1
277	28	dec0h 10997	. . . . . . . 8 |- 7 = ; 0 7
278	140	addid2i 9768	. . . . . . . . . 10 |- ( 0 + 3 ) = 3
279	41	dec0h 10997	. . . . . . . . . 10 |- 3 = ; 0 3
280	278, 279	eqtri 2470	. . . . . . . . 9 |- ( 0 + 3 ) = ; 0 3
281	124, 61	oveq12i 6290	. . . . . . . . . . 11 |- ( ( 2 x. 4 ) + ( 0 + 0 ) ) = ( 8 + 0 )
282	281, 265	eqtri 2470	. . . . . . . . . 10 |- ( ( 2 x. 4 ) + ( 0 + 0 ) ) = 8
283	20, 3, 3, 16, 242, 213, 2, 16, 3, 282, 216	decmac 11020	. . . . . . . . 9 |- ( (; 2 0 x. 4 ) + ( 0 + 1 ) ) = ; 8 1
284		6p3e9 10681	. . . . . . . . . 10 |- ( 6 + 3 ) = 9
285	16, 15, 41, 105, 284	decaddi 11025	. . . . . . . . 9 |- ( ( 4 x. 4 ) + 3 ) = ; 1 9
286	35, 2, 3, 41, 238, 280, 2, 12, 16, 283, 285	decmac 11020	. . . . . . . 8 |- ( (;; 2 0 4 x. 4 ) + ( 0 + 3 ) ) = ;; 8 1 9
287	157, 64, 206	addcomli 9772	. . . . . . . . 9 |- ( 4 + 7 ) = ; 1 1
288	20, 2, 28, 97, 248, 16, 287	decaddci 11026	. . . . . . . 8 |- ( ( 6 x. 4 ) + 7 ) = ; 3 1
289	36, 15, 3, 28, 235, 277, 2, 16, 41, 286, 288	decmac 11020	. . . . . . 7 |- ( (;;; 2 0 4 6 x. 4 ) + 7 ) = ;;; 8 1 9 1
290	35, 2, 236, 28, 238, 239, 37, 16, 241, 276, 289	decma2c 11021	. . . . . 6 |- ( (;;; 2 0 4 6 x. ;; 2 0 4 ) + ;;; 1 2 2 7 ) = ;;;;; 4 1 8 6 1 1
291	53	oveq1i 6288	. . . . . . . . . 10 |- ( ( 2 x. 6 ) + 0 ) = (; 1 2 + 0 )
292	43	nn0cni 10810	. . . . . . . . . . 11 |- ; 1 2 e. CC
293	292	addid1i 9767	. . . . . . . . . 10 |- (; 1 2 + 0 ) = ; 1 2
294	291, 293	eqtri 2470	. . . . . . . . 9 |- ( ( 2 x. 6 ) + 0 ) = ; 1 2
295	50	mul02i 9769	. . . . . . . . . . 11 |- ( 0 x. 6 ) = 0
296	295	oveq1i 6288	. . . . . . . . . 10 |- ( ( 0 x. 6 ) + 2 ) = ( 0 + 2 )
297	296, 134	eqtri 2470	. . . . . . . . 9 |- ( ( 0 x. 6 ) + 2 ) = 2
298	20, 3, 3, 20, 242, 136, 15, 294, 297	decma 11019	. . . . . . . 8 |- ( (; 2 0 x. 6 ) + ( 0 + 2 ) ) = ;; 1 2 2
299		4p3e7 10674	. . . . . . . . 9 |- ( 4 + 3 ) = 7
300	20, 2, 41, 98, 299	decaddi 11025	. . . . . . . 8 |- ( ( 4 x. 6 ) + 3 ) = ; 2 7
301	35, 2, 3, 41, 238, 279, 15, 28, 20, 298, 300	decmac 11020	. . . . . . 7 |- ( (;; 2 0 4 x. 6 ) + 3 ) = ;;; 1 2 2 7
302	15, 36, 15, 235, 15, 41, 301, 92	decmul1c 11028	. . . . . 6 |- (;;; 2 0 4 6 x. 6 ) = ;;;; 1 2 2 7 6
303	37, 36, 15, 235, 15, 237, 290, 302	decmul2c 11029	. . . . 5 |- (;;; 2 0 4 6 x. ;;; 2 0 4 6 ) = ;;;;;; 4 1 8 6 1 1 6
304	234, 303	eqtr4i 2473	. . . 4 |- ( (;; 10 4 6 x. N ) + ;; 10 7 0 ) = (;;; 2 0 4 6 x. ;;; 2 0 4 6 )
305	8, 9, 31, 34, 37, 30, 191, 198, 304	mod2xi 14429	. . 3 |- ( ( 2 ^; 5 0 ) mod N ) = (;; 10 7 0 mod N )
306		eqid 2441	. . . 4 |- ; 5 0 = ; 5 0
307	195	oveq1i 6288	. . . . 5 |- ( ( 2 x. 5 ) + 0 ) = ( 10 + 0 )
308		10nn 10704	. . . . . . 7 |- 10 e. NN
309	308	nncni 10549	. . . . . 6 |- 10 e. CC
310	309	addid1i 9767	. . . . 5 |- ( 10 + 0 ) = 10
311	307, 310	eqtri 2470	. . . 4 |- ( ( 2 x. 5 ) + 0 ) = 10
312	129, 62	eqtri 2470	. . . 4 |- ( 2 x. 0 ) = ; 0 0
313	20, 22, 3, 306, 3, 3, 311, 312	decmul2c 11029	. . 3 |- ( 2 x. ; 5 0 ) = ; 10 0
314		eqid 2441	. . . . 5 |- ;; 6 1 4 = ;; 6 1 4
315	20, 12	deccl 10995	. . . . 5 |- ; 2 9 e. NN0
316		eqid 2441	. . . . . . 7 |- ; 6 1 = ; 6 1
317		eqid 2441	. . . . . . 7 |- ; 2 9 = ; 2 9
318	218	oveq1i 6288	. . . . . . . 8 |- ( ( 6 + 2 ) + 1 ) = ( 8 + 1 )
319	318, 127	eqtri 2470	. . . . . . 7 |- ( ( 6 + 2 ) + 1 ) = 9
320	15, 16, 20, 12, 316, 317, 319, 152	decaddc2 11024	. . . . . 6 |- (; 6 1 + ; 2 9 ) = ; 9 0
321		eqid 2441	. . . . . . . 8 |- ;; 2 8 6 = ;; 2 8 6
322		eqid 2441	. . . . . . . . 9 |- ; 2 8 = ; 2 8
323	124, 278	oveq12i 6290	. . . . . . . . . 10 |- ( ( 2 x. 4 ) + ( 0 + 3 ) ) = ( 8 + 3 )
324		8p3e11 11037	. . . . . . . . . 10 |- ( 8 + 3 ) = ; 1 1
325	323, 324	eqtri 2470	. . . . . . . . 9 |- ( ( 2 x. 4 ) + ( 0 + 3 ) ) = ; 1 1
326		8t4e32 11071	. . . . . . . . . 10 |- ( 8 x. 4 ) = ; 3 2
327	41, 20, 20, 326, 90	decaddi 11025	. . . . . . . . 9 |- ( ( 8 x. 4 ) + 2 ) = ; 3 4
328	20, 24, 3, 20, 322, 136, 2, 2, 41, 325, 327	decmac 11020	. . . . . . . 8 |- ( (; 2 8 x. 4 ) + ( 0 + 2 ) ) = ;; 1 1 4
329	97	oveq1i 6288	. . . . . . . . 9 |- ( ( 6 x. 4 ) + 0 ) = (; 2 4 + 0 )
330	38	nn0cni 10810	. . . . . . . . . 10 |- ; 2 4 e. CC
331	330	addid1i 9767	. . . . . . . . 9 |- (; 2 4 + 0 ) = ; 2 4
332	329, 331	eqtri 2470	. . . . . . . 8 |- ( ( 6 x. 4 ) + 0 ) = ; 2 4
333	25, 15, 3, 3, 321, 63, 2, 2, 20, 328, 332	decmac 11020	. . . . . . 7 |- ( (;; 2 8 6 x. 4 ) + ( 0 + 0 ) ) = ;;; 1 1 4 4
334	26	nn0cni 10810	. . . . . . . . . 10 |- ;; 2 8 6 e. CC
335	334	mul01i 9770	. . . . . . . . 9 |- (;; 2 8 6 x. 0 ) = 0
336	335	oveq1i 6288	. . . . . . . 8 |- ( (;; 2 8 6 x. 0 ) + 9 ) = ( 0 + 9 )
337	336, 76	eqtri 2470	. . . . . . 7 |- ( (;; 2 8 6 x. 0 ) + 9 ) = ; 0 9
338	2, 3, 3, 12, 60, 59, 26, 12, 3, 333, 337	decma2c 11021	. . . . . 6 |- ( (;; 2 8 6 x. ; 4 0 ) + ( 9 + 0 ) ) = ;;;; 1 1 4 4 9
339	335	oveq1i 6288	. . . . . . 7 |- ( (;; 2 8 6 x. 0 ) + 0 ) = ( 0 + 0 )
340	339, 63	eqtri 2470	. . . . . 6 |- ( (;; 2 8 6 x. 0 ) + 0 ) = ; 0 0
341	4, 3, 12, 3, 55, 320, 26, 3, 3, 338, 340	decma2c 11021	. . . . 5 |- ( (;; 2 8 6 x. ;; 4 0 0 ) + (; 6 1 + ; 2 9 ) ) = ;;;;; 1 1 4 4 9 0
342	111, 61	oveq12i 6290	. . . . . . . 8 |- ( ( 2 x. 1 ) + ( 0 + 0 ) ) = ( 2 + 0 )
343	342, 113	eqtri 2470	. . . . . . 7 |- ( ( 2 x. 1 ) + ( 0 + 0 ) ) = 2
344	246	mulid1i 9598	. . . . . . . . 9 |- ( 8 x. 1 ) = 8
345	344	oveq1i 6288	. . . . . . . 8 |- ( ( 8 x. 1 ) + 1 ) = ( 8 + 1 )
346	127, 58	eqtri 2470	. . . . . . . 8 |- ( 8 + 1 ) = ; 0 9
347	345, 346	eqtri 2470	. . . . . . 7 |- ( ( 8 x. 1 ) + 1 ) = ; 0 9
348	20, 24, 3, 16, 322, 213, 16, 12, 3, 343, 347	decmac 11020	. . . . . 6 |- ( (; 2 8 x. 1 ) + ( 0 + 1 ) ) = ; 2 9
349	50	mulid1i 9598	. . . . . . . 8 |- ( 6 x. 1 ) = 6
350	349	oveq1i 6288	. . . . . . 7 |- ( ( 6 x. 1 ) + 4 ) = ( 6 + 4 )
351	94, 196	eqtri 2470	. . . . . . 7 |- ( 6 + 4 ) = ; 1 0
352	350, 351	eqtri 2470	. . . . . 6 |- ( ( 6 x. 1 ) + 4 ) = ; 1 0
353	25, 15, 3, 2, 321, 116, 16, 3, 16, 348, 352	decmac 11020	. . . . 5 |- ( (;; 2 8 6 x. 1 ) + 4 ) = ;; 2 9 0
354	5, 16, 17, 2, 1, 314, 26, 3, 315, 341, 353	decma2c 11021	. . . 4 |- ( (;; 2 8 6 x. N ) + ;; 6 1 4 ) = ;;;;;; 1 1 4 4 9 0 0
355	16, 16	deccl 10995	. . . . . . . . 9 |- ; 1 1 e. NN0
356	355, 2	deccl 10995	. . . . . . . 8 |- ;; 1 1 4 e. NN0
357	356, 2	deccl 10995	. . . . . . 7 |- ;;; 1 1 4 4 e. NN0
358	357, 12	deccl 10995	. . . . . 6 |- ;;;; 1 1 4 4 9 e. NN0
359	28, 2	deccl 10995	. . . . . . . 8 |- ; 7 4 e. NN0
360	359, 12	deccl 10995	. . . . . . 7 |- ;; 7 4 9 e. NN0
361		eqid 2441	. . . . . . . 8 |- ;; 7 4 9 = ;; 7 4 9
362	359	nn0cni 10810	. . . . . . . . . 10 |- ; 7 4 e. CC
363	362	addid1i 9767	. . . . . . . . 9 |- (; 7 4 + 0 ) = ; 7 4
364	157	addid1i 9767	. . . . . . . . . . 11 |- ( 7 + 0 ) = 7
365	364, 277	eqtri 2470	. . . . . . . . . 10 |- ( 7 + 0 ) = ; 0 7
366	79, 61	oveq12i 6290	. . . . . . . . . . . 12 |- ( ( 1 x. 1 ) + ( 0 + 0 ) ) = ( 1 + 0 )
367	366, 125	eqtri 2470	. . . . . . . . . . 11 |- ( ( 1 x. 1 ) + ( 0 + 0 ) ) = 1
368	69	mul02i 9769	. . . . . . . . . . . . 13 |- ( 0 x. 1 ) = 0
369	368	oveq1i 6288	. . . . . . . . . . . 12 |- ( ( 0 x. 1 ) + 1 ) = ( 0 + 1 )
370	369, 213	eqtri 2470	. . . . . . . . . . 11 |- ( ( 0 x. 1 ) + 1 ) = ; 0 1
371	16, 3, 3, 16, 196, 213, 16, 16, 3, 367, 370	decmac 11020	. . . . . . . . . 10 |- ( ( 10 x. 1 ) + ( 0 + 1 ) ) = ; 1 1
372	157	mulid1i 9598	. . . . . . . . . . . 12 |- ( 7 x. 1 ) = 7
373	372	oveq1i 6288	. . . . . . . . . . 11 |- ( ( 7 x. 1 ) + 7 ) = ( 7 + 7 )
374		7p7e14 11036	. . . . . . . . . . 11 |- ( 7 + 7 ) = ; 1 4
375	373, 374	eqtri 2470	. . . . . . . . . 10 |- ( ( 7 x. 1 ) + 7 ) = ; 1 4
376	10, 28, 3, 28, 201, 365, 16, 2, 16, 371, 375	decmac 11020	. . . . . . . . 9 |- ( (; 10 7 x. 1 ) + ( 7 + 0 ) ) = ;; 1 1 4
377	368	oveq1i 6288	. . . . . . . . . 10 |- ( ( 0 x. 1 ) + 4 ) = ( 0 + 4 )
378	64	addid2i 9768	. . . . . . . . . . 11 |- ( 0 + 4 ) = 4
379	378, 116	eqtri 2470	. . . . . . . . . 10 |- ( 0 + 4 ) = ; 0 4
380	377, 379	eqtri 2470	. . . . . . . . 9 |- ( ( 0 x. 1 ) + 4 ) = ; 0 4
381	29, 3, 28, 2, 199, 363, 16, 2, 3, 376, 380	decmac 11020	. . . . . . . 8 |- ( (;; 10 7 0 x. 1 ) + (; 7 4 + 0 ) ) = ;;; 1 1 4 4
382	30	nn0cni 10810	. . . . . . . . . . 11 |- ;; 10 7 0 e. CC
383	382	mul01i 9770	. . . . . . . . . 10 |- (;; 10 7 0 x. 0 ) = 0
384	383	oveq1i 6288	. . . . . . . . 9 |- ( (;; 10 7 0 x. 0 ) + 9 ) = ( 0 + 9 )
385	384, 76	eqtri 2470	. . . . . . . 8 |- ( (;; 10 7 0 x. 0 ) + 9 ) = ; 0 9
386	16, 3, 359, 12, 196, 361, 30, 12, 3, 381, 385	decma2c 11021	. . . . . . 7 |- ( (;; 10 7 0 x. 10 ) + ;; 7 4 9 ) = ;;;; 1 1 4 4 9
387	157	mulid2i 9599	. . . . . . . . . . . . . 14 |- ( 1 x. 7 ) = 7
388	387, 61	oveq12i 6290	. . . . . . . . . . . . 13 |- ( ( 1 x. 7 ) + ( 0 + 0 ) ) = ( 7 + 0 )
389	388, 364	eqtri 2470	. . . . . . . . . . . 12 |- ( ( 1 x. 7 ) + ( 0 + 0 ) ) = 7
390	157	mul02i 9769	. . . . . . . . . . . . . 14 |- ( 0 x. 7 ) = 0
391	390	oveq1i 6288	. . . . . . . . . . . . 13 |- ( ( 0 x. 7 ) + 4 ) = ( 0 + 4 )
392	391, 379	eqtri 2470	. . . . . . . . . . . 12 |- ( ( 0 x. 7 ) + 4 ) = ; 0 4
393	16, 3, 3, 2, 196, 116, 28, 2, 3, 389, 392	decmac 11020	. . . . . . . . . . 11 |- ( ( 10 x. 7 ) + 4 ) = ; 7 4
394		7t7e49 11068	. . . . . . . . . . 11 |- ( 7 x. 7 ) = ; 4 9
395	28, 10, 28, 201, 12, 2, 393, 394	decmul1c 11028	. . . . . . . . . 10 |- (; 10 7 x. 7 ) = ;; 7 4 9
396	395	oveq1i 6288	. . . . . . . . 9 |- ( (; 10 7 x. 7 ) + 0 ) = (;; 7 4 9 + 0 )
397	360	nn0cni 10810	. . . . . . . . . 10 |- ;; 7 4 9 e. CC
398	397	addid1i 9767	. . . . . . . . 9 |- (;; 7 4 9 + 0 ) = ;; 7 4 9
399	396, 398	eqtri 2470	. . . . . . . 8 |- ( (; 10 7 x. 7 ) + 0 ) = ;; 7 4 9
400	390, 62	eqtri 2470	. . . . . . . 8 |- ( 0 x. 7 ) = ; 0 0
401	28, 29, 3, 199, 3, 3, 399, 400	decmul1c 11028	. . . . . . 7 |- (;; 10 7 0 x. 7 ) = ;;; 7 4 9 0
402	30, 10, 28, 201, 3, 360, 386, 401	decmul2c 11029	. . . . . 6 |- (;; 10 7 0 x. ; 10 7 ) = ;;;;; 1 1 4 4 9 0
403	358, 3, 3, 402, 61	decaddi 11025	. . . . 5 |- ( (;; 10 7 0 x. ; 10 7 ) + 0 ) = ;;;;; 1 1 4 4 9 0
404	383, 62	eqtri 2470	. . . . 5 |- (;; 10 7 0 x. 0 ) = ; 0 0
405	30, 29, 3, 199, 3, 3, 403, 404	decmul2c 11029	. . . 4 |- (;; 10 7 0 x. ;; 10 7 0 ) = ;;;;;; 1 1 4 4 9 0 0
406	354, 405	eqtr4i 2473	. . 3 |- ( (;; 2 8 6 x. N ) + ;; 6 1 4 ) = (;; 10 7 0 x. ;; 10 7 0 )
407	8, 9, 23, 27, 30, 18, 305, 313, 406	mod2xi 14429	. 2 |- ( ( 2 ^; 10 0 ) mod N ) = (;; 6 1 4 mod N )
408		eqid 2441	. . 3 |- ; 10 0 = ; 10 0
409	20, 16, 3, 196, 3, 3, 114, 312	decmul2c 11029	. . . . 5 |- ( 2 x. 10 ) = ; 2 0
410	409	oveq1i 6288	. . . 4 |- ( ( 2 x. 10 ) + 0 ) = (; 2 0 + 0 )
411	410, 180	eqtri 2470	. . 3 |- ( ( 2 x. 10 ) + 0 ) = ; 2 0
412	20, 10, 3, 408, 3, 3, 411, 312	decmul2c 11029	. 2 |- ( 2 x. ; 10 0 ) = ;; 2 0 0
413		eqid 2441	. . . 4 |- ;; 9 0 2 = ;; 9 0 2
414		eqid 2441	. . . . . 6 |- ; 9 0 = ; 9 0
415	12, 3, 12, 414, 75	decaddi 11025	. . . . 5 |- (; 9 0 + 9 ) = ; 9 9
416		eqid 2441	. . . . . . 7 |- ; 9 4 = ; 9 4
417	203	oveq2i 6289	. . . . . . . 8 |- ( ( 9 x. 4 ) + ( 0 + 1 ) ) = ( ( 9 x. 4 ) + 1 )
418		6p1e7 10667	. . . . . . . . 9 |- ( 6 + 1 ) = 7
419		9t4e36 11078	. . . . . . . . 9 |- ( 9 x. 4 ) = ; 3 6
420	41, 15, 418, 419	decsuc 11004	. . . . . . . 8 |- ( ( 9 x. 4 ) + 1 ) = ; 3 7
421	417, 420	eqtri 2470	. . . . . . 7 |- ( ( 9 x. 4 ) + ( 0 + 1 ) ) = ; 3 7
422	105	oveq1i 6288	. . . . . . . 8 |- ( ( 4 x. 4 ) + 0 ) = (; 1 6 + 0 )
423	16, 15	deccl 10995	. . . . . . . . . 10 |- ; 1 6 e. NN0
424	423	nn0cni 10810	. . . . . . . . 9 |- ; 1 6 e. CC
425	424	addid1i 9767	. . . . . . . 8 |- (; 1 6 + 0 ) = ; 1 6
426	422, 425	eqtri 2470	. . . . . . 7 |- ( ( 4 x. 4 ) + 0 ) = ; 1 6
427	12, 2, 3, 3, 416, 63, 2, 15, 16, 421, 426	decmac 11020	. . . . . 6 |- ( (; 9 4 x. 4 ) + ( 0 + 0 ) ) = ;; 3 7 6
428	254	mul01i 9770	. . . . . . . 8 |- (; 9 4 x. 0 ) = 0
429	428	oveq1i 6288	. . . . . . 7 |- ( (; 9 4 x. 0 ) + 9 ) = ( 0 + 9 )
430	429, 76	eqtri 2470	. . . . . 6 |- ( (; 9 4 x. 0 ) + 9 ) = ; 0 9
431	2, 3, 3, 12, 60, 59, 13, 12, 3, 427, 430	decma2c 11021	. . . . 5 |- ( (; 9 4 x. ; 4 0 ) + ( 9 + 0 ) ) = ;;; 3 7 6 9
432	4, 3, 12, 12, 55, 415, 13, 12, 3, 431, 430	decma2c 11021	. . . 4 |- ( (; 9 4 x. ;; 4 0 0 ) + (; 9 0 + 9 ) ) = ;;;; 3 7 6 9 9
433	56	mulid1i 9598	. . . . . . 7 |- ( 9 x. 1 ) = 9
434	433, 61	oveq12i 6290	. . . . . 6 |- ( ( 9 x. 1 ) + ( 0 + 0 ) ) = ( 9 + 0 )
435	434, 57	eqtri 2470	. . . . 5 |- ( ( 9 x. 1 ) + ( 0 + 0 ) ) = 9
436	64	mulid1i 9598	. . . . . . 7 |- ( 4 x. 1 ) = 4
437	436	oveq1i 6288	. . . . . 6 |- ( ( 4 x. 1 ) + 2 ) = ( 4 + 2 )
438	221, 84	eqtri 2470	. . . . . 6 |- ( 4 + 2 ) = ; 0 6
439	437, 438	eqtri 2470	. . . . 5 |- ( ( 4 x. 1 ) + 2 ) = ; 0 6
440	12, 2, 3, 20, 416, 135, 16, 15, 3, 435, 439	decmac 11020	. . . 4 |- ( (; 9 4 x. 1 ) + 2 ) = ; 9 6
441	5, 16, 19, 20, 1, 413, 13, 15, 12, 432, 440	decma2c 11021	. . 3 |- ( (; 9 4 x. N ) + ;; 9 0 2 ) = ;;;;; 3 7 6 9 9 6
442	38, 22	deccl 10995	. . . 4 |- ;; 2 4 5 e. NN0
443		eqid 2441	. . . . 5 |- ;; 2 4 5 = ;; 2 4 5
444	50, 51, 218	addcomli 9772	. . . . . . 7 |- ( 2 + 6 ) = 8
445	20, 2, 15, 16, 169, 316, 444, 103	decadd 11022	. . . . . 6 |- (; 2 4 + ; 6 1 ) = ; 8 5
446		8p2e10 10685	. . . . . . . 8 |- ( 8 + 2 ) = 10
447	446, 196	eqtri 2470	. . . . . . 7 |- ( 8 + 2 ) = ; 1 0
448	41, 15, 418, 92	decsuc 11004	. . . . . . 7 |- ( ( 6 x. 6 ) + 1 ) = ; 3 7
449	50	mulid2i 9599	. . . . . . . . 9 |- ( 1 x. 6 ) = 6
450	449	oveq1i 6288	. . . . . . . 8 |- ( ( 1 x. 6 ) + 0 ) = ( 6 + 0 )
451	50	addid1i 9767	. . . . . . . 8 |- ( 6 + 0 ) = 6
452	450, 451	eqtri 2470	. . . . . . 7 |- ( ( 1 x. 6 ) + 0 ) = 6
453	15, 16, 16, 3, 316, 447, 15, 448, 452	decma 11019	. . . . . 6 |- ( (; 6 1 x. 6 ) + ( 8 + 2 ) ) = ;; 3 7 6
454	17, 2, 24, 22, 314, 445, 15, 12, 20, 453, 101	decmac 11020	. . . . 5 |- ( (;; 6 1 4 x. 6 ) + (; 2 4 + ; 6 1 ) ) = ;;; 3 7 6 9
455	349, 61	oveq12i 6290	. . . . . . . 8 |- ( ( 6 x. 1 ) + ( 0 + 0 ) ) = ( 6 + 0 )
456	455, 451	eqtri 2470	. . . . . . 7 |- ( ( 6 x. 1 ) + ( 0 + 0 ) ) = 6
457	79	oveq1i 6288	. . . . . . . 8 |- ( ( 1 x. 1 ) + 0 ) = ( 1 + 0 )
458	457, 257	eqtri 2470	. . . . . . 7 |- ( ( 1 x. 1 ) + 0 ) = ; 0 1
459	15, 16, 3, 3, 316, 63, 16, 16, 3, 456, 458	decmac 11020	. . . . . 6 |- ( (; 6 1 x. 1 ) + ( 0 + 0 ) ) = ; 6 1
460	436	oveq1i 6288	. . . . . . 7 |- ( ( 4 x. 1 ) + 5 ) = ( 4 + 5 )
461	100, 58	eqtri 2470	. . . . . . 7 |- ( 4 + 5 ) = ; 0 9
462	460, 461	eqtri 2470	. . . . . 6 |- ( ( 4 x. 1 ) + 5 ) = ; 0 9
463	17, 2, 3, 22, 314, 143, 16, 12, 3, 459, 462	decmac 11020	. . . . 5 |- ( (;; 6 1 4 x. 1 ) + 5 ) = ;; 6 1 9
464	15, 16, 38, 22, 316, 443, 18, 12, 17, 454, 463	decma2c 11021	. . . 4 |- ( (;; 6 1 4 x. ; 6 1 ) + ;; 2 4 5 ) = ;;;; 3 7 6 9 9
465	65	oveq1i 6288	. . . . . . 7 |- ( ( 1 x. 4 ) + 1 ) = ( 4 + 1 )
466	465, 103	eqtri 2470	. . . . . 6 |- ( ( 1 x. 4 ) + 1 ) = 5
467	15, 16, 3, 16, 316, 212, 2, 332, 466	decma 11019	. . . . 5 |- ( (; 6 1 x. 4 ) + 1 ) = ;; 2 4 5
468	2, 17, 2, 314, 15, 16, 467, 105	decmul1c 11028	. . . 4 |- (;; 6 1 4 x. 4 ) = ;;; 2 4 5 6
469	18, 17, 2, 314, 15, 442, 464, 468	decmul2c 11029	. . 3 |- (;; 6 1 4 x. ;; 6 1 4 ) = ;;;;; 3 7 6 9 9 6
470	441, 469	eqtr4i 2473	. 2 |- ( (; 9 4 x. N ) + ;; 9 0 2 ) = (;; 6 1 4 x. ;; 6 1 4 )
471	8, 9, 11, 14, 18, 21, 407, 412, 470	mod2xi 14429	1 |- ( ( 2 ^;; 2 0 0 ) mod N ) = (;; 9 0 2 mod N )

Syntax hints:   = wceq 1381  (class class class)co 6278   0cc0 9492   1c1 9493   + caddc 9495   x. cmul 9497   NNcn 10539   2c2 10588   3c3 10589   4c4 10590   5c5 10591   6c6 10592   7c7 10593   8c8 10594   9c9 10595   10c10 10596  ;cdc 10981   mod cmo 11972   ^cexp 12142

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-8 1804  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-sep 4555  ax-nul 4563  ax-pow 4612  ax-pr 4673  ax-un 6574  ax-cnex 9548  ax-resscn 9549  ax-1cn 9550  ax-icn 9551  ax-addcl 9552  ax-addrcl 9553  ax-mulcl 9554  ax-mulrcl 9555  ax-mulcom 9556  ax-addass 9557  ax-mulass 9558  ax-distr 9559  ax-i2m1 9560  ax-1ne0 9561  ax-1rid 9562  ax-rnegex 9563  ax-rrecex 9564  ax-cnre 9565  ax-pre-lttri 9566  ax-pre-lttrn 9567  ax-pre-ltadd 9568  ax-pre-mulgt0 9569  ax-pre-sup 9570

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 973  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-nel 2639  df-ral 2796  df-rex 2797  df-reu 2798  df-rmo 2799  df-rab 2800  df-v 3095  df-sbc 3312  df-csb 3419  df-dif 3462  df-un 3464  df-in 3466  df-ss 3473  df-pss 3475  df-nul 3769  df-if 3924  df-pw 3996  df-sn 4012  df-pr 4014  df-tp 4016  df-op 4018  df-uni 4232  df-iun 4314  df-br 4435  df-opab 4493  df-mpt 4494  df-tr 4528  df-eprel 4778  df-id 4782  df-po 4787  df-so 4788  df-fr 4825  df-we 4827  df-ord 4868  df-on 4869  df-lim 4870  df-suc 4871  df-xp 4992  df-rel 4993  df-cnv 4994  df-co 4995  df-dm 4996  df-rn 4997  df-res 4998  df-ima 4999  df-iota 5538  df-fun 5577  df-fn 5578  df-f 5579  df-f1 5580  df-fo 5581  df-f1o 5582  df-fv 5583  df-riota 6239  df-ov 6281  df-oprab 6282  df-mpt2 6283  df-om 6683  df-2nd 6783  df-recs 7041  df-rdg 7075  df-er 7310  df-en 7516  df-dom 7517  df-sdom 7518  df-sup 7900  df-pnf 9630  df-mnf 9631  df-xr 9632  df-ltxr 9633  df-le 9634  df-sub 9809  df-neg 9810  df-div 10210  df-nn 10540  df-2 10597  df-3 10598  df-4 10599  df-5 10600  df-6 10601  df-7 10602  df-8 10603  df-9 10604  df-10 10605  df-n0 10799  df-z 10868  df-dec 10982  df-uz 11088  df-rp 11227  df-fl 11905  df-mod 11973  df-seq 12084  df-exp 12143

This theorem is referenced by:  4001lem2  14498  4001lem3  14499