### Nuprl Lemma : prime_divs_prod

`∀p:ℤ. (prime(p) `` (∀a1,a2:ℤ.  ((p | (a1 * a2)) `` ((p | a1) ∨ (p | a2)))))`

Proof

Definitions occuring in Statement :  prime: `prime(a)` divides: `b | a` all: `∀x:A. B[x]` implies: `P `` Q` or: `P ∨ Q` multiply: `n * m` int: `ℤ`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` member: `t ∈ T` uall: `∀[x:A]. B[x]` prop: `ℙ` guard: `{T}` prime: `prime(a)` and: `P ∧ Q`
Lemmas referenced :  divides_wf prime_wf istype-int
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :lambdaFormation_alt,  Error :universeIsType,  cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality multiplyEquality hypothesis Error :inhabitedIsType,  productElimination dependent_functionElimination independent_functionElimination

Latex:
\mforall{}p:\mBbbZ{}.  (prime(p)  {}\mRightarrow{}  (\mforall{}a1,a2:\mBbbZ{}.    ((p  |  (a1  *  a2))  {}\mRightarrow{}  ((p  |  a1)  \mvee{}  (p  |  a2)))))

Date html generated: 2019_06_20-PM-02_23_58
Last ObjectModification: 2018_10_03-AM-00_12_59

Theory : num_thy_1

Home Index