Metamath Proof Explorer

Theorem rmxnn

Description: The X-sequence is defined to range over NN0 but never actually takes the value 0. (Contributed by Stefan O'Rear, 4-Oct-2014)

Ref Expression
Assertion rmxnn 
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmX N ) e. NN )

Proof

Step Hyp Ref Expression
1 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
2 frmx 
 |-  rmX : ( ( ZZ>= ` 2 ) X. ZZ ) --> NN0
3 2 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmX N ) e. NN0 )
4 1 3 sylan2 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> ( A rmX N ) e. NN0 )
5 rmxypos 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> ( 0 < ( A rmX N ) /\ 0 <_ ( A rmY N ) ) )
6 5 simpld 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> 0 < ( A rmX N ) )
7 elnnnn0b 
 |-  ( ( A rmX N ) e. NN <-> ( ( A rmX N ) e. NN0 /\ 0 < ( A rmX N ) ) )
8 4 6 7 sylanbrc 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> ( A rmX N ) e. NN )
9 8 adantlr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ N e. NN0 ) -> ( A rmX N ) e. NN )
10 rmxneg 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmX -u N ) = ( A rmX N ) )
11 10 adantr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ -u N e. NN0 ) -> ( A rmX -u N ) = ( A rmX N ) )
12 nn0z 
 |-  ( -u N e. NN0 -> -u N e. ZZ )
13 2 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ -u N e. ZZ ) -> ( A rmX -u N ) e. NN0 )
14 12 13 sylan2 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ -u N e. NN0 ) -> ( A rmX -u N ) e. NN0 )
15 rmxypos 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ -u N e. NN0 ) -> ( 0 < ( A rmX -u N ) /\ 0 <_ ( A rmY -u N ) ) )
16 15 simpld 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ -u N e. NN0 ) -> 0 < ( A rmX -u N ) )
17 elnnnn0b 
 |-  ( ( A rmX -u N ) e. NN <-> ( ( A rmX -u N ) e. NN0 /\ 0 < ( A rmX -u N ) ) )
18 14 16 17 sylanbrc 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ -u N e. NN0 ) -> ( A rmX -u N ) e. NN )
19 18 adantlr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ -u N e. NN0 ) -> ( A rmX -u N ) e. NN )
20 11 19 eqeltrrd 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ -u N e. NN0 ) -> ( A rmX N ) e. NN )
21 elznn0 
 |-  ( N e. ZZ <-> ( N e. RR /\ ( N e. NN0 \/ -u N e. NN0 ) ) )
22 21 simprbi 
 |-  ( N e. ZZ -> ( N e. NN0 \/ -u N e. NN0 ) )
23 22 adantl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( N e. NN0 \/ -u N e. NN0 ) )
24 9 20 23 mpjaodan 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmX N ) e. NN )