Metamath Proof Explorer

Theorem lermy

Description: Y is monotonic (non-strict). (Contributed by Stefan O'Rear, 3-Oct-2014)

Ref Expression
Assertion lermy ⊢ A ∈ ℤ ≥ 2 ∧ M ∈ ℤ ∧ N ∈ ℤ → M ≤ N ↔ A Y rm M ≤ A Y rm N

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ a = b → A Y rm a = A Y rm b
2 oveq2 ⊢ a = M → A Y rm a = A Y rm M
3 oveq2 ⊢ a = N → A Y rm a = A Y rm N
4 zssre ⊢ ℤ ⊆ ℝ
5 frmy ⊢ Y rm : ℤ ≥ 2 × ℤ ⟶ ℤ
6 5 fovcl ⊢ A ∈ ℤ ≥ 2 ∧ a ∈ ℤ → A Y rm a ∈ ℤ
7 6 zred ⊢ A ∈ ℤ ≥ 2 ∧ a ∈ ℤ → A Y rm a ∈ ℝ
8 ltrmy ⊢ A ∈ ℤ ≥ 2 ∧ a ∈ ℤ ∧ b ∈ ℤ → a < b ↔ A Y rm a < A Y rm b
9 8 biimpd ⊢ A ∈ ℤ ≥ 2 ∧ a ∈ ℤ ∧ b ∈ ℤ → a < b → A Y rm a < A Y rm b
10 9 3expb ⊢ A ∈ ℤ ≥ 2 ∧ a ∈ ℤ ∧ b ∈ ℤ → a < b → A Y rm a < A Y rm b
11 1 2 3 4 7 10 leord1 ⊢ A ∈ ℤ ≥ 2 ∧ M ∈ ℤ ∧ N ∈ ℤ → M ≤ N ↔ A Y rm M ≤ A Y rm N
12 11 3impb ⊢ A ∈ ℤ ≥ 2 ∧ M ∈ ℤ ∧ N ∈ ℤ → M ≤ N ↔ A Y rm M ≤ A Y rm N