Theorem fmtno5

Description: The 5 th Fermat number. (Contributed by AV, 30-Jul-2021)

	Ref	Expression
Assertion	fmtno5	⊢ ( FermatNo ‘ 5 ) = ; ; ; ; ; ; ; ; ; 4 2 9 4 9 6 7 2 9 7

Proof

Step	Hyp	Ref	Expression
1		df-5	⊢ 5 = ( 4 + 1 )
2	1	fveq2i	⊢ ( FermatNo ‘ 5 ) = ( FermatNo ‘ ( 4 + 1 ) )
3		4nn0	⊢ 4 ∈ ℕ0
4		fmtnorec1	⊢ ( 4 ∈ ℕ0 → ( FermatNo ‘ ( 4 + 1 ) ) = ( ( ( ( FermatNo ‘ 4 ) − 1 ) ↑ 2 ) + 1 ) )
5	3 4	ax-mp	⊢ ( FermatNo ‘ ( 4 + 1 ) ) = ( ( ( ( FermatNo ‘ 4 ) − 1 ) ↑ 2 ) + 1 )
6	2 5	eqtri	⊢ ( FermatNo ‘ 5 ) = ( ( ( ( FermatNo ‘ 4 ) − 1 ) ↑ 2 ) + 1 )
7		2nn0	⊢ 2 ∈ ℕ0
8	3 7	deccl	⊢ ; 4 2 ∈ ℕ0
9		9nn0	⊢ 9 ∈ ℕ0
10	8 9	deccl	⊢ ; ; 4 2 9 ∈ ℕ0
11	10 3	deccl	⊢ ; ; ; 4 2 9 4 ∈ ℕ0
12	11 9	deccl	⊢ ; ; ; ; 4 2 9 4 9 ∈ ℕ0
13		6nn0	⊢ 6 ∈ ℕ0
14	12 13	deccl	⊢ ; ; ; ; ; 4 2 9 4 9 6 ∈ ℕ0
15		7nn0	⊢ 7 ∈ ℕ0
16	14 15	deccl	⊢ ; ; ; ; ; ; 4 2 9 4 9 6 7 ∈ ℕ0
17	16 7	deccl	⊢ ; ; ; ; ; ; ; 4 2 9 4 9 6 7 2 ∈ ℕ0
18	17 9	deccl	⊢ ; ; ; ; ; ; ; ; 4 2 9 4 9 6 7 2 9 ∈ ℕ0
19		6p1e7	⊢ ( 6 + 1 ) = 7
20		5nn0	⊢ 5 ∈ ℕ0
21	13 20	deccl	⊢ ; 6 5 ∈ ℕ0
22	21 20	deccl	⊢ ; ; 6 5 5 ∈ ℕ0
23		3nn0	⊢ 3 ∈ ℕ0
24	22 23	deccl	⊢ ; ; ; 6 5 5 3 ∈ ℕ0
25		1nn0	⊢ 1 ∈ ℕ0
26		fmtno4	⊢ ( FermatNo ‘ 4 ) = ; ; ; ; 6 5 5 3 7
27		3p1e4	⊢ ( 3 + 1 ) = 4
28		eqid	⊢ ; ; ; 6 5 5 3 = ; ; ; 6 5 5 3
29	22 23 27 28	decsuc	⊢ ( ; ; ; 6 5 5 3 + 1 ) = ; ; ; 6 5 5 4
30		6cn	⊢ 6 ∈ ℂ
31		ax-1cn	⊢ 1 ∈ ℂ
32		df-7	⊢ 7 = ( 6 + 1 )
33	30 31 32	mvrraddi	⊢ ( 7 − 1 ) = 6
34	24 15 25 26 29 33	decsubi	⊢ ( ( FermatNo ‘ 4 ) − 1 ) = ; ; ; ; 6 5 5 3 6
35	34	oveq1i	⊢ ( ( ( FermatNo ‘ 4 ) − 1 ) ↑ 2 ) = ( ; ; ; ; 6 5 5 3 6 ↑ 2 )
36		fmtno5lem4	⊢ ( ; ; ; ; 6 5 5 3 6 ↑ 2 ) = ; ; ; ; ; ; ; ; ; 4 2 9 4 9 6 7 2 9 6
37	35 36	eqtri	⊢ ( ( ( FermatNo ‘ 4 ) − 1 ) ↑ 2 ) = ; ; ; ; ; ; ; ; ; 4 2 9 4 9 6 7 2 9 6
38	18 13 19 37	decsuc	⊢ ( ( ( ( FermatNo ‘ 4 ) − 1 ) ↑ 2 ) + 1 ) = ; ; ; ; ; ; ; ; ; 4 2 9 4 9 6 7 2 9 7
39	6 38	eqtri	⊢ ( FermatNo ‘ 5 ) = ; ; ; ; ; ; ; ; ; 4 2 9 4 9 6 7 2 9 7