---
tag: 03H7WZ4T3K
kind: statement
role: theorem
name: Pythagorean trigonometric identity
msc: [33B10]
uses: [0WB57D9488, 00R4MWW532, 0V2DV29EGT, 003QDZ4T16]
sources:
  - url: https://en.wikipedia.org/wiki/Pythagorean_trigonometric_identity
    locator: Proof using the differential equation
same_as:
  wikidata: Q2039117
  wikipedia: Pythagorean trigonometric identity
---

## Statement

For every real $x$,
$$\sin^2 x + \cos^2 x = 1.$$

## Remarks

Let $f(x) = \sin^2 x + \cos^2 x$. By the [[derivatives|00R4MWW532]] [[of sine and cosine|0V2DV29EGT]], $f'(x) = 2 \sin x \cos x - 2 \cos x \sin x = 0$. So $f$ is [[constant|003QDZ4T16]], and $f(0) = 1$.
So $|\sin x| \le 1$ and $|\cos x| \le 1$.
Geometrically, the point $(\cos x, \sin x)$ lies on the unit circle. Mathlib states it as `Real.sin_sq_add_cos_sq`.

## Explanations

### L1 human

In a right triangle with hypotenuse $1$, the legs are $\cos x$ and $\sin x$.
The Pythagorean theorem then says that their squares add up to $1$.
