Step |
Hyp |
Ref |
Expression |
1 |
|
elpell1qr |
⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( 𝐴 ∈ ( Pell1QR ‘ 𝐷 ) ↔ ( 𝐴 ∈ ℝ ∧ ∃ 𝑎 ∈ ℕ0 ∃ 𝑏 ∈ ℕ0 ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ) ) |
2 |
1
|
adantr |
⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 1 < 𝐴 ) → ( 𝐴 ∈ ( Pell1QR ‘ 𝐷 ) ↔ ( 𝐴 ∈ ℝ ∧ ∃ 𝑎 ∈ ℕ0 ∃ 𝑏 ∈ ℕ0 ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ) ) |
3 |
|
eldifi |
⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → 𝐷 ∈ ℕ ) |
4 |
3
|
ad4antr |
⊢ ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 1 < 𝐴 ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) → 𝐷 ∈ ℕ ) |
5 |
|
simplr |
⊢ ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 1 < 𝐴 ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) → ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) ) |
6 |
|
simp-4r |
⊢ ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 1 < 𝐴 ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) → 1 < 𝐴 ) |
7 |
|
simprl |
⊢ ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 1 < 𝐴 ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) → 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ) |
8 |
6 7
|
breqtrd |
⊢ ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 1 < 𝐴 ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) → 1 < ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ) |
9 |
|
simprr |
⊢ ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 1 < 𝐴 ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) → ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) |
10 |
|
pell1qrgaplem |
⊢ ( ( ( 𝐷 ∈ ℕ ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) → ( ( √ ‘ ( 𝐷 + 1 ) ) + ( √ ‘ 𝐷 ) ) ≤ ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ) |
11 |
4 5 8 9 10
|
syl22anc |
⊢ ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 1 < 𝐴 ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) → ( ( √ ‘ ( 𝐷 + 1 ) ) + ( √ ‘ 𝐷 ) ) ≤ ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ) |
12 |
11 7
|
breqtrrd |
⊢ ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 1 < 𝐴 ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) → ( ( √ ‘ ( 𝐷 + 1 ) ) + ( √ ‘ 𝐷 ) ) ≤ 𝐴 ) |
13 |
12
|
ex |
⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 1 < 𝐴 ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) ) → ( ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) → ( ( √ ‘ ( 𝐷 + 1 ) ) + ( √ ‘ 𝐷 ) ) ≤ 𝐴 ) ) |
14 |
13
|
rexlimdvva |
⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 1 < 𝐴 ) ∧ 𝐴 ∈ ℝ ) → ( ∃ 𝑎 ∈ ℕ0 ∃ 𝑏 ∈ ℕ0 ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) → ( ( √ ‘ ( 𝐷 + 1 ) ) + ( √ ‘ 𝐷 ) ) ≤ 𝐴 ) ) |
15 |
14
|
expimpd |
⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 1 < 𝐴 ) → ( ( 𝐴 ∈ ℝ ∧ ∃ 𝑎 ∈ ℕ0 ∃ 𝑏 ∈ ℕ0 ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) → ( ( √ ‘ ( 𝐷 + 1 ) ) + ( √ ‘ 𝐷 ) ) ≤ 𝐴 ) ) |
16 |
2 15
|
sylbid |
⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 1 < 𝐴 ) → ( 𝐴 ∈ ( Pell1QR ‘ 𝐷 ) → ( ( √ ‘ ( 𝐷 + 1 ) ) + ( √ ‘ 𝐷 ) ) ≤ 𝐴 ) ) |
17 |
16
|
ex |
⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( 1 < 𝐴 → ( 𝐴 ∈ ( Pell1QR ‘ 𝐷 ) → ( ( √ ‘ ( 𝐷 + 1 ) ) + ( √ ‘ 𝐷 ) ) ≤ 𝐴 ) ) ) |
18 |
17
|
com23 |
⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( 𝐴 ∈ ( Pell1QR ‘ 𝐷 ) → ( 1 < 𝐴 → ( ( √ ‘ ( 𝐷 + 1 ) ) + ( √ ‘ 𝐷 ) ) ≤ 𝐴 ) ) ) |
19 |
18
|
3imp |
⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell1QR ‘ 𝐷 ) ∧ 1 < 𝐴 ) → ( ( √ ‘ ( 𝐷 + 1 ) ) + ( √ ‘ 𝐷 ) ) ≤ 𝐴 ) |