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

Metamath Proof Explorer

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 ) )