### Nuprl Lemma : harmonic-series-diverges

`Σn.(r1/r(n + 1))↑`

Proof

Definitions occuring in Statement :  series-diverges: `Σn.x[n]↑` rdiv: `(x/y)` int-to-real: `r(n)` add: `n + m` natural_number: `\$n`
Definitions unfolded in proof :  so_apply: `x[s]` ge: `i ≥ j ` sq_exists: `∃x:A [B[x]]` rless: `x < y` le: `A ≤ B` lelt: `i ≤ j < k` int_seg: `{i..j-}` so_lambda: `λ2x.t[x]` nat: `ℕ` false: `False` satisfiable_int_formula: `satisfiable_int_formula(fmla)` not: `¬A` decidable: `Dec(P)` nat_plus: `ℕ+` cand: `A c∧ B` prop: `ℙ` true: `True` less_than': `less_than'(a;b)` squash: `↓T` less_than: `a < b` implies: `P `` Q` rev_implies: `P `` Q` and: `P ∧ Q` iff: `P `⇐⇒` Q` all: `∀x:A. B[x]` or: `P ∨ Q` guard: `{T}` rneq: `x ≠ y` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` member: `t ∈ T` exists: `∃x:A. B[x]` diverges: `n.x[n]↑` series-diverges: `Σn.x[n]↑` uiff: `uiff(P;Q)` sq_stable: `SqStable(P)` subtype_rel: `A ⊆r B` primtailrec: `primtailrec(n;i;b;f)` primrec: `primrec(n;b;c)` exp: `i^n` subtract: `n - m` int_upper: `{i...}` top: `Top` real: `ℝ` rev_uimplies: `rev_uimplies(P;Q)` rdiv: `(x/y)` req_int_terms: `t1 ≡ t2` rge: `x ≥ y` assert: `↑b` bnot: `¬bb` sq_type: `SQType(T)` bfalse: `ff` ifthenelse: `if b then t else f fi ` btrue: `tt` it: `⋅` unit: `Unit` bool: `𝔹` nequal: `a ≠ b ∈ T `

Latex:
\mSigma{}n.(r1/r(n  +  1))\muparrow{}

Date html generated: 2020_05_20-AM-11_21_18
Last ObjectModification: 2019_12_28-AM-11_02_27

Theory : reals

Home Index