Metamath Proof Explorer

Theorem 4sqlem8

Description: Lemma for 4sq . (Contributed by Mario Carneiro, 15-Jul-2014)

Ref Expression
Hypotheses 4sqlem5.2 ⊢ φ → A ∈ ℤ
4sqlem5.3 ⊢ φ → M ∈ ℕ
4sqlem5.4 ⊢ B = A + M 2 mod M − M 2
Assertion 4sqlem8 ⊢ φ → M ∥ A 2 − B 2

Proof

Step Hyp Ref Expression
1 4sqlem5.2 ⊢ φ → A ∈ ℤ
2 4sqlem5.3 ⊢ φ → M ∈ ℕ
3 4sqlem5.4 ⊢ B = A + M 2 mod M − M 2
4 2 nnzd ⊢ φ → M ∈ ℤ
5 1 2 3 4sqlem5 ⊢ φ → B ∈ ℤ ∧ A − B M ∈ ℤ
6 5 simpld ⊢ φ → B ∈ ℤ
7 1 6 zsubcld ⊢ φ → A − B ∈ ℤ
8 zsqcl ⊢ A ∈ ℤ → A 2 ∈ ℤ
9 1 8 syl ⊢ φ → A 2 ∈ ℤ
10 zsqcl ⊢ B ∈ ℤ → B 2 ∈ ℤ
11 6 10 syl ⊢ φ → B 2 ∈ ℤ
12 9 11 zsubcld ⊢ φ → A 2 − B 2 ∈ ℤ
13 5 simprd ⊢ φ → A − B M ∈ ℤ
14 2 nnne0d ⊢ φ → M ≠ 0
15 dvdsval2 ⊢ M ∈ ℤ ∧ M ≠ 0 ∧ A − B ∈ ℤ → M ∥ A − B ↔ A − B M ∈ ℤ
16 4 14 7 15 syl3anc ⊢ φ → M ∥ A − B ↔ A − B M ∈ ℤ
17 13 16 mpbird ⊢ φ → M ∥ A − B
18 1 6 zaddcld ⊢ φ → A + B ∈ ℤ
19 dvdsmul2 ⊢ A + B ∈ ℤ ∧ A − B ∈ ℤ → A − B ∥ A + B ⁢ A − B
20 18 7 19 syl2anc ⊢ φ → A − B ∥ A + B ⁢ A − B
21 1 zcnd ⊢ φ → A ∈ ℂ
22 6 zcnd ⊢ φ → B ∈ ℂ
23 subsq ⊢ A ∈ ℂ ∧ B ∈ ℂ → A 2 − B 2 = A + B ⁢ A − B
24 21 22 23 syl2anc ⊢ φ → A 2 − B 2 = A + B ⁢ A − B
25 20 24 breqtrrd ⊢ φ → A − B ∥ A 2 − B 2
26 4 7 12 17 25 dvdstrd ⊢ φ → M ∥ A 2 − B 2