Metamath Proof Explorer

Theorem pellfundex

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 . (Contributed by Stefan O'Rear, 18-Sep-2014)

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

Proof

Step Hyp Ref Expression
1 2re 
 |-  2 e. RR
2 pellfundre 
 |-  ( D e. ( NN \ []NN ) -> ( PellFund ` D ) e. RR )
3 remulcl 
 |-  ( ( 2 e. RR /\ ( PellFund ` D ) e. RR ) -> ( 2 x. ( PellFund ` D ) ) e. RR )
4 1 2 3 sylancr 
 |-  ( D e. ( NN \ []NN ) -> ( 2 x. ( PellFund ` D ) ) e. RR )
5 0red 
 |-  ( D e. ( NN \ []NN ) -> 0 e. RR )
6 1red 
 |-  ( D e. ( NN \ []NN ) -> 1 e. RR )
7 0lt1 
 |-  0 < 1
8 7 a1i 
 |-  ( D e. ( NN \ []NN ) -> 0 < 1 )
9 pellfundgt1 
 |-  ( D e. ( NN \ []NN ) -> 1 < ( PellFund ` D ) )
10 5 6 2 8 9 lttrd 
 |-  ( D e. ( NN \ []NN ) -> 0 < ( PellFund ` D ) )
11 2 10 elrpd 
 |-  ( D e. ( NN \ []NN ) -> ( PellFund ` D ) e. RR+ )
12 2 11 ltaddrpd 
 |-  ( D e. ( NN \ []NN ) -> ( PellFund ` D ) < ( ( PellFund ` D ) + ( PellFund ` D ) ) )
13 2 recnd 
 |-  ( D e. ( NN \ []NN ) -> ( PellFund ` D ) e. CC )
14 13 2timesd 
 |-  ( D e. ( NN \ []NN ) -> ( 2 x. ( PellFund ` D ) ) = ( ( PellFund ` D ) + ( PellFund ` D ) ) )
15 12 14 breqtrrd 
 |-  ( D e. ( NN \ []NN ) -> ( PellFund ` D ) < ( 2 x. ( PellFund ` D ) ) )
16 pellfundglb 
 |-  ( ( 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 ) ) ) )
17 4 15 16 mpd3an23 
 |-  ( D e. ( NN \ []NN ) -> E. a e. ( Pell1QR ` D ) ( ( PellFund ` D ) <_ a /\ a < ( 2 x. ( PellFund ` D ) ) ) )
18 2 adantr 
 |-  ( ( D e. ( NN \ []NN ) /\ a e. ( Pell1QR ` D ) ) -> ( PellFund ` D ) e. RR )
19 pell1qrss14 
 |-  ( D e. ( NN \ []NN ) -> ( Pell1QR ` D ) C_ ( Pell14QR ` D ) )
20 19 sselda 
 |-  ( ( D e. ( NN \ []NN ) /\ a e. ( Pell1QR ` D ) ) -> a e. ( Pell14QR ` D ) )
21 pell14qrre 
 |-  ( ( D e. ( NN \ []NN ) /\ a e. ( Pell14QR ` D ) ) -> a e. RR )
22 20 21 syldan 
 |-  ( ( D e. ( NN \ []NN ) /\ a e. ( Pell1QR ` D ) ) -> a e. RR )
23 18 22 leloed 
 |-  ( ( D e. ( NN \ []NN ) /\ a e. ( Pell1QR ` D ) ) -> ( ( PellFund ` D ) <_ a <-> ( ( PellFund ` D ) < a \/ ( PellFund ` D ) = a ) ) )
24 simp-4l 
 |-  ( ( ( ( ( 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 
 |-  ( ( ( ( ( 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 
 |-  ( ( ( ( ( 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 
 |-  ( ( ( ( ( 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 )
28 22 ad3antrrr 
 |-  ( ( ( ( ( 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 )
29 4 ad4antr 
 |-  ( ( ( ( ( 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 )
30 19 ad4antr 
 |-  ( ( ( ( ( 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 ) )
31 30 26 sseldd 
 |-  ( ( ( ( ( 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 
 |-  ( ( D e. ( NN \ []NN ) /\ b e. ( Pell14QR ` D ) ) -> b e. RR )
