4sqlem6

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		0red	$⊢ φ \to 0 \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		modge0	$⊢ (A + (\frac{M}{2}) \in ℝ \land M \in ℝ^{+}) \to 0 \leq (A + (\frac{M}{2})) \mod M$
12	8 9 11	syl2anc	$⊢ φ \to 0 \leq (A + (\frac{M}{2})) \mod M$
13	4 10 7 12	lesub1dd	$⊢ φ \to 0 - (\frac{M}{2}) \leq ((A + (\frac{M}{2})) \mod M) - (\frac{M}{2})$
14		df-neg	$⊢ - \frac{M}{2} = 0 - (\frac{M}{2})$
15	13 14 3	3brtr4g	$⊢ φ \to - \frac{M}{2} \leq B$
16		modlt	$⊢ (A + (\frac{M}{2}) \in ℝ \land M \in ℝ^{+}) \to (A + (\frac{M}{2})) \mod M < M$
17	8 9 16	syl2anc	$⊢ φ \to (A + (\frac{M}{2})) \mod M < M$
18	2	nncnd	$⊢ φ \to M \in ℂ$
19	18	2halvesd	$⊢ φ \to (\frac{M}{2}) + (\frac{M}{2}) = M$
20	17 19	breqtrrd	$⊢ φ \to (A + (\frac{M}{2})) \mod M < (\frac{M}{2}) + (\frac{M}{2})$
21	10 7 7	ltsubaddd	$⊢ φ \to (((A + (\frac{M}{2})) \mod M) - (\frac{M}{2}) < \frac{M}{2} \leftrightarrow (A + (\frac{M}{2})) \mod M < (\frac{M}{2}) + (\frac{M}{2}))$
22	20 21	mpbird	$⊢ φ \to ((A + (\frac{M}{2})) \mod M) - (\frac{M}{2}) < \frac{M}{2}$
23	3 22	eqbrtrid	$⊢ φ \to B < \frac{M}{2}$
24	15 23	jca	$⊢ φ \to (- \frac{M}{2} \leq B \land B < \frac{M}{2})$

Metamath Proof Explorer