Most Recent Proofs - Intuitionistic Logic Explorer

Most recent proofs    These are the 100 (Unicode, GIF) or 1000 (Unicode, GIF) most recent proofs in the iset.mm database for the Intuitionistic Logic Explorer. The iset.mm database is maintained on GitHub with master (stable) and develop (development) versions. This page was created from the commit given on the MPE Most Recent Proofs page. The database from that commit is also available here: iset.mm.

See the MPE Most Recent Proofs page for news and some useful links.

Last updated on 17-Jan-2021 at 12:07 PM ET.

Recent Additions to the Intuitionistic Logic Explorer

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↑𝑁) ∈ ℝ)