33 24 31 32 syl2anc 
 |-  ( ( ( ( ( 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 
 |-  ( ( 2 e. RR /\ b e. RR ) -> ( 2 x. b ) e. RR )
35 1 33 34 sylancr 
 |-  ( ( ( ( ( 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 
 |-  ( ( ( D e. ( NN \ []NN ) /\ a e. ( Pell1QR ` D ) ) /\ ( ( PellFund ` D ) < a /\ a < ( 2 x. ( PellFund ` D ) ) ) ) -> a < ( 2 x. ( PellFund ` D ) ) )
37 36 ad2antrr 
 |-  ( ( ( ( ( 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 
 |-  ( ( ( ( ( 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 )
39 2 ad4antr 
 |-  ( ( ( ( ( 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 )
40 1 a1i 
 |-  ( ( ( ( ( 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 
 |-  0 < 2
42 41 a1i 
 |-  ( ( ( ( ( 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 
 |-  ( ( ( PellFund ` D ) e. RR /\ b e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( PellFund ` D ) <_ b <-> ( 2 x. ( PellFund ` D ) ) <_ ( 2 x. b ) ) )
44 39 33 40 42 43 syl112anc 
 |-  ( ( ( ( ( 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 ) ) )
45 38 44 mpbid 
 |-  ( ( ( ( ( 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 ) )
46 28 29 35 37 45 ltletrd 
 |-  ( ( ( ( ( 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 
 |-  ( ( D e. ( NN \ []NN ) /\ ( a e. ( Pell1QR ` D ) /\ b e. ( Pell1QR ` D ) ) /\ ( b < a /\ a < ( 2 x. b ) ) ) -> D e. ( NN \ []NN ) )
48 19 3ad2ant1 
 |-  ( ( 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 
 |-  ( ( D e. ( NN \ []NN ) /\ ( a e. ( Pell1QR ` D ) /\ b e. ( Pell1QR ` D ) ) /\ ( b < a /\ a < ( 2 x. b ) ) ) -> a e. ( Pell1QR ` D ) )
50 48 49 sseldd 
 |-  ( ( D e. ( NN \ []NN ) /\ ( a e. ( Pell1QR ` D ) /\ b e. ( Pell1QR ` D ) ) /\ ( b < a /\ a < ( 2 x. b ) ) ) -> a e. ( Pell14QR ` D ) )
51 simp2r 
 |-  ( ( D e. ( NN \ []NN ) /\ ( a e. ( Pell1QR ` D ) /\ b e. ( Pell1QR ` D ) ) /\ ( b < a /\ a < ( 2 x. b ) ) ) -> b e. ( Pell1QR ` D ) )
52 48 51 sseldd 
 |-  ( ( D e. ( NN \ []NN ) /\ ( a e. ( Pell1QR ` D ) /\ b e. ( Pell1QR ` D ) ) /\ ( b < a /\ a < ( 2 x. b ) ) ) -> b e. ( Pell14QR ` D ) )
53 pell14qrdivcl 
 |-  ( ( D e. ( NN \ []NN ) /\ a e. ( Pell14QR ` D ) /\ b e. ( Pell14QR ` D ) ) -> ( a / b ) e. ( Pell14QR ` D ) )
54 47 50 52 53 syl3anc 
 |-  ( ( D e. ( NN \ []NN ) /\ ( a e. ( Pell1QR ` D ) /\ b e. ( Pell1QR ` D ) ) /\ ( b < a /\ a < ( 2 x. b ) ) ) -> ( a / b ) e. ( Pell14QR ` D ) )
55 47 52 32 syl2anc 
 |-  ( ( D e. ( NN \ []NN ) /\ ( a e. ( Pell1QR ` D ) /\ b e. ( Pell1QR ` D ) ) /\ ( b < a /\ a < ( 2 x. b ) ) ) -> b e. RR )
56 55 recnd 
 |-  ( ( D e. ( NN \ []NN ) /\ ( a e. ( Pell1QR ` D ) /\ b e. ( Pell1QR ` D ) ) /\ ( b < a /\ a < ( 2 x. b ) ) ) -> b e. CC )
57 56 mulid2d 
 |-  ( ( D e. ( NN \ []NN ) /\ ( a e. ( Pell1QR ` D ) /\ b e. ( Pell1QR ` D ) ) /\ ( b < a /\ a < ( 2 x. b ) ) ) -> ( 1 x. b ) = b )
58 simp3l 
 |-  ( ( D e. ( NN \ []NN ) /\ ( a e. ( Pell1QR ` D ) /\ b e. ( Pell1QR ` D ) ) /\ ( b < a /\ a < ( 2 x. b ) ) ) -> b < a )
59 57 58 eqbrtrd 
 |-  ( ( D e. ( NN \ []NN ) /\ ( a e. ( Pell1QR ` D ) /\ b e. ( Pell1QR ` D ) ) /\ ( b < a /\ a < ( 2 x. b ) ) ) -> ( 1 x. b ) < a )
60 1red 
 |-  ( ( D e. ( NN \ []NN ) /\ ( a e. ( Pell1QR ` D ) /\ b e. ( Pell1QR ` D ) ) /\ ( b < a /\ a < ( 2 x. b ) ) ) -> 1 e. RR )
61 47 50 21 syl2anc 
 |-  ( ( D e. ( NN \ []NN ) /\ ( a e. ( Pell1QR ` D ) /\ b e. ( Pell1QR ` D ) ) /\ ( b < a /\ a < ( 2 x. b ) ) ) -> a e. RR )
62 pell14qrgt0 
 |-  ( ( D e. ( NN \ []NN ) /\ b e. ( Pell14QR ` D ) ) -> 0 < b )
63 47 52 62 syl2anc 
 |-  ( ( D e. ( NN \ []NN ) /\ ( a e. ( Pell1QR ` D ) /\ b e. ( Pell1QR ` D ) ) /\ ( b < a /\ a < ( 2 x. b ) ) ) -> 0 < b )
64 ltmuldiv 
 |-  ( ( 1 e. RR /\ a e. RR /\ ( b e. RR /\ 0 < b ) ) -> ( ( 1 x. b ) < a <-> 1 < ( a / b ) ) )
65 60 61 55 63 64 syl112anc 
 |-  ( ( 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 ) ) )
66 59 65 mpbid 
 |-  ( ( D e. ( NN \ []NN ) /\ ( a e. ( Pell1QR ` D ) /\ b e. ( Pell1QR ` D ) ) /\ ( b < a /\ a < ( 2 x. b ) ) ) -> 1 < ( a / b ) )
67 simp3r 
 |-  ( ( D e. ( NN \ []NN ) /\ ( a e. ( Pell1QR ` D ) /\ b e. ( Pell1QR ` D ) ) /\ ( b < a /\ a < ( 2 x. b ) ) ) -> a < ( 2 x. b ) )
68 1 a1i 
 |-  ( ( D e. ( NN \ []NN ) /\ ( a e. ( Pell1QR ` D ) /\ b e. ( Pell1QR ` D ) ) /\ ( b < a /\ a < ( 2 x. b ) ) ) -> 2 e. RR )
69 ltdivmul2 
 |-  ( ( a e. RR /\ 2 e. RR /\ ( b e. RR /\ 0 < b ) ) -> ( ( a / b ) < 2 <-> a < ( 2 x. b ) ) )
70 61 68 55 63 69 syl112anc 
 |-  ( ( 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 ) ) )
71 67 70 mpbird 
 |-  ( ( D e. ( NN \ []NN ) /\ ( a e. ( Pell1QR ` D ) /\ b e. ( Pell1QR ` D ) ) /\ ( b < a /\ a < ( 2 x. b ) ) ) -> ( a / b ) < 2 )
72 simprr 
 |-  ( ( ( D e. ( NN \ []NN ) /\ ( a / b ) e. ( Pell14QR ` D ) ) /\ ( 1 < ( a / b ) /\ ( a / b ) < 2 ) ) -> ( a / b ) < 2 )
73 simpll 
 |-  ( ( ( D e. ( NN \ []NN ) /\ ( a / b ) e. ( Pell14QR ` D ) ) /\ ( 1 < ( a / b ) /\ ( a / b ) < 2 ) ) -> D e. ( NN \ []NN ) )
74 simplr 
 |-  ( ( ( D e. ( NN \ []NN ) /\ ( a / b ) e. ( Pell14QR ` D ) ) /\ ( 1 < ( a / b ) /\ ( a / b ) < 2 ) ) -> ( a / b ) e. ( Pell14QR ` D ) )
75 simprl 
 |-  ( ( ( D e. ( NN \ []NN ) /\ ( a / b ) e. ( Pell14QR ` D ) ) /\ ( 1 < ( a / b ) /\ ( a / b ) < 2 ) ) -> 1 < ( a / b ) )
76 pell14qrgapw 
 |-  ( ( D e. ( NN \ []NN ) /\ ( a / b ) e. ( Pell14QR ` D ) /\ 1 < ( a / b ) ) -> 2 < ( a / b ) )
77 73 74 75 76 syl3anc 
 |-  ( ( ( D e. ( NN \ []NN ) /\ ( a / b ) e. ( Pell14QR ` D ) ) /\ ( 1 < ( a / b ) /\ ( a / b ) < 2 ) ) -> 2 < ( a / b ) )
78 pell14qrre 
 |-  ( ( D e. ( NN \ []NN ) /\ ( a / b ) e. ( Pell14QR ` D ) ) -> ( a / b ) e. RR )
79 78 adantr 
 |-  ( ( ( D e. ( NN \ []NN ) /\ ( a / b ) e. ( Pell14QR ` D ) ) /\ ( 1 < ( a / b ) /\ ( a / b ) < 2 ) ) -> ( a / b ) e. RR )
80 ltnsym 
 |-  ( ( 2 e. RR /\ ( a / b ) e. RR ) -> ( 2 < ( a / b ) -> -. ( a / b ) < 2 ) )
81 1 79 80 sylancr 
 |-  ( ( ( D e. ( NN \ []NN ) /\ ( a / b ) e. ( Pell14QR ` D ) ) /\ ( 1 < ( a / b ) /\ ( a / b ) < 2 ) ) -> ( 2 < ( a / b ) -> -. ( a / b ) < 2 ) )
82 77 81 mpd 
 |-  ( ( ( D e. ( NN \ []NN ) /\ ( a / b ) e. ( Pell14QR ` D ) ) /\ ( 1 < ( a / b ) /\ ( a / b ) < 2 ) ) -> -. ( a / b ) < 2 )
83 72 82 pm2.21dd 
 |-  ( ( ( D e. ( NN \ []NN ) /\ ( a / b ) e. ( Pell14QR ` D ) ) /\ ( 1 < ( a / b ) /\ ( a / b ) < 2 ) ) -> ( PellFund ` D ) e. ( Pell1QR ` D ) )
84 47 54 66 71 83 syl22anc 
 |-  ( ( D e. ( NN \ []NN ) /\ ( a e. ( Pell1QR ` D ) /\ b e. ( Pell1QR ` D ) ) /\ ( b < a /\ a < ( 2 x. b ) ) ) -> ( PellFund ` D ) e. ( Pell1QR ` D ) )
85 24 25 26 27 46 84 syl122anc 
 |-  ( ( ( ( ( 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 
 |-  ( ( ( D e. ( NN \ []NN ) /\ a e. ( Pell1QR ` D ) ) /\ ( ( PellFund ` D ) < a /\ a < ( 2 x. ( PellFund ` D ) ) ) ) -> D e. ( NN \ []NN ) )
87 22 adantr 
 |-  ( ( ( D e. ( NN \ []NN ) /\ a e. ( Pell1QR ` D ) ) /\ ( ( PellFund ` D ) < a /\ a < ( 2 x. ( PellFund ` D ) ) ) ) -> a e. RR )
88 simprl 
 |-  ( ( ( D e. ( NN \ []NN ) /\ a e. ( Pell1QR ` D ) ) /\ ( ( PellFund ` D ) < a /\ a < ( 2 x. ( PellFund ` D ) ) ) ) -> ( PellFund ` D ) < a )
89 pellfundglb 
 |-  ( ( D e. ( NN \ []NN ) /\ a e. RR /\ ( PellFund ` D ) < a ) -> E. b e. ( Pell1QR ` D ) ( ( PellFund ` D ) <_ b /\ b < a ) )
90 86 87 88 89 syl3anc 
 |-  ( ( ( 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 ) )
91 85 90 r19.29a 
 |-  ( ( ( D e. ( NN \ []NN ) /\ a e. ( Pell1QR ` D ) ) /\ ( ( PellFund ` D ) < a /\ a < ( 2 x. ( PellFund ` D ) ) ) ) -> ( PellFund ` D ) e. ( Pell1QR ` D ) )
92 91 exp32 
 |-  ( ( D e. ( NN \ []NN ) /\ a e. ( Pell1QR ` D ) ) -> ( ( PellFund ` D ) < a -> ( a < ( 2 x. ( PellFund ` D ) ) -> ( PellFund ` D ) e. ( Pell1QR ` D ) ) ) )
93 simp2 
 |-  ( ( ( D e. ( NN \ []NN ) /\ a e. ( Pell1QR ` D ) ) /\ ( PellFund ` D ) = a /\ a < ( 2 x. ( PellFund ` D ) ) ) -> ( PellFund ` D ) = a )
94 simp1r 
 |-  ( ( ( D e. ( NN \ []NN ) /\ a e. ( Pell1QR ` D ) ) /\ ( PellFund ` D ) = a /\ a < ( 2 x. ( PellFund ` D ) ) ) -> a e. ( Pell1QR ` D ) )
95 93 94 eqeltrd 
 |-  ( ( ( D e. ( NN \ []NN ) /\ a e. ( Pell1QR ` D ) ) /\ ( PellFund ` D ) = a /\ a < ( 2 x. ( PellFund ` D ) ) ) -> ( PellFund ` D ) e. ( Pell1QR ` D ) )
96 95 3exp 
 |-  ( ( D e. ( NN \ []NN ) /\ a e. ( Pell1QR ` D ) ) -> ( ( PellFund ` D ) = a -> ( a < ( 2 x. ( PellFund ` D ) ) -> ( PellFund ` D ) e. ( Pell1QR ` D ) ) ) )
97 92 96 jaod 
 |-  ( ( D e. ( NN \ []NN ) /\ a e. ( Pell1QR ` D ) ) -> ( ( ( PellFund ` D ) < a \/ ( PellFund ` D ) = a ) -> ( a < ( 2 x. ( PellFund ` D ) ) -> ( PellFund ` D ) e. ( Pell1QR ` D ) ) ) )
98 23 97 sylbid 
 |-  ( ( D e. ( NN \ []NN ) /\ a e. ( Pell1QR ` D ) ) -> ( ( PellFund ` D ) <_ a -> ( a < ( 2 x. ( PellFund ` D ) ) -> ( PellFund ` D ) e. ( Pell1QR ` D ) ) ) )
99 98 impd 
 |-  ( ( D e. ( NN \ []NN ) /\ a e. ( Pell1QR ` D ) ) -> ( ( ( PellFund ` D ) <_ a /\ a < ( 2 x. ( PellFund ` D ) ) ) -> ( PellFund ` D ) e. ( Pell1QR ` D ) ) )
100 99 rexlimdva 
 |-  ( D e. ( NN \ []NN ) -> ( E. a e. ( Pell1QR ` D ) ( ( PellFund ` D ) <_ a /\ a < ( 2 x. ( PellFund ` D ) ) ) -> ( PellFund ` D ) e. ( Pell1QR ` D ) ) )
101 17 100 mpd 
 |-  ( D e. ( NN \ []NN ) -> ( PellFund ` D ) e. ( Pell1QR ` D ) )