Metamath Proof Explorer


Theorem ltrmxnn0

Description: The X-sequence is strictly monotonic on NN0 . (Contributed by Stefan O'Rear, 4-Oct-2014)

Ref Expression
Assertion ltrmxnn0 A 2 M 0 N 0 M < N A X rm M < A X rm N

Proof

Step Hyp Ref Expression
1 nn0z b 0 b
2 frmx X rm : 2 × 0
3 2 fovcl A 2 b A X rm b 0
4 1 3 sylan2 A 2 b 0 A X rm b 0
5 4 nn0red A 2 b 0 A X rm b
6 eluzelre A 2 A
7 6 adantr A 2 b 0 A
8 5 7 remulcld A 2 b 0 A X rm b A
9 1 peano2zd b 0 b + 1
10 2 fovcl A 2 b + 1 A X rm b + 1 0
11 9 10 sylan2 A 2 b 0 A X rm b + 1 0
12 11 nn0red A 2 b 0 A X rm b + 1
13 eluz2b2 A 2 A 1 < A
14 13 simprbi A 2 1 < A
15 14 adantr A 2 b 0 1 < A
16 rmxypos A 2 b 0 0 < A X rm b 0 A Y rm b
17 16 simpld A 2 b 0 0 < A X rm b
18 ltmulgt11 A X rm b A 0 < A X rm b 1 < A A X rm b < A X rm b A
19 5 7 17 18 syl3anc A 2 b 0 1 < A A X rm b < A X rm b A
20 15 19 mpbid A 2 b 0 A X rm b < A X rm b A
21 rmspecnonsq A 2 A 2 1
22 21 eldifad A 2 A 2 1
23 22 adantr A 2 b 0 A 2 1
24 23 nnred A 2 b 0 A 2 1
25 frmy Y rm : 2 ×
26 25 fovcl A 2 b A Y rm b
27 1 26 sylan2 A 2 b 0 A Y rm b
28 27 zred A 2 b 0 A Y rm b
29 23 nnnn0d A 2 b 0 A 2 1 0
30 29 nn0ge0d A 2 b 0 0 A 2 1
31 16 simprd A 2 b 0 0 A Y rm b
32 24 28 30 31 mulge0d A 2 b 0 0 A 2 1 A Y rm b
33 24 28 remulcld A 2 b 0 A 2 1 A Y rm b
34 8 33 addge01d A 2 b 0 0 A 2 1 A Y rm b A X rm b A A X rm b A + A 2 1 A Y rm b
35 32 34 mpbid A 2 b 0 A X rm b A A X rm b A + A 2 1 A Y rm b
36 rmxp1 A 2 b A X rm b + 1 = A X rm b A + A 2 1 A Y rm b
37 1 36 sylan2 A 2 b 0 A X rm b + 1 = A X rm b A + A 2 1 A Y rm b
38 35 37 breqtrrd A 2 b 0 A X rm b A A X rm b + 1
39 5 8 12 20 38 ltletrd A 2 b 0 A X rm b < A X rm b + 1
40 nn0z a 0 a
41 2 fovcl A 2 a A X rm a 0
42 40 41 sylan2 A 2 a 0 A X rm a 0
43 42 nn0red A 2 a 0 A X rm a
44 nn0uz 0 = 0
45 oveq2 a = b + 1 A X rm a = A X rm b + 1
46 oveq2 a = b A X rm a = A X rm b
47 oveq2 a = M A X rm a = A X rm M
48 oveq2 a = N A X rm a = A X rm N
49 39 43 44 45 46 47 48 monotuz A 2 M 0 N 0 M < N A X rm M < A X rm N
50 49 3impb A 2 M 0 N 0 M < N A X rm M < A X rm N