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 1 2 3 4sqlem5 ⊢ φ → B ∈ ℤ ∧ A − B M ∈ ℤ
5 4 simprd ⊢ φ → A − B M ∈ ℤ
6 2 nnzd ⊢ φ → M ∈ ℤ
7 2 nnne0d ⊢ φ → M ≠ 0
8 4 simpld ⊢ φ → B ∈ ℤ
9 1 8 zsubcld ⊢ φ → A − B ∈ ℤ
10 dvdsval2 ⊢ M ∈ ℤ ∧ M ≠ 0 ∧ A − B ∈ ℤ → M ∥ A − B ↔ A − B M ∈ ℤ
11 6 7 9 10 syl3anc ⊢ φ → M ∥ A − B ↔ A − B M ∈ ℤ
12 5 11 mpbird ⊢ φ → M ∥ A − B
13 1 8 zaddcld ⊢ φ → A + B ∈ ℤ
14 dvdsmul2 ⊢ A + B ∈ ℤ ∧ A − B ∈ ℤ → A − B ∥ A + B ⁢ A − B
15 13 9 14 syl2anc ⊢ φ → A − B ∥ A + B ⁢ A − B
16 1 zcnd ⊢ φ → A ∈ ℂ
17 8 zcnd ⊢ φ → B ∈ ℂ
18 subsq ⊢ A ∈ ℂ ∧ B ∈ ℂ → A 2 − B 2 = A + B ⁢ A − B
19 16 17 18 syl2anc ⊢ φ → A 2 − B 2 = A + B ⁢ A − B
20 15 19 breqtrrd ⊢ φ → A − B ∥ A 2 − B 2
21 zsqcl ⊢ A ∈ ℤ → A 2 ∈ ℤ
22 1 21 syl ⊢ φ → A 2 ∈ ℤ
23 zsqcl ⊢ B ∈ ℤ → B 2 ∈ ℤ
24 8 23 syl ⊢ φ → B 2 ∈ ℤ
25 22 24 zsubcld ⊢ φ → A 2 − B 2 ∈ ℤ
26 dvdstr ⊢ M ∈ ℤ ∧ A − B ∈ ℤ ∧ A 2 − B 2 ∈ ℤ → M ∥ A − B ∧ A − B ∥ A 2 − B 2 → M ∥ A 2 − B 2
27 6 9 25 26 syl3anc ⊢ φ → M ∥ A − B ∧ A − B ∥ A 2 − B 2 → M ∥ A 2 − B 2
28 12 20 27 mp2and ⊢ φ → M ∥ A 2 − B 2