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		1nn0	|- 1 e. NN0
3		2nn0	|- 2 e. NN0
4	2 3	deccl	|- ; 1 2 e. NN0
5		5nn0	|- 5 e. NN0
6	4 5	deccl	|- ; ; 1 2 5 e. NN0
7		9nn	|- 9 e. NN
8	6 7	decnncl	|- ; ; ; 1 2 5 9 e. NN
9	1 8	eqeltri	|- N e. NN
10		2nn	|- 2 e. NN
11		7nn0	|- 7 e. NN0
12	2 11	deccl	|- ; 1 7 e. NN0
13		4nn0	|- 4 e. NN0
14	2 13	deccl	|- ; 1 4 e. NN0
15	14	nn0zi	|- ; 1 4 e. ZZ
16		3nn0	|- 3 e. NN0
17	2 16	deccl	|- ; 1 3 e. NN0
18		6nn0	|- 6 e. NN0
19	17 18	deccl	|- ; ; 1 3 6 e. NN0
20		8nn0	|- 8 e. NN0
21	20 11	deccl	|- ; 8 7 e. NN0
22		0nn0	|- 0 e. NN0
23	21 22	deccl	|- ; ; 8 7 0 e. NN0
24	1	1259lem1	|- ( ( 2 ^ ; 1 7 ) mod N ) = ( ; ; 1 3 6 mod N )
25		eqid	|- ; 1 7 = ; 1 7
26		2cn	|- 2 e. CC
27	26	mulid1i	|- ( 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	3 2 11 25 13 2 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	20 11 2 3 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	13	dec0h	|- 4 = ; 0 4
50	48 49	eqtri	|- ( 1 + 3 ) = ; 0 4
51	46	mulid1i	|- ( 1 x. 1 ) = 1
52		00id	|- ( 0 + 0 ) = 0
53	51 52	oveq12i	|- ( ( 1 x. 1 ) + ( 0 + 0 ) ) = ( 1 + 0 )
54	46	addid1i	|- ( 1 + 0 ) = 1
55	53 54	eqtri	|- ( ( 1 x. 1 ) + ( 0 + 0 ) ) = 1
56		4cn	|- 4 e. CC
57	56	mulid1i	|- ( 4 x. 1 ) = 4
58	57	oveq1i	|- ( ( 4 x. 1 ) + 4 ) = ( 4 + 4 )
59		4p4e8	|- ( 4 + 4 ) = 8
60	20	dec0h	|- 8 = ; 0 8
61	58 59 60	3eqtri	|- ( ( 4 x. 1 ) + 4 ) = ; 0 8
62	2 13 22 13 44 50 2 20 22 55 61	decmac	|- ( ( ; 1 4 x. 1 ) + ( 1 + 3 ) ) = ; 1 8
63	18	dec0h	|- 6 = ; 0 6
64	26	mulid2i	|- ( 1 x. 2 ) = 2
65	46	addid2i	|- ( 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	2 13 22 18 44 63 3 13 2 67 71	decmac	|- ( ( ; 1 4 x. 2 ) + 6 ) = ; 3 4
73	2 3 2 18 39 43 14 13 16 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	mulid2i	|- ( 1 x. 5 ) = 5
77	26	addid2i	|- ( 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	addid2i	|- ( 0 + 9 ) = 9
85	3 22 35 82 84	decaddi	|- ( ( 4 x. 5 ) + 9 ) = ; 2 9
86	2 13 22 35 44 74 5 35 3 80 85	decmac	|- ( ( ; 1 4 x. 5 ) + 9 ) = ; 7 9
87	4 5 35 35 37 42 14 35 11 73 86	decma2c	|- ( ( ; 1 4 x. ; ; 1 2 5 ) + ( ; 8 7 + ; 1 2 ) ) = ; ; ; 1 8 4 9
88	83	mulid2i	|- ( 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 2 13 44 18 16 91 93	decmul1c	|- ( ; 1 4 x. 9 ) = ; ; 1 2 6
95	94	oveq1i	|- ( ( ; 1 4 x. 9 ) + 0 ) = ( ; ; 1 2 6 + 0 )
96	4 18	deccl	|- ; ; 1 2 6 e. NN0
97	96	nn0cni	|- ; ; 1 2 6 e. CC
98	97	addid1i	|- ( ; ; 1 2 6 + 0 ) = ; ; 1 2 6
99	95 98	eqtri	|- ( ( ; 1 4 x. 9 ) + 0 ) = ; ; 1 2 6
100	6 35 21 22 1 36 14 18 4 87 99	decma2c	|- ( ( ; 1 4 x. N ) + ; ; 8 7 0 ) = ; ; ; ; 1 8 4 9 6
101		eqid	|- ; ; 1 3 6 = ; ; 1 3 6
102	20 2	deccl	|- ; 8 1 e. NN0
103		eqid	|- ; 1 3 = ; 1 3
104		eqid	|- ; 8 1 = ; 8 1
105	13 22	deccl	|- ; 4 0 e. NN0
106		eqid	|- ; 4 0 = ; 4 0
107	56	addid2i	|- ( 0 + 4 ) = 4
108		8cn	|- 8 e. CC
109	108	addid1i	|- ( 8 + 0 ) = 8
110	22 20 13 22 60 106 107 109	decadd	|- ( 8 + ; 4 0 ) = ; 4 8
111		4p1e5	|- ( 4 + 1 ) = 5
112	5	dec0h	|- 5 = ; 0 5
113	111 112	eqtri	|- ( 4 + 1 ) = ; 0 5
114	45	mulid1i	|- ( 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	2 16 22 5 103 113 2 20 22 55 118	decmac	|- ( ( ; 1 3 x. 1 ) + ( 4 + 1 ) ) = ; 1 8
120		6cn	|- 6 e. CC
121	120	mulid1i	|- ( 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	17 18 13 20 101 110 2 13 2 119 124	decmac	|- ( ( ; ; 1 3 6 x. 1 ) + ( 8 + ; 4 0 ) ) = ; ; 1 8 4
126	2	dec0h	|- 1 = ; 0 1
127	65 126	eqtri	|- ( 0 + 1 ) = ; 0 1
128	45	mulid2i	|- ( 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	2 16 22 2 103 127 16 22 2 130 134	decmac	|- ( ( ; 1 3 x. 3 ) + ( 0 + 1 ) ) = ; 4 0
136		6t3e18	|- ( 6 x. 3 ) = ; 1 8
137	2 20 2 136 40	decaddi	|- ( ( 6 x. 3 ) + 1 ) = ; 1 9
138	17 18 22 2 101 126 16 35 2 135 137	decmac	|- ( ( ; ; 1 3 6 x. 3 ) + 1 ) = ; ; 4 0 9
139	2 16 20 2 103 104 19 35 105 125 138	decma2c	|- ( ( ; ; 1 3 6 x. ; 1 3 ) + ; 8 1 ) = ; ; ; 1 8 4 9
140	16	dec0h	|- 3 = ; 0 3
141	120	mulid2i	|- ( 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	2 20 16 145 146 2 147	decaddci	|- ( ( 3 x. 6 ) + 3 ) = ; 2 1
149	2 16 22 16 103 140 18 2 3 144 148	decmac	|- ( ( ; 1 3 x. 6 ) + 3 ) = ; 8 1
150		6t6e36	|- ( 6 x. 6 ) = ; 3 6
151	18 17 18 101 18 16 149 150	decmul1c	|- ( ; ; 1 3 6 x. 6 ) = ; ; 8 1 6
152	19 17 18 101 18 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	9 10 12 15 19 23 24 34 153	mod2xi	|- ( ( 2 ^ ; 3 4 ) mod N ) = ( ; ; 8 7 0 mod N )