pell14qrdich

Description: A positive Pell solution is either in the first quadrant, or its reciprocal is. (Contributed by Stefan O'Rear, 18-Sep-2014)

		Ref	Expression
	Assertion	pell14qrdich	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to (A \in Pell1QR (D) \lor \frac{1}{A} \in Pell1QR (D))$

Proof

Step	Hyp	Ref	Expression
1		elpell14qr	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to (A \in Pell14QR (D) \leftrightarrow (A \in ℝ \land \exists a \in ℕ_{0} \exists b \in ℤ (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)))$
2	1	biimpa	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to (A \in ℝ \land \exists a \in ℕ_{0} \exists b \in ℤ (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1))$
3		simplrr	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to b \in ℤ$
4		elznn0	$⊢ b \in ℤ \leftrightarrow (b \in ℝ \land (b \in ℕ_{0} \lor - b \in ℕ_{0}))$
5	3 4	sylib	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to (b \in ℝ \land (b \in ℕ_{0} \lor - b \in ℕ_{0}))$
6	5	simprd	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to (b \in ℕ_{0} \lor - b \in ℕ_{0})$
7		simplr	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \to A \in ℝ$
8	7	ad2antrr	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land b \in ℕ_{0}) \to A \in ℝ$
9		simprl	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \to a \in ℕ_{0}$
10	9	ad2antrr	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land b \in ℕ_{0}) \to a \in ℕ_{0}$
11		simpr	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land b \in ℕ_{0}) \to b \in ℕ_{0}$
12		simplr	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land b \in ℕ_{0}) \to (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)$
13		rsp2e	$⊢ (a \in ℕ_{0} \land b \in ℕ_{0} \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to \exists a \in ℕ_{0} \exists b \in ℕ_{0} (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)$
14	10 11 12 13	syl3anc	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land b \in ℕ_{0}) \to \exists a \in ℕ_{0} \exists b \in ℕ_{0} (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)$
15	8 14	jca	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land b \in ℕ_{0}) \to (A \in ℝ \land \exists a \in ℕ_{0} \exists b \in ℕ_{0} (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1))$
16	15	ex	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to (b \in ℕ_{0} \to (A \in ℝ \land \exists a \in ℕ_{0} \exists b \in ℕ_{0} (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)))$
17		elpell1qr	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to (A \in Pell1QR (D) \leftrightarrow (A \in ℝ \land \exists a \in ℕ_{0} \exists b \in ℕ_{0} (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)))$
18	17	ad4antr	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to (A \in Pell1QR (D) \leftrightarrow (A \in ℝ \land \exists a \in ℕ_{0} \exists b \in ℕ_{0} (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)))$
19	16 18	sylibrd	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to (b \in ℕ_{0} \to A \in Pell1QR (D))$
20	7	ad2antrr	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land - b \in ℕ_{0}) \to A \in ℝ$
21		pell14qrne0	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to A \neq 0$
22	21	ad4antr	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land - b \in ℕ_{0}) \to A \neq 0$
23	20 22	rereccld	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land - b \in ℕ_{0}) \to \frac{1}{A} \in ℝ$
24	9	ad2antrr	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land - b \in ℕ_{0}) \to a \in ℕ_{0}$
25		simpr	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land - b \in ℕ_{0}) \to - b \in ℕ_{0}$
26		pell14qrre	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to A \in ℝ$
27	26	recnd	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to A \in ℂ$
28	27 21	reccld	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to \frac{1}{A} \in ℂ$
29	28	ad3antrrr	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to \frac{1}{A} \in ℂ$
30		nn0cn	$⊢ a \in ℕ_{0} \to a \in ℂ$
31	30	ad2antrl	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \to a \in ℂ$
32		eldifi	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to D \in ℕ$
33	32	nncnd	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to D \in ℂ$
34	33	ad3antrrr	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \to D \in ℂ$
35	34	sqrtcld	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \to \sqrt{D} \in ℂ$
36		zcn	$⊢ b \in ℤ \to b \in ℂ$
37	36	ad2antll	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \to b \in ℂ$
38	37	negcld	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \to - b \in ℂ$
39	35 38	mulcld	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \to \sqrt{D} (- b) \in ℂ$
40	31 39	addcld	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \to a + \sqrt{D} (- b) \in ℂ$
41	40	adantr	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to a + \sqrt{D} (- b) \in ℂ$
42	27	ad3antrrr	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to A \in ℂ$
43	21	ad3antrrr	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to A \neq 0$
44	27 21	recidd	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to A (\frac{1}{A}) = 1$
45	44	ad3antrrr	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to A (\frac{1}{A}) = 1$
46		simprr	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to a^{2} - D b^{2} = 1$
47	45 46	eqtr4d	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to A (\frac{1}{A}) = a^{2} - D b^{2}$
48	31	adantr	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land A = a + \sqrt{D} b) \to a \in ℂ$
49	35 37	mulcld	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \to \sqrt{D} b \in ℂ$
50	49	adantr	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land A = a + \sqrt{D} b) \to \sqrt{D} b \in ℂ$
51		subsq	$⊢ (a \in ℂ \land \sqrt{D} b \in ℂ) \to a^{2} - {\sqrt{D} b}^{2} = (a + \sqrt{D} b) (a - \sqrt{D} b)$
52	48 50 51	syl2anc	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land A = a + \sqrt{D} b) \to a^{2} - {\sqrt{D} b}^{2} = (a + \sqrt{D} b) (a - \sqrt{D} b)$
53	35 37	sqmuld	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \to {\sqrt{D} b}^{2} = {\sqrt{D}}^{2} b^{2}$
54	34	sqsqrtd	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \to {\sqrt{D}}^{2} = D$
55	54	oveq1d	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \to {\sqrt{D}}^{2} b^{2} = D b^{2}$
56	53 55	eqtr2d	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \to D b^{2} = {\sqrt{D} b}^{2}$
57	56	oveq2d	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \to a^{2} - D b^{2} = a^{2} - {\sqrt{D} b}^{2}$
58	57	adantr	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land A = a + \sqrt{D} b) \to a^{2} - D b^{2} = a^{2} - {\sqrt{D} b}^{2}$
59		simpr	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land A = a + \sqrt{D} b) \to A = a + \sqrt{D} b$
60	35 37	mulneg2d	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \to \sqrt{D} (- b) = - \sqrt{D} b$
61	60	oveq2d	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \to a + \sqrt{D} (- b) = a + (- \sqrt{D} b)$
62		negsub	$⊢ (a \in ℂ \land \sqrt{D} b \in ℂ) \to a + (- \sqrt{D} b) = a - \sqrt{D} b$
63	62	eqcomd	$⊢ (a \in ℂ \land \sqrt{D} b \in ℂ) \to a - \sqrt{D} b = a + (- \sqrt{D} b)$
64	31 49 63	syl2anc	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \to a - \sqrt{D} b = a + (- \sqrt{D} b)$
65	61 64	eqtr4d	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \to a + \sqrt{D} (- b) = a - \sqrt{D} b$
66	65	adantr	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land A = a + \sqrt{D} b) \to a + \sqrt{D} (- b) = a - \sqrt{D} b$
67	59 66	oveq12d	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land A = a + \sqrt{D} b) \to A (a + \sqrt{D} (- b)) = (a + \sqrt{D} b) (a - \sqrt{D} b)$
68	52 58 67	3eqtr4d	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land A = a + \sqrt{D} b) \to a^{2} - D b^{2} = A (a + \sqrt{D} (- b))$
69	68	adantrr	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to a^{2} - D b^{2} = A (a + \sqrt{D} (- b))$
70	47 69	eqtrd	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \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))$
71	29 41 42 43 70	mulcanad	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to \frac{1}{A} = a + \sqrt{D} (- b)$
72	71	adantr	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land - b \in ℕ_{0}) \to \frac{1}{A} = a + \sqrt{D} (- b)$
73	37	ad2antrr	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land - b \in ℕ_{0}) \to b \in ℂ$
74		sqneg	$⊢ b \in ℂ \to {(- b)}^{2} = b^{2}$
75	73 74	syl	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land - b \in ℕ_{0}) \to {(- b)}^{2} = b^{2}$
76	75	oveq2d	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land - b \in ℕ_{0}) \to D {(- b)}^{2} = D b^{2}$
77	76	oveq2d	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land - b \in ℕ_{0}) \to a^{2} - D {(- b)}^{2} = a^{2} - D b^{2}$
78		simplrr	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land - b \in ℕ_{0}) \to a^{2} - D b^{2} = 1$
79	77 78	eqtrd	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land - b \in ℕ_{0}) \to a^{2} - D {(- b)}^{2} = 1$
80	72 79	jca	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land - b \in ℕ_{0}) \to (\frac{1}{A} = a + \sqrt{D} (- b) \land a^{2} - D {(- b)}^{2} = 1)$
81		oveq2	$⊢ c = - b \to \sqrt{D} c = \sqrt{D} (- b)$
82	81	oveq2d	$⊢ c = - b \to a + \sqrt{D} c = a + \sqrt{D} (- b)$
83	82	eqeq2d	$⊢ c = - b \to (\frac{1}{A} = a + \sqrt{D} c \leftrightarrow \frac{1}{A} = a + \sqrt{D} (- b))$
84		oveq1	$⊢ c = - b \to c^{2} = {(- b)}^{2}$
85	84	oveq2d	$⊢ c = - b \to D c^{2} = D {(- b)}^{2}$
86	85	oveq2d	$⊢ c = - b \to a^{2} - D c^{2} = a^{2} - D {(- b)}^{2}$
87	86	eqeq1d	$⊢ c = - b \to (a^{2} - D c^{2} = 1 \leftrightarrow a^{2} - D {(- b)}^{2} = 1)$
88	83 87	anbi12d	$⊢ c = - b \to ((\frac{1}{A} = a + \sqrt{D} c \land a^{2} - D c^{2} = 1) \leftrightarrow (\frac{1}{A} = a + \sqrt{D} (- b) \land a^{2} - D {(- b)}^{2} = 1))$
89	88	rspcev	$⊢ (- b \in ℕ_{0} \land (\frac{1}{A} = a + \sqrt{D} (- b) \land a^{2} - D {(- b)}^{2} = 1)) \to \exists c \in ℕ_{0} (\frac{1}{A} = a + \sqrt{D} c \land a^{2} - D c^{2} = 1)$
90	25 80 89	syl2anc	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land - b \in ℕ_{0}) \to \exists c \in ℕ_{0} (\frac{1}{A} = a + \sqrt{D} c \land a^{2} - D c^{2} = 1)$
91		rspe	$⊢ (a \in ℕ_{0} \land \exists c \in ℕ_{0} (\frac{1}{A} = a + \sqrt{D} c \land a^{2} - D c^{2} = 1)) \to \exists a \in ℕ_{0} \exists c \in ℕ_{0} (\frac{1}{A} = a + \sqrt{D} c \land a^{2} - D c^{2} = 1)$
92	24 90 91	syl2anc	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land - b \in ℕ_{0}) \to \exists a \in ℕ_{0} \exists c \in ℕ_{0} (\frac{1}{A} = a + \sqrt{D} c \land a^{2} - D c^{2} = 1)$
93	23 92	jca	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \land - b \in ℕ_{0}) \to (\frac{1}{A} \in ℝ \land \exists a \in ℕ_{0} \exists c \in ℕ_{0} (\frac{1}{A} = a + \sqrt{D} c \land a^{2} - D c^{2} = 1))$
94	93	ex	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to (- b \in ℕ_{0} \to (\frac{1}{A} \in ℝ \land \exists a \in ℕ_{0} \exists c \in ℕ_{0} (\frac{1}{A} = a + \sqrt{D} c \land a^{2} - D c^{2} = 1)))$
95		elpell1qr	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to (\frac{1}{A} \in Pell1QR (D) \leftrightarrow (\frac{1}{A} \in ℝ \land \exists a \in ℕ_{0} \exists c \in ℕ_{0} (\frac{1}{A} = a + \sqrt{D} c \land a^{2} - D c^{2} = 1)))$
96	95	ad4antr	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to (\frac{1}{A} \in Pell1QR (D) \leftrightarrow (\frac{1}{A} \in ℝ \land \exists a \in ℕ_{0} \exists c \in ℕ_{0} (\frac{1}{A} = a + \sqrt{D} c \land a^{2} - D c^{2} = 1)))$
97	94 96	sylibrd	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to (- b \in ℕ_{0} \to \frac{1}{A} \in Pell1QR (D))$
98	19 97	orim12d	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to ((b \in ℕ_{0} \lor - b \in ℕ_{0}) \to (A \in Pell1QR (D) \lor \frac{1}{A} \in Pell1QR (D)))$
99	6 98	mpd	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to (A \in Pell1QR (D) \lor \frac{1}{A} \in Pell1QR (D))$
100	99	ex	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \to ((A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1) \to (A \in Pell1QR (D) \lor \frac{1}{A} \in Pell1QR (D)))$
101	100	rexlimdvva	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land A \in ℝ) \to (\exists a \in ℕ_{0} \exists b \in ℤ (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1) \to (A \in Pell1QR (D) \lor \frac{1}{A} \in Pell1QR (D)))$
102	101	expimpd	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to ((A \in ℝ \land \exists a \in ℕ_{0} \exists b \in ℤ (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to (A \in Pell1QR (D) \lor \frac{1}{A} \in Pell1QR (D)))$
103	2 102	mpd	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to (A \in Pell1QR (D) \lor \frac{1}{A} \in Pell1QR (D))$

Metamath Proof Explorer

Theorem pell14qrdich

Proof