Step |
Hyp |
Ref |
Expression |
1 |
|
simp2 |
⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝐴 ) → 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) |
2 |
|
1re |
⊢ 1 ∈ ℝ |
3 |
|
pell14qrre |
⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) → 𝐴 ∈ ℝ ) |
4 |
|
ltle |
⊢ ( ( 1 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 1 < 𝐴 → 1 ≤ 𝐴 ) ) |
5 |
2 3 4
|
sylancr |
⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) → ( 1 < 𝐴 → 1 ≤ 𝐴 ) ) |
6 |
5
|
3impia |
⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝐴 ) → 1 ≤ 𝐴 ) |
7 |
|
elpell1qr2 |
⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( 𝐴 ∈ ( Pell1QR ‘ 𝐷 ) ↔ ( 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 ≤ 𝐴 ) ) ) |
8 |
7
|
3ad2ant1 |
⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝐴 ) → ( 𝐴 ∈ ( Pell1QR ‘ 𝐷 ) ↔ ( 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 ≤ 𝐴 ) ) ) |
9 |
1 6 8
|
mpbir2and |
⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝐴 ) → 𝐴 ∈ ( Pell1QR ‘ 𝐷 ) ) |
10 |
|
pell1qrgap |
⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell1QR ‘ 𝐷 ) ∧ 1 < 𝐴 ) → ( ( √ ‘ ( 𝐷 + 1 ) ) + ( √ ‘ 𝐷 ) ) ≤ 𝐴 ) |
11 |
9 10
|
syld3an2 |
⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝐴 ) → ( ( √ ‘ ( 𝐷 + 1 ) ) + ( √ ‘ 𝐷 ) ) ≤ 𝐴 ) |