Step |
Hyp |
Ref |
Expression |
1 |
|
0lt1 |
|- 0 < 1 |
2 |
|
0re |
|- 0 e. RR |
3 |
|
1re |
|- 1 e. RR |
4 |
|
lttr |
|- ( ( 0 e. RR /\ 1 e. RR /\ A e. RR ) -> ( ( 0 < 1 /\ 1 < A ) -> 0 < A ) ) |
5 |
2 3 4
|
mp3an12 |
|- ( A e. RR -> ( ( 0 < 1 /\ 1 < A ) -> 0 < A ) ) |
6 |
1 5
|
mpani |
|- ( A e. RR -> ( 1 < A -> 0 < A ) ) |
7 |
6
|
imdistani |
|- ( ( A e. RR /\ 1 < A ) -> ( A e. RR /\ 0 < A ) ) |
8 |
|
recgt0 |
|- ( ( A e. RR /\ 0 < A ) -> 0 < ( 1 / A ) ) |
9 |
7 8
|
syl |
|- ( ( A e. RR /\ 1 < A ) -> 0 < ( 1 / A ) ) |
10 |
|
recgt1 |
|- ( ( A e. RR /\ 0 < A ) -> ( 1 < A <-> ( 1 / A ) < 1 ) ) |
11 |
10
|
biimpa |
|- ( ( ( A e. RR /\ 0 < A ) /\ 1 < A ) -> ( 1 / A ) < 1 ) |
12 |
7 11
|
sylancom |
|- ( ( A e. RR /\ 1 < A ) -> ( 1 / A ) < 1 ) |
13 |
9 12
|
jca |
|- ( ( A e. RR /\ 1 < A ) -> ( 0 < ( 1 / A ) /\ ( 1 / A ) < 1 ) ) |