Step
*
1
1
2
of Lemma
rmin-positive
1. x : ℝ
2. y : ℝ
3. n1 : ℕ+
4. ∀m:ℕ+. ((n1 ≤ m)
⇒ (m ≤ (n1 * (x m))))
5. n : ℕ+
6. ¬(n1 ≤ n)
7. ∀m:ℕ+. ((n ≤ m)
⇒ (m ≤ (n * (y m))))
8. m : ℕ+
9. ¬((x m) ≤ (y m))
10. imax(n1;n) ≤ m
11. (n1 ≤ m) ∧ (n ≤ m)
12. (n1 ≤ m) ∧ (n ≤ m)
13. m ≤ (n * (y m))
14. m ≤ (n1 * (x m))
⊢ m ≤ (n1 * (y m))
BY
{ (Assert ⌜n ≤ n1⌝⋅ THEN Auto THEN Mul ⌜y m⌝ (-1)⋅ THEN Auto) }
1
.....wf.....
1. x : ℝ
2. y : ℝ
3. n1 : ℕ+
4. ∀m:ℕ+. ((n1 ≤ m)
⇒ (m ≤ (n1 * (x m))))
5. n : ℕ+
6. ¬(n1 ≤ n)
7. ∀m:ℕ+. ((n ≤ m)
⇒ (m ≤ (n * (y m))))
8. m : ℕ+
9. ¬((x m) ≤ (y m))
10. imax(n1;n) ≤ m
11. n1 ≤ m
12. n ≤ m
13. n1 ≤ m
14. n ≤ m
15. m ≤ (n * (y m))
16. m ≤ (n1 * (x m))
17. n ≤ n1
⊢ y m ∈ ℕ
Latex:
Latex:
1. x : \mBbbR{}
2. y : \mBbbR{}
3. n1 : \mBbbN{}\msupplus{}
4. \mforall{}m:\mBbbN{}\msupplus{}. ((n1 \mleq{} m) {}\mRightarrow{} (m \mleq{} (n1 * (x m))))
5. n : \mBbbN{}\msupplus{}
6. \mneg{}(n1 \mleq{} n)
7. \mforall{}m:\mBbbN{}\msupplus{}. ((n \mleq{} m) {}\mRightarrow{} (m \mleq{} (n * (y m))))
8. m : \mBbbN{}\msupplus{}
9. \mneg{}((x m) \mleq{} (y m))
10. imax(n1;n) \mleq{} m
11. (n1 \mleq{} m) \mwedge{} (n \mleq{} m)
12. (n1 \mleq{} m) \mwedge{} (n \mleq{} m)
13. m \mleq{} (n * (y m))
14. m \mleq{} (n1 * (x m))
\mvdash{} m \mleq{} (n1 * (y m))
By
Latex:
(Assert \mkleeneopen{}n \mleq{} n1\mkleeneclose{}\mcdot{} THEN Auto THEN Mul \mkleeneopen{}y m\mkleeneclose{} (-1)\mcdot{} THEN Auto)
Home
Index