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 = ; ; ; 1 2 5 9
Assertion	1259lem3	|- ( ( 2 ^ ; 7 6 ) mod N ) = ( 5 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		3nn0	|- 3 e. NN0
12		8nn0	|- 8 e. NN0
13	11 12	deccl	|- ; 3 8 e. NN0
14		4z	|- 4 e. ZZ
15		7nn0	|- 7 e. NN0
16	15 2	deccl	|- ; 7 1 e. NN0
17		4nn0	|- 4 e. NN0
18	11 17	deccl	|- ; 3 4 e. NN0
19	2 2	deccl	|- ; 1 1 e. NN0
20	19	nn0zi	|- ; 1 1 e. ZZ
21	12 15	deccl	|- ; 8 7 e. NN0
22		0nn0	|- 0 e. NN0
23	21 22	deccl	|- ; ; 8 7 0 e. NN0
24		6nn0	|- 6 e. NN0
25	2 24	deccl	|- ; 1 6 e. NN0
26	1	1259lem2	|- ( ( 2 ^ ; 3 4 ) mod N ) = ( ; ; 8 7 0 mod N )
27		2exp4	|- ( 2 ^ 4 ) = ; 1 6
28	27	oveq1i	|- ( ( 2 ^ 4 ) mod N ) = ( ; 1 6 mod N )
29		eqid	|- ; 3 4 = ; 3 4
30		4p4e8	|- ( 4 + 4 ) = 8
31	11 17 17 29 30	decaddi	|- ( ; 3 4 + 4 ) = ; 3 8
32		9nn0	|- 9 e. NN0
33		eqid	|- ; 7 1 = ; 7 1
34		10nn0	|- ; 1 0 e. NN0
35		eqid	|- ; 1 1 = ; 1 1
36	34	nn0cni	|- ; 1 0 e. CC
37		7cn	|- 7 e. CC
38		dec10p	|- ( ; 1 0 + 7 ) = ; 1 7
39	36 37 38	addcomli	|- ( 7 + ; 1 0 ) = ; 1 7
40	2 11	deccl	|- ; 1 3 e. NN0
41	6	nn0cni	|- ; ; 1 2 5 e. CC
42	41	mulid2i	|- ( 1 x. ; ; 1 2 5 ) = ; ; 1 2 5
43	2	dec0h	|- 1 = ; 0 1
44		eqid	|- ; 1 3 = ; 1 3
45		0p1e1	|- ( 0 + 1 ) = 1
46		3cn	|- 3 e. CC
47		ax-1cn	|- 1 e. CC
48		3p1e4	|- ( 3 + 1 ) = 4
49	46 47 48	addcomli	|- ( 1 + 3 ) = 4
50	22 2 2 11 43 44 45 49	decadd	|- ( 1 + ; 1 3 ) = ; 1 4
51		2p1e3	|- ( 2 + 1 ) = 3
52		eqid	|- ; 1 2 = ; 1 2
53	2 3 51 52	decsuc	|- ( ; 1 2 + 1 ) = ; 1 3
54		5p4e9	|- ( 5 + 4 ) = 9
55	4 5 2 17 42 50 53 54	decadd	|- ( ( 1 x. ; ; 1 2 5 ) + ( 1 + ; 1 3 ) ) = ; ; 1 3 9
56		5cn	|- 5 e. CC
57		7p5e12	|- ( 7 + 5 ) = ; 1 2
58	37 56 57	addcomli	|- ( 5 + 7 ) = ; 1 2
59	4 5 15 42 53 3 58	decaddci	|- ( ( 1 x. ; ; 1 2 5 ) + 7 ) = ; ; 1 3 2
60	2 2 2 15 35 39 6 3 40 55 59	decmac	|- ( ( ; 1 1 x. ; ; 1 2 5 ) + ( 7 + ; 1 0 ) ) = ; ; ; 1 3 9 2
61		9p1e10	|- ( 9 + 1 ) = ; 1 0
62		9cn	|- 9 e. CC
63	19	nn0cni	|- ; 1 1 e. CC
64		9t11e99	|- ( 9 x. ; 1 1 ) = ; 9 9
65	62 63 64	mulcomli	|- ( ; 1 1 x. 9 ) = ; 9 9
66	32 61 65	decsucc	|- ( ( ; 1 1 x. 9 ) + 1 ) = ; ; 1 0 0
67	6 32 15 2 1 33 19 22 34 60 66	decma2c	|- ( ( ; 1 1 x. N ) + ; 7 1 ) = ; ; ; ; 1 3 9 2 0
68		eqid	|- ; 1 6 = ; 1 6
69	5 3	deccl	|- ; 5 2 e. NN0
70	69 3	deccl	|- ; ; 5 2 2 e. NN0
71		eqid	|- ; ; 8 7 0 = ; ; 8 7 0
72		eqid	|- ; ; 5 2 2 = ; ; 5 2 2
73		eqid	|- ; 8 7 = ; 8 7
74	69	nn0cni	|- ; 5 2 e. CC
75	74	addid1i	|- ( ; 5 2 + 0 ) = ; 5 2
76		8cn	|- 8 e. CC
77	76	mulid1i	|- ( 8 x. 1 ) = 8
78	56	addid1i	|- ( 5 + 0 ) = 5
79	77 78	oveq12i	|- ( ( 8 x. 1 ) + ( 5 + 0 ) ) = ( 8 + 5 )
80		8p5e13	|- ( 8 + 5 ) = ; 1 3
81	79 80	eqtri	|- ( ( 8 x. 1 ) + ( 5 + 0 ) ) = ; 1 3
82	37	mulid1i	|- ( 7 x. 1 ) = 7
83	82	oveq1i	|- ( ( 7 x. 1 ) + 2 ) = ( 7 + 2 )
84		7p2e9	|- ( 7 + 2 ) = 9
85	32	dec0h	|- 9 = ; 0 9
86	83 84 85	3eqtri	|- ( ( 7 x. 1 ) + 2 ) = ; 0 9
87	12 15 5 3 73 75 2 32 22 81 86	decmac	|- ( ( ; 8 7 x. 1 ) + ( ; 5 2 + 0 ) ) = ; ; 1 3 9
88	47	mul02i	|- ( 0 x. 1 ) = 0
89	88	oveq1i	|- ( ( 0 x. 1 ) + 2 ) = ( 0 + 2 )
90		2cn	|- 2 e. CC
91	90	addid2i	|- ( 0 + 2 ) = 2
92	3	dec0h	|- 2 = ; 0 2
93	89 91 92	3eqtri	|- ( ( 0 x. 1 ) + 2 ) = ; 0 2
94	21 22 69 3 71 72 2 3 22 87 93	decmac	|- ( ( ; ; 8 7 0 x. 1 ) + ; ; 5 2 2 ) = ; ; ; 1 3 9 2
95		8t6e48	|- ( 8 x. 6 ) = ; 4 8
96		4p1e5	|- ( 4 + 1 ) = 5
97		8p4e12	|- ( 8 + 4 ) = ; 1 2
98	17 12 17 95 96 3 97	decaddci	|- ( ( 8 x. 6 ) + 4 ) = ; 5 2
99		7t6e42	|- ( 7 x. 6 ) = ; 4 2
100	24 12 15 73 3 17 98 99	decmul1c	|- ( ; 8 7 x. 6 ) = ; ; 5 2 2
101		6cn	|- 6 e. CC
102	101	mul02i	|- ( 0 x. 6 ) = 0
103	24 21 22 71 100 102	decmul1	|- ( ; ; 8 7 0 x. 6 ) = ; ; ; 5 2 2 0
104	23 2 24 68 22 70 94 103	decmul2c	|- ( ; ; 8 7 0 x. ; 1 6 ) = ; ; ; ; 1 3 9 2 0
105	67 104	eqtr4i	|- ( ( ; 1 1 x. N ) + ; 7 1 ) = ( ; ; 8 7 0 x. ; 1 6 )
106	9 10 18 20 23 16 17 25 26 28 31 105	modxai	|- ( ( 2 ^ ; 3 8 ) mod N ) = ( ; 7 1 mod N )
107		eqid	|- ; 3 8 = ; 3 8
108		3t2e6	|- ( 3 x. 2 ) = 6
109	46 90 108	mulcomli	|- ( 2 x. 3 ) = 6
110	109	oveq1i	|- ( ( 2 x. 3 ) + 1 ) = ( 6 + 1 )
111		6p1e7	|- ( 6 + 1 ) = 7
112	110 111	eqtri	|- ( ( 2 x. 3 ) + 1 ) = 7
113		8t2e16	|- ( 8 x. 2 ) = ; 1 6
114	76 90 113	mulcomli	|- ( 2 x. 8 ) = ; 1 6
115	3 11 12 107 24 2 112 114	decmul2c	|- ( 2 x. ; 3 8 ) = ; 7 6
116	5	dec0h	|- 5 = ; 0 5
117		eqid	|- ; ; 1 2 5 = ; ; 1 2 5
118		4cn	|- 4 e. CC
119	118	addid2i	|- ( 0 + 4 ) = 4
120	17	dec0h	|- 4 = ; 0 4
121	119 120	eqtri	|- ( 0 + 4 ) = ; 0 4
122	91 92	eqtri	|- ( 0 + 2 ) = ; 0 2
123	118	mulid1i	|- ( 4 x. 1 ) = 4
124	123 45	oveq12i	|- ( ( 4 x. 1 ) + ( 0 + 1 ) ) = ( 4 + 1 )
125	124 96	eqtri	|- ( ( 4 x. 1 ) + ( 0 + 1 ) ) = 5
126		4t2e8	|- ( 4 x. 2 ) = 8
127	126	oveq1i	|- ( ( 4 x. 2 ) + 2 ) = ( 8 + 2 )
128		8p2e10	|- ( 8 + 2 ) = ; 1 0
129	127 128	eqtri	|- ( ( 4 x. 2 ) + 2 ) = ; 1 0
130	2 3 22 3 52 122 17 22 2 125 129	decma2c	|- ( ( 4 x. ; 1 2 ) + ( 0 + 2 ) ) = ; 5 0
131		5t4e20	|- ( 5 x. 4 ) = ; 2 0
132	56 118 131	mulcomli	|- ( 4 x. 5 ) = ; 2 0
133	3 22 17 132 119	decaddi	|- ( ( 4 x. 5 ) + 4 ) = ; 2 4
134	4 5 22 17 117 121 17 17 3 130 133	decma2c	|- ( ( 4 x. ; ; 1 2 5 ) + ( 0 + 4 ) ) = ; ; 5 0 4
135		9t4e36	|- ( 9 x. 4 ) = ; 3 6
136	62 118 135	mulcomli	|- ( 4 x. 9 ) = ; 3 6
137		6p5e11	|- ( 6 + 5 ) = ; 1 1
138	11 24 5 136 48 2 137	decaddci	|- ( ( 4 x. 9 ) + 5 ) = ; 4 1
139	6 32 22 5 1 116 17 2 17 134 138	decma2c	|- ( ( 4 x. N ) + 5 ) = ; ; ; 5 0 4 1
140		7t7e49	|- ( 7 x. 7 ) = ; 4 9
141	17 96 140	decsucc	|- ( ( 7 x. 7 ) + 1 ) = ; 5 0
142	37	mulid2i	|- ( 1 x. 7 ) = 7
143	142	oveq1i	|- ( ( 1 x. 7 ) + 7 ) = ( 7 + 7 )
144		7p7e14	|- ( 7 + 7 ) = ; 1 4
145	143 144	eqtri	|- ( ( 1 x. 7 ) + 7 ) = ; 1 4
146	15 2 15 33 15 17 2 141 145	decrmac	|- ( ( ; 7 1 x. 7 ) + 7 ) = ; ; 5 0 4
147	16	nn0cni	|- ; 7 1 e. CC
148	147	mulid1i	|- ( ; 7 1 x. 1 ) = ; 7 1
149	16 15 2 33 2 15 146 148	decmul2c	|- ( ; 7 1 x. ; 7 1 ) = ; ; ; 5 0 4 1
150	139 149	eqtr4i	|- ( ( 4 x. N ) + 5 ) = ( ; 7 1 x. ; 7 1 )
151	9 10 13 14 16 5 106 115 150	mod2xi	|- ( ( 2 ^ ; 7 6 ) mod N ) = ( 5 mod N )