Theorem pell14qrdivcl

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

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

Proof

Step	Hyp	Ref	Expression
1		pell14qrre	⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) → 𝐴 ∈ ℝ )
2	1	recnd	⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) → 𝐴 ∈ ℂ )
3	2	3adant3	⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 𝐵 ∈ ( Pell14QR ‘ 𝐷 ) ) → 𝐴 ∈ ℂ )
4		pell14qrre	⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐵 ∈ ( Pell14QR ‘ 𝐷 ) ) → 𝐵 ∈ ℝ )
5	4	recnd	⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐵 ∈ ( Pell14QR ‘ 𝐷 ) ) → 𝐵 ∈ ℂ )
6	5	3adant2	⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 𝐵 ∈ ( Pell14QR ‘ 𝐷 ) ) → 𝐵 ∈ ℂ )
7		pell14qrne0	⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐵 ∈ ( Pell14QR ‘ 𝐷 ) ) → 𝐵 ≠ 0 )
8	7	3adant2	⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 𝐵 ∈ ( Pell14QR ‘ 𝐷 ) ) → 𝐵 ≠ 0 )
9	3 6 8	divrecd	⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 𝐵 ∈ ( Pell14QR ‘ 𝐷 ) ) → ( 𝐴 / 𝐵 ) = ( 𝐴 · ( 1 / 𝐵 ) ) )
10		pell14qrreccl	⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐵 ∈ ( Pell14QR ‘ 𝐷 ) ) → ( 1 / 𝐵 ) ∈ ( Pell14QR ‘ 𝐷 ) )
11	10	3adant2	⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 𝐵 ∈ ( Pell14QR ‘ 𝐷 ) ) → ( 1 / 𝐵 ) ∈ ( Pell14QR ‘ 𝐷 ) )
12		pell14qrmulcl	⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ ( 1 / 𝐵 ) ∈ ( Pell14QR ‘ 𝐷 ) ) → ( 𝐴 · ( 1 / 𝐵 ) ) ∈ ( Pell14QR ‘ 𝐷 ) )
13	11 12	syld3an3	⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 𝐵 ∈ ( Pell14QR ‘ 𝐷 ) ) → ( 𝐴 · ( 1 / 𝐵 ) ) ∈ ( Pell14QR ‘ 𝐷 ) )
14	9 13	eqeltrd	⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 𝐵 ∈ ( Pell14QR ‘ 𝐷 ) ) → ( 𝐴 / 𝐵 ) ∈ ( Pell14QR ‘ 𝐷 ) )