Theorem rmxyelxp

Description: Lemma for frmx and frmy . (Contributed by Stefan O'Rear, 22-Sep-2014)

	Ref	Expression
Assertion	rmxyelxp	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ◡ ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st ‘ 𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd ‘ 𝑏 ) ) ) ) ‘ ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ) ∈ ( ℕ0 × ℤ ) )

Proof

Step	Hyp	Ref	Expression
1		rmxypairf1o	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st ‘ 𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd ‘ 𝑏 ) ) ) ) : ( ℕ0 × ℤ ) –1-1-onto→ { 𝑎 ∣ ∃ 𝑐 ∈ ℕ0 ∃ 𝑑 ∈ ℤ 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) } )
2	1	adantr	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st ‘ 𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd ‘ 𝑏 ) ) ) ) : ( ℕ0 × ℤ ) –1-1-onto→ { 𝑎 ∣ ∃ 𝑐 ∈ ℕ0 ∃ 𝑑 ∈ ℤ 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) } )
3		rmxyelqirr	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ∈ { 𝑎 ∣ ∃ 𝑐 ∈ ℕ0 ∃ 𝑑 ∈ ℤ 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) } )
4		f1ocnvdm	⊢ ( ( ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st ‘ 𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd ‘ 𝑏 ) ) ) ) : ( ℕ0 × ℤ ) –1-1-onto→ { 𝑎 ∣ ∃ 𝑐 ∈ ℕ0 ∃ 𝑑 ∈ ℤ 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) } ∧ ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ∈ { 𝑎 ∣ ∃ 𝑐 ∈ ℕ0 ∃ 𝑑 ∈ ℤ 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) } ) → ( ◡ ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st ‘ 𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd ‘ 𝑏 ) ) ) ) ‘ ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ) ∈ ( ℕ0 × ℤ ) )
5	2 3 4	syl2anc	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ◡ ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st ‘ 𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd ‘ 𝑏 ) ) ) ) ‘ ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ) ∈ ( ℕ0 × ℤ ) )