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 ∈ ℤ → A X rm N 2 − A 2 − 1 ⁢ A Y rm N 2 = 1

Proof

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