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 ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm 𝑁 ) ∈ ℕ )

Proof

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