Theorem goldbachthlem1

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

	Ref	Expression
Assertion	goldbachthlem1	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑀 < 𝑁 ) → ( FermatNo ‘ 𝑀 ) ∥ ( ( FermatNo ‘ 𝑁 ) − 2 ) )

Proof

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