Metamath Proof Explorer

Theorem pellfundgt1

Description: Weak lower bound on the Pell fundamental solution. (Contributed by Stefan O'Rear, 19-Sep-2014)

Ref Expression
Assertion pellfundgt1 ⊢D∈ℕ∖◻ℕ→1<PellFund⁡D

Proof

Step Hyp Ref Expression
1 1red ⊢D∈ℕ∖◻ℕ→1∈ℝ
2 eldifi ⊢D∈ℕ∖◻ℕ→D∈ℕ
3 2 peano2nnd ⊢D∈ℕ∖◻ℕ→D+1∈ℕ
4 3 nnrpd ⊢D∈ℕ∖◻ℕ→D+1∈ℝ+
5 4 rpsqrtcld ⊢D∈ℕ∖◻ℕ→D+1∈ℝ+
6 5 rpred ⊢D∈ℕ∖◻ℕ→D+1∈ℝ
7 2 nnrpd ⊢D∈ℕ∖◻ℕ→D∈ℝ+
8 7 rpsqrtcld ⊢D∈ℕ∖◻ℕ→D∈ℝ+
9 8 rpred ⊢D∈ℕ∖◻ℕ→D∈ℝ
10 6 9 readdcld ⊢D∈ℕ∖◻ℕ→D+1+D∈ℝ
11 pellfundre ⊢D∈ℕ∖◻ℕ→PellFund⁡D∈ℝ
12 sqrt1 ⊢1=1
13 12 1 eqeltrid ⊢D∈ℕ∖◻ℕ→1∈ℝ
14 13 13 readdcld ⊢D∈ℕ∖◻ℕ→1+1∈ℝ
15 1lt2 ⊢1<2
16 12 12 oveq12i ⊢1+1=1+1
17 1p1e2 ⊢1+1=2
18 16 17 eqtri ⊢1+1=2
19 15 18 breqtrri ⊢1<1+1
20 19 a1i ⊢D∈ℕ∖◻ℕ→1<1+1
21 3 nnge1d ⊢D∈ℕ∖◻ℕ→1≤D+1
22 0le1 ⊢0≤1
23 22 a1i ⊢D∈ℕ∖◻ℕ→0≤1
24 2 nnred ⊢D∈ℕ∖◻ℕ→D∈ℝ
25 peano2re ⊢D∈ℝ→D+1∈ℝ
26 24 25 syl ⊢D∈ℕ∖◻ℕ→D+1∈ℝ
27 3 nnnn0d ⊢D∈ℕ∖◻ℕ→D+1∈ℕ0
28 27 nn0ge0d ⊢D∈ℕ∖◻ℕ→0≤D+1
29 1 23 26 28 sqrtled ⊢D∈ℕ∖◻ℕ→1≤D+1↔1≤D+1
30 21 29 mpbid ⊢D∈ℕ∖◻ℕ→1≤D+1
31 2 nnge1d ⊢D∈ℕ∖◻ℕ→1≤D
32 2 nnnn0d ⊢D∈ℕ∖◻ℕ→D∈ℕ0
33 32 nn0ge0d ⊢D∈ℕ∖◻ℕ→0≤D
34 1 23 24 33 sqrtled ⊢D∈ℕ∖◻ℕ→1≤D↔1≤D
35 31 34 mpbid ⊢D∈ℕ∖◻ℕ→1≤D
36 13 13 6 9 30 35 le2addd ⊢D∈ℕ∖◻ℕ→1+1≤D+1+D
37 1 14 10 20 36 ltletrd ⊢D∈ℕ∖◻ℕ→1<D+1+D
38 pellfundge ⊢D∈ℕ∖◻ℕ→D+1+D≤PellFund⁡D
39 1 10 11 37 38 ltletrd ⊢D∈ℕ∖◻ℕ→1<PellFund⁡D