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