Metamath Proof Explorer


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 ‘ 𝐵 ) ) )