Theorem lermxnn0

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

	Ref	Expression
Assertion	lermxnn0	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑀 ≤ 𝑁 ↔ ( 𝐴 Xrm 𝑀 ) ≤ ( 𝐴 Xrm 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		oveq2	⊢ ( 𝑎 = 𝑏 → ( 𝐴 Xrm 𝑎 ) = ( 𝐴 Xrm 𝑏 ) )
2		oveq2	⊢ ( 𝑎 = 𝑀 → ( 𝐴 Xrm 𝑎 ) = ( 𝐴 Xrm 𝑀 ) )
3		oveq2	⊢ ( 𝑎 = 𝑁 → ( 𝐴 Xrm 𝑎 ) = ( 𝐴 Xrm 𝑁 ) )
4		nn0ssre	⊢ ℕ0 ⊆ ℝ
5		nn0z	⊢ ( 𝑎 ∈ ℕ0 → 𝑎 ∈ ℤ )
6		frmx	⊢ Xrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℕ0
7	6	fovcl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑎 ∈ ℤ ) → ( 𝐴 Xrm 𝑎 ) ∈ ℕ0 )
8	5 7	sylan2	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑎 ∈ ℕ0 ) → ( 𝐴 Xrm 𝑎 ) ∈ ℕ0 )
9	8	nn0red	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑎 ∈ ℕ0 ) → ( 𝐴 Xrm 𝑎 ) ∈ ℝ )
10		ltrmxnn0	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) → ( 𝑎 < 𝑏 ↔ ( 𝐴 Xrm 𝑎 ) < ( 𝐴 Xrm 𝑏 ) ) )
11	10	biimpd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) → ( 𝑎 < 𝑏 → ( 𝐴 Xrm 𝑎 ) < ( 𝐴 Xrm 𝑏 ) ) )
12	11	3expb	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) ) → ( 𝑎 < 𝑏 → ( 𝐴 Xrm 𝑎 ) < ( 𝐴 Xrm 𝑏 ) ) )
13	1 2 3 4 9 12	leord1	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) → ( 𝑀 ≤ 𝑁 ↔ ( 𝐴 Xrm 𝑀 ) ≤ ( 𝐴 Xrm 𝑁 ) ) )
14	13	3impb	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑀 ≤ 𝑁 ↔ ( 𝐴 Xrm 𝑀 ) ≤ ( 𝐴 Xrm 𝑁 ) ) )