Intuitionistic Logic Explorer Home Intuitionistic Logic Explorer
Most Recent Proofs
 
Mirrors  >  Home  >  ILE Home  >  Th. List  >  Recent MPE Most Recent             Other  >  MM 100

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.

Color key:   Intuitionistic Logic Explorer  Intuitionistic Logic Explorer   User Mathboxes  User Mathboxes  

Last updated on 21-Jan-2020 at 12:30 AM ET.
Recent Additions to the Intuitionistic Logic Explorer
DateLabelDescription
Theorem
 
17-Jan-2020addcom 6737 Addition commutes. (Contributed by Jim Kingdon, 17-Jan-2020.)
((A B ℂ) → (A + B) = (B + A))
 
17-Jan-2020ax-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-2020axaddcom 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-2020addid1 6738 0 is an additive identity. (Contributed by Jim Kingdon, 16-Jan-2020.)
(A ℂ → (A + 0) = A)
 
16-Jan-2020ax-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-2020ax0id 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-2020axltwlin 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-2020axltirr 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-20202pwuninelg 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-20201re 6628 1 is a real number. (Contributed by Jim Kingdon, 13-Jan-2020.)
1
 
13-Jan-2020ax-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-2020ax1re 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-2020ax-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-2020ax-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-2020ax-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-2020ax-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-2020axpre-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-2020axpre-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-2020axprecex 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-2020ax0lt1 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-2020ecidg 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-20201idsr 6515 1 is an identity element for multiplication. (Contributed by Jim Kingdon, 5-Jan-2020.)
(A R → (A ·R 1R) = A)
 
4-Jan-2020distrsrg 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-2020mulasssrg 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-2020mulcomsrg 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-2020addasssrg 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-2020addcomsrg 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-2020caovlem2d 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-2020bj-d0clsepcl 7148 Δ0-classical logic and separation implies classical logic. (Contributed by BJ, 2-Jan-2020.) (Proof modification is discouraged.)
(φ ¬ φ)
 
2-Jan-2020ax-bj-d0cl 7147 Axiom for Δ0-classical logic. (Contributed by BJ, 2-Jan-2020.)
BOUNDED φ       (φ ¬ φ)
 
1-Jan-2020mulcmpblnrlemg 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-2019eceq1d 6053 Equality theorem for equivalence class (deduction form). (Contributed by Jim Kingdon, 31-Dec-2019.)
(φA = B)       (φ → [A]𝐶 = [B]𝐶)
 
30-Dec-2019mulsrmo 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 )) → ∃*zwvu𝑡((A = [⟨w, v⟩] ~R B = [⟨u, 𝑡⟩] ~R ) z = [⟨((w ·P u) +P (v ·P 𝑡)), ((w ·P 𝑡) +P (v ·P u))⟩] ~R ))
 
30-Dec-2019addsrmo 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 )) → ∃*zwvu𝑡((A = [⟨w, v⟩] ~R B = [⟨u, 𝑡⟩] ~R ) z = [⟨(w +P u), (v +P 𝑡)⟩] ~R ))
 
30-Dec-2019prsrlem1 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-2019bj-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-2019bj-omord 7180 The set 𝜔 is an ordinal. (Contributed by BJ, 29-Dec-2019.) (Proof modification is discouraged.)
Ord 𝜔
 
29-Dec-2019bj-omtrans2 7179 The set 𝜔 is transitive. (Contributed by BJ, 29-Dec-2019.) (Proof modification is discouraged.)
Tr 𝜔
 
29-Dec-2019bj-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-2019ltrnqg 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 ↔ (*QB) <Q (*QA)))
 
29-Dec-2019rec1nq 6254 Reciprocal of positive fraction one. (Contributed by Jim Kingdon, 29-Dec-2019.)
(*Q‘1Q) = 1Q
 
