Theorem List for Intuitionistic Logic Explorer - 6701-6800 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | genpelxp 6701* |
Set containing the result of adding or multiplying positive reals.
(Contributed by Jim Kingdon, 5-Dec-2019.)
|
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ 〈{𝑥 ∈ Q ∣
∃𝑦 ∈
Q ∃𝑧
∈ Q (𝑦
∈ (1st ‘𝑤) ∧ 𝑧 ∈ (1st ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q
∃𝑧 ∈
Q (𝑦 ∈
(2nd ‘𝑤)
∧ 𝑧 ∈
(2nd ‘𝑣)
∧ 𝑥 = (𝑦𝐺𝑧))}〉) ⇒ ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) →
(𝐴𝐹𝐵) ∈ (𝒫 Q ×
𝒫 Q)) |
|
Theorem | genpelvl 6702* |
Membership in lower cut of general operation (addition or
multiplication) on positive reals. (Contributed by Jim Kingdon,
2-Oct-2019.)
|
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ 〈{𝑥 ∈ Q ∣
∃𝑦 ∈
Q ∃𝑧
∈ Q (𝑦
∈ (1st ‘𝑤) ∧ 𝑧 ∈ (1st ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q
∃𝑧 ∈
Q (𝑦 ∈
(2nd ‘𝑤)
∧ 𝑧 ∈
(2nd ‘𝑣)
∧ 𝑥 = (𝑦𝐺𝑧))}〉) & ⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q)
→ (𝑦𝐺𝑧) ∈
Q) ⇒ ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) →
(𝐶 ∈ (1st
‘(𝐴𝐹𝐵)) ↔ ∃𝑔 ∈ (1st ‘𝐴)∃ℎ ∈ (1st ‘𝐵)𝐶 = (𝑔𝐺ℎ))) |
|
Theorem | genpelvu 6703* |
Membership in upper cut of general operation (addition or
multiplication) on positive reals. (Contributed by Jim Kingdon,
15-Oct-2019.)
|
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ 〈{𝑥 ∈ Q ∣
∃𝑦 ∈
Q ∃𝑧
∈ Q (𝑦
∈ (1st ‘𝑤) ∧ 𝑧 ∈ (1st ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q
∃𝑧 ∈
Q (𝑦 ∈
(2nd ‘𝑤)
∧ 𝑧 ∈
(2nd ‘𝑣)
∧ 𝑥 = (𝑦𝐺𝑧))}〉) & ⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q)
→ (𝑦𝐺𝑧) ∈
Q) ⇒ ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) →
(𝐶 ∈ (2nd
‘(𝐴𝐹𝐵)) ↔ ∃𝑔 ∈ (2nd ‘𝐴)∃ℎ ∈ (2nd ‘𝐵)𝐶 = (𝑔𝐺ℎ))) |
|
Theorem | genpprecll 6704* |
Pre-closure law for general operation on lower cuts. (Contributed by
Jim Kingdon, 2-Oct-2019.)
|
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ 〈{𝑥 ∈ Q ∣
∃𝑦 ∈
Q ∃𝑧
∈ Q (𝑦
∈ (1st ‘𝑤) ∧ 𝑧 ∈ (1st ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q
∃𝑧 ∈
Q (𝑦 ∈
(2nd ‘𝑤)
∧ 𝑧 ∈
(2nd ‘𝑣)
∧ 𝑥 = (𝑦𝐺𝑧))}〉) & ⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q)
→ (𝑦𝐺𝑧) ∈
Q) ⇒ ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) →
((𝐶 ∈ (1st
‘𝐴) ∧ 𝐷 ∈ (1st
‘𝐵)) → (𝐶𝐺𝐷) ∈ (1st ‘(𝐴𝐹𝐵)))) |
|
Theorem | genppreclu 6705* |
Pre-closure law for general operation on upper cuts. (Contributed by
Jim Kingdon, 7-Nov-2019.)
|
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ 〈{𝑥 ∈ Q ∣
∃𝑦 ∈
Q ∃𝑧
∈ Q (𝑦
∈ (1st ‘𝑤) ∧ 𝑧 ∈ (1st ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q
∃𝑧 ∈
Q (𝑦 ∈
(2nd ‘𝑤)
∧ 𝑧 ∈
(2nd ‘𝑣)
∧ 𝑥 = (𝑦𝐺𝑧))}〉) & ⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q)
→ (𝑦𝐺𝑧) ∈
Q) ⇒ ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) →
((𝐶 ∈ (2nd
‘𝐴) ∧ 𝐷 ∈ (2nd
‘𝐵)) → (𝐶𝐺𝐷) ∈ (2nd ‘(𝐴𝐹𝐵)))) |
|
Theorem | genipdm 6706* |
Domain of general operation on positive reals. (Contributed by Jim
Kingdon, 2-Oct-2019.)
|
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ 〈{𝑥 ∈ Q ∣
∃𝑦 ∈
Q ∃𝑧
∈ Q (𝑦
∈ (1st ‘𝑤) ∧ 𝑧 ∈ (1st ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q
∃𝑧 ∈
Q (𝑦 ∈
(2nd ‘𝑤)
∧ 𝑧 ∈
(2nd ‘𝑣)
∧ 𝑥 = (𝑦𝐺𝑧))}〉) & ⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q)
→ (𝑦𝐺𝑧) ∈
Q) ⇒ ⊢ dom 𝐹 = (P ×
P) |
|
Theorem | genpml 6707* |
The lower cut produced by addition or multiplication on positive reals
is inhabited. (Contributed by Jim Kingdon, 5-Oct-2019.)
|
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ 〈{𝑥 ∈ Q ∣
∃𝑦 ∈
Q ∃𝑧
∈ Q (𝑦
∈ (1st ‘𝑤) ∧ 𝑧 ∈ (1st ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q
∃𝑧 ∈
Q (𝑦 ∈
(2nd ‘𝑤)
∧ 𝑧 ∈
(2nd ‘𝑣)
∧ 𝑥 = (𝑦𝐺𝑧))}〉) & ⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q)
→ (𝑦𝐺𝑧) ∈
Q) ⇒ ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) →
∃𝑞 ∈
Q 𝑞 ∈
(1st ‘(𝐴𝐹𝐵))) |
|
Theorem | genpmu 6708* |
The upper cut produced by addition or multiplication on positive reals
is inhabited. (Contributed by Jim Kingdon, 5-Dec-2019.)
|
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ 〈{𝑥 ∈ Q ∣
∃𝑦 ∈
Q ∃𝑧
∈ Q (𝑦
∈ (1st ‘𝑤) ∧ 𝑧 ∈ (1st ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q
∃𝑧 ∈
Q (𝑦 ∈
(2nd ‘𝑤)
∧ 𝑧 ∈
(2nd ‘𝑣)
∧ 𝑥 = (𝑦𝐺𝑧))}〉) & ⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q)
→ (𝑦𝐺𝑧) ∈
Q) ⇒ ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) →
∃𝑞 ∈
Q 𝑞 ∈
(2nd ‘(𝐴𝐹𝐵))) |
|
Theorem | genpcdl 6709* |
Downward closure of an operation on positive reals. (Contributed by
Jim Kingdon, 14-Oct-2019.)
|
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ 〈{𝑥 ∈ Q ∣
∃𝑦 ∈
Q ∃𝑧
∈ Q (𝑦
∈ (1st ‘𝑤) ∧ 𝑧 ∈ (1st ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q
∃𝑧 ∈
Q (𝑦 ∈
(2nd ‘𝑤)
∧ 𝑧 ∈
(2nd ‘𝑣)
∧ 𝑥 = (𝑦𝐺𝑧))}〉) & ⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q)
→ (𝑦𝐺𝑧) ∈ Q) & ⊢ ((((𝐴 ∈ P ∧
𝑔 ∈ (1st
‘𝐴)) ∧ (𝐵 ∈ P ∧
ℎ ∈ (1st
‘𝐵))) ∧ 𝑥 ∈ Q) →
(𝑥
<Q (𝑔𝐺ℎ) → 𝑥 ∈ (1st ‘(𝐴𝐹𝐵)))) ⇒ ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) →
(𝑓 ∈ (1st
‘(𝐴𝐹𝐵)) → (𝑥 <Q 𝑓 → 𝑥 ∈ (1st ‘(𝐴𝐹𝐵))))) |
|
Theorem | genpcuu 6710* |
Upward closure of an operation on positive reals. (Contributed by Jim
Kingdon, 8-Nov-2019.)
|
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ 〈{𝑥 ∈ Q ∣
∃𝑦 ∈
Q ∃𝑧
∈ Q (𝑦
∈ (1st ‘𝑤) ∧ 𝑧 ∈ (1st ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q
∃𝑧 ∈
Q (𝑦 ∈
(2nd ‘𝑤)
∧ 𝑧 ∈
(2nd ‘𝑣)
∧ 𝑥 = (𝑦𝐺𝑧))}〉) & ⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q)
→ (𝑦𝐺𝑧) ∈ Q) & ⊢ ((((𝐴 ∈ P ∧
𝑔 ∈ (2nd
‘𝐴)) ∧ (𝐵 ∈ P ∧
ℎ ∈ (2nd
‘𝐵))) ∧ 𝑥 ∈ Q) →
((𝑔𝐺ℎ) <Q 𝑥 → 𝑥 ∈ (2nd ‘(𝐴𝐹𝐵)))) ⇒ ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) →
(𝑓 ∈ (2nd
‘(𝐴𝐹𝐵)) → (𝑓 <Q 𝑥 → 𝑥 ∈ (2nd ‘(𝐴𝐹𝐵))))) |
|
Theorem | genprndl 6711* |
The lower cut produced by addition or multiplication on positive reals
is rounded. (Contributed by Jim Kingdon, 7-Oct-2019.)
|
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ 〈{𝑥 ∈ Q ∣
∃𝑦 ∈
Q ∃𝑧
∈ Q (𝑦
∈ (1st ‘𝑤) ∧ 𝑧 ∈ (1st ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q
∃𝑧 ∈
Q (𝑦 ∈
(2nd ‘𝑤)
∧ 𝑧 ∈
(2nd ‘𝑣)
∧ 𝑥 = (𝑦𝐺𝑧))}〉) & ⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q)
→ (𝑦𝐺𝑧) ∈ Q) & ⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q
∧ 𝑧 ∈
Q) → (𝑥
<Q 𝑦 ↔ (𝑧𝐺𝑥) <Q (𝑧𝐺𝑦))) & ⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q)
→ (𝑥𝐺𝑦) = (𝑦𝐺𝑥))
& ⊢ ((((𝐴 ∈ P ∧ 𝑔 ∈ (1st
‘𝐴)) ∧ (𝐵 ∈ P ∧
ℎ ∈ (1st
‘𝐵))) ∧ 𝑥 ∈ Q) →
(𝑥
<Q (𝑔𝐺ℎ) → 𝑥 ∈ (1st ‘(𝐴𝐹𝐵)))) ⇒ ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) →
∀𝑞 ∈
Q (𝑞 ∈
(1st ‘(𝐴𝐹𝐵)) ↔ ∃𝑟 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑟 ∈ (1st ‘(𝐴𝐹𝐵))))) |
|
Theorem | genprndu 6712* |
The upper cut produced by addition or multiplication on positive reals
is rounded. (Contributed by Jim Kingdon, 7-Oct-2019.)
|
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ 〈{𝑥 ∈ Q ∣
∃𝑦 ∈
Q ∃𝑧
∈ Q (𝑦
∈ (1st ‘𝑤) ∧ 𝑧 ∈ (1st ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q
∃𝑧 ∈
Q (𝑦 ∈
(2nd ‘𝑤)
∧ 𝑧 ∈
(2nd ‘𝑣)
∧ 𝑥 = (𝑦𝐺𝑧))}〉) & ⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q)
→ (𝑦𝐺𝑧) ∈ Q) & ⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q
∧ 𝑧 ∈
Q) → (𝑥
<Q 𝑦 ↔ (𝑧𝐺𝑥) <Q (𝑧𝐺𝑦))) & ⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q)
→ (𝑥𝐺𝑦) = (𝑦𝐺𝑥))
& ⊢ ((((𝐴 ∈ P ∧ 𝑔 ∈ (2nd
‘𝐴)) ∧ (𝐵 ∈ P ∧
ℎ ∈ (2nd
‘𝐵))) ∧ 𝑥 ∈ Q) →
((𝑔𝐺ℎ) <Q 𝑥 → 𝑥 ∈ (2nd ‘(𝐴𝐹𝐵)))) ⇒ ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) →
∀𝑟 ∈
Q (𝑟 ∈
(2nd ‘(𝐴𝐹𝐵)) ↔ ∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑞 ∈ (2nd ‘(𝐴𝐹𝐵))))) |
|
Theorem | genpdisj 6713* |
The lower and upper cuts produced by addition or multiplication on
positive reals are disjoint. (Contributed by Jim Kingdon,
15-Oct-2019.)
|
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ 〈{𝑥 ∈ Q ∣
∃𝑦 ∈
Q ∃𝑧
∈ Q (𝑦
∈ (1st ‘𝑤) ∧ 𝑧 ∈ (1st ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q
∃𝑧 ∈
Q (𝑦 ∈
(2nd ‘𝑤)
∧ 𝑧 ∈
(2nd ‘𝑣)
∧ 𝑥 = (𝑦𝐺𝑧))}〉) & ⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q)
→ (𝑦𝐺𝑧) ∈ Q) & ⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q
∧ 𝑧 ∈
Q) → (𝑥
<Q 𝑦 ↔ (𝑧𝐺𝑥) <Q (𝑧𝐺𝑦))) & ⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q)
→ (𝑥𝐺𝑦) = (𝑦𝐺𝑥)) ⇒ ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) →
∀𝑞 ∈
Q ¬ (𝑞
∈ (1st ‘(𝐴𝐹𝐵)) ∧ 𝑞 ∈ (2nd ‘(𝐴𝐹𝐵)))) |
|
Theorem | genpassl 6714* |
Associativity of lower cuts. Lemma for genpassg 6716. (Contributed by
Jim Kingdon, 11-Dec-2019.)
|
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ 〈{𝑥 ∈ Q ∣
∃𝑦 ∈
Q ∃𝑧
∈ Q (𝑦
∈ (1st ‘𝑤) ∧ 𝑧 ∈ (1st ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q
∃𝑧 ∈
Q (𝑦 ∈
(2nd ‘𝑤)
∧ 𝑧 ∈
(2nd ‘𝑣)
∧ 𝑥 = (𝑦𝐺𝑧))}〉) & ⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q)
→ (𝑦𝐺𝑧) ∈ Q) & ⊢ dom 𝐹 = (P ×
P)
& ⊢ ((𝑓 ∈ P ∧ 𝑔 ∈ P) →
(𝑓𝐹𝑔) ∈ P) & ⊢ ((𝑓 ∈ Q ∧
𝑔 ∈ Q
∧ ℎ ∈
Q) → ((𝑓𝐺𝑔)𝐺ℎ) = (𝑓𝐺(𝑔𝐺ℎ))) ⇒ ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧
𝐶 ∈ P)
→ (1st ‘((𝐴𝐹𝐵)𝐹𝐶)) = (1st ‘(𝐴𝐹(𝐵𝐹𝐶)))) |
|
Theorem | genpassu 6715* |
Associativity of upper cuts. Lemma for genpassg 6716. (Contributed by
Jim Kingdon, 11-Dec-2019.)
|
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ 〈{𝑥 ∈ Q ∣
∃𝑦 ∈
Q ∃𝑧
∈ Q (𝑦
∈ (1st ‘𝑤) ∧ 𝑧 ∈ (1st ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q
∃𝑧 ∈
Q (𝑦 ∈
(2nd ‘𝑤)
∧ 𝑧 ∈
(2nd ‘𝑣)
∧ 𝑥 = (𝑦𝐺𝑧))}〉) & ⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q)
→ (𝑦𝐺𝑧) ∈ Q) & ⊢ dom 𝐹 = (P ×
P)
& ⊢ ((𝑓 ∈ P ∧ 𝑔 ∈ P) →
(𝑓𝐹𝑔) ∈ P) & ⊢ ((𝑓 ∈ Q ∧
𝑔 ∈ Q
∧ ℎ ∈
Q) → ((𝑓𝐺𝑔)𝐺ℎ) = (𝑓𝐺(𝑔𝐺ℎ))) ⇒ ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧
𝐶 ∈ P)
→ (2nd ‘((𝐴𝐹𝐵)𝐹𝐶)) = (2nd ‘(𝐴𝐹(𝐵𝐹𝐶)))) |
|
Theorem | genpassg 6716* |
Associativity of an operation on reals. (Contributed by Jim Kingdon,
11-Dec-2019.)
|
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ 〈{𝑥 ∈ Q ∣
∃𝑦 ∈
Q ∃𝑧
∈ Q (𝑦
∈ (1st ‘𝑤) ∧ 𝑧 ∈ (1st ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q
∃𝑧 ∈
Q (𝑦 ∈
(2nd ‘𝑤)
∧ 𝑧 ∈
(2nd ‘𝑣)
∧ 𝑥 = (𝑦𝐺𝑧))}〉) & ⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q)
→ (𝑦𝐺𝑧) ∈ Q) & ⊢ dom 𝐹 = (P ×
P)
& ⊢ ((𝑓 ∈ P ∧ 𝑔 ∈ P) →
(𝑓𝐹𝑔) ∈ P) & ⊢ ((𝑓 ∈ Q ∧
𝑔 ∈ Q
∧ ℎ ∈
Q) → ((𝑓𝐺𝑔)𝐺ℎ) = (𝑓𝐺(𝑔𝐺ℎ))) ⇒ ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧
𝐶 ∈ P)
→ ((𝐴𝐹𝐵)𝐹𝐶) = (𝐴𝐹(𝐵𝐹𝐶))) |
|
Theorem | addnqprllem 6717 |
Lemma to prove downward closure in positive real addition. (Contributed
by Jim Kingdon, 7-Dec-2019.)
|
⊢ (((〈𝐿, 𝑈〉 ∈ P ∧ 𝐺 ∈ 𝐿) ∧ 𝑋 ∈ Q) → (𝑋 <Q
𝑆 → ((𝑋
·Q (*Q‘𝑆))
·Q 𝐺) ∈ 𝐿)) |
|
Theorem | addnqprulem 6718 |
Lemma to prove upward closure in positive real addition. (Contributed
by Jim Kingdon, 7-Dec-2019.)
|
⊢ (((〈𝐿, 𝑈〉 ∈ P ∧ 𝐺 ∈ 𝑈) ∧ 𝑋 ∈ Q) → (𝑆 <Q
𝑋 → ((𝑋
·Q (*Q‘𝑆))
·Q 𝐺) ∈ 𝑈)) |
|
Theorem | addnqprl 6719 |
Lemma to prove downward closure in positive real addition. (Contributed
by Jim Kingdon, 5-Dec-2019.)
|
⊢ ((((𝐴 ∈ P ∧ 𝐺 ∈ (1st
‘𝐴)) ∧ (𝐵 ∈ P ∧
𝐻 ∈ (1st
‘𝐵))) ∧ 𝑋 ∈ Q) →
(𝑋
<Q (𝐺 +Q 𝐻) → 𝑋 ∈ (1st ‘(𝐴 +P
𝐵)))) |
|
Theorem | addnqpru 6720 |
Lemma to prove upward closure in positive real addition. (Contributed
by Jim Kingdon, 5-Dec-2019.)
|
⊢ ((((𝐴 ∈ P ∧ 𝐺 ∈ (2nd
‘𝐴)) ∧ (𝐵 ∈ P ∧
𝐻 ∈ (2nd
‘𝐵))) ∧ 𝑋 ∈ Q) →
((𝐺
+Q 𝐻) <Q 𝑋 → 𝑋 ∈ (2nd ‘(𝐴 +P
𝐵)))) |
|
Theorem | addlocprlemlt 6721 |
Lemma for addlocpr 6726. The 𝑄 <Q (𝐷 +Q
𝐸) case.
(Contributed by
Jim Kingdon, 6-Dec-2019.)
|
⊢ (𝜑 → 𝐴 ∈ P) & ⊢ (𝜑 → 𝐵 ∈ P) & ⊢ (𝜑 → 𝑄 <Q 𝑅) & ⊢ (𝜑 → 𝑃 ∈ Q) & ⊢ (𝜑 → (𝑄 +Q (𝑃 +Q
𝑃)) = 𝑅)
& ⊢ (𝜑 → 𝐷 ∈ (1st ‘𝐴)) & ⊢ (𝜑 → 𝑈 ∈ (2nd ‘𝐴)) & ⊢ (𝜑 → 𝑈 <Q (𝐷 +Q
𝑃)) & ⊢ (𝜑 → 𝐸 ∈ (1st ‘𝐵)) & ⊢ (𝜑 → 𝑇 ∈ (2nd ‘𝐵)) & ⊢ (𝜑 → 𝑇 <Q (𝐸 +Q
𝑃)) ⇒ ⊢ (𝜑 → (𝑄 <Q (𝐷 +Q
𝐸) → 𝑄 ∈ (1st
‘(𝐴
+P 𝐵)))) |
|
Theorem | addlocprlemeqgt 6722 |
Lemma for addlocpr 6726. This is a step used in both the
𝑄 =
(𝐷
+Q 𝐸) and (𝐷 +Q
𝐸)
<Q 𝑄 cases. (Contributed by Jim
Kingdon, 7-Dec-2019.)
|
⊢ (𝜑 → 𝐴 ∈ P) & ⊢ (𝜑 → 𝐵 ∈ P) & ⊢ (𝜑 → 𝑄 <Q 𝑅) & ⊢ (𝜑 → 𝑃 ∈ Q) & ⊢ (𝜑 → (𝑄 +Q (𝑃 +Q
𝑃)) = 𝑅)
& ⊢ (𝜑 → 𝐷 ∈ (1st ‘𝐴)) & ⊢ (𝜑 → 𝑈 ∈ (2nd ‘𝐴)) & ⊢ (𝜑 → 𝑈 <Q (𝐷 +Q
𝑃)) & ⊢ (𝜑 → 𝐸 ∈ (1st ‘𝐵)) & ⊢ (𝜑 → 𝑇 ∈ (2nd ‘𝐵)) & ⊢ (𝜑 → 𝑇 <Q (𝐸 +Q
𝑃)) ⇒ ⊢ (𝜑 → (𝑈 +Q 𝑇)
<Q ((𝐷 +Q 𝐸) +Q
(𝑃
+Q 𝑃))) |
|
Theorem | addlocprlemeq 6723 |
Lemma for addlocpr 6726. The 𝑄 = (𝐷 +Q 𝐸) case. (Contributed by
Jim Kingdon, 6-Dec-2019.)
|
⊢ (𝜑 → 𝐴 ∈ P) & ⊢ (𝜑 → 𝐵 ∈ P) & ⊢ (𝜑 → 𝑄 <Q 𝑅) & ⊢ (𝜑 → 𝑃 ∈ Q) & ⊢ (𝜑 → (𝑄 +Q (𝑃 +Q
𝑃)) = 𝑅)
& ⊢ (𝜑 → 𝐷 ∈ (1st ‘𝐴)) & ⊢ (𝜑 → 𝑈 ∈ (2nd ‘𝐴)) & ⊢ (𝜑 → 𝑈 <Q (𝐷 +Q
𝑃)) & ⊢ (𝜑 → 𝐸 ∈ (1st ‘𝐵)) & ⊢ (𝜑 → 𝑇 ∈ (2nd ‘𝐵)) & ⊢ (𝜑 → 𝑇 <Q (𝐸 +Q
𝑃)) ⇒ ⊢ (𝜑 → (𝑄 = (𝐷 +Q 𝐸) → 𝑅 ∈ (2nd ‘(𝐴 +P
𝐵)))) |
|
Theorem | addlocprlemgt 6724 |
Lemma for addlocpr 6726. The (𝐷 +Q 𝐸) <Q
𝑄 case.
(Contributed by
Jim Kingdon, 6-Dec-2019.)
|
⊢ (𝜑 → 𝐴 ∈ P) & ⊢ (𝜑 → 𝐵 ∈ P) & ⊢ (𝜑 → 𝑄 <Q 𝑅) & ⊢ (𝜑 → 𝑃 ∈ Q) & ⊢ (𝜑 → (𝑄 +Q (𝑃 +Q
𝑃)) = 𝑅)
& ⊢ (𝜑 → 𝐷 ∈ (1st ‘𝐴)) & ⊢ (𝜑 → 𝑈 ∈ (2nd ‘𝐴)) & ⊢ (𝜑 → 𝑈 <Q (𝐷 +Q
𝑃)) & ⊢ (𝜑 → 𝐸 ∈ (1st ‘𝐵)) & ⊢ (𝜑 → 𝑇 ∈ (2nd ‘𝐵)) & ⊢ (𝜑 → 𝑇 <Q (𝐸 +Q
𝑃)) ⇒ ⊢ (𝜑 → ((𝐷 +Q 𝐸)
<Q 𝑄 → 𝑅 ∈ (2nd ‘(𝐴 +P
𝐵)))) |
|
Theorem | addlocprlem 6725 |
Lemma for addlocpr 6726. The result, in deduction form.
(Contributed by
Jim Kingdon, 6-Dec-2019.)
|
⊢ (𝜑 → 𝐴 ∈ P) & ⊢ (𝜑 → 𝐵 ∈ P) & ⊢ (𝜑 → 𝑄 <Q 𝑅) & ⊢ (𝜑 → 𝑃 ∈ Q) & ⊢ (𝜑 → (𝑄 +Q (𝑃 +Q
𝑃)) = 𝑅)
& ⊢ (𝜑 → 𝐷 ∈ (1st ‘𝐴)) & ⊢ (𝜑 → 𝑈 ∈ (2nd ‘𝐴)) & ⊢ (𝜑 → 𝑈 <Q (𝐷 +Q
𝑃)) & ⊢ (𝜑 → 𝐸 ∈ (1st ‘𝐵)) & ⊢ (𝜑 → 𝑇 ∈ (2nd ‘𝐵)) & ⊢ (𝜑 → 𝑇 <Q (𝐸 +Q
𝑃)) ⇒ ⊢ (𝜑 → (𝑄 ∈ (1st ‘(𝐴 +P
𝐵)) ∨ 𝑅 ∈ (2nd ‘(𝐴 +P
𝐵)))) |
|
Theorem | addlocpr 6726* |
Locatedness of addition on positive reals. Lemma 11.16 in
[BauerTaylor], p. 53. The proof in
BauerTaylor relies on signed
rationals, so we replace it with another proof which applies prarloc 6693
to both 𝐴 and 𝐵, and uses nqtri3or 6586 rather than prloc 6681 to
decide whether 𝑞 is too big to be in the lower cut of
𝐴
+P 𝐵
(and deduce that if it is, then 𝑟 must be in the upper cut). What
the two proofs have in common is that they take the difference between
𝑞 and 𝑟 to determine how tight a
range they need around the real
numbers. (Contributed by Jim Kingdon, 5-Dec-2019.)
|
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) →
∀𝑞 ∈
Q ∀𝑟
∈ Q (𝑞
<Q 𝑟 → (𝑞 ∈ (1st ‘(𝐴 +P
𝐵)) ∨ 𝑟 ∈ (2nd
‘(𝐴
+P 𝐵))))) |
|
Theorem | addclpr 6727 |
Closure of addition on positive reals. First statement of Proposition
9-3.5 of [Gleason] p. 123. Combination
of Lemma 11.13 and Lemma 11.16
in [BauerTaylor], p. 53.
(Contributed by NM, 13-Mar-1996.)
|
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) →
(𝐴
+P 𝐵) ∈ P) |
|
Theorem | plpvlu 6728* |
Value of addition on positive reals. (Contributed by Jim Kingdon,
8-Dec-2019.)
|
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) →
(𝐴
+P 𝐵) = 〈{𝑥 ∈ Q ∣ ∃𝑦 ∈ (1st
‘𝐴)∃𝑧 ∈ (1st
‘𝐵)𝑥 = (𝑦 +Q 𝑧)}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ (2nd
‘𝐴)∃𝑧 ∈ (2nd
‘𝐵)𝑥 = (𝑦 +Q 𝑧)}〉) |
|
Theorem | mpvlu 6729* |
Value of multiplication on positive reals. (Contributed by Jim Kingdon,
8-Dec-2019.)
|
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) →
(𝐴
·P 𝐵) = 〈{𝑥 ∈ Q ∣ ∃𝑦 ∈ (1st
‘𝐴)∃𝑧 ∈ (1st
‘𝐵)𝑥 = (𝑦 ·Q 𝑧)}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ (2nd
‘𝐴)∃𝑧 ∈ (2nd
‘𝐵)𝑥 = (𝑦 ·Q 𝑧)}〉) |
|
Theorem | dmplp 6730 |
Domain of addition on positive reals. (Contributed by NM,
18-Nov-1995.)
|
⊢ dom +P =
(P × P) |
|
Theorem | dmmp 6731 |
Domain of multiplication on positive reals. (Contributed by NM,
18-Nov-1995.)
|
⊢ dom ·P =
(P × P) |
|
Theorem | nqprm 6732* |
A cut produced from a rational is inhabited. Lemma for nqprlu 6737.
(Contributed by Jim Kingdon, 8-Dec-2019.)
|
⊢ (𝐴 ∈ Q →
(∃𝑞 ∈
Q 𝑞 ∈
{𝑥 ∣ 𝑥 <Q
𝐴} ∧ ∃𝑟 ∈ Q 𝑟 ∈ {𝑥 ∣ 𝐴 <Q 𝑥})) |
|
Theorem | nqprrnd 6733* |
A cut produced from a rational is rounded. Lemma for nqprlu 6737.
(Contributed by Jim Kingdon, 8-Dec-2019.)
|
⊢ (𝐴 ∈ Q →
(∀𝑞 ∈
Q (𝑞 ∈
{𝑥 ∣ 𝑥 <Q
𝐴} ↔ ∃𝑟 ∈ Q (𝑞 <Q
𝑟 ∧ 𝑟 ∈ {𝑥 ∣ 𝑥 <Q 𝐴})) ∧ ∀𝑟 ∈ Q (𝑟 ∈ {𝑥 ∣ 𝐴 <Q 𝑥} ↔ ∃𝑞 ∈ Q (𝑞 <Q
𝑟 ∧ 𝑞 ∈ {𝑥 ∣ 𝐴 <Q 𝑥})))) |
|
Theorem | nqprdisj 6734* |
A cut produced from a rational is disjoint. Lemma for nqprlu 6737.
(Contributed by Jim Kingdon, 8-Dec-2019.)
|
⊢ (𝐴 ∈ Q →
∀𝑞 ∈
Q ¬ (𝑞
∈ {𝑥 ∣ 𝑥 <Q
𝐴} ∧ 𝑞 ∈ {𝑥 ∣ 𝐴 <Q 𝑥})) |
|
Theorem | nqprloc 6735* |
A cut produced from a rational is located. Lemma for nqprlu 6737.
(Contributed by Jim Kingdon, 8-Dec-2019.)
|
⊢ (𝐴 ∈ Q →
∀𝑞 ∈
Q ∀𝑟
∈ Q (𝑞
<Q 𝑟 → (𝑞 ∈ {𝑥 ∣ 𝑥 <Q 𝐴} ∨ 𝑟 ∈ {𝑥 ∣ 𝐴 <Q 𝑥}))) |
|
Theorem | nqprxx 6736* |
The canonical embedding of the rationals into the reals, expressed with
the same variable for the lower and upper cuts. (Contributed by Jim
Kingdon, 8-Dec-2019.)
|
⊢ (𝐴 ∈ Q → 〈{𝑥 ∣ 𝑥 <Q 𝐴}, {𝑥 ∣ 𝐴 <Q 𝑥}〉 ∈
P) |
|
Theorem | nqprlu 6737* |
The canonical embedding of the rationals into the reals. (Contributed
by Jim Kingdon, 24-Jun-2020.)
|
⊢ (𝐴 ∈ Q → 〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉 ∈
P) |
|
Theorem | recnnpr 6738* |
The reciprocal of a positive integer, as a positive real. (Contributed
by Jim Kingdon, 27-Feb-2021.)
|
⊢ (𝐴 ∈ N → 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝐴, 1𝑜〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝐴, 1𝑜〉]
~Q ) <Q 𝑢}〉 ∈
P) |
|
Theorem | ltnqex 6739 |
The class of rationals less than a given rational is a set. (Contributed
by Jim Kingdon, 13-Dec-2019.)
|
⊢ {𝑥 ∣ 𝑥 <Q 𝐴} ∈ V |
|
Theorem | gtnqex 6740 |
The class of rationals greater than a given rational is a set.
(Contributed by Jim Kingdon, 13-Dec-2019.)
|
⊢ {𝑥 ∣ 𝐴 <Q 𝑥} ∈ V |
|
Theorem | nqprl 6741* |
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.)
|
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ P) →
(𝐴 ∈ (1st
‘𝐵) ↔
〈{𝑙 ∣ 𝑙 <Q
𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉<P 𝐵)) |
|
Theorem | nqpru 6742* |
Comparing a fraction to a real can be done by whether it is an element
of the upper cut, or by <P. (Contributed by Jim Kingdon,
29-Nov-2020.)
|
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ P) →
(𝐴 ∈ (2nd
‘𝐵) ↔ 𝐵<P
〈{𝑙 ∣ 𝑙 <Q
𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉)) |
|
Theorem | nnprlu 6743* |
The canonical embedding of positive integers into the positive reals.
(Contributed by Jim Kingdon, 23-Apr-2020.)
|
⊢ (𝐴 ∈ N → 〈{𝑙 ∣ 𝑙 <Q [〈𝐴, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝐴, 1𝑜〉]
~Q <Q 𝑢}〉 ∈
P) |
|
Theorem | 1pr 6744 |
The positive real number 'one'. (Contributed by NM, 13-Mar-1996.)
(Revised by Mario Carneiro, 12-Jun-2013.)
|
⊢ 1P ∈
P |
|
Theorem | 1prl 6745 |
The lower cut of the positive real number 'one'. (Contributed by Jim
Kingdon, 28-Dec-2019.)
|
⊢ (1st
‘1P) = {𝑥 ∣ 𝑥 <Q
1Q} |
|
Theorem | 1pru 6746 |
The upper cut of the positive real number 'one'. (Contributed by Jim
Kingdon, 28-Dec-2019.)
|
⊢ (2nd
‘1P) = {𝑥 ∣ 1Q
<Q 𝑥} |
|
Theorem | addnqprlemrl 6747* |
Lemma for addnqpr 6751. The reverse subset relationship for the
lower
cut. (Contributed by Jim Kingdon, 19-Aug-2020.)
|
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) →
(1st ‘(〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
+P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉)) ⊆
(1st ‘〈{𝑙 ∣ 𝑙 <Q (𝐴 +Q
𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵)
<Q 𝑢}〉)) |
|
Theorem | addnqprlemru 6748* |
Lemma for addnqpr 6751. The reverse subset relationship for the
upper
cut. (Contributed by Jim Kingdon, 19-Aug-2020.)
|
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) →
(2nd ‘(〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
+P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉)) ⊆
(2nd ‘〈{𝑙 ∣ 𝑙 <Q (𝐴 +Q
𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵)
<Q 𝑢}〉)) |
|
Theorem | addnqprlemfl 6749* |
Lemma for addnqpr 6751. The forward subset relationship for the
lower
cut. (Contributed by Jim Kingdon, 19-Aug-2020.)
|
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) →
(1st ‘〈{𝑙 ∣ 𝑙 <Q (𝐴 +Q
𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵)
<Q 𝑢}〉) ⊆ (1st
‘(〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
+P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) |
|
Theorem | addnqprlemfu 6750* |
Lemma for addnqpr 6751. The forward subset relationship for the
upper
cut. (Contributed by Jim Kingdon, 19-Aug-2020.)
|
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) →
(2nd ‘〈{𝑙 ∣ 𝑙 <Q (𝐴 +Q
𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵)
<Q 𝑢}〉) ⊆ (2nd
‘(〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
+P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) |
|
Theorem | addnqpr 6751* |
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.)
|
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) →
〈{𝑙 ∣ 𝑙 <Q
(𝐴
+Q 𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵)
<Q 𝑢}〉 = (〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
+P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉)) |
|
Theorem | addnqpr1 6752* |
Addition of one to a fraction embedded into a positive real. One can
either add the fraction one to the fraction, or the positive real one to
the positive real, and get the same result. Special case of addnqpr 6751.
(Contributed by Jim Kingdon, 26-Apr-2020.)
|
⊢ (𝐴 ∈ Q → 〈{𝑙 ∣ 𝑙 <Q (𝐴 +Q
1Q)}, {𝑢 ∣ (𝐴 +Q
1Q) <Q 𝑢}〉 = (〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
+P 1P)) |
|
Theorem | appdivnq 6753* |
Approximate division for positive rationals. Proposition 12.7 of
[BauerTaylor], p. 55 (a special case
where 𝐴 and 𝐵 are positive,
as well as 𝐶). Our proof is simpler than the one
in BauerTaylor
because we have reciprocals. (Contributed by Jim Kingdon,
8-Dec-2019.)
|
⊢ ((𝐴 <Q 𝐵 ∧ 𝐶 ∈ Q) →
∃𝑚 ∈
Q (𝐴
<Q (𝑚 ·Q 𝐶) ∧ (𝑚 ·Q 𝐶)
<Q 𝐵)) |
|
Theorem | appdiv0nq 6754* |
Approximate division for positive rationals. This can be thought of as
a variation of appdivnq 6753 in which 𝐴 is zero, although it can be
stated and proved in terms of positive rationals alone, without zero as
such. (Contributed by Jim Kingdon, 9-Dec-2019.)
|
⊢ ((𝐵 ∈ Q ∧ 𝐶 ∈ Q) →
∃𝑚 ∈
Q (𝑚
·Q 𝐶) <Q 𝐵) |
|
Theorem | prmuloclemcalc 6755 |
Calculations for prmuloc 6756. (Contributed by Jim Kingdon,
9-Dec-2019.)
|
⊢ (𝜑 → 𝑅 <Q 𝑈) & ⊢ (𝜑 → 𝑈 <Q (𝐷 +Q
𝑃)) & ⊢ (𝜑 → (𝐴 +Q 𝑋) = 𝐵)
& ⊢ (𝜑 → (𝑃 ·Q 𝐵)
<Q (𝑅 ·Q 𝑋)) & ⊢ (𝜑 → 𝐴 ∈ Q) & ⊢ (𝜑 → 𝐵 ∈ Q) & ⊢ (𝜑 → 𝐷 ∈ Q) & ⊢ (𝜑 → 𝑃 ∈ Q) & ⊢ (𝜑 → 𝑋 ∈
Q) ⇒ ⊢ (𝜑 → (𝑈 ·Q 𝐴)
<Q (𝐷 ·Q 𝐵)) |
|
Theorem | prmuloc 6756* |
Positive reals are multiplicatively located. Lemma 12.8 of
[BauerTaylor], p. 56. (Contributed
by Jim Kingdon, 8-Dec-2019.)
|
⊢ ((〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 <Q
𝐵) → ∃𝑑 ∈ Q
∃𝑢 ∈
Q (𝑑 ∈
𝐿 ∧ 𝑢 ∈ 𝑈 ∧ (𝑢 ·Q 𝐴)
<Q (𝑑 ·Q 𝐵))) |
|
Theorem | prmuloc2 6757* |
Positive reals are multiplicatively located. This is a variation of
prmuloc 6756 which only constructs one (named) point and
is therefore often
easier to work with. It states that given a ratio 𝐵, 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 𝐵) → ∃𝑥 ∈ 𝐿 (𝑥 ·Q 𝐵) ∈ 𝑈) |
|
Theorem | mulnqprl 6758 |
Lemma to prove downward closure in positive real multiplication.
(Contributed by Jim Kingdon, 10-Dec-2019.)
|
⊢ ((((𝐴 ∈ P ∧ 𝐺 ∈ (1st
‘𝐴)) ∧ (𝐵 ∈ P ∧
𝐻 ∈ (1st
‘𝐵))) ∧ 𝑋 ∈ Q) →
(𝑋
<Q (𝐺 ·Q 𝐻) → 𝑋 ∈ (1st ‘(𝐴
·P 𝐵)))) |
|
Theorem | mulnqpru 6759 |
Lemma to prove upward closure in positive real multiplication.
(Contributed by Jim Kingdon, 10-Dec-2019.)
|
⊢ ((((𝐴 ∈ P ∧ 𝐺 ∈ (2nd
‘𝐴)) ∧ (𝐵 ∈ P ∧
𝐻 ∈ (2nd
‘𝐵))) ∧ 𝑋 ∈ Q) →
((𝐺
·Q 𝐻) <Q 𝑋 → 𝑋 ∈ (2nd ‘(𝐴
·P 𝐵)))) |
|
Theorem | mullocprlem 6760 |
Calculations for mullocpr 6761. (Contributed by Jim Kingdon,
10-Dec-2019.)
|
⊢ (𝜑 → (𝐴 ∈ P ∧ 𝐵 ∈
P))
& ⊢ (𝜑 → (𝑈 ·Q 𝑄)
<Q (𝐸 ·Q (𝐷
·Q 𝑈))) & ⊢ (𝜑 → (𝐸 ·Q (𝐷
·Q 𝑈)) <Q (𝑇
·Q (𝐷 ·Q 𝑈))) & ⊢ (𝜑 → (𝑇 ·Q (𝐷
·Q 𝑈)) <Q (𝐷
·Q 𝑅)) & ⊢ (𝜑 → (𝑄 ∈ Q ∧ 𝑅 ∈
Q))
& ⊢ (𝜑 → (𝐷 ∈ Q ∧ 𝑈 ∈
Q))
& ⊢ (𝜑 → (𝐷 ∈ (1st ‘𝐴) ∧ 𝑈 ∈ (2nd ‘𝐴))) & ⊢ (𝜑 → (𝐸 ∈ Q ∧ 𝑇 ∈
Q)) ⇒ ⊢ (𝜑 → (𝑄 ∈ (1st ‘(𝐴
·P 𝐵)) ∨ 𝑅 ∈ (2nd ‘(𝐴
·P 𝐵)))) |
|
Theorem | mullocpr 6761* |
Locatedness of multiplication on positive reals. Lemma 12.9 in
[BauerTaylor], p. 56 (but where both
𝐴
and 𝐵 are positive, not
just 𝐴). (Contributed by Jim Kingdon,
8-Dec-2019.)
|
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) →
∀𝑞 ∈
Q ∀𝑟
∈ Q (𝑞
<Q 𝑟 → (𝑞 ∈ (1st ‘(𝐴
·P 𝐵)) ∨ 𝑟 ∈ (2nd ‘(𝐴
·P 𝐵))))) |
|
Theorem | mulclpr 6762 |
Closure of multiplication on positive reals. First statement of
Proposition 9-3.7 of [Gleason] p. 124.
(Contributed by NM,
13-Mar-1996.)
|
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) →
(𝐴
·P 𝐵) ∈ P) |
|
Theorem | mulnqprlemrl 6763* |
Lemma for mulnqpr 6767. The reverse subset relationship for the
lower
cut. (Contributed by Jim Kingdon, 18-Jul-2021.)
|
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) →
(1st ‘(〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
·P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉)) ⊆
(1st ‘〈{𝑙 ∣ 𝑙 <Q (𝐴
·Q 𝐵)}, {𝑢 ∣ (𝐴 ·Q 𝐵)
<Q 𝑢}〉)) |
|
Theorem | mulnqprlemru 6764* |
Lemma for mulnqpr 6767. The reverse subset relationship for the
upper
cut. (Contributed by Jim Kingdon, 18-Jul-2021.)
|
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) →
(2nd ‘(〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
·P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉)) ⊆
(2nd ‘〈{𝑙 ∣ 𝑙 <Q (𝐴
·Q 𝐵)}, {𝑢 ∣ (𝐴 ·Q 𝐵)
<Q 𝑢}〉)) |
|
Theorem | mulnqprlemfl 6765* |
Lemma for mulnqpr 6767. The forward subset relationship for the
lower
cut. (Contributed by Jim Kingdon, 18-Jul-2021.)
|
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) →
(1st ‘〈{𝑙 ∣ 𝑙 <Q (𝐴
·Q 𝐵)}, {𝑢 ∣ (𝐴 ·Q 𝐵)
<Q 𝑢}〉) ⊆ (1st
‘(〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
·P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) |
|
Theorem | mulnqprlemfu 6766* |
Lemma for mulnqpr 6767. The forward subset relationship for the
upper
cut. (Contributed by Jim Kingdon, 18-Jul-2021.)
|
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) →
(2nd ‘〈{𝑙 ∣ 𝑙 <Q (𝐴
·Q 𝐵)}, {𝑢 ∣ (𝐴 ·Q 𝐵)
<Q 𝑢}〉) ⊆ (2nd
‘(〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
·P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) |
|
Theorem | mulnqpr 6767* |
Multiplication of fractions embedded into positive reals. One can
either multiply the fractions as fractions, or embed them into positive
reals and multiply them as positive reals, and get the same result.
(Contributed by Jim Kingdon, 18-Jul-2021.)
|
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) →
〈{𝑙 ∣ 𝑙 <Q
(𝐴
·Q 𝐵)}, {𝑢 ∣ (𝐴 ·Q 𝐵)
<Q 𝑢}〉 = (〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
·P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉)) |
|
Theorem | addcomprg 6768 |
Addition of positive reals is commutative. Proposition 9-3.5(ii) of
[Gleason] p. 123. (Contributed by Jim
Kingdon, 11-Dec-2019.)
|
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) →
(𝐴
+P 𝐵) = (𝐵 +P 𝐴)) |
|
Theorem | addassprg 6769 |
Addition of positive reals is associative. Proposition 9-3.5(i) of
[Gleason] p. 123. (Contributed by Jim
Kingdon, 11-Dec-2019.)
|
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧
𝐶 ∈ P)
→ ((𝐴
+P 𝐵) +P 𝐶) = (𝐴 +P (𝐵 +P
𝐶))) |
|
Theorem | mulcomprg 6770 |
Multiplication of positive reals is commutative. Proposition 9-3.7(ii)
of [Gleason] p. 124. (Contributed by
Jim Kingdon, 11-Dec-2019.)
|
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) →
(𝐴
·P 𝐵) = (𝐵 ·P 𝐴)) |
|
Theorem | mulassprg 6771 |
Multiplication of positive reals is associative. Proposition 9-3.7(i)
of [Gleason] p. 124. (Contributed by
Jim Kingdon, 11-Dec-2019.)
|
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧
𝐶 ∈ P)
→ ((𝐴
·P 𝐵) ·P 𝐶) = (𝐴 ·P (𝐵
·P 𝐶))) |
|
Theorem | distrlem1prl 6772 |
Lemma for distributive law for positive reals. (Contributed by Jim
Kingdon, 12-Dec-2019.)
|
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧
𝐶 ∈ P)
→ (1st ‘(𝐴 ·P (𝐵 +P
𝐶))) ⊆
(1st ‘((𝐴
·P 𝐵) +P (𝐴
·P 𝐶)))) |
|
Theorem | distrlem1pru 6773 |
Lemma for distributive law for positive reals. (Contributed by Jim
Kingdon, 12-Dec-2019.)
|
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧
𝐶 ∈ P)
→ (2nd ‘(𝐴 ·P (𝐵 +P
𝐶))) ⊆
(2nd ‘((𝐴
·P 𝐵) +P (𝐴
·P 𝐶)))) |
|
Theorem | distrlem4prl 6774* |
Lemma for distributive law for positive reals. (Contributed by Jim
Kingdon, 12-Dec-2019.)
|
⊢ (((𝐴 ∈ P ∧ 𝐵 ∈ P ∧
𝐶 ∈ P)
∧ ((𝑥 ∈
(1st ‘𝐴)
∧ 𝑦 ∈
(1st ‘𝐵))
∧ (𝑓 ∈
(1st ‘𝐴)
∧ 𝑧 ∈
(1st ‘𝐶)))) → ((𝑥 ·Q 𝑦) +Q
(𝑓
·Q 𝑧)) ∈ (1st ‘(𝐴
·P (𝐵 +P 𝐶)))) |
|
Theorem | distrlem4pru 6775* |
Lemma for distributive law for positive reals. (Contributed by Jim
Kingdon, 12-Dec-2019.)
|
⊢ (((𝐴 ∈ P ∧ 𝐵 ∈ P ∧
𝐶 ∈ P)
∧ ((𝑥 ∈
(2nd ‘𝐴)
∧ 𝑦 ∈
(2nd ‘𝐵))
∧ (𝑓 ∈
(2nd ‘𝐴)
∧ 𝑧 ∈
(2nd ‘𝐶)))) → ((𝑥 ·Q 𝑦) +Q
(𝑓
·Q 𝑧)) ∈ (2nd ‘(𝐴
·P (𝐵 +P 𝐶)))) |
|
Theorem | distrlem5prl 6776 |
Lemma for distributive law for positive reals. (Contributed by Jim
Kingdon, 12-Dec-2019.)
|
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧
𝐶 ∈ P)
→ (1st ‘((𝐴 ·P 𝐵) +P
(𝐴
·P 𝐶))) ⊆ (1st ‘(𝐴
·P (𝐵 +P 𝐶)))) |
|
Theorem | distrlem5pru 6777 |
Lemma for distributive law for positive reals. (Contributed by Jim
Kingdon, 12-Dec-2019.)
|
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧
𝐶 ∈ P)
→ (2nd ‘((𝐴 ·P 𝐵) +P
(𝐴
·P 𝐶))) ⊆ (2nd ‘(𝐴
·P (𝐵 +P 𝐶)))) |
|
Theorem | distrprg 6778 |
Multiplication of positive reals is distributive. Proposition 9-3.7(iii)
of [Gleason] p. 124. (Contributed by Jim
Kingdon, 12-Dec-2019.)
|
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧
𝐶 ∈ P)
→ (𝐴
·P (𝐵 +P 𝐶)) = ((𝐴 ·P 𝐵) +P
(𝐴
·P 𝐶))) |
|
Theorem | ltprordil 6779 |
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.)
|
⊢ (𝐴<P 𝐵 → (1st
‘𝐴) ⊆
(1st ‘𝐵)) |
|
Theorem | 1idprl 6780 |
Lemma for 1idpr 6782. (Contributed by Jim Kingdon, 13-Dec-2019.)
|
⊢ (𝐴 ∈ P →
(1st ‘(𝐴
·P 1P)) =
(1st ‘𝐴)) |
|
Theorem | 1idpru 6781 |
Lemma for 1idpr 6782. (Contributed by Jim Kingdon, 13-Dec-2019.)
|
⊢ (𝐴 ∈ P →
(2nd ‘(𝐴
·P 1P)) =
(2nd ‘𝐴)) |
|
Theorem | 1idpr 6782 |
1 is an identity element for positive real multiplication. Theorem
9-3.7(iv) of [Gleason] p. 124.
(Contributed by NM, 2-Apr-1996.)
|
⊢ (𝐴 ∈ P → (𝐴
·P 1P) = 𝐴) |
|
Theorem | ltnqpr 6783* |
We can order fractions via <Q or <P. (Contributed by Jim
Kingdon, 19-Jun-2021.)
|
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) →
(𝐴
<Q 𝐵 ↔ 〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉<P
〈{𝑙 ∣ 𝑙 <Q
𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉)) |
|
Theorem | ltnqpri 6784* |
We can order fractions via <Q or <P. (Contributed by Jim
Kingdon, 8-Jan-2021.)
|
⊢ (𝐴 <Q 𝐵 → 〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉<P
〈{𝑙 ∣ 𝑙 <Q
𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉) |
|
Theorem | ltpopr 6785 |
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 6786. (Contributed by Jim Kingdon,
15-Dec-2019.)
|
⊢ <P Po
P |
|
Theorem | ltsopr 6786 |
Positive real 'less than' is a weak linear order (in the sense of
df-iso 4052). Proposition 11.2.3 of [HoTT], p. (varies). (Contributed
by Jim Kingdon, 16-Dec-2019.)
|
⊢ <P Or
P |
|
Theorem | ltaddpr 6787 |
The sum of two positive reals is greater than one of them. Proposition
9-3.5(iii) of [Gleason] p. 123.
(Contributed by NM, 26-Mar-1996.)
(Revised by Mario Carneiro, 12-Jun-2013.)
|
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) →
𝐴<P (𝐴 +P
𝐵)) |
|
Theorem | ltexprlemell 6788* |
Element in lower cut of the constructed difference. Lemma for
ltexpri 6803. (Contributed by Jim Kingdon, 21-Dec-2019.)
|
⊢ 𝐶 = 〈{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (1st
‘𝐵))}, {𝑥 ∈ Q ∣
∃𝑦(𝑦 ∈ (1st
‘𝐴) ∧ (𝑦 +Q
𝑥) ∈ (2nd
‘𝐵))}〉 ⇒ ⊢ (𝑞 ∈ (1st ‘𝐶) ↔ (𝑞 ∈ Q ∧ ∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑞) ∈ (1st
‘𝐵)))) |
|
Theorem | ltexprlemelu 6789* |
Element in upper cut of the constructed difference. Lemma for
ltexpri 6803. (Contributed by Jim Kingdon, 21-Dec-2019.)
|
⊢ 𝐶 = 〈{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (1st
‘𝐵))}, {𝑥 ∈ Q ∣
∃𝑦(𝑦 ∈ (1st
‘𝐴) ∧ (𝑦 +Q
𝑥) ∈ (2nd
‘𝐵))}〉 ⇒ ⊢ (𝑟 ∈ (2nd ‘𝐶) ↔ (𝑟 ∈ Q ∧ ∃𝑦(𝑦 ∈ (1st ‘𝐴) ∧ (𝑦 +Q 𝑟) ∈ (2nd
‘𝐵)))) |
|
Theorem | ltexprlemm 6790* |
Our constructed difference is inhabited. Lemma for ltexpri 6803.
(Contributed by Jim Kingdon, 17-Dec-2019.)
|
⊢ 𝐶 = 〈{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (1st
‘𝐵))}, {𝑥 ∈ Q ∣
∃𝑦(𝑦 ∈ (1st
‘𝐴) ∧ (𝑦 +Q
𝑥) ∈ (2nd
‘𝐵))}〉 ⇒ ⊢ (𝐴<P 𝐵 → (∃𝑞 ∈ Q 𝑞 ∈ (1st
‘𝐶) ∧
∃𝑟 ∈
Q 𝑟 ∈
(2nd ‘𝐶))) |
|
Theorem | ltexprlemopl 6791* |
The lower cut of our constructed difference is open. Lemma for
ltexpri 6803. (Contributed by Jim Kingdon, 21-Dec-2019.)
|
⊢ 𝐶 = 〈{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (1st
‘𝐵))}, {𝑥 ∈ Q ∣
∃𝑦(𝑦 ∈ (1st
‘𝐴) ∧ (𝑦 +Q
𝑥) ∈ (2nd
‘𝐵))}〉 ⇒ ⊢ ((𝐴<P 𝐵 ∧ 𝑞 ∈ Q ∧ 𝑞 ∈ (1st
‘𝐶)) →
∃𝑟 ∈
Q (𝑞
<Q 𝑟 ∧ 𝑟 ∈ (1st ‘𝐶))) |
|
Theorem | ltexprlemlol 6792* |
The lower cut of our constructed difference is lower. Lemma for
ltexpri 6803. (Contributed by Jim Kingdon, 21-Dec-2019.)
|
⊢ 𝐶 = 〈{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (1st
‘𝐵))}, {𝑥 ∈ Q ∣
∃𝑦(𝑦 ∈ (1st
‘𝐴) ∧ (𝑦 +Q
𝑥) ∈ (2nd
‘𝐵))}〉 ⇒ ⊢ ((𝐴<P 𝐵 ∧ 𝑞 ∈ Q) →
(∃𝑟 ∈
Q (𝑞
<Q 𝑟 ∧ 𝑟 ∈ (1st ‘𝐶)) → 𝑞 ∈ (1st ‘𝐶))) |
|
Theorem | ltexprlemopu 6793* |
The upper cut of our constructed difference is open. Lemma for
ltexpri 6803. (Contributed by Jim Kingdon, 21-Dec-2019.)
|
⊢ 𝐶 = 〈{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (1st
‘𝐵))}, {𝑥 ∈ Q ∣
∃𝑦(𝑦 ∈ (1st
‘𝐴) ∧ (𝑦 +Q
𝑥) ∈ (2nd
‘𝐵))}〉 ⇒ ⊢ ((𝐴<P 𝐵 ∧ 𝑟 ∈ Q ∧ 𝑟 ∈ (2nd
‘𝐶)) →
∃𝑞 ∈
Q (𝑞
<Q 𝑟 ∧ 𝑞 ∈ (2nd ‘𝐶))) |
|
Theorem | ltexprlemupu 6794* |
The upper cut of our constructed difference is upper. Lemma for
ltexpri 6803. (Contributed by Jim Kingdon, 21-Dec-2019.)
|
⊢ 𝐶 = 〈{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (1st
‘𝐵))}, {𝑥 ∈ Q ∣
∃𝑦(𝑦 ∈ (1st
‘𝐴) ∧ (𝑦 +Q
𝑥) ∈ (2nd
‘𝐵))}〉 ⇒ ⊢ ((𝐴<P 𝐵 ∧ 𝑟 ∈ Q) →
(∃𝑞 ∈
Q (𝑞
<Q 𝑟 ∧ 𝑞 ∈ (2nd ‘𝐶)) → 𝑟 ∈ (2nd ‘𝐶))) |
|
Theorem | ltexprlemrnd 6795* |
Our constructed difference is rounded. Lemma for ltexpri 6803.
(Contributed by Jim Kingdon, 17-Dec-2019.)
|
⊢ 𝐶 = 〈{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (1st
‘𝐵))}, {𝑥 ∈ Q ∣
∃𝑦(𝑦 ∈ (1st
‘𝐴) ∧ (𝑦 +Q
𝑥) ∈ (2nd
‘𝐵))}〉 ⇒ ⊢ (𝐴<P 𝐵 → (∀𝑞 ∈ Q (𝑞 ∈ (1st
‘𝐶) ↔
∃𝑟 ∈
Q (𝑞
<Q 𝑟 ∧ 𝑟 ∈ (1st ‘𝐶))) ∧ ∀𝑟 ∈ Q (𝑟 ∈ (2nd
‘𝐶) ↔
∃𝑞 ∈
Q (𝑞
<Q 𝑟 ∧ 𝑞 ∈ (2nd ‘𝐶))))) |
|
Theorem | ltexprlemdisj 6796* |
Our constructed difference is disjoint. Lemma for ltexpri 6803.
(Contributed by Jim Kingdon, 17-Dec-2019.)
|
⊢ 𝐶 = 〈{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (1st
‘𝐵))}, {𝑥 ∈ Q ∣
∃𝑦(𝑦 ∈ (1st
‘𝐴) ∧ (𝑦 +Q
𝑥) ∈ (2nd
‘𝐵))}〉 ⇒ ⊢ (𝐴<P 𝐵 → ∀𝑞 ∈ Q ¬
(𝑞 ∈ (1st
‘𝐶) ∧ 𝑞 ∈ (2nd
‘𝐶))) |
|
Theorem | ltexprlemloc 6797* |
Our constructed difference is located. Lemma for ltexpri 6803.
(Contributed by Jim Kingdon, 17-Dec-2019.)
|
⊢ 𝐶 = 〈{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (1st
‘𝐵))}, {𝑥 ∈ Q ∣
∃𝑦(𝑦 ∈ (1st
‘𝐴) ∧ (𝑦 +Q
𝑥) ∈ (2nd
‘𝐵))}〉 ⇒ ⊢ (𝐴<P 𝐵 → ∀𝑞 ∈ Q
∀𝑟 ∈
Q (𝑞
<Q 𝑟 → (𝑞 ∈ (1st ‘𝐶) ∨ 𝑟 ∈ (2nd ‘𝐶)))) |
|
Theorem | ltexprlempr 6798* |
Our constructed difference is a positive real. Lemma for ltexpri 6803.
(Contributed by Jim Kingdon, 17-Dec-2019.)
|
⊢ 𝐶 = 〈{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (1st
‘𝐵))}, {𝑥 ∈ Q ∣
∃𝑦(𝑦 ∈ (1st
‘𝐴) ∧ (𝑦 +Q
𝑥) ∈ (2nd
‘𝐵))}〉 ⇒ ⊢ (𝐴<P 𝐵 → 𝐶 ∈ P) |
|
Theorem | ltexprlemfl 6799* |
Lemma for ltexpri 6803. One directon of our result for lower cuts.
(Contributed by Jim Kingdon, 17-Dec-2019.)
|
⊢ 𝐶 = 〈{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (1st
‘𝐵))}, {𝑥 ∈ Q ∣
∃𝑦(𝑦 ∈ (1st
‘𝐴) ∧ (𝑦 +Q
𝑥) ∈ (2nd
‘𝐵))}〉 ⇒ ⊢ (𝐴<P 𝐵 → (1st
‘(𝐴
+P 𝐶)) ⊆ (1st ‘𝐵)) |
|
Theorem | ltexprlemrl 6800* |
Lemma for ltexpri 6803. Reverse directon of our result for lower
cuts.
(Contributed by Jim Kingdon, 17-Dec-2019.)
|
⊢ 𝐶 = 〈{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (1st
‘𝐵))}, {𝑥 ∈ Q ∣
∃𝑦(𝑦 ∈ (1st
‘𝐴) ∧ (𝑦 +Q
𝑥) ∈ (2nd
‘𝐵))}〉 ⇒ ⊢ (𝐴<P 𝐵 → (1st
‘𝐵) ⊆
(1st ‘(𝐴
+P 𝐶))) |