![]() |
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: | ![]() |
![]() |
Date | Label | Description |
---|---|---|
Theorem | ||
17-Nov-2020 | pm3.2 126 | Join antecedents with conjunction. Theorem *3.2 of [WhiteheadRussell] p. 111. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 12-Nov-2012.) (Proof shortened by Jia Ming, 17-Nov-2020.) |
⊢ (φ → (ψ → (φ ∧ ψ))) | ||
27-Oct-2020 | bj-omssonALT 9423 | Alternate proof of bj-omsson 9422. (Contributed by BJ, 27-Oct-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜔 ⊆ On | ||
27-Oct-2020 | bj-omsson 9422 | Constructive proof of omsson 4278. See also bj-omssonALT 9423. (Contributed by BJ, 27-Oct-2020.) (Proof modification is discouraged.) (New usage is discouraged. |
⊢ 𝜔 ⊆ On | ||
27-Oct-2020 | bj-nnelon 9419 | A natural number is an ordinal. Constructive proof of nnon 4275. Can also be proved from bj-omssonALT 9423. (Contributed by BJ, 27-Oct-2020.) (Proof modification is discouraged.) |
⊢ (A ∈ 𝜔 → A ∈ On) | ||
27-Oct-2020 | bj-nnord 9418 | A natural number is an ordinal. Constructive proof of nnord 4277. Can also be proved from bj-nnelon 9419 if the latter is proved from bj-omssonALT 9423. (Contributed by BJ, 27-Oct-2020.) (Proof modification is discouraged.) |
⊢ (A ∈ 𝜔 → Ord A) | ||
27-Oct-2020 | bj-axempty2 9349 | Axiom of the empty set from bounded separation, alternate version to bj-axempty 9348. (Contributed by BJ, 27-Oct-2020.) (Proof modification is discouraged.) Use ax-nul 3874 instead. (New usage is discouraged.) |
⊢ ∃x∀y ¬ y ∈ x | ||
25-Oct-2020 | bj-indind 9391 | If A is inductive and B is "inductive in A", then (A ∩ B) is inductive. (Contributed by BJ, 25-Oct-2020.) |
⊢ ((Ind A ∧ (∅ ∈ B ∧ ∀x ∈ A (x ∈ B → suc x ∈ B))) → Ind (A ∩ B)) | ||
25-Oct-2020 | bj-axempty 9348 | Axiom of the empty set from bounded separation. It is provable from bounded separation since the intuitionistic FOL used in iset.mm assumes a non-empty universe. See axnul 3873. (Contributed by BJ, 25-Oct-2020.) (Proof modification is discouraged.) Use ax-nul 3874 instead. (New usage is discouraged.) |
⊢ ∃x∀y ∈ x ⊥ | ||
25-Oct-2020 | bj-axemptylem 9347 | Lemma for bj-axempty 9348 and bj-axempty2 9349. (Contributed by BJ, 25-Oct-2020.) (Proof modification is discouraged.) Use ax-nul 3874 instead. (New usage is discouraged.) |
⊢ ∃x∀y(y ∈ x → ⊥ ) | ||
23-Oct-2020 | caucvgprlemnkj 6637 | Lemma for caucvgpr 6653. Part of disjointness. (Contributed by Jim Kingdon, 23-Oct-2020.) |
⊢ (φ → 𝐹:N⟶Q) & ⊢ (φ → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛) <Q ((𝐹‘𝑘) +Q (*Q‘[〈𝑛, 1𝑜〉] ~Q )) ∧ (𝐹‘𝑘) <Q ((𝐹‘𝑛) +Q (*Q‘[〈𝑛, 1𝑜〉] ~Q ))))) & ⊢ (φ → 𝐾 ∈ N) & ⊢ (φ → 𝐽 ∈ N) & ⊢ (φ → 𝑆 ∈ Q) ⇒ ⊢ (φ → ¬ ((𝑆 +Q (*Q‘[〈𝐾, 1𝑜〉] ~Q )) <Q (𝐹‘𝐾) ∧ ((𝐹‘𝐽) +Q (*Q‘[〈𝐽, 1𝑜〉] ~Q )) <Q 𝑆)) | ||
20-Oct-2020 | caucvgprlemupu 6643 | Lemma for caucvgpr 6653. The upper cut of the putative limit is upper. (Contributed by Jim Kingdon, 20-Oct-2020.) |
⊢ (φ → 𝐹:N⟶Q) & ⊢ (φ → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛) <Q ((𝐹‘𝑘) +Q (*Q‘[〈𝑛, 1𝑜〉] ~Q )) ∧ (𝐹‘𝑘) <Q ((𝐹‘𝑛) +Q (*Q‘[〈𝑛, 1𝑜〉] ~Q ))))) & ⊢ (φ → ∀𝑗 ∈ N A <Q (𝐹‘𝑗)) & ⊢ 𝐿 = 〈{𝑙 ∈ Q ∣ ∃𝑗 ∈ N (𝑙 +Q (*Q‘[〈𝑗, 1𝑜〉] ~Q )) <Q (𝐹‘𝑗)}, {u ∈ Q ∣ ∃𝑗 ∈ N ((𝐹‘𝑗) +Q (*Q‘[〈𝑗, 1𝑜〉] ~Q )) <Q u}〉 ⇒ ⊢ ((φ ∧ 𝑠 <Q 𝑟 ∧ 𝑠 ∈ (2nd ‘𝐿)) → 𝑟 ∈ (2nd ‘𝐿)) | ||
20-Oct-2020 | caucvgprlemopu 6642 | Lemma for caucvgpr 6653. The upper cut of the putative limit is open. (Contributed by Jim Kingdon, 20-Oct-2020.) |
⊢ (φ → 𝐹:N⟶Q) & ⊢ (φ → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛) <Q ((𝐹‘𝑘) +Q (*Q‘[〈𝑛, 1𝑜〉] ~Q )) ∧ (𝐹‘𝑘) <Q ((𝐹‘𝑛) +Q (*Q‘[〈𝑛, 1𝑜〉] ~Q ))))) & ⊢ (φ → ∀𝑗 ∈ N A <Q (𝐹‘𝑗)) & ⊢ 𝐿 = 〈{𝑙 ∈ Q ∣ ∃𝑗 ∈ N (𝑙 +Q (*Q‘[〈𝑗, 1𝑜〉] ~Q )) <Q (𝐹‘𝑗)}, {u ∈ Q ∣ ∃𝑗 ∈ N ((𝐹‘𝑗) +Q (*Q‘[〈𝑗, 1𝑜〉] ~Q )) <Q u}〉 ⇒ ⊢ ((φ ∧ 𝑟 ∈ (2nd ‘𝐿)) → ∃𝑠 ∈ Q (𝑠 <Q 𝑟 ∧ 𝑠 ∈ (2nd ‘𝐿))) | ||
20-Oct-2020 | caucvgprlemlol 6641 | Lemma for caucvgpr 6653. The lower cut of the putative limit is lower. (Contributed by Jim Kingdon, 20-Oct-2020.) |
⊢ (φ → 𝐹:N⟶Q) & ⊢ (φ → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛) <Q ((𝐹‘𝑘) +Q (*Q‘[〈𝑛, 1𝑜〉] ~Q )) ∧ (𝐹‘𝑘) <Q ((𝐹‘𝑛) +Q (*Q‘[〈𝑛, 1𝑜〉] ~Q ))))) & ⊢ (φ → ∀𝑗 ∈ N A <Q (𝐹‘𝑗)) & ⊢ 𝐿 = 〈{𝑙 ∈ Q ∣ ∃𝑗 ∈ N (𝑙 +Q (*Q‘[〈𝑗, 1𝑜〉] ~Q )) <Q (𝐹‘𝑗)}, {u ∈ Q ∣ ∃𝑗 ∈ N ((𝐹‘𝑗) +Q (*Q‘[〈𝑗, 1𝑜〉] ~Q )) <Q u}〉 ⇒ ⊢ ((φ ∧ 𝑠 <Q 𝑟 ∧ 𝑟 ∈ (1st ‘𝐿)) → 𝑠 ∈ (1st ‘𝐿)) | ||
20-Oct-2020 | caucvgprlemopl 6640 | Lemma for caucvgpr 6653. The lower cut of the putative limit is open. (Contributed by Jim Kingdon, 20-Oct-2020.) |
⊢ (φ → 𝐹:N⟶Q) & ⊢ (φ → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛) <Q ((𝐹‘𝑘) +Q (*Q‘[〈𝑛, 1𝑜〉] ~Q )) ∧ (𝐹‘𝑘) <Q ((𝐹‘𝑛) +Q (*Q‘[〈𝑛, 1𝑜〉] ~Q ))))) & ⊢ (φ → ∀𝑗 ∈ N A <Q (𝐹‘𝑗)) & ⊢ 𝐿 = 〈{𝑙 ∈ Q ∣ ∃𝑗 ∈ N (𝑙 +Q (*Q‘[〈𝑗, 1𝑜〉] ~Q )) <Q (𝐹‘𝑗)}, {u ∈ Q ∣ ∃𝑗 ∈ N ((𝐹‘𝑗) +Q (*Q‘[〈𝑗, 1𝑜〉] ~Q )) <Q u}〉 ⇒ ⊢ ((φ ∧ 𝑠 ∈ (1st ‘𝐿)) → ∃𝑟 ∈ Q (𝑠 <Q 𝑟 ∧ 𝑟 ∈ (1st ‘𝐿))) | ||
18-Oct-2020 | caucvgprlemnbj 6638 | Lemma for caucvgpr 6653. Non-existence of two elements of the sequence which are too far from each other. (Contributed by Jim Kingdon, 18-Oct-2020.) |
⊢ (φ → 𝐹:N⟶Q) & ⊢ (φ → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛) <Q ((𝐹‘𝑘) +Q (*Q‘[〈𝑛, 1𝑜〉] ~Q )) ∧ (𝐹‘𝑘) <Q ((𝐹‘𝑛) +Q (*Q‘[〈𝑛, 1𝑜〉] ~Q ))))) & ⊢ (φ → B ∈ N) & ⊢ (φ → 𝐽 ∈ N) ⇒ ⊢ (φ → ¬ (((𝐹‘B) +Q (*Q‘[〈B, 1𝑜〉] ~Q )) +Q (*Q‘[〈𝐽, 1𝑜〉] ~Q )) <Q (𝐹‘𝐽)) | ||
9-Oct-2020 | caucvgprlemladdfu 6648 | Lemma for caucvgpr 6653. Adding 𝑆 after embedding in positive reals, or adding it as a rational. (Contributed by Jim Kingdon, 9-Oct-2020.) |
⊢ (φ → 𝐹:N⟶Q) & ⊢ (φ → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛) <Q ((𝐹‘𝑘) +Q (*Q‘[〈𝑛, 1𝑜〉] ~Q )) ∧ (𝐹‘𝑘) <Q ((𝐹‘𝑛) +Q (*Q‘[〈𝑛, 1𝑜〉] ~Q ))))) & ⊢ (φ → ∀𝑗 ∈ N A <Q (𝐹‘𝑗)) & ⊢ 𝐿 = 〈{𝑙 ∈ Q ∣ ∃𝑗 ∈ N (𝑙 +Q (*Q‘[〈𝑗, 1𝑜〉] ~Q )) <Q (𝐹‘𝑗)}, {u ∈ Q ∣ ∃𝑗 ∈ N ((𝐹‘𝑗) +Q (*Q‘[〈𝑗, 1𝑜〉] ~Q )) <Q u}〉 & ⊢ (φ → 𝑆 ∈ Q) ⇒ ⊢ (φ → (2nd ‘(𝐿 +P 〈{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}〉)) ⊆ {u ∈ Q ∣ ∃𝑗 ∈ N (((𝐹‘𝑗) +Q (*Q‘[〈𝑗, 1𝑜〉] ~Q )) +Q 𝑆) <Q u}) | ||
9-Oct-2020 | caucvgprlemk 6636 | Lemma for caucvgpr 6653. Reciprocals of positive integers decrease as the positive integers increase. (Contributed by Jim Kingdon, 9-Oct-2020.) |
⊢ (φ → 𝐽 <N 𝐾) & ⊢ (φ → (*Q‘[〈𝐽, 1𝑜〉] ~Q ) <Q 𝑄) ⇒ ⊢ (φ → (*Q‘[〈𝐾, 1𝑜〉] ~Q ) <Q 𝑄) | ||
8-Oct-2020 | caucvgprlemladdrl 6649 | Lemma for caucvgpr 6653. Adding 𝑆 after embedding in positive reals, or adding it as a rational. (Contributed by Jim Kingdon, 8-Oct-2020.) |
⊢ (φ → 𝐹:N⟶Q) & ⊢ (φ → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛) <Q ((𝐹‘𝑘) +Q (*Q‘[〈𝑛, 1𝑜〉] ~Q )) ∧ (𝐹‘𝑘) <Q ((𝐹‘𝑛) +Q (*Q‘[〈𝑛, 1𝑜〉] ~Q ))))) & ⊢ (φ → ∀𝑗 ∈ N A <Q (𝐹‘𝑗)) & ⊢ 𝐿 = 〈{𝑙 ∈ Q ∣ ∃𝑗 ∈ N (𝑙 +Q (*Q‘[〈𝑗, 1𝑜〉] ~Q )) <Q (𝐹‘𝑗)}, {u ∈ Q ∣ ∃𝑗 ∈ N ((𝐹‘𝑗) +Q (*Q‘[〈𝑗, 1𝑜〉] ~Q )) <Q u}〉 & ⊢ (φ → 𝑆 ∈ Q) ⇒ ⊢ (φ → {𝑙 ∈ Q ∣ ∃𝑗 ∈ N (𝑙 +Q (*Q‘[〈𝑗, 1𝑜〉] ~Q )) <Q ((𝐹‘𝑗) +Q 𝑆)} ⊆ (1st ‘(𝐿 +P 〈{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}〉))) | ||
3-Oct-2020 | caucvgprlem2 6651 | Lemma for caucvgpr 6653. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 3-Oct-2020.) |
⊢ (φ → 𝐹:N⟶Q) & ⊢ (φ → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛) <Q ((𝐹‘𝑘) +Q (*Q‘[〈𝑛, 1𝑜〉] ~Q )) ∧ (𝐹‘𝑘) <Q ((𝐹‘𝑛) +Q (*Q‘[〈𝑛, 1𝑜〉] ~Q ))))) & ⊢ (φ → ∀𝑗 ∈ N A <Q (𝐹‘𝑗)) & ⊢ 𝐿 = 〈{𝑙 ∈ Q ∣ ∃𝑗 ∈ N (𝑙 +Q (*Q‘[〈𝑗, 1𝑜〉] ~Q )) <Q (𝐹‘𝑗)}, {u ∈ Q ∣ ∃𝑗 ∈ N ((𝐹‘𝑗) +Q (*Q‘[〈𝑗, 1𝑜〉] ~Q )) <Q u}〉 & ⊢ (φ → 𝑄 ∈ Q) & ⊢ (φ → 𝐽 <N 𝐾) & ⊢ (φ → (*Q‘[〈𝐽, 1𝑜〉] ~Q ) <Q 𝑄) ⇒ ⊢ (φ → 𝐿<P 〈{𝑙 ∣ 𝑙 <Q ((𝐹‘𝐾) +Q 𝑄)}, {u ∣ ((𝐹‘𝐾) +Q 𝑄) <Q u}〉) | ||
3-Oct-2020 | caucvgprlem1 6650 | Lemma for caucvgpr 6653. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 3-Oct-2020.) |
⊢ (φ → 𝐹:N⟶Q) & ⊢ (φ → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛) <Q ((𝐹‘𝑘) +Q (*Q‘[〈𝑛, 1𝑜〉] ~Q )) ∧ (𝐹‘𝑘) <Q ((𝐹‘𝑛) +Q (*Q‘[〈𝑛, 1𝑜〉] ~Q ))))) & ⊢ (φ → ∀𝑗 ∈ N A <Q (𝐹‘𝑗)) & ⊢ 𝐿 = 〈{𝑙 ∈ Q ∣ ∃𝑗 ∈ N (𝑙 +Q (*Q‘[〈𝑗, 1𝑜〉] ~Q )) <Q (𝐹‘𝑗)}, {u ∈ Q ∣ ∃𝑗 ∈ N ((𝐹‘𝑗) +Q (*Q‘[〈𝑗, 1𝑜〉] ~Q )) <Q u}〉 & ⊢ (φ → 𝑄 ∈ Q) & ⊢ (φ → 𝐽 <N 𝐾) & ⊢ (φ → (*Q‘[〈𝐽, 1𝑜〉] ~Q ) <Q 𝑄) ⇒ ⊢ (φ → 〈{𝑙 ∣ 𝑙 <Q (𝐹‘𝐾)}, {u ∣ (𝐹‘𝐾) <Q u}〉<P (𝐿 +P 〈{𝑙 ∣ 𝑙 <Q 𝑄}, {u ∣ 𝑄 <Q u}〉)) | ||
3-Oct-2020 | ltnnnq 6406 | Ordering of positive integers via <N or <Q is equivalent. (Contributed by Jim Kingdon, 3-Oct-2020.) |
⊢ ((A ∈ N ∧ B ∈ N) → (A <N B ↔ [〈A, 1𝑜〉] ~Q <Q [〈B, 1𝑜〉] ~Q )) | ||
1-Oct-2020 | caucvgprlemlim 6652 | Lemma for caucvgpr 6653. The putative limit is a limit. (Contributed by Jim Kingdon, 1-Oct-2020.) |
⊢ (φ → 𝐹:N⟶Q) & ⊢ (φ → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛) <Q ((𝐹‘𝑘) +Q (*Q‘[〈𝑛, 1𝑜〉] ~Q )) ∧ (𝐹‘𝑘) <Q ((𝐹‘𝑛) +Q (*Q‘[〈𝑛, 1𝑜〉] ~Q ))))) & ⊢ (φ → ∀𝑗 ∈ N A <Q (𝐹‘𝑗)) & ⊢ 𝐿 = 〈{𝑙 ∈ Q ∣ ∃𝑗 ∈ N (𝑙 +Q (*Q‘[〈𝑗, 1𝑜〉] ~Q )) <Q (𝐹‘𝑗)}, {u ∈ Q ∣ ∃𝑗 ∈ N ((𝐹‘𝑗) +Q (*Q‘[〈𝑗, 1𝑜〉] ~Q )) <Q u}〉 ⇒ ⊢ (φ → ∀x ∈ Q ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <N 𝑘 → (〈{𝑙 ∣ 𝑙 <Q (𝐹‘𝑘)}, {u ∣ (𝐹‘𝑘) <Q u}〉<P (𝐿 +P 〈{𝑙 ∣ 𝑙 <Q x}, {u ∣ x <Q u}〉) ∧ 𝐿<P 〈{𝑙 ∣ 𝑙 <Q ((𝐹‘𝑘) +Q x)}, {u ∣ ((𝐹‘𝑘) +Q x) <Q u}〉))) | ||
27-Sep-2020 | caucvgprlemloc 6646 | Lemma for caucvgpr 6653. The putative limit is located. (Contributed by Jim Kingdon, 27-Sep-2020.) |
⊢ (φ → 𝐹:N⟶Q) & ⊢ (φ → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛) <Q ((𝐹‘𝑘) +Q (*Q‘[〈𝑛, 1𝑜〉] ~Q )) ∧ (𝐹‘𝑘) <Q ((𝐹‘𝑛) +Q (*Q‘[〈𝑛, 1𝑜〉] ~Q ))))) & ⊢ (φ → ∀𝑗 ∈ N A <Q (𝐹‘𝑗)) & ⊢ 𝐿 = 〈{𝑙 ∈ Q ∣ ∃𝑗 ∈ N (𝑙 +Q (*Q‘[〈𝑗, 1𝑜〉] ~Q )) <Q (𝐹‘𝑗)}, {u ∈ Q ∣ ∃𝑗 ∈ N ((𝐹‘𝑗) +Q (*Q‘[〈𝑗, 1𝑜〉] ~Q )) <Q u}〉 ⇒ ⊢ (φ → ∀𝑠 ∈ Q ∀𝑟 ∈ Q (𝑠 <Q 𝑟 → (𝑠 ∈ (1st ‘𝐿) ∨ 𝑟 ∈ (2nd ‘𝐿)))) | ||
27-Sep-2020 | caucvgprlemdisj 6645 | Lemma for caucvgpr 6653. The putative limit is disjoint. (Contributed by Jim Kingdon, 27-Sep-2020.) |
⊢ (φ → 𝐹:N⟶Q) & ⊢ (φ → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛) <Q ((𝐹‘𝑘) +Q (*Q‘[〈𝑛, 1𝑜〉] ~Q )) ∧ (𝐹‘𝑘) <Q ((𝐹‘𝑛) +Q (*Q‘[〈𝑛, 1𝑜〉] ~Q ))))) & ⊢ (φ → ∀𝑗 ∈ N A <Q (𝐹‘𝑗)) & ⊢ 𝐿 = 〈{𝑙 ∈ Q ∣ ∃𝑗 ∈ N (𝑙 +Q (*Q‘[〈𝑗, 1𝑜〉] ~Q )) <Q (𝐹‘𝑗)}, {u ∈ Q ∣ ∃𝑗 ∈ N ((𝐹‘𝑗) +Q (*Q‘[〈𝑗, 1𝑜〉] ~Q )) <Q u}〉 ⇒ ⊢ (φ → ∀𝑠 ∈ Q ¬ (𝑠 ∈ (1st ‘𝐿) ∧ 𝑠 ∈ (2nd ‘𝐿))) | ||
27-Sep-2020 | caucvgprlemrnd 6644 | Lemma for caucvgpr 6653. The putative limit is rounded. (Contributed by Jim Kingdon, 27-Sep-2020.) |
⊢ (φ → 𝐹:N⟶Q) & ⊢ (φ → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛) <Q ((𝐹‘𝑘) +Q (*Q‘[〈𝑛, 1𝑜〉] ~Q )) ∧ (𝐹‘𝑘) <Q ((𝐹‘𝑛) +Q (*Q‘[〈𝑛, 1𝑜〉] ~Q ))))) & ⊢ (φ → ∀𝑗 ∈ N A <Q (𝐹‘𝑗)) & ⊢ 𝐿 = 〈{𝑙 ∈ Q ∣ ∃𝑗 ∈ N (𝑙 +Q (*Q‘[〈𝑗, 1𝑜〉] ~Q )) <Q (𝐹‘𝑗)}, {u ∈ Q ∣ ∃𝑗 ∈ N ((𝐹‘𝑗) +Q (*Q‘[〈𝑗, 1𝑜〉] ~Q )) <Q u}〉 ⇒ ⊢ (φ → (∀𝑠 ∈ Q (𝑠 ∈ (1st ‘𝐿) ↔ ∃𝑟 ∈ Q (𝑠 <Q 𝑟 ∧ 𝑟 ∈ (1st ‘𝐿))) ∧ ∀𝑟 ∈ Q (𝑟 ∈ (2nd ‘𝐿) ↔ ∃𝑠 ∈ Q (𝑠 <Q 𝑟 ∧ 𝑠 ∈ (2nd ‘𝐿))))) | ||
27-Sep-2020 | caucvgprlemm 6639 | Lemma for caucvgpr 6653. The putative limit is inhabited. (Contributed by Jim Kingdon, 27-Sep-2020.) |
⊢ (φ → 𝐹:N⟶Q) & ⊢ (φ → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛) <Q ((𝐹‘𝑘) +Q (*Q‘[〈𝑛, 1𝑜〉] ~Q )) ∧ (𝐹‘𝑘) <Q ((𝐹‘𝑛) +Q (*Q‘[〈𝑛, 1𝑜〉] ~Q ))))) & ⊢ (φ → ∀𝑗 ∈ N A <Q (𝐹‘𝑗)) & ⊢ 𝐿 = 〈{𝑙 ∈ Q ∣ ∃𝑗 ∈ N (𝑙 +Q (*Q‘[〈𝑗, 1𝑜〉] ~Q )) <Q (𝐹‘𝑗)}, {u ∈ Q ∣ ∃𝑗 ∈ N ((𝐹‘𝑗) +Q (*Q‘[〈𝑗, 1𝑜〉] ~Q )) <Q u}〉 ⇒ ⊢ (φ → (∃𝑠 ∈ Q 𝑠 ∈ (1st ‘𝐿) ∧ ∃𝑟 ∈ Q 𝑟 ∈ (2nd ‘𝐿))) | ||
27-Sep-2020 | archrecnq 6635 | Archimedean principle for fractions (reciprocal version). (Contributed by Jim Kingdon, 27-Sep-2020.) |
⊢ (A ∈ Q → ∃𝑗 ∈ N (*Q‘[〈𝑗, 1𝑜〉] ~Q ) <Q A) | ||
26-Sep-2020 | caucvgprlemcl 6647 | Lemma for caucvgpr 6653. The putative limit is a positive real. (Contributed by Jim Kingdon, 26-Sep-2020.) |
⊢ (φ → 𝐹:N⟶Q) & ⊢ (φ → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛) <Q ((𝐹‘𝑘) +Q (*Q‘[〈𝑛, 1𝑜〉] ~Q )) ∧ (𝐹‘𝑘) <Q ((𝐹‘𝑛) +Q (*Q‘[〈𝑛, 1𝑜〉] ~Q ))))) & ⊢ (φ → ∀𝑗 ∈ N A <Q (𝐹‘𝑗)) & ⊢ 𝐿 = 〈{𝑙 ∈ Q ∣ ∃𝑗 ∈ N (𝑙 +Q (*Q‘[〈𝑗, 1𝑜〉] ~Q )) <Q (𝐹‘𝑗)}, {u ∈ Q ∣ ∃𝑗 ∈ N ((𝐹‘𝑗) +Q (*Q‘[〈𝑗, 1𝑜〉] ~Q )) <Q u}〉 ⇒ ⊢ (φ → 𝐿 ∈ P) | ||
26-Aug-2020 | sqrt0rlem 9212 | Lemma for sqrt0 9213. (Contributed by Jim Kingdon, 26-Aug-2020.) |
⊢ ((A ∈ ℝ ∧ ((A↑2) = 0 ∧ 0 ≤ A)) ↔ A = 0) | ||
23-Aug-2020 | sqrtrval 9209 | 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 9207 |
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 6542 | 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 6541 | Lemma for addnqpr 6542. 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 6540 | Lemma for addnqpr 6542. 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 6539 | Lemma for addnqpr 6542. 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 6538 | Lemma for addnqpr 6542. 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 6616 | Lemma for cauappcvgprlemladdrl 6629. 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 6621 | Lemma for cauappcvgpr 6634. 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 6620 | Lemma for cauappcvgpr 6634. 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 6619 | Lemma for cauappcvgpr 6634. 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 6618 | Lemma for cauappcvgpr 6634. 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 6624 | Lemma for cauappcvgpr 6634. 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 6623 | Lemma for cauappcvgpr 6634. 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 6622 | Lemma for cauappcvgpr 6634. 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 6617 | Lemma for cauappcvgpr 6634. 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 6629 | Lemma for cauappcvgprlemladd 6630. 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 6628 | Lemma for cauappcvgprlemladd 6630. 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 6627 | Lemma for cauappcvgprlemladd 6630. 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 6626 | Lemma for cauappcvgprlemladd 6630. 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 6533 | 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 6530 | 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 6632 | Lemma for cauappcvgpr 6634. 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 6631 | Lemma for cauappcvgpr 6634. 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 6630 | Lemma for cauappcvgpr 6634. 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 6633 | Lemma for cauappcvgpr 6634. 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 6625 | Lemma for cauappcvgpr 6634. 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 6634 | 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}〉)) | ||
18-Jun-2020 | caucvgpr 6653 | A Cauchy sequence of positive fractions with a modulus of convergence converges to a positive real. This is basically Corollary 11.2.13 of [HoTT], p. (varies) (one key difference being that this is for positive reals rather than signed reals). Also, the HoTT book theorem has a modulus of convergence (that is, a rate of convergence) specified by (11.2.9) in HoTT whereas this theorem fixes the rate of convergence to say that all terms after the nth term must be within 1 / 𝑛 of the nth term (it should later be able to prove versions of this theorem with a different fixed rate or a modulus of convergence supplied as a hypothesis). 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, 18-Jun-2020.) |
⊢ (φ → 𝐹:N⟶Q) & ⊢ (φ → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛) <Q ((𝐹‘𝑘) +Q (*Q‘[〈𝑛, 1𝑜〉] ~Q )) ∧ (𝐹‘𝑘) <Q ((𝐹‘𝑛) +Q (*Q‘[〈𝑛, 1𝑜〉] ~Q ))))) & ⊢ (φ → ∀𝑗 ∈ N A <Q (𝐹‘𝑗)) ⇒ ⊢ (φ → ∃y ∈ P ∀x ∈ Q ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <N 𝑘 → (〈{𝑙 ∣ 𝑙 <Q (𝐹‘𝑘)}, {u ∣ (𝐹‘𝑘) <Q u}〉<P (y +P 〈{𝑙 ∣ 𝑙 <Q x}, {u ∣ x <Q u}〉) ∧ y<P 〈{𝑙 ∣ 𝑙 <Q ((𝐹‘𝑘) +Q x)}, {u ∣ ((𝐹‘𝑘) +Q x) <Q u}〉))) | ||
15-Jun-2020 | imdivapd 9202 | Imaginary part of a division. Related to remul2 9101. (Contributed by Jim Kingdon, 15-Jun-2020.) |
⊢ (φ → A ∈ ℝ) & ⊢ (φ → B ∈ ℂ) & ⊢ (φ → A # 0) ⇒ ⊢ (φ → (ℑ‘(B / A)) = ((ℑ‘B) / A)) | ||
15-Jun-2020 | redivapd 9201 | Real part of a division. Related to remul2 9101. (Contributed by Jim Kingdon, 15-Jun-2020.) |
⊢ (φ → A ∈ ℝ) & ⊢ (φ → B ∈ ℂ) & ⊢ (φ → A # 0) ⇒ ⊢ (φ → (ℜ‘(B / A)) = ((ℜ‘B) / A)) | ||
15-Jun-2020 | cjdivapd 9195 | 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 9163 | Complex conjugate distributes over division. (Contributed by Jim Kingdon, 14-Jun-2020.) |
⊢ A ∈ ℂ & ⊢ B ∈ ℂ ⇒ ⊢ (B # 0 → (∗‘(A / B)) = ((∗‘A) / (∗‘B))) | ||
14-Jun-2020 | cjdivap 9137 | Complex conjugate distributes over division. (Contributed by Jim Kingdon, 14-Jun-2020.) |
⊢ ((A ∈ ℂ ∧ B ∈ ℂ ∧ B # 0) → (∗‘(A / B)) = ((∗‘A) / (∗‘B))) | ||
14-Jun-2020 | cjap0 9135 | 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 9134 | Complex conjugate and apartness. (Contributed by Jim Kingdon, 14-Jun-2020.) |
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → ((∗‘A) # (∗‘B) ↔ A # B)) | ||
14-Jun-2020 | imdivap 9109 | Imaginary part of a division. Related to immul2 9108. (Contributed by Jim Kingdon, 14-Jun-2020.) |
⊢ ((A ∈ ℂ ∧ B ∈ ℝ ∧ B # 0) → (ℑ‘(A / B)) = ((ℑ‘A) / B)) | ||
14-Jun-2020 | redivap 9102 | Real part of a division. Related to remul2 9101. (Contributed by Jim Kingdon, 14-Jun-2020.) |
⊢ ((A ∈ ℂ ∧ B ∈ ℝ ∧ B # 0) → (ℜ‘(A / B)) = ((ℜ‘A) / B)) | ||
14-Jun-2020 | mulreap 9092 | 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 9061 | 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 9058 | Closure of exponentiation of reals. (Contributed by Jim Kingdon, 13-Jun-2020.) |
⊢ (φ → A ∈ ℝ) & ⊢ (φ → A # 0) & ⊢ (φ → 𝑁 ∈ ℤ) ⇒ ⊢ (φ → (A↑𝑁) ∈ ℝ) | ||
13-Jun-2020 | expdivapd 9048 | 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 9047 | 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 9045 | Exponent subtraction law for nonnegative integer exponentiation. (Contributed by Jim Kingdon, 12-Jun-2020.) |
⊢ (φ → A ∈ ℂ) & ⊢ (φ → A # 0) & ⊢ (φ → 𝑁 ∈ ℤ) & ⊢ (φ → 𝑀 ∈ ℤ) ⇒ ⊢ (φ → (A↑(𝑀 − 𝑁)) = ((A↑𝑀) / (A↑𝑁))) | ||
12-Jun-2020 | expm1apd 9044 | 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 9043 | 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 9042 | Nonnegative integer exponentiation of a reciprocal. (Contributed by Jim Kingdon, 12-Jun-2020.) |
⊢ (φ → A ∈ ℂ) & ⊢ (φ → A # 0) & ⊢ (φ → 𝑁 ∈ ℤ) ⇒ ⊢ (φ → ((1 / A)↑𝑁) = (1 / (A↑𝑁))) | ||
12-Jun-2020 | expnegapd 9041 | 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 9040 | 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 9039 | Closure law for integer exponentiation. (Contributed by Jim Kingdon, 12-Jun-2020.) |
⊢ (φ → A ∈ ℂ) & ⊢ (φ → A # 0) & ⊢ (φ → 𝑁 ∈ ℤ) ⇒ ⊢ (φ → (A↑𝑁) ∈ ℂ) | ||
12-Jun-2020 | sqrecapd 9038 | Square of reciprocal. (Contributed by Jim Kingdon, 12-Jun-2020.) |
⊢ (φ → A ∈ ℂ) & ⊢ (φ → A # 0) ⇒ ⊢ (φ → ((1 / A)↑2) = (1 / (A↑2))) | ||
12-Jun-2020 | sqgt0api 8992 | 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 8990 | 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 8975 | 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 8972 | 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 8959 | 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 8958 | 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 8957 | 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 8956 | Exponent subtraction law for nonnegative integer exponentiation. (Contributed by Jim Kingdon, 11-Jun-2020.) |
⊢ (((A ∈ ℂ ∧ A # 0) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (A↑(𝑀 − 𝑁)) = ((A↑𝑀) / (A↑𝑁))) | ||
11-Jun-2020 | expmulzap 8955 | Product of exponents law for integer exponentiation. (Contributed by Jim Kingdon, 11-Jun-2020.) |
⊢ (((A ∈ ℂ ∧ A # 0) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (A↑(𝑀 · 𝑁)) = ((A↑𝑀)↑𝑁)) | ||
10-Jun-2020 | expaddzap 8953 | Sum of exponents law for integer exponentiation. (Contributed by Jim Kingdon, 10-Jun-2020.) |
⊢ (((A ∈ ℂ ∧ A # 0) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (A↑(𝑀 + 𝑁)) = ((A↑𝑀) · (A↑𝑁))) | ||
10-Jun-2020 | expaddzaplem 8952 | Lemma for expaddzap 8953. (Contributed by Jim Kingdon, 10-Jun-2020.) |
⊢ (((A ∈ ℂ ∧ A # 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) → (A↑(𝑀 + 𝑁)) = ((A↑𝑀) · (A↑𝑁))) | ||
10-Jun-2020 | exprecap 8950 | Nonnegative integer exponentiation of a reciprocal. (Contributed by Jim Kingdon, 10-Jun-2020.) |
⊢ ((A ∈ ℂ ∧ A # 0 ∧ 𝑁 ∈ ℤ) → ((1 / A)↑𝑁) = (1 / (A↑𝑁))) | ||
10-Jun-2020 | mulexpzap 8949 | 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 8941 | 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 8939 | 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 8940 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 7590 | 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 8934 | Closure law for integer exponentiation. (Contributed by Jim Kingdon, 9-Jun-2020.) |
⊢ ((A ∈ ℂ ∧ A # 0 ∧ 𝑁 ∈ ℤ) → (A↑𝑁) ∈ ℂ) | ||
9-Jun-2020 | expclzaplem 8933 | Closure law for integer exponentiation. Lemma for expclzap 8934 and expap0i 8941. (Contributed by Jim Kingdon, 9-Jun-2020.) |
⊢ ((A ∈ ℂ ∧ A # 0 ∧ 𝑁 ∈ ℤ) → (A↑𝑁) ∈ {z ∈ ℂ ∣ z # 0}) | ||
9-Jun-2020 | reexpclzap 8929 | Closure of exponentiation of reals. (Contributed by Jim Kingdon, 9-Jun-2020.) |
⊢ ((A ∈ ℝ ∧ A # 0 ∧ 𝑁 ∈ ℤ) → (A↑𝑁) ∈ ℝ) |
Copyright terms: Public domain | W3C HTML validation [external] |