This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem qextltlem

Description: Lemma for qextlt and qextle . (Contributed by Mario Carneiro, 3-Oct-2014)

Ref Expression
Assertion qextltlem 
|- ( ( A e. RR* /\ B e. RR* ) -> ( A < B -> E. x e. QQ ( -. ( x < A <-> x < B ) /\ -. ( x <_ A <-> x <_ B ) ) ) )

Proof

Step Hyp Ref Expression
1 qbtwnxr 
 |-  ( ( A e. RR* /\ B e. RR* /\ A < B ) -> E. x e. QQ ( A < x /\ x < B ) )
2 1 3expia 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A < B -> E. x e. QQ ( A < x /\ x < B ) ) )
3 simprl 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ x e. QQ ) /\ ( A < x /\ x < B ) ) -> A < x )
4 simplll 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ x e. QQ ) /\ ( A < x /\ x < B ) ) -> A e. RR* )
5 qre 
 |-  ( x e. QQ -> x e. RR )
6 5 rexrd 
 |-  ( x e. QQ -> x e. RR* )
7 6 ad2antlr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ x e. QQ ) /\ ( A < x /\ x < B ) ) -> x e. RR* )
8 xrltnle 
 |-  ( ( A e. RR* /\ x e. RR* ) -> ( A < x <-> -. x <_ A ) )
9 4 7 8 syl2anc 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ x e. QQ ) /\ ( A < x /\ x < B ) ) -> ( A < x <-> -. x <_ A ) )
10 3 9 mpbid 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ x e. QQ ) /\ ( A < x /\ x < B ) ) -> -. x <_ A )
11 xrltle 
 |-  ( ( x e. RR* /\ A e. RR* ) -> ( x < A -> x <_ A ) )
12 7 4 11 syl2anc 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ x e. QQ ) /\ ( A < x /\ x < B ) ) -> ( x < A -> x <_ A ) )
13 10 12 mtod 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ x e. QQ ) /\ ( A < x /\ x < B ) ) -> -. x < A )
14 simprr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ x e. QQ ) /\ ( A < x /\ x < B ) ) -> x < B )
15 13 14 2thd 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ x e. QQ ) /\ ( A < x /\ x < B ) ) -> ( -. x < A <-> x < B ) )
16 nbbn 
 |-  ( ( -. x < A <-> x < B ) <-> -. ( x < A <-> x < B ) )
17 15 16 sylib 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ x e. QQ ) /\ ( A < x /\ x < B ) ) -> -. ( x < A <-> x < B ) )
18 simpllr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ x e. QQ ) /\ ( A < x /\ x < B ) ) -> B e. RR* )
19 7 18 14 xrltled 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ x e. QQ ) /\ ( A < x /\ x < B ) ) -> x <_ B )
20 10 19 2thd 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ x e. QQ ) /\ ( A < x /\ x < B ) ) -> ( -. x <_ A <-> x <_ B ) )
21 nbbn 
 |-  ( ( -. x <_ A <-> x <_ B ) <-> -. ( x <_ A <-> x <_ B ) )
22 20 21 sylib 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ x e. QQ ) /\ ( A < x /\ x < B ) ) -> -. ( x <_ A <-> x <_ B ) )
23 17 22 jca 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ x e. QQ ) /\ ( A < x /\ x < B ) ) -> ( -. ( x < A <-> x < B ) /\ -. ( x <_ A <-> x <_ B ) ) )
24 23 ex 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ x e. QQ ) -> ( ( A < x /\ x < B ) -> ( -. ( x < A <-> x < B ) /\ -. ( x <_ A <-> x <_ B ) ) ) )
25 24 reximdva 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( E. x e. QQ ( A < x /\ x < B ) -> E. x e. QQ ( -. ( x < A <-> x < B ) /\ -. ( x <_ A <-> x <_ B ) ) ) )
26 2 25 syld 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A < B -> E. x e. QQ ( -. ( x < A <-> x < B ) /\ -. ( x <_ A <-> x <_ B ) ) ) )