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