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 18-Apr-2024 at 6:14 AM ET.
Recent Additions to the Intuitionistic Logic Explorer
DateLabelDescription
Theorem
 
4-Apr-2024prodrbdclem 11333 Lemma for prodrbdc 11336. (Contributed by Scott Fenton, 4-Dec-2017.) (Revised by Jim Kingdon, 4-Apr-2024.)
𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))    &   ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → DECID 𝑘 ∈ 𝐴)    &   (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    ⇒   ((𝜑 ∧ 𝐴 ⊆ (ℤ≥‘𝑁)) → (seq𝑀( · , 𝐹) ↾ (ℤ≥‘𝑁)) = seq𝑁( · , 𝐹))
 
24-Mar-2024prodfdivap 11309 The quotient of two products. (Contributed by Scott Fenton, 15-Jan-2018.) (Revised by Jim Kingdon, 24-Mar-2024.)
(𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) ∈ ℂ)    &   ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑘) ∈ ℂ)    &   ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑘) # 0)    &   ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐻‘𝑘) = ((𝐹‘𝑘) / (𝐺‘𝑘)))    ⇒   (𝜑 → (seq𝑀( · , 𝐻)‘𝑁) = ((seq𝑀( · , 𝐹)‘𝑁) / (seq𝑀( · , 𝐺)‘𝑁)))
 
24-Mar-2024prodfrecap 11308 The reciprocal of a finite product. (Contributed by Scott Fenton, 15-Jan-2018.) (Revised by Jim Kingdon, 24-Mar-2024.)
(𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) ∈ ℂ)    &   ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) # 0)    &   ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐺‘𝑘) = (1 / (𝐹‘𝑘)))    &   ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑘) ∈ ℂ)    ⇒   (𝜑 → (seq𝑀( · , 𝐺)‘𝑁) = (1 / (seq𝑀( · , 𝐹)‘𝑁)))
 
23-Mar-2024prodfap0 11307 The product of finitely many terms apart from zero is apart from zero. (Contributed by Scott Fenton, 14-Jan-2018.) (Revised by Jim Kingdon, 23-Mar-2024.)
(𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) ∈ ℂ)    &   ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) # 0)    ⇒   (𝜑 → (seq𝑀( · , 𝐹)‘𝑁) # 0)
 
22-Mar-2024prod3fmul 11303 The product of two infinite products. (Contributed by Scott Fenton, 18-Dec-2017.) (Revised by Jim Kingdon, 22-Mar-2024.)
(𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) ∈ ℂ)    &   ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑘) ∈ ℂ)    &   ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐻‘𝑘) = ((𝐹‘𝑘) · (𝐺‘𝑘)))    ⇒   (𝜑 → (seq𝑀( · , 𝐻)‘𝑁) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq𝑀( · , 𝐺)‘𝑁)))
 
21-Mar-2024df-proddc 11313 Define the product of a series with an index set of integers 𝐴. This definition takes most of the aspects of df-sumdc 11116 and adapts them for multiplication instead of addition. However, we insist that in the infinite case, there is a nonzero tail of the sequence. This ensures that the convergence criteria match those of infinite sums. (Contributed by Scott Fenton, 4-Dec-2017.) (Revised by Jim Kingdon, 21-Mar-2024.)
∏𝑘 ∈ 𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚))))
 
19-Mar-2024cos02pilt1 12921 Cosine is less than one between zero and 2 · π. (Contributed by Jim Kingdon, 19-Mar-2024.)
(𝐴 ∈ (0(,)(2 · π)) → (cos‘𝐴) < 1)
 
19-Mar-2024cosq34lt1 12920 Cosine is less than one in the third and fourth quadrants. (Contributed by Jim Kingdon, 19-Mar-2024.)
(𝐴 ∈ (π[,)(2 · π)) → (cos‘𝐴) < 1)
 
14-Mar-2024coseq0q4123 12904 Location of the zeroes of cosine in (-(π / 2)(,)(3 · (π / 2))). (Contributed by Jim Kingdon, 14-Mar-2024.)
(𝐴 ∈ (-(π / 2)(,)(3 · (π / 2))) → ((cos‘𝐴) = 0 ↔ 𝐴 = (π / 2)))
 
14-Mar-2024cosq23lt0 12903 The cosine of a number in the second and third quadrants is negative. (Contributed by Jim Kingdon, 14-Mar-2024.)
(𝐴 ∈ ((π / 2)(,)(3 · (π / 2))) → (cos‘𝐴) < 0)
 
9-Mar-2024pilem3 12853 Lemma for pi related theorems. (Contributed by Jim Kingdon, 9-Mar-2024.)
(π ∈ (2(,)4) ∧ (sin‘π) = 0)
 
9-Mar-2024exmidonfin 7043 If a finite ordinal is a natural number, excluded middle follows. That excluded middle implies that a finite ordinal is a natural number is proved in the Metamath Proof Explorer. That a natural number is a finite ordinal is shown at nnfi 6759 and nnon 4518. (Contributed by Andrew W Swan and Jim Kingdon, 9-Mar-2024.)
(ω = (On ∩ Fin) → EXMID)
 
9-Mar-2024exmidonfinlem 7042 Lemma for exmidonfin 7043. (Contributed by Andrew W Swan and Jim Kingdon, 9-Mar-2024.)
𝐴 = {{𝑥 ∈ {∅} ∣ 𝜑}, {𝑥 ∈ {∅} ∣ ¬ 𝜑}}    ⇒   (ω = (On ∩ Fin) → DECID 𝜑)
 
8-Mar-2024sin0pilem2 12852 Lemma for pi related theorems. (Contributed by Mario Carneiro and Jim Kingdon, 8-Mar-2024.)
∃𝑞 ∈ (2(,)4)((sin‘𝑞) = 0 ∧ ∀𝑥 ∈ (0(,)𝑞)0 < (sin‘𝑥))
 
8-Mar-2024sin0pilem1 12851 Lemma for pi related theorems. (Contributed by Mario Carneiro and Jim Kingdon, 8-Mar-2024.)
∃𝑝 ∈ (1(,)2)((cos‘𝑝) = 0 ∧ ∀𝑥 ∈ (𝑝(,)(2 · 𝑝))0 < (sin‘𝑥))
 
7-Mar-2024cosz12 12850 Cosine has a zero between 1 and 2. (Contributed by Mario Carneiro and Jim Kingdon, 7-Mar-2024.)
∃𝑝 ∈ (1(,)2)(cos‘𝑝) = 0
 
6-Mar-2024cos12dec 11463 Cosine is decreasing from one to two. (Contributed by Mario Carneiro and Jim Kingdon, 6-Mar-2024.)
((𝐴 ∈ (1[,]2) ∧ 𝐵 ∈ (1[,]2) ∧ 𝐴 < 𝐵) → (cos‘𝐵) < (cos‘𝐴))
 
25-Feb-2024mul2lt0pn 9544 The product of multiplicands of different signs is negative. (Contributed by Jim Kingdon, 25-Feb-2024.)
(𝜑 → 𝐴 ∈ ℝ)    &   (𝜑 → 𝐵 ∈ ℝ)    &   (𝜑 → 𝐴 < 0)    &   (𝜑 → 0 < 𝐵)    ⇒   (𝜑 → (𝐵 · 𝐴) < 0)
 
25-Feb-2024mul2lt0np 9543 The product of multiplicands of different signs is negative. (Contributed by Jim Kingdon, 25-Feb-2024.)
(𝜑 → 𝐴 ∈ ℝ)    &   (𝜑 → 𝐵 ∈ ℝ)    &   (𝜑 → 𝐴 < 0)    &   (𝜑 → 0 < 𝐵)    ⇒   (𝜑 → (𝐴 · 𝐵) < 0)
 
25-Feb-2024lt0ap0 8403 A number which is less than zero is apart from zero. (Contributed by Jim Kingdon, 25-Feb-2024.)
((𝐴 ∈ ℝ ∧ 𝐴 < 0) → 𝐴 # 0)
 
25-Feb-2024negap0d 8386 The negative of a number apart from zero is apart from zero. (Contributed by Jim Kingdon, 25-Feb-2024.)
(𝜑 → 𝐴 ∈ ℂ)    &   (𝜑 → 𝐴 # 0)    ⇒   (𝜑 → -𝐴 # 0)
 
24-Feb-2024lt0ap0d 8404 A real number less than zero is apart from zero. Deduction form. (Contributed by Jim Kingdon, 24-Feb-2024.)
(𝜑 → 𝐴 ∈ ℝ)    &   (𝜑 → 𝐴 < 0)    ⇒   (𝜑 → 𝐴 # 0)
 
20-Feb-2024ivthdec 12780 The intermediate value theorem, decreasing case, for a strictly monotonic function. (Contributed by Jim Kingdon, 20-Feb-2024.)
(𝜑 → 𝐴 ∈ ℝ)    &   (𝜑 → 𝐵 ∈ ℝ)    &   (𝜑 → 𝑈 ∈ ℝ)    &   (𝜑 → 𝐴 < 𝐵)    &   (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)    &   (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ))    &   ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ)    &   (𝜑 → ((𝐹‘𝐵) < 𝑈 ∧ 𝑈 < (𝐹‘𝐴)))    &   (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑥 < 𝑦)) → (𝐹‘𝑦) < (𝐹‘𝑥))    ⇒   (𝜑 → ∃𝑐 ∈ (𝐴(,)𝐵)(𝐹‘𝑐) = 𝑈)
 
