TheoremStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck 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.

Derivatives and fundamental periods of tangent, cotangent, secant, and cosecant

Statement

On their natural domains, $(\tan x)'=\sec^2x,\qquad(\cot x)'=-\csc^2x,\qquad(\sec x)'=\sec x\tan x,\qquad(\csc x)'=-\csc x\cot x.$ Tangent and cotangent have least positive period $\pi$ ; secant and cosecant have least positive period $2\pi$ .

Facts & Assumptions

Given: A real $x$ in the domain of the function under discussion.

[L1]

The quotient definitions and exact excluded points are those of Tangent, cotangent, secant, and cosecant on their exact natural domains.

[L2]

$\sin'=\cos$ , $\cos'=-\sin$ , and $\sin^2+\cos^2=1$ (The derivatives of sine and cosine are cosine and minus sine, Parity and the Pythagorean identity for sine and cosine).

[L3]

Quotient and reciprocal differentiation rules apply, and the zero sets and periods of sine/cosine are known (Sums, scalar multiples, products and quotients: $(f+g)'(c) = f'(c) + g'(c)$ , $(\alpha f)'(c) = \alpha f'(c)$ , $(fg)'(c) = f'(c)g(c) + f(c)g'(c)$ , and $(f/g)'(c) = \bigl(f'(c)g(c) - f(c)g'(c)\bigr)/g(c)^{2}$ when $g(c) \ne 0$ , The zero sets of sine and cosine and the least positive common period 2 pi).

Proof

technique · direct

1.1

Quotient and reciprocal differentiation applied to [L1] gives the four displayed derivatives after using $\sin^2+\cos^2=1$ .

L1L2L3

1.2

Shifting by $\pi$ negates both sine and cosine, so their quotients have period $\pi$ , while their reciprocals change sign and therefore have period $2\pi$ .

L1L3

2.1

The zero-set and quarter-turn values rule out a smaller positive period in each case.

step 1.2L2L3∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 73 results over 25 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

NIST Digital Library of Mathematical Functions, Chapter 4 (standard reference, not scraped)
C. Schmeiser, Introduction to Analysis (standard reference, not scraped)