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 ↔ A Y rm N = 0

Proof

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