Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-02
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The derivatives of sine and cosine are cosine and minus sine

Statement

The functions sin⁡ and cos⁡ are differentiable on R, with (sin⁡x)′=cos⁡x,(cos⁡x)′=−sin⁡x. Also sin⁡0=0 and cos⁡0=1.

Facts & Assumptions

Given: The sine and cosine power series.

[L1]

Both defining series converge on all of R (The sine and cosine power series converge absolutely for every real argument, Sine and cosine defined by their real power series).

[L2]

A real power series may be differentiated term by term inside its radius of convergence (Inside its radius a real power series may be differentiated term by term, and the differentiated series has the same radius).

Proof

technique · direct
1.1L1L2

Termwise differentiation of the sine series gives ∑n≥0(−1)nx2n/(2n)!=cos⁡x.

1.2L1L2

Termwise differentiation of the cosine series gives −∑n≥0(−1)nx2n+1/(2n+1)!=−sin⁡x.

2.1L1algebra∎

Evaluating the defining series at 0 gives sin⁡0=0 and cos⁡0=1.

Depends on

Dependency tree · 2 levels

Sources