---

Step * of Lemma no-nontrivial-decidable-real-prop

∀[A:ℝ ⟶ ℙ]. ((∀x,y:ℝ.  ((x = y) ⇒ (A[x] ⇐⇒ A[y]))) ⇒ (∀r:ℝ. (A[r] ∨ (¬A[r]))) ⇒ ((∀x:ℝ. A[x]) ∨ (∀x:ℝ. (¬A[x]))))
BY
{ (Auto
   THEN (InstHyp [⌜r0⌝] (-1)⋅ THENA Auto)
   THEN ParallelLast
   THEN Auto
   THEN (InstHyp [⌜x⌝] (-3)⋅ THENA Auto)
   THEN D -1
   THEN Auto
   THEN (Assert ⌜False⌝⋅ THEN Auto)
   THEN (InstLemma `no-real-separation-corollary` [⌜A⌝;⌜λ2x.¬A[x]⌝]⋅ THENA Auto)
   THEN (SupposeMore (-1) THENA Auto)
   THEN ExRepD) }

1
1. A : ℝ ⟶ ℙ
2. ∀x,y:ℝ.  ((x = y) ⇒ (A[x] ⇐⇒ A[y]))
3. ∀r:ℝ. (A[r] ∨ (¬A[r]))
4. A[r0]
5. x : ℝ
6. ¬A[x]
7. x1 : ℝ
8. y : ℝ
9. x1 = y
10. A[x1]
11. ¬A[y]
⊢ False

2
1. A : ℝ ⟶ ℙ
2. ∀x,y:ℝ.  ((x = y) ⇒ (A[x] ⇐⇒ A[y]))
3. ∀r:ℝ. (A[r] ∨ (¬A[r]))
4. ¬A[r0]
5. x : ℝ
6. A[x]
7. x1 : ℝ
8. y : ℝ
9. x1 = y
10. A[x1]
11. ¬A[y]
⊢ False

---

Latex:

---

Latex:
\mforall{}[A:\mBbbR{}  {}\mrightarrow{}  \mBbbP{}]
    ((\mforall{}x,y:\mBbbR{}.    ((x  =  y)  {}\mRightarrow{}  (A[x]  \mLeftarrow{}{}\mRightarrow{}  A[y])))
    {}\mRightarrow{}  (\mforall{}r:\mBbbR{}.  (A[r]  \mvee{}  (\mneg{}A[r])))
    {}\mRightarrow{}  ((\mforall{}x:\mBbbR{}.  A[x])  \mvee{}  (\mforall{}x:\mBbbR{}.  (\mneg{}A[x]))))


By

---

Latex:
(Auto
  THEN  (InstHyp  [\mkleeneopen{}r0\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  ParallelLast
  THEN  Auto
  THEN  (InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  Auto
  THEN  (Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  (InstLemma  `no-real-separation-corollary`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.\mneg{}A[x]\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (SupposeMore  (-1)  THENA  Auto)
  THEN  ExRepD)

---

Home Index