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		1nn0	$$⊢1\in {\mathbb{N}}_0$$
3		2nn0	$$⊢2\in {\mathbb{N}}_0$$
4	2 3	deccl	$$⊢12\in {\mathbb{N}}_0$$
5		5nn0	$$⊢5\in {\mathbb{N}}_0$$
6	4 5	deccl	$$⊢125\in {\mathbb{N}}_0$$
7		9nn	$$⊢9\in \mathbb{N}$$
8	6 7	decnncl	$$⊢1259\in \mathbb{N}$$
9	1 8	eqeltri	$$⊢N\in \mathbb{N}$$
10		2nn	$$⊢2\in \mathbb{N}$$
11		7nn0	$$⊢7\in {\mathbb{N}}_0$$
12	2 11	deccl	$$⊢17\in {\mathbb{N}}_0$$
13		4nn0	$$⊢4\in {\mathbb{N}}_0$$
14	2 13	deccl	$$⊢14\in {\mathbb{N}}_0$$
15	14	nn0zi	$$⊢14\in \mathbb{Z}$$
16		3nn0	$$⊢3\in {\mathbb{N}}_0$$
17	2 16	deccl	$$⊢13\in {\mathbb{N}}_0$$
18		6nn0	$$⊢6\in {\mathbb{N}}_0$$
19	17 18	deccl	$$⊢136\in {\mathbb{N}}_0$$
20		8nn0	$$⊢8\in {\mathbb{N}}_0$$
21	20 11	deccl	$$⊢87\in {\mathbb{N}}_0$$
22		0nn0	$$⊢0\in {\mathbb{N}}_0$$
23	21 22	deccl	$$⊢870\in {\mathbb{N}}_0$$
24	1	1259lem1	$$⊢2^{17}\mathrm{mod}N=136\mathrm{mod}N$$
25		eqid	$$⊢17=17$$
26		2cn	$$⊢2\in ℂ$$
27	26	mulid1i	$$⊢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	3 2 11 25 13 2 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	20 11 2 3 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	13	dec0h	$$⊢4=04$$
50	48 49	eqtri	$$⊢1+3=04$$
51	46	mulid1i	$$⊢1\cdot 1=1$$
52		00id	$$⊢0+0=0$$
53	51 52	oveq12i	$$⊢1\cdot 1+0+0=1+0$$
54	46	addid1i	$$⊢1+0=1$$
55	53 54	eqtri	$$⊢1\cdot 1+0+0=1$$
56		4cn	$$⊢4\in ℂ$$
57	56	mulid1i	$$⊢4\cdot 1=4$$
58	57	oveq1i	$$⊢4\cdot 1+4=4+4$$
59		4p4e8	$$⊢4+4=8$$
60	20	dec0h	$$⊢8=08$$
61	58 59 60	3eqtri	$$⊢4\cdot 1+4=08$$
62	2 13 22 13 44 50 2 20 22 55 61	decmac	$$⊢14\cdot 1+1+3=18$$
63	18	dec0h	$$⊢6=06$$
64	26	mulid2i	$$⊢1\cdot 2=2$$
65	46	addid2i	$$⊢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	2 13 22 18 44 63 3 13 2 67 71	decmac	$$⊢14\cdot 2+6=34$$
73	2 3 2 18 39 43 14 13 16 62 72	decma2c	$$⊢14\cdot 12+9+7=184$$
74	35	dec0h	$$⊢9=09$$
75		5cn	$$⊢5\in ℂ$$
76	75	mulid2i	$$⊢1\cdot 5=5$$
77	26	addid2i	$$⊢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	addid2i	$$⊢0+9=9$$
85	3 22 35 82 84	decaddi	$$⊢4\cdot 5+9=29$$
86	2 13 22 35 44 74 5 35 3 80 85	decmac	$$⊢14\cdot 5+9=79$$
87	4 5 35 35 37 42 14 35 11 73 86	decma2c	$$⊢14\cdot 125+87+12=1849$$
88	83	mulid2i	$$⊢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 2 13 44 18 16 91 93	decmul1c	$$⊢14\cdot 9=126$$
95	94	oveq1i	$$⊢14\cdot 9+0=126+0$$
96	4 18	deccl	$$⊢126\in {\mathbb{N}}_0$$
97	96	nn0cni	$$⊢126\in ℂ$$
98	97	addid1i	$$⊢126+0=126$$
99	95 98	eqtri	$$⊢14\cdot 9+0=126$$
100	6 35 21 22 1 36 14 18 4 87 99	decma2c	$$⊢14\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+870=18496$$
101		eqid	$$⊢136=136$$
102	20 2	deccl	$$⊢81\in {\mathbb{N}}_0$$
103		eqid	$$⊢13=13$$
104		eqid	$$⊢81=81$$
105	13 22	deccl	$$⊢40\in {\mathbb{N}}_0$$
106		eqid	$$⊢40=40$$
107	56	addid2i	$$⊢0+4=4$$
108		8cn	$$⊢8\in ℂ$$
109	108	addid1i	$$⊢8+0=8$$
110	22 20 13 22 60 106 107 109	decadd	$$⊢8+40=48$$
111		4p1e5	$$⊢4+1=5$$
112	5	dec0h	$$⊢5=05$$
113	111 112	eqtri	$$⊢4+1=05$$
114	45	mulid1i	$$⊢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	2 16 22 5 103 113 2 20 22 55 118	decmac	$$⊢13\cdot 1+4+1=18$$
120		6cn	$$⊢6\in ℂ$$
121	120	mulid1i	$$⊢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	17 18 13 20 101 110 2 13 2 119 124	decmac	$$⊢136\cdot 1+8+40=184$$
126	2	dec0h	$$⊢1=01$$
127	65 126	eqtri	$$⊢0+1=01$$
128	45	mulid2i	$$⊢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	2 16 22 2 103 127 16 22 2 130 134	decmac	$$⊢13\cdot 3+0+1=40$$
136		6t3e18	$$⊢6\cdot 3=18$$
137	2 20 2 136 40	decaddi	$$⊢6\cdot 3+1=19$$
138	17 18 22 2 101 126 16 35 2 135 137	decmac	$$⊢136\cdot 3+1=409$$
139	2 16 20 2 103 104 19 35 105 125 138	decma2c	$$⊢136\cdot 13+81=1849$$
140	16	dec0h	$$⊢3=03$$
141	120	mulid2i	$$⊢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	2 20 16 145 146 2 147	decaddci	$$⊢3\cdot 6+3=21$$
149	2 16 22 16 103 140 18 2 3 144 148	decmac	$$⊢13\cdot 6+3=81$$
150		6t6e36	$$⊢6\cdot 6=36$$
151	18 17 18 101 18 16 149 150	decmul1c	$$⊢136\cdot 6=816$$
152	19 17 18 101 18 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	9 10 12 15 19 23 24 34 153	mod2xi	$$⊢2^{34}\mathrm{mod}N=870\mathrm{mod}N$$