Theorem rmyeq0

Description: Y is zero only at zero. (Contributed by Stefan O'Rear, 26-Sep-2014)

	Ref	Expression
Assertion	rmyeq0	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝑁 = 0 ↔ ( 𝐴 Yrm 𝑁 ) = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		0z	⊢ 0 ∈ ℤ
2		oveq2	⊢ ( 𝑎 = 𝑏 → ( 𝐴 Yrm 𝑎 ) = ( 𝐴 Yrm 𝑏 ) )
3		oveq2	⊢ ( 𝑎 = 𝑁 → ( 𝐴 Yrm 𝑎 ) = ( 𝐴 Yrm 𝑁 ) )
4		oveq2	⊢ ( 𝑎 = 0 → ( 𝐴 Yrm 𝑎 ) = ( 𝐴 Yrm 0 ) )
5		zssre	⊢ ℤ ⊆ ℝ
6		frmy	⊢ Yrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℤ
7	6	fovcl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑎 ∈ ℤ ) → ( 𝐴 Yrm 𝑎 ) ∈ ℤ )
8	7	zred	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑎 ∈ ℤ ) → ( 𝐴 Yrm 𝑎 ) ∈ ℝ )
9		ltrmy	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( 𝑎 < 𝑏 ↔ ( 𝐴 Yrm 𝑎 ) < ( 𝐴 Yrm 𝑏 ) ) )
10	9	biimpd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( 𝑎 < 𝑏 → ( 𝐴 Yrm 𝑎 ) < ( 𝐴 Yrm 𝑏 ) ) )
11	10	3expb	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑎 < 𝑏 → ( 𝐴 Yrm 𝑎 ) < ( 𝐴 Yrm 𝑏 ) ) )
12	2 3 4 5 8 11	eqord1	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 0 ∈ ℤ ) ) → ( 𝑁 = 0 ↔ ( 𝐴 Yrm 𝑁 ) = ( 𝐴 Yrm 0 ) ) )
13	1 12	mpanr2	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝑁 = 0 ↔ ( 𝐴 Yrm 𝑁 ) = ( 𝐴 Yrm 0 ) ) )
14		rmy0	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 Yrm 0 ) = 0 )
15	14	adantr	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm 0 ) = 0 )
16	15	eqeq2d	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Yrm 𝑁 ) = ( 𝐴 Yrm 0 ) ↔ ( 𝐴 Yrm 𝑁 ) = 0 ) )
17	13 16	bitrd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝑁 = 0 ↔ ( 𝐴 Yrm 𝑁 ) = 0 ) )