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 ⊢ ( 𝜑 → 𝐴 ∈ ℤ )
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 ) ) )