pellqrex

Description: There is a nontrivial solution of a Pell equation in the first quadrant. (Contributed by Stefan O'Rear, 18-Sep-2014)

		Ref	Expression
	Assertion	pellqrex	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to \exists x \in Pell1QR (D) 1 < x$

Proof

Step	Hyp	Ref	Expression
1		eldifi	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to D \in ℕ$
2		eldifn	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to \neg D \in ◻_{ℕ}$
3	1	anim1i	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land \sqrt{D} \in ℚ) \to (D \in ℕ \land \sqrt{D} \in ℚ)$
4		fveq2	$⊢ a = D \to \sqrt{a} = \sqrt{D}$
5	4	eleq1d	$⊢ a = D \to (\sqrt{a} \in ℚ \leftrightarrow \sqrt{D} \in ℚ)$
6		df-squarenn	$⊢ ◻_{ℕ} = \{a \in ℕ \| \sqrt{a} \in ℚ\}$
7	5 6	elrab2	$⊢ D \in ◻_{ℕ} \leftrightarrow (D \in ℕ \land \sqrt{D} \in ℚ)$
8	3 7	sylibr	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land \sqrt{D} \in ℚ) \to D \in ◻_{ℕ}$
9	2 8	mtand	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to \neg \sqrt{D} \in ℚ$
10		pellex	$⊢ (D \in ℕ \land \neg \sqrt{D} \in ℚ) \to \exists c \in ℕ \exists d \in ℕ c^{2} - D d^{2} = 1$
11	1 9 10	syl2anc	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to \exists c \in ℕ \exists d \in ℕ c^{2} - D d^{2} = 1$
12		simpll	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land (c \in ℕ \land d \in ℕ)) \land c^{2} - D d^{2} = 1) \to D \in (ℕ ∖ ◻_{ℕ})$
13		nnnn0	$⊢ c \in ℕ \to c \in ℕ_{0}$
14	13	adantr	$⊢ (c \in ℕ \land d \in ℕ) \to c \in ℕ_{0}$
15	14	ad2antlr	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land (c \in ℕ \land d \in ℕ)) \land c^{2} - D d^{2} = 1) \to c \in ℕ_{0}$
16		nnnn0	$⊢ d \in ℕ \to d \in ℕ_{0}$
17	16	adantl	$⊢ (c \in ℕ \land d \in ℕ) \to d \in ℕ_{0}$
18	17	ad2antlr	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land (c \in ℕ \land d \in ℕ)) \land c^{2} - D d^{2} = 1) \to d \in ℕ_{0}$
19		simpr	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land (c \in ℕ \land d \in ℕ)) \land c^{2} - D d^{2} = 1) \to c^{2} - D d^{2} = 1$
20		pellqrexplicit	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land c \in ℕ_{0} \land d \in ℕ_{0}) \land c^{2} - D d^{2} = 1) \to c + \sqrt{D} d \in Pell1QR (D)$
21	12 15 18 19 20	syl31anc	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land (c \in ℕ \land d \in ℕ)) \land c^{2} - D d^{2} = 1) \to c + \sqrt{D} d \in Pell1QR (D)$
22		1re	$⊢ 1 \in ℝ$
23	22	a1i	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land (c \in ℕ \land d \in ℕ)) \to 1 \in ℝ$
24	22 22	readdcli	$⊢ 1 + 1 \in ℝ$
25	24	a1i	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land (c \in ℕ \land d \in ℕ)) \to 1 + 1 \in ℝ$
26		nnre	$⊢ c \in ℕ \to c \in ℝ$
27	26	ad2antrl	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land (c \in ℕ \land d \in ℕ)) \to c \in ℝ$
28	1	adantr	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land (c \in ℕ \land d \in ℕ)) \to D \in ℕ$
29	28	nnrpd	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land (c \in ℕ \land d \in ℕ)) \to D \in ℝ^{+}$
30	29	rpsqrtcld	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land (c \in ℕ \land d \in ℕ)) \to \sqrt{D} \in ℝ^{+}$
31	30	rpred	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land (c \in ℕ \land d \in ℕ)) \to \sqrt{D} \in ℝ$
32		nnre	$⊢ d \in ℕ \to d \in ℝ$
33	32	ad2antll	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land (c \in ℕ \land d \in ℕ)) \to d \in ℝ$
34	31 33	remulcld	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land (c \in ℕ \land d \in ℕ)) \to \sqrt{D} d \in ℝ$
35	27 34	readdcld	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land (c \in ℕ \land d \in ℕ)) \to c + \sqrt{D} d \in ℝ$
36	22	ltp1i	$⊢ 1 < 1 + 1$
37	36	a1i	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land (c \in ℕ \land d \in ℕ)) \to 1 < 1 + 1$
38		nnge1	$⊢ c \in ℕ \to 1 \leq c$
39	38	ad2antrl	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land (c \in ℕ \land d \in ℕ)) \to 1 \leq c$
40		1t1e1	$⊢ 1 \cdot 1 = 1$
41		nnge1	$⊢ D \in ℕ \to 1 \leq D$
42		sq1	$⊢ 1^{2} = 1$
43	42	a1i	$⊢ D \in ℕ \to 1^{2} = 1$
44		nncn	$⊢ D \in ℕ \to D \in ℂ$
45	44	sqsqrtd	$⊢ D \in ℕ \to {\sqrt{D}}^{2} = D$
46	41 43 45	3brtr4d	$⊢ D \in ℕ \to 1^{2} \leq {\sqrt{D}}^{2}$
47	22	a1i	$⊢ D \in ℕ \to 1 \in ℝ$
48		nnrp	$⊢ D \in ℕ \to D \in ℝ^{+}$
49	48	rpsqrtcld	$⊢ D \in ℕ \to \sqrt{D} \in ℝ^{+}$
50	49	rpred	$⊢ D \in ℕ \to \sqrt{D} \in ℝ$
51		0le1	$⊢ 0 \leq 1$
52	51	a1i	$⊢ D \in ℕ \to 0 \leq 1$
53	49	rpge0d	$⊢ D \in ℕ \to 0 \leq \sqrt{D}$
54	47 50 52 53	le2sqd	$⊢ D \in ℕ \to (1 \leq \sqrt{D} \leftrightarrow 1^{2} \leq {\sqrt{D}}^{2})$
55	46 54	mpbird	$⊢ D \in ℕ \to 1 \leq \sqrt{D}$
56	28 55	syl	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land (c \in ℕ \land d \in ℕ)) \to 1 \leq \sqrt{D}$
57		nnge1	$⊢ d \in ℕ \to 1 \leq d$
58	57	ad2antll	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land (c \in ℕ \land d \in ℕ)) \to 1 \leq d$
59	23 51	jctir	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land (c \in ℕ \land d \in ℕ)) \to (1 \in ℝ \land 0 \leq 1)$
60		lemul12a	$⊢ (((1 \in ℝ \land 0 \leq 1) \land \sqrt{D} \in ℝ) \land ((1 \in ℝ \land 0 \leq 1) \land d \in ℝ)) \to ((1 \leq \sqrt{D} \land 1 \leq d) \to 1 \cdot 1 \leq \sqrt{D} d)$
61	59 31 59 33 60	syl22anc	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land (c \in ℕ \land d \in ℕ)) \to ((1 \leq \sqrt{D} \land 1 \leq d) \to 1 \cdot 1 \leq \sqrt{D} d)$
62	56 58 61	mp2and	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land (c \in ℕ \land d \in ℕ)) \to 1 \cdot 1 \leq \sqrt{D} d$
63	40 62	eqbrtrrid	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land (c \in ℕ \land d \in ℕ)) \to 1 \leq \sqrt{D} d$
64	23 23 27 34 39 63	le2addd	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land (c \in ℕ \land d \in ℕ)) \to 1 + 1 \leq c + \sqrt{D} d$
65	23 25 35 37 64	ltletrd	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land (c \in ℕ \land d \in ℕ)) \to 1 < c + \sqrt{D} d$
66	65	adantr	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land (c \in ℕ \land d \in ℕ)) \land c^{2} - D d^{2} = 1) \to 1 < c + \sqrt{D} d$
67		breq2	$⊢ x = c + \sqrt{D} d \to (1 < x \leftrightarrow 1 < c + \sqrt{D} d)$
68	67	rspcev	$⊢ (c + \sqrt{D} d \in Pell1QR (D) \land 1 < c + \sqrt{D} d) \to \exists x \in Pell1QR (D) 1 < x$
69	21 66 68	syl2anc	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land (c \in ℕ \land d \in ℕ)) \land c^{2} - D d^{2} = 1) \to \exists x \in Pell1QR (D) 1 < x$
70	69	ex	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land (c \in ℕ \land d \in ℕ)) \to (c^{2} - D d^{2} = 1 \to \exists x \in Pell1QR (D) 1 < x)$
71	70	rexlimdvva	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to (\exists c \in ℕ \exists d \in ℕ c^{2} - D d^{2} = 1 \to \exists x \in Pell1QR (D) 1 < x)$
72	11 71	mpd	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to \exists x \in Pell1QR (D) 1 < x$

Metamath Proof Explorer

Theorem pellqrex

Proof