Theorem 4sqlem7

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

	Ref	Expression
Hypotheses	4sqlem5.2	⊢ ( 𝜑 → 𝐴 ∈ ℤ )
	4sqlem5.3	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
	4sqlem5.4	⊢ 𝐵 = ( ( ( 𝐴 + ( 𝑀 / 2 ) ) mod 𝑀 ) − ( 𝑀 / 2 ) )
Assertion	4sqlem7	⊢ ( 𝜑 → ( 𝐵 ↑ 2 ) ≤ ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) )

Proof

Step	Hyp	Ref	Expression
1		4sqlem5.2	⊢ ( 𝜑 → 𝐴 ∈ ℤ )
2		4sqlem5.3	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
3		4sqlem5.4	⊢ 𝐵 = ( ( ( 𝐴 + ( 𝑀 / 2 ) ) mod 𝑀 ) − ( 𝑀 / 2 ) )
4	1 2 3	4sqlem5	⊢ ( 𝜑 → ( 𝐵 ∈ ℤ ∧ ( ( 𝐴 − 𝐵 ) / 𝑀 ) ∈ ℤ ) )
5	4	simpld	⊢ ( 𝜑 → 𝐵 ∈ ℤ )
6	5	zred	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
7	2	nnrpd	⊢ ( 𝜑 → 𝑀 ∈ ℝ+ )
8	7	rphalfcld	⊢ ( 𝜑 → ( 𝑀 / 2 ) ∈ ℝ+ )
9	8	rpred	⊢ ( 𝜑 → ( 𝑀 / 2 ) ∈ ℝ )
10	1 2 3	4sqlem6	⊢ ( 𝜑 → ( - ( 𝑀 / 2 ) ≤ 𝐵 ∧ 𝐵 < ( 𝑀 / 2 ) ) )
11	10	simprd	⊢ ( 𝜑 → 𝐵 < ( 𝑀 / 2 ) )
12	6 9 11	ltled	⊢ ( 𝜑 → 𝐵 ≤ ( 𝑀 / 2 ) )
13	10	simpld	⊢ ( 𝜑 → - ( 𝑀 / 2 ) ≤ 𝐵 )
14	9 6 13	lenegcon1d	⊢ ( 𝜑 → - 𝐵 ≤ ( 𝑀 / 2 ) )
15	8	rpge0d	⊢ ( 𝜑 → 0 ≤ ( 𝑀 / 2 ) )
16		lenegsq	⊢ ( ( 𝐵 ∈ ℝ ∧ ( 𝑀 / 2 ) ∈ ℝ ∧ 0 ≤ ( 𝑀 / 2 ) ) → ( ( 𝐵 ≤ ( 𝑀 / 2 ) ∧ - 𝐵 ≤ ( 𝑀 / 2 ) ) ↔ ( 𝐵 ↑ 2 ) ≤ ( ( 𝑀 / 2 ) ↑ 2 ) ) )
17	6 9 15 16	syl3anc	⊢ ( 𝜑 → ( ( 𝐵 ≤ ( 𝑀 / 2 ) ∧ - 𝐵 ≤ ( 𝑀 / 2 ) ) ↔ ( 𝐵 ↑ 2 ) ≤ ( ( 𝑀 / 2 ) ↑ 2 ) ) )
18	12 14 17	mpbi2and	⊢ ( 𝜑 → ( 𝐵 ↑ 2 ) ≤ ( ( 𝑀 / 2 ) ↑ 2 ) )
19		2cnd	⊢ ( 𝜑 → 2 ∈ ℂ )
20	19	sqvald	⊢ ( 𝜑 → ( 2 ↑ 2 ) = ( 2 · 2 ) )
21	20	oveq2d	⊢ ( 𝜑 → ( ( 𝑀 ↑ 2 ) / ( 2 ↑ 2 ) ) = ( ( 𝑀 ↑ 2 ) / ( 2 · 2 ) ) )
22	2	nncnd	⊢ ( 𝜑 → 𝑀 ∈ ℂ )
23		2ne0	⊢ 2 ≠ 0
24	23	a1i	⊢ ( 𝜑 → 2 ≠ 0 )
25	22 19 24	sqdivd	⊢ ( 𝜑 → ( ( 𝑀 / 2 ) ↑ 2 ) = ( ( 𝑀 ↑ 2 ) / ( 2 ↑ 2 ) ) )
26	22	sqcld	⊢ ( 𝜑 → ( 𝑀 ↑ 2 ) ∈ ℂ )
27	26 19 19 24 24	divdiv1d	⊢ ( 𝜑 → ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) = ( ( 𝑀 ↑ 2 ) / ( 2 · 2 ) ) )
28	21 25 27	3eqtr4d	⊢ ( 𝜑 → ( ( 𝑀 / 2 ) ↑ 2 ) = ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) )
29	18 28	breqtrd	⊢ ( 𝜑 → ( 𝐵 ↑ 2 ) ≤ ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) )