Description: Logarithm of a non-1 positive real number is not zero and thus suitable as a divisor. (Contributed by Stefan O'Rear, 19-Sep-2014) (Proof shortened by AV, 14-Jun-2020)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | logne0 | |- ( ( A e. RR+ /\ A =/= 1 ) -> ( log ` A ) =/= 0 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | rpcn | |- ( A e. RR+ -> A e. CC ) |
|
| 2 | 1 | adantr | |- ( ( A e. RR+ /\ A =/= 1 ) -> A e. CC ) |
| 3 | rpne0 | |- ( A e. RR+ -> A =/= 0 ) |
|
| 4 | 3 | adantr | |- ( ( A e. RR+ /\ A =/= 1 ) -> A =/= 0 ) |
| 5 | simpr | |- ( ( A e. RR+ /\ A =/= 1 ) -> A =/= 1 ) |
|
| 6 | logccne0 | |- ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( log ` A ) =/= 0 ) |
|
| 7 | 2 4 5 6 | syl3anc | |- ( ( A e. RR+ /\ A =/= 1 ) -> ( log ` A ) =/= 0 ) |