Theorem fmtno5nprm

Description: The 5 th Fermat number is a not a prime. (Contributed by AV, 22-Jul-2021)

	Ref	Expression
Assertion	fmtno5nprm	⊢ ( FermatNo ‘ 5 ) ∉ ℙ

Proof

Step	Hyp	Ref	Expression
1		6nn0	⊢ 6 ∈ ℕ0
2		7nn0	⊢ 7 ∈ ℕ0
3	1 2	deccl	⊢ ; 6 7 ∈ ℕ0
4		0nn0	⊢ 0 ∈ ℕ0
5	3 4	deccl	⊢ ; ; 6 7 0 ∈ ℕ0
6	5 4	deccl	⊢ ; ; ; 6 7 0 0 ∈ ℕ0
7		4nn0	⊢ 4 ∈ ℕ0
8	6 7	deccl	⊢ ; ; ; ; 6 7 0 0 4 ∈ ℕ0
9		1nn0	⊢ 1 ∈ ℕ0
10	8 9	deccl	⊢ ; ; ; ; ; 6 7 0 0 4 1 ∈ ℕ0
11		7nn	⊢ 7 ∈ ℕ
12	10 11	decnncl	⊢ ; ; ; ; ; ; 6 7 0 0 4 1 7 ∈ ℕ
13	1 7	deccl	⊢ ; 6 4 ∈ ℕ0
14		1nn	⊢ 1 ∈ ℕ
15	13 14	decnncl	⊢ ; ; 6 4 1 ∈ ℕ
16	8 14	decnncl	⊢ ; ; ; ; ; 6 7 0 0 4 1 ∈ ℕ
17		1lt10	⊢ 1 < ; 1 0
18	16 2 9 17	declti	⊢ 1 < ; ; ; ; ; ; 6 7 0 0 4 1 7
19		4nn	⊢ 4 ∈ ℕ
20	1 19	decnncl	⊢ ; 6 4 ∈ ℕ
21	20 9 9 17	declti	⊢ 1 < ; ; 6 4 1
22		fmtno5fac	⊢ ( FermatNo ‘ 5 ) = ( ; ; ; ; ; ; 6 7 0 0 4 1 7 · ; ; 6 4 1 )
23	22	eqcomi	⊢ ( ; ; ; ; ; ; 6 7 0 0 4 1 7 · ; ; 6 4 1 ) = ( FermatNo ‘ 5 )
24	12 15 18 21 23	nprmi	⊢ ¬ ( FermatNo ‘ 5 ) ∈ ℙ
25	24	nelir	⊢ ( FermatNo ‘ 5 ) ∉ ℙ