Metamath Proof Explorer

Theorem rmyabs

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

Ref Expression
Assertion rmyabs 
|- ( ( A e. ( ZZ>= ` 2 ) /\ B e. ZZ ) -> ( abs ` ( A rmY B ) ) = ( A rmY ( abs ` B ) ) )

Proof

Step Hyp Ref Expression
1 frmy 
 |-  rmY : ( ( ZZ>= ` 2 ) X. ZZ ) --> ZZ
2 1 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ a e. ZZ ) -> ( A rmY a ) e. ZZ )
3 2 zred 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ a e. ZZ ) -> ( A rmY a ) e. RR )
4 simp1 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ a e. ZZ /\ 0 <_ a ) -> A e. ( ZZ>= ` 2 ) )
5 elnn0z 
 |-  ( a e. NN0 <-> ( a e. ZZ /\ 0 <_ a ) )
6 5 biimpri 
 |-  ( ( a e. ZZ /\ 0 <_ a ) -> a e. NN0 )
7 6 3adant1 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ a e. ZZ /\ 0 <_ a ) -> a e. NN0 )
8 rmxypos 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ a e. NN0 ) -> ( 0 < ( A rmX a ) /\ 0 <_ ( A rmY a ) ) )
9 4 7 8 syl2anc 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ a e. ZZ /\ 0 <_ a ) -> ( 0 < ( A rmX a ) /\ 0 <_ ( A rmY a ) ) )
10 9 simprd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ a e. ZZ /\ 0 <_ a ) -> 0 <_ ( A rmY a ) )
11 rmyneg 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ b e. ZZ ) -> ( A rmY -u b ) = -u ( A rmY b ) )
12 oveq2 
 |-  ( a = b -> ( A rmY a ) = ( A rmY b ) )
13 oveq2 
 |-  ( a = -u b -> ( A rmY a ) = ( A rmY -u b ) )
14 oveq2 
 |-  ( a = B -> ( A rmY a ) = ( A rmY B ) )
15 oveq2 
 |-  ( a = ( abs ` B ) -> ( A rmY a ) = ( A rmY ( abs ` B ) ) )
16 3 10 11 12 13 14 15 oddcomabszz 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ B e. ZZ ) -> ( abs ` ( A rmY B ) ) = ( A rmY ( abs ` B ) ) )