SupplementaryAngles.mmt

namespace http://mathhub.info/FrameIT/frameworld ❚
fixmeta ?FrameworldMeta ❚

/T
      \
       \ D
        \
 ________\_________
A         B        C

The scroll encodes "angle ABD + angle DBC = 180°", or rather, "angle DBC = 180° - angle ABD"
❚
theory SupplementaryAngles =
    theory Problem =
        A: point ❘ meta ?MetaAnnotations?label "A" ❙
        B: point ❘ meta ?MetaAnnotations?label "B" ❙
        C: point ❘ meta ?MetaAnnotations?label "C" ❙
        D: point ❘ meta ?MetaAnnotations?label "D" ❙

        L: line ❘ meta ?MetaAnnotations?label "L"❙
        A_on_L : ⊦ A on L ❘ meta ?MetaAnnotations?label s"${lverb A} ∈ ${lverb L}"❙
        B_on_L : ⊦ B on L ❘ meta ?MetaAnnotations?label s"${lverb B} ∈ ${lverb L}"❙
        C_on_L : ⊦ C on L ❘ meta ?MetaAnnotations?label s"${lverb C} ∈ ${lverb L}"❙

        angleABD
            : Σ α: ℝ. ⊦ ( ∠ A,B,D ) ≐ α ❘
            meta ?MetaAnnotations?label s"∠${lverb A B D}"
        ❙
    ❚

    theory Solution =
        meta ?MetaAnnotations?label "AngleSum" ❙
        meta ?MetaAnnotations?problemTheory ?SupplementaryAngles/Problem ❙
        meta ?MetaAnnotations?solutionTheory ?SupplementaryAngles/Solution ❙
        meta ?MetaAnnotations?description "Supplementary angles add up to 180 degree " ❙

        include ?SupplementaryAngles/Problem ❙

        angleDBC
            : Σ γ: ℝ. ⊦ ( ∠ D,B,C ) ≐ γ ❘
            = ⟨180.0 - (πl angleABD), sketch "By some theorem"⟩ ❘
            meta ?MetaAnnotations?label s"∠${lverb D B C}" ❘
            meta ?MetaAnnotations?description s"The deduced angle by calculating 180° - ${lverb angleABD}"
        ❙
    ❚
❚