pell1qrge1

Description: A Pell solution in the first quadrant is at least 1. (Contributed by Stefan O'Rear, 17-Sep-2014)

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

Proof

Step	Hyp	Ref	Expression
1		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)))$
2		1red	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \land a^{2} - D b^{2} = 1) \to 1 \in ℝ$
3		simplrl	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \land a^{2} - D b^{2} = 1) \to a \in ℕ_{0}$
4	3	nn0red	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \land a^{2} - D b^{2} = 1) \to a \in ℝ$
5		eldifi	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to D \in ℕ$
6	5	ad3antrrr	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \land a^{2} - D b^{2} = 1) \to D \in ℕ$
7	6	nnnn0d	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \land a^{2} - D b^{2} = 1) \to D \in ℕ_{0}$
8	7	nn0red	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \land a^{2} - D b^{2} = 1) \to D \in ℝ$
9	7	nn0ge0d	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \land a^{2} - D b^{2} = 1) \to 0 \leq D$
10	8 9	resqrtcld	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \land a^{2} - D b^{2} = 1) \to \sqrt{D} \in ℝ$
11		simplrr	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \land a^{2} - D b^{2} = 1) \to b \in ℕ_{0}$
12	11	nn0red	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \land a^{2} - D b^{2} = 1) \to b \in ℝ$
13	10 12	remulcld	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \land a^{2} - D b^{2} = 1) \to \sqrt{D} b \in ℝ$
14	4 13	readdcld	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \land a^{2} - D b^{2} = 1) \to a + \sqrt{D} b \in ℝ$
15		2nn0	$⊢ 2 \in ℕ_{0}$
16	15	a1i	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \land a^{2} - D b^{2} = 1) \to 2 \in ℕ_{0}$
17	11 16	nn0expcld	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \land a^{2} - D b^{2} = 1) \to b^{2} \in ℕ_{0}$
18	7 17	nn0mulcld	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \land a^{2} - D b^{2} = 1) \to D b^{2} \in ℕ_{0}$
19	18	nn0ge0d	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \land a^{2} - D b^{2} = 1) \to 0 \leq D b^{2}$
20	18	nn0red	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \land a^{2} - D b^{2} = 1) \to D b^{2} \in ℝ$
21	2 20	addge02d	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \land a^{2} - D b^{2} = 1) \to (0 \leq D b^{2} \leftrightarrow 1 \leq D b^{2} + 1)$
22	19 21	mpbid	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \land a^{2} - D b^{2} = 1) \to 1 \leq D b^{2} + 1$
23		sq1	$⊢ 1^{2} = 1$
24	23	a1i	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \land a^{2} - D b^{2} = 1) \to 1^{2} = 1$
25		nn0cn	$⊢ a \in ℕ_{0} \to a \in ℂ$
26	25	ad2antrl	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \to a \in ℂ$
27	26	sqcld	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \to a^{2} \in ℂ$
28	5	ad2antrr	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \to D \in ℕ$
29	28	nncnd	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \to D \in ℂ$
30		nn0cn	$⊢ b \in ℕ_{0} \to b \in ℂ$
31	30	ad2antll	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \to b \in ℂ$
32	31	sqcld	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \to b^{2} \in ℂ$
33	29 32	mulcld	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \to D b^{2} \in ℂ$
34		1cnd	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \to 1 \in ℂ$
35	27 33 34	subaddd	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \to (a^{2} - D b^{2} = 1 \leftrightarrow D b^{2} + 1 = a^{2})$
36	35	biimpa	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \land a^{2} - D b^{2} = 1) \to D b^{2} + 1 = a^{2}$
37	36	eqcomd	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \land a^{2} - D b^{2} = 1) \to a^{2} = D b^{2} + 1$
38	22 24 37	3brtr4d	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \land a^{2} - D b^{2} = 1) \to 1^{2} \leq a^{2}$
39		0le1	$⊢ 0 \leq 1$
40	39	a1i	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \land a^{2} - D b^{2} = 1) \to 0 \leq 1$
41	3	nn0ge0d	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \land a^{2} - D b^{2} = 1) \to 0 \leq a$
42	2 4 40 41	le2sqd	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \land a^{2} - D b^{2} = 1) \to (1 \leq a \leftrightarrow 1^{2} \leq a^{2})$
43	38 42	mpbird	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \land a^{2} - D b^{2} = 1) \to 1 \leq a$
44	8 9	sqrtge0d	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \land a^{2} - D b^{2} = 1) \to 0 \leq \sqrt{D}$
45	11	nn0ge0d	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \land a^{2} - D b^{2} = 1) \to 0 \leq b$
46	10 12 44 45	mulge0d	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \land a^{2} - D b^{2} = 1) \to 0 \leq \sqrt{D} b$
47	4 13	addge01d	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \land a^{2} - D b^{2} = 1) \to (0 \leq \sqrt{D} b \leftrightarrow a \leq a + \sqrt{D} b)$
48	46 47	mpbid	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \land a^{2} - D b^{2} = 1) \to a \leq a + \sqrt{D} b$
49	2 4 14 43 48	letrd	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \land a^{2} - D b^{2} = 1) \to 1 \leq a + \sqrt{D} b$
50	49	adantrl	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to 1 \leq a + \sqrt{D} b$
51		simprl	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to A = a + \sqrt{D} b$
52	50 51	breqtrrd	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to 1 \leq A$
53	52	ex	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \to ((A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1) \to 1 \leq A)$
54	53	rexlimdvva	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \to (\exists a \in ℕ_{0} \exists b \in ℕ_{0} (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1) \to 1 \leq A)$
55	54	expimpd	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to ((A \in ℝ \land \exists a \in ℕ_{0} \exists b \in ℕ_{0} (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to 1 \leq A)$
56	1 55	sylbid	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to (A \in Pell1QR (D) \to 1 \leq A)$
57	56	imp	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1QR (D)) \to 1 \leq A$

Metamath Proof Explorer

Theorem pell1qrge1

Proof