P. 160 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 15901-16000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	plymullem1 15901*	Derive the coefficient function for the product of two polynomials. (Contributed by Mario Carneiro, 23-Jul-2014.)
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ (𝜑 → 𝐵:ℕ0⟶ℂ)    &   ⊢ (𝜑 → (𝐴 “ (ℤ≥‘(𝑀 + 1))) = {0})    &   ⊢ (𝜑 → (𝐵 “ (ℤ≥‘(𝑁 + 1))) = {0})    &   ⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘))))    &   ⊢ (𝜑 → 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘))))    ⇒   ⊢ (𝜑 → (𝐹 ∘𝑓 · 𝐺) = (𝑧 ∈ ℂ ↦ Σ𝑛 ∈ (0...(𝑀 + 𝑁))(Σ𝑘 ∈ (0...𝑛)((𝐴‘𝑘) · (𝐵‘(𝑛 − 𝑘))) · (𝑧↑𝑛))))
Theorem	plyaddlem 15902*	Lemma for plyadd 15904. (Contributed by Mario Carneiro, 21-Jul-2014.)
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐴 ∈ ((𝑆 ∪ {0}) ↑𝑚 ℕ0))    &   ⊢ (𝜑 → 𝐵 ∈ ((𝑆 ∪ {0}) ↑𝑚 ℕ0))    &   ⊢ (𝜑 → (𝐴 “ (ℤ≥‘(𝑀 + 1))) = {0})    &   ⊢ (𝜑 → (𝐵 “ (ℤ≥‘(𝑁 + 1))) = {0})    &   ⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘))))    &   ⊢ (𝜑 → 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘))))    ⇒   ⊢ (𝜑 → (𝐹 ∘𝑓 + 𝐺) ∈ (Poly‘𝑆))
Theorem	plymullem 15903*	Lemma for plymul 15905. (Contributed by Mario Carneiro, 21-Jul-2014.)
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐴 ∈ ((𝑆 ∪ {0}) ↑𝑚 ℕ0))    &   ⊢ (𝜑 → 𝐵 ∈ ((𝑆 ∪ {0}) ↑𝑚 ℕ0))    &   ⊢ (𝜑 → (𝐴 “ (ℤ≥‘(𝑀 + 1))) = {0})    &   ⊢ (𝜑 → (𝐵 “ (ℤ≥‘(𝑁 + 1))) = {0})    &   ⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘))))    &   ⊢ (𝜑 → 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘))))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 · 𝑦) ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝐹 ∘𝑓 · 𝐺) ∈ (Poly‘𝑆))
Theorem	plyadd 15904*	The sum of two polynomials is a polynomial. (Contributed by Mario Carneiro, 21-Jul-2014.)
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝐹 ∘𝑓 + 𝐺) ∈ (Poly‘𝑆))
Theorem	plymul 15905*	The product of two polynomials is a polynomial. (Contributed by Mario Carneiro, 21-Jul-2014.)
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 · 𝑦) ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝐹 ∘𝑓 · 𝐺) ∈ (Poly‘𝑆))
Theorem	plysub 15906*	The difference of two polynomials is a polynomial. (Contributed by Mario Carneiro, 21-Jul-2014.)
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 · 𝑦) ∈ 𝑆)    &   ⊢ (𝜑 → -1 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝐹 ∘𝑓 − 𝐺) ∈ (Poly‘𝑆))
Theorem	plyaddcl 15907	The sum of two polynomials is a polynomial. (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (𝐹 ∘𝑓 + 𝐺) ∈ (Poly‘ℂ))
Theorem	plymulcl 15908	The product of two polynomials is a polynomial. (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (𝐹 ∘𝑓 · 𝐺) ∈ (Poly‘ℂ))
Theorem	plysubcl 15909	The difference of two polynomials is a polynomial. (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (𝐹 ∘𝑓 − 𝐺) ∈ (Poly‘ℂ))
Theorem	plycoeid3 15910*	Reconstruct a polynomial as an explicit sum of the coefficient function up to an index no smaller than the degree of the polynomial. (Contributed by Jim Kingdon, 17-Oct-2025.)
⊢ (𝜑 → 𝐷 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ (𝜑 → (𝐴 “ (ℤ≥‘(𝐷 + 1))) = {0})    &   ⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝐷)((𝐴‘𝑘) · (𝑧↑𝑘))))    &   ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝐷))    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐹‘𝑋) = Σ𝑗 ∈ (0...𝑀)((𝐴‘𝑗) · (𝑋↑𝑗)))
Theorem	plycolemc 15911*	Lemma for plyco 15912. The result expressed as a sum, with a degree and coefficients for 𝐹 specified as hypotheses. (Contributed by Jim Kingdon, 20-Sep-2025.)
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 · 𝑦) ∈ 𝑆)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐴:ℕ0⟶(𝑆 ∪ {0}))    &   ⊢ (𝜑 → (𝐴 “ (ℤ≥‘(𝑁 + 1))) = {0})    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑥↑𝑘))))    ⇒   ⊢ (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · ((𝐺‘𝑧)↑𝑘))) ∈ (Poly‘𝑆))
Theorem	plyco 15912*	The composition of two polynomials is a polynomial. (Contributed by Mario Carneiro, 23-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 · 𝑦) ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝐹 ∘ 𝐺) ∈ (Poly‘𝑆))
Theorem	plycjlemc 15913*	Lemma for plycj 15914. (Contributed by Mario Carneiro, 24-Jul-2014.) (Revised by Jim Kingdon, 22-Sep-2025.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ 𝐺 = ((∗ ∘ 𝐹) ∘ ∗)    &   ⊢ (𝜑 → 𝐴:ℕ0⟶(𝑆 ∪ {0}))    &   ⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘))))    &   ⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))    ⇒   ⊢ (𝜑 → 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(((∗ ∘ 𝐴)‘𝑘) · (𝑧↑𝑘))))
Theorem	plycj 15914*	The double conjugation of a polynomial is a polynomial. (The single conjugation is not because our definition of polynomial includes only holomorphic functions, i.e. no dependence on (∗‘𝑧) independently of 𝑧.) (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ 𝐺 = ((∗ ∘ 𝐹) ∘ ∗)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (∗‘𝑥) ∈ 𝑆)    &   ⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))    ⇒   ⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆))
Theorem	plycn 15915	A polynomial is a continuous function. (Contributed by Mario Carneiro, 23-Jul-2014.) Avoid ax-mulf 8303. (Revised by GG, 16-Mar-2025.)
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹 ∈ (ℂ–cn→ℂ))
Theorem	plyrecj 15916	A polynomial with real coefficients distributes under conjugation. (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ ((𝐹 ∈ (Poly‘ℝ) ∧ 𝐴 ∈ ℂ) → (∗‘(𝐹‘𝐴)) = (𝐹‘(∗‘𝐴)))
Theorem	plyreres 15917	Real-coefficient polynomials restrict to real functions. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ (𝐹 ∈ (Poly‘ℝ) → (𝐹 ↾ ℝ):ℝ⟶ℝ)
Theorem	dvply1 15918*	Derivative of a polynomial, explicit sum version. (Contributed by Stefan O'Rear, 13-Nov-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘))))    &   ⊢ (𝜑 → 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...(𝑁 − 1))((𝐵‘𝑘) · (𝑧↑𝑘))))    &   ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ 𝐵 = (𝑘 ∈ ℕ0 ↦ ((𝑘 + 1) · (𝐴‘(𝑘 + 1))))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (ℂ D 𝐹) = 𝐺)
Theorem	dvply2g 15919	The derivative of a polynomial with coefficients in a subring is a polynomial with coefficients in the same ring. (Contributed by Mario Carneiro, 1-Jan-2017.) (Revised by GG, 30-Apr-2025.)
⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (ℂ D 𝐹) ∈ (Poly‘𝑆))
Theorem	dvply2 15920	The derivative of a polynomial is a polynomial. (Contributed by Stefan O'Rear, 14-Nov-2014.) (Proof shortened by Mario Carneiro, 1-Jan-2017.)
⊢ (𝐹 ∈ (Poly‘𝑆) → (ℂ D 𝐹) ∈ (Poly‘ℂ))
11.2  Basic trigonometry
11.2.1  The exponential, sine, and cosine functions (cont.)
Theorem	efcn 15921	The exponential function is continuous. (Contributed by Paul Chapman, 15-Sep-2007.) (Revised by Mario Carneiro, 20-Jun-2015.)
⊢ exp ∈ (ℂ–cn→ℂ)
Theorem	sincn 15922	Sine is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 3-Sep-2014.)
⊢ sin ∈ (ℂ–cn→ℂ)
Theorem	coscn 15923	Cosine is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 3-Sep-2014.)
⊢ cos ∈ (ℂ–cn→ℂ)
Theorem	reeff1olem 15924*	Lemma for reeff1o 15926. (Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 30-Apr-2014.)
⊢ ((𝑈 ∈ ℝ ∧ 1 < 𝑈) → ∃𝑥 ∈ ℝ (exp‘𝑥) = 𝑈)
Theorem	reeff1oleme 15925*	Lemma for reeff1o 15926. (Contributed by Jim Kingdon, 15-May-2024.)
⊢ (𝑈 ∈ (0(,)e) → ∃𝑥 ∈ ℝ (exp‘𝑥) = 𝑈)
Theorem	reeff1o 15926	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 15927	Lemma for eflt 15928. The converse of efltim 12483 plus the epsilon-delta setup. (Contributed by Jim Kingdon, 22-May-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (exp‘𝐴) < (exp‘𝐵))    &   ⊢ (𝜑 → 𝐷 ∈ ℝ+)    &   ⊢ (𝜑 → ((abs‘(𝐴 − 𝐵)) < 𝐷 → (abs‘((exp‘𝐴) − (exp‘𝐵))) < ((exp‘𝐵) − (exp‘𝐴))))    ⇒   ⊢ (𝜑 → 𝐴 < 𝐵)
Theorem	eflt 15928	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 15929	The exponential function on the reals is nondecreasing. (Contributed by Mario Carneiro, 11-Mar-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (exp‘𝐴) ≤ (exp‘𝐵)))
Theorem	reefiso 15930	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 15931	Apartness and the exponential function for reals. (Contributed by Jim Kingdon, 11-Jul-2024.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 # 𝐵 ↔ (exp‘𝐴) # (exp‘𝐵)))
Theorem	efap1p 15932	If the exponential of a number is apart from one plus that number, the number is apart from zero. To some extent can be thought of as the converse of efgt1p 12481. (Contributed by Jim Kingdon, 13-Aug-2026.)
⊢ ((𝐴 ∈ ℝ ∧ (1 + 𝐴) # (exp‘𝐴)) → 𝐴 # 0)
11.2.2  Properties of pi = 3.14159...
Theorem	pilem1 15933	Lemma for pire , pigt2lt4 and sinpi . (Contributed by Mario Carneiro, 9-May-2014.)
⊢ (𝐴 ∈ (ℝ+ ∩ (◡sin “ {0})) ↔ (𝐴 ∈ ℝ+ ∧ (sin‘𝐴) = 0))
Theorem	cosz12 15934	Cosine has a zero between 1 and 2. (Contributed by Mario Carneiro and Jim Kingdon, 7-Mar-2024.)
⊢ ∃𝑝 ∈ (1(,)2)(cos‘𝑝) = 0
Theorem	sin0pilem1 15935*	Lemma for pi related theorems. (Contributed by Mario Carneiro and Jim Kingdon, 8-Mar-2024.)
⊢ ∃𝑝 ∈ (1(,)2)((cos‘𝑝) = 0 ∧ ∀𝑥 ∈ (𝑝(,)(2 · 𝑝))0 < (sin‘𝑥))
Theorem	sin0pilem2 15936*	Lemma for pi related theorems. (Contributed by Mario Carneiro and Jim Kingdon, 8-Mar-2024.)
⊢ ∃𝑞 ∈ (2(,)4)((sin‘𝑞) = 0 ∧ ∀𝑥 ∈ (0(,)𝑞)0 < (sin‘𝑥))
Theorem	pilem3 15937	Lemma for pi related theorems. (Contributed by Jim Kingdon, 9-Mar-2024.)
⊢ (π ∈ (2(,)4) ∧ (sin‘π) = 0)
Theorem	pigt2lt4 15938	π is between 2 and 4. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 9-May-2014.)
⊢ (2 < π ∧ π < 4)
Theorem	sinpi 15939	The sine of π is 0. (Contributed by Paul Chapman, 23-Jan-2008.)
⊢ (sin‘π) = 0
Theorem	pire 15940	π is a real number. (Contributed by Paul Chapman, 23-Jan-2008.)
⊢ π ∈ ℝ
Theorem	picn 15941	π is a complex number. (Contributed by David A. Wheeler, 6-Dec-2018.)
⊢ π ∈ ℂ
Theorem	pipos 15942	π is positive. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 9-May-2014.)
⊢ 0 < π
Theorem	pirp 15943	π is a positive real. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ π ∈ ℝ+
Theorem	negpicn 15944	-π is a real number. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ -π ∈ ℂ
Theorem	sinhalfpilem 15945	Lemma for sinhalfpi 15950 and coshalfpi 15951. (Contributed by Paul Chapman, 23-Jan-2008.)
⊢ ((sin‘(π / 2)) = 1 ∧ (cos‘(π / 2)) = 0)
Theorem	halfpire 15946	π / 2 is real. (Contributed by David Moews, 28-Feb-2017.)
⊢ (π / 2) ∈ ℝ
Theorem	neghalfpire 15947	-π / 2 is real. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ -(π / 2) ∈ ℝ
Theorem	neghalfpirx 15948	-π / 2 is an extended real. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ -(π / 2) ∈ ℝ*
Theorem	pidiv2halves 15949	Adding π / 2 to itself gives π. See 2halves 9539. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ ((π / 2) + (π / 2)) = π
Theorem	sinhalfpi 15950	The sine of π / 2 is 1. (Contributed by Paul Chapman, 23-Jan-2008.)
⊢ (sin‘(π / 2)) = 1
Theorem	coshalfpi 15951	The cosine of π / 2 is 0. (Contributed by Paul Chapman, 23-Jan-2008.)
⊢ (cos‘(π / 2)) = 0
Theorem	cosneghalfpi 15952	The cosine of -π / 2 is zero. (Contributed by David Moews, 28-Feb-2017.)
⊢ (cos‘-(π / 2)) = 0
Theorem	efhalfpi 15953	The exponential of iπ / 2 is i. (Contributed by Mario Carneiro, 9-May-2014.)
⊢ (exp‘(i · (π / 2))) = i
Theorem	cospi 15954	The cosine of π is -1. (Contributed by Paul Chapman, 23-Jan-2008.)
⊢ (cos‘π) = -1
Theorem	efipi 15955	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 15956	Euler's identity. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 9-May-2014.)
⊢ ((exp‘(i · π)) + 1) = 0
Theorem	sin2pi 15957	The sine of 2π is 0. (Contributed by Paul Chapman, 23-Jan-2008.)
⊢ (sin‘(2 · π)) = 0
Theorem	cos2pi 15958	The cosine of 2π is 1. (Contributed by Paul Chapman, 23-Jan-2008.)
⊢ (cos‘(2 · π)) = 1
Theorem	ef2pi 15959	The exponential of 2πi is 1. (Contributed by Mario Carneiro, 9-May-2014.)
⊢ (exp‘(i · (2 · π))) = 1
Theorem	ef2kpi 15960	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 15961	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 15962	Lemma for sinper 15963 and cosper 15964. (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 15963	The sine function is periodic. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) → (sin‘(𝐴 + (𝐾 · (2 · π)))) = (sin‘𝐴))
Theorem	cosper 15964	The cosine function is periodic. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) → (cos‘(𝐴 + (𝐾 · (2 · π)))) = (cos‘𝐴))
Theorem	sin2kpi 15965	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 15966	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 15967	Sine of a number subtracted from 2 · π. (Contributed by Paul Chapman, 15-Mar-2008.)
⊢ (𝐴 ∈ ℂ → (sin‘((2 · π) − 𝐴)) = -(sin‘𝐴))
Theorem	cos2pim 15968	Cosine of a number subtracted from 2 · π. (Contributed by Paul Chapman, 15-Mar-2008.)
⊢ (𝐴 ∈ ℂ → (cos‘((2 · π) − 𝐴)) = (cos‘𝐴))
Theorem	sinmpi 15969	Sine of a number less π. (Contributed by Paul Chapman, 15-Mar-2008.)
⊢ (𝐴 ∈ ℂ → (sin‘(𝐴 − π)) = -(sin‘𝐴))
Theorem	cosmpi 15970	Cosine of a number less π. (Contributed by Paul Chapman, 15-Mar-2008.)
⊢ (𝐴 ∈ ℂ → (cos‘(𝐴 − π)) = -(cos‘𝐴))
Theorem	sinppi 15971	Sine of a number plus π. (Contributed by NM, 10-Aug-2008.)
⊢ (𝐴 ∈ ℂ → (sin‘(𝐴 + π)) = -(sin‘𝐴))
Theorem	cosppi 15972	Cosine of a number plus π. (Contributed by NM, 18-Aug-2008.)
⊢ (𝐴 ∈ ℂ → (cos‘(𝐴 + π)) = -(cos‘𝐴))
Theorem	efimpi 15973	The exponential function at i times a real number less π. (Contributed by Paul Chapman, 15-Mar-2008.)
⊢ (𝐴 ∈ ℂ → (exp‘(i · (𝐴 − π))) = -(exp‘(i · 𝐴)))
Theorem	sinhalfpip 15974	The sine of π / 2 plus a number. (Contributed by Paul Chapman, 24-Jan-2008.)
⊢ (𝐴 ∈ ℂ → (sin‘((π / 2) + 𝐴)) = (cos‘𝐴))
Theorem	sinhalfpim 15975	The sine of π / 2 minus a number. (Contributed by Paul Chapman, 24-Jan-2008.)
⊢ (𝐴 ∈ ℂ → (sin‘((π / 2) − 𝐴)) = (cos‘𝐴))
Theorem	coshalfpip 15976	The cosine of π / 2 plus a number. (Contributed by Paul Chapman, 24-Jan-2008.)
⊢ (𝐴 ∈ ℂ → (cos‘((π / 2) + 𝐴)) = -(sin‘𝐴))
Theorem	coshalfpim 15977	The cosine of π / 2 minus a number. (Contributed by Paul Chapman, 24-Jan-2008.)
⊢ (𝐴 ∈ ℂ → (cos‘((π / 2) − 𝐴)) = (sin‘𝐴))
Theorem	ptolemy 15978	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 12529, 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 15979	Lemma for sincosq1sgn 15980. (Contributed by Paul Chapman, 24-Jan-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 < (π / 2)) → 0 < (sin‘𝐴))
Theorem	sincosq1sgn 15980	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 15981	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 15982	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 15983	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 15984	The sine of a number strictly between 0 and π is positive. (Contributed by Paul Chapman, 15-Mar-2008.)
⊢ (𝐴 ∈ (0(,)π) → 0 < (sin‘𝐴))
Theorem	sinq34lt0t 15985	The sine of a number strictly between π and 2 · π is negative. (Contributed by NM, 17-Aug-2008.)
⊢ (𝐴 ∈ (π(,)(2 · π)) → (sin‘𝐴) < 0)
Theorem	cosq14gt0 15986	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 15987	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 15988	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 15989	Location of the zeroes of cosine in (0[,]π). (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝐴 ∈ (0[,]π) → ((cos‘𝐴) = 0 ↔ 𝐴 = (π / 2)))
Theorem	coseq0negpitopi 15990	Location of the zeroes of cosine in (-π(,]π). (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝐴 ∈ (-π(,]π) → ((cos‘𝐴) = 0 ↔ 𝐴 ∈ {(π / 2), -(π / 2)}))
Theorem	tanrpcl 15991	Positive real closure of the tangent function. (Contributed by Mario Carneiro, 29-Jul-2014.)
⊢ (𝐴 ∈ (0(,)(π / 2)) → (tan‘𝐴) ∈ ℝ+)
Theorem	tangtx 15992	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 15993	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 15994	The sine and cosine of π / 4. (Contributed by Paul Chapman, 25-Jan-2008.)
⊢ ((sin‘(π / 4)) = (1 / (√‘2)) ∧ (cos‘(π / 4)) = (1 / (√‘2)))
Theorem	tan4thpi 15995	The tangent of π / 4. (Contributed by Mario Carneiro, 5-Apr-2015.)
⊢ (tan‘(π / 4)) = 1
Theorem	sincos6thpi 15996	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 15997	The sine and cosine of π / 3. (Contributed by Mario Carneiro, 21-May-2016.)
⊢ ((sin‘(π / 3)) = ((√‘3) / 2) ∧ (cos‘(π / 3)) = (1 / 2))
Theorem	pigt3 15998	π is greater than 3. (Contributed by Brendan Leahy, 21-Aug-2020.)
⊢ 3 < π
Theorem	pige3 15999	π is greater than or equal to 3. (Contributed by Mario Carneiro, 21-May-2016.)
⊢ 3 ≤ π
Theorem	abssinper 16000	The absolute value of sine has period π. (Contributed by NM, 17-Aug-2008.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) → (abs‘(sin‘(𝐴 + (𝐾 · π)))) = (abs‘(sin‘𝐴)))