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

Metamath Proof Explorer

Theorem 4sqlem5

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

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

Proof

Step Hyp Ref Expression
1 4sqlem5.2 ⊢ ( 𝜑 → 𝐴 ∈ ℤ )
2 4sqlem5.3 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
3 4sqlem5.4 ⊢ 𝐵 = ( ( ( 𝐴 + ( 𝑀 / 2 ) ) mod 𝑀 ) − ( 𝑀 / 2 ) )
4 1 zcnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
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 10 recnd ⊢ ( 𝜑 → ( ( 𝐴 + ( 𝑀 / 2 ) ) mod 𝑀 ) ∈ ℂ )
12 7 recnd ⊢ ( 𝜑 → ( 𝑀 / 2 ) ∈ ℂ )
13 11 12 subcld ⊢ ( 𝜑 → ( ( ( 𝐴 + ( 𝑀 / 2 ) ) mod 𝑀 ) − ( 𝑀 / 2 ) ) ∈ ℂ )
14 3 13 eqeltrid ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
15 4 14 nncand ⊢ ( 𝜑 → ( 𝐴 − ( 𝐴 − 𝐵 ) ) = 𝐵 )
16 4 14 subcld ⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) ∈ ℂ )
17 6 recnd ⊢ ( 𝜑 → 𝑀 ∈ ℂ )
18 2 nnne0d ⊢ ( 𝜑 → 𝑀 ≠ 0 )
19 16 17 18 divcan1d ⊢ ( 𝜑 → ( ( ( 𝐴 − 𝐵 ) / 𝑀 ) · 𝑀 ) = ( 𝐴 − 𝐵 ) )
20 3 oveq2i ⊢ ( 𝐴 − 𝐵 ) = ( 𝐴 − ( ( ( 𝐴 + ( 𝑀 / 2 ) ) mod 𝑀 ) − ( 𝑀 / 2 ) ) )
21 4 11 12 subsub3d ⊢ ( 𝜑 → ( 𝐴 − ( ( ( 𝐴 + ( 𝑀 / 2 ) ) mod 𝑀 ) − ( 𝑀 / 2 ) ) ) = ( ( 𝐴 + ( 𝑀 / 2 ) ) − ( ( 𝐴 + ( 𝑀 / 2 ) ) mod 𝑀 ) ) )
22 20 21 eqtrid ⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) = ( ( 𝐴 + ( 𝑀 / 2 ) ) − ( ( 𝐴 + ( 𝑀 / 2 ) ) mod 𝑀 ) ) )
23 22 oveq1d ⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) / 𝑀 ) = ( ( ( 𝐴 + ( 𝑀 / 2 ) ) − ( ( 𝐴 + ( 𝑀 / 2 ) ) mod 𝑀 ) ) / 𝑀 ) )
24 moddifz ⊢ ( ( ( 𝐴 + ( 𝑀 / 2 ) ) ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( ( ( 𝐴 + ( 𝑀 / 2 ) ) − ( ( 𝐴 + ( 𝑀 / 2 ) ) mod 𝑀 ) ) / 𝑀 ) ∈ ℤ )
25 8 9 24 syl2anc ⊢ ( 𝜑 → ( ( ( 𝐴 + ( 𝑀 / 2 ) ) − ( ( 𝐴 + ( 𝑀 / 2 ) ) mod 𝑀 ) ) / 𝑀 ) ∈ ℤ )
26 23 25 eqeltrd ⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) / 𝑀 ) ∈ ℤ )
27 2 nnzd ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
28 26 27 zmulcld ⊢ ( 𝜑 → ( ( ( 𝐴 − 𝐵 ) / 𝑀 ) · 𝑀 ) ∈ ℤ )
29 19 28 eqeltrrd ⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) ∈ ℤ )
30 1 29 zsubcld ⊢ ( 𝜑 → ( 𝐴 − ( 𝐴 − 𝐵 ) ) ∈ ℤ )
31 15 30 eqeltrrd ⊢ ( 𝜑 → 𝐵 ∈ ℤ )
32 31 26 jca ⊢ ( 𝜑 → ( 𝐵 ∈ ℤ ∧ ( ( 𝐴 − 𝐵 ) / 𝑀 ) ∈ ℤ ) )