28-Dec-2019recexprlemupu 6462 The upper cut of B is upper. Lemma for recexpr 6472. (Contributed by Jim Kingdon, 28-Dec-2019.)
B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩       ((A P 𝑟 Q) → (𝑞 Q (𝑞 <Q 𝑟 𝑞 (2ndB)) → 𝑟 (2ndB)))
 
28-Dec-2019recexprlemopu 6461 The upper cut of B is open. Lemma for recexpr 6472. (Contributed by Jim Kingdon, 28-Dec-2019.)
B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩       ((A P 𝑟 Q 𝑟 (2ndB)) → 𝑞 Q (𝑞 <Q 𝑟 𝑞 (2ndB)))
 
28-Dec-2019recexprlemlol 6460 The lower cut of B is lower. Lemma for recexpr 6472. (Contributed by Jim Kingdon, 28-Dec-2019.)
B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩       ((A P 𝑞 Q) → (𝑟 Q (𝑞 <Q 𝑟 𝑟 (1stB)) → 𝑞 (1stB)))
 
28-Dec-2019recexprlemopl 6459 The lower cut of B is open. Lemma for recexpr 6472. (Contributed by Jim Kingdon, 28-Dec-2019.)
B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩       ((A P 𝑞 Q 𝑞 (1stB)) → 𝑟 Q (𝑞 <Q 𝑟 𝑟 (1stB)))
 
28-Dec-2019prmuloc2 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-20191pru 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-20191prl 6405 The lower cut of the positive real number 'one'. (Contributed by Jim Kingdon, 28-Dec-2019.)
(1st ‘1P) = {xx <Q 1Q}
 
27-Dec-2019recexprlemex 6471 B is the reciprocal of A. Lemma for recexpr 6472. (Contributed by Jim Kingdon, 27-Dec-2019.)
B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩       (A P → (A ·P B) = 1P)
 
27-Dec-2019recexprlemss1u 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 = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩       (A P → (2nd ‘(A ·P B)) ⊆ (2nd ‘1P))
 
27-Dec-2019recexprlemss1l 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 = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩       (A P → (1st ‘(A ·P B)) ⊆ (1st ‘1P))
 
27-Dec-2019recexprlem1ssu 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 = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩       (A P → (2nd ‘1P) ⊆ (2nd ‘(A ·P B)))
 
27-Dec-2019recexprlem1ssl 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 = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩       (A P → (1st ‘1P) ⊆ (1st ‘(A ·P B)))
 
27-Dec-2019recexprlempr 6466 B is a positive real. Lemma for recexpr 6472. (Contributed by Jim Kingdon, 27-Dec-2019.)
B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩       (A PB P)
 
27-Dec-2019recexprlemloc 6465 B is located. Lemma for recexpr 6472. (Contributed by Jim Kingdon, 27-Dec-2019.)
B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩       (A P𝑞 Q 𝑟 Q (𝑞 <Q 𝑟 → (𝑞 (1stB) 𝑟 (2ndB))))
 
27-Dec-2019recexprlemdisj 6464 B is disjoint. Lemma for recexpr 6472. (Contributed by Jim Kingdon, 27-Dec-2019.)
B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩       (A P𝑞 Q ¬ (𝑞 (1stB) 𝑞 (2ndB)))
 
27-Dec-2019recexprlemrnd 6463 B is rounded. Lemma for recexpr 6472. (Contributed by Jim Kingdon, 27-Dec-2019.)
B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩       (A P → (𝑞 Q (𝑞 (1stB) ↔ 𝑟 Q (𝑞 <Q 𝑟 𝑟 (1stB))) 𝑟 Q (𝑟 (2ndB) ↔ 𝑞 Q (𝑞 <Q 𝑟 𝑞 (2ndB)))))
 
27-Dec-2019recexprlemm 6458 B is inhabited. Lemma for recexpr 6472. (Contributed by Jim Kingdon, 27-Dec-2019.)
B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩       (A P → (𝑞 Q 𝑞 (1stB) 𝑟 Q 𝑟 (2ndB)))
 
