Theorem List for Intuitionistic Logic Explorer - 13501-13600 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | pire 13501 |
π is a real number. (Contributed by Paul Chapman,
23-Jan-2008.)
|
⊢ π ∈ ℝ |
|
Theorem | picn 13502 |
π is a complex number. (Contributed by David A.
Wheeler,
6-Dec-2018.)
|
⊢ π ∈ ℂ |
|
Theorem | pipos 13503 |
π is positive. (Contributed by Paul Chapman,
23-Jan-2008.)
(Revised by Mario Carneiro, 9-May-2014.)
|
⊢ 0 < π |
|
Theorem | pirp 13504 |
π is a positive real. (Contributed by Glauco
Siliprandi,
11-Dec-2019.)
|
⊢ π ∈
ℝ+ |
|
Theorem | negpicn 13505 |
-π is a real number. (Contributed by David A.
Wheeler,
8-Dec-2018.)
|
⊢ -π ∈ ℂ |
|
Theorem | sinhalfpilem 13506 |
Lemma for sinhalfpi 13511 and coshalfpi 13512. (Contributed by Paul Chapman,
23-Jan-2008.)
|
⊢ ((sin‘(π / 2)) = 1 ∧
(cos‘(π / 2)) = 0) |
|
Theorem | halfpire 13507 |
π / 2 is real. (Contributed by David Moews,
28-Feb-2017.)
|
⊢ (π / 2) ∈ ℝ |
|
Theorem | neghalfpire 13508 |
-π / 2 is real. (Contributed by David A. Wheeler,
8-Dec-2018.)
|
⊢ -(π / 2) ∈ ℝ |
|
Theorem | neghalfpirx 13509 |
-π / 2 is an extended real. (Contributed by David
A. Wheeler,
8-Dec-2018.)
|
⊢ -(π / 2) ∈
ℝ* |
|
Theorem | pidiv2halves 13510 |
Adding π / 2 to itself gives π. See 2halves 9107.
(Contributed by David A. Wheeler, 8-Dec-2018.)
|
⊢ ((π / 2) + (π / 2)) =
π |
|
Theorem | sinhalfpi 13511 |
The sine of π / 2 is 1. (Contributed by Paul
Chapman,
23-Jan-2008.)
|
⊢ (sin‘(π / 2)) = 1 |
|
Theorem | coshalfpi 13512 |
The cosine of π / 2 is 0. (Contributed by Paul
Chapman,
23-Jan-2008.)
|
⊢ (cos‘(π / 2)) = 0 |
|
Theorem | cosneghalfpi 13513 |
The cosine of -π / 2 is zero. (Contributed by David
Moews,
28-Feb-2017.)
|
⊢ (cos‘-(π / 2)) = 0 |
|
Theorem | efhalfpi 13514 |
The exponential of iπ / 2 is i. (Contributed by Mario
Carneiro, 9-May-2014.)
|
⊢ (exp‘(i · (π / 2))) =
i |
|
Theorem | cospi 13515 |
The cosine of π is -1.
(Contributed by Paul Chapman,
23-Jan-2008.)
|
⊢ (cos‘π) = -1 |
|
Theorem | efipi 13516 |
The exponential of i · π is -1. (Contributed by Paul
Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
|
⊢ (exp‘(i · π)) =
-1 |
|
Theorem | eulerid 13517 |
Euler's identity. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised
by Mario Carneiro, 9-May-2014.)
|
⊢ ((exp‘(i · π)) + 1) =
0 |
|
Theorem | sin2pi 13518 |
The sine of 2π is 0. (Contributed by Paul Chapman,
23-Jan-2008.)
|
⊢ (sin‘(2 · π)) =
0 |
|
Theorem | cos2pi 13519 |
The cosine of 2π is 1. (Contributed by Paul
Chapman,
23-Jan-2008.)
|
⊢ (cos‘(2 · π)) =
1 |
|
Theorem | ef2pi 13520 |
The exponential of 2πi is 1.
(Contributed by Mario
Carneiro, 9-May-2014.)
|
⊢ (exp‘(i · (2 · π))) =
1 |
|
Theorem | ef2kpi 13521 |
If 𝐾 is an integer, then the exponential
of 2𝐾πi is 1.
(Contributed by Mario Carneiro, 9-May-2014.)
|
⊢ (𝐾 ∈ ℤ → (exp‘((i
· (2 · π)) · 𝐾)) = 1) |
|
Theorem | efper 13522 |
The exponential function is periodic. (Contributed by Paul Chapman,
21-Apr-2008.) (Proof shortened by Mario Carneiro, 10-May-2014.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) → (exp‘(𝐴 + ((i · (2 ·
π)) · 𝐾))) =
(exp‘𝐴)) |
|
Theorem | sinperlem 13523 |
Lemma for sinper 13524 and cosper 13525. (Contributed by Paul Chapman,
23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
|
⊢ (𝐴 ∈ ℂ → (𝐹‘𝐴) = (((exp‘(i · 𝐴))𝑂(exp‘(-i · 𝐴))) / 𝐷)) & ⊢ ((𝐴 + (𝐾 · (2 · π))) ∈
ℂ → (𝐹‘(𝐴 + (𝐾 · (2 · π)))) =
(((exp‘(i · (𝐴 + (𝐾 · (2 · π)))))𝑂(exp‘(-i · (𝐴 + (𝐾 · (2 · π)))))) / 𝐷))
⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) → (𝐹‘(𝐴 + (𝐾 · (2 · π)))) = (𝐹‘𝐴)) |
|
Theorem | sinper 13524 |
The sine function is periodic. (Contributed by Paul Chapman,
23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) → (sin‘(𝐴 + (𝐾 · (2 · π)))) =
(sin‘𝐴)) |
|
Theorem | cosper 13525 |
The cosine function is periodic. (Contributed by Paul Chapman,
23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) → (cos‘(𝐴 + (𝐾 · (2 · π)))) =
(cos‘𝐴)) |
|
Theorem | sin2kpi 13526 |
If 𝐾 is an integer, then the sine of
2𝐾π is 0. (Contributed
by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro,
10-May-2014.)
|
⊢ (𝐾 ∈ ℤ → (sin‘(𝐾 · (2 · π))) =
0) |
|
Theorem | cos2kpi 13527 |
If 𝐾 is an integer, then the cosine of
2𝐾π is 1. (Contributed
by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro,
10-May-2014.)
|
⊢ (𝐾 ∈ ℤ → (cos‘(𝐾 · (2 · π))) =
1) |
|
Theorem | sin2pim 13528 |
Sine of a number subtracted from 2 · π.
(Contributed by Paul
Chapman, 15-Mar-2008.)
|
⊢ (𝐴 ∈ ℂ → (sin‘((2
· π) − 𝐴))
= -(sin‘𝐴)) |
|
Theorem | cos2pim 13529 |
Cosine of a number subtracted from 2 · π.
(Contributed by Paul
Chapman, 15-Mar-2008.)
|
⊢ (𝐴 ∈ ℂ → (cos‘((2
· π) − 𝐴))
= (cos‘𝐴)) |
|
Theorem | sinmpi 13530 |
Sine of a number less π. (Contributed by Paul
Chapman,
15-Mar-2008.)
|
⊢ (𝐴 ∈ ℂ → (sin‘(𝐴 − π)) =
-(sin‘𝐴)) |
|
Theorem | cosmpi 13531 |
Cosine of a number less π. (Contributed by Paul
Chapman,
15-Mar-2008.)
|
⊢ (𝐴 ∈ ℂ → (cos‘(𝐴 − π)) =
-(cos‘𝐴)) |
|
Theorem | sinppi 13532 |
Sine of a number plus π. (Contributed by NM,
10-Aug-2008.)
|
⊢ (𝐴 ∈ ℂ → (sin‘(𝐴 + π)) = -(sin‘𝐴)) |
|
Theorem | cosppi 13533 |
Cosine of a number plus π. (Contributed by NM,
18-Aug-2008.)
|
⊢ (𝐴 ∈ ℂ → (cos‘(𝐴 + π)) = -(cos‘𝐴)) |
|
Theorem | efimpi 13534 |
The exponential function at i times a real number less
π.
(Contributed by Paul Chapman, 15-Mar-2008.)
|
⊢ (𝐴 ∈ ℂ → (exp‘(i
· (𝐴 −
π))) = -(exp‘(i · 𝐴))) |
|
Theorem | sinhalfpip 13535 |
The sine of π / 2 plus a number. (Contributed by
Paul Chapman,
24-Jan-2008.)
|
⊢ (𝐴 ∈ ℂ → (sin‘((π /
2) + 𝐴)) =
(cos‘𝐴)) |
|
Theorem | sinhalfpim 13536 |
The sine of π / 2 minus a number. (Contributed by
Paul Chapman,
24-Jan-2008.)
|
⊢ (𝐴 ∈ ℂ → (sin‘((π /
2) − 𝐴)) =
(cos‘𝐴)) |
|
Theorem | coshalfpip 13537 |
The cosine of π / 2 plus a number. (Contributed by
Paul Chapman,
24-Jan-2008.)
|
⊢ (𝐴 ∈ ℂ → (cos‘((π /
2) + 𝐴)) =
-(sin‘𝐴)) |
|
Theorem | coshalfpim 13538 |
The cosine of π / 2 minus a number. (Contributed by
Paul Chapman,
24-Jan-2008.)
|
⊢ (𝐴 ∈ ℂ → (cos‘((π /
2) − 𝐴)) =
(sin‘𝐴)) |
|
Theorem | ptolemy 13539 |
Ptolemy's Theorem. This theorem is named after the Greek astronomer and
mathematician Ptolemy (Claudius Ptolemaeus). This particular version is
expressed using the sine function. It is proved by expanding all the
multiplication of sines to a product of cosines of differences using
sinmul 11707, then using algebraic simplification to show
that both sides are
equal. This formalization is based on the proof in
"Trigonometry" by
Gelfand and Saul. This is Metamath 100 proof #95. (Contributed by David
A. Wheeler, 31-May-2015.)
|
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ) ∧ ((𝐴 + 𝐵) + (𝐶 + 𝐷)) = π) → (((sin‘𝐴) · (sin‘𝐵)) + ((sin‘𝐶) · (sin‘𝐷))) = ((sin‘(𝐵 + 𝐶)) · (sin‘(𝐴 + 𝐶)))) |
|
Theorem | sincosq1lem 13540 |
Lemma for sincosq1sgn 13541. (Contributed by Paul Chapman,
24-Jan-2008.)
|
⊢ ((𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 < (π / 2)) → 0 <
(sin‘𝐴)) |
|
Theorem | sincosq1sgn 13541 |
The signs of the sine and cosine functions in the first quadrant.
(Contributed by Paul Chapman, 24-Jan-2008.)
|
⊢ (𝐴 ∈ (0(,)(π / 2)) → (0 <
(sin‘𝐴) ∧ 0 <
(cos‘𝐴))) |
|
Theorem | sincosq2sgn 13542 |
The signs of the sine and cosine functions in the second quadrant.
(Contributed by Paul Chapman, 24-Jan-2008.)
|
⊢ (𝐴 ∈ ((π / 2)(,)π) → (0 <
(sin‘𝐴) ∧
(cos‘𝐴) <
0)) |
|
Theorem | sincosq3sgn 13543 |
The signs of the sine and cosine functions in the third quadrant.
(Contributed by Paul Chapman, 24-Jan-2008.)
|
⊢ (𝐴 ∈ (π(,)(3 · (π / 2)))
→ ((sin‘𝐴) <
0 ∧ (cos‘𝐴) <
0)) |
|
Theorem | sincosq4sgn 13544 |
The signs of the sine and cosine functions in the fourth quadrant.
(Contributed by Paul Chapman, 24-Jan-2008.)
|
⊢ (𝐴 ∈ ((3 · (π / 2))(,)(2
· π)) → ((sin‘𝐴) < 0 ∧ 0 < (cos‘𝐴))) |
|
Theorem | sinq12gt0 13545 |
The sine of a number strictly between 0 and π is positive.
(Contributed by Paul Chapman, 15-Mar-2008.)
|
⊢ (𝐴 ∈ (0(,)π) → 0 <
(sin‘𝐴)) |
|
Theorem | sinq34lt0t 13546 |
The sine of a number strictly between π and 2 · π is
negative. (Contributed by NM, 17-Aug-2008.)
|
⊢ (𝐴 ∈ (π(,)(2 · π)) →
(sin‘𝐴) <
0) |
|
Theorem | cosq14gt0 13547 |
The cosine of a number strictly between -π / 2 and
π / 2 is
positive. (Contributed by Mario Carneiro, 25-Feb-2015.)
|
⊢ (𝐴 ∈ (-(π / 2)(,)(π / 2)) → 0
< (cos‘𝐴)) |
|
Theorem | cosq23lt0 13548 |
The cosine of a number in the second and third quadrants is negative.
(Contributed by Jim Kingdon, 14-Mar-2024.)
|
⊢ (𝐴 ∈ ((π / 2)(,)(3 · (π /
2))) → (cos‘𝐴)
< 0) |
|
Theorem | coseq0q4123 13549 |
Location of the zeroes of cosine in
(-(π / 2)(,)(3 · (π / 2))).
(Contributed by Jim
Kingdon, 14-Mar-2024.)
|
⊢ (𝐴 ∈ (-(π / 2)(,)(3 · (π /
2))) → ((cos‘𝐴)
= 0 ↔ 𝐴 = (π /
2))) |
|
Theorem | coseq00topi 13550 |
Location of the zeroes of cosine in (0[,]π).
(Contributed by
David Moews, 28-Feb-2017.)
|
⊢ (𝐴 ∈ (0[,]π) → ((cos‘𝐴) = 0 ↔ 𝐴 = (π / 2))) |
|
Theorem | coseq0negpitopi 13551 |
Location of the zeroes of cosine in (-π(,]π).
(Contributed
by David Moews, 28-Feb-2017.)
|
⊢ (𝐴 ∈ (-π(,]π) →
((cos‘𝐴) = 0 ↔
𝐴 ∈ {(π / 2),
-(π / 2)})) |
|
Theorem | tanrpcl 13552 |
Positive real closure of the tangent function. (Contributed by Mario
Carneiro, 29-Jul-2014.)
|
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(tan‘𝐴) ∈
ℝ+) |
|
Theorem | tangtx 13553 |
The tangent function is greater than its argument on positive reals in its
principal domain. (Contributed by Mario Carneiro, 29-Jul-2014.)
|
⊢ (𝐴 ∈ (0(,)(π / 2)) → 𝐴 < (tan‘𝐴)) |
|
Theorem | sincosq1eq 13554 |
Complementarity of the sine and cosine functions in the first quadrant.
(Contributed by Paul Chapman, 25-Jan-2008.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐴 + 𝐵) = 1) → (sin‘(𝐴 · (π / 2))) = (cos‘(𝐵 · (π /
2)))) |
|
Theorem | sincos4thpi 13555 |
The sine and cosine of π / 4. (Contributed by Paul
Chapman,
25-Jan-2008.)
|
⊢ ((sin‘(π / 4)) = (1 /
(√‘2)) ∧ (cos‘(π / 4)) = (1 /
(√‘2))) |
|
Theorem | tan4thpi 13556 |
The tangent of π / 4. (Contributed by Mario
Carneiro,
5-Apr-2015.)
|
⊢ (tan‘(π / 4)) = 1 |
|
Theorem | sincos6thpi 13557 |
The sine and cosine of π / 6. (Contributed by Paul
Chapman,
25-Jan-2008.) (Revised by Wolf Lammen, 24-Sep-2020.)
|
⊢ ((sin‘(π / 6)) = (1 / 2) ∧
(cos‘(π / 6)) = ((√‘3) / 2)) |
|
Theorem | sincos3rdpi 13558 |
The sine and cosine of π / 3. (Contributed by Mario
Carneiro,
21-May-2016.)
|
⊢ ((sin‘(π / 3)) = ((√‘3)
/ 2) ∧ (cos‘(π / 3)) = (1 / 2)) |
|
Theorem | pigt3 13559 |
π is greater than 3. (Contributed by Brendan Leahy,
21-Aug-2020.)
|
⊢ 3 < π |
|
Theorem | pige3 13560 |
π is greater than or equal to 3. (Contributed by
Mario Carneiro,
21-May-2016.)
|
⊢ 3 ≤ π |
|
Theorem | abssinper 13561 |
The absolute value of sine has period π.
(Contributed by NM,
17-Aug-2008.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) →
(abs‘(sin‘(𝐴 +
(𝐾 · π)))) =
(abs‘(sin‘𝐴))) |
|
Theorem | sinkpi 13562 |
The sine of an integer multiple of π is 0.
(Contributed by NM,
11-Aug-2008.)
|
⊢ (𝐾 ∈ ℤ → (sin‘(𝐾 · π)) =
0) |
|
Theorem | coskpi 13563 |
The absolute value of the cosine of an integer multiple of π is 1.
(Contributed by NM, 19-Aug-2008.)
|
⊢ (𝐾 ∈ ℤ →
(abs‘(cos‘(𝐾
· π))) = 1) |
|
Theorem | cosordlem 13564 |
Cosine is decreasing over the closed interval from 0 to
π.
(Contributed by Mario Carneiro, 10-May-2014.)
|
⊢ (𝜑 → 𝐴 ∈ (0[,]π)) & ⊢ (𝜑 → 𝐵 ∈ (0[,]π)) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → (cos‘𝐵) < (cos‘𝐴)) |
|
Theorem | cosq34lt1 13565 |
Cosine is less than one in the third and fourth quadrants. (Contributed
by Jim Kingdon, 19-Mar-2024.)
|
⊢ (𝐴 ∈ (π[,)(2 · π)) →
(cos‘𝐴) <
1) |
|
Theorem | cos02pilt1 13566 |
Cosine is less than one between zero and 2 ·
π. (Contributed by
Jim Kingdon, 19-Mar-2024.)
|
⊢ (𝐴 ∈ (0(,)(2 · π)) →
(cos‘𝐴) <
1) |
|
Theorem | cos0pilt1 13567 |
Cosine is between minus one and one on the open interval between zero and
π. (Contributed by Jim Kingdon, 7-May-2024.)
|
⊢ (𝐴 ∈ (0(,)π) → (cos‘𝐴) ∈
(-1(,)1)) |
|
Theorem | cos11 13568 |
Cosine is one-to-one over the closed interval from 0 to
π.
(Contributed by Paul Chapman, 16-Mar-2008.) (Revised by Jim Kingdon,
6-May-2024.)
|
⊢ ((𝐴 ∈ (0[,]π) ∧ 𝐵 ∈ (0[,]π)) → (𝐴 = 𝐵 ↔ (cos‘𝐴) = (cos‘𝐵))) |
|
Theorem | ioocosf1o 13569 |
The cosine function is a bijection when restricted to its principal
domain. (Contributed by Mario Carneiro, 12-May-2014.) (Revised by Jim
Kingdon, 7-May-2024.)
|
⊢ (cos ↾
(0(,)π)):(0(,)π)–1-1-onto→(-1(,)1) |
|
Theorem | negpitopissre 13570 |
The interval (-π(,]π) is a subset of the reals.
(Contributed by David Moews, 28-Feb-2017.)
|
⊢ (-π(,]π) ⊆
ℝ |
|
10.1.3 The natural logarithm on complex
numbers
|
|
Syntax | clog 13571 |
Extend class notation with the natural logarithm function on complex
numbers.
|
class log |
|
Syntax | ccxp 13572 |
Extend class notation with the complex power function.
|
class ↑𝑐 |
|
Definition | df-relog 13573 |
Define the natural logarithm function. Defining the logarithm on complex
numbers is similar to square root - there are ways to define it but they
tend to make use of excluded middle. Therefore, we merely define
logarithms on positive reals. See
http://en.wikipedia.org/wiki/Natural_logarithm
and
https://en.wikipedia.org/wiki/Complex_logarithm.
(Contributed by Jim
Kingdon, 14-May-2024.)
|
⊢ log = ◡(exp ↾ ℝ) |
|
Definition | df-rpcxp 13574* |
Define the power function on complex numbers. Because df-relog 13573 is
only defined on positive reals, this definition only allows for a base
which is a positive real. (Contributed by Jim Kingdon, 12-Jun-2024.)
|
⊢ ↑𝑐 = (𝑥 ∈ ℝ+,
𝑦 ∈ ℂ ↦
(exp‘(𝑦 ·
(log‘𝑥)))) |
|
Theorem | dfrelog 13575 |
The natural logarithm function on the positive reals in terms of the real
exponential function. (Contributed by Paul Chapman, 21-Apr-2008.)
|
⊢ (log ↾ ℝ+) = ◡(exp ↾ ℝ) |
|
Theorem | relogf1o 13576 |
The natural logarithm function maps the positive reals one-to-one onto the
real numbers. (Contributed by Paul Chapman, 21-Apr-2008.)
|
⊢ (log ↾
ℝ+):ℝ+–1-1-onto→ℝ |
|
Theorem | relogcl 13577 |
Closure of the natural logarithm function on positive reals. (Contributed
by Steve Rodriguez, 25-Nov-2007.)
|
⊢ (𝐴 ∈ ℝ+ →
(log‘𝐴) ∈
ℝ) |
|
Theorem | reeflog 13578 |
Relationship between the natural logarithm function and the exponential
function. (Contributed by Steve Rodriguez, 25-Nov-2007.)
|
⊢ (𝐴 ∈ ℝ+ →
(exp‘(log‘𝐴))
= 𝐴) |
|
Theorem | relogef 13579 |
Relationship between the natural logarithm function and the exponential
function. (Contributed by Steve Rodriguez, 25-Nov-2007.)
|
⊢ (𝐴 ∈ ℝ →
(log‘(exp‘𝐴))
= 𝐴) |
|
Theorem | relogeftb 13580 |
Relationship between the natural logarithm function and the exponential
function. (Contributed by Steve Rodriguez, 25-Nov-2007.)
|
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ) →
((log‘𝐴) = 𝐵 ↔ (exp‘𝐵) = 𝐴)) |
|
Theorem | log1 13581 |
The natural logarithm of 1. One case of Property 1a of
[Cohen]
p. 301. (Contributed by Steve Rodriguez, 25-Nov-2007.)
|
⊢ (log‘1) = 0 |
|
Theorem | loge 13582 |
The natural logarithm of e. One case of Property 1b of
[Cohen]
p. 301. (Contributed by Steve Rodriguez, 25-Nov-2007.)
|
⊢ (log‘e) = 1 |
|
Theorem | relogoprlem 13583 |
Lemma for relogmul 13584 and relogdiv 13585. Remark of [Cohen] p. 301 ("The
proof of Property 3 is quite similar to the proof given for Property
2"). (Contributed by Steve Rodriguez, 25-Nov-2007.)
|
⊢ (((log‘𝐴) ∈ ℂ ∧ (log‘𝐵) ∈ ℂ) →
(exp‘((log‘𝐴)𝐹(log‘𝐵))) = ((exp‘(log‘𝐴))𝐺(exp‘(log‘𝐵)))) & ⊢
(((log‘𝐴)
∈ ℝ ∧ (log‘𝐵) ∈ ℝ) → ((log‘𝐴)𝐹(log‘𝐵)) ∈ ℝ)
⇒ ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+)
→ (log‘(𝐴𝐺𝐵)) = ((log‘𝐴)𝐹(log‘𝐵))) |
|
Theorem | relogmul 13584 |
The natural logarithm of the product of two positive real numbers is the
sum of natural logarithms. Property 2 of [Cohen] p. 301, restricted to
natural logarithms. (Contributed by Steve Rodriguez, 25-Nov-2007.)
|
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+)
→ (log‘(𝐴
· 𝐵)) =
((log‘𝐴) +
(log‘𝐵))) |
|
Theorem | relogdiv 13585 |
The natural logarithm of the quotient of two positive real numbers is the
difference of natural logarithms. Exercise 72(a) and Property 3 of
[Cohen] p. 301, restricted to natural
logarithms. (Contributed by Steve
Rodriguez, 25-Nov-2007.)
|
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+)
→ (log‘(𝐴 /
𝐵)) = ((log‘𝐴) − (log‘𝐵))) |
|
Theorem | reexplog 13586 |
Exponentiation of a positive real number to an integer power.
(Contributed by Steve Rodriguez, 25-Nov-2007.)
|
⊢ ((𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) = (exp‘(𝑁 · (log‘𝐴)))) |
|
Theorem | relogexp 13587 |
The natural logarithm of positive 𝐴 raised to an integer power.
Property 4 of [Cohen] p. 301-302, restricted
to natural logarithms and
integer powers 𝑁. (Contributed by Steve Rodriguez,
25-Nov-2007.)
|
⊢ ((𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℤ) →
(log‘(𝐴↑𝑁)) = (𝑁 · (log‘𝐴))) |
|
Theorem | relogiso 13588 |
The natural logarithm function on positive reals determines an isomorphism
from the positive reals onto the reals. (Contributed by Steve Rodriguez,
25-Nov-2007.)
|
⊢ (log ↾ ℝ+) Isom <
, < (ℝ+, ℝ) |
|
Theorem | logltb 13589 |
The natural logarithm function on positive reals is strictly monotonic.
(Contributed by Steve Rodriguez, 25-Nov-2007.)
|
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+)
→ (𝐴 < 𝐵 ↔ (log‘𝐴) < (log‘𝐵))) |
|
Theorem | logleb 13590 |
Natural logarithm preserves ≤. (Contributed by
Stefan O'Rear,
19-Sep-2014.)
|
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+)
→ (𝐴 ≤ 𝐵 ↔ (log‘𝐴) ≤ (log‘𝐵))) |
|
Theorem | logrpap0b 13591 |
The logarithm is apart from 0 if and only if its argument is apart from 1.
(Contributed by Jim Kingdon, 3-Jul-2024.)
|
⊢ (𝐴 ∈ ℝ+ → (𝐴 # 1 ↔ (log‘𝐴) # 0)) |
|
Theorem | logrpap0 13592 |
The logarithm is apart from 0 if its argument is apart from 1.
(Contributed by Jim Kingdon, 5-Jul-2024.)
|
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐴 # 1) → (log‘𝐴) # 0) |
|
Theorem | logrpap0d 13593 |
Deduction form of logrpap0 13592. (Contributed by Jim Kingdon,
3-Jul-2024.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐴 # 1) ⇒ ⊢ (𝜑 → (log‘𝐴) # 0) |
|
Theorem | rplogcl 13594 |
Closure of the logarithm function in the positive reals. (Contributed by
Mario Carneiro, 21-Sep-2014.)
|
⊢ ((𝐴 ∈ ℝ ∧ 1 < 𝐴) → (log‘𝐴) ∈
ℝ+) |
|
Theorem | logge0 13595 |
The logarithm of a number greater than 1 is nonnegative. (Contributed by
Mario Carneiro, 29-May-2016.)
|
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → 0 ≤
(log‘𝐴)) |
|
Theorem | logdivlti 13596 |
The log𝑥 /
𝑥 function is
strictly decreasing on the reals greater
than e. (Contributed by Mario Carneiro,
14-Mar-2014.)
|
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴) ∧ 𝐴 < 𝐵) → ((log‘𝐵) / 𝐵) < ((log‘𝐴) / 𝐴)) |
|
Theorem | relogcld 13597 |
Closure of the natural logarithm function. (Contributed by Mario
Carneiro, 29-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈
ℝ+) ⇒ ⊢ (𝜑 → (log‘𝐴) ∈ ℝ) |
|
Theorem | reeflogd 13598 |
Relationship between the natural logarithm function and the exponential
function. (Contributed by Mario Carneiro, 29-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈
ℝ+) ⇒ ⊢ (𝜑 → (exp‘(log‘𝐴)) = 𝐴) |
|
Theorem | relogmuld 13599 |
The natural logarithm of the product of two positive real numbers is the
sum of natural logarithms. Property 2 of [Cohen] p. 301, restricted to
natural logarithms. (Contributed by Mario Carneiro, 29-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈
ℝ+) ⇒ ⊢ (𝜑 → (log‘(𝐴 · 𝐵)) = ((log‘𝐴) + (log‘𝐵))) |
|
Theorem | relogdivd 13600 |
The natural logarithm of the quotient of two positive real numbers is
the difference of natural logarithms. Exercise 72(a) and Property 3 of
[Cohen] p. 301, restricted to natural
logarithms. (Contributed by Mario
Carneiro, 29-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈
ℝ+) ⇒ ⊢ (𝜑 → (log‘(𝐴 / 𝐵)) = ((log‘𝐴) − (log‘𝐵))) |