BetweennessOuterTransitivityFlipped-ad Show Code edit
thm (BetweennessOuterTransitivityFlipped-ad () () (→ (∧ (∧ (∧ (∧ (between A C a) (≡ C a C D)) (between B C a)) (between B C D)) (¬ (= B C))) (= a D))
# We'll be applying <code>SegmentConstructionUniqueness</code>. It has five antecedents. The first is <code>B ≠ C</code>.
(∧ (∧ (∧ (between A C a) (≡ C a C D)) (between B C a)) (between B C D)) (¬ (= B C)) ConjunctionLeftElimination
(→ (∧ (∧ (∧ (∧ (between A C a) (≡ C a C D)) (between B C a)) (between B C D)) (¬ (= B C))) (¬ (= B C)))
# The second is <code>between B C a</code>
(∧ (∧ (∧ (between A C a) (≡ C a C D)) (between B C a)) (between B C D)) (¬ (= B C)) ConjunctionRightElimination
(→ (∧ (∧ (∧ (∧ (between A C a) (≡ C a C D)) (between B C a)) (between B C D)) (¬ (= B C))) (∧ (∧ (∧ (between A C a) (≡ C a C D)) (between B C a)) (between B C D)))
eliminateRightConjunctInConsequent
(→ (∧ (∧ (∧ (∧ (between A C a) (≡ C a C D)) (between B C a)) (between B C D)) (¬ (= B C))) (∧ (∧ (between A C a) (≡ C a C D)) (between B C a)))
eliminateLeftConjunctInConsequent
(→ (∧ (∧ (∧ (∧ (between A C a) (≡ C a C D)) (between B C a)) (between B C D)) (¬ (= B C))) (between B C a))
composeConjunction
(→ (∧ (∧ (∧ (∧ (between A C a) (≡ C a C D)) (between B C a)) (between B C D)) (¬ (= B C))) (∧ (¬ (= B C)) (between B C a)))
# The third is <code>C a ≡ C D</code>
(∧ (∧ (∧ (between A C a) (≡ C a C D)) (between B C a)) (between B C D)) (¬ (= B C)) ConjunctionRightElimination
(→ (∧ (∧ (∧ (∧ (between A C a) (≡ C a C D)) (between B C a)) (between B C D)) (¬ (= B C))) (∧ (∧ (∧ (between A C a) (≡ C a C D)) (between B C a)) (between B C D)))
eliminateRightConjunctInConsequent
(→ (∧ (∧ (∧ (∧ (between A C a) (≡ C a C D)) (between B C a)) (between B C D)) (¬ (= B C))) (∧ (∧ (between A C a) (≡ C a C D)) (between B C a)))
eliminateRightConjunctInConsequent
(→ (∧ (∧ (∧ (∧ (between A C a) (≡ C a C D)) (between B C a)) (between B C D)) (¬ (= B C))) (∧ (between A C a) (≡ C a C D)))
eliminateLeftConjunctInConsequent
(→ (∧ (∧ (∧ (∧ (between A C a) (≡ C a C D)) (between B C a)) (between B C D)) (¬ (= B C))) (≡ C a C D))
composeConjunction
(→ (∧ (∧ (∧ (∧ (between A C a) (≡ C a C D)) (between B C a)) (between B C D)) (¬ (= B C))) (∧ (∧ (¬ (= B C)) (between B C a)) (≡ C a C D)))
# The fourth is <code>between B C D</code>
(∧ (∧ (∧ (between A C a) (≡ C a C D)) (between B C a)) (between B C D)) (¬ (= B C)) ConjunctionRightElimination
(→ (∧ (∧ (∧ (∧ (between A C a) (≡ C a C D)) (between B C a)) (between B C D)) (¬ (= B C))) (∧ (∧ (∧ (between A C a) (≡ C a C D)) (between B C a)) (between B C D)))
eliminateLeftConjunctInConsequent
(→ (∧ (∧ (∧ (∧ (between A C a) (≡ C a C D)) (between B C a)) (between B C D)) (¬ (= B C))) (between B C D))
composeConjunction
(→ (∧ (∧ (∧ (∧ (between A C a) (≡ C a C D)) (between B C a)) (between B C D)) (¬ (= B C))) (∧ (∧ (∧ (¬ (= B C)) (between B C a)) (≡ C a C D)) (between B C D)))
# The fifth is <code>C D ≡ C D</code>
C D CongruenceReflexivity
(≡ C D C D)
(∧ (∧ (∧ (∧ (between A C a) (≡ C a C D)) (between B C a)) (between B C D)) (¬ (= B C))) introduceAntecedent
(→ (∧ (∧ (∧ (∧ (between A C a) (≡ C a C D)) (between B C a)) (between B C D)) (¬ (= B C))) (≡ C D C D))
composeConjunction
(→ (∧ (∧ (∧ (∧ (between A C a) (≡ C a C D)) (between B C a)) (between B C D)) (¬ (= B C))) (∧ (∧ (∧ (∧ (¬ (= B C)) (between B C a)) (≡ C a C D)) (between B C D)) (≡ C D C D)))
# Applying <code>SegmentConstructionUniqueness</code> we can conclude <code>a = D</code>.
B C a C D D SegmentConstructionUniqueness
(→ (∧ (∧ (∧ (∧ (¬ (= B C)) (between B C a)) (≡ C a C D)) (between B C D)) (≡ C D C D)) (= a D))
applySyllogism
(→ (∧ (∧ (∧ (∧ (between A C a) (≡ C a C D)) (between B C a)) (between B C D)) (¬ (= B C))) (= a D))
)
edit