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 ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → 1 < ( PellFund ‘ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 1red ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → 1 ∈ ℝ )
2 eldifi ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → 𝐷 ∈ ℕ )
3 2 peano2nnd ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( 𝐷 + 1 ) ∈ ℕ )
4 3 nnrpd ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( 𝐷 + 1 ) ∈ ℝ+ )
5 4 rpsqrtcld ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( √ ‘ ( 𝐷 + 1 ) ) ∈ ℝ+ )
6 5 rpred ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( √ ‘ ( 𝐷 + 1 ) ) ∈ ℝ )
7 2 nnrpd ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → 𝐷 ∈ ℝ+ )
8 7 rpsqrtcld ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( √ ‘ 𝐷 ) ∈ ℝ+ )
9 8 rpred ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( √ ‘ 𝐷 ) ∈ ℝ )
10 6 9 readdcld ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( ( √ ‘ ( 𝐷 + 1 ) ) + ( √ ‘ 𝐷 ) ) ∈ ℝ )
11 pellfundre ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( PellFund ‘ 𝐷 ) ∈ ℝ )
12 sqrt1 ⊢ ( √ ‘ 1 ) = 1
13 12 1 eqeltrid ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( √ ‘ 1 ) ∈ ℝ )
14 13 13 readdcld ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( ( √ ‘ 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 ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → 1 < ( ( √ ‘ 1 ) + ( √ ‘ 1 ) ) )
21 3 nnge1d ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → 1 ≤ ( 𝐷 + 1 ) )
22 0le1 ⊢ 0 ≤ 1
23 22 a1i ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → 0 ≤ 1 )
24 2 nnred ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → 𝐷 ∈ ℝ )
25 peano2re ⊢ ( 𝐷 ∈ ℝ → ( 𝐷 + 1 ) ∈ ℝ )
26 24 25 syl ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( 𝐷 + 1 ) ∈ ℝ )
27 3 nnnn0d ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( 𝐷 + 1 ) ∈ ℕ0 )
28 27 nn0ge0d ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → 0 ≤ ( 𝐷 + 1 ) )
29 1 23 26 28 sqrtled ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( 1 ≤ ( 𝐷 + 1 ) ↔ ( √ ‘ 1 ) ≤ ( √ ‘ ( 𝐷 + 1 ) ) ) )
30 21 29 mpbid ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( √ ‘ 1 ) ≤ ( √ ‘ ( 𝐷 + 1 ) ) )
31 2 nnge1d ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → 1 ≤ 𝐷 )
32 2 nnnn0d ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → 𝐷 ∈ ℕ0 )
33 32 nn0ge0d ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → 0 ≤ 𝐷 )
34 1 23 24 33 sqrtled ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( 1 ≤ 𝐷 ↔ ( √ ‘ 1 ) ≤ ( √ ‘ 𝐷 ) ) )
35 31 34 mpbid ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( √ ‘ 1 ) ≤ ( √ ‘ 𝐷 ) )
36 13 13 6 9 30 35 le2addd ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( ( √ ‘ 1 ) + ( √ ‘ 1 ) ) ≤ ( ( √ ‘ ( 𝐷 + 1 ) ) + ( √ ‘ 𝐷 ) ) )
37 1 14 10 20 36 ltletrd ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → 1 < ( ( √ ‘ ( 𝐷 + 1 ) ) + ( √ ‘ 𝐷 ) ) )
38 pellfundge ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( ( √ ‘ ( 𝐷 + 1 ) ) + ( √ ‘ 𝐷 ) ) ≤ ( PellFund ‘ 𝐷 ) )
39 1 10 11 37 38 ltletrd ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → 1 < ( PellFund ‘ 𝐷 ) )