HomeTheorem List (p. 447 of 502)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 447 of 502) | < Previous Next > |
| Bad symbols? Try the
GIF version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | Metamath Proof Explorer
(1-31005) |
Hilbert Space Explorer
(31006-32528) |
Users' Mathboxes
(32529-50153) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | nfcoll 44601 | Bound-variable hypothesis builder for the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
| ⊢ Ⅎ𝑥𝐹 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥(𝐹 Coll 𝐴) | ||
| Theorem | collexd 44602 | The output of the collection operation is a set if the second input is. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐹 Coll 𝐴) ∈ V) | ||
| Theorem | cpcolld 44603* | Property of the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
| ⊢ (𝜑 → 𝑥 ∈ 𝐴) & ⊢ (𝜑 → 𝑥𝐹𝑦) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ (𝐹 Coll 𝐴)𝑥𝐹𝑦) | ||
| Theorem | cpcoll2d 44604* | cpcolld 44603 with an extra existential quantifier. (Contributed by Rohan Ridenour, 12-Aug-2023.) |
| ⊢ (𝜑 → 𝑥 ∈ 𝐴) & ⊢ (𝜑 → ∃𝑦 𝑥𝐹𝑦) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ (𝐹 Coll 𝐴)𝑥𝐹𝑦) | ||
| Theorem | grucollcld 44605 | A Grothendieck universe contains the output of a collection operation whenever its left input is a relation on the universe, and its right input is in the universe. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
| ⊢ (𝜑 → 𝐺 ∈ Univ) & ⊢ (𝜑 → 𝐹 ⊆ (𝐺 × 𝐺)) & ⊢ (𝜑 → 𝐴 ∈ 𝐺) ⇒ ⊢ (𝜑 → (𝐹 Coll 𝐴) ∈ 𝐺) | ||
| Theorem | ismnu 44606* |
The hypothesis of this theorem defines a class M of sets that we
temporarily call "minimal universes", and which will turn out
in
grumnueq 44632 to be exactly Grothendicek universes.
Minimal universes are
sets which satisfy the predicate on 𝑦 in rr-groth 44644, except for the
𝑥
∈ 𝑦 clause.
A minimal universe is closed under subsets (mnussd 44608), powersets (mnupwd 44612), and an operation which is similar to a combination of collection and union (mnuop3d 44616), from which closure under pairing (mnuprd 44621), unions (mnuunid 44622), and function ranges (mnurnd 44628) can be deduced, from which equivalence with Grothendieck universes (grumnueq 44632) can be deduced. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
| ⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} ⇒ ⊢ (𝑈 ∈ 𝑉 → (𝑈 ∈ 𝑀 ↔ ∀𝑧 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))))) | ||
| Theorem | mnuop123d 44607* | Operations of a minimal universe. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
| ⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝒫 𝐴 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝐴 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝐴 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))) | ||
| Theorem | mnussd 44608* | Minimal universes are closed under subsets. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
| ⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) ⇒ ⊢ (𝜑 → 𝐵 ∈ 𝑈) | ||
| Theorem | mnuss2d 44609* | mnussd 44608 with arguments provided with an existential quantifier. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
| ⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → ∃𝑥 ∈ 𝑈 𝐴 ⊆ 𝑥) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝑈) | ||
| Theorem | mnu0eld 44610* | A nonempty minimal universe contains the empty set. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
| ⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) ⇒ ⊢ (𝜑 → ∅ ∈ 𝑈) | ||
| Theorem | mnuop23d 44611* | Second and third operations of a minimal universe. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
| ⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) ⇒ ⊢ (𝜑 → ∃𝑤 ∈ 𝑈 (𝒫 𝐴 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝐴 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝐹) → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) | ||
| Theorem | mnupwd 44612* | Minimal universes are closed under powersets. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
| ⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) ⇒ ⊢ (𝜑 → 𝒫 𝐴 ∈ 𝑈) | ||
| Theorem | mnusnd 44613* | Minimal universes are closed under singletons. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
| ⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) ⇒ ⊢ (𝜑 → {𝐴} ∈ 𝑈) | ||
| Theorem | mnuprssd 44614* | A minimal universe contains pairs of subsets of an element of the universe. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
| ⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐶 ∈ 𝑈) & ⊢ (𝜑 → 𝐴 ⊆ 𝐶) & ⊢ (𝜑 → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → {𝐴, 𝐵} ∈ 𝑈) | ||
| Theorem | mnuprss2d 44615* | Special case of mnuprssd 44614. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
| ⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐶 ∈ 𝑈) & ⊢ 𝐴 ⊆ 𝐶 & ⊢ 𝐵 ⊆ 𝐶 ⇒ ⊢ (𝜑 → {𝐴, 𝐵} ∈ 𝑈) | ||
| Theorem | mnuop3d 44616* | Third operation of a minimal universe. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
| ⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐹 ⊆ 𝑈) ⇒ ⊢ (𝜑 → ∃𝑤 ∈ 𝑈 ∀𝑖 ∈ 𝐴 (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) | ||
| Theorem | mnuprdlem1 44617* | Lemma for mnuprd 44621. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
| ⊢ 𝐹 = {{∅, {𝐴}}, {{∅}, {𝐵}}} & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑈) & ⊢ (𝜑 → ∀𝑖 ∈ {∅, {∅}}∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝑤) | ||
| Theorem | mnuprdlem2 44618* | Lemma for mnuprd 44621. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
| ⊢ 𝐹 = {{∅, {𝐴}}, {{∅}, {𝐵}}} & ⊢ (𝜑 → 𝐵 ∈ 𝑈) & ⊢ (𝜑 → ¬ 𝐴 = ∅) & ⊢ (𝜑 → ∀𝑖 ∈ {∅, {∅}}∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)) ⇒ ⊢ (𝜑 → 𝐵 ∈ 𝑤) | ||
| Theorem | mnuprdlem3 44619* | Lemma for mnuprd 44621. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
| ⊢ 𝐹 = {{∅, {𝐴}}, {{∅}, {𝐵}}} & ⊢ Ⅎ𝑖𝜑 ⇒ ⊢ (𝜑 → ∀𝑖 ∈ {∅, {∅}}∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣) | ||
| Theorem | mnuprdlem4 44620* | Lemma for mnuprd 44621. General case. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
| ⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ 𝐹 = {{∅, {𝐴}}, {{∅}, {𝐵}}} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑈) & ⊢ (𝜑 → ¬ 𝐴 = ∅) ⇒ ⊢ (𝜑 → {𝐴, 𝐵} ∈ 𝑈) | ||
| Theorem | mnuprd 44621* | Minimal universes are closed under pairing. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
| ⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑈) ⇒ ⊢ (𝜑 → {𝐴, 𝐵} ∈ 𝑈) | ||
| Theorem | mnuunid 44622* | Minimal universes are closed under union. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
| ⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) ⇒ ⊢ (𝜑 → ∪ 𝐴 ∈ 𝑈) | ||
| Theorem | mnuund 44623* | Minimal universes are closed under binary unions. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
| ⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝐴 ∪ 𝐵) ∈ 𝑈) | ||
| Theorem | mnutrcld 44624* | Minimal universes contain the elements of their elements. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
| ⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝐵 ∈ 𝑈) | ||
| Theorem | mnutrd 44625* | Minimal universes are transitive. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
| ⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) ⇒ ⊢ (𝜑 → Tr 𝑈) | ||
| Theorem | mnurndlem1 44626* | Lemma for mnurnd 44628. (Contributed by Rohan Ridenour, 12-Aug-2023.) |
| ⊢ (𝜑 → 𝐹:𝐴⟶𝑈) & ⊢ 𝐴 ∈ V & ⊢ (𝜑 → ∀𝑖 ∈ 𝐴 (∃𝑣 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})𝑖 ∈ 𝑣 → ∃𝑢 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})(𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) ⇒ ⊢ (𝜑 → ran 𝐹 ⊆ 𝑤) | ||
| Theorem | mnurndlem2 44627* | Lemma for mnurnd 44628. Deduction theorem input. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
| ⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑈) & ⊢ 𝐴 ∈ V ⇒ ⊢ (𝜑 → ran 𝐹 ∈ 𝑈) | ||
| Theorem | mnurnd 44628* | Minimal universes contain ranges of functions from an element of the universe to the universe. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
| ⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑈) ⇒ ⊢ (𝜑 → ran 𝐹 ∈ 𝑈) | ||
| Theorem | mnugrud 44629* | Minimal universes are Grothendieck universes. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
| ⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) ⇒ ⊢ (𝜑 → 𝑈 ∈ Univ) | ||
| Theorem | grumnudlem 44630* | Lemma for grumnud 44631. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
| ⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝐺 ∈ Univ) & ⊢ 𝐹 = ({⟨𝑏, 𝑐⟩ ∣ ∃𝑑(∪ 𝑑 = 𝑐 ∧ 𝑑 ∈ 𝑓 ∧ 𝑏 ∈ 𝑑)} ∩ (𝐺 × 𝐺)) & ⊢ ((𝑖 ∈ 𝐺 ∧ ℎ ∈ 𝐺) → (𝑖𝐹ℎ ↔ ∃𝑗(∪ 𝑗 = ℎ ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗))) & ⊢ ((ℎ ∈ (𝐹 Coll 𝑧) ∧ (∪ 𝑗 = ℎ ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗)) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ∈ (𝐹 Coll 𝑧))) ⇒ ⊢ (𝜑 → 𝐺 ∈ 𝑀) | ||
| Theorem | grumnud 44631* | Grothendieck universes are minimal universes. (Contributed by Rohan Ridenour, 12-Aug-2023.) |
| ⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝐺 ∈ Univ) ⇒ ⊢ (𝜑 → 𝐺 ∈ 𝑀) | ||
| Theorem | grumnueq 44632* | The class of Grothendieck universes is equal to the class of minimal universes. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
| ⊢ Univ = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} | ||
| Theorem | expandan 44633 | Expand conjunction to primitives. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
| ⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜒 ↔ 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜒) ↔ ¬ (𝜓 → ¬ 𝜃)) | ||
| Theorem | expandexn 44634 | Expand an existential quantifier to primitives while contracting a double negation. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
| ⊢ (𝜑 ↔ ¬ 𝜓) ⇒ ⊢ (∃𝑥𝜑 ↔ ¬ ∀𝑥𝜓) | ||
| Theorem | expandral 44635 | Expand a restricted universal quantifier to primitives. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
| ⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓)) | ||
| Theorem | expandrexn 44636 | Expand a restricted existential quantifier to primitives while contracting a double negation. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
| ⊢ (𝜑 ↔ ¬ 𝜓) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓)) | ||
| Theorem | expandrex 44637 | Expand a restricted existential quantifier to primitives. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
| ⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝜓)) | ||
| Theorem | expanduniss 44638* | Expand ∪ 𝐴 ⊆ 𝐵 to primitives. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
| ⊢ (∪ 𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵))) | ||
| Theorem | ismnuprim 44639* | Express the predicate on 𝑈 in ismnu 44606 using only primitives. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
| ⊢ (∀𝑧 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) ↔ ∀𝑧(𝑧 ∈ 𝑈 → ∀𝑓 ¬ ∀𝑤(𝑤 ∈ 𝑈 → ¬ ∀𝑣 ¬ ((∀𝑡(𝑡 ∈ 𝑣 → 𝑡 ∈ 𝑧) → ¬ (𝑣 ∈ 𝑈 → ¬ 𝑣 ∈ 𝑤)) → ¬ ∀𝑖(𝑖 ∈ 𝑧 → (𝑣 ∈ 𝑈 → (𝑖 ∈ 𝑣 → (𝑣 ∈ 𝑓 → ¬ ∀𝑢(𝑢 ∈ 𝑓 → (𝑖 ∈ 𝑢 → ¬ ∀𝑜(𝑜 ∈ 𝑢 → ∀𝑠(𝑠 ∈ 𝑜 → 𝑠 ∈ 𝑤)))))))))))) | ||
| Theorem | rr-grothprimbi 44640* | Express "every set is contained in a Grothendieck universe" using only primitives. The right side (without the outermost universal quantifier) is proven as rr-grothprim 44645. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
| ⊢ (∀𝑥∃𝑦 ∈ Univ 𝑥 ∈ 𝑦 ↔ ∀𝑥 ¬ ∀𝑦(𝑥 ∈ 𝑦 → ¬ ∀𝑧(𝑧 ∈ 𝑦 → ∀𝑓 ¬ ∀𝑤(𝑤 ∈ 𝑦 → ¬ ∀𝑣 ¬ ((∀𝑡(𝑡 ∈ 𝑣 → 𝑡 ∈ 𝑧) → ¬ (𝑣 ∈ 𝑦 → ¬ 𝑣 ∈ 𝑤)) → ¬ ∀𝑖(𝑖 ∈ 𝑧 → (𝑣 ∈ 𝑦 → (𝑖 ∈ 𝑣 → (𝑣 ∈ 𝑓 → ¬ ∀𝑢(𝑢 ∈ 𝑓 → (𝑖 ∈ 𝑢 → ¬ ∀𝑜(𝑜 ∈ 𝑢 → ∀𝑠(𝑠 ∈ 𝑜 → 𝑠 ∈ 𝑤))))))))))))) | ||
| Theorem | inagrud 44641 | Inaccessible levels of the cumulative hierarchy are Grothendieck universes. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
| ⊢ (𝜑 → 𝐼 ∈ Inacc) ⇒ ⊢ (𝜑 → (𝑅1‘𝐼) ∈ Univ) | ||
| Theorem | inaex 44642* | Assuming the Tarski-Grothendieck axiom, every ordinal is contained in an inaccessible ordinal. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
| ⊢ (𝐴 ∈ On → ∃𝑥 ∈ Inacc 𝐴 ∈ 𝑥) | ||
| Theorem | gruex 44643* | Assuming the Tarski-Grothendieck axiom, every set is contained in a Grothendieck universe. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
| ⊢ ∃𝑦 ∈ Univ 𝑥 ∈ 𝑦 | ||
| Theorem | rr-groth 44644* | An equivalent of ax-groth 10746 using only simple defined symbols. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
| ⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝒫 𝑧 ⊆ 𝑦 ∧ ∀𝑓∃𝑤 ∈ 𝑦 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑦 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))) | ||
| Theorem | rr-grothprim 44645* | An equivalent of ax-groth 10746 using only primitives. This uses only 123 symbols, which is significantly less than the previous record of 163 established by grothprim 10757 (which uses some defined symbols, and requires 229 symbols if expanded to primitives). (Contributed by Rohan Ridenour, 13-Aug-2023.) |
| ⊢ ¬ ∀𝑦(𝑥 ∈ 𝑦 → ¬ ∀𝑧(𝑧 ∈ 𝑦 → ∀𝑓 ¬ ∀𝑤(𝑤 ∈ 𝑦 → ¬ ∀𝑣 ¬ ((∀𝑡(𝑡 ∈ 𝑣 → 𝑡 ∈ 𝑧) → ¬ (𝑣 ∈ 𝑦 → ¬ 𝑣 ∈ 𝑤)) → ¬ ∀𝑖(𝑖 ∈ 𝑧 → (𝑣 ∈ 𝑦 → (𝑖 ∈ 𝑣 → (𝑣 ∈ 𝑓 → ¬ ∀𝑢(𝑢 ∈ 𝑓 → (𝑖 ∈ 𝑢 → ¬ ∀𝑜(𝑜 ∈ 𝑢 → ∀𝑠(𝑠 ∈ 𝑜 → 𝑠 ∈ 𝑤)))))))))))) | ||
| Theorem | ismnushort 44646* | Express the predicate on 𝑈 and 𝑧 in ismnu 44606 in a shorter form while avoiding complicated definitions. (Contributed by Rohan Ridenour, 10-Oct-2024.) |
| ⊢ (∀𝑓 ∈ 𝒫 𝑈∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ (𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))) | ||
| Theorem | dfuniv2 44647* | Alternative definition of Univ using only simple defined symbols. (Contributed by Rohan Ridenour, 10-Oct-2024.) |
| ⊢ Univ = {𝑦 ∣ ∀𝑧 ∈ 𝑦 ∀𝑓 ∈ 𝒫 𝑦∃𝑤 ∈ 𝑦 (𝒫 𝑧 ⊆ (𝑦 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤))} | ||
| Theorem | rr-grothshortbi 44648* | Express "every set is contained in a Grothendieck universe" in a short form while avoiding complicated definitions. (Contributed by Rohan Ridenour, 8-Oct-2024.) |
| ⊢ (∀𝑥∃𝑦 ∈ Univ 𝑥 ∈ 𝑦 ↔ ∀𝑥∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 ∀𝑓 ∈ 𝒫 𝑦∃𝑤 ∈ 𝑦 (𝒫 𝑧 ⊆ (𝑦 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)))) | ||
| Theorem | rr-grothshort 44649* | A shorter equivalent of ax-groth 10746 than rr-groth 44644 using a few more simple defined symbols. (Contributed by Rohan Ridenour, 8-Oct-2024.) |
| ⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 ∀𝑓 ∈ 𝒫 𝑦∃𝑤 ∈ 𝑦 (𝒫 𝑧 ⊆ (𝑦 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤))) | ||
| Theorem | nanorxor 44650 | 'nand' is equivalent to the equivalence of inclusive and exclusive or. (Contributed by Steve Rodriguez, 28-Feb-2020.) |
| ⊢ ((𝜑 ⊼ 𝜓) ↔ ((𝜑 ∨ 𝜓) ↔ (𝜑 ⊻ 𝜓))) | ||
| Theorem | undisjrab 44651 | Union of two disjoint restricted class abstractions; compare unrab 4269. (Contributed by Steve Rodriguez, 28-Feb-2020.) |
| ⊢ (({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐴 ∣ 𝜓}) = ∅ ↔ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ⊻ 𝜓)}) | ||
| Theorem | iso0 44652 | The empty set is an 𝑅, 𝑆 isomorphism from the empty set to the empty set. (Contributed by Steve Rodriguez, 24-Oct-2015.) |
| ⊢ ∅ Isom 𝑅, 𝑆 (∅, ∅) | ||
| Theorem | ssrecnpr 44653 | ℝ is a subset of both ℝ and ℂ. (Contributed by Steve Rodriguez, 22-Nov-2015.) |
| ⊢ (𝑆 ∈ {ℝ, ℂ} → ℝ ⊆ 𝑆) | ||
| Theorem | seff 44654 | Let set 𝑆 be the real or complex numbers. Then the exponential function restricted to 𝑆 is a mapping from 𝑆 to 𝑆. (Contributed by Steve Rodriguez, 6-Nov-2015.) |
| ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) ⇒ ⊢ (𝜑 → (exp ↾ 𝑆):𝑆⟶𝑆) | ||
| Theorem | sblpnf 44655 | The infinity ball in the absolute value metric is just the whole space. 𝑆 analogue of blpnf 24353. (Contributed by Steve Rodriguez, 8-Nov-2015.) |
| ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ 𝐷 = ((abs ∘ − ) ↾ (𝑆 × 𝑆)) ⇒ ⊢ ((𝜑 ∧ 𝑃 ∈ 𝑆) → (𝑃(ball‘𝐷)+∞) = 𝑆) | ||
| Theorem | prmunb2 44656* | The primes are unbounded. This generalizes prmunb 16854 to real 𝐴 with arch 12410 and lttrd 11306: every real is less than some positive integer, itself less than some prime. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
| ⊢ (𝐴 ∈ ℝ → ∃𝑝 ∈ ℙ 𝐴 < 𝑝) | ||
| Theorem | dvgrat 44657* | Ratio test for divergence of a complex infinite series. See e.g. remark "if (abs‘((𝑎‘(𝑛 + 1)) / (𝑎‘𝑛))) ≥ 1 for all large n..." in https://en.wikipedia.org/wiki/Ratio_test#The_test. (Contributed by Steve Rodriguez, 28-Feb-2020.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝑊 = (ℤ≥‘𝑁) & ⊢ (𝜑 → 𝑁 ∈ 𝑍) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → (𝐹‘𝑘) ≠ 0) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → (abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))) ⇒ ⊢ (𝜑 → seq𝑀( + , 𝐹) ∉ dom ⇝ ) | ||
| Theorem | cvgdvgrat 44658* |
Ratio test for convergence and divergence of a complex infinite series.
If the ratio 𝑅 of the absolute values of successive
terms in an
infinite sequence 𝐹 converges to less than one, then the
infinite
sum of the terms of 𝐹 converges to a complex number; and
if 𝑅
converges greater then the sum diverges. This combined form of
cvgrat 15818 and dvgrat 44657 directly uses the limit of the ratio.
(It also demonstrates how to use climi2 15446 and absltd 15367 to transform a limit to an inequality cf. https://math.stackexchange.com/q/2215191 15367, and how to use r19.29a 3146 in a similar fashion to Mario Carneiro's proof sketch with rexlimdva 3139 at https://groups.google.com/g/metamath/c/2RPikOiXLMo 3139.) (Contributed by Steve Rodriguez, 28-Feb-2020.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝑊 = (ℤ≥‘𝑁) & ⊢ (𝜑 → 𝑁 ∈ 𝑍) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → (𝐹‘𝑘) ≠ 0) & ⊢ 𝑅 = (𝑘 ∈ 𝑊 ↦ (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘)))) & ⊢ (𝜑 → 𝑅 ⇝ 𝐿) & ⊢ (𝜑 → 𝐿 ≠ 1) ⇒ ⊢ (𝜑 → (𝐿 < 1 ↔ seq𝑀( + , 𝐹) ∈ dom ⇝ )) | ||
| Theorem | radcnvrat 44659* | Let 𝐿 be the limit, if one exists, of the ratio (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))) (as in the ratio test cvgdvgrat 44658) as 𝑘 increases. Then the radius of convergence of power series Σ𝑛 ∈ ℕ0((𝐴‘𝑛) · (𝑥↑𝑛)) is (1 / 𝐿) if 𝐿 is nonzero. Proof "The limit involved in the ratio test..." in https://en.wikipedia.org/wiki/Radius_of_convergence 44658 —a few lines that evidently hide quite an involved process to confirm. (Contributed by Steve Rodriguez, 8-Mar-2020.) |
| ⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) & ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) & ⊢ 𝐷 = (𝑘 ∈ ℕ0 ↦ (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)))) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐴‘𝑘) ≠ 0) & ⊢ (𝜑 → 𝐷 ⇝ 𝐿) & ⊢ (𝜑 → 𝐿 ≠ 0) ⇒ ⊢ (𝜑 → 𝑅 = (1 / 𝐿)) | ||
| Theorem | reldvds 44660 | The divides relation is in fact a relation. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
| ⊢ Rel ∥ | ||
| Theorem | nznngen 44661 | All positive integers in the set of multiples of n, nℤ, are the absolute value of n or greater. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
| ⊢ (𝜑 → 𝑁 ∈ ℤ) ⇒ ⊢ (𝜑 → (( ∥ “ {𝑁}) ∩ ℕ) ⊆ (ℤ≥‘(abs‘𝑁))) | ||
| Theorem | nzss 44662 | The set of multiples of m, mℤ, is a subset of those of n, nℤ, iff n divides m. Lemma 2.1(a) of https://www.mscs.dal.ca/~selinger/3343/handouts/ideals.pdf p. 5, with mℤ and nℤ as images of the divides relation under m and n. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
| ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ 𝑉) ⇒ ⊢ (𝜑 → (( ∥ “ {𝑀}) ⊆ ( ∥ “ {𝑁}) ↔ 𝑁 ∥ 𝑀)) | ||
| Theorem | nzin 44663 | The intersection of the set of multiples of m, mℤ, and those of n, nℤ, is the set of multiples of their least common multiple. Roughly Lemma 2.1(c) of https://www.mscs.dal.ca/~selinger/3343/handouts/ideals.pdf p. 5 and Problem 1(b) of https://people.math.binghamton.edu/mazur/teach/40107/40107h16sol.pdf p. 1, with mℤ and nℤ as images of the divides relation under m and n. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
| ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) ⇒ ⊢ (𝜑 → (( ∥ “ {𝑀}) ∩ ( ∥ “ {𝑁})) = ( ∥ “ {(𝑀 lcm 𝑁)})) | ||
| Theorem | nzprmdif 44664 | Subtract one prime's multiples from an unequal prime's. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
| ⊢ (𝜑 → 𝑀 ∈ ℙ) & ⊢ (𝜑 → 𝑁 ∈ ℙ) & ⊢ (𝜑 → 𝑀 ≠ 𝑁) ⇒ ⊢ (𝜑 → (( ∥ “ {𝑀}) ∖ ( ∥ “ {𝑁})) = (( ∥ “ {𝑀}) ∖ ( ∥ “ {(𝑀 · 𝑁)}))) | ||
| Theorem | hashnzfz 44665 | Special case of hashdvds 16714: the count of multiples in nℤ restricted to an interval. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐽 ∈ ℤ) & ⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘(𝐽 − 1))) ⇒ ⊢ (𝜑 → (♯‘(( ∥ “ {𝑁}) ∩ (𝐽...𝐾))) = ((⌊‘(𝐾 / 𝑁)) − (⌊‘((𝐽 − 1) / 𝑁)))) | ||
| Theorem | hashnzfz2 44666 | Special case of hashnzfz 44665: the count of multiples in nℤ, n greater than one, restricted to an interval starting at two. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
| ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘2)) & ⊢ (𝜑 → 𝐾 ∈ ℕ) ⇒ ⊢ (𝜑 → (♯‘(( ∥ “ {𝑁}) ∩ (2...𝐾))) = (⌊‘(𝐾 / 𝑁))) | ||
| Theorem | hashnzfzclim 44667* | As the upper bound 𝐾 of the constraint interval (𝐽...𝐾) in hashnzfz 44665 increases, the resulting count of multiples tends to (𝐾 / 𝑀) —that is, there are approximately (𝐾 / 𝑀) multiples of 𝑀 in a finite interval of integers. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
| ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐽 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝑘 ∈ (ℤ≥‘(𝐽 − 1)) ↦ ((♯‘(( ∥ “ {𝑀}) ∩ (𝐽...𝑘))) / 𝑘)) ⇝ (1 / 𝑀)) | ||
| Theorem | caofcan 44668* | Transfer a cancellation law like mulcan 11786 to the function operation. (Contributed by Steve Rodriguez, 16-Nov-2015.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑇) & ⊢ (𝜑 → 𝐺:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐻:𝐴⟶𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑇 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝑅𝑦) = (𝑥𝑅𝑧) ↔ 𝑦 = 𝑧)) ⇒ ⊢ (𝜑 → ((𝐹 ∘f 𝑅𝐺) = (𝐹 ∘f 𝑅𝐻) ↔ 𝐺 = 𝐻)) | ||
| Theorem | ofsubid 44669 | Function analogue of subid 11412. (Contributed by Steve Rodriguez, 5-Nov-2015.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ) → (𝐹 ∘f − 𝐹) = (𝐴 × {0})) | ||
| Theorem | ofmul12 44670 | Function analogue of mul12 11310. (Contributed by Steve Rodriguez, 13-Nov-2015.) |
| ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐺:𝐴⟶ℂ ∧ 𝐻:𝐴⟶ℂ)) → (𝐹 ∘f · (𝐺 ∘f · 𝐻)) = (𝐺 ∘f · (𝐹 ∘f · 𝐻))) | ||
| Theorem | ofdivrec 44671 | Function analogue of divrec 11824, a division analogue of ofnegsub 12155. (Contributed by Steve Rodriguez, 3-Nov-2015.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ ∧ 𝐺:𝐴⟶(ℂ ∖ {0})) → (𝐹 ∘f · ((𝐴 × {1}) ∘f / 𝐺)) = (𝐹 ∘f / 𝐺)) | ||
| Theorem | ofdivcan4 44672 | Function analogue of divcan4 11835. (Contributed by Steve Rodriguez, 4-Nov-2015.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ ∧ 𝐺:𝐴⟶(ℂ ∖ {0})) → ((𝐹 ∘f · 𝐺) ∘f / 𝐺) = 𝐹) | ||
| Theorem | ofdivdiv2 44673 | Function analogue of divdiv2 11865. (Contributed by Steve Rodriguez, 23-Nov-2015.) |
| ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐺:𝐴⟶(ℂ ∖ {0}) ∧ 𝐻:𝐴⟶(ℂ ∖ {0}))) → (𝐹 ∘f / (𝐺 ∘f / 𝐻)) = ((𝐹 ∘f · 𝐻) ∘f / 𝐺)) | ||
| Theorem | lhe4.4ex1a 44674 | Example of the Fundamental Theorem of Calculus, part two (ftc2 26019): ∫(1(,)2)((𝑥↑2) − 3) d𝑥 = -(2 / 3). Section 4.4 example 1a of [LarsonHostetlerEdwards] p. 311. (The book teaches ftc2 26019 as simply the "Fundamental Theorem of Calculus", then ftc1 26017 as the "Second Fundamental Theorem of Calculus".) (Contributed by Steve Rodriguez, 28-Oct-2015.) (Revised by Steve Rodriguez, 31-Oct-2015.) |
| ⊢ ∫(1(,)2)((𝑥↑2) − 3) d𝑥 = -(2 / 3) | ||
| Theorem | dvsconst 44675 | Derivative of a constant function on the real or complex numbers. The function may return a complex 𝐴 even if 𝑆 is ℝ. (Contributed by Steve Rodriguez, 11-Nov-2015.) |
| ⊢ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐴 ∈ ℂ) → (𝑆 D (𝑆 × {𝐴})) = (𝑆 × {0})) | ||
| Theorem | dvsid 44676 | Derivative of the identity function on the real or complex numbers. (Contributed by Steve Rodriguez, 11-Nov-2015.) |
| ⊢ (𝑆 ∈ {ℝ, ℂ} → (𝑆 D ( I ↾ 𝑆)) = (𝑆 × {1})) | ||
| Theorem | dvsef 44677 | Derivative of the exponential function on the real or complex numbers. (Contributed by Steve Rodriguez, 12-Nov-2015.) |
| ⊢ (𝑆 ∈ {ℝ, ℂ} → (𝑆 D (exp ↾ 𝑆)) = (exp ↾ 𝑆)) | ||
| Theorem | expgrowthi 44678* | Exponential growth and decay model. See expgrowth 44680 for more information. (Contributed by Steve Rodriguez, 4-Nov-2015.) |
| ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝐾 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ 𝑌 = (𝑡 ∈ 𝑆 ↦ (𝐶 · (exp‘(𝐾 · 𝑡)))) ⇒ ⊢ (𝜑 → (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) | ||
| Theorem | dvconstbi 44679* | The derivative of a function on 𝑆 is zero iff it is a constant function. Roughly a biconditional 𝑆 analogue of dvconst 25886 and dveq0 25973. Corresponds to integration formula "∫0 d𝑥 = 𝐶 " in section 4.1 of [LarsonHostetlerEdwards] p. 278. (Contributed by Steve Rodriguez, 11-Nov-2015.) |
| ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝑌:𝑆⟶ℂ) & ⊢ (𝜑 → dom (𝑆 D 𝑌) = 𝑆) ⇒ ⊢ (𝜑 → ((𝑆 D 𝑌) = (𝑆 × {0}) ↔ ∃𝑐 ∈ ℂ 𝑌 = (𝑆 × {𝑐}))) | ||
| Theorem | expgrowth 44680* |
Exponential growth and decay model. The derivative of a function y of
variable t equals a constant k times y itself, iff
y equals some
constant C times the exponential of kt. This theorem and
expgrowthi 44678 illustrate one of the simplest and most
crucial classes of
differential equations, equations that relate functions to their
derivatives.
Section 6.3 of [Strang] p. 242 calls y' = ky "the most important differential equation in applied mathematics". In the field of population ecology it is known as the Malthusian growth model or exponential law, and C, k, and t correspond to initial population size, growth rate, and time respectively (https://en.wikipedia.org/wiki/Malthusian_growth_model 44678); and in finance, the model appears in a similar role in continuous compounding with C as the initial amount of money. In exponential decay models, k is often expressed as the negative of a positive constant λ. Here y' is given as (𝑆 D 𝑌), C as 𝑐, and ky as ((𝑆 × {𝐾}) ∘f · 𝑌). (𝑆 × {𝐾}) is the constant function that maps any real or complex input to k and ∘f · is multiplication as a function operation. The leftward direction of the biconditional is as given in http://www.saylor.org/site/wp-content/uploads/2011/06/MA221-2.1.1.pdf 44678 pp. 1-2, which also notes the reverse direction ("While we will not prove this here, it turns out that these are the only functions that satisfy this equation."). The rightward direction is Theorem 5.1 of [LarsonHostetlerEdwards] p. 375 (which notes " C is the initial value of y, and k is the proportionality constant. Exponential growth occurs when k > 0, and exponential decay occurs when k < 0."); its proof here closely follows the proof of y' = y in https://proofwiki.org/wiki/Exponential_Growth_Equation/Special_Case 44678. Statements for this and expgrowthi 44678 formulated by Mario Carneiro. (Contributed by Steve Rodriguez, 24-Nov-2015.) |
| ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝐾 ∈ ℂ) & ⊢ (𝜑 → 𝑌:𝑆⟶ℂ) & ⊢ (𝜑 → dom (𝑆 D 𝑌) = 𝑆) ⇒ ⊢ (𝜑 → ((𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌) ↔ ∃𝑐 ∈ ℂ 𝑌 = (𝑡 ∈ 𝑆 ↦ (𝑐 · (exp‘(𝐾 · 𝑡)))))) | ||
| Syntax | cbcc 44681 | Extend class notation to include the generalized binomial coefficient operation. |
| class C𝑐 | ||
| Definition | df-bcc 44682* | Define a generalized binomial coefficient operation, which unlike df-bc 14238 allows complex numbers for the first argument. (Contributed by Steve Rodriguez, 22-Apr-2020.) |
| ⊢ C𝑐 = (𝑐 ∈ ℂ, 𝑘 ∈ ℕ0 ↦ ((𝑐 FallFac 𝑘) / (!‘𝑘))) | ||
| Theorem | bccval 44683 | Value of the generalized binomial coefficient, 𝐶 choose 𝐾. (Contributed by Steve Rodriguez, 22-Apr-2020.) |
| ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐾 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝐶C𝑐𝐾) = ((𝐶 FallFac 𝐾) / (!‘𝐾))) | ||
| Theorem | bcccl 44684 | Closure of the generalized binomial coefficient. (Contributed by Steve Rodriguez, 22-Apr-2020.) |
| ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐾 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝐶C𝑐𝐾) ∈ ℂ) | ||
| Theorem | bcc0 44685 | The generalized binomial coefficient 𝐶 choose 𝐾 is zero iff 𝐶 is an integer between zero and (𝐾 − 1) inclusive. (Contributed by Steve Rodriguez, 22-Apr-2020.) |
| ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐾 ∈ ℕ0) ⇒ ⊢ (𝜑 → ((𝐶C𝑐𝐾) = 0 ↔ 𝐶 ∈ (0...(𝐾 − 1)))) | ||
| Theorem | bccp1k 44686 | Generalized binomial coefficient: 𝐶 choose (𝐾 + 1). (Contributed by Steve Rodriguez, 22-Apr-2020.) |
| ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐾 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝐶C𝑐(𝐾 + 1)) = ((𝐶C𝑐𝐾) · ((𝐶 − 𝐾) / (𝐾 + 1)))) | ||
| Theorem | bccm1k 44687 | Generalized binomial coefficient: 𝐶 choose (𝐾 − 1), when 𝐶 is not (𝐾 − 1). (Contributed by Steve Rodriguez, 22-Apr-2020.) |
| ⊢ (𝜑 → 𝐶 ∈ (ℂ ∖ {(𝐾 − 1)})) & ⊢ (𝜑 → 𝐾 ∈ ℕ) ⇒ ⊢ (𝜑 → (𝐶C𝑐(𝐾 − 1)) = ((𝐶C𝑐𝐾) / ((𝐶 − (𝐾 − 1)) / 𝐾))) | ||
| Theorem | bccn0 44688 | Generalized binomial coefficient: 𝐶 choose 0. (Contributed by Steve Rodriguez, 22-Apr-2020.) |
| ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐶C𝑐0) = 1) | ||
| Theorem | bccn1 44689 | Generalized binomial coefficient: 𝐶 choose 1. (Contributed by Steve Rodriguez, 22-Apr-2020.) |
| ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐶C𝑐1) = 𝐶) | ||
| Theorem | bccbc 44690 | The binomial coefficient and generalized binomial coefficient are equal when their arguments are nonnegative integers. (Contributed by Steve Rodriguez, 22-Apr-2020.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐾 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝑁C𝑐𝐾) = (𝑁C𝐾)) | ||
| Theorem | uzmptshftfval 44691* | When 𝐹 is a maps-to function on some set of upper integers 𝑍 that returns a set 𝐵, (𝐹 shift 𝑁) is another maps-to function on the shifted set of upper integers 𝑊. (Contributed by Steve Rodriguez, 22-Apr-2020.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝑍 ↦ 𝐵) & ⊢ 𝐵 ∈ V & ⊢ (𝑥 = (𝑦 − 𝑁) → 𝐵 = 𝐶) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝑊 = (ℤ≥‘(𝑀 + 𝑁)) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝐹 shift 𝑁) = (𝑦 ∈ 𝑊 ↦ 𝐶)) | ||
| Theorem | dvradcnv2 44692* | The radius of convergence of the (formal) derivative 𝐻 of the power series 𝐺 is (at least) as large as the radius of convergence of 𝐺. This version of dvradcnv 26398 uses a shifted version of 𝐻 to match the sum form of (ℂ D 𝐹) in pserdv2 26408 (and shows how to use uzmptshftfval 44691 to shift a maps-to function on a set of upper integers). (Contributed by Steve Rodriguez, 22-Apr-2020.) |
| ⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) & ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) & ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ ((𝑛 · (𝐴‘𝑛)) · (𝑋↑(𝑛 − 1)))) & ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → (abs‘𝑋) < 𝑅) ⇒ ⊢ (𝜑 → seq1( + , 𝐻) ∈ dom ⇝ ) | ||
| Theorem | binomcxplemwb 44693 | Lemma for binomcxp 44702. The lemma in the Wikibooks proof. (Contributed by Steve Rodriguez, 22-Apr-2020.) |
| ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐾 ∈ ℕ) ⇒ ⊢ (𝜑 → (((𝐶 − 𝐾) · (𝐶C𝑐𝐾)) + ((𝐶 − (𝐾 − 1)) · (𝐶C𝑐(𝐾 − 1)))) = (𝐶 · (𝐶C𝑐𝐾))) | ||
| Theorem | binomcxplemnn0 44694* | Lemma for binomcxp 44702. When 𝐶 is a nonnegative integer, the binomial's finite sum value by the standard binomial theorem binom 15765 equals this generalized infinite sum: the generalized binomial coefficient and exponentiation operators give exactly the same values in the standard index set (0...𝐶), and when the index set is widened beyond 𝐶 the additional values are just zeroes. (Contributed by Steve Rodriguez, 22-Apr-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (abs‘𝐵) < (abs‘𝐴)) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ ((𝜑 ∧ 𝐶 ∈ ℕ0) → ((𝐴 + 𝐵)↑𝑐𝐶) = Σ𝑘 ∈ ℕ0 ((𝐶C𝑐𝑘) · ((𝐴↑𝑐(𝐶 − 𝑘)) · (𝐵↑𝑘)))) | ||
| Theorem | binomcxplemrat 44695* | Lemma for binomcxp 44702. As 𝑘 increases, this ratio's absolute value converges to one. Part of equation "Since continuity of the absolute value..." in the Wikibooks proof (proven for the inverse ratio, which we later show is no problem). (Contributed by Steve Rodriguez, 22-Apr-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (abs‘𝐵) < (abs‘𝐴)) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ (abs‘((𝐶 − 𝑘) / (𝑘 + 1)))) ⇝ 1) | ||
| Theorem | binomcxplemfrat 44696* | Lemma for binomcxp 44702. binomcxplemrat 44695 implies that when 𝐶 is not a nonnegative integer, the absolute value of the ratio ((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘)) converges to one. The rest of equation "Since continuity of the absolute value..." in the Wikibooks proof. (Contributed by Steve Rodriguez, 22-Apr-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (abs‘𝐵) < (abs‘𝐴)) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ 𝐹 = (𝑗 ∈ ℕ0 ↦ (𝐶C𝑐𝑗)) ⇒ ⊢ ((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) → (𝑘 ∈ ℕ0 ↦ (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘)))) ⇝ 1) | ||
| Theorem | binomcxplemradcnv 44697* | Lemma for binomcxp 44702. By binomcxplemfrat 44696 and radcnvrat 44659 the radius of convergence of power series Σ𝑘 ∈ ℕ0((𝐹‘𝑘) · (𝑏↑𝑘)) is one. (Contributed by Steve Rodriguez, 22-Apr-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (abs‘𝐵) < (abs‘𝐴)) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ 𝐹 = (𝑗 ∈ ℕ0 ↦ (𝐶C𝑐𝑗)) & ⊢ 𝑆 = (𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘)))) & ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑆‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) ⇒ ⊢ ((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) → 𝑅 = 1) | ||
| Theorem | binomcxplemdvbinom 44698* | Lemma for binomcxp 44702. By the power and chain rules, calculate the derivative of ((1 + 𝑏)↑𝑐-𝐶), with respect to 𝑏 in the disk of convergence 𝐷. We later multiply the derivative in the later binomcxplemdvsum 44700 by this derivative to show that ((1 + 𝑏)↑𝑐𝐶) (with a nonnegated 𝐶) and the later sum, since both at 𝑏 = 0 equal one, are the same. (Contributed by Steve Rodriguez, 22-Apr-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (abs‘𝐵) < (abs‘𝐴)) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ 𝐹 = (𝑗 ∈ ℕ0 ↦ (𝐶C𝑐𝑗)) & ⊢ 𝑆 = (𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘)))) & ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑆‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) & ⊢ 𝐸 = (𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ ↦ ((𝑘 · (𝐹‘𝑘)) · (𝑏↑(𝑘 − 1))))) & ⊢ 𝐷 = (◡abs “ (0[,)𝑅)) ⇒ ⊢ ((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) → (ℂ D (𝑏 ∈ 𝐷 ↦ ((1 + 𝑏)↑𝑐-𝐶))) = (𝑏 ∈ 𝐷 ↦ (-𝐶 · ((1 + 𝑏)↑𝑐(-𝐶 − 1))))) | ||
| Theorem | binomcxplemcvg 44699* | Lemma for binomcxp 44702. The sum in binomcxplemnn0 44694 and its derivative (see the next theorem, binomcxplemdvsum 44700) converge, as long as their base 𝐽 is within the disk of convergence. Part of remark "This convergence allows us to apply term-by-term differentiation..." in the Wikibooks proof. (Contributed by Steve Rodriguez, 22-Apr-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (abs‘𝐵) < (abs‘𝐴)) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ 𝐹 = (𝑗 ∈ ℕ0 ↦ (𝐶C𝑐𝑗)) & ⊢ 𝑆 = (𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘)))) & ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑆‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) & ⊢ 𝐸 = (𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ ↦ ((𝑘 · (𝐹‘𝑘)) · (𝑏↑(𝑘 − 1))))) & ⊢ 𝐷 = (◡abs “ (0[,)𝑅)) ⇒ ⊢ ((𝜑 ∧ 𝐽 ∈ 𝐷) → (seq0( + , (𝑆‘𝐽)) ∈ dom ⇝ ∧ seq1( + , (𝐸‘𝐽)) ∈ dom ⇝ )) | ||
| Theorem | binomcxplemdvsum 44700* | Lemma for binomcxp 44702. The derivative of the generalized sum in binomcxplemnn0 44694. Part of remark "This convergence allows to apply term-by-term differentiation..." in the Wikibooks proof. (Contributed by Steve Rodriguez, 22-Apr-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (abs‘𝐵) < (abs‘𝐴)) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ 𝐹 = (𝑗 ∈ ℕ0 ↦ (𝐶C𝑐𝑗)) & ⊢ 𝑆 = (𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘)))) & ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑆‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) & ⊢ 𝐸 = (𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ ↦ ((𝑘 · (𝐹‘𝑘)) · (𝑏↑(𝑘 − 1))))) & ⊢ 𝐷 = (◡abs “ (0[,)𝑅)) & ⊢ 𝑃 = (𝑏 ∈ 𝐷 ↦ Σ𝑘 ∈ ℕ0 ((𝑆‘𝑏)‘𝑘)) ⇒ ⊢ (𝜑 → (ℂ D 𝑃) = (𝑏 ∈ 𝐷 ↦ Σ𝑘 ∈ ℕ ((𝐸‘𝑏)‘𝑘))) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |