Theorem fmtno4

Description: The 4 th Fermat number, see remark in ApostolNT p. 7. (Contributed by AV, 13-Jun-2021)

	Ref	Expression
Assertion	fmtno4	⊢ ( FermatNo ‘ 4 ) = ; ; ; ; 6 5 5 3 7

Proof

Step	Hyp	Ref	Expression
1		4nn0	⊢ 4 ∈ ℕ0
2		fmtno	⊢ ( 4 ∈ ℕ0 → ( FermatNo ‘ 4 ) = ( ( 2 ↑ ( 2 ↑ 4 ) ) + 1 ) )
3	1 2	ax-mp	⊢ ( FermatNo ‘ 4 ) = ( ( 2 ↑ ( 2 ↑ 4 ) ) + 1 )
4		2exp4	⊢ ( 2 ↑ 4 ) = ; 1 6
5	4	oveq2i	⊢ ( 2 ↑ ( 2 ↑ 4 ) ) = ( 2 ↑ ; 1 6 )
6	5	oveq1i	⊢ ( ( 2 ↑ ( 2 ↑ 4 ) ) + 1 ) = ( ( 2 ↑ ; 1 6 ) + 1 )
7		2exp16	⊢ ( 2 ↑ ; 1 6 ) = ; ; ; ; 6 5 5 3 6
8	7	oveq1i	⊢ ( ( 2 ↑ ; 1 6 ) + 1 ) = ( ; ; ; ; 6 5 5 3 6 + 1 )
9		6nn0	⊢ 6 ∈ ℕ0
10		5nn0	⊢ 5 ∈ ℕ0
11	9 10	deccl	⊢ ; 6 5 ∈ ℕ0
12	11 10	deccl	⊢ ; ; 6 5 5 ∈ ℕ0
13		3nn0	⊢ 3 ∈ ℕ0
14	12 13	deccl	⊢ ; ; ; 6 5 5 3 ∈ ℕ0
15		6p1e7	⊢ ( 6 + 1 ) = 7
16		eqid	⊢ ; ; ; ; 6 5 5 3 6 = ; ; ; ; 6 5 5 3 6
17	14 9 15 16	decsuc	⊢ ( ; ; ; ; 6 5 5 3 6 + 1 ) = ; ; ; ; 6 5 5 3 7
18	6 8 17	3eqtri	⊢ ( ( 2 ↑ ( 2 ↑ 4 ) ) + 1 ) = ; ; ; ; 6 5 5 3 7
19	3 18	eqtri	⊢ ( FermatNo ‘ 4 ) = ; ; ; ; 6 5 5 3 7