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	syl5eq	⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) = ( ( 𝐴 + ( 𝑀 / 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	⊢ ( 𝜑 → ( 𝐵 ∈ ℤ ∧ ( ( 𝐴 − 𝐵 ) / 𝑀 ) ∈ ℤ ) )