lermy

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

		Ref	Expression
	Assertion	lermy	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to (M \leq N \leftrightarrow A Y_{rm} M \leq A Y_{rm} N)$

Step	Hyp	Ref	Expression
1		oveq2	$⊢ a = b \to A Y_{rm} a = A Y_{rm} b$
2		oveq2	$⊢ a = M \to A Y_{rm} a = A Y_{rm} M$
3		oveq2	$⊢ a = N \to A Y_{rm} a = A Y_{rm} N$
4		zssre	$⊢ ℤ \subseteq ℝ$
5		frmy	$⊢ Y_{rm} : ℤ_{\geq 2} \times ℤ ⟶ ℤ$
6	5	fovcl	$⊢ (A \in ℤ_{\geq 2} \land a \in ℤ) \to A Y_{rm} a \in ℤ$
7	6	zred	$⊢ (A \in ℤ_{\geq 2} \land a \in ℤ) \to A Y_{rm} a \in ℝ$
8		ltrmy	$⊢ (A \in ℤ_{\geq 2} \land a \in ℤ \land b \in ℤ) \to (a < b \leftrightarrow A Y_{rm} a < A Y_{rm} b)$
9	8	biimpd	$⊢ (A \in ℤ_{\geq 2} \land a \in ℤ \land b \in ℤ) \to (a < b \to A Y_{rm} a < A Y_{rm} b)$
10	9	3expb	$⊢ (A \in ℤ_{\geq 2} \land (a \in ℤ \land b \in ℤ)) \to (a < b \to A Y_{rm} a < A Y_{rm} b)$
11	1 2 3 4 7 10	leord1	$⊢ (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \to (M \leq N \leftrightarrow A Y_{rm} M \leq A Y_{rm} N)$
12	11	3impb	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to (M \leq N \leftrightarrow A Y_{rm} M \leq A Y_{rm} N)$

Metamath Proof Explorer