Step |
Hyp |
Ref |
Expression |
1 |
|
rehalfcl |
|- ( x e. RR -> ( x / 2 ) e. RR ) |
2 |
|
2re |
|- 2 e. RR |
3 |
|
2pos |
|- 0 < 2 |
4 |
|
divgt0 |
|- ( ( ( x e. RR /\ 0 < x ) /\ ( 2 e. RR /\ 0 < 2 ) ) -> 0 < ( x / 2 ) ) |
5 |
2 3 4
|
mpanr12 |
|- ( ( x e. RR /\ 0 < x ) -> 0 < ( x / 2 ) ) |
6 |
5
|
ex |
|- ( x e. RR -> ( 0 < x -> 0 < ( x / 2 ) ) ) |
7 |
|
halfpos |
|- ( x e. RR -> ( 0 < x <-> ( x / 2 ) < x ) ) |
8 |
7
|
biimpd |
|- ( x e. RR -> ( 0 < x -> ( x / 2 ) < x ) ) |
9 |
6 8
|
jcad |
|- ( x e. RR -> ( 0 < x -> ( 0 < ( x / 2 ) /\ ( x / 2 ) < x ) ) ) |
10 |
|
breq2 |
|- ( y = ( x / 2 ) -> ( 0 < y <-> 0 < ( x / 2 ) ) ) |
11 |
|
breq1 |
|- ( y = ( x / 2 ) -> ( y < x <-> ( x / 2 ) < x ) ) |
12 |
10 11
|
anbi12d |
|- ( y = ( x / 2 ) -> ( ( 0 < y /\ y < x ) <-> ( 0 < ( x / 2 ) /\ ( x / 2 ) < x ) ) ) |
13 |
12
|
rspcev |
|- ( ( ( x / 2 ) e. RR /\ ( 0 < ( x / 2 ) /\ ( x / 2 ) < x ) ) -> E. y e. RR ( 0 < y /\ y < x ) ) |
14 |
1 9 13
|
syl6an |
|- ( x e. RR -> ( 0 < x -> E. y e. RR ( 0 < y /\ y < x ) ) ) |
15 |
|
iman |
|- ( ( 0 < x -> E. y e. RR ( 0 < y /\ y < x ) ) <-> -. ( 0 < x /\ -. E. y e. RR ( 0 < y /\ y < x ) ) ) |
16 |
14 15
|
sylib |
|- ( x e. RR -> -. ( 0 < x /\ -. E. y e. RR ( 0 < y /\ y < x ) ) ) |
17 |
16
|
nrex |
|- -. E. x e. RR ( 0 < x /\ -. E. y e. RR ( 0 < y /\ y < x ) ) |