This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 4sqlem6

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

Ref Expression
Hypotheses 4sqlem5.2 ⊢ φ → A ∈ ℤ
4sqlem5.3 ⊢ φ → M ∈ ℕ
4sqlem5.4 ⊢ B = A + M 2 mod M − M 2
Assertion 4sqlem6 ⊢ φ → − M 2 ≤ B ∧ B < M 2

Proof

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