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 21-Jan-2020 at 12:30 AM ET.

Recent Additions to the Intuitionistic Logic Explorer

Date	Label	Description
Theorem
17-Jan-2020	addcom 6737	Addition commutes. (Contributed by Jim Kingdon, 17-Jan-2020.)
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → (A + B) = (B + A))
17-Jan-2020	ax-addcom 6590	Addition commutes. Axiom for real and complex numbers, justified by theorem axaddcom 6564. Proofs should normally use addcom 6737 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 17-Jan-2020.)
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → (A + B) = (B + A))
17-Jan-2020	axaddcom 6564	Addition commutes. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-addcom 6590 be used later. Instead, use addcom 6737. In the Metamath Proof Explorer this is not a complex number axiom but is instead proved from other axioms. That proof relies on real number trichotomy and it is not known whether it is possible to prove this from the other axioms without it. (Contributed by Jim Kingdon, 17-Jan-2020.) (New usage is discouraged.)
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → (A + B) = (B + A))
16-Jan-2020	addid1 6738	0 is an additive identity. (Contributed by Jim Kingdon, 16-Jan-2020.)
⊢ (A ∈ ℂ → (A + 0) = A)
16-Jan-2020	ax-0id 6598	0 is an identity element for real addition. Axiom for real and complex numbers, justified by theorem ax0id 6572. Proofs should normally use addid1 6738 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 16-Jan-2020.)
⊢ (A ∈ ℂ → (A + 0) = A)
16-Jan-2020	ax0id 6572	0 is an identity element for real addition. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-0id 6598. In the Metamath Proof Explorer this is not a complex number axiom but is instead proved from other axioms. That proof relies on excluded middle and it is not known whether it is possible to prove this from the other axioms without excluded middle. (Contributed by Jim Kingdon, 16-Jan-2020.) (New usage is discouraged.)
⊢ (A ∈ ℂ → (A + 0) = A)
15-Jan-2020	axltwlin 6688	Real number less-than is weakly linear. Axiom for real and complex numbers, derived from set theory. This restates ax-pre-ltwlin 6603 with ordering on the extended reals. (Contributed by Jim Kingdon, 15-Jan-2020.)
⊢ ((A ∈ ℝ ∧ B ∈ ℝ ∧ 𝐶 ∈ ℝ) → (A < B → (A < 𝐶 ∨ 𝐶 < B)))
15-Jan-2020	axltirr 6687	Real number less-than is irreflexive. Axiom for real and complex numbers, derived from set theory. This restates ax-pre-ltirr 6602 with ordering on the extended reals. New proofs should use ltnr 6695 instead for naming consistency. (New usage is discouraged.) (Contributed by Jim Kingdon, 15-Jan-2020.)
⊢ (A ∈ ℝ → ¬ A < A)
14-Jan-2020	2pwuninelg 5820	The power set of the power set of the union of a set does not belong to the set. This theorem provides a way of constructing a new set that doesn't belong to a given set. (Contributed by Jim Kingdon, 14-Jan-2020.)
⊢ (A ∈ 𝑉 → ¬ 𝒫 𝒫 ∪ A ∈ A)
13-Jan-2020	1re 6628	1 is a real number. (Contributed by Jim Kingdon, 13-Jan-2020.)
⊢ 1 ∈ ℝ
13-Jan-2020	ax-1re 6584	1 is a real number. Axiom for real and complex numbers, justified by theorem ax1re 6558. Proofs should use 1re 6628 instead. (Contributed by Jim Kingdon, 13-Jan-2020.) (New usage is discouraged.)
⊢ 1 ∈ ℝ
13-Jan-2020	ax1re 6558	1 is a real number. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-1re 6584. In the Metamath Proof Explorer, this is not a complex number axiom but is proved from ax-1cn 6583 and the other axioms. It is not known whether we can do so here, but the Metamath Proof Explorer proof (accessed 13-Jan-2020) uses excluded middle. (Contributed by Jim Kingdon, 13-Jan-2020.) (New usage is discouraged.)
⊢ 1 ∈ ℝ
12-Jan-2020	ax-pre-ltwlin 6603	Real number less-than is weakly linear. Axiom for real and complex numbers, justified by theorem axpre-ltwlin 6577. (Contributed by Jim Kingdon, 12-Jan-2020.)
⊢ ((A ∈ ℝ ∧ B ∈ ℝ ∧ 𝐶 ∈ ℝ) → (A <ℝ B → (A <ℝ 𝐶 ∨ 𝐶 <ℝ B)))
12-Jan-2020	ax-pre-ltirr 6602	Real number less-than is irreflexive. Axiom for real and complex numbers, justified by theorem ax-pre-ltirr 6602. (Contributed by Jim Kingdon, 12-Jan-2020.)
⊢ (A ∈ ℝ → ¬ A <ℝ A)
12-Jan-2020	ax-precex 6600	Existence of reciprocal of positive real number. Axiom for real and complex numbers, justified by theorem axprecex 6574. In treatments which assume excluded middle, the 0 <ℝ A condition is generally replaced by A ≠ 0. (Contributed by Jim Kingdon, 12-Jan-2020.)
⊢ ((A ∈ ℝ ∧ 0 <ℝ A) → ∃x ∈ ℝ (A · x) = 1)
12-Jan-2020	ax-0lt1 6596	0 is less than 1. Axiom for real and complex numbers, justified by theorem ax0lt1 6570. (Contributed by Jim Kingdon, 12-Jan-2020.)
⊢ 0 <ℝ 1
12-Jan-2020	axpre-ltwlin 6577	Real number less-than is weakly linear. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-ltwlin 6603. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.)
⊢ ((A ∈ ℝ ∧ B ∈ ℝ ∧ 𝐶 ∈ ℝ) → (A <ℝ B → (A <ℝ 𝐶 ∨ 𝐶 <ℝ B)))
12-Jan-2020	axpre-ltirr 6576	Real number less-than is irreflexive. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-ltirr 6602. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.)
⊢ (A ∈ ℝ → ¬ A <ℝ A)
12-Jan-2020	axprecex 6574	Existence of reciprocal of positive real number. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-precex 6600. In treatments which assume excluded middle, the 0 <ℝ A condition is generally replaced by A ≠ 0. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.)
⊢ ((A ∈ ℝ ∧ 0 <ℝ A) → ∃x ∈ ℝ (A · x) = 1)
12-Jan-2020	ax0lt1 6570	0 is less than 1. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-0lt1 6596. The version of this axiom in the Metamath Proof Explorer reads 1 ≠ 0; here we change it to 0 <ℝ 1. The proof of 0 <ℝ 1 from 1 ≠ 0 in the Metamath Proof Explorer (accessed 12-Jan-2020) relies on real number trichotomy. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.)
⊢ 0 <ℝ 1
8-Jan-2020	ecidg 6081	A set is equal to its converse epsilon coset. (Note: converse epsilon is not an equivalence relation.) (Contributed by Jim Kingdon, 8-Jan-2020.)
⊢ (A ∈ 𝑉 → [A]◡ E = A)
5-Jan-2020	1idsr 6515	1 is an identity element for multiplication. (Contributed by Jim Kingdon, 5-Jan-2020.)
⊢ (A ∈ R → (A ·R 1R) = A)
4-Jan-2020	distrsrg 6506	Multiplication of signed reals is distributive. (Contributed by Jim Kingdon, 4-Jan-2020.)
⊢ ((A ∈ R ∧ B ∈ R ∧ 𝐶 ∈ R) → (A ·R (B +R 𝐶)) = ((A ·R B) +R (A ·R 𝐶)))
3-Jan-2020	mulasssrg 6505	Multiplication of signed reals is associative. (Contributed by Jim Kingdon, 3-Jan-2020.)
⊢ ((A ∈ R ∧ B ∈ R ∧ 𝐶 ∈ R) → ((A ·R B) ·R 𝐶) = (A ·R (B ·R 𝐶)))
3-Jan-2020	mulcomsrg 6504	Multiplication of signed reals is commutative. (Contributed by Jim Kingdon, 3-Jan-2020.)
⊢ ((A ∈ R ∧ B ∈ R) → (A ·R B) = (B ·R A))
3-Jan-2020	addasssrg 6503	Addition of signed reals is associative. (Contributed by Jim Kingdon, 3-Jan-2020.)
⊢ ((A ∈ R ∧ B ∈ R ∧ 𝐶 ∈ R) → ((A +R B) +R 𝐶) = (A +R (B +R 𝐶)))
3-Jan-2020	addcomsrg 6502	Addition of signed reals is commutative. (Contributed by Jim Kingdon, 3-Jan-2020.)
⊢ ((A ∈ R ∧ B ∈ R) → (A +R B) = (B +R A))
3-Jan-2020	caovlem2d 5616	Rearrangement of expression involving multiplication (𝐺) and addition (𝐹). (Contributed by Jim Kingdon, 3-Jan-2020.)
⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆)) → (x𝐺y) = (y𝐺x))    &   ⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆 ∧ z ∈ 𝑆)) → ((x𝐹y)𝐺z) = ((x𝐺z)𝐹(y𝐺z)))    &   ⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆 ∧ z ∈ 𝑆)) → ((x𝐺y)𝐺z) = (x𝐺(y𝐺z)))    &   ⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆)) → (x𝐺y) ∈ 𝑆)    &   ⊢ (φ → A ∈ 𝑆)    &   ⊢ (φ → B ∈ 𝑆)    &   ⊢ (φ → 𝐶 ∈ 𝑆)    &   ⊢ (φ → 𝐷 ∈ 𝑆)    &   ⊢ (φ → 𝐻 ∈ 𝑆)    &   ⊢ (φ → 𝑅 ∈ 𝑆)    &   ⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆)) → (x𝐹y) = (y𝐹x))    &   ⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆 ∧ z ∈ 𝑆)) → ((x𝐹y)𝐹z) = (x𝐹(y𝐹z)))    &   ⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆)) → (x𝐹y) ∈ 𝑆)    ⇒   ⊢ (φ → ((((A𝐺𝐶)𝐹(B𝐺𝐷))𝐺𝐻)𝐹(((A𝐺𝐷)𝐹(B𝐺𝐶))𝐺𝑅)) = ((A𝐺((𝐶𝐺𝐻)𝐹(𝐷𝐺𝑅)))𝐹(B𝐺((𝐶𝐺𝑅)𝐹(𝐷𝐺𝐻)))))
2-Jan-2020	bj-d0clsepcl 7148	Δ0-classical logic and separation implies classical logic. (Contributed by BJ, 2-Jan-2020.) (Proof modification is discouraged.)
⊢ (φ ∨ ¬ φ)
2-Jan-2020	ax-bj-d0cl 7147	Axiom for Δ0-classical logic. (Contributed by BJ, 2-Jan-2020.)
⊢ BOUNDED φ    ⇒   ⊢ (φ ∨ ¬ φ)
1-Jan-2020	mulcmpblnrlemg 6487	Lemma used in lemma showing compatibility of multiplication. (Contributed by Jim Kingdon, 1-Jan-2020.)
⊢ ((((A ∈ P ∧ B ∈ P) ∧ (𝐶 ∈ P ∧ 𝐷 ∈ P)) ∧ ((𝐹 ∈ P ∧ 𝐺 ∈ P) ∧ (𝑅 ∈ P ∧ 𝑆 ∈ P))) → (((A +P 𝐷) = (B +P 𝐶) ∧ (𝐹 +P 𝑆) = (𝐺 +P 𝑅)) → ((𝐷 ·P 𝐹) +P (((A ·P 𝐹) +P (B ·P 𝐺)) +P ((𝐶 ·P 𝑆) +P (𝐷 ·P 𝑅)))) = ((𝐷 ·P 𝐹) +P (((A ·P 𝐺) +P (B ·P 𝐹)) +P ((𝐶 ·P 𝑅) +P (𝐷 ·P 𝑆))))))
31-Dec-2019	eceq1d 6053	Equality theorem for equivalence class (deduction form). (Contributed by Jim Kingdon, 31-Dec-2019.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → [A]𝐶 = [B]𝐶)
30-Dec-2019	mulsrmo 6491	There is at most one result from multiplying signed reals. (Contributed by Jim Kingdon, 30-Dec-2019.)
⊢ ((A ∈ ((P × P) / ~R ) ∧ B ∈ ((P × P) / ~R )) → ∃*z∃w∃v∃u∃𝑡((A = [⟨w, v⟩] ~R ∧ B = [⟨u, 𝑡⟩] ~R ) ∧ z = [⟨((w ·P u) +P (v ·P 𝑡)), ((w ·P 𝑡) +P (v ·P u))⟩] ~R ))
30-Dec-2019	addsrmo 6490	There is at most one result from adding signed reals. (Contributed by Jim Kingdon, 30-Dec-2019.)
⊢ ((A ∈ ((P × P) / ~R ) ∧ B ∈ ((P × P) / ~R )) → ∃*z∃w∃v∃u∃𝑡((A = [⟨w, v⟩] ~R ∧ B = [⟨u, 𝑡⟩] ~R ) ∧ z = [⟨(w +P u), (v +P 𝑡)⟩] ~R ))
30-Dec-2019	prsrlem1 6489	Decomposing signed reals into positive reals. Lemma for addsrpr 6492 and mulsrpr 6493. (Contributed by Jim Kingdon, 30-Dec-2019.)
⊢ (((A ∈ ((P × P) / ~R ) ∧ B ∈ ((P × P) / ~R )) ∧ ((A = [⟨w, v⟩] ~R ∧ B = [⟨u, 𝑡⟩] ~R ) ∧ (A = [⟨𝑠, f⟩] ~R ∧ B = [⟨g, ℎ⟩] ~R ))) → ((((w ∈ P ∧ v ∈ P) ∧ (𝑠 ∈ P ∧ f ∈ P)) ∧ ((u ∈ P ∧ 𝑡 ∈ P) ∧ (g ∈ P ∧ ℎ ∈ P))) ∧ ((w +P f) = (v +P 𝑠) ∧ (u +P ℎ) = (𝑡 +P g))))
29-Dec-2019	bj-omelon 7181	The set 𝜔 is an ordinal. Constructive proof of omelon 4258. (Contributed by BJ, 29-Dec-2019.) (Proof modification is discouraged.)
⊢ 𝜔 ∈ On
29-Dec-2019	bj-omord 7180	The set 𝜔 is an ordinal. (Contributed by BJ, 29-Dec-2019.) (Proof modification is discouraged.)
⊢ Ord 𝜔
29-Dec-2019	bj-omtrans2 7179	The set 𝜔 is transitive. (Contributed by BJ, 29-Dec-2019.) (Proof modification is discouraged.)
⊢ Tr 𝜔
29-Dec-2019	bj-omtrans 7178	The set 𝜔 is transitive. A natural number is included in 𝜔. The idea is to use bounded induction with the formula x ⊆ 𝜔. This formula, in a logic with terms, is bounded. So in our logic without terms, we need to temporarily replace it with x ⊆ 𝑎 and then deduce the original claim. (Contributed by BJ, 29-Dec-2019.) (Proof modification is discouraged.)
⊢ (A ∈ 𝜔 → A ⊆ 𝜔)
29-Dec-2019	ltrnqg 6277	Ordering property of reciprocal for positive fractions. For a simplified version of the forward implication, see ltrnqi 6278. (Contributed by Jim Kingdon, 29-Dec-2019.)
⊢ ((A ∈ Q ∧ B ∈ Q) → (A <Q B ↔ (*Q‘B) <Q (*Q‘A)))
29-Dec-2019	rec1nq 6254	Reciprocal of positive fraction one. (Contributed by Jim Kingdon, 29-Dec-2019.)
⊢ (*Q‘1Q) = 1Q
28-Dec-2019	recexprlemupu 6462	The upper cut of B is upper. Lemma for recexpr 6472. (Contributed by Jim Kingdon, 28-Dec-2019.)
⊢ B = ⟨{x ∣ ∃y(x <Q y ∧ (*Q‘y) ∈ (2nd ‘A))}, {x ∣ ∃y(y <Q x ∧ (*Q‘y) ∈ (1st ‘A))}⟩    ⇒   ⊢ ((A ∈ P ∧ 𝑟 ∈ Q) → (∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑞 ∈ (2nd ‘B)) → 𝑟 ∈ (2nd ‘B)))
28-Dec-2019	recexprlemopu 6461	The upper cut of B is open. Lemma for recexpr 6472. (Contributed by Jim Kingdon, 28-Dec-2019.)
⊢ B = ⟨{x ∣ ∃y(x <Q y ∧ (*Q‘y) ∈ (2nd ‘A))}, {x ∣ ∃y(y <Q x ∧ (*Q‘y) ∈ (1st ‘A))}⟩    ⇒   ⊢ ((A ∈ P ∧ 𝑟 ∈ Q ∧ 𝑟 ∈ (2nd ‘B)) → ∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑞 ∈ (2nd ‘B)))
28-Dec-2019	recexprlemlol 6460	The lower cut of B is lower. Lemma for recexpr 6472. (Contributed by Jim Kingdon, 28-Dec-2019.)
⊢ B = ⟨{x ∣ ∃y(x <Q y ∧ (*Q‘y) ∈ (2nd ‘A))}, {x ∣ ∃y(y <Q x ∧ (*Q‘y) ∈ (1st ‘A))}⟩    ⇒   ⊢ ((A ∈ P ∧ 𝑞 ∈ Q) → (∃𝑟 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑟 ∈ (1st ‘B)) → 𝑞 ∈ (1st ‘B)))
28-Dec-2019	recexprlemopl 6459	The lower cut of B is open. Lemma for recexpr 6472. (Contributed by Jim Kingdon, 28-Dec-2019.)
⊢ B = ⟨{x ∣ ∃y(x <Q y ∧ (*Q‘y) ∈ (2nd ‘A))}, {x ∣ ∃y(y <Q x ∧ (*Q‘y) ∈ (1st ‘A))}⟩    ⇒   ⊢ ((A ∈ P ∧ 𝑞 ∈ Q ∧ 𝑞 ∈ (1st ‘B)) → ∃𝑟 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑟 ∈ (1st ‘B)))
28-Dec-2019	prmuloc2 6411	Positive reals are multiplicatively located. This is a variation of prmuloc 6410 which only constructs one (named) point and is therefore often easier to work with. It states that given a ratio B, there are elements of the lower and upper cut which have exactly that ratio between them. (Contributed by Jim Kingdon, 28-Dec-2019.)
⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 1Q <Q B) → ∃x ∈ 𝐿 (x ·Q B) ∈ 𝑈)
28-Dec-2019	1pru 6406	The upper cut of the positive real number 'one'. (Contributed by Jim Kingdon, 28-Dec-2019.)
⊢ (2nd ‘1P) = {x ∣ 1Q <Q x}
28-Dec-2019	1prl 6405	The lower cut of the positive real number 'one'. (Contributed by Jim Kingdon, 28-Dec-2019.)
⊢ (1st ‘1P) = {x ∣ x <Q 1Q}
27-Dec-2019	recexprlemex 6471	B is the reciprocal of A. Lemma for recexpr 6472. (Contributed by Jim Kingdon, 27-Dec-2019.)
⊢ B = ⟨{x ∣ ∃y(x <Q y ∧ (*Q‘y) ∈ (2nd ‘A))}, {x ∣ ∃y(y <Q x ∧ (*Q‘y) ∈ (1st ‘A))}⟩    ⇒   ⊢ (A ∈ P → (A ·P B) = 1P)
27-Dec-2019	recexprlemss1u 6470	The upper cut of A ·P B is a subset of the upper cut of one. Lemma for recexpr 6472. (Contributed by Jim Kingdon, 27-Dec-2019.)
⊢ B = ⟨{x ∣ ∃y(x <Q y ∧ (*Q‘y) ∈ (2nd ‘A))}, {x ∣ ∃y(y <Q x ∧ (*Q‘y) ∈ (1st ‘A))}⟩    ⇒   ⊢ (A ∈ P → (2nd ‘(A ·P B)) ⊆ (2nd ‘1P))
27-Dec-2019	recexprlemss1l 6469	The lower cut of A ·P B is a subset of the lower cut of one. Lemma for recexpr 6472. (Contributed by Jim Kingdon, 27-Dec-2019.)
⊢ B = ⟨{x ∣ ∃y(x <Q y ∧ (*Q‘y) ∈ (2nd ‘A))}, {x ∣ ∃y(y <Q x ∧ (*Q‘y) ∈ (1st ‘A))}⟩    ⇒   ⊢ (A ∈ P → (1st ‘(A ·P B)) ⊆ (1st ‘1P))
27-Dec-2019	recexprlem1ssu 6468	The upper cut of one is a subset of the upper cut of A ·P B. Lemma for recexpr 6472. (Contributed by Jim Kingdon, 27-Dec-2019.)
⊢ B = ⟨{x ∣ ∃y(x <Q y ∧ (*Q‘y) ∈ (2nd ‘A))}, {x ∣ ∃y(y <Q x ∧ (*Q‘y) ∈ (1st ‘A))}⟩    ⇒   ⊢ (A ∈ P → (2nd ‘1P) ⊆ (2nd ‘(A ·P B)))
27-Dec-2019	recexprlem1ssl 6467	The lower cut of one is a subset of the lower cut of A ·P B. Lemma for recexpr 6472. (Contributed by Jim Kingdon, 27-Dec-2019.)
⊢ B = ⟨{x ∣ ∃y(x <Q y ∧ (*Q‘y) ∈ (2nd ‘A))}, {x ∣ ∃y(y <Q x ∧ (*Q‘y) ∈ (1st ‘A))}⟩    ⇒   ⊢ (A ∈ P → (1st ‘1P) ⊆ (1st ‘(A ·P B)))
27-Dec-2019	recexprlempr 6466	B is a positive real. Lemma for recexpr 6472. (Contributed by Jim Kingdon, 27-Dec-2019.)
⊢ B = ⟨{x ∣ ∃y(x <Q y ∧ (*Q‘y) ∈ (2nd ‘A))}, {x ∣ ∃y(y <Q x ∧ (*Q‘y) ∈ (1st ‘A))}⟩    ⇒   ⊢ (A ∈ P → B ∈ P)
27-Dec-2019	recexprlemloc 6465	B is located. Lemma for recexpr 6472. (Contributed by Jim Kingdon, 27-Dec-2019.)
⊢ B = ⟨{x ∣ ∃y(x <Q y ∧ (*Q‘y) ∈ (2nd ‘A))}, {x ∣ ∃y(y <Q x ∧ (*Q‘y) ∈ (1st ‘A))}⟩    ⇒   ⊢ (A ∈ P → ∀𝑞 ∈ Q ∀𝑟 ∈ Q (𝑞 <Q 𝑟 → (𝑞 ∈ (1st ‘B) ∨ 𝑟 ∈ (2nd ‘B))))
27-Dec-2019	recexprlemdisj 6464	B is disjoint. Lemma for recexpr 6472. (Contributed by Jim Kingdon, 27-Dec-2019.)
⊢ B = ⟨{x ∣ ∃y(x <Q y ∧ (*Q‘y) ∈ (2nd ‘A))}, {x ∣ ∃y(y <Q x ∧ (*Q‘y) ∈ (1st ‘A))}⟩    ⇒   ⊢ (A ∈ P → ∀𝑞 ∈ Q ¬ (𝑞 ∈ (1st ‘B) ∧ 𝑞 ∈ (2nd ‘B)))
27-Dec-2019	recexprlemrnd 6463	B is rounded. Lemma for recexpr 6472. (Contributed by Jim Kingdon, 27-Dec-2019.)
⊢ B = ⟨{x ∣ ∃y(x <Q y ∧ (*Q‘y) ∈ (2nd ‘A))}, {x ∣ ∃y(y <Q x ∧ (*Q‘y) ∈ (1st ‘A))}⟩    ⇒   ⊢ (A ∈ P → (∀𝑞 ∈ Q (𝑞 ∈ (1st ‘B) ↔ ∃𝑟 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑟 ∈ (1st ‘B))) ∧ ∀𝑟 ∈ Q (𝑟 ∈ (2nd ‘B) ↔ ∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑞 ∈ (2nd ‘B)))))
27-Dec-2019	recexprlemm 6458	B is inhabited. Lemma for recexpr 6472. (Contributed by Jim Kingdon, 27-Dec-2019.)
⊢ B = ⟨{x ∣ ∃y(x <Q y ∧ (*Q‘y) ∈ (2nd ‘A))}, {x ∣ ∃y(y <Q x ∧ (*Q‘y) ∈ (1st ‘A))}⟩    ⇒   ⊢ (A ∈ P → (∃𝑞 ∈ Q 𝑞 ∈ (1st ‘B) ∧ ∃𝑟 ∈ Q 𝑟 ∈ (2nd ‘B)))
27-Dec-2019	recexprlemelu 6457	Membership in the upper cut of B. Lemma for recexpr 6472. (Contributed by Jim Kingdon, 27-Dec-2019.)
⊢ B = ⟨{x ∣ ∃y(x <Q y ∧ (*Q‘y) ∈ (2nd ‘A))}, {x ∣ ∃y(y <Q x ∧ (*Q‘y) ∈ (1st ‘A))}⟩    ⇒   ⊢ (𝐶 ∈ (2nd ‘B) ↔ ∃y(y <Q 𝐶 ∧ (*Q‘y) ∈ (1st ‘A)))
27-Dec-2019	recexprlemell 6456	Membership in the lower cut of B. Lemma for recexpr 6472. (Contributed by Jim Kingdon, 27-Dec-2019.)
⊢ B = ⟨{x ∣ ∃y(x <Q y ∧ (*Q‘y) ∈ (2nd ‘A))}, {x ∣ ∃y(y <Q x ∧ (*Q‘y) ∈ (1st ‘A))}⟩    ⇒   ⊢ (𝐶 ∈ (1st ‘B) ↔ ∃y(𝐶 <Q y ∧ (*Q‘y) ∈ (2nd ‘A)))
26-Dec-2019	ltaprg 6455	Ordering property of addition. Proposition 9-3.5(v) of [Gleason] p. 123. Part of Definition 11.2.7(vi) of [HoTT]], p. (varies). (Contributed by Jim Kingdon, 26-Dec-2019.)
⊢ ((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) → (A<P B ↔ (𝐶 +P A)<P (𝐶 +P B)))
26-Dec-2019	prarloc2 6358	A Dedekind cut is arithmetically located. This is a variation of prarloc 6357 which only constructs one (named) point and is therefore often easier to work with. It states that given a tolerance 𝑃, there are elements of the lower and upper cut which are exactly that tolerance from each other. (Contributed by Jim Kingdon, 26-Dec-2019.)
⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) → ∃𝑎 ∈ 𝐿 (𝑎 +Q 𝑃) ∈ 𝑈)
25-Dec-2019	addcanprlemu 6452	Lemma for addcanprg 6453. (Contributed by Jim Kingdon, 25-Dec-2019.)
⊢ (((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) ∧ (A +P B) = (A +P 𝐶)) → (2nd ‘B) ⊆ (2nd ‘𝐶))
25-Dec-2019	addcanprleml 6451	Lemma for addcanprg 6453. (Contributed by Jim Kingdon, 25-Dec-2019.)
⊢ (((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) ∧ (A +P B) = (A +P 𝐶)) → (1st ‘B) ⊆ (1st ‘𝐶))
24-Dec-2019	addcanprg 6453	Addition cancellation law for positive reals. Proposition 9-3.5(vi) of [Gleason] p. 123. (Contributed by Jim Kingdon, 24-Dec-2019.)
⊢ ((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) → ((A +P B) = (A +P 𝐶) → B = 𝐶))
23-Dec-2019	ltprordil 6428	If a positive real is less than a second positive real, its lower cut is a subset of the second's lower cut. (Contributed by Jim Kingdon, 23-Dec-2019.)
⊢ (A<P B → (1st ‘A) ⊆ (1st ‘B))
22-Dec-2019	bj-findis 7197	Principle of induction, using implicit substitutions (the biconditional versions of the hypotheses are implicit substitutions, and we have weakened them to implications). Constructive proof (from CZF). See bj-bdfindis 7169 for a bounded version not requiring ax-setind 4204. See finds 4250 for a proof in IZF. From this version, it is easy to prove of finds 4250, finds2 4251, finds1 4252. (Contributed by BJ, 22-Dec-2019.) (Proof modification is discouraged.)
⊢ Ⅎxψ    &   ⊢ Ⅎxχ    &   ⊢ Ⅎxθ    &   ⊢ (x = ∅ → (ψ → φ))    &   ⊢ (x = y → (φ → χ))    &   ⊢ (x = suc y → (θ → φ))    ⇒   ⊢ ((ψ ∧ ∀y ∈ 𝜔 (χ → θ)) → ∀x ∈ 𝜔 φ)
21-Dec-2019	ltexprlemupu 6441	The upper cut of our constructed difference is upper. Lemma for ltexpri 6450. (Contributed by Jim Kingdon, 21-Dec-2019.)
⊢ 𝐶 = ⟨{x ∈ Q ∣ ∃y(y ∈ (2nd ‘A) ∧ (y +Q x) ∈ (1st ‘B))}, {x ∈ Q ∣ ∃y(y ∈ (1st ‘A) ∧ (y +Q x) ∈ (2nd ‘B))}⟩    ⇒   ⊢ ((A<P B ∧ 𝑟 ∈ Q) → (∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑞 ∈ (2nd ‘𝐶)) → 𝑟 ∈ (2nd ‘𝐶)))
21-Dec-2019	ltexprlemopu 6440	The upper cut of our constructed difference is open. Lemma for ltexpri 6450. (Contributed by Jim Kingdon, 21-Dec-2019.)
⊢ 𝐶 = ⟨{x ∈ Q ∣ ∃y(y ∈ (2nd ‘A) ∧ (y +Q x) ∈ (1st ‘B))}, {x ∈ Q ∣ ∃y(y ∈ (1st ‘A) ∧ (y +Q x) ∈ (2nd ‘B))}⟩    ⇒   ⊢ ((A<P B ∧ 𝑟 ∈ Q ∧ 𝑟 ∈ (2nd ‘𝐶)) → ∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑞 ∈ (2nd ‘𝐶)))
21-Dec-2019	ltexprlemlol 6439	The lower cut of our constructed difference is lower. Lemma for ltexpri 6450. (Contributed by Jim Kingdon, 21-Dec-2019.)
⊢ 𝐶 = ⟨{x ∈ Q ∣ ∃y(y ∈ (2nd ‘A) ∧ (y +Q x) ∈ (1st ‘B))}, {x ∈ Q ∣ ∃y(y ∈ (1st ‘A) ∧ (y +Q x) ∈ (2nd ‘B))}⟩    ⇒   ⊢ ((A<P B ∧ 𝑞 ∈ Q) → (∃𝑟 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑟 ∈ (1st ‘𝐶)) → 𝑞 ∈ (1st ‘𝐶)))
21-Dec-2019	ltexprlemopl 6438	The lower cut of our constructed difference is open. Lemma for ltexpri 6450. (Contributed by Jim Kingdon, 21-Dec-2019.)
⊢ 𝐶 = ⟨{x ∈ Q ∣ ∃y(y ∈ (2nd ‘A) ∧ (y +Q x) ∈ (1st ‘B))}, {x ∈ Q ∣ ∃y(y ∈ (1st ‘A) ∧ (y +Q x) ∈ (2nd ‘B))}⟩    ⇒   ⊢ ((A<P B ∧ 𝑞 ∈ Q ∧ 𝑞 ∈ (1st ‘𝐶)) → ∃𝑟 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑟 ∈ (1st ‘𝐶)))
21-Dec-2019	ltexprlemelu 6436	Element in upper cut of the constructed difference. Lemma for ltexpri 6450. (Contributed by Jim Kingdon, 21-Dec-2019.)
⊢ 𝐶 = ⟨{x ∈ Q ∣ ∃y(y ∈ (2nd ‘A) ∧ (y +Q x) ∈ (1st ‘B))}, {x ∈ Q ∣ ∃y(y ∈ (1st ‘A) ∧ (y +Q x) ∈ (2nd ‘B))}⟩    ⇒   ⊢ (𝑟 ∈ (2nd ‘𝐶) ↔ (𝑟 ∈ Q ∧ ∃y(y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B))))
21-Dec-2019	ltexprlemell 6435	Element in lower cut of the constructed difference. Lemma for ltexpri 6450. (Contributed by Jim Kingdon, 21-Dec-2019.)
⊢ 𝐶 = ⟨{x ∈ Q ∣ ∃y(y ∈ (2nd ‘A) ∧ (y +Q x) ∈ (1st ‘B))}, {x ∈ Q ∣ ∃y(y ∈ (1st ‘A) ∧ (y +Q x) ∈ (2nd ‘B))}⟩    ⇒   ⊢ (𝑞 ∈ (1st ‘𝐶) ↔ (𝑞 ∈ Q ∧ ∃y(y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈ (1st ‘B))))
17-Dec-2019	ltexprlemru 6449	Lemma for ltexpri 6450. One direction of our result for upper cuts. (Contributed by Jim Kingdon, 17-Dec-2019.)
⊢ 𝐶 = ⟨{x ∈ Q ∣ ∃y(y ∈ (2nd ‘A) ∧ (y +Q x) ∈ (1st ‘B))}, {x ∈ Q ∣ ∃y(y ∈ (1st ‘A) ∧ (y +Q x) ∈ (2nd ‘B))}⟩    ⇒   ⊢ (A<P B → (2nd ‘B) ⊆ (2nd ‘(A +P 𝐶)))
17-Dec-2019	ltexprlemfu 6448	Lemma for ltexpri 6450. One direction of our result for upper cuts. (Contributed by Jim Kingdon, 17-Dec-2019.)
⊢ 𝐶 = ⟨{x ∈ Q ∣ ∃y(y ∈ (2nd ‘A) ∧ (y +Q x) ∈ (1st ‘B))}, {x ∈ Q ∣ ∃y(y ∈ (1st ‘A) ∧ (y +Q x) ∈ (2nd ‘B))}⟩    ⇒   ⊢ (A<P B → (2nd ‘(A +P 𝐶)) ⊆ (2nd ‘B))
17-Dec-2019	ltexprlemrl 6447	Lemma for ltexpri 6450. Reverse directon of our result for lower cuts. (Contributed by Jim Kingdon, 17-Dec-2019.)
⊢ 𝐶 = ⟨{x ∈ Q ∣ ∃y(y ∈ (2nd ‘A) ∧ (y +Q x) ∈ (1st ‘B))}, {x ∈ Q ∣ ∃y(y ∈ (1st ‘A) ∧ (y +Q x) ∈ (2nd ‘B))}⟩    ⇒   ⊢ (A<P B → (1st ‘B) ⊆ (1st ‘(A +P 𝐶)))
17-Dec-2019	ltexprlemfl 6446	Lemma for ltexpri 6450. One directon of our result for lower cuts. (Contributed by Jim Kingdon, 17-Dec-2019.)
⊢ 𝐶 = ⟨{x ∈ Q ∣ ∃y(y ∈ (2nd ‘A) ∧ (y +Q x) ∈ (1st ‘B))}, {x ∈ Q ∣ ∃y(y ∈ (1st ‘A) ∧ (y +Q x) ∈ (2nd ‘B))}⟩    ⇒   ⊢ (A<P B → (1st ‘(A +P 𝐶)) ⊆ (1st ‘B))
17-Dec-2019	ltexprlempr 6445	Our constructed difference is a positive real. Lemma for ltexpri 6450. (Contributed by Jim Kingdon, 17-Dec-2019.)
⊢ 𝐶 = ⟨{x ∈ Q ∣ ∃y(y ∈ (2nd ‘A) ∧ (y +Q x) ∈ (1st ‘B))}, {x ∈ Q ∣ ∃y(y ∈ (1st ‘A) ∧ (y +Q x) ∈ (2nd ‘B))}⟩    ⇒   ⊢ (A<P B → 𝐶 ∈ P)
17-Dec-2019	ltexprlemloc 6444	Our constructed difference is located. Lemma for ltexpri 6450. (Contributed by Jim Kingdon, 17-Dec-2019.)
⊢ 𝐶 = ⟨{x ∈ Q ∣ ∃y(y ∈ (2nd ‘A) ∧ (y +Q x) ∈ (1st ‘B))}, {x ∈ Q ∣ ∃y(y ∈ (1st ‘A) ∧ (y +Q x) ∈ (2nd ‘B))}⟩    ⇒   ⊢ (A<P B → ∀𝑞 ∈ Q ∀𝑟 ∈ Q (𝑞 <Q 𝑟 → (𝑞 ∈ (1st ‘𝐶) ∨ 𝑟 ∈ (2nd ‘𝐶))))
17-Dec-2019	ltexprlemdisj 6443	Our constructed difference is disjoint. Lemma for ltexpri 6450. (Contributed by Jim Kingdon, 17-Dec-2019.)
⊢ 𝐶 = ⟨{x ∈ Q ∣ ∃y(y ∈ (2nd ‘A) ∧ (y +Q x) ∈ (1st ‘B))}, {x ∈ Q ∣ ∃y(y ∈ (1st ‘A) ∧ (y +Q x) ∈ (2nd ‘B))}⟩    ⇒   ⊢ (A<P B → ∀𝑞 ∈ Q ¬ (𝑞 ∈ (1st ‘𝐶) ∧ 𝑞 ∈ (2nd ‘𝐶)))
17-Dec-2019	ltexprlemrnd 6442	Our constructed difference is rounded. Lemma for ltexpri 6450. (Contributed by Jim Kingdon, 17-Dec-2019.)
⊢ 𝐶 = ⟨{x ∈ Q ∣ ∃y(y ∈ (2nd ‘A) ∧ (y +Q x) ∈ (1st ‘B))}, {x ∈ Q ∣ ∃y(y ∈ (1st ‘A) ∧ (y +Q x) ∈ (2nd ‘B))}⟩    ⇒   ⊢ (A<P B → (∀𝑞 ∈ Q (𝑞 ∈ (1st ‘𝐶) ↔ ∃𝑟 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑟 ∈ (1st ‘𝐶))) ∧ ∀𝑟 ∈ Q (𝑟 ∈ (2nd ‘𝐶) ↔ ∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑞 ∈ (2nd ‘𝐶)))))
17-Dec-2019	ltexprlemm 6437	Our constructed difference is inhabited. Lemma for ltexpri 6450. (Contributed by Jim Kingdon, 17-Dec-2019.)
⊢ 𝐶 = ⟨{x ∈ Q ∣ ∃y(y ∈ (2nd ‘A) ∧ (y +Q x) ∈ (1st ‘B))}, {x ∈ Q ∣ ∃y(y ∈ (1st ‘A) ∧ (y +Q x) ∈ (2nd ‘B))}⟩    ⇒   ⊢ (A<P B → (∃𝑞 ∈ Q 𝑞 ∈ (1st ‘𝐶) ∧ ∃𝑟 ∈ Q 𝑟 ∈ (2nd ‘𝐶)))
16-Dec-2019	bj-sbime 7020	A strengthening of sbie 1656 (same proof). (Contributed by BJ, 16-Dec-2019.)
⊢ Ⅎxψ    &   ⊢ (x = y → (φ → ψ))    ⇒   ⊢ ([y / x]φ → ψ)
16-Dec-2019	bj-sbimeh 7019	A strengthening of sbieh 1655 (same proof). (Contributed by BJ, 16-Dec-2019.)
⊢ (ψ → ∀xψ)    &   ⊢ (x = y → (φ → ψ))    ⇒   ⊢ ([y / x]φ → ψ)
16-Dec-2019	bj-sbimedh 7018	A strengthening of sbiedh 1652 (same proof). (Contributed by BJ, 16-Dec-2019.)
⊢ (φ → ∀xφ)    &   ⊢ (φ → (χ → ∀xχ))    &   ⊢ (φ → (x = y → (ψ → χ)))    ⇒   ⊢ (φ → ([y / x]ψ → χ))
16-Dec-2019	ltsopr 6433	Positive real 'less than' is a weak linear order (in the sense of df-iso 4008). Proposition 11.2.3 of [HoTT], p. (varies). (Contributed by Jim Kingdon, 16-Dec-2019.)
⊢ <P Or P
15-Dec-2019	ltpopr 6432	Positive real 'less than' is a partial ordering. Remark ("< is transitive and irreflexive") preceding Proposition 11.2.3 of [HoTT], p. (varies). Lemma for ltsopr 6433. (Contributed by Jim Kingdon, 15-Dec-2019.)
⊢ <P Po P
15-Dec-2019	ltdfpr 6360	More convenient form of df-iltp 6324. (Contributed by Jim Kingdon, 15-Dec-2019.)
⊢ ((A ∈ P ∧ B ∈ P) → (A<P B ↔ ∃𝑞 ∈ Q (𝑞 ∈ (2nd ‘A) ∧ 𝑞 ∈ (1st ‘B))))
15-Dec-2019	prdisj 6346	A Dedekind cut is disjoint. (Contributed by Jim Kingdon, 15-Dec-2019.)
⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ A ∈ Q) → ¬ (A ∈ 𝐿 ∧ A ∈ 𝑈))
13-Dec-2019	1idpru 6430	Lemma for 1idpr 6431. (Contributed by Jim Kingdon, 13-Dec-2019.)
⊢ (A ∈ P → (2nd ‘(A ·P 1P)) = (2nd ‘A))
13-Dec-2019	1idprl 6429	Lemma for 1idpr 6431. (Contributed by Jim Kingdon, 13-Dec-2019.)
⊢ (A ∈ P → (1st ‘(A ·P 1P)) = (1st ‘A))
13-Dec-2019	gtnqex 6403	The class of rationals greater than a given rational is a set. (Contributed by Jim Kingdon, 13-Dec-2019.)
⊢ {x ∣ A <Q x} ∈ V
13-Dec-2019	ltnqex 6402	The class of rationals less than a given rational is a set. (Contributed by Jim Kingdon, 13-Dec-2019.)
⊢ {x ∣ x <Q A} ∈ V
13-Dec-2019	sotritrieq 4036	A trichotomy relationship, given a trichotomous order. (Contributed by Jim Kingdon, 13-Dec-2019.)
⊢ 𝑅 Or A    &   ⊢ ((B ∈ A ∧ 𝐶 ∈ A) → (B𝑅𝐶 ∨ B = 𝐶 ∨ 𝐶𝑅B))    ⇒   ⊢ ((B ∈ A ∧ 𝐶 ∈ A) → (B = 𝐶 ↔ ¬ (B𝑅𝐶 ∨ 𝐶𝑅B)))
12-Dec-2019	distrprg 6427	Multiplication of positive reals is distributive. Proposition 9-3.7(iii) of [Gleason] p. 124. (Contributed by Jim Kingdon, 12-Dec-2019.)
⊢ ((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) → (A ·P (B +P 𝐶)) = ((A ·P B) +P (A ·P 𝐶)))
12-Dec-2019	distrlem5pru 6426	Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.)
⊢ ((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) → (2nd ‘((A ·P B) +P (A ·P 𝐶))) ⊆ (2nd ‘(A ·P (B +P 𝐶))))
12-Dec-2019	distrlem5prl 6425	Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.)
⊢ ((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) → (1st ‘((A ·P B) +P (A ·P 𝐶))) ⊆ (1st ‘(A ·P (B +P 𝐶))))
12-Dec-2019	distrlem4pru 6424	Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.)
⊢ (((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) ∧ ((x ∈ (2nd ‘A) ∧ y ∈ (2nd ‘B)) ∧ (f ∈ (2nd ‘A) ∧ z ∈ (2nd ‘𝐶)))) → ((x ·Q y) +Q (f ·Q z)) ∈ (2nd ‘(A ·P (B +P 𝐶))))
12-Dec-2019	distrlem4prl 6423	Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.)
⊢ (((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) ∧ ((x ∈ (1st ‘A) ∧ y ∈ (1st ‘B)) ∧ (f ∈ (1st ‘A) ∧ z ∈ (1st ‘𝐶)))) → ((x ·Q y) +Q (f ·Q z)) ∈ (1st ‘(A ·P (B +P 𝐶))))
12-Dec-2019	distrlem1pru 6422	Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.)
⊢ ((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) → (2nd ‘(A ·P (B +P 𝐶))) ⊆ (2nd ‘((A ·P B) +P (A ·P 𝐶))))