PointConstructionDifferent Show Code edit
thm (PointConstructionDifferent ((A c) (B c)) () (∃ c (∧ (between A B c) (¬ (= B c))))
# The proof of our main theorem will proceed by constructing two different points <code>a</code> and <code>b</code>, and using them to extend the segment <code>A B</code> to a distinct point.
#
# We start with the extension of <code>A B</code> beyond <code>B</code> to a point <code>c</code>.
c A B a b SegmentConstruction
(∃ c (∧ (between A B c) (≡ B c a b)))
# That gives us <code>∃ c (between A B c ∧ B c ≡ a b)</code>. This a relationship which holds for any values of <code>a</code> and <code>b</code>
b generalize
(∀ b (∃ c (∧ (between A B c) (≡ B c a b))))
a generalize
(∀ a (∀ b (∃ c (∧ (between A B c) (≡ B c a b)))))
# Now we put in the construction of the two distinct points,
a b Twoness
(∃ a (∃ b (¬ (= a b))))
# and combine the two statements and gather the quantifiers at the beginning to get <code>∃ a ∃ b ∃ c ((between A B c ∧ B c ≡ a b) ∧ a ≠ b)</code>
introduceConjunction
(∧ (∀ a (∀ b (∃ c (∧ (between A B c) (≡ B c a b))))) (∃ a (∃ b (¬ (= a b)))))
a (∀ b (∃ c (∧ (between A B c) (≡ B c a b)))) (∃ b (¬ (= a b))) ThereExistsConjunctionCombining
(→ (∧ (∀ a (∀ b (∃ c (∧ (between A B c) (≡ B c a b))))) (∃ a (∃ b (¬ (= a b))))) (∃ a (∧ (∀ b (∃ c (∧ (between A B c) (≡ B c a b)))) (∃ b (¬ (= a b))))))
applyModusPonens
(∃ a (∧ (∀ b (∃ c (∧ (between A B c) (≡ B c a b)))) (∃ b (¬ (= a b)))))
b (∃ c (∧ (between A B c) (≡ B c a b))) (¬ (= a b)) ThereExistsConjunctionCombining
(→ (∧ (∀ b (∃ c (∧ (between A B c) (≡ B c a b)))) (∃ b (¬ (= a b)))) (∃ b (∧ (∃ c (∧ (between A B c) (≡ B c a b))) (¬ (= a b)))))
a addThereExists
(→ (∃ a (∧ (∀ b (∃ c (∧ (between A B c) (≡ B c a b)))) (∃ b (¬ (= a b))))) (∃ a (∃ b (∧ (∃ c (∧ (between A B c) (≡ B c a b))) (¬ (= a b))))))
applyModusPonens
(∃ a (∃ b (∧ (∃ c (∧ (between A B c) (≡ B c a b))) (¬ (= a b)))))
c (∧ (between A B c) (≡ B c a b)) (¬ (= a b)) ThereExistsConjunctionRightMovement
(↔ (∃ c (∧ (∧ (between A B c) (≡ B c a b)) (¬ (= a b)))) (∧ (∃ c (∧ (between A B c) (≡ B c a b))) (¬ (= a b))))
b buildThereExists
(↔ (∃ b (∃ c (∧ (∧ (between A B c) (≡ B c a b)) (¬ (= a b))))) (∃ b (∧ (∃ c (∧ (between A B c) (≡ B c a b))) (¬ (= a b)))))
a buildThereExists
(↔ (∃ a (∃ b (∃ c (∧ (∧ (between A B c) (≡ B c a b)) (¬ (= a b)))))) (∃ a (∃ b (∧ (∃ c (∧ (between A B c) (≡ B c a b))) (¬ (= a b))))))
eliminateBiconditionalForward
(→ (∃ a (∃ b (∧ (∃ c (∧ (between A B c) (≡ B c a b))) (¬ (= a b))))) (∃ a (∃ b (∃ c (∧ (∧ (between A B c) (≡ B c a b)) (¬ (= a b)))))))
applyModusPonens
(∃ a (∃ b (∃ c (∧ (∧ (between A B c) (≡ B c a b)) (¬ (= a b))))))
# Applying our lemma, we get <code>∃ a ∃ b ∃ c (between A B c ∧ B ≠ c)</code>
A B c a b PointConstructionDifferentLemma2
(→ (∧ (∧ (between A B c) (≡ B c a b)) (¬ (= a b))) (∧ (between A B c) (¬ (= B c))))
c addThereExists
(→ (∃ c (∧ (∧ (between A B c) (≡ B c a b)) (¬ (= a b)))) (∃ c (∧ (between A B c) (¬ (= B c)))))
b addThereExists
(→ (∃ b (∃ c (∧ (∧ (between A B c) (≡ B c a b)) (¬ (= a b))))) (∃ b (∃ c (∧ (between A B c) (¬ (= B c))))))
a addThereExists
(→ (∃ a (∃ b (∃ c (∧ (∧ (between A B c) (≡ B c a b)) (¬ (= a b)))))) (∃ a (∃ b (∃ c (∧ (between A B c) (¬ (= B c)))))))
applyModusPonens
(∃ a (∃ b (∃ c (∧ (between A B c) (¬ (= B c))))))
# The first two quantifiers are no longer needed, and that finishes the proof.
removeThereExists
(∃ b (∃ c (∧ (between A B c) (¬ (= B c)))))
removeThereExists
(∃ c (∧ (between A B c) (¬ (= B c))))
)
edit