4sqlem10

	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})$
	4sqlem10.5	$⊢ (φ \land ψ) \to (\frac{\frac{M^{2}}{2}}{2}) - B^{2} = 0$
Assertion	4sqlem10	$⊢ (φ \land ψ) \to M^{2} ∥ (A^{2} - (\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		4sqlem10.5	$⊢ (φ \land ψ) \to (\frac{\frac{M^{2}}{2}}{2}) - B^{2} = 0$
5	2	adantr	$⊢ (φ \land ψ) \to M \in ℕ$
6	5	nnzd	$⊢ (φ \land ψ) \to M \in ℤ$
7		zsqcl	$⊢ M \in ℤ \to M^{2} \in ℤ$
8	6 7	syl	$⊢ (φ \land ψ) \to M^{2} \in ℤ$
9	1	adantr	$⊢ (φ \land ψ) \to A \in ℤ$
10	5	nnred	$⊢ (φ \land ψ) \to M \in ℝ$
11	10	rehalfcld	$⊢ (φ \land ψ) \to \frac{M}{2} \in ℝ$
12	11	recnd	$⊢ (φ \land ψ) \to \frac{M}{2} \in ℂ$
13	12	negnegd	$⊢ (φ \land ψ) \to - (- \frac{M}{2}) = \frac{M}{2}$
14	1 2 3	4sqlem5	$⊢ φ \to (B \in ℤ \land \frac{A - B}{M} \in ℤ)$
15	14	adantr	$⊢ (φ \land ψ) \to (B \in ℤ \land \frac{A - B}{M} \in ℤ)$
16	15	simpld	$⊢ (φ \land ψ) \to B \in ℤ$
17	16	zred	$⊢ (φ \land ψ) \to B \in ℝ$
18	1 2 3	4sqlem6	$⊢ φ \to (- \frac{M}{2} \leq B \land B < \frac{M}{2})$
19	18	adantr	$⊢ (φ \land ψ) \to (- \frac{M}{2} \leq B \land B < \frac{M}{2})$
20	19	simprd	$⊢ (φ \land ψ) \to B < \frac{M}{2}$
21	17 20	ltned	$⊢ (φ \land ψ) \to B \neq \frac{M}{2}$
22	21	neneqd	$⊢ (φ \land ψ) \to \neg B = \frac{M}{2}$
23		2cnd	$⊢ (φ \land ψ) \to 2 \in ℂ$
24	23	sqvald	$⊢ (φ \land ψ) \to 2^{2} = 2 \cdot 2$
25	24	oveq2d	$⊢ (φ \land ψ) \to \frac{M^{2}}{2^{2}} = \frac{M^{2}}{2 \cdot 2}$
26	5	nncnd	$⊢ (φ \land ψ) \to M \in ℂ$
27		2ne0	$⊢ 2 \neq 0$
28	27	a1i	$⊢ (φ \land ψ) \to 2 \neq 0$
29	26 23 28	sqdivd	$⊢ (φ \land ψ) \to {(\frac{M}{2})}^{2} = \frac{M^{2}}{2^{2}}$
30	26	sqcld	$⊢ (φ \land ψ) \to M^{2} \in ℂ$
31	30 23 23 28 28	divdiv1d	$⊢ (φ \land ψ) \to \frac{\frac{M^{2}}{2}}{2} = \frac{M^{2}}{2 \cdot 2}$
32	25 29 31	3eqtr4d	$⊢ (φ \land ψ) \to {(\frac{M}{2})}^{2} = \frac{\frac{M^{2}}{2}}{2}$
33	30	halfcld	$⊢ (φ \land ψ) \to \frac{M^{2}}{2} \in ℂ$
34	33	halfcld	$⊢ (φ \land ψ) \to \frac{\frac{M^{2}}{2}}{2} \in ℂ$
35	16	zcnd	$⊢ (φ \land ψ) \to B \in ℂ$
36	35	sqcld	$⊢ (φ \land ψ) \to B^{2} \in ℂ$
37	34 36 4	subeq0d	$⊢ (φ \land ψ) \to \frac{\frac{M^{2}}{2}}{2} = B^{2}$
38	32 37	eqtr2d	$⊢ (φ \land ψ) \to B^{2} = {(\frac{M}{2})}^{2}$
39		sqeqor	$⊢ (B \in ℂ \land \frac{M}{2} \in ℂ) \to (B^{2} = {(\frac{M}{2})}^{2} \leftrightarrow (B = \frac{M}{2} \lor B = - \frac{M}{2}))$
40	35 12 39	syl2anc	$⊢ (φ \land ψ) \to (B^{2} = {(\frac{M}{2})}^{2} \leftrightarrow (B = \frac{M}{2} \lor B = - \frac{M}{2}))$
41	38 40	mpbid	$⊢ (φ \land ψ) \to (B = \frac{M}{2} \lor B = - \frac{M}{2})$
42	41	ord	$⊢ (φ \land ψ) \to (\neg B = \frac{M}{2} \to B = - \frac{M}{2})$
43	22 42	mpd	$⊢ (φ \land ψ) \to B = - \frac{M}{2}$
44	43 16	eqeltrrd	$⊢ (φ \land ψ) \to - \frac{M}{2} \in ℤ$
45	44	znegcld	$⊢ (φ \land ψ) \to - (- \frac{M}{2}) \in ℤ$
46	13 45	eqeltrrd	$⊢ (φ \land ψ) \to \frac{M}{2} \in ℤ$
47	9 46	zaddcld	$⊢ (φ \land ψ) \to A + (\frac{M}{2}) \in ℤ$
48		zsqcl	$⊢ A + (\frac{M}{2}) \in ℤ \to {(A + (\frac{M}{2}))}^{2} \in ℤ$
49	47 48	syl	$⊢ (φ \land ψ) \to {(A + (\frac{M}{2}))}^{2} \in ℤ$
50	47 6	zmulcld	$⊢ (φ \land ψ) \to (A + (\frac{M}{2})) \cdot M \in ℤ$
51	47	zred	$⊢ (φ \land ψ) \to A + (\frac{M}{2}) \in ℝ$
52	5	nnrpd	$⊢ (φ \land ψ) \to M \in ℝ^{+}$
53	51 52	modcld	$⊢ (φ \land ψ) \to (A + (\frac{M}{2})) \mod M \in ℝ$
54	53	recnd	$⊢ (φ \land ψ) \to (A + (\frac{M}{2})) \mod M \in ℂ$
55		0cnd	$⊢ (φ \land ψ) \to 0 \in ℂ$
56		df-neg	$⊢ - \frac{M}{2} = 0 - (\frac{M}{2})$
57	43 3 56	3eqtr3g	$⊢ (φ \land ψ) \to ((A + (\frac{M}{2})) \mod M) - (\frac{M}{2}) = 0 - (\frac{M}{2})$
58	54 55 12 57	subcan2d	$⊢ (φ \land ψ) \to (A + (\frac{M}{2})) \mod M = 0$
59		dvdsval3	$⊢ (M \in ℕ \land A + (\frac{M}{2}) \in ℤ) \to (M ∥ (A + (\frac{M}{2})) \leftrightarrow (A + (\frac{M}{2})) \mod M = 0)$
60	5 47 59	syl2anc	$⊢ (φ \land ψ) \to (M ∥ (A + (\frac{M}{2})) \leftrightarrow (A + (\frac{M}{2})) \mod M = 0)$
61	58 60	mpbird	$⊢ (φ \land ψ) \to M ∥ (A + (\frac{M}{2}))$
62		dvdssq	$⊢ (M \in ℤ \land A + (\frac{M}{2}) \in ℤ) \to (M ∥ (A + (\frac{M}{2})) \leftrightarrow M^{2} ∥ {(A + (\frac{M}{2}))}^{2})$
63	6 47 62	syl2anc	$⊢ (φ \land ψ) \to (M ∥ (A + (\frac{M}{2})) \leftrightarrow M^{2} ∥ {(A + (\frac{M}{2}))}^{2})$
64	61 63	mpbid	$⊢ (φ \land ψ) \to M^{2} ∥ {(A + (\frac{M}{2}))}^{2}$
65	26	sqvald	$⊢ (φ \land ψ) \to M^{2} = M \cdot M$
66	5	nnne0d	$⊢ (φ \land ψ) \to M \neq 0$
67		dvdsmulcr	$⊢ (M \in ℤ \land A + (\frac{M}{2}) \in ℤ \land (M \in ℤ \land M \neq 0)) \to (M \cdot M ∥ (A + (\frac{M}{2})) \cdot M \leftrightarrow M ∥ (A + (\frac{M}{2})))$
68	6 47 6 66 67	syl112anc	$⊢ (φ \land ψ) \to (M \cdot M ∥ (A + (\frac{M}{2})) \cdot M \leftrightarrow M ∥ (A + (\frac{M}{2})))$
69	61 68	mpbird	$⊢ (φ \land ψ) \to M \cdot M ∥ (A + (\frac{M}{2})) \cdot M$
70	65 69	eqbrtrd	$⊢ (φ \land ψ) \to M^{2} ∥ (A + (\frac{M}{2})) \cdot M$
71	8 49 50 64 70	dvds2subd	$⊢ (φ \land ψ) \to M^{2} ∥ ({(A + (\frac{M}{2}))}^{2} - (A + (\frac{M}{2})) \cdot M)$
72	47	zcnd	$⊢ (φ \land ψ) \to A + (\frac{M}{2}) \in ℂ$
73	72	sqvald	$⊢ (φ \land ψ) \to {(A + (\frac{M}{2}))}^{2} = (A + (\frac{M}{2})) (A + (\frac{M}{2}))$
74	73	oveq1d	$⊢ (φ \land ψ) \to {(A + (\frac{M}{2}))}^{2} - (A + (\frac{M}{2})) \cdot M = (A + (\frac{M}{2})) (A + (\frac{M}{2})) - (A + (\frac{M}{2})) \cdot M$
75	72 72 26	subdid	$⊢ (φ \land ψ) \to (A + (\frac{M}{2})) (A + (\frac{M}{2}) - M) = (A + (\frac{M}{2})) (A + (\frac{M}{2})) - (A + (\frac{M}{2})) \cdot M$
76	26	2halvesd	$⊢ (φ \land ψ) \to (\frac{M}{2}) + (\frac{M}{2}) = M$
77	76	oveq2d	$⊢ (φ \land ψ) \to A + (\frac{M}{2}) - ((\frac{M}{2}) + (\frac{M}{2})) = A + (\frac{M}{2}) - M$
78	9	zcnd	$⊢ (φ \land ψ) \to A \in ℂ$
79	78 12 12	pnpcan2d	$⊢ (φ \land ψ) \to A + (\frac{M}{2}) - ((\frac{M}{2}) + (\frac{M}{2})) = A - (\frac{M}{2})$
80	77 79	eqtr3d	$⊢ (φ \land ψ) \to A + (\frac{M}{2}) - M = A - (\frac{M}{2})$
81	80	oveq2d	$⊢ (φ \land ψ) \to (A + (\frac{M}{2})) (A + (\frac{M}{2}) - M) = (A + (\frac{M}{2})) (A - (\frac{M}{2}))$
82		subsq	$⊢ (A \in ℂ \land \frac{M}{2} \in ℂ) \to A^{2} - {(\frac{M}{2})}^{2} = (A + (\frac{M}{2})) (A - (\frac{M}{2}))$
83	78 12 82	syl2anc	$⊢ (φ \land ψ) \to A^{2} - {(\frac{M}{2})}^{2} = (A + (\frac{M}{2})) (A - (\frac{M}{2}))$
84	32	oveq2d	$⊢ (φ \land ψ) \to A^{2} - {(\frac{M}{2})}^{2} = A^{2} - (\frac{\frac{M^{2}}{2}}{2})$
85	81 83 84	3eqtr2d	$⊢ (φ \land ψ) \to (A + (\frac{M}{2})) (A + (\frac{M}{2}) - M) = A^{2} - (\frac{\frac{M^{2}}{2}}{2})$
86	74 75 85	3eqtr2d	$⊢ (φ \land ψ) \to {(A + (\frac{M}{2}))}^{2} - (A + (\frac{M}{2})) \cdot M = A^{2} - (\frac{\frac{M^{2}}{2}}{2})$
87	71 86	breqtrd	$⊢ (φ \land ψ) \to M^{2} ∥ (A^{2} - (\frac{\frac{M^{2}}{2}}{2}))$

Metamath Proof Explorer

Theorem 4sqlem10

Proof