Metamath Proof Explorer

Theorem pell1qrgap

Description: First-quadrant Pell solutions are bounded away from 1. (This particular bound allows to prove exact values for the fundamental solution later.) (Contributed by Stefan O'Rear, 18-Sep-2014)

Ref Expression
Assertion pell1qrgap ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell1QR ‘ 𝐷 ) ∧ 1 < 𝐴 ) → ( ( √ ‘ ( 𝐷 + 1 ) ) + ( √ ‘ 𝐷 ) ) ≤ 𝐴 )

Proof

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 ) ) + ( √ ‘ 𝐷 ) ) ≤ 𝐴 )