Metamath Proof Explorer

Theorem pellfund14gap

Description: There are no solutions between 1 and the fundamental solution. (Contributed by Stefan O'Rear, 18-Sep-2014)

Ref Expression
Assertion pellfund14gap 
|- ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ ( 1 <_ A /\ A < ( PellFund ` D ) ) ) -> A = 1 )

Proof

Step Hyp Ref Expression
1 simp3r 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ ( 1 <_ A /\ A < ( PellFund ` D ) ) ) -> A < ( PellFund ` D ) )
2 pell14qrre 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> A e. RR )
3 2 3adant3 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ ( 1 <_ A /\ A < ( PellFund ` D ) ) ) -> A e. RR )
4 pellfundre 
 |-  ( D e. ( NN \ []NN ) -> ( PellFund ` D ) e. RR )
5 4 3ad2ant1 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ ( 1 <_ A /\ A < ( PellFund ` D ) ) ) -> ( PellFund ` D ) e. RR )
6 3 5 ltnled 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ ( 1 <_ A /\ A < ( PellFund ` D ) ) ) -> ( A < ( PellFund ` D ) <-> -. ( PellFund ` D ) <_ A ) )
7 1 6 mpbid 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ ( 1 <_ A /\ A < ( PellFund ` D ) ) ) -> -. ( PellFund ` D ) <_ A )
8 simpl1 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ ( 1 <_ A /\ A < ( PellFund ` D ) ) ) /\ 1 < A ) -> D e. ( NN \ []NN ) )
9 simpl2 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ ( 1 <_ A /\ A < ( PellFund ` D ) ) ) /\ 1 < A ) -> A e. ( Pell14QR ` D ) )
10 simpr 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ ( 1 <_ A /\ A < ( PellFund ` D ) ) ) /\ 1 < A ) -> 1 < A )
11 pellfundlb 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ 1 < A ) -> ( PellFund ` D ) <_ A )
12 8 9 10 11 syl3anc 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ ( 1 <_ A /\ A < ( PellFund ` D ) ) ) /\ 1 < A ) -> ( PellFund ` D ) <_ A )
13 7 12 mtand 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ ( 1 <_ A /\ A < ( PellFund ` D ) ) ) -> -. 1 < A )
14 simp3l 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ ( 1 <_ A /\ A < ( PellFund ` D ) ) ) -> 1 <_ A )
15 1re 
 |-  1 e. RR
16 leloe 
 |-  ( ( 1 e. RR /\ A e. RR ) -> ( 1 <_ A <-> ( 1 < A \/ 1 = A ) ) )
17 15 3 16 sylancr 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ ( 1 <_ A /\ A < ( PellFund ` D ) ) ) -> ( 1 <_ A <-> ( 1 < A \/ 1 = A ) ) )
18 14 17 mpbid 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ ( 1 <_ A /\ A < ( PellFund ` D ) ) ) -> ( 1 < A \/ 1 = A ) )
19 orel1 
 |-  ( -. 1 < A -> ( ( 1 < A \/ 1 = A ) -> 1 = A ) )
20 13 18 19 sylc 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ ( 1 <_ A /\ A < ( PellFund ` D ) ) ) -> 1 = A )
21 20 eqcomd 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ ( 1 <_ A /\ A < ( PellFund ` D ) ) ) -> A = 1 )