Metamath Proof Explorer


Theorem ltrmy

Description: The Y-sequence is strictly monotonic over ZZ . (Contributed by Stefan O'Rear, 25-Sep-2014)

Ref Expression
Assertion ltrmy A 2 M N M < N A Y rm M < A Y rm N

Proof

Step Hyp Ref Expression
1 ltrmynn0 A 2 a 0 b 0 a < b A Y rm a < A Y rm b
2 1 biimpd A 2 a 0 b 0 a < b A Y rm a < A Y rm b
3 frmy Y rm : 2 ×
4 3 fovcl A 2 a A Y rm a
5 4 zred A 2 a A Y rm a
6 rmyneg A 2 b A Y rm b = A Y rm b
7 oveq2 a = M A Y rm a = A Y rm M
8 oveq2 a = N A Y rm a = A Y rm N
9 oveq2 a = b A Y rm a = A Y rm b
10 oveq2 a = b A Y rm a = A Y rm b
11 2 5 6 7 8 9 10 monotoddzz A 2 M N M < N A Y rm M < A Y rm N