Metamath Proof Explorer

Theorem 4sqlem5

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 4sqlem5 ⊢ φ → B ∈ ℤ ∧ A − B M ∈ ℤ

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 1 zcnd ⊢ φ → A ∈ ℂ
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 10 recnd ⊢ φ → A + M 2 mod M ∈ ℂ
12 7 recnd ⊢ φ → M 2 ∈ ℂ
13 11 12 subcld ⊢ φ → A + M 2 mod M − M 2 ∈ ℂ
14 3 13 eqeltrid ⊢ φ → B ∈ ℂ
15 4 14 nncand ⊢ φ → A − A − B = B
16 4 14 subcld ⊢ φ → A − B ∈ ℂ
17 6 recnd ⊢ φ → M ∈ ℂ
18 2 nnne0d ⊢ φ → M ≠ 0
19 16 17 18 divcan1d ⊢ φ → A − B M ⋅ M = A − B
20 3 oveq2i ⊢ A − B = A − A + M 2 mod M − M 2
21 4 11 12 subsub3d ⊢ φ → A − A + M 2 mod M − M 2 = A + M 2 - A + M 2 mod M
22 20 21 syl5eq ⊢ φ → A − B = A + M 2 - A + M 2 mod M
23 22 oveq1d ⊢ φ → A − B M = A + M 2 - A + M 2 mod M M
24 moddifz ⊢ A + M 2 ∈ ℝ ∧ M ∈ ℝ + → A + M 2 - A + M 2 mod M M ∈ ℤ
25 8 9 24 syl2anc ⊢ φ → A + M 2 - A + M 2 mod M M ∈ ℤ
26 23 25 eqeltrd ⊢ φ → A − B M ∈ ℤ
27 2 nnzd ⊢ φ → M ∈ ℤ
28 26 27 zmulcld ⊢ φ → A − B M ⋅ M ∈ ℤ
29 19 28 eqeltrrd ⊢ φ → A − B ∈ ℤ
30 1 29 zsubcld ⊢ φ → A − A − B ∈ ℤ
31 15 30 eqeltrrd ⊢ φ → B ∈ ℤ
32 31 26 jca ⊢ φ → B ∈ ℤ ∧ A − B M ∈ ℤ