jm2.19lem2

		Ref	Expression
	Assertion	jm2.19lem2	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to ((A Y_{rm} M) ∥ (A Y_{rm} N) \leftrightarrow (A Y_{rm} M) ∥ (A Y_{rm} (N + M)))$

Proof

Step	Hyp	Ref	Expression
1		frmy	$⊢ Y_{rm} : ℤ_{\geq 2} \times ℤ ⟶ ℤ$
2	1	fovcl	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ) \to A Y_{rm} M \in ℤ$
3	2	3adant3	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to A Y_{rm} M \in ℤ$
4	1	fovcl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A Y_{rm} N \in ℤ$
5	4	3adant2	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to A Y_{rm} N \in ℤ$
6		frmx	$⊢ X_{rm} : ℤ_{\geq 2} \times ℤ ⟶ ℕ_{0}$
7	6	fovcl	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ) \to A X_{rm} M \in ℕ_{0}$
8	7	3adant3	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to A X_{rm} M \in ℕ_{0}$
9	8	nn0zd	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to A X_{rm} M \in ℤ$
10	3 9	gcdcomd	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to (A Y_{rm} M) \gcd (A X_{rm} M) = (A X_{rm} M) \gcd (A Y_{rm} M)$
11		jm2.19lem1	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ) \to (A X_{rm} M) \gcd (A Y_{rm} M) = 1$
12	11	3adant3	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to (A X_{rm} M) \gcd (A Y_{rm} M) = 1$
13	10 12	eqtrd	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to (A Y_{rm} M) \gcd (A X_{rm} M) = 1$
14		coprmdvdsb	$⊢ (A Y_{rm} M \in ℤ \land A Y_{rm} N \in ℤ \land (A X_{rm} M \in ℤ \land (A Y_{rm} M) \gcd (A X_{rm} M) = 1)) \to ((A Y_{rm} M) ∥ (A Y_{rm} N) \leftrightarrow (A Y_{rm} M) ∥ (A X_{rm} M) (A Y_{rm} N))$
15	3 5 9 13 14	syl112anc	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to ((A Y_{rm} M) ∥ (A Y_{rm} N) \leftrightarrow (A Y_{rm} M) ∥ (A X_{rm} M) (A Y_{rm} N))$
16	8	nn0cnd	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to A X_{rm} M \in ℂ$
17	5	zcnd	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to A Y_{rm} N \in ℂ$
18	16 17	mulcomd	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to (A X_{rm} M) (A Y_{rm} N) = (A Y_{rm} N) (A X_{rm} M)$
19	18	breq2d	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to ((A Y_{rm} M) ∥ (A X_{rm} M) (A Y_{rm} N) \leftrightarrow (A Y_{rm} M) ∥ (A Y_{rm} N) (A X_{rm} M))$
20	15 19	bitrd	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to ((A Y_{rm} M) ∥ (A Y_{rm} N) \leftrightarrow (A Y_{rm} M) ∥ (A Y_{rm} N) (A X_{rm} M))$
21	5 9	zmulcld	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to (A Y_{rm} N) (A X_{rm} M) \in ℤ$
22	6	fovcl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A X_{rm} N \in ℕ_{0}$
23	22	3adant2	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to A X_{rm} N \in ℕ_{0}$
24	23	nn0zd	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to A X_{rm} N \in ℤ$
25	24 3	zmulcld	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to (A X_{rm} N) (A Y_{rm} M) \in ℤ$
26		dvdsmul2	$⊢ (A X_{rm} N \in ℤ \land A Y_{rm} M \in ℤ) \to (A Y_{rm} M) ∥ (A X_{rm} N) (A Y_{rm} M)$
27	24 3 26	syl2anc	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to (A Y_{rm} M) ∥ (A X_{rm} N) (A Y_{rm} M)$
28		dvdsadd2b	$⊢ (A Y_{rm} M \in ℤ \land (A Y_{rm} N) (A X_{rm} M) \in ℤ \land ((A X_{rm} N) (A Y_{rm} M) \in ℤ \land (A Y_{rm} M) ∥ (A X_{rm} N) (A Y_{rm} M))) \to ((A Y_{rm} M) ∥ (A Y_{rm} N) (A X_{rm} M) \leftrightarrow (A Y_{rm} M) ∥ ((A X_{rm} N) (A Y_{rm} M) + (A Y_{rm} N) (A X_{rm} M)))$
29	3 21 25 27 28	syl112anc	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to ((A Y_{rm} M) ∥ (A Y_{rm} N) (A X_{rm} M) \leftrightarrow (A Y_{rm} M) ∥ ((A X_{rm} N) (A Y_{rm} M) + (A Y_{rm} N) (A X_{rm} M)))$
30		rmyadd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land M \in ℤ) \to A Y_{rm} (N + M) = (A Y_{rm} N) (A X_{rm} M) + (A X_{rm} N) (A Y_{rm} M)$
31	30	3com23	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to A Y_{rm} (N + M) = (A Y_{rm} N) (A X_{rm} M) + (A X_{rm} N) (A Y_{rm} M)$
32	17 16	mulcld	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to (A Y_{rm} N) (A X_{rm} M) \in ℂ$
33	23	nn0cnd	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to A X_{rm} N \in ℂ$
34	3	zcnd	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to A Y_{rm} M \in ℂ$
35	33 34	mulcld	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to (A X_{rm} N) (A Y_{rm} M) \in ℂ$
36	32 35	addcomd	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to (A Y_{rm} N) (A X_{rm} M) + (A X_{rm} N) (A Y_{rm} M) = (A X_{rm} N) (A Y_{rm} M) + (A Y_{rm} N) (A X_{rm} M)$
37	31 36	eqtr2d	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to (A X_{rm} N) (A Y_{rm} M) + (A Y_{rm} N) (A X_{rm} M) = A Y_{rm} (N + M)$
38	37	breq2d	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to ((A Y_{rm} M) ∥ ((A X_{rm} N) (A Y_{rm} M) + (A Y_{rm} N) (A X_{rm} M)) \leftrightarrow (A Y_{rm} M) ∥ (A Y_{rm} (N + M)))$
39	20 29 38	3bitrd	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to ((A Y_{rm} M) ∥ (A Y_{rm} N) \leftrightarrow (A Y_{rm} M) ∥ (A Y_{rm} (N + M)))$

Metamath Proof Explorer

Theorem jm2.19lem2

Proof