Step
*
2
1
of Lemma
not-prime-mult
1. n : {2...}
2. m : {2...}
3. x : ℤ
4. prime((n * m) * x)
5. prime(n * m)
6. ¬((n * m) = 0 ∈ ℤ)
7. ¬((n * m) ~ 1)
⊢ reducible(n * m)
BY
{ ((D 0 With ⌜n⌝ THEN Auto)
THEN D 0 With ⌜m⌝
THEN Auto
THEN (D 0 THENA Auto)
THEN (RWO "assoced_elim" (-1) THENA Auto)
THEN D -1
THEN Auto) }
Latex:
Latex:
1. n : \{2...\}
2. m : \{2...\}
3. x : \mBbbZ{}
4. prime((n * m) * x)
5. prime(n * m)
6. \mneg{}((n * m) = 0)
7. \mneg{}((n * m) \msim{} 1)
\mvdash{} reducible(n * m)
By
Latex:
((D 0 With \mkleeneopen{}n\mkleeneclose{} THEN Auto)
THEN D 0 With \mkleeneopen{}m\mkleeneclose{}
THEN Auto
THEN (D 0 THENA Auto)
THEN (RWO "assoced\_elim" (-1) THENA Auto)
THEN D -1
THEN Auto)
Home
Index