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 = ; ; ; 1 2 5 9
Assertion	1259lem2	|- ( ( 2 ^ ; 3 4 ) mod N ) = ( ; ; 8 7 0 mod N )

Proof

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