Metamath Proof Explorer

Theorem rmyeq0

Description: Y is zero only at zero. (Contributed by Stefan O'Rear, 26-Sep-2014)

Ref Expression
Assertion rmyeq0 
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( N = 0 <-> ( A rmY N ) = 0 ) )

Proof

Step Hyp Ref Expression
1 0z 
 |-  0 e. ZZ
2 oveq2 
 |-  ( a = b -> ( A rmY a ) = ( A rmY b ) )
3 oveq2 
 |-  ( a = N -> ( A rmY a ) = ( A rmY N ) )
4 oveq2 
 |-  ( a = 0 -> ( A rmY a ) = ( A rmY 0 ) )
5 zssre 
 |-  ZZ C_ RR
6 frmy 
 |-  rmY : ( ( ZZ>= ` 2 ) X. ZZ ) --> ZZ
7 6 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ a e. ZZ ) -> ( A rmY a ) e. ZZ )
8 7 zred 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ a e. ZZ ) -> ( A rmY a ) e. RR )
9 ltrmy 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ a e. ZZ /\ b e. ZZ ) -> ( a < b <-> ( A rmY a ) < ( A rmY b ) ) )
10 9 biimpd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ a e. ZZ /\ b e. ZZ ) -> ( a < b -> ( A rmY a ) < ( A rmY b ) ) )
11 10 3expb 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( a < b -> ( A rmY a ) < ( A rmY b ) ) )
12 2 3 4 5 8 11 eqord1 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ 0 e. ZZ ) ) -> ( N = 0 <-> ( A rmY N ) = ( A rmY 0 ) ) )
13 1 12 mpanr2 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( N = 0 <-> ( A rmY N ) = ( A rmY 0 ) ) )
14 rmy0 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A rmY 0 ) = 0 )
15 14 adantr 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmY 0 ) = 0 )
16 15 eqeq2d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A rmY N ) = ( A rmY 0 ) <-> ( A rmY N ) = 0 ) )
17 13 16 bitrd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( N = 0 <-> ( A rmY N ) = 0 ) )