Metamath Proof Explorer

Theorem rmxypos

Description: For all nonnegative indices, X is positive and Y is nonnegative. (Contributed by Stefan O'Rear, 24-Sep-2014)

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

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( a = 0 -> ( A rmX a ) = ( A rmX 0 ) )
2 1 breq2d 
 |-  ( a = 0 -> ( 0 < ( A rmX a ) <-> 0 < ( A rmX 0 ) ) )
3 oveq2 
 |-  ( a = 0 -> ( A rmY a ) = ( A rmY 0 ) )
4 3 breq2d 
 |-  ( a = 0 -> ( 0 <_ ( A rmY a ) <-> 0 <_ ( A rmY 0 ) ) )
5 2 4 anbi12d 
 |-  ( a = 0 -> ( ( 0 < ( A rmX a ) /\ 0 <_ ( A rmY a ) ) <-> ( 0 < ( A rmX 0 ) /\ 0 <_ ( A rmY 0 ) ) ) )
6 5 imbi2d 
 |-  ( a = 0 -> ( ( A e. ( ZZ>= ` 2 ) -> ( 0 < ( A rmX a ) /\ 0 <_ ( A rmY a ) ) ) <-> ( A e. ( ZZ>= ` 2 ) -> ( 0 < ( A rmX 0 ) /\ 0 <_ ( A rmY 0 ) ) ) ) )
7 oveq2 
 |-  ( a = b -> ( A rmX a ) = ( A rmX b ) )
8 7 breq2d 
 |-  ( a = b -> ( 0 < ( A rmX a ) <-> 0 < ( A rmX b ) ) )
9 oveq2 
 |-  ( a = b -> ( A rmY a ) = ( A rmY b ) )
10 9 breq2d 
 |-  ( a = b -> ( 0 <_ ( A rmY a ) <-> 0 <_ ( A rmY b ) ) )
11 8 10 anbi12d 
 |-  ( a = b -> ( ( 0 < ( A rmX a ) /\ 0 <_ ( A rmY a ) ) <-> ( 0 < ( A rmX b ) /\ 0 <_ ( A rmY b ) ) ) )
12 11 imbi2d 
 |-  ( a = b -> ( ( A e. ( ZZ>= ` 2 ) -> ( 0 < ( A rmX a ) /\ 0 <_ ( A rmY a ) ) ) <-> ( A e. ( ZZ>= ` 2 ) -> ( 0 < ( A rmX b ) /\ 0 <_ ( A rmY b ) ) ) ) )
13 oveq2 
 |-  ( a = ( b + 1 ) -> ( A rmX a ) = ( A rmX ( b + 1 ) ) )
14 13 breq2d 
 |-  ( a = ( b + 1 ) -> ( 0 < ( A rmX a ) <-> 0 < ( A rmX ( b + 1 ) ) ) )
15 oveq2 
 |-  ( a = ( b + 1 ) -> ( A rmY a ) = ( A rmY ( b + 1 ) ) )
16 15 breq2d 
 |-  ( a = ( b + 1 ) -> ( 0 <_ ( A rmY a ) <-> 0 <_ ( A rmY ( b + 1 ) ) ) )
17 14 16 anbi12d 
 |-  ( a = ( b + 1 ) -> ( ( 0 < ( A rmX a ) /\ 0 <_ ( A rmY a ) ) <-> ( 0 < ( A rmX ( b + 1 ) ) /\ 0 <_ ( A rmY ( b + 1 ) ) ) ) )
18 17 imbi2d 
 |-  ( a = ( b + 1 ) -> ( ( A e. ( ZZ>= ` 2 ) -> ( 0 < ( A rmX a ) /\ 0 <_ ( A rmY a ) ) ) <-> ( A e. ( ZZ>= ` 2 ) -> ( 0 < ( A rmX ( b + 1 ) ) /\ 0 <_ ( A rmY ( b + 1 ) ) ) ) ) )
19 oveq2 
 |-  ( a = N -> ( A rmX a ) = ( A rmX N ) )
20 19 breq2d 
 |-  ( a = N -> ( 0 < ( A rmX a ) <-> 0 < ( A rmX N ) ) )
21 oveq2 
 |-  ( a = N -> ( A rmY a ) = ( A rmY N ) )
22 21 breq2d 
 |-  ( a = N -> ( 0 <_ ( A rmY a ) <-> 0 <_ ( A rmY N ) ) )
23 20 22 anbi12d 
 |-  ( a = N -> ( ( 0 < ( A rmX a ) /\ 0 <_ ( A rmY a ) ) <-> ( 0 < ( A rmX N ) /\ 0 <_ ( A rmY N ) ) ) )
24 23 imbi2d 
 |-  ( a = N -> ( ( A e. ( ZZ>= ` 2 ) -> ( 0 < ( A rmX a ) /\ 0 <_ ( A rmY a ) ) ) <-> ( A e. ( ZZ>= ` 2 ) -> ( 0 < ( A rmX N ) /\ 0 <_ ( A rmY N ) ) ) ) )
25 0lt1 
 |-  0 < 1
26 rmx0 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A rmX 0 ) = 1 )
27 25 26 breqtrrid 
 |-  ( A e. ( ZZ>= ` 2 ) -> 0 < ( A rmX 0 ) )
28 0le0 
 |-  0 <_ 0
29 rmy0 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A rmY 0 ) = 0 )
30 28 29 breqtrrid 
 |-  ( A e. ( ZZ>= ` 2 ) -> 0 <_ ( A rmY 0 ) )