20-Feb-2024ivthinclemex 12778 Lemma for ivthinc 12779. Existence of a number between the lower cut and the upper cut. (Contributed by Jim Kingdon, 20-Feb-2024.)
(𝜑 → 𝐴 ∈ ℝ)    &   (𝜑 → 𝐵 ∈ ℝ)    &   (𝜑 → 𝑈 ∈ ℝ)    &   (𝜑 → 𝐴 < 𝐵)    &   (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)    &   (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ))    &   ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ)    &   (𝜑 → ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵)))    &   (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑥 < 𝑦)) → (𝐹‘𝑥) < (𝐹‘𝑦))    &   𝐿 = {𝑤 ∈ (𝐴[,]𝐵) ∣ (𝐹‘𝑤) < 𝑈}    &   𝑅 = {𝑤 ∈ (𝐴[,]𝐵) ∣ 𝑈 < (𝐹‘𝑤)}    ⇒   (𝜑 → ∃!𝑧 ∈ (𝐴(,)𝐵)(∀𝑞 ∈ 𝐿 𝑞 < 𝑧 ∧ ∀𝑟 ∈ 𝑅 𝑧 < 𝑟))
 
19-Feb-2024ivthinclemuopn 12774 Lemma for ivthinc 12779. The upper cut is open. (Contributed by Jim Kingdon, 19-Feb-2024.)
(𝜑 → 𝐴 ∈ ℝ)    &   (𝜑 → 𝐵 ∈ ℝ)    &   (𝜑 → 𝑈 ∈ ℝ)    &   (𝜑 → 𝐴 < 𝐵)    &   (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)    &   (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ))    &   ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ)    &   (𝜑 → ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵)))    &   (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑥 < 𝑦)) → (𝐹‘𝑥) < (𝐹‘𝑦))    &   𝐿 = {𝑤 ∈ (𝐴[,]𝐵) ∣ (𝐹‘𝑤) < 𝑈}    &   𝑅 = {𝑤 ∈ (𝐴[,]𝐵) ∣ 𝑈 < (𝐹‘𝑤)}    &   (𝜑 → 𝑆 ∈ 𝑅)    ⇒   (𝜑 → ∃𝑞 ∈ 𝑅 𝑞 < 𝑆)
 
19-Feb-2024dedekindicc 12769 A Dedekind cut identifies a unique real number. Similar to df-inp 7267 except that the Dedekind cut is formed by sets of reals (rather than positive rationals). But in both cases the defining property of a Dedekind cut is that it is inhabited (bounded), rounded, disjoint, and located. (Contributed by Jim Kingdon, 19-Feb-2024.)
(𝜑 → 𝐴 ∈ ℝ)    &   (𝜑 → 𝐵 ∈ ℝ)    &   (𝜑 → 𝐿 ⊆ (𝐴[,]𝐵))    &   (𝜑 → 𝑈 ⊆ (𝐴[,]𝐵))    &   (𝜑 → ∃𝑞 ∈ (𝐴[,]𝐵)𝑞 ∈ 𝐿)    &   (𝜑 → ∃𝑟 ∈ (𝐴[,]𝐵)𝑟 ∈ 𝑈)    &   (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)(𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))    &   (𝜑 → ∀𝑟 ∈ (𝐴[,]𝐵)(𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟))    &   (𝜑 → (𝐿 ∩ 𝑈) = ∅)    &   (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)∀𝑟 ∈ (𝐴[,]𝐵)(𝑞 < 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈)))    &   (𝜑 → 𝐴 < 𝐵)    ⇒   (𝜑 → ∃!𝑥 ∈ (𝐴(,)𝐵)(∀𝑞 ∈ 𝐿 𝑞 < 𝑥 ∧ ∀𝑟 ∈ 𝑈 𝑥 < 𝑟))
 
18-Feb-2024ivthinclemloc 12777 Lemma for ivthinc 12779. Locatedness. (Contributed by Jim Kingdon, 18-Feb-2024.)
(𝜑 → 𝐴 ∈ ℝ)    &   (𝜑 → 𝐵 ∈ ℝ)    &   (𝜑 → 𝑈 ∈ ℝ)    &   (𝜑 → 𝐴 < 𝐵)    &   (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)    &   (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ))    &   ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ)    &   (𝜑 → ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵)))    &   (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑥 < 𝑦)) → (𝐹‘𝑥) < (𝐹‘𝑦))    &   𝐿 = {𝑤 ∈ (𝐴[,]𝐵) ∣ (𝐹‘𝑤) < 𝑈}    &   𝑅 = {𝑤 ∈ (𝐴[,]𝐵) ∣ 𝑈 < (𝐹‘𝑤)}    ⇒   (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)∀𝑟 ∈ (𝐴[,]𝐵)(𝑞 < 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑅)))
 
18-Feb-2024ivthinclemdisj 12776 Lemma for ivthinc 12779. The lower and upper cuts are disjoint. (Contributed by Jim Kingdon, 18-Feb-2024.)
(𝜑 → 𝐴 ∈ ℝ)    &   (𝜑 → 𝐵 ∈ ℝ)    &   (𝜑 → 𝑈 ∈ ℝ)    &   (𝜑 → 𝐴 < 𝐵)    &   (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)    &   (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ))    &   ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ)    &   (𝜑 → ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵)))    &   (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑥 < 𝑦)) → (𝐹‘𝑥) < (𝐹‘𝑦))    &   𝐿 = {𝑤 ∈ (𝐴[,]𝐵) ∣ (𝐹‘𝑤) < 𝑈}    &   𝑅 = {𝑤 ∈ (𝐴[,]𝐵) ∣ 𝑈 < (𝐹‘𝑤)}    ⇒   (𝜑 → (𝐿 ∩ 𝑅) = ∅)
 
18-Feb-2024ivthinclemur 12775 Lemma for ivthinc 12779. The upper cut is rounded. (Contributed by Jim Kingdon, 18-Feb-2024.)
(𝜑 → 𝐴 ∈ ℝ)    &   (𝜑 → 𝐵 ∈ ℝ)    &   (𝜑 → 𝑈 ∈ ℝ)    &   (𝜑 → 𝐴 < 𝐵)    &   (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)    &   (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ))    &   ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ)    &   (𝜑 → ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵)))    &   (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑥 < 𝑦)) → (𝐹‘𝑥) < (𝐹‘𝑦))    &   𝐿 = {𝑤 ∈ (𝐴[,]𝐵) ∣ (𝐹‘𝑤) < 𝑈}    &   𝑅 = {𝑤 ∈ (𝐴[,]𝐵) ∣ 𝑈 < (𝐹‘𝑤)}    ⇒   (𝜑 → ∀𝑟 ∈ (𝐴[,]𝐵)(𝑟 ∈ 𝑅 ↔ ∃𝑞 ∈ 𝑅 𝑞 < 𝑟))
 
18-Feb-2024ivthinclemlr 12773 Lemma for ivthinc 12779. The lower cut is rounded. (Contributed by Jim Kingdon, 18-Feb-2024.)
(𝜑 → 𝐴 ∈ ℝ)    &   (𝜑 → 𝐵 ∈ ℝ)    &   (𝜑 → 𝑈 ∈ ℝ)    &   (𝜑 → 𝐴 < 𝐵)    &   (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)    &   (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ))    &   ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ)    &   (𝜑 → ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵)))    &   (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑥 < 𝑦)) → (𝐹‘𝑥) < (𝐹‘𝑦))    &   𝐿 = {𝑤 ∈ (𝐴[,]𝐵) ∣ (𝐹‘𝑤) < 𝑈}    &   𝑅 = {𝑤 ∈ (𝐴[,]𝐵) ∣ 𝑈 < (𝐹‘𝑤)}    ⇒   (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)(𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))
 
