Theorem lermy

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

	Ref	Expression
Assertion	lermy	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ≤ 𝑁 ↔ ( 𝐴 Yrm 𝑀 ) ≤ ( 𝐴 Yrm 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		oveq2	⊢ ( 𝑎 = 𝑏 → ( 𝐴 Yrm 𝑎 ) = ( 𝐴 Yrm 𝑏 ) )
2		oveq2	⊢ ( 𝑎 = 𝑀 → ( 𝐴 Yrm 𝑎 ) = ( 𝐴 Yrm 𝑀 ) )
3		oveq2	⊢ ( 𝑎 = 𝑁 → ( 𝐴 Yrm 𝑎 ) = ( 𝐴 Yrm 𝑁 ) )
4		zssre	⊢ ℤ ⊆ ℝ
5		frmy	⊢ Yrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℤ
6	5	fovcl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑎 ∈ ℤ ) → ( 𝐴 Yrm 𝑎 ) ∈ ℤ )
7	6	zred	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑎 ∈ ℤ ) → ( 𝐴 Yrm 𝑎 ) ∈ ℝ )
8		ltrmy	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( 𝑎 < 𝑏 ↔ ( 𝐴 Yrm 𝑎 ) < ( 𝐴 Yrm 𝑏 ) ) )
9	8	biimpd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( 𝑎 < 𝑏 → ( 𝐴 Yrm 𝑎 ) < ( 𝐴 Yrm 𝑏 ) ) )
10	9	3expb	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑎 < 𝑏 → ( 𝐴 Yrm 𝑎 ) < ( 𝐴 Yrm 𝑏 ) ) )
11	1 2 3 4 7 10	leord1	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( 𝑀 ≤ 𝑁 ↔ ( 𝐴 Yrm 𝑀 ) ≤ ( 𝐴 Yrm 𝑁 ) ) )
12	11	3impb	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ≤ 𝑁 ↔ ( 𝐴 Yrm 𝑀 ) ≤ ( 𝐴 Yrm 𝑁 ) ) )