Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  pellfundex Structured version   Visualization version   Unicode version

Theorem pellfundex 35805
Description: The fundamental solution as an infimum is itself a solution, showing that the solution set is discrete.

Since the fundamental solution is an infimum, there must be an element ge to Fund and lt 2*Fund. If this element is equal to the fundamental solution we're done, otherwise use the infimum again to find another element which must be ge Fund and lt the first element; their ratio is a group element in (1,2), contradicting pell14qrgapw 35793. (Contributed by Stefan O'Rear, 18-Sep-2014.)

Assertion
Ref Expression
pellfundex  |-  ( D  e.  ( NN  \NN )  -> 
(PellFund `  D )  e.  (Pell1QR `  D )
)

Proof of Theorem pellfundex
Dummy variables  a 
b are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 2re 10701 . . . 4  |-  2  e.  RR
2 pellfundre 35800 . . . 4  |-  ( D  e.  ( NN  \NN )  -> 
(PellFund `  D )  e.  RR )
3 remulcl 9642 . . . 4  |-  ( ( 2  e.  RR  /\  (PellFund `  D )  e.  RR )  ->  (
2  x.  (PellFund `  D
) )  e.  RR )
41, 2, 3sylancr 676 . . 3  |-  ( D  e.  ( NN  \NN )  -> 
( 2  x.  (PellFund `  D ) )  e.  RR )
5 0red 9662 . . . . . . 7  |-  ( D  e.  ( NN  \NN )  -> 
0  e.  RR )
6 1red 9676 . . . . . . 7  |-  ( D  e.  ( NN  \NN )  -> 
1  e.  RR )
7 0lt1 10157 . . . . . . . 8  |-  0  <  1
87a1i 11 . . . . . . 7  |-  ( D  e.  ( NN  \NN )  -> 
0  <  1 )
9 pellfundgt1 35802 . . . . . . 7  |-  ( D  e.  ( NN  \NN )  -> 
1  <  (PellFund `  D
) )
105, 6, 2, 8, 9lttrd 9813 . . . . . 6  |-  ( D  e.  ( NN  \NN )  -> 
0  <  (PellFund `  D
) )
112, 10elrpd 11361 . . . . 5  |-  ( D  e.  ( NN  \NN )  -> 
(PellFund `  D )  e.  RR+ )
122, 11ltaddrpd 11394 . . . 4  |-  ( D  e.  ( NN  \NN )  -> 
(PellFund `  D )  < 
( (PellFund `  D )  +  (PellFund `  D )
) )
132recnd 9687 . . . . 5  |-  ( D  e.  ( NN  \NN )  -> 
(PellFund `  D )  e.  CC )
14132timesd 10878 . . . 4  |-  ( D  e.  ( NN  \NN )  -> 
( 2  x.  (PellFund `  D ) )  =  ( (PellFund `  D
)  +  (PellFund `  D
) ) )
1512, 14breqtrrd 4422 . . 3  |-  ( D  e.  ( NN  \NN )  -> 
(PellFund `  D )  < 
( 2  x.  (PellFund `  D ) ) )
16 pellfundglb 35804 . . 3  |-  ( ( D  e.  ( NN 
\NN )  /\  ( 2  x.  (PellFund `  D )
)  e.  RR  /\  (PellFund `  D )  < 
( 2  x.  (PellFund `  D ) ) )  ->  E. a  e.  (Pell1QR `  D ) ( (PellFund `  D )  <_  a  /\  a  <  ( 2  x.  (PellFund `  D
) ) ) )
174, 15, 16mpd3an23 1392 . 2  |-  ( D  e.  ( NN  \NN )  ->  E. a  e.  (Pell1QR `  D ) ( (PellFund `  D )  <_  a  /\  a  <  ( 2  x.  (PellFund `  D
) ) ) )
182adantr 472 . . . . . 6  |-  ( ( D  e.  ( NN 
\NN )  /\  a  e.  (Pell1QR `  D ) )  -> 
(PellFund `  D )  e.  RR )
19 pell1qrss14 35785 . . . . . . . 8  |-  ( D  e.  ( NN  \NN )  -> 
(Pell1QR `  D )  C_  (Pell14QR `  D ) )
2019sselda 3418 . . . . . . 7  |-  ( ( D  e.  ( NN 
\NN )  /\  a  e.  (Pell1QR `  D ) )  -> 
a  e.  (Pell14QR `  D
) )
21 pell14qrre 35774 . . . . . . 7  |-  ( ( D  e.  ( NN 
\NN )  /\  a  e.  (Pell14QR `  D ) )  -> 
a  e.  RR )
2220, 21syldan 478 . . . . . 6  |-  ( ( D  e.  ( NN 
\NN )  /\  a  e.  (Pell1QR `  D ) )  -> 
a  e.  RR )
2318, 22leloed 9795 . . . . 5  |-  ( ( D  e.  ( NN 
\NN )  /\  a  e.  (Pell1QR `  D ) )  -> 
( (PellFund `  D )  <_  a  <->  ( (PellFund `  D
)  <  a  \/  (PellFund `  D )  =  a ) ) )
24 simp-4l 784 . . . . . . . . 9  |-  ( ( ( ( ( D  e.  ( NN  \NN )  /\  a  e.  (Pell1QR `  D
) )  /\  (
(PellFund `  D )  < 
a  /\  a  <  ( 2  x.  (PellFund `  D
) ) ) )  /\  b  e.  (Pell1QR `  D ) )  /\  ( (PellFund `  D )  <_  b  /\  b  < 
a ) )  ->  D  e.  ( NN  \NN )
)
25 simp-4r 785 . . . . . . . . 9  |-  ( ( ( ( ( D  e.  ( NN  \NN )  /\  a  e.  (Pell1QR `  D
) )  /\  (
(PellFund `  D )  < 
a  /\  a  <  ( 2  x.  (PellFund `  D
) ) ) )  /\  b  e.  (Pell1QR `  D ) )  /\  ( (PellFund `  D )  <_  b  /\  b  < 
a ) )  -> 
a  e.  (Pell1QR `  D
) )
26 simplr 770 . . . . . . . . 9  |-  ( ( ( ( ( D  e.  ( NN  \NN )  /\  a  e.  (Pell1QR `  D
) )  /\  (
(PellFund `  D )  < 
a  /\  a  <  ( 2  x.  (PellFund `  D
) ) ) )  /\  b  e.  (Pell1QR `  D ) )  /\  ( (PellFund `  D )  <_  b  /\  b  < 
a ) )  -> 
b  e.  (Pell1QR `  D
) )
27 simprr 774 . . . . . . . . 9  |-  ( ( ( ( ( D  e.  ( NN  \NN )  /\  a  e.  (Pell1QR `  D
) )  /\  (
(PellFund `  D )  < 
a  /\  a  <  ( 2  x.  (PellFund `  D
) ) ) )  /\  b  e.  (Pell1QR `  D ) )  /\  ( (PellFund `  D )  <_  b  /\  b  < 
a ) )  -> 
b  <  a )
2822ad3antrrr 744 . . . . . . . . . 10  |-  ( ( ( ( ( D  e.  ( NN  \NN )  /\  a  e.  (Pell1QR `  D
) )  /\  (
(PellFund `  D )  < 
a  /\  a  <  ( 2  x.  (PellFund `  D
) ) ) )  /\  b  e.  (Pell1QR `  D ) )  /\  ( (PellFund `  D )  <_  b  /\  b  < 
a ) )  -> 
a  e.  RR )
294ad4antr 746 . . . . . . . . . 10  |-  ( ( ( ( ( D  e.  ( NN  \NN )  /\  a  e.  (Pell1QR `  D
) )  /\  (
(PellFund `  D )  < 
a  /\  a  <  ( 2  x.  (PellFund `  D
) ) ) )  /\  b  e.  (Pell1QR `  D ) )  /\  ( (PellFund `  D )  <_  b  /\  b  < 
a ) )  -> 
( 2  x.  (PellFund `  D ) )  e.  RR )
3019ad4antr 746 . . . . . . . . . . . . 13  |-  ( ( ( ( ( D  e.  ( NN  \NN )  /\  a  e.  (Pell1QR `  D
) )  /\  (
(PellFund `  D )  < 
a  /\  a  <  ( 2  x.  (PellFund `  D
) ) ) )  /\  b  e.  (Pell1QR `  D ) )  /\  ( (PellFund `  D )  <_  b  /\  b  < 
a ) )  -> 
(Pell1QR `  D )  C_  (Pell14QR `  D ) )
3130, 26sseldd 3419 . . . . . . . . . . . 12  |-  ( ( ( ( ( D  e.  ( NN  \NN )  /\  a  e.  (Pell1QR `  D
) )  /\  (
(PellFund `  D )  < 
a  /\  a  <  ( 2  x.  (PellFund `  D
) ) ) )  /\  b  e.  (Pell1QR `  D ) )  /\  ( (PellFund `  D )  <_  b  /\  b  < 
a ) )  -> 
b  e.  (Pell14QR `  D
) )
32 pell14qrre 35774 . . . . . . . . . . . 12  |-  ( ( D  e.  ( NN 
\NN )  /\  b  e.  (Pell14QR `  D ) )  -> 
b  e.  RR )
3324, 31, 32syl2anc 673 . . . . . . . . . . 11  |-  ( ( ( ( ( D  e.  ( NN  \NN )  /\  a  e.  (Pell1QR `  D
) )  /\  (
(PellFund `  D )  < 
a  /\  a  <  ( 2  x.  (PellFund `  D
) ) ) )  /\  b  e.  (Pell1QR `  D ) )  /\  ( (PellFund `  D )  <_  b  /\  b  < 
a ) )  -> 
b  e.  RR )
34 remulcl 9642 . . . . . . . . . . 11  |-  ( ( 2  e.  RR  /\  b  e.  RR )  ->  ( 2  x.  b
)  e.  RR )
351, 33, 34sylancr 676 . . . . . . . . . 10  |-  ( ( ( ( ( D  e.  ( NN  \NN )  /\  a  e.  (Pell1QR `  D
) )  /\  (
(PellFund `  D )  < 
a  /\  a  <  ( 2  x.  (PellFund `  D
) ) ) )  /\  b  e.  (Pell1QR `  D ) )  /\  ( (PellFund `  D )  <_  b  /\  b  < 
a ) )  -> 
( 2  x.  b
)  e.  RR )
36 simprr 774 . . . . . . . . . . 11  |-  ( ( ( D  e.  ( NN  \NN )  /\  a  e.  (Pell1QR `  D )
)  /\  ( (PellFund `  D )  <  a  /\  a  <  ( 2  x.  (PellFund `  D
) ) ) )  ->  a  <  (
2  x.  (PellFund `  D
) ) )
3736ad2antrr 740 . . . . . . . . . 10  |-  ( ( ( ( ( D  e.  ( NN  \NN )  /\  a  e.  (Pell1QR `  D
) )  /\  (
(PellFund `  D )  < 
a  /\  a  <  ( 2  x.  (PellFund `  D
) ) ) )  /\  b  e.  (Pell1QR `  D ) )  /\  ( (PellFund `  D )  <_  b  /\  b  < 
a ) )  -> 
a  <  ( 2  x.  (PellFund `  D
) ) )
38 simprl 772 . . . . . . . . . . 11  |-  ( ( ( ( ( D  e.  ( NN  \NN )  /\  a  e.  (Pell1QR `  D
) )  /\  (
(PellFund `  D )  < 
a  /\  a  <  ( 2  x.  (PellFund `  D
) ) ) )  /\  b  e.  (Pell1QR `  D ) )  /\  ( (PellFund `  D )  <_  b  /\  b  < 
a ) )  -> 
(PellFund `  D )  <_ 
b )
392ad4antr 746 . . . . . . . . . . . 12  |-  ( ( ( ( ( D  e.  ( NN  \NN )  /\  a  e.  (Pell1QR `  D
) )  /\  (
(PellFund `  D )  < 
a  /\  a  <  ( 2  x.  (PellFund `  D
) ) ) )  /\  b  e.  (Pell1QR `  D ) )  /\  ( (PellFund `  D )  <_  b  /\  b  < 
a ) )  -> 
(PellFund `  D )  e.  RR )
401a1i 11 . . . . . . . . . . . 12  |-  ( ( ( ( ( D  e.  ( NN  \NN )  /\  a  e.  (Pell1QR `  D
) )  /\  (
(PellFund `  D )  < 
a  /\  a  <  ( 2  x.  (PellFund `  D
) ) ) )  /\  b  e.  (Pell1QR `  D ) )  /\  ( (PellFund `  D )  <_  b  /\  b  < 
a ) )  -> 
2  e.  RR )
41 2pos 10723 . . . . . . . . . . . . 13  |-  0  <  2
4241a1i 11 . . . . . . . . . . . 12  |-  ( ( ( ( ( D  e.  ( NN  \NN )  /\  a  e.  (Pell1QR `  D
) )  /\  (
(PellFund `  D )  < 
a  /\  a  <  ( 2  x.  (PellFund `  D
) ) ) )  /\  b  e.  (Pell1QR `  D ) )  /\  ( (PellFund `  D )  <_  b  /\  b  < 
a ) )  -> 
0  <  2 )
43 lemul2 10480 . . . . . . . . . . . 12  |-  ( ( (PellFund `  D )  e.  RR  /\  b  e.  RR  /\  ( 2  e.  RR  /\  0  <  2 ) )  -> 
( (PellFund `  D )  <_  b  <->  ( 2  x.  (PellFund `  D )
)  <_  ( 2  x.  b ) ) )
4439, 33, 40, 42, 43syl112anc 1296 . . . . . . . . . . 11  |-  ( ( ( ( ( D  e.  ( NN  \NN )  /\  a  e.  (Pell1QR `  D
) )  /\  (
(PellFund `  D )  < 
a  /\  a  <  ( 2  x.  (PellFund `  D
) ) ) )  /\  b  e.  (Pell1QR `  D ) )  /\  ( (PellFund `  D )  <_  b  /\  b  < 
a ) )  -> 
( (PellFund `  D )  <_  b  <->  ( 2  x.  (PellFund `  D )
)  <_  ( 2  x.  b ) ) )
4538, 44mpbid 215 . . . . . . . . . 10  |-  ( ( ( ( ( D  e.  ( NN  \NN )  /\  a  e.  (Pell1QR `  D
) )  /\  (
(PellFund `  D )  < 
a  /\  a  <  ( 2  x.  (PellFund `  D
) ) ) )  /\  b  e.  (Pell1QR `  D ) )  /\  ( (PellFund `  D )  <_  b  /\  b  < 
a ) )  -> 
( 2  x.  (PellFund `  D ) )  <_ 
( 2  x.  b
) )
4628, 29, 35, 37, 45ltletrd 9812 . . . . . . . . 9  |-  ( ( ( ( ( D  e.  ( NN  \NN )  /\  a  e.  (Pell1QR `  D
) )  /\  (
(PellFund `  D )  < 
a  /\  a  <  ( 2  x.  (PellFund `  D
) ) ) )  /\  b  e.  (Pell1QR `  D ) )  /\  ( (PellFund `  D )  <_  b  /\  b  < 
a ) )  -> 
a  <  ( 2  x.  b ) )
47 simp1 1030 . . . . . . . . . 10  |-  ( ( D  e.  ( NN 
\NN )  /\  ( a  e.  (Pell1QR `  D )  /\  b  e.  (Pell1QR `  D ) )  /\  ( b  <  a  /\  a  <  ( 2  x.  b ) ) )  ->  D  e.  ( NN  \NN ) )
48193ad2ant1 1051 . . . . . . . . . . . 12  |-  ( ( D  e.  ( NN 
\NN )  /\  ( a  e.  (Pell1QR `  D )  /\  b  e.  (Pell1QR `  D ) )  /\  ( b  <  a  /\  a  <  ( 2  x.  b ) ) )  ->  (Pell1QR `  D
)  C_  (Pell14QR `  D
) )
49 simp2l 1056 . . . . . . . . . . . 12  |-  ( ( D  e.  ( NN 
\NN )  /\  ( a  e.  (Pell1QR `  D )  /\  b  e.  (Pell1QR `  D ) )  /\  ( b  <  a  /\  a  <  ( 2  x.  b ) ) )  ->  a  e.  (Pell1QR `  D ) )
5048, 49sseldd 3419 . . . . . . . . . . 11  |-  ( ( D  e.  ( NN 
\NN )  /\  ( a  e.  (Pell1QR `  D )  /\  b  e.  (Pell1QR `  D ) )  /\  ( b  <  a  /\  a  <  ( 2  x.  b ) ) )  ->  a  e.  (Pell14QR `  D ) )
51 simp2r 1057 . . . . . . . . . . . 12  |-  ( ( D  e.  ( NN 
\NN )  /\  ( a  e.  (Pell1QR `  D )  /\  b  e.  (Pell1QR `  D ) )  /\  ( b  <  a  /\  a  <  ( 2  x.  b ) ) )  ->  b  e.  (Pell1QR `  D ) )
5248, 51sseldd 3419 . . . . . . . . . . 11  |-  ( ( D  e.  ( NN 
\NN )  /\  ( a  e.  (Pell1QR `  D )  /\  b  e.  (Pell1QR `  D ) )  /\  ( b  <  a  /\  a  <  ( 2  x.  b ) ) )  ->  b  e.  (Pell14QR `  D ) )
53 pell14qrdivcl 35782 . . . . . . . . . . 11  |-  ( ( D  e.  ( NN 
\NN )  /\  a  e.  (Pell14QR `  D )  /\  b  e.  (Pell14QR `  D )
)  ->  ( a  /  b )  e.  (Pell14QR `  D )
)
5447, 50, 52, 53syl3anc 1292 . . . . . . . . . 10  |-  ( ( D  e.  ( NN 
\NN )  /\  ( a  e.  (Pell1QR `  D )  /\  b  e.  (Pell1QR `  D ) )  /\  ( b  <  a  /\  a  <  ( 2  x.  b ) ) )  ->  ( a  /  b )  e.  (Pell14QR `  D )
)
5547, 52, 32syl2anc 673 . . . . . . . . . . . . . 14  |-  ( ( D  e.  ( NN 
\NN )  /\  ( a  e.  (Pell1QR `  D )  /\  b  e.  (Pell1QR `  D ) )  /\  ( b  <  a  /\  a  <  ( 2  x.  b ) ) )  ->  b  e.  RR )
5655recnd 9687 . . . . . . . . . . . . 13  |-  ( ( D  e.  ( NN 
\NN )  /\  ( a  e.  (Pell1QR `  D )  /\  b  e.  (Pell1QR `  D ) )  /\  ( b  <  a  /\  a  <  ( 2  x.  b ) ) )  ->  b  e.  CC )
5756mulid2d 9679 . . . . . . . . . . . 12  |-  ( ( D  e.  ( NN 
\NN )  /\  ( a  e.  (Pell1QR `  D )  /\  b  e.  (Pell1QR `  D ) )  /\  ( b  <  a  /\  a  <  ( 2  x.  b ) ) )  ->  ( 1  x.  b )  =  b )
58 simp3l 1058 . . . . . . . . . . . 12  |-  ( ( D  e.  ( NN 
\NN )  /\  ( a  e.  (Pell1QR `  D )  /\  b  e.  (Pell1QR `  D ) )  /\  ( b  <  a  /\  a  <  ( 2  x.  b ) ) )  ->  b  <  a )
5957, 58eqbrtrd 4416 . . . . . . . . . . 11  |-  ( ( D  e.  ( NN 
\NN )  /\  ( a  e.  (Pell1QR `  D )  /\  b  e.  (Pell1QR `  D ) )  /\  ( b  <  a  /\  a  <  ( 2  x.  b ) ) )  ->  ( 1  x.  b )  < 
a )
60 1red 9676 . . . . . . . . . . . 12  |-  ( ( D  e.  ( NN 
\NN )  /\  ( a  e.  (Pell1QR `  D )  /\  b  e.  (Pell1QR `  D ) )  /\  ( b  <  a  /\  a  <  ( 2  x.  b ) ) )  ->  1  e.  RR )
6147, 50, 21syl2anc 673 . . . . . . . . . . . 12  |-  ( ( D  e.  ( NN 
\NN )  /\  ( a  e.  (Pell1QR `  D )  /\  b  e.  (Pell1QR `  D ) )  /\  ( b  <  a  /\  a  <  ( 2  x.  b ) ) )  ->  a  e.  RR )
62 pell14qrgt0 35776 . . . . . . . . . . . . 13  |-  ( ( D  e.  ( NN 
\NN )  /\  b  e.  (Pell14QR `  D ) )  -> 
0  <  b )
6347, 52, 62syl2anc 673 . . . . . . . . . . . 12  |-  ( ( D  e.  ( NN 
\NN )  /\  ( a  e.  (Pell1QR `  D )  /\  b  e.  (Pell1QR `  D ) )  /\  ( b  <  a  /\  a  <  ( 2  x.  b ) ) )  ->  0  <  b )
64 ltmuldiv 10500 . . . . . . . . . . . 12  |-  ( ( 1  e.  RR  /\  a  e.  RR  /\  (
b  e.  RR  /\  0  <  b ) )  ->  ( ( 1  x.  b )  < 
a  <->  1  <  (
a  /  b ) ) )
6560, 61, 55, 63, 64syl112anc 1296 . . . . . . . . . . 11  |-  ( ( D  e.  ( NN 
\NN )  /\  ( a  e.  (Pell1QR `  D )  /\  b  e.  (Pell1QR `  D ) )  /\  ( b  <  a  /\  a  <  ( 2  x.  b ) ) )  ->  ( (
1  x.  b )  <  a  <->  1  <  ( a  /  b ) ) )
6659, 65mpbid 215 . . . . . . . . . 10  |-  ( ( D  e.  ( NN 
\NN )  /\  ( a  e.  (Pell1QR `  D )  /\  b  e.  (Pell1QR `  D ) )  /\  ( b  <  a  /\  a  <  ( 2  x.  b ) ) )  ->  1  <  ( a  /  b ) )
67 simp3r 1059 . . . . . . . . . . 11  |-  ( ( D  e.  ( NN 
\NN )  /\  ( a  e.  (Pell1QR `  D )  /\  b  e.  (Pell1QR `  D ) )  /\  ( b  <  a  /\  a  <  ( 2  x.  b ) ) )  ->  a  <  ( 2  x.  b ) )
681a1i 11 . . . . . . . . . . . 12  |-  ( ( D  e.  ( NN 
\NN )  /\  ( a  e.  (Pell1QR `  D )  /\  b  e.  (Pell1QR `  D ) )  /\  ( b  <  a  /\  a  <  ( 2  x.  b ) ) )  ->  2  e.  RR )
69 ltdivmul2 10504 . . . . . . . . . . . 12  |-  ( ( a  e.  RR  /\  2  e.  RR  /\  (
b  e.  RR  /\  0  <  b ) )  ->  ( ( a  /  b )  <  2  <->  a  <  (
2  x.  b ) ) )
7061, 68, 55, 63, 69syl112anc 1296 . . . . . . . . . . 11  |-  ( ( D  e.  ( NN 
\NN )  /\  ( a  e.  (Pell1QR `  D )  /\  b  e.  (Pell1QR `  D ) )  /\  ( b  <  a  /\  a  <  ( 2  x.  b ) ) )  ->  ( (
a  /  b )  <  2  <->  a  <  ( 2  x.  b ) ) )
7167, 70mpbird 240 . . . . . . . . . 10  |-  ( ( D  e.  ( NN 
\NN )  /\  ( a  e.  (Pell1QR `  D )  /\  b  e.  (Pell1QR `  D ) )  /\  ( b  <  a  /\  a  <  ( 2  x.  b ) ) )  ->  ( a  /  b )  <  2 )
72 simprr 774 . . . . . . . . . . 11  |-  ( ( ( D  e.  ( NN  \NN )  /\  ( a  /  b )  e.  (Pell14QR `  D )
)  /\  ( 1  <  ( a  / 
b )  /\  (
a  /  b )  <  2 ) )  ->  ( a  / 
b )  <  2
)
73 simpll 768 . . . . . . . . . . . . 13  |-  ( ( ( D  e.  ( NN  \NN )  /\  ( a  /  b )  e.  (Pell14QR `  D )
)  /\  ( 1  <  ( a  / 
b )  /\  (
a  /  b )  <  2 ) )  ->  D  e.  ( NN  \NN ) )
74 simplr 770 . . . . . . . . . . . . 13  |-  ( ( ( D  e.  ( NN  \NN )  /\  ( a  /  b )  e.  (Pell14QR `  D )
)  /\  ( 1  <  ( a  / 
b )  /\  (
a  /  b )  <  2 ) )  ->  ( a  / 
b )  e.  (Pell14QR `  D ) )
75 simprl 772 . . . . . . . . . . . . 13  |-  ( ( ( D  e.  ( NN  \NN )  /\  ( a  /  b )  e.  (Pell14QR `  D )
)  /\  ( 1  <  ( a  / 
b )  /\  (
a  /  b )  <  2 ) )  ->  1  <  (
a  /  b ) )
76 pell14qrgapw 35793 . . . . . . . . . . . . 13  |-  ( ( D  e.  ( NN 
\NN )  /\  ( a  / 
b )  e.  (Pell14QR `  D )  /\  1  <  ( a  /  b
) )  ->  2  <  ( a  /  b
) )
7773, 74, 75, 76syl3anc 1292 . . . . . . . . . . . 12  |-  ( ( ( D  e.  ( NN  \NN )  /\  ( a  /  b )  e.  (Pell14QR `  D )
)  /\  ( 1  <  ( a  / 
b )  /\  (
a  /  b )  <  2 ) )  ->  2  <  (
a  /  b ) )
78 pell14qrre 35774 . . . . . . . . . . . . . 14  |-  ( ( D  e.  ( NN 
\NN )  /\  ( a  / 
b )  e.  (Pell14QR `  D ) )  -> 
( a  /  b
)  e.  RR )
7978adantr 472 . . . . . . . . . . . . 13  |-  ( ( ( D  e.  ( NN  \NN )  /\  ( a  /  b )  e.  (Pell14QR `  D )
)  /\  ( 1  <  ( a  / 
b )  /\  (
a  /  b )  <  2 ) )  ->  ( a  / 
b )  e.  RR )
80 ltnsym 9750 . . . . . . . . . . . . 13  |-  ( ( 2  e.  RR  /\  ( a  /  b
)  e.  RR )  ->  ( 2  < 
( a  /  b
)  ->  -.  (
a  /  b )  <  2 ) )
811, 79, 80sylancr 676 . . . . . . . . . . . 12  |-  ( ( ( D  e.  ( NN  \NN )  /\  ( a  /  b )  e.  (Pell14QR `  D )
)  /\  ( 1  <  ( a  / 
b )  /\  (
a  /  b )  <  2 ) )  ->  ( 2  < 
( a  /  b
)  ->  -.  (
a  /  b )  <  2 ) )
8277, 81mpd 15 . . . . . . . . . . 11  |-  ( ( ( D  e.  ( NN  \NN )  /\  ( a  /  b )  e.  (Pell14QR `  D )
)  /\  ( 1  <  ( a  / 
b )  /\  (
a  /  b )  <  2 ) )  ->  -.  ( a  /  b )  <  2 )
8372, 82pm2.21dd 179 . . . . . . . . . 10  |-  ( ( ( D  e.  ( NN  \NN )  /\  ( a  /  b )  e.  (Pell14QR `  D )
)  /\  ( 1  <  ( a  / 
b )  /\  (
a  /  b )  <  2 ) )  ->  (PellFund `  D )  e.  (Pell1QR `  D )
)
8447, 54, 66, 71, 83syl22anc 1293 . . . . . . . . 9  |-  ( ( D  e.  ( NN 
\NN )  /\  ( a  e.  (Pell1QR `  D )  /\  b  e.  (Pell1QR `  D ) )  /\  ( b  <  a  /\  a  <  ( 2  x.  b ) ) )  ->  (PellFund `  D
)  e.  (Pell1QR `  D
) )
8524, 25, 26, 27, 46, 84syl122anc 1301 . . . . . . . 8  |-  ( ( ( ( ( D  e.  ( NN  \NN )  /\  a  e.  (Pell1QR `  D
) )  /\  (
(PellFund `  D )  < 
a  /\  a  <  ( 2  x.  (PellFund `  D
) ) ) )  /\  b  e.  (Pell1QR `  D ) )  /\  ( (PellFund `  D )  <_  b  /\  b  < 
a ) )  -> 
(PellFund `  D )  e.  (Pell1QR `  D )
)
86 simpll 768 . . . . . . . . 9  |-  ( ( ( D  e.  ( NN  \NN )  /\  a  e.  (Pell1QR `  D )
)  /\  ( (PellFund `  D )  <  a  /\  a  <  ( 2  x.  (PellFund `  D
) ) ) )  ->  D  e.  ( NN  \NN ) )
8722adantr 472 . . . . . . . . 9  |-  ( ( ( D  e.  ( NN  \NN )  /\  a  e.  (Pell1QR `  D )
)  /\  ( (PellFund `  D )  <  a  /\  a  <  ( 2  x.  (PellFund `  D
) ) ) )  ->  a  e.  RR )
88 simprl 772 . . . . . . . . 9  |-  ( ( ( D  e.  ( NN  \NN )  /\  a  e.  (Pell1QR `  D )
)  /\  ( (PellFund `  D )  <  a  /\  a  <  ( 2  x.  (PellFund `  D
) ) ) )  ->  (PellFund `  D )  <  a )
89 pellfundglb 35804 . . . . . . . . 9  |-  ( ( D  e.  ( NN 
\NN )  /\  a  e.  RR  /\  (PellFund `  D )  <  a )  ->  E. b  e.  (Pell1QR `  D )
( (PellFund `  D )  <_  b  /\  b  < 
a ) )
9086, 87, 88, 89syl3anc 1292 . . . . . . . 8  |-  ( ( ( D  e.  ( NN  \NN )  /\  a  e.  (Pell1QR `  D )
)  /\  ( (PellFund `  D )  <  a  /\  a  <  ( 2  x.  (PellFund `  D
) ) ) )  ->  E. b  e.  (Pell1QR `  D ) ( (PellFund `  D )  <_  b  /\  b  <  a ) )
9185, 90r19.29a 2918 . . . . . . 7  |-  ( ( ( D  e.  ( NN  \NN )  /\  a  e.  (Pell1QR `  D )
)  /\  ( (PellFund `  D )  <  a  /\  a  <  ( 2  x.  (PellFund `  D
) ) ) )  ->  (PellFund `  D )  e.  (Pell1QR `  D )
)
9291exp32 616 . . . . . 6  |-  ( ( D  e.  ( NN 
\NN )  /\  a  e.  (Pell1QR `  D ) )  -> 
( (PellFund `  D )  <  a  ->  ( a  <  ( 2  x.  (PellFund `  D ) )  -> 
(PellFund `  D )  e.  (Pell1QR `  D )
) ) )
93 simp2 1031 . . . . . . . 8  |-  ( ( ( D  e.  ( NN  \NN )  /\  a  e.  (Pell1QR `  D )
)  /\  (PellFund `  D
)  =  a  /\  a  <  ( 2  x.  (PellFund `  D )
) )  ->  (PellFund `  D )  =  a )
94 simp1r 1055 . . . . . . . 8  |-  ( ( ( D  e.  ( NN  \NN )  /\  a  e.  (Pell1QR `  D )
)  /\  (PellFund `  D
)  =  a  /\  a  <  ( 2  x.  (PellFund `  D )
) )  ->  a  e.  (Pell1QR `  D )
)
9593, 94eqeltrd 2549 . . . . . . 7  |-  ( ( ( D  e.  ( NN  \NN )  /\  a  e.  (Pell1QR `  D )
)  /\  (PellFund `  D
)  =  a  /\  a  <  ( 2  x.  (PellFund `  D )
) )  ->  (PellFund `  D )  e.  (Pell1QR `  D ) )
96953exp 1230 . . . . . 6  |-  ( ( D  e.  ( NN 
\NN )  /\  a  e.  (Pell1QR `  D ) )  -> 
( (PellFund `  D )  =  a  ->  ( a  <  ( 2  x.  (PellFund `  D )
)  ->  (PellFund `  D
)  e.  (Pell1QR `  D
) ) ) )
9792, 96jaod 387 . . . . 5  |-  ( ( D  e.  ( NN 
\NN )  /\  a  e.  (Pell1QR `  D ) )  -> 
( ( (PellFund `  D
)  <  a  \/  (PellFund `  D )  =  a )  ->  (
a  <  ( 2  x.  (PellFund `  D
) )  ->  (PellFund `  D )  e.  (Pell1QR `  D ) ) ) )
9823, 97sylbid 223 . . . 4  |-  ( ( D  e.  ( NN 
\NN )  /\  a  e.  (Pell1QR `  D ) )  -> 
( (PellFund `  D )  <_  a  ->  ( a  <  ( 2  x.  (PellFund `  D ) )  -> 
(PellFund `  D )  e.  (Pell1QR `  D )
) ) )
9998impd 438 . . 3  |-  ( ( D  e.  ( NN 
\NN )  /\  a  e.  (Pell1QR `  D ) )  -> 
( ( (PellFund `  D
)  <_  a  /\  a  <  ( 2  x.  (PellFund `  D )
) )  ->  (PellFund `  D )  e.  (Pell1QR `  D ) ) )
10099rexlimdva 2871 . 2  |-  ( D  e.  ( NN  \NN )  -> 
( E. a  e.  (Pell1QR `  D )
( (PellFund `  D )  <_  a  /\  a  < 
( 2  x.  (PellFund `  D ) ) )  ->  (PellFund `  D )  e.  (Pell1QR `  D )
) )
10117, 100mpd 15 1  |-  ( D  e.  ( NN  \NN )  -> 
(PellFund `  D )  e.  (Pell1QR `  D )
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 189    \/ wo 375    /\ wa 376    /\ w3a 1007    = wceq 1452    e. wcel 1904   E.wrex 2757    \ cdif 3387    C_ wss 3390   class class class wbr 4395   ` cfv 5589  (class class class)co 6308   RRcr 9556   0cc0 9557   1c1 9558    + caddc 9560    x. cmul 9562    < clt 9693    <_ cle 9694    / cdiv 10291   NNcn 10631   2c2 10681  ◻NNcsquarenn 35751  Pell1QRcpell1qr 35752  Pell14QRcpell14qr 35754  PellFundcpellfund 35755
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602  ax-inf2 8164  ax-cnex 9613  ax-resscn 9614  ax-1cn 9615  ax-icn 9616  ax-addcl 9617  ax-addrcl 9618  ax-mulcl 9619  ax-mulrcl 9620  ax-mulcom 9621  ax-addass 9622  ax-mulass 9623  ax-distr 9624  ax-i2m1 9625  ax-1ne0 9626  ax-1rid 9627  ax-rnegex 9628  ax-rrecex 9629  ax-cnre 9630  ax-pre-lttri 9631  ax-pre-lttrn 9632  ax-pre-ltadd 9633  ax-pre-mulgt0 9634  ax-pre-sup 9635
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-nel 2644  df-ral 2761  df-rex 2762  df-reu 2763  df-rmo 2764  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4191  df-int 4227  df-iun 4271  df-br 4396  df-opab 4455  df-mpt 4456  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-se 4799  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-pred 5387  df-ord 5433  df-on 5434  df-lim 5435  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-isom 5598  df-riota 6270  df-ov 6311  df-oprab 6312  df-mpt2 6313  df-om 6712  df-1st 6812  df-2nd 6813  df-wrecs 7046  df-recs 7108  df-rdg 7146  df-1o 7200  df-oadd 7204  df-omul 7205  df-er 7381  df-map 7492  df-en 7588  df-dom 7589  df-sdom 7590  df-fin 7591  df-sup 7974  df-inf 7975  df-oi 8043  df-card 8391  df-acn 8394  df-pnf 9695  df-mnf 9696  df-xr 9697  df-ltxr 9698  df-le 9699  df-sub 9882  df-neg 9883  df-div 10292  df-nn 10632  df-2 10690  df-3 10691  df-n0 10894  df-z 10962  df-uz 11183  df-q 11288  df-rp 11326  df-ico 11666  df-fz 11811  df-fl 12061  df-mod 12130  df-seq 12252  df-exp 12311  df-hash 12554  df-cj 13239  df-re 13240  df-im 13241  df-sqrt 13375  df-abs 13376  df-dvds 14383  df-gcd 14548  df-numer 14763  df-denom 14764  df-squarenn 35757  df-pell1qr 35758  df-pell14qr 35759  df-pell1234qr 35760  df-pellfund 35761
This theorem is referenced by:  pellfund14  35817  pellfund14b  35818
  Copyright terms: Public domain W3C validator