pellfundglb

Description: If a real is larger than the fundamental solution, there is a nontrivial solution less than it. (Contributed by Stefan O'Rear, 18-Sep-2014)

		Ref	Expression
	Assertion	pellfundglb	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ \land PellFund (D) < A) \to \exists x \in Pell1QR (D) (PellFund (D) \leq x \land x < A)$

Proof

Step	Hyp	Ref	Expression
1		pellfundval	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to PellFund (D) = sup (\{a \in Pell14QR (D) \| 1 < a\} ℝ <)$
2	1	3ad2ant1	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ \land PellFund (D) < A) \to PellFund (D) = sup (\{a \in Pell14QR (D) \| 1 < a\} ℝ <)$
3		simp3	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ \land PellFund (D) < A) \to PellFund (D) < A$
4	2 3	eqbrtrrd	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ \land PellFund (D) < A) \to sup (\{a \in Pell14QR (D) \| 1 < a\} ℝ <) < A$
5		pellfundre	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to PellFund (D) \in ℝ$
6	5	3ad2ant1	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ \land PellFund (D) < A) \to PellFund (D) \in ℝ$
7	2 6	eqeltrrd	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ \land PellFund (D) < A) \to sup (\{a \in Pell14QR (D) \| 1 < a\} ℝ <) \in ℝ$
8		simp2	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ \land PellFund (D) < A) \to A \in ℝ$
9	7 8	ltnled	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ \land PellFund (D) < A) \to (sup (\{a \in Pell14QR (D) \| 1 < a\} ℝ <) < A \leftrightarrow \neg A \leq sup (\{a \in Pell14QR (D) \| 1 < a\} ℝ <))$
10	4 9	mpbid	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ \land PellFund (D) < A) \to \neg A \leq sup (\{a \in Pell14QR (D) \| 1 < a\} ℝ <)$
11		ssrab2	$⊢ \{a \in Pell14QR (D) \| 1 < a\} \subseteq Pell14QR (D)$
12		pell14qrre	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land a \in Pell14QR (D)) \to a \in ℝ$
13	12	ex	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to (a \in Pell14QR (D) \to a \in ℝ)$
14	13	ssrdv	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to Pell14QR (D) \subseteq ℝ$
15	14	3ad2ant1	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ \land PellFund (D) < A) \to Pell14QR (D) \subseteq ℝ$
16	11 15	sstrid	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ \land PellFund (D) < A) \to \{a \in Pell14QR (D) \| 1 < a\} \subseteq ℝ$
17		pell1qrss14	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to Pell1QR (D) \subseteq Pell14QR (D)$
18	17	3ad2ant1	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ \land PellFund (D) < A) \to Pell1QR (D) \subseteq Pell14QR (D)$
19		pellqrex	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to \exists a \in Pell1QR (D) 1 < a$
20	19	3ad2ant1	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ \land PellFund (D) < A) \to \exists a \in Pell1QR (D) 1 < a$
21		ssrexv	$⊢ Pell1QR (D) \subseteq Pell14QR (D) \to (\exists a \in Pell1QR (D) 1 < a \to \exists a \in Pell14QR (D) 1 < a)$
22	18 20 21	sylc	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ \land PellFund (D) < A) \to \exists a \in Pell14QR (D) 1 < a$
23		rabn0	$⊢ \{a \in Pell14QR (D) \| 1 < a\} \neq \emptyset \leftrightarrow \exists a \in Pell14QR (D) 1 < a$
24	22 23	sylibr	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ \land PellFund (D) < A) \to \{a \in Pell14QR (D) \| 1 < a\} \neq \emptyset$
25		infmrgelbi	$⊢ ((\{a \in Pell14QR (D) \| 1 < a\} \subseteq ℝ \land \{a \in Pell14QR (D) \| 1 < a\} \neq \emptyset \land A \in ℝ) \land \forall x \in \{a \in Pell14QR (D) \| 1 < a\} A \leq x) \to A \leq sup (\{a \in Pell14QR (D) \| 1 < a\} ℝ <)$
26	25	ex	$⊢ (\{a \in Pell14QR (D) \| 1 < a\} \subseteq ℝ \land \{a \in Pell14QR (D) \| 1 < a\} \neq \emptyset \land A \in ℝ) \to (\forall x \in \{a \in Pell14QR (D) \| 1 < a\} A \leq x \to A \leq sup (\{a \in Pell14QR (D) \| 1 < a\} ℝ <))$
27	16 24 8 26	syl3anc	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ \land PellFund (D) < A) \to (\forall x \in \{a \in Pell14QR (D) \| 1 < a\} A \leq x \to A \leq sup (\{a \in Pell14QR (D) \| 1 < a\} ℝ <))$
28	10 27	mtod	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ \land PellFund (D) < A) \to \neg \forall x \in \{a \in Pell14QR (D) \| 1 < a\} A \leq x$
29		rexnal	$⊢ \exists x \in \{a \in Pell14QR (D) \| 1 < a\} \neg A \leq x \leftrightarrow \neg \forall x \in \{a \in Pell14QR (D) \| 1 < a\} A \leq x$
30	28 29	sylibr	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ \land PellFund (D) < A) \to \exists x \in \{a \in Pell14QR (D) \| 1 < a\} \neg A \leq x$
31		breq2	$⊢ a = x \to (1 < a \leftrightarrow 1 < x)$
32	31	elrab	$⊢ x \in \{a \in Pell14QR (D) \| 1 < a\} \leftrightarrow (x \in Pell14QR (D) \land 1 < x)$
33		simprl	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ \land PellFund (D) < A) \land (x \in Pell14QR (D) \land 1 < x)) \to x \in Pell14QR (D)$
34		1red	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ \land PellFund (D) < A) \land (x \in Pell14QR (D) \land 1 < x)) \to 1 \in ℝ$
35		simpl1	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ \land PellFund (D) < A) \land (x \in Pell14QR (D) \land 1 < x)) \to D \in (ℕ ∖ ◻_{ℕ})$
36		pell14qrre	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land x \in Pell14QR (D)) \to x \in ℝ$
37	35 33 36	syl2anc	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ \land PellFund (D) < A) \land (x \in Pell14QR (D) \land 1 < x)) \to x \in ℝ$
38		simprr	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ \land PellFund (D) < A) \land (x \in Pell14QR (D) \land 1 < x)) \to 1 < x$
39	34 37 38	ltled	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ \land PellFund (D) < A) \land (x \in Pell14QR (D) \land 1 < x)) \to 1 \leq x$
40	33 39	jca	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ \land PellFund (D) < A) \land (x \in Pell14QR (D) \land 1 < x)) \to (x \in Pell14QR (D) \land 1 \leq x)$
41		elpell1qr2	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to (x \in Pell1QR (D) \leftrightarrow (x \in Pell14QR (D) \land 1 \leq x))$
42	35 41	syl	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ \land PellFund (D) < A) \land (x \in Pell14QR (D) \land 1 < x)) \to (x \in Pell1QR (D) \leftrightarrow (x \in Pell14QR (D) \land 1 \leq x))$
43	40 42	mpbird	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ \land PellFund (D) < A) \land (x \in Pell14QR (D) \land 1 < x)) \to x \in Pell1QR (D)$
44	32 43	sylan2b	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ \land PellFund (D) < A) \land x \in \{a \in Pell14QR (D) \| 1 < a\}) \to x \in Pell1QR (D)$
45	44	adantrr	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ \land PellFund (D) < A) \land (x \in \{a \in Pell14QR (D) \| 1 < a\} \land \neg A \leq x)) \to x \in Pell1QR (D)$
46		simpl1	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ \land PellFund (D) < A) \land (x \in \{a \in Pell14QR (D) \| 1 < a\} \land \neg A \leq x)) \to D \in (ℕ ∖ ◻_{ℕ})$
47		simprl	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ \land PellFund (D) < A) \land (x \in \{a \in Pell14QR (D) \| 1 < a\} \land \neg A \leq x)) \to x \in \{a \in Pell14QR (D) \| 1 < a\}$
48	11 47	sselid	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ \land PellFund (D) < A) \land (x \in \{a \in Pell14QR (D) \| 1 < a\} \land \neg A \leq x)) \to x \in Pell14QR (D)$
49		simpr	$⊢ (x \in Pell14QR (D) \land 1 < x) \to 1 < x$
50	49	a1i	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ \land PellFund (D) < A) \to ((x \in Pell14QR (D) \land 1 < x) \to 1 < x)$
51	32 50	biimtrid	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ \land PellFund (D) < A) \to (x \in \{a \in Pell14QR (D) \| 1 < a\} \to 1 < x)$
52	51	imp	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ \land PellFund (D) < A) \land x \in \{a \in Pell14QR (D) \| 1 < a\}) \to 1 < x$
53	52	adantrr	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ \land PellFund (D) < A) \land (x \in \{a \in Pell14QR (D) \| 1 < a\} \land \neg A \leq x)) \to 1 < x$
54		pellfundlb	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land x \in Pell14QR (D) \land 1 < x) \to PellFund (D) \leq x$
55	46 48 53 54	syl3anc	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ \land PellFund (D) < A) \land (x \in \{a \in Pell14QR (D) \| 1 < a\} \land \neg A \leq x)) \to PellFund (D) \leq x$
56		simprr	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ \land PellFund (D) < A) \land (x \in \{a \in Pell14QR (D) \| 1 < a\} \land \neg A \leq x)) \to \neg A \leq x$
57	15	adantr	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ \land PellFund (D) < A) \land (x \in \{a \in Pell14QR (D) \| 1 < a\} \land \neg A \leq x)) \to Pell14QR (D) \subseteq ℝ$
58	57 48	sseldd	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ \land PellFund (D) < A) \land (x \in \{a \in Pell14QR (D) \| 1 < a\} \land \neg A \leq x)) \to x \in ℝ$
59		simpl2	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ \land PellFund (D) < A) \land (x \in \{a \in Pell14QR (D) \| 1 < a\} \land \neg A \leq x)) \to A \in ℝ$
60	58 59	ltnled	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ \land PellFund (D) < A) \land (x \in \{a \in Pell14QR (D) \| 1 < a\} \land \neg A \leq x)) \to (x < A \leftrightarrow \neg A \leq x)$
61	56 60	mpbird	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ \land PellFund (D) < A) \land (x \in \{a \in Pell14QR (D) \| 1 < a\} \land \neg A \leq x)) \to x < A$
62	55 61	jca	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ \land PellFund (D) < A) \land (x \in \{a \in Pell14QR (D) \| 1 < a\} \land \neg A \leq x)) \to (PellFund (D) \leq x \land x < A)$
63	30 45 62	reximssdv	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ \land PellFund (D) < A) \to \exists x \in Pell1QR (D) (PellFund (D) \leq x \land x < A)$

Metamath Proof Explorer

Theorem pellfundglb

Proof