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