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 ) ) )