4sqlem5

	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})$
Assertion	4sqlem5	$⊢ φ \to (B \in ℤ \land \frac{A - B}{M} \in ℤ)$

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	1	zcnd	$⊢ φ \to A \in ℂ$
5	1	zred	$⊢ φ \to A \in ℝ$
6	2	nnred	$⊢ φ \to M \in ℝ$
7	6	rehalfcld	$⊢ φ \to \frac{M}{2} \in ℝ$
8	5 7	readdcld	$⊢ φ \to A + (\frac{M}{2}) \in ℝ$
9	2	nnrpd	$⊢ φ \to M \in ℝ^{+}$
10	8 9	modcld	$⊢ φ \to (A + (\frac{M}{2})) \mod M \in ℝ$
11	10	recnd	$⊢ φ \to (A + (\frac{M}{2})) \mod M \in ℂ$
12	7	recnd	$⊢ φ \to \frac{M}{2} \in ℂ$
13	11 12	subcld	$⊢ φ \to ((A + (\frac{M}{2})) \mod M) - (\frac{M}{2}) \in ℂ$
14	3 13	eqeltrid	$⊢ φ \to B \in ℂ$
15	4 14	nncand	$⊢ φ \to A - (A - B) = B$
16	4 14	subcld	$⊢ φ \to A - B \in ℂ$
17	6	recnd	$⊢ φ \to M \in ℂ$
18	2	nnne0d	$⊢ φ \to M \neq 0$
19	16 17 18	divcan1d	$⊢ φ \to (\frac{A - B}{M}) \cdot M = A - B$
20	3	oveq2i	$⊢ A - B = A - (((A + (\frac{M}{2})) \mod M) - (\frac{M}{2}))$
21	4 11 12	subsub3d	$⊢ φ \to A - (((A + (\frac{M}{2})) \mod M) - (\frac{M}{2})) = A + (\frac{M}{2}) - ((A + (\frac{M}{2})) \mod M)$
22	20 21	eqtrid	$⊢ φ \to A - B = A + (\frac{M}{2}) - ((A + (\frac{M}{2})) \mod M)$
23	22	oveq1d	$⊢ φ \to \frac{A - B}{M} = \frac{A + (\frac{M}{2}) - ((A + (\frac{M}{2})) \mod M)}{M}$
24		moddifz	$⊢ (A + (\frac{M}{2}) \in ℝ \land M \in ℝ^{+}) \to \frac{A + (\frac{M}{2}) - ((A + (\frac{M}{2})) \mod M)}{M} \in ℤ$
25	8 9 24	syl2anc	$⊢ φ \to \frac{A + (\frac{M}{2}) - ((A + (\frac{M}{2})) \mod M)}{M} \in ℤ$
26	23 25	eqeltrd	$⊢ φ \to \frac{A - B}{M} \in ℤ$
27	2	nnzd	$⊢ φ \to M \in ℤ$
28	26 27	zmulcld	$⊢ φ \to (\frac{A - B}{M}) \cdot M \in ℤ$
29	19 28	eqeltrrd	$⊢ φ \to A - B \in ℤ$
30	1 29	zsubcld	$⊢ φ \to A - (A - B) \in ℤ$
31	15 30	eqeltrrd	$⊢ φ \to B \in ℤ$
32	31 26	jca	$⊢ φ \to (B \in ℤ \land \frac{A - B}{M} \in ℤ)$

Metamath Proof Explorer

Theorem 4sqlem5

Proof