Metamath Proof Explorer


Theorem ltbtwnnq

Description: There exists a number between any two positive fractions. Proposition 9-2.6(i) of Gleason p. 120. (Contributed by NM, 17-Mar-1996) (Revised by Mario Carneiro, 10-May-2013) (New usage is discouraged.)

Ref Expression
Assertion ltbtwnnq
|- ( A  E. x ( A 

Proof

Step Hyp Ref Expression
1 ltrelnq
 |-  
2 1 brel
 |-  ( A  ( A e. Q. /\ B e. Q. ) )
3 2 simprd
 |-  ( A  B e. Q. )
4 ltexnq
 |-  ( B e. Q. -> ( A  E. y ( A +Q y ) = B ) )
5 eleq1
 |-  ( ( A +Q y ) = B -> ( ( A +Q y ) e. Q. <-> B e. Q. ) )
6 5 biimparc
 |-  ( ( B e. Q. /\ ( A +Q y ) = B ) -> ( A +Q y ) e. Q. )
7 addnqf
 |-  +Q : ( Q. X. Q. ) --> Q.
8 7 fdmi
 |-  dom +Q = ( Q. X. Q. )
9 0nnq
 |-  -. (/) e. Q.
10 8 9 ndmovrcl
 |-  ( ( A +Q y ) e. Q. -> ( A e. Q. /\ y e. Q. ) )
11 6 10 syl
 |-  ( ( B e. Q. /\ ( A +Q y ) = B ) -> ( A e. Q. /\ y e. Q. ) )
12 11 simprd
 |-  ( ( B e. Q. /\ ( A +Q y ) = B ) -> y e. Q. )
13 nsmallnq
 |-  ( y e. Q. -> E. z z 
14 11 simpld
 |-  ( ( B e. Q. /\ ( A +Q y ) = B ) -> A e. Q. )
15 1 brel
 |-  ( z  ( z e. Q. /\ y e. Q. ) )
16 15 simpld
 |-  ( z  z e. Q. )
17 ltaddnq
 |-  ( ( A e. Q. /\ z e. Q. ) -> A 
18 14 16 17 syl2an
 |-  ( ( ( B e. Q. /\ ( A +Q y ) = B ) /\ z  A 
19 ltanq
 |-  ( A e. Q. -> ( z  ( A +Q z ) 
20 19 biimpa
 |-  ( ( A e. Q. /\ z  ( A +Q z ) 
21 14 20 sylan
 |-  ( ( ( B e. Q. /\ ( A +Q y ) = B ) /\ z  ( A +Q z ) 
22 simplr
 |-  ( ( ( B e. Q. /\ ( A +Q y ) = B ) /\ z  ( A +Q y ) = B )
23 21 22 breqtrd
 |-  ( ( ( B e. Q. /\ ( A +Q y ) = B ) /\ z  ( A +Q z ) 
24 ovex
 |-  ( A +Q z ) e. _V
25 breq2
 |-  ( x = ( A +Q z ) -> ( A  A 
26 breq1
 |-  ( x = ( A +Q z ) -> ( x  ( A +Q z ) 
27 25 26 anbi12d
 |-  ( x = ( A +Q z ) -> ( ( A  ( A 
28 24 27 spcev
 |-  ( ( A  E. x ( A 
29 18 23 28 syl2anc
 |-  ( ( ( B e. Q. /\ ( A +Q y ) = B ) /\ z  E. x ( A 
30 29 ex
 |-  ( ( B e. Q. /\ ( A +Q y ) = B ) -> ( z  E. x ( A 
31 30 exlimdv
 |-  ( ( B e. Q. /\ ( A +Q y ) = B ) -> ( E. z z  E. x ( A 
32 13 31 syl5
 |-  ( ( B e. Q. /\ ( A +Q y ) = B ) -> ( y e. Q. -> E. x ( A 
33 12 32 mpd
 |-  ( ( B e. Q. /\ ( A +Q y ) = B ) -> E. x ( A 
34 33 ex
 |-  ( B e. Q. -> ( ( A +Q y ) = B -> E. x ( A 
35 34 exlimdv
 |-  ( B e. Q. -> ( E. y ( A +Q y ) = B -> E. x ( A 
36 4 35 sylbid
 |-  ( B e. Q. -> ( A  E. x ( A 
37 3 36 mpcom
 |-  ( A  E. x ( A 
38 ltsonq
 |-  
39 38 1 sotri
 |-  ( ( A  A 
40 39 exlimiv
 |-  ( E. x ( A  A 
41 37 40 impbii
 |-  ( A  E. x ( A