rmyabs

Description: rmY commutes with abs . (Contributed by Stefan O'Rear, 26-Sep-2014)

		Ref	Expression
	Assertion	rmyabs	$⊢ (A \in ℤ_{\geq 2} \land B \in ℤ) \to \|A Y_{rm} B\| = A Y_{rm} \|B\|$

Step	Hyp	Ref	Expression
1		frmy	$⊢ Y_{rm} : ℤ_{\geq 2} \times ℤ ⟶ ℤ$
2	1	fovcl	$⊢ (A \in ℤ_{\geq 2} \land a \in ℤ) \to A Y_{rm} a \in ℤ$
3	2	zred	$⊢ (A \in ℤ_{\geq 2} \land a \in ℤ) \to A Y_{rm} a \in ℝ$
4		simp1	$⊢ (A \in ℤ_{\geq 2} \land a \in ℤ \land 0 \leq a) \to A \in ℤ_{\geq 2}$
5		elnn0z	$⊢ a \in ℕ_{0} \leftrightarrow (a \in ℤ \land 0 \leq a)$
6	5	biimpri	$⊢ (a \in ℤ \land 0 \leq a) \to a \in ℕ_{0}$
7	6	3adant1	$⊢ (A \in ℤ_{\geq 2} \land a \in ℤ \land 0 \leq a) \to a \in ℕ_{0}$
8		rmxypos	$⊢ (A \in ℤ_{\geq 2} \land a \in ℕ_{0}) \to (0 < A X_{rm} a \land 0 \leq A Y_{rm} a)$
9	4 7 8	syl2anc	$⊢ (A \in ℤ_{\geq 2} \land a \in ℤ \land 0 \leq a) \to (0 < A X_{rm} a \land 0 \leq A Y_{rm} a)$
10	9	simprd	$⊢ (A \in ℤ_{\geq 2} \land a \in ℤ \land 0 \leq a) \to 0 \leq A Y_{rm} a$
11		rmyneg	$⊢ (A \in ℤ_{\geq 2} \land b \in ℤ) \to A Y_{rm} (- b) = - (A Y_{rm} b)$
12		oveq2	$⊢ a = b \to A Y_{rm} a = A Y_{rm} b$
13		oveq2	$⊢ a = - b \to A Y_{rm} a = A Y_{rm} (- b)$
14		oveq2	$⊢ a = B \to A Y_{rm} a = A Y_{rm} B$
15		oveq2	$⊢ a = \|B\| \to A Y_{rm} a = A Y_{rm} \|B\|$
16	3 10 11 12 13 14 15	oddcomabszz	$⊢ (A \in ℤ_{\geq 2} \land B \in ℤ) \to \|A Y_{rm} B\| = A Y_{rm} \|B\|$

Metamath Proof Explorer