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 ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( 𝐴 ∈ ( Pell1QR ‘ 𝐷 ) ↔ ( 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 ≤ 𝐴 ) ) )

Proof

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