pell14qrgapw

Description: Positive Pell solutions are bounded away from 1, with a friendlier bound. (Contributed by Stefan O'Rear, 18-Sep-2014)

		Ref	Expression
	Assertion	pell14qrgapw	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D) \land 1 < A) \to 2 < A$

Proof

Step	Hyp	Ref	Expression
1		2re	$⊢ 2 \in ℝ$
2	1	a1i	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D) \land 1 < A) \to 2 \in ℝ$
3		eldifi	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to D \in ℕ$
4	3	3ad2ant1	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D) \land 1 < A) \to D \in ℕ$
5	4	nnrpd	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D) \land 1 < A) \to D \in ℝ^{+}$
6		1rp	$⊢ 1 \in ℝ^{+}$
7	6	a1i	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D) \land 1 < A) \to 1 \in ℝ^{+}$
8	5 7	rpaddcld	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D) \land 1 < A) \to D + 1 \in ℝ^{+}$
9	8	rpsqrtcld	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D) \land 1 < A) \to \sqrt{D + 1} \in ℝ^{+}$
10	9	rpred	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D) \land 1 < A) \to \sqrt{D + 1} \in ℝ$
11	5	rpsqrtcld	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D) \land 1 < A) \to \sqrt{D} \in ℝ^{+}$
12	11	rpred	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D) \land 1 < A) \to \sqrt{D} \in ℝ$
13	10 12	readdcld	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D) \land 1 < A) \to \sqrt{D + 1} + \sqrt{D} \in ℝ$
14		pell14qrre	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to A \in ℝ$
15	14	3adant3	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D) \land 1 < A) \to A \in ℝ$
16		df-2	$⊢ 2 = 1 + 1$
17		1red	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D) \land 1 < A) \to 1 \in ℝ$
18	4	nnred	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D) \land 1 < A) \to D \in ℝ$
19		peano2re	$⊢ D \in ℝ \to D + 1 \in ℝ$
20	18 19	syl	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D) \land 1 < A) \to D + 1 \in ℝ$
21	4	nnge1d	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D) \land 1 < A) \to 1 \leq D$
22	18	ltp1d	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D) \land 1 < A) \to D < D + 1$
23	17 18 20 21 22	lelttrd	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D) \land 1 < A) \to 1 < D + 1$
24		sq1	$⊢ 1^{2} = 1$
25	24	a1i	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D) \land 1 < A) \to 1^{2} = 1$
26	4	nncnd	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D) \land 1 < A) \to D \in ℂ$
27		peano2cn	$⊢ D \in ℂ \to D + 1 \in ℂ$
28	26 27	syl	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D) \land 1 < A) \to D + 1 \in ℂ$
29	28	sqsqrtd	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D) \land 1 < A) \to {\sqrt{D + 1}}^{2} = D + 1$
30	23 25 29	3brtr4d	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D) \land 1 < A) \to 1^{2} < {\sqrt{D + 1}}^{2}$
31		0le1	$⊢ 0 \leq 1$
32	31	a1i	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D) \land 1 < A) \to 0 \leq 1$
33	9	rpge0d	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D) \land 1 < A) \to 0 \leq \sqrt{D + 1}$
34	17 10 32 33	lt2sqd	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D) \land 1 < A) \to (1 < \sqrt{D + 1} \leftrightarrow 1^{2} < {\sqrt{D + 1}}^{2})$
35	30 34	mpbird	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D) \land 1 < A) \to 1 < \sqrt{D + 1}$
36	26	sqsqrtd	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D) \land 1 < A) \to {\sqrt{D}}^{2} = D$
37	21 25 36	3brtr4d	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D) \land 1 < A) \to 1^{2} \leq {\sqrt{D}}^{2}$
38	11	rpge0d	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D) \land 1 < A) \to 0 \leq \sqrt{D}$
39	17 12 32 38	le2sqd	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D) \land 1 < A) \to (1 \leq \sqrt{D} \leftrightarrow 1^{2} \leq {\sqrt{D}}^{2})$
40	37 39	mpbird	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D) \land 1 < A) \to 1 \leq \sqrt{D}$
41	17 17 10 12 35 40	ltleaddd	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D) \land 1 < A) \to 1 + 1 < \sqrt{D + 1} + \sqrt{D}$
42	16 41	eqbrtrid	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D) \land 1 < A) \to 2 < \sqrt{D + 1} + \sqrt{D}$
43		pell14qrgap	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D) \land 1 < A) \to \sqrt{D + 1} + \sqrt{D} \leq A$
44	2 13 15 42 43	ltletrd	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D) \land 1 < A) \to 2 < A$

Metamath Proof Explorer

Theorem pell14qrgapw

Proof