pellfundex

Description: The fundamental solution as an infimum is itself a solution, showing that the solution set is discrete.

Since the fundamental solution is an infimum, there must be an element ge to Fund and lt 2*Fund. If this element is equal to the fundamental solution we're done, otherwise use the infimum again to find another element which must be ge Fund and lt the first element; their ratio is a group element in (1,2), contradicting pell14qrgapw . (Contributed by Stefan O'Rear, 18-Sep-2014)

		Ref	Expression
	Assertion	pellfundex	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to PellFund (D) \in Pell1QR (D)$

Proof

Step	Hyp	Ref	Expression
1		2re	$⊢ 2 \in ℝ$
2		pellfundre	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to PellFund (D) \in ℝ$
3		remulcl	$⊢ (2 \in ℝ \land PellFund (D) \in ℝ) \to 2 PellFund (D) \in ℝ$
4	1 2 3	sylancr	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to 2 PellFund (D) \in ℝ$
5		0red	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to 0 \in ℝ$
6		1red	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to 1 \in ℝ$
7		0lt1	$⊢ 0 < 1$
8	7	a1i	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to 0 < 1$
9		pellfundgt1	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to 1 < PellFund (D)$
10	5 6 2 8 9	lttrd	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to 0 < PellFund (D)$
11	2 10	elrpd	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to PellFund (D) \in ℝ^{+}$
12	2 11	ltaddrpd	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to PellFund (D) < PellFund (D) + PellFund (D)$
13	2	recnd	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to PellFund (D) \in ℂ$
14	13	2timesd	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to 2 PellFund (D) = PellFund (D) + PellFund (D)$
15	12 14	breqtrrd	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to PellFund (D) < 2 PellFund (D)$
16		pellfundglb	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land 2 PellFund (D) \in ℝ \land PellFund (D) < 2 PellFund (D)) \to \exists a \in Pell1QR (D) (PellFund (D) \leq a \land a < 2 PellFund (D))$
17	4 15 16	mpd3an23	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to \exists a \in Pell1QR (D) (PellFund (D) \leq a \land a < 2 PellFund (D))$
18	2	adantr	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land a \in Pell1QR (D)) \to PellFund (D) \in ℝ$
19		pell1qrss14	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to Pell1QR (D) \subseteq Pell14QR (D)$
20	19	sselda	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land a \in Pell1QR (D)) \to a \in Pell14QR (D)$
21		pell14qrre	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land a \in Pell14QR (D)) \to a \in ℝ$
22	20 21	syldan	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land a \in Pell1QR (D)) \to a \in ℝ$
23	18 22	leloed	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land a \in Pell1QR (D)) \to (PellFund (D) \leq a \leftrightarrow (PellFund (D) < a \lor PellFund (D) = a))$
24		simp-4l	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land a \in Pell1QR (D)) \land (PellFund (D) < a \land a < 2 PellFund (D))) \land b \in Pell1QR (D)) \land (PellFund (D) \leq b \land b < a)) \to D \in (ℕ ∖ ◻_{ℕ})$
25		simp-4r	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land a \in Pell1QR (D)) \land (PellFund (D) < a \land a < 2 PellFund (D))) \land b \in Pell1QR (D)) \land (PellFund (D) \leq b \land b < a)) \to a \in Pell1QR (D)$
26		simplr	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land a \in Pell1QR (D)) \land (PellFund (D) < a \land a < 2 PellFund (D))) \land b \in Pell1QR (D)) \land (PellFund (D) \leq b \land b < a)) \to b \in Pell1QR (D)$
27		simprr	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land a \in Pell1QR (D)) \land (PellFund (D) < a \land a < 2 PellFund (D))) \land b \in Pell1QR (D)) \land (PellFund (D) \leq b \land b < a)) \to b < a$
28	22	ad3antrrr	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land a \in Pell1QR (D)) \land (PellFund (D) < a \land a < 2 PellFund (D))) \land b \in Pell1QR (D)) \land (PellFund (D) \leq b \land b < a)) \to a \in ℝ$
29	4	ad4antr	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land a \in Pell1QR (D)) \land (PellFund (D) < a \land a < 2 PellFund (D))) \land b \in Pell1QR (D)) \land (PellFund (D) \leq b \land b < a)) \to 2 PellFund (D) \in ℝ$
30	19	ad4antr	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land a \in Pell1QR (D)) \land (PellFund (D) < a \land a < 2 PellFund (D))) \land b \in Pell1QR (D)) \land (PellFund (D) \leq b \land b < a)) \to Pell1QR (D) \subseteq Pell14QR (D)$
31	30 26	sseldd	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land a \in Pell1QR (D)) \land (PellFund (D) < a \land a < 2 PellFund (D))) \land b \in Pell1QR (D)) \land (PellFund (D) \leq b \land b < a)) \to b \in Pell14QR (D)$
32		pell14qrre	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land b \in Pell14QR (D)) \to b \in ℝ$
33	24 31 32	syl2anc	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land a \in Pell1QR (D)) \land (PellFund (D) < a \land a < 2 PellFund (D))) \land b \in Pell1QR (D)) \land (PellFund (D) \leq b \land b < a)) \to b \in ℝ$
34		remulcl	$⊢ (2 \in ℝ \land b \in ℝ) \to 2 b \in ℝ$
35	1 33 34	sylancr	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land a \in Pell1QR (D)) \land (PellFund (D) < a \land a < 2 PellFund (D))) \land b \in Pell1QR (D)) \land (PellFund (D) \leq b \land b < a)) \to 2 b \in ℝ$
36		simprr	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land a \in Pell1QR (D)) \land (PellFund (D) < a \land a < 2 PellFund (D))) \to a < 2 PellFund (D)$
37	36	ad2antrr	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land a \in Pell1QR (D)) \land (PellFund (D) < a \land a < 2 PellFund (D))) \land b \in Pell1QR (D)) \land (PellFund (D) \leq b \land b < a)) \to a < 2 PellFund (D)$
38		simprl	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land a \in Pell1QR (D)) \land (PellFund (D) < a \land a < 2 PellFund (D))) \land b \in Pell1QR (D)) \land (PellFund (D) \leq b \land b < a)) \to PellFund (D) \leq b$
39	2	ad4antr	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land a \in Pell1QR (D)) \land (PellFund (D) < a \land a < 2 PellFund (D))) \land b \in Pell1QR (D)) \land (PellFund (D) \leq b \land b < a)) \to PellFund (D) \in ℝ$
40	1	a1i	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land a \in Pell1QR (D)) \land (PellFund (D) < a \land a < 2 PellFund (D))) \land b \in Pell1QR (D)) \land (PellFund (D) \leq b \land b < a)) \to 2 \in ℝ$
41		2pos	$⊢ 0 < 2$
42	41	a1i	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land a \in Pell1QR (D)) \land (PellFund (D) < a \land a < 2 PellFund (D))) \land b \in Pell1QR (D)) \land (PellFund (D) \leq b \land b < a)) \to 0 < 2$
43		lemul2	$⊢ (PellFund (D) \in ℝ \land b \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (PellFund (D) \leq b \leftrightarrow 2 PellFund (D) \leq 2 b)$
44	39 33 40 42 43	syl112anc	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land a \in Pell1QR (D)) \land (PellFund (D) < a \land a < 2 PellFund (D))) \land b \in Pell1QR (D)) \land (PellFund (D) \leq b \land b < a)) \to (PellFund (D) \leq b \leftrightarrow 2 PellFund (D) \leq 2 b)$
45	38 44	mpbid	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land a \in Pell1QR (D)) \land (PellFund (D) < a \land a < 2 PellFund (D))) \land b \in Pell1QR (D)) \land (PellFund (D) \leq b \land b < a)) \to 2 PellFund (D) \leq 2 b$
46	28 29 35 37 45	ltletrd	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land a \in Pell1QR (D)) \land (PellFund (D) < a \land a < 2 PellFund (D))) \land b \in Pell1QR (D)) \land (PellFund (D) \leq b \land b < a)) \to a < 2 b$
47		simp1	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land (a \in Pell1QR (D) \land b \in Pell1QR (D)) \land (b < a \land a < 2 b)) \to D \in (ℕ ∖ ◻_{ℕ})$
48	19	3ad2ant1	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land (a \in Pell1QR (D) \land b \in Pell1QR (D)) \land (b < a \land a < 2 b)) \to Pell1QR (D) \subseteq Pell14QR (D)$
49		simp2l	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land (a \in Pell1QR (D) \land b \in Pell1QR (D)) \land (b < a \land a < 2 b)) \to a \in Pell1QR (D)$
50	48 49	sseldd	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land (a \in Pell1QR (D) \land b \in Pell1QR (D)) \land (b < a \land a < 2 b)) \to a \in Pell14QR (D)$
51		simp2r	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land (a \in Pell1QR (D) \land b \in Pell1QR (D)) \land (b < a \land a < 2 b)) \to b \in Pell1QR (D)$
52	48 51	sseldd	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land (a \in Pell1QR (D) \land b \in Pell1QR (D)) \land (b < a \land a < 2 b)) \to b \in Pell14QR (D)$
53		pell14qrdivcl	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land a \in Pell14QR (D) \land b \in Pell14QR (D)) \to \frac{a}{b} \in Pell14QR (D)$
54	47 50 52 53	syl3anc	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land (a \in Pell1QR (D) \land b \in Pell1QR (D)) \land (b < a \land a < 2 b)) \to \frac{a}{b} \in Pell14QR (D)$
55	47 52 32	syl2anc	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land (a \in Pell1QR (D) \land b \in Pell1QR (D)) \land (b < a \land a < 2 b)) \to b \in ℝ$
56	55	recnd	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land (a \in Pell1QR (D) \land b \in Pell1QR (D)) \land (b < a \land a < 2 b)) \to b \in ℂ$
57	56	mullidd	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land (a \in Pell1QR (D) \land b \in Pell1QR (D)) \land (b < a \land a < 2 b)) \to 1 b = b$
58		simp3l	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land (a \in Pell1QR (D) \land b \in Pell1QR (D)) \land (b < a \land a < 2 b)) \to b < a$
59	57 58	eqbrtrd	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land (a \in Pell1QR (D) \land b \in Pell1QR (D)) \land (b < a \land a < 2 b)) \to 1 b < a$
60		1red	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land (a \in Pell1QR (D) \land b \in Pell1QR (D)) \land (b < a \land a < 2 b)) \to 1 \in ℝ$
61	47 50 21	syl2anc	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land (a \in Pell1QR (D) \land b \in Pell1QR (D)) \land (b < a \land a < 2 b)) \to a \in ℝ$
62		pell14qrgt0	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land b \in Pell14QR (D)) \to 0 < b$
63	47 52 62	syl2anc	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land (a \in Pell1QR (D) \land b \in Pell1QR (D)) \land (b < a \land a < 2 b)) \to 0 < b$
64		ltmuldiv	$⊢ (1 \in ℝ \land a \in ℝ \land (b \in ℝ \land 0 < b)) \to (1 b < a \leftrightarrow 1 < \frac{a}{b})$
65	60 61 55 63 64	syl112anc	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land (a \in Pell1QR (D) \land b \in Pell1QR (D)) \land (b < a \land a < 2 b)) \to (1 b < a \leftrightarrow 1 < \frac{a}{b})$
66	59 65	mpbid	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land (a \in Pell1QR (D) \land b \in Pell1QR (D)) \land (b < a \land a < 2 b)) \to 1 < \frac{a}{b}$
67		simp3r	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land (a \in Pell1QR (D) \land b \in Pell1QR (D)) \land (b < a \land a < 2 b)) \to a < 2 b$
68	1	a1i	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land (a \in Pell1QR (D) \land b \in Pell1QR (D)) \land (b < a \land a < 2 b)) \to 2 \in ℝ$
69		ltdivmul2	$⊢ (a \in ℝ \land 2 \in ℝ \land (b \in ℝ \land 0 < b)) \to (\frac{a}{b} < 2 \leftrightarrow a < 2 b)$
70	61 68 55 63 69	syl112anc	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land (a \in Pell1QR (D) \land b \in Pell1QR (D)) \land (b < a \land a < 2 b)) \to (\frac{a}{b} < 2 \leftrightarrow a < 2 b)$
71	67 70	mpbird	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land (a \in Pell1QR (D) \land b \in Pell1QR (D)) \land (b < a \land a < 2 b)) \to \frac{a}{b} < 2$
72		simprr	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land \frac{a}{b} \in Pell14QR (D)) \land (1 < \frac{a}{b} \land \frac{a}{b} < 2)) \to \frac{a}{b} < 2$
73		simpll	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land \frac{a}{b} \in Pell14QR (D)) \land (1 < \frac{a}{b} \land \frac{a}{b} < 2)) \to D \in (ℕ ∖ ◻_{ℕ})$
74		simplr	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land \frac{a}{b} \in Pell14QR (D)) \land (1 < \frac{a}{b} \land \frac{a}{b} < 2)) \to \frac{a}{b} \in Pell14QR (D)$
75		simprl	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land \frac{a}{b} \in Pell14QR (D)) \land (1 < \frac{a}{b} \land \frac{a}{b} < 2)) \to 1 < \frac{a}{b}$
76		pell14qrgapw	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land \frac{a}{b} \in Pell14QR (D) \land 1 < \frac{a}{b}) \to 2 < \frac{a}{b}$
77	73 74 75 76	syl3anc	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land \frac{a}{b} \in Pell14QR (D)) \land (1 < \frac{a}{b} \land \frac{a}{b} < 2)) \to 2 < \frac{a}{b}$
78		pell14qrre	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land \frac{a}{b} \in Pell14QR (D)) \to \frac{a}{b} \in ℝ$
79	78	adantr	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land \frac{a}{b} \in Pell14QR (D)) \land (1 < \frac{a}{b} \land \frac{a}{b} < 2)) \to \frac{a}{b} \in ℝ$
80		ltnsym	$⊢ (2 \in ℝ \land \frac{a}{b} \in ℝ) \to (2 < \frac{a}{b} \to \neg \frac{a}{b} < 2)$
81	1 79 80	sylancr	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land \frac{a}{b} \in Pell14QR (D)) \land (1 < \frac{a}{b} \land \frac{a}{b} < 2)) \to (2 < \frac{a}{b} \to \neg \frac{a}{b} < 2)$
82	77 81	mpd	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land \frac{a}{b} \in Pell14QR (D)) \land (1 < \frac{a}{b} \land \frac{a}{b} < 2)) \to \neg \frac{a}{b} < 2$
83	72 82	pm2.21dd	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land \frac{a}{b} \in Pell14QR (D)) \land (1 < \frac{a}{b} \land \frac{a}{b} < 2)) \to PellFund (D) \in Pell1QR (D)$
84	47 54 66 71 83	syl22anc	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land (a \in Pell1QR (D) \land b \in Pell1QR (D)) \land (b < a \land a < 2 b)) \to PellFund (D) \in Pell1QR (D)$
85	24 25 26 27 46 84	syl122anc	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land a \in Pell1QR (D)) \land (PellFund (D) < a \land a < 2 PellFund (D))) \land b \in Pell1QR (D)) \land (PellFund (D) \leq b \land b < a)) \to PellFund (D) \in Pell1QR (D)$
86		simpll	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land a \in Pell1QR (D)) \land (PellFund (D) < a \land a < 2 PellFund (D))) \to D \in (ℕ ∖ ◻_{ℕ})$
87	22	adantr	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land a \in Pell1QR (D)) \land (PellFund (D) < a \land a < 2 PellFund (D))) \to a \in ℝ$
88		simprl	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land a \in Pell1QR (D)) \land (PellFund (D) < a \land a < 2 PellFund (D))) \to PellFund (D) < a$
89		pellfundglb	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land a \in ℝ \land PellFund (D) < a) \to \exists b \in Pell1QR (D) (PellFund (D) \leq b \land b < a)$
90	86 87 88 89	syl3anc	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land a \in Pell1QR (D)) \land (PellFund (D) < a \land a < 2 PellFund (D))) \to \exists b \in Pell1QR (D) (PellFund (D) \leq b \land b < a)$
91	85 90	r19.29a	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land a \in Pell1QR (D)) \land (PellFund (D) < a \land a < 2 PellFund (D))) \to PellFund (D) \in Pell1QR (D)$
92	91	exp32	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land a \in Pell1QR (D)) \to (PellFund (D) < a \to (a < 2 PellFund (D) \to PellFund (D) \in Pell1QR (D)))$
93		simp2	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land a \in Pell1QR (D)) \land PellFund (D) = a \land a < 2 PellFund (D)) \to PellFund (D) = a$
94		simp1r	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land a \in Pell1QR (D)) \land PellFund (D) = a \land a < 2 PellFund (D)) \to a \in Pell1QR (D)$
95	93 94	eqeltrd	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land a \in Pell1QR (D)) \land PellFund (D) = a \land a < 2 PellFund (D)) \to PellFund (D) \in Pell1QR (D)$
96	95	3exp	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land a \in Pell1QR (D)) \to (PellFund (D) = a \to (a < 2 PellFund (D) \to PellFund (D) \in Pell1QR (D)))$
97	92 96	jaod	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land a \in Pell1QR (D)) \to ((PellFund (D) < a \lor PellFund (D) = a) \to (a < 2 PellFund (D) \to PellFund (D) \in Pell1QR (D)))$
98	23 97	sylbid	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land a \in Pell1QR (D)) \to (PellFund (D) \leq a \to (a < 2 PellFund (D) \to PellFund (D) \in Pell1QR (D)))$
99	98	impd	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land a \in Pell1QR (D)) \to ((PellFund (D) \leq a \land a < 2 PellFund (D)) \to PellFund (D) \in Pell1QR (D))$
100	99	rexlimdva	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to (\exists a \in Pell1QR (D) (PellFund (D) \leq a \land a < 2 PellFund (D)) \to PellFund (D) \in Pell1QR (D))$
101	17 100	mpd	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to PellFund (D) \in Pell1QR (D)$

Metamath Proof Explorer

Theorem pellfundex

Proof