Pythagorean theorem: a proof by dot products in the coordinate model

Goal and scope

In the Euclidean plane represented by ℝ² (with Euclidean length as distance), prove: for every right triangle ABC with the right angle at C, legs of lengths a=d(C,B) and b=d(C,A), and hypotenuse of length c=d(B,A), a²+b²=c². Then check the example C=(1,2), B=(4,6), A=(−7,8) (25+100=125), and use the non-right triangle E=(0,0), F=(4,0), H=(1,2) to show that without a right angle the relation fails in general.

Proves the theorem in the coordinate model of ℝ²: lengths come from the Euclidean length MKO, right angles from the right-triangle MKO, and angle measures from the cosine formula in G2. The proof is the dot-product version, corresponding to the vector-angle version mentioned by the MKO; it does not prove the area-rearrangement argument summarized in the MKO, nor the converse; it does not treat the equivalence of this model with synthetic geometry or with other vertex representations (MKO formal next); and it does not change the canonical MKO or its English edition.

Givens and symbols

• square_nonneg
• sqrt_def
• distributive
• cartesian_product_def
• numeric_evaluation

• G1 — Model: the Euclidean plane is represented by ℝ² (MKO assumption a1), with real coordinates and coordinatewise operations; distance d(P,Q)=√((x₂−x₁)²+(y₂−y₁)²); dot product u·v=u₁v₁+u₂v₂; for distinct points P≠Q, the line L(P,Q)={P+t(Q−P) ∣ t∈ℝ}.
• G2 — Interior angle measure: at a vertex X of a nondegenerate triangle, with u=Y−X and v=Z−X (both nonzero), the interior angle is the unique θ∈[0,π] with cos θ=(u·v)/(|u||v|), where |u|=√(u·u).
• G3 — ABC is an arbitrary nondegenerate triangle whose interior angle at C is γ=π/2 (MKO assumption a2); a=d(C,B) and b=d(C,A) are the leg lengths and c=d(B,A) is the hypotenuse length (assumption a3), all nonnegative reals (assumption a4). Nothing else is assumed about ABC.
• G4 — Example: C=(1,2), B=(4,6), A=(−7,8); comparison: E=(0,0), F=(4,0), H=(1,2).

• a,b,c — the leg lengths and the hypotenuse length
• u=B-C,\ v=A-C — the two side vectors from the right-angle vertex C
• u\cdot v — dot product u₁v₁+u₂v₂
• d(P,Q) — Euclidean distance
• \gamma — the interior angle measure at C

Rules and sources

