Intuitionistic Logic Explorer Most Recent Proofs |
||
Mirrors > Home > ILE Home > Th. List > Recent | MPE Most Recent Other > MM 100 |
See the MPE Most Recent Proofs page for news and some useful links.
Color key: | Intuitionistic Logic Explorer | User Mathboxes |
Date | Label | Description |
---|---|---|
Theorem | ||
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} 1_{R}) = 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}‘1_{Q}) = 1_{Q} | ||
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) ∈ (2^{nd} ‘A))}, {x ∣ ∃y(y <_{Q} x ∧ (*_{Q}‘y) ∈ (1^{st} ‘A))}⟩ ⇒ ⊢ ((A ∈ P ∧ 𝑟 ∈ Q) → (∃𝑞 ∈ Q (𝑞 <_{Q} 𝑟 ∧ 𝑞 ∈ (2^{nd} ‘B)) → 𝑟 ∈ (2^{nd} ‘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) ∈ (2^{nd} ‘A))}, {x ∣ ∃y(y <_{Q} x ∧ (*_{Q}‘y) ∈ (1^{st} ‘A))}⟩ ⇒ ⊢ ((A ∈ P ∧ 𝑟 ∈ Q ∧ 𝑟 ∈ (2^{nd} ‘B)) → ∃𝑞 ∈ Q (𝑞 <_{Q} 𝑟 ∧ 𝑞 ∈ (2^{nd} ‘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) ∈ (2^{nd} ‘A))}, {x ∣ ∃y(y <_{Q} x ∧ (*_{Q}‘y) ∈ (1^{st} ‘A))}⟩ ⇒ ⊢ ((A ∈ P ∧ 𝑞 ∈ Q) → (∃𝑟 ∈ Q (𝑞 <_{Q} 𝑟 ∧ 𝑟 ∈ (1^{st} ‘B)) → 𝑞 ∈ (1^{st} ‘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) ∈ (2^{nd} ‘A))}, {x ∣ ∃y(y <_{Q} x ∧ (*_{Q}‘y) ∈ (1^{st} ‘A))}⟩ ⇒ ⊢ ((A ∈ P ∧ 𝑞 ∈ Q ∧ 𝑞 ∈ (1^{st} ‘B)) → ∃𝑟 ∈ Q (𝑞 <_{Q} 𝑟 ∧ 𝑟 ∈ (1^{st} ‘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 ∧ 1_{Q} <_{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.) |
⊢ (2^{nd} ‘1_{P}) = {x ∣ 1_{Q} <_{Q} x} | ||
28-Dec-2019 | 1prl 6405 | The lower cut of the positive real number 'one'. (Contributed by Jim Kingdon, 28-Dec-2019.) |
⊢ (1^{st} ‘1_{P}) = {x ∣ x <_{Q} 1_{Q}} | ||
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) ∈ (2^{nd} ‘A))}, {x ∣ ∃y(y <_{Q} x ∧ (*_{Q}‘y) ∈ (1^{st} ‘A))}⟩ ⇒ ⊢ (A ∈ P → (A ·_{P} B) = 1_{P}) | ||
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) ∈ (2^{nd} ‘A))}, {x ∣ ∃y(y <_{Q} x ∧ (*_{Q}‘y) ∈ (1^{st} ‘A))}⟩ ⇒ ⊢ (A ∈ P → (2^{nd} ‘(A ·_{P} B)) ⊆ (2^{nd} ‘1_{P})) | ||
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) ∈ (2^{nd} ‘A))}, {x ∣ ∃y(y <_{Q} x ∧ (*_{Q}‘y) ∈ (1^{st} ‘A))}⟩ ⇒ ⊢ (A ∈ P → (1^{st} ‘(A ·_{P} B)) ⊆ (1^{st} ‘1_{P})) | ||
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) ∈ (2^{nd} ‘A))}, {x ∣ ∃y(y <_{Q} x ∧ (*_{Q}‘y) ∈ (1^{st} ‘A))}⟩ ⇒ ⊢ (A ∈ P → (2^{nd} ‘1_{P}) ⊆ (2^{nd} ‘(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) ∈ (2^{nd} ‘A))}, {x ∣ ∃y(y <_{Q} x ∧ (*_{Q}‘y) ∈ (1^{st} ‘A))}⟩ ⇒ ⊢ (A ∈ P → (1^{st} ‘1_{P}) ⊆ (1^{st} ‘(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) ∈ (2^{nd} ‘A))}, {x ∣ ∃y(y <_{Q} x ∧ (*_{Q}‘y) ∈ (1^{st} ‘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) ∈ (2^{nd} ‘A))}, {x ∣ ∃y(y <_{Q} x ∧ (*_{Q}‘y) ∈ (1^{st} ‘A))}⟩ ⇒ ⊢ (A ∈ P → ∀𝑞 ∈ Q ∀𝑟 ∈ Q (𝑞 <_{Q} 𝑟 → (𝑞 ∈ (1^{st} ‘B) ∨ 𝑟 ∈ (2^{nd} ‘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) ∈ (2^{nd} ‘A))}, {x ∣ ∃y(y <_{Q} x ∧ (*_{Q}‘y) ∈ (1^{st} ‘A))}⟩ ⇒ ⊢ (A ∈ P → ∀𝑞 ∈ Q ¬ (𝑞 ∈ (1^{st} ‘B) ∧ 𝑞 ∈ (2^{nd} ‘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) ∈ (2^{nd} ‘A))}, {x ∣ ∃y(y <_{Q} x ∧ (*_{Q}‘y) ∈ (1^{st} ‘A))}⟩ ⇒ ⊢ (A ∈ P → (∀𝑞 ∈ Q (𝑞 ∈ (1^{st} ‘B) ↔ ∃𝑟 ∈ Q (𝑞 <_{Q} 𝑟 ∧ 𝑟 ∈ (1^{st} ‘B))) ∧ ∀𝑟 ∈ Q (𝑟 ∈ (2^{nd} ‘B) ↔ ∃𝑞 ∈ Q (𝑞 <_{Q} 𝑟 ∧ 𝑞 ∈ (2^{nd} ‘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) ∈ (2^{nd} ‘A))}, {x ∣ ∃y(y <_{Q} x ∧ (*_{Q}‘y) ∈ (1^{st} ‘A))}⟩ ⇒ ⊢ (A ∈ P → (∃𝑞 ∈ Q 𝑞 ∈ (1^{st} ‘B) ∧ ∃𝑟 ∈ Q 𝑟 ∈ (2^{nd} ‘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) ∈ (2^{nd} ‘A))}, {x ∣ ∃y(y <_{Q} x ∧ (*_{Q}‘y) ∈ (1^{st} ‘A))}⟩ ⇒ ⊢ (𝐶 ∈ (2^{nd} ‘B) ↔ ∃y(y <_{Q} 𝐶 ∧ (*_{Q}‘y) ∈ (1^{st} ‘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) ∈ (2^{nd} ‘A))}, {x ∣ ∃y(y <_{Q} x ∧ (*_{Q}‘y) ∈ (1^{st} ‘A))}⟩ ⇒ ⊢ (𝐶 ∈ (1^{st} ‘B) ↔ ∃y(𝐶 <_{Q} y ∧ (*_{Q}‘y) ∈ (2^{nd} ‘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} 𝐶)) → (2^{nd} ‘B) ⊆ (2^{nd} ‘𝐶)) | ||
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} 𝐶)) → (1^{st} ‘B) ⊆ (1^{st} ‘𝐶)) | ||
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 → (1^{st} ‘A) ⊆ (1^{st} ‘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 ∈ (2^{nd} ‘A) ∧ (y +_{Q} x) ∈ (1^{st} ‘B))}, {x ∈ Q ∣ ∃y(y ∈ (1^{st} ‘A) ∧ (y +_{Q} x) ∈ (2^{nd} ‘B))}⟩ ⇒ ⊢ ((A<_{P} B ∧ 𝑟 ∈ Q) → (∃𝑞 ∈ Q (𝑞 <_{Q} 𝑟 ∧ 𝑞 ∈ (2^{nd} ‘𝐶)) → 𝑟 ∈ (2^{nd} ‘𝐶))) | ||
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 ∈ (2^{nd} ‘A) ∧ (y +_{Q} x) ∈ (1^{st} ‘B))}, {x ∈ Q ∣ ∃y(y ∈ (1^{st} ‘A) ∧ (y +_{Q} x) ∈ (2^{nd} ‘B))}⟩ ⇒ ⊢ ((A<_{P} B ∧ 𝑟 ∈ Q ∧ 𝑟 ∈ (2^{nd} ‘𝐶)) → ∃𝑞 ∈ Q (𝑞 <_{Q} 𝑟 ∧ 𝑞 ∈ (2^{nd} ‘𝐶))) | ||
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 ∈ (2^{nd} ‘A) ∧ (y +_{Q} x) ∈ (1^{st} ‘B))}, {x ∈ Q ∣ ∃y(y ∈ (1^{st} ‘A) ∧ (y +_{Q} x) ∈ (2^{nd} ‘B))}⟩ ⇒ ⊢ ((A<_{P} B ∧ 𝑞 ∈ Q) → (∃𝑟 ∈ Q (𝑞 <_{Q} 𝑟 ∧ 𝑟 ∈ (1^{st} ‘𝐶)) → 𝑞 ∈ (1^{st} ‘𝐶))) | ||
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 ∈ (2^{nd} ‘A) ∧ (y +_{Q} x) ∈ (1^{st} ‘B))}, {x ∈ Q ∣ ∃y(y ∈ (1^{st} ‘A) ∧ (y +_{Q} x) ∈ (2^{nd} ‘B))}⟩ ⇒ ⊢ ((A<_{P} B ∧ 𝑞 ∈ Q ∧ 𝑞 ∈ (1^{st} ‘𝐶)) → ∃𝑟 ∈ Q (𝑞 <_{Q} 𝑟 ∧ 𝑟 ∈ (1^{st} ‘𝐶))) | ||
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 ∈ (2^{nd} ‘A) ∧ (y +_{Q} x) ∈ (1^{st} ‘B))}, {x ∈ Q ∣ ∃y(y ∈ (1^{st} ‘A) ∧ (y +_{Q} x) ∈ (2^{nd} ‘B))}⟩ ⇒ ⊢ (𝑟 ∈ (2^{nd} ‘𝐶) ↔ (𝑟 ∈ Q ∧ ∃y(y ∈ (1^{st} ‘A) ∧ (y +_{Q} 𝑟) ∈ (2^{nd} ‘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 ∈ (2^{nd} ‘A) ∧ (y +_{Q} x) ∈ (1^{st} ‘B))}, {x ∈ Q ∣ ∃y(y ∈ (1^{st} ‘A) ∧ (y +_{Q} x) ∈ (2^{nd} ‘B))}⟩ ⇒ ⊢ (𝑞 ∈ (1^{st} ‘𝐶) ↔ (𝑞 ∈ Q ∧ ∃y(y ∈ (2^{nd} ‘A) ∧ (y +_{Q} 𝑞) ∈ (1^{st} ‘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 ∈ (2^{nd} ‘A) ∧ (y +_{Q} x) ∈ (1^{st} ‘B))}, {x ∈ Q ∣ ∃y(y ∈ (1^{st} ‘A) ∧ (y +_{Q} x) ∈ (2^{nd} ‘B))}⟩ ⇒ ⊢ (A<_{P} B → (2^{nd} ‘B) ⊆ (2^{nd} ‘(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 ∈ (2^{nd} ‘A) ∧ (y +_{Q} x) ∈ (1^{st} ‘B))}, {x ∈ Q ∣ ∃y(y ∈ (1^{st} ‘A) ∧ (y +_{Q} x) ∈ (2^{nd} ‘B))}⟩ ⇒ ⊢ (A<_{P} B → (2^{nd} ‘(A +_{P} 𝐶)) ⊆ (2^{nd} ‘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 ∈ (2^{nd} ‘A) ∧ (y +_{Q} x) ∈ (1^{st} ‘B))}, {x ∈ Q ∣ ∃y(y ∈ (1^{st} ‘A) ∧ (y +_{Q} x) ∈ (2^{nd} ‘B))}⟩ ⇒ ⊢ (A<_{P} B → (1^{st} ‘B) ⊆ (1^{st} ‘(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 ∈ (2^{nd} ‘A) ∧ (y +_{Q} x) ∈ (1^{st} ‘B))}, {x ∈ Q ∣ ∃y(y ∈ (1^{st} ‘A) ∧ (y +_{Q} x) ∈ (2^{nd} ‘B))}⟩ ⇒ ⊢ (A<_{P} B → (1^{st} ‘(A +_{P} 𝐶)) ⊆ (1^{st} ‘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 ∈ (2^{nd} ‘A) ∧ (y +_{Q} x) ∈ (1^{st} ‘B))}, {x ∈ Q ∣ ∃y(y ∈ (1^{st} ‘A) ∧ (y +_{Q} x) ∈ (2^{nd} ‘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 ∈ (2^{nd} ‘A) ∧ (y +_{Q} x) ∈ (1^{st} ‘B))}, {x ∈ Q ∣ ∃y(y ∈ (1^{st} ‘A) ∧ (y +_{Q} x) ∈ (2^{nd} ‘B))}⟩ ⇒ ⊢ (A<_{P} B → ∀𝑞 ∈ Q ∀𝑟 ∈ Q (𝑞 <_{Q} 𝑟 → (𝑞 ∈ (1^{st} ‘𝐶) ∨ 𝑟 ∈ (2^{nd} ‘𝐶)))) | ||
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 ∈ (2^{nd} ‘A) ∧ (y +_{Q} x) ∈ (1^{st} ‘B))}, {x ∈ Q ∣ ∃y(y ∈ (1^{st} ‘A) ∧ (y +_{Q} x) ∈ (2^{nd} ‘B))}⟩ ⇒ ⊢ (A<_{P} B → ∀𝑞 ∈ Q ¬ (𝑞 ∈ (1^{st} ‘𝐶) ∧ 𝑞 ∈ (2^{nd} ‘𝐶))) | ||
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 ∈ (2^{nd} ‘A) ∧ (y +_{Q} x) ∈ (1^{st} ‘B))}, {x ∈ Q ∣ ∃y(y ∈ (1^{st} ‘A) ∧ (y +_{Q} x) ∈ (2^{nd} ‘B))}⟩ ⇒ ⊢ (A<_{P} B → (∀𝑞 ∈ Q (𝑞 ∈ (1^{st} ‘𝐶) ↔ ∃𝑟 ∈ Q (𝑞 <_{Q} 𝑟 ∧ 𝑟 ∈ (1^{st} ‘𝐶))) ∧ ∀𝑟 ∈ Q (𝑟 ∈ (2^{nd} ‘𝐶) ↔ ∃𝑞 ∈ Q (𝑞 <_{Q} 𝑟 ∧ 𝑞 ∈ (2^{nd} ‘𝐶))))) | ||
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 ∈ (2^{nd} ‘A) ∧ (y +_{Q} x) ∈ (1^{st} ‘B))}, {x ∈ Q ∣ ∃y(y ∈ (1^{st} ‘A) ∧ (y +_{Q} x) ∈ (2^{nd} ‘B))}⟩ ⇒ ⊢ (A<_{P} B → (∃𝑞 ∈ Q 𝑞 ∈ (1^{st} ‘𝐶) ∧ ∃𝑟 ∈ Q 𝑟 ∈ (2^{nd} ‘𝐶))) | ||
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 (𝑞 ∈ (2^{nd} ‘A) ∧ 𝑞 ∈ (1^{st} ‘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 → (2^{nd} ‘(A ·_{P} 1_{P})) = (2^{nd} ‘A)) | ||
13-Dec-2019 | 1idprl 6429 | Lemma for 1idpr 6431. (Contributed by Jim Kingdon, 13-Dec-2019.) |
⊢ (A ∈ P → (1^{st} ‘(A ·_{P} 1_{P})) = (1^{st} ‘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) → (2^{nd} ‘((A ·_{P} B) +_{P} (A ·_{P} 𝐶))) ⊆ (2^{nd} ‘(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) → (1^{st} ‘((A ·_{P} B) +_{P} (A ·_{P} 𝐶))) ⊆ (1^{st} ‘(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 ∈ (2^{nd} ‘A) ∧ y ∈ (2^{nd} ‘B)) ∧ (f ∈ (2^{nd} ‘A) ∧ z ∈ (2^{nd} ‘𝐶)))) → ((x ·_{Q} y) +_{Q} (f ·_{Q} z)) ∈ (2^{nd} ‘(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 ∈ (1^{st} ‘A) ∧ y ∈ (1^{st} ‘B)) ∧ (f ∈ (1^{st} ‘A) ∧ z ∈ (1^{st} ‘𝐶)))) → ((x ·_{Q} y) +_{Q} (f ·_{Q} z)) ∈ (1^{st} ‘(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) → (2^{nd} ‘(A ·_{P} (B +_{P} 𝐶))) ⊆ (2^{nd} ‘((A ·_{P} B) +_{P} (A ·_{P} 𝐶)))) |
Copyright terms: Public domain | W3C HTML validation [external] |