`∀a,a',p:ℤ.  ((a' ≡ a mod p) `` (a' is a quadratic residue mod p `⇐⇒` a is a quadratic residue mod p))`

Proof

Definitions occuring in Statement :  quadratic-residue: `a is a quadratic residue mod p` eqmod: `a ≡ b mod m` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` implies: `P `` Q` int: `ℤ`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` member: `t ∈ T` prop: `ℙ` uall: `∀[x:A]. B[x]` quadratic-residue: `a is a quadratic residue mod p` iff: `P `⇐⇒` Q` and: `P ∧ Q` so_lambda: `λ2x.t[x]` so_apply: `x[s]` rev_implies: `P `` Q` exists: `∃x:A. B[x]` uimplies: `b supposing a`
Lemmas referenced :  eqmod_wf exists_wf iff_wf eqmod_functionality_wrt_eqmod eqmod_weakening
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis intEquality independent_pairFormation sqequalRule lambdaEquality multiplyEquality because_Cache addLevel productElimination impliesFunctionality existsFunctionality dependent_functionElimination independent_isectElimination independent_functionElimination existsLevelFunctionality

Latex:
\mforall{}a,a',p:\mBbbZ{}.    ((a'  \mequiv{}  a  mod  p)  {}\mRightarrow{}  (a'  is  a  quadratic  residue  mod  p  \mLeftarrow{}{}\mRightarrow{}  a  is  a  quadratic  residue  mod  p))

Date html generated: 2016_05_14-PM-04_27_27
Last ObjectModification: 2015_12_26-PM-08_05_24

Theory : num_thy_1

Home Index