Step
*
1
1
2
1
1
of Lemma
injection_le
1. k : ℤ
2. 0 < k
3. ∀[m:ℕ]. (k - 1) ≤ m supposing ∃f:ℕk - 1 ⟶ ℕm. Inj(ℕk - 1;ℕm;f)
4. m : ℕ
5. f : ℕk ⟶ ℕm
6. ∀a1,a2:ℕk. (((f a1) = (f a2) ∈ ℕm) ⇒ (a1 = a2 ∈ ℕk))
7. f 0 ∈ ℕm
8. g : ℕk - 1 ⟶ ℕm - 1
9. ∀i:ℕk - 1. ((g i) = if (f i =z m - 1) then f (k - 1) else f i fi ∈ ℤ)
10. a1 : ℕk - 1
11. (g a1) = if (f a1 =z m - 1) then f (k - 1) else f a1 fi ∈ ℤ
12. a2 : ℕk - 1
13. (g a2) = if (f a2 =z m - 1) then f (k - 1) else f a2 fi ∈ ℤ
14. (g a1) = (g a2) ∈ ℕm - 1
⊢ a1 = a2 ∈ ℕk - 1
BY
{ (HypSubst' -4 -1 THEN HypSubst' -2 -1 THEN (SplitOnHypITE -1 THENA Auto) THEN (SplitOnHypITE -2 THENA Auto)) }
1
.....truecase.....
1. k : ℤ
2. 0 < k
3. ∀[m:ℕ]. (k - 1) ≤ m supposing ∃f:ℕk - 1 ⟶ ℕm. Inj(ℕk - 1;ℕm;f)
4. m : ℕ
5. f : ℕk ⟶ ℕm
6. ∀a1,a2:ℕk. (((f a1) = (f a2) ∈ ℕm) ⇒ (a1 = a2 ∈ ℕk))
7. f 0 ∈ ℕm
8. g : ℕk - 1 ⟶ ℕm - 1
9. ∀i:ℕk - 1. ((g i) = if (f i =z m - 1) then f (k - 1) else f i fi ∈ ℤ)
10. a1 : ℕk - 1
11. (g a1) = if (f a1 =z m - 1) then f (k - 1) else f a1 fi ∈ ℤ
12. a2 : ℕk - 1
13. (g a2) = if (f a2 =z m - 1) then f (k - 1) else f a2 fi ∈ ℤ
14. (f (k - 1)) = (f (k - 1)) ∈ ℕm - 1
15. (f a1) = (m - 1) ∈ ℤ
16. (f a2) = (m - 1) ∈ ℤ
⊢ a1 = a2 ∈ ℕk - 1
2
.....falsecase.....
1. k : ℤ
2. 0 < k
3. ∀[m:ℕ]. (k - 1) ≤ m supposing ∃f:ℕk - 1 ⟶ ℕm. Inj(ℕk - 1;ℕm;f)
4. m : ℕ
5. f : ℕk ⟶ ℕm
6. ∀a1,a2:ℕk. (((f a1) = (f a2) ∈ ℕm) ⇒ (a1 = a2 ∈ ℕk))
7. f 0 ∈ ℕm
8. g : ℕk - 1 ⟶ ℕm - 1
9. ∀i:ℕk - 1. ((g i) = if (f i =z m - 1) then f (k - 1) else f i fi ∈ ℤ)
10. a1 : ℕk - 1
11. (g a1) = if (f a1 =z m - 1) then f (k - 1) else f a1 fi ∈ ℤ
12. a2 : ℕk - 1
13. (g a2) = if (f a2 =z m - 1) then f (k - 1) else f a2 fi ∈ ℤ
14. (f (k - 1)) = (f a2) ∈ ℕm - 1
15. (f a1) = (m - 1) ∈ ℤ
16. ¬((f a2) = (m - 1) ∈ ℤ)
⊢ a1 = a2 ∈ ℕk - 1
3
.....truecase.....
1. k : ℤ
2. 0 < k
3. ∀[m:ℕ]. (k - 1) ≤ m supposing ∃f:ℕk - 1 ⟶ ℕm. Inj(ℕk - 1;ℕm;f)
4. m : ℕ
5. f : ℕk ⟶ ℕm
6. ∀a1,a2:ℕk. (((f a1) = (f a2) ∈ ℕm) ⇒ (a1 = a2 ∈ ℕk))
7. f 0 ∈ ℕm
8. g : ℕk - 1 ⟶ ℕm - 1
9. ∀i:ℕk - 1. ((g i) = if (f i =z m - 1) then f (k - 1) else f i fi ∈ ℤ)
10. a1 : ℕk - 1
11. (g a1) = if (f a1 =z m - 1) then f (k - 1) else f a1 fi ∈ ℤ
12. a2 : ℕk - 1
13. (g a2) = if (f a2 =z m - 1) then f (k - 1) else f a2 fi ∈ ℤ
14. (f a1) = (f (k - 1)) ∈ ℕm - 1
15. ¬((f a1) = (m - 1) ∈ ℤ)
16. (f a2) = (m - 1) ∈ ℤ
⊢ a1 = a2 ∈ ℕk - 1
4
.....falsecase.....
1. k : ℤ
2. 0 < k
3. ∀[m:ℕ]. (k - 1) ≤ m supposing ∃f:ℕk - 1 ⟶ ℕm. Inj(ℕk - 1;ℕm;f)
4. m : ℕ
5. f : ℕk ⟶ ℕm
6. ∀a1,a2:ℕk. (((f a1) = (f a2) ∈ ℕm) ⇒ (a1 = a2 ∈ ℕk))
7. f 0 ∈ ℕm
8. g : ℕk - 1 ⟶ ℕm - 1
9. ∀i:ℕk - 1. ((g i) = if (f i =z m - 1) then f (k - 1) else f i fi ∈ ℤ)
10. a1 : ℕk - 1
11. (g a1) = if (f a1 =z m - 1) then f (k - 1) else f a1 fi ∈ ℤ
12. a2 : ℕk - 1
13. (g a2) = if (f a2 =z m - 1) then f (k - 1) else f a2 fi ∈ ℤ
14. (f a1) = (f a2) ∈ ℕm - 1
15. ¬((f a1) = (m - 1) ∈ ℤ)
16. ¬((f a2) = (m - 1) ∈ ℤ)
⊢ a1 = a2 ∈ ℕk - 1
Latex:
Latex:
1. k : \mBbbZ{}
2. 0 < k
3. \mforall{}[m:\mBbbN{}]. (k - 1) \mleq{} m supposing \mexists{}f:\mBbbN{}k - 1 {}\mrightarrow{} \mBbbN{}m. Inj(\mBbbN{}k - 1;\mBbbN{}m;f)
4. m : \mBbbN{}
5. f : \mBbbN{}k {}\mrightarrow{} \mBbbN{}m
6. \mforall{}a1,a2:\mBbbN{}k. (((f a1) = (f a2)) {}\mRightarrow{} (a1 = a2))
7. f 0 \mmember{} \mBbbN{}m
8. g : \mBbbN{}k - 1 {}\mrightarrow{} \mBbbN{}m - 1
9. \mforall{}i:\mBbbN{}k - 1. ((g i) = if (f i =\msubz{} m - 1) then f (k - 1) else f i fi )
10. a1 : \mBbbN{}k - 1
11. (g a1) = if (f a1 =\msubz{} m - 1) then f (k - 1) else f a1 fi
12. a2 : \mBbbN{}k - 1
13. (g a2) = if (f a2 =\msubz{} m - 1) then f (k - 1) else f a2 fi
14. (g a1) = (g a2)
\mvdash{} a1 = a2
By
Latex:
(HypSubst' -4 -1
THEN HypSubst' -2 -1
THEN (SplitOnHypITE -1 THENA Auto)
THEN (SplitOnHypITE -2 THENA Auto))
Home
Index