Metamath Proof Explorer

Theorem elpell1qr2

Description: The first quadrant solutions are precisely the positive Pell solutions which are at least one. (Contributed by Stefan O'Rear, 18-Sep-2014)

Ref Expression
Assertion elpell1qr2 ⊢ D ∈ ℕ ∖ ◻ ℕ → A ∈ Pell1QR ⁡ D ↔ A ∈ Pell14QR ⁡ D ∧ 1 ≤ A

Proof

Step Hyp Ref Expression
1 pell1qrss14 ⊢ D ∈ ℕ ∖ ◻ ℕ → Pell1QR ⁡ D ⊆ Pell14QR ⁡ D
2 1 sselda ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell1QR ⁡ D → A ∈ Pell14QR ⁡ D
3 pell1qrge1 ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell1QR ⁡ D → 1 ≤ A
4 2 3 jca ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell1QR ⁡ D → A ∈ Pell14QR ⁡ D ∧ 1 ≤ A
5 1red ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D → 1 ∈ ℝ
6 pell14qrre ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D → A ∈ ℝ
7 5 6 leloed ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D → 1 ≤ A ↔ 1 < A ∨ 1 = A
8 5 6 ltnled ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D → 1 < A ↔ ¬ A ≤ 1
9 8 biimpa ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D ∧ 1 < A → ¬ A ≤ 1
10 1div1e1 ⊢ 1 1 = 1
11 10 eqcomi ⊢ 1 = 1 1
12 11 a1i ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D ∧ 1 < A → 1 = 1 1
13 12 breq2d ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D ∧ 1 < A → A ≤ 1 ↔ A ≤ 1 1
14 6 adantr ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D ∧ 1 < A → A ∈ ℝ
15 pell14qrgt0 ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D → 0 < A
16 15 adantr ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D ∧ 1 < A → 0 < A
17 1red ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D ∧ 1 < A → 1 ∈ ℝ
18 0lt1 ⊢ 0 < 1
19 18 a1i ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D ∧ 1 < A → 0 < 1
20 lerec2 ⊢ A ∈ ℝ ∧ 0 < A ∧ 1 ∈ ℝ ∧ 0 < 1 → A ≤ 1 1 ↔ 1 ≤ 1 A
21 14 16 17 19 20 syl22anc ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D ∧ 1 < A → A ≤ 1 1 ↔ 1 ≤ 1 A
22 13 21 bitrd ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D ∧ 1 < A → A ≤ 1 ↔ 1 ≤ 1 A
23 9 22 mtbid ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D ∧ 1 < A → ¬ 1 ≤ 1 A
24 simplll ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D ∧ 1 < A ∧ 1 A ∈ Pell1QR ⁡ D → D ∈ ℕ ∖ ◻ ℕ
25 pell1qrge1 ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ 1 A ∈ Pell1QR ⁡ D → 1 ≤ 1 A
26 24 25 sylancom ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D ∧ 1 < A ∧ 1 A ∈ Pell1QR ⁡ D → 1 ≤ 1 A
27 23 26 mtand ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D ∧ 1 < A → ¬ 1 A ∈ Pell1QR ⁡ D
28 pell14qrdich ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D → A ∈ Pell1QR ⁡ D ∨ 1 A ∈ Pell1QR ⁡ D
29 28 adantr ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D ∧ 1 < A → A ∈ Pell1QR ⁡ D ∨ 1 A ∈ Pell1QR ⁡ D
30 orel2 ⊢ ¬ 1 A ∈ Pell1QR ⁡ D → A ∈ Pell1QR ⁡ D ∨ 1 A ∈ Pell1QR ⁡ D → A ∈ Pell1QR ⁡ D
31 27 29 30 sylc ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D ∧ 1 < A → A ∈ Pell1QR ⁡ D
32 simpr ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D ∧ 1 = A → 1 = A
33 pell1qr1 ⊢ D ∈ ℕ ∖ ◻ ℕ → 1 ∈ Pell1QR ⁡ D
34 33 ad2antrr ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D ∧ 1 = A → 1 ∈ Pell1QR ⁡ D
35 32 34 eqeltrrd ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D ∧ 1 = A → A ∈ Pell1QR ⁡ D
36 31 35 jaodan ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D ∧ 1 < A ∨ 1 = A → A ∈ Pell1QR ⁡ D
37 36 ex ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D → 1 < A ∨ 1 = A → A ∈ Pell1QR ⁡ D
38 7 37 sylbid ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D → 1 ≤ A → A ∈ Pell1QR ⁡ D
39 38 impr ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D ∧ 1 ≤ A → A ∈ Pell1QR ⁡ D
40 4 39 impbida ⊢ D ∈ ℕ ∖ ◻ ℕ → A ∈ Pell1QR ⁡ D ↔ A ∈ Pell14QR ⁡ D ∧ 1 ≤ A