pell14qrmulcl

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

		Ref	Expression
	Assertion	pell14qrmulcl	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D) \land B \in Pell14QR (D)) \to A B \in Pell14QR (D)$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land ((A \in Pell1234QR (D) \land 0 < A) \land (B \in Pell1234QR (D) \land 0 < B))) \to D \in (ℕ ∖ ◻_{ℕ})$
2		simprll	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land ((A \in Pell1234QR (D) \land 0 < A) \land (B \in Pell1234QR (D) \land 0 < B))) \to A \in Pell1234QR (D)$
3		simprrl	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land ((A \in Pell1234QR (D) \land 0 < A) \land (B \in Pell1234QR (D) \land 0 < B))) \to B \in Pell1234QR (D)$
4		pell1234qrmulcl	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1234QR (D) \land B \in Pell1234QR (D)) \to A B \in Pell1234QR (D)$
5	1 2 3 4	syl3anc	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land ((A \in Pell1234QR (D) \land 0 < A) \land (B \in Pell1234QR (D) \land 0 < B))) \to A B \in Pell1234QR (D)$
6		pell1234qrre	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1234QR (D)) \to A \in ℝ$
7	2 6	syldan	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land ((A \in Pell1234QR (D) \land 0 < A) \land (B \in Pell1234QR (D) \land 0 < B))) \to A \in ℝ$
8		pell1234qrre	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land B \in Pell1234QR (D)) \to B \in ℝ$
9	3 8	syldan	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land ((A \in Pell1234QR (D) \land 0 < A) \land (B \in Pell1234QR (D) \land 0 < B))) \to B \in ℝ$
10		simprlr	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land ((A \in Pell1234QR (D) \land 0 < A) \land (B \in Pell1234QR (D) \land 0 < B))) \to 0 < A$
11		simprrr	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land ((A \in Pell1234QR (D) \land 0 < A) \land (B \in Pell1234QR (D) \land 0 < B))) \to 0 < B$
12	7 9 10 11	mulgt0d	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land ((A \in Pell1234QR (D) \land 0 < A) \land (B \in Pell1234QR (D) \land 0 < B))) \to 0 < A B$
13	5 12	jca	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land ((A \in Pell1234QR (D) \land 0 < A) \land (B \in Pell1234QR (D) \land 0 < B))) \to (A B \in Pell1234QR (D) \land 0 < A B)$
14	13	ex	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to (((A \in Pell1234QR (D) \land 0 < A) \land (B \in Pell1234QR (D) \land 0 < B)) \to (A B \in Pell1234QR (D) \land 0 < A B))$
15		elpell14qr2	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to (A \in Pell14QR (D) \leftrightarrow (A \in Pell1234QR (D) \land 0 < A))$
16		elpell14qr2	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to (B \in Pell14QR (D) \leftrightarrow (B \in Pell1234QR (D) \land 0 < B))$
17	15 16	anbi12d	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to ((A \in Pell14QR (D) \land B \in Pell14QR (D)) \leftrightarrow ((A \in Pell1234QR (D) \land 0 < A) \land (B \in Pell1234QR (D) \land 0 < B)))$
18		elpell14qr2	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to (A B \in Pell14QR (D) \leftrightarrow (A B \in Pell1234QR (D) \land 0 < A B))$
19	14 17 18	3imtr4d	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to ((A \in Pell14QR (D) \land B \in Pell14QR (D)) \to A B \in Pell14QR (D))$
20	19	3impib	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D) \land B \in Pell14QR (D)) \to A B \in Pell14QR (D)$

Metamath Proof Explorer

Theorem pell14qrmulcl

Proof