Step
*
1
1
2
1
1
4
of Lemma
injection_le
.....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
BY
{ (InstHyp [a1;a2] 6 THEN Auto) }
Latex:
Latex:
.....falsecase.....
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. (f a1) = (f a2)
15. \mneg{}((f a1) = (m - 1))
16. \mneg{}((f a2) = (m - 1))
\mvdash{} a1 = a2
By
Latex:
(InstHyp [a1;a2] 6 THEN Auto)
Home
Index