18-Feb-2024ivthinclemum 12771 Lemma for ivthinc 12779. The upper cut is bounded. (Contributed by Jim Kingdon, 18-Feb-2024.)
(𝜑 → 𝐴 ∈ ℝ)    &   (𝜑 → 𝐵 ∈ ℝ)    &   (𝜑 → 𝑈 ∈ ℝ)    &   (𝜑 → 𝐴 < 𝐵)    &   (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)    &   (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ))    &   ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ)    &   (𝜑 → ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵)))    &   (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑥 < 𝑦)) → (𝐹‘𝑥) < (𝐹‘𝑦))    &   𝐿 = {𝑤 ∈ (𝐴[,]𝐵) ∣ (𝐹‘𝑤) < 𝑈}    &   𝑅 = {𝑤 ∈ (𝐴[,]𝐵) ∣ 𝑈 < (𝐹‘𝑤)}    ⇒   (𝜑 → ∃𝑟 ∈ (𝐴[,]𝐵)𝑟 ∈ 𝑅)
 
18-Feb-2024ivthinclemlm 12770 Lemma for ivthinc 12779. The lower cut is bounded. (Contributed by Jim Kingdon, 18-Feb-2024.)
(𝜑 → 𝐴 ∈ ℝ)    &   (𝜑 → 𝐵 ∈ ℝ)    &   (𝜑 → 𝑈 ∈ ℝ)    &   (𝜑 → 𝐴 < 𝐵)    &   (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)    &   (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ))    &   ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ)    &   (𝜑 → ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵)))    &   (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑥 < 𝑦)) → (𝐹‘𝑥) < (𝐹‘𝑦))    &   𝐿 = {𝑤 ∈ (𝐴[,]𝐵) ∣ (𝐹‘𝑤) < 𝑈}    &   𝑅 = {𝑤 ∈ (𝐴[,]𝐵) ∣ 𝑈 < (𝐹‘𝑤)}    ⇒   (𝜑 → ∃𝑞 ∈ (𝐴[,]𝐵)𝑞 ∈ 𝐿)
 
15-Feb-2024dedekindicclemeu 12767 Lemma for dedekindicc 12769. Part of proving uniqueness. (Contributed by Jim Kingdon, 15-Feb-2024.)
(𝜑 → 𝐴 ∈ ℝ)    &   (𝜑 → 𝐵 ∈ ℝ)    &   (𝜑 → 𝐿 ⊆ (𝐴[,]𝐵))    &   (𝜑 → 𝑈 ⊆ (𝐴[,]𝐵))    &   (𝜑 → ∃𝑞 ∈ (𝐴[,]𝐵)𝑞 ∈ 𝐿)    &   (𝜑 → ∃𝑟 ∈ (𝐴[,]𝐵)𝑟 ∈ 𝑈)    &   (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)(𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))    &   (𝜑 → ∀𝑟 ∈ (𝐴[,]𝐵)(𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟))    &   (𝜑 → (𝐿 ∩ 𝑈) = ∅)    &   (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)∀𝑟 ∈ (𝐴[,]𝐵)(𝑞 < 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈)))    &   (𝜑 → 𝐴 < 𝐵)    &   (𝜑 → 𝐶 ∈ (𝐴[,]𝐵))    &   (𝜑 → (∀𝑞 ∈ 𝐿 𝑞 < 𝐶 ∧ ∀𝑟 ∈ 𝑈 𝐶 < 𝑟))    &   (𝜑 → 𝐷 ∈ (𝐴[,]𝐵))    &   (𝜑 → (∀𝑞 ∈ 𝐿 𝑞 < 𝐷 ∧ ∀𝑟 ∈ 𝑈 𝐷 < 𝑟))    &   (𝜑 → 𝐶 < 𝐷)    ⇒   (𝜑 → ⊥)
 
15-Feb-2024dedekindicclemlu 12766 Lemma for dedekindicc 12769. There is a number which separates the lower and upper cuts. (Contributed by Jim Kingdon, 15-Feb-2024.)
(𝜑 → 𝐴 ∈ ℝ)    &   (𝜑 → 𝐵 ∈ ℝ)    &   (𝜑 → 𝐿 ⊆ (𝐴[,]𝐵))    &   (𝜑 → 𝑈 ⊆ (𝐴[,]𝐵))    &   (𝜑 → ∃𝑞 ∈ (𝐴[,]𝐵)𝑞 ∈ 𝐿)    &   (𝜑 → ∃𝑟 ∈ (𝐴[,]𝐵)𝑟 ∈ 𝑈)    &   (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)(𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))    &   (𝜑 → ∀𝑟 ∈ (𝐴[,]𝐵)(𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟))    &   (𝜑 → (𝐿 ∩ 𝑈) = ∅)    &   (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)∀𝑟 ∈ (𝐴[,]𝐵)(𝑞 < 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈)))    &   (𝜑 → 𝐴 < 𝐵)    ⇒   (𝜑 → ∃𝑥 ∈ (𝐴[,]𝐵)(∀𝑞 ∈ 𝐿 𝑞 < 𝑥 ∧ ∀𝑟 ∈ 𝑈 𝑥 < 𝑟))
 
15-Feb-2024dedekindicclemlub 12765 Lemma for dedekindicc 12769. The set L has a least upper bound. (Contributed by Jim Kingdon, 15-Feb-2024.)
(𝜑 → 𝐴 ∈ ℝ)    &   (𝜑 → 𝐵 ∈ ℝ)    &   (𝜑 → 𝐿 ⊆ (𝐴[,]𝐵))    &   (𝜑 → 𝑈 ⊆ (𝐴[,]𝐵))    &   (𝜑 → ∃𝑞 ∈ (𝐴[,]𝐵)𝑞 ∈ 𝐿)    &   (𝜑 → ∃𝑟 ∈ (𝐴[,]𝐵)𝑟 ∈ 𝑈)    &   (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)(𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))    &   (𝜑 → ∀𝑟 ∈ (𝐴[,]𝐵)(𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟))    &   (𝜑 → (𝐿 ∩ 𝑈) = ∅)    &   (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)∀𝑟 ∈ (𝐴[,]𝐵)(𝑞 < 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈)))    &   (𝜑 → 𝐴 < 𝐵)    ⇒   (𝜑 → ∃𝑥 ∈ (𝐴[,]𝐵)(∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧)))
 
15-Feb-2024dedekindicclemloc 12764 Lemma for dedekindicc 12769. The set L is located. (Contributed by Jim Kingdon, 15-Feb-2024.)
(𝜑 → 𝐴 ∈ ℝ)    &   (𝜑 → 𝐵 ∈ ℝ)    &   (𝜑 → 𝐿 ⊆ (𝐴[,]𝐵))    &   (𝜑 → 𝑈 ⊆ (𝐴[,]𝐵))    &   (𝜑 → ∃𝑞 ∈ (𝐴[,]𝐵)𝑞 ∈ 𝐿)    &   (𝜑 → ∃𝑟 ∈ (𝐴[,]𝐵)𝑟 ∈ 𝑈)    &   (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)(𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))    &   (𝜑 → ∀𝑟 ∈ (𝐴[,]𝐵)(𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟))    &   (𝜑 → (𝐿 ∩ 𝑈) = ∅)    &   (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)∀𝑟 ∈ (𝐴[,]𝐵)(𝑞 < 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈)))    ⇒   (𝜑 → ∀𝑥 ∈ (𝐴[,]𝐵)∀𝑦 ∈ (𝐴[,]𝐵)(𝑥 < 𝑦 → (∃𝑧 ∈ 𝐿 𝑥 < 𝑧 ∨ ∀𝑧 ∈ 𝐿 𝑧 < 𝑦)))
 
15-Feb-2024dedekindicclemub 12763 Lemma for dedekindicc 12769. The lower cut has an upper bound. (Contributed by Jim Kingdon, 15-Feb-2024.)
(𝜑 → 𝐴 ∈ ℝ)    &   (𝜑 → 𝐵 ∈ ℝ)    &   (𝜑 → 𝐿 ⊆ (𝐴[,]𝐵))    &   (𝜑 → 𝑈 ⊆ (𝐴[,]𝐵))    &   (𝜑 → ∃𝑞 ∈ (𝐴[,]𝐵)𝑞 ∈ 𝐿)    &   (𝜑 → ∃𝑟 ∈ (𝐴[,]𝐵)𝑟 ∈ 𝑈)    &   (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)(𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))    &   (𝜑 → ∀𝑟 ∈ (𝐴[,]𝐵)(𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟))    &   (𝜑 → (𝐿 ∩ 𝑈) = ∅)    &   (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)∀𝑟 ∈ (𝐴[,]𝐵)(𝑞 < 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈)))    ⇒   (𝜑 → ∃𝑥 ∈ (𝐴[,]𝐵)∀𝑦 ∈ 𝐿 𝑦 < 𝑥)
 