• square_nonneg · prerequisite — Squares are nonnegative: for every real u, u²≥0, and u²=0 ⇔ u=0.
• sqrt_def · prerequisite — Principal square root: for a≥0, √a is the unique real b with b≥0 and b²=a. Negative numbers have no real square root.
• distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
• cartesian_product_def · prerequisite — Cartesian product: A×B is the set of ordered pairs (a,b) with a∈A and b∈B; (a,b)=(c,d) ⇔ a=c and b=d.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• def_intro · prerequisite — Introducing a definition: a statement, expression or object may be given a name, after which the name and what it stands for are interchangeable.
• add_assoc · prerequisite — Associativity of addition: (u+v)+w=u+(v+w).
• add_comm · prerequisite — Commutativity of addition: u+v=v+u.
• add_inverse · prerequisite — Additive inverse: every u has −u with u+(−u)=0; u−v means u+(−v).
• mul_inverse_nonzero · prerequisite — Inverse of a nonzero number: in ℚ, ℝ or ℂ, if u≠0 there is 1/u with u·(1/u)=1, and v/u means v·(1/u). 0 has no inverse, so v/0 is undefined.
• order_basics · prerequisite — Order of the reals: exactly one of u<v, u=v, u>v holds; u<v and v<w give u<w; u<v gives u+w<v+w; u<v and w>0 give uw<vw; u<v and w<0 give uw>vw.
• mul_zero · prerequisite — Multiplying by zero: u·0=0. Reason: u·0=u·(0+0)=u·0+u·0; subtracting u·0 from both sides gives 0=u·0.
• logic_chain · prerequisite — Chaining: from P⇒Q and Q⇒R infer P⇒R; likewise for ⇔.
• injective_surjective_def · prerequisite — Injective: f(a)=f(a′) ⇒ a=a′. Surjective: every b∈B has some a∈A with f(a)=b. Bijective: both; then there is a unique inverse f⁻¹ with f⁻¹∘f=id_A and f∘f⁻¹=id_B.
• eq_replace · prerequisite — Replacement of equals: an expression inside a statement may be replaced by an equal expression without changing whether the statement is true.
• mul_comm · prerequisite — Commutativity of multiplication: uv=vu (in commutative number systems such as ℤ, ℚ, ℝ, ℂ).
• neg_mul · prerequisite — Signs and multiplication: (−u)v=−(uv) and (−u)(−v)=uv.
• add_zero · prerequisite — Additive identity: u+0=u.
• eq_refl_symm_trans · prerequisite — Properties of equality: u=u; if u=v then v=u; if u=v and v=w then u=w.
• forall_intro · prerequisite — ∀-introduction (generalization): if a statement is proved for an arbitrary element x, with no extra assumption on x, it holds for every x in the domain.
• image_preimage_def · prerequisite — Image and preimage: f(S)={f(a) ∣ a∈S}; f⁻¹(T)={a∈A ∣ f(a)∈T}. The preimage notation does not presuppose that f has an inverse.
• contradiction · prerequisite — Proof by contradiction: if assuming ¬P leads to a contradiction (a statement and its negation both hold), then P holds.
• power_laws · prerequisite — Integer exponent laws (base nonzero, or exponents positive integers): a^m·a^n=a^{m+n}, (a^m)^n=a^{mn}, (ab)^n=a^n b^n, a^0=1.
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• mko_right_triangle_def · cited — A triangle is called a right triangle if one interior angle equals ninety degrees, equivalently π/2 radians. · mko-right-triangle
• mko_length_def · cited — Independent append-only source erratum (owner-adopted in this local revision; not merged or published): in the Euclidean plane, for P=(x₁,y₁) and Q=(x₂,y₂), their distance is the nonnegative principal square root of the sum of the squared coordinate differences; it is 0 when P=Q. The original Chinese positive-root wording remains in the parent and revision history. · mko-euclidean-length
• dot_def · prerequisite — Dot product and length: u·v=u₁v₁+u₂v₂ and |u|=√(u₁²+u₂²).
• coord_ops · prerequisite — Coordinatewise operations: (a,b)+(c,d)=(a+c,b+d), (a,b)−(c,d)=(a−c,b−d), t(a,b)=(ta,tb).
• angle_cos_def · prerequisite — Interior angle measure in the coordinate model: at a vertex X with nonzero u=Y−X and v=Z−X, the interior angle is the unique θ∈[0,π] with cos θ=(u·v)/(|u||v|).
• cos_facts · prerequisite — The cosine function is strictly decreasing on [0,π] (hence injective there), and cos(π/2)=0.
• line_unique · prerequisite — In ℝ², exactly one line passes through two distinct points X and Y, namely L(X,Y).
• L_right_iff_dot · lemma — For nonzero vectors u, v and θ∈[0,π] with cos θ=(u·v)/(|u||v|): θ=π/2 ⇔ u·v=0.
• L_sq_diff · lemma — For reals p, q: (p−q)²=p²−2pq+q².

Main derivation

\text{right triangle }ABC,\ \gamma=\tfrac{\pi}{2}

a=d(C,B),\ b=d(C,A),\ c=d(B,A);\ \text{goal}\ a^2+b^2=c^2

B-C,\ A-C

u=(u_1,u_2)=B-C,\ v=(v_1,v_2)=A-C,\ u\neq 0,\ v\neq 0

A-B

v-u

