Home | Metamath
Proof Explorer Theorem List (p. 407 of 449) | < 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-28689) |
Hilbert Space Explorer
(28690-30212) |
Users' Mathboxes
(30213-44899) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | mnuprdlem1 40601* | Lemma for mnuprd 40605. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
⊢ 𝐹 = {{∅, {𝐴}}, {{∅}, {𝐵}}} & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑈) & ⊢ (𝜑 → ∀𝑖 ∈ {∅, {∅}}∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝑤) | ||
Theorem | mnuprdlem2 40602* | Lemma for mnuprd 40605. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
⊢ 𝐹 = {{∅, {𝐴}}, {{∅}, {𝐵}}} & ⊢ (𝜑 → 𝐵 ∈ 𝑈) & ⊢ (𝜑 → ¬ 𝐴 = ∅) & ⊢ (𝜑 → ∀𝑖 ∈ {∅, {∅}}∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)) ⇒ ⊢ (𝜑 → 𝐵 ∈ 𝑤) | ||
Theorem | mnuprdlem3 40603* | Lemma for mnuprd 40605. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
⊢ 𝐹 = {{∅, {𝐴}}, {{∅}, {𝐵}}} & ⊢ Ⅎ𝑖𝜑 ⇒ ⊢ (𝜑 → ∀𝑖 ∈ {∅, {∅}}∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣) | ||
Theorem | mnuprdlem4 40604* | Lemma for mnuprd 40605. General case. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ 𝐹 = {{∅, {𝐴}}, {{∅}, {𝐵}}} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑈) & ⊢ (𝜑 → ¬ 𝐴 = ∅) ⇒ ⊢ (𝜑 → {𝐴, 𝐵} ∈ 𝑈) | ||
Theorem | mnuprd 40605* | Minimal universes are closed under pairing. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑈) ⇒ ⊢ (𝜑 → {𝐴, 𝐵} ∈ 𝑈) | ||
Theorem | mnuunid 40606* | Minimal universes are closed under union. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) ⇒ ⊢ (𝜑 → ∪ 𝐴 ∈ 𝑈) | ||
Theorem | mnuund 40607* | Minimal universes are closed under binary unions. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝐴 ∪ 𝐵) ∈ 𝑈) | ||
Theorem | mnutrcld 40608* | Minimal universes contain the elements of their elements. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝐵 ∈ 𝑈) | ||
Theorem | mnutrd 40609* | Minimal universes are transitive. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) ⇒ ⊢ (𝜑 → Tr 𝑈) | ||
Theorem | mnurndlem1 40610* | Lemma for mnurnd 40612. (Contributed by Rohan Ridenour, 12-Aug-2023.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝑈) & ⊢ 𝐴 ∈ V & ⊢ (𝜑 → ∀𝑖 ∈ 𝐴 (∃𝑣 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})𝑖 ∈ 𝑣 → ∃𝑢 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})(𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) ⇒ ⊢ (𝜑 → ran 𝐹 ⊆ 𝑤) | ||
Theorem | mnurndlem2 40611* | Lemma for mnurnd 40612. Deduction theorem input. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑈) & ⊢ 𝐴 ∈ V ⇒ ⊢ (𝜑 → ran 𝐹 ∈ 𝑈) | ||
Theorem | mnurnd 40612* | 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 40613* | Minimal universes are Grothendieck universes. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) ⇒ ⊢ (𝜑 → 𝑈 ∈ Univ) | ||
Theorem | grumnudlem 40614* | Lemma for grumnud 40615. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝐺 ∈ Univ) & ⊢ 𝐹 = ({〈𝑏, 𝑐〉 ∣ ∃𝑑(∪ 𝑑 = 𝑐 ∧ 𝑑 ∈ 𝑓 ∧ 𝑏 ∈ 𝑑)} ∩ (𝐺 × 𝐺)) & ⊢ ((𝑖 ∈ 𝐺 ∧ ℎ ∈ 𝐺) → (𝑖𝐹ℎ ↔ ∃𝑗(∪ 𝑗 = ℎ ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗))) & ⊢ ((ℎ ∈ (𝐹 Coll 𝑧) ∧ (∪ 𝑗 = ℎ ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗)) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ∈ (𝐹 Coll 𝑧))) ⇒ ⊢ (𝜑 → 𝐺 ∈ 𝑀) | ||
Theorem | grumnud 40615* | Grothendieck universes are minimal universes. (Contributed by Rohan Ridenour, 12-Aug-2023.) |
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝐺 ∈ Univ) ⇒ ⊢ (𝜑 → 𝐺 ∈ 𝑀) | ||
Theorem | grumnueq 40616* | The class of Grothendieck universes is equal to the class of minimal universes. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ Univ = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} | ||
Theorem | expandan 40617 | Expand conjunction to primitives. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜒 ↔ 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜒) ↔ ¬ (𝜓 → ¬ 𝜃)) | ||
Theorem | expandexn 40618 | Expand an existential quantifier to primitives while contracting a double negation. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ (𝜑 ↔ ¬ 𝜓) ⇒ ⊢ (∃𝑥𝜑 ↔ ¬ ∀𝑥𝜓) | ||
Theorem | expandral 40619 | Expand a restricted universal quantifier to primitives. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓)) | ||
Theorem | expandrexn 40620 | Expand a restricted existential quantifier to primitives while contracting a double negation. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ (𝜑 ↔ ¬ 𝜓) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓)) | ||
Theorem | expandrex 40621 | Expand a restricted existential quantifier to primitives. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝜓)) | ||
Theorem | expanduniss 40622* | Expand ∪ 𝐴 ⊆ 𝐵 to primitives. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ (∪ 𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵))) | ||
Theorem | ismnuprim 40623* | Express the predicate on 𝑈 in ismnu 40590 using only primitives. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ (∀𝑧 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) ↔ ∀𝑧(𝑧 ∈ 𝑈 → ∀𝑓 ¬ ∀𝑤(𝑤 ∈ 𝑈 → ¬ ∀𝑣 ¬ ((∀𝑡(𝑡 ∈ 𝑣 → 𝑡 ∈ 𝑧) → ¬ (𝑣 ∈ 𝑈 → ¬ 𝑣 ∈ 𝑤)) → ¬ ∀𝑖(𝑖 ∈ 𝑧 → (𝑣 ∈ 𝑈 → (𝑖 ∈ 𝑣 → (𝑣 ∈ 𝑓 → ¬ ∀𝑢(𝑢 ∈ 𝑓 → (𝑖 ∈ 𝑢 → ¬ ∀𝑜(𝑜 ∈ 𝑢 → ∀𝑠(𝑠 ∈ 𝑜 → 𝑠 ∈ 𝑤)))))))))))) | ||
Theorem | rr-grothprimbi 40624* | 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 40629. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ (∀𝑥∃𝑦 ∈ Univ 𝑥 ∈ 𝑦 ↔ ∀𝑥 ¬ ∀𝑦(𝑥 ∈ 𝑦 → ¬ ∀𝑧(𝑧 ∈ 𝑦 → ∀𝑓 ¬ ∀𝑤(𝑤 ∈ 𝑦 → ¬ ∀𝑣 ¬ ((∀𝑡(𝑡 ∈ 𝑣 → 𝑡 ∈ 𝑧) → ¬ (𝑣 ∈ 𝑦 → ¬ 𝑣 ∈ 𝑤)) → ¬ ∀𝑖(𝑖 ∈ 𝑧 → (𝑣 ∈ 𝑦 → (𝑖 ∈ 𝑣 → (𝑣 ∈ 𝑓 → ¬ ∀𝑢(𝑢 ∈ 𝑓 → (𝑖 ∈ 𝑢 → ¬ ∀𝑜(𝑜 ∈ 𝑢 → ∀𝑠(𝑠 ∈ 𝑜 → 𝑠 ∈ 𝑤))))))))))))) | ||
Theorem | inagrud 40625 | Inaccessible levels of the cumulative hierarchy are Grothendieck universes. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ (𝜑 → 𝐼 ∈ Inacc) ⇒ ⊢ (𝜑 → (𝑅1‘𝐼) ∈ Univ) | ||
Theorem | inaex 40626* | Assuming the Tarski-Grothendieck axiom, every ordinal is contained in an inaccessible ordinal. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ (𝐴 ∈ On → ∃𝑥 ∈ Inacc 𝐴 ∈ 𝑥) | ||
Theorem | gruex 40627* | Assuming the Tarski-Grothendieck axiom, every set is contained in a Grothendieck universe. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ ∃𝑦 ∈ Univ 𝑥 ∈ 𝑦 | ||
Theorem | rr-groth 40628* | An equivalent of ax-groth 10239 using only simple defined symbols. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝒫 𝑧 ⊆ 𝑦 ∧ ∀𝑓∃𝑤 ∈ 𝑦 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑦 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))) | ||
Theorem | rr-grothprim 40629* | An equivalent of ax-groth 10239 using only primitives. This uses only 123 symbols, which is significantly less than the previous record of 163 established by grothprim 10250 (which uses some defined symbols, and requires 229 symbols if expanded to primitives). (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ ¬ ∀𝑦(𝑥 ∈ 𝑦 → ¬ ∀𝑧(𝑧 ∈ 𝑦 → ∀𝑓 ¬ ∀𝑤(𝑤 ∈ 𝑦 → ¬ ∀𝑣 ¬ ((∀𝑡(𝑡 ∈ 𝑣 → 𝑡 ∈ 𝑧) → ¬ (𝑣 ∈ 𝑦 → ¬ 𝑣 ∈ 𝑤)) → ¬ ∀𝑖(𝑖 ∈ 𝑧 → (𝑣 ∈ 𝑦 → (𝑖 ∈ 𝑣 → (𝑣 ∈ 𝑓 → ¬ ∀𝑢(𝑢 ∈ 𝑓 → (𝑖 ∈ 𝑢 → ¬ ∀𝑜(𝑜 ∈ 𝑢 → ∀𝑠(𝑠 ∈ 𝑜 → 𝑠 ∈ 𝑤)))))))))))) | ||
Theorem | nanorxor 40630 | 'nand' is equivalent to the equivalence of inclusive and exclusive or. (Contributed by Steve Rodriguez, 28-Feb-2020.) |
⊢ ((𝜑 ⊼ 𝜓) ↔ ((𝜑 ∨ 𝜓) ↔ (𝜑 ⊻ 𝜓))) | ||
Theorem | undisjrab 40631 | Union of two disjoint restricted class abstractions; compare unrab 4274. (Contributed by Steve Rodriguez, 28-Feb-2020.) |
⊢ (({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐴 ∣ 𝜓}) = ∅ ↔ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ⊻ 𝜓)}) | ||
Theorem | iso0 40632 | The empty set is an 𝑅, 𝑆 isomorphism from the empty set to the empty set. (Contributed by Steve Rodriguez, 24-Oct-2015.) |
⊢ ∅ Isom 𝑅, 𝑆 (∅, ∅) | ||
Theorem | ssrecnpr 40633 | ℝ is a subset of both ℝ and ℂ. (Contributed by Steve Rodriguez, 22-Nov-2015.) |
⊢ (𝑆 ∈ {ℝ, ℂ} → ℝ ⊆ 𝑆) | ||
Theorem | seff 40634 | 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 40635 | The infinity ball in the absolute value metric is just the whole space. 𝑆 analogue of blpnf 23001. (Contributed by Steve Rodriguez, 8-Nov-2015.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ 𝐷 = ((abs ∘ − ) ↾ (𝑆 × 𝑆)) ⇒ ⊢ ((𝜑 ∧ 𝑃 ∈ 𝑆) → (𝑃(ball‘𝐷)+∞) = 𝑆) | ||
Theorem | prmunb2 40636* | The primes are unbounded. This generalizes prmunb 16244 to real 𝐴 with arch 11888 and lttrd 10795: every real is less than some positive integer, itself less than some prime. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
⊢ (𝐴 ∈ ℝ → ∃𝑝 ∈ ℙ 𝐴 < 𝑝) | ||
Theorem | dvgrat 40637* | 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 40638* |
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 15233 and dvgrat 40637 directly uses the limit of the ratio.
(It also demonstrates how to use climi2 14862 and absltd 14783 to transform a limit to an inequality cf. https://math.stackexchange.com/q/2215191 14783, and how to use r19.29a 3289 in a similar fashion to Mario Carneiro's proof sketch with rexlimdva 3284 at https://groups.google.com/g/metamath/c/2RPikOiXLMo 3284.) (Contributed by Steve Rodriguez, 28-Feb-2020.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝑊 = (ℤ≥‘𝑁) & ⊢ (𝜑 → 𝑁 ∈ 𝑍) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → (𝐹‘𝑘) ≠ 0) & ⊢ 𝑅 = (𝑘 ∈ 𝑊 ↦ (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘)))) & ⊢ (𝜑 → 𝑅 ⇝ 𝐿) & ⊢ (𝜑 → 𝐿 ≠ 1) ⇒ ⊢ (𝜑 → (𝐿 < 1 ↔ seq𝑀( + , 𝐹) ∈ dom ⇝ )) | ||
Theorem | radcnvrat 40639* | Let 𝐿 be the limit, if one exists, of the ratio (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))) (as in the ratio test cvgdvgrat 40638) 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 40638 —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 40640 | The divides relation is in fact a relation. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
⊢ Rel ∥ | ||
Theorem | nznngen 40641 | 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 40642 | 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 40643 | 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 40644 | Subtract one prime's multiples from an unequal prime's. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℙ) & ⊢ (𝜑 → 𝑁 ∈ ℙ) & ⊢ (𝜑 → 𝑀 ≠ 𝑁) ⇒ ⊢ (𝜑 → (( ∥ “ {𝑀}) ∖ ( ∥ “ {𝑁})) = (( ∥ “ {𝑀}) ∖ ( ∥ “ {(𝑀 · 𝑁)}))) | ||
Theorem | hashnzfz 40645 | Special case of hashdvds 16106: the count of multiples in nℤ restricted to an interval. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐽 ∈ ℤ) & ⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘(𝐽 − 1))) ⇒ ⊢ (𝜑 → (♯‘(( ∥ “ {𝑁}) ∩ (𝐽...𝐾))) = ((⌊‘(𝐾 / 𝑁)) − (⌊‘((𝐽 − 1) / 𝑁)))) | ||
Theorem | hashnzfz2 40646 | Special case of hashnzfz 40645: 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 40647* | As the upper bound 𝐾 of the constraint interval (𝐽...𝐾) in hashnzfz 40645 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 40648* | Transfer a cancellation law like mulcan 11271 to the function operation. (Contributed by Steve Rodriguez, 16-Nov-2015.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑇) & ⊢ (𝜑 → 𝐺:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐻:𝐴⟶𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑇 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝑅𝑦) = (𝑥𝑅𝑧) ↔ 𝑦 = 𝑧)) ⇒ ⊢ (𝜑 → ((𝐹 ∘f 𝑅𝐺) = (𝐹 ∘f 𝑅𝐻) ↔ 𝐺 = 𝐻)) | ||
Theorem | ofsubid 40649 | Function analogue of subid 10899. (Contributed by Steve Rodriguez, 5-Nov-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ) → (𝐹 ∘f − 𝐹) = (𝐴 × {0})) | ||
Theorem | ofmul12 40650 | Function analogue of mul12 10799. (Contributed by Steve Rodriguez, 13-Nov-2015.) |
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐺:𝐴⟶ℂ ∧ 𝐻:𝐴⟶ℂ)) → (𝐹 ∘f · (𝐺 ∘f · 𝐻)) = (𝐺 ∘f · (𝐹 ∘f · 𝐻))) | ||
Theorem | ofdivrec 40651 | Function analogue of divrec 11308, a division analogue of ofnegsub 11630. (Contributed by Steve Rodriguez, 3-Nov-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ ∧ 𝐺:𝐴⟶(ℂ ∖ {0})) → (𝐹 ∘f · ((𝐴 × {1}) ∘f / 𝐺)) = (𝐹 ∘f / 𝐺)) | ||
Theorem | ofdivcan4 40652 | Function analogue of divcan4 11319. (Contributed by Steve Rodriguez, 4-Nov-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ ∧ 𝐺:𝐴⟶(ℂ ∖ {0})) → ((𝐹 ∘f · 𝐺) ∘f / 𝐺) = 𝐹) | ||
Theorem | ofdivdiv2 40653 | Function analogue of divdiv2 11346. (Contributed by Steve Rodriguez, 23-Nov-2015.) |
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐺:𝐴⟶(ℂ ∖ {0}) ∧ 𝐻:𝐴⟶(ℂ ∖ {0}))) → (𝐹 ∘f / (𝐺 ∘f / 𝐻)) = ((𝐹 ∘f · 𝐻) ∘f / 𝐺)) | ||
Theorem | lhe4.4ex1a 40654 | Example of the Fundamental Theorem of Calculus, part two (ftc2 24635): ∫(1(,)2)((𝑥↑2) − 3) d𝑥 = -(2 / 3). Section 4.4 example 1a of [LarsonHostetlerEdwards] p. 311. (The book teaches ftc2 24635 as simply the "Fundamental Theorem of Calculus", then ftc1 24633 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 40655 | 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 40656 | Derivative of the identity function on the real or complex numbers. (Contributed by Steve Rodriguez, 11-Nov-2015.) |
⊢ (𝑆 ∈ {ℝ, ℂ} → (𝑆 D ( I ↾ 𝑆)) = (𝑆 × {1})) | ||
Theorem | dvsef 40657 | Derivative of the exponential function on the real or complex numbers. (Contributed by Steve Rodriguez, 12-Nov-2015.) |
⊢ (𝑆 ∈ {ℝ, ℂ} → (𝑆 D (exp ↾ 𝑆)) = (exp ↾ 𝑆)) | ||
Theorem | expgrowthi 40658* | Exponential growth and decay model. See expgrowth 40660 for more information. (Contributed by Steve Rodriguez, 4-Nov-2015.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝐾 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ 𝑌 = (𝑡 ∈ 𝑆 ↦ (𝐶 · (exp‘(𝐾 · 𝑡)))) ⇒ ⊢ (𝜑 → (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) | ||
Theorem | dvconstbi 40659* | The derivative of a function on 𝑆 is zero iff it is a constant function. Roughly a biconditional 𝑆 analogue of dvconst 24508 and dveq0 24591. 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 40660* |
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 40658 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 40658); 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 40658 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 40658. Statements for this and expgrowthi 40658 formulated by Mario Carneiro. (Contributed by Steve Rodriguez, 24-Nov-2015.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝐾 ∈ ℂ) & ⊢ (𝜑 → 𝑌:𝑆⟶ℂ) & ⊢ (𝜑 → dom (𝑆 D 𝑌) = 𝑆) ⇒ ⊢ (𝜑 → ((𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌) ↔ ∃𝑐 ∈ ℂ 𝑌 = (𝑡 ∈ 𝑆 ↦ (𝑐 · (exp‘(𝐾 · 𝑡)))))) | ||
Syntax | cbcc 40661 | Extend class notation to include the generalized binomial coefficient operation. |
class C𝑐 | ||
Definition | df-bcc 40662* | Define a generalized binomial coefficient operation, which unlike df-bc 13657 allows complex numbers for the first argument. (Contributed by Steve Rodriguez, 22-Apr-2020.) |
⊢ C𝑐 = (𝑐 ∈ ℂ, 𝑘 ∈ ℕ0 ↦ ((𝑐 FallFac 𝑘) / (!‘𝑘))) | ||
Theorem | bccval 40663 | Value of the generalized binomial coefficient, 𝐶 choose 𝐾. (Contributed by Steve Rodriguez, 22-Apr-2020.) |
⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐾 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝐶C𝑐𝐾) = ((𝐶 FallFac 𝐾) / (!‘𝐾))) | ||
Theorem | bcccl 40664 | Closure of the generalized binomial coefficient. (Contributed by Steve Rodriguez, 22-Apr-2020.) |
⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐾 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝐶C𝑐𝐾) ∈ ℂ) | ||
Theorem | bcc0 40665 | 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 40666 | Generalized binomial coefficient: 𝐶 choose (𝐾 + 1). (Contributed by Steve Rodriguez, 22-Apr-2020.) |
⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐾 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝐶C𝑐(𝐾 + 1)) = ((𝐶C𝑐𝐾) · ((𝐶 − 𝐾) / (𝐾 + 1)))) | ||
Theorem | bccm1k 40667 | Generalized binomial coefficient: 𝐶 choose (𝐾 − 1), when 𝐶 is not (𝐾 − 1). (Contributed by Steve Rodriguez, 22-Apr-2020.) |
⊢ (𝜑 → 𝐶 ∈ (ℂ ∖ {(𝐾 − 1)})) & ⊢ (𝜑 → 𝐾 ∈ ℕ) ⇒ ⊢ (𝜑 → (𝐶C𝑐(𝐾 − 1)) = ((𝐶C𝑐𝐾) / ((𝐶 − (𝐾 − 1)) / 𝐾))) | ||
Theorem | bccn0 40668 | Generalized binomial coefficient: 𝐶 choose 0. (Contributed by Steve Rodriguez, 22-Apr-2020.) |
⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐶C𝑐0) = 1) | ||
Theorem | bccn1 40669 | Generalized binomial coefficient: 𝐶 choose 1. (Contributed by Steve Rodriguez, 22-Apr-2020.) |
⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐶C𝑐1) = 𝐶) | ||
Theorem | bccbc 40670 | 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 40671* | 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 40672* | 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 25003 uses a shifted version of 𝐻 to match the sum form of (ℂ D 𝐹) in pserdv2 25012 (and shows how to use uzmptshftfval 40671 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 40673 | Lemma for binomcxp 40682. The lemma in the Wikibooks proof. (Contributed by Steve Rodriguez, 22-Apr-2020.) |
⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐾 ∈ ℕ) ⇒ ⊢ (𝜑 → (((𝐶 − 𝐾) · (𝐶C𝑐𝐾)) + ((𝐶 − (𝐾 − 1)) · (𝐶C𝑐(𝐾 − 1)))) = (𝐶 · (𝐶C𝑐𝐾))) | ||
Theorem | binomcxplemnn0 40674* | Lemma for binomcxp 40682. When 𝐶 is a nonnegative integer, the binomial's finite sum value by the standard binomial theorem binom 15179 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 40675* | Lemma for binomcxp 40682. 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 40676* | Lemma for binomcxp 40682. binomcxplemrat 40675 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 40677* | Lemma for binomcxp 40682. By binomcxplemfrat 40676 and radcnvrat 40639 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 40678* | Lemma for binomcxp 40682. 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 40680 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 40679* | Lemma for binomcxp 40682. The sum in binomcxplemnn0 40674 and its derivative (see the next theorem, binomcxplemdvsum 40680) 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 40680* | Lemma for binomcxp 40682. The derivative of the generalized sum in binomcxplemnn0 40674. 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[,)𝑅)) & ⊢ 𝑃 = (𝑏 ∈ 𝐷 ↦ Σ𝑘 ∈ ℕ0 ((𝑆‘𝑏)‘𝑘)) ⇒ ⊢ (𝜑 → (ℂ D 𝑃) = (𝑏 ∈ 𝐷 ↦ Σ𝑘 ∈ ℕ ((𝐸‘𝑏)‘𝑘))) | ||
Theorem | binomcxplemnotnn0 40681* |
Lemma for binomcxp 40682. When 𝐶 is not a nonnegative integer, the
generalized sum in binomcxplemnn0 40674 —which we will call 𝑃
—is a convergent power series: its base 𝑏 is always of
smaller absolute value than the radius of convergence.
pserdv2 25012 gives the derivative of 𝑃, which by dvradcnv 25003 also converges in that radius. When 𝐴 is fixed at one, (𝐴 + 𝑏) times that derivative equals (𝐶 · 𝑃) and fraction (𝑃 / ((𝐴 + 𝑏)↑𝑐𝐶)) is always defined with derivative zero, so the fraction is a constant—specifically one, because ((1 + 0)↑𝑐𝐶) = 1. Thus ((1 + 𝑏)↑𝑐𝐶) = (𝑃‘𝑏). Finally, let 𝑏 be (𝐵 / 𝐴), and multiply both the binomial ((1 + (𝐵 / 𝐴))↑𝑐𝐶) and the sum (𝑃‘(𝐵 / 𝐴)) by (𝐴↑𝑐𝐶) to get the result. (Contributed by Steve Rodriguez, 22-Apr-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (abs‘𝐵) < (abs‘𝐴)) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ 𝐹 = (𝑗 ∈ ℕ0 ↦ (𝐶C𝑐𝑗)) & ⊢ 𝑆 = (𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘)))) & ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑆‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) & ⊢ 𝐸 = (𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ ↦ ((𝑘 · (𝐹‘𝑘)) · (𝑏↑(𝑘 − 1))))) & ⊢ 𝐷 = (◡abs “ (0[,)𝑅)) & ⊢ 𝑃 = (𝑏 ∈ 𝐷 ↦ Σ𝑘 ∈ ℕ0 ((𝑆‘𝑏)‘𝑘)) ⇒ ⊢ ((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) → ((𝐴 + 𝐵)↑𝑐𝐶) = Σ𝑘 ∈ ℕ0 ((𝐶C𝑐𝑘) · ((𝐴↑𝑐(𝐶 − 𝑘)) · (𝐵↑𝑘)))) | ||
Theorem | binomcxp 40682* | Generalize the binomial theorem binom 15179 to positive real summand 𝐴, real summand 𝐵, and complex exponent 𝐶. Proof in https://en.wikibooks.org/wiki/Advanced_Calculus 15179; see also https://en.wikipedia.org/wiki/Binomial_series 15179, https://en.wikipedia.org/wiki/Binomial_theorem 15179 (sections "Newton's generalized binomial theorem" and "Future generalizations"), and proof "General Binomial Theorem" in https://proofwiki.org/wiki/Binomial_Theorem 15179. (Contributed by Steve Rodriguez, 22-Apr-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (abs‘𝐵) < (abs‘𝐴)) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐵)↑𝑐𝐶) = Σ𝑘 ∈ ℕ0 ((𝐶C𝑐𝑘) · ((𝐴↑𝑐(𝐶 − 𝑘)) · (𝐵↑𝑘)))) | ||
Theorem | pm10.12 40683* | Theorem *10.12 in [WhiteheadRussell] p. 146. In *10, this is treated as an axiom, and the proofs in *10 are based on this theorem. (Contributed by Andrew Salmon, 17-Jun-2011.) |
⊢ (∀𝑥(𝜑 ∨ 𝜓) → (𝜑 ∨ ∀𝑥𝜓)) | ||
Theorem | pm10.14 40684 | Theorem *10.14 in [WhiteheadRussell] p. 146. (Contributed by Andrew Salmon, 17-Jun-2011.) |
⊢ ((∀𝑥𝜑 ∧ ∀𝑥𝜓) → ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓)) | ||
Theorem | pm10.251 40685 | Theorem *10.251 in [WhiteheadRussell] p. 149. (Contributed by Andrew Salmon, 17-Jun-2011.) |
⊢ (∀𝑥 ¬ 𝜑 → ¬ ∀𝑥𝜑) | ||
Theorem | pm10.252 40686 | Theorem *10.252 in [WhiteheadRussell] p. 149. (Contributed by Andrew Salmon, 17-Jun-2011.) (New usage is discouraged.) |
⊢ (¬ ∃𝑥𝜑 ↔ ∀𝑥 ¬ 𝜑) | ||
Theorem | pm10.253 40687 | Theorem *10.253 in [WhiteheadRussell] p. 149. (Contributed by Andrew Salmon, 17-Jun-2011.) |
⊢ (¬ ∀𝑥𝜑 ↔ ∃𝑥 ¬ 𝜑) | ||
Theorem | albitr 40688 | Theorem *10.301 in [WhiteheadRussell] p. 151. (Contributed by Andrew Salmon, 24-May-2011.) |
⊢ ((∀𝑥(𝜑 ↔ 𝜓) ∧ ∀𝑥(𝜓 ↔ 𝜒)) → ∀𝑥(𝜑 ↔ 𝜒)) | ||
Theorem | pm10.42 40689 | Theorem *10.42 in [WhiteheadRussell] p. 155. (Contributed by Andrew Salmon, 17-Jun-2011.) |
⊢ ((∃𝑥𝜑 ∨ ∃𝑥𝜓) ↔ ∃𝑥(𝜑 ∨ 𝜓)) | ||
Theorem | pm10.52 40690* | Theorem *10.52 in [WhiteheadRussell] p. 155. (Contributed by Andrew Salmon, 24-May-2011.) |
⊢ (∃𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) ↔ 𝜓)) | ||
Theorem | pm10.53 40691 | Theorem *10.53 in [WhiteheadRussell] p. 155. (Contributed by Andrew Salmon, 24-May-2011.) |
⊢ (¬ ∃𝑥𝜑 → ∀𝑥(𝜑 → 𝜓)) | ||
Theorem | pm10.541 40692* | Theorem *10.541 in [WhiteheadRussell] p. 155. (Contributed by Andrew Salmon, 24-May-2011.) |
⊢ (∀𝑥(𝜑 → (𝜒 ∨ 𝜓)) ↔ (𝜒 ∨ ∀𝑥(𝜑 → 𝜓))) | ||
Theorem | pm10.542 40693* | Theorem *10.542 in [WhiteheadRussell] p. 156. (Contributed by Andrew Salmon, 24-May-2011.) |
⊢ (∀𝑥(𝜑 → (𝜒 → 𝜓)) ↔ (𝜒 → ∀𝑥(𝜑 → 𝜓))) | ||
Theorem | pm10.55 40694 | Theorem *10.55 in [WhiteheadRussell] p. 156. (Contributed by Andrew Salmon, 24-May-2011.) |
⊢ ((∃𝑥(𝜑 ∧ 𝜓) ∧ ∀𝑥(𝜑 → 𝜓)) ↔ (∃𝑥𝜑 ∧ ∀𝑥(𝜑 → 𝜓))) | ||
Theorem | pm10.56 40695 | Theorem *10.56 in [WhiteheadRussell] p. 156. (Contributed by Andrew Salmon, 24-May-2011.) |
⊢ ((∀𝑥(𝜑 → 𝜓) ∧ ∃𝑥(𝜑 ∧ 𝜒)) → ∃𝑥(𝜓 ∧ 𝜒)) | ||
Theorem | pm10.57 40696 | Theorem *10.57 in [WhiteheadRussell] p. 156. (Contributed by Andrew Salmon, 24-May-2011.) |
⊢ (∀𝑥(𝜑 → (𝜓 ∨ 𝜒)) → (∀𝑥(𝜑 → 𝜓) ∨ ∃𝑥(𝜑 ∧ 𝜒))) | ||
Theorem | 2alanimi 40697 | Removes two universal quantifiers from a statement. (Contributed by Andrew Salmon, 24-May-2011.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ ((∀𝑥∀𝑦𝜑 ∧ ∀𝑥∀𝑦𝜓) → ∀𝑥∀𝑦𝜒) | ||
Theorem | 2al2imi 40698 | Removes two universal quantifiers from a statement. (Contributed by Andrew Salmon, 24-May-2011.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (∀𝑥∀𝑦𝜑 → (∀𝑥∀𝑦𝜓 → ∀𝑥∀𝑦𝜒)) | ||
Theorem | pm11.11 40699 | Theorem *11.11 in [WhiteheadRussell] p. 159. (Contributed by Andrew Salmon, 17-Jun-2011.) |
⊢ 𝜑 ⇒ ⊢ ∀𝑧∀𝑤[𝑧 / 𝑥][𝑤 / 𝑦]𝜑 | ||
Theorem | pm11.12 40700* | Theorem *11.12 in [WhiteheadRussell] p. 159. (Contributed by Andrew Salmon, 17-Jun-2011.) |
⊢ (∀𝑥∀𝑦(𝜑 ∨ 𝜓) → (𝜑 ∨ ∀𝑥∀𝑦𝜓)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |