This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 4sqlem8

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

Ref Expression
Hypotheses 4sqlem5.2 ⊢ ( 𝜑 → 𝐴 ∈ ℤ )
4sqlem5.3 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
4sqlem5.4 ⊢ 𝐵 = ( ( ( 𝐴 + ( 𝑀 / 2 ) ) mod 𝑀 ) − ( 𝑀 / 2 ) )
Assertion 4sqlem8 ( 𝜑 → 𝑀 ∥ ( ( 𝐴 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) )

Proof

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