P. 260 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 25901-26000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dcubic 25901*	Solutions to the depressed cubic, a special case of cubic 25904. (The definitions of 𝑀, 𝑁, 𝐺, 𝑇 here differ from mcubic 25902 by scale factors of -9, 54, 54 and -27 respectively, to simplify the algebra and presentation.) (Contributed by Mario Carneiro, 26-Apr-2015.)
⊢ (𝜑 → 𝑃 ∈ ℂ)    &   ⊢ (𝜑 → 𝑄 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝑇 ∈ ℂ)    &   ⊢ (𝜑 → (𝑇↑3) = (𝐺 − 𝑁))    &   ⊢ (𝜑 → 𝐺 ∈ ℂ)    &   ⊢ (𝜑 → (𝐺↑2) = ((𝑁↑2) + (𝑀↑3)))    &   ⊢ (𝜑 → 𝑀 = (𝑃 / 3))    &   ⊢ (𝜑 → 𝑁 = (𝑄 / 2))    &   ⊢ (𝜑 → 𝑇 ≠ 0)    ⇒   ⊢ (𝜑 → (((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0 ↔ ∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))))
Theorem	mcubic 25902*	Solutions to a monic cubic equation, a special case of cubic 25904. (Contributed by Mario Carneiro, 24-Apr-2015.)
⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝑇 ∈ ℂ)    &   ⊢ (𝜑 → (𝑇↑3) = ((𝑁 + 𝐺) / 2))    &   ⊢ (𝜑 → 𝐺 ∈ ℂ)    &   ⊢ (𝜑 → (𝐺↑2) = ((𝑁↑2) − (4 · (𝑀↑3))))    &   ⊢ (𝜑 → 𝑀 = ((𝐵↑2) − (3 · 𝐶)))    &   ⊢ (𝜑 → 𝑁 = (((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) + (;27 · 𝐷)))    &   ⊢ (𝜑 → 𝑇 ≠ 0)    ⇒   ⊢ (𝜑 → ((((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((𝐶 · 𝑋) + 𝐷)) = 0 ↔ ∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ 𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3))))
Theorem	cubic2 25903*	The solution to the general cubic equation, for arbitrary choices 𝐺 and 𝑇 of the square and cube roots. (Contributed by Mario Carneiro, 23-Apr-2015.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝑇 ∈ ℂ)    &   ⊢ (𝜑 → (𝑇↑3) = ((𝑁 + 𝐺) / 2))    &   ⊢ (𝜑 → 𝐺 ∈ ℂ)    &   ⊢ (𝜑 → (𝐺↑2) = ((𝑁↑2) − (4 · (𝑀↑3))))    &   ⊢ (𝜑 → 𝑀 = ((𝐵↑2) − (3 · (𝐴 · 𝐶))))    &   ⊢ (𝜑 → 𝑁 = (((2 · (𝐵↑3)) − ((9 · 𝐴) · (𝐵 · 𝐶))) + (;27 · ((𝐴↑2) · 𝐷))))    &   ⊢ (𝜑 → 𝑇 ≠ 0)    ⇒   ⊢ (𝜑 → ((((𝐴 · (𝑋↑3)) + (𝐵 · (𝑋↑2))) + ((𝐶 · 𝑋) + 𝐷)) = 0 ↔ ∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ 𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / (3 · 𝐴)))))
Theorem	cubic 25904*	The cubic equation, which gives the roots of an arbitrary (nondegenerate) cubic function. Use rextp 4639 to convert the existential quantifier to a triple disjunction. This is Metamath 100 proof #37. (Contributed by Mario Carneiro, 26-Apr-2015.)
⊢ 𝑅 = {1, ((-1 + (i · (√‘3))) / 2), ((-1 − (i · (√‘3))) / 2)}    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝑇 = (((𝑁 + (√‘𝐺)) / 2)↑𝑐(1 / 3)))    &   ⊢ (𝜑 → 𝐺 = ((𝑁↑2) − (4 · (𝑀↑3))))    &   ⊢ (𝜑 → 𝑀 = ((𝐵↑2) − (3 · (𝐴 · 𝐶))))    &   ⊢ (𝜑 → 𝑁 = (((2 · (𝐵↑3)) − ((9 · 𝐴) · (𝐵 · 𝐶))) + (;27 · ((𝐴↑2) · 𝐷))))    &   ⊢ (𝜑 → 𝑀 ≠ 0)    ⇒   ⊢ (𝜑 → ((((𝐴 · (𝑋↑3)) + (𝐵 · (𝑋↑2))) + ((𝐶 · 𝑋) + 𝐷)) = 0 ↔ ∃𝑟 ∈ 𝑅 𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / (3 · 𝐴))))
Theorem	binom4 25905	Work out a quartic binomial. (You would think that by this point it would be faster to use binom 15470, but it turns out to be just as much work to put it into this form after clearing all the sums and calculating binomial coefficients.) (Contributed by Mario Carneiro, 6-May-2015.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵)↑4) = (((𝐴↑4) + (4 · ((𝐴↑3) · 𝐵))) + ((6 · ((𝐴↑2) · (𝐵↑2))) + ((4 · (𝐴 · (𝐵↑3))) + (𝐵↑4)))))
Theorem	dquartlem1 25906	Lemma for dquart 25908. (Contributed by Mario Carneiro, 6-May-2015.)
⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝑆 ∈ ℂ)    &   ⊢ (𝜑 → 𝑀 = ((2 · 𝑆)↑2))    &   ⊢ (𝜑 → 𝑀 ≠ 0)    &   ⊢ (𝜑 → 𝐼 ∈ ℂ)    &   ⊢ (𝜑 → (𝐼↑2) = ((-(𝑆↑2) − (𝐵 / 2)) + ((𝐶 / 4) / 𝑆)))    ⇒   ⊢ (𝜑 → ((((𝑋↑2) + ((𝑀 + 𝐵) / 2)) + ((((𝑀 / 2) · 𝑋) − (𝐶 / 4)) / 𝑆)) = 0 ↔ (𝑋 = (-𝑆 + 𝐼) ∨ 𝑋 = (-𝑆 − 𝐼))))
Theorem	dquartlem2 25907	Lemma for dquart 25908. (Contributed by Mario Carneiro, 6-May-2015.)
⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝑆 ∈ ℂ)    &   ⊢ (𝜑 → 𝑀 = ((2 · 𝑆)↑2))    &   ⊢ (𝜑 → 𝑀 ≠ 0)    &   ⊢ (𝜑 → 𝐼 ∈ ℂ)    &   ⊢ (𝜑 → (𝐼↑2) = ((-(𝑆↑2) − (𝐵 / 2)) + ((𝐶 / 4) / 𝑆)))    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → (((𝑀↑3) + ((2 · 𝐵) · (𝑀↑2))) + ((((𝐵↑2) − (4 · 𝐷)) · 𝑀) + -(𝐶↑2))) = 0)    ⇒   ⊢ (𝜑 → ((((𝑀 + 𝐵) / 2)↑2) − (((𝐶↑2) / 4) / 𝑀)) = 𝐷)
Theorem	dquart 25908	Solve a depressed quartic equation. To eliminate 𝑆, which is the square root of a solution 𝑀 to the resolvent cubic equation, apply cubic 25904 or one of its variants. (Contributed by Mario Carneiro, 6-May-2015.)
⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝑆 ∈ ℂ)    &   ⊢ (𝜑 → 𝑀 = ((2 · 𝑆)↑2))    &   ⊢ (𝜑 → 𝑀 ≠ 0)    &   ⊢ (𝜑 → 𝐼 ∈ ℂ)    &   ⊢ (𝜑 → (𝐼↑2) = ((-(𝑆↑2) − (𝐵 / 2)) + ((𝐶 / 4) / 𝑆)))    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → (((𝑀↑3) + ((2 · 𝐵) · (𝑀↑2))) + ((((𝐵↑2) − (4 · 𝐷)) · 𝑀) + -(𝐶↑2))) = 0)    &   ⊢ (𝜑 → 𝐽 ∈ ℂ)    &   ⊢ (𝜑 → (𝐽↑2) = ((-(𝑆↑2) − (𝐵 / 2)) − ((𝐶 / 4) / 𝑆)))    ⇒   ⊢ (𝜑 → ((((𝑋↑4) + (𝐵 · (𝑋↑2))) + ((𝐶 · 𝑋) + 𝐷)) = 0 ↔ ((𝑋 = (-𝑆 + 𝐼) ∨ 𝑋 = (-𝑆 − 𝐼)) ∨ (𝑋 = (𝑆 + 𝐽) ∨ 𝑋 = (𝑆 − 𝐽)))))
Theorem	quart1cl 25909	Closure lemmas for quart 25916. (Contributed by Mario Carneiro, 7-May-2015.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → 𝑃 = (𝐵 − ((3 / 8) · (𝐴↑2))))    &   ⊢ (𝜑 → 𝑄 = ((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8)))    &   ⊢ (𝜑 → 𝑅 = ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))    ⇒   ⊢ (𝜑 → (𝑃 ∈ ℂ ∧ 𝑄 ∈ ℂ ∧ 𝑅 ∈ ℂ))
Theorem	quart1lem 25910	Lemma for quart1 25911. (Contributed by Mario Carneiro, 6-May-2015.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → 𝑃 = (𝐵 − ((3 / 8) · (𝐴↑2))))    &   ⊢ (𝜑 → 𝑄 = ((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8)))    &   ⊢ (𝜑 → 𝑅 = ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝑌 = (𝑋 + (𝐴 / 4)))    ⇒   ⊢ (𝜑 → 𝐷 = ((((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2))) + ((𝑄 · (𝐴 / 4)) + 𝑅)))
Theorem	quart1 25911	Depress a quartic equation. (Contributed by Mario Carneiro, 6-May-2015.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → 𝑃 = (𝐵 − ((3 / 8) · (𝐴↑2))))    &   ⊢ (𝜑 → 𝑄 = ((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8)))    &   ⊢ (𝜑 → 𝑅 = ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝑌 = (𝑋 + (𝐴 / 4)))    ⇒   ⊢ (𝜑 → (((𝑋↑4) + (𝐴 · (𝑋↑3))) + ((𝐵 · (𝑋↑2)) + ((𝐶 · 𝑋) + 𝐷))) = (((𝑌↑4) + (𝑃 · (𝑌↑2))) + ((𝑄 · 𝑌) + 𝑅)))
Theorem	quartlem1 25912	Lemma for quart 25916. (Contributed by Mario Carneiro, 6-May-2015.)
⊢ (𝜑 → 𝑃 ∈ ℂ)    &   ⊢ (𝜑 → 𝑄 ∈ ℂ)    &   ⊢ (𝜑 → 𝑅 ∈ ℂ)    &   ⊢ (𝜑 → 𝑈 = ((𝑃↑2) + (;12 · 𝑅)))    &   ⊢ (𝜑 → 𝑉 = ((-(2 · (𝑃↑3)) − (;27 · (𝑄↑2))) + (;72 · (𝑃 · 𝑅))))    ⇒   ⊢ (𝜑 → (𝑈 = (((2 · 𝑃)↑2) − (3 · ((𝑃↑2) − (4 · 𝑅)))) ∧ 𝑉 = (((2 · ((2 · 𝑃)↑3)) − (9 · ((2 · 𝑃) · ((𝑃↑2) − (4 · 𝑅))))) + (;27 · -(𝑄↑2)))))
Theorem	quartlem2 25913	Closure lemmas for quart 25916. (Contributed by Mario Carneiro, 7-May-2015.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝐸 = -(𝐴 / 4))    &   ⊢ (𝜑 → 𝑃 = (𝐵 − ((3 / 8) · (𝐴↑2))))    &   ⊢ (𝜑 → 𝑄 = ((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8)))    &   ⊢ (𝜑 → 𝑅 = ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))    &   ⊢ (𝜑 → 𝑈 = ((𝑃↑2) + (;12 · 𝑅)))    &   ⊢ (𝜑 → 𝑉 = ((-(2 · (𝑃↑3)) − (;27 · (𝑄↑2))) + (;72 · (𝑃 · 𝑅))))    &   ⊢ (𝜑 → 𝑊 = (√‘((𝑉↑2) − (4 · (𝑈↑3)))))    ⇒   ⊢ (𝜑 → (𝑈 ∈ ℂ ∧ 𝑉 ∈ ℂ ∧ 𝑊 ∈ ℂ))
Theorem	quartlem3 25914	Closure lemmas for quart 25916. (Contributed by Mario Carneiro, 7-May-2015.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝐸 = -(𝐴 / 4))    &   ⊢ (𝜑 → 𝑃 = (𝐵 − ((3 / 8) · (𝐴↑2))))    &   ⊢ (𝜑 → 𝑄 = ((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8)))    &   ⊢ (𝜑 → 𝑅 = ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))    &   ⊢ (𝜑 → 𝑈 = ((𝑃↑2) + (;12 · 𝑅)))    &   ⊢ (𝜑 → 𝑉 = ((-(2 · (𝑃↑3)) − (;27 · (𝑄↑2))) + (;72 · (𝑃 · 𝑅))))    &   ⊢ (𝜑 → 𝑊 = (√‘((𝑉↑2) − (4 · (𝑈↑3)))))    &   ⊢ (𝜑 → 𝑆 = ((√‘𝑀) / 2))    &   ⊢ (𝜑 → 𝑀 = -((((2 · 𝑃) + 𝑇) + (𝑈 / 𝑇)) / 3))    &   ⊢ (𝜑 → 𝑇 = (((𝑉 + 𝑊) / 2)↑𝑐(1 / 3)))    &   ⊢ (𝜑 → 𝑇 ≠ 0)    ⇒   ⊢ (𝜑 → (𝑆 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝑇 ∈ ℂ))
Theorem	quartlem4 25915	Closure lemmas for quart 25916. (Contributed by Mario Carneiro, 7-May-2015.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝐸 = -(𝐴 / 4))    &   ⊢ (𝜑 → 𝑃 = (𝐵 − ((3 / 8) · (𝐴↑2))))    &   ⊢ (𝜑 → 𝑄 = ((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8)))    &   ⊢ (𝜑 → 𝑅 = ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))    &   ⊢ (𝜑 → 𝑈 = ((𝑃↑2) + (;12 · 𝑅)))    &   ⊢ (𝜑 → 𝑉 = ((-(2 · (𝑃↑3)) − (;27 · (𝑄↑2))) + (;72 · (𝑃 · 𝑅))))    &   ⊢ (𝜑 → 𝑊 = (√‘((𝑉↑2) − (4 · (𝑈↑3)))))    &   ⊢ (𝜑 → 𝑆 = ((√‘𝑀) / 2))    &   ⊢ (𝜑 → 𝑀 = -((((2 · 𝑃) + 𝑇) + (𝑈 / 𝑇)) / 3))    &   ⊢ (𝜑 → 𝑇 = (((𝑉 + 𝑊) / 2)↑𝑐(1 / 3)))    &   ⊢ (𝜑 → 𝑇 ≠ 0)    &   ⊢ (𝜑 → 𝑀 ≠ 0)    &   ⊢ (𝜑 → 𝐼 = (√‘((-(𝑆↑2) − (𝑃 / 2)) + ((𝑄 / 4) / 𝑆))))    &   ⊢ (𝜑 → 𝐽 = (√‘((-(𝑆↑2) − (𝑃 / 2)) − ((𝑄 / 4) / 𝑆))))    ⇒   ⊢ (𝜑 → (𝑆 ≠ 0 ∧ 𝐼 ∈ ℂ ∧ 𝐽 ∈ ℂ))
Theorem	quart 25916	The quartic equation, writing out all roots using square and cube root functions so that only direct substitutions remain, and we can actually claim to have a "quartic equation". Naturally, this theorem is ridiculously long (see quartfull 33027) if all the substitutions are performed. This is Metamath 100 proof #46. (Contributed by Mario Carneiro, 6-May-2015.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝐸 = -(𝐴 / 4))    &   ⊢ (𝜑 → 𝑃 = (𝐵 − ((3 / 8) · (𝐴↑2))))    &   ⊢ (𝜑 → 𝑄 = ((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8)))    &   ⊢ (𝜑 → 𝑅 = ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))    &   ⊢ (𝜑 → 𝑈 = ((𝑃↑2) + (;12 · 𝑅)))    &   ⊢ (𝜑 → 𝑉 = ((-(2 · (𝑃↑3)) − (;27 · (𝑄↑2))) + (;72 · (𝑃 · 𝑅))))    &   ⊢ (𝜑 → 𝑊 = (√‘((𝑉↑2) − (4 · (𝑈↑3)))))    &   ⊢ (𝜑 → 𝑆 = ((√‘𝑀) / 2))    &   ⊢ (𝜑 → 𝑀 = -((((2 · 𝑃) + 𝑇) + (𝑈 / 𝑇)) / 3))    &   ⊢ (𝜑 → 𝑇 = (((𝑉 + 𝑊) / 2)↑𝑐(1 / 3)))    &   ⊢ (𝜑 → 𝑇 ≠ 0)    &   ⊢ (𝜑 → 𝑀 ≠ 0)    &   ⊢ (𝜑 → 𝐼 = (√‘((-(𝑆↑2) − (𝑃 / 2)) + ((𝑄 / 4) / 𝑆))))    &   ⊢ (𝜑 → 𝐽 = (√‘((-(𝑆↑2) − (𝑃 / 2)) − ((𝑄 / 4) / 𝑆))))    ⇒   ⊢ (𝜑 → ((((𝑋↑4) + (𝐴 · (𝑋↑3))) + ((𝐵 · (𝑋↑2)) + ((𝐶 · 𝑋) + 𝐷))) = 0 ↔ ((𝑋 = ((𝐸 − 𝑆) + 𝐼) ∨ 𝑋 = ((𝐸 − 𝑆) − 𝐼)) ∨ (𝑋 = ((𝐸 + 𝑆) + 𝐽) ∨ 𝑋 = ((𝐸 + 𝑆) − 𝐽)))))
14.3.8  Inverse trigonometric functions
Syntax	casin 25917	The arcsine function.
class arcsin
Syntax	cacos 25918	The arccosine function.
class arccos
Syntax	catan 25919	The arctangent function.
class arctan
Definition	df-asin 25920	Define the arcsine function. Because sin is not a one-to-one function, the literal inverse ◡sin is not a function. Rather than attempt to find the right domain on which to restrict sin in order to get a total function, we just define it in terms of log, which we already know is total (except at 0). There are branch points at -1 and 1 (at which the function is defined), and branch cuts along the real line not between -1 and 1, which is to say (-∞, -1) ∪ (1, +∞). (Contributed by Mario Carneiro, 31-Mar-2015.)
⊢ arcsin = (𝑥 ∈ ℂ ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2)))))))
Definition	df-acos 25921	Define the arccosine function. See also remarks for df-asin 25920. Since we define arccos in terms of arcsin, it shares the same branch points and cuts, namely (-∞, -1) ∪ (1, +∞). (Contributed by Mario Carneiro, 31-Mar-2015.)
⊢ arccos = (𝑥 ∈ ℂ ↦ ((π / 2) − (arcsin‘𝑥)))
Definition	df-atan 25922	Define the arctangent function. See also remarks for df-asin 25920. Unlike arcsin and arccos, this function is not defined everywhere, because tan(𝑧) ≠ ±i for all 𝑧 ∈ ℂ. For all other 𝑧, there is a formula for arctan(𝑧) in terms of log, and we take that as the definition. Branch points are at ±i; branch cuts are on the pure imaginary axis not between -i and i, which is to say {𝑧 ∈ ℂ ∣ (i · 𝑧) ∈ (-∞, -1) ∪ (1, +∞)}. (Contributed by Mario Carneiro, 31-Mar-2015.)
⊢ arctan = (𝑥 ∈ (ℂ ∖ {-i, i}) ↦ ((i / 2) · ((log‘(1 − (i · 𝑥))) − (log‘(1 + (i · 𝑥))))))
Theorem	asinlem 25923	The argument to the logarithm in df-asin 25920 is always nonzero. (Contributed by Mario Carneiro, 31-Mar-2015.)
⊢ (𝐴 ∈ ℂ → ((i · 𝐴) + (√‘(1 − (𝐴↑2)))) ≠ 0)
Theorem	asinlem2 25924	The argument to the logarithm in df-asin 25920 has the property that replacing 𝐴 with -𝐴 in the expression gives the reciprocal. (Contributed by Mario Carneiro, 1-Apr-2015.)
⊢ (𝐴 ∈ ℂ → (((i · 𝐴) + (√‘(1 − (𝐴↑2)))) · ((i · -𝐴) + (√‘(1 − (-𝐴↑2))))) = 1)
Theorem	asinlem3a 25925	Lemma for asinlem3 25926. (Contributed by Mario Carneiro, 1-Apr-2015.)
⊢ ((𝐴 ∈ ℂ ∧ (ℑ‘𝐴) ≤ 0) → 0 ≤ (ℜ‘((i · 𝐴) + (√‘(1 − (𝐴↑2))))))
Theorem	asinlem3 25926	The argument to the logarithm in df-asin 25920 has nonnegative real part. (Contributed by Mario Carneiro, 1-Apr-2015.)
⊢ (𝐴 ∈ ℂ → 0 ≤ (ℜ‘((i · 𝐴) + (√‘(1 − (𝐴↑2))))))
Theorem	asinf 25927	Domain and range of the arcsin function. (Contributed by Mario Carneiro, 31-Mar-2015.)
⊢ arcsin:ℂ⟶ℂ
Theorem	asincl 25928	Closure for the arcsin function. (Contributed by Mario Carneiro, 31-Mar-2015.)
⊢ (𝐴 ∈ ℂ → (arcsin‘𝐴) ∈ ℂ)
Theorem	acosf 25929	Domain and range of the arccos function. (Contributed by Mario Carneiro, 31-Mar-2015.)
⊢ arccos:ℂ⟶ℂ
Theorem	acoscl 25930	Closure for the arccos function. (Contributed by Mario Carneiro, 31-Mar-2015.)
⊢ (𝐴 ∈ ℂ → (arccos‘𝐴) ∈ ℂ)
Theorem	atandm 25931	Since the property is a little lengthy, we abbreviate 𝐴 ∈ ℂ ∧ 𝐴 ≠ -i ∧ 𝐴 ≠ i as 𝐴 ∈ dom arctan. This is the necessary precondition for the definition of arctan to make sense. (Contributed by Mario Carneiro, 31-Mar-2015.)
⊢ (𝐴 ∈ dom arctan ↔ (𝐴 ∈ ℂ ∧ 𝐴 ≠ -i ∧ 𝐴 ≠ i))
Theorem	atandm2 25932	This form of atandm 25931 is a bit more useful for showing that the logarithms in df-atan 25922 are well-defined. (Contributed by Mario Carneiro, 31-Mar-2015.)
⊢ (𝐴 ∈ dom arctan ↔ (𝐴 ∈ ℂ ∧ (1 − (i · 𝐴)) ≠ 0 ∧ (1 + (i · 𝐴)) ≠ 0))
Theorem	atandm3 25933	A compact form of atandm 25931. (Contributed by Mario Carneiro, 31-Mar-2015.)
⊢ (𝐴 ∈ dom arctan ↔ (𝐴 ∈ ℂ ∧ (𝐴↑2) ≠ -1))
Theorem	atandm4 25934	A compact form of atandm 25931. (Contributed by Mario Carneiro, 3-Apr-2015.)
⊢ (𝐴 ∈ dom arctan ↔ (𝐴 ∈ ℂ ∧ (1 + (𝐴↑2)) ≠ 0))
Theorem	atanf 25935	Domain and range of the arctan function. (Contributed by Mario Carneiro, 31-Mar-2015.)
⊢ arctan:(ℂ ∖ {-i, i})⟶ℂ
Theorem	atancl 25936	Closure for the arctan function. (Contributed by Mario Carneiro, 31-Mar-2015.)
⊢ (𝐴 ∈ dom arctan → (arctan‘𝐴) ∈ ℂ)
Theorem	asinval 25937	Value of the arcsin function. (Contributed by Mario Carneiro, 31-Mar-2015.)
⊢ (𝐴 ∈ ℂ → (arcsin‘𝐴) = (-i · (log‘((i · 𝐴) + (√‘(1 − (𝐴↑2)))))))
Theorem	acosval 25938	Value of the arccos function. (Contributed by Mario Carneiro, 31-Mar-2015.)
⊢ (𝐴 ∈ ℂ → (arccos‘𝐴) = ((π / 2) − (arcsin‘𝐴)))
Theorem	atanval 25939	Value of the arctan function. (Contributed by Mario Carneiro, 31-Mar-2015.)
⊢ (𝐴 ∈ dom arctan → (arctan‘𝐴) = ((i / 2) · ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i · 𝐴))))))
Theorem	atanre 25940	A real number is in the domain of the arctangent function. (Contributed by Mario Carneiro, 31-Mar-2015.)
⊢ (𝐴 ∈ ℝ → 𝐴 ∈ dom arctan)
Theorem	asinneg 25941	The arcsine function is odd. (Contributed by Mario Carneiro, 1-Apr-2015.)
⊢ (𝐴 ∈ ℂ → (arcsin‘-𝐴) = -(arcsin‘𝐴))
Theorem	acosneg 25942	The negative symmetry relation of the arccosine. (Contributed by Mario Carneiro, 2-Apr-2015.)
⊢ (𝐴 ∈ ℂ → (arccos‘-𝐴) = (π − (arccos‘𝐴)))
Theorem	efiasin 25943	The exponential of the arcsine function. (Contributed by Mario Carneiro, 31-Mar-2015.)
⊢ (𝐴 ∈ ℂ → (exp‘(i · (arcsin‘𝐴))) = ((i · 𝐴) + (√‘(1 − (𝐴↑2)))))
Theorem	sinasin 25944	The arcsine function is an inverse to sin. This is the main property that justifies the notation arcsin or sin↑-1. Because sin is not an injection, the other converse identity asinsin 25947 is only true under limited circumstances. (Contributed by Mario Carneiro, 1-Apr-2015.)
⊢ (𝐴 ∈ ℂ → (sin‘(arcsin‘𝐴)) = 𝐴)
Theorem	cosacos 25945	The arccosine function is an inverse to cos. (Contributed by Mario Carneiro, 1-Apr-2015.)
⊢ (𝐴 ∈ ℂ → (cos‘(arccos‘𝐴)) = 𝐴)
Theorem	asinsinlem 25946	Lemma for asinsin 25947. (Contributed by Mario Carneiro, 2-Apr-2015.)
⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → 0 < (ℜ‘(exp‘(i · 𝐴))))
Theorem	asinsin 25947	The arcsine function composed with sin is equal to the identity. This plus sinasin 25944 allow us to view sin and arcsin as inverse operations to each other. For ease of use, we have not defined precisely the correct domain of correctness of this identity; in addition to the main region described here it is also true for some points on the branch cuts, namely when 𝐴 = (π / 2) − i𝑦 for nonnegative real 𝑦 and also symmetrically at 𝐴 = i𝑦 − (π / 2). In particular, when restricted to reals this identity extends to the closed interval [-(π / 2), (π / 2)], not just the open interval (see reasinsin 25951). (Contributed by Mario Carneiro, 2-Apr-2015.)
⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (arcsin‘(sin‘𝐴)) = 𝐴)
Theorem	acoscos 25948	The arccosine function is an inverse to cos. (Contributed by Mario Carneiro, 2-Apr-2015.)
⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (0(,)π)) → (arccos‘(cos‘𝐴)) = 𝐴)
Theorem	asin1 25949	The arcsine of 1 is π / 2. (Contributed by Mario Carneiro, 2-Apr-2015.)
⊢ (arcsin‘1) = (π / 2)
Theorem	acos1 25950	The arccosine of 1 is 0. (Contributed by Mario Carneiro, 2-Apr-2015.)
⊢ (arccos‘1) = 0
Theorem	reasinsin 25951	The arcsine function composed with sin is equal to the identity. (Contributed by Mario Carneiro, 2-Apr-2015.)
⊢ (𝐴 ∈ (-(π / 2)[,](π / 2)) → (arcsin‘(sin‘𝐴)) = 𝐴)
Theorem	asinsinb 25952	Relationship between sine and arcsine. (Contributed by Mario Carneiro, 2-Apr-2015.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (ℜ‘𝐵) ∈ (-(π / 2)(,)(π / 2))) → ((arcsin‘𝐴) = 𝐵 ↔ (sin‘𝐵) = 𝐴))
Theorem	acoscosb 25953	Relationship between cosine and arccosine. (Contributed by Mario Carneiro, 2-Apr-2015.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (ℜ‘𝐵) ∈ (0(,)π)) → ((arccos‘𝐴) = 𝐵 ↔ (cos‘𝐵) = 𝐴))
Theorem	asinbnd 25954	The arcsine function has range within a vertical strip of the complex plane with real part between -π / 2 and π / 2. (Contributed by Mario Carneiro, 2-Apr-2015.)
⊢ (𝐴 ∈ ℂ → (ℜ‘(arcsin‘𝐴)) ∈ (-(π / 2)[,](π / 2)))
Theorem	acosbnd 25955	The arccosine function has range within a vertical strip of the complex plane with real part between 0 and π. (Contributed by Mario Carneiro, 2-Apr-2015.)
⊢ (𝐴 ∈ ℂ → (ℜ‘(arccos‘𝐴)) ∈ (0[,]π))
Theorem	asinrebnd 25956	Bounds on the arcsine function. (Contributed by Mario Carneiro, 2-Apr-2015.)
⊢ (𝐴 ∈ (-1[,]1) → (arcsin‘𝐴) ∈ (-(π / 2)[,](π / 2)))
Theorem	asinrecl 25957	The arcsine function is real in its principal domain. (Contributed by Mario Carneiro, 2-Apr-2015.)
⊢ (𝐴 ∈ (-1[,]1) → (arcsin‘𝐴) ∈ ℝ)
Theorem	acosrecl 25958	The arccosine function is real in its principal domain. (Contributed by Mario Carneiro, 2-Apr-2015.)
⊢ (𝐴 ∈ (-1[,]1) → (arccos‘𝐴) ∈ ℝ)
Theorem	cosasin 25959	The cosine of the arcsine of 𝐴 is √(1 − 𝐴↑2). (Contributed by Mario Carneiro, 2-Apr-2015.)
⊢ (𝐴 ∈ ℂ → (cos‘(arcsin‘𝐴)) = (√‘(1 − (𝐴↑2))))
Theorem	sinacos 25960	The sine of the arccosine of 𝐴 is √(1 − 𝐴↑2). (Contributed by Mario Carneiro, 2-Apr-2015.)
⊢ (𝐴 ∈ ℂ → (sin‘(arccos‘𝐴)) = (√‘(1 − (𝐴↑2))))
Theorem	atandmneg 25961	The domain of the arctangent function is closed under negatives. (Contributed by Mario Carneiro, 3-Apr-2015.)
⊢ (𝐴 ∈ dom arctan → -𝐴 ∈ dom arctan)
Theorem	atanneg 25962	The arctangent function is odd. (Contributed by Mario Carneiro, 3-Apr-2015.)
⊢ (𝐴 ∈ dom arctan → (arctan‘-𝐴) = -(arctan‘𝐴))
Theorem	atan0 25963	The arctangent of zero is zero. (Contributed by Mario Carneiro, 31-Mar-2015.)
⊢ (arctan‘0) = 0
Theorem	atandmcj 25964	The arctangent function distributes under conjugation. (Contributed by Mario Carneiro, 31-Mar-2015.)
⊢ (𝐴 ∈ dom arctan → (∗‘𝐴) ∈ dom arctan)
Theorem	atancj 25965	The arctangent function distributes under conjugation. (The condition that ℜ(𝐴) ≠ 0 is necessary because the branch cuts are chosen so that the negative imaginary line "agrees with" neighboring values with negative real part, while the positive imaginary line agrees with values with positive real part. This makes atanneg 25962 true unconditionally but messes up conjugation symmetry, and it is impossible to have both in a single-valued function. The claim is true on the imaginary line between -1 and 1, though.) (Contributed by Mario Carneiro, 31-Mar-2015.)
⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (𝐴 ∈ dom arctan ∧ (∗‘(arctan‘𝐴)) = (arctan‘(∗‘𝐴))))
Theorem	atanrecl 25966	The arctangent function is real for all real inputs. (Contributed by Mario Carneiro, 31-Mar-2015.)
⊢ (𝐴 ∈ ℝ → (arctan‘𝐴) ∈ ℝ)
Theorem	efiatan 25967	Value of the exponential of an artcangent. (Contributed by Mario Carneiro, 2-Apr-2015.)
⊢ (𝐴 ∈ dom arctan → (exp‘(i · (arctan‘𝐴))) = ((√‘(1 + (i · 𝐴))) / (√‘(1 − (i · 𝐴)))))
Theorem	atanlogaddlem 25968	Lemma for atanlogadd 25969. (Contributed by Mario Carneiro, 3-Apr-2015.)
⊢ ((𝐴 ∈ dom arctan ∧ 0 ≤ (ℜ‘𝐴)) → ((log‘(1 + (i · 𝐴))) + (log‘(1 − (i · 𝐴)))) ∈ ran log)
Theorem	atanlogadd 25969	The rule √(𝑧𝑤) = (√𝑧)(√𝑤) is not always true on the complex numbers, but it is true when the arguments of 𝑧 and 𝑤 sum to within the interval (-π, π], so there are some cases such as this one with 𝑧 = 1 + i𝐴 and 𝑤 = 1 − i𝐴 which are true unconditionally. This result can also be stated as "√(1 + 𝑧) + √(1 − 𝑧) is analytic". (Contributed by Mario Carneiro, 3-Apr-2015.)
⊢ (𝐴 ∈ dom arctan → ((log‘(1 + (i · 𝐴))) + (log‘(1 − (i · 𝐴)))) ∈ ran log)
Theorem	atanlogsublem 25970	Lemma for atanlogsub 25971. (Contributed by Mario Carneiro, 4-Apr-2015.)
⊢ ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1 − (i · 𝐴))))) ∈ (-π(,)π))
Theorem	atanlogsub 25971	A variation on atanlogadd 25969, to show that √(1 + i𝑧) / √(1 − i𝑧) = √((1 + i𝑧) / (1 − i𝑧)) under more limited conditions. (Contributed by Mario Carneiro, 4-Apr-2015.)
⊢ ((𝐴 ∈ dom arctan ∧ (ℜ‘𝐴) ≠ 0) → ((log‘(1 + (i · 𝐴))) − (log‘(1 − (i · 𝐴)))) ∈ ran log)
Theorem	efiatan2 25972	Value of the exponential of an artcangent. (Contributed by Mario Carneiro, 3-Apr-2015.)
⊢ (𝐴 ∈ dom arctan → (exp‘(i · (arctan‘𝐴))) = ((1 + (i · 𝐴)) / (√‘(1 + (𝐴↑2)))))
Theorem	2efiatan 25973	Value of the exponential of an artcangent. (Contributed by Mario Carneiro, 2-Apr-2015.)
⊢ (𝐴 ∈ dom arctan → (exp‘(2 · (i · (arctan‘𝐴)))) = (((2 · i) / (𝐴 + i)) − 1))
Theorem	tanatan 25974	The arctangent function is an inverse to tan. (Contributed by Mario Carneiro, 2-Apr-2015.)
⊢ (𝐴 ∈ dom arctan → (tan‘(arctan‘𝐴)) = 𝐴)
Theorem	atandmtan 25975	The tangent function has range contained in the domain of the arctangent. (Contributed by Mario Carneiro, 31-Mar-2015.)
⊢ ((𝐴 ∈ ℂ ∧ (cos‘𝐴) ≠ 0) → (tan‘𝐴) ∈ dom arctan)
Theorem	cosatan 25976	The cosine of an arctangent. (Contributed by Mario Carneiro, 3-Apr-2015.)
⊢ (𝐴 ∈ dom arctan → (cos‘(arctan‘𝐴)) = (1 / (√‘(1 + (𝐴↑2)))))
Theorem	cosatanne0 25977	The arctangent function has range contained in the domain of the tangent. (Contributed by Mario Carneiro, 3-Apr-2015.)
⊢ (𝐴 ∈ dom arctan → (cos‘(arctan‘𝐴)) ≠ 0)
Theorem	atantan 25978	The arctangent function is an inverse to tan. (Contributed by Mario Carneiro, 5-Apr-2015.)
⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (arctan‘(tan‘𝐴)) = 𝐴)
Theorem	atantanb 25979	Relationship between tangent and arctangent. (Contributed by Mario Carneiro, 5-Apr-2015.)
⊢ ((𝐴 ∈ dom arctan ∧ 𝐵 ∈ ℂ ∧ (ℜ‘𝐵) ∈ (-(π / 2)(,)(π / 2))) → ((arctan‘𝐴) = 𝐵 ↔ (tan‘𝐵) = 𝐴))
Theorem	atanbndlem 25980	Lemma for atanbnd 25981. (Contributed by Mario Carneiro, 5-Apr-2015.)
⊢ (𝐴 ∈ ℝ+ → (arctan‘𝐴) ∈ (-(π / 2)(,)(π / 2)))
Theorem	atanbnd 25981	The arctangent function is bounded by π / 2 on the reals. (Contributed by Mario Carneiro, 5-Apr-2015.)
⊢ (𝐴 ∈ ℝ → (arctan‘𝐴) ∈ (-(π / 2)(,)(π / 2)))
Theorem	atanord 25982	The arctangent function is strictly increasing. (Contributed by Mario Carneiro, 5-Apr-2015.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ (arctan‘𝐴) < (arctan‘𝐵)))
Theorem	atan1 25983	The arctangent of 1 is π / 4. (Contributed by Mario Carneiro, 2-Apr-2015.)
⊢ (arctan‘1) = (π / 4)
Theorem	bndatandm 25984	A point in the open unit disk is in the domain of the arctangent. (Contributed by Mario Carneiro, 5-Apr-2015.)
⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → 𝐴 ∈ dom arctan)
Theorem	atans 25985*	The "domain of continuity" of the arctangent. (Contributed by Mario Carneiro, 7-Apr-2015.)
⊢ 𝐷 = (ℂ ∖ (-∞(,]0))    &   ⊢ 𝑆 = {𝑦 ∈ ℂ ∣ (1 + (𝑦↑2)) ∈ 𝐷}    ⇒   ⊢ (𝐴 ∈ 𝑆 ↔ (𝐴 ∈ ℂ ∧ (1 + (𝐴↑2)) ∈ 𝐷))
Theorem	atans2 25986*	It suffices to show that 1 − i𝐴 and 1 + i𝐴 are in the continuity domain of log to show that 𝐴 is in the continuity domain of arctangent. (Contributed by Mario Carneiro, 7-Apr-2015.)
⊢ 𝐷 = (ℂ ∖ (-∞(,]0))    &   ⊢ 𝑆 = {𝑦 ∈ ℂ ∣ (1 + (𝑦↑2)) ∈ 𝐷}    ⇒   ⊢ (𝐴 ∈ 𝑆 ↔ (𝐴 ∈ ℂ ∧ (1 − (i · 𝐴)) ∈ 𝐷 ∧ (1 + (i · 𝐴)) ∈ 𝐷))
Theorem	atansopn 25987*	The domain of continuity of the arctangent is an open set. (Contributed by Mario Carneiro, 7-Apr-2015.)
⊢ 𝐷 = (ℂ ∖ (-∞(,]0))    &   ⊢ 𝑆 = {𝑦 ∈ ℂ ∣ (1 + (𝑦↑2)) ∈ 𝐷}    ⇒   ⊢ 𝑆 ∈ (TopOpen‘ℂfld)
Theorem	atansssdm 25988*	The domain of continuity of the arctangent is a subset of the actual domain of the arctangent. (Contributed by Mario Carneiro, 7-Apr-2015.)
⊢ 𝐷 = (ℂ ∖ (-∞(,]0))    &   ⊢ 𝑆 = {𝑦 ∈ ℂ ∣ (1 + (𝑦↑2)) ∈ 𝐷}    ⇒   ⊢ 𝑆 ⊆ dom arctan
Theorem	ressatans 25989*	The real number line is a subset of the domain of continuity of the arctangent. (Contributed by Mario Carneiro, 7-Apr-2015.)
⊢ 𝐷 = (ℂ ∖ (-∞(,]0))    &   ⊢ 𝑆 = {𝑦 ∈ ℂ ∣ (1 + (𝑦↑2)) ∈ 𝐷}    ⇒   ⊢ ℝ ⊆ 𝑆
Theorem	dvatan 25990*	The derivative of the arctangent. (Contributed by Mario Carneiro, 7-Apr-2015.)
⊢ 𝐷 = (ℂ ∖ (-∞(,]0))    &   ⊢ 𝑆 = {𝑦 ∈ ℂ ∣ (1 + (𝑦↑2)) ∈ 𝐷}    ⇒   ⊢ (ℂ D (arctan ↾ 𝑆)) = (𝑥 ∈ 𝑆 ↦ (1 / (1 + (𝑥↑2))))
Theorem	atancn 25991*	The arctangent is a continuous function. (Contributed by Mario Carneiro, 7-Apr-2015.)
⊢ 𝐷 = (ℂ ∖ (-∞(,]0))    &   ⊢ 𝑆 = {𝑦 ∈ ℂ ∣ (1 + (𝑦↑2)) ∈ 𝐷}    ⇒   ⊢ (arctan ↾ 𝑆) ∈ (𝑆–cn→ℂ)
Theorem	atantayl 25992*	The Taylor series for arctan(𝐴). (Contributed by Mario Carneiro, 1-Apr-2015.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (((i · ((-i↑𝑛) − (i↑𝑛))) / 2) · ((𝐴↑𝑛) / 𝑛)))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq1( + , 𝐹) ⇝ (arctan‘𝐴))
Theorem	atantayl2 25993*	The Taylor series for arctan(𝐴). (Contributed by Mario Carneiro, 1-Apr-2015.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, ((-1↑((𝑛 − 1) / 2)) · ((𝐴↑𝑛) / 𝑛))))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq1( + , 𝐹) ⇝ (arctan‘𝐴))
Theorem	atantayl3 25994*	The Taylor series for arctan(𝐴). (Contributed by Mario Carneiro, 7-Apr-2015.)
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((-1↑𝑛) · ((𝐴↑((2 · 𝑛) + 1)) / ((2 · 𝑛) + 1))))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq0( + , 𝐹) ⇝ (arctan‘𝐴))
Theorem	leibpilem1 25995	Lemma for leibpi 25997. (Contributed by Mario Carneiro, 7-Apr-2015.) (Proof shortened by Steven Nguyen, 23-Mar-2023.)
⊢ ((𝑁 ∈ ℕ0 ∧ (¬ 𝑁 = 0 ∧ ¬ 2 ∥ 𝑁)) → (𝑁 ∈ ℕ ∧ ((𝑁 − 1) / 2) ∈ ℕ0))
Theorem	leibpilem2 25996*	The Leibniz formula for π. (Contributed by Mario Carneiro, 7-Apr-2015.)
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((-1↑𝑛) / ((2 · 𝑛) + 1)))    &   ⊢ 𝐺 = (𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))    &   ⊢ 𝐴 ∈ V    ⇒   ⊢ (seq0( + , 𝐹) ⇝ 𝐴 ↔ seq0( + , 𝐺) ⇝ 𝐴)
Theorem	leibpi 25997	The Leibniz formula for π. This proof depends on three main facts: (1) the series 𝐹 is convergent, because it is an alternating series (iseralt 15324). (2) Using leibpilem2 25996 to rewrite the series as a power series, it is the 𝑥 = 1 special case of the Taylor series for arctan (atantayl2 25993). (3) Although we cannot directly plug 𝑥 = 1 into atantayl2 25993, Abel's theorem (abelth2 25506) says that the limit along any sequence converging to 1, such as 1 − 1 / 𝑛, of the power series converges to the power series extended to 1, and then since arctan is continuous at 1 (atancn 25991) we get the desired result. This is Metamath 100 proof #26. (Contributed by Mario Carneiro, 7-Apr-2015.)
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((-1↑𝑛) / ((2 · 𝑛) + 1)))    ⇒   ⊢ seq0( + , 𝐹) ⇝ (π / 4)
Theorem	leibpisum 25998	The Leibniz formula for π. This version of leibpi 25997 looks nicer but does not assert that the series is convergent so is not as practically useful. (Contributed by Mario Carneiro, 7-Apr-2015.)
⊢ Σ𝑛 ∈ ℕ0 ((-1↑𝑛) / ((2 · 𝑛) + 1)) = (π / 4)
Theorem	log2cnv 25999	Using the Taylor series for arctan(i / 3), produce a rapidly convergent series for log2. (Contributed by Mario Carneiro, 7-Apr-2015.)
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))))    ⇒   ⊢ seq0( + , 𝐹) ⇝ (log‘2)
Theorem	log2tlbnd 26000*	Bound the error term in the series of log2cnv 25999. (Contributed by Mario Carneiro, 7-Apr-2015.)
⊢ (𝑁 ∈ ℕ0 → ((log‘2) − Σ𝑛 ∈ (0...(𝑁 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ∈ (0[,](3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁)))))