Theorem 1259lem3

Description: Lemma for 1259prm . Calculate a power mod. In decimal, we calculate 2 ^ 3 8 = 2 ^ 3 4 x. 2 ^ 4 == 8 7 0 x. 1 6 = 1 1 N + 7 1 and 2 ^ 7 6 = ( 2 ^ 3 4 ) ^ 2 == 7 1 ^ 2 = 4 N + 5 == 5 . (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	1259lem3	$$⊢2^{76}\mathrm{mod}N=5\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		3nn0	$$⊢3\in {\mathbb{N}}_0$$
12		8nn0	$$⊢8\in {\mathbb{N}}_0$$
13	11 12	deccl	$$⊢38\in {\mathbb{N}}_0$$
14		4z	$$⊢4\in \mathbb{Z}$$
15		7nn0	$$⊢7\in {\mathbb{N}}_0$$
16	15 2	deccl	$$⊢71\in {\mathbb{N}}_0$$
17		4nn0	$$⊢4\in {\mathbb{N}}_0$$
18	11 17	deccl	$$⊢34\in {\mathbb{N}}_0$$
19	2 2	deccl	$$⊢11\in {\mathbb{N}}_0$$
20	19	nn0zi	$$⊢11\in \mathbb{Z}$$
21	12 15	deccl	$$⊢87\in {\mathbb{N}}_0$$
22		0nn0	$$⊢0\in {\mathbb{N}}_0$$
23	21 22	deccl	$$⊢870\in {\mathbb{N}}_0$$
24		6nn0	$$⊢6\in {\mathbb{N}}_0$$
25	2 24	deccl	$$⊢16\in {\mathbb{N}}_0$$
26	1	1259lem2	$$⊢2^{34}\mathrm{mod}N=870\mathrm{mod}N$$
27		2exp4	$$⊢2^4=16$$
28	27	oveq1i	$$⊢2^4\mathrm{mod}N=16\mathrm{mod}N$$
29		eqid	$$⊢34=34$$
30		4p4e8	$$⊢4+4=8$$
31	11 17 17 29 30	decaddi	$$⊢34+4=38$$
32		9nn0	$$⊢9\in {\mathbb{N}}_0$$
33		eqid	$$⊢71=71$$
34		10nn0	$$⊢10\in {\mathbb{N}}_0$$
35		eqid	$$⊢11=11$$
36	34	nn0cni	$$⊢10\in ℂ$$
37		7cn	$$⊢7\in ℂ$$
38		dec10p	$$⊢10+7=17$$
39	36 37 38	addcomli	$$⊢7+10=17$$
40	2 11	deccl	$$⊢13\in {\mathbb{N}}_0$$
41	6	nn0cni	$$⊢125\in ℂ$$
42	41	mullidi	$$⊢1\cdot 125=125$$
43	2	dec0h	$$⊢1=01$$
44		eqid	$$⊢13=13$$
45		0p1e1	$$⊢0+1=1$$
46		3cn	$$⊢3\in ℂ$$
47		ax-1cn	$$⊢1\in ℂ$$
48		3p1e4	$$⊢3+1=4$$
49	46 47 48	addcomli	$$⊢1+3=4$$
50	22 2 2 11 43 44 45 49	decadd	$$⊢1+13=14$$
51		2p1e3	$$⊢2+1=3$$
52		eqid	$$⊢12=12$$
53	2 3 51 52	decsuc	$$⊢12+1=13$$
54		5p4e9	$$⊢5+4=9$$
55	4 5 2 17 42 50 53 54	decadd	$$⊢1\cdot 125+1+13=139$$
56		5cn	$$⊢5\in ℂ$$
57		7p5e12	$$⊢7+5=12$$
58	37 56 57	addcomli	$$⊢5+7=12$$
59	4 5 15 42 53 3 58	decaddci	$$⊢1\cdot 125+7=132$$
60	2 2 2 15 35 39 6 3 40 55 59	decmac	$$⊢11\cdot 125+7+10=1392$$
61		9p1e10	$$⊢9+1=10$$
62		9cn	$$⊢9\in ℂ$$
63	19	nn0cni	$$⊢11\in ℂ$$
64		9t11e99	$$⊢9\cdot 11=99$$
65	62 63 64	mulcomli	$$⊢11\cdot 9=99$$
66	32 61 65	decsucc	$$⊢11\cdot 9+1=100$$
67	6 32 15 2 1 33 19 22 34 60 66	decma2c	$$⊢11\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+71=13920$$
68		eqid	$$⊢16=16$$
69	5 3	deccl	$$⊢52\in {\mathbb{N}}_0$$
70	69 3	deccl	$$⊢522\in {\mathbb{N}}_0$$
71		eqid	$$⊢870=870$$
72		eqid	$$⊢522=522$$
73		eqid	$$⊢87=87$$
74	69	nn0cni	$$⊢52\in ℂ$$
75	74	addridi	$$⊢52+0=52$$
76		8cn	$$⊢8\in ℂ$$
77	76	mulridi	$$⊢8\cdot 1=8$$
78	56	addridi	$$⊢5+0=5$$
79	77 78	oveq12i	$$⊢8\cdot 1+5+0=8+5$$
80		8p5e13	$$⊢8+5=13$$
81	79 80	eqtri	$$⊢8\cdot 1+5+0=13$$
82	37	mulridi	$$⊢7\cdot 1=7$$
83	82	oveq1i	$$⊢7\cdot 1+2=7+2$$
84		7p2e9	$$⊢7+2=9$$
85	32	dec0h	$$⊢9=09$$
86	83 84 85	3eqtri	$$⊢7\cdot 1+2=09$$
87	12 15 5 3 73 75 2 32 22 81 86	decmac	$$⊢87\cdot 1+52+0=139$$
88	47	mul02i	$$⊢0\cdot 1=0$$
89	88	oveq1i	$$⊢0\cdot 1+2=0+2$$
90		2cn	$$⊢2\in ℂ$$
91	90	addlidi	$$⊢0+2=2$$
92	3	dec0h	$$⊢2=02$$
93	89 91 92	3eqtri	$$⊢0\cdot 1+2=02$$
94	21 22 69 3 71 72 2 3 22 87 93	decmac	$$⊢870\cdot 1+522=1392$$
95		8t6e48	$$⊢8\cdot 6=48$$
96		4p1e5	$$⊢4+1=5$$
97		8p4e12	$$⊢8+4=12$$
98	17 12 17 95 96 3 97	decaddci	$$⊢8\cdot 6+4=52$$
99		7t6e42	$$⊢7\cdot 6=42$$
100	24 12 15 73 3 17 98 99	decmul1c	$$⊢87\cdot 6=522$$
101		6cn	$$⊢6\in ℂ$$
102	101	mul02i	$$⊢0\cdot 6=0$$
103	24 21 22 71 100 102	decmul1	$$⊢870\cdot 6=5220$$
104	23 2 24 68 22 70 94 103	decmul2c	$$⊢870\cdot 16=13920$$
105	67 104	eqtr4i	$$⊢11\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+71=870\cdot 16$$
106	9 10 18 20 23 16 17 25 26 28 31 105	modxai	$$⊢2^{38}\mathrm{mod}N=71\mathrm{mod}N$$
107		eqid	$$⊢38=38$$
108		3t2e6	$$⊢3\cdot 2=6$$
109	46 90 108	mulcomli	$$⊢2\cdot 3=6$$
110	109	oveq1i	$$⊢2\cdot 3+1=6+1$$
111		6p1e7	$$⊢6+1=7$$
112	110 111	eqtri	$$⊢2\cdot 3+1=7$$
113		8t2e16	$$⊢8\cdot 2=16$$
114	76 90 113	mulcomli	$$⊢2\cdot 8=16$$
115	3 11 12 107 24 2 112 114	decmul2c	$$⊢2\cdot 38=76$$
116	5	dec0h	$$⊢5=05$$
117		eqid	$$⊢125=125$$
118		4cn	$$⊢4\in ℂ$$
119	118	addlidi	$$⊢0+4=4$$
120	17	dec0h	$$⊢4=04$$
121	119 120	eqtri	$$⊢0+4=04$$
122	91 92	eqtri	$$⊢0+2=02$$
123	118	mulridi	$$⊢4\cdot 1=4$$
124	123 45	oveq12i	$$⊢4\cdot 1+0+1=4+1$$
125	124 96	eqtri	$$⊢4\cdot 1+0+1=5$$
126		4t2e8	$$⊢4\cdot 2=8$$
127	126	oveq1i	$$⊢4\cdot 2+2=8+2$$
128		8p2e10	$$⊢8+2=10$$
129	127 128	eqtri	$$⊢4\cdot 2+2=10$$
130	2 3 22 3 52 122 17 22 2 125 129	decma2c	$$⊢4\cdot 12+0+2=50$$
131		5t4e20	$$⊢5\cdot 4=20$$
132	56 118 131	mulcomli	$$⊢4\cdot 5=20$$
133	3 22 17 132 119	decaddi	$$⊢4\cdot 5+4=24$$
134	4 5 22 17 117 121 17 17 3 130 133	decma2c	$$⊢4\cdot 125+0+4=504$$
135		9t4e36	$$⊢9\cdot 4=36$$
136	62 118 135	mulcomli	$$⊢4\cdot 9=36$$
137		6p5e11	$$⊢6+5=11$$
138	11 24 5 136 48 2 137	decaddci	$$⊢4\cdot 9+5=41$$
139	6 32 22 5 1 116 17 2 17 134 138	decma2c	$$⊢4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+5=5041$$
140		7t7e49	$$⊢7\cdot 7=49$$
141	17 96 140	decsucc	$$⊢7\cdot 7+1=50$$
142	37	mullidi	$$⊢1\cdot 7=7$$
143	142	oveq1i	$$⊢1\cdot 7+7=7+7$$
144		7p7e14	$$⊢7+7=14$$
145	143 144	eqtri	$$⊢1\cdot 7+7=14$$
146	15 2 15 33 15 17 2 141 145	decrmac	$$⊢71\cdot 7+7=504$$
147	16	nn0cni	$$⊢71\in ℂ$$
148	147	mulridi	$$⊢71\cdot 1=71$$
149	16 15 2 33 2 15 146 148	decmul2c	$$⊢71\cdot 71=5041$$
150	139 149	eqtr4i	$$⊢4\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+5=71\cdot 71$$
151	9 10 13 14 16 5 106 115 150	mod2xi	$$⊢2^{76}\mathrm{mod}N=5\mathrm{mod}N$$