Nuprl Lemma : quadratic1_functionality

[a,b,c,a',b',c':ℝ].
  (quadratic1(a;b;c) quadratic1(a';b';c')) supposing 
     ((c c') and 
     (b b') and 
     (a a') and 
     (r0 ≤ ((b b) r(4) c)) and 
     a ≠ r0)


Proof




Definitions occuring in Statement :  quadratic1: quadratic1(a;b;c) rneq: x ≠ y rleq: x ≤ y rsub: y req: y rmul: b int-to-real: r(n) real: uimplies: supposing a uall: [x:A]. B[x] natural_number: $n
Definitions unfolded in proof :  uall: [x:A]. B[x] uimplies: supposing a quadratic1: quadratic1(a;b;c) member: t ∈ T prop: subtype_rel: A ⊆B all: x:A. B[x] so_lambda: λ2x.t[x] rneq: x ≠ y guard: {T} or: P ∨ Q iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q implies:  Q less_than: a < b squash: T less_than': less_than'(a;b) true: True so_apply: x[s] false: False not: ¬A rat_term_to_real: rat_term_to_real(f;t) rtermVar: rtermVar(var) rat_term_ind: rat_term_ind pi1: fst(t) rtermDivide: num "/" denom rtermMultiply: left "*" right rtermConstant: "const" pi2: snd(t) stable: Stable{P} uiff: uiff(P;Q) rev_uimplies: rev_uimplies(P;Q) int_nzero: -o nequal: a ≠ b ∈  sq_type: SQType(T) decidable: Dec(P) satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x]

Latex:
\mforall{}[a,b,c,a',b',c':\mBbbR{}].
    (quadratic1(a;b;c)  =  quadratic1(a';b';c'))  supposing 
          ((c  =  c')  and 
          (b  =  b')  and 
          (a  =  a')  and 
          (r0  \mleq{}  ((b  *  b)  -  r(4)  *  a  *  c))  and 
          a  \mneq{}  r0)



Date html generated: 2020_05_20-PM-00_33_21
Last ObjectModification: 2020_01_06-PM-00_14_02

Theory : reals


Home Index