P. 250 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 24901-25000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cxpsubd 24901	Exponent subtraction law for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴↑𝑐(𝐵 − 𝐶)) = ((𝐴↑𝑐𝐵) / (𝐴↑𝑐𝐶)))
Theorem	cxpltd 24902	Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 1 < 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐵 < 𝐶 ↔ (𝐴↑𝑐𝐵) < (𝐴↑𝑐𝐶)))
Theorem	cxpled 24903	Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 1 < 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐵 ≤ 𝐶 ↔ (𝐴↑𝑐𝐵) ≤ (𝐴↑𝑐𝐶)))
Theorem	cxplead 24904	Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 1 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≤ 𝐶)    ⇒   ⊢ (𝜑 → (𝐴↑𝑐𝐵) ≤ (𝐴↑𝑐𝐶))
Theorem	divcxpd 24905	Complex exponentiation of a quotient. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵)↑𝑐𝐶) = ((𝐴↑𝑐𝐶) / (𝐵↑𝑐𝐶)))
Theorem	recxpcld 24906	Positive real closure of the complex power function. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐴↑𝑐𝐵) ∈ ℝ)
Theorem	cxpge0d 24907	Nonnegative exponentiation with a real exponent is nonnegative. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → 0 ≤ (𝐴↑𝑐𝐵))
Theorem	cxple2ad 24908	Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐶)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    ⇒   ⊢ (𝜑 → (𝐴↑𝑐𝐶) ≤ (𝐵↑𝑐𝐶))
Theorem	cxplt2d 24909	Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (𝐴↑𝑐𝐶) < (𝐵↑𝑐𝐶)))
Theorem	cxple2d 24910	Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (𝐴↑𝑐𝐶) ≤ (𝐵↑𝑐𝐶)))
Theorem	mulcxpd 24911	Complex exponentiation of a product. Proposition 10-4.2(c) of [Gleason] p. 135. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐵)↑𝑐𝐶) = ((𝐴↑𝑐𝐶) · (𝐵↑𝑐𝐶)))
Theorem	cxpsqrtth 24912	Square root theorem over the complex numbers for the complex power function. Theorem I.35 of [Apostol] p. 29. Compare with sqrtth 14511. (Contributed by AV, 23-Dec-2022.)
⊢ (𝐴 ∈ ℂ → ((√‘𝐴)↑𝑐2) = 𝐴)
Theorem	2irrexpq 24913*	There exist irrational numbers 𝑎 and 𝑏 such that (𝑎↑𝑐𝑏) is rational. Statement in the Metamath book, section 1.1.5, footnote 27 on page 17, and the "classical proof" for theorem 1.2 of [Bauer], p. 483. This proof is not acceptable in intuitionistic logic, since it is based on the law of excluded middle: Either ((√‘2)↑𝑐(√‘2)) is rational, in which case (√‘2), being irrational (see sqrt2irr 15382), can be chosen for both 𝑎 and 𝑏, or ((√‘2)↑𝑐(√‘2)) is irrational, in which case ((√‘2)↑𝑐(√‘2)) can be chosen for 𝑎 and (√‘2) for 𝑏, since (((√‘2)↑𝑐(√‘2))↑𝑐(√‘2)) = 2 is rational. For an alternate proof, which can be used in intuitionistic logic, see 2irrexpqALT 24978. (Contributed by AV, 23-Dec-2022.)
⊢ ∃𝑎 ∈ (ℝ ∖ ℚ)∃𝑏 ∈ (ℝ ∖ ℚ)(𝑎↑𝑐𝑏) ∈ ℚ
Theorem	cxprecd 24914	Complex exponentiation of a reciprocal. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((1 / 𝐴)↑𝑐𝐵) = (1 / (𝐴↑𝑐𝐵)))
Theorem	rpcxpcld 24915	Positive real closure of the complex power function. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐴↑𝑐𝐵) ∈ ℝ+)
Theorem	logcxpd 24916	Logarithm of a complex power. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (log‘(𝐴↑𝑐𝐵)) = (𝐵 · (log‘𝐴)))
Theorem	cxplt3d 24917	Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 1)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐵 < 𝐶 ↔ (𝐴↑𝑐𝐶) < (𝐴↑𝑐𝐵)))
Theorem	cxple3d 24918	Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 1)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐵 ≤ 𝐶 ↔ (𝐴↑𝑐𝐶) ≤ (𝐴↑𝑐𝐵)))
Theorem	cxpmuld 24919	Product of exponents law for complex exponentiation. Proposition 10-4.2(b) of [Gleason] p. 135. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴↑𝑐(𝐵 · 𝐶)) = ((𝐴↑𝑐𝐵)↑𝑐𝐶))
Theorem	cxpcom 24920	Commutative law for real exponentiation. (Contributed by AV, 29-Dec-2022.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴↑𝑐𝐵)↑𝑐𝐶) = ((𝐴↑𝑐𝐶)↑𝑐𝐵))
Theorem	dvcxp1 24921*	The derivative of a complex power with respect to the first argument. (Contributed by Mario Carneiro, 24-Feb-2015.)
⊢ (𝐴 ∈ ℂ → (ℝ D (𝑥 ∈ ℝ+ ↦ (𝑥↑𝑐𝐴))) = (𝑥 ∈ ℝ+ ↦ (𝐴 · (𝑥↑𝑐(𝐴 − 1)))))
Theorem	dvcxp2 24922*	The derivative of a complex power with respect to the second argument. (Contributed by Mario Carneiro, 24-Feb-2015.)
⊢ (𝐴 ∈ ℝ+ → (ℂ D (𝑥 ∈ ℂ ↦ (𝐴↑𝑐𝑥))) = (𝑥 ∈ ℂ ↦ ((log‘𝐴) · (𝐴↑𝑐𝑥))))
Theorem	dvsqrt 24923	The derivative of the real square root function. (Contributed by Mario Carneiro, 1-May-2016.)
⊢ (ℝ D (𝑥 ∈ ℝ+ ↦ (√‘𝑥))) = (𝑥 ∈ ℝ+ ↦ (1 / (2 · (√‘𝑥))))
Theorem	dvcncxp1 24924*	Derivative of complex power with respect to first argument on the complex plane. (Contributed by Brendan Leahy, 18-Dec-2018.)
⊢ 𝐷 = (ℂ ∖ (-∞(,]0))    ⇒   ⊢ (𝐴 ∈ ℂ → (ℂ D (𝑥 ∈ 𝐷 ↦ (𝑥↑𝑐𝐴))) = (𝑥 ∈ 𝐷 ↦ (𝐴 · (𝑥↑𝑐(𝐴 − 1)))))
Theorem	dvcnsqrt 24925*	Derivative of square root function. (Contributed by Brendan Leahy, 18-Dec-2018.)
⊢ 𝐷 = (ℂ ∖ (-∞(,]0))    ⇒   ⊢ (ℂ D (𝑥 ∈ 𝐷 ↦ (√‘𝑥))) = (𝑥 ∈ 𝐷 ↦ (1 / (2 · (√‘𝑥))))
Theorem	cxpcn 24926*	Domain of continuity of the complex power function. (Contributed by Mario Carneiro, 1-May-2016.)
⊢ 𝐷 = (ℂ ∖ (-∞(,]0))    &   ⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ 𝐾 = (𝐽 ↾t 𝐷)    ⇒   ⊢ (𝑥 ∈ 𝐷, 𝑦 ∈ ℂ ↦ (𝑥↑𝑐𝑦)) ∈ ((𝐾 ×t 𝐽) Cn 𝐽)
Theorem	cxpcn2 24927*	Continuity of the complex power function, when the base is real. (Contributed by Mario Carneiro, 1-May-2016.)
⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ 𝐾 = (𝐽 ↾t ℝ+)    ⇒   ⊢ (𝑥 ∈ ℝ+, 𝑦 ∈ ℂ ↦ (𝑥↑𝑐𝑦)) ∈ ((𝐾 ×t 𝐽) Cn 𝐽)
Theorem	cxpcn3lem 24928*	Lemma for cxpcn3 24929. (Contributed by Mario Carneiro, 2-May-2016.)
⊢ 𝐷 = (◡ℜ “ ℝ+)    &   ⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ 𝐾 = (𝐽 ↾t (0[,)+∞))    &   ⊢ 𝐿 = (𝐽 ↾t 𝐷)    &   ⊢ 𝑈 = (if((ℜ‘𝐴) ≤ 1, (ℜ‘𝐴), 1) / 2)    &   ⊢ 𝑇 = if(𝑈 ≤ (𝐸↑𝑐(1 / 𝑈)), 𝑈, (𝐸↑𝑐(1 / 𝑈)))    ⇒   ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) → ∃𝑑 ∈ ℝ+ ∀𝑎 ∈ (0[,)+∞)∀𝑏 ∈ 𝐷 (((abs‘𝑎) < 𝑑 ∧ (abs‘(𝐴 − 𝑏)) < 𝑑) → (abs‘(𝑎↑𝑐𝑏)) < 𝐸))
Theorem	cxpcn3 24929*	Extend continuity of the complex power function to a base of zero, as long as the exponent has strictly positive real part. (Contributed by Mario Carneiro, 2-May-2016.)
⊢ 𝐷 = (◡ℜ “ ℝ+)    &   ⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ 𝐾 = (𝐽 ↾t (0[,)+∞))    &   ⊢ 𝐿 = (𝐽 ↾t 𝐷)    ⇒   ⊢ (𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) ∈ ((𝐾 ×t 𝐿) Cn 𝐽)
Theorem	resqrtcn 24930	Continuity of the real square root function. (Contributed by Mario Carneiro, 2-May-2016.)
⊢ (√ ↾ (0[,)+∞)) ∈ ((0[,)+∞)–cn→ℝ)
Theorem	sqrtcn 24931	Continuity of the square root function. (Contributed by Mario Carneiro, 2-May-2016.)
⊢ 𝐷 = (ℂ ∖ (-∞(,]0))    ⇒   ⊢ (√ ↾ 𝐷) ∈ (𝐷–cn→ℂ)
Theorem	cxpaddlelem 24932	Lemma for cxpaddle 24933. (Contributed by Mario Carneiro, 2-Aug-2014.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐴 ≤ 1)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ≤ 1)    ⇒   ⊢ (𝜑 → 𝐴 ≤ (𝐴↑𝑐𝐵))
Theorem	cxpaddle 24933	Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐶 ≤ 1)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵)↑𝑐𝐶) ≤ ((𝐴↑𝑐𝐶) + (𝐵↑𝑐𝐶)))
Theorem	abscxpbnd 24934	Bound on the absolute value of a complex power. (Contributed by Mario Carneiro, 15-Sep-2014.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 0 ≤ (ℜ‘𝐵))    &   ⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ (𝜑 → (abs‘𝐴) ≤ 𝑀)    ⇒   ⊢ (𝜑 → (abs‘(𝐴↑𝑐𝐵)) ≤ ((𝑀↑𝑐(ℜ‘𝐵)) · (exp‘((abs‘𝐵) · π))))
Theorem	root1id 24935	Property of an 𝑁-th root of unity. (Contributed by Mario Carneiro, 23-Apr-2015.)
⊢ (𝑁 ∈ ℕ → ((-1↑𝑐(2 / 𝑁))↑𝑁) = 1)
Theorem	root1eq1 24936	The only powers of an 𝑁-th root of unity that equal 1 are the multiples of 𝑁. In other words, -1↑𝑐(2 / 𝑁) has order 𝑁 in the multiplicative group of nonzero complex numbers. (In fact, these and their powers are the only elements of finite order in the complex numbers.) (Contributed by Mario Carneiro, 28-Apr-2016.)
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ) → (((-1↑𝑐(2 / 𝑁))↑𝐾) = 1 ↔ 𝑁 ∥ 𝐾))
Theorem	root1cj 24937	Within the 𝑁-th roots of unity, the conjugate of the 𝐾-th root is the 𝑁 − 𝐾-th root. (Contributed by Mario Carneiro, 23-Apr-2015.)
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ) → (∗‘((-1↑𝑐(2 / 𝑁))↑𝐾)) = ((-1↑𝑐(2 / 𝑁))↑(𝑁 − 𝐾)))
Theorem	cxpeq 24938*	Solve an equation involving an 𝑁-th power. The expression -1↑𝑐(2 / 𝑁) = exp(2πi / 𝑁) is a way to write the primitive 𝑁-th root of unity with the smallest positive argument. (Contributed by Mario Carneiro, 23-Apr-2015.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → ((𝐴↑𝑁) = 𝐵 ↔ ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = ((𝐵↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛))))
Theorem	loglesqrt 24939	An upper bound on the logarithm. (Contributed by Mario Carneiro, 2-May-2016.) (Proof shortened by AV, 2-Aug-2021.)
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (log‘(𝐴 + 1)) ≤ (√‘𝐴))
Theorem	logreclem 24940	Symmetry of the natural logarithm range by negation. Lemma for logrec 24941. (Contributed by Saveliy Skresanov, 27-Dec-2016.)
⊢ ((𝐴 ∈ ran log ∧ ¬ (ℑ‘𝐴) = π) → -𝐴 ∈ ran log)
Theorem	logrec 24941	Logarithm of a reciprocal changes sign. (Contributed by Saveliy Skresanov, 28-Dec-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ (ℑ‘(log‘𝐴)) ≠ π) → (log‘𝐴) = -(log‘(1 / 𝐴)))
14.3.5  Logarithms to an arbitrary base Define "log using an arbitrary base" function and then prove some of its properties. Note that logb is generalized to an arbitrary base and arbitrary parameter in ℂ, but it doesn't accept infinities as arguments, unlike log. Metamath doesn't care what letters are used to represent classes. Usually classes begin with the letter "A", but here we use "B" and "X" to more clearly distinguish between "base" and "other parameter of log". There are different ways this could be defined in Metamath. The approach used here is intentionally similar to existing 2-parameter Metamath functions (operations): (𝐵 logb 𝑋) where 𝐵 is the base and 𝑋 is the argument of the logarithm function. An alternative would be to support the notational form (( logb ‘𝐵)‘𝑋); that looks a little more like traditional notation. Such a function ( logb ‘𝐵) for a fixed base can be obtained in Metamath (without the need for a new definition) by the curry function: (curry logb ‘𝐵), see logbmpt 24966, logbf 24967 and logbfval 24968.
Syntax	clogb 24942	Extend class notation to include the logarithm generalized to an arbitrary base.
class logb
Definition	df-logb 24943*	Define the logb operator. This is the logarithm generalized to an arbitrary base. It can be used as (𝐵 logb 𝑋) for "log base B of X". In the most common traditional notation, base B is a subscript of "log". The definition is according to Wikipedia "Complex logarithm": https://en.wikipedia.org/wiki/Complex_logarithm#Logarithms_to_other_bases (10-Jun-2020). (Contributed by David A. Wheeler, 21-Jan-2017.)
⊢ logb = (𝑥 ∈ (ℂ ∖ {0, 1}), 𝑦 ∈ (ℂ ∖ {0}) ↦ ((log‘𝑦) / (log‘𝑥)))
Theorem	logbval 24944	Define the value of the logb function, the logarithm generalized to an arbitrary base, when used as infix. Most Metamath statements select variables in order of their use, but to make the order clearer we use "B" for base and "X" for the argument of the logarithm function here. (Contributed by David A. Wheeler, 21-Jan-2017.) (Revised by David A. Wheeler, 16-Jul-2017.)
⊢ ((𝐵 ∈ (ℂ ∖ {0, 1}) ∧ 𝑋 ∈ (ℂ ∖ {0})) → (𝐵 logb 𝑋) = ((log‘𝑋) / (log‘𝐵)))
Theorem	logbcl 24945	General logarithm closure. (Contributed by David A. Wheeler, 17-Jul-2017.)
⊢ ((𝐵 ∈ (ℂ ∖ {0, 1}) ∧ 𝑋 ∈ (ℂ ∖ {0})) → (𝐵 logb 𝑋) ∈ ℂ)
Theorem	logbid1 24946	General logarithm is 1 when base and arg match. Property 1(a) of [Cohen4] p. 361. (Contributed by Stefan O'Rear, 19-Sep-2014.) (Revised by David A. Wheeler, 22-Jul-2017.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (𝐴 logb 𝐴) = 1)
Theorem	logb1 24947	The logarithm of 1 to an arbitrary base 𝐵 is 0. Property 1(b) of [Cohen4] p. 361. See log1 24769. (Contributed by Stefan O'Rear, 19-Sep-2014.) (Revised by Thierry Arnoux, 27-Sep-2017.)
⊢ ((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1) → (𝐵 logb 1) = 0)
Theorem	elogb 24948	The general logarithm of a number to the base being Euler's constant is the natural logarithm of the number. Put another way, using e as the base in logb is the same as log. Definition in [Cohen4] p. 352. (Contributed by David A. Wheeler, 17-Oct-2017.) (Revised by David A. Wheeler and AV, 16-Jun-2020.)
⊢ (𝐴 ∈ (ℂ ∖ {0}) → (e logb 𝐴) = (log‘𝐴))
Theorem	logbchbase 24949	Change of base for logarithms. Property in [Cohen4] p. 367. (Contributed by AV, 11-Jun-2020.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1) ∧ 𝑋 ∈ (ℂ ∖ {0})) → (𝐴 logb 𝑋) = ((𝐵 logb 𝑋) / (𝐵 logb 𝐴)))
Theorem	relogbval 24950	Value of the general logarithm with integer base. (Contributed by Thierry Arnoux, 27-Sep-2017.)
⊢ ((𝐵 ∈ (ℤ≥‘2) ∧ 𝑋 ∈ ℝ+) → (𝐵 logb 𝑋) = ((log‘𝑋) / (log‘𝐵)))
Theorem	relogbcl 24951	Closure of the general logarithm with a positive real base on positive reals. (Contributed by Stefan O'Rear, 19-Sep-2014.) (Revised by Thierry Arnoux, 27-Sep-2017.)
⊢ ((𝐵 ∈ ℝ+ ∧ 𝑋 ∈ ℝ+ ∧ 𝐵 ≠ 1) → (𝐵 logb 𝑋) ∈ ℝ)
Theorem	relogbzcl 24952	Closure of the general logarithm with integer base on positive reals. (Contributed by Thierry Arnoux, 27-Sep-2017.) (Proof shortened by AV, 9-Jun-2020.)
⊢ ((𝐵 ∈ (ℤ≥‘2) ∧ 𝑋 ∈ ℝ+) → (𝐵 logb 𝑋) ∈ ℝ)
Theorem	relogbreexp 24953	Power law for the general logarithm for real powers: The logarithm of a positive real number to the power of a real number is equal to the product of the exponent and the logarithm of the base of the power. Property 4 of [Cohen4] p. 361. (Contributed by AV, 9-Jun-2020.)
⊢ ((𝐵 ∈ (ℂ ∖ {0, 1}) ∧ 𝐶 ∈ ℝ+ ∧ 𝐸 ∈ ℝ) → (𝐵 logb (𝐶↑𝑐𝐸)) = (𝐸 · (𝐵 logb 𝐶)))
Theorem	relogbzexp 24954	Power law for the general logarithm for integer powers: The logarithm of a positive real number to the power of an integer is equal to the product of the exponent and the logarithm of the base of the power. (Contributed by Stefan O'Rear, 19-Sep-2014.) (Revised by AV, 9-Jun-2020.)
⊢ ((𝐵 ∈ (ℂ ∖ {0, 1}) ∧ 𝐶 ∈ ℝ+ ∧ 𝑁 ∈ ℤ) → (𝐵 logb (𝐶↑𝑁)) = (𝑁 · (𝐵 logb 𝐶)))
Theorem	relogbmul 24955	The logarithm of the product of two positive real numbers is the sum of logarithms. Property 2 of [Cohen4] p. 361. (Contributed by Stefan O'Rear, 19-Sep-2014.) (Revised by AV, 29-May-2020.)
⊢ ((𝐵 ∈ (ℂ ∖ {0, 1}) ∧ (𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+)) → (𝐵 logb (𝐴 · 𝐶)) = ((𝐵 logb 𝐴) + (𝐵 logb 𝐶)))
Theorem	relogbmulexp 24956	The logarithm of the product of a positive real and a positive real number to the power of a real number is the sum of the logarithm of the first real number and the scaled logarithm of the second real number. (Contributed by AV, 29-May-2020.)
⊢ ((𝐵 ∈ (ℂ ∖ {0, 1}) ∧ (𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ∧ 𝐸 ∈ ℝ)) → (𝐵 logb (𝐴 · (𝐶↑𝑐𝐸))) = ((𝐵 logb 𝐴) + (𝐸 · (𝐵 logb 𝐶))))
Theorem	relogbdiv 24957	The logarithm of the quotient of two positive real numbers is the difference of logarithms. Property 3 of [Cohen4] p. 361. (Contributed by AV, 29-May-2020.)
⊢ ((𝐵 ∈ (ℂ ∖ {0, 1}) ∧ (𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+)) → (𝐵 logb (𝐴 / 𝐶)) = ((𝐵 logb 𝐴) − (𝐵 logb 𝐶)))
Theorem	relogbexp 24958	Identity law for general logarithm: the logarithm of a power to the base is the exponent. Property 6 of [Cohen4] p. 361. (Contributed by Stefan O'Rear, 19-Sep-2014.) (Revised by AV, 9-Jun-2020.)
⊢ ((𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1 ∧ 𝑀 ∈ ℤ) → (𝐵 logb (𝐵↑𝑀)) = 𝑀)
Theorem	nnlogbexp 24959	Identity law for general logarithm with integer base. (Contributed by Stefan O'Rear, 19-Sep-2014.) (Revised by Thierry Arnoux, 27-Sep-2017.)
⊢ ((𝐵 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ) → (𝐵 logb (𝐵↑𝑀)) = 𝑀)
Theorem	logbrec 24960	Logarithm of a reciprocal changes sign. See logrec 24941. Particular case of Property 3 of [Cohen4] p. 361. (Contributed by Thierry Arnoux, 27-Sep-2017.)
⊢ ((𝐵 ∈ (ℤ≥‘2) ∧ 𝐴 ∈ ℝ+) → (𝐵 logb (1 / 𝐴)) = -(𝐵 logb 𝐴))
Theorem	logbleb 24961	The general logarithm function is monotone/increasing. See logleb 24786. (Contributed by Stefan O'Rear, 19-Oct-2014.) (Revised by AV, 31-May-2020.)
⊢ ((𝐵 ∈ (ℤ≥‘2) ∧ 𝑋 ∈ ℝ+ ∧ 𝑌 ∈ ℝ+) → (𝑋 ≤ 𝑌 ↔ (𝐵 logb 𝑋) ≤ (𝐵 logb 𝑌)))
Theorem	logblt 24962	The general logarithm function is strictly monotone/increasing. Property 2 of [Cohen4] p. 377. See logltb 24783. (Contributed by Stefan O'Rear, 19-Oct-2014.) (Revised by Thierry Arnoux, 27-Sep-2017.)
⊢ ((𝐵 ∈ (ℤ≥‘2) ∧ 𝑋 ∈ ℝ+ ∧ 𝑌 ∈ ℝ+) → (𝑋 < 𝑌 ↔ (𝐵 logb 𝑋) < (𝐵 logb 𝑌)))
Theorem	relogbcxp 24963	Identity law for the general logarithm for real numbers. (Contributed by AV, 22-May-2020.)
⊢ ((𝐵 ∈ (ℝ+ ∖ {1}) ∧ 𝑋 ∈ ℝ) → (𝐵 logb (𝐵↑𝑐𝑋)) = 𝑋)
Theorem	cxplogb 24964	Identity law for the general logarithm. (Contributed by AV, 22-May-2020.)
⊢ ((𝐵 ∈ (ℂ ∖ {0, 1}) ∧ 𝑋 ∈ (ℂ ∖ {0})) → (𝐵↑𝑐(𝐵 logb 𝑋)) = 𝑋)
Theorem	relogbcxpb 24965	The logarithm is the inverse of the exponentiation. Observation in [Cohen4] p. 348. (Contributed by AV, 11-Jun-2020.)
⊢ (((𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1) ∧ 𝑋 ∈ ℝ+ ∧ 𝑌 ∈ ℝ) → ((𝐵 logb 𝑋) = 𝑌 ↔ (𝐵↑𝑐𝑌) = 𝑋))
Theorem	logbmpt 24966*	The general logarithm to a fixed base regarded as mapping. (Contributed by AV, 11-Jun-2020.)
⊢ ((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1) → (curry logb ‘𝐵) = (𝑦 ∈ (ℂ ∖ {0}) ↦ ((log‘𝑦) / (log‘𝐵))))
Theorem	logbf 24967	The general logarithm to a fixed base regarded as function. (Contributed by AV, 11-Jun-2020.)
⊢ ((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1) → (curry logb ‘𝐵):(ℂ ∖ {0})⟶ℂ)
Theorem	logbfval 24968	The general logarithm of a complex number to a fixed base. (Contributed by AV, 11-Jun-2020.)
⊢ (((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1) ∧ 𝑋 ∈ (ℂ ∖ {0})) → ((curry logb ‘𝐵)‘𝑋) = (𝐵 logb 𝑋))
Theorem	relogbf 24969	The general logarithm to a real base greater than 1 regarded as function restricted to the positive integers. Property in [Cohen4] p. 349. (Contributed by AV, 12-Jun-2020.)
⊢ ((𝐵 ∈ ℝ+ ∧ 1 < 𝐵) → ((curry logb ‘𝐵) ↾ ℝ+):ℝ+⟶ℝ)
Theorem	logblog 24970	The general logarithm to the base being Euler's constant regarded as function is the natural logarithm. (Contributed by AV, 12-Jun-2020.)
⊢ (curry logb ‘e) = log
Theorem	logbgt0b 24971	The logarithm of a positive real number to a real base greater than 1 is positive iff the number is greater than 1. (Contributed by AV, 29-Dec-2022.)
⊢ ((𝐴 ∈ ℝ+ ∧ (𝐵 ∈ ℝ+ ∧ 1 < 𝐵)) → (0 < (𝐵 logb 𝐴) ↔ 1 < 𝐴))
Theorem	logbgcd1irr 24972	The logarithm of an integer greater than 1 to an integer base greater than 1 is an irrational number if the argument and the base are relatively prime. For example, (2 logb 9) ∈ (ℝ ∖ ℚ) (see 2logb9irr 24973). (Contributed by AV, 29-Dec-2022.)
⊢ ((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2) ∧ (𝑋 gcd 𝐵) = 1) → (𝐵 logb 𝑋) ∈ (ℝ ∖ ℚ))
Theorem	2logb9irr 24973	Example for logbgcd1irr 24972. The logarithm of nine to base two is irrational. (Contributed by AV, 29-Dec-2022.)
⊢ (2 logb 9) ∈ (ℝ ∖ ℚ)
Theorem	logbprmirr 24974	The logarithm of a prime to a different prime base is an irrational number. For example, (2 logb 3) ∈ (ℝ ∖ ℚ) (see 2logb3irr 24975). (Contributed by AV, 31-Dec-2022.)
⊢ ((𝑋 ∈ ℙ ∧ 𝐵 ∈ ℙ ∧ 𝑋 ≠ 𝐵) → (𝐵 logb 𝑋) ∈ (ℝ ∖ ℚ))
Theorem	2logb3irr 24975	Example for logbprmirr 24974. The logarithm of three to base two is irrational. (Contributed by AV, 31-Dec-2022.)
⊢ (2 logb 3) ∈ (ℝ ∖ ℚ)
Theorem	2logb9irrALT 24976	Alternate proof of 2logb9irr 24973: The logarithm of nine to base two is irrational. (Contributed by AV, 31-Dec-2022.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (2 logb 9) ∈ (ℝ ∖ ℚ)
Theorem	sqrt2cxp2logb9e3 24977	The square root of two to the power of the logarithm of nine to base two is three. (√‘2) and (2 logb 9) are irrational numbers (see sqrt2irr0 15384 resp. 2logb9irr 24973), satisfying the statement in 2irrexpqALT 24978. (Contributed by AV, 29-Dec-2022.)
⊢ ((√‘2)↑𝑐(2 logb 9)) = 3
Theorem	2irrexpqALT 24978*	Alternate proof of 2irrexpq 24913: There exist irrational numbers 𝑎 and 𝑏 such that (𝑎↑𝑏) is rational. Statement in the Metamath book, section 1.1.5, footnote 27 on page 17, and the "constructive proof" for theorem 1.2 of [Bauer], p. 483. In contrast to 2irrexpq 24913, this is a constructive proof because it is based on two explicitly named irrational numbers (√‘2) and (2 logb 9), see sqrt2irr0 15384, 2logb9irr 24973 and sqrt2cxp2logb9e3 24977. Therefore, this proof is also acceptable/usable in intuitionistic logic. (Contributed by AV, 23-Dec-2022.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ ∃𝑎 ∈ (ℝ ∖ ℚ)∃𝑏 ∈ (ℝ ∖ ℚ)(𝑎↑𝑐𝑏) ∈ ℚ
14.3.6  Theorems of Pythagoras, isosceles triangles, and intersecting chords
Theorem	angval 24979*	Define the angle function, which takes two complex numbers, treated as vectors from the origin, and returns the angle between them, in the range ( − π, π]. To convert from the geometry notation, 𝑚𝐴𝐵𝐶, the measure of the angle with legs 𝐴𝐵, 𝐶𝐵 where 𝐶 is more counterclockwise for positive angles, is represented by ((𝐶 − 𝐵)𝐹(𝐴 − 𝐵)). (Contributed by Mario Carneiro, 23-Sep-2014.)
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥))))    ⇒   ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) → (𝐴𝐹𝐵) = (ℑ‘(log‘(𝐵 / 𝐴))))
Theorem	angcan 24980*	Cancel a constant multiplier in the angle function. (Contributed by Mario Carneiro, 23-Sep-2014.)
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥))))    ⇒   ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐶 · 𝐴)𝐹(𝐶 · 𝐵)) = (𝐴𝐹𝐵))
Theorem	angneg 24981*	Cancel a negative sign in the angle function. (Contributed by Mario Carneiro, 23-Sep-2014.)
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥))))    ⇒   ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) → (-𝐴𝐹-𝐵) = (𝐴𝐹𝐵))
Theorem	angvald 24982*	The (signed) angle between two vectors is the argument of their quotient. Deduction form of angval 24979. (Contributed by David Moews, 28-Feb-2017.)
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥))))    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ≠ 0)    &   ⊢ (𝜑 → 𝑌 ∈ ℂ)    &   ⊢ (𝜑 → 𝑌 ≠ 0)    ⇒   ⊢ (𝜑 → (𝑋𝐹𝑌) = (ℑ‘(log‘(𝑌 / 𝑋))))
Theorem	angcld 24983*	The (signed) angle between two vectors is in (-π(,]π). Deduction form. (Contributed by David Moews, 28-Feb-2017.)
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥))))    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ≠ 0)    &   ⊢ (𝜑 → 𝑌 ∈ ℂ)    &   ⊢ (𝜑 → 𝑌 ≠ 0)    ⇒   ⊢ (𝜑 → (𝑋𝐹𝑌) ∈ (-π(,]π))
Theorem	angrteqvd 24984*	Two vectors are at a right angle iff their quotient is purely imaginary. (Contributed by David Moews, 28-Feb-2017.)
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥))))    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ≠ 0)    &   ⊢ (𝜑 → 𝑌 ∈ ℂ)    &   ⊢ (𝜑 → 𝑌 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝑋𝐹𝑌) ∈ {(π / 2), -(π / 2)} ↔ (ℜ‘(𝑌 / 𝑋)) = 0))
Theorem	cosangneg2d 24985*	The cosine of the angle between 𝑋 and -𝑌 is the negative of that between 𝑋 and 𝑌. If A, B and C are collinear points, this implies that the cosines of DBA and DBC sum to zero, i.e., that DBA and DBC are supplementary. (Contributed by David Moews, 28-Feb-2017.)
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥))))    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ≠ 0)    &   ⊢ (𝜑 → 𝑌 ∈ ℂ)    &   ⊢ (𝜑 → 𝑌 ≠ 0)    ⇒   ⊢ (𝜑 → (cos‘(𝑋𝐹-𝑌)) = -(cos‘(𝑋𝐹𝑌)))
Theorem	angrtmuld 24986*	Perpendicularity of two vectors does not change under rescaling the second. (Contributed by David Moews, 28-Feb-2017.)
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥))))    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝑌 ∈ ℂ)    &   ⊢ (𝜑 → 𝑍 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ≠ 0)    &   ⊢ (𝜑 → 𝑌 ≠ 0)    &   ⊢ (𝜑 → 𝑍 ≠ 0)    &   ⊢ (𝜑 → (𝑍 / 𝑌) ∈ ℝ)    ⇒   ⊢ (𝜑 → ((𝑋𝐹𝑌) ∈ {(π / 2), -(π / 2)} ↔ (𝑋𝐹𝑍) ∈ {(π / 2), -(π / 2)}))
Theorem	ang180lem1 24987*	Lemma for ang180 24992. Show that the "revolution number" 𝑁 is an integer, using efeq1 24713 to show that since the product of the three arguments 𝐴, 1 / (1 − 𝐴), (𝐴 − 1) / 𝐴 is -1, the sum of the logarithms must be an integer multiple of 2πi away from πi = log(-1). (Contributed by Mario Carneiro, 23-Sep-2014.)
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥))))    &   ⊢ 𝑇 = (((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))) + (log‘𝐴))    &   ⊢ 𝑁 = (((𝑇 / i) / (2 · π)) − (1 / 2))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (𝑁 ∈ ℤ ∧ (𝑇 / i) ∈ ℝ))
Theorem	ang180lem2 24988*	Lemma for ang180 24992. Show that the revolution number 𝑁 is strictly between -2 and 1. Both bounds are established by iterating using the bounds on the imaginary part of the logarithm, logimcl 24753, but the resulting bound gives only 𝑁 ≤ 1 for the upper bound. The case 𝑁 = 1 is not ruled out here, but it is in some sense an "edge case" that can only happen under very specific conditions; in particular we show that all the angle arguments 𝐴, 1 / (1 − 𝐴), (𝐴 − 1) / 𝐴 must lie on the negative real axis, which is a contradiction because clearly if 𝐴 is negative then the other two are positive real. (Contributed by Mario Carneiro, 23-Sep-2014.)
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥))))    &   ⊢ 𝑇 = (((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))) + (log‘𝐴))    &   ⊢ 𝑁 = (((𝑇 / i) / (2 · π)) − (1 / 2))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (-2 < 𝑁 ∧ 𝑁 < 1))
Theorem	ang180lem3 24989*	Lemma for ang180 24992. Since ang180lem1 24987 shows that 𝑁 is an integer and ang180lem2 24988 shows that 𝑁 is strictly between -2 and 1, it follows that 𝑁 ∈ {-1, 0}, and these two cases correspond to the two possible values for 𝑇. (Contributed by Mario Carneiro, 23-Sep-2014.)
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥))))    &   ⊢ 𝑇 = (((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))) + (log‘𝐴))    &   ⊢ 𝑁 = (((𝑇 / i) / (2 · π)) − (1 / 2))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → 𝑇 ∈ {-(i · π), (i · π)})
Theorem	ang180lem4 24990*	Lemma for ang180 24992. Reduce the statement to one variable. (Contributed by Mario Carneiro, 23-Sep-2014.)
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥))))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((((1 − 𝐴)𝐹1) + (𝐴𝐹(𝐴 − 1))) + (1𝐹𝐴)) ∈ {-π, π})
Theorem	ang180lem5 24991*	Lemma for ang180 24992: Reduce the statement to two variables. (Contributed by Mario Carneiro, 23-Sep-2014.)
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥))))    ⇒   ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ 𝐴 ≠ 𝐵) → ((((𝐴 − 𝐵)𝐹𝐴) + (𝐵𝐹(𝐵 − 𝐴))) + (𝐴𝐹𝐵)) ∈ {-π, π})
Theorem	ang180 24992*	The sum of angles 𝑚𝐴𝐵𝐶 + 𝑚𝐵𝐶𝐴 + 𝑚𝐶𝐴𝐵 in a triangle adds up to either π or -π, i.e. 180 degrees. (The sign is due to the two possible orientations of vertex arrangement and our signed notion of angle). This is Metamath 100 proof #27. (Contributed by Mario Carneiro, 23-Sep-2014.)
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥))))    ⇒   ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐴 ≠ 𝐶)) → ((((𝐶 − 𝐵)𝐹(𝐴 − 𝐵)) + ((𝐴 − 𝐶)𝐹(𝐵 − 𝐶))) + ((𝐵 − 𝐴)𝐹(𝐶 − 𝐴))) ∈ {-π, π})
Theorem	lawcoslem1 24993	Lemma for lawcos 24994. Here we prove the law for a point at the origin and two distinct points U and V, using an expanded version of the signed angle expression on the complex plane. (Contributed by David A. Wheeler, 11-Jun-2015.)
⊢ (𝜑 → 𝑈 ∈ ℂ)    &   ⊢ (𝜑 → 𝑉 ∈ ℂ)    &   ⊢ (𝜑 → 𝑈 ≠ 0)    &   ⊢ (𝜑 → 𝑉 ≠ 0)    ⇒   ⊢ (𝜑 → ((abs‘(𝑈 − 𝑉))↑2) = ((((abs‘𝑈)↑2) + ((abs‘𝑉)↑2)) − (2 · (((abs‘𝑈) · (abs‘𝑉)) · ((ℜ‘(𝑈 / 𝑉)) / (abs‘(𝑈 / 𝑉)))))))
Theorem	lawcos 24994*	Law of cosines (also known as the Al-Kashi theorem or the generalized Pythagorean theorem, or the cosine formula or cosine rule). Given three distinct points A, B, and C, prove a relationship between their segment lengths. This theorem is expressed using the complex number plane as a plane, where 𝐹 is the signed angle construct (as used in ang180 24992), 𝑋 is the distance of line segment BC, 𝑌 is the distance of line segment AC, 𝑍 is the distance of line segment AB, and 𝑂 is the signed angle m/_ BCA on the complex plane. We translate triangle ABC to move C to the origin (C-C), B to U=(B-C), and A to V=(A-C), then use lemma lawcoslem1 24993 to prove this algebraically simpler case. The Metamath convention is to use a signed angle; in this case the sign doesn't matter because we use the cosine of the angle (see cosneg 15279). The Pythagorean theorem pythag 24995 is a special case of the law of cosines. The theorem's expression and approach were suggested by Mario Carneiro. This is Metamath 100 proof #94. (Contributed by David A. Wheeler, 12-Jun-2015.)
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥))))    &   ⊢ 𝑋 = (abs‘(𝐵 − 𝐶))    &   ⊢ 𝑌 = (abs‘(𝐴 − 𝐶))    &   ⊢ 𝑍 = (abs‘(𝐴 − 𝐵))    &   ⊢ 𝑂 = ((𝐵 − 𝐶)𝐹(𝐴 − 𝐶))    ⇒   ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → (𝑍↑2) = (((𝑋↑2) + (𝑌↑2)) − (2 · ((𝑋 · 𝑌) · (cos‘𝑂)))))
Theorem	pythag 24995*	Pythagorean theorem. Given three distinct points A, B, and C that form a right triangle (with the right angle at C), prove a relationship between their segment lengths. This theorem is expressed using the complex number plane as a plane, where 𝐹 is the signed angle construct (as used in ang180 24992), 𝑋 is the distance of line segment BC, 𝑌 is the distance of line segment AC, 𝑍 is the distance of line segment AB (the hypotenuse), and 𝑂 is the signed right angle m/_ BCA. We use the law of cosines lawcos 24994 to prove this, along with simple trigonometry facts like coshalfpi 24659 and cosneg 15279. (Contributed by David A. Wheeler, 13-Jun-2015.)
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥))))    &   ⊢ 𝑋 = (abs‘(𝐵 − 𝐶))    &   ⊢ 𝑌 = (abs‘(𝐴 − 𝐶))    &   ⊢ 𝑍 = (abs‘(𝐴 − 𝐵))    &   ⊢ 𝑂 = ((𝐵 − 𝐶)𝐹(𝐴 − 𝐶))    ⇒   ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ 𝑂 ∈ {(π / 2), -(π / 2)}) → (𝑍↑2) = ((𝑋↑2) + (𝑌↑2)))
Theorem	isosctrlem1 24996	Lemma for isosctr 24999. (Contributed by Saveliy Skresanov, 30-Dec-2016.)
⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → (ℑ‘(log‘(1 − 𝐴))) ≠ π)
Theorem	isosctrlem2 24997	Lemma for isosctr 24999. Corresponds to the case where one vertex is at 0, another at 1 and the third lies on the unit circle. (Contributed by Saveliy Skresanov, 31-Dec-2016.)
⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → (ℑ‘(log‘(1 − 𝐴))) = (ℑ‘(log‘(-𝐴 / (1 − 𝐴)))))
Theorem	isosctrlem3 24998*	Lemma for isosctr 24999. Corresponds to the case where one vertex is at 0. (Contributed by Saveliy Skresanov, 1-Jan-2017.)
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥))))    ⇒   ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ∧ 𝐴 ≠ 𝐵) ∧ (abs‘𝐴) = (abs‘𝐵)) → (-𝐴𝐹(𝐵 − 𝐴)) = ((𝐴 − 𝐵)𝐹-𝐵))
Theorem	isosctr 24999*	Isosceles triangle theorem. This is Metamath 100 proof #65. (Contributed by Saveliy Skresanov, 1-Jan-2017.)
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥))))    ⇒   ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ∧ 𝐴 ≠ 𝐵) ∧ (abs‘(𝐴 − 𝐶)) = (abs‘(𝐵 − 𝐶))) → ((𝐶 − 𝐴)𝐹(𝐵 − 𝐴)) = ((𝐴 − 𝐵)𝐹(𝐶 − 𝐵)))
Theorem	ssscongptld 25000*	If two triangles have equal sides, one angle in one triangle has the same cosine as the corresponding angle in the other triangle. This is a partial form of the SSS congruence theorem. This theorem is proven by using lawcos 24994 on both triangles to express one side in terms of the other two, and then equating these expressions and reducing this algebraically to get an equality of cosines of angles. (Contributed by David Moews, 28-Feb-2017.)
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥))))    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → 𝐸 ∈ ℂ)    &   ⊢ (𝜑 → 𝐺 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    &   ⊢ (𝜑 → 𝐷 ≠ 𝐸)    &   ⊢ (𝜑 → 𝐸 ≠ 𝐺)    &   ⊢ (𝜑 → (abs‘(𝐴 − 𝐵)) = (abs‘(𝐷 − 𝐸)))    &   ⊢ (𝜑 → (abs‘(𝐵 − 𝐶)) = (abs‘(𝐸 − 𝐺)))    &   ⊢ (𝜑 → (abs‘(𝐶 − 𝐴)) = (abs‘(𝐺 − 𝐷)))    ⇒   ⊢ (𝜑 → (cos‘((𝐴 − 𝐵)𝐹(𝐶 − 𝐵))) = (cos‘((𝐷 − 𝐸)𝐹(𝐺 − 𝐸))))