---

Step * of Lemma finite-double-negation-shift

∀[A:ℙ]. ∀[B:ℕ ⟶ ℙ].  ∀n:ℕ. ((∀i:ℕn. (((B i) ⇒ A) ⇒ A)) ⇒ ((∀i:ℕn. (B i)) ⇒ A) ⇒ A)
BY
{ (RepeatFor 3 ((D 0 THENA Auto)) THEN GeneralNatInd (-1) THEN Auto THEN CaseNat 0 `n') }

1
1. [A] : ℙ
2. [B] : ℕ ⟶ ℙ
3. n : ℕ@i
4. ∀n1:ℕn. ((∀i:ℕn1. (((B i) ⇒ A) ⇒ A)) ⇒ ((∀i:ℕn1. (B i)) ⇒ A) ⇒ A)@i
5. ∀i:ℕn. (((B i) ⇒ A) ⇒ A)@i
6. (∀i:ℕn. (B i)) ⇒ A@i
7. n = 0 ∈ ℤ
⊢ A

2
1. [A] : ℙ
2. [B] : ℕ ⟶ ℙ
3. n : ℕ@i
4. ∀n1:ℕn. ((∀i:ℕn1. (((B i) ⇒ A) ⇒ A)) ⇒ ((∀i:ℕn1. (B i)) ⇒ A) ⇒ A)@i
5. ∀i:ℕn. (((B i) ⇒ A) ⇒ A)@i
6. (∀i:ℕn. (B i)) ⇒ A@i
7. ¬(n = 0 ∈ ℤ)
⊢ A

---

Latex:

---

Latex:
\mforall{}[A:\mBbbP{}].  \mforall{}[B:\mBbbN{}  {}\mrightarrow{}  \mBbbP{}].    \mforall{}n:\mBbbN{}.  ((\mforall{}i:\mBbbN{}n.  (((B  i)  {}\mRightarrow{}  A)  {}\mRightarrow{}  A))  {}\mRightarrow{}  ((\mforall{}i:\mBbbN{}n.  (B  i))  {}\mRightarrow{}  A)  {}\mRightarrow{}  A)


By

---

Latex:
(RepeatFor  3  ((D  0  THENA  Auto))  THEN  GeneralNatInd  (-1)  THEN  Auto  THEN  CaseNat  0  `n')

---

Home Index