Metamath Proof Explorer

Theorem pell1qrgap

Description: First-quadrant Pell solutions are bounded away from 1. (This particular bound allows to prove exact values for the fundamental solution later.) (Contributed by Stefan O'Rear, 18-Sep-2014)

		Ref	Expression
	Assertion	pell1qrgap	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1QR (D) \land 1 < A) \to \sqrt{D + 1} + \sqrt{D} \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	1	adantr	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land 1 < A) \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)))$
3		eldifi	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to D \in ℕ$
4	3	ad4antr	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land 1 < A) \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 D \in ℕ$
5		simplr	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land 1 < A) \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 \in ℕ_{0} \land b \in ℕ_{0})$
6		simp-4r	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land 1 < A) \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 < A$
7		simprl	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land 1 < A) \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$
8	6 7	breqtrd	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land 1 < A) \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 < a + \sqrt{D} b$
9		simprr	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land 1 < A) \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^{2} - D b^{2} = 1$
10		pell1qrgaplem	$⊢ ((D \in ℕ \land (a \in ℕ_{0} \land b \in ℕ_{0})) \land (1 < a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to \sqrt{D + 1} + \sqrt{D} \leq a + \sqrt{D} b$
11	4 5 8 9 10	syl22anc	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land 1 < A) \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 \sqrt{D + 1} + \sqrt{D} \leq a + \sqrt{D} b$
12	11 7	breqtrrd	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land 1 < A) \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 \sqrt{D + 1} + \sqrt{D} \leq A$
13	12	ex	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land 1 < A) \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 \sqrt{D + 1} + \sqrt{D} \leq A)$
14	13	rexlimdvva	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land 1 < A) \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 \sqrt{D + 1} + \sqrt{D} \leq A)$
15	14	expimpd	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land 1 < A) \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 \sqrt{D + 1} + \sqrt{D} \leq A)$
16	2 15	sylbid	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land 1 < A) \to (A \in Pell1QR (D) \to \sqrt{D + 1} + \sqrt{D} \leq A)$
17	16	ex	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to (1 < A \to (A \in Pell1QR (D) \to \sqrt{D + 1} + \sqrt{D} \leq A))$
18	17	com23	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to (A \in Pell1QR (D) \to (1 < A \to \sqrt{D + 1} + \sqrt{D} \leq A))$
19	18	3imp	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1QR (D) \land 1 < A) \to \sqrt{D + 1} + \sqrt{D} \leq A$