Theorem 1259lem1

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

	Ref	Expression
Hypothesis	1259prm.1	$$⊢N=1259$$
Assertion	1259lem1	$$⊢2^{17}\mathrm{mod}N=136\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		6nn0	$$⊢6\in {\mathbb{N}}_0$$
12	2 11	deccl	$$⊢16\in {\mathbb{N}}_0$$
13		0z	$$⊢0\in \mathbb{Z}$$
14		8nn0	$$⊢8\in {\mathbb{N}}_0$$
15	11 14	deccl	$$⊢68\in {\mathbb{N}}_0$$
16		3nn0	$$⊢3\in {\mathbb{N}}_0$$
17	2 16	deccl	$$⊢13\in {\mathbb{N}}_0$$
18	17 11	deccl	$$⊢136\in {\mathbb{N}}_0$$
19	5 3	deccl	$$⊢52\in {\mathbb{N}}_0$$
20	19	nn0zi	$$⊢52\in \mathbb{Z}$$
21	3 14	nn0expcli	$$⊢2^8\in {\mathbb{N}}_0$$
22		eqid	$$⊢2^8\mathrm{mod}N=2^8\mathrm{mod}N$$
23	14	nn0cni	$$⊢8\in ℂ$$
24		2cn	$$⊢2\in ℂ$$
25		8t2e16	$$⊢8\cdot 2=16$$
26	23 24 25	mulcomli	$$⊢2\cdot 8=16$$
27		9nn0	$$⊢9\in {\mathbb{N}}_0$$
28		eqid	$$⊢68=68$$
29		4nn0	$$⊢4\in {\mathbb{N}}_0$$
30		7nn0	$$⊢7\in {\mathbb{N}}_0$$
31	29 30	deccl	$$⊢47\in {\mathbb{N}}_0$$
32		eqid	$$⊢125=125$$
33		0nn0	$$⊢0\in {\mathbb{N}}_0$$
34	11	dec0h	$$⊢6=06$$
35		eqid	$$⊢47=47$$
36		4cn	$$⊢4\in ℂ$$
37	36	addid2i	$$⊢0+4=4$$
38	37	oveq1i	$$⊢0+4+1=4+1$$
39		4p1e5	$$⊢4+1=5$$
40	38 39	eqtri	$$⊢0+4+1=5$$
41		7cn	$$⊢7\in ℂ$$
42		6cn	$$⊢6\in ℂ$$
43		7p6e13	$$⊢7+6=13$$
44	41 42 43	addcomli	$$⊢6+7=13$$
45	33 11 29 30 34 35 40 16 44	decaddc	$$⊢6+47=53$$
46	3 11	deccl	$$⊢26\in {\mathbb{N}}_0$$
47		eqid	$$⊢12=12$$
48	5	dec0h	$$⊢5=05$$
49		eqid	$$⊢26=26$$
50	24	addid2i	$$⊢0+2=2$$
51	50	oveq1i	$$⊢0+2+1=2+1$$
52		2p1e3	$$⊢2+1=3$$
53	51 52	eqtri	$$⊢0+2+1=3$$
54		5cn	$$⊢5\in ℂ$$
55		6p5e11	$$⊢6+5=11$$
56	42 54 55	addcomli	$$⊢5+6=11$$
57	33 5 3 11 48 49 53 2 56	decaddc	$$⊢5+26=31$$
58		10nn0	$$⊢10\in {\mathbb{N}}_0$$
59		eqid	$$⊢52=52$$
60	58	nn0cni	$$⊢10\in ℂ$$
61		3cn	$$⊢3\in ℂ$$
62		dec10p	$$⊢10+3=13$$
63	60 61 62	addcomli	$$⊢3+10=13$$
64	54	mulid1i	$$⊢5\cdot 1=5$$
65		1p0e1	$$⊢1+0=1$$
66	64 65	oveq12i	$$⊢5\cdot 1+1+0=5+1$$
67		5p1e6	$$⊢5+1=6$$
68	66 67	eqtri	$$⊢5\cdot 1+1+0=6$$
69	24	mulid1i	$$⊢2\cdot 1=2$$
70	69	oveq1i	$$⊢2\cdot 1+3=2+3$$
71		3p2e5	$$⊢3+2=5$$
72	61 24 71	addcomli	$$⊢2+3=5$$
73	70 72 48	3eqtri	$$⊢2\cdot 1+3=05$$
74	5 3 2 16 59 63 2 5 33 68 73	decmac	$$⊢52\cdot 1+3+10=65$$
75	2	dec0h	$$⊢1=01$$
76		5t2e10	$$⊢5\cdot 2=10$$
77		00id	$$⊢0+0=0$$
78	76 77	oveq12i	$$⊢5\cdot 2+0+0=10+0$$
79		dec10p	$$⊢10+0=10$$
80	78 79	eqtri	$$⊢5\cdot 2+0+0=10$$
81		2t2e4	$$⊢2\cdot 2=4$$
82	81	oveq1i	$$⊢2\cdot 2+1=4+1$$
83	82 39 48	3eqtri	$$⊢2\cdot 2+1=05$$
84	5 3 33 2 59 75 3 5 33 80 83	decmac	$$⊢52\cdot 2+1=105$$
85	2 3 16 2 47 57 19 5 58 74 84	decma2c	$$⊢52\cdot 12+5+26=655$$
86		5t5e25	$$⊢5\cdot 5=25$$
87	3 5 67 86	decsuc	$$⊢5\cdot 5+1=26$$
88	54 24 76	mulcomli	$$⊢2\cdot 5=10$$
89	61	addid2i	$$⊢0+3=3$$
90	2 33 16 88 89	decaddi	$$⊢2\cdot 5+3=13$$
91	5 3 16 59 5 16 2 87 90	decrmac	$$⊢52\cdot 5+3=263$$
92	4 5 5 16 32 45 19 16 46 85 91	decma2c	$$⊢52\cdot 125+6+47=6553$$
93		9cn	$$⊢9\in ℂ$$
94		9t5e45	$$⊢9\cdot 5=45$$
95	93 54 94	mulcomli	$$⊢5\cdot 9=45$$
96		5p2e7	$$⊢5+2=7$$
97	29 5 3 95 96	decaddi	$$⊢5\cdot 9+2=47$$
98		9t2e18	$$⊢9\cdot 2=18$$
99	93 24 98	mulcomli	$$⊢2\cdot 9=18$$
100		1p1e2	$$⊢1+1=2$$
101		8p8e16	$$⊢8+8=16$$
102	2 14 14 99 100 11 101	decaddci	$$⊢2\cdot 9+8=26$$
103	5 3 14 59 27 11 3 97 102	decrmac	$$⊢52\cdot 9+8=476$$
104	6 27 11 14 1 28 19 11 31 92 103	decma2c	$$⊢52\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+68=65536$$
105		2exp16	$$⊢2^{16}=65536$$
106		eqid	$$⊢2^8=2^8$$
107		eqid	$$⊢2^8{2}^8=2^8{2}^8$$
108	3 14 26 106 107	numexp2x	$$⊢2^{16}=2^8{2}^8$$
109	104 105 108	3eqtr2i	$$⊢52\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+68=2^8{2}^8$$
110	9 10 14 20 21 15 22 26 109	mod2xi	$$⊢2^{16}\mathrm{mod}N=68\mathrm{mod}N$$
111		6p1e7	$$⊢6+1=7$$
112		eqid	$$⊢16=16$$
113	2 11 111 112	decsuc	$$⊢16+1=17$$
114	18	nn0cni	$$⊢136\in ℂ$$
115	114	addid2i	$$⊢0+136=136$$
116	9	nncni	$$⊢N\in ℂ$$
117	116	mul02i	$$⊢0\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=0$$
118	117	oveq1i	$$⊢0\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+136=0+136$$
119		6t2e12	$$⊢6\cdot 2=12$$
120	2 3 52 119	decsuc	$$⊢6\cdot 2+1=13$$
121	3 11 14 28 11 2 120 25	decmul1c	$$⊢68\cdot 2=136$$
122	115 118 121	3eqtr4i	$$⊢0\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+136=68\cdot 2$$
123	9 10 12 13 15 18 110 113 122	modxp1i	$$⊢2^{17}\mathrm{mod}N=136\mathrm{mod}N$$