goldbachthlem1

		Ref	Expression
	Assertion	goldbachthlem1	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0} \land M < N) \to FermatNo (M) ∥ (FermatNo (N) - 2)$

Step	Hyp	Ref	Expression
1		simp2	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0} \land M < N) \to M \in ℕ_{0}$
2		nn0z	$⊢ M \in ℕ_{0} \to M \in ℤ$
3		nn0z	$⊢ N \in ℕ_{0} \to N \in ℤ$
4		znnsub	$⊢ (M \in ℤ \land N \in ℤ) \to (M < N \leftrightarrow N - M \in ℕ)$
5	2 3 4	syl2anr	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0}) \to (M < N \leftrightarrow N - M \in ℕ)$
6	5	biimp3a	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0} \land M < N) \to N - M \in ℕ$
7		fmtnodvds	$⊢ (M \in ℕ_{0} \land N - M \in ℕ) \to FermatNo (M) ∥ (FermatNo (M + N - M) - 2)$
8	1 6 7	syl2anc	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0} \land M < N) \to FermatNo (M) ∥ (FermatNo (M + N - M) - 2)$
9		nn0cn	$⊢ N \in ℕ_{0} \to N \in ℂ$
10		nn0cn	$⊢ M \in ℕ_{0} \to M \in ℂ$
11	9 10	anim12ci	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0}) \to (M \in ℂ \land N \in ℂ)$
12	11	3adant3	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0} \land M < N) \to (M \in ℂ \land N \in ℂ)$
13		pncan3	$⊢ (M \in ℂ \land N \in ℂ) \to M + N - M = N$
14	12 13	syl	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0} \land M < N) \to M + N - M = N$
15	14	eqcomd	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0} \land M < N) \to N = M + N - M$
16	15	fveq2d	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0} \land M < N) \to FermatNo (N) = FermatNo (M + N - M)$
17	16	oveq1d	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0} \land M < N) \to FermatNo (N) - 2 = FermatNo (M + N - M) - 2$
18	8 17	breqtrrd	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0} \land M < N) \to FermatNo (M) ∥ (FermatNo (N) - 2)$

Metamath Proof Explorer