Metamath Proof Explorer

Theorem goldbachthlem1

Description: Lemma 1 for goldbachth . (Contributed by AV, 1-Aug-2021)

Ref Expression
Assertion goldbachthlem1 ⊢ N ∈ ℕ 0 ∧ M ∈ ℕ 0 ∧ M < N → FermatNo ⁡ M ∥ FermatNo ⁡ N − 2

Proof

Step Hyp Ref Expression
1 simp2 ⊢ N ∈ ℕ 0 ∧ M ∈ ℕ 0 ∧ M < N → M ∈ ℕ 0
2 nn0z ⊢ M ∈ ℕ 0 → M ∈ ℤ
3 nn0z ⊢ N ∈ ℕ 0 → N ∈ ℤ
4 znnsub ⊢ M ∈ ℤ ∧ N ∈ ℤ → M < N ↔ N − M ∈ ℕ
5 2 3 4 syl2anr ⊢ N ∈ ℕ 0 ∧ M ∈ ℕ 0 → M < N ↔ N − M ∈ ℕ
6 5 biimp3a ⊢ N ∈ ℕ 0 ∧ M ∈ ℕ 0 ∧ M < N → N − M ∈ ℕ
7 fmtnodvds ⊢ M ∈ ℕ 0 ∧ N − M ∈ ℕ → FermatNo ⁡ M ∥ FermatNo ⁡ M + N - M − 2
8 1 6 7 syl2anc ⊢ N ∈ ℕ 0 ∧ M ∈ ℕ 0 ∧ M < N → FermatNo ⁡ M ∥ FermatNo ⁡ M + N - M − 2
9 nn0cn ⊢ N ∈ ℕ 0 → N ∈ ℂ
10 nn0cn ⊢ M ∈ ℕ 0 → M ∈ ℂ
11 9 10 anim12ci ⊢ N ∈ ℕ 0 ∧ M ∈ ℕ 0 → M ∈ ℂ ∧ N ∈ ℂ
12 11 3adant3 ⊢ N ∈ ℕ 0 ∧ M ∈ ℕ 0 ∧ M < N → M ∈ ℂ ∧ N ∈ ℂ
13 pncan3 ⊢ M ∈ ℂ ∧ N ∈ ℂ → M + N - M = N
14 12 13 syl ⊢ N ∈ ℕ 0 ∧ M ∈ ℕ 0 ∧ M < N → M + N - M = N
15 14 eqcomd ⊢ N ∈ ℕ 0 ∧ M ∈ ℕ 0 ∧ M < N → N = M + N - M
16 15 fveq2d ⊢ N ∈ ℕ 0 ∧ M ∈ ℕ 0 ∧ M < N → FermatNo ⁡ N = FermatNo ⁡ M + N - M
17 16 oveq1d ⊢ N ∈ ℕ 0 ∧ M ∈ ℕ 0 ∧ M < N → FermatNo ⁡ N − 2 = FermatNo ⁡ M + N - M − 2
18 8 17 breqtrrd ⊢ N ∈ ℕ 0 ∧ M ∈ ℕ 0 ∧ M < N → FermatNo ⁡ M ∥ FermatNo ⁡ N − 2