15-Feb-2024dedekindicclemuub 12762 Lemma for dedekindicc 12769. Any element of the upper cut is an upper bound for the lower cut. (Contributed by Jim Kingdon, 15-Feb-2024.)
(𝜑 → 𝐴 ∈ ℝ)    &   (𝜑 → 𝐵 ∈ ℝ)    &   (𝜑 → 𝐿 ⊆ (𝐴[,]𝐵))    &   (𝜑 → 𝑈 ⊆ (𝐴[,]𝐵))    &   (𝜑 → ∃𝑞 ∈ (𝐴[,]𝐵)𝑞 ∈ 𝐿)    &   (𝜑 → ∃𝑟 ∈ (𝐴[,]𝐵)𝑟 ∈ 𝑈)    &   (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)(𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))    &   (𝜑 → ∀𝑟 ∈ (𝐴[,]𝐵)(𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟))    &   (𝜑 → (𝐿 ∩ 𝑈) = ∅)    &   (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)∀𝑟 ∈ (𝐴[,]𝐵)(𝑞 < 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈)))    &   (𝜑 → 𝐶 ∈ 𝑈)    ⇒   (𝜑 → ∀𝑧 ∈ 𝐿 𝑧 < 𝐶)
 
14-Feb-2024suplociccex 12761 An inhabited, bounded-above, located set of reals in a closed interval has a supremum. A similar theorem is axsuploc 7830 but that one is for the entire real line rather than a closed interval. (Contributed by Jim Kingdon, 14-Feb-2024.)
(𝜑 → 𝐵 ∈ ℝ)    &   (𝜑 → 𝐶 ∈ ℝ)    &   (𝜑 → 𝐵 < 𝐶)    &   (𝜑 → 𝐴 ⊆ (𝐵[,]𝐶))    &   (𝜑 → ∃𝑥 𝑥 ∈ 𝐴)    &   (𝜑 → ∀𝑥 ∈ (𝐵[,]𝐶)∀𝑦 ∈ (𝐵[,]𝐶)(𝑥 < 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 < 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 < 𝑦)))    ⇒   (𝜑 → ∃𝑥 ∈ (𝐵[,]𝐶)(∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐵[,]𝐶)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)))
 
14-Feb-2024suplociccreex 12760 An inhabited, bounded-above, located set of reals in a closed interval has a supremum. A similar theorem is axsuploc 7830 but that one is for the entire real line rather than a closed interval. (Contributed by Jim Kingdon, 14-Feb-2024.)
(𝜑 → 𝐵 ∈ ℝ)    &   (𝜑 → 𝐶 ∈ ℝ)    &   (𝜑 → 𝐵 < 𝐶)    &   (𝜑 → 𝐴 ⊆ (𝐵[,]𝐶))    &   (𝜑 → ∃𝑥 𝑥 ∈ 𝐴)    &   (𝜑 → ∀𝑥 ∈ (𝐵[,]𝐶)∀𝑦 ∈ (𝐵[,]𝐶)(𝑥 < 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 < 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 < 𝑦)))    ⇒   (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)))
 
6-Feb-2024ivthinclemlopn 12772 Lemma for ivthinc 12779. The lower cut is open. (Contributed by Jim Kingdon, 6-Feb-2024.)
(𝜑 → 𝐴 ∈ ℝ)    &   (𝜑 → 𝐵 ∈ ℝ)    &   (𝜑 → 𝑈 ∈ ℝ)    &   (𝜑 → 𝐴 < 𝐵)    &   (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)    &   (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ))    &   ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ)    &   (𝜑 → ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵)))    &   (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑥 < 𝑦)) → (𝐹‘𝑥) < (𝐹‘𝑦))    &   𝐿 = {𝑤 ∈ (𝐴[,]𝐵) ∣ (𝐹‘𝑤) < 𝑈}    &   𝑅 = {𝑤 ∈ (𝐴[,]𝐵) ∣ 𝑈 < (𝐹‘𝑤)}    &   (𝜑 → 𝑄 ∈ 𝐿)    ⇒   (𝜑 → ∃𝑟 ∈ 𝐿 𝑄 < 𝑟)
 
5-Feb-2024ivthinc 12779 The intermediate value theorem, increasing case, for a strictly monotonic function. Theorem 5.5 of [Bauer], p. 494. This is Metamath 100 proof #79. (Contributed by Jim Kingdon, 5-Feb-2024.)
(𝜑 → 𝐴 ∈ ℝ)    &   (𝜑 → 𝐵 ∈ ℝ)    &   (𝜑 → 𝑈 ∈ ℝ)    &   (𝜑 → 𝐴 < 𝐵)    &   (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)    &   (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ))    &   ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ)    &   (𝜑 → ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵)))    &   (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑥 < 𝑦)) → (𝐹‘𝑥) < (𝐹‘𝑦))    ⇒   (𝜑 → ∃𝑐 ∈ (𝐴(,)𝐵)(𝐹‘𝑐) = 𝑈)
 
2-Feb-2024dedekindeulemuub 12753 Lemma for dedekindeu 12759. Any element of the upper cut is an upper bound for the lower cut. (Contributed by Jim Kingdon, 2-Feb-2024.)
(𝜑 → 𝐿 ⊆ ℝ)    &   (𝜑 → 𝑈 ⊆ ℝ)    &   (𝜑 → ∃𝑞 ∈ ℝ 𝑞 ∈ 𝐿)    &   (𝜑 → ∃𝑟 ∈ ℝ 𝑟 ∈ 𝑈)    &   (𝜑 → ∀𝑞 ∈ ℝ (𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))    &   (𝜑 → ∀𝑟 ∈ ℝ (𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟))    &   (𝜑 → (𝐿 ∩ 𝑈) = ∅)    &   (𝜑 → ∀𝑞 ∈ ℝ ∀𝑟 ∈ ℝ (𝑞 < 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈)))    &   (𝜑 → 𝐴 ∈ 𝑈)    ⇒   (𝜑 → ∀𝑧 ∈ 𝐿 𝑧 < 𝐴)
 
31-Jan-2024dedekindeulemeu 12758 Lemma for dedekindeu 12759. Part of proving uniqueness. (Contributed by Jim Kingdon, 31-Jan-2024.)
(𝜑 → 𝐿 ⊆ ℝ)    &   (𝜑 → 𝑈 ⊆ ℝ)    &   (𝜑 → ∃𝑞 ∈ ℝ 𝑞 ∈ 𝐿)    &   (𝜑 → ∃𝑟 ∈ ℝ 𝑟 ∈ 𝑈)    &   (𝜑 → ∀𝑞 ∈ ℝ (𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))    &   (𝜑 → ∀𝑟 ∈ ℝ (𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟))    &   (𝜑 → (𝐿 ∩ 𝑈) = ∅)    &   (𝜑 → ∀𝑞 ∈ ℝ ∀𝑟 ∈ ℝ (𝑞 < 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈)))    &   (𝜑 → 𝐴 ∈ ℝ)    &   (𝜑 → (∀𝑞 ∈ 𝐿 𝑞 < 𝐴 ∧ ∀𝑟 ∈ 𝑈 𝐴 < 𝑟))    &   (𝜑 → 𝐵 ∈ ℝ)    &   (𝜑 → (∀𝑞 ∈ 𝐿 𝑞 < 𝐵 ∧ ∀𝑟 ∈ 𝑈 𝐵 < 𝑟))    &   (𝜑 → 𝐴 < 𝐵)    ⇒   (𝜑 → ⊥)
 
31-Jan-2024dedekindeulemlu 12757 Lemma for dedekindeu 12759. There is a number which separates the lower and upper cuts. (Contributed by Jim Kingdon, 31-Jan-2024.)
(𝜑 → 𝐿 ⊆ ℝ)    &   (𝜑 → 𝑈 ⊆ ℝ)    &   (𝜑 → ∃𝑞 ∈ ℝ 𝑞 ∈ 𝐿)    &   (𝜑 → ∃𝑟 ∈ ℝ 𝑟 ∈ 𝑈)    &   (𝜑 → ∀𝑞 ∈ ℝ (𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))    &   (𝜑 → ∀𝑟 ∈ ℝ (𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟))    &   (𝜑 → (𝐿 ∩ 𝑈) = ∅)    &   (𝜑 → ∀𝑞 ∈ ℝ ∀𝑟 ∈ ℝ (𝑞 < 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈)))    ⇒   (𝜑 → ∃𝑥 ∈ ℝ (∀𝑞 ∈ 𝐿 𝑞 < 𝑥 ∧ ∀𝑟 ∈ 𝑈 𝑥 < 𝑟))
 
