Most Recent Proofs
|
|
Intuitionistic Logic Explorer Most Recent Proofs |
|
| Mirrors > Home > ILE Home > Th. List > Recent | MPE Most Recent Other > MM 100 | |
See the MPE Most Recent Proofs page for news and some useful links.
| Color key: |
Intuitionistic Logic Explorer |
 User Mathboxes |
| Date | Label | Description |
|---|---|---|
| Theorem | ||
| 26-Aug-2020 | sqrt0rlem 9192 | Lemma for sqrt0 9193. (Contributed by Jim Kingdon, 26-Aug-2020.) |
| ⊢ ((A ∈ ℝ ∧ ((A↑2) = 0 ∧ 0 ≤ A)) ↔ A = 0) | ||
| 23-Aug-2020 | sqrtrval 9189 | Value of square root function. (Contributed by Jim Kingdon, 23-Aug-2020.) |
| ⊢ (A ∈ ℝ → (√‘A) = (℩x ∈ ℝ ((x↑2) = A ∧ 0 ≤ x))) | ||
| 23-Aug-2020 | df-rsqrt 9187 |
Define a function whose value is the square root of a nonnegative real
number.
Defining the square root for complex numbers has one difficult part: choosing between the two roots. The usual way to define a principal square root for all complex numbers relies on excluded middle or something similar. But in the case of a nonnegative real number, we don't have the complications presented for general complex numbers, and we can choose the nonnegative root. (Contributed by Jim Kingdon, 23-Aug-2020.) |
| ⊢ √ = (x ∈ ℝ ↦ (℩y ∈ ℝ ((y↑2) = x ∧ 0 ≤ y))) | ||
| 19-Aug-2020 | addnqpr 6541 | Addition of fractions embedded into positive reals. One can either add the fractions as fractions, or embed them into positive reals and add them as positive reals, and get the same result. (Contributed by Jim Kingdon, 19-Aug-2020.) |
| ⊢ ((A ∈ Q ∧ B ∈ Q) → ⟨{𝑙 ∣ 𝑙 <Q (A +Q B)}, {u ∣ (A +Q B) <Q u}⟩ = (⟨{𝑙 ∣ 𝑙 <Q A}, {u ∣ A <Q u}⟩ +P ⟨{𝑙 ∣ 𝑙 <Q B}, {u ∣ B <Q u}⟩)) | ||
| 19-Aug-2020 | addnqprlemfu 6540 | Lemma for addnqpr 6541. The forward subset relationship for the upper cut. (Contributed by Jim Kingdon, 19-Aug-2020.) |
| ⊢ ((A ∈ Q ∧ B ∈ Q) → (2nd ‘⟨{𝑙 ∣ 𝑙 <Q (A +Q B)}, {u ∣ (A +Q B) <Q u}⟩) ⊆ (2nd ‘(⟨{𝑙 ∣ 𝑙 <Q A}, {u ∣ A <Q u}⟩ +P ⟨{𝑙 ∣ 𝑙 <Q B}, {u ∣ B <Q u}⟩))) | ||
| 19-Aug-2020 | addnqprlemfl 6539 | Lemma for addnqpr 6541. The forward subset relationship for the lower cut. (Contributed by Jim Kingdon, 19-Aug-2020.) |
| ⊢ ((A ∈ Q ∧ B ∈ Q) → (1st ‘⟨{𝑙 ∣ 𝑙 <Q (A +Q B)}, {u ∣ (A +Q B) <Q u}⟩) ⊆ (1st ‘(⟨{𝑙 ∣ 𝑙 <Q A}, {u ∣ A <Q u}⟩ +P ⟨{𝑙 ∣ 𝑙 <Q B}, {u ∣ B <Q u}⟩))) | ||
| 19-Aug-2020 | addnqprlemru 6538 | Lemma for addnqpr 6541. The reverse subset relationship for the upper cut. (Contributed by Jim Kingdon, 19-Aug-2020.) |
| ⊢ ((A ∈ Q ∧ B ∈ Q) → (2nd ‘(⟨{𝑙 ∣ 𝑙 <Q A}, {u ∣ A <Q u}⟩ +P ⟨{𝑙 ∣ 𝑙 <Q B}, {u ∣ B <Q u}⟩)) ⊆ (2nd ‘⟨{𝑙 ∣ 𝑙 <Q (A +Q B)}, {u ∣ (A +Q B) <Q u}⟩)) | ||
| 19-Aug-2020 | addnqprlemrl 6537 | Lemma for addnqpr 6541. The reverse subset relationship for the lower cut. (Contributed by Jim Kingdon, 19-Aug-2020.) |
| ⊢ ((A ∈ Q ∧ B ∈ Q) → (1st ‘(⟨{𝑙 ∣ 𝑙 <Q A}, {u ∣ A <Q u}⟩ +P ⟨{𝑙 ∣ 𝑙 <Q B}, {u ∣ B <Q u}⟩)) ⊆ (1st ‘⟨{𝑙 ∣ 𝑙 <Q (A +Q B)}, {u ∣ (A +Q B) <Q u}⟩)) | ||
| 15-Aug-2020 | cauappcvgprlemcan 6615 | Lemma for cauappcvgprlemladdrl 6628. Cancelling a term from both sides. (Contributed by Jim Kingdon, 15-Aug-2020.) |
| ⊢ (φ → 𝐿 ∈ P) & ⊢ (φ → 𝑆 ∈ Q) & ⊢ (φ → 𝑅 ∈ Q) & ⊢ (φ → 𝑄 ∈ Q) ⇒ ⊢ (φ → ((𝑅 +Q 𝑄) ∈ (1st ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q (𝑆 +Q 𝑄)}, {u ∣ (𝑆 +Q 𝑄) <Q u}⟩)) ↔ 𝑅 ∈ (1st ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}⟩)))) | ||
| 4-Aug-2020 | cauappcvgprlemupu 6620 | Lemma for cauappcvgpr 6633. The upper cut of the putative limit is upper. (Contributed by Jim Kingdon, 4-Aug-2020.) |
| ⊢ (φ → 𝐹:Q⟶Q) & ⊢ (φ → ∀𝑝 ∈ Q ∀𝑞 ∈ Q ((𝐹‘𝑝) <Q ((𝐹‘𝑞) +Q (𝑝 +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘𝑝) +Q (𝑝 +Q 𝑞)))) & ⊢ (φ → ∀𝑝 ∈ Q A <Q (𝐹‘𝑝)) & ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q (𝐹‘𝑞)}, {u ∈ Q ∣ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q u}⟩ ⇒ ⊢ ((φ ∧ 𝑠 <Q 𝑟 ∧ 𝑠 ∈ (2nd ‘𝐿)) → 𝑟 ∈ (2nd ‘𝐿)) | ||
| 4-Aug-2020 | cauappcvgprlemopu 6619 | Lemma for cauappcvgpr 6633. The upper cut of the putative limit is open. (Contributed by Jim Kingdon, 4-Aug-2020.) |
| ⊢ (φ → 𝐹:Q⟶Q) & ⊢ (φ → ∀𝑝 ∈ Q ∀𝑞 ∈ Q ((𝐹‘𝑝) <Q ((𝐹‘𝑞) +Q (𝑝 +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘𝑝) +Q (𝑝 +Q 𝑞)))) & ⊢ (φ → ∀𝑝 ∈ Q A <Q (𝐹‘𝑝)) & ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q (𝐹‘𝑞)}, {u ∈ Q ∣ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q u}⟩ ⇒ ⊢ ((φ ∧ 𝑟 ∈ (2nd ‘𝐿)) → ∃𝑠 ∈ Q (𝑠 <Q 𝑟 ∧ 𝑠 ∈ (2nd ‘𝐿))) | ||
| 4-Aug-2020 | cauappcvgprlemlol 6618 | Lemma for cauappcvgpr 6633. The lower cut of the putative limit is lower. (Contributed by Jim Kingdon, 4-Aug-2020.) |
| ⊢ (φ → 𝐹:Q⟶Q) & ⊢ (φ → ∀𝑝 ∈ Q ∀𝑞 ∈ Q ((𝐹‘𝑝) <Q ((𝐹‘𝑞) +Q (𝑝 +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘𝑝) +Q (𝑝 +Q 𝑞)))) & ⊢ (φ → ∀𝑝 ∈ Q A <Q (𝐹‘𝑝)) & ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q (𝐹‘𝑞)}, {u ∈ Q ∣ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q u}⟩ ⇒ ⊢ ((φ ∧ 𝑠 <Q 𝑟 ∧ 𝑟 ∈ (1st ‘𝐿)) → 𝑠 ∈ (1st ‘𝐿)) | ||
| 4-Aug-2020 | cauappcvgprlemopl 6617 | Lemma for cauappcvgpr 6633. The lower cut of the putative limit is open. (Contributed by Jim Kingdon, 4-Aug-2020.) |
| ⊢ (φ → 𝐹:Q⟶Q) & ⊢ (φ → ∀𝑝 ∈ Q ∀𝑞 ∈ Q ((𝐹‘𝑝) <Q ((𝐹‘𝑞) +Q (𝑝 +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘𝑝) +Q (𝑝 +Q 𝑞)))) & ⊢ (φ → ∀𝑝 ∈ Q A <Q (𝐹‘𝑝)) & ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q (𝐹‘𝑞)}, {u ∈ Q ∣ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q u}⟩ ⇒ ⊢ ((φ ∧ 𝑠 ∈ (1st ‘𝐿)) → ∃𝑟 ∈ Q (𝑠 <Q 𝑟 ∧ 𝑟 ∈ (1st ‘𝐿))) | ||
| 18-Jul-2020 | cauappcvgprlemloc 6623 | Lemma for cauappcvgpr 6633. The putative limit is located. (Contributed by Jim Kingdon, 18-Jul-2020.) |
| ⊢ (φ → 𝐹:Q⟶Q) & ⊢ (φ → ∀𝑝 ∈ Q ∀𝑞 ∈ Q ((𝐹‘𝑝) <Q ((𝐹‘𝑞) +Q (𝑝 +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘𝑝) +Q (𝑝 +Q 𝑞)))) & ⊢ (φ → ∀𝑝 ∈ Q A <Q (𝐹‘𝑝)) & ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q (𝐹‘𝑞)}, {u ∈ Q ∣ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q u}⟩ ⇒ ⊢ (φ → ∀𝑠 ∈ Q ∀𝑟 ∈ Q (𝑠 <Q 𝑟 → (𝑠 ∈ (1st ‘𝐿) ∨ 𝑟 ∈ (2nd ‘𝐿)))) | ||
| 18-Jul-2020 | cauappcvgprlemdisj 6622 | Lemma for cauappcvgpr 6633. The putative limit is disjoint. (Contributed by Jim Kingdon, 18-Jul-2020.) |
| ⊢ (φ → 𝐹:Q⟶Q) & ⊢ (φ → ∀𝑝 ∈ Q ∀𝑞 ∈ Q ((𝐹‘𝑝) <Q ((𝐹‘𝑞) +Q (𝑝 +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘𝑝) +Q (𝑝 +Q 𝑞)))) & ⊢ (φ → ∀𝑝 ∈ Q A <Q (𝐹‘𝑝)) & ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q (𝐹‘𝑞)}, {u ∈ Q ∣ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q u}⟩ ⇒ ⊢ (φ → ∀𝑠 ∈ Q ¬ (𝑠 ∈ (1st ‘𝐿) ∧ 𝑠 ∈ (2nd ‘𝐿))) | ||
| 18-Jul-2020 | cauappcvgprlemrnd 6621 | Lemma for cauappcvgpr 6633. The putative limit is rounded. (Contributed by Jim Kingdon, 18-Jul-2020.) |
| ⊢ (φ → 𝐹:Q⟶Q) & ⊢ (φ → ∀𝑝 ∈ Q ∀𝑞 ∈ Q ((𝐹‘𝑝) <Q ((𝐹‘𝑞) +Q (𝑝 +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘𝑝) +Q (𝑝 +Q 𝑞)))) & ⊢ (φ → ∀𝑝 ∈ Q A <Q (𝐹‘𝑝)) & ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q (𝐹‘𝑞)}, {u ∈ Q ∣ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q u}⟩ ⇒ ⊢ (φ → (∀𝑠 ∈ Q (𝑠 ∈ (1st ‘𝐿) ↔ ∃𝑟 ∈ Q (𝑠 <Q 𝑟 ∧ 𝑟 ∈ (1st ‘𝐿))) ∧ ∀𝑟 ∈ Q (𝑟 ∈ (2nd ‘𝐿) ↔ ∃𝑠 ∈ Q (𝑠 <Q 𝑟 ∧ 𝑠 ∈ (2nd ‘𝐿))))) | ||
| 18-Jul-2020 | cauappcvgprlemm 6616 | Lemma for cauappcvgpr 6633. The putative limit is inhabited. (Contributed by Jim Kingdon, 18-Jul-2020.) |
| ⊢ (φ → 𝐹:Q⟶Q) & ⊢ (φ → ∀𝑝 ∈ Q ∀𝑞 ∈ Q ((𝐹‘𝑝) <Q ((𝐹‘𝑞) +Q (𝑝 +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘𝑝) +Q (𝑝 +Q 𝑞)))) & ⊢ (φ → ∀𝑝 ∈ Q A <Q (𝐹‘𝑝)) & ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q (𝐹‘𝑞)}, {u ∈ Q ∣ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q u}⟩ ⇒ ⊢ (φ → (∃𝑠 ∈ Q 𝑠 ∈ (1st ‘𝐿) ∧ ∃𝑟 ∈ Q 𝑟 ∈ (2nd ‘𝐿))) | ||
| 11-Jul-2020 | cauappcvgprlemladdrl 6628 | Lemma for cauappcvgprlemladd 6629. The forward subset relationship for the lower cut. (Contributed by Jim Kingdon, 11-Jul-2020.) |
| ⊢ (φ → 𝐹:Q⟶Q) & ⊢ (φ → ∀𝑝 ∈ Q ∀𝑞 ∈ Q ((𝐹‘𝑝) <Q ((𝐹‘𝑞) +Q (𝑝 +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘𝑝) +Q (𝑝 +Q 𝑞)))) & ⊢ (φ → ∀𝑝 ∈ Q A <Q (𝐹‘𝑝)) & ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q (𝐹‘𝑞)}, {u ∈ Q ∣ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q u}⟩ & ⊢ (φ → 𝑆 ∈ Q) ⇒ ⊢ (φ → (1st ‘⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q ((𝐹‘𝑞) +Q 𝑆)}, {u ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q u}⟩) ⊆ (1st ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}⟩))) | ||
| 11-Jul-2020 | cauappcvgprlemladdru 6627 | Lemma for cauappcvgprlemladd 6629. The reverse subset relationship for the upper cut. (Contributed by Jim Kingdon, 11-Jul-2020.) |
| ⊢ (φ → 𝐹:Q⟶Q) & ⊢ (φ → ∀𝑝 ∈ Q ∀𝑞 ∈ Q ((𝐹‘𝑝) <Q ((𝐹‘𝑞) +Q (𝑝 +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘𝑝) +Q (𝑝 +Q 𝑞)))) & ⊢ (φ → ∀𝑝 ∈ Q A <Q (𝐹‘𝑝)) & ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q (𝐹‘𝑞)}, {u ∈ Q ∣ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q u}⟩ & ⊢ (φ → 𝑆 ∈ Q) ⇒ ⊢ (φ → (2nd ‘⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q ((𝐹‘𝑞) +Q 𝑆)}, {u ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q u}⟩) ⊆ (2nd ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}⟩))) | ||
| 11-Jul-2020 | cauappcvgprlemladdfl 6626 | Lemma for cauappcvgprlemladd 6629. The forward subset relationship for the lower cut. (Contributed by Jim Kingdon, 11-Jul-2020.) |
| ⊢ (φ → 𝐹:Q⟶Q) & ⊢ (φ → ∀𝑝 ∈ Q ∀𝑞 ∈ Q ((𝐹‘𝑝) <Q ((𝐹‘𝑞) +Q (𝑝 +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘𝑝) +Q (𝑝 +Q 𝑞)))) & ⊢ (φ → ∀𝑝 ∈ Q A <Q (𝐹‘𝑝)) & ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q (𝐹‘𝑞)}, {u ∈ Q ∣ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q u}⟩ & ⊢ (φ → 𝑆 ∈ Q) ⇒ ⊢ (φ → (1st ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}⟩)) ⊆ (1st ‘⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q ((𝐹‘𝑞) +Q 𝑆)}, {u ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q u}⟩)) | ||
| 11-Jul-2020 | cauappcvgprlemladdfu 6625 | Lemma for cauappcvgprlemladd 6629. The forward subset relationship for the upper cut. (Contributed by Jim Kingdon, 11-Jul-2020.) |
| ⊢ (φ → 𝐹:Q⟶Q) & ⊢ (φ → ∀𝑝 ∈ Q ∀𝑞 ∈ Q ((𝐹‘𝑝) <Q ((𝐹‘𝑞) +Q (𝑝 +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘𝑝) +Q (𝑝 +Q 𝑞)))) & ⊢ (φ → ∀𝑝 ∈ Q A <Q (𝐹‘𝑝)) & ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q (𝐹‘𝑞)}, {u ∈ Q ∣ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q u}⟩ & ⊢ (φ → 𝑆 ∈ Q) ⇒ ⊢ (φ → (2nd ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}⟩)) ⊆ (2nd ‘⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q ((𝐹‘𝑞) +Q 𝑆)}, {u ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q u}⟩)) | ||
| 8-Jul-2020 | nqprl 6532 | Comparing a fraction to a real can be done by whether it is an element of the lower cut, or by <P. (Contributed by Jim Kingdon, 8-Jul-2020.) |
| ⊢ ((A ∈ Q ∧ B ∈ P) → (A ∈ (1st ‘B) ↔ ⟨{𝑙 ∣ 𝑙 <Q A}, {u ∣ A <Q u}⟩<P B)) | ||
| 24-Jun-2020 | nqprlu 6529 | The canonical embedding of the rationals into the reals. (Contributed by Jim Kingdon, 24-Jun-2020.) |
| ⊢ (A ∈ Q → ⟨{𝑙 ∣ 𝑙 <Q A}, {u ∣ A <Q u}⟩ ∈ P) | ||
| 23-Jun-2020 | cauappcvgprlem2 6631 | Lemma for cauappcvgpr 6633. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 23-Jun-2020.) |
| ⊢ (φ → 𝐹:Q⟶Q) & ⊢ (φ → ∀𝑝 ∈ Q ∀𝑞 ∈ Q ((𝐹‘𝑝) <Q ((𝐹‘𝑞) +Q (𝑝 +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘𝑝) +Q (𝑝 +Q 𝑞)))) & ⊢ (φ → ∀𝑝 ∈ Q A <Q (𝐹‘𝑝)) & ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q (𝐹‘𝑞)}, {u ∈ Q ∣ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q u}⟩ & ⊢ (φ → 𝑄 ∈ Q) & ⊢ (φ → 𝑅 ∈ Q) ⇒ ⊢ (φ → 𝐿<P ⟨{𝑙 ∣ 𝑙 <Q ((𝐹‘𝑄) +Q (𝑄 +Q 𝑅))}, {u ∣ ((𝐹‘𝑄) +Q (𝑄 +Q 𝑅)) <Q u}⟩) | ||
| 23-Jun-2020 | cauappcvgprlem1 6630 | Lemma for cauappcvgpr 6633. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 23-Jun-2020.) |
| ⊢ (φ → 𝐹:Q⟶Q) & ⊢ (φ → ∀𝑝 ∈ Q ∀𝑞 ∈ Q ((𝐹‘𝑝) <Q ((𝐹‘𝑞) +Q (𝑝 +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘𝑝) +Q (𝑝 +Q 𝑞)))) & ⊢ (φ → ∀𝑝 ∈ Q A <Q (𝐹‘𝑝)) & ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q (𝐹‘𝑞)}, {u ∈ Q ∣ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q u}⟩ & ⊢ (φ → 𝑄 ∈ Q) & ⊢ (φ → 𝑅 ∈ Q) ⇒ ⊢ (φ → ⟨{𝑙 ∣ 𝑙 <Q (𝐹‘𝑄)}, {u ∣ (𝐹‘𝑄) <Q u}⟩<P (𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q (𝑄 +Q 𝑅)}, {u ∣ (𝑄 +Q 𝑅) <Q u}⟩)) | ||
| 23-Jun-2020 | cauappcvgprlemladd 6629 | Lemma for cauappcvgpr 6633. This takes 𝐿 and offsets it by the positive fraction 𝑆. (Contributed by Jim Kingdon, 23-Jun-2020.) |
| ⊢ (φ → 𝐹:Q⟶Q) & ⊢ (φ → ∀𝑝 ∈ Q ∀𝑞 ∈ Q ((𝐹‘𝑝) <Q ((𝐹‘𝑞) +Q (𝑝 +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘𝑝) +Q (𝑝 +Q 𝑞)))) & ⊢ (φ → ∀𝑝 ∈ Q A <Q (𝐹‘𝑝)) & ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q (𝐹‘𝑞)}, {u ∈ Q ∣ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q u}⟩ & ⊢ (φ → 𝑆 ∈ Q) ⇒ ⊢ (φ → (𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}⟩) = ⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q ((𝐹‘𝑞) +Q 𝑆)}, {u ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q u}⟩) | ||
| 20-Jun-2020 | cauappcvgprlemlim 6632 | Lemma for cauappcvgpr 6633. The putative limit is a limit. (Contributed by Jim Kingdon, 20-Jun-2020.) |
| ⊢ (φ → 𝐹:Q⟶Q) & ⊢ (φ → ∀𝑝 ∈ Q ∀𝑞 ∈ Q ((𝐹‘𝑝) <Q ((𝐹‘𝑞) +Q (𝑝 +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘𝑝) +Q (𝑝 +Q 𝑞)))) & ⊢ (φ → ∀𝑝 ∈ Q A <Q (𝐹‘𝑝)) & ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q (𝐹‘𝑞)}, {u ∈ Q ∣ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q u}⟩ ⇒ ⊢ (φ → ∀𝑞 ∈ Q ∀𝑟 ∈ Q (⟨{𝑙 ∣ 𝑙 <Q (𝐹‘𝑞)}, {u ∣ (𝐹‘𝑞) <Q u}⟩<P (𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q (𝑞 +Q 𝑟)}, {u ∣ (𝑞 +Q 𝑟) <Q u}⟩) ∧ 𝐿<P ⟨{𝑙 ∣ 𝑙 <Q ((𝐹‘𝑞) +Q (𝑞 +Q 𝑟))}, {u ∣ ((𝐹‘𝑞) +Q (𝑞 +Q 𝑟)) <Q u}⟩)) | ||
| 20-Jun-2020 | cauappcvgprlemcl 6624 | Lemma for cauappcvgpr 6633. The putative limit is a positive real. (Contributed by Jim Kingdon, 20-Jun-2020.) |
| ⊢ (φ → 𝐹:Q⟶Q) & ⊢ (φ → ∀𝑝 ∈ Q ∀𝑞 ∈ Q ((𝐹‘𝑝) <Q ((𝐹‘𝑞) +Q (𝑝 +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘𝑝) +Q (𝑝 +Q 𝑞)))) & ⊢ (φ → ∀𝑝 ∈ Q A <Q (𝐹‘𝑝)) & ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q (𝐹‘𝑞)}, {u ∈ Q ∣ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q u}⟩ ⇒ ⊢ (φ → 𝐿 ∈ P) | ||
| 19-Jun-2020 | cauappcvgpr 6633 | A Cauchy approximation has a limit. A Cauchy approximation, here 𝐹, is similar to a Cauchy sequence but is indexed by the desired tolerance (that is, how close together terms needs to be) rather than by natural numbers. This is basically Theorem 11.2.12 of [HoTT], p. (varies) with a few differences such as that we are proving the existence of a limit without anything about how fast it converges (that is, mere existence instead of existence, in HoTT terms), and that the codomain of 𝐹 is Q rather than P. We also specify that every term needs to be larger than a fraction A, to avoid the case where we have positive fractions which converge to zero (which is not a positive real). (Contributed by Jim Kingdon, 19-Jun-2020.) |
| ⊢ (φ → 𝐹:Q⟶Q) & ⊢ (φ → ∀𝑝 ∈ Q ∀𝑞 ∈ Q ((𝐹‘𝑝) <Q ((𝐹‘𝑞) +Q (𝑝 +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘𝑝) +Q (𝑝 +Q 𝑞)))) & ⊢ (φ → ∀𝑝 ∈ Q A <Q (𝐹‘𝑝)) ⇒ ⊢ (φ → ∃y ∈ P ∀𝑞 ∈ Q ∀𝑟 ∈ Q (⟨{𝑙 ∣ 𝑙 <Q (𝐹‘𝑞)}, {u ∣ (𝐹‘𝑞) <Q u}⟩<P (y +P ⟨{𝑙 ∣ 𝑙 <Q (𝑞 +Q 𝑟)}, {u ∣ (𝑞 +Q 𝑟) <Q u}⟩) ∧ y<P ⟨{𝑙 ∣ 𝑙 <Q ((𝐹‘𝑞) +Q (𝑞 +Q 𝑟))}, {u ∣ ((𝐹‘𝑞) +Q (𝑞 +Q 𝑟)) <Q u}⟩)) | ||
| 15-Jun-2020 | imdivapd 9182 | Imaginary part of a division. Related to remul2 9081. (Contributed by Jim Kingdon, 15-Jun-2020.) |
| ⊢ (φ → A ∈ ℝ) & ⊢ (φ → B ∈ ℂ) & ⊢ (φ → A # 0) ⇒ ⊢ (φ → (ℑ‘(B / A)) = ((ℑ‘B) / A)) | ||
| 15-Jun-2020 | redivapd 9181 | Real part of a division. Related to remul2 9081. (Contributed by Jim Kingdon, 15-Jun-2020.) |
| ⊢ (φ → A ∈ ℝ) & ⊢ (φ → B ∈ ℂ) & ⊢ (φ → A # 0) ⇒ ⊢ (φ → (ℜ‘(B / A)) = ((ℜ‘B) / A)) | ||
| 15-Jun-2020 | cjdivapd 9175 | Complex conjugate distributes over division. (Contributed by Jim Kingdon, 15-Jun-2020.) |
| ⊢ (φ → A ∈ ℂ) & ⊢ (φ → B ∈ ℂ) & ⊢ (φ → B # 0) ⇒ ⊢ (φ → (∗‘(A / B)) = ((∗‘A) / (∗‘B))) | ||
| 15-Jun-2020 | riotaexg 5415 | Restricted iota is a set. (Contributed by Jim Kingdon, 15-Jun-2020.) |
| ⊢ (A ∈ 𝑉 → (℩x ∈ A ψ) ∈ V) | ||
| 14-Jun-2020 | cjdivapi 9143 | Complex conjugate distributes over division. (Contributed by Jim Kingdon, 14-Jun-2020.) |
| ⊢ A ∈ ℂ & ⊢ B ∈ ℂ ⇒ ⊢ (B # 0 → (∗‘(A / B)) = ((∗‘A) / (∗‘B))) | ||
| 14-Jun-2020 | cjdivap 9117 | Complex conjugate distributes over division. (Contributed by Jim Kingdon, 14-Jun-2020.) |
| ⊢ ((A ∈ ℂ ∧ B ∈ ℂ ∧ B # 0) → (∗‘(A / B)) = ((∗‘A) / (∗‘B))) | ||
| 14-Jun-2020 | cjap0 9115 | A number is apart from zero iff its complex conjugate is apart from zero. (Contributed by Jim Kingdon, 14-Jun-2020.) |
| ⊢ (A ∈ ℂ → (A # 0 ↔ (∗‘A) # 0)) | ||
| 14-Jun-2020 | cjap 9114 | Complex conjugate and apartness. (Contributed by Jim Kingdon, 14-Jun-2020.) |
| ⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → ((∗‘A) # (∗‘B) ↔ A # B)) | ||
| 14-Jun-2020 | imdivap 9089 | Imaginary part of a division. Related to immul2 9088. (Contributed by Jim Kingdon, 14-Jun-2020.) |
| ⊢ ((A ∈ ℂ ∧ B ∈ ℝ ∧ B # 0) → (ℑ‘(A / B)) = ((ℑ‘A) / B)) | ||
| 14-Jun-2020 | redivap 9082 | Real part of a division. Related to remul2 9081. (Contributed by Jim Kingdon, 14-Jun-2020.) |
| ⊢ ((A ∈ ℂ ∧ B ∈ ℝ ∧ B # 0) → (ℜ‘(A / B)) = ((ℜ‘A) / B)) | ||
| 14-Jun-2020 | mulreap 9072 | A product with a real multiplier apart from zero is real iff the multiplicand is real. (Contributed by Jim Kingdon, 14-Jun-2020.) |
| ⊢ ((A ∈ ℂ ∧ B ∈ ℝ ∧ B # 0) → (A ∈ ℝ ↔ (B · A) ∈ ℝ)) | ||
| 13-Jun-2020 | sqgt0apd 9041 | The square of a real apart from zero is positive. (Contributed by Jim Kingdon, 13-Jun-2020.) |
| ⊢ (φ → A ∈ ℝ) & ⊢ (φ → A # 0) ⇒ ⊢ (φ → 0 < (A↑2)) | ||
| 13-Jun-2020 | reexpclzapd 9038 | Closure of exponentiation of reals. (Contributed by Jim Kingdon, 13-Jun-2020.) |
| ⊢ (φ → A ∈ ℝ) & ⊢ (φ → A # 0) & ⊢ (φ → 𝑁 ∈ ℤ) ⇒ ⊢ (φ → (A↑𝑁) ∈ ℝ) | ||
| 13-Jun-2020 | expdivapd 9028 | Nonnegative integer exponentiation of a quotient. (Contributed by Jim Kingdon, 13-Jun-2020.) |
| ⊢ (φ → A ∈ ℂ) & ⊢ (φ → B ∈ ℂ) & ⊢ (φ → B # 0) & ⊢ (φ → 𝑁 ∈ ℕ0) ⇒ ⊢ (φ → ((A / B)↑𝑁) = ((A↑𝑁) / (B↑𝑁))) | ||
| 13-Jun-2020 | sqdivapd 9027 | Distribution of square over division. (Contributed by Jim Kingdon, 13-Jun-2020.) |
| ⊢ (φ → A ∈ ℂ) & ⊢ (φ → B ∈ ℂ) & ⊢ (φ → B # 0) ⇒ ⊢ (φ → ((A / B)↑2) = ((A↑2) / (B↑2))) | ||
| 12-Jun-2020 | expsubapd 9025 | Exponent subtraction law for nonnegative integer exponentiation. (Contributed by Jim Kingdon, 12-Jun-2020.) |
| ⊢ (φ → A ∈ ℂ) & ⊢ (φ → A # 0) & ⊢ (φ → 𝑁 ∈ ℤ) & ⊢ (φ → 𝑀 ∈ ℤ) ⇒ ⊢ (φ → (A↑(𝑀 − 𝑁)) = ((A↑𝑀) / (A↑𝑁))) | ||
| 12-Jun-2020 | expm1apd 9024 | Value of a complex number raised to an integer power minus one. (Contributed by Jim Kingdon, 12-Jun-2020.) |
| ⊢ (φ → A ∈ ℂ) & ⊢ (φ → A # 0) & ⊢ (φ → 𝑁 ∈ ℤ) ⇒ ⊢ (φ → (A↑(𝑁 − 1)) = ((A↑𝑁) / A)) | ||
| 12-Jun-2020 | expp1zapd 9023 | Value of a nonzero complex number raised to an integer power plus one. (Contributed by Jim Kingdon, 12-Jun-2020.) |
| ⊢ (φ → A ∈ ℂ) & ⊢ (φ → A # 0) & ⊢ (φ → 𝑁 ∈ ℤ) ⇒ ⊢ (φ → (A↑(𝑁 + 1)) = ((A↑𝑁) · A)) | ||
| 12-Jun-2020 | exprecapd 9022 | Nonnegative integer exponentiation of a reciprocal. (Contributed by Jim Kingdon, 12-Jun-2020.) |
| ⊢ (φ → A ∈ ℂ) & ⊢ (φ → A # 0) & ⊢ (φ → 𝑁 ∈ ℤ) ⇒ ⊢ (φ → ((1 / A)↑𝑁) = (1 / (A↑𝑁))) | ||
| 12-Jun-2020 | expnegapd 9021 | Value of a complex number raised to a negative power. (Contributed by Jim Kingdon, 12-Jun-2020.) |
| ⊢ (φ → A ∈ ℂ) & ⊢ (φ → A # 0) & ⊢ (φ → 𝑁 ∈ ℤ) ⇒ ⊢ (φ → (A↑-𝑁) = (1 / (A↑𝑁))) | ||
| 12-Jun-2020 | expap0d 9020 | Nonnegative integer exponentiation is nonzero if its mantissa is nonzero. (Contributed by Jim Kingdon, 12-Jun-2020.) |
| ⊢ (φ → A ∈ ℂ) & ⊢ (φ → A # 0) & ⊢ (φ → 𝑁 ∈ ℤ) ⇒ ⊢ (φ → (A↑𝑁) # 0) | ||
| 12-Jun-2020 | expclzapd 9019 | Closure law for integer exponentiation. (Contributed by Jim Kingdon, 12-Jun-2020.) |
| ⊢ (φ → A ∈ ℂ) & ⊢ (φ → A # 0) & ⊢ (φ → 𝑁 ∈ ℤ) ⇒ ⊢ (φ → (A↑𝑁) ∈ ℂ) | ||
| 12-Jun-2020 | sqrecapd 9018 | Square of reciprocal. (Contributed by Jim Kingdon, 12-Jun-2020.) |
| ⊢ (φ → A ∈ ℂ) & ⊢ (φ → A # 0) ⇒ ⊢ (φ → ((1 / A)↑2) = (1 / (A↑2))) | ||
| 12-Jun-2020 | sqgt0api 8972 | The square of a nonzero real is positive. (Contributed by Jim Kingdon, 12-Jun-2020.) |
| ⊢ A ∈ ℝ ⇒ ⊢ (A # 0 → 0 < (A↑2)) | ||
| 12-Jun-2020 | sqdivapi 8970 | Distribution of square over division. (Contributed by Jim Kingdon, 12-Jun-2020.) |
| ⊢ A ∈ ℂ & ⊢ B ∈ ℂ & ⊢ B # 0 ⇒ ⊢ ((A / B)↑2) = ((A↑2) / (B↑2)) | ||
| 11-Jun-2020 | sqgt0ap 8955 | The square of a nonzero real is positive. (Contributed by Jim Kingdon, 11-Jun-2020.) |
| ⊢ ((A ∈ ℝ ∧ A # 0) → 0 < (A↑2)) | ||
| 11-Jun-2020 | sqdivap 8952 | Distribution of square over division. (Contributed by Jim Kingdon, 11-Jun-2020.) |
| ⊢ ((A ∈ ℂ ∧ B ∈ ℂ ∧ B # 0) → ((A / B)↑2) = ((A↑2) / (B↑2))) | ||
| 11-Jun-2020 | expdivap 8939 | Nonnegative integer exponentiation of a quotient. (Contributed by Jim Kingdon, 11-Jun-2020.) |
| ⊢ ((A ∈ ℂ ∧ (B ∈ ℂ ∧ B # 0) ∧ 𝑁 ∈ ℕ0) → ((A / B)↑𝑁) = ((A↑𝑁) / (B↑𝑁))) | ||
| 11-Jun-2020 | expm1ap 8938 | Value of a complex number raised to an integer power minus one. (Contributed by Jim Kingdon, 11-Jun-2020.) |
| ⊢ ((A ∈ ℂ ∧ A # 0 ∧ 𝑁 ∈ ℤ) → (A↑(𝑁 − 1)) = ((A↑𝑁) / A)) | ||
| 11-Jun-2020 | expp1zap 8937 | Value of a nonzero complex number raised to an integer power plus one. (Contributed by Jim Kingdon, 11-Jun-2020.) |
| ⊢ ((A ∈ ℂ ∧ A # 0 ∧ 𝑁 ∈ ℤ) → (A↑(𝑁 + 1)) = ((A↑𝑁) · A)) | ||
| 11-Jun-2020 | expsubap 8936 | Exponent subtraction law for nonnegative integer exponentiation. (Contributed by Jim Kingdon, 11-Jun-2020.) |
| ⊢ (((A ∈ ℂ ∧ A # 0) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (A↑(𝑀 − 𝑁)) = ((A↑𝑀) / (A↑𝑁))) | ||
| 11-Jun-2020 | expmulzap 8935 | Product of exponents law for integer exponentiation. (Contributed by Jim Kingdon, 11-Jun-2020.) |
| ⊢ (((A ∈ ℂ ∧ A # 0) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (A↑(𝑀 · 𝑁)) = ((A↑𝑀)↑𝑁)) | ||
| 10-Jun-2020 | expaddzap 8933 | Sum of exponents law for integer exponentiation. (Contributed by Jim Kingdon, 10-Jun-2020.) |
| ⊢ (((A ∈ ℂ ∧ A # 0) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (A↑(𝑀 + 𝑁)) = ((A↑𝑀) · (A↑𝑁))) | ||
| 10-Jun-2020 | expaddzaplem 8932 | Lemma for expaddzap 8933. (Contributed by Jim Kingdon, 10-Jun-2020.) |
| ⊢ (((A ∈ ℂ ∧ A # 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) → (A↑(𝑀 + 𝑁)) = ((A↑𝑀) · (A↑𝑁))) | ||
| 10-Jun-2020 | exprecap 8930 | Nonnegative integer exponentiation of a reciprocal. (Contributed by Jim Kingdon, 10-Jun-2020.) |
| ⊢ ((A ∈ ℂ ∧ A # 0 ∧ 𝑁 ∈ ℤ) → ((1 / A)↑𝑁) = (1 / (A↑𝑁))) | ||
| 10-Jun-2020 | mulexpzap 8929 | Integer exponentiation of a product. (Contributed by Jim Kingdon, 10-Jun-2020.) |
| ⊢ (((A ∈ ℂ ∧ A # 0) ∧ (B ∈ ℂ ∧ B # 0) ∧ 𝑁 ∈ ℤ) → ((A · B)↑𝑁) = ((A↑𝑁) · (B↑𝑁))) | ||
| 10-Jun-2020 | expap0i 8921 | Integer exponentiation is apart from zero if its mantissa is apart from zero. (Contributed by Jim Kingdon, 10-Jun-2020.) |
| ⊢ ((A ∈ ℂ ∧ A # 0 ∧ 𝑁 ∈ ℤ) → (A↑𝑁) # 0) | ||
| 10-Jun-2020 | expap0 8919 | Positive integer exponentiation is apart from zero iff its mantissa is apart from zero. That it is easier to prove this first, and then prove expeq0 8920 in terms of it, rather than the other way around, is perhaps an illustration of the maxim "In constructive analysis, the apartness is more basic [ than ] equality." ([Geuvers], p. 1). (Contributed by Jim Kingdon, 10-Jun-2020.) |
| ⊢ ((A ∈ ℂ ∧ 𝑁 ∈ ℕ) → ((A↑𝑁) # 0 ↔ A # 0)) | ||
| 10-Jun-2020 | mvllmulapd 7570 | Move LHS left multiplication to RHS. (Contributed by Jim Kingdon, 10-Jun-2020.) |
| ⊢ (φ → A ∈ ℂ) & ⊢ (φ → B ∈ ℂ) & ⊢ (φ → A # 0) & ⊢ (φ → (A · B) = 𝐶) ⇒ ⊢ (φ → B = (𝐶 / A)) | ||
| 9-Jun-2020 | expclzap 8914 | Closure law for integer exponentiation. (Contributed by Jim Kingdon, 9-Jun-2020.) |
| ⊢ ((A ∈ ℂ ∧ A # 0 ∧ 𝑁 ∈ ℤ) → (A↑𝑁) ∈ ℂ) | ||
| 9-Jun-2020 | expclzaplem 8913 | Closure law for integer exponentiation. Lemma for expclzap 8914 and expap0i 8921. (Contributed by Jim Kingdon, 9-Jun-2020.) |
| ⊢ ((A ∈ ℂ ∧ A # 0 ∧ 𝑁 ∈ ℤ) → (A↑𝑁) ∈ {z ∈ ℂ ∣ z # 0}) | ||
| 9-Jun-2020 | reexpclzap 8909 | Closure of exponentiation of reals. (Contributed by Jim Kingdon, 9-Jun-2020.) |
| ⊢ ((A ∈ ℝ ∧ A # 0 ∧ 𝑁 ∈ ℤ) → (A↑𝑁) ∈ ℝ) | ||
| 9-Jun-2020 | neg1ap0 7784 | -1 is apart from zero. (Contributed by Jim Kingdon, 9-Jun-2020.) |
| ⊢ -1 # 0 | ||
| 8-Jun-2020 | expcl2lemap 8901 | Lemma for proving integer exponentiation closure laws. (Contributed by Jim Kingdon, 8-Jun-2020.) |
| ⊢ 𝐹 ⊆ ℂ & ⊢ ((x ∈ 𝐹 ∧ y ∈ 𝐹) → (x · y) ∈ 𝐹) & ⊢ 1 ∈ 𝐹 & ⊢ ((x ∈ 𝐹 ∧ x # 0) → (1 / x) ∈ 𝐹) ⇒ ⊢ ((A ∈ 𝐹 ∧ A # 0 ∧ B ∈ ℤ) → (A↑B) ∈ 𝐹) | ||
| 8-Jun-2020 | expn1ap0 8899 | A number to the negative one power is the reciprocal. (Contributed by Jim Kingdon, 8-Jun-2020.) |
| ⊢ ((A ∈ ℂ ∧ A # 0) → (A↑-1) = (1 / A)) | ||
| 8-Jun-2020 | expineg2 8898 | Value of a complex number raised to a negative integer power. (Contributed by Jim Kingdon, 8-Jun-2020.) |
| ⊢ (((A ∈ ℂ ∧ A # 0) ∧ (𝑁 ∈ ℂ ∧ -𝑁 ∈ ℕ0)) → (A↑𝑁) = (1 / (A↑-𝑁))) | ||
| 8-Jun-2020 | expnegap0 8897 | Value of a complex number raised to a negative integer power. (Contributed by Jim Kingdon, 8-Jun-2020.) |
| ⊢ ((A ∈ ℂ ∧ A # 0 ∧ 𝑁 ∈ ℕ0) → (A↑-𝑁) = (1 / (A↑𝑁))) | ||
| 8-Jun-2020 | expinnval 8892 | Value of exponentiation to positive integer powers. (Contributed by Jim Kingdon, 8-Jun-2020.) |
| ⊢ ((A ∈ ℂ ∧ 𝑁 ∈ ℕ) → (A↑𝑁) = (seq1( · , (ℕ × {A}), ℂ)‘𝑁)) | ||
| 7-Jun-2020 | expival 8891 | Value of exponentiation to integer powers. (Contributed by Jim Kingdon, 7-Jun-2020.) |
| ⊢ ((A ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (A # 0 ∨ 0 ≤ 𝑁)) → (A↑𝑁) = if(𝑁 = 0, 1, if(0 < 𝑁, (seq1( · , (ℕ × {A}), ℂ)‘𝑁), (1 / (seq1( · , (ℕ × {A}), ℂ)‘-𝑁))))) | ||
| 7-Jun-2020 | expivallem 8890 | Lemma for expival 8891. If we take a complex number apart from zero and raise it to a positive integer power, the result is apart from zero. (Contributed by Jim Kingodon, 7-Jun-2020.) |
| ⊢ ((A ∈ ℂ ∧ A # 0 ∧ 𝑁 ∈ ℕ) → (seq1( · , (ℕ × {A}), ℂ)‘𝑁) # 0) | ||
| 7-Jun-2020 | df-iexp 8889 | Define exponentiation to nonnegative integer powers. This definition is not meant to be used directly; instead, exp0 8893 and expp1 8896 provide the standard recursive definition. The up-arrow notation is used by Donald Knuth for iterated exponentiation (Science 194, 1235-1242, 1976) and is convenient for us since we don't have superscripts. 10-Jun-2005: The definition was extended to include zero exponents, so that 0↑0 = 1 per the convention of Definition 10-4.1 of [Gleason] p. 134. 4-Jun-2014: The definition was extended to include negative integer exponents. The case x = 0, y < 0 gives the value (1 / 0), so we will avoid this case in our theorems. (Contributed by Jim Kingodon, 7-Jun-2020.) |
| ⊢ ↑ = (x ∈ ℂ, y ∈ ℤ ↦ if(y = 0, 1, if(0 < y, (seq1( · , (ℕ × {x}), ℂ)‘y), (1 / (seq1( · , (ℕ × {x}), ℂ)‘-y))))) | ||
| 4-Jun-2020 | iseqfveq 8887 | Equality of sequences. (Contributed by Jim Kingdon, 4-Jun-2020.) |
| ⊢ (φ → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((φ ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) = (𝐺‘𝑘)) & ⊢ (φ → 𝑆 ∈ 𝑉) & ⊢ ((φ ∧ x ∈ (ℤ≥‘𝑀)) → (𝐹‘x) ∈ 𝑆) & ⊢ ((φ ∧ x ∈ (ℤ≥‘𝑀)) → (𝐺‘x) ∈ 𝑆) & ⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆)) → (x + y) ∈ 𝑆) ⇒ ⊢ (φ → (seq𝑀( + , 𝐹, 𝑆)‘𝑁) = (seq𝑀( + , 𝐺, 𝑆)‘𝑁)) | ||
| 3-Jun-2020 | iseqfeq2 8886 | Equality of sequences. (Contributed by Jim Kingdon, 3-Jun-2020.) |
| ⊢ (φ → 𝐾 ∈ (ℤ≥‘𝑀)) & ⊢ (φ → (seq𝑀( + , 𝐹, 𝑆)‘𝐾) = (𝐺‘𝐾)) & ⊢ (φ → 𝑆 ∈ 𝑉) & ⊢ ((φ ∧ x ∈ (ℤ≥‘𝑀)) → (𝐹‘x) ∈ 𝑆) & ⊢ ((φ ∧ x ∈ (ℤ≥‘𝐾)) → (𝐺‘x) ∈ 𝑆) & ⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆)) → (x + y) ∈ 𝑆) & ⊢ ((φ ∧ 𝑘 ∈ (ℤ≥‘(𝐾 + 1))) → (𝐹‘𝑘) = (𝐺‘𝑘)) ⇒ ⊢ (φ → (seq𝑀( + , 𝐹, 𝑆) ↾ (ℤ≥‘𝐾)) = seq𝐾( + , 𝐺, 𝑆)) | ||
| 3-Jun-2020 | iseqfveq2 8885 | Equality of sequences. (Contributed by Jim Kingdon, 3-Jun-2020.) |
| ⊢ (φ → 𝐾 ∈ (ℤ≥‘𝑀)) & ⊢ (φ → (seq𝑀( + , 𝐹, 𝑆)‘𝐾) = (𝐺‘𝐾)) & ⊢ (φ → 𝑆 ∈ 𝑉) & ⊢ ((φ ∧ x ∈ (ℤ≥‘𝑀)) → (𝐹‘x) ∈ 𝑆) & ⊢ ((φ ∧ x ∈ (ℤ≥‘𝐾)) → (𝐺‘x) ∈ 𝑆) & ⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆)) → (x + y) ∈ 𝑆) & ⊢ (φ → 𝑁 ∈ (ℤ≥‘𝐾)) & ⊢ ((φ ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝐹‘𝑘) = (𝐺‘𝑘)) ⇒ ⊢ (φ → (seq𝑀( + , 𝐹, 𝑆)‘𝑁) = (seq𝐾( + , 𝐺, 𝑆)‘𝑁)) | ||
| 1-Jun-2020 | iseqcl 8883 | Closure properties of the recursive sequence builder. (Contributed by Jim Kingdon, 1-Jun-2020.) |
| ⊢ (φ → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ (φ → 𝑆 ∈ 𝑉) & ⊢ ((φ ∧ x ∈ (ℤ≥‘𝑀)) → (𝐹‘x) ∈ 𝑆) & ⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆)) → (x + y) ∈ 𝑆) ⇒ ⊢ (φ → (seq𝑀( + , 𝐹, 𝑆)‘𝑁) ∈ 𝑆) | ||
| 1-Jun-2020 | fzdcel 8654 | Decidability of membership in a finite interval of integers. (Contributed by Jim Kingdon, 1-Jun-2020.) |
| ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → DECID 𝐾 ∈ (𝑀...𝑁)) | ||
| 1-Jun-2020 | fztri3or 8653 | Trichotomy in terms of a finite interval of integers. (Contributed by Jim Kingdon, 1-Jun-2020.) |
| ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 < 𝑀 ∨ 𝐾 ∈ (𝑀...𝑁) ∨ 𝑁 < 𝐾)) | ||
| 1-Jun-2020 | zdclt 8074 | Integer < is decidable. (Contributed by Jim Kingdon, 1-Jun-2020.) |
| ⊢ ((A ∈ ℤ ∧ B ∈ ℤ) → DECID A < B) | ||
| 31-May-2020 | iseqp1 8884 | Value of the sequence builder function at a successor. (Contributed by Jim Kingdon, 31-May-2020.) |
| ⊢ (φ → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ (φ → 𝑆 ∈ 𝑉) & ⊢ ((φ ∧ x ∈ (ℤ≥‘𝑀)) → (𝐹‘x) ∈ 𝑆) & ⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆)) → (x + y) ∈ 𝑆) ⇒ ⊢ (φ → (seq𝑀( + , 𝐹, 𝑆)‘(𝑁 + 1)) = ((seq𝑀( + , 𝐹, 𝑆)‘𝑁) + (𝐹‘(𝑁 + 1)))) | ||
| 31-May-2020 | iseq1 8882 | Value of the sequence builder function at its initial value. (Contributed by Jim Kingdon, 31-May-2020.) |
| ⊢ (φ → 𝑀 ∈ ℤ) & ⊢ (φ → 𝑆 ∈ 𝑉) & ⊢ ((φ ∧ x ∈ (ℤ≥‘𝑀)) → (𝐹‘x) ∈ 𝑆) & ⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆)) → (x + y) ∈ 𝑆) ⇒ ⊢ (φ → (seq𝑀( + , 𝐹, 𝑆)‘𝑀) = (𝐹‘𝑀)) | ||
| 31-May-2020 | iseqovex 8879 | Closure of a function used in proving sequence builder theorems. This can be thought of as a lemma for the small number of sequence builder theorems which need it. (Contributed by Jim Kingdon, 31-May-2020.) |
| ⊢ ((φ ∧ x ∈ (ℤ≥‘𝑀)) → (𝐹‘x) ∈ 𝑆) & ⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆)) → (x + y) ∈ 𝑆) ⇒ ⊢ ((φ ∧ (x ∈ (ℤ≥‘𝑀) ∧ y ∈ 𝑆)) → (x(z ∈ (ℤ≥‘𝑀), w ∈ 𝑆 ↦ (w + (𝐹‘(z + 1))))y) ∈ 𝑆) | ||
| 31-May-2020 | frecuzrdgcl 8860 | Closure law for the recursive definition generator on upper integers. See comment in frec2uz0d 8846 for the description of 𝐺 as the mapping from 𝜔 to (ℤ≥‘𝐶). (Contributed by Jim Kingdon, 31-May-2020.) |
| ⊢ (φ → 𝐶 ∈ ℤ) & ⊢ 𝐺 = frec((x ∈ ℤ ↦ (x + 1)), 𝐶) & ⊢ (φ → 𝑆 ∈ 𝑉) & ⊢ (φ → A ∈ 𝑆) & ⊢ ((φ ∧ (x ∈ (ℤ≥‘𝐶) ∧ y ∈ 𝑆)) → (x𝐹y) ∈ 𝑆) & ⊢ 𝑅 = frec((x ∈ (ℤ≥‘𝐶), y ∈ 𝑆 ↦ ⟨(x + 1), (x𝐹y)⟩), ⟨𝐶, A⟩) & ⊢ (φ → 𝑇 = ran 𝑅) ⇒ ⊢ ((φ ∧ B ∈ (ℤ≥‘𝐶)) → (𝑇‘B) ∈ 𝑆) | ||
| 30-May-2020 | iseqfn 8881 | The sequence builder function is a function. (Contributed by Jim Kingdon, 30-May-2020.) |
| ⊢ (φ → 𝑀 ∈ ℤ) & ⊢ (φ → 𝑆 ∈ 𝑉) & ⊢ ((φ ∧ x ∈ (ℤ≥‘𝑀)) → (𝐹‘x) ∈ 𝑆) & ⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆)) → (x + y) ∈ 𝑆) ⇒ ⊢ (φ → seq𝑀( + , 𝐹, 𝑆) Fn (ℤ≥‘𝑀)) | ||
| 30-May-2020 | iseqval 8880 | Value of the sequence builder function. (Contributed by Jim Kingdon, 30-May-2020.) |
| ⊢ 𝑅 = frec((x ∈ (ℤ≥‘𝑀), y ∈ 𝑆 ↦ ⟨(x + 1), (x(z ∈ (ℤ≥‘𝑀), w ∈ 𝑆 ↦ (w + (𝐹‘(z + 1))))y)⟩), ⟨𝑀, (𝐹‘𝑀)⟩) & ⊢ ((φ ∧ x ∈ (ℤ≥‘𝑀)) → (𝐹‘x) ∈ 𝑆) & ⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆)) → (x + y) ∈ 𝑆) ⇒ ⊢ (φ → seq𝑀( + , 𝐹, 𝑆) = ran 𝑅) | ||
| 30-May-2020 | nfiseq 8878 | Hypothesis builder for the sequence builder operation. (Contributed by Jim Kingdon, 30-May-2020.) |
| ⊢ Ⅎx𝑀 & ⊢ Ⅎx + & ⊢ Ⅎx𝐹 & ⊢ Ⅎx𝑆 ⇒ ⊢ Ⅎxseq𝑀( + , 𝐹, 𝑆) | ||
| 30-May-2020 | iseqeq4 8877 | Equality theorem for the sequence builder operation. (Contributed by Jim Kingdon, 30-May-2020.) |
| ⊢ (𝑆 = 𝑇 → seq𝑀( + , 𝐹, 𝑆) = seq𝑀( + , 𝐹, 𝑇)) | ||
| 30-May-2020 | iseqeq3 8876 | Equality theorem for the sequence builder operation. (Contributed by Jim Kingdon, 30-May-2020.) |
| ⊢ (𝐹 = 𝐺 → seq𝑀( + , 𝐹, 𝑆) = seq𝑀( + , 𝐺, 𝑆)) | ||
| 30-May-2020 | iseqeq2 8875 | Equality theorem for the sequence builder operation. (Contributed by Jim Kingdon, 30-May-2020.) |
| ⊢ ( + = 𝑄 → seq𝑀( + , 𝐹, 𝑆) = seq𝑀(𝑄, 𝐹, 𝑆)) | ||
| 30-May-2020 | iseqeq1 8874 | Equality theorem for the sequence builder operation. (Contributed by Jim Kingdon, 30-May-2020.) |
| ⊢ (𝑀 = 𝑁 → seq𝑀( + , 𝐹, 𝑆) = seq𝑁( + , 𝐹, 𝑆)) | ||
| 30-May-2020 | nffrec 5921 | Bound-variable hypothesis builder for the finite recursive definition generator. (Contributed by Jim Kingdon, 30-May-2020.) |
| ⊢ Ⅎx𝐹 & ⊢ ℲxA ⇒ ⊢ Ⅎxfrec(𝐹, A) | ||
| 30-May-2020 | freceq2 5920 | Equality theorem for the finite recursive definition generator. (Contributed by Jim Kingdon, 30-May-2020.) |
| ⊢ (A = B → frec(𝐹, A) = frec(𝐹, B)) | ||
| Copyright terms: Public domain | W3C HTML validation [external] |