Metamath Proof Explorer

Theorem frmy

Description: The Y sequence is an integer. (Contributed by Stefan O'Rear, 22-Sep-2014)

Ref Expression
Assertion frmy ⊢ Y rm : ℤ ≥ 2 × ℤ ⟶ ℤ

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 xp2nd ⊢ c ∈ ℕ 0 × ℤ ⟼ 1 st ⁡ c + a 2 − 1 ⁢ 2 nd ⁡ c -1 ⁡ a + a 2 − 1 b ∈ ℕ 0 × ℤ → 2 nd ⁡ c ∈ ℕ 0 × ℤ ⟼ 1 st ⁡ c + a 2 − 1 ⁢ 2 nd ⁡ c -1 ⁡ a + a 2 − 1 b ∈ ℤ
3 1 2 syl ⊢ a ∈ ℤ ≥ 2 ∧ b ∈ ℤ → 2 nd ⁡ c ∈ ℕ 0 × ℤ ⟼ 1 st ⁡ c + a 2 − 1 ⁢ 2 nd ⁡ c -1 ⁡ a + a 2 − 1 b ∈ ℤ
4 3 rgen2 ⊢ ∀ a ∈ ℤ ≥ 2 ∀ b ∈ ℤ 2 nd ⁡ c ∈ ℕ 0 × ℤ ⟼ 1 st ⁡ c + a 2 − 1 ⁢ 2 nd ⁡ c -1 ⁡ a + a 2 − 1 b ∈ ℤ
5 df-rmy ⊢ Y rm = a ∈ ℤ ≥ 2 , b ∈ ℤ ⟼ 2 nd ⁡ c ∈ ℕ 0 × ℤ ⟼ 1 st ⁡ c + a 2 − 1 ⁢ 2 nd ⁡ c -1 ⁡ a + a 2 − 1 b
6 5 fmpo ⊢ ∀ a ∈ ℤ ≥ 2 ∀ b ∈ ℤ 2 nd ⁡ c ∈ ℕ 0 × ℤ ⟼ 1 st ⁡ c + a 2 − 1 ⁢ 2 nd ⁡ c -1 ⁡ a + a 2 − 1 b ∈ ℤ ↔ Y rm : ℤ ≥ 2 × ℤ ⟶ ℤ
7 4 6 mpbi ⊢ Y rm : ℤ ≥ 2 × ℤ ⟶ ℤ