Metamath Proof Explorer

Theorem elpell14qr2

Description: A number is a positive Pell solution iff it is positive and a Pell solution, justifying our name choice. (Contributed by Stefan O'Rear, 19-Oct-2014)

Ref Expression
Assertion elpell14qr2 ⊢ D ∈ ℕ ∖ ◻ ℕ → A ∈ Pell14QR ⁡ D ↔ A ∈ Pell1234QR ⁡ D ∧ 0 < A

Proof

Step Hyp Ref Expression
1 pell14qrss1234 ⊢ D ∈ ℕ ∖ ◻ ℕ → Pell14QR ⁡ D ⊆ Pell1234QR ⁡ D
2 1 sselda ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D → A ∈ Pell1234QR ⁡ D
3 pell14qrgt0 ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D → 0 < A
4 2 3 jca ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D → A ∈ Pell1234QR ⁡ D ∧ 0 < A
5 0re ⊢ 0 ∈ ℝ
6 pell1234qrre ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell1234QR ⁡ D → A ∈ ℝ
7 ltnsym ⊢ 0 ∈ ℝ ∧ A ∈ ℝ → 0 < A → ¬ A < 0
8 5 6 7 sylancr ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell1234QR ⁡ D → 0 < A → ¬ A < 0
9 8 impr ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell1234QR ⁡ D ∧ 0 < A → ¬ A < 0
10 6 adantrr ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell1234QR ⁡ D ∧ 0 < A → A ∈ ℝ
11 10 lt0neg1d ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell1234QR ⁡ D ∧ 0 < A → A < 0 ↔ 0 < − A
12 9 11 mtbid ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell1234QR ⁡ D ∧ 0 < A → ¬ 0 < − A
13 pell14qrgt0 ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ − A ∈ Pell14QR ⁡ D → 0 < − A
14 13 ex ⊢ D ∈ ℕ ∖ ◻ ℕ → − A ∈ Pell14QR ⁡ D → 0 < − A
15 14 adantr ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell1234QR ⁡ D ∧ 0 < A → − A ∈ Pell14QR ⁡ D → 0 < − A
16 12 15 mtod ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell1234QR ⁡ D ∧ 0 < A → ¬ − A ∈ Pell14QR ⁡ D
17 pell1234qrdich ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell1234QR ⁡ D → A ∈ Pell14QR ⁡ D ∨ − A ∈ Pell14QR ⁡ D
18 17 adantrr ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell1234QR ⁡ D ∧ 0 < A → A ∈ Pell14QR ⁡ D ∨ − A ∈ Pell14QR ⁡ D
19 orel2 ⊢ ¬ − A ∈ Pell14QR ⁡ D → A ∈ Pell14QR ⁡ D ∨ − A ∈ Pell14QR ⁡ D → A ∈ Pell14QR ⁡ D
20 16 18 19 sylc ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell1234QR ⁡ D ∧ 0 < A → A ∈ Pell14QR ⁡ D
21 4 20 impbida ⊢ D ∈ ℕ ∖ ◻ ℕ → A ∈ Pell14QR ⁡ D ↔ A ∈ Pell1234QR ⁡ D ∧ 0 < A