31-Jan-2024dedekindeulemlub 12756 Lemma for dedekindeu 12759. The set L has a least upper bound. (Contributed by Jim Kingdon, 31-Jan-2024.)
(𝜑 → 𝐿 ⊆ ℝ)    &   (𝜑 → 𝑈 ⊆ ℝ)    &   (𝜑 → ∃𝑞 ∈ ℝ 𝑞 ∈ 𝐿)    &   (𝜑 → ∃𝑟 ∈ ℝ 𝑟 ∈ 𝑈)    &   (𝜑 → ∀𝑞 ∈ ℝ (𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))    &   (𝜑 → ∀𝑟 ∈ ℝ (𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟))    &   (𝜑 → (𝐿 ∩ 𝑈) = ∅)    &   (𝜑 → ∀𝑞 ∈ ℝ ∀𝑟 ∈ ℝ (𝑞 < 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈)))    ⇒   (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧)))
 
31-Jan-2024dedekindeulemloc 12755 Lemma for dedekindeu 12759. The set L is located. (Contributed by Jim Kingdon, 31-Jan-2024.)
(𝜑 → 𝐿 ⊆ ℝ)    &   (𝜑 → 𝑈 ⊆ ℝ)    &   (𝜑 → ∃𝑞 ∈ ℝ 𝑞 ∈ 𝐿)    &   (𝜑 → ∃𝑟 ∈ ℝ 𝑟 ∈ 𝑈)    &   (𝜑 → ∀𝑞 ∈ ℝ (𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))    &   (𝜑 → ∀𝑟 ∈ ℝ (𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟))    &   (𝜑 → (𝐿 ∩ 𝑈) = ∅)    &   (𝜑 → ∀𝑞 ∈ ℝ ∀𝑟 ∈ ℝ (𝑞 < 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈)))    ⇒   (𝜑 → ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → (∃𝑧 ∈ 𝐿 𝑥 < 𝑧 ∨ ∀𝑧 ∈ 𝐿 𝑧 < 𝑦)))
 
31-Jan-2024dedekindeulemub 12754 Lemma for dedekindeu 12759. The lower cut has an upper bound. (Contributed by Jim Kingdon, 31-Jan-2024.)
(𝜑 → 𝐿 ⊆ ℝ)    &   (𝜑 → 𝑈 ⊆ ℝ)    &   (𝜑 → ∃𝑞 ∈ ℝ 𝑞 ∈ 𝐿)    &   (𝜑 → ∃𝑟 ∈ ℝ 𝑟 ∈ 𝑈)    &   (𝜑 → ∀𝑞 ∈ ℝ (𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))    &   (𝜑 → ∀𝑟 ∈ ℝ (𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟))    &   (𝜑 → (𝐿 ∩ 𝑈) = ∅)    &   (𝜑 → ∀𝑞 ∈ ℝ ∀𝑟 ∈ ℝ (𝑞 < 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈)))    ⇒   (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐿 𝑦 < 𝑥)
 
30-Jan-2024axsuploc 7830 An inhabited, bounded-above, located set of reals has a supremum. Axiom for real and complex numbers, derived from ZF set theory. (This restates ax-pre-suploc 7734 with ordering on the extended reals.) (Contributed by Jim Kingdon, 30-Jan-2024.)
(((𝐴 ⊆ ℝ ∧ ∃𝑥 𝑥 ∈ 𝐴) ∧ (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 < 𝑥 ∧ ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 < 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 < 𝑦)))) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)))
 
24-Jan-2024axpre-suploclemres 7702 Lemma for axpre-suploc 7703. The result. The proof just needs to define 𝐵 as basically the same set as 𝐴 (but expressed as a subset of R rather than a subset of ℝ), and apply suplocsr 7610. (Contributed by Jim Kingdon, 24-Jan-2024.)
(𝜑 → 𝐴 ⊆ ℝ)    &   (𝜑 → 𝐶 ∈ 𝐴)    &   (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥)    &   (𝜑 → ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 <ℝ 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 <ℝ 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 <ℝ 𝑦)))    &   𝐵 = {𝑤 ∈ R ∣ ⟨𝑤, 0R⟩ ∈ 𝐴}    ⇒   (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <ℝ 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)))
 
23-Jan-2024ax-pre-suploc 7734 An inhabited, bounded-above, located set of reals has a supremum.

Locatedness here means that given 𝑥 < 𝑦, either there is an element of the set greater than 𝑥, or 𝑦 is an upper bound.

Although this and ax-caucvg 7733 are both completeness properties, countable choice would probably be needed to derive this from ax-caucvg 7733.

(Contributed by Jim Kingdon, 23-Jan-2024.)

(((𝐴 ⊆ ℝ ∧ ∃𝑥 𝑥 ∈ 𝐴) ∧ (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥 ∧ ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 <ℝ 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 <ℝ 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 <ℝ 𝑦)))) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <ℝ 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)))
 
23-Jan-2024axpre-suploc 7703 An inhabited, bounded-above, located set of reals has a supremum.

Locatedness here means that given 𝑥 < 𝑦, either there is an element of the set greater than 𝑥, or 𝑦 is an upper bound.

This construction-dependent theorem should not be referenced directly; instead, use ax-pre-suploc 7734. (Contributed by Jim Kingdon, 23-Jan-2024.) (New usage is discouraged.)

(((𝐴 ⊆ ℝ ∧ ∃𝑥 𝑥 ∈ 𝐴) ∧ (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥 ∧ ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 <ℝ 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 <ℝ 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 <ℝ 𝑦)))) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <ℝ 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)))
 
22-Jan-2024suplocsr 7610 An inhabited, bounded, located set of signed reals has a supremum. (Contributed by Jim Kingdon, 22-Jan-2024.)
(𝜑 → ∃𝑥 𝑥 ∈ 𝐴)    &   (𝜑 → ∃𝑥 ∈ R ∀𝑦 ∈ 𝐴 𝑦 <R 𝑥)    &   (𝜑 → ∀𝑥 ∈ R ∀𝑦 ∈ R (𝑥 <R 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 <R 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 <R 𝑦)))    ⇒   (𝜑 → ∃𝑥 ∈ R (∀𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀𝑦 ∈ R (𝑦 <R 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)))
 
21-Jan-2024bj-el2oss1o 12970 Shorter proof of el2oss1o 13177 using more axioms. (Contributed by BJ, 21-Jan-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
(𝐴 ∈ 2o → 𝐴 ⊆ 1o)
 
21-Jan-2024ltm1sr 7578 Adding minus one to a signed real yields a smaller signed real. (Contributed by Jim Kingdon, 21-Jan-2024.)
(𝐴 ∈ R → (𝐴 +R -1R) <R 𝐴)
 
19-Jan-2024suplocsrlempr 7608 Lemma for suplocsr 7610. The set 𝐵 has a least upper bound. (Contributed by Jim Kingdon, 19-Jan-2024.)
𝐵 = {𝑤 ∈ P ∣ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) ∈ 𝐴}    &   (𝜑 → 𝐴 ⊆ R)    &   (𝜑 → 𝐶 ∈ 𝐴)    &   (𝜑 → ∃𝑥 ∈ R ∀𝑦 ∈ 𝐴 𝑦 <R 𝑥)    &   (𝜑 → ∀𝑥 ∈ R ∀𝑦 ∈ R (𝑥 <R 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 <R 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 <R 𝑦)))    ⇒   (𝜑 → ∃𝑣 ∈ P (∀𝑤 ∈ 𝐵 ¬ 𝑣<P 𝑤 ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)))
 
18-Jan-2024suplocsrlemb 7607 Lemma for suplocsr 7610. The set 𝐵 is located. (Contributed by Jim Kingdon, 18-Jan-2024.)
𝐵 = {𝑤 ∈ P ∣ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) ∈ 𝐴}    &   (𝜑 → 𝐴 ⊆ R)    &   (𝜑 → 𝐶 ∈ 𝐴)    &   (𝜑 → ∃𝑥 ∈ R ∀𝑦 ∈ 𝐴 𝑦 <R 𝑥)    &   (𝜑 → ∀𝑥 ∈ R ∀𝑦 ∈ R (𝑥 <R 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 <R 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 <R 𝑦)))    ⇒   (𝜑 → ∀𝑢 ∈ P ∀𝑣 ∈ P (𝑢<P 𝑣 → (∃𝑞 ∈ 𝐵 𝑢<P 𝑞 ∨ ∀𝑞 ∈ 𝐵 𝑞<P 𝑣)))
 
