Theorem jm2.19lem2

Description: Lemma for jm2.19 . (Contributed by Stefan O'Rear, 23-Sep-2014)

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

Proof

Step	Hyp	Ref	Expression
1		frmy	⊢ Yrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℤ
2	1	fovcl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) → ( 𝐴 Yrm 𝑀 ) ∈ ℤ )
3	2	3adant3	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm 𝑀 ) ∈ ℤ )
4	1	fovcl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm 𝑁 ) ∈ ℤ )
5	4	3adant2	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm 𝑁 ) ∈ ℤ )
6		frmx	⊢ Xrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℕ0
7	6	fovcl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) → ( 𝐴 Xrm 𝑀 ) ∈ ℕ0 )
8	7	3adant3	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm 𝑀 ) ∈ ℕ0 )
9	8	nn0zd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm 𝑀 ) ∈ ℤ )
10	3 9	gcdcomd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Yrm 𝑀 ) gcd ( 𝐴 Xrm 𝑀 ) ) = ( ( 𝐴 Xrm 𝑀 ) gcd ( 𝐴 Yrm 𝑀 ) ) )
11		jm2.19lem1	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) → ( ( 𝐴 Xrm 𝑀 ) gcd ( 𝐴 Yrm 𝑀 ) ) = 1 )
12	11	3adant3	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Xrm 𝑀 ) gcd ( 𝐴 Yrm 𝑀 ) ) = 1 )
13	10 12	eqtrd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Yrm 𝑀 ) gcd ( 𝐴 Xrm 𝑀 ) ) = 1 )
14		coprmdvdsb	⊢ ( ( ( 𝐴 Yrm 𝑀 ) ∈ ℤ ∧ ( 𝐴 Yrm 𝑁 ) ∈ ℤ ∧ ( ( 𝐴 Xrm 𝑀 ) ∈ ℤ ∧ ( ( 𝐴 Yrm 𝑀 ) gcd ( 𝐴 Xrm 𝑀 ) ) = 1 ) ) → ( ( 𝐴 Yrm 𝑀 ) ∥ ( 𝐴 Yrm 𝑁 ) ↔ ( 𝐴 Yrm 𝑀 ) ∥ ( ( 𝐴 Xrm 𝑀 ) · ( 𝐴 Yrm 𝑁 ) ) ) )
15	3 5 9 13 14	syl112anc	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Yrm 𝑀 ) ∥ ( 𝐴 Yrm 𝑁 ) ↔ ( 𝐴 Yrm 𝑀 ) ∥ ( ( 𝐴 Xrm 𝑀 ) · ( 𝐴 Yrm 𝑁 ) ) ) )
16	8	nn0cnd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm 𝑀 ) ∈ ℂ )
17	5	zcnd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm 𝑁 ) ∈ ℂ )
18	16 17	mulcomd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Xrm 𝑀 ) · ( 𝐴 Yrm 𝑁 ) ) = ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Xrm 𝑀 ) ) )
19	18	breq2d	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Yrm 𝑀 ) ∥ ( ( 𝐴 Xrm 𝑀 ) · ( 𝐴 Yrm 𝑁 ) ) ↔ ( 𝐴 Yrm 𝑀 ) ∥ ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Xrm 𝑀 ) ) ) )
20	15 19	bitrd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Yrm 𝑀 ) ∥ ( 𝐴 Yrm 𝑁 ) ↔ ( 𝐴 Yrm 𝑀 ) ∥ ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Xrm 𝑀 ) ) ) )
21	5 9	zmulcld	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Xrm 𝑀 ) ) ∈ ℤ )
22	6	fovcl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm 𝑁 ) ∈ ℕ0 )
23	22	3adant2	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm 𝑁 ) ∈ ℕ0 )
24	23	nn0zd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm 𝑁 ) ∈ ℤ )
25	24 3	zmulcld	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Yrm 𝑀 ) ) ∈ ℤ )
26		dvdsmul2	⊢ ( ( ( 𝐴 Xrm 𝑁 ) ∈ ℤ ∧ ( 𝐴 Yrm 𝑀 ) ∈ ℤ ) → ( 𝐴 Yrm 𝑀 ) ∥ ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Yrm 𝑀 ) ) )
27	24 3 26	syl2anc	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm 𝑀 ) ∥ ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Yrm 𝑀 ) ) )
28		dvdsadd2b	⊢ ( ( ( 𝐴 Yrm 𝑀 ) ∈ ℤ ∧ ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Xrm 𝑀 ) ) ∈ ℤ ∧ ( ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Yrm 𝑀 ) ) ∈ ℤ ∧ ( 𝐴 Yrm 𝑀 ) ∥ ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Yrm 𝑀 ) ) ) ) → ( ( 𝐴 Yrm 𝑀 ) ∥ ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Xrm 𝑀 ) ) ↔ ( 𝐴 Yrm 𝑀 ) ∥ ( ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Yrm 𝑀 ) ) + ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Xrm 𝑀 ) ) ) ) )
29	3 21 25 27 28	syl112anc	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Yrm 𝑀 ) ∥ ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Xrm 𝑀 ) ) ↔ ( 𝐴 Yrm 𝑀 ) ∥ ( ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Yrm 𝑀 ) ) + ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Xrm 𝑀 ) ) ) ) )
30		rmyadd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝐴 Yrm ( 𝑁 + 𝑀 ) ) = ( ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Xrm 𝑀 ) ) + ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Yrm 𝑀 ) ) ) )
31	30	3com23	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm ( 𝑁 + 𝑀 ) ) = ( ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Xrm 𝑀 ) ) + ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Yrm 𝑀 ) ) ) )
32	17 16	mulcld	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Xrm 𝑀 ) ) ∈ ℂ )
33	23	nn0cnd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm 𝑁 ) ∈ ℂ )
34	3	zcnd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm 𝑀 ) ∈ ℂ )
35	33 34	mulcld	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Yrm 𝑀 ) ) ∈ ℂ )
36	32 35	addcomd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Xrm 𝑀 ) ) + ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Yrm 𝑀 ) ) ) = ( ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Yrm 𝑀 ) ) + ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Xrm 𝑀 ) ) ) )
37	31 36	eqtr2d	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Yrm 𝑀 ) ) + ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Xrm 𝑀 ) ) ) = ( 𝐴 Yrm ( 𝑁 + 𝑀 ) ) )
38	37	breq2d	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Yrm 𝑀 ) ∥ ( ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Yrm 𝑀 ) ) + ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Xrm 𝑀 ) ) ) ↔ ( 𝐴 Yrm 𝑀 ) ∥ ( 𝐴 Yrm ( 𝑁 + 𝑀 ) ) ) )
39	20 29 38	3bitrd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Yrm 𝑀 ) ∥ ( 𝐴 Yrm 𝑁 ) ↔ ( 𝐴 Yrm 𝑀 ) ∥ ( 𝐴 Yrm ( 𝑁 + 𝑀 ) ) ) )