---

Step * 1 of Lemma qexp-qdiv


1. a : ℚ
2. b : ℚ
3. ¬(b = 0 ∈ ℚ)
4. n : ℤ
5. 0 < n
6. (a/b) ↑ n - 1 = (a ↑ n - 1/b ↑ n - 1) ∈ ℚ
7. ¬(b ↑ n = 0 ∈ ℚ)
8. ¬((b ↑ n - 1 * b) = 0 ∈ ℚ)
9. ¬(b ↑ n - 1 = 0 ∈ ℚ)
10. ¬(b = 0 ∈ ℚ)
⊢ ((a ↑ n - 1/b ↑ n - 1) * (a/b)) = (a ↑ n - 1 * a/b ↑ n - 1 * b) ∈ ℚ
BY
{ (MoveToConcl (-2) THEN GenConclAtAddr [1;1;2] THEN GenConclAtAddr [2;2;1;1] THEN Lemmaize [3]) }

1
∀a,b,v,v1:ℚ.  ((¬(b = 0 ∈ ℚ)) ⇒ (¬(v = 0 ∈ ℚ)) ⇒ (((v1/v) * (a/b)) = (v1 * a/v * b) ∈ ℚ))

---

Latex:

---

Latex:

1.  a  :  \mBbbQ{}
2.  b  :  \mBbbQ{}
3.  \mneg{}(b  =  0)
4.  n  :  \mBbbZ{}
5.  0  <  n
6.  (a/b)  \muparrow{}  n  -  1  =  (a  \muparrow{}  n  -  1/b  \muparrow{}  n  -  1)
7.  \mneg{}(b  \muparrow{}  n  =  0)
8.  \mneg{}((b  \muparrow{}  n  -  1  *  b)  =  0)
9.  \mneg{}(b  \muparrow{}  n  -  1  =  0)
10.  \mneg{}(b  =  0)
\mvdash{}  ((a  \muparrow{}  n  -  1/b  \muparrow{}  n  -  1)  *  (a/b))  =  (a  \muparrow{}  n  -  1  *  a/b  \muparrow{}  n  -  1  *  b)


By

---

Latex:
(MoveToConcl  (-2)  THEN  GenConclAtAddr  [1;1;2]  THEN  GenConclAtAddr  [2;2;1;1]  THEN  Lemmaize  [3])

---

Home Index