16-Jan-2024suplocsrlem 7609 Lemma for suplocsr 7610. The set 𝐴 has a least upper bound. (Contributed by Jim Kingdon, 16-Jan-2024.)
𝐵 = {𝑤 ∈ P ∣ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) ∈ 𝐴}    &   (𝜑 → 𝐴 ⊆ R)    &   (𝜑 → 𝐶 ∈ 𝐴)    &   (𝜑 → ∃𝑥 ∈ R ∀𝑦 ∈ 𝐴 𝑦 <R 𝑥)    &   (𝜑 → ∀𝑥 ∈ R ∀𝑦 ∈ R (𝑥 <R 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 <R 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 <R 𝑦)))    ⇒   (𝜑 → ∃𝑥 ∈ R (∀𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀𝑦 ∈ R (𝑦 <R 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)))
 
14-Jan-2024suplocexprlemlub 7525 Lemma for suplocexpr 7526. The putative supremum is a least upper bound. (Contributed by Jim Kingdon, 14-Jan-2024.)
(𝜑 → ∃𝑥 𝑥 ∈ 𝐴)    &   (𝜑 → ∃𝑥 ∈ P ∀𝑦 ∈ 𝐴 𝑦<P 𝑥)    &   (𝜑 → ∀𝑥 ∈ P ∀𝑦 ∈ P (𝑥<P 𝑦 → (∃𝑧 ∈ 𝐴 𝑥<P 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧<P 𝑦)))    &   𝐵 = ⟨∪ (1st “ 𝐴), {𝑢 ∈ Q ∣ ∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑢}⟩    ⇒   (𝜑 → (𝑦<P 𝐵 → ∃𝑧 ∈ 𝐴 𝑦<P 𝑧))
 
14-Jan-2024suplocexprlemub 7524 Lemma for suplocexpr 7526. The putative supremum is an upper bound. (Contributed by Jim Kingdon, 14-Jan-2024.)
(𝜑 → ∃𝑥 𝑥 ∈ 𝐴)    &   (𝜑 → ∃𝑥 ∈ P ∀𝑦 ∈ 𝐴 𝑦<P 𝑥)    &   (𝜑 → ∀𝑥 ∈ P ∀𝑦 ∈ P (𝑥<P 𝑦 → (∃𝑧 ∈ 𝐴 𝑥<P 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧<P 𝑦)))    &   𝐵 = ⟨∪ (1st “ 𝐴), {𝑢 ∈ Q ∣ ∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑢}⟩    ⇒   (𝜑 → ∀𝑦 ∈ 𝐴 ¬ 𝐵<P 𝑦)
 
10-Jan-2024cbvcsbw 3002 Version of cbvcsb 3003 with a disjoint variable condition. (Contributed by Gino Giotto, 10-Jan-2024.)
Ⅎ𝑦𝐶    &   Ⅎ𝑥𝐷    &   (𝑥 = 𝑦 → 𝐶 = 𝐷)    ⇒   ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐴 / 𝑦⦌𝐷
 
10-Jan-2024cbvsbcw 2931 Version of cbvsbc 2932 with a disjoint variable condition. (Contributed by Gino Giotto, 10-Jan-2024.)
Ⅎ𝑦𝜑    &   Ⅎ𝑥𝜓    &   (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑦]𝜓)
 
10-Jan-2024cbvabw 2260 Version of cbvab 2261 with a disjoint variable condition. (Contributed by Gino Giotto, 10-Jan-2024.)
Ⅎ𝑦𝜑    &   Ⅎ𝑥𝜓    &   (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓}
 
9-Jan-2024suplocexprlemloc 7522 Lemma for suplocexpr 7526. The putative supremum is located. (Contributed by Jim Kingdon, 9-Jan-2024.)
(𝜑 → ∃𝑥 𝑥 ∈ 𝐴)    &   (𝜑 → ∃𝑥 ∈ P ∀𝑦 ∈ 𝐴 𝑦<P 𝑥)    &   (𝜑 → ∀𝑥 ∈ P ∀𝑦 ∈ P (𝑥<P 𝑦 → (∃𝑧 ∈ 𝐴 𝑥<P 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧<P 𝑦)))    &   𝐵 = ⟨∪ (1st “ 𝐴), {𝑢 ∈ Q ∣ ∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑢}⟩    ⇒   (𝜑 → ∀𝑞 ∈ Q ∀𝑟 ∈ Q (𝑞 <Q 𝑟 → (𝑞 ∈ ∪ (1st “ 𝐴) ∨ 𝑟 ∈ (2nd ‘𝐵))))
 
9-Jan-2024suplocexprlemdisj 7521 Lemma for suplocexpr 7526. The putative supremum is disjoint. (Contributed by Jim Kingdon, 9-Jan-2024.)
(𝜑 → ∃𝑥 𝑥 ∈ 𝐴)    &   (𝜑 → ∃𝑥 ∈ P ∀𝑦 ∈ 𝐴 𝑦<P 𝑥)    &   (𝜑 → ∀𝑥 ∈ P ∀𝑦 ∈ P (𝑥<P 𝑦 → (∃𝑧 ∈ 𝐴 𝑥<P 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧<P 𝑦)))    &   𝐵 = ⟨∪ (1st “ 𝐴), {𝑢 ∈ Q ∣ ∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑢}⟩    ⇒   (𝜑 → ∀𝑞 ∈ Q ¬ (𝑞 ∈ ∪ (1st “ 𝐴) ∧ 𝑞 ∈ (2nd ‘𝐵)))
 
9-Jan-2024suplocexprlemru 7520 Lemma for suplocexpr 7526. The upper cut of the putative supremum is rounded. (Contributed by Jim Kingdon, 9-Jan-2024.)
(𝜑 → ∃𝑥 𝑥 ∈ 𝐴)    &   (𝜑 → ∃𝑥 ∈ P ∀𝑦 ∈ 𝐴 𝑦<P 𝑥)    &   (𝜑 → ∀𝑥 ∈ P ∀𝑦 ∈ P (𝑥<P 𝑦 → (∃𝑧 ∈ 𝐴 𝑥<P 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧<P 𝑦)))    &   𝐵 = ⟨∪ (1st “ 𝐴), {𝑢 ∈ Q ∣ ∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑢}⟩    ⇒   (𝜑 → ∀𝑟 ∈ Q (𝑟 ∈ (2nd ‘𝐵) ↔ ∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑞 ∈ (2nd ‘𝐵))))
 
9-Jan-2024suplocexprlemrl 7518 Lemma for suplocexpr 7526. The lower cut of the putative supremum is rounded. (Contributed by Jim Kingdon, 9-Jan-2024.)
(𝜑 → ∃𝑥 𝑥 ∈ 𝐴)    &   (𝜑 → ∃𝑥 ∈ P ∀𝑦 ∈ 𝐴 𝑦<P 𝑥)    &   (𝜑 → ∀𝑥 ∈ P ∀𝑦 ∈ P (𝑥<P 𝑦 → (∃𝑧 ∈ 𝐴 𝑥<P 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧<P 𝑦)))    ⇒   (𝜑 → ∀𝑞 ∈ Q (𝑞 ∈ ∪ (1st “ 𝐴) ↔ ∃𝑟 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑟 ∈ ∪ (1st “ 𝐴))))
 
9-Jan-2024suplocexprlem2b 7515 Lemma for suplocexpr 7526. Expression for the lower cut of the putative supremum. (Contributed by Jim Kingdon, 9-Jan-2024.)
𝐵 = ⟨∪ (1st “ 𝐴), {𝑢 ∈ Q ∣ ∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑢}⟩    ⇒   (𝐴 ⊆ P → (2nd ‘𝐵) = {𝑢 ∈ Q ∣ ∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑢})
 
9-Jan-2024suplocexprlemell 7514 Lemma for suplocexpr 7526. Membership in the lower cut of the putative supremum. (Contributed by Jim Kingdon, 9-Jan-2024.)
(𝐵 ∈ ∪ (1st “ 𝐴) ↔ ∃𝑥 ∈ 𝐴 𝐵 ∈ (1st ‘𝑥))
 
