Theorem rmyabs

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

	Ref	Expression
Assertion	rmyabs	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ℤ ) → ( abs ‘ ( 𝐴 Yrm 𝐵 ) ) = ( 𝐴 Yrm ( abs ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		frmy	⊢ Yrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℤ
2	1	fovcl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑎 ∈ ℤ ) → ( 𝐴 Yrm 𝑎 ) ∈ ℤ )
3	2	zred	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑎 ∈ ℤ ) → ( 𝐴 Yrm 𝑎 ) ∈ ℝ )
4		simp1	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑎 ∈ ℤ ∧ 0 ≤ 𝑎 ) → 𝐴 ∈ ( ℤ≥ ‘ 2 ) )
5		elnn0z	⊢ ( 𝑎 ∈ ℕ0 ↔ ( 𝑎 ∈ ℤ ∧ 0 ≤ 𝑎 ) )
6	5	biimpri	⊢ ( ( 𝑎 ∈ ℤ ∧ 0 ≤ 𝑎 ) → 𝑎 ∈ ℕ0 )
7	6	3adant1	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑎 ∈ ℤ ∧ 0 ≤ 𝑎 ) → 𝑎 ∈ ℕ0 )
8		rmxypos	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑎 ∈ ℕ0 ) → ( 0 < ( 𝐴 Xrm 𝑎 ) ∧ 0 ≤ ( 𝐴 Yrm 𝑎 ) ) )
9	4 7 8	syl2anc	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑎 ∈ ℤ ∧ 0 ≤ 𝑎 ) → ( 0 < ( 𝐴 Xrm 𝑎 ) ∧ 0 ≤ ( 𝐴 Yrm 𝑎 ) ) )
10	9	simprd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑎 ∈ ℤ ∧ 0 ≤ 𝑎 ) → 0 ≤ ( 𝐴 Yrm 𝑎 ) )
11		rmyneg	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℤ ) → ( 𝐴 Yrm - 𝑏 ) = - ( 𝐴 Yrm 𝑏 ) )
12		oveq2	⊢ ( 𝑎 = 𝑏 → ( 𝐴 Yrm 𝑎 ) = ( 𝐴 Yrm 𝑏 ) )
13		oveq2	⊢ ( 𝑎 = - 𝑏 → ( 𝐴 Yrm 𝑎 ) = ( 𝐴 Yrm - 𝑏 ) )
14		oveq2	⊢ ( 𝑎 = 𝐵 → ( 𝐴 Yrm 𝑎 ) = ( 𝐴 Yrm 𝐵 ) )
15		oveq2	⊢ ( 𝑎 = ( abs ‘ 𝐵 ) → ( 𝐴 Yrm 𝑎 ) = ( 𝐴 Yrm ( abs ‘ 𝐵 ) ) )
16	3 10 11 12 13 14 15	oddcomabszz	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ℤ ) → ( abs ‘ ( 𝐴 Yrm 𝐵 ) ) = ( 𝐴 Yrm ( abs ‘ 𝐵 ) ) )