# Metamath Proof Explorer

## Theorem rmxfval

Description: Value of the X sequence. Not used after rmxyval is proved. (Contributed by Stefan O'Rear, 21-Sep-2014)

Ref Expression
Assertion rmxfval $⊢ A ∈ ℤ ≥ 2 ∧ N ∈ ℤ → A X rm N = 1 st ⁡ b ∈ ℕ 0 × ℤ ⟼ 1 st ⁡ b + A 2 − 1 ⁢ 2 nd ⁡ b -1 ⁡ A + A 2 − 1 N$

### Proof

Step Hyp Ref Expression
1 oveq1 $⊢ a = A → a 2 = A 2$
2 1 fvoveq1d $⊢ a = A → a 2 − 1 = A 2 − 1$
3 2 oveq1d $⊢ a = A → a 2 − 1 ⁢ 2 nd ⁡ b = A 2 − 1 ⁢ 2 nd ⁡ b$
4 3 oveq2d $⊢ a = A → 1 st ⁡ b + a 2 − 1 ⁢ 2 nd ⁡ b = 1 st ⁡ b + A 2 − 1 ⁢ 2 nd ⁡ b$
5 4 mpteq2dv $⊢ a = A → b ∈ ℕ 0 × ℤ ⟼ 1 st ⁡ b + a 2 − 1 ⁢ 2 nd ⁡ b = b ∈ ℕ 0 × ℤ ⟼ 1 st ⁡ b + A 2 − 1 ⁢ 2 nd ⁡ b$
6 5 cnveqd $⊢ a = A → b ∈ ℕ 0 × ℤ ⟼ 1 st ⁡ b + a 2 − 1 ⁢ 2 nd ⁡ b -1 = b ∈ ℕ 0 × ℤ ⟼ 1 st ⁡ b + A 2 − 1 ⁢ 2 nd ⁡ b -1$
7 6 adantr $⊢ a = A ∧ n = N → b ∈ ℕ 0 × ℤ ⟼ 1 st ⁡ b + a 2 − 1 ⁢ 2 nd ⁡ b -1 = b ∈ ℕ 0 × ℤ ⟼ 1 st ⁡ b + A 2 − 1 ⁢ 2 nd ⁡ b -1$
8 id $⊢ a = A → a = A$
9 8 2 oveq12d $⊢ a = A → a + a 2 − 1 = A + A 2 − 1$
10 id $⊢ n = N → n = N$
11 9 10 oveqan12d $⊢ a = A ∧ n = N → a + a 2 − 1 n = A + A 2 − 1 N$
12 7 11 fveq12d $⊢ a = A ∧ n = N → b ∈ ℕ 0 × ℤ ⟼ 1 st ⁡ b + a 2 − 1 ⁢ 2 nd ⁡ b -1 ⁡ a + a 2 − 1 n = b ∈ ℕ 0 × ℤ ⟼ 1 st ⁡ b + A 2 − 1 ⁢ 2 nd ⁡ b -1 ⁡ A + A 2 − 1 N$
13 12 fveq2d $⊢ a = A ∧ n = N → 1 st ⁡ b ∈ ℕ 0 × ℤ ⟼ 1 st ⁡ b + a 2 − 1 ⁢ 2 nd ⁡ b -1 ⁡ a + a 2 − 1 n = 1 st ⁡ b ∈ ℕ 0 × ℤ ⟼ 1 st ⁡ b + A 2 − 1 ⁢ 2 nd ⁡ b -1 ⁡ A + A 2 − 1 N$
14 df-rmx $⊢ X rm = a ∈ ℤ ≥ 2 , n ∈ ℤ ⟼ 1 st ⁡ b ∈ ℕ 0 × ℤ ⟼ 1 st ⁡ b + a 2 − 1 ⁢ 2 nd ⁡ b -1 ⁡ a + a 2 − 1 n$
15 fvex $⊢ 1 st ⁡ b ∈ ℕ 0 × ℤ ⟼ 1 st ⁡ b + A 2 − 1 ⁢ 2 nd ⁡ b -1 ⁡ A + A 2 − 1 N ∈ V$
16 13 14 15 ovmpoa $⊢ A ∈ ℤ ≥ 2 ∧ N ∈ ℤ → A X rm N = 1 st ⁡ b ∈ ℕ 0 × ℤ ⟼ 1 st ⁡ b + A 2 − 1 ⁢ 2 nd ⁡ b -1 ⁡ A + A 2 − 1 N$