Metamath Proof Explorer

Theorem rmxyelqirr

Description: The solutions used to construct the X and Y sequences are quadratic irrationals. (Contributed by Stefan O'Rear, 21-Sep-2014)

Ref Expression
Assertion rmxyelqirr ⊢ A ∈ ℤ ≥ 2 ∧ N ∈ ℤ → A + A 2 − 1 N ∈ a | ∃ c ∈ ℕ 0 ∃ d ∈ ℤ a = c + A 2 − 1 ⁢ d

Proof

Step Hyp Ref Expression
1 rmspecnonsq ⊢ A ∈ ℤ ≥ 2 → A 2 − 1 ∈ ℕ ∖ ◻ ℕ
2 1 adantr ⊢ A ∈ ℤ ≥ 2 ∧ N ∈ ℤ → A 2 − 1 ∈ ℕ ∖ ◻ ℕ
3 pell14qrval ⊢ A 2 − 1 ∈ ℕ ∖ ◻ ℕ → Pell14QR ⁡ A 2 − 1 = a ∈ ℝ | ∃ c ∈ ℕ 0 ∃ d ∈ ℤ a = c + A 2 − 1 ⁢ d ∧ c 2 − A 2 − 1 ⁢ d 2 = 1
4 2 3 syl ⊢ A ∈ ℤ ≥ 2 ∧ N ∈ ℤ → Pell14QR ⁡ A 2 − 1 = a ∈ ℝ | ∃ c ∈ ℕ 0 ∃ d ∈ ℤ a = c + A 2 − 1 ⁢ d ∧ c 2 − A 2 − 1 ⁢ d 2 = 1
5 simpl ⊢ a = c + A 2 − 1 ⁢ d ∧ c 2 − A 2 − 1 ⁢ d 2 = 1 → a = c + A 2 − 1 ⁢ d
6 5 reximi ⊢ ∃ d ∈ ℤ a = c + A 2 − 1 ⁢ d ∧ c 2 − A 2 − 1 ⁢ d 2 = 1 → ∃ d ∈ ℤ a = c + A 2 − 1 ⁢ d
7 6 reximi ⊢ ∃ c ∈ ℕ 0 ∃ d ∈ ℤ a = c + A 2 − 1 ⁢ d ∧ c 2 − A 2 − 1 ⁢ d 2 = 1 → ∃ c ∈ ℕ 0 ∃ d ∈ ℤ a = c + A 2 − 1 ⁢ d
8 7 rgenw ⊢ ∀ a ∈ ℝ ∃ c ∈ ℕ 0 ∃ d ∈ ℤ a = c + A 2 − 1 ⁢ d ∧ c 2 − A 2 − 1 ⁢ d 2 = 1 → ∃ c ∈ ℕ 0 ∃ d ∈ ℤ a = c + A 2 − 1 ⁢ d
9 8 a1i ⊢ A ∈ ℤ ≥ 2 ∧ N ∈ ℤ → ∀ a ∈ ℝ ∃ c ∈ ℕ 0 ∃ d ∈ ℤ a = c + A 2 − 1 ⁢ d ∧ c 2 − A 2 − 1 ⁢ d 2 = 1 → ∃ c ∈ ℕ 0 ∃ d ∈ ℤ a = c + A 2 − 1 ⁢ d
10 ss2rab ⊢ a ∈ ℝ | ∃ c ∈ ℕ 0 ∃ d ∈ ℤ a = c + A 2 − 1 ⁢ d ∧ c 2 − A 2 − 1 ⁢ d 2 = 1 ⊆ a ∈ ℝ | ∃ c ∈ ℕ 0 ∃ d ∈ ℤ a = c + A 2 − 1 ⁢ d ↔ ∀ a ∈ ℝ ∃ c ∈ ℕ 0 ∃ d ∈ ℤ a = c + A 2 − 1 ⁢ d ∧ c 2 − A 2 − 1 ⁢ d 2 = 1 → ∃ c ∈ ℕ 0 ∃ d ∈ ℤ a = c + A 2 − 1 ⁢ d
11 9 10 sylibr ⊢ A ∈ ℤ ≥ 2 ∧ N ∈ ℤ → a ∈ ℝ | ∃ c ∈ ℕ 0 ∃ d ∈ ℤ a = c + A 2 − 1 ⁢ d ∧ c 2 − A 2 − 1 ⁢ d 2 = 1 ⊆ a ∈ ℝ | ∃ c ∈ ℕ 0 ∃ d ∈ ℤ a = c + A 2 − 1 ⁢ d
12 ssv ⊢ ℝ ⊆ V
13 rabss2 ⊢ ℝ ⊆ V → a ∈ ℝ | ∃ c ∈ ℕ 0 ∃ d ∈ ℤ a = c + A 2 − 1 ⁢ d ⊆ a ∈ V | ∃ c ∈ ℕ 0 ∃ d ∈ ℤ a = c + A 2 − 1 ⁢ d
14 12 13 ax-mp ⊢ a ∈ ℝ | ∃ c ∈ ℕ 0 ∃ d ∈ ℤ a = c + A 2 − 1 ⁢ d ⊆ a ∈ V | ∃ c ∈ ℕ 0 ∃ d ∈ ℤ a = c + A 2 − 1 ⁢ d
15 11 14 sstrdi ⊢ A ∈ ℤ ≥ 2 ∧ N ∈ ℤ → a ∈ ℝ | ∃ c ∈ ℕ 0 ∃ d ∈ ℤ a = c + A 2 − 1 ⁢ d ∧ c 2 − A 2 − 1 ⁢ d 2 = 1 ⊆ a ∈ V | ∃ c ∈ ℕ 0 ∃ d ∈ ℤ a = c + A 2 − 1 ⁢ d
16 rabab ⊢ a ∈ V | ∃ c ∈ ℕ 0 ∃ d ∈ ℤ a = c + A 2 − 1 ⁢ d = a | ∃ c ∈ ℕ 0 ∃ d ∈ ℤ a = c + A 2 − 1 ⁢ d
17 15 16 sseqtrdi ⊢ A ∈ ℤ ≥ 2 ∧ N ∈ ℤ → a ∈ ℝ | ∃ c ∈ ℕ 0 ∃ d ∈ ℤ a = c + A 2 − 1 ⁢ d ∧ c 2 − A 2 − 1 ⁢ d 2 = 1 ⊆ a | ∃ c ∈ ℕ 0 ∃ d ∈ ℤ a = c + A 2 − 1 ⁢ d
18 4 17 eqsstrd ⊢ A ∈ ℤ ≥ 2 ∧ N ∈ ℤ → Pell14QR ⁡ A 2 − 1 ⊆ a | ∃ c ∈ ℕ 0 ∃ d ∈ ℤ a = c + A 2 − 1 ⁢ d
19 simpr ⊢ A ∈ ℤ ≥ 2 ∧ N ∈ ℤ → N ∈ ℤ
20 rmspecfund ⊢ A ∈ ℤ ≥ 2 → PellFund ⁡ A 2 − 1 = A + A 2 − 1
21 20 adantr ⊢ A ∈ ℤ ≥ 2 ∧ N ∈ ℤ → PellFund ⁡ A 2 − 1 = A + A 2 − 1
22 21 eqcomd ⊢ A ∈ ℤ ≥ 2 ∧ N ∈ ℤ → A + A 2 − 1 = PellFund ⁡ A 2 − 1
23 22 oveq1d ⊢ A ∈ ℤ ≥ 2 ∧ N ∈ ℤ → A + A 2 − 1 N = PellFund ⁡ A 2 − 1 N
24 oveq2 ⊢ a = N → PellFund ⁡ A 2 − 1 a = PellFund ⁡ A 2 − 1 N
25 24 rspceeqv ⊢ N ∈ ℤ ∧ A + A 2 − 1 N = PellFund ⁡ A 2 − 1 N → ∃ a ∈ ℤ A + A 2 − 1 N = PellFund ⁡ A 2 − 1 a
26 19 23 25 syl2anc ⊢ A ∈ ℤ ≥ 2 ∧ N ∈ ℤ → ∃ a ∈ ℤ A + A 2 − 1 N = PellFund ⁡ A 2 − 1 a
27 pellfund14b ⊢ A 2 − 1 ∈ ℕ ∖ ◻ ℕ → A + A 2 − 1 N ∈ Pell14QR ⁡ A 2 − 1 ↔ ∃ a ∈ ℤ A + A 2 − 1 N = PellFund ⁡ A 2 − 1 a
28 2 27 syl ⊢ A ∈ ℤ ≥ 2 ∧ N ∈ ℤ → A + A 2 − 1 N ∈ Pell14QR ⁡ A 2 − 1 ↔ ∃ a ∈ ℤ A + A 2 − 1 N = PellFund ⁡ A 2 − 1 a
29 26 28 mpbird ⊢ A ∈ ℤ ≥ 2 ∧ N ∈ ℤ → A + A 2 − 1 N ∈ Pell14QR ⁡ A 2 − 1
30 18 29 sseldd ⊢ A ∈ ℤ ≥ 2 ∧ N ∈ ℤ → A + A 2 − 1 N ∈ a | ∃ c ∈ ℕ 0 ∃ d ∈ ℤ a = c + A 2 − 1 ⁢ d