Theorem List for Intuitionistic Logic Explorer - 12901-13000 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | reeff1oleme 12901* |
Lemma for reeff1o 12902. (Contributed by Jim Kingdon, 15-May-2024.)
|
⊢ (𝑈 ∈ (0(,)e) → ∃𝑥 ∈ ℝ
(exp‘𝑥) = 𝑈) |
|
Theorem | reeff1o 12902 |
The real exponential function is one-to-one onto. (Contributed by Paul
Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 10-Nov-2013.)
|
⊢ (exp ↾ ℝ):ℝ–1-1-onto→ℝ+ |
|
Theorem | efltlemlt 12903 |
Lemma for eflt 12904. The converse of efltim 11441 plus the epsilon-delta
setup. (Contributed by Jim Kingdon, 22-May-2024.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (exp‘𝐴) < (exp‘𝐵)) & ⊢ (𝜑 → 𝐷 ∈ ℝ+) & ⊢ (𝜑 → ((abs‘(𝐴 − 𝐵)) < 𝐷 → (abs‘((exp‘𝐴) − (exp‘𝐵))) < ((exp‘𝐵) − (exp‘𝐴))))
⇒ ⊢ (𝜑 → 𝐴 < 𝐵) |
|
Theorem | eflt 12904 |
The exponential function on the reals is strictly increasing.
(Contributed by Paul Chapman, 21-Aug-2007.) (Revised by Jim Kingdon,
21-May-2024.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ (exp‘𝐴) < (exp‘𝐵))) |
|
Theorem | efle 12905 |
The exponential function on the reals is nondecreasing. (Contributed by
Mario Carneiro, 11-Mar-2014.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (exp‘𝐴) ≤ (exp‘𝐵))) |
|
Theorem | reefiso 12906 |
The exponential function on the reals determines an isomorphism from
reals onto positive reals. (Contributed by Steve Rodriguez,
25-Nov-2007.) (Revised by Mario Carneiro, 11-Mar-2014.)
|
⊢ (exp ↾ ℝ) Isom < , <
(ℝ, ℝ+) |
|
Theorem | reapef 12907 |
Apartness and the exponential function for reals. (Contributed by Jim
Kingdon, 11-Jul-2024.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 # 𝐵 ↔ (exp‘𝐴) # (exp‘𝐵))) |
|
9.1.2 Properties of pi =
3.14159...
|
|
Theorem | pilem1 12908 |
Lemma for pire , pigt2lt4 and sinpi . (Contributed by Mario Carneiro,
9-May-2014.)
|
⊢ (𝐴 ∈ (ℝ+ ∩ (◡sin “ {0})) ↔ (𝐴 ∈ ℝ+ ∧
(sin‘𝐴) =
0)) |
|
Theorem | cosz12 12909 |
Cosine has a zero between 1 and 2. (Contributed by Mario Carneiro and
Jim Kingdon, 7-Mar-2024.)
|
⊢ ∃𝑝 ∈ (1(,)2)(cos‘𝑝) = 0 |
|
Theorem | sin0pilem1 12910* |
Lemma for pi related theorems. (Contributed by Mario Carneiro and Jim
Kingdon, 8-Mar-2024.)
|
⊢ ∃𝑝 ∈ (1(,)2)((cos‘𝑝) = 0 ∧ ∀𝑥 ∈ (𝑝(,)(2 · 𝑝))0 < (sin‘𝑥)) |
|
Theorem | sin0pilem2 12911* |
Lemma for pi related theorems. (Contributed by Mario Carneiro and Jim
Kingdon, 8-Mar-2024.)
|
⊢ ∃𝑞 ∈ (2(,)4)((sin‘𝑞) = 0 ∧ ∀𝑥 ∈ (0(,)𝑞)0 < (sin‘𝑥)) |
|
Theorem | pilem3 12912 |
Lemma for pi related theorems. (Contributed by Jim Kingdon,
9-Mar-2024.)
|
⊢ (π ∈ (2(,)4) ∧ (sin‘π)
= 0) |
|
Theorem | pigt2lt4 12913 |
π is between 2 and 4. (Contributed by Paul Chapman,
23-Jan-2008.)
(Revised by Mario Carneiro, 9-May-2014.)
|
⊢ (2 < π ∧ π <
4) |
|
Theorem | sinpi 12914 |
The sine of π is 0. (Contributed by Paul Chapman,
23-Jan-2008.)
|
⊢ (sin‘π) = 0 |
|
Theorem | pire 12915 |
π is a real number. (Contributed by Paul Chapman,
23-Jan-2008.)
|
⊢ π ∈ ℝ |
|
Theorem | picn 12916 |
π is a complex number. (Contributed by David A.
Wheeler,
6-Dec-2018.)
|
⊢ π ∈ ℂ |
|
Theorem | pipos 12917 |
π is positive. (Contributed by Paul Chapman,
23-Jan-2008.)
(Revised by Mario Carneiro, 9-May-2014.)
|
⊢ 0 < π |
|
Theorem | pirp 12918 |
π is a positive real. (Contributed by Glauco
Siliprandi,
11-Dec-2019.)
|
⊢ π ∈
ℝ+ |
|
Theorem | negpicn 12919 |
-π is a real number. (Contributed by David A.
Wheeler,
8-Dec-2018.)
|
⊢ -π ∈ ℂ |
|
Theorem | sinhalfpilem 12920 |
Lemma for sinhalfpi 12925 and coshalfpi 12926. (Contributed by Paul Chapman,
23-Jan-2008.)
|
⊢ ((sin‘(π / 2)) = 1 ∧
(cos‘(π / 2)) = 0) |
|
Theorem | halfpire 12921 |
π / 2 is real. (Contributed by David Moews,
28-Feb-2017.)
|
⊢ (π / 2) ∈ ℝ |
|
Theorem | neghalfpire 12922 |
-π / 2 is real. (Contributed by David A. Wheeler,
8-Dec-2018.)
|
⊢ -(π / 2) ∈ ℝ |
|
Theorem | neghalfpirx 12923 |
-π / 2 is an extended real. (Contributed by David
A. Wheeler,
8-Dec-2018.)
|
⊢ -(π / 2) ∈
ℝ* |
|
Theorem | pidiv2halves 12924 |
Adding π / 2 to itself gives π. See 2halves 8973.
(Contributed by David A. Wheeler, 8-Dec-2018.)
|
⊢ ((π / 2) + (π / 2)) =
π |
|
Theorem | sinhalfpi 12925 |
The sine of π / 2 is 1. (Contributed by Paul
Chapman,
23-Jan-2008.)
|
⊢ (sin‘(π / 2)) = 1 |
|
Theorem | coshalfpi 12926 |
The cosine of π / 2 is 0. (Contributed by Paul
Chapman,
23-Jan-2008.)
|
⊢ (cos‘(π / 2)) = 0 |
|
Theorem | cosneghalfpi 12927 |
The cosine of -π / 2 is zero. (Contributed by David
Moews,
28-Feb-2017.)
|
⊢ (cos‘-(π / 2)) = 0 |
|
Theorem | efhalfpi 12928 |
The exponential of iπ / 2 is i. (Contributed by Mario
Carneiro, 9-May-2014.)
|
⊢ (exp‘(i · (π / 2))) =
i |
|
Theorem | cospi 12929 |
The cosine of π is -1.
(Contributed by Paul Chapman,
23-Jan-2008.)
|
⊢ (cos‘π) = -1 |
|
Theorem | efipi 12930 |
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 12931 |
Euler's identity. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised
by Mario Carneiro, 9-May-2014.)
|
⊢ ((exp‘(i · π)) + 1) =
0 |
|
Theorem | sin2pi 12932 |
The sine of 2π is 0. (Contributed by Paul Chapman,
23-Jan-2008.)
|
⊢ (sin‘(2 · π)) =
0 |
|
Theorem | cos2pi 12933 |
The cosine of 2π is 1. (Contributed by Paul
Chapman,
23-Jan-2008.)
|
⊢ (cos‘(2 · π)) =
1 |
|
Theorem | ef2pi 12934 |
The exponential of 2πi is 1.
(Contributed by Mario
Carneiro, 9-May-2014.)
|
⊢ (exp‘(i · (2 · π))) =
1 |
|
Theorem | ef2kpi 12935 |
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 12936 |
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 12937 |
Lemma for sinper 12938 and cosper 12939. (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 12938 |
The sine function is periodic. (Contributed by Paul Chapman,
23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) → (sin‘(𝐴 + (𝐾 · (2 · π)))) =
(sin‘𝐴)) |
|
Theorem | cosper 12939 |
The cosine function is periodic. (Contributed by Paul Chapman,
23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) → (cos‘(𝐴 + (𝐾 · (2 · π)))) =
(cos‘𝐴)) |
|
Theorem | sin2kpi 12940 |
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 12941 |
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 12942 |
Sine of a number subtracted from 2 · π.
(Contributed by Paul
Chapman, 15-Mar-2008.)
|
⊢ (𝐴 ∈ ℂ → (sin‘((2
· π) − 𝐴))
= -(sin‘𝐴)) |
|
Theorem | cos2pim 12943 |
Cosine of a number subtracted from 2 · π.
(Contributed by Paul
Chapman, 15-Mar-2008.)
|
⊢ (𝐴 ∈ ℂ → (cos‘((2
· π) − 𝐴))
= (cos‘𝐴)) |
|
Theorem | sinmpi 12944 |
Sine of a number less π. (Contributed by Paul
Chapman,
15-Mar-2008.)
|
⊢ (𝐴 ∈ ℂ → (sin‘(𝐴 − π)) =
-(sin‘𝐴)) |
|
Theorem | cosmpi 12945 |
Cosine of a number less π. (Contributed by Paul
Chapman,
15-Mar-2008.)
|
⊢ (𝐴 ∈ ℂ → (cos‘(𝐴 − π)) =
-(cos‘𝐴)) |
|
Theorem | sinppi 12946 |
Sine of a number plus π. (Contributed by NM,
10-Aug-2008.)
|
⊢ (𝐴 ∈ ℂ → (sin‘(𝐴 + π)) = -(sin‘𝐴)) |
|
Theorem | cosppi 12947 |
Cosine of a number plus π. (Contributed by NM,
18-Aug-2008.)
|
⊢ (𝐴 ∈ ℂ → (cos‘(𝐴 + π)) = -(cos‘𝐴)) |
|
Theorem | efimpi 12948 |
The exponential function at i times a real number less
π.
(Contributed by Paul Chapman, 15-Mar-2008.)
|
⊢ (𝐴 ∈ ℂ → (exp‘(i
· (𝐴 −
π))) = -(exp‘(i · 𝐴))) |
|
Theorem | sinhalfpip 12949 |
The sine of π / 2 plus a number. (Contributed by
Paul Chapman,
24-Jan-2008.)
|
⊢ (𝐴 ∈ ℂ → (sin‘((π /
2) + 𝐴)) =
(cos‘𝐴)) |
|
Theorem | sinhalfpim 12950 |
The sine of π / 2 minus a number. (Contributed by
Paul Chapman,
24-Jan-2008.)
|
⊢ (𝐴 ∈ ℂ → (sin‘((π /
2) − 𝐴)) =
(cos‘𝐴)) |
|
Theorem | coshalfpip 12951 |
The cosine of π / 2 plus a number. (Contributed by
Paul Chapman,
24-Jan-2008.)
|
⊢ (𝐴 ∈ ℂ → (cos‘((π /
2) + 𝐴)) =
-(sin‘𝐴)) |
|
Theorem | coshalfpim 12952 |
The cosine of π / 2 minus a number. (Contributed by
Paul Chapman,
24-Jan-2008.)
|
⊢ (𝐴 ∈ ℂ → (cos‘((π /
2) − 𝐴)) =
(sin‘𝐴)) |
|
Theorem | ptolemy 12953 |
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 11487, 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 12954 |
Lemma for sincosq1sgn 12955. (Contributed by Paul Chapman,
24-Jan-2008.)
|
⊢ ((𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 < (π / 2)) → 0 <
(sin‘𝐴)) |
|
Theorem | sincosq1sgn 12955 |
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 12956 |
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 12957 |
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 12958 |
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 12959 |
The sine of a number strictly between 0 and π is positive.
(Contributed by Paul Chapman, 15-Mar-2008.)
|
⊢ (𝐴 ∈ (0(,)π) → 0 <
(sin‘𝐴)) |
|
Theorem | sinq34lt0t 12960 |
The sine of a number strictly between π and 2 · π is
negative. (Contributed by NM, 17-Aug-2008.)
|
⊢ (𝐴 ∈ (π(,)(2 · π)) →
(sin‘𝐴) <
0) |
|
Theorem | cosq14gt0 12961 |
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 12962 |
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 12963 |
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 12964 |
Location of the zeroes of cosine in (0[,]π).
(Contributed by
David Moews, 28-Feb-2017.)
|
⊢ (𝐴 ∈ (0[,]π) → ((cos‘𝐴) = 0 ↔ 𝐴 = (π / 2))) |
|
Theorem | coseq0negpitopi 12965 |
Location of the zeroes of cosine in (-π(,]π).
(Contributed
by David Moews, 28-Feb-2017.)
|
⊢ (𝐴 ∈ (-π(,]π) →
((cos‘𝐴) = 0 ↔
𝐴 ∈ {(π / 2),
-(π / 2)})) |
|
Theorem | tanrpcl 12966 |
Positive real closure of the tangent function. (Contributed by Mario
Carneiro, 29-Jul-2014.)
|
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(tan‘𝐴) ∈
ℝ+) |
|
Theorem | tangtx 12967 |
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 12968 |
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 12969 |
The sine and cosine of π / 4. (Contributed by Paul
Chapman,
25-Jan-2008.)
|
⊢ ((sin‘(π / 4)) = (1 /
(√‘2)) ∧ (cos‘(π / 4)) = (1 /
(√‘2))) |
|
Theorem | tan4thpi 12970 |
The tangent of π / 4. (Contributed by Mario
Carneiro,
5-Apr-2015.)
|
⊢ (tan‘(π / 4)) = 1 |
|
Theorem | sincos6thpi 12971 |
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 12972 |
The sine and cosine of π / 3. (Contributed by Mario
Carneiro,
21-May-2016.)
|
⊢ ((sin‘(π / 3)) = ((√‘3)
/ 2) ∧ (cos‘(π / 3)) = (1 / 2)) |
|
Theorem | pigt3 12973 |
π is greater than 3. (Contributed by Brendan Leahy,
21-Aug-2020.)
|
⊢ 3 < π |
|
Theorem | pige3 12974 |
π is greater than or equal to 3. (Contributed by
Mario Carneiro,
21-May-2016.)
|
⊢ 3 ≤ π |
|
Theorem | abssinper 12975 |
The absolute value of sine has period π.
(Contributed by NM,
17-Aug-2008.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) →
(abs‘(sin‘(𝐴 +
(𝐾 · π)))) =
(abs‘(sin‘𝐴))) |
|
Theorem | sinkpi 12976 |
The sine of an integer multiple of π is 0.
(Contributed by NM,
11-Aug-2008.)
|
⊢ (𝐾 ∈ ℤ → (sin‘(𝐾 · π)) =
0) |
|
Theorem | coskpi 12977 |
The absolute value of the cosine of an integer multiple of π is 1.
(Contributed by NM, 19-Aug-2008.)
|
⊢ (𝐾 ∈ ℤ →
(abs‘(cos‘(𝐾
· π))) = 1) |
|
Theorem | cosordlem 12978 |
Cosine is decreasing over the closed interval from 0 to
π.
(Contributed by Mario Carneiro, 10-May-2014.)
|
⊢ (𝜑 → 𝐴 ∈ (0[,]π)) & ⊢ (𝜑 → 𝐵 ∈ (0[,]π)) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → (cos‘𝐵) < (cos‘𝐴)) |
|
Theorem | cosq34lt1 12979 |
Cosine is less than one in the third and fourth quadrants. (Contributed
by Jim Kingdon, 19-Mar-2024.)
|
⊢ (𝐴 ∈ (π[,)(2 · π)) →
(cos‘𝐴) <
1) |
|
Theorem | cos02pilt1 12980 |
Cosine is less than one between zero and 2 ·
π. (Contributed by
Jim Kingdon, 19-Mar-2024.)
|
⊢ (𝐴 ∈ (0(,)(2 · π)) →
(cos‘𝐴) <
1) |
|
Theorem | cos0pilt1 12981 |
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 12982 |
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 12983 |
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 12984 |
The interval (-π(,]π) is a subset of the reals.
(Contributed by David Moews, 28-Feb-2017.)
|
⊢ (-π(,]π) ⊆
ℝ |
|
9.1.3 The natural logarithm on complex
numbers
|
|
Syntax | clog 12985 |
Extend class notation with the natural logarithm function on complex
numbers.
|
class log |
|
Syntax | ccxp 12986 |
Extend class notation with the complex power function.
|
class ↑𝑐 |
|
Definition | df-relog 12987 |
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 12988* |
Define the power function on complex numbers. Because df-relog 12987 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 12989 |
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 12990 |
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 12991 |
Closure of the natural logarithm function on positive reals. (Contributed
by Steve Rodriguez, 25-Nov-2007.)
|
⊢ (𝐴 ∈ ℝ+ →
(log‘𝐴) ∈
ℝ) |
|
Theorem | reeflog 12992 |
Relationship between the natural logarithm function and the exponential
function. (Contributed by Steve Rodriguez, 25-Nov-2007.)
|
⊢ (𝐴 ∈ ℝ+ →
(exp‘(log‘𝐴))
= 𝐴) |
|
Theorem | relogef 12993 |
Relationship between the natural logarithm function and the exponential
function. (Contributed by Steve Rodriguez, 25-Nov-2007.)
|
⊢ (𝐴 ∈ ℝ →
(log‘(exp‘𝐴))
= 𝐴) |
|
Theorem | relogeftb 12994 |
Relationship between the natural logarithm function and the exponential
function. (Contributed by Steve Rodriguez, 25-Nov-2007.)
|
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ) →
((log‘𝐴) = 𝐵 ↔ (exp‘𝐵) = 𝐴)) |
|
Theorem | log1 12995 |
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 12996 |
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 12997 |
Lemma for relogmul 12998 and relogdiv 12999. 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 12998 |
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 12999 |
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 13000 |
Exponentiation of a positive real number to an integer power.
(Contributed by Steve Rodriguez, 25-Nov-2007.)
|
⊢ ((𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) = (exp‘(𝑁 · (log‘𝐴)))) |