\gamma=\tfrac{\pi}{2}

u\cdot v=u_1v_1+u_2v_2=0

a=d(C,B),\ b=d(C,A),\ c=d(B,A)

a^2=u_1^2+u_2^2,\ b^2=v_1^2+v_2^2,\ c^2=(v_1-u_1)^2+(v_2-u_2)^2

(v_1-u_1)^2+(v_2-u_2)^2

(v_1^2-2u_1v_1+u_1^2)+(v_2^2-2u_2v_2+u_2^2)

(v_1^2-2u_1v_1+u_1^2)+(v_2^2-2u_2v_2+u_2^2)

c^2=a^2+b^2-2\,u\cdot v

c^2=a^2+b^2-2\,u\cdot v,\ u\cdot v=0

a^2+b^2=c^2

a^2+b^2=c^2\ \text{for the arbitrary right triangle of G3}

\text{every right triangle of the model}:\ a^2+b^2=c^2

C=(1,2),\ B=(4,6),\ A=(-7,8)

\triangle ABC\ \text{nondegenerate}

u=B-C=(3,4),\ v=A-C=(-8,6)

u\cdot v=-24+24=0,\ \gamma=\tfrac{\pi}{2}

a^2,\ b^2,\ c^2\ \text{for the example}

25+100=125

E=(0,0),\ F=(4,0),\ H=(1,2)

d(E,F)^2=16\neq 13+5=d(H,F)^2+d(H,E)^2

\text{S08, S09, S12, S13}

\forall\ \text{right triangles}:\ a^2+b^2=c^2

Substeps and lemmas

\cos\theta=\frac{u\cdot v}{|u|\,|v|},\ u\neq 0,\ v\neq 0

\cos\theta=0\iff u\cdot v=0

\theta\in[0,\pi]

\theta=\tfrac{\pi}{2}\iff\cos\theta=0\iff u\cdot v=0

(p-q)^2=(p-q)(p-q)

p^2-2pq+q^2

Reverse audits

• S14 · sufficient_goal_reduction · S04, S07, S08, S09 — Goal: a²+b²=c² for all right triangles of the model. Sufficient condition H: for an arbitrary right triangle, c²=a²+b²−2u·v (S07) and u·v=0 (S04); H gives the goal through S08 and S09. H is proved forwards from definitions and identities; the goal is never used as a premise.
• S13 · premise_audit · S07, dot_def, numeric_evaluation — This shows the right-angle hypothesis cannot be dropped; it is not a counterexample to the theorem, because EFH is not a right triangle.
• S12 · premise_audit · S05, S11, numeric_evaluation — Independently recomputable (N8 to N12); it supports S08 but cannot replace the general proof in S01 to S09.
• S11 · inverse_equivalence · L_right_iff_dot, dot_def, numeric_evaluation — The exact computation can be redone (N7); the lemma holds both ways.
• S10 · premise_audit · line_unique, contradiction — The example must also be checked to be nondegenerate first; otherwise G3 does not apply.
• S09 · premise_audit · S01, S08, forall_intro — ∀-introduction requires that no extra assumption was put on ABC; finitely many examples (such as S12) cannot replace this step.
• S08 · premise_audit · S04, S07, eq_replace, mul_zero — It needs u·v=0; without a right angle the extra term −2u·v is in general not 0 (see S13). No converse is claimed in this step.
• S07 · inverse_equivalence · add_comm, add_assoc, distributive, dot_def — It is an identity and holds both ways.
• S06.1 · inverse_equivalence · distributive, mul_comm, neg_mul — It is an identity and holds both ways.
• S06 · inverse_equivalence · L_sq_diff, mul_comm — It is an identity and holds both ways.
• S05 · inverse_equivalence · sqrt_def, mko_length_def — For nonnegative x and s, x=√s ⇔ x²=s; all three lengths are nonnegative (assumption a4), so squaring loses no information.
• S04.2 · inverse_equivalence · cos_facts, logic_chain, S04.1 — The ⇐ direction needs θ restricted to [0,π]; if θ=3π/2 were allowed, cos θ=0 would hold too.
• S04.1 · inverse_equivalence · mul_inverse_nonzero, square_nonneg, sqrt_def — Multiplying and dividing by |u||v| undo each other, given |u||v|≠0; if u=0 the denominator is 0 and the formula is undefined.
• S04 · inverse_equivalence · L_right_iff_dot, S02 — The lemma is a biconditional; u and v being nonzero (S02) cannot be dropped.
• S03 · inverse_equivalence · coord_ops, add_inverse — It is an identity and holds both ways.
• S02 · premise_audit · G3, def_intro, cartesian_product_def — Nonzero-ness comes from nondegeneracy; if B=C then u=0 and there is no angle at C.
• S01 · premise_audit · G3, def_intro, mko_right_triangle_def, mko_length_def — This step only names things; it puts no extra assumption on ABC, which is what lets S09 generalize to every right triangle.

