Nuprl Lemma : rnonneg-radd
∀x,y:ℝ. (rnonneg(x) ⇒ rnonneg(y) ⇒ rnonneg(x + y))
Proof
Definitions occuring in Statement :
rnonneg: rnonneg(x),
radd: a + b,
real: ℝ,
all: ∀x:A. B[x],
implies: P ⇒ Q
Definitions unfolded in proof :
all: ∀x:A. B[x],
implies: P ⇒ Q,
radd: a + b,
member: t ∈ T,
uall: ∀[x:A]. B[x],
nat_plus: ℕ+,
decidable: Dec(P),
or: P ∨ Q,
uimplies: b supposing a,
not: ¬A,
satisfiable_int_formula: satisfiable_int_formula(fmla),
exists: ∃x:A. B[x],
prop: ℙ,
false: False,
subtype_rel: A ⊆r B,
length: ||as||,
list_ind: list_ind,
cons: [a / b],
nil: [],
it: ⋅,
real: ℝ,
iff: P ⇐⇒ Q,
and: P ∧ Q,
rev_implies: P ⇐ Q,
squash: ↓T,
true: True,
guard: {T},
rnonneg2: rnonneg2(x),
int_upper: {i...},
uiff: uiff(P;Q),
rev_uimplies: rev_uimplies(P;Q),
ge: i ≥ j ,
le: A ≤ B
Latex:
\mforall{}x,y:\mBbbR{}. (rnonneg(x) {}\mRightarrow{} rnonneg(y) {}\mRightarrow{} rnonneg(x + y))
Date html generated:
2020_05_20-AM-10_56_17
Last ObjectModification:
2020_03_20-PM-00_21_28
Theory : reals
Home
Index