7-Jan-2024suplocexpr 7526 An inhabited, bounded-above, located set of positive reals has a supremum. (Contributed by Jim Kingdon, 7-Jan-2024.)
(𝜑 → ∃𝑥 𝑥 ∈ 𝐴)    &   (𝜑 → ∃𝑥 ∈ P ∀𝑦 ∈ 𝐴 𝑦<P 𝑥)    &   (𝜑 → ∀𝑥 ∈ P ∀𝑦 ∈ P (𝑥<P 𝑦 → (∃𝑧 ∈ 𝐴 𝑥<P 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧<P 𝑦)))    ⇒   (𝜑 → ∃𝑥 ∈ P (∀𝑦 ∈ 𝐴 ¬ 𝑥<P 𝑦 ∧ ∀𝑦 ∈ P (𝑦<P 𝑥 → ∃𝑧 ∈ 𝐴 𝑦<P 𝑧)))
 
7-Jan-2024suplocexprlemex 7523 Lemma for suplocexpr 7526. The putative supremum is a positive real. (Contributed by Jim Kingdon, 7-Jan-2024.)
(𝜑 → ∃𝑥 𝑥 ∈ 𝐴)    &   (𝜑 → ∃𝑥 ∈ P ∀𝑦 ∈ 𝐴 𝑦<P 𝑥)    &   (𝜑 → ∀𝑥 ∈ P ∀𝑦 ∈ P (𝑥<P 𝑦 → (∃𝑧 ∈ 𝐴 𝑥<P 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧<P 𝑦)))    &   𝐵 = ⟨∪ (1st “ 𝐴), {𝑢 ∈ Q ∣ ∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑢}⟩    ⇒   (𝜑 → 𝐵 ∈ P)
 
7-Jan-2024suplocexprlemmu 7519 Lemma for suplocexpr 7526. The upper cut of the putative supremum is inhabited. (Contributed by Jim Kingdon, 7-Jan-2024.)
(𝜑 → ∃𝑥 𝑥 ∈ 𝐴)    &   (𝜑 → ∃𝑥 ∈ P ∀𝑦 ∈ 𝐴 𝑦<P 𝑥)    &   (𝜑 → ∀𝑥 ∈ P ∀𝑦 ∈ P (𝑥<P 𝑦 → (∃𝑧 ∈ 𝐴 𝑥<P 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧<P 𝑦)))    &   𝐵 = ⟨∪ (1st “ 𝐴), {𝑢 ∈ Q ∣ ∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑢}⟩    ⇒   (𝜑 → ∃𝑠 ∈ Q 𝑠 ∈ (2nd ‘𝐵))
 
7-Jan-2024suplocexprlemml 7517 Lemma for suplocexpr 7526. The lower cut of the putative supremum is inhabited. (Contributed by Jim Kingdon, 7-Jan-2024.)
(𝜑 → ∃𝑥 𝑥 ∈ 𝐴)    &   (𝜑 → ∃𝑥 ∈ P ∀𝑦 ∈ 𝐴 𝑦<P 𝑥)    &   (𝜑 → ∀𝑥 ∈ P ∀𝑦 ∈ P (𝑥<P 𝑦 → (∃𝑧 ∈ 𝐴 𝑥<P 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧<P 𝑦)))    ⇒   (𝜑 → ∃𝑠 ∈ Q 𝑠 ∈ ∪ (1st “ 𝐴))
 
7-Jan-2024suplocexprlemss 7516 Lemma for suplocexpr 7526. 𝐴 is a set of positive reals. (Contributed by Jim Kingdon, 7-Jan-2024.)
(𝜑 → ∃𝑥 𝑥 ∈ 𝐴)    &   (𝜑 → ∃𝑥 ∈ P ∀𝑦 ∈ 𝐴 𝑦<P 𝑥)    &   (𝜑 → ∀𝑥 ∈ P ∀𝑦 ∈ P (𝑥<P 𝑦 → (∃𝑧 ∈ 𝐴 𝑥<P 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧<P 𝑦)))    ⇒   (𝜑 → 𝐴 ⊆ P)
 
5-Jan-2024dedekindicclemicc 12768 Lemma for dedekindicc 12769. Same as dedekindicc 12769, except that we merely show 𝑥 to be an element of (𝐴[,]𝐵). Later we will strengthen that to (𝐴(,)𝐵). (Contributed by Jim Kingdon, 5-Jan-2024.)
(𝜑 → 𝐴 ∈ ℝ)    &   (𝜑 → 𝐵 ∈ ℝ)    &   (𝜑 → 𝐿 ⊆ (𝐴[,]𝐵))    &   (𝜑 → 𝑈 ⊆ (𝐴[,]𝐵))    &   (𝜑 → ∃𝑞 ∈ (𝐴[,]𝐵)𝑞 ∈ 𝐿)    &   (𝜑 → ∃𝑟 ∈ (𝐴[,]𝐵)𝑟 ∈ 𝑈)    &   (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)(𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))    &   (𝜑 → ∀𝑟 ∈ (𝐴[,]𝐵)(𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟))    &   (𝜑 → (𝐿 ∩ 𝑈) = ∅)    &   (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)∀𝑟 ∈ (𝐴[,]𝐵)(𝑞 < 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈)))    &   (𝜑 → 𝐴 < 𝐵)    ⇒   (𝜑 → ∃!𝑥 ∈ (𝐴[,]𝐵)(∀𝑞 ∈ 𝐿 𝑞 < 𝑥 ∧ ∀𝑟 ∈ 𝑈 𝑥 < 𝑟))
 
5-Jan-2024dedekindeu 12759 A Dedekind cut identifies a unique real number. Similar to df-inp 7267 except that the the Dedekind cut is formed by sets of reals (rather than positive rationals). But in both cases the defining property of a Dedekind cut is that it is inhabited (bounded), rounded, disjoint, and located. (Contributed by Jim Kingdon, 5-Jan-2024.)
(𝜑 → 𝐿 ⊆ ℝ)    &   (𝜑 → 𝑈 ⊆ ℝ)    &   (𝜑 → ∃𝑞 ∈ ℝ 𝑞 ∈ 𝐿)    &   (𝜑 → ∃𝑟 ∈ ℝ 𝑟 ∈ 𝑈)    &   (𝜑 → ∀𝑞 ∈ ℝ (𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))    &   (𝜑 → ∀𝑟 ∈ ℝ (𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟))    &   (𝜑 → (𝐿 ∩ 𝑈) = ∅)    &   (𝜑 → ∀𝑞 ∈ ℝ ∀𝑟 ∈ ℝ (𝑞 < 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈)))    ⇒   (𝜑 → ∃!𝑥 ∈ ℝ (∀𝑞 ∈ 𝐿 𝑞 < 𝑥 ∧ ∀𝑟 ∈ 𝑈 𝑥 < 𝑟))
 
31-Dec-2023dvmptsubcn 12843 Function-builder for derivative, subtraction rule. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 31-Dec-2023.)
((𝜑 ∧ 𝑥 ∈ ℂ) → 𝐴 ∈ ℂ)    &   ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝐵 ∈ 𝑉)    &   (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ 𝐴)) = (𝑥 ∈ ℂ ↦ 𝐵))    &   ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝐶 ∈ ℂ)    &   ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝐷 ∈ 𝑊)    &   (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ 𝐶)) = (𝑥 ∈ ℂ ↦ 𝐷))    ⇒   (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ (𝐴 − 𝐶))) = (𝑥 ∈ ℂ ↦ (𝐵 − 𝐷)))
 
31-Dec-2023dvmptnegcn 12842 Function-builder for derivative, product rule for negatives. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 31-Dec-2023.)
((𝜑 ∧ 𝑥 ∈ ℂ) → 𝐴 ∈ ℂ)    &   ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝐵 ∈ 𝑉)    &   (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ 𝐴)) = (𝑥 ∈ ℂ ↦ 𝐵))    ⇒   (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ -𝐴)) = (𝑥 ∈ ℂ ↦ -𝐵))
 
31-Dec-2023dvmptcmulcn 12841 Function-builder for derivative, product rule for constant multiplier. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 31-Dec-2023.)
((𝜑 ∧ 𝑥 ∈ ℂ) → 𝐴 ∈ ℂ)    &   ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝐵 ∈ 𝑉)    &   (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ 𝐴)) = (𝑥 ∈ ℂ ↦ 𝐵))    &   (𝜑 → 𝐶 ∈ ℂ)    ⇒   (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ (𝐶 · 𝐴))) = (𝑥 ∈ ℂ ↦ (𝐶 · 𝐵)))
 
31-Dec-2023brm 3973 If two sets are in a binary relation, the relation is inhabited. (Contributed by Jim Kingdon, 31-Dec-2023.)
(𝐴𝑅𝐵 → ∃𝑥 𝑥 ∈ 𝑅)
 
30-Dec-2023dvmptccn 12837 Function-builder for derivative: derivative of a constant. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 30-Dec-2023.)
(𝜑 → 𝐴 ∈ ℂ)    ⇒   (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ 𝐴)) = (𝑥 ∈ ℂ ↦ 0))
 
