4sqlem8

Step	Hyp	Ref	Expression
1		4sqlem5.2	$⊢ φ \to A \in ℤ$
2		4sqlem5.3	$⊢ φ \to M \in ℕ$
3		4sqlem5.4	$⊢ B = ((A + (\frac{M}{2})) \mod M) - (\frac{M}{2})$
4	2	nnzd	$⊢ φ \to M \in ℤ$
5	1 2 3	4sqlem5	$⊢ φ \to (B \in ℤ \land \frac{A - B}{M} \in ℤ)$
6	5	simpld	$⊢ φ \to B \in ℤ$
7	1 6	zsubcld	$⊢ φ \to A - B \in ℤ$
8		zsqcl	$⊢ A \in ℤ \to A^{2} \in ℤ$
9	1 8	syl	$⊢ φ \to A^{2} \in ℤ$
10		zsqcl	$⊢ B \in ℤ \to B^{2} \in ℤ$
11	6 10	syl	$⊢ φ \to B^{2} \in ℤ$
12	9 11	zsubcld	$⊢ φ \to A^{2} - B^{2} \in ℤ$
13	5	simprd	$⊢ φ \to \frac{A - B}{M} \in ℤ$
14	2	nnne0d	$⊢ φ \to M \neq 0$
15		dvdsval2	$⊢ (M \in ℤ \land M \neq 0 \land A - B \in ℤ) \to (M ∥ (A - B) \leftrightarrow \frac{A - B}{M} \in ℤ)$
16	4 14 7 15	syl3anc	$⊢ φ \to (M ∥ (A - B) \leftrightarrow \frac{A - B}{M} \in ℤ)$
17	13 16	mpbird	$⊢ φ \to M ∥ (A - B)$
18	1 6	zaddcld	$⊢ φ \to A + B \in ℤ$
19		dvdsmul2	$⊢ (A + B \in ℤ \land A - B \in ℤ) \to (A - B) ∥ (A + B) (A - B)$
20	18 7 19	syl2anc	$⊢ φ \to (A - B) ∥ (A + B) (A - B)$
21	1	zcnd	$⊢ φ \to A \in ℂ$
22	6	zcnd	$⊢ φ \to B \in ℂ$
23		subsq	$⊢ (A \in ℂ \land B \in ℂ) \to A^{2} - B^{2} = (A + B) (A - B)$
24	21 22 23	syl2anc	$⊢ φ \to A^{2} - B^{2} = (A + B) (A - B)$
25	20 24	breqtrrd	$⊢ φ \to (A - B) ∥ (A^{2} - B^{2})$
26	4 7 12 17 25	dvdstrd	$⊢ φ \to M ∥ (A^{2} - B^{2})$

Metamath Proof Explorer