pell1234qrmulcl

Description: General solutions of the Pell equation are closed under multiplication. (Contributed by Stefan O'Rear, 18-Sep-2014)

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

Proof

Step	Hyp	Ref	Expression
1		remulcl	$⊢ (A \in ℝ \land B \in ℝ) \to A B \in ℝ$
2	1	ad5antlr	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to A B \in ℝ$
3		simprl	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \to a \in ℤ$
4	3	ad3antrrr	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to a \in ℤ$
5		simplrl	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to c \in ℤ$
6	4 5	zmulcld	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to a c \in ℤ$
7		eldifi	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to D \in ℕ$
8	7	ad2antrr	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \to D \in ℕ$
9	8	nnzd	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \to D \in ℤ$
10	9	ad3antrrr	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to D \in ℤ$
11		simplrr	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to d \in ℤ$
12		simprr	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \to b \in ℤ$
13	12	ad3antrrr	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to b \in ℤ$
14	11 13	zmulcld	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to d b \in ℤ$
15	10 14	zmulcld	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to D d b \in ℤ$
16	6 15	zaddcld	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to a c + D d b \in ℤ$
17	4 11	zmulcld	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to a d \in ℤ$
18	5 13	zmulcld	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to c b \in ℤ$
19	17 18	zaddcld	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to a d + c b \in ℤ$
20		simprl	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to A = a + \sqrt{D} b$
21	20	ad2antrr	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to A = a + \sqrt{D} b$
22		simprl	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to B = c + \sqrt{D} d$
23	21 22	oveq12d	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to A B = (a + \sqrt{D} b) (c + \sqrt{D} d)$
24		zcn	$⊢ a \in ℤ \to a \in ℂ$
25	24	ad2antrl	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \to a \in ℂ$
26	25	ad3antrrr	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to a \in ℂ$
27	8	nncnd	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \to D \in ℂ$
28	27	ad3antrrr	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to D \in ℂ$
29	28	sqrtcld	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to \sqrt{D} \in ℂ$
30		zcn	$⊢ b \in ℤ \to b \in ℂ$
31	30	ad2antll	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \to b \in ℂ$
32	31	ad3antrrr	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to b \in ℂ$
33	29 32	mulcld	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to \sqrt{D} b \in ℂ$
34		zcn	$⊢ c \in ℤ \to c \in ℂ$
35	34	adantr	$⊢ (c \in ℤ \land d \in ℤ) \to c \in ℂ$
36	35	ad2antlr	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to c \in ℂ$
37		zcn	$⊢ d \in ℤ \to d \in ℂ$
38	37	adantl	$⊢ (c \in ℤ \land d \in ℤ) \to d \in ℂ$
39	38	ad2antlr	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to d \in ℂ$
40	29 39	mulcld	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to \sqrt{D} d \in ℂ$
41	26 33 36 40	muladdd	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to (a + \sqrt{D} b) (c + \sqrt{D} d) = a c + \sqrt{D} d \sqrt{D} b + a \sqrt{D} d + c \sqrt{D} b$
42	29 39 29 32	mul4d	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to \sqrt{D} d \sqrt{D} b = \sqrt{D} \sqrt{D} d b$
43	28	msqsqrtd	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to \sqrt{D} \sqrt{D} = D$
44	43	oveq1d	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to \sqrt{D} \sqrt{D} d b = D d b$
45	42 44	eqtrd	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to \sqrt{D} d \sqrt{D} b = D d b$
46	45	oveq2d	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to a c + \sqrt{D} d \sqrt{D} b = a c + D d b$
47	26 29 39	mul12d	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to a \sqrt{D} d = \sqrt{D} a d$
48	36 29 32	mul12d	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to c \sqrt{D} b = \sqrt{D} c b$
49	47 48	oveq12d	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to a \sqrt{D} d + c \sqrt{D} b = \sqrt{D} a d + \sqrt{D} c b$
50	26 39	mulcld	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to a d \in ℂ$
51	36 32	mulcld	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to c b \in ℂ$
52	29 50 51	adddid	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to \sqrt{D} (a d + c b) = \sqrt{D} a d + \sqrt{D} c b$
53	49 52	eqtr4d	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to a \sqrt{D} d + c \sqrt{D} b = \sqrt{D} (a d + c b)$
54	46 53	oveq12d	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to a c + \sqrt{D} d \sqrt{D} b + a \sqrt{D} d + c \sqrt{D} b = a c + D d b + \sqrt{D} (a d + c b)$
55	23 41 54	3eqtrd	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to A B = a c + D d b + \sqrt{D} (a d + c b)$
56	50 51	addcld	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to a d + c b \in ℂ$
57	29 56	sqmuld	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to {\sqrt{D} (a d + c b)}^{2} = {\sqrt{D}}^{2} {(a d + c b)}^{2}$
58	28	sqsqrtd	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to {\sqrt{D}}^{2} = D$
59	58	oveq1d	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to {\sqrt{D}}^{2} {(a d + c b)}^{2} = D {(a d + c b)}^{2}$
60	57 59	eqtr2d	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to D {(a d + c b)}^{2} = {\sqrt{D} (a d + c b)}^{2}$
61	60	oveq2d	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to {(a c + D d b)}^{2} - D {(a d + c b)}^{2} = {(a c + D d b)}^{2} - {\sqrt{D} (a d + c b)}^{2}$
62	26 36	mulcld	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to a c \in ℂ$
63	39 32	mulcld	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to d b \in ℂ$
64	28 63	mulcld	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to D d b \in ℂ$
65	62 64	addcld	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to a c + D d b \in ℂ$
66	29 56	mulcld	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to \sqrt{D} (a d + c b) \in ℂ$
67		subsq	$⊢ (a c + D d b \in ℂ \land \sqrt{D} (a d + c b) \in ℂ) \to {(a c + D d b)}^{2} - {\sqrt{D} (a d + c b)}^{2} = (a c + D d b + \sqrt{D} (a d + c b)) (a c + D d b - \sqrt{D} (a d + c b))$
68	65 66 67	syl2anc	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to {(a c + D d b)}^{2} - {\sqrt{D} (a d + c b)}^{2} = (a c + D d b + \sqrt{D} (a d + c b)) (a c + D d b - \sqrt{D} (a d + c b))$
69	41 54	eqtr2d	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to a c + D d b + \sqrt{D} (a d + c b) = (a + \sqrt{D} b) (c + \sqrt{D} d)$
70	26 33 36 40	mulsubd	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to (a - \sqrt{D} b) (c - \sqrt{D} d) = a c + \sqrt{D} d \sqrt{D} b - (a \sqrt{D} d + c \sqrt{D} b)$
71	46 53	oveq12d	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to a c + \sqrt{D} d \sqrt{D} b - (a \sqrt{D} d + c \sqrt{D} b) = a c + D d b - \sqrt{D} (a d + c b)$
72	70 71	eqtr2d	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to a c + D d b - \sqrt{D} (a d + c b) = (a - \sqrt{D} b) (c - \sqrt{D} d)$
73	69 72	oveq12d	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to (a c + D d b + \sqrt{D} (a d + c b)) (a c + D d b - \sqrt{D} (a d + c b)) = (a + \sqrt{D} b) (c + \sqrt{D} d) (a - \sqrt{D} b) (c - \sqrt{D} d)$
74	61 68 73	3eqtrd	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to {(a c + D d b)}^{2} - D {(a d + c b)}^{2} = (a + \sqrt{D} b) (c + \sqrt{D} d) (a - \sqrt{D} b) (c - \sqrt{D} d)$
75	26 33	addcld	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to a + \sqrt{D} b \in ℂ$
76	36 40	addcld	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to c + \sqrt{D} d \in ℂ$
77	26 33	subcld	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to a - \sqrt{D} b \in ℂ$
78	36 40	subcld	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to c - \sqrt{D} d \in ℂ$
79	75 76 77 78	mul4d	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to (a + \sqrt{D} b) (c + \sqrt{D} d) (a - \sqrt{D} b) (c - \sqrt{D} d) = (a + \sqrt{D} b) (a - \sqrt{D} b) (c + \sqrt{D} d) (c - \sqrt{D} d)$
80		subsq	$⊢ (a \in ℂ \land \sqrt{D} b \in ℂ) \to a^{2} - {\sqrt{D} b}^{2} = (a + \sqrt{D} b) (a - \sqrt{D} b)$
81	26 33 80	syl2anc	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to a^{2} - {\sqrt{D} b}^{2} = (a + \sqrt{D} b) (a - \sqrt{D} b)$
82		subsq	$⊢ (c \in ℂ \land \sqrt{D} d \in ℂ) \to c^{2} - {\sqrt{D} d}^{2} = (c + \sqrt{D} d) (c - \sqrt{D} d)$
83	36 40 82	syl2anc	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to c^{2} - {\sqrt{D} d}^{2} = (c + \sqrt{D} d) (c - \sqrt{D} d)$
84	81 83	oveq12d	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to (a^{2} - {\sqrt{D} b}^{2}) (c^{2} - {\sqrt{D} d}^{2}) = (a + \sqrt{D} b) (a - \sqrt{D} b) (c + \sqrt{D} d) (c - \sqrt{D} d)$
85	29 32	sqmuld	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to {\sqrt{D} b}^{2} = {\sqrt{D}}^{2} b^{2}$
86	85	oveq2d	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to a^{2} - {\sqrt{D} b}^{2} = a^{2} - {\sqrt{D}}^{2} b^{2}$
87	29 39	sqmuld	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to {\sqrt{D} d}^{2} = {\sqrt{D}}^{2} d^{2}$
88	87	oveq2d	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to c^{2} - {\sqrt{D} d}^{2} = c^{2} - {\sqrt{D}}^{2} d^{2}$
89	86 88	oveq12d	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to (a^{2} - {\sqrt{D} b}^{2}) (c^{2} - {\sqrt{D} d}^{2}) = (a^{2} - {\sqrt{D}}^{2} b^{2}) (c^{2} - {\sqrt{D}}^{2} d^{2})$
90	79 84 89	3eqtr2d	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to (a + \sqrt{D} b) (c + \sqrt{D} d) (a - \sqrt{D} b) (c - \sqrt{D} d) = (a^{2} - {\sqrt{D}}^{2} b^{2}) (c^{2} - {\sqrt{D}}^{2} d^{2})$
91	58	oveq1d	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to {\sqrt{D}}^{2} b^{2} = D b^{2}$
92	91	oveq2d	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to a^{2} - {\sqrt{D}}^{2} b^{2} = a^{2} - D b^{2}$
93	58	oveq1d	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to {\sqrt{D}}^{2} d^{2} = D d^{2}$
94	93	oveq2d	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to c^{2} - {\sqrt{D}}^{2} d^{2} = c^{2} - D d^{2}$
95	92 94	oveq12d	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to (a^{2} - {\sqrt{D}}^{2} b^{2}) (c^{2} - {\sqrt{D}}^{2} d^{2}) = (a^{2} - D b^{2}) (c^{2} - D d^{2})$
96		simprr	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to a^{2} - D b^{2} = 1$
97	96	ad2antrr	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to a^{2} - D b^{2} = 1$
98		simprr	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to c^{2} - D d^{2} = 1$
99	97 98	oveq12d	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to (a^{2} - D b^{2}) (c^{2} - D d^{2}) = 1 \cdot 1$
100		1t1e1	$⊢ 1 \cdot 1 = 1$
101	100	a1i	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to 1 \cdot 1 = 1$
102	95 99 101	3eqtrd	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to (a^{2} - {\sqrt{D}}^{2} b^{2}) (c^{2} - {\sqrt{D}}^{2} d^{2}) = 1$
103	74 90 102	3eqtrd	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to {(a c + D d b)}^{2} - D {(a d + c b)}^{2} = 1$
104		oveq1	$⊢ e = a c + D d b \to e + \sqrt{D} f = a c + D d b + \sqrt{D} f$
105	104	eqeq2d	$⊢ e = a c + D d b \to (A B = e + \sqrt{D} f \leftrightarrow A B = a c + D d b + \sqrt{D} f)$
106		oveq1	$⊢ e = a c + D d b \to e^{2} = {(a c + D d b)}^{2}$
107	106	oveq1d	$⊢ e = a c + D d b \to e^{2} - D f^{2} = {(a c + D d b)}^{2} - D f^{2}$
108	107	eqeq1d	$⊢ e = a c + D d b \to (e^{2} - D f^{2} = 1 \leftrightarrow {(a c + D d b)}^{2} - D f^{2} = 1)$
109	105 108	anbi12d	$⊢ e = a c + D d b \to ((A B = e + \sqrt{D} f \land e^{2} - D f^{2} = 1) \leftrightarrow (A B = a c + D d b + \sqrt{D} f \land {(a c + D d b)}^{2} - D f^{2} = 1))$
110		oveq2	$⊢ f = a d + c b \to \sqrt{D} f = \sqrt{D} (a d + c b)$
111	110	oveq2d	$⊢ f = a d + c b \to a c + D d b + \sqrt{D} f = a c + D d b + \sqrt{D} (a d + c b)$
112	111	eqeq2d	$⊢ f = a d + c b \to (A B = a c + D d b + \sqrt{D} f \leftrightarrow A B = a c + D d b + \sqrt{D} (a d + c b))$
113		oveq1	$⊢ f = a d + c b \to f^{2} = {(a d + c b)}^{2}$
114	113	oveq2d	$⊢ f = a d + c b \to D f^{2} = D {(a d + c b)}^{2}$
115	114	oveq2d	$⊢ f = a d + c b \to {(a c + D d b)}^{2} - D f^{2} = {(a c + D d b)}^{2} - D {(a d + c b)}^{2}$
116	115	eqeq1d	$⊢ f = a d + c b \to ({(a c + D d b)}^{2} - D f^{2} = 1 \leftrightarrow {(a c + D d b)}^{2} - D {(a d + c b)}^{2} = 1)$
117	112 116	anbi12d	$⊢ f = a d + c b \to ((A B = a c + D d b + \sqrt{D} f \land {(a c + D d b)}^{2} - D f^{2} = 1) \leftrightarrow (A B = a c + D d b + \sqrt{D} (a d + c b) \land {(a c + D d b)}^{2} - D {(a d + c b)}^{2} = 1))$
118	109 117	rspc2ev	$⊢ (a c + D d b \in ℤ \land a d + c b \in ℤ \land (A B = a c + D d b + \sqrt{D} (a d + c b) \land {(a c + D d b)}^{2} - D {(a d + c b)}^{2} = 1)) \to \exists e \in ℤ \exists f \in ℤ (A B = e + \sqrt{D} f \land e^{2} - D f^{2} = 1)$
119	16 19 55 103 118	syl112anc	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to \exists e \in ℤ \exists f \in ℤ (A B = e + \sqrt{D} f \land e^{2} - D f^{2} = 1)$
120	2 119	jca	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to (A B \in ℝ \land \exists e \in ℤ \exists f \in ℤ (A B = e + \sqrt{D} f \land e^{2} - D f^{2} = 1))$
121	120	ex	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (c \in ℤ \land d \in ℤ)) \to ((B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1) \to (A B \in ℝ \land \exists e \in ℤ \exists f \in ℤ (A B = e + \sqrt{D} f \land e^{2} - D f^{2} = 1)))$
122	121	rexlimdvva	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to (\exists c \in ℤ \exists d \in ℤ (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1) \to (A B \in ℝ \land \exists e \in ℤ \exists f \in ℤ (A B = e + \sqrt{D} f \land e^{2} - D f^{2} = 1)))$
123	122	ex	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \land (a \in ℤ \land b \in ℤ)) \to ((A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1) \to (\exists c \in ℤ \exists d \in ℤ (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1) \to (A B \in ℝ \land \exists e \in ℤ \exists f \in ℤ (A B = e + \sqrt{D} f \land e^{2} - D f^{2} = 1))))$
124	123	rexlimdvva	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \to (\exists a \in ℤ \exists b \in ℤ (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1) \to (\exists c \in ℤ \exists d \in ℤ (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1) \to (A B \in ℝ \land \exists e \in ℤ \exists f \in ℤ (A B = e + \sqrt{D} f \land e^{2} - D f^{2} = 1))))$
125	124	impd	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land (A \in ℝ \land B \in ℝ)) \to ((\exists a \in ℤ \exists b \in ℤ (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1) \land \exists c \in ℤ \exists d \in ℤ (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)) \to (A B \in ℝ \land \exists e \in ℤ \exists f \in ℤ (A B = e + \sqrt{D} f \land e^{2} - D f^{2} = 1)))$
126	125	expimpd	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to (((A \in ℝ \land B \in ℝ) \land (\exists a \in ℤ \exists b \in ℤ (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1) \land \exists c \in ℤ \exists d \in ℤ (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1))) \to (A B \in ℝ \land \exists e \in ℤ \exists f \in ℤ (A B = e + \sqrt{D} f \land e^{2} - D f^{2} = 1)))$
127		elpell1234qr	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to (A \in Pell1234QR (D) \leftrightarrow (A \in ℝ \land \exists a \in ℤ \exists b \in ℤ (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)))$
128		elpell1234qr	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to (B \in Pell1234QR (D) \leftrightarrow (B \in ℝ \land \exists c \in ℤ \exists d \in ℤ (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)))$
129	127 128	anbi12d	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to ((A \in Pell1234QR (D) \land B \in Pell1234QR (D)) \leftrightarrow ((A \in ℝ \land \exists a \in ℤ \exists b \in ℤ (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (B \in ℝ \land \exists c \in ℤ \exists d \in ℤ (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1))))$
130		an4	$⊢ ((A \in ℝ \land \exists a \in ℤ \exists b \in ℤ (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land (B \in ℝ \land \exists c \in ℤ \exists d \in ℤ (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1))) \leftrightarrow ((A \in ℝ \land B \in ℝ) \land (\exists a \in ℤ \exists b \in ℤ (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1) \land \exists c \in ℤ \exists d \in ℤ (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)))$
131	129 130	syl6bb	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to ((A \in Pell1234QR (D) \land B \in Pell1234QR (D)) \leftrightarrow ((A \in ℝ \land B \in ℝ) \land (\exists a \in ℤ \exists b \in ℤ (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1) \land \exists c \in ℤ \exists d \in ℤ (B = c + \sqrt{D} d \land c^{2} - D d^{2} = 1))))$
132		elpell1234qr	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to (A B \in Pell1234QR (D) \leftrightarrow (A B \in ℝ \land \exists e \in ℤ \exists f \in ℤ (A B = e + \sqrt{D} f \land e^{2} - D f^{2} = 1)))$
133	126 131 132	3imtr4d	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to ((A \in Pell1234QR (D) \land B \in Pell1234QR (D)) \to A B \in Pell1234QR (D))$
134	133	3impib	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1234QR (D) \land B \in Pell1234QR (D)) \to A B \in Pell1234QR (D)$

Metamath Proof Explorer

Theorem pell1234qrmulcl

Proof