Metamath Proof Explorer

Theorem frmx

Description: The X sequence is a nonnegative integer. See rmxnn for a strengthening. (Contributed by Stefan O'Rear, 22-Sep-2014)

Ref Expression
Assertion frmx ⊢ X rm : ℤ ≥ 2 × ℤ ⟶ ℕ 0

Proof

Step Hyp Ref Expression
1 rmxyelxp ⊢ a ∈ ℤ ≥ 2 ∧ b ∈ ℤ → c ∈ ℕ 0 × ℤ ⟼ 1 st ⁡ c + a 2 − 1 ⁢ 2 nd ⁡ c -1 ⁡ a + a 2 − 1 b ∈ ℕ 0 × ℤ
2 xp1st ⊢ c ∈ ℕ 0 × ℤ ⟼ 1 st ⁡ c + a 2 − 1 ⁢ 2 nd ⁡ c -1 ⁡ a + a 2 − 1 b ∈ ℕ 0 × ℤ → 1 st ⁡ c ∈ ℕ 0 × ℤ ⟼ 1 st ⁡ c + a 2 − 1 ⁢ 2 nd ⁡ c -1 ⁡ a + a 2 − 1 b ∈ ℕ 0
3 1 2 syl ⊢ a ∈ ℤ ≥ 2 ∧ b ∈ ℤ → 1 st ⁡ c ∈ ℕ 0 × ℤ ⟼ 1 st ⁡ c + a 2 − 1 ⁢ 2 nd ⁡ c -1 ⁡ a + a 2 − 1 b ∈ ℕ 0
4 3 rgen2 ⊢ ∀ a ∈ ℤ ≥ 2 ∀ b ∈ ℤ 1 st ⁡ c ∈ ℕ 0 × ℤ ⟼ 1 st ⁡ c + a 2 − 1 ⁢ 2 nd ⁡ c -1 ⁡ a + a 2 − 1 b ∈ ℕ 0
5 df-rmx ⊢ X rm = a ∈ ℤ ≥ 2 , b ∈ ℤ ⟼ 1 st ⁡ c ∈ ℕ 0 × ℤ ⟼ 1 st ⁡ c + a 2 − 1 ⁢ 2 nd ⁡ c -1 ⁡ a + a 2 − 1 b
6 5 fmpo ⊢ ∀ a ∈ ℤ ≥ 2 ∀ b ∈ ℤ 1 st ⁡ c ∈ ℕ 0 × ℤ ⟼ 1 st ⁡ c + a 2 − 1 ⁢ 2 nd ⁡ c -1 ⁡ a + a 2 − 1 b ∈ ℕ 0 ↔ X rm : ℤ ≥ 2 × ℤ ⟶ ℕ 0
7 4 6 mpbi ⊢ X rm : ℤ ≥ 2 × ℤ ⟶ ℕ 0