Angle: a step-by-step proof that vertical angles are equal

Goal and scope

Distinct lines AB and CD meet at O, with O between A and B and between C and D. Prove that vertical angles are equal: m∠AOC=m∠BOD and m∠COB=m∠DOA; then, for m∠AOC=35°, compute all four angles.

Works inside the MKO's scope: elementary plane Euclidean geometry, degree measure, unoriented angles from 0° to 180°. Proves the vertical-angle theorem from the linear pair postulate; it does not derive the angle postulates themselves, does not treat directed angles or radians, and does not change the canonical MKO or its English edition.

Givens and symbols

• eq_refl_symm_trans
• eq_congruence
• add_inverse
• numeric_evaluation

• G1 — Elementary plane Euclidean geometry; angles are measured in degrees, unoriented, with values from 0° to 180° (MKO assumption a1).
• G2 — Lines AB and CD are distinct and meet at O; O lies between A and B and between C and D. Since the lines meet only at O, C and D are not on line AB, and A and B are not on line CD.
• G3 — Example: m∠AOC=35°.

• m\angle AOC — the degree measure of angle AOC
• \alpha,\beta,\gamma,\delta — names for the four measures
• O — the intersection point, common vertex of the four angles
• A\text{-}O\text{-}B — O lies between A and B on one line
• \overleftrightarrow{AB} — the line through A and B

Rules and sources

• 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.
• 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.
• add_inverse · prerequisite — Additive inverse: every u has −u with u+(−u)=0; u−v means u+(−v).
• 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_comm · prerequisite — Commutativity of addition: u+v=v+u.
• add_assoc · prerequisite — Associativity of addition: (u+v)+w=u+(v+w).
• add_zero · prerequisite — Additive identity: u+0=u.
• 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.
• 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.
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• mko_angle_def · cited — Two rays with a common endpoint form an angle. The common endpoint is the vertex and the rays are the sides; this object treats unoriented angles from 0° through 180° measured in degrees. · mko-angle
• linear_pair · prerequisite — Linear pair postulate: if O lies between A and B and a point X is not on line AB, then m∠AOX+m∠XOB=180°.
• angle_symmetric · prerequisite — The measure of an unoriented angle does not depend on the order in which its sides are written: m∠XOY=m∠YOX.
• L_cancel · lemma — For reals u, v, w: u+w=v+w ⇔ u=v.

Main derivation

\angle AOC,\ \angle COB,\ \angle BOD,\ \angle DOA

\alpha=m\angle AOC,\ \beta=m\angle COB,\ \gamma=m\angle BOD,\ \delta=m\angle DOA

A\text{-}O\text{-}B,\ C\notin\overleftrightarrow{AB}

\alpha+\beta=180

C\text{-}O\text{-}D,\ B\notin\overleftrightarrow{CD}

\beta+\gamma=180

\alpha+\beta=180,\ \beta+\gamma=180

\alpha+\beta=\gamma+\beta

\alpha+\beta=\gamma+\beta

\alpha=\gamma

A\text{-}O\text{-}B,\ D\notin\overleftrightarrow{AB}

\delta+\gamma=180

\beta+\gamma=180,\ \delta+\gamma=180

\beta+\gamma=\delta+\gamma

\beta+\gamma=\delta+\gamma

\beta=\delta

\alpha=\gamma,\ \beta=\delta

m\angle AOC=m\angle BOD,\ m\angle COB=m\angle DOA

\alpha=35

\beta=145,\ \gamma=35,\ \delta=145

Substeps and lemmas

u+w=v+w

(u+w)+(-w)=(v+w)+(-w)

(u+w)+(-w)=(v+w)+(-w)

u=v

Reverse audits

• S10 · premise_audit · G3, S02, S05, S08 — This is the computation for one example and can be recomputed (N1, N2), but it cannot replace the general proof in S02 to S09.
• S09 · sufficient_goal_reduction · S05, S08, def_unfold — Goal G: both pairs of vertical angles are equal. Sufficient condition H: α=γ and β=δ; H⇒G by the naming in S01. H is proved forwards from G2 and the postulate in S05 and S08; G is never used as a premise.
• S08 · inverse_equivalence · L_cancel — Backward: add γ to both sides; both directions of the lemma are proved.
• S07 · premise_audit · S03, S06, eq_refl_symm_trans — As in S04, only the two equations are used and no converse is claimed.
• S06 · premise_audit · G2, linear_pair, angle_symmetric — It needs O between A and B and D off line AB, both from G2; renaming the angles only uses that an unoriented angle does not depend on the order of its sides.
• S05.2 · inverse_equivalence · add_assoc, add_inverse, add_zero — These are identities for all reals; replacing equal expressions does not change whether the equation holds, so the step is two-way.
• S05.1 · inverse_equivalence · eq_congruence, add_inverse — Adding −w and adding w undo each other and are possible for every real w.
• S05 · inverse_equivalence · L_cancel — Backward: add β to both sides to return to α+β=γ+β; both directions of the lemma are proved in the sub-steps.
• S04 · premise_audit · S02, S03, eq_refl_symm_trans — Only the two equations are needed; the converse, recovering that each sum is 180 from α+β=γ+β, is not claimed.
• S03 · premise_audit · G2, linear_pair — O between C and D, and B not on line CD (the lines are distinct and meet only at O), are both given by G2.
• S02 · premise_audit · G2, linear_pair — The postulate needs A, O, B collinear with O in the middle, and C off that line; both are stated in G2. Being adjacent alone would not give a sum of 180°.
• S01 · premise_audit · G1, G2, def_intro, mko_angle_def — This step only introduces names and derives no new fact. All four angles are defined: for example C is not on line AB, so OA and OC are not collinear and ∠AOC is a genuine angle.

Error controls and negative controls

Measuring a figure is not a proof

The MKO notes the common mistake of guessing measures from a sketch. Measuring ∠AOC and ∠BOD as apparently equal in one drawing supports only that drawing, with measurement error; the proof here uses only the incidence data of G2 and the linear pair postulate, so it covers every configuration satisfying G2.

Adjacent angles are not always supplementary

The linear pair postulate needs A, O, B collinear with O in the middle. If three rays from O point in the directions 0°, 50° and 120°, the two adjacent angles are 50° and 70°, summing to 120°, not 180°. That is why S02, S03 and S06 must cite 'O between the two points' from G2.

Supplementary angles need not be adjacent

The MKO explains that being supplementary depends only on the measures summing to 180° and does not require the angles to be adjacent. This proof uses the special adjacent case of a linear pair to obtain supplementary angles; conversely, supplementary angles need not form a linear pair.

• ∠AOC and ∠COB share the side OC, so m∠AOC+m∠COB=180° → reject — A, O, B must also be collinear with O in the middle; rays at 0°, 50° and 120° give 50°+70°=120°.
• Vertical angles are equal, so adjacent angles are equal too → reject — With α=35 we get β=145, so adjacent angles differ.
• Supplementary angles must be adjacent in the figure → reject — Angles of 30° and 150° may lie in different figures; their measures sum to 180°, so they are supplementary (MKO).
• In a drawing ∠AOC measures about the same as ∠BOD, so the vertical-angle theorem is proved → reject — One measurement supports only that drawing, with error, and does not cover all configurations.

Result and limitations

Under the setting of G2, m∠AOC=m∠BOD and m∠COB=m∠DOA: vertical angles are equal. If m∠AOC=35°, the four angles are 35°, 145°, 35° and 145° in order.

• The linear pair postulate and angle_symmetric are premises of this guide; they are not derived here from more basic axioms.

Verification and source binding

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

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

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