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