Metamath Proof Explorer


Theorem pell1qrgap

Description: First-quadrant Pell solutions are bounded away from 1. (This particular bound allows us 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 ) ) + ( √ ‘ 𝐷 ) ) ≤ 𝐴 )