TwonessLemma Show Code edit
thm (TwonessLemma () () (∃ a (∃ b (∃ c (∨ (¬ (= a b)) (¬ (= b c))))))
a b c LowerDimension
(∃ a (∃ b (∃ c (∧ (∧ (¬ (between a b c)) (¬ (between b c a))) (¬ (between c a b))))))
# The <code>a = b</code> case involves first picking out <code>¬ between b c a</code>.
(∧
(¬ (between a b c)) (¬ (between b c a)))
(¬ (between c a b))
ConjunctionRightElimination
(→ (∧ (∧ (¬ (between a b c)) (¬ (between b c a))) (¬ (between c a b))) (∧ (¬ (between a b c)) (¬ (between b c a))))
eliminateLeftConjunctInConsequent
(→ (∧ (∧ (¬ (between a b c)) (¬ (between b c a))) (¬ (between c a b))) (¬ (between b c a)))
(= a b) introduceAntecedent
(→ (= a b) (→ (∧ (∧ (¬ (between a b c)) (¬ (between b c a))) (¬ (between c a b))) (¬ (between b c a))))
# Now we prove a substitution, <code>a = b → (¬ between b c a ↔ ¬ between b c b)</code>
b EqualityReflexivity
(= b b)
c EqualityReflexivity
(= c c)
b b c c a b BetweenBuilder
(→ (∧ (∧ (= b b) (= c c)) (= a b)) (↔ (between b c a) (between b c b)))
detach2of3
(→ (∧ (= b b) (= a b)) (↔ (between b c a) (between b c b)))
detach1of2
(→ (= a b) (↔ (between b c a) (between b c b)))
(→ (= a b) (↔ (¬ (between b c a)) (¬ (between b c b))))
# We combine the substitution with our previous result to get <code>a = b → (¬ between a b c ∧ ¬ between b c a ∧ ¬ between c a b → ¬ between b c b)</code>.
eliminateBiconditionalReverseInConsequent
(→ (= a b) (→ (¬ (between b c a)) (¬ (between b c b))))
applySyllogismInConsequent
(→ (= a b) (→ (∧ (∧ (¬ (between a b c)) (¬ (between b c a))) (¬ (between c a b))) (¬ (between b c b))))
# Now we turn the consequent into <code>b ≠ c</code>,
(↔ (between b c b) (= b c))
(↔ (¬ (between b c b)) (¬ (= b c)))
eliminateBiconditionalReverse
(→ (¬ (between b c b)) (¬ (= b c)))
(= a b) introduceAntecedent
(→ (= a b) (→ (¬ (between b c b)) (¬ (= b c))))
applySyllogismInConsequent
(→ (= a b) (→ (∧ (∧ (¬ (between a b c)) (¬ (between b c a))) (¬ (between c a b))) (¬ (= b c))))
# and add the <code>a ≠ b</code> disjunct.
(¬ (= b c)) (¬ (= a b)) DisjunctionLeftIntroduction
(→ (¬ (= b c)) (∨ (¬ (= a b)) (¬ (= b c))))
(= a b) introduceAntecedent
(→ (= a b) (→ (¬ (= b c)) (∨ (¬ (= a b)) (¬ (= b c)))))
applySyllogismInConsequent
(→ (= a b) (→ (∧ (∧ (¬ (between a b c)) (¬ (between b c a))) (¬ (between c a b))) (∨ (¬ (= a b)) (¬ (= b c)))))
# The <code>a ≠ b</code> case is just a matter of arranging formulas for the case elimination and hooking to <code>LowerDimension</code>.
(¬ (= a b)) (¬ (= b c)) DisjunctionRightIntroduction
(→ (¬ (= a b)) (∨ (¬ (= a b)) (¬ (= b c))))
(∨ (¬ (= a b)) (¬ (= b c)))
(∧
(∧
(¬ (between a b c)) (¬ (between b c a))) (¬ (between c a b))
) AntecedentIntroduction
(→ (∨ (¬ (= a b)) (¬ (= b c))) (→ (∧ (∧ (¬ (between a b c)) (¬ (between b c a))) (¬ (between c a b))) (∨ (¬ (= a b)) (¬ (= b c)))))
applySyllogism
(→ (¬ (= a b)) (→ (∧ (∧ (¬ (between a b c)) (¬ (between b c a))) (¬ (between c a b))) (∨ (¬ (= a b)) (¬ (= b c)))))
# We combine the cases and finish the proof.
eliminateCases
(→ (∧ (∧ (¬ (between a b c)) (¬ (between b c a))) (¬ (between c a b))) (∨ (¬ (= a b)) (¬ (= b c))))