Theorem pellfundge

Description: Lower bound on the fundamental solution of a Pell equation. (Contributed by Stefan O'Rear, 19-Sep-2014)

	Ref	Expression
Assertion	pellfundge	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( ( √ ‘ ( 𝐷 + 1 ) ) + ( √ ‘ 𝐷 ) ) ≤ ( PellFund ‘ 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		ssrab2	⊢ { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } ⊆ ( Pell14QR ‘ 𝐷 )
2		pell14qrre	⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ) → 𝑎 ∈ ℝ )
3	2	ex	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) → 𝑎 ∈ ℝ ) )
4	3	ssrdv	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( Pell14QR ‘ 𝐷 ) ⊆ ℝ )
5	1 4	sstrid	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } ⊆ ℝ )
6		pell1qrss14	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( Pell1QR ‘ 𝐷 ) ⊆ ( Pell14QR ‘ 𝐷 ) )
7		pellqrex	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ∃ 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) 1 < 𝑎 )
8		ssrexv	⊢ ( ( Pell1QR ‘ 𝐷 ) ⊆ ( Pell14QR ‘ 𝐷 ) → ( ∃ 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) 1 < 𝑎 → ∃ 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) 1 < 𝑎 ) )
9	6 7 8	sylc	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ∃ 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) 1 < 𝑎 )
10		rabn0	⊢ ( { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } ≠ ∅ ↔ ∃ 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) 1 < 𝑎 )
11	9 10	sylibr	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } ≠ ∅ )
12		eldifi	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → 𝐷 ∈ ℕ )
13	12	peano2nnd	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( 𝐷 + 1 ) ∈ ℕ )
14	13	nnrpd	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( 𝐷 + 1 ) ∈ ℝ+ )
15	14	rpsqrtcld	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( √ ‘ ( 𝐷 + 1 ) ) ∈ ℝ+ )
16	15	rpred	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( √ ‘ ( 𝐷 + 1 ) ) ∈ ℝ )
17	12	nnrpd	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → 𝐷 ∈ ℝ+ )
18	17	rpsqrtcld	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( √ ‘ 𝐷 ) ∈ ℝ+ )
19	18	rpred	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( √ ‘ 𝐷 ) ∈ ℝ )
20	16 19	readdcld	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( ( √ ‘ ( 𝐷 + 1 ) ) + ( √ ‘ 𝐷 ) ) ∈ ℝ )
21		breq2	⊢ ( 𝑎 = 𝑏 → ( 1 < 𝑎 ↔ 1 < 𝑏 ) )
22	21	elrab	⊢ ( 𝑏 ∈ { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } ↔ ( 𝑏 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝑏 ) )
23		pell14qrgap	⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝑏 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝑏 ) → ( ( √ ‘ ( 𝐷 + 1 ) ) + ( √ ‘ 𝐷 ) ) ≤ 𝑏 )
24	23	3expib	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( ( 𝑏 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝑏 ) → ( ( √ ‘ ( 𝐷 + 1 ) ) + ( √ ‘ 𝐷 ) ) ≤ 𝑏 ) )
25	22 24	biimtrid	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( 𝑏 ∈ { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } → ( ( √ ‘ ( 𝐷 + 1 ) ) + ( √ ‘ 𝐷 ) ) ≤ 𝑏 ) )
26	25	ralrimiv	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ∀ 𝑏 ∈ { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } ( ( √ ‘ ( 𝐷 + 1 ) ) + ( √ ‘ 𝐷 ) ) ≤ 𝑏 )
27		infmrgelbi	⊢ ( ( ( { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } ⊆ ℝ ∧ { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } ≠ ∅ ∧ ( ( √ ‘ ( 𝐷 + 1 ) ) + ( √ ‘ 𝐷 ) ) ∈ ℝ ) ∧ ∀ 𝑏 ∈ { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } ( ( √ ‘ ( 𝐷 + 1 ) ) + ( √ ‘ 𝐷 ) ) ≤ 𝑏 ) → ( ( √ ‘ ( 𝐷 + 1 ) ) + ( √ ‘ 𝐷 ) ) ≤ inf ( { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } , ℝ , < ) )
28	5 11 20 26 27	syl31anc	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( ( √ ‘ ( 𝐷 + 1 ) ) + ( √ ‘ 𝐷 ) ) ≤ inf ( { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } , ℝ , < ) )
29		pellfundval	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( PellFund ‘ 𝐷 ) = inf ( { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } , ℝ , < ) )
30	28 29	breqtrrd	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( ( √ ‘ ( 𝐷 + 1 ) ) + ( √ ‘ 𝐷 ) ) ≤ ( PellFund ‘ 𝐷 ) )