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