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→1A∈Pell14QR⁡D

Proof

Step Hyp Ref Expression
1 pell1234qrreccl ⊢D∈ℕ∖◻ℕ∧A∈Pell1234QR⁡D→1A∈Pell1234QR⁡D
2 1 adantrr ⊢D∈ℕ∖◻ℕ∧A∈Pell1234QR⁡D∧0<A→1A∈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<1A
7 2 6 jca ⊢D∈ℕ∖◻ℕ∧A∈Pell1234QR⁡D∧0<A→1A∈Pell1234QR⁡D∧0<1A
8 7 ex ⊢D∈ℕ∖◻ℕ→A∈Pell1234QR⁡D∧0<A→1A∈Pell1234QR⁡D∧0<1A
9 elpell14qr2 ⊢D∈ℕ∖◻ℕ→A∈Pell14QR⁡D↔A∈Pell1234QR⁡D∧0<A
10 elpell14qr2 ⊢D∈ℕ∖◻ℕ→1A∈Pell14QR⁡D↔1A∈Pell1234QR⁡D∧0<1A
11 8 9 10 3imtr4d ⊢D∈ℕ∖◻ℕ→A∈Pell14QR⁡D→1A∈Pell14QR⁡D
12 11 imp ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D→1A∈Pell14QR⁡D