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))

)