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		2t3e6	$$⊢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		2t4e8	$$⊢2\cdot 4=8$$
96	95 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 |-
97	94 96	eqtri	$$⊢2\cdot 42=84$$
98	21	nn0cni	$$⊢16\in ℂ$$
99	98	addlidi	$$⊢0+16=16$$
100	75	oveq1i	$$⊢0\cdot 341+16=0+16$$
101		4t4e16	$$⊢4\cdot 4=16$$
102	99 100 101	3eqtr4i	$$⊢0\cdot 341+16=4\cdot 4$$
103	5 6 22 12 2 21 93 97 102	mod2xi	$$⊢2^{84}\mathrm{mod}341=16\mathrm{mod}341$$
104		4p1e5	$$⊢4+1=5$$
105		eqid	$$⊢84=84$$
106	13 2 104 105	decsuc	$$⊢84+1=85$$
107	18	nn0cni	$$⊢32\in ℂ$$
108	107	addlidi	$$⊢0+32=32$$
109	75	oveq1i	$$⊢0\cdot 341+32=0+32$$
110		eqid	$$⊢16=16$$
111	84	oveq1i	$$⊢1\cdot 2+1=2+1$$
112		2p1e3	$$⊢2+1=3$$
113	111 112	eqtri	$$⊢1\cdot 2+1=3$$
114		6t2e12	$$⊢6\cdot 2=12$$
115	17 7 20 110 17 7 113 114	decmul1c	$$⊢16\cdot 2=32$$
116	108 109 115	3eqtr4i	$$⊢0\cdot 341+32=16\cdot 2$$
117	5 6 19 12 21 18 103 106 116	modxp1i	$$⊢2^{85}\mathrm{mod}341=32\mathrm{mod}341$$
118		eqid	$$⊢85=85$$
119		6p1e7	$$⊢6+1=7$$
120		8cn	$$⊢8\in ℂ$$
121		8t2e16	$$⊢8\cdot 2=16$$
122	120 29 121	mulcomli	$$⊢2\cdot 8=16$$
123	7 20 119 122	decsuc	$$⊢2\cdot 8+1=17$$
124	17 13 14 118 10 7 123 31	decmul2c	$$⊢2\cdot 85=170$$
125	5 6 15 16 18 7 117 124 66	mod2xi	$$⊢2^{170}\mathrm{mod}341=1\mathrm{mod}341$$
126	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 |-
127		eqid	$$⊢17=17$$
128	69	oveq1i	$$⊢2\cdot 1+1=2+1$$
129	128 112	eqtri	$$⊢2\cdot 1+1=3$$
130		7cn	$$⊢7\in ℂ$$
131		7t2e14	$$⊢7\cdot 2=14$$
132	130 29 131	mulcomli	$$⊢2\cdot 7=14$$
133	17 7 8 127 2 7 129 132	decmul2c	$$⊢2\cdot 17=34$$
134	133 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 |-
135	126 134	eqtri	$$⊢2\cdot 170=340$$
136	5 6 11 12 7 7 125 135 78	mod2xi	$$⊢2^{340}\mathrm{mod}341=1\mathrm{mod}341$$
137		1re	$$⊢1\in ℝ$$
138		nnrp	$$⊢341\in \mathbb{N}\to 341\in {ℝ}^{+}$$
139	5 138	ax-mp	$$⊢341\in {ℝ}^{+}$$
140		0le1	$$⊢0\le 1$$
141		4nn	$$⊢4\in \mathbb{N}$$
142	1 141	decnncl	$$⊢34\in \mathbb{N}$$
143		9re	$$⊢9\in ℝ$$
144		1lt9	$$⊢1<9$$
145	137 143 144	ltleii	$$⊢1\le 9$$
146	142 7 7 145	decltdi	$$⊢1<341$$
147		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$$
148	137 139 140 146 147	mp4an	$$⊢1\mathrm{mod}341=1$$
149	136 148	eqtri	$$⊢2^{340}\mathrm{mod}341=1$$