27-Dec-2019recexprlemelu 6457 Membership in the upper cut of B. Lemma for recexpr 6472. (Contributed by Jim Kingdon, 27-Dec-2019.)
B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩       (𝐶 (2ndB) ↔ y(y <Q 𝐶 (*Qy) (1stA)))
 
27-Dec-2019recexprlemell 6456 Membership in the lower cut of B. Lemma for recexpr 6472. (Contributed by Jim Kingdon, 27-Dec-2019.)
B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩       (𝐶 (1stB) ↔ y(𝐶 <Q y (*Qy) (2ndA)))
 
26-Dec-2019ltaprg 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-2019prarloc2 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-2019addcanprlemu 6452 Lemma for addcanprg 6453. (Contributed by Jim Kingdon, 25-Dec-2019.)
(((A P B P 𝐶 P) (A +P B) = (A +P 𝐶)) → (2ndB) ⊆ (2nd𝐶))
 
25-Dec-2019addcanprleml 6451 Lemma for addcanprg 6453. (Contributed by Jim Kingdon, 25-Dec-2019.)
(((A P B P 𝐶 P) (A +P B) = (A +P 𝐶)) → (1stB) ⊆ (1st𝐶))
 
24-Dec-2019addcanprg 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-2019ltprordil 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 → (1stA) ⊆ (1stB))
 
22-Dec-2019bj-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-2019ltexprlemupu 6441 The upper cut of our constructed difference is upper. Lemma for ltexpri 6450. (Contributed by Jim Kingdon, 21-Dec-2019.)
𝐶 = ⟨{x Qy(y (2ndA) (y +Q x) (1stB))}, {x Qy(y (1stA) (y +Q x) (2ndB))}⟩       ((A<P B 𝑟 Q) → (𝑞 Q (𝑞 <Q 𝑟 𝑞 (2nd𝐶)) → 𝑟 (2nd𝐶)))
 
21-Dec-2019ltexprlemopu 6440 The upper cut of our constructed difference is open. Lemma for ltexpri 6450. (Contributed by Jim Kingdon, 21-Dec-2019.)
𝐶 = ⟨{x Qy(y (2ndA) (y +Q x) (1stB))}, {x Qy(y (1stA) (y +Q x) (2ndB))}⟩       ((A<P B 𝑟 Q 𝑟 (2nd𝐶)) → 𝑞 Q (𝑞 <Q 𝑟 𝑞 (2nd𝐶)))
 
21-Dec-2019ltexprlemlol 6439 The lower cut of our constructed difference is lower. Lemma for ltexpri 6450. (Contributed by Jim Kingdon, 21-Dec-2019.)
𝐶 = ⟨{x Qy(y (2ndA) (y +Q x) (1stB))}, {x Qy(y (1stA) (y +Q x) (2ndB))}⟩       ((A<P B 𝑞 Q) → (𝑟 Q (𝑞 <Q 𝑟 𝑟 (1st𝐶)) → 𝑞 (1st𝐶)))
 
21-Dec-2019ltexprlemopl 6438 The lower cut of our constructed difference is open. Lemma for ltexpri 6450. (Contributed by Jim Kingdon, 21-Dec-2019.)
𝐶 = ⟨{x Qy(y (2ndA) (y +Q x) (1stB))}, {x Qy(y (1stA) (y +Q x) (2ndB))}⟩       ((A<P B 𝑞 Q 𝑞 (1st𝐶)) → 𝑟 Q (𝑞 <Q 𝑟 𝑟 (1st𝐶)))
 
21-Dec-2019ltexprlemelu 6436 Element in upper cut of the constructed difference. Lemma for ltexpri 6450. (Contributed by Jim Kingdon, 21-Dec-2019.)
𝐶 = ⟨{x Qy(y (2ndA) (y +Q x) (1stB))}, {x Qy(y (1stA) (y +Q x) (2ndB))}⟩       (𝑟 (2nd𝐶) ↔ (𝑟 Q y(y (1stA) (y +Q 𝑟) (2ndB))))
 
