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 D A Pell1QR D 1 < A D + 1 + D A

Proof

Step Hyp Ref Expression
1 elpell1qr D A Pell1QR D A a 0 b 0 A = a + D b a 2 D b 2 = 1
2 1 adantr D 1 < A A Pell1QR D A a 0 b 0 A = a + D b a 2 D b 2 = 1
3 eldifi D D
4 3 ad4antr D 1 < A A a 0 b 0 A = a + D b a 2 D b 2 = 1 D
5 simplr D 1 < A A a 0 b 0 A = a + D b a 2 D b 2 = 1 a 0 b 0
6 simp-4r D 1 < A A a 0 b 0 A = a + D b a 2 D b 2 = 1 1 < A
7 simprl D 1 < A A a 0 b 0 A = a + D b a 2 D b 2 = 1 A = a + D b
8 6 7 breqtrd D 1 < A A a 0 b 0 A = a + D b a 2 D b 2 = 1 1 < a + D b
9 simprr D 1 < A A a 0 b 0 A = a + D b a 2 D b 2 = 1 a 2 D b 2 = 1
10 pell1qrgaplem D a 0 b 0 1 < a + D b a 2 D b 2 = 1 D + 1 + D a + D b
11 4 5 8 9 10 syl22anc D 1 < A A a 0 b 0 A = a + D b a 2 D b 2 = 1 D + 1 + D a + D b
12 11 7 breqtrrd D 1 < A A a 0 b 0 A = a + D b a 2 D b 2 = 1 D + 1 + D A
13 12 ex D 1 < A A a 0 b 0 A = a + D b a 2 D b 2 = 1 D + 1 + D A
14 13 rexlimdvva D 1 < A A a 0 b 0 A = a + D b a 2 D b 2 = 1 D + 1 + D A
15 14 expimpd D 1 < A A a 0 b 0 A = a + D b a 2 D b 2 = 1 D + 1 + D A
16 2 15 sylbid D 1 < A A Pell1QR D D + 1 + D A
17 16 ex D 1 < A A Pell1QR D D + 1 + D A
18 17 com23 D A Pell1QR D 1 < A D + 1 + D A
19 18 3imp D A Pell1QR D 1 < A D + 1 + D A