Theorem 1259lem2

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

	Ref	Expression
Hypothesis	1259prm.1	$$⊢N=1259$$
Assertion	1259lem2	$$⊢2^{34}\mathrm{mod}N=870\mathrm{mod}N$$

Proof

Step	Hyp	Ref	Expression
1		1259prm.1	$$⊢N=1259$$
2		12nn0	$$⊢12\in {\mathbb{N}}_0$$
3		5nn0	$$⊢5\in {\mathbb{N}}_0$$
4	2 3	deccl	$$⊢125\in {\mathbb{N}}_0$$
5		9nn	$$⊢9\in \mathbb{N}$$
6	4 5	decnncl	$$⊢1259\in \mathbb{N}$$
7	1 6	eqeltri	$$⊢N\in \mathbb{N}$$
8		2nn	$$⊢2\in \mathbb{N}$$
9		1nn0	$$⊢1\in {\mathbb{N}}_0$$
10		7nn0	$$⊢7\in {\mathbb{N}}_0$$
11	9 10	deccl	$$⊢17\in {\mathbb{N}}_0$$
12		4nn0	$$⊢4\in {\mathbb{N}}_0$$
13	9 12	deccl	$$⊢14\in {\mathbb{N}}_0$$
14	13	nn0zi	$$⊢14\in \mathbb{Z}$$
15		3nn0	$$⊢3\in {\mathbb{N}}_0$$
16	9 15	deccl	$$⊢13\in {\mathbb{N}}_0$$
17		6nn0	$$⊢6\in {\mathbb{N}}_0$$
18	16 17	deccl	$$⊢136\in {\mathbb{N}}_0$$
19		8nn0	$$⊢8\in {\mathbb{N}}_0$$
20	19 10	deccl	$$⊢87\in {\mathbb{N}}_0$$
21		0nn0	$$⊢0\in {\mathbb{N}}_0$$
22	20 21	deccl	$$⊢870\in {\mathbb{N}}_0$$
23	1	1259lem1	$$⊢2^{17}\mathrm{mod}N=136\mathrm{mod}N$$
24		2nn0	$$⊢2\in {\mathbb{N}}_0$$
25		eqid	$$⊢17=17$$
26		2cn	$$⊢2\in ℂ$$
27	26	mulridi	$$⊢2\cdot 1=2$$
28	27	oveq1i	$$⊢2\cdot 1+1=2+1$$
29		2p1e3	$$⊢2+1=3$$
30	28 29	eqtri	$$⊢2\cdot 1+1=3$$
31		7cn	$$⊢7\in ℂ$$
32		7t2e14	$$⊢7\cdot 2=14$$
33	31 26 32	mulcomli	$$⊢2\cdot 7=14$$
34	24 9 10 25 12 9 30 33	decmul2c	$$⊢2\cdot 17=34$$
35		9nn0	$$⊢9\in {\mathbb{N}}_0$$
36		eqid	$$⊢870=870$$
37		eqid	$$⊢125=125$$
38		eqid	$$⊢87=87$$
39		eqid	$$⊢12=12$$
40		8p1e9	$$⊢8+1=9$$
41		7p2e9	$$⊢7+2=9$$
42	19 10 9 24 38 39 40 41	decadd	$$⊢87+12=99$$
43		9p7e16	$$⊢9+7=16$$
44		eqid	$$⊢14=14$$
45		3cn	$$⊢3\in ℂ$$
46		ax-1cn	$$⊢1\in ℂ$$
47		3p1e4	$$⊢3+1=4$$
48	45 46 47	addcomli	$$⊢1+3=4$$
49	12	dec0h	$$⊢4=04$$
50	48 49	eqtri	$$⊢1+3=04$$
51	46	mulridi	$$⊢1\cdot 1=1$$
52		00id	$$⊢0+0=0$$
53	51 52	oveq12i	$$⊢1\cdot 1+0+0=1+0$$
54	46	addridi	$$⊢1+0=1$$
55	53 54	eqtri	$$⊢1\cdot 1+0+0=1$$
56		4cn	$$⊢4\in ℂ$$
57	56	mulridi	$$⊢4\cdot 1=4$$
58	57	oveq1i	$$⊢4\cdot 1+4=4+4$$
59		4p4e8	$$⊢4+4=8$$
60	19	dec0h	$$⊢8=08$$
61	58 59 60	3eqtri	$$⊢4\cdot 1+4=08$$
62	9 12 21 12 44 50 9 19 21 55 61	decmac	$$⊢14\cdot 1+1+3=18$$
63	17	dec0h	$$⊢6=06$$
64	26	mullidi	$$⊢1\cdot 2=2$$
65	46	addlidi	$$⊢0+1=1$$
66	64 65	oveq12i	$$⊢1\cdot 2+0+1=2+1$$
67	66 29	eqtri	$$⊢1\cdot 2+0+1=3$$
68		4t2e8	$$⊢4\cdot 2=8$$
69	68	oveq1i	$$⊢4\cdot 2+6=8+6$$
70		8p6e14	$$⊢8+6=14$$
71	69 70	eqtri	$$⊢4\cdot 2+6=14$$
72	9 12 21 17 44 63 24 12 9 67 71	decmac	$$⊢14\cdot 2+6=34$$
73	9 24 9 17 39 43 13 12 15 62 72	decma2c	$$⊢14\cdot 12+9+7=184$$
74	35	dec0h	$$⊢9=09$$
75		5cn	$$⊢5\in ℂ$$
76	75	mullidi	$$⊢1\cdot 5=5$$
77	26	addlidi	$$⊢0+2=2$$
78	76 77	oveq12i	$$⊢1\cdot 5+0+2=5+2$$
79		5p2e7	$$⊢5+2=7$$
80	78 79	eqtri	$$⊢1\cdot 5+0+2=7$$
81		5t4e20	$$⊢5\cdot 4=20$$
82	75 56 81	mulcomli	$$⊢4\cdot 5=20$$
83		9cn	$$⊢9\in ℂ$$
84	83	addlidi	$$⊢0+9=9$$
85	24 21 35 82 84	decaddi	$$⊢4\cdot 5+9=29$$
86	9 12 21 35 44 74 3 35 24 80 85	decmac	$$⊢14\cdot 5+9=79$$
87	2 3 35 35 37 42 13 35 10 73 86	decma2c	$$⊢14\cdot 125+87+12=1849$$
88	83	mullidi	$$⊢1\cdot 9=9$$
89	88	oveq1i	$$⊢1\cdot 9+3=9+3$$
90		9p3e12	$$⊢9+3=12$$
91	89 90	eqtri	$$⊢1\cdot 9+3=12$$
92		9t4e36	$$⊢9\cdot 4=36$$
93	83 56 92	mulcomli	$$⊢4\cdot 9=36$$
94	35 9 12 44 17 15 91 93	decmul1c	$$⊢14\cdot 9=126$$
95	94	oveq1i	$$⊢14\cdot 9+0=126+0$$
96	2 17	deccl	$$⊢126\in {\mathbb{N}}_0$$
97	96	nn0cni	$$⊢126\in ℂ$$
98	97	addridi	$$⊢126+0=126$$
99	95 98	eqtri	$$⊢14\cdot 9+0=126$$
100	4 35 20 21 1 36 13 17 2 87 99	decma2c	$$⊢14\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+870=18496$$
101		eqid	$$⊢136=136$$
102	19 9	deccl	$$⊢81\in {\mathbb{N}}_0$$
103		eqid	$$⊢13=13$$
104		eqid	$$⊢81=81$$
105	12 21	deccl	$$⊢40\in {\mathbb{N}}_0$$
106		eqid	$$⊢40=40$$
107	56	addlidi	$$⊢0+4=4$$
108		8cn	$$⊢8\in ℂ$$
109	108	addridi	$$⊢8+0=8$$
110	21 19 12 21 60 106 107 109	decadd	$$⊢8+40=48$$
111		4p1e5	$$⊢4+1=5$$
112	3	dec0h	$$⊢5=05$$
113	111 112	eqtri	$$⊢4+1=05$$
114	45	mulridi	$$⊢3\cdot 1=3$$
115	114	oveq1i	$$⊢3\cdot 1+5=3+5$$
116		5p3e8	$$⊢5+3=8$$
117	75 45 116	addcomli	$$⊢3+5=8$$
118	115 117 60	3eqtri	$$⊢3\cdot 1+5=08$$
119	9 15 21 3 103 113 9 19 21 55 118	decmac	$$⊢13\cdot 1+4+1=18$$
120		6cn	$$⊢6\in ℂ$$
121	120	mulridi	$$⊢6\cdot 1=6$$
122	121	oveq1i	$$⊢6\cdot 1+8=6+8$$
123	108 120 70	addcomli	$$⊢6+8=14$$
124	122 123	eqtri	$$⊢6\cdot 1+8=14$$
125	16 17 12 19 101 110 9 12 9 119 124	decmac	$$⊢136\cdot 1+8+40=184$$
126	9	dec0h	$$⊢1=01$$
127	65 126	eqtri	$$⊢0+1=01$$
128	45	mullidi	$$⊢1\cdot 3=3$$
129	128 65	oveq12i	$$⊢1\cdot 3+0+1=3+1$$
130	129 47	eqtri	$$⊢1\cdot 3+0+1=4$$
131		3t3e9	$$⊢3\cdot 3=9$$
132	131	oveq1i	$$⊢3\cdot 3+1=9+1$$
133		9p1e10	$$⊢9+1=10$$
134	132 133	eqtri	$$⊢3\cdot 3+1=10$$
135	9 15 21 9 103 127 15 21 9 130 134	decmac	$$⊢13\cdot 3+0+1=40$$
136		6t3e18	$$⊢6\cdot 3=18$$
137	9 19 9 136 40	decaddi	$$⊢6\cdot 3+1=19$$
138	16 17 21 9 101 126 15 35 9 135 137	decmac	$$⊢136\cdot 3+1=409$$
139	9 15 19 9 103 104 18 35 105 125 138	decma2c	$$⊢136\cdot 13+81=1849$$
140	15	dec0h	$$⊢3=03$$
141	120	mullidi	$$⊢1\cdot 6=6$$
142	141 77	oveq12i	$$⊢1\cdot 6+0+2=6+2$$
143		6p2e8	$$⊢6+2=8$$
144	142 143	eqtri	$$⊢1\cdot 6+0+2=8$$
145	120 45 136	mulcomli	$$⊢3\cdot 6=18$$
146		1p1e2	$$⊢1+1=2$$
147		8p3e11	$$⊢8+3=11$$
148	9 19 15 145 146 9 147	decaddci	$$⊢3\cdot 6+3=21$$
149	9 15 21 15 103 140 17 9 24 144 148	decmac	$$⊢13\cdot 6+3=81$$
150		6t6e36	$$⊢6\cdot 6=36$$
151	17 16 17 101 17 15 149 150	decmul1c	$$⊢136\cdot 6=816$$
152	18 16 17 101 17 102 139 151	decmul2c	$$⊢136\cdot 136=18496$$
153	100 152	eqtr4i	$$⊢14\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+870=136\cdot 136$$
154	7 8 11 14 18 22 23 34 153	mod2xi	$$⊢2^{34}\mathrm{mod}N=870\mathrm{mod}N$$