Theorem 4001lem3

Description: Lemma for 4001prm . Calculate a power mod. In decimal, we calculate 2 ^ 1 0 0 0 = 2 ^ 8 0 0 x. 2 ^ 2 0 0 == 2 3 1 1 x. 9 0 2 = 5 2 1 N + 1 and finally 2 ^ ( N - 1 ) = ( 2 ^ 1 0 0 0 ) ^ 4 == 1 ^ 4 = 1 . (Contributed by Mario Carneiro, 3-Mar-2014) (Revised by Mario Carneiro, 20-Apr-2015) (Proof shortened by AV, 16-Sep-2021)

	Ref	Expression
Hypothesis	4001prm.1	$$⊢N=4001$$
Assertion	4001lem3	$$⊢2^{N-1}\mathrm{mod}N=1\mathrm{mod}N$$

Proof

Step	Hyp	Ref	Expression
1		4001prm.1	$$⊢N=4001$$
2		4nn0	$$⊢4\in {\mathbb{N}}_0$$
3		0nn0	$$⊢0\in {\mathbb{N}}_0$$
4	2 3	deccl	$$⊢40\in {\mathbb{N}}_0$$
5	4 3	deccl	$$⊢400\in {\mathbb{N}}_0$$
6		1nn	$$⊢1\in \mathbb{N}$$
7	5 6	decnncl	$$⊢4001\in \mathbb{N}$$
8	1 7	eqeltri	$$⊢N\in \mathbb{N}$$
9		2nn	$$⊢2\in \mathbb{N}$$
10		2nn0	$$⊢2\in {\mathbb{N}}_0$$
11	10 3	deccl	$$⊢20\in {\mathbb{N}}_0$$
12	11 3	deccl	$$⊢200\in {\mathbb{N}}_0$$
13	12 3	deccl	$$⊢2000\in {\mathbb{N}}_0$$
14		0z	$$⊢0\in \mathbb{Z}$$
15		1nn0	$$⊢1\in {\mathbb{N}}_0$$
16		10nn0	$$⊢10\in {\mathbb{N}}_0$$
17	16 3	deccl	$$⊢100\in {\mathbb{N}}_0$$
18	17 3	deccl	$$⊢1000\in {\mathbb{N}}_0$$
19		8nn0	$$⊢8\in {\mathbb{N}}_0$$
20	19 3	deccl	$$⊢80\in {\mathbb{N}}_0$$
21	20 3	deccl	$$⊢800\in {\mathbb{N}}_0$$
22		5nn0	$$⊢5\in {\mathbb{N}}_0$$
23	22 10	deccl	$$⊢52\in {\mathbb{N}}_0$$
24	23 15	deccl	$$⊢521\in {\mathbb{N}}_0$$
25	24	nn0zi	$$⊢521\in \mathbb{Z}$$
26		3nn0	$$⊢3\in {\mathbb{N}}_0$$
27	10 26	deccl	$$⊢23\in {\mathbb{N}}_0$$
28	27 15	deccl	$$⊢231\in {\mathbb{N}}_0$$
29	28 15	deccl	$$⊢2311\in {\mathbb{N}}_0$$
30		9nn0	$$⊢9\in {\mathbb{N}}_0$$
31	30 3	deccl	$$⊢90\in {\mathbb{N}}_0$$
32	31 10	deccl	$$⊢902\in {\mathbb{N}}_0$$
33	1	4001lem2	$$⊢2^{800}\mathrm{mod}N=2311\mathrm{mod}N$$
34	1	4001lem1	$$⊢2^{200}\mathrm{mod}N=902\mathrm{mod}N$$
35		eqid	$$⊢800=800$$
36		eqid	$$⊢200=200$$
37		eqid	$$⊢80=80$$
38		eqid	$$⊢20=20$$
39		8p2e10	$$⊢8+2=10$$
40		00id	$$⊢0+0=0$$
41	19 3 10 3 37 38 39 40	decadd	$$⊢80+20=100$$
42	20 3 11 3 35 36 41 40	decadd	$$⊢800+200=1000$$
43	15	dec0h	$$⊢1=01$$
44		eqid	$$⊢400=400$$
45	23	nn0cni	$$⊢52\in ℂ$$
46	45	addid2i	$$⊢0+52=52$$
47		eqid	$$⊢40=40$$
48		5cn	$$⊢5\in ℂ$$
49	48	addid1i	$$⊢5+0=5$$
50	22	dec0h	$$⊢5=05$$
51	49 50	eqtri	$$⊢5+0=05$$
52	40 3	eqeltri	$$⊢0+0\in {\mathbb{N}}_0$$
53		eqid	$$⊢521=521$$
54		eqid	$$⊢52=52$$
55		5t4e20	$$⊢5\cdot 4=20$$
56		4cn	$$⊢4\in ℂ$$
57		2cn	$$⊢2\in ℂ$$
58		4t2e8	$$⊢4\cdot 2=8$$
59	56 57 58	mulcomli	$$⊢2\cdot 4=8$$
60	2 22 10 54 55 59	decmul1	$$⊢52\cdot 4=208$$
61	56	mulid2i	$$⊢1\cdot 4=4$$
62	61 40	oveq12i	$$⊢1\cdot 4+0+0=4+0$$
63	56	addid1i	$$⊢4+0=4$$
64	62 63	eqtri	$$⊢1\cdot 4+0+0=4$$
65	23 15 52 53 2 60 64	decrmanc	$$⊢521\cdot 4+0+0=2084$$
66	24	nn0cni	$$⊢521\in ℂ$$
67	66	mul01i	$$⊢521\cdot 0=0$$
68	67	oveq1i	$$⊢521\cdot 0+5=0+5$$
69	48	addid2i	$$⊢0+5=5$$
70	68 69 50	3eqtri	$$⊢521\cdot 0+5=05$$
71	2 3 3 22 47 51 24 22 3 65 70	decma2c	$$⊢521\cdot 40+5+0=20845$$
72	67	oveq1i	$$⊢521\cdot 0+2=0+2$$
73	57	addid2i	$$⊢0+2=2$$
74	10	dec0h	$$⊢2=02$$
75	72 73 74	3eqtri	$$⊢521\cdot 0+2=02$$
76	4 3 22 10 44 46 24 10 3 71 75	decma2c	$$⊢521\cdot 400+0+52=208452$$
77	45	mulid1i	$$⊢52\cdot 1=52$$
78		ax-1cn	$$⊢1\in ℂ$$
79	78	mulid2i	$$⊢1\cdot 1=1$$
80	79	oveq1i	$$⊢1\cdot 1+1=1+1$$
81		1p1e2	$$⊢1+1=2$$
82	80 81	eqtri	$$⊢1\cdot 1+1=2$$
83	23 15 15 53 15 77 82	decrmanc	$$⊢521\cdot 1+1=522$$
84	5 15 3 15 1 43 24 10 23 76 83	decma2c	$$⊢521\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1=2084522$$
85		eqid	$$⊢902=902$$
86		6nn0	$$⊢6\in {\mathbb{N}}_0$$
87	2 86	deccl	$$⊢46\in {\mathbb{N}}_0$$
88	87 10	deccl	$$⊢462\in {\mathbb{N}}_0$$
89		eqid	$$⊢90=90$$
90		eqid	$$⊢462=462$$
91		eqid	$$⊢2311=2311$$
92	87	nn0cni	$$⊢46\in ℂ$$
93	92	addid1i	$$⊢46+0=46$$
94		4p1e5	$$⊢4+1=5$$
95	94 22	eqeltri	$$⊢4+1\in {\mathbb{N}}_0$$
96		eqid	$$⊢231=231$$
97		eqid	$$⊢23=23$$
98		9cn	$$⊢9\in ℂ$$
99		9t2e18	$$⊢9\cdot 2=18$$
100	98 57 99	mulcomli	$$⊢2\cdot 9=18$$
101	15 19 10 100 81 39	decaddci2	$$⊢2\cdot 9+2=20$$
102		7nn0	$$⊢7\in {\mathbb{N}}_0$$
103		7p1e8	$$⊢7+1=8$$
104		3cn	$$⊢3\in ℂ$$
105		9t3e27	$$⊢9\cdot 3=27$$
106	98 104 105	mulcomli	$$⊢3\cdot 9=27$$
107	10 102 103 106	decsuc	$$⊢3\cdot 9+1=28$$
108	10 26 15 97 30 19 10 101 107	decrmac	$$⊢23\cdot 9+1=208$$
109	98	mulid2i	$$⊢1\cdot 9=9$$
110	109 94	oveq12i	$$⊢1\cdot 9+4+1=9+5$$
111		9p5e14	$$⊢9+5=14$$
112	110 111	eqtri	$$⊢1\cdot 9+4+1=14$$
113	27 15 95 96 30 2 15 108 112	decrmac	$$⊢231\cdot 9+4+1=2084$$
114	109	oveq1i	$$⊢1\cdot 9+6=9+6$$
115		9p6e15	$$⊢9+6=15$$
116	114 115	eqtri	$$⊢1\cdot 9+6=15$$
117	28 15 2 86 91 93 30 22 15 113 116	decmac	$$⊢2311\cdot 9+46+0=20845$$
118	29	nn0cni	$$⊢2311\in ℂ$$
119	118	mul01i	$$⊢2311\cdot 0=0$$
120	119	oveq1i	$$⊢2311\cdot 0+2=0+2$$
121	120 73 74	3eqtri	$$⊢2311\cdot 0+2=02$$
122	30 3 87 10 89 90 29 10 3 117 121	decma2c	$$⊢2311\cdot 90+462=208452$$
123		2t2e4	$$⊢2\cdot 2=4$$
124		3t2e6	$$⊢3\cdot 2=6$$
125	10 10 26 97 123 124	decmul1	$$⊢23\cdot 2=46$$
126	57	mulid2i	$$⊢1\cdot 2=2$$
127	10 27 15 96 125 126	decmul1	$$⊢231\cdot 2=462$$
128	10 28 15 91 127 126	decmul1	$$⊢2311\cdot 2=4622$$
129	29 31 10 85 10 88 122 128	decmul2c	$$⊢2311\cdot 902=2084522$$
130	84 129	eqtr4i	$$⊢521\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1=2311\cdot 902$$
131	8 9 21 25 29 15 12 32 33 34 42 130	modxai	$$⊢2^{1000}\mathrm{mod}N=1\mathrm{mod}N$$
132	18	nn0cni	$$⊢1000\in ℂ$$
133		eqid	$$⊢1000=1000$$
134		eqid	$$⊢100=100$$
135	10	dec0u	$$⊢10\cdot 2=20$$
136	57	mul02i	$$⊢0\cdot 2=0$$
137	10 16 3 134 135 136	decmul1	$$⊢100\cdot 2=200$$
138	10 17 3 133 137 136	decmul1	$$⊢1000\cdot 2=2000$$
139	132 57 138	mulcomli	$$⊢2\cdot 1000=2000$$
140	8	nncni	$$⊢N\in ℂ$$
141	140	mul02i	$$⊢0\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=0$$
142	141	oveq1i	$$⊢0\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1=0+1$$
143	78	addid2i	$$⊢0+1=1$$
144	79 143	eqtr4i	$$⊢1\cdot 1=0+1$$
145	142 144	eqtr4i	$$⊢0\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1=1\cdot 1$$
146	8 9 18 14 15 15 131 139 145	mod2xi	$$⊢2^{2000}\mathrm{mod}N=1\mathrm{mod}N$$
147	13	nn0cni	$$⊢2000\in ℂ$$
148		eqid	$$⊢2000=2000$$
149	10 10 3 38 123 136	decmul1	$$⊢20\cdot 2=40$$
150	10 11 3 36 149 136	decmul1	$$⊢200\cdot 2=400$$
151	10 12 3 148 150 136	decmul1	$$⊢2000\cdot 2=4000$$
152	147 57 151	mulcomli	$$⊢2\cdot 2000=4000$$
153	5 3	deccl	$$⊢4000\in {\mathbb{N}}_0$$
154	153	nn0cni	$$⊢4000\in ℂ$$
155		eqid	$$⊢4000=4000$$
156	5 3 143 155	decsuc	$$⊢4000+1=4001$$
157	1 156	eqtr4i	$$⊢N=4000+1$$
158	154 78 157	mvrraddi	$$⊢N-1=4000$$
159	152 158	eqtr4i	$$⊢2\cdot 2000=N-1$$
160	8 9 13 14 15 15 146 159 145	mod2xi	$$⊢2^{N-1}\mathrm{mod}N=1\mathrm{mod}N$$