Step * of Lemma atomic_imp_prime

a:ℤprime(a) supposing atomic(a)
BY
((UnivCD THENM FLemma `atomic_char` [-1]) THENA Auto) }

1
1. : ℤ
2. atomic(a)
3. (a 1)) ∧ (∀b:ℤ((b a)  ((b 1) ∨ (b a))))
⊢ prime(a)


Latex:


Latex:
\mforall{}a:\mBbbZ{}.  prime(a)  supposing  atomic(a)


By


Latex:
((UnivCD  THENM  FLemma  `atomic\_char`  [-1])  THENA  Auto)




Home Index