Step |
Hyp |
Ref |
Expression |
1 |
|
qelioo.1 |
|- ( ph -> A e. RR* ) |
2 |
|
qelioo.2 |
|- ( ph -> B e. RR* ) |
3 |
|
qelioo.3 |
|- ( ph -> A < B ) |
4 |
|
qbtwnxr |
|- ( ( A e. RR* /\ B e. RR* /\ A < B ) -> E. x e. QQ ( A < x /\ x < B ) ) |
5 |
1 2 3 4
|
syl3anc |
|- ( ph -> E. x e. QQ ( A < x /\ x < B ) ) |
6 |
1
|
ad2antrr |
|- ( ( ( ph /\ x e. QQ ) /\ ( A < x /\ x < B ) ) -> A e. RR* ) |
7 |
2
|
ad2antrr |
|- ( ( ( ph /\ x e. QQ ) /\ ( A < x /\ x < B ) ) -> B e. RR* ) |
8 |
|
qre |
|- ( x e. QQ -> x e. RR ) |
9 |
8
|
ad2antlr |
|- ( ( ( ph /\ x e. QQ ) /\ ( A < x /\ x < B ) ) -> x e. RR ) |
10 |
|
simprl |
|- ( ( ( ph /\ x e. QQ ) /\ ( A < x /\ x < B ) ) -> A < x ) |
11 |
|
simprr |
|- ( ( ( ph /\ x e. QQ ) /\ ( A < x /\ x < B ) ) -> x < B ) |
12 |
6 7 9 10 11
|
eliood |
|- ( ( ( ph /\ x e. QQ ) /\ ( A < x /\ x < B ) ) -> x e. ( A (,) B ) ) |
13 |
12
|
ex |
|- ( ( ph /\ x e. QQ ) -> ( ( A < x /\ x < B ) -> x e. ( A (,) B ) ) ) |
14 |
13
|
reximdva |
|- ( ph -> ( E. x e. QQ ( A < x /\ x < B ) -> E. x e. QQ x e. ( A (,) B ) ) ) |
15 |
5 14
|
mpd |
|- ( ph -> E. x e. QQ x e. ( A (,) B ) ) |