Theorem 4001lem3 15850

Description: Lemma for 4001prm 15852. 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.)

Hypothesis

Ref	Expression
4001prm.1	|- N = ;;; 4 0 0 1

Assertion

Ref	Expression
4001lem3	|- ( ( 2 ^ ( N - 1 ) ) mod N ) = ( 1 mod N )

Proof of Theorem 4001lem3

Step	Hyp	Ref	Expression
1		4001prm.1	. . 3 |- N = ;;; 4 0 0 1
2		4nn0 11311	. . . . . 6 |- 4 e. NN0
3		0nn0 11307	. . . . . 6 |- 0 e. NN0
4	2, 3	deccl 11512	. . . . 5 |- ; 4 0 e. NN0
5	4, 3	deccl 11512	. . . 4 |- ;; 4 0 0 e. NN0
6		1nn 11031	. . . 4 |- 1 e. NN
7	5, 6	decnncl 11518	. . 3 |- ;;; 4 0 0 1 e. NN
8	1, 7	eqeltri 2697	. 2 |- N e. NN
9		2nn 11185	. 2 |- 2 e. NN
10		2nn0 11309	. . . . 5 |- 2 e. NN0
11	10, 3	deccl 11512	. . . 4 |- ; 2 0 e. NN0
12	11, 3	deccl 11512	. . 3 |- ;; 2 0 0 e. NN0
13	12, 3	deccl 11512	. 2 |- ;;; 2 0 0 0 e. NN0
14		0z 11388	. 2 |- 0 e. ZZ
15		1nn0 11308	. 2 |- 1 e. NN0
16		10nn0 11516	. . . . 5 |- ; 1 0 e. NN0
17	16, 3	deccl 11512	. . . 4 |- ;; 1 0 0 e. NN0
18	17, 3	deccl 11512	. . 3 |- ;;; 1 0 0 0 e. NN0
19		8nn0 11315	. . . . . 6 |- 8 e. NN0
20	19, 3	deccl 11512	. . . . 5 |- ; 8 0 e. NN0
21	20, 3	deccl 11512	. . . 4 |- ;; 8 0 0 e. NN0
22		5nn0 11312	. . . . . . 7 |- 5 e. NN0
23	22, 10	deccl 11512	. . . . . 6 |- ; 5 2 e. NN0
24	23, 15	deccl 11512	. . . . 5 |- ;; 5 2 1 e. NN0
25	24	nn0zi 11402	. . . 4 |- ;; 5 2 1 e. ZZ
26		3nn0 11310	. . . . . . 7 |- 3 e. NN0
27	10, 26	deccl 11512	. . . . . 6 |- ; 2 3 e. NN0
28	27, 15	deccl 11512	. . . . 5 |- ;; 2 3 1 e. NN0
29	28, 15	deccl 11512	. . . 4 |- ;;; 2 3 1 1 e. NN0
30		9nn0 11316	. . . . . 6 |- 9 e. NN0
31	30, 3	deccl 11512	. . . . 5 |- ; 9 0 e. NN0
32	31, 10	deccl 11512	. . . 4 |- ;; 9 0 2 e. NN0
33	1	4001lem2 15849	. . . 4 |- ( ( 2 ^;; 8 0 0 ) mod N ) = (;;; 2 3 1 1 mod N )
34	1	4001lem1 15848	. . . 4 |- ( ( 2 ^;; 2 0 0 ) mod N ) = (;; 9 0 2 mod N )
35		eqid 2622	. . . . 5 |- ;; 8 0 0 = ;; 8 0 0
36		eqid 2622	. . . . 5 |- ;; 2 0 0 = ;; 2 0 0
37		eqid 2622	. . . . . 6 |- ; 8 0 = ; 8 0
38		eqid 2622	. . . . . 6 |- ; 2 0 = ; 2 0
39		8p2e10 11610	. . . . . 6 |- ( 8 + 2 ) = ; 1 0
40		00id 10211	. . . . . 6 |- ( 0 + 0 ) = 0
41	19, 3, 10, 3, 37, 38, 39, 40	decadd 11570	. . . . 5 |- (; 8 0 + ; 2 0 ) = ;; 1 0 0
42	20, 3, 11, 3, 35, 36, 41, 40	decadd 11570	. . . 4 |- (;; 8 0 0 + ;; 2 0 0 ) = ;;; 1 0 0 0
43	15	dec0h 11522	. . . . . 6 |- 1 = ; 0 1
44		eqid 2622	. . . . . . 7 |- ;; 4 0 0 = ;; 4 0 0
45	23	nn0cni 11304	. . . . . . . 8 |- ; 5 2 e. CC
46	45	addid2i 10224	. . . . . . 7 |- ( 0 + ; 5 2 ) = ; 5 2
47		eqid 2622	. . . . . . . 8 |- ; 4 0 = ; 4 0
48		5cn 11100	. . . . . . . . . 10 |- 5 e. CC
49	48	addid1i 10223	. . . . . . . . 9 |- ( 5 + 0 ) = 5
50	22	dec0h 11522	. . . . . . . . 9 |- 5 = ; 0 5
51	49, 50	eqtri 2644	. . . . . . . 8 |- ( 5 + 0 ) = ; 0 5
52	40, 3	eqeltri 2697	. . . . . . . . 9 |- ( 0 + 0 ) e. NN0
53		eqid 2622	. . . . . . . . 9 |- ;; 5 2 1 = ;; 5 2 1
54		eqid 2622	. . . . . . . . . 10 |- ; 5 2 = ; 5 2
55		5t4e20 11637	. . . . . . . . . 10 |- ( 5 x. 4 ) = ; 2 0
56		4cn 11098	. . . . . . . . . . 11 |- 4 e. CC
57		2cn 11091	. . . . . . . . . . 11 |- 2 e. CC
58		4t2e8 11181	. . . . . . . . . . 11 |- ( 4 x. 2 ) = 8
59	56, 57, 58	mulcomli 10047	. . . . . . . . . 10 |- ( 2 x. 4 ) = 8
60	2, 22, 10, 54, 19, 55, 59	decmul1 11585	. . . . . . . . 9 |- (; 5 2 x. 4 ) = ;; 2 0 8
61	56	mulid2i 10043	. . . . . . . . . . 11 |- ( 1 x. 4 ) = 4
62	61, 40	oveq12i 6662	. . . . . . . . . 10 |- ( ( 1 x. 4 ) + ( 0 + 0 ) ) = ( 4 + 0 )
63	56	addid1i 10223	. . . . . . . . . 10 |- ( 4 + 0 ) = 4
64	62, 63	eqtri 2644	. . . . . . . . 9 |- ( ( 1 x. 4 ) + ( 0 + 0 ) ) = 4
65	23, 15, 52, 53, 2, 60, 64	decrmanc 11576	. . . . . . . 8 |- ( (;; 5 2 1 x. 4 ) + ( 0 + 0 ) ) = ;;; 2 0 8 4
66	24	nn0cni 11304	. . . . . . . . . . 11 |- ;; 5 2 1 e. CC
67	66	mul01i 10226	. . . . . . . . . 10 |- (;; 5 2 1 x. 0 ) = 0
68	67	oveq1i 6660	. . . . . . . . 9 |- ( (;; 5 2 1 x. 0 ) + 5 ) = ( 0 + 5 )
69	48	addid2i 10224	. . . . . . . . 9 |- ( 0 + 5 ) = 5
70	68, 69, 50	3eqtri 2648	. . . . . . . 8 |- ( (;; 5 2 1 x. 0 ) + 5 ) = ; 0 5
71	2, 3, 3, 22, 47, 51, 24, 22, 3, 65, 70	decma2c 11568	. . . . . . 7 |- ( (;; 5 2 1 x. ; 4 0 ) + ( 5 + 0 ) ) = ;;;; 2 0 8 4 5
72	67	oveq1i 6660	. . . . . . . 8 |- ( (;; 5 2 1 x. 0 ) + 2 ) = ( 0 + 2 )
73	57	addid2i 10224	. . . . . . . 8 |- ( 0 + 2 ) = 2
74	10	dec0h 11522	. . . . . . . 8 |- 2 = ; 0 2
75	72, 73, 74	3eqtri 2648	. . . . . . 7 |- ( (;; 5 2 1 x. 0 ) + 2 ) = ; 0 2
76	4, 3, 22, 10, 44, 46, 24, 10, 3, 71, 75	decma2c 11568	. . . . . 6 |- ( (;; 5 2 1 x. ;; 4 0 0 ) + ( 0 + ; 5 2 ) ) = ;;;;; 2 0 8 4 5 2
77	45	mulid1i 10042	. . . . . . 7 |- (; 5 2 x. 1 ) = ; 5 2
78		ax-1cn 9994	. . . . . . . . . 10 |- 1 e. CC
79	78	mulid2i 10043	. . . . . . . . 9 |- ( 1 x. 1 ) = 1
80	79	oveq1i 6660	. . . . . . . 8 |- ( ( 1 x. 1 ) + 1 ) = ( 1 + 1 )
81		1p1e2 11134	. . . . . . . 8 |- ( 1 + 1 ) = 2
82	80, 81	eqtri 2644	. . . . . . 7 |- ( ( 1 x. 1 ) + 1 ) = 2
83	23, 15, 15, 53, 15, 77, 82	decrmanc 11576	. . . . . 6 |- ( (;; 5 2 1 x. 1 ) + 1 ) = ;; 5 2 2
84	5, 15, 3, 15, 1, 43, 24, 10, 23, 76, 83	decma2c 11568	. . . . 5 |- ( (;; 5 2 1 x. N ) + 1 ) = ;;;;;; 2 0 8 4 5 2 2
85		eqid 2622	. . . . . 6 |- ;; 9 0 2 = ;; 9 0 2
86		6nn0 11313	. . . . . . . 8 |- 6 e. NN0
87	2, 86	deccl 11512	. . . . . . 7 |- ; 4 6 e. NN0
88	87, 10	deccl 11512	. . . . . 6 |- ;; 4 6 2 e. NN0
89		eqid 2622	. . . . . . 7 |- ; 9 0 = ; 9 0
90		eqid 2622	. . . . . . 7 |- ;; 4 6 2 = ;; 4 6 2
91		eqid 2622	. . . . . . . 8 |- ;;; 2 3 1 1 = ;;; 2 3 1 1
92	87	nn0cni 11304	. . . . . . . . 9 |- ; 4 6 e. CC
93	92	addid1i 10223	. . . . . . . 8 |- (; 4 6 + 0 ) = ; 4 6
94		4p1e5 11154	. . . . . . . . . 10 |- ( 4 + 1 ) = 5
95	94, 22	eqeltri 2697	. . . . . . . . 9 |- ( 4 + 1 ) e. NN0
96		eqid 2622	. . . . . . . . 9 |- ;; 2 3 1 = ;; 2 3 1
97		eqid 2622	. . . . . . . . . 10 |- ; 2 3 = ; 2 3
98		9cn 11108	. . . . . . . . . . . 12 |- 9 e. CC
99		9t2e18 11663	. . . . . . . . . . . 12 |- ( 9 x. 2 ) = ; 1 8
100	98, 57, 99	mulcomli 10047	. . . . . . . . . . 11 |- ( 2 x. 9 ) = ; 1 8
101	15, 19, 10, 100, 81, 39	decaddci2 11581	. . . . . . . . . 10 |- ( ( 2 x. 9 ) + 2 ) = ; 2 0
102		7nn0 11314	. . . . . . . . . . 11 |- 7 e. NN0
103		7p1e8 11157	. . . . . . . . . . 11 |- ( 7 + 1 ) = 8
104		3cn 11095	. . . . . . . . . . . 12 |- 3 e. CC
105		9t3e27 11664	. . . . . . . . . . . 12 |- ( 9 x. 3 ) = ; 2 7
106	98, 104, 105	mulcomli 10047	. . . . . . . . . . 11 |- ( 3 x. 9 ) = ; 2 7
107	10, 102, 103, 106	decsuc 11535	. . . . . . . . . 10 |- ( ( 3 x. 9 ) + 1 ) = ; 2 8
108	10, 26, 15, 97, 30, 19, 10, 101, 107	decrmac 11577	. . . . . . . . 9 |- ( (; 2 3 x. 9 ) + 1 ) = ;; 2 0 8
109	98	mulid2i 10043	. . . . . . . . . . 11 |- ( 1 x. 9 ) = 9
110	109, 94	oveq12i 6662	. . . . . . . . . 10 |- ( ( 1 x. 9 ) + ( 4 + 1 ) ) = ( 9 + 5 )
111		9p5e14 11623	. . . . . . . . . 10 |- ( 9 + 5 ) = ; 1 4
112	110, 111	eqtri 2644	. . . . . . . . 9 |- ( ( 1 x. 9 ) + ( 4 + 1 ) ) = ; 1 4
113	27, 15, 95, 96, 30, 2, 15, 108, 112	decrmac 11577	. . . . . . . 8 |- ( (;; 2 3 1 x. 9 ) + ( 4 + 1 ) ) = ;;; 2 0 8 4
114	109	oveq1i 6660	. . . . . . . . 9 |- ( ( 1 x. 9 ) + 6 ) = ( 9 + 6 )
115		9p6e15 11624	. . . . . . . . 9 |- ( 9 + 6 ) = ; 1 5
116	114, 115	eqtri 2644	. . . . . . . 8 |- ( ( 1 x. 9 ) + 6 ) = ; 1 5
117	28, 15, 2, 86, 91, 93, 30, 22, 15, 113, 116	decmac 11566	. . . . . . 7 |- ( (;;; 2 3 1 1 x. 9 ) + (; 4 6 + 0 ) ) = ;;;; 2 0 8 4 5
118	29	nn0cni 11304	. . . . . . . . . 10 |- ;;; 2 3 1 1 e. CC
119	118	mul01i 10226	. . . . . . . . 9 |- (;;; 2 3 1 1 x. 0 ) = 0
120	119	oveq1i 6660	. . . . . . . 8 |- ( (;;; 2 3 1 1 x. 0 ) + 2 ) = ( 0 + 2 )
121	120, 73, 74	3eqtri 2648	. . . . . . 7 |- ( (;;; 2 3 1 1 x. 0 ) + 2 ) = ; 0 2
122	30, 3, 87, 10, 89, 90, 29, 10, 3, 117, 121	decma2c 11568	. . . . . 6 |- ( (;;; 2 3 1 1 x. ; 9 0 ) + ;; 4 6 2 ) = ;;;;; 2 0 8 4 5 2
123		2t2e4 11177	. . . . . . . . 9 |- ( 2 x. 2 ) = 4
124		3t2e6 11179	. . . . . . . . 9 |- ( 3 x. 2 ) = 6
125	10, 10, 26, 97, 86, 123, 124	decmul1 11585	. . . . . . . 8 |- (; 2 3 x. 2 ) = ; 4 6
126	57	mulid2i 10043	. . . . . . . 8 |- ( 1 x. 2 ) = 2
127	10, 27, 15, 96, 10, 125, 126	decmul1 11585	. . . . . . 7 |- (;; 2 3 1 x. 2 ) = ;; 4 6 2
128	10, 28, 15, 91, 10, 127, 126	decmul1 11585	. . . . . 6 |- (;;; 2 3 1 1 x. 2 ) = ;;; 4 6 2 2
129	29, 31, 10, 85, 10, 88, 122, 128	decmul2c 11589	. . . . 5 |- (;;; 2 3 1 1 x. ;; 9 0 2 ) = ;;;;;; 2 0 8 4 5 2 2
130	84, 129	eqtr4i 2647	. . . 4 |- ( (;; 5 2 1 x. N ) + 1 ) = (;;; 2 3 1 1 x. ;; 9 0 2 )
131	8, 9, 21, 25, 29, 15, 12, 32, 33, 34, 42, 130	modxai 15772	. . 3 |- ( ( 2 ^;;; 1 0 0 0 ) mod N ) = ( 1 mod N )
132	18	nn0cni 11304	. . . 4 |- ;;; 1 0 0 0 e. CC
133		eqid 2622	. . . . 5 |- ;;; 1 0 0 0 = ;;; 1 0 0 0
134		eqid 2622	. . . . . 6 |- ;; 1 0 0 = ;; 1 0 0
135	10	dec0u 11520	. . . . . 6 |- (; 1 0 x. 2 ) = ; 2 0
136	57	mul02i 10225	. . . . . 6 |- ( 0 x. 2 ) = 0
137	10, 16, 3, 134, 3, 135, 136	decmul1 11585	. . . . 5 |- (;; 1 0 0 x. 2 ) = ;; 2 0 0
138	10, 17, 3, 133, 3, 137, 136	decmul1 11585	. . . 4 |- (;;; 1 0 0 0 x. 2 ) = ;;; 2 0 0 0
139	132, 57, 138	mulcomli 10047	. . 3 |- ( 2 x. ;;; 1 0 0 0 ) = ;;; 2 0 0 0
140	8	nncni 11030	. . . . . 6 |- N e. CC
141	140	mul02i 10225	. . . . 5 |- ( 0 x. N ) = 0
142	141	oveq1i 6660	. . . 4 |- ( ( 0 x. N ) + 1 ) = ( 0 + 1 )
143	78	addid2i 10224	. . . . 5 |- ( 0 + 1 ) = 1
144	79, 143	eqtr4i 2647	. . . 4 |- ( 1 x. 1 ) = ( 0 + 1 )
145	142, 144	eqtr4i 2647	. . 3 |- ( ( 0 x. N ) + 1 ) = ( 1 x. 1 )
146	8, 9, 18, 14, 15, 15, 131, 139, 145	mod2xi 15773	. 2 |- ( ( 2 ^;;; 2 0 0 0 ) mod N ) = ( 1 mod N )
147	13	nn0cni 11304	. . . 4 |- ;;; 2 0 0 0 e. CC
148		eqid 2622	. . . . 5 |- ;;; 2 0 0 0 = ;;; 2 0 0 0
149	10, 10, 3, 38, 3, 123, 136	decmul1 11585	. . . . . 6 |- (; 2 0 x. 2 ) = ; 4 0
150	10, 11, 3, 36, 3, 149, 136	decmul1 11585	. . . . 5 |- (;; 2 0 0 x. 2 ) = ;; 4 0 0
151	10, 12, 3, 148, 3, 150, 136	decmul1 11585	. . . 4 |- (;;; 2 0 0 0 x. 2 ) = ;;; 4 0 0 0
152	147, 57, 151	mulcomli 10047	. . 3 |- ( 2 x. ;;; 2 0 0 0 ) = ;;; 4 0 0 0
153	5, 3	deccl 11512	. . . . 5 |- ;;; 4 0 0 0 e. NN0
154	153	nn0cni 11304	. . . 4 |- ;;; 4 0 0 0 e. CC
155		eqid 2622	. . . . . 6 |- ;;; 4 0 0 0 = ;;; 4 0 0 0
156	5, 3, 143, 155	decsuc 11535	. . . . 5 |- (;;; 4 0 0 0 + 1 ) = ;;; 4 0 0 1
157	1, 156	eqtr4i 2647	. . . 4 |- N = (;;; 4 0 0 0 + 1 )
158	154, 78, 157	mvrraddi 10298	. . 3 |- ( N - 1 ) = ;;; 4 0 0 0
159	152, 158	eqtr4i 2647	. 2 |- ( 2 x. ;;; 2 0 0 0 ) = ( N - 1 )
160	8, 9, 13, 14, 15, 15, 146, 159, 145	mod2xi 15773	1 |- ( ( 2 ^ ( N - 1 ) ) mod N ) = ( 1 mod N )

Syntax hints:   = wceq 1483  (class class class)co 6650   0cc0 9936   1c1 9937   + caddc 9939   x. cmul 9941   - cmin 10266   NNcn 11020   2c2 11070   3c3 11071   4c4 11072   5c5 11073   6c6 11074   7c7 11075   8c8 11076   9c9 11077   NN0cn0 11292  ;cdc 11493   mod cmo 12668   ^cexp 12860

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-pre-sup 10014

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-er 7742  df-en 7956  df-dom 7957  df-sdom 7958  df-sup 8348  df-inf 8349  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-3 11080  df-4 11081  df-5 11082  df-6 11083  df-7 11084  df-8 11085  df-9 11086  df-n0 11293  df-z 11378  df-dec 11494  df-uz 11688  df-rp 11833  df-fl 12593  df-mod 12669  df-seq 12802  df-exp 12861

This theorem is referenced by:  4001prm  15852