21-Dec-2019ltexprlemell 6435 Element in lower cut of the constructed difference. Lemma for ltexpri 6450. (Contributed by Jim Kingdon, 21-Dec-2019.)
𝐶 = ⟨{x Qy(y (2ndA) (y +Q x) (1stB))}, {x Qy(y (1stA) (y +Q x) (2ndB))}⟩       (𝑞 (1st𝐶) ↔ (𝑞 Q y(y (2ndA) (y +Q 𝑞) (1stB))))
 
17-Dec-2019ltexprlemru 6449 Lemma for ltexpri 6450. One direction of our result for upper cuts. (Contributed by Jim Kingdon, 17-Dec-2019.)
𝐶 = ⟨{x Qy(y (2ndA) (y +Q x) (1stB))}, {x Qy(y (1stA) (y +Q x) (2ndB))}⟩       (A<P B → (2ndB) ⊆ (2nd ‘(A +P 𝐶)))
 
17-Dec-2019ltexprlemfu 6448 Lemma for ltexpri 6450. One direction of our result for upper cuts. (Contributed by Jim Kingdon, 17-Dec-2019.)
𝐶 = ⟨{x Qy(y (2ndA) (y +Q x) (1stB))}, {x Qy(y (1stA) (y +Q x) (2ndB))}⟩       (A<P B → (2nd ‘(A +P 𝐶)) ⊆ (2ndB))
 
17-Dec-2019ltexprlemrl 6447 Lemma for ltexpri 6450. Reverse directon of our result for lower cuts. (Contributed by Jim Kingdon, 17-Dec-2019.)
𝐶 = ⟨{x Qy(y (2ndA) (y +Q x) (1stB))}, {x Qy(y (1stA) (y +Q x) (2ndB))}⟩       (A<P B → (1stB) ⊆ (1st ‘(A +P 𝐶)))
 
17-Dec-2019ltexprlemfl 6446 Lemma for ltexpri 6450. One directon of our result for lower cuts. (Contributed by Jim Kingdon, 17-Dec-2019.)
𝐶 = ⟨{x Qy(y (2ndA) (y +Q x) (1stB))}, {x Qy(y (1stA) (y +Q x) (2ndB))}⟩       (A<P B → (1st ‘(A +P 𝐶)) ⊆ (1stB))
 
17-Dec-2019ltexprlempr 6445 Our constructed difference is a positive real. Lemma for ltexpri 6450. (Contributed by Jim Kingdon, 17-Dec-2019.)
𝐶 = ⟨{x Qy(y (2ndA) (y +Q x) (1stB))}, {x Qy(y (1stA) (y +Q x) (2ndB))}⟩       (A<P B𝐶 P)
 
17-Dec-2019ltexprlemloc 6444 Our constructed difference is located. Lemma for ltexpri 6450. (Contributed by Jim Kingdon, 17-Dec-2019.)
𝐶 = ⟨{x Qy(y (2ndA) (y +Q x) (1stB))}, {x Qy(y (1stA) (y +Q x) (2ndB))}⟩       (A<P B𝑞 Q 𝑟 Q (𝑞 <Q 𝑟 → (𝑞 (1st𝐶) 𝑟 (2nd𝐶))))
 
17-Dec-2019ltexprlemdisj 6443 Our constructed difference is disjoint. Lemma for ltexpri 6450. (Contributed by Jim Kingdon, 17-Dec-2019.)
𝐶 = ⟨{x Qy(y (2ndA) (y +Q x) (1stB))}, {x Qy(y (1stA) (y +Q x) (2ndB))}⟩       (A<P B𝑞 Q ¬ (𝑞 (1st𝐶) 𝑞 (2nd𝐶)))
 
