Nuprl Lemma : coprime-exp

a,b:ℤ.  (CoPrime(a,b)  (∀n,m:ℕ.  CoPrime(a^m,b^n)))


Proof




Definitions occuring in Statement :  coprime: CoPrime(a,b) exp: i^n nat: all: x:A. B[x] implies:  Q int:
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q member: t ∈ T uall: [x:A]. B[x] prop:
Lemmas referenced :  coprime-exp1 exp_wf2 coprime_symmetry nat_wf coprime_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut lemma_by_obid sqequalHypSubstitution dependent_functionElimination thin isectElimination hypothesisEquality hypothesis independent_functionElimination because_Cache intEquality

Latex:
\mforall{}a,b:\mBbbZ{}.    (CoPrime(a,b)  {}\mRightarrow{}  (\mforall{}n,m:\mBbbN{}.    CoPrime(a\^{}m,b\^{}n)))



Date html generated: 2018_05_21-PM-01_09_55
Last ObjectModification: 2018_01_28-PM-02_03_39

Theory : num_thy_1


Home Index