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∈ℤ≥2∧N∈ℕ0→0<AXrmN∧0≤AYrmN

Proof

Step Hyp Ref Expression
1 oveq2 ⊢a=0→AXrma=AXrm0
2 1 breq2d ⊢a=0→0<AXrma↔0<AXrm0
3 oveq2 ⊢a=0→AYrma=AYrm0
4 3 breq2d ⊢a=0→0≤AYrma↔0≤AYrm0
5 2 4 anbi12d ⊢a=0→0<AXrma∧0≤AYrma↔0<AXrm0∧0≤AYrm0
6 5 imbi2d ⊢a=0→A∈ℤ≥2→0<AXrma∧0≤AYrma↔A∈ℤ≥2→0<AXrm0∧0≤AYrm0
7 oveq2 ⊢a=b→AXrma=AXrmb
8 7 breq2d ⊢a=b→0<AXrma↔0<AXrmb
9 oveq2 ⊢a=b→AYrma=AYrmb
10 9 breq2d ⊢a=b→0≤AYrma↔0≤AYrmb
11 8 10 anbi12d ⊢a=b→0<AXrma∧0≤AYrma↔0<AXrmb∧0≤AYrmb
12 11 imbi2d ⊢a=b→A∈ℤ≥2→0<AXrma∧0≤AYrma↔A∈ℤ≥2→0<AXrmb∧0≤AYrmb
13 oveq2 ⊢a=b+1→AXrma=AXrmb+1
14 13 breq2d ⊢a=b+1→0<AXrma↔0<AXrmb+1
15 oveq2 ⊢a=b+1→AYrma=AYrmb+1
16 15 breq2d ⊢a=b+1→0≤AYrma↔0≤AYrmb+1
17 14 16 anbi12d ⊢a=b+1→0<AXrma∧0≤AYrma↔0<AXrmb+1∧0≤AYrmb+1
18 17 imbi2d ⊢a=b+1→A∈ℤ≥2→0<AXrma∧0≤AYrma↔A∈ℤ≥2→0<AXrmb+1∧0≤AYrmb+1
19 oveq2 ⊢a=N→AXrma=AXrmN
20 19 breq2d ⊢a=N→0<AXrma↔0<AXrmN
21 oveq2 ⊢a=N→AYrma=AYrmN
22 21 breq2d ⊢a=N→0≤AYrma↔0≤AYrmN
23 20 22 anbi12d ⊢a=N→0<AXrma∧0≤AYrma↔0<AXrmN∧0≤AYrmN
24 23 imbi2d ⊢a=N→A∈ℤ≥2→0<AXrma∧0≤AYrma↔A∈ℤ≥2→0<AXrmN∧0≤AYrmN
25 0lt1 ⊢0<1
26 rmx0 ⊢A∈ℤ≥2→AXrm0=1
27 25 26 breqtrrid ⊢A∈ℤ≥2→0<AXrm0
28 0le0 ⊢0≤0
29 rmy0 ⊢A∈ℤ≥2→AYrm0=0
30 28 29 breqtrrid ⊢A∈ℤ≥2→0≤AYrm0
31 27 30 jca ⊢A∈ℤ≥2→0<AXrm0∧0≤AYrm0
32 simp2 ⊢b∈ℕ0∧A∈ℤ≥2∧0<AXrmb∧0≤AYrmb→A∈ℤ≥2
33 nn0z ⊢b∈ℕ0→b∈ℤ
34 33 3ad2ant1 ⊢b∈ℕ0∧A∈ℤ≥2∧0<AXrmb∧0≤AYrmb→b∈ℤ
35 frmx ⊢Xrm:ℤ≥2×ℤ⟶ℕ0
36 35 fovcl ⊢A∈ℤ≥2∧b∈ℤ→AXrmb∈ℕ0
37 32 34 36 syl2anc ⊢b∈ℕ0∧A∈ℤ≥2∧0<AXrmb∧0≤AYrmb→AXrmb∈ℕ0
38 37 nn0red ⊢b∈ℕ0∧A∈ℤ≥2∧0<AXrmb∧0≤AYrmb→AXrmb∈ℝ
39 eluzelre ⊢A∈ℤ≥2→A∈ℝ
40 39 3ad2ant2 ⊢b∈ℕ0∧A∈ℤ≥2∧0<AXrmb∧0≤AYrmb→A∈ℝ
41 38 40 remulcld ⊢b∈ℕ0∧A∈ℤ≥2∧0<AXrmb∧0≤AYrmb→AXrmb⁢A∈ℝ
42 rmspecpos ⊢A∈ℤ≥2→A2−1∈ℝ+
43 42 rpred ⊢A∈ℤ≥2→A2−1∈ℝ
44 43 3ad2ant2 ⊢b∈ℕ0∧A∈ℤ≥2∧0<AXrmb∧0≤AYrmb→A2−1∈ℝ
45 frmy ⊢Yrm:ℤ≥2×ℤ⟶ℤ
46 45 fovcl ⊢A∈ℤ≥2∧b∈ℤ→AYrmb∈ℤ
47 32 34 46 syl2anc ⊢b∈ℕ0∧A∈ℤ≥2∧0<AXrmb∧0≤AYrmb→AYrmb∈ℤ
48 47 zred ⊢b∈ℕ0∧A∈ℤ≥2∧0<AXrmb∧0≤AYrmb→AYrmb∈ℝ
49 44 48 remulcld ⊢b∈ℕ0∧A∈ℤ≥2∧0<AXrmb∧0≤AYrmb→A2−1⁢AYrmb∈ℝ
50 simp3l ⊢b∈ℕ0∧A∈ℤ≥2∧0<AXrmb∧0≤AYrmb→0<AXrmb
51 eluz2nn ⊢A∈ℤ≥2→A∈ℕ
52 51 nngt0d ⊢A∈ℤ≥2→0<A
53 52 3ad2ant2 ⊢b∈ℕ0∧A∈ℤ≥2∧0<AXrmb∧0≤AYrmb→0<A
54 38 40 50 53 mulgt0d ⊢b∈ℕ0∧A∈ℤ≥2∧0<AXrmb∧0≤AYrmb→0<AXrmb⁢A
55 42 rpge0d ⊢A∈ℤ≥2→0≤A2−1
56 55 3ad2ant2 ⊢b∈ℕ0∧A∈ℤ≥2∧0<AXrmb∧0≤AYrmb→0≤A2−1
57 simp3r ⊢b∈ℕ0∧A∈ℤ≥2∧0<AXrmb∧0≤AYrmb→0≤AYrmb
58 44 48 56 57 mulge0d ⊢b∈ℕ0∧A∈ℤ≥2∧0<AXrmb∧0≤AYrmb→0≤A2−1⁢AYrmb
59 41 49 54 58 addgtge0d ⊢b∈ℕ0∧A∈ℤ≥2∧0<AXrmb∧0≤AYrmb→0<AXrmb⁢A+A2−1⁢AYrmb
60 rmxp1 ⊢A∈ℤ≥2∧b∈ℤ→AXrmb+1=AXrmb⁢A+A2−1⁢AYrmb
61 32 34 60 syl2anc ⊢b∈ℕ0∧A∈ℤ≥2∧0<AXrmb∧0≤AYrmb→AXrmb+1=AXrmb⁢A+A2−1⁢AYrmb
62 59 61 breqtrrd ⊢b∈ℕ0∧A∈ℤ≥2∧0<AXrmb∧0≤AYrmb→0<AXrmb+1
63 48 40 remulcld ⊢b∈ℕ0∧A∈ℤ≥2∧0<AXrmb∧0≤AYrmb→AYrmb⁢A∈ℝ
64 eluzge2nn0 ⊢A∈ℤ≥2→A∈ℕ0
65 64 nn0ge0d ⊢A∈ℤ≥2→0≤A
66 65 3ad2ant2 ⊢b∈ℕ0∧A∈ℤ≥2∧0<AXrmb∧0≤AYrmb→0≤A
67 48 40 57 66 mulge0d ⊢b∈ℕ0∧A∈ℤ≥2∧0<AXrmb∧0≤AYrmb→0≤AYrmb⁢A
68 37 nn0ge0d ⊢b∈ℕ0∧A∈ℤ≥2∧0<AXrmb∧0≤AYrmb→0≤AXrmb
69 63 38 67 68 addge0d ⊢b∈ℕ0∧A∈ℤ≥2∧0<AXrmb∧0≤AYrmb→0≤AYrmb⁢A+AXrmb
70 rmyp1 ⊢A∈ℤ≥2∧b∈ℤ→AYrmb+1=AYrmb⁢A+AXrmb
71 32 34 70 syl2anc ⊢b∈ℕ0∧A∈ℤ≥2∧0<AXrmb∧0≤AYrmb→AYrmb+1=AYrmb⁢A+AXrmb
72 69 71 breqtrrd ⊢b∈ℕ0∧A∈ℤ≥2∧0<AXrmb∧0≤AYrmb→0≤AYrmb+1
73 62 72 jca ⊢b∈ℕ0∧A∈ℤ≥2∧0<AXrmb∧0≤AYrmb→0<AXrmb+1∧0≤AYrmb+1
74 73 3exp ⊢b∈ℕ0→A∈ℤ≥2→0<AXrmb∧0≤AYrmb→0<AXrmb+1∧0≤AYrmb+1
75 74 a2d ⊢b∈ℕ0→A∈ℤ≥2→0<AXrmb∧0≤AYrmb→A∈ℤ≥2→0<AXrmb+1∧0≤AYrmb+1
76 6 12 18 24 31 75 nn0ind ⊢N∈ℕ0→A∈ℤ≥2→0<AXrmN∧0≤AYrmN
77 76 impcom ⊢A∈ℤ≥2∧N∈ℕ0→0<AXrmN∧0≤AYrmN