31 27 30 jca 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( 0 < ( A rmX 0 ) /\ 0 <_ ( A rmY 0 ) ) )
32 simp2 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ ( 0 < ( A rmX b ) /\ 0 <_ ( A rmY b ) ) ) -> A e. ( ZZ>= ` 2 ) )
33 nn0z 
 |-  ( b e. NN0 -> b e. ZZ )
34 33 3ad2ant1 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ ( 0 < ( A rmX b ) /\ 0 <_ ( A rmY b ) ) ) -> b e. ZZ )
35 frmx 
 |-  rmX : ( ( ZZ>= ` 2 ) X. ZZ ) --> NN0
36 35 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ b e. ZZ ) -> ( A rmX b ) e. NN0 )
37 32 34 36 syl2anc 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ ( 0 < ( A rmX b ) /\ 0 <_ ( A rmY b ) ) ) -> ( A rmX b ) e. NN0 )
38 37 nn0red 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ ( 0 < ( A rmX b ) /\ 0 <_ ( A rmY b ) ) ) -> ( A rmX b ) e. RR )
39 eluzelre 
 |-  ( A e. ( ZZ>= ` 2 ) -> A e. RR )
40 39 3ad2ant2 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ ( 0 < ( A rmX b ) /\ 0 <_ ( A rmY b ) ) ) -> A e. RR )
41 38 40 remulcld 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ ( 0 < ( A rmX b ) /\ 0 <_ ( A rmY b ) ) ) -> ( ( A rmX b ) x. A ) e. RR )
42 rmspecpos 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( A ^ 2 ) - 1 ) e. RR+ )
43 42 rpred 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( A ^ 2 ) - 1 ) e. RR )
44 43 3ad2ant2 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ ( 0 < ( A rmX b ) /\ 0 <_ ( A rmY b ) ) ) -> ( ( A ^ 2 ) - 1 ) e. RR )
45 frmy 
 |-  rmY : ( ( ZZ>= ` 2 ) X. ZZ ) --> ZZ
46 45 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ b e. ZZ ) -> ( A rmY b ) e. ZZ )
47 32 34 46 syl2anc 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ ( 0 < ( A rmX b ) /\ 0 <_ ( A rmY b ) ) ) -> ( A rmY b ) e. ZZ )
48 47 zred 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ ( 0 < ( A rmX b ) /\ 0 <_ ( A rmY b ) ) ) -> ( A rmY b ) e. RR )
49 44 48 remulcld 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ ( 0 < ( A rmX b ) /\ 0 <_ ( A rmY b ) ) ) -> ( ( ( A ^ 2 ) - 1 ) x. ( A rmY b ) ) e. RR )
50 simp3l 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ ( 0 < ( A rmX b ) /\ 0 <_ ( A rmY b ) ) ) -> 0 < ( A rmX b ) )
51 eluz2nn 
 |-  ( A e. ( ZZ>= ` 2 ) -> A e. NN )
52 51 nngt0d 
 |-  ( A e. ( ZZ>= ` 2 ) -> 0 < A )
