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