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 
|- ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1QR ` D ) /\ 1 < A ) -> ( ( sqrt ` ( D + 1 ) ) + ( sqrt ` D ) ) <_ A )

Proof

Step Hyp Ref Expression
1 elpell1qr 
 |-  ( D e. ( NN \ []NN ) -> ( A e. ( Pell1QR ` D ) <-> ( A e. RR /\ E. a e. NN0 E. b e. NN0 ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) ) )
2 1 adantr 
 |-  ( ( D e. ( NN \ []NN ) /\ 1 < A ) -> ( A e. ( Pell1QR ` D ) <-> ( A e. RR /\ E. a e. NN0 E. b e. NN0 ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) ) )
3 eldifi 
 |-  ( D e. ( NN \ []NN ) -> D e. NN )
4 3 ad4antr 
 |-  ( ( ( ( ( D e. ( NN \ []NN ) /\ 1 < A ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> D e. NN )
5 simplr 
 |-  ( ( ( ( ( D e. ( NN \ []NN ) /\ 1 < A ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( a e. NN0 /\ b e. NN0 ) )
6 simp-4r 
 |-  ( ( ( ( ( D e. ( NN \ []NN ) /\ 1 < A ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> 1 < A )
7 simprl 
 |-  ( ( ( ( ( D e. ( NN \ []NN ) /\ 1 < A ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> A = ( a + ( ( sqrt ` D ) x. b ) ) )
8 6 7 breqtrd 
 |-  ( ( ( ( ( D e. ( NN \ []NN ) /\ 1 < A ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> 1 < ( a + ( ( sqrt ` D ) x. b ) ) )
9 simprr 
 |-  ( ( ( ( ( D e. ( NN \ []NN ) /\ 1 < A ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 )
10 pell1qrgaplem 
 |-  ( ( ( D e. NN /\ ( a e. NN0 /\ b e. NN0 ) ) /\ ( 1 < ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( ( sqrt ` ( D + 1 ) ) + ( sqrt ` D ) ) <_ ( a + ( ( sqrt ` D ) x. b ) ) )
11 4 5 8 9 10 syl22anc 
 |-  ( ( ( ( ( D e. ( NN \ []NN ) /\ 1 < A ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( ( sqrt ` ( D + 1 ) ) + ( sqrt ` D ) ) <_ ( a + ( ( sqrt ` D ) x. b ) ) )
12 11 7 breqtrrd 
 |-  ( ( ( ( ( D e. ( NN \ []NN ) /\ 1 < A ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( ( sqrt ` ( D + 1 ) ) + ( sqrt ` D ) ) <_ A )
13 12 ex 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ 1 < A ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) -> ( ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> ( ( sqrt ` ( D + 1 ) ) + ( sqrt ` D ) ) <_ A ) )
14 13 rexlimdvva 
 |-  ( ( ( D e. ( NN \ []NN ) /\ 1 < A ) /\ A e. RR ) -> ( E. a e. NN0 E. b e. NN0 ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> ( ( sqrt ` ( D + 1 ) ) + ( sqrt ` D ) ) <_ A ) )
15 14 expimpd 
 |-  ( ( D e. ( NN \ []NN ) /\ 1 < A ) -> ( ( A e. RR /\ E. a e. NN0 E. b e. NN0 ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( ( sqrt ` ( D + 1 ) ) + ( sqrt ` D ) ) <_ A ) )
16 2 15 sylbid 
 |-  ( ( D e. ( NN \ []NN ) /\ 1 < A ) -> ( A e. ( Pell1QR ` D ) -> ( ( sqrt ` ( D + 1 ) ) + ( sqrt ` D ) ) <_ A ) )
17 16 ex 
 |-  ( D e. ( NN \ []NN ) -> ( 1 < A -> ( A e. ( Pell1QR ` D ) -> ( ( sqrt ` ( D + 1 ) ) + ( sqrt ` D ) ) <_ A ) ) )
18 17 com23 
 |-  ( D e. ( NN \ []NN ) -> ( A e. ( Pell1QR ` D ) -> ( 1 < A -> ( ( sqrt ` ( D + 1 ) ) + ( sqrt ` D ) ) <_ A ) ) )
19 18 3imp 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1QR ` D ) /\ 1 < A ) -> ( ( sqrt ` ( D + 1 ) ) + ( sqrt ` D ) ) <_ A )