30-Dec-2023dvmptidcn 12836 Function-builder for derivative: derivative of the identity. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 30-Dec-2023.)
(ℂ D (𝑥 ∈ ℂ ↦ 𝑥)) = (𝑥 ∈ ℂ ↦ 1)
 
25-Dec-2023ctfoex 6996 A countable class is a set. (Contributed by Jim Kingdon, 25-Dec-2023.)
(∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o) → 𝐴 ∈ V)
 
23-Dec-2023enct 11935 Countability is invariant relative to equinumerosity. (Contributed by Jim Kingdon, 23-Dec-2023.)
(𝐴 ≈ 𝐵 → (∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o) ↔ ∃𝑔 𝑔:ω–onto→(𝐵 ⊔ 1o)))
 
23-Dec-2023enctlem 11934 Lemma for enct 11935. One direction of the biconditional. (Contributed by Jim Kingdon, 23-Dec-2023.)
(𝐴 ≈ 𝐵 → (∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o) → ∃𝑔 𝑔:ω–onto→(𝐵 ⊔ 1o)))
 
23-Dec-2023omct 6995 ω is countable. (Contributed by Jim Kingdon, 23-Dec-2023.)
∃𝑓 𝑓:ω–onto→(ω ⊔ 1o)
 
21-Dec-2023dvcoapbr 12829 The chain rule for derivatives at a point. The 𝑢 # 𝐶 → (𝐺‘𝑢) # (𝐺‘𝐶) hypothesis constrains what functions work for 𝐺. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Jim Kingdon, 21-Dec-2023.)
(𝜑 → 𝐹:𝑋⟶ℂ)    &   (𝜑 → 𝑋 ⊆ 𝑆)    &   (𝜑 → 𝐺:𝑌⟶𝑋)    &   (𝜑 → 𝑌 ⊆ 𝑇)    &   (𝜑 → ∀𝑢 ∈ 𝑌 (𝑢 # 𝐶 → (𝐺‘𝑢) # (𝐺‘𝐶)))    &   (𝜑 → 𝑆 ⊆ ℂ)    &   (𝜑 → 𝑇 ⊆ ℂ)    &   (𝜑 → (𝐺‘𝐶)(𝑆 D 𝐹)𝐾)    &   (𝜑 → 𝐶(𝑇 D 𝐺)𝐿)    &   𝐽 = (MetOpen‘(abs ∘ − ))    ⇒   (𝜑 → 𝐶(𝑇 D (𝐹 ∘ 𝐺))(𝐾 · 𝐿))
 
19-Dec-2023apsscn 8402 The points apart from a given point are complex numbers. (Contributed by Jim Kingdon, 19-Dec-2023.)
{𝑥 ∈ 𝐴 ∣ 𝑥 # 𝐵} ⊆ ℂ
 
19-Dec-2023aprcl 8401 Reverse closure for apartness. (Contributed by Jim Kingdon, 19-Dec-2023.)
(𝐴 # 𝐵 → (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ))
 
18-Dec-2023limccoap 12805 Composition of two limits. This theorem is only usable in the case where 𝑥 # 𝑋 implies R(x) # 𝐶 so it is less general than might appear at first. (Contributed by Mario Carneiro, 29-Dec-2016.) (Revised by Jim Kingdon, 18-Dec-2023.)
((𝜑 ∧ 𝑥 ∈ {𝑤 ∈ 𝐴 ∣ 𝑤 # 𝑋}) → 𝑅 ∈ {𝑤 ∈ 𝐵 ∣ 𝑤 # 𝐶})    &   ((𝜑 ∧ 𝑦 ∈ {𝑤 ∈ 𝐵 ∣ 𝑤 # 𝐶}) → 𝑆 ∈ ℂ)    &   (𝜑 → 𝐶 ∈ ((𝑥 ∈ {𝑤 ∈ 𝐴 ∣ 𝑤 # 𝑋} ↦ 𝑅) limℂ 𝑋))    &   (𝜑 → 𝐷 ∈ ((𝑦 ∈ {𝑤 ∈ 𝐵 ∣ 𝑤 # 𝐶} ↦ 𝑆) limℂ 𝐶))    &   (𝑦 = 𝑅 → 𝑆 = 𝑇)    ⇒   (𝜑 → 𝐷 ∈ ((𝑥 ∈ {𝑤 ∈ 𝐴 ∣ 𝑤 # 𝑋} ↦ 𝑇) limℂ 𝑋))
 
16-Dec-2023cnreim 10743 Complex apartness in terms of real and imaginary parts. See also apreim 8358 which is similar but with different notation. (Contributed by Jim Kingdon, 16-Dec-2023.)
((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 # 𝐵 ↔ ((ℜ‘𝐴) # (ℜ‘𝐵) ∨ (ℑ‘𝐴) # (ℑ‘𝐵))))
 
14-Dec-2023cnopnap 12752 The complex numbers apart from a given complex number form an open set. (Contributed by Jim Kingdon, 14-Dec-2023.)
(𝐴 ∈ ℂ → {𝑤 ∈ ℂ ∣ 𝑤 # 𝐴} ∈ (MetOpen‘(abs ∘ − )))
 
14-Dec-2023cnovex 12354 The class of all continuous functions from a topology to another is a set. (Contributed by Jim Kingdon, 14-Dec-2023.)
((𝐽 ∈ Top ∧ 𝐾 ∈ Top) → (𝐽 Cn 𝐾) ∈ V)
 
13-Dec-2023reopnap 12696 The real numbers apart from a given real number form an open set. (Contributed by Jim Kingdon, 13-Dec-2023.)
(𝐴 ∈ ℝ → {𝑤 ∈ ℝ ∣ 𝑤 # 𝐴} ∈ (topGen‘ran (,)))
 
12-Dec-2023cnopncntop 12695 The set of complex numbers is open with respect to the standard topology on complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by Jim Kingdon, 12-Dec-2023.)
ℂ ∈ (MetOpen‘(abs ∘ − ))
 
12-Dec-2023unicntopcntop 12694 The underlying set of the standard topology on the complex numbers is the set of complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by Jim Kingdon, 12-Dec-2023.)
ℂ = ∪ (MetOpen‘(abs ∘ − ))
 
4-Dec-2023bj-pm2.18st 12947 Clavius law for stable formulas. See pm2.18dc 840. (Contributed by BJ, 4-Dec-2023.)
(STAB 𝜑 → ((¬ 𝜑 → 𝜑) → 𝜑))
 
4-Dec-2023bj-nnclavius 12939 Clavius law with doubly negated consequent. (Contributed by BJ, 4-Dec-2023.)
((¬ 𝜑 → 𝜑) → ¬ ¬ 𝜑)
 
2-Dec-2023dvmulxx 12826 The product rule for derivatives at a point. For the (more general) relation version, see dvmulxxbr 12824. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Jim Kingdon, 2-Dec-2023.)
(𝜑 → 𝐹:𝑋⟶ℂ)    &   (𝜑 → 𝑋 ⊆ 𝑆)    &   (𝜑 → 𝐺:𝑋⟶ℂ)    &   (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   (𝜑 → 𝐶 ∈ dom (𝑆 D 𝐹))    &   (𝜑 → 𝐶 ∈ dom (𝑆 D 𝐺))    ⇒   (𝜑 → ((𝑆 D (𝐹 ∘𝑓 · 𝐺))‘𝐶) = ((((𝑆 D 𝐹)‘𝐶) · (𝐺‘𝐶)) + (((𝑆 D 𝐺)‘𝐶) · (𝐹‘𝐶))))
 
1-Dec-2023dvmulxxbr 12824 The product rule for derivatives at a point. For the (simpler but more limited) function version, see dvmulxx 12826. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Jim Kingdon, 1-Dec-2023.)
(𝜑 → 𝐹:𝑋⟶ℂ)    &   (𝜑 → 𝑋 ⊆ 𝑆)    &   (𝜑 → 𝐺:𝑋⟶ℂ)    &   (𝜑 → 𝑆 ⊆ ℂ)    &   (𝜑 → 𝐶(𝑆 D 𝐹)𝐾)    &   (𝜑 → 𝐶(𝑆 D 𝐺)𝐿)    &   𝐽 = (MetOpen‘(abs ∘ − ))    ⇒   (𝜑 → 𝐶(𝑆 D (𝐹 ∘𝑓 · 𝐺))((𝐾 · (𝐺‘𝐶)) + (𝐿 · (𝐹‘𝐶))))
  Copyright terms: Public domain W3C HTML validation [external]