Error controls and negative controls

It holds only for right triangles

The misconception the MKO names is applying a²+b²=c² to any triangle. S07 shows that a general triangle satisfies c²=a²+b²−2u·v; only a right angle (u·v=0) removes the last term. EFH has no right angle and 13+5=18≠16 (S13), so the theorem may not be applied to it.

The scope of the model

Another misconception identified in the MKO is taking the formalized model with specified vector side lengths as if every affine representation were automatically proved equivalent. Likewise this guide proves the theorem only in the coordinate model of ℝ², with side vectors from C; the equivalence of this model with other vertex representations or with a synthetic Euclidean plane needs a separate theorem (MKO formal next) and is not proved here.

The hypotenuse must be opposite the right angle; an example is not a proof

The c in the formula must be the side opposite the right angle. In the example, mistaking the leg b=10 for the hypotenuse gives 25+125=100, which is false (N23). Also, as the MKO warns, finite checks cannot replace a general proof: 25+100=125 in S12 checks one example, and the theorem's generality comes from S01 to S09.

• For triangle EFH, the squares of the two shorter sides add to the square of the longest: 13+5=16 → reject — 13+5=18≠16; EFH has no right angle (S13).
• 25+100=125 holds in the example, so the theorem is proved for all right triangles → reject — Finitely many examples are only checks; generality comes from the argument for an arbitrary triangle in S01 to S09.
• In the example, treat b=10 as the hypotenuse: 25+125=100 → reject — 150≠100 (N23); the hypotenuse is AB, the side opposite the right angle C.
• In a right triangle the leg lengths add to the hypotenuse length: 5+10=√125 → reject — (5+10)²=225≠125 (N24); the theorem is a relation between squares.

Result and limitations

In the coordinate model of ℝ², for any right triangle (right angle at C), writing u=B−C and v=A−C, always c²=a²+b²−2u·v, and the right angle is equivalent to u·v=0, so a²+b²=c². The example C=(1,2), B=(4,6), A=(−7,8) gives 25+100=125; the non-right triangle EFH gives 13+5=18≠16, and the difference is exactly 2u·v=2.

• Angle measure is defined by the cosine formula of G2; cos_facts and line_unique are premises and are not derived here.
• This guide proves neither the converse (a²+b²=c² implies a right angle) nor the area-rearrangement argument summarized in the MKO.
• The model here is ℝ² with Euclidean length; its equivalence with synthetic Euclidean geometry or other affine representations needs a separate theorem (MKO formal next).

Verification and source binding

24 declared checks for this guide; only the listed expressions are covered.

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: 8723c1e344103a9b4fb116bcfed73b10bf9b0fbc16c5935a181e826d20f1685b
• original source SHA-256: 54d2c3d929a38adb25ccbcded51b2cfc53d2a26489ddb50f38f6f0d5fd2b93e7
• Lean: NOT_RUN · independent AI: NOT_MEASURED

Same-source full JSON (formulas, ASTs, controls and revision log)