Theorem 2exp340mod341

Description: Eight to the eighth power modulo nine is one. (Contributed by AV, 3-Jun-2023)

	Ref	Expression
Assertion	2exp340mod341	$$⊢2^{340}\mathrm{mod}341=1$$

Proof

Step	Hyp	Ref	Expression
1		3nn0	$$⊢3\in {\mathbb{N}}_0$$
2		4nn0	$$⊢4\in {\mathbb{N}}_0$$
3	1 2	deccl	$$⊢34\in {\mathbb{N}}_0$$
4		1nn	$$⊢1\in \mathbb{N}$$
5	3 4	decnncl	$$⊢341\in \mathbb{N}$$
6		2nn	$$⊢2\in \mathbb{N}$$
7		1nn0	$$⊢1\in {\mathbb{N}}_0$$
8		7nn0	$$⊢7\in {\mathbb{N}}_0$$
9	7 8	deccl	$$⊢17\in {\mathbb{N}}_0$$
10		0nn0	$$⊢0\in {\mathbb{N}}_0$$
11	9 10	deccl	$$⊢170\in {\mathbb{N}}_0$$
12		0z	$$⊢0\in \mathbb{Z}$$
13		8nn0	$$⊢8\in {\mathbb{N}}_0$$
14		5nn0	$$⊢5\in {\mathbb{N}}_0$$
15	13 14	deccl	$$⊢85\in {\mathbb{N}}_0$$
16		3z	$$⊢3\in \mathbb{Z}$$
17		2nn0	$$⊢2\in {\mathbb{N}}_0$$
18	1 17	deccl	$$⊢32\in {\mathbb{N}}_0$$
19	13 2	deccl	$$⊢84\in {\mathbb{N}}_0$$
20		6nn0	$$⊢6\in {\mathbb{N}}_0$$
21	7 20	deccl	$$⊢16\in {\mathbb{N}}_0$$
22	2 17	deccl	$$⊢42\in {\mathbb{N}}_0$$
23	17 7	deccl	$$⊢21\in {\mathbb{N}}_0$$
24	17 10	deccl	$$⊢20\in {\mathbb{N}}_0$$
25	7 10	deccl	$$⊢10\in {\mathbb{N}}_0$$
26		2exp5	$$⊢2^5=32$$
27	26	oveq1i	$$⊢2^5\mathrm{mod}341=32\mathrm{mod}341$$
28		5cn	$$⊢5\in ℂ$$
29		2cn	$$⊢2\in ℂ$$
30		5t2e10	$$⊢5\cdot 2=10$$
31	28 29 30	mulcomli	$$⊢2\cdot 5=10$$
32	25 17	deccl	$$⊢102\in {\mathbb{N}}_0$$
33		3p1e4	$$⊢3+1=4$$
34		eqid	$$⊢1023=1023$$
35	32 1 33 34	decsuc	$$⊢1023+1=1024$$
36	1 3 7	decmulnc	Could not format ( 3 x. ; ; 3 4 1 ) = ; ( 3 x. ; 3 4 ) ( 3 x. 1 ) : No typesetting found for |- ( 3 x. ; ; 3 4 1 ) = ; ( 3 x. ; 3 4 ) ( 3 x. 1 ) with typecode |-
37		eqid	$$⊢34=34$$
38		3t3e9	$$⊢3\cdot 3=9$$
39	38	oveq1i	$$⊢3\cdot 3+1=9+1$$
40		9p1e10	$$⊢9+1=10$$
41	39 40	eqtri	$$⊢3\cdot 3+1=10$$
42		4cn	$$⊢4\in ℂ$$
43		3cn	$$⊢3\in ℂ$$
44		4t3e12	$$⊢4\cdot 3=12$$
45	42 43 44	mulcomli	$$⊢3\cdot 4=12$$
46	1 1 2 37 17 7 41 45	decmul2c	$$⊢3\cdot 34=102$$
47	43	mulridi	$$⊢3\cdot 1=3$$
48	46 47	deceq12i	Could not format ; ( 3 x. ; 3 4 ) ( 3 x. 1 ) = ; ; ; 1 0 2 3 : No typesetting found for |- ; ( 3 x. ; 3 4 ) ( 3 x. 1 ) = ; ; ; 1 0 2 3 with typecode |-
49	36 48	eqtri	$$⊢3\cdot 341=1023$$
50	49	oveq1i	$$⊢3\cdot 341+1=1023+1$$
51		eqid	$$⊢32=32$$
52	1 1 17	decmulnc	Could not format ( 3 x. ; 3 2 ) = ; ( 3 x. 3 ) ( 3 x. 2 ) : No typesetting found for |- ( 3 x. ; 3 2 ) = ; ( 3 x. 3 ) ( 3 x. 2 ) with typecode |-
53	52	oveq1i	Could not format ( ( 3 x. ; 3 2 ) + 6 ) = ( ; ( 3 x. 3 ) ( 3 x. 2 ) + 6 ) : No typesetting found for |- ( ( 3 x. ; 3 2 ) + 6 ) = ( ; ( 3 x. 3 ) ( 3 x. 2 ) + 6 ) with typecode |-
54		9nn0	$$⊢9\in {\mathbb{N}}_0$$
55		3t2e6	$$⊢3\cdot 2=6$$
56	38 55	deceq12i	Could not format ; ( 3 x. 3 ) ( 3 x. 2 ) = ; 9 6 : No typesetting found for |- ; ( 3 x. 3 ) ( 3 x. 2 ) = ; 9 6 with typecode |-
57		6p6e12	$$⊢6+6=12$$
58	54 20 20 56 40 17 57	decaddci	Could not format ( ; ( 3 x. 3 ) ( 3 x. 2 ) + 6 ) = ; ; 1 0 2 : No typesetting found for |- ( ; ( 3 x. 3 ) ( 3 x. 2 ) + 6 ) = ; ; 1 0 2 with typecode |-
59	53 58	eqtri	$$⊢3\cdot 32+6=102$$
60	17 1 17	decmulnc	Could not format ( 2 x. ; 3 2 ) = ; ( 2 x. 3 ) ( 2 x. 2 ) : No typesetting found for |- ( 2 x. ; 3 2 ) = ; ( 2 x. 3 ) ( 2 x. 2 ) with typecode |-
61	43 29 55	mulcomli	$$⊢2\cdot 3=6$$
62		2t2e4	$$⊢2\cdot 2=4$$
63	61 62	deceq12i	Could not format ; ( 2 x. 3 ) ( 2 x. 2 ) = ; 6 4 : No typesetting found for |- ; ( 2 x. 3 ) ( 2 x. 2 ) = ; 6 4 with typecode |-
64	60 63	eqtri	$$⊢2\cdot 32=64$$
65	18 1 17 51 2 20 59 64	decmul1c	$$⊢32\cdot 32=1024$$
66	35 50 65	3eqtr4i	$$⊢3\cdot 341+1=32\cdot 32$$
67	5 6 14 16 18 7 27 31 66	mod2xi	$$⊢2^{10}\mathrm{mod}341=1\mathrm{mod}341$$
68	17 7 10	decmulnc	Could not format ( 2 x. ; 1 0 ) = ; ( 2 x. 1 ) ( 2 x. 0 ) : No typesetting found for |- ( 2 x. ; 1 0 ) = ; ( 2 x. 1 ) ( 2 x. 0 ) with typecode |-
69	29	mulridi	$$⊢2\cdot 1=2$$
70		2t0e0	$$⊢2\cdot 0=0$$
71	69 70	deceq12i	Could not format ; ( 2 x. 1 ) ( 2 x. 0 ) = ; 2 0 : No typesetting found for |- ; ( 2 x. 1 ) ( 2 x. 0 ) = ; 2 0 with typecode |-
72	68 71	eqtri	$$⊢2\cdot 10=20$$
73		0p1e1	$$⊢0+1=1$$
74	5	nncni	$$⊢341\in ℂ$$
75	74	mul02i	$$⊢0\cdot 341=0$$
76	75	oveq1i	$$⊢0\cdot 341+1=0+1$$
77		1t1e1	$$⊢1\cdot 1=1$$
78	73 76 77	3eqtr4i	$$⊢0\cdot 341+1=1\cdot 1$$
79	5 6 25 12 7 7 67 72 78	mod2xi	$$⊢2^{20}\mathrm{mod}341=1\mathrm{mod}341$$
80		eqid	$$⊢20=20$$
81	17 10 73 80	decsuc	$$⊢20+1=21$$
82	29	addlidi	$$⊢0+2=2$$
83	75	oveq1i	$$⊢0\cdot 341+2=0+2$$
84	29	mullidi	$$⊢1\cdot 2=2$$
85	82 83 84	3eqtr4i	$$⊢0\cdot 341+2=1\cdot 2$$
86	5 6 24 12 7 17 79 81 85	modxp1i	$$⊢2^{21}\mathrm{mod}341=2\mathrm{mod}341$$
87	17 17 7	decmulnc	Could not format ( 2 x. ; 2 1 ) = ; ( 2 x. 2 ) ( 2 x. 1 ) : No typesetting found for |- ( 2 x. ; 2 1 ) = ; ( 2 x. 2 ) ( 2 x. 1 ) with typecode |-
88	62 69	deceq12i	Could not format ; ( 2 x. 2 ) ( 2 x. 1 ) = ; 4 2 : No typesetting found for |- ; ( 2 x. 2 ) ( 2 x. 1 ) = ; 4 2 with typecode |-
89	87 88	eqtri	$$⊢2\cdot 21=42$$
90	42	addlidi	$$⊢0+4=4$$
91	75	oveq1i	$$⊢0\cdot 341+4=0+4$$
92	90 91 62	3eqtr4i	$$⊢0\cdot 341+4=2\cdot 2$$
93	5 6 23 12 17 2 86 89 92	mod2xi	$$⊢2^{42}\mathrm{mod}341=4\mathrm{mod}341$$
94	17 2 17	decmulnc	Could not format ( 2 x. ; 4 2 ) = ; ( 2 x. 4 ) ( 2 x. 2 ) : No typesetting found for |- ( 2 x. ; 4 2 ) = ; ( 2 x. 4 ) ( 2 x. 2 ) with typecode |-
95		4t2e8	$$⊢4\cdot 2=8$$
96	42 29 95	mulcomli	$$⊢2\cdot 4=8$$
97	96 62	deceq12i	Could not format ; ( 2 x. 4 ) ( 2 x. 2 ) = ; 8 4 : No typesetting found for |- ; ( 2 x. 4 ) ( 2 x. 2 ) = ; 8 4 with typecode |-
98	94 97	eqtri	$$⊢2\cdot 42=84$$
99	21	nn0cni	$$⊢16\in ℂ$$
100	99	addlidi	$$⊢0+16=16$$
101	75	oveq1i	$$⊢0\cdot 341+16=0+16$$
102		4t4e16	$$⊢4\cdot 4=16$$
103	100 101 102	3eqtr4i	$$⊢0\cdot 341+16=4\cdot 4$$
104	5 6 22 12 2 21 93 98 103	mod2xi	$$⊢2^{84}\mathrm{mod}341=16\mathrm{mod}341$$
105		4p1e5	$$⊢4+1=5$$
106		eqid	$$⊢84=84$$
107	13 2 105 106	decsuc	$$⊢84+1=85$$
108	18	nn0cni	$$⊢32\in ℂ$$
109	108	addlidi	$$⊢0+32=32$$
110	75	oveq1i	$$⊢0\cdot 341+32=0+32$$
111		eqid	$$⊢16=16$$
112	84	oveq1i	$$⊢1\cdot 2+1=2+1$$
113		2p1e3	$$⊢2+1=3$$
114	112 113	eqtri	$$⊢1\cdot 2+1=3$$
115		6t2e12	$$⊢6\cdot 2=12$$
116	17 7 20 111 17 7 114 115	decmul1c	$$⊢16\cdot 2=32$$
117	109 110 116	3eqtr4i	$$⊢0\cdot 341+32=16\cdot 2$$
118	5 6 19 12 21 18 104 107 117	modxp1i	$$⊢2^{85}\mathrm{mod}341=32\mathrm{mod}341$$
119		eqid	$$⊢85=85$$
120		6p1e7	$$⊢6+1=7$$
121		8cn	$$⊢8\in ℂ$$
122		8t2e16	$$⊢8\cdot 2=16$$
123	121 29 122	mulcomli	$$⊢2\cdot 8=16$$
124	7 20 120 123	decsuc	$$⊢2\cdot 8+1=17$$
125	17 13 14 119 10 7 124 31	decmul2c	$$⊢2\cdot 85=170$$
126	5 6 15 16 18 7 118 125 66	mod2xi	$$⊢2^{170}\mathrm{mod}341=1\mathrm{mod}341$$
127	17 9 10	decmulnc	Could not format ( 2 x. ; ; 1 7 0 ) = ; ( 2 x. ; 1 7 ) ( 2 x. 0 ) : No typesetting found for |- ( 2 x. ; ; 1 7 0 ) = ; ( 2 x. ; 1 7 ) ( 2 x. 0 ) with typecode |-
128		eqid	$$⊢17=17$$
129	69	oveq1i	$$⊢2\cdot 1+1=2+1$$
130	129 113	eqtri	$$⊢2\cdot 1+1=3$$
131		7cn	$$⊢7\in ℂ$$
132		7t2e14	$$⊢7\cdot 2=14$$
133	131 29 132	mulcomli	$$⊢2\cdot 7=14$$
134	17 7 8 128 2 7 130 133	decmul2c	$$⊢2\cdot 17=34$$
135	134 70	deceq12i	Could not format ; ( 2 x. ; 1 7 ) ( 2 x. 0 ) = ; ; 3 4 0 : No typesetting found for |- ; ( 2 x. ; 1 7 ) ( 2 x. 0 ) = ; ; 3 4 0 with typecode |-
136	127 135	eqtri	$$⊢2\cdot 170=340$$
137	5 6 11 12 7 7 126 136 78	mod2xi	$$⊢2^{340}\mathrm{mod}341=1\mathrm{mod}341$$
138		1re	$$⊢1\in ℝ$$
139		nnrp	$$⊢341\in \mathbb{N}\to 341\in {ℝ}^{+}$$
140	5 139	ax-mp	$$⊢341\in {ℝ}^{+}$$
141		0le1	$$⊢0\le 1$$
142		4nn	$$⊢4\in \mathbb{N}$$
143	1 142	decnncl	$$⊢34\in \mathbb{N}$$
144		9re	$$⊢9\in ℝ$$
145		1lt9	$$⊢1<9$$
146	138 144 145	ltleii	$$⊢1\le 9$$
147	143 7 7 146	decltdi	$$⊢1<341$$
148		modid	$$⊢\left(\left(1\in ℝ\wedge 341\in {ℝ}^{+}\right)\wedge \left(0\le 1\wedge 1<341\right)\right)\to 1\mathrm{mod}341=1$$
149	138 140 141 147 148	mp4an	$$⊢1\mathrm{mod}341=1$$
150	137 149	eqtri	$$⊢2^{340}\mathrm{mod}341=1$$