Metamath Proof Explorer

Theorem rmxynorm

Description: The X and Y sequences define a solution to the corresponding Pell equation. (Contributed by Stefan O'Rear, 22-Sep-2014)

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

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → 𝑁 ∈ ℤ )
2 eqidd ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 Xrm 𝑁 ) = ( 𝐴 Xrm 𝑁 ) )
3 eqidd ⊢ ( 𝑁 ∈ ℤ → ( 𝐴 Yrm 𝑁 ) = ( 𝐴 Yrm 𝑁 ) )
4 2 3 anim12i ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Xrm 𝑁 ) = ( 𝐴 Xrm 𝑁 ) ∧ ( 𝐴 Yrm 𝑁 ) = ( 𝐴 Yrm 𝑁 ) ) )
5 oveq2 ⊢ ( 𝑎 = 𝑁 → ( 𝐴 Xrm 𝑎 ) = ( 𝐴 Xrm 𝑁 ) )
6 5 eqeq2d ⊢ ( 𝑎 = 𝑁 → ( ( 𝐴 Xrm 𝑁 ) = ( 𝐴 Xrm 𝑎 ) ↔ ( 𝐴 Xrm 𝑁 ) = ( 𝐴 Xrm 𝑁 ) ) )
7 oveq2 ⊢ ( 𝑎 = 𝑁 → ( 𝐴 Yrm 𝑎 ) = ( 𝐴 Yrm 𝑁 ) )
8 7 eqeq2d ⊢ ( 𝑎 = 𝑁 → ( ( 𝐴 Yrm 𝑁 ) = ( 𝐴 Yrm 𝑎 ) ↔ ( 𝐴 Yrm 𝑁 ) = ( 𝐴 Yrm 𝑁 ) ) )
9 6 8 anbi12d ⊢ ( 𝑎 = 𝑁 → ( ( ( 𝐴 Xrm 𝑁 ) = ( 𝐴 Xrm 𝑎 ) ∧ ( 𝐴 Yrm 𝑁 ) = ( 𝐴 Yrm 𝑎 ) ) ↔ ( ( 𝐴 Xrm 𝑁 ) = ( 𝐴 Xrm 𝑁 ) ∧ ( 𝐴 Yrm 𝑁 ) = ( 𝐴 Yrm 𝑁 ) ) ) )
10 9 rspcev ⊢ ( ( 𝑁 ∈ ℤ ∧ ( ( 𝐴 Xrm 𝑁 ) = ( 𝐴 Xrm 𝑁 ) ∧ ( 𝐴 Yrm 𝑁 ) = ( 𝐴 Yrm 𝑁 ) ) ) → ∃ 𝑎 ∈ ℤ ( ( 𝐴 Xrm 𝑁 ) = ( 𝐴 Xrm 𝑎 ) ∧ ( 𝐴 Yrm 𝑁 ) = ( 𝐴 Yrm 𝑎 ) ) )
11 1 4 10 syl2anc ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ∃ 𝑎 ∈ ℤ ( ( 𝐴 Xrm 𝑁 ) = ( 𝐴 Xrm 𝑎 ) ∧ ( 𝐴 Yrm 𝑁 ) = ( 𝐴 Yrm 𝑎 ) ) )
12 simpl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → 𝐴 ∈ ( ℤ≥ ‘ 2 ) )
13 frmx ⊢ Xrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℕ0
14 13 fovcl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm 𝑁 ) ∈ ℕ0 )
15 frmy ⊢ Yrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℤ
16 15 fovcl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm 𝑁 ) ∈ ℤ )
17 rmxycomplete ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝐴 Xrm 𝑁 ) ∈ ℕ0 ∧ ( 𝐴 Yrm 𝑁 ) ∈ ℤ ) → ( ( ( ( 𝐴 Xrm 𝑁 ) ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ) ) = 1 ↔ ∃ 𝑎 ∈ ℤ ( ( 𝐴 Xrm 𝑁 ) = ( 𝐴 Xrm 𝑎 ) ∧ ( 𝐴 Yrm 𝑁 ) = ( 𝐴 Yrm 𝑎 ) ) ) )
18 12 14 16 17 syl3anc ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( ( ( 𝐴 Xrm 𝑁 ) ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ) ) = 1 ↔ ∃ 𝑎 ∈ ℤ ( ( 𝐴 Xrm 𝑁 ) = ( 𝐴 Xrm 𝑎 ) ∧ ( 𝐴 Yrm 𝑁 ) = ( 𝐴 Yrm 𝑎 ) ) ) )
19 11 18 mpbird ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝐴 Xrm 𝑁 ) ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ) ) = 1 )