Theorem 3exp4mod41

Description: 3 to the fourth power is -1 modulo 41. (Contributed by AV, 5-Jul-2020)

	Ref	Expression
Assertion	3exp4mod41	$$⊢3^4\mathrm{mod}41=-1\mathrm{mod}41$$

Proof

Step	Hyp	Ref	Expression
1		2p2e4	$$⊢2+2=4$$
2	1	eqcomi	$$⊢4=2+2$$
3	2	oveq2i	$$⊢3^4=3^{2+2}$$
4		3cn	$$⊢3\in ℂ$$
5		2nn0	$$⊢2\in {\mathbb{N}}_0$$
6		expadd	$$⊢\left(3\in ℂ\wedge 2\in {\mathbb{N}}_0\wedge 2\in {\mathbb{N}}_0\right)\to 3^{2+2}=3^2{3}^2$$
7	4 5 5 6	mp3an	$$⊢3^{2+2}=3^2{3}^2$$
8		sq3	$$⊢3^2=9$$
9	8 8	oveq12i	$$⊢3^2{3}^2=9\cdot 9$$
10		9t9e81	$$⊢9\cdot 9=81$$
11	9 10	eqtri	$$⊢3^2{3}^2=81$$
12	3 7 11	3eqtri	$$⊢3^4=81$$
13	12	oveq1i	$$⊢3^4\mathrm{mod}41=81\mathrm{mod}41$$
14		dfdec10	$$⊢81=10\cdot 8+1$$
15		4cn	$$⊢4\in ℂ$$
16		2cn	$$⊢2\in ℂ$$
17		4t2e8	$$⊢4\cdot 2=8$$
18	15 16 17	mulcomli	$$⊢2\cdot 4=8$$
19	18	eqcomi	$$⊢8=2\cdot 4$$
20	19	oveq2i	$$⊢10\cdot 8=102\cdot 4$$
21		ax-1cn	$$⊢1\in ℂ$$
22	16 21	negsubi	$$⊢2+-1=2-1$$
23		2m1e1	$$⊢2-1=1$$
24	22 23	eqtri	$$⊢2+-1=1$$
25	24	eqcomi	$$⊢1=2+-1$$
26	20 25	oveq12i	$$⊢10\cdot 8+1=102\cdot 4+2+-1$$
27		10nn	$$⊢10\in \mathbb{N}$$
28	27	nncni	$$⊢10\in ℂ$$
29	16 15	mulcli	$$⊢2\cdot 4\in ℂ$$
30	28 29	mulcli	$$⊢102\cdot 4\in ℂ$$
31		neg1cn	$$⊢-1\in ℂ$$
32	30 16 31	addassi	$$⊢102\cdot 4+2+-1=102\cdot 4+2+-1$$
33	28 15	mulcli	$$⊢10\cdot 4\in ℂ$$
34	16 33 21	adddii	$$⊢2\left(10\cdot 4+1\right)=210\cdot 4+2\cdot 1$$
35		dfdec10	$$⊢41=10\cdot 4+1$$
36	35	eqcomi	$$⊢10\cdot 4+1=41$$
37	36	oveq2i	$$⊢2\left(10\cdot 4+1\right)=2\cdot 41$$
38	16 28 15	mul12i	$$⊢210\cdot 4=102\cdot 4$$
39		2t1e2	$$⊢2\cdot 1=2$$
40	38 39	oveq12i	$$⊢210\cdot 4+2\cdot 1=102\cdot 4+2$$
41	34 37 40	3eqtr3ri	$$⊢102\cdot 4+2=2\cdot 41$$
42	41	oveq1i	$$⊢102\cdot 4+2+-1=2\cdot 41+-1$$
43	26 32 42	3eqtr2i	$$⊢10\cdot 8+1=2\cdot 41+-1$$
44	14 43	eqtri	$$⊢81=2\cdot 41+-1$$
45	44	oveq1i	$$⊢81\mathrm{mod}41=\left(2\cdot 41+-1\right)\mathrm{mod}41$$
46		4nn0	$$⊢4\in {\mathbb{N}}_0$$
47		1nn	$$⊢1\in \mathbb{N}$$
48	46 47	decnncl	$$⊢41\in \mathbb{N}$$
49	48	nncni	$$⊢41\in ℂ$$
50	16 49	mulcli	$$⊢2\cdot 41\in ℂ$$
51	50 31	addcomi	$$⊢2\cdot 41+-1=-1+2\cdot 41$$
52	51	oveq1i	$$⊢\left(2\cdot 41+-1\right)\mathrm{mod}41=\left(-1+2\cdot 41\right)\mathrm{mod}41$$
53		neg1rr	$$⊢-1\in ℝ$$
54		nnrp	$$⊢41\in \mathbb{N}\to 41\in {ℝ}^{+}$$
55	48 54	ax-mp	$$⊢41\in {ℝ}^{+}$$
56		2z	$$⊢2\in \mathbb{Z}$$
57		modcyc	$$⊢\left(-1\in ℝ\wedge 41\in {ℝ}^{+}\wedge 2\in \mathbb{Z}\right)\to \left(-1+2\cdot 41\right)\mathrm{mod}41=-1\mathrm{mod}41$$
58	53 55 56 57	mp3an	$$⊢\left(-1+2\cdot 41\right)\mathrm{mod}41=-1\mathrm{mod}41$$
59	52 58	eqtri	$$⊢\left(2\cdot 41+-1\right)\mathrm{mod}41=-1\mathrm{mod}41$$
60	13 45 59	3eqtri	$$⊢3^4\mathrm{mod}41=-1\mathrm{mod}41$$