Theorem pell14qrreccl

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

	Ref	Expression
Assertion	pell14qrreccl	⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) → ( 1 / 𝐴 ) ∈ ( Pell14QR ‘ 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		pell1234qrreccl	⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell1234QR ‘ 𝐷 ) ) → ( 1 / 𝐴 ) ∈ ( Pell1234QR ‘ 𝐷 ) )
2	1	adantrr	⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ( Pell1234QR ‘ 𝐷 ) ∧ 0 < 𝐴 ) ) → ( 1 / 𝐴 ) ∈ ( Pell1234QR ‘ 𝐷 ) )
3		pell1234qrre	⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell1234QR ‘ 𝐷 ) ) → 𝐴 ∈ ℝ )
4	3	adantrr	⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ( Pell1234QR ‘ 𝐷 ) ∧ 0 < 𝐴 ) ) → 𝐴 ∈ ℝ )
5		simprr	⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ( Pell1234QR ‘ 𝐷 ) ∧ 0 < 𝐴 ) ) → 0 < 𝐴 )
6	4 5	recgt0d	⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ( Pell1234QR ‘ 𝐷 ) ∧ 0 < 𝐴 ) ) → 0 < ( 1 / 𝐴 ) )
7	2 6	jca	⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ( Pell1234QR ‘ 𝐷 ) ∧ 0 < 𝐴 ) ) → ( ( 1 / 𝐴 ) ∈ ( Pell1234QR ‘ 𝐷 ) ∧ 0 < ( 1 / 𝐴 ) ) )
8	7	ex	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( ( 𝐴 ∈ ( Pell1234QR ‘ 𝐷 ) ∧ 0 < 𝐴 ) → ( ( 1 / 𝐴 ) ∈ ( Pell1234QR ‘ 𝐷 ) ∧ 0 < ( 1 / 𝐴 ) ) ) )
9		elpell14qr2	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ↔ ( 𝐴 ∈ ( Pell1234QR ‘ 𝐷 ) ∧ 0 < 𝐴 ) ) )
10		elpell14qr2	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( ( 1 / 𝐴 ) ∈ ( Pell14QR ‘ 𝐷 ) ↔ ( ( 1 / 𝐴 ) ∈ ( Pell1234QR ‘ 𝐷 ) ∧ 0 < ( 1 / 𝐴 ) ) ) )
11	8 9 10	3imtr4d	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) → ( 1 / 𝐴 ) ∈ ( Pell14QR ‘ 𝐷 ) ) )
12	11	imp	⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) → ( 1 / 𝐴 ) ∈ ( Pell14QR ‘ 𝐷 ) )