Metamath Proof Explorer

Theorem pell14qrdivcl

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

Ref Expression
Assertion pell14qrdivcl ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D ∧ B ∈ Pell14QR ⁡ D → A B ∈ Pell14QR ⁡ D

Proof

Step Hyp Ref Expression
1 pell14qrre ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D → A ∈ ℝ
2 1 recnd ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D → A ∈ ℂ
3 2 3adant3 ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D ∧ B ∈ Pell14QR ⁡ D → A ∈ ℂ
4 pell14qrre ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ B ∈ Pell14QR ⁡ D → B ∈ ℝ
5 4 recnd ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ B ∈ Pell14QR ⁡ D → B ∈ ℂ
6 5 3adant2 ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D ∧ B ∈ Pell14QR ⁡ D → B ∈ ℂ
7 pell14qrne0 ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ B ∈ Pell14QR ⁡ D → B ≠ 0
8 7 3adant2 ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D ∧ B ∈ Pell14QR ⁡ D → B ≠ 0
9 3 6 8 divrecd ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D ∧ B ∈ Pell14QR ⁡ D → A B = A ⁢ 1 B
10 pell14qrreccl ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ B ∈ Pell14QR ⁡ D → 1 B ∈ Pell14QR ⁡ D
11 10 3adant2 ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D ∧ B ∈ Pell14QR ⁡ D → 1 B ∈ Pell14QR ⁡ D
12 pell14qrmulcl ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D ∧ 1 B ∈ Pell14QR ⁡ D → A ⁢ 1 B ∈ Pell14QR ⁡ D
13 11 12 syld3an3 ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D ∧ B ∈ Pell14QR ⁡ D → A ⁢ 1 B ∈ Pell14QR ⁡ D
14 9 13 eqeltrd ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D ∧ B ∈ Pell14QR ⁡ D → A B ∈ Pell14QR ⁡ D