### Nuprl Lemma : nat-mul-absval

[n:ℕ]. ∀[x:ℤ].  ((n |x|) |n x| ∈ ℤ)

Proof

Definitions occuring in Statement :  absval: |i| nat: uall: [x:A]. B[x] multiply: m int: equal: t ∈ T
Definitions unfolded in proof :  implies:  Q rev_implies:  Q and: P ∧ Q iff: ⇐⇒ Q guard: {T} uimplies: supposing a true: True subtype_rel: A ⊆B nat: squash: T member: t ∈ T uall: [x:A]. B[x]
Lemmas referenced :  istype-nat istype-int absval_pos iff_weakening_equal absval_mul absval_wf equal_wf
Rules used in proof :  isectIsTypeImplies axiomEquality isect_memberEquality_alt independent_functionElimination productElimination independent_isectElimination baseClosed imageMemberEquality natural_numberEquality sqequalRule equalitySymmetry equalityTransitivity inhabitedIsType hypothesisEquality rename setElimination multiplyEquality intEquality hypothesis because_Cache isectElimination extract_by_obid imageElimination sqequalHypSubstitution lambdaEquality_alt thin applyEquality cut introduction isect_memberFormation_alt sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[x:\mBbbZ{}].    ((n  *  |x|)  =  |n  *  x|)

Date html generated: 2019_10_15-AM-10_19_42
Last ObjectModification: 2019_10_10-PM-00_20_17

Theory : arithmetic

Home Index