Metamath Proof Explorer

Theorem pell14qrreccl

Description: Positive Pell solutions are closed under reciprocal. (Contributed by Stefan O'Rear, 18-Sep-2014)

Ref Expression
Assertion pell14qrreccl ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D → 1 A ∈ Pell14QR ⁡ D

Proof

Step Hyp Ref Expression
1 pell1234qrreccl ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell1234QR ⁡ D → 1 A ∈ Pell1234QR ⁡ D
2 1 adantrr ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell1234QR ⁡ D ∧ 0 < A → 1 A ∈ Pell1234QR ⁡ D
3 pell1234qrre ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell1234QR ⁡ D → A ∈ ℝ
4 3 adantrr ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell1234QR ⁡ D ∧ 0 < A → A ∈ ℝ
5 simprr ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell1234QR ⁡ D ∧ 0 < A → 0 < A
6 4 5 recgt0d ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell1234QR ⁡ D ∧ 0 < A → 0 < 1 A
7 2 6 jca ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell1234QR ⁡ D ∧ 0 < A → 1 A ∈ Pell1234QR ⁡ D ∧ 0 < 1 A
8 7 ex ⊢ D ∈ ℕ ∖ ◻ ℕ → A ∈ Pell1234QR ⁡ D ∧ 0 < A → 1 A ∈ Pell1234QR ⁡ D ∧ 0 < 1 A
9 elpell14qr2 ⊢ D ∈ ℕ ∖ ◻ ℕ → A ∈ Pell14QR ⁡ D ↔ A ∈ Pell1234QR ⁡ D ∧ 0 < A
10 elpell14qr2 ⊢ D ∈ ℕ ∖ ◻ ℕ → 1 A ∈ Pell14QR ⁡ D ↔ 1 A ∈ Pell1234QR ⁡ D ∧ 0 < 1 A
11 8 9 10 3imtr4d ⊢ D ∈ ℕ ∖ ◻ ℕ → A ∈ Pell14QR ⁡ D → 1 A ∈ Pell14QR ⁡ D
12 11 imp ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D → 1 A ∈ Pell14QR ⁡ D