4sqlem9

	Ref	Expression
Hypotheses	4sqlem5.2	$⊢ φ \to A \in ℤ$
	4sqlem5.3	$⊢ φ \to M \in ℕ$
	4sqlem5.4	$⊢ B = ((A + (\frac{M}{2})) \mod M) - (\frac{M}{2})$
	4sqlem9.5	$⊢ (φ \land ψ) \to B^{2} = 0$
Assertion	4sqlem9	$⊢ (φ \land ψ) \to M^{2} ∥ A^{2}$

Proof

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		4sqlem9.5	$⊢ (φ \land ψ) \to B^{2} = 0$
5	1 2 3	4sqlem5	$⊢ φ \to (B \in ℤ \land \frac{A - B}{M} \in ℤ)$
6	5	simpld	$⊢ φ \to B \in ℤ$
7	6	zcnd	$⊢ φ \to B \in ℂ$
8		sqeq0	$⊢ B \in ℂ \to (B^{2} = 0 \leftrightarrow B = 0)$
9	7 8	syl	$⊢ φ \to (B^{2} = 0 \leftrightarrow B = 0)$
10	9	biimpa	$⊢ (φ \land B^{2} = 0) \to B = 0$
11	4 10	syldan	$⊢ (φ \land ψ) \to B = 0$
12	11	oveq2d	$⊢ (φ \land ψ) \to A - B = A - 0$
13	1	adantr	$⊢ (φ \land ψ) \to A \in ℤ$
14	13	zcnd	$⊢ (φ \land ψ) \to A \in ℂ$
15	14	subid1d	$⊢ (φ \land ψ) \to A - 0 = A$
16	12 15	eqtrd	$⊢ (φ \land ψ) \to A - B = A$
17	16	oveq1d	$⊢ (φ \land ψ) \to \frac{A - B}{M} = \frac{A}{M}$
18	5	simprd	$⊢ φ \to \frac{A - B}{M} \in ℤ$
19	18	adantr	$⊢ (φ \land ψ) \to \frac{A - B}{M} \in ℤ$
20	17 19	eqeltrrd	$⊢ (φ \land ψ) \to \frac{A}{M} \in ℤ$
21	2	nnzd	$⊢ φ \to M \in ℤ$
22	2	nnne0d	$⊢ φ \to M \neq 0$
23		dvdsval2	$⊢ (M \in ℤ \land M \neq 0 \land A \in ℤ) \to (M ∥ A \leftrightarrow \frac{A}{M} \in ℤ)$
24	21 22 1 23	syl3anc	$⊢ φ \to (M ∥ A \leftrightarrow \frac{A}{M} \in ℤ)$
25	24	adantr	$⊢ (φ \land ψ) \to (M ∥ A \leftrightarrow \frac{A}{M} \in ℤ)$
26	20 25	mpbird	$⊢ (φ \land ψ) \to M ∥ A$
27		dvdssq	$⊢ (M \in ℤ \land A \in ℤ) \to (M ∥ A \leftrightarrow M^{2} ∥ A^{2})$
28	21 13 27	syl2an2r	$⊢ (φ \land ψ) \to (M ∥ A \leftrightarrow M^{2} ∥ A^{2})$
29	26 28	mpbid	$⊢ (φ \land ψ) \to M^{2} ∥ A^{2}$

Metamath Proof Explorer

Theorem 4sqlem9

Proof