pell1234qrreccl

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

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

Proof

Step	Hyp	Ref	Expression
1		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)))$
2	1	biimpa	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1234QR (D)) \to (A \in ℝ \land \exists a \in ℤ \exists b \in ℤ (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1))$
3		pell1234qrre	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1234QR (D)) \to A \in ℝ$
4		pell1234qrne0	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1234QR (D)) \to A \neq 0$
5	3 4	rereccld	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1234QR (D)) \to \frac{1}{A} \in ℝ$
6	5	ad2antrr	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1234QR (D)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to \frac{1}{A} \in ℝ$
7		simplrl	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1234QR (D)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to a \in ℤ$
8		simplrr	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1234QR (D)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to b \in ℤ$
9	8	znegcld	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1234QR (D)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to - b \in ℤ$
10	5	recnd	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1234QR (D)) \to \frac{1}{A} \in ℂ$
11	10	ad2antrr	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1234QR (D)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to \frac{1}{A} \in ℂ$
12		zcn	$⊢ a \in ℤ \to a \in ℂ$
13	12	adantr	$⊢ (a \in ℤ \land b \in ℤ) \to a \in ℂ$
14	13	ad2antlr	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1234QR (D)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to a \in ℂ$
15		eldifi	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to D \in ℕ$
16	15	nncnd	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to D \in ℂ$
17	16	ad3antrrr	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1234QR (D)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to D \in ℂ$
18	17	sqrtcld	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1234QR (D)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to \sqrt{D} \in ℂ$
19	8	zcnd	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1234QR (D)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to b \in ℂ$
20	19	negcld	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1234QR (D)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to - b \in ℂ$
21	18 20	mulcld	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1234QR (D)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to \sqrt{D} (- b) \in ℂ$
22	14 21	addcld	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1234QR (D)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to a + \sqrt{D} (- b) \in ℂ$
23	3	recnd	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1234QR (D)) \to A \in ℂ$
24	23	ad2antrr	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1234QR (D)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to A \in ℂ$
25	4	ad2antrr	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1234QR (D)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to A \neq 0$
26	18 19	sqmuld	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1234QR (D)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to {\sqrt{D} b}^{2} = {\sqrt{D}}^{2} b^{2}$
27	17	sqsqrtd	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1234QR (D)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to {\sqrt{D}}^{2} = D$
28	27	oveq1d	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1234QR (D)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to {\sqrt{D}}^{2} b^{2} = D b^{2}$
29	26 28	eqtr2d	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1234QR (D)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to D b^{2} = {\sqrt{D} b}^{2}$
30	29	oveq2d	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1234QR (D)) \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} = a^{2} - {\sqrt{D} b}^{2}$
31		simprr	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1234QR (D)) \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$
32	18 19	mulcld	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1234QR (D)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to \sqrt{D} b \in ℂ$
33		subsq	$⊢ (a \in ℂ \land \sqrt{D} b \in ℂ) \to a^{2} - {\sqrt{D} b}^{2} = (a + \sqrt{D} b) (a - \sqrt{D} b)$
34	14 32 33	syl2anc	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1234QR (D)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to a^{2} - {\sqrt{D} b}^{2} = (a + \sqrt{D} b) (a - \sqrt{D} b)$
35	30 31 34	3eqtr3d	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1234QR (D)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to 1 = (a + \sqrt{D} b) (a - \sqrt{D} b)$
36	24 25	recidd	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1234QR (D)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to A (\frac{1}{A}) = 1$
37		simprl	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1234QR (D)) \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$
38	18 19	mulneg2d	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1234QR (D)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to \sqrt{D} (- b) = - \sqrt{D} b$
39	38	oveq2d	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1234QR (D)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to a + \sqrt{D} (- b) = a + (- \sqrt{D} b)$
40	14 32	negsubd	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1234QR (D)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to a + (- \sqrt{D} b) = a - \sqrt{D} b$
41	39 40	eqtrd	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1234QR (D)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to a + \sqrt{D} (- b) = a - \sqrt{D} b$
42	37 41	oveq12d	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1234QR (D)) \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)) = (a + \sqrt{D} b) (a - \sqrt{D} b)$
43	35 36 42	3eqtr4d	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1234QR (D)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to A (\frac{1}{A}) = A (a + \sqrt{D} (- b))$
44	11 22 24 25 43	mulcanad	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1234QR (D)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to \frac{1}{A} = a + \sqrt{D} (- b)$
45		sqneg	$⊢ b \in ℂ \to {(- b)}^{2} = b^{2}$
46	19 45	syl	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1234QR (D)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to {(- b)}^{2} = b^{2}$
47	46	oveq2d	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1234QR (D)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to D {(- b)}^{2} = D b^{2}$
48	47	oveq2d	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1234QR (D)) \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} = a^{2} - D b^{2}$
49	48 31	eqtrd	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1234QR (D)) \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$
50		oveq1	$⊢ c = a \to c + \sqrt{D} d = a + \sqrt{D} d$
51	50	eqeq2d	$⊢ c = a \to (\frac{1}{A} = c + \sqrt{D} d \leftrightarrow \frac{1}{A} = a + \sqrt{D} d)$
52		oveq1	$⊢ c = a \to c^{2} = a^{2}$
53	52	oveq1d	$⊢ c = a \to c^{2} - D d^{2} = a^{2} - D d^{2}$
54	53	eqeq1d	$⊢ c = a \to (c^{2} - D d^{2} = 1 \leftrightarrow a^{2} - D d^{2} = 1)$
55	51 54	anbi12d	$⊢ c = a \to ((\frac{1}{A} = c + \sqrt{D} d \land c^{2} - D d^{2} = 1) \leftrightarrow (\frac{1}{A} = a + \sqrt{D} d \land a^{2} - D d^{2} = 1))$
56		oveq2	$⊢ d = - b \to \sqrt{D} d = \sqrt{D} (- b)$
57	56	oveq2d	$⊢ d = - b \to a + \sqrt{D} d = a + \sqrt{D} (- b)$
58	57	eqeq2d	$⊢ d = - b \to (\frac{1}{A} = a + \sqrt{D} d \leftrightarrow \frac{1}{A} = a + \sqrt{D} (- b))$
59		oveq1	$⊢ d = - b \to d^{2} = {(- b)}^{2}$
60	59	oveq2d	$⊢ d = - b \to D d^{2} = D {(- b)}^{2}$
61	60	oveq2d	$⊢ d = - b \to a^{2} - D d^{2} = a^{2} - D {(- b)}^{2}$
62	61	eqeq1d	$⊢ d = - b \to (a^{2} - D d^{2} = 1 \leftrightarrow a^{2} - D {(- b)}^{2} = 1)$
63	58 62	anbi12d	$⊢ d = - b \to ((\frac{1}{A} = a + \sqrt{D} d \land a^{2} - D d^{2} = 1) \leftrightarrow (\frac{1}{A} = a + \sqrt{D} (- b) \land a^{2} - D {(- b)}^{2} = 1))$
64	55 63	rspc2ev	$⊢ (a \in ℤ \land - b \in ℤ \land (\frac{1}{A} = a + \sqrt{D} (- b) \land a^{2} - D {(- b)}^{2} = 1)) \to \exists c \in ℤ \exists d \in ℤ (\frac{1}{A} = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)$
65	7 9 44 49 64	syl112anc	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1234QR (D)) \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 ℤ (\frac{1}{A} = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)$
66	6 65	jca	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1234QR (D)) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to (\frac{1}{A} \in ℝ \land \exists c \in ℤ \exists d \in ℤ (\frac{1}{A} = c + \sqrt{D} d \land c^{2} - D d^{2} = 1))$
67	66	ex	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1234QR (D)) \land (a \in ℤ \land b \in ℤ)) \to ((A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1) \to (\frac{1}{A} \in ℝ \land \exists c \in ℤ \exists d \in ℤ (\frac{1}{A} = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)))$
68	67	rexlimdvva	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1234QR (D)) \to (\exists a \in ℤ \exists b \in ℤ (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1) \to (\frac{1}{A} \in ℝ \land \exists c \in ℤ \exists d \in ℤ (\frac{1}{A} = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)))$
69	68	adantld	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1234QR (D)) \to ((A \in ℝ \land \exists a \in ℤ \exists b \in ℤ (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to (\frac{1}{A} \in ℝ \land \exists c \in ℤ \exists d \in ℤ (\frac{1}{A} = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)))$
70	2 69	mpd	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1234QR (D)) \to (\frac{1}{A} \in ℝ \land \exists c \in ℤ \exists d \in ℤ (\frac{1}{A} = c + \sqrt{D} d \land c^{2} - D d^{2} = 1))$
71		elpell1234qr	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to (\frac{1}{A} \in Pell1234QR (D) \leftrightarrow (\frac{1}{A} \in ℝ \land \exists c \in ℤ \exists d \in ℤ (\frac{1}{A} = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)))$
72	71	adantr	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1234QR (D)) \to (\frac{1}{A} \in Pell1234QR (D) \leftrightarrow (\frac{1}{A} \in ℝ \land \exists c \in ℤ \exists d \in ℤ (\frac{1}{A} = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)))$
73	70 72	mpbird	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1234QR (D)) \to \frac{1}{A} \in Pell1234QR (D)$

Metamath Proof Explorer

Theorem pell1234qrreccl

Proof