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

Metamath Proof Explorer

Theorem 4sqlem9

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

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

Proof

Step Hyp Ref Expression
1 4sqlem5.2 ⊢ ( 𝜑 → 𝐴 ∈ ℤ )
2 4sqlem5.3 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
3 4sqlem5.4 ⊢ 𝐵 = ( ( ( 𝐴 + ( 𝑀 / 2 ) ) mod 𝑀 ) − ( 𝑀 / 2 ) )
4 4sqlem9.5 ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝐵 ↑ 2 ) = 0 )
5 1 2 3 4sqlem5 ⊢ ( 𝜑 → ( 𝐵 ∈ ℤ ∧ ( ( 𝐴 − 𝐵 ) / 𝑀 ) ∈ ℤ ) )
6 5 simpld ⊢ ( 𝜑 → 𝐵 ∈ ℤ )
7 6 zcnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
8 sqeq0 ⊢ ( 𝐵 ∈ ℂ → ( ( 𝐵 ↑ 2 ) = 0 ↔ 𝐵 = 0 ) )
9 7 8 syl ⊢ ( 𝜑 → ( ( 𝐵 ↑ 2 ) = 0 ↔ 𝐵 = 0 ) )
10 9 biimpa ⊢ ( ( 𝜑 ∧ ( 𝐵 ↑ 2 ) = 0 ) → 𝐵 = 0 )
11 4 10 syldan ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐵 = 0 )
12 11 oveq2d ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝐴 − 𝐵 ) = ( 𝐴 − 0 ) )
13 1 adantr ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐴 ∈ ℤ )
14 13 zcnd ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐴 ∈ ℂ )
15 14 subid1d ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝐴 − 0 ) = 𝐴 )
16 12 15 eqtrd ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝐴 − 𝐵 ) = 𝐴 )
17 16 oveq1d ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝐴 − 𝐵 ) / 𝑀 ) = ( 𝐴 / 𝑀 ) )
18 5 simprd ⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) / 𝑀 ) ∈ ℤ )
19 18 adantr ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝐴 − 𝐵 ) / 𝑀 ) ∈ ℤ )
20 17 19 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝐴 / 𝑀 ) ∈ ℤ )
21 2 nnzd ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
22 2 nnne0d ⊢ ( 𝜑 → 𝑀 ≠ 0 )
23 dvdsval2 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝐴 ∈ ℤ ) → ( 𝑀 ∥ 𝐴 ↔ ( 𝐴 / 𝑀 ) ∈ ℤ ) )
24 21 22 1 23 syl3anc ⊢ ( 𝜑 → ( 𝑀 ∥ 𝐴 ↔ ( 𝐴 / 𝑀 ) ∈ ℤ ) )
25 24 adantr ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑀 ∥ 𝐴 ↔ ( 𝐴 / 𝑀 ) ∈ ℤ ) )
26 20 25 mpbird ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑀 ∥ 𝐴 )
27 dvdssq ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( 𝑀 ∥ 𝐴 ↔ ( 𝑀 ↑ 2 ) ∥ ( 𝐴 ↑ 2 ) ) )
28 21 13 27 syl2an2r ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑀 ∥ 𝐴 ↔ ( 𝑀 ↑ 2 ) ∥ ( 𝐴 ↑ 2 ) ) )
29 26 28 mpbid ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑀 ↑ 2 ) ∥ ( 𝐴 ↑ 2 ) )