Theorem 4sqlem6

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

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

Proof

Step	Hyp	Ref	Expression
1		4sqlem5.2	⊢ ( 𝜑 → 𝐴 ∈ ℤ )
2		4sqlem5.3	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
3		4sqlem5.4	⊢ 𝐵 = ( ( ( 𝐴 + ( 𝑀 / 2 ) ) mod 𝑀 ) − ( 𝑀 / 2 ) )
4		0red	⊢ ( 𝜑 → 0 ∈ ℝ )
5	1	zred	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
6	2	nnred	⊢ ( 𝜑 → 𝑀 ∈ ℝ )
7	6	rehalfcld	⊢ ( 𝜑 → ( 𝑀 / 2 ) ∈ ℝ )
8	5 7	readdcld	⊢ ( 𝜑 → ( 𝐴 + ( 𝑀 / 2 ) ) ∈ ℝ )
9	2	nnrpd	⊢ ( 𝜑 → 𝑀 ∈ ℝ+ )
10	8 9	modcld	⊢ ( 𝜑 → ( ( 𝐴 + ( 𝑀 / 2 ) ) mod 𝑀 ) ∈ ℝ )
11		modge0	⊢ ( ( ( 𝐴 + ( 𝑀 / 2 ) ) ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → 0 ≤ ( ( 𝐴 + ( 𝑀 / 2 ) ) mod 𝑀 ) )
12	8 9 11	syl2anc	⊢ ( 𝜑 → 0 ≤ ( ( 𝐴 + ( 𝑀 / 2 ) ) mod 𝑀 ) )
13	4 10 7 12	lesub1dd	⊢ ( 𝜑 → ( 0 − ( 𝑀 / 2 ) ) ≤ ( ( ( 𝐴 + ( 𝑀 / 2 ) ) mod 𝑀 ) − ( 𝑀 / 2 ) ) )
14		df-neg	⊢ - ( 𝑀 / 2 ) = ( 0 − ( 𝑀 / 2 ) )
15	13 14 3	3brtr4g	⊢ ( 𝜑 → - ( 𝑀 / 2 ) ≤ 𝐵 )
16		modlt	⊢ ( ( ( 𝐴 + ( 𝑀 / 2 ) ) ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( ( 𝐴 + ( 𝑀 / 2 ) ) mod 𝑀 ) < 𝑀 )
17	8 9 16	syl2anc	⊢ ( 𝜑 → ( ( 𝐴 + ( 𝑀 / 2 ) ) mod 𝑀 ) < 𝑀 )
18	2	nncnd	⊢ ( 𝜑 → 𝑀 ∈ ℂ )
19	18	2halvesd	⊢ ( 𝜑 → ( ( 𝑀 / 2 ) + ( 𝑀 / 2 ) ) = 𝑀 )
20	17 19	breqtrrd	⊢ ( 𝜑 → ( ( 𝐴 + ( 𝑀 / 2 ) ) mod 𝑀 ) < ( ( 𝑀 / 2 ) + ( 𝑀 / 2 ) ) )
21	10 7 7	ltsubaddd	⊢ ( 𝜑 → ( ( ( ( 𝐴 + ( 𝑀 / 2 ) ) mod 𝑀 ) − ( 𝑀 / 2 ) ) < ( 𝑀 / 2 ) ↔ ( ( 𝐴 + ( 𝑀 / 2 ) ) mod 𝑀 ) < ( ( 𝑀 / 2 ) + ( 𝑀 / 2 ) ) ) )
22	20 21	mpbird	⊢ ( 𝜑 → ( ( ( 𝐴 + ( 𝑀 / 2 ) ) mod 𝑀 ) − ( 𝑀 / 2 ) ) < ( 𝑀 / 2 ) )
23	3 22	eqbrtrid	⊢ ( 𝜑 → 𝐵 < ( 𝑀 / 2 ) )
24	15 23	jca	⊢ ( 𝜑 → ( - ( 𝑀 / 2 ) ≤ 𝐵 ∧ 𝐵 < ( 𝑀 / 2 ) ) )