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