Metamath Proof Explorer

Theorem rmxnn

Description: The X-sequence is defined to range over NN0 but never actually takes the value 0. (Contributed by Stefan O'Rear, 4-Oct-2014)

Ref Expression
Assertion rmxnn ⊢ A ∈ ℤ ≥ 2 ∧ N ∈ ℤ → A X rm N ∈ ℕ

Proof

Step Hyp Ref Expression
1 nn0z ⊢ N ∈ ℕ 0 → N ∈ ℤ
2 frmx ⊢ X rm : ℤ ≥ 2 × ℤ ⟶ ℕ 0
3 2 fovcl ⊢ A ∈ ℤ ≥ 2 ∧ N ∈ ℤ → A X rm N ∈ ℕ 0
4 1 3 sylan2 ⊢ A ∈ ℤ ≥ 2 ∧ N ∈ ℕ 0 → A X rm N ∈ ℕ 0
5 rmxypos ⊢ A ∈ ℤ ≥ 2 ∧ N ∈ ℕ 0 → 0 < A X rm N ∧ 0 ≤ A Y rm N
6 5 simpld ⊢ A ∈ ℤ ≥ 2 ∧ N ∈ ℕ 0 → 0 < A X rm N
7 elnnnn0b ⊢ A X rm N ∈ ℕ ↔ A X rm N ∈ ℕ 0 ∧ 0 < A X rm N
8 4 6 7 sylanbrc ⊢ A ∈ ℤ ≥ 2 ∧ N ∈ ℕ 0 → A X rm N ∈ ℕ
9 8 adantlr ⊢ A ∈ ℤ ≥ 2 ∧ N ∈ ℤ ∧ N ∈ ℕ 0 → A X rm N ∈ ℕ
10 rmxneg ⊢ A ∈ ℤ ≥ 2 ∧ N ∈ ℤ → A X rm -N = A X rm N
11 10 adantr ⊢ A ∈ ℤ ≥ 2 ∧ N ∈ ℤ ∧ − N ∈ ℕ 0 → A X rm -N = A X rm N
12 nn0z ⊢ − N ∈ ℕ 0 → − N ∈ ℤ
13 2 fovcl ⊢ A ∈ ℤ ≥ 2 ∧ − N ∈ ℤ → A X rm -N ∈ ℕ 0
14 12 13 sylan2 ⊢ A ∈ ℤ ≥ 2 ∧ − N ∈ ℕ 0 → A X rm -N ∈ ℕ 0
15 rmxypos ⊢ A ∈ ℤ ≥ 2 ∧ − N ∈ ℕ 0 → 0 < A X rm -N ∧ 0 ≤ A Y rm -N
16 15 simpld ⊢ A ∈ ℤ ≥ 2 ∧ − N ∈ ℕ 0 → 0 < A X rm -N
17 elnnnn0b ⊢ A X rm -N ∈ ℕ ↔ A X rm -N ∈ ℕ 0 ∧ 0 < A X rm -N
18 14 16 17 sylanbrc ⊢ A ∈ ℤ ≥ 2 ∧ − N ∈ ℕ 0 → A X rm -N ∈ ℕ
19 18 adantlr ⊢ A ∈ ℤ ≥ 2 ∧ N ∈ ℤ ∧ − N ∈ ℕ 0 → A X rm -N ∈ ℕ
20 11 19 eqeltrrd ⊢ A ∈ ℤ ≥ 2 ∧ N ∈ ℤ ∧ − N ∈ ℕ 0 → A X rm N ∈ ℕ
21 elznn0 ⊢ N ∈ ℤ ↔ N ∈ ℝ ∧ N ∈ ℕ 0 ∨ − N ∈ ℕ 0
22 21 simprbi ⊢ N ∈ ℤ → N ∈ ℕ 0 ∨ − N ∈ ℕ 0
23 22 adantl ⊢ A ∈ ℤ ≥ 2 ∧ N ∈ ℤ → N ∈ ℕ 0 ∨ − N ∈ ℕ 0
24 9 20 23 mpjaodan ⊢ A ∈ ℤ ≥ 2 ∧ N ∈ ℤ → A X rm N ∈ ℕ