17-Dec-2019ltexprlemrnd 6442 Our constructed difference is rounded. Lemma for ltexpri 6450. (Contributed by Jim Kingdon, 17-Dec-2019.)
𝐶 = ⟨{x Qy(y (2ndA) (y +Q x) (1stB))}, {x Qy(y (1stA) (y +Q x) (2ndB))}⟩       (A<P B → (𝑞 Q (𝑞 (1st𝐶) ↔ 𝑟 Q (𝑞 <Q 𝑟 𝑟 (1st𝐶))) 𝑟 Q (𝑟 (2nd𝐶) ↔ 𝑞 Q (𝑞 <Q 𝑟 𝑞 (2nd𝐶)))))
 
17-Dec-2019ltexprlemm 6437 Our constructed difference is inhabited. Lemma for ltexpri 6450. (Contributed by Jim Kingdon, 17-Dec-2019.)
𝐶 = ⟨{x Qy(y (2ndA) (y +Q x) (1stB))}, {x Qy(y (1stA) (y +Q x) (2ndB))}⟩       (A<P B → (𝑞 Q 𝑞 (1st𝐶) 𝑟 Q 𝑟 (2nd𝐶)))
 
16-Dec-2019bj-sbime 7020 A strengthening of sbie 1656 (same proof). (Contributed by BJ, 16-Dec-2019.)
xψ    &   (x = y → (φψ))       ([y / x]φψ)
 
16-Dec-2019bj-sbimeh 7019 A strengthening of sbieh 1655 (same proof). (Contributed by BJ, 16-Dec-2019.)
(ψxψ)    &   (x = y → (φψ))       ([y / x]φψ)
 
16-Dec-2019bj-sbimedh 7018 A strengthening of sbiedh 1652 (same proof). (Contributed by BJ, 16-Dec-2019.)
(φxφ)    &   (φ → (χxχ))    &   (φ → (x = y → (ψχ)))       (φ → ([y / x]ψχ))
 
16-Dec-2019ltsopr 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-2019ltpopr 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-2019ltdfpr 6360 More convenient form of df-iltp 6324. (Contributed by Jim Kingdon, 15-Dec-2019.)
((A P B P) → (A<P B𝑞 Q (𝑞 (2ndA) 𝑞 (1stB))))
 
15-Dec-2019prdisj 6346 A Dedekind cut is disjoint. (Contributed by Jim Kingdon, 15-Dec-2019.)
((⟨𝐿, 𝑈 P A Q) → ¬ (A 𝐿 A 𝑈))
 
13-Dec-20191idpru 6430 Lemma for 1idpr 6431. (Contributed by Jim Kingdon, 13-Dec-2019.)
(A P → (2nd ‘(A ·P 1P)) = (2ndA))
 
13-Dec-20191idprl 6429 Lemma for 1idpr 6431. (Contributed by Jim Kingdon, 13-Dec-2019.)
(A P → (1st ‘(A ·P 1P)) = (1stA))
 
13-Dec-2019gtnqex 6403 The class of rationals greater than a given rational is a set. (Contributed by Jim Kingdon, 13-Dec-2019.)
{xA <Q x} V
 
13-Dec-2019ltnqex 6402 The class of rationals less than a given rational is a set. (Contributed by Jim Kingdon, 13-Dec-2019.)
{xx <Q A} V
 
13-Dec-2019sotritrieq 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-2019distrprg 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-2019distrlem5pru 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-2019distrlem5prl 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-2019distrlem4pru 6424 Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.)
(((A P B P 𝐶 P) ((x (2ndA) y (2ndB)) (f (2ndA) z (2nd𝐶)))) → ((x ·Q y) +Q (f ·Q z)) (2nd ‘(A ·P (B +P 𝐶))))
 
12-Dec-2019distrlem4prl 6423 Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.)
(((A P B P 𝐶 P) ((x (1stA) y (1stB)) (f (1stA) z (1st𝐶)))) → ((x ·Q y) +Q (f ·Q z)) (1st ‘(A ·P (B +P 𝐶))))
 
12-Dec-2019distrlem1pru 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 𝐶))))

  Copyright terms: Public domain W3C HTML validation [external]