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 ⊢A∈ℤ≥2∧N∈ℤ→AXrmN2−A2−1⁢AYrmN2=1

Proof

Step Hyp Ref Expression
1 simpr ⊢A∈ℤ≥2∧N∈ℤ→N∈ℤ
2 eqidd ⊢A∈ℤ≥2→AXrmN=AXrmN
3 eqidd ⊢N∈ℤ→AYrmN=AYrmN
4 2 3 anim12i ⊢A∈ℤ≥2∧N∈ℤ→AXrmN=AXrmN∧AYrmN=AYrmN
5 oveq2 ⊢a=N→AXrma=AXrmN
6 5 eqeq2d ⊢a=N→AXrmN=AXrma↔AXrmN=AXrmN
7 oveq2 ⊢a=N→AYrma=AYrmN
8 7 eqeq2d ⊢a=N→AYrmN=AYrma↔AYrmN=AYrmN
9 6 8 anbi12d ⊢a=N→AXrmN=AXrma∧AYrmN=AYrma↔AXrmN=AXrmN∧AYrmN=AYrmN
10 9 rspcev ⊢N∈ℤ∧AXrmN=AXrmN∧AYrmN=AYrmN→∃a∈ℤAXrmN=AXrma∧AYrmN=AYrma
11 1 4 10 syl2anc ⊢A∈ℤ≥2∧N∈ℤ→∃a∈ℤAXrmN=AXrma∧AYrmN=AYrma
12 simpl ⊢A∈ℤ≥2∧N∈ℤ→A∈ℤ≥2
13 frmx ⊢Xrm:ℤ≥2×ℤ⟶ℕ0
14 13 fovcl ⊢A∈ℤ≥2∧N∈ℤ→AXrmN∈ℕ0
15 frmy ⊢Yrm:ℤ≥2×ℤ⟶ℤ
16 15 fovcl ⊢A∈ℤ≥2∧N∈ℤ→AYrmN∈ℤ
17 rmxycomplete ⊢A∈ℤ≥2∧AXrmN∈ℕ0∧AYrmN∈ℤ→AXrmN2−A2−1⁢AYrmN2=1↔∃a∈ℤAXrmN=AXrma∧AYrmN=AYrma
18 12 14 16 17 syl3anc ⊢A∈ℤ≥2∧N∈ℤ→AXrmN2−A2−1⁢AYrmN2=1↔∃a∈ℤAXrmN=AXrma∧AYrmN=AYrma
19 11 18 mpbird ⊢A∈ℤ≥2∧N∈ℤ→AXrmN2−A2−1⁢AYrmN2=1