4sqlem7

	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	4sqlem7	$⊢ φ \to B^{2} \leq \frac{\frac{M^{2}}{2}}{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	1 2 3	4sqlem5	$⊢ φ \to (B \in ℤ \land \frac{A - B}{M} \in ℤ)$
5	4	simpld	$⊢ φ \to B \in ℤ$
6	5	zred	$⊢ φ \to B \in ℝ$
7	2	nnrpd	$⊢ φ \to M \in ℝ^{+}$
8	7	rphalfcld	$⊢ φ \to \frac{M}{2} \in ℝ^{+}$
9	8	rpred	$⊢ φ \to \frac{M}{2} \in ℝ$
10	1 2 3	4sqlem6	$⊢ φ \to (- \frac{M}{2} \leq B \land B < \frac{M}{2})$
11	10	simprd	$⊢ φ \to B < \frac{M}{2}$
12	6 9 11	ltled	$⊢ φ \to B \leq \frac{M}{2}$
13	10	simpld	$⊢ φ \to - \frac{M}{2} \leq B$
14	9 6 13	lenegcon1d	$⊢ φ \to - B \leq \frac{M}{2}$
15	8	rpge0d	$⊢ φ \to 0 \leq \frac{M}{2}$
16		lenegsq	$⊢ (B \in ℝ \land \frac{M}{2} \in ℝ \land 0 \leq \frac{M}{2}) \to ((B \leq \frac{M}{2} \land - B \leq \frac{M}{2}) \leftrightarrow B^{2} \leq {(\frac{M}{2})}^{2})$
17	6 9 15 16	syl3anc	$⊢ φ \to ((B \leq \frac{M}{2} \land - B \leq \frac{M}{2}) \leftrightarrow B^{2} \leq {(\frac{M}{2})}^{2})$
18	12 14 17	mpbi2and	$⊢ φ \to B^{2} \leq {(\frac{M}{2})}^{2}$
19		2cnd	$⊢ φ \to 2 \in ℂ$
20	19	sqvald	$⊢ φ \to 2^{2} = 2 \cdot 2$
21	20	oveq2d	$⊢ φ \to \frac{M^{2}}{2^{2}} = \frac{M^{2}}{2 \cdot 2}$
22	2	nncnd	$⊢ φ \to M \in ℂ$
23		2ne0	$⊢ 2 \neq 0$
24	23	a1i	$⊢ φ \to 2 \neq 0$
25	22 19 24	sqdivd	$⊢ φ \to {(\frac{M}{2})}^{2} = \frac{M^{2}}{2^{2}}$
26	22	sqcld	$⊢ φ \to M^{2} \in ℂ$
27	26 19 19 24 24	divdiv1d	$⊢ φ \to \frac{\frac{M^{2}}{2}}{2} = \frac{M^{2}}{2 \cdot 2}$
28	21 25 27	3eqtr4d	$⊢ φ \to {(\frac{M}{2})}^{2} = \frac{\frac{M^{2}}{2}}{2}$
29	18 28	breqtrd	$⊢ φ \to B^{2} \leq \frac{\frac{M^{2}}{2}}{2}$

Metamath Proof Explorer

Theorem 4sqlem7

Proof