fmtnoodd

		Ref	Expression
	Assertion	fmtnoodd	$⊢ N \in ℕ_{0} \to \neg 2 ∥ FermatNo (N)$

Proof

Step	Hyp	Ref	Expression
1		2nn	$⊢ 2 \in ℕ$
2	1	a1i	$⊢ N \in ℕ_{0} \to 2 \in ℕ$
3		id	$⊢ N \in ℕ_{0} \to N \in ℕ_{0}$
4	2 3	nnexpcld	$⊢ N \in ℕ_{0} \to 2^{N} \in ℕ$
5		nnm1nn0	$⊢ 2^{N} \in ℕ \to 2^{N} - 1 \in ℕ_{0}$
6	4 5	syl	$⊢ N \in ℕ_{0} \to 2^{N} - 1 \in ℕ_{0}$
7	2 6	nnexpcld	$⊢ N \in ℕ_{0} \to 2^{2^{N} - 1} \in ℕ$
8	7	nnzd	$⊢ N \in ℕ_{0} \to 2^{2^{N} - 1} \in ℤ$
9		oveq2	$⊢ k = 2^{2^{N} - 1} \to 2 k = 2 2^{2^{N} - 1}$
10	9	oveq1d	$⊢ k = 2^{2^{N} - 1} \to 2 k + 1 = 2 2^{2^{N} - 1} + 1$
11		fmtno	$⊢ N \in ℕ_{0} \to FermatNo (N) = 2^{2^{N}} + 1$
12	10 11	eqeqan12rd	$⊢ (N \in ℕ_{0} \land k = 2^{2^{N} - 1}) \to (2 k + 1 = FermatNo (N) \leftrightarrow 2 2^{2^{N} - 1} + 1 = 2^{2^{N}} + 1)$
13		2cnd	$⊢ N \in ℕ_{0} \to 2 \in ℂ$
14	7	nncnd	$⊢ N \in ℕ_{0} \to 2^{2^{N} - 1} \in ℂ$
15	13 14	mulcomd	$⊢ N \in ℕ_{0} \to 2 2^{2^{N} - 1} = 2^{2^{N} - 1} \cdot 2$
16		expm1t	$⊢ (2 \in ℂ \land 2^{N} \in ℕ) \to 2^{2^{N}} = 2^{2^{N} - 1} \cdot 2$
17	13 4 16	syl2anc	$⊢ N \in ℕ_{0} \to 2^{2^{N}} = 2^{2^{N} - 1} \cdot 2$
18	15 17	eqtr4d	$⊢ N \in ℕ_{0} \to 2 2^{2^{N} - 1} = 2^{2^{N}}$
19	18	oveq1d	$⊢ N \in ℕ_{0} \to 2 2^{2^{N} - 1} + 1 = 2^{2^{N}} + 1$
20	8 12 19	rspcedvd	$⊢ N \in ℕ_{0} \to \exists k \in ℤ 2 k + 1 = FermatNo (N)$
21		fmtnonn	$⊢ N \in ℕ_{0} \to FermatNo (N) \in ℕ$
22	21	nnzd	$⊢ N \in ℕ_{0} \to FermatNo (N) \in ℤ$
23		odd2np1	$⊢ FermatNo (N) \in ℤ \to (\neg 2 ∥ FermatNo (N) \leftrightarrow \exists k \in ℤ 2 k + 1 = FermatNo (N))$
24	22 23	syl	$⊢ N \in ℕ_{0} \to (\neg 2 ∥ FermatNo (N) \leftrightarrow \exists k \in ℤ 2 k + 1 = FermatNo (N))$
25	20 24	mpbird	$⊢ N \in ℕ_{0} \to \neg 2 ∥ FermatNo (N)$

Metamath Proof Explorer

Theorem fmtnoodd

Proof