Alphabeta Math
CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The integral logarithm is continuous and strictly increasing on (0,∞)

Statement

The function L:(0,∞)→R is continuous and strictly increasing.

Facts & Assumptions

Given: L on (0,∞).

[L1]

L is differentiable and L′(x)=1/x for x>0 (The integral logarithm satisfies L′(x)=1/x for x>0 and L(1)=0).

[L2]

Differentiability at a point implies continuity there (A function differentiable at c is continuous at c).

[L3]

If a function is continuous on [a,b] and differentiable on (a,b), then f(b)−f(a)=f′(c)(b−a) for some c∈(a,b) (The mean value theorem, as the case g(x)=x of Cauchy's: for f continuous on [a,b] with a<b and differentiable on (a,b) there is c∈(a,b) with f(b)−f(a)=f′(c)(b−a)).

Proof

technique · direct
1.1

By [L1] and [L2], L is continuous at every point of (0,∞).

L1L2
1.2

Let 0<a<b. Applying [L3] gives a c∈(a,b) such that L(b)−L(a)=L′(c)(b−a)=b−ac>0.

L1L3algebra
2.1

Hence L(a)<L(b) whenever 0<a<b, so L is strictly increasing; step 1.1 supplies continuity.

step 1.1step 1.2∎

Depends on

Used by

Dependency tree · two levels

15 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources