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↔AXrmM<AXrmN

Proof

Step Hyp Ref Expression
1 nn0z ⊢b∈ℕ0→b∈ℤ
2 frmx ⊢Xrm:ℤ≥2×ℤ⟶ℕ0
3 2 fovcl ⊢A∈ℤ≥2∧b∈ℤ→AXrmb∈ℕ0
4 1 3 sylan2 ⊢A∈ℤ≥2∧b∈ℕ0→AXrmb∈ℕ0
5 4 nn0red ⊢A∈ℤ≥2∧b∈ℕ0→AXrmb∈ℝ
6 eluzelre ⊢A∈ℤ≥2→A∈ℝ
7 6 adantr ⊢A∈ℤ≥2∧b∈ℕ0→A∈ℝ
8 5 7 remulcld ⊢A∈ℤ≥2∧b∈ℕ0→AXrmb⁢A∈ℝ
9 1 peano2zd ⊢b∈ℕ0→b+1∈ℤ
10 2 fovcl ⊢A∈ℤ≥2∧b+1∈ℤ→AXrmb+1∈ℕ0
11 9 10 sylan2 ⊢A∈ℤ≥2∧b∈ℕ0→AXrmb+1∈ℕ0
12 11 nn0red ⊢A∈ℤ≥2∧b∈ℕ0→AXrmb+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<AXrmb∧0≤AYrmb
17 16 simpld ⊢A∈ℤ≥2∧b∈ℕ0→0<AXrmb
18 ltmulgt11 ⊢AXrmb∈ℝ∧A∈ℝ∧0<AXrmb→1<A↔AXrmb<AXrmb⁢A
19 5 7 17 18 syl3anc ⊢A∈ℤ≥2∧b∈ℕ0→1<A↔AXrmb<AXrmb⁢A
20 15 19 mpbid ⊢A∈ℤ≥2∧b∈ℕ0→AXrmb<AXrmb⁢A
21 rmspecnonsq ⊢A∈ℤ≥2→A2−1∈ℕ∖◻ℕ
22 21 eldifad ⊢A∈ℤ≥2→A2−1∈ℕ
23 22 adantr ⊢A∈ℤ≥2∧b∈ℕ0→A2−1∈ℕ
24 23 nnred ⊢A∈ℤ≥2∧b∈ℕ0→A2−1∈ℝ
25 frmy ⊢Yrm:ℤ≥2×ℤ⟶ℤ
26 25 fovcl ⊢A∈ℤ≥2∧b∈ℤ→AYrmb∈ℤ
27 1 26 sylan2 ⊢A∈ℤ≥2∧b∈ℕ0→AYrmb∈ℤ
28 27 zred ⊢A∈ℤ≥2∧b∈ℕ0→AYrmb∈ℝ
29 23 nnnn0d ⊢A∈ℤ≥2∧b∈ℕ0→A2−1∈ℕ0
30 29 nn0ge0d ⊢A∈ℤ≥2∧b∈ℕ0→0≤A2−1
31 16 simprd ⊢A∈ℤ≥2∧b∈ℕ0→0≤AYrmb
32 24 28 30 31 mulge0d ⊢A∈ℤ≥2∧b∈ℕ0→0≤A2−1⁢AYrmb
33 24 28 remulcld ⊢A∈ℤ≥2∧b∈ℕ0→A2−1⁢AYrmb∈ℝ
34 8 33 addge01d ⊢A∈ℤ≥2∧b∈ℕ0→0≤A2−1⁢AYrmb↔AXrmb⁢A≤AXrmb⁢A+A2−1⁢AYrmb
35 32 34 mpbid ⊢A∈ℤ≥2∧b∈ℕ0→AXrmb⁢A≤AXrmb⁢A+A2−1⁢AYrmb
36 rmxp1 ⊢A∈ℤ≥2∧b∈ℤ→AXrmb+1=AXrmb⁢A+A2−1⁢AYrmb
37 1 36 sylan2 ⊢A∈ℤ≥2∧b∈ℕ0→AXrmb+1=AXrmb⁢A+A2−1⁢AYrmb
38 35 37 breqtrrd ⊢A∈ℤ≥2∧b∈ℕ0→AXrmb⁢A≤AXrmb+1
39 5 8 12 20 38 ltletrd ⊢A∈ℤ≥2∧b∈ℕ0→AXrmb<AXrmb+1
40 nn0z ⊢a∈ℕ0→a∈ℤ
41 2 fovcl ⊢A∈ℤ≥2∧a∈ℤ→AXrma∈ℕ0
42 40 41 sylan2 ⊢A∈ℤ≥2∧a∈ℕ0→AXrma∈ℕ0
43 42 nn0red ⊢A∈ℤ≥2∧a∈ℕ0→AXrma∈ℝ
44 nn0uz ⊢ℕ0=ℤ≥0
45 oveq2 ⊢a=b+1→AXrma=AXrmb+1
46 oveq2 ⊢a=b→AXrma=AXrmb
47 oveq2 ⊢a=M→AXrma=AXrmM
48 oveq2 ⊢a=N→AXrma=AXrmN
49 39 43 44 45 46 47 48 monotuz ⊢A∈ℤ≥2∧M∈ℕ0∧N∈ℕ0→M<N↔AXrmM<AXrmN
50 49 3impb ⊢A∈ℤ≥2∧M∈ℕ0∧N∈ℕ0→M<N↔AXrmM<AXrmN