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	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm 𝑁 ) = ( 1st ‘ ( ◡ ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st ‘ 𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd ‘ 𝑏 ) ) ) ) ‘ ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		oveq1	⊢ ( 𝑎 = 𝐴 → ( 𝑎 ↑ 2 ) = ( 𝐴 ↑ 2 ) )
2	1	fvoveq1d	⊢ ( 𝑎 = 𝐴 → ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) = ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) )
3	2	oveq1d	⊢ ( 𝑎 = 𝐴 → ( ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) · ( 2nd ‘ 𝑏 ) ) = ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd ‘ 𝑏 ) ) )
4	3	oveq2d	⊢ ( 𝑎 = 𝐴 → ( ( 1st ‘ 𝑏 ) + ( ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) · ( 2nd ‘ 𝑏 ) ) ) = ( ( 1st ‘ 𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd ‘ 𝑏 ) ) ) )
5	4	mpteq2dv	⊢ ( 𝑎 = 𝐴 → ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st ‘ 𝑏 ) + ( ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) · ( 2nd ‘ 𝑏 ) ) ) ) = ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st ‘ 𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd ‘ 𝑏 ) ) ) ) )
6	5	cnveqd	⊢ ( 𝑎 = 𝐴 → ◡ ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st ‘ 𝑏 ) + ( ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) · ( 2nd ‘ 𝑏 ) ) ) ) = ◡ ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st ‘ 𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd ‘ 𝑏 ) ) ) ) )
7	6	adantr	⊢ ( ( 𝑎 = 𝐴 ∧ 𝑛 = 𝑁 ) → ◡ ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st ‘ 𝑏 ) + ( ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) · ( 2nd ‘ 𝑏 ) ) ) ) = ◡ ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st ‘ 𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd ‘ 𝑏 ) ) ) ) )
8		id	⊢ ( 𝑎 = 𝐴 → 𝑎 = 𝐴 )
9	8 2	oveq12d	⊢ ( 𝑎 = 𝐴 → ( 𝑎 + ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) ) = ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) )
10		id	⊢ ( 𝑛 = 𝑁 → 𝑛 = 𝑁 )
11	9 10	oveqan12d	⊢ ( ( 𝑎 = 𝐴 ∧ 𝑛 = 𝑁 ) → ( ( 𝑎 + ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) ) ↑ 𝑛 ) = ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) )
12	7 11	fveq12d	⊢ ( ( 𝑎 = 𝐴 ∧ 𝑛 = 𝑁 ) → ( ◡ ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st ‘ 𝑏 ) + ( ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) · ( 2nd ‘ 𝑏 ) ) ) ) ‘ ( ( 𝑎 + ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) ) ↑ 𝑛 ) ) = ( ◡ ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st ‘ 𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd ‘ 𝑏 ) ) ) ) ‘ ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ) )
13	12	fveq2d	⊢ ( ( 𝑎 = 𝐴 ∧ 𝑛 = 𝑁 ) → ( 1st ‘ ( ◡ ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st ‘ 𝑏 ) + ( ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) · ( 2nd ‘ 𝑏 ) ) ) ) ‘ ( ( 𝑎 + ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) ) ↑ 𝑛 ) ) ) = ( 1st ‘ ( ◡ ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st ‘ 𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd ‘ 𝑏 ) ) ) ) ‘ ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ) ) )
14		df-rmx	⊢ Xrm = ( 𝑎 ∈ ( ℤ≥ ‘ 2 ) , 𝑛 ∈ ℤ ↦ ( 1st ‘ ( ◡ ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st ‘ 𝑏 ) + ( ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) · ( 2nd ‘ 𝑏 ) ) ) ) ‘ ( ( 𝑎 + ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) ) ↑ 𝑛 ) ) ) )
15		fvex	⊢ ( 1st ‘ ( ◡ ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st ‘ 𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd ‘ 𝑏 ) ) ) ) ‘ ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ) ) ∈ V
16	13 14 15	ovmpoa	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm 𝑁 ) = ( 1st ‘ ( ◡ ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st ‘ 𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd ‘ 𝑏 ) ) ) ) ‘ ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ) ) )