53 52 3ad2ant2 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ ( 0 < ( A rmX b ) /\ 0 <_ ( A rmY b ) ) ) -> 0 < A )
54 38 40 50 53 mulgt0d 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ ( 0 < ( A rmX b ) /\ 0 <_ ( A rmY b ) ) ) -> 0 < ( ( A rmX b ) x. A ) )
55 42 rpge0d 
 |-  ( A e. ( ZZ>= ` 2 ) -> 0 <_ ( ( A ^ 2 ) - 1 ) )
56 55 3ad2ant2 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ ( 0 < ( A rmX b ) /\ 0 <_ ( A rmY b ) ) ) -> 0 <_ ( ( A ^ 2 ) - 1 ) )
57 simp3r 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ ( 0 < ( A rmX b ) /\ 0 <_ ( A rmY b ) ) ) -> 0 <_ ( A rmY b ) )
58 44 48 56 57 mulge0d 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ ( 0 < ( A rmX b ) /\ 0 <_ ( A rmY b ) ) ) -> 0 <_ ( ( ( A ^ 2 ) - 1 ) x. ( A rmY b ) ) )
59 41 49 54 58 addgtge0d 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ ( 0 < ( A rmX b ) /\ 0 <_ ( A rmY b ) ) ) -> 0 < ( ( ( A rmX b ) x. A ) + ( ( ( A ^ 2 ) - 1 ) x. ( A rmY b ) ) ) )
60 rmxp1 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ b e. ZZ ) -> ( A rmX ( b + 1 ) ) = ( ( ( A rmX b ) x. A ) + ( ( ( A ^ 2 ) - 1 ) x. ( A rmY b ) ) ) )
61 32 34 60 syl2anc 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ ( 0 < ( A rmX b ) /\ 0 <_ ( A rmY b ) ) ) -> ( A rmX ( b + 1 ) ) = ( ( ( A rmX b ) x. A ) + ( ( ( A ^ 2 ) - 1 ) x. ( A rmY b ) ) ) )
62 59 61 breqtrrd 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ ( 0 < ( A rmX b ) /\ 0 <_ ( A rmY b ) ) ) -> 0 < ( A rmX ( b + 1 ) ) )
63 48 40 remulcld 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ ( 0 < ( A rmX b ) /\ 0 <_ ( A rmY b ) ) ) -> ( ( A rmY b ) x. A ) e. RR )
64 eluzge2nn0 
 |-  ( A e. ( ZZ>= ` 2 ) -> A e. NN0 )
65 64 nn0ge0d 
 |-  ( A e. ( ZZ>= ` 2 ) -> 0 <_ A )
66 65 3ad2ant2 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ ( 0 < ( A rmX b ) /\ 0 <_ ( A rmY b ) ) ) -> 0 <_ A )
67 48 40 57 66 mulge0d 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ ( 0 < ( A rmX b ) /\ 0 <_ ( A rmY b ) ) ) -> 0 <_ ( ( A rmY b ) x. A ) )
68 37 nn0ge0d 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ ( 0 < ( A rmX b ) /\ 0 <_ ( A rmY b ) ) ) -> 0 <_ ( A rmX b ) )
69 63 38 67 68 addge0d 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ ( 0 < ( A rmX b ) /\ 0 <_ ( A rmY b ) ) ) -> 0 <_ ( ( ( A rmY b ) x. A ) + ( A rmX b ) ) )
70 rmyp1 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ b e. ZZ ) -> ( A rmY ( b + 1 ) ) = ( ( ( A rmY b ) x. A ) + ( A rmX b ) ) )
71 32 34 70 syl2anc 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ ( 0 < ( A rmX b ) /\ 0 <_ ( A rmY b ) ) ) -> ( A rmY ( b + 1 ) ) = ( ( ( A rmY b ) x. A ) + ( A rmX b ) ) )
72 69 71 breqtrrd 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ ( 0 < ( A rmX b ) /\ 0 <_ ( A rmY b ) ) ) -> 0 <_ ( A rmY ( b + 1 ) ) )
73 62 72 jca 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ ( 0 < ( A rmX b ) /\ 0 <_ ( A rmY b ) ) ) -> ( 0 < ( A rmX ( b + 1 ) ) /\ 0 <_ ( A rmY ( b + 1 ) ) ) )
74 73 3exp 
 |-  ( b e. NN0 -> ( A e. ( ZZ>= ` 2 ) -> ( ( 0 < ( A rmX b ) /\ 0 <_ ( A rmY b ) ) -> ( 0 < ( A rmX ( b + 1 ) ) /\ 0 <_ ( A rmY ( b + 1 ) ) ) ) ) )
75 74 a2d 
 |-  ( b e. NN0 -> ( ( A e. ( ZZ>= ` 2 ) -> ( 0 < ( A rmX b ) /\ 0 <_ ( A rmY b ) ) ) -> ( A e. ( ZZ>= ` 2 ) -> ( 0 < ( A rmX ( b + 1 ) ) /\ 0 <_ ( A rmY ( b + 1 ) ) ) ) ) )
76 6 12 18 24 31 75 nn0ind 
 |-  ( N e. NN0 -> ( A e. ( ZZ>= ` 2 ) -> ( 0 < ( A rmX N ) /\ 0 <_ ( A rmY N ) ) ) )
77 76 impcom 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> ( 0 < ( A rmX N ) /\ 0 <_ ( A rmY N ) ) )