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 ) ) ) ↑ 𝑁 ) )