# Metamath Proof Explorer

## Theorem rmxyval

Description: Main definition of the X and Y sequences. Compare definition 2.3 of JonesMatijasevic p. 694. (Contributed by Stefan O'Rear, 19-Oct-2014)

Ref Expression
Assertion rmxyval ( ( 𝐴 ∈ ( ℤ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Xrm 𝑁 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) ) = ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) )

### Proof

Step Hyp Ref Expression
1 rmxfval ( ( 𝐴 ∈ ( ℤ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm 𝑁 ) = ( 1st ‘ ( ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) ‘ ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ) ) )
2 rmyfval ( ( 𝐴 ∈ ( ℤ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm 𝑁 ) = ( 2nd ‘ ( ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) ‘ ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ) ) )
3 2 oveq2d ( ( 𝐴 ∈ ( ℤ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) = ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd ‘ ( ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) ‘ ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ) ) ) )
4 1 3 oveq12d ( ( 𝐴 ∈ ( ℤ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Xrm 𝑁 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) ) = ( ( 1st ‘ ( ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) ‘ ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ) ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd ‘ ( ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) ‘ ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ) ) ) ) )
5 rmxyelxp ( ( 𝐴 ∈ ( ℤ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) ‘ ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ) ∈ ( ℕ0 × ℤ ) )
6 fveq2 ( 𝑎 = ( ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) ‘ ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ) → ( 1st𝑎 ) = ( 1st ‘ ( ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) ‘ ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ) ) )
7 fveq2 ( 𝑎 = ( ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) ‘ ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ) → ( 2nd𝑎 ) = ( 2nd ‘ ( ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) ‘ ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ) ) )
8 7 oveq2d ( 𝑎 = ( ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) ‘ ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ) → ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑎 ) ) = ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd ‘ ( ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) ‘ ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ) ) ) )
9 6 8 oveq12d ( 𝑎 = ( ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) ‘ ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ) → ( ( 1st𝑎 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑎 ) ) ) = ( ( 1st ‘ ( ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) ‘ ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ) ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd ‘ ( ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) ‘ ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ) ) ) ) )
10 fveq2 ( 𝑏 = 𝑎 → ( 1st𝑏 ) = ( 1st𝑎 ) )
11 fveq2 ( 𝑏 = 𝑎 → ( 2nd𝑏 ) = ( 2nd𝑎 ) )
12 11 oveq2d ( 𝑏 = 𝑎 → ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) = ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑎 ) ) )
13 10 12 oveq12d ( 𝑏 = 𝑎 → ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) = ( ( 1st𝑎 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑎 ) ) ) )
14 13 cbvmptv ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) = ( 𝑎 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑎 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑎 ) ) ) )
15 ovex ( ( 1st ‘ ( ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) ‘ ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ) ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd ‘ ( ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) ‘ ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ) ) ) ) ∈ V
16 9 14 15 fvmpt ( ( ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) ‘ ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ) ∈ ( ℕ0 × ℤ ) → ( ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) ‘ ( ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) ‘ ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ) ) = ( ( 1st ‘ ( ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) ‘ ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ) ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd ‘ ( ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) ‘ ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ) ) ) ) )
17 5 16 syl ( ( 𝐴 ∈ ( ℤ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) ‘ ( ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) ‘ ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ) ) = ( ( 1st ‘ ( ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) ‘ ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ) ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd ‘ ( ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) ‘ ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ) ) ) ) )
18 rmxypairf1o ( 𝐴 ∈ ( ℤ ‘ 2 ) → ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) : ( ℕ0 × ℤ ) –1-1-onto→ { 𝑎 ∣ ∃ 𝑐 ∈ ℕ0𝑑 ∈ ℤ 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) } )
19 18 adantr ( ( 𝐴 ∈ ( ℤ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) : ( ℕ0 × ℤ ) –1-1-onto→ { 𝑎 ∣ ∃ 𝑐 ∈ ℕ0𝑑 ∈ ℤ 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) } )
20 rmxyelqirr ( ( 𝐴 ∈ ( ℤ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ∈ { 𝑎 ∣ ∃ 𝑐 ∈ ℕ0𝑑 ∈ ℤ 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) } )
21 f1ocnvfv2 ( ( ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) : ( ℕ0 × ℤ ) –1-1-onto→ { 𝑎 ∣ ∃ 𝑐 ∈ ℕ0𝑑 ∈ ℤ 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) } ∧ ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ∈ { 𝑎 ∣ ∃ 𝑐 ∈ ℕ0𝑑 ∈ ℤ 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) } ) → ( ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) ‘ ( ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) ‘ ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ) ) = ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) )
22 19 20 21 syl2anc ( ( 𝐴 ∈ ( ℤ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) ‘ ( ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) ‘ ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ) ) = ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) )
23 4 17 22 3eqtr2d ( ( 𝐴 ∈ ( ℤ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Xrm 𝑁 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) ) = ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) )