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