Theorem jm2.19lem4

Description: Lemma for jm2.19 . Extend to ZZ by symmetry. TODO: use zindbi . (Contributed by Stefan O'Rear, 26-Sep-2014)

	Ref	Expression
Assertion	jm2.19lem4	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐼 ∈ ℤ ) → ( ( 𝐴 Yrm 𝑀 ) ∥ ( 𝐴 Yrm 𝑁 ) ↔ ( 𝐴 Yrm 𝑀 ) ∥ ( 𝐴 Yrm ( 𝑁 + ( 𝐼 · 𝑀 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		elznn0	⊢ ( 𝐼 ∈ ℤ ↔ ( 𝐼 ∈ ℝ ∧ ( 𝐼 ∈ ℕ0 ∨ - 𝐼 ∈ ℕ0 ) ) )
2		jm2.19lem3	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐼 ∈ ℕ0 ) → ( ( 𝐴 Yrm 𝑀 ) ∥ ( 𝐴 Yrm 𝑁 ) ↔ ( 𝐴 Yrm 𝑀 ) ∥ ( 𝐴 Yrm ( 𝑁 + ( 𝐼 · 𝑀 ) ) ) ) )
3	2	3expia	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( 𝐼 ∈ ℕ0 → ( ( 𝐴 Yrm 𝑀 ) ∥ ( 𝐴 Yrm 𝑁 ) ↔ ( 𝐴 Yrm 𝑀 ) ∥ ( 𝐴 Yrm ( 𝑁 + ( 𝐼 · 𝑀 ) ) ) ) ) )
4	3	adantr	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ∧ 𝐼 ∈ ℝ ) → ( 𝐼 ∈ ℕ0 → ( ( 𝐴 Yrm 𝑀 ) ∥ ( 𝐴 Yrm 𝑁 ) ↔ ( 𝐴 Yrm 𝑀 ) ∥ ( 𝐴 Yrm ( 𝑁 + ( 𝐼 · 𝑀 ) ) ) ) ) )
5		simplll	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ∧ 𝐼 ∈ ℝ ) ∧ - 𝐼 ∈ ℕ0 ) → 𝐴 ∈ ( ℤ≥ ‘ 2 ) )
6		simprl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → 𝑀 ∈ ℤ )
7	6	ad2antrr	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ∧ 𝐼 ∈ ℝ ) ∧ - 𝐼 ∈ ℕ0 ) → 𝑀 ∈ ℤ )
8		simprr	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → 𝑁 ∈ ℤ )
9	8	ad2antrr	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ∧ 𝐼 ∈ ℝ ) ∧ - 𝐼 ∈ ℕ0 ) → 𝑁 ∈ ℤ )
10		nn0z	⊢ ( - 𝐼 ∈ ℕ0 → - 𝐼 ∈ ℤ )
11	10	adantl	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ∧ 𝐼 ∈ ℝ ) ∧ - 𝐼 ∈ ℕ0 ) → - 𝐼 ∈ ℤ )
12		simplr	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ∧ 𝐼 ∈ ℝ ) ∧ - 𝐼 ∈ ℕ0 ) → 𝐼 ∈ ℝ )
13	12	recnd	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ∧ 𝐼 ∈ ℝ ) ∧ - 𝐼 ∈ ℕ0 ) → 𝐼 ∈ ℂ )
14		znegclb	⊢ ( 𝐼 ∈ ℂ → ( 𝐼 ∈ ℤ ↔ - 𝐼 ∈ ℤ ) )
15	13 14	syl	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ∧ 𝐼 ∈ ℝ ) ∧ - 𝐼 ∈ ℕ0 ) → ( 𝐼 ∈ ℤ ↔ - 𝐼 ∈ ℤ ) )
16	11 15	mpbird	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ∧ 𝐼 ∈ ℝ ) ∧ - 𝐼 ∈ ℕ0 ) → 𝐼 ∈ ℤ )
17	16 7	zmulcld	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ∧ 𝐼 ∈ ℝ ) ∧ - 𝐼 ∈ ℕ0 ) → ( 𝐼 · 𝑀 ) ∈ ℤ )
18	9 17	zaddcld	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ∧ 𝐼 ∈ ℝ ) ∧ - 𝐼 ∈ ℕ0 ) → ( 𝑁 + ( 𝐼 · 𝑀 ) ) ∈ ℤ )
19		simpr	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ∧ 𝐼 ∈ ℝ ) ∧ - 𝐼 ∈ ℕ0 ) → - 𝐼 ∈ ℕ0 )
20		jm2.19lem3	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ ( 𝑁 + ( 𝐼 · 𝑀 ) ) ∈ ℤ ) ∧ - 𝐼 ∈ ℕ0 ) → ( ( 𝐴 Yrm 𝑀 ) ∥ ( 𝐴 Yrm ( 𝑁 + ( 𝐼 · 𝑀 ) ) ) ↔ ( 𝐴 Yrm 𝑀 ) ∥ ( 𝐴 Yrm ( ( 𝑁 + ( 𝐼 · 𝑀 ) ) + ( - 𝐼 · 𝑀 ) ) ) ) )
21	5 7 18 19 20	syl121anc	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ∧ 𝐼 ∈ ℝ ) ∧ - 𝐼 ∈ ℕ0 ) → ( ( 𝐴 Yrm 𝑀 ) ∥ ( 𝐴 Yrm ( 𝑁 + ( 𝐼 · 𝑀 ) ) ) ↔ ( 𝐴 Yrm 𝑀 ) ∥ ( 𝐴 Yrm ( ( 𝑁 + ( 𝐼 · 𝑀 ) ) + ( - 𝐼 · 𝑀 ) ) ) ) )
22		zcn	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ )
23	22	ad2antrl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → 𝑀 ∈ ℂ )
24	23	ad2antrr	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ∧ 𝐼 ∈ ℝ ) ∧ - 𝐼 ∈ ℕ0 ) → 𝑀 ∈ ℂ )
25	13 24	mulneg1d	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ∧ 𝐼 ∈ ℝ ) ∧ - 𝐼 ∈ ℕ0 ) → ( - 𝐼 · 𝑀 ) = - ( 𝐼 · 𝑀 ) )
26	25	oveq2d	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ∧ 𝐼 ∈ ℝ ) ∧ - 𝐼 ∈ ℕ0 ) → ( ( 𝑁 + ( 𝐼 · 𝑀 ) ) + ( - 𝐼 · 𝑀 ) ) = ( ( 𝑁 + ( 𝐼 · 𝑀 ) ) + - ( 𝐼 · 𝑀 ) ) )
27		zcn	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
28	27	ad2antll	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → 𝑁 ∈ ℂ )
29	28	ad2antrr	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ∧ 𝐼 ∈ ℝ ) ∧ - 𝐼 ∈ ℕ0 ) → 𝑁 ∈ ℂ )
30	13 24	mulcld	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ∧ 𝐼 ∈ ℝ ) ∧ - 𝐼 ∈ ℕ0 ) → ( 𝐼 · 𝑀 ) ∈ ℂ )
31	29 30	addcld	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ∧ 𝐼 ∈ ℝ ) ∧ - 𝐼 ∈ ℕ0 ) → ( 𝑁 + ( 𝐼 · 𝑀 ) ) ∈ ℂ )
32	31 30	negsubd	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ∧ 𝐼 ∈ ℝ ) ∧ - 𝐼 ∈ ℕ0 ) → ( ( 𝑁 + ( 𝐼 · 𝑀 ) ) + - ( 𝐼 · 𝑀 ) ) = ( ( 𝑁 + ( 𝐼 · 𝑀 ) ) − ( 𝐼 · 𝑀 ) ) )
33	29 30	pncand	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ∧ 𝐼 ∈ ℝ ) ∧ - 𝐼 ∈ ℕ0 ) → ( ( 𝑁 + ( 𝐼 · 𝑀 ) ) − ( 𝐼 · 𝑀 ) ) = 𝑁 )
34	26 32 33	3eqtrd	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ∧ 𝐼 ∈ ℝ ) ∧ - 𝐼 ∈ ℕ0 ) → ( ( 𝑁 + ( 𝐼 · 𝑀 ) ) + ( - 𝐼 · 𝑀 ) ) = 𝑁 )
35	34	oveq2d	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ∧ 𝐼 ∈ ℝ ) ∧ - 𝐼 ∈ ℕ0 ) → ( 𝐴 Yrm ( ( 𝑁 + ( 𝐼 · 𝑀 ) ) + ( - 𝐼 · 𝑀 ) ) ) = ( 𝐴 Yrm 𝑁 ) )
36	35	breq2d	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ∧ 𝐼 ∈ ℝ ) ∧ - 𝐼 ∈ ℕ0 ) → ( ( 𝐴 Yrm 𝑀 ) ∥ ( 𝐴 Yrm ( ( 𝑁 + ( 𝐼 · 𝑀 ) ) + ( - 𝐼 · 𝑀 ) ) ) ↔ ( 𝐴 Yrm 𝑀 ) ∥ ( 𝐴 Yrm 𝑁 ) ) )
37	21 36	bitr2d	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ∧ 𝐼 ∈ ℝ ) ∧ - 𝐼 ∈ ℕ0 ) → ( ( 𝐴 Yrm 𝑀 ) ∥ ( 𝐴 Yrm 𝑁 ) ↔ ( 𝐴 Yrm 𝑀 ) ∥ ( 𝐴 Yrm ( 𝑁 + ( 𝐼 · 𝑀 ) ) ) ) )
38	37	ex	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ∧ 𝐼 ∈ ℝ ) → ( - 𝐼 ∈ ℕ0 → ( ( 𝐴 Yrm 𝑀 ) ∥ ( 𝐴 Yrm 𝑁 ) ↔ ( 𝐴 Yrm 𝑀 ) ∥ ( 𝐴 Yrm ( 𝑁 + ( 𝐼 · 𝑀 ) ) ) ) ) )
39	4 38	jaod	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ∧ 𝐼 ∈ ℝ ) → ( ( 𝐼 ∈ ℕ0 ∨ - 𝐼 ∈ ℕ0 ) → ( ( 𝐴 Yrm 𝑀 ) ∥ ( 𝐴 Yrm 𝑁 ) ↔ ( 𝐴 Yrm 𝑀 ) ∥ ( 𝐴 Yrm ( 𝑁 + ( 𝐼 · 𝑀 ) ) ) ) ) )
40	39	expimpd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( 𝐼 ∈ ℝ ∧ ( 𝐼 ∈ ℕ0 ∨ - 𝐼 ∈ ℕ0 ) ) → ( ( 𝐴 Yrm 𝑀 ) ∥ ( 𝐴 Yrm 𝑁 ) ↔ ( 𝐴 Yrm 𝑀 ) ∥ ( 𝐴 Yrm ( 𝑁 + ( 𝐼 · 𝑀 ) ) ) ) ) )
41	1 40	syl5bi	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( 𝐼 ∈ ℤ → ( ( 𝐴 Yrm 𝑀 ) ∥ ( 𝐴 Yrm 𝑁 ) ↔ ( 𝐴 Yrm 𝑀 ) ∥ ( 𝐴 Yrm ( 𝑁 + ( 𝐼 · 𝑀 ) ) ) ) ) )
42	41	3impia	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐼 ∈ ℤ ) → ( ( 𝐴 Yrm 𝑀 ) ∥ ( 𝐴 Yrm 𝑁 ) ↔ ( 𝐴 Yrm 𝑀 ) ∥ ( 𝐴 Yrm ( 𝑁 + ( 𝐼 · 𝑀 ) ) ) ) )