Theorem 4sqlem7

Description: Lemma for 4sq . (Contributed by Mario Carneiro, 15-Jul-2014)

	Ref	Expression
Hypotheses	4sqlem5.2	$$⊢\phi \to A\in \mathbb{Z}$$
	4sqlem5.3	$$⊢\phi \to M\in \mathbb{N}$$
	4sqlem5.4	$$⊢B=\left(\left(A+\left(\frac{M}{2}\right)\right)\mathrm{mod}M\right)-\left(\frac{M}{2}\right)$$
Assertion	4sqlem7	$$⊢\phi \to B^2\le \frac{\frac{M^2}{2}}{2}$$

Proof

Step	Hyp	Ref	Expression
1		4sqlem5.2	$$⊢\phi \to A\in \mathbb{Z}$$
2		4sqlem5.3	$$⊢\phi \to M\in \mathbb{N}$$
3		4sqlem5.4	$$⊢B=\left(\left(A+\left(\frac{M}{2}\right)\right)\mathrm{mod}M\right)-\left(\frac{M}{2}\right)$$
4	1 2 3	4sqlem5	$$⊢\phi \to \left(B\in \mathbb{Z}\wedge \frac{A-B}{M}\in \mathbb{Z}\right)$$
5	4	simpld	$$⊢\phi \to B\in \mathbb{Z}$$
6	5	zred	$$⊢\phi \to B\in ℝ$$
7	2	nnrpd	$$⊢\phi \to M\in {ℝ}^{+}$$
8	7	rphalfcld	$$⊢\phi \to \frac{M}{2}\in {ℝ}^{+}$$
9	8	rpred	$$⊢\phi \to \frac{M}{2}\in ℝ$$
10	1 2 3	4sqlem6	$$⊢\phi \to \left(-\frac{M}{2}\le B\wedge B<\frac{M}{2}\right)$$
11	10	simprd	$$⊢\phi \to B<\frac{M}{2}$$
12	6 9 11	ltled	$$⊢\phi \to B\le \frac{M}{2}$$
13	10	simpld	$$⊢\phi \to -\frac{M}{2}\le B$$
14	9 6 13	lenegcon1d	$$⊢\phi \to -B\le \frac{M}{2}$$
15	8	rpge0d	$$⊢\phi \to 0\le \frac{M}{2}$$
16		lenegsq	$$⊢\left(B\in ℝ\wedge \frac{M}{2}\in ℝ\wedge 0\le \frac{M}{2}\right)\to \left(\left(B\le \frac{M}{2}\wedge -B\le \frac{M}{2}\right)\leftrightarrow B^2\le {\left(\frac{M}{2}\right)}^2\right)$$
17	6 9 15 16	syl3anc	$$⊢\phi \to \left(\left(B\le \frac{M}{2}\wedge -B\le \frac{M}{2}\right)\leftrightarrow B^2\le {\left(\frac{M}{2}\right)}^2\right)$$
18	12 14 17	mpbi2and	$$⊢\phi \to B^2\le {\left(\frac{M}{2}\right)}^2$$
19		2cnd	$$⊢\phi \to 2\in ℂ$$
20	19	sqvald	$$⊢\phi \to 2^2=2\cdot 2$$
21	20	oveq2d	$$⊢\phi \to \frac{M^2}{2^2}=\frac{M^2}{2\cdot 2}$$
22	2	nncnd	$$⊢\phi \to M\in ℂ$$
23		2ne0	$$⊢2\ne 0$$
24	23	a1i	$$⊢\phi \to 2\ne 0$$
25	22 19 24	sqdivd	$$⊢\phi \to {\left(\frac{M}{2}\right)}^2=\frac{M^2}{2^2}$$
26	22	sqcld	$$⊢\phi \to M^2\in ℂ$$
27	26 19 19 24 24	divdiv1d	$$⊢\phi \to \frac{\frac{M^2}{2}}{2}=\frac{M^2}{2\cdot 2}$$
28	21 25 27	3eqtr4d	$$⊢\phi \to {\left(\frac{M}{2}\right)}^2=\frac{\frac{M^2}{2}}{2}$$
29	18 28	breqtrd	$$⊢\phi \to B^2\le \frac{\frac{M^2}{2}}{2}$$