pellexlem3

Description: Lemma for pellex . To each good rational approximation of ( sqrtD ) , there exists a near-solution. (Contributed by Stefan O'Rear, 14-Sep-2014)

		Ref	Expression
	Assertion	pellexlem3	$⊢ (D \in ℕ \land \neg \sqrt{D} \in ℚ) \to \{x \in ℚ \| (0 < x \land \|x - \sqrt{D}\| < {denom (x)}^{- 2})\} ≼ \{⟨y, z⟩ \| ((y \in ℕ \land z \in ℕ) \land (y^{2} - D z^{2} \neq 0 \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D}))\}$

Proof

Step	Hyp	Ref	Expression
1		nnex	$⊢ ℕ \in V$
2	1 1	xpex	$⊢ ℕ \times ℕ \in V$
3		opabssxp	$⊢ \{⟨y, z⟩ \| ((y \in ℕ \land z \in ℕ) \land (y^{2} - D z^{2} \neq 0 \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D}))\} \subseteq ℕ \times ℕ$
4	2 3	ssexi	$⊢ \{⟨y, z⟩ \| ((y \in ℕ \land z \in ℕ) \land (y^{2} - D z^{2} \neq 0 \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D}))\} \in V$
5		simprl	$⊢ ((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land (a \in ℚ \land (0 < a \land \|a - \sqrt{D}\| < {denom (a)}^{- 2}))) \to a \in ℚ$
6		simprrl	$⊢ ((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land (a \in ℚ \land (0 < a \land \|a - \sqrt{D}\| < {denom (a)}^{- 2}))) \to 0 < a$
7		qgt0numnn	$⊢ (a \in ℚ \land 0 < a) \to numer (a) \in ℕ$
8	5 6 7	syl2anc	$⊢ ((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land (a \in ℚ \land (0 < a \land \|a - \sqrt{D}\| < {denom (a)}^{- 2}))) \to numer (a) \in ℕ$
9		qdencl	$⊢ a \in ℚ \to denom (a) \in ℕ$
10	5 9	syl	$⊢ ((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land (a \in ℚ \land (0 < a \land \|a - \sqrt{D}\| < {denom (a)}^{- 2}))) \to denom (a) \in ℕ$
11	8 10	jca	$⊢ ((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land (a \in ℚ \land (0 < a \land \|a - \sqrt{D}\| < {denom (a)}^{- 2}))) \to (numer (a) \in ℕ \land denom (a) \in ℕ)$
12		simpll	$⊢ ((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land (a \in ℚ \land (0 < a \land \|a - \sqrt{D}\| < {denom (a)}^{- 2}))) \to D \in ℕ$
13		simplr	$⊢ ((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land (a \in ℚ \land (0 < a \land \|a - \sqrt{D}\| < {denom (a)}^{- 2}))) \to \neg \sqrt{D} \in ℚ$
14		pellexlem1	$⊢ ((D \in ℕ \land numer (a) \in ℕ \land denom (a) \in ℕ) \land \neg \sqrt{D} \in ℚ) \to {numer (a)}^{2} - D {denom (a)}^{2} \neq 0$
15	12 8 10 13 14	syl31anc	$⊢ ((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land (a \in ℚ \land (0 < a \land \|a - \sqrt{D}\| < {denom (a)}^{- 2}))) \to {numer (a)}^{2} - D {denom (a)}^{2} \neq 0$
16		simprrr	$⊢ ((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land (a \in ℚ \land (0 < a \land \|a - \sqrt{D}\| < {denom (a)}^{- 2}))) \to \|a - \sqrt{D}\| < {denom (a)}^{- 2}$
17		qeqnumdivden	$⊢ a \in ℚ \to a = \frac{numer (a)}{denom (a)}$
18	17	oveq1d	$⊢ a \in ℚ \to a - \sqrt{D} = (\frac{numer (a)}{denom (a)}) - \sqrt{D}$
19	18	fveq2d	$⊢ a \in ℚ \to \|a - \sqrt{D}\| = \|(\frac{numer (a)}{denom (a)}) - \sqrt{D}\|$
20	19	breq1d	$⊢ a \in ℚ \to (\|a - \sqrt{D}\| < {denom (a)}^{- 2} \leftrightarrow \|(\frac{numer (a)}{denom (a)}) - \sqrt{D}\| < {denom (a)}^{- 2})$
21	5 20	syl	$⊢ ((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land (a \in ℚ \land (0 < a \land \|a - \sqrt{D}\| < {denom (a)}^{- 2}))) \to (\|a - \sqrt{D}\| < {denom (a)}^{- 2} \leftrightarrow \|(\frac{numer (a)}{denom (a)}) - \sqrt{D}\| < {denom (a)}^{- 2})$
22	16 21	mpbid	$⊢ ((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land (a \in ℚ \land (0 < a \land \|a - \sqrt{D}\| < {denom (a)}^{- 2}))) \to \|(\frac{numer (a)}{denom (a)}) - \sqrt{D}\| < {denom (a)}^{- 2}$
23		pellexlem2	$⊢ ((D \in ℕ \land numer (a) \in ℕ \land denom (a) \in ℕ) \land \|(\frac{numer (a)}{denom (a)}) - \sqrt{D}\| < {denom (a)}^{- 2}) \to \|{numer (a)}^{2} - D {denom (a)}^{2}\| < 1 + 2 \sqrt{D}$
24	12 8 10 22 23	syl31anc	$⊢ ((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land (a \in ℚ \land (0 < a \land \|a - \sqrt{D}\| < {denom (a)}^{- 2}))) \to \|{numer (a)}^{2} - D {denom (a)}^{2}\| < 1 + 2 \sqrt{D}$
25	11 15 24	jca32	$⊢ ((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land (a \in ℚ \land (0 < a \land \|a - \sqrt{D}\| < {denom (a)}^{- 2}))) \to ((numer (a) \in ℕ \land denom (a) \in ℕ) \land ({numer (a)}^{2} - D {denom (a)}^{2} \neq 0 \land \|{numer (a)}^{2} - D {denom (a)}^{2}\| < 1 + 2 \sqrt{D}))$
26	25	ex	$⊢ (D \in ℕ \land \neg \sqrt{D} \in ℚ) \to ((a \in ℚ \land (0 < a \land \|a - \sqrt{D}\| < {denom (a)}^{- 2})) \to ((numer (a) \in ℕ \land denom (a) \in ℕ) \land ({numer (a)}^{2} - D {denom (a)}^{2} \neq 0 \land \|{numer (a)}^{2} - D {denom (a)}^{2}\| < 1 + 2 \sqrt{D})))$
27		breq2	$⊢ x = a \to (0 < x \leftrightarrow 0 < a)$
28		fvoveq1	$⊢ x = a \to \|x - \sqrt{D}\| = \|a - \sqrt{D}\|$
29		fveq2	$⊢ x = a \to denom (x) = denom (a)$
30	29	oveq1d	$⊢ x = a \to {denom (x)}^{- 2} = {denom (a)}^{- 2}$
31	28 30	breq12d	$⊢ x = a \to (\|x - \sqrt{D}\| < {denom (x)}^{- 2} \leftrightarrow \|a - \sqrt{D}\| < {denom (a)}^{- 2})$
32	27 31	anbi12d	$⊢ x = a \to ((0 < x \land \|x - \sqrt{D}\| < {denom (x)}^{- 2}) \leftrightarrow (0 < a \land \|a - \sqrt{D}\| < {denom (a)}^{- 2}))$
33	32	elrab	$⊢ a \in \{x \in ℚ \| (0 < x \land \|x - \sqrt{D}\| < {denom (x)}^{- 2})\} \leftrightarrow (a \in ℚ \land (0 < a \land \|a - \sqrt{D}\| < {denom (a)}^{- 2}))$
34		fvex	$⊢ numer (a) \in V$
35		fvex	$⊢ denom (a) \in V$
36		eleq1	$⊢ y = numer (a) \to (y \in ℕ \leftrightarrow numer (a) \in ℕ)$
37	36	anbi1d	$⊢ y = numer (a) \to ((y \in ℕ \land z \in ℕ) \leftrightarrow (numer (a) \in ℕ \land z \in ℕ))$
38		oveq1	$⊢ y = numer (a) \to y^{2} = {numer (a)}^{2}$
39	38	oveq1d	$⊢ y = numer (a) \to y^{2} - D z^{2} = {numer (a)}^{2} - D z^{2}$
40	39	neeq1d	$⊢ y = numer (a) \to (y^{2} - D z^{2} \neq 0 \leftrightarrow {numer (a)}^{2} - D z^{2} \neq 0)$
41	39	fveq2d	$⊢ y = numer (a) \to \|y^{2} - D z^{2}\| = \|{numer (a)}^{2} - D z^{2}\|$
42	41	breq1d	$⊢ y = numer (a) \to (\|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D} \leftrightarrow \|{numer (a)}^{2} - D z^{2}\| < 1 + 2 \sqrt{D})$
43	40 42	anbi12d	$⊢ y = numer (a) \to ((y^{2} - D z^{2} \neq 0 \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D}) \leftrightarrow ({numer (a)}^{2} - D z^{2} \neq 0 \land \|{numer (a)}^{2} - D z^{2}\| < 1 + 2 \sqrt{D}))$
44	37 43	anbi12d	$⊢ y = numer (a) \to (((y \in ℕ \land z \in ℕ) \land (y^{2} - D z^{2} \neq 0 \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D})) \leftrightarrow ((numer (a) \in ℕ \land z \in ℕ) \land ({numer (a)}^{2} - D z^{2} \neq 0 \land \|{numer (a)}^{2} - D z^{2}\| < 1 + 2 \sqrt{D})))$
45		eleq1	$⊢ z = denom (a) \to (z \in ℕ \leftrightarrow denom (a) \in ℕ)$
46	45	anbi2d	$⊢ z = denom (a) \to ((numer (a) \in ℕ \land z \in ℕ) \leftrightarrow (numer (a) \in ℕ \land denom (a) \in ℕ))$
47		oveq1	$⊢ z = denom (a) \to z^{2} = {denom (a)}^{2}$
48	47	oveq2d	$⊢ z = denom (a) \to D z^{2} = D {denom (a)}^{2}$
49	48	oveq2d	$⊢ z = denom (a) \to {numer (a)}^{2} - D z^{2} = {numer (a)}^{2} - D {denom (a)}^{2}$
50	49	neeq1d	$⊢ z = denom (a) \to ({numer (a)}^{2} - D z^{2} \neq 0 \leftrightarrow {numer (a)}^{2} - D {denom (a)}^{2} \neq 0)$
51	49	fveq2d	$⊢ z = denom (a) \to \|{numer (a)}^{2} - D z^{2}\| = \|{numer (a)}^{2} - D {denom (a)}^{2}\|$
52	51	breq1d	$⊢ z = denom (a) \to (\|{numer (a)}^{2} - D z^{2}\| < 1 + 2 \sqrt{D} \leftrightarrow \|{numer (a)}^{2} - D {denom (a)}^{2}\| < 1 + 2 \sqrt{D})$
53	50 52	anbi12d	$⊢ z = denom (a) \to (({numer (a)}^{2} - D z^{2} \neq 0 \land \|{numer (a)}^{2} - D z^{2}\| < 1 + 2 \sqrt{D}) \leftrightarrow ({numer (a)}^{2} - D {denom (a)}^{2} \neq 0 \land \|{numer (a)}^{2} - D {denom (a)}^{2}\| < 1 + 2 \sqrt{D}))$
54	46 53	anbi12d	$⊢ z = denom (a) \to (((numer (a) \in ℕ \land z \in ℕ) \land ({numer (a)}^{2} - D z^{2} \neq 0 \land \|{numer (a)}^{2} - D z^{2}\| < 1 + 2 \sqrt{D})) \leftrightarrow ((numer (a) \in ℕ \land denom (a) \in ℕ) \land ({numer (a)}^{2} - D {denom (a)}^{2} \neq 0 \land \|{numer (a)}^{2} - D {denom (a)}^{2}\| < 1 + 2 \sqrt{D})))$
55	34 35 44 54	opelopab	$⊢ ⟨numer (a), denom (a)⟩ \in \{⟨y, z⟩ \| ((y \in ℕ \land z \in ℕ) \land (y^{2} - D z^{2} \neq 0 \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D}))\} \leftrightarrow ((numer (a) \in ℕ \land denom (a) \in ℕ) \land ({numer (a)}^{2} - D {denom (a)}^{2} \neq 0 \land \|{numer (a)}^{2} - D {denom (a)}^{2}\| < 1 + 2 \sqrt{D}))$
56	26 33 55	3imtr4g	$⊢ (D \in ℕ \land \neg \sqrt{D} \in ℚ) \to (a \in \{x \in ℚ \| (0 < x \land \|x - \sqrt{D}\| < {denom (x)}^{- 2})\} \to ⟨numer (a), denom (a)⟩ \in \{⟨y, z⟩ \| ((y \in ℕ \land z \in ℕ) \land (y^{2} - D z^{2} \neq 0 \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D}))\})$
57		ssrab2	$⊢ \{x \in ℚ \| (0 < x \land \|x - \sqrt{D}\| < {denom (x)}^{- 2})\} \subseteq ℚ$
58		simprl	$⊢ ((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land (a \in \{x \in ℚ \| (0 < x \land \|x - \sqrt{D}\| < {denom (x)}^{- 2})\} \land b \in \{x \in ℚ \| (0 < x \land \|x - \sqrt{D}\| < {denom (x)}^{- 2})\})) \to a \in \{x \in ℚ \| (0 < x \land \|x - \sqrt{D}\| < {denom (x)}^{- 2})\}$
59	57 58	sselid	$⊢ ((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land (a \in \{x \in ℚ \| (0 < x \land \|x - \sqrt{D}\| < {denom (x)}^{- 2})\} \land b \in \{x \in ℚ \| (0 < x \land \|x - \sqrt{D}\| < {denom (x)}^{- 2})\})) \to a \in ℚ$
60		simprr	$⊢ ((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land (a \in \{x \in ℚ \| (0 < x \land \|x - \sqrt{D}\| < {denom (x)}^{- 2})\} \land b \in \{x \in ℚ \| (0 < x \land \|x - \sqrt{D}\| < {denom (x)}^{- 2})\})) \to b \in \{x \in ℚ \| (0 < x \land \|x - \sqrt{D}\| < {denom (x)}^{- 2})\}$
61	57 60	sselid	$⊢ ((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land (a \in \{x \in ℚ \| (0 < x \land \|x - \sqrt{D}\| < {denom (x)}^{- 2})\} \land b \in \{x \in ℚ \| (0 < x \land \|x - \sqrt{D}\| < {denom (x)}^{- 2})\})) \to b \in ℚ$
62	34 35	opth	$⊢ ⟨numer (a), denom (a)⟩ = ⟨numer (b), denom (b)⟩ \leftrightarrow (numer (a) = numer (b) \land denom (a) = denom (b))$
63		simprl	$⊢ ((a \in ℚ \land b \in ℚ) \land (numer (a) = numer (b) \land denom (a) = denom (b))) \to numer (a) = numer (b)$
64		simprr	$⊢ ((a \in ℚ \land b \in ℚ) \land (numer (a) = numer (b) \land denom (a) = denom (b))) \to denom (a) = denom (b)$
65	63 64	oveq12d	$⊢ ((a \in ℚ \land b \in ℚ) \land (numer (a) = numer (b) \land denom (a) = denom (b))) \to \frac{numer (a)}{denom (a)} = \frac{numer (b)}{denom (b)}$
66		simpll	$⊢ ((a \in ℚ \land b \in ℚ) \land (numer (a) = numer (b) \land denom (a) = denom (b))) \to a \in ℚ$
67	66 17	syl	$⊢ ((a \in ℚ \land b \in ℚ) \land (numer (a) = numer (b) \land denom (a) = denom (b))) \to a = \frac{numer (a)}{denom (a)}$
68		simplr	$⊢ ((a \in ℚ \land b \in ℚ) \land (numer (a) = numer (b) \land denom (a) = denom (b))) \to b \in ℚ$
69		qeqnumdivden	$⊢ b \in ℚ \to b = \frac{numer (b)}{denom (b)}$
70	68 69	syl	$⊢ ((a \in ℚ \land b \in ℚ) \land (numer (a) = numer (b) \land denom (a) = denom (b))) \to b = \frac{numer (b)}{denom (b)}$
71	65 67 70	3eqtr4d	$⊢ ((a \in ℚ \land b \in ℚ) \land (numer (a) = numer (b) \land denom (a) = denom (b))) \to a = b$
72	71	ex	$⊢ (a \in ℚ \land b \in ℚ) \to ((numer (a) = numer (b) \land denom (a) = denom (b)) \to a = b)$
73	62 72	syl5bi	$⊢ (a \in ℚ \land b \in ℚ) \to (⟨numer (a), denom (a)⟩ = ⟨numer (b), denom (b)⟩ \to a = b)$
74		fveq2	$⊢ a = b \to numer (a) = numer (b)$
75		fveq2	$⊢ a = b \to denom (a) = denom (b)$
76	74 75	opeq12d	$⊢ a = b \to ⟨numer (a), denom (a)⟩ = ⟨numer (b), denom (b)⟩$
77	73 76	impbid1	$⊢ (a \in ℚ \land b \in ℚ) \to (⟨numer (a), denom (a)⟩ = ⟨numer (b), denom (b)⟩ \leftrightarrow a = b)$
78	59 61 77	syl2anc	$⊢ ((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land (a \in \{x \in ℚ \| (0 < x \land \|x - \sqrt{D}\| < {denom (x)}^{- 2})\} \land b \in \{x \in ℚ \| (0 < x \land \|x - \sqrt{D}\| < {denom (x)}^{- 2})\})) \to (⟨numer (a), denom (a)⟩ = ⟨numer (b), denom (b)⟩ \leftrightarrow a = b)$
79	78	ex	$⊢ (D \in ℕ \land \neg \sqrt{D} \in ℚ) \to ((a \in \{x \in ℚ \| (0 < x \land \|x - \sqrt{D}\| < {denom (x)}^{- 2})\} \land b \in \{x \in ℚ \| (0 < x \land \|x - \sqrt{D}\| < {denom (x)}^{- 2})\}) \to (⟨numer (a), denom (a)⟩ = ⟨numer (b), denom (b)⟩ \leftrightarrow a = b))$
80	56 79	dom2d	$⊢ (D \in ℕ \land \neg \sqrt{D} \in ℚ) \to (\{⟨y, z⟩ \| ((y \in ℕ \land z \in ℕ) \land (y^{2} - D z^{2} \neq 0 \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D}))\} \in V \to \{x \in ℚ \| (0 < x \land \|x - \sqrt{D}\| < {denom (x)}^{- 2})\} ≼ \{⟨y, z⟩ \| ((y \in ℕ \land z \in ℕ) \land (y^{2} - D z^{2} \neq 0 \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D}))\})$
81	4 80	mpi	$⊢ (D \in ℕ \land \neg \sqrt{D} \in ℚ) \to \{x \in ℚ \| (0 < x \land \|x - \sqrt{D}\| < {denom (x)}^{- 2})\} ≼ \{⟨y, z⟩ \| ((y \in ℕ \land z \in ℕ) \land (y^{2} - D z^{2} \neq 0 \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D}))\}$

Metamath Proof Explorer

Theorem pellexlem3

Proof