Metamath Proof Explorer

Theorem rmyeq0

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

Ref Expression
Assertion rmyeq0 ⊢A∈ℤ≥2∧N∈ℤ→N=0↔AYrmN=0

Proof

Step Hyp Ref Expression
1 0z ⊢0∈ℤ
2 oveq2 ⊢a=b→AYrma=AYrmb
3 oveq2 ⊢a=N→AYrma=AYrmN
4 oveq2 ⊢a=0→AYrma=AYrm0
5 zssre ⊢ℤ⊆ℝ
6 frmy ⊢Yrm:ℤ≥2×ℤ⟶ℤ
7 6 fovcl ⊢A∈ℤ≥2∧a∈ℤ→AYrma∈ℤ
8 7 zred ⊢A∈ℤ≥2∧a∈ℤ→AYrma∈ℝ
9 ltrmy ⊢A∈ℤ≥2∧a∈ℤ∧b∈ℤ→a<b↔AYrma<AYrmb
10 9 biimpd ⊢A∈ℤ≥2∧a∈ℤ∧b∈ℤ→a<b→AYrma<AYrmb
11 10 3expb ⊢A∈ℤ≥2∧a∈ℤ∧b∈ℤ→a<b→AYrma<AYrmb
12 2 3 4 5 8 11 eqord1 ⊢A∈ℤ≥2∧N∈ℤ∧0∈ℤ→N=0↔AYrmN=AYrm0
13 1 12 mpanr2 ⊢A∈ℤ≥2∧N∈ℤ→N=0↔AYrmN=AYrm0
14 rmy0 ⊢A∈ℤ≥2→AYrm0=0
15 14 adantr ⊢A∈ℤ≥2∧N∈ℤ→AYrm0=0
16 15 eqeq2d ⊢A∈ℤ≥2∧N∈ℤ→AYrmN=AYrm0↔AYrmN=0
17 13 16 bitrd ⊢A∈ℤ≥2∧N∈ℤ→N=0↔AYrmN=0