Right triangle: deciding in coordinates which interior angle is right

Goal and scope

In the coordinate-plane model ℝ², let A=(1,1), B=(5,3), C=(0,3). Prove that A, B, C form a nondegenerate triangle whose interior angle at A equals 90° (that is, π/2), so ABC is a right triangle; show that the other two angles are not right and that any nondegenerate triangle has at most one right angle, and identify the hypotenuse and the legs. Then, with D=(1,4), show that triangle ABD is not a right triangle.

Works in the coordinate model of ℝ², with interior angle measures defined by the cosine formula of G2 and taking values in [0,π]; it uses the MKO's definition directly (one interior angle equals 90°=π/2) and first confirms a nondegenerate triangle (MKO assumption a1). The angle-sum theorem is cited from outside (citation_verified); facts about cosine and uniqueness of lines are prerequisites. It proves neither the Pythagorean theorem nor the general claim that the hypotenuse is longest, and does not change the canonical MKO or its English edition.

Givens and symbols

• cartesian_product_def
• image_preimage_def
• square_nonneg
• sqrt_def
• numeric_evaluation

• G1 — Model: points are ordered pairs of reals in ℝ², with coordinatewise operations; dot product u·v=u₁v₁+u₂v₂ and length |u|=√(u₁²+u₂²); for distinct points P≠Q, the line L(P,Q)={P+t(Q−P) ∣ t∈ℝ}.
• G2 — Interior angle measure: for a vertex X of a nondegenerate triangle with other vertices Y, Z, let u=Y−X and v=Z−X (both nonzero); the measure of the interior angle at X is the unique θ∈[0,π] (radians) with cos θ=(u·v)/(|u||v|).
• G3 — A=(1,1), B=(5,3), C=(0,3), D=(1,4).

• u\cdot v — dot product u₁v₁+u₂v₂
• |u| — length of a vector, √(u₁²+u₂²)
• \theta_A,\theta_B,\theta_C — the interior angle measures at A, B, C (radians)
• L(P,Q) — the line through distinct points P and Q
• 90^\circ,\ \tfrac{\pi}{2} — the same angle in degrees and in radians

Rules and sources

• 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.
• 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.
• 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.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true.
• frac_rules · prerequisite — Fraction rules (all denominators nonzero): a/c+b/c=(a+b)/c; (a/b)(c/d)=(ac)/(bd); (a/b)/(c/d)=(ad)/(bc) (also needing c≠0); a/b=(ak)/(bk) for k≠0.
• eq_congruence · prerequisite — Congruence of equality: if u=v, applying the same defined operation f to both sides gives f(u)=f(v). Operating on one side only is not an instance of this rule.
• 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.
• contradiction · prerequisite — Proof by contradiction: if assuming ¬P leads to a contradiction (a statement and its negation both hold), then P holds.
• 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.
• 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.
• exists_intro · prerequisite — ∃-introduction: if some a∈D satisfies P(a), then ∃x∈D, P(x).
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• 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.
• 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.
• de_morgan_logic · prerequisite — De Morgan's laws for logic: ¬(P∧Q) ⇔ ¬P∨¬Q and ¬(P∨Q) ⇔ ¬P∧¬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_triangle_def · cited — Given three distinct noncollinear points A, B, and C in the plane, the union of segments AB, BC, and CA determines the nondegenerate triangle ABC. · mko-triangle
• deg_rad · prerequisite — Degrees and radians: θ degrees equals θ·π/180 radians; 90° and π/2 denote the same angle (MKO assumption a2).
• 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).
• collinear_def · prerequisite — Collinear: points are collinear if some line contains all of them.
• thm_angle_sum · cited — In the Euclidean plane, the three interior angles of a nondegenerate triangle together equal two right angles, that is, π (180°). · Euclid, Elements, Book I, Proposition 32
• angle_positive · prerequisite — Each interior angle of a nondegenerate triangle has measure strictly between 0 and π.
• L_right_iff_dot · lemma — For nonzero vectors u, v and θ∈[0,π] with cos θ=(u·v)/(|u||v|): θ=π/2 ⇔ u·v=0.

Main derivation

\triangle ABC\ \text{is a right triangle}

\triangle ABC\ \text{nondegenerate and some interior angle}=90^\circ=\tfrac{\pi}{2}

90^\circ

\tfrac{\pi}{2}\ \text{rad}

A=(1,1),\ B=(5,3),\ C=(0,3)

A\neq B,\ B\neq C,\ C\neq A

C\in L(A,B)

\exists t\in\mathbb{R}:\ t=-\tfrac{1}{4}\ \land\ t=1

\exists t:\ t=-\tfrac{1}{4}\ \land\ t=1

C\notin L(A,B)

A\neq B,\ C\notin L(A,B)

\triangle ABC\ \text{nondegenerate}

u=B-A,\ v=C-A

u=(4,2),\ v=(-1,2),\ u\cdot v=0

u\cdot v=0,\ u\neq 0,\ v\neq 0

\theta_A=\tfrac{\pi}{2}

\triangle ABC\ \text{nondegenerate},\ \theta_A=\tfrac{\pi}{2}

\triangle ABC\ \text{is a right triangle with the right angle at}\ A

(A-B)\cdot(C-B)=(-4,-2)\cdot(-5,0)

20\neq 0,\ \theta_B\neq\tfrac{\pi}{2}

(A-C)\cdot(B-C)=(1,-2)\cdot(5,0)

5\neq 0,\ \theta_C\neq\tfrac{\pi}{2}

\theta_X=\theta_Y=\tfrac{\pi}{2}\ \text{at two vertices}\ X\neq Y

\text{contradiction; a nondegenerate triangle has at most one right angle}

\theta_A=\tfrac{\pi}{2}

\text{hypotenuse}\ BC,\ \text{legs}\ AB,\ AC

A,\ B,\ D=(1,4)

\triangle ABD\ \text{nondegenerate}

(B-A)\cdot(D-A),\ (A-B)\cdot(D-B),\ (A-D)\cdot(B-D)

6,\ 14,\ 3\neq 0;\ \triangle ABD\ \text{not right}

\text{S09, S12, S13, S15}

\triangle ABC\ \text{right at}\ A;\ \triangle ABD\ \text{not right}

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

Reverse audits

• S16 · sufficient_goal_reduction · S06, S08, S14, S15, mko_right_triangle_def — Goal: ABC is a right triangle and ABD is not. Sufficient condition H: ABC is nondegenerate with θ_A=π/2 (S06, S08), and ABD is nondegenerate with no angle equal to π/2 (S14, S15); H gives the goal by the MKO's definition. H is proved forwards in the earlier steps; the goal is never used as a premise.
• S15 · premise_audit · S14, L_right_iff_dot, dot_def, numeric_evaluation — To show a triangle is not right, all three angles must be excluded; excluding one is not enough.
• S14 · premise_audit · line_unique, contradiction, mko_triangle_def — The same three checks as S04 to S06: distinctness, not on L(A,B), and uniqueness of the line.
• S13 · premise_audit · S09, def_intro, dot_def — The naming depends only on where the right angle is (S09); the squared lengths are a check and play no part in the inference.
• S12 · premise_audit · thm_angle_sum, angle_positive, contradiction, forall_intro — It needs the angle-sum theorem (cited from outside, citation_verified) and positivity of each angle; computations for one example could not establish that every nondegenerate triangle has at most one right angle.
• S11 · inverse_equivalence · L_right_iff_dot, dot_def, numeric_evaluation — As in S10, both sides of the lemma's biconditional are negated (N7).
• S10 · inverse_equivalence · L_right_iff_dot, dot_def, numeric_evaluation — P⇔Q is equivalent to ¬P⇔¬Q; the computation can be redone (N6).
• S09 · premise_audit · S06, S08, mko_right_triangle_def, exists_intro — The definition asks only for one right angle to exist; both requirements (nondegenerate, one angle equal to π/2) are proved.
• S08.2 · inverse_equivalence · cos_facts, logic_chain, S08.1 — The ⇐ direction needs θ restricted to [0,π]; if θ=3π/2 were allowed, cos θ=0 would hold too, so the range in G2 cannot be dropped.
• S08.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 for cos θ is undefined.
• S08 · inverse_equivalence · L_right_iff_dot, S03, S06 — The lemma is a biconditional with both directions proved in the sub-steps; the condition that u and v are nonzero cannot be dropped.
• S07 · inverse_equivalence · dot_def, coord_ops, numeric_evaluation — Backward: A+u=(1+4,1+2)=(5,3)=B and A+v=(1−1,1+2)=(0,3)=C; the dot product can be recomputed independently (N5).
• S06 · premise_audit · S03, S05, line_unique, collinear_def, mko_triangle_def, contradiction — Uniqueness is the key: C∉L(A,B) alone does not rule out other lines unless the line through A and B is unique.
• S05 · premise_audit · S04, contradiction, eq_refl_symm_trans — Each coordinate equation alone has a solution; the contradiction comes from both needing the same t.
• S04 · inverse_equivalence · image_preimage_def, cartesian_product_def, eq_congruence, mul_inverse_nonzero — Substituting back: 1+4·(−1/4)=0 and 1+2·1=3; each move is reversible (the divisors are nonzero).
• S03 · premise_audit · G3, cartesian_product_def — One differing coordinate shows two points differ; all three pairs are checked.
• S02 · inverse_equivalence · deg_rad, numeric_evaluation — Backward: (π/2)·(180/π)=90, giving back 90°; both forms denote the same angle.
• S01 · premise_audit · mko_right_triangle_def, G2 — This step only states the definition and derives nothing yet; the order matters: without a nondegenerate triangle there are no interior angles to speak of.

Error controls and negative controls

First confirm a nondegenerate triangle

The misconception identified in the MKO is seeing two sides perpendicular without confirming that they form a nondegenerate triangle with the third side. For example, with E=(1,1)=A we get (B−A)·(E−A)=(4,2)·(0,0)=0 (N18), but the dot product is 0 only because E−A is the zero vector; A, B, E are not three distinct points and there is no angle at all. Likewise the segments [(0,0),(2,0)] and [(5,1),(5,3)] have perpendicular directions but share no endpoint, so they are not two sides of one triangle. That is why S03 to S06 must come before any angle is computed.

Do not mix degrees and radians

90° and π/2 radians are the same angle (S02), but the numbers 90 and π/2 are not equal. Putting θ=90 into G2, whose unit is the radian, means 90 radians, which is not a right angle: since π<4, π/2<2<90. Angles must be written with their unit.

A program's tolerance check is a check of concrete input

The MKO notes that a program can check whether three input angles sum to 180° within a tolerance and whether one is 90°, but that is only a check of concrete input. This guide decides exactly with integer dot products (0, 20, 5), so no tolerance is needed; and 'at most one right angle' is the general argument of S12, which no computation on finitely many examples can replace.

• With E=(1,1), (B−A)·(E−A)=0, so ABE is a right triangle with the right angle at A → reject — E=A, so the points are not distinct and E−A is the zero vector; there is no nondegenerate triangle and no angle (MKO assumption a1, G2).
• Side AD of triangle ABD is vertical, so ABD has a right angle → reject — The dot products at the three vertices are 6, 14 and 3, all nonzero (S15), so no interior angle equals π/2.
• Some nondegenerate triangles have two right angles → reject — Then the third angle would be π−π/2−π/2=0, contradicting that every interior angle is positive (S12).
• The right angle of ABC is at A, so the hypotenuse is AB → reject — The hypotenuse is the side opposite the right angle, namely BC; AB has A as an endpoint and is a leg. In this example |BC|²=25 is also larger than |AB|²=20.

Result and limitations

A=(1,1), B=(5,3), C=(0,3) form a nondegenerate triangle; u=B−A=(4,2) and v=C−A=(−1,2) have dot product 0, so θ_A=π/2=90° and ABC is a right triangle with the right angle at A, hypotenuse BC and legs AB, AC. The dot products at B and C are 20 and 5, so those angles are not right; any nondegenerate triangle has at most one right angle. Triangle ABD (D=(1,4)) has dot products 6, 14 and 3, so it has no right angle and is not a right triangle.

• Interior angle measure is defined by the cosine formula of G2; that it agrees with angle measure in synthetic geometry is not proved here.
• cos_facts, line_unique and angle_positive are premises and are not derived in this guide.
• N17 (20+5=25) is only a side check consistent with the Pythagorean theorem; the argument here does not use it.

Verification and source binding

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

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: 59d80db968e3384bccfcb59d56d000c022e245739089f60fee3f366ca873745c
• original source SHA-256: 59d80db968e3384bccfcb59d56d000c022e245739089f60fee3f366ca873745c
• Lean: NOT_RUN · independent AI: NOT_MEASURED

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