Step * 1 1 of Lemma posint_atom_imp_prime


1. {a:ℕ+(a 1)) ∧ (∃b,c:ℕ+((¬(b 1)) ∧ (c 1)) ∧ (a (b c) ∈ ℕ+))))} 
2. ¬(a 1)
3. : ℕ+
4. : ℕ+
5. (b c)
6. ¬(∃b,c:ℕ+((¬(b 1)) ∧ (c 1)) ∧ (a (b c) ∈ ℕ+)))
⊢ (a b) ∨ (a c)
BY
TACTIC:(Assert ∀x:ℕ+(a ⇐⇒ x) BY
                (RepUR ``mdivides divides`` 0
                 THEN Auto
                 THEN ParallelLast
                 THEN Auto
                 THEN (InstLemma `pos_mul_arg_bounds` [⌜a⌝;⌜c1⌝]⋅ THENA Auto)
                 THEN ((D -1 THEN -2) THENA Auto)
                 THEN -1
                 THEN Auto)) }

1
1. {a:ℕ+(a 1)) ∧ (∃b,c:ℕ+((¬(b 1)) ∧ (c 1)) ∧ (a (b c) ∈ ℕ+))))} 
2. ¬(a 1)
3. : ℕ+
4. : ℕ+
5. (b c)
6. ¬(∃b,c:ℕ+((¬(b 1)) ∧ (c 1)) ∧ (a (b c) ∈ ℕ+)))
7. ∀x:ℕ+(a ⇐⇒ x)
⊢ (a b) ∨ (a c)


Latex:


Latex:

1.  a  :  \{a:\mBbbN{}\msupplus{}|  (\mneg{}(a  |  1))  \mwedge{}  (\mneg{}(\mexists{}b,c:\mBbbN{}\msupplus{}.  ((\mneg{}(b  |  1))  \mwedge{}  (\mneg{}(c  |  1))  \mwedge{}  (a  =  (b  *  c)))))\} 
2.  \mneg{}(a  |  1)
3.  b  :  \mBbbN{}\msupplus{}
4.  c  :  \mBbbN{}\msupplus{}
5.  a  |  (b  *  c)
6.  \mneg{}(\mexists{}b,c:\mBbbN{}\msupplus{}.  ((\mneg{}(b  |  1))  \mwedge{}  (\mneg{}(c  |  1))  \mwedge{}  (a  =  (b  *  c))))
\mvdash{}  (a  |  b)  \mvee{}  (a  |  c)


By


Latex:
TACTIC:(Assert  \mforall{}x:\mBbbN{}\msupplus{}.  (a  |  x  \mLeftarrow{}{}\mRightarrow{}  a  |  x)  BY
                            (RepUR  ``mdivides  divides``  0
                              THEN  Auto
                              THEN  ParallelLast
                              THEN  Auto
                              THEN  (InstLemma  `pos\_mul\_arg\_bounds`  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}c1\mkleeneclose{}]\mcdot{}  THENA  Auto)
                              THEN  ((D  -1  THEN  D  -2)  THENA  Auto)
                              THEN  D  -1
                              THEN  Auto))




Home Index