Theorem ltrmy

Description: The Y-sequence is strictly monotonic over ZZ . (Contributed by Stefan O'Rear, 25-Sep-2014)

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

Proof

Step	Hyp	Ref	Expression
1		ltrmynn0	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) → ( 𝑎 < 𝑏 ↔ ( 𝐴 Yrm 𝑎 ) < ( 𝐴 Yrm 𝑏 ) ) )
2	1	biimpd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) → ( 𝑎 < 𝑏 → ( 𝐴 Yrm 𝑎 ) < ( 𝐴 Yrm 𝑏 ) ) )
3		frmy	⊢ Yrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℤ
4	3	fovcl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑎 ∈ ℤ ) → ( 𝐴 Yrm 𝑎 ) ∈ ℤ )
5	4	zred	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑎 ∈ ℤ ) → ( 𝐴 Yrm 𝑎 ) ∈ ℝ )
6		rmyneg	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℤ ) → ( 𝐴 Yrm - 𝑏 ) = - ( 𝐴 Yrm 𝑏 ) )
7		oveq2	⊢ ( 𝑎 = 𝑀 → ( 𝐴 Yrm 𝑎 ) = ( 𝐴 Yrm 𝑀 ) )
8		oveq2	⊢ ( 𝑎 = 𝑁 → ( 𝐴 Yrm 𝑎 ) = ( 𝐴 Yrm 𝑁 ) )
9		oveq2	⊢ ( 𝑎 = 𝑏 → ( 𝐴 Yrm 𝑎 ) = ( 𝐴 Yrm 𝑏 ) )
10		oveq2	⊢ ( 𝑎 = - 𝑏 → ( 𝐴 Yrm 𝑎 ) = ( 𝐴 Yrm - 𝑏 ) )
11	2 5 6 7 8 9 10	monotoddzz	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 < 𝑁 ↔ ( 𝐴 Yrm 𝑀 ) < ( 𝐴 Yrm 𝑁 ) ) )