Theorem 2503lem1

Description: Lemma for 2503prm . Calculate a power mod. In decimal, we calculate 2 ^ 1 8 = 5 1 2 ^ 2 = 1 0 4 N + 1 8 3 2 == 1 8 3 2 . (Contributed by Mario Carneiro, 3-Mar-2014) (Revised by Mario Carneiro, 20-Apr-2015) (Proof shortened by AV, 16-Sep-2021)

	Ref	Expression
Hypothesis	2503prm.1	$$⊢N=2503$$
Assertion	2503lem1	$$⊢2^{18}\mathrm{mod}N=1832\mathrm{mod}N$$

Proof

Step	Hyp	Ref	Expression
1		2503prm.1	$$⊢N=2503$$
2		2nn0	$$⊢2\in {\mathbb{N}}_0$$
3		5nn0	$$⊢5\in {\mathbb{N}}_0$$
4	2 3	deccl	$$⊢25\in {\mathbb{N}}_0$$
5		0nn0	$$⊢0\in {\mathbb{N}}_0$$
6	4 5	deccl	$$⊢250\in {\mathbb{N}}_0$$
7		3nn	$$⊢3\in \mathbb{N}$$
8	6 7	decnncl	$$⊢2503\in \mathbb{N}$$
9	1 8	eqeltri	$$⊢N\in \mathbb{N}$$
10		2nn	$$⊢2\in \mathbb{N}$$
11		9nn0	$$⊢9\in {\mathbb{N}}_0$$
12		10nn0	$$⊢10\in {\mathbb{N}}_0$$
13		4nn0	$$⊢4\in {\mathbb{N}}_0$$
14	12 13	deccl	$$⊢104\in {\mathbb{N}}_0$$
15	14	nn0zi	$$⊢104\in \mathbb{Z}$$
16		1nn0	$$⊢1\in {\mathbb{N}}_0$$
17	3 16	deccl	$$⊢51\in {\mathbb{N}}_0$$
18	17 2	deccl	$$⊢512\in {\mathbb{N}}_0$$
19		8nn0	$$⊢8\in {\mathbb{N}}_0$$
20	16 19	deccl	$$⊢18\in {\mathbb{N}}_0$$
21		3nn0	$$⊢3\in {\mathbb{N}}_0$$
22	20 21	deccl	$$⊢183\in {\mathbb{N}}_0$$
23	22 2	deccl	$$⊢1832\in {\mathbb{N}}_0$$
24		8p1e9	$$⊢8+1=9$$
25		6nn0	$$⊢6\in {\mathbb{N}}_0$$
26		2exp8	$$⊢2^8=256$$
27		eqid	$$⊢25=25$$
28	16	dec0h	$$⊢1=01$$
29		2t2e4	$$⊢2\cdot 2=4$$
30		ax-1cn	$$⊢1\in ℂ$$
31	30	addlidi	$$⊢0+1=1$$
32	29 31	oveq12i	$$⊢2\cdot 2+0+1=4+1$$
33		4p1e5	$$⊢4+1=5$$
34	32 33	eqtri	$$⊢2\cdot 2+0+1=5$$
35		5t2e10	$$⊢5\cdot 2=10$$
36	16 5 31 35	decsuc	$$⊢5\cdot 2+1=11$$
37	2 3 5 16 27 28 2 16 16 34 36	decmac	$$⊢25\cdot 2+1=51$$
38		6t2e12	$$⊢6\cdot 2=12$$
39	2 4 25 26 2 16 37 38	decmul1c	$$⊢2^8\cdot 2=512$$
40	2 19 24 39	numexpp1	$$⊢2^9=512$$
41	40	oveq1i	$$⊢2^9\mathrm{mod}N=512\mathrm{mod}N$$
42		9cn	$$⊢9\in ℂ$$
43		2cn	$$⊢2\in ℂ$$
44		9t2e18	$$⊢9\cdot 2=18$$
45	42 43 44	mulcomli	$$⊢2\cdot 9=18$$
46		eqid	$$⊢1832=1832$$
47	21 16	deccl	$$⊢31\in {\mathbb{N}}_0$$
48	2 16	deccl	$$⊢21\in {\mathbb{N}}_0$$
49		eqid	$$⊢250=250$$
50		eqid	$$⊢183=183$$
51		eqid	$$⊢31=31$$
52		eqid	$$⊢18=18$$
53		1p1e2	$$⊢1+1=2$$
54		8p3e11	$$⊢8+3=11$$
55	16 19 21 52 53 16 54	decaddci	$$⊢18+3=21$$
56		3p1e4	$$⊢3+1=4$$
57	20 21 21 16 50 51 55 56	decadd	$$⊢183+31=214$$
58	48	nn0cni	$$⊢21\in ℂ$$
59	58	addridi	$$⊢21+0=21$$
60	3 2	deccl	$$⊢52\in {\mathbb{N}}_0$$
61		eqid	$$⊢104=104$$
62	60	nn0cni	$$⊢52\in ℂ$$
63		eqid	$$⊢52=52$$
64		2p2e4	$$⊢2+2=4$$
65	3 2 2 63 64	decaddi	$$⊢52+2=54$$
66	62 43 65	addcomli	$$⊢2+52=54$$
67	2	dec0u	$$⊢10\cdot 2=20$$
68		5p1e6	$$⊢5+1=6$$
69	67 68	oveq12i	$$⊢10\cdot 2+5+1=20+6$$
70		eqid	$$⊢20=20$$
71		6cn	$$⊢6\in ℂ$$
72	71	addlidi	$$⊢0+6=6$$
73	2 5 25 70 72	decaddi	$$⊢20+6=26$$
74	69 73	eqtri	$$⊢10\cdot 2+5+1=26$$
75		4t2e8	$$⊢4\cdot 2=8$$
76	75	oveq1i	$$⊢4\cdot 2+4=8+4$$
77		8p4e12	$$⊢8+4=12$$
78	76 77	eqtri	$$⊢4\cdot 2+4=12$$
79	12 13 3 13 61 66 2 2 16 74 78	decmac	$$⊢104\cdot 2+2+52=262$$
80	3	dec0u	$$⊢10\cdot 5=50$$
81	43	addlidi	$$⊢0+2=2$$
82	80 81	oveq12i	$$⊢10\cdot 5+0+2=50+2$$
83		eqid	$$⊢50=50$$
84	3 5 2 83 81	decaddi	$$⊢50+2=52$$
85	82 84	eqtri	$$⊢10\cdot 5+0+2=52$$
86		5cn	$$⊢5\in ℂ$$
87		4cn	$$⊢4\in ℂ$$
88		5t4e20	$$⊢5\cdot 4=20$$
89	86 87 88	mulcomli	$$⊢4\cdot 5=20$$
90	2 5 31 89	decsuc	$$⊢4\cdot 5+1=21$$
91	12 13 5 16 61 28 3 16 2 85 90	decmac	$$⊢104\cdot 5+1=521$$
92	2 3 2 16 27 59 14 16 60 79 91	decma2c	$$⊢104\cdot 25+21+0=2621$$
93	14	nn0cni	$$⊢104\in ℂ$$
94	93	mul01i	$$⊢104\cdot 0=0$$
95	94	oveq1i	$$⊢104\cdot 0+4=0+4$$
96	87	addlidi	$$⊢0+4=4$$
97	13	dec0h	$$⊢4=04$$
98	95 96 97	3eqtri	$$⊢104\cdot 0+4=04$$
99	4 5 48 13 49 57 14 13 5 92 98	decma2c	$$⊢104\cdot 250+183+31=26214$$
100		eqid	$$⊢10=10$$
101		3cn	$$⊢3\in ℂ$$
102	101	mullidi	$$⊢1\cdot 3=3$$
103		00id	$$⊢0+0=0$$
104	102 103	oveq12i	$$⊢1\cdot 3+0+0=3+0$$
105	101	addridi	$$⊢3+0=3$$
106	104 105	eqtri	$$⊢1\cdot 3+0+0=3$$
107	101	mul02i	$$⊢0\cdot 3=0$$
108	107	oveq1i	$$⊢0\cdot 3+1=0+1$$
109	108 31 28	3eqtri	$$⊢0\cdot 3+1=01$$
110	16 5 5 16 100 28 21 16 5 106 109	decmac	$$⊢10\cdot 3+1=31$$
111		4t3e12	$$⊢4\cdot 3=12$$
112	16 2 2 111 64	decaddi	$$⊢4\cdot 3+2=14$$
113	12 13 2 61 21 13 16 110 112	decrmac	$$⊢104\cdot 3+2=314$$
114	6 21 22 2 1 46 14 13 47 99 113	decma2c	$$⊢104\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1832=262144$$
115		eqid	$$⊢512=512$$
116	12 2	deccl	$$⊢102\in {\mathbb{N}}_0$$
117		eqid	$$⊢51=51$$
118		eqid	$$⊢102=102$$
119	86 30 68	addcomli	$$⊢1+5=6$$
120	16 5 3 16 100 117 119 31	decadd	$$⊢10+51=61$$
121		7nn0	$$⊢7\in {\mathbb{N}}_0$$
122		6p1e7	$$⊢6+1=7$$
123	121	dec0h	$$⊢7=07$$
124	122 123	eqtri	$$⊢6+1=07$$
125	31	oveq2i	$$⊢5\cdot 5+0+1=5\cdot 5+1$$
126		5t5e25	$$⊢5\cdot 5=25$$
127	2 3 68 126	decsuc	$$⊢5\cdot 5+1=26$$
128	125 127	eqtri	$$⊢5\cdot 5+0+1=26$$
129	86	mullidi	$$⊢1\cdot 5=5$$
130	129	oveq1i	$$⊢1\cdot 5+7=5+7$$
131		7cn	$$⊢7\in ℂ$$
132		7p5e12	$$⊢7+5=12$$
133	131 86 132	addcomli	$$⊢5+7=12$$
134	130 133	eqtri	$$⊢1\cdot 5+7=12$$
135	3 16 5 121 117 124 3 2 16 128 134	decmac	$$⊢51\cdot 5+6+1=262$$
136	86 43 35	mulcomli	$$⊢2\cdot 5=10$$
137	16 5 31 136	decsuc	$$⊢2\cdot 5+1=11$$
138	17 2 25 16 115 120 3 16 16 135 137	decmac	$$⊢512\cdot 5+10+51=2621$$
139	17	nn0cni	$$⊢51\in ℂ$$
140	139	mulridi	$$⊢51\cdot 1=51$$
141	43	mulridi	$$⊢2\cdot 1=2$$
142	141	oveq1i	$$⊢2\cdot 1+2=2+2$$
143	142 64	eqtri	$$⊢2\cdot 1+2=4$$
144	17 2 2 115 16 140 143	decrmanc	$$⊢512\cdot 1+2=514$$
145	3 16 12 2 117 118 18 13 17 138 144	decma2c	$$⊢512\cdot 51+102=26214$$
146	43	mullidi	$$⊢1\cdot 2=2$$
147	2 3 16 117 35 146	decmul1	$$⊢51\cdot 2=102$$
148	2 17 2 115 147 29	decmul1	$$⊢512\cdot 2=1024$$
149	18 17 2 115 13 116 145 148	decmul2c	$$⊢512\cdot 512=262144$$
150	114 149	eqtr4i	$$⊢104\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1832=512\cdot 512$$
151	9 10 11 15 18 23 41 45 150	mod2xi	$$⊢2^{18}\mathrm{mod}N=1832\mathrm{mod}N$$