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

Proof

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