Theorem 4001lem2 15849

Description: Lemma for 4001prm 15852. 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.) (Proof shortened by AV, 16-Sep-2021.)

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 11311	. . . . . 6 |- 4 e. NN0
3		0nn0 11307	. . . . . 6 |- 0 e. NN0
4	2, 3	deccl 11512	. . . . 5 |- ; 4 0 e. NN0
5	4, 3	deccl 11512	. . . 4 |- ;; 4 0 0 e. NN0
6		1nn 11031	. . . 4 |- 1 e. NN
7	5, 6	decnncl 11518	. . 3 |- ;;; 4 0 0 1 e. NN
8	1, 7	eqeltri 2697	. 2 |- N e. NN
9		2nn 11185	. 2 |- 2 e. NN
10		9nn0 11316	. . . . 5 |- 9 e. NN0
11	2, 10	deccl 11512	. . . 4 |- ; 4 9 e. NN0
12	11, 3	deccl 11512	. . 3 |- ;; 4 9 0 e. NN0
13	12	nn0zi 11402	. 2 |- ;; 4 9 0 e. ZZ
14		1nn0 11308	. . . . 5 |- 1 e. NN0
15	14, 2	deccl 11512	. . . 4 |- ; 1 4 e. NN0
16	15, 3	deccl 11512	. . 3 |- ;; 1 4 0 e. NN0
17	16, 14	deccl 11512	. 2 |- ;;; 1 4 0 1 e. NN0
18		2nn0 11309	. . . . 5 |- 2 e. NN0
19		3nn0 11310	. . . . 5 |- 3 e. NN0
20	18, 19	deccl 11512	. . . 4 |- ; 2 3 e. NN0
21	20, 14	deccl 11512	. . 3 |- ;; 2 3 1 e. NN0
22	21, 14	deccl 11512	. 2 |- ;;; 2 3 1 1 e. NN0
23	18, 3	deccl 11512	. . . 4 |- ; 2 0 e. NN0
24	23, 3	deccl 11512	. . 3 |- ;; 2 0 0 e. NN0
25	23, 19	deccl 11512	. . . 4 |- ;; 2 0 3 e. NN0
26	25	nn0zi 11402	. . 3 |- ;; 2 0 3 e. ZZ
27	10, 3	deccl 11512	. . . 4 |- ; 9 0 e. NN0
28	27, 18	deccl 11512	. . 3 |- ;; 9 0 2 e. NN0
29	1	4001lem1 15848	. . 3 |- ( ( 2 ^;; 2 0 0 ) mod N ) = (;; 9 0 2 mod N )
30	24	nn0cni 11304	. . . 4 |- ;; 2 0 0 e. CC
31		2cn 11091	. . . 4 |- 2 e. CC
32		eqid 2622	. . . . 5 |- ;; 2 0 0 = ;; 2 0 0
33		eqid 2622	. . . . . 6 |- ; 2 0 = ; 2 0
34		2t2e4 11177	. . . . . 6 |- ( 2 x. 2 ) = 4
35	31	mul02i 10225	. . . . . 6 |- ( 0 x. 2 ) = 0
36	18, 18, 3, 33, 3, 34, 35	decmul1 11585	. . . . 5 |- (; 2 0 x. 2 ) = ; 4 0
37	18, 23, 3, 32, 3, 36, 35	decmul1 11585	. . . 4 |- (;; 2 0 0 x. 2 ) = ;; 4 0 0
38	30, 31, 37	mulcomli 10047	. . 3 |- ( 2 x. ;; 2 0 0 ) = ;; 4 0 0
39		eqid 2622	. . . . 5 |- ;;; 1 4 0 1 = ;;; 1 4 0 1
40		6nn0 11313	. . . . . . 7 |- 6 e. NN0
41	14, 40	deccl 11512	. . . . . 6 |- ; 1 6 e. NN0
42		eqid 2622	. . . . . 6 |- ;; 4 0 0 = ;; 4 0 0
43		eqid 2622	. . . . . . 7 |- ;; 1 4 0 = ;; 1 4 0
44		eqid 2622	. . . . . . . 8 |- ; 1 4 = ; 1 4
45		4p2e6 11162	. . . . . . . 8 |- ( 4 + 2 ) = 6
46	14, 2, 18, 44, 45	decaddi 11579	. . . . . . 7 |- (; 1 4 + 2 ) = ; 1 6
47		00id 10211	. . . . . . 7 |- ( 0 + 0 ) = 0
48	15, 3, 18, 3, 43, 33, 46, 47	decadd 11570	. . . . . 6 |- (;; 1 4 0 + ; 2 0 ) = ;; 1 6 0
49		eqid 2622	. . . . . . 7 |- ; 4 0 = ; 4 0
50	41	nn0cni 11304	. . . . . . . 8 |- ; 1 6 e. CC
51	50	addid1i 10223	. . . . . . 7 |- (; 1 6 + 0 ) = ; 1 6
52		eqid 2622	. . . . . . . 8 |- ;; 2 0 3 = ;; 2 0 3
53		ax-1cn 9994	. . . . . . . . . 10 |- 1 e. CC
54	53	addid1i 10223	. . . . . . . . 9 |- ( 1 + 0 ) = 1
55	14	dec0h 11522	. . . . . . . . 9 |- 1 = ; 0 1
56	54, 55	eqtri 2644	. . . . . . . 8 |- ( 1 + 0 ) = ; 0 1
57	53	addid2i 10224	. . . . . . . . . 10 |- ( 0 + 1 ) = 1
58	57, 14	eqeltri 2697	. . . . . . . . 9 |- ( 0 + 1 ) e. NN0
59		4cn 11098	. . . . . . . . . 10 |- 4 e. CC
60		4t2e8 11181	. . . . . . . . . 10 |- ( 4 x. 2 ) = 8
61	59, 31, 60	mulcomli 10047	. . . . . . . . 9 |- ( 2 x. 4 ) = 8
62	59	mul02i 10225	. . . . . . . . . . 11 |- ( 0 x. 4 ) = 0
63	62, 57	oveq12i 6662	. . . . . . . . . 10 |- ( ( 0 x. 4 ) + ( 0 + 1 ) ) = ( 0 + 1 )
64	63, 57	eqtri 2644	. . . . . . . . 9 |- ( ( 0 x. 4 ) + ( 0 + 1 ) ) = 1
65	18, 3, 58, 33, 2, 61, 64	decrmanc 11576	. . . . . . . 8 |- ( (; 2 0 x. 4 ) + ( 0 + 1 ) ) = ; 8 1
66		2p1e3 11151	. . . . . . . . 9 |- ( 2 + 1 ) = 3
67		3cn 11095	. . . . . . . . . 10 |- 3 e. CC
68		4t3e12 11632	. . . . . . . . . 10 |- ( 4 x. 3 ) = ; 1 2
69	59, 67, 68	mulcomli 10047	. . . . . . . . 9 |- ( 3 x. 4 ) = ; 1 2
70	14, 18, 66, 69	decsuc 11535	. . . . . . . 8 |- ( ( 3 x. 4 ) + 1 ) = ; 1 3
71	23, 19, 3, 14, 52, 56, 2, 19, 14, 65, 70	decmac 11566	. . . . . . 7 |- ( (;; 2 0 3 x. 4 ) + ( 1 + 0 ) ) = ;; 8 1 3
72	25	nn0cni 11304	. . . . . . . . . 10 |- ;; 2 0 3 e. CC
73	72	mul01i 10226	. . . . . . . . 9 |- (;; 2 0 3 x. 0 ) = 0
74	73	oveq1i 6660	. . . . . . . 8 |- ( (;; 2 0 3 x. 0 ) + 6 ) = ( 0 + 6 )
75		6cn 11102	. . . . . . . . 9 |- 6 e. CC
76	75	addid2i 10224	. . . . . . . 8 |- ( 0 + 6 ) = 6
77	40	dec0h 11522	. . . . . . . 8 |- 6 = ; 0 6
78	74, 76, 77	3eqtri 2648	. . . . . . 7 |- ( (;; 2 0 3 x. 0 ) + 6 ) = ; 0 6
79	2, 3, 14, 40, 49, 51, 25, 40, 3, 71, 78	decma2c 11568	. . . . . 6 |- ( (;; 2 0 3 x. ; 4 0 ) + (; 1 6 + 0 ) ) = ;;; 8 1 3 6
80	73	oveq1i 6660	. . . . . . 7 |- ( (;; 2 0 3 x. 0 ) + 0 ) = ( 0 + 0 )
81	3	dec0h 11522	. . . . . . 7 |- 0 = ; 0 0
82	80, 47, 81	3eqtri 2648	. . . . . 6 |- ( (;; 2 0 3 x. 0 ) + 0 ) = ; 0 0
83	4, 3, 41, 3, 42, 48, 25, 3, 3, 79, 82	decma2c 11568	. . . . 5 |- ( (;; 2 0 3 x. ;; 4 0 0 ) + (;; 1 4 0 + ; 2 0 ) ) = ;;;; 8 1 3 6 0
84	31	mulid1i 10042	. . . . . . 7 |- ( 2 x. 1 ) = 2
85	53	mul02i 10225	. . . . . . 7 |- ( 0 x. 1 ) = 0
86	14, 18, 3, 33, 3, 84, 85	decmul1 11585	. . . . . 6 |- (; 2 0 x. 1 ) = ; 2 0
87	67	mulid1i 10042	. . . . . . . 8 |- ( 3 x. 1 ) = 3
88	87	oveq1i 6660	. . . . . . 7 |- ( ( 3 x. 1 ) + 1 ) = ( 3 + 1 )
89		3p1e4 11153	. . . . . . 7 |- ( 3 + 1 ) = 4
90	88, 89	eqtri 2644	. . . . . 6 |- ( ( 3 x. 1 ) + 1 ) = 4
91	23, 19, 14, 52, 14, 86, 90	decrmanc 11576	. . . . 5 |- ( (;; 2 0 3 x. 1 ) + 1 ) = ;; 2 0 4
92	5, 14, 16, 14, 1, 39, 25, 2, 23, 83, 91	decma2c 11568	. . . 4 |- ( (;; 2 0 3 x. N ) + ;;; 1 4 0 1 ) = ;;;;; 8 1 3 6 0 4
93		eqid 2622	. . . . 5 |- ;; 9 0 2 = ;; 9 0 2
94		8nn0 11315	. . . . . . 7 |- 8 e. NN0
95	14, 94	deccl 11512	. . . . . 6 |- ; 1 8 e. NN0
96	95, 3	deccl 11512	. . . . 5 |- ;; 1 8 0 e. NN0
97		eqid 2622	. . . . . 6 |- ; 9 0 = ; 9 0
98		eqid 2622	. . . . . 6 |- ;; 1 8 0 = ;; 1 8 0
99	95	nn0cni 11304	. . . . . . . 8 |- ; 1 8 e. CC
100	99	addid1i 10223	. . . . . . 7 |- (; 1 8 + 0 ) = ; 1 8
101		1p2e3 11152	. . . . . . . . 9 |- ( 1 + 2 ) = 3
102	101, 19	eqeltri 2697	. . . . . . . 8 |- ( 1 + 2 ) e. NN0
103		9t9e81 11670	. . . . . . . 8 |- ( 9 x. 9 ) = ; 8 1
104		9cn 11108	. . . . . . . . . . 11 |- 9 e. CC
105	104	mul02i 10225	. . . . . . . . . 10 |- ( 0 x. 9 ) = 0
106	105, 101	oveq12i 6662	. . . . . . . . 9 |- ( ( 0 x. 9 ) + ( 1 + 2 ) ) = ( 0 + 3 )
107	67	addid2i 10224	. . . . . . . . 9 |- ( 0 + 3 ) = 3
108	106, 107	eqtri 2644	. . . . . . . 8 |- ( ( 0 x. 9 ) + ( 1 + 2 ) ) = 3
109	10, 3, 102, 97, 10, 103, 108	decrmanc 11576	. . . . . . 7 |- ( (; 9 0 x. 9 ) + ( 1 + 2 ) ) = ;; 8 1 3
110		9t2e18 11663	. . . . . . . . 9 |- ( 9 x. 2 ) = ; 1 8
111	104, 31, 110	mulcomli 10047	. . . . . . . 8 |- ( 2 x. 9 ) = ; 1 8
112		1p1e2 11134	. . . . . . . 8 |- ( 1 + 1 ) = 2
113		8p8e16 11618	. . . . . . . 8 |- ( 8 + 8 ) = ; 1 6
114	14, 94, 94, 111, 112, 40, 113	decaddci 11580	. . . . . . 7 |- ( ( 2 x. 9 ) + 8 ) = ; 2 6
115	27, 18, 14, 94, 93, 100, 10, 40, 18, 109, 114	decmac 11566	. . . . . 6 |- ( (;; 9 0 2 x. 9 ) + (; 1 8 + 0 ) ) = ;;; 8 1 3 6
116	28	nn0cni 11304	. . . . . . . . 9 |- ;; 9 0 2 e. CC
117	116	mul01i 10226	. . . . . . . 8 |- (;; 9 0 2 x. 0 ) = 0
118	117	oveq1i 6660	. . . . . . 7 |- ( (;; 9 0 2 x. 0 ) + 0 ) = ( 0 + 0 )
119	118, 47, 81	3eqtri 2648	. . . . . 6 |- ( (;; 9 0 2 x. 0 ) + 0 ) = ; 0 0
120	10, 3, 95, 3, 97, 98, 28, 3, 3, 115, 119	decma2c 11568	. . . . 5 |- ( (;; 9 0 2 x. ; 9 0 ) + ;; 1 8 0 ) = ;;;; 8 1 3 6 0
121	18, 10, 3, 97, 3, 110, 35	decmul1 11585	. . . . . 6 |- (; 9 0 x. 2 ) = ;; 1 8 0
122	18, 27, 18, 93, 2, 121, 34	decmul1 11585	. . . . 5 |- (;; 9 0 2 x. 2 ) = ;;; 1 8 0 4
123	28, 27, 18, 93, 2, 96, 120, 122	decmul2c 11589	. . . 4 |- (;; 9 0 2 x. ;; 9 0 2 ) = ;;;;; 8 1 3 6 0 4
124	92, 123	eqtr4i 2647	. . 3 |- ( (;; 2 0 3 x. N ) + ;;; 1 4 0 1 ) = (;; 9 0 2 x. ;; 9 0 2 )
125	8, 9, 24, 26, 28, 17, 29, 38, 124	mod2xi 15773	. 2 |- ( ( 2 ^;; 4 0 0 ) mod N ) = (;;; 1 4 0 1 mod N )
126	5	nn0cni 11304	. . 3 |- ;; 4 0 0 e. CC
127	18, 2, 3, 49, 3, 60, 35	decmul1 11585	. . . 4 |- (; 4 0 x. 2 ) = ; 8 0
128	18, 4, 3, 42, 3, 127, 35	decmul1 11585	. . 3 |- (;; 4 0 0 x. 2 ) = ;; 8 0 0
129	126, 31, 128	mulcomli 10047	. 2 |- ( 2 x. ;; 4 0 0 ) = ;; 8 0 0
130		eqid 2622	. . . 4 |- ;;; 2 3 1 1 = ;;; 2 3 1 1
131	18, 94	deccl 11512	. . . . 5 |- ; 2 8 e. NN0
132		eqid 2622	. . . . . 6 |- ;; 2 3 1 = ;; 2 3 1
133		eqid 2622	. . . . . 6 |- ; 4 9 = ; 4 9
134		7nn0 11314	. . . . . . 7 |- 7 e. NN0
135		7p1e8 11157	. . . . . . 7 |- ( 7 + 1 ) = 8
136		eqid 2622	. . . . . . . 8 |- ; 2 3 = ; 2 3
137		4p3e7 11163	. . . . . . . . 9 |- ( 4 + 3 ) = 7
138	59, 67, 137	addcomli 10228	. . . . . . . 8 |- ( 3 + 4 ) = 7
139	18, 19, 2, 136, 138	decaddi 11579	. . . . . . 7 |- (; 2 3 + 4 ) = ; 2 7
140	18, 134, 135, 139	decsuc 11535	. . . . . 6 |- ( (; 2 3 + 4 ) + 1 ) = ; 2 8
141		9p1e10 11496	. . . . . . 7 |- ( 9 + 1 ) = ; 1 0
142	104, 53, 141	addcomli 10228	. . . . . 6 |- ( 1 + 9 ) = ; 1 0
143	20, 14, 2, 10, 132, 133, 140, 142	decaddc2 11575	. . . . 5 |- (;; 2 3 1 + ; 4 9 ) = ;; 2 8 0
144	131	nn0cni 11304	. . . . . . 7 |- ; 2 8 e. CC
145	144	addid1i 10223	. . . . . 6 |- (; 2 8 + 0 ) = ; 2 8
146	31	addid1i 10223	. . . . . . . 8 |- ( 2 + 0 ) = 2
147	146, 18	eqeltri 2697	. . . . . . 7 |- ( 2 + 0 ) e. NN0
148		eqid 2622	. . . . . . 7 |- ;; 4 9 0 = ;; 4 9 0
149		4t4e16 11633	. . . . . . . . 9 |- ( 4 x. 4 ) = ; 1 6
150		6p3e9 11170	. . . . . . . . 9 |- ( 6 + 3 ) = 9
151	14, 40, 19, 149, 150	decaddi 11579	. . . . . . . 8 |- ( ( 4 x. 4 ) + 3 ) = ; 1 9
152		9t4e36 11665	. . . . . . . 8 |- ( 9 x. 4 ) = ; 3 6
153	2, 2, 10, 133, 40, 19, 151, 152	decmul1c 11587	. . . . . . 7 |- (; 4 9 x. 4 ) = ;; 1 9 6
154	62, 146	oveq12i 6662	. . . . . . . 8 |- ( ( 0 x. 4 ) + ( 2 + 0 ) ) = ( 0 + 2 )
155	31	addid2i 10224	. . . . . . . 8 |- ( 0 + 2 ) = 2
156	154, 155	eqtri 2644	. . . . . . 7 |- ( ( 0 x. 4 ) + ( 2 + 0 ) ) = 2
157	11, 3, 147, 148, 2, 153, 156	decrmanc 11576	. . . . . 6 |- ( (;; 4 9 0 x. 4 ) + ( 2 + 0 ) ) = ;;; 1 9 6 2
158	12	nn0cni 11304	. . . . . . . . 9 |- ;; 4 9 0 e. CC
159	158	mul01i 10226	. . . . . . . 8 |- (;; 4 9 0 x. 0 ) = 0
160	159	oveq1i 6660	. . . . . . 7 |- ( (;; 4 9 0 x. 0 ) + 8 ) = ( 0 + 8 )
161		8cn 11106	. . . . . . . 8 |- 8 e. CC
162	161	addid2i 10224	. . . . . . 7 |- ( 0 + 8 ) = 8
163	94	dec0h 11522	. . . . . . 7 |- 8 = ; 0 8
164	160, 162, 163	3eqtri 2648	. . . . . 6 |- ( (;; 4 9 0 x. 0 ) + 8 ) = ; 0 8
165	2, 3, 18, 94, 49, 145, 12, 94, 3, 157, 164	decma2c 11568	. . . . 5 |- ( (;; 4 9 0 x. ; 4 0 ) + (; 2 8 + 0 ) ) = ;;;; 1 9 6 2 8
166	159	oveq1i 6660	. . . . . 6 |- ( (;; 4 9 0 x. 0 ) + 0 ) = ( 0 + 0 )
167	166, 47, 81	3eqtri 2648	. . . . 5 |- ( (;; 4 9 0 x. 0 ) + 0 ) = ; 0 0
168	4, 3, 131, 3, 42, 143, 12, 3, 3, 165, 167	decma2c 11568	. . . 4 |- ( (;; 4 9 0 x. ;; 4 0 0 ) + (;; 2 3 1 + ; 4 9 ) ) = ;;;;; 1 9 6 2 8 0
169	59	mulid1i 10042	. . . . . 6 |- ( 4 x. 1 ) = 4
170	104	mulid1i 10042	. . . . . 6 |- ( 9 x. 1 ) = 9
171	14, 2, 10, 133, 10, 169, 170	decmul1 11585	. . . . 5 |- (; 4 9 x. 1 ) = ; 4 9
172	85	oveq1i 6660	. . . . . 6 |- ( ( 0 x. 1 ) + 1 ) = ( 0 + 1 )
173	172, 57	eqtri 2644	. . . . 5 |- ( ( 0 x. 1 ) + 1 ) = 1
174	11, 3, 14, 148, 14, 171, 173	decrmanc 11576	. . . 4 |- ( (;; 4 9 0 x. 1 ) + 1 ) = ;; 4 9 1
175	5, 14, 21, 14, 1, 130, 12, 14, 11, 168, 174	decma2c 11568	. . 3 |- ( (;; 4 9 0 x. N ) + ;;; 2 3 1 1 ) = ;;;;;; 1 9 6 2 8 0 1
176	15	nn0cni 11304	. . . . . . 7 |- ; 1 4 e. CC
177	176	addid1i 10223	. . . . . 6 |- (; 1 4 + 0 ) = ; 1 4
178		5nn0 11312	. . . . . . . 8 |- 5 e. NN0
179	178, 40	deccl 11512	. . . . . . 7 |- ; 5 6 e. NN0
180	179, 3	deccl 11512	. . . . . 6 |- ;; 5 6 0 e. NN0
181		eqid 2622	. . . . . . . 8 |- ;; 5 6 0 = ;; 5 6 0
182	179	nn0cni 11304	. . . . . . . . 9 |- ; 5 6 e. CC
183	182	addid2i 10224	. . . . . . . 8 |- ( 0 + ; 5 6 ) = ; 5 6
184	3, 14, 179, 3, 55, 181, 183, 54	decadd 11570	. . . . . . 7 |- ( 1 + ;; 5 6 0 ) = ;; 5 6 1
185	182	addid1i 10223	. . . . . . . 8 |- (; 5 6 + 0 ) = ; 5 6
186		5cn 11100	. . . . . . . . . . 11 |- 5 e. CC
187	186	addid1i 10223	. . . . . . . . . 10 |- ( 5 + 0 ) = 5
188	187, 178	eqeltri 2697	. . . . . . . . 9 |- ( 5 + 0 ) e. NN0
189	53	mulid1i 10042	. . . . . . . . 9 |- ( 1 x. 1 ) = 1
190	169, 187	oveq12i 6662	. . . . . . . . . 10 |- ( ( 4 x. 1 ) + ( 5 + 0 ) ) = ( 4 + 5 )
191		5p4e9 11167	. . . . . . . . . . 11 |- ( 5 + 4 ) = 9
192	186, 59, 191	addcomli 10228	. . . . . . . . . 10 |- ( 4 + 5 ) = 9
193	190, 192	eqtri 2644	. . . . . . . . 9 |- ( ( 4 x. 1 ) + ( 5 + 0 ) ) = 9
194	14, 2, 188, 44, 14, 189, 193	decrmanc 11576	. . . . . . . 8 |- ( (; 1 4 x. 1 ) + ( 5 + 0 ) ) = ; 1 9
195	85	oveq1i 6660	. . . . . . . . 9 |- ( ( 0 x. 1 ) + 6 ) = ( 0 + 6 )
196	195, 76, 77	3eqtri 2648	. . . . . . . 8 |- ( ( 0 x. 1 ) + 6 ) = ; 0 6
197	15, 3, 178, 40, 43, 185, 14, 40, 3, 194, 196	decmac 11566	. . . . . . 7 |- ( (;; 1 4 0 x. 1 ) + (; 5 6 + 0 ) ) = ;; 1 9 6
198	189	oveq1i 6660	. . . . . . . 8 |- ( ( 1 x. 1 ) + 1 ) = ( 1 + 1 )
199	18	dec0h 11522	. . . . . . . 8 |- 2 = ; 0 2
200	198, 112, 199	3eqtri 2648	. . . . . . 7 |- ( ( 1 x. 1 ) + 1 ) = ; 0 2
201	16, 14, 179, 14, 39, 184, 14, 18, 3, 197, 200	decmac 11566	. . . . . 6 |- ( (;;; 1 4 0 1 x. 1 ) + ( 1 + ;; 5 6 0 ) ) = ;;; 1 9 6 2
202	59	mulid2i 10043	. . . . . . . . . . . 12 |- ( 1 x. 4 ) = 4
203	202	oveq1i 6660	. . . . . . . . . . 11 |- ( ( 1 x. 4 ) + 1 ) = ( 4 + 1 )
204		4p1e5 11154	. . . . . . . . . . 11 |- ( 4 + 1 ) = 5
205	203, 204	eqtri 2644	. . . . . . . . . 10 |- ( ( 1 x. 4 ) + 1 ) = 5
206	2, 14, 2, 44, 40, 14, 205, 149	decmul1c 11587	. . . . . . . . 9 |- (; 1 4 x. 4 ) = ; 5 6
207	75	addid1i 10223	. . . . . . . . 9 |- ( 6 + 0 ) = 6
208	178, 40, 3, 206, 207	decaddi 11579	. . . . . . . 8 |- ( (; 1 4 x. 4 ) + 0 ) = ; 5 6
209		0cn 10032	. . . . . . . . 9 |- 0 e. CC
210	59	mul01i 10226	. . . . . . . . . 10 |- ( 4 x. 0 ) = 0
211	210, 81	eqtri 2644	. . . . . . . . 9 |- ( 4 x. 0 ) = ; 0 0
212	59, 209, 211	mulcomli 10047	. . . . . . . 8 |- ( 0 x. 4 ) = ; 0 0
213	2, 15, 3, 43, 3, 3, 208, 212	decmul1c 11587	. . . . . . 7 |- (;; 1 4 0 x. 4 ) = ;; 5 6 0
214	202	oveq1i 6660	. . . . . . . 8 |- ( ( 1 x. 4 ) + 4 ) = ( 4 + 4 )
215		4p4e8 11164	. . . . . . . 8 |- ( 4 + 4 ) = 8
216	214, 215	eqtri 2644	. . . . . . 7 |- ( ( 1 x. 4 ) + 4 ) = 8
217	16, 14, 2, 39, 2, 213, 216	decrmanc 11576	. . . . . 6 |- ( (;;; 1 4 0 1 x. 4 ) + 4 ) = ;;; 5 6 0 8
218	14, 2, 14, 2, 44, 177, 17, 94, 180, 201, 217	decma2c 11568	. . . . 5 |- ( (;;; 1 4 0 1 x. ; 1 4 ) + (; 1 4 + 0 ) ) = ;;;; 1 9 6 2 8
219	17	nn0cni 11304	. . . . . . . 8 |- ;;; 1 4 0 1 e. CC
220	219	mul01i 10226	. . . . . . 7 |- (;;; 1 4 0 1 x. 0 ) = 0
221	220	oveq1i 6660	. . . . . 6 |- ( (;;; 1 4 0 1 x. 0 ) + 0 ) = ( 0 + 0 )
222	221, 47, 81	3eqtri 2648	. . . . 5 |- ( (;;; 1 4 0 1 x. 0 ) + 0 ) = ; 0 0
223	15, 3, 15, 3, 43, 43, 17, 3, 3, 218, 222	decma2c 11568	. . . 4 |- ( (;;; 1 4 0 1 x. ;; 1 4 0 ) + ;; 1 4 0 ) = ;;;;; 1 9 6 2 8 0
224	219	mulid1i 10042	. . . 4 |- (;;; 1 4 0 1 x. 1 ) = ;;; 1 4 0 1
225	17, 16, 14, 39, 14, 16, 223, 224	decmul2c 11589	. . 3 |- (;;; 1 4 0 1 x. ;;; 1 4 0 1 ) = ;;;;;; 1 9 6 2 8 0 1
226	175, 225	eqtr4i 2647	. 2 |- ( (;; 4 9 0 x. N ) + ;;; 2 3 1 1 ) = (;;; 1 4 0 1 x. ;;; 1 4 0 1 )
227	8, 9, 5, 13, 17, 22, 125, 129, 226	mod2xi 15773	1 |- ( ( 2 ^;; 8 0 0 ) mod N ) = (;;; 2 3 1 1 mod N )

Syntax hints:   = wceq 1483  (class class class)co 6650   0cc0 9936   1c1 9937   + caddc 9939   x. cmul 9941   NNcn 11020   2c2 11070   3c3 11071   4c4 11072   5c5 11073   6c6 11074   7c7 11075   8c8 11076   9c9 11077   NN0cn0 11292  ;cdc 11493   mod cmo 12668   ^cexp 12860

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-pre-sup 10014

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-er 7742  df-en 7956  df-dom 7957  df-sdom 7958  df-sup 8348  df-inf 8349  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-3 11080  df-4 11081  df-5 11082  df-6 11083  df-7 11084  df-8 11085  df-9 11086  df-n0 11293  df-z 11378  df-dec 11494  df-uz 11688  df-rp 11833  df-fl 12593  df-mod 12669  df-seq 12802  df-exp 12861

This theorem is referenced by:  4001lem3  15850  4001lem4  15851