elpell1qr2

Description: The first quadrant solutions are precisely the positive Pell solutions which are at least one. (Contributed by Stefan O'Rear, 18-Sep-2014)

		Ref	Expression
	Assertion	elpell1qr2	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to (A \in Pell1QR (D) \leftrightarrow (A \in Pell14QR (D) \land 1 \leq A))$

Proof

Step	Hyp	Ref	Expression
1		pell1qrss14	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to Pell1QR (D) \subseteq Pell14QR (D)$
2	1	sselda	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1QR (D)) \to A \in Pell14QR (D)$
3		pell1qrge1	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1QR (D)) \to 1 \leq A$
4	2 3	jca	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1QR (D)) \to (A \in Pell14QR (D) \land 1 \leq A)$
5		1red	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to 1 \in ℝ$
6		pell14qrre	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to A \in ℝ$
7	5 6	leloed	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to (1 \leq A \leftrightarrow (1 < A \lor 1 = A))$
8	5 6	ltnled	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to (1 < A \leftrightarrow \neg A \leq 1)$
9	8	biimpa	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land 1 < A) \to \neg A \leq 1$
10		1div1e1	$⊢ \frac{1}{1} = 1$
11	10	eqcomi	$⊢ 1 = \frac{1}{1}$
12	11	a1i	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land 1 < A) \to 1 = \frac{1}{1}$
13	12	breq2d	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land 1 < A) \to (A \leq 1 \leftrightarrow A \leq \frac{1}{1})$
14	6	adantr	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land 1 < A) \to A \in ℝ$
15		pell14qrgt0	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to 0 < A$
16	15	adantr	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land 1 < A) \to 0 < A$
17		1red	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land 1 < A) \to 1 \in ℝ$
18		0lt1	$⊢ 0 < 1$
19	18	a1i	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land 1 < A) \to 0 < 1$
20		lerec2	$⊢ ((A \in ℝ \land 0 < A) \land (1 \in ℝ \land 0 < 1)) \to (A \leq \frac{1}{1} \leftrightarrow 1 \leq \frac{1}{A})$
21	14 16 17 19 20	syl22anc	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land 1 < A) \to (A \leq \frac{1}{1} \leftrightarrow 1 \leq \frac{1}{A})$
22	13 21	bitrd	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land 1 < A) \to (A \leq 1 \leftrightarrow 1 \leq \frac{1}{A})$
23	9 22	mtbid	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land 1 < A) \to \neg 1 \leq \frac{1}{A}$
24		simplll	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land 1 < A) \land \frac{1}{A} \in Pell1QR (D)) \to D \in (ℕ ∖ ◻_{ℕ})$
25		pell1qrge1	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land \frac{1}{A} \in Pell1QR (D)) \to 1 \leq \frac{1}{A}$
26	24 25	sylancom	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land 1 < A) \land \frac{1}{A} \in Pell1QR (D)) \to 1 \leq \frac{1}{A}$
27	23 26	mtand	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land 1 < A) \to \neg \frac{1}{A} \in Pell1QR (D)$
28		pell14qrdich	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to (A \in Pell1QR (D) \lor \frac{1}{A} \in Pell1QR (D))$
29	28	adantr	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land 1 < A) \to (A \in Pell1QR (D) \lor \frac{1}{A} \in Pell1QR (D))$
30		orel2	$⊢ \neg \frac{1}{A} \in Pell1QR (D) \to ((A \in Pell1QR (D) \lor \frac{1}{A} \in Pell1QR (D)) \to A \in Pell1QR (D))$
31	27 29 30	sylc	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land 1 < A) \to A \in Pell1QR (D)$
32		simpr	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land 1 = A) \to 1 = A$
33		pell1qr1	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to 1 \in Pell1QR (D)$
34	33	ad2antrr	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land 1 = A) \to 1 \in Pell1QR (D)$
35	32 34	eqeltrrd	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land 1 = A) \to A \in Pell1QR (D)$
36	31 35	jaodan	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land (1 < A \lor 1 = A)) \to A \in Pell1QR (D)$
37	36	ex	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to ((1 < A \lor 1 = A) \to A \in Pell1QR (D))$
38	7 37	sylbid	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to (1 \leq A \to A \in Pell1QR (D))$
39	38	impr	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land (A \in Pell14QR (D) \land 1 \leq A)) \to A \in Pell1QR (D)$
40	4 39	impbida	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to (A \in Pell1QR (D) \leftrightarrow (A \in Pell14QR (D) \land 1 \leq A))$

Metamath Proof Explorer

Theorem elpell1qr2

Proof