/* global React, Shape, Peek, Cite, ENT */ const { useState: useStatePf } = React; function ProofPage({ peekPattern = "drawer" }) { const [view, setView] = useStatePf("seq"); // 'seq' | 'tree' const [treeMode, setTreeMode] = useStatePf("outline"); // 'outline' | 'graph' const [peeked, setPeeked] = useStatePf(null); const open = (e) => setPeeked(e); const close = () => setPeeked(null); const steps = [ { n: "01", stmt: "Form the difference quotient at x.", math: "(f∘g)(x+h) − (f∘g)(x)\n―――――――――――――――――\n h", comm: "Direct from the definition.", just: { rule: "def.calc.derivative", note: "Limit of this expression as h → 0 is, by definition, (f∘g)′(x)." } }, { n: "02", stmt: "Multiply numerator and denominator by Δg = g(x+h) − g(x), assuming Δg ≠ 0 in a punctured neighborhood of x.", math: "f(g(x+h)) − f(g(x)) g(x+h) − g(x)\n――――――――――――――――― · ―――――――――――――\n g(x+h) − g(x) h", comm: "The Δg = 0 case is handled in step 06.", just: { rule: "algebraic identity", note: "Multiplying by 1 in the form Δg / Δg is valid because Δg ≠ 0." } }, { n: "03", current: true, stmt: "Recognize the first factor as the difference quotient of f at g(x), with increment Δg.", math: "lim_{h→0} [f(g(x)+Δg) − f(g(x))] / Δg", comm: "As h→0, Δg → 0 by continuity of g (which differentiability implies).", just: { rule: "thm.calc.diff_implies_cont", note: "Differentiability ⟹ continuity. So Δg→0 follows from h→0." } }, { n: "04", stmt: "Take the limit. The first factor → f′(g(x)); the second → g′(x).", math: "= f′(g(x)) · g′(x)", comm: "Apply the product-of-limits law since both limits exist.", just: { rule: "thm.calc.limit_product", note: "lim(AB) = (lim A)(lim B) when both factors converge." } }, { n: "05", stmt: "Edge case: Δg = 0 for h arbitrarily close to 0.", math: "(f∘g)′(x) = f′(g(x)) · 0 = 0", comm: "If Δg vanishes infinitely often, then g′(x) = 0, and the composition's difference quotient is 0 there too.", just: { rule: "Carathéodory characterization", note: "A standard workaround; see lem.calc.caratheodory." } }, ]; return (

← chain rule

proof pf.calc.chain_rule.0

proof of

(f ∘ g)′(x) = f′(g(x)) · g′(x), under of f at g(x) and of g at x.

strategy direct from definition length 7 steps · ~6 min read citations 3 def · 2 thm · 1 lem your progress step 03 / 7

{view === "seq" && (

{steps.map((s, i) => (

{s.n}

{s.stmt}

{s.math}

— {s.comm}

justified by {s.just.rule} {s.just.note}

))}

— 2 more steps · combine cases —

Q.E.D. 7 steps · 1 edge case · 6 cited entities

)} {view === "tree" && (

{treeMode === "outline" ? (

{[ ["1", "Set up the difference quotient", "step", "l1"], ["1.1", "Apply def.calc.derivative", "cite", "l2"], ["1.2", "Substitute composition (f∘g)(x) = f(g(x))", "step", "l2"], ["2", "Reduce to a product of difference quotients", "step", "l1"], ["2.1", "Multiply by Δg / Δg, assuming Δg ≠ 0", "step", "l2"], ["2.2", "Identify f's difference quotient with increment Δg", "step", "l2"], ["2.2.1", "Use thm.calc.diff_implies_cont so Δg → 0 as h → 0", "cite", "l3"], ["3", "Pass to the limit", "step", "l1"], ["3.1", "Apply thm.calc.limit_product", "cite", "l2"], ["3.2", "First factor → f′(g(x)); second → g′(x)", "step", "l2"], ["4", "Handle the edge case Δg = 0 frequently near x", "step", "l1"], ["4.1", "Apply lem.calc.caratheodory", "cite", "l2"], ["5", "Combine cases · QED", "step", "l1"], ].map(([n, t, kind, lvl]) => (

{n} {t} {kind}

))}

) : ( )}

)}

); } window.ProofPage = ProofPage;