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 12-Feb-2022 at 12:00 PM ET.
Recent Additions to the Intuitionistic Logic Explorer
DateLabelDescription
Theorem
 
10-Feb-2022ltmininf 10116 Two ways of saying a number is less than the minimum of two others. (Contributed by Jim Kingdon, 10-Feb-2022.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < inf({𝐵, 𝐶}, ℝ, < ) ↔ (𝐴 < 𝐵 ∧ 𝐴 < 𝐶)))
 
10-Feb-2022maxltsup 10104 Two ways of saying the maximum of two numbers is less than a third. (Contributed by Jim Kingdon, 10-Feb-2022.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (sup({𝐴, 𝐵}, ℝ, < ) < 𝐶 ↔ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)))
 
9-Feb-2022maxleastlt 10101 The maximum as a least upper bound, in terms of less than. (Contributed by Jim Kingdon, 9-Feb-2022.)
(((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐶 < sup({𝐴, 𝐵}, ℝ, < ))) → (𝐶 < 𝐴 ∨ 𝐶 < 𝐵))
 
6-Feb-2022unsnfidcel 6386 The ¬ 𝐵 ∈ 𝐴 condition in unsnfi 6384. This is intended to show that unsnfi 6384 without that condition would not be provable but it probably would need to be strengthened (for example, to imply included middle) to fully show that. (Contributed by Jim Kingdon, 6-Feb-2022.)
((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ Fin) → DECID ¬ 𝐵 ∈ 𝐴)
 
6-Feb-2022unsnfidcex 6385 The 𝐵 ∈ 𝑉 condition in unsnfi 6384. This is intended to show that unsnfi 6384 without that condition would not be provable but it probably would need to be strengthened (for example, to imply included middle) to fully show that. (Contributed by Jim Kingdon, 6-Feb-2022.)
((𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ 𝐴 ∧ (𝐴 ∪ {𝐵}) ∈ Fin) → DECID ¬ 𝐵 ∈ V)
 
5-Feb-2022funrnfi 6392 The range of a finite relation is finite if its converse is a function. (Contributed by Jim Kingdon, 5-Feb-2022.)
((Rel 𝐴 ∧ Fun ◡𝐴 ∧ 𝐴 ∈ Fin) → ran 𝐴 ∈ Fin)
 
5-Feb-2022relcnvfi 6391 If a relation is finite, its converse is as well. (Contributed by Jim Kingdon, 5-Feb-2022.)
((Rel 𝐴 ∧ 𝐴 ∈ Fin) → ◡𝐴 ∈ Fin)
 
5-Feb-2022fundmfi 6389 The domain of a finite function is finite. (Contributed by Jim Kingdon, 5-Feb-2022.)
((𝐴 ∈ Fin ∧ Fun 𝐴) → dom 𝐴 ∈ Fin)
 
5-Feb-2022infiexmid 6362 If the intersection of any finite set and any other set is finite, excluded middle follows. (Contributed by Jim Kingdon, 5-Feb-2022.)
(𝑥 ∈ Fin → (𝑥 ∩ 𝑦) ∈ Fin)    ⇒   (𝜑 ∨ ¬ 𝜑)
 
3-Feb-2022unsnfi 6384 Adding a singleton to a finite set yields a finite set. (Contributed by Jim Kingdon, 3-Feb-2022.)
((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉 ∧ ¬ 𝐵 ∈ 𝐴) → (𝐴 ∪ {𝐵}) ∈ Fin)
 
3-Feb-2022domfiexmid 6363 If any set dominated by a finite set is finite, excluded middle follows. (Contributed by Jim Kingdon, 3-Feb-2022.)
((𝑥 ∈ Fin ∧ 𝑦 ≼ 𝑥) → 𝑦 ∈ Fin)    ⇒   (𝜑 ∨ ¬ 𝜑)
 
3-Feb-2022ssfilem 6360 Lemma for ssfiexmid 6361. (Contributed by Jim Kingdon, 3-Feb-2022.)
{𝑧 ∈ {∅} ∣ 𝜑} ∈ Fin    ⇒   (𝜑 ∨ ¬ 𝜑)
 
1-Feb-2022maxclpr 10108 The maximum of two real numbers is one of those numbers if and only if dichotomy (𝐴 ≤ 𝐵 ∨ 𝐵 ≤ 𝐴) holds. For example, this can be combined with zletric 8395 if one is dealing with integers, but real number dichotomy in general does not follow from our axioms. (Contributed by Jim Kingdon, 1-Feb-2022.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (sup({𝐴, 𝐵}, ℝ, < ) ∈ {𝐴, 𝐵} ↔ (𝐴 ≤ 𝐵 ∨ 𝐵 ≤ 𝐴)))
 
31-Jan-2022znege1 10556 The absolute value of the difference between two unequal integers is at least one. (Contributed by Jim Kingdon, 31-Jan-2022.)
((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ≠ 𝐵) → 1 ≤ (abs‘(𝐴 − 𝐵)))
 
31-Jan-2022maxleastb 10100 Two ways of saying the maximum of two numbers is less than or equal to a third. (Contributed by Jim Kingdon, 31-Jan-2022.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (sup({𝐴, 𝐵}, ℝ, < ) ≤ 𝐶 ↔ (𝐴 ≤ 𝐶 ∧ 𝐵 ≤ 𝐶)))
 
30-Jan-2022max0addsup 10105 The sum of the positive and negative part functions is the absolute value function over the reals. (Contributed by Jim Kingdon, 30-Jan-2022.)
(𝐴 ∈ ℝ → (sup({𝐴, 0}, ℝ, < ) + sup({-𝐴, 0}, ℝ, < )) = (abs‘𝐴))
 
29-Jan-2022expcanlem 9643 Lemma for expcan 9644. Proving the order in one direction. (Contributed by Jim Kingdon, 29-Jan-2022.)
(𝜑 → 𝐴 ∈ ℝ)    &   (𝜑 → 𝑀 ∈ ℤ)    &   (𝜑 → 𝑁 ∈ ℤ)    &   (𝜑 → 1 < 𝐴)    ⇒   (𝜑 → ((𝐴↑𝑀) ≤ (𝐴↑𝑁) → 𝑀 ≤ 𝑁))
 
28-Jan-2022exfzdc 9249 Decidability of the existence of an integer defined by a decidable proposition. (Contributed by Jim Kingdon, 28-Jan-2022.)
(𝜑 → 𝑀 ∈ ℤ)    &   (𝜑 → 𝑁 ∈ ℤ)    &   ((𝜑 ∧ 𝑛 ∈ (𝑀...𝑁)) → DECID 𝜓)    ⇒   (𝜑 → DECID ∃𝑛 ∈ (𝑀...𝑁)𝜓)
 
25-Jan-20221nen2 6347 One and two are not equinumerous. (Contributed by Jim Kingdon, 25-Jan-2022.)
¬ 1𝑜 ≈ 2𝑜
 
24-Jan-2022divmulasscomap 7784 An associative/commutative law for division and multiplication. (Contributed by Jim Kingdon, 24-Jan-2022.)
(((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐷 # 0)) → ((𝐴 · (𝐵 / 𝐷)) · 𝐶) = (𝐵 · ((𝐴 · 𝐶) / 𝐷)))
 
24-Jan-2022divmulassap 7783 An associative law for division and multiplication. (Contributed by Jim Kingdon, 24-Jan-2022.)
(((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐷 # 0)) → ((𝐴 · (𝐵 / 𝐷)) · 𝐶) = ((𝐴 · 𝐵) · (𝐶 / 𝐷)))
 
21-Jan-2022lcmmndc 10444 Decidablity lemma used in various proofs related to lcm. (Contributed by Jim Kingdon, 21-Jan-2022.)
((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → DECID (𝑀 = 0 ∨ 𝑁 = 0))
 
20-Jan-2022infssuzcldc 10347 The infimum of a subset of an upper set of integers belongs to the subset. (Contributed by Jim Kingdon, 20-Jan-2022.)
(𝜑 → 𝑀 ∈ ℤ)    &   𝑆 = {𝑛 ∈ (ℤ≥‘𝑀) ∣ 𝜓}    &   (𝜑 → 𝐴 ∈ 𝑆)    &   ((𝜑 ∧ 𝑛 ∈ (𝑀...𝐴)) → DECID 𝜓)    ⇒   (𝜑 → inf(𝑆, ℝ, < ) ∈ 𝑆)
 
19-Jan-2022suprnubex 8031 An upper bound is not less than the supremum of a nonempty bounded set of reals. (Contributed by Jim Kingdon, 19-Jan-2022.)
(𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)))    &   (𝜑 → 𝐴 ⊆ ℝ)    &   (𝜑 → 𝐵 ∈ ℝ)    ⇒   (𝜑 → (¬ 𝐵 < sup(𝐴, ℝ, < ) ↔ ∀𝑧 ∈ 𝐴 ¬ 𝐵 < 𝑧))
 
19-Jan-2022suprlubex 8030 The supremum of a nonempty bounded set of reals is the least upper bound. (Contributed by Jim Kingdon, 19-Jan-2022.)
(𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)))    &   (𝜑 → 𝐴 ⊆ ℝ)    &   (𝜑 → 𝐵 ∈ ℝ)    ⇒   (𝜑 → (𝐵 < sup(𝐴, ℝ, < ) ↔ ∃𝑧 ∈ 𝐴 𝐵 < 𝑧))
 
18-Jan-2022suprubex 8029 A member of a nonempty bounded set of reals is less than or equal to the set's upper bound. (Contributed by Jim Kingdon, 18-Jan-2022.)
(𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)))    &   (𝜑 → 𝐴 ⊆ ℝ)    &   (𝜑 → 𝐵 ∈ 𝐴)    ⇒   (𝜑 → 𝐵 ≤ sup(𝐴, ℝ, < ))
 
17-Jan-2022zdvdsdc 10216 Divisibility of integers is decidable. (Contributed by Jim Kingdon, 17-Jan-2022.)
((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → DECID 𝑀 ∥ 𝑁)
 
17-Jan-2022suplub2ti 6414 Bidirectional form of suplubti 6413. (Contributed by Jim Kingdon, 17-Jan-2022.)
((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢)))    &   (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧)))    &   (𝜑 → 𝑅 Or 𝐴)    &   (𝜑 → 𝐵 ⊆ 𝐴)    ⇒   ((𝜑 ∧ 𝐶 ∈ 𝐴) → (𝐶𝑅sup(𝐵, 𝐴, 𝑅) ↔ ∃𝑧 ∈ 𝐵 𝐶𝑅𝑧))
 
16-Jan-2022zssinfcl 10344 The infimum of a set of integers is an element of the set. (Contributed by Jim Kingdon, 16-Jan-2022.)
(𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐵 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐵 𝑧 < 𝑦)))    &   (𝜑 → 𝐵 ⊆ ℤ)    &   (𝜑 → inf(𝐵, ℝ, < ) ∈ ℤ)    ⇒   (𝜑 → inf(𝐵, ℝ, < ) ∈ 𝐵)
 
16-Jan-2022supelti 6415 Supremum membership in a set. (Contributed by Jim Kingdon, 16-Jan-2022.)
((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢)))    &   (𝜑 → ∃𝑥 ∈ 𝐶 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧)))    &   (𝜑 → 𝐶 ⊆ 𝐴)    ⇒   (𝜑 → sup(𝐵, 𝐴, 𝑅) ∈ 𝐶)
 
15-Jan-2022infsupneg 8684 If a set of real numbers has a greatest lower bound, the set of the negation of those numbers has a least upper bound. To go in the other direction see supinfneg 8683. (Contributed by Jim Kingdon, 15-Jan-2022.)
(𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))    &   (𝜑 → 𝐴 ⊆ ℝ)    ⇒   (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧)))
 
15-Jan-2022supinfneg 8683 If a set of real numbers has a least upper bound, the set of the negation of those numbers has a greatest lower bound. For a theorem which is similar but only for the boundedness part, see ublbneg 8698. (Contributed by Jim Kingdon, 15-Jan-2022.)
(𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)))    &   (𝜑 → 𝐴 ⊆ ℝ)    ⇒   (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑧 < 𝑦)))
 
14-Jan-2022supminfex 8685 A supremum is the negation of the infimum of that set's image under negation. (Contributed by Jim Kingdon, 14-Jan-2022.)
(𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)))    &   (𝜑 → 𝐴 ⊆ ℝ)    ⇒   (𝜑 → sup(𝐴, ℝ, < ) = -inf({𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}, ℝ, < ))
 
14-Jan-2022infrenegsupex 8682 The infimum of a set of reals 𝐴 is the negative of the supremum of the negatives of its elements. (Contributed by Jim Kingdon, 14-Jan-2022.)
(𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))    &   (𝜑 → 𝐴 ⊆ ℝ)    ⇒   (𝜑 → inf(𝐴, ℝ, < ) = -sup({𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴}, ℝ, < ))
 
13-Jan-2022infssuzledc 10346 The infimum of a subset of an upper set of integers is less than or equal to all members of the subset. (Contributed by Jim Kingdon, 13-Jan-2022.)
(𝜑 → 𝑀 ∈ ℤ)    &   𝑆 = {𝑛 ∈ (ℤ≥‘𝑀) ∣ 𝜓}    &   (𝜑 → 𝐴 ∈ 𝑆)    &   ((𝜑 ∧ 𝑛 ∈ (𝑀...𝐴)) → DECID 𝜓)    ⇒   (𝜑 → inf(𝑆, ℝ, < ) ≤ 𝐴)
 
13-Jan-2022infssuzex 10345 Existence of the infimum of a subset of an upper set of integers. (Contributed by Jim Kingdon, 13-Jan-2022.)
(𝜑 → 𝑀 ∈ ℤ)    &   𝑆 = {𝑛 ∈ (ℤ≥‘𝑀) ∣ 𝜓}    &   (𝜑 → 𝐴 ∈ 𝑆)    &   ((𝜑 ∧ 𝑛 ∈ (𝑀...𝐴)) → DECID 𝜓)    ⇒   (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝑆 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝑆 𝑧 < 𝑦)))
 
11-Jan-2022eucialg 10441 Euclid's Algorithm computes the greatest common divisor of two nonnegative integers by repeatedly replacing the larger of them with its remainder modulo the smaller until the remainder is 0. Theorem 1.15 in [ApostolNT] p. 20.

Upon halting, the 1st member of the final state (𝑅‘𝑁) is equal to the gcd of the values comprising the input state ⟨𝑀, 𝑁⟩. This is Metamath 100 proof #69 (greatest common divisor algorithm). (Contributed by Jim Kingdon, 11-Jan-2022.)

𝐸 = (𝑥 ∈ ℕ0, 𝑦 ∈ ℕ0 ↦ if(𝑦 = 0, ⟨𝑥, 𝑦⟩, ⟨𝑦, (𝑥 mod 𝑦)⟩))    &   𝑅 = seq0((𝐸 ∘ 1st ), (ℕ0 × {𝐴}), (ℕ0 × ℕ0))    &   𝑁 = (2nd ‘𝐴)    &   𝐴 = ⟨𝑀, 𝑁⟩    ⇒   ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (1st ‘(𝑅‘𝑁)) = (𝑀 gcd 𝑁))
 
11-Jan-2022eucialgcvga 10440 Once Euclid's Algorithm halts after 𝑁 steps, the second element of the state remains 0 . (Contributed by Jim Kingdon, 11-Jan-2022.)
𝐸 = (𝑥 ∈ ℕ0, 𝑦 ∈ ℕ0 ↦ if(𝑦 = 0, ⟨𝑥, 𝑦⟩, ⟨𝑦, (𝑥 mod 𝑦)⟩))    &   𝑅 = seq0((𝐸 ∘ 1st ), (ℕ0 × {𝐴}), (ℕ0 × ℕ0))    &   𝑁 = (2nd ‘𝐴)    ⇒   (𝐴 ∈ (ℕ0 × ℕ0) → (𝐾 ∈ (ℤ≥‘𝑁) → (2nd ‘(𝑅‘𝐾)) = 0))
 
11-Jan-2022ifcldadc 3378 Conditional closure. (Contributed by Jim Kingdon, 11-Jan-2022.)
((𝜑 ∧ 𝜓) → 𝐴 ∈ 𝐶)    &   ((𝜑 ∧ ¬ 𝜓) → 𝐵 ∈ 𝐶)    &   (𝜑 → DECID 𝜓)    ⇒   (𝜑 → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
 
9-Jan-2022bezoutlemsup 10398 Lemma for Bézout's identity. The number satisfying the greatest common divisor condition is the supremum of divisors of both 𝐴 and 𝐵. (Contributed by Mario Carneiro and Jim Kingdon, 9-Jan-2022.)
(𝜑 → 𝐴 ∈ ℤ)    &   (𝜑 → 𝐵 ∈ ℤ)    &   (𝜑 → 𝐷 ∈ ℕ0)    &   (𝜑 → ∀𝑧 ∈ ℤ (𝑧 ∥ 𝐷 ↔ (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)))    &   (𝜑 → ¬ (𝐴 = 0 ∧ 𝐵 = 0))    ⇒   (𝜑 → 𝐷 = sup({𝑧 ∈ ℤ ∣ (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)}, ℝ, < ))
 
9-Jan-2022bezoutlemle 10397 Lemma for Bézout's identity. The number satisfying the greatest common divisor condition is the largest number which divides both 𝐴 and 𝐵. (Contributed by Mario Carneiro and Jim Kingdon, 9-Jan-2022.)
(𝜑 → 𝐴 ∈ ℤ)    &   (𝜑 → 𝐵 ∈ ℤ)    &   (𝜑 → 𝐷 ∈ ℕ0)    &   (𝜑 → ∀𝑧 ∈ ℤ (𝑧 ∥ 𝐷 ↔ (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)))    &   (𝜑 → ¬ (𝐴 = 0 ∧ 𝐵 = 0))    ⇒   (𝜑 → ∀𝑧 ∈ ℤ ((𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵) → 𝑧 ≤ 𝐷))
 
9-Jan-2022bezoutlemeu 10396 Lemma for Bézout's identity. There is exactly one nonnegative integer meeting the greatest common divisor condition. (Contributed by Mario Carneiro and Jim Kingdon, 9-Jan-2022.)
(𝜑 → 𝐴 ∈ ℤ)    &   (𝜑 → 𝐵 ∈ ℤ)    &   (𝜑 → 𝐷 ∈ ℕ0)    &   (𝜑 → ∀𝑧 ∈ ℤ (𝑧 ∥ 𝐷 ↔ (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)))    ⇒   (𝜑 → ∃!𝑑 ∈ ℕ0 ∀𝑧 ∈ ℤ (𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)))
 
9-Jan-2022bezoutlemmo 10395 Lemma for Bézout's identity. There is at most one nonnegative integer meeting the greatest common divisor condition. (Contributed by Mario Carneiro and Jim Kingdon, 9-Jan-2022.)
(𝜑 → 𝐴 ∈ ℤ)    &   (𝜑 → 𝐵 ∈ ℤ)    &   (𝜑 → 𝐷 ∈ ℕ0)    &   (𝜑 → ∀𝑧 ∈ ℤ (𝑧 ∥ 𝐷 ↔ (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)))    &   (𝜑 → 𝐸 ∈ ℕ0)    &   (𝜑 → ∀𝑧 ∈ ℤ (𝑧 ∥ 𝐸 ↔ (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)))    ⇒   (𝜑 → 𝐷 = 𝐸)
 
8-Jan-2022bezoutlembi 10394 Lemma for Bézout's identity. Like bezoutlembz 10393 but the greatest common divisor condition is a biconditional, not just an implication. (Contributed by Mario Carneiro and Jim Kingdon, 8-Jan-2022.)
((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ∃𝑑 ∈ ℕ0 (∀𝑧 ∈ ℤ (𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)) ∧ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑑 = ((𝐴 · 𝑥) + (𝐵 · 𝑦))))
 
8-Jan-2022bezoutlembz 10393 Lemma for Bézout's identity. Like bezoutlemaz 10392 but where ' B ' can be any integer, not just a nonnegative one. (Contributed by Mario Carneiro and Jim Kingdon, 8-Jan-2022.)
((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ∃𝑑 ∈ ℕ0 (∀𝑧 ∈ ℤ (𝑧 ∥ 𝑑 → (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)) ∧ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑑 = ((𝐴 · 𝑥) + (𝐵 · 𝑦))))
 
8-Jan-2022bezoutlemaz 10392 Lemma for Bézout's identity. Like bezoutlemzz 10391 but where ' A ' can be any integer, not just a nonnegative one. (Contributed by Mario Carneiro and Jim Kingdon, 8-Jan-2022.)
((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ0) → ∃𝑑 ∈ ℕ0 (∀𝑧 ∈ ℤ (𝑧 ∥ 𝑑 → (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)) ∧ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑑 = ((𝐴 · 𝑥) + (𝐵 · 𝑦))))
 
8-Jan-2022bezoutlemzz 10391 Lemma for Bézout's identity. Like bezoutlemex 10390 but where ' z ' is any integer, not just a nonnegative one. (Contributed by Mario Carneiro and Jim Kingdon, 8-Jan-2022.)
((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → ∃𝑑 ∈ ℕ0 (∀𝑧 ∈ ℤ (𝑧 ∥ 𝑑 → (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)) ∧ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑑 = ((𝐴 · 𝑥) + (𝐵 · 𝑦))))
 
6-Jan-2022bezoutlemnewy 10385 Lemma for Bézout's identity. The is-bezout predicate holds for (𝑦 mod 𝑊). (Contributed by Jim Kingdon, 6-Jan-2022.)
(𝜑 ↔ ∃𝑠 ∈ ℤ ∃𝑡 ∈ ℤ 𝑟 = ((𝐴 · 𝑠) + (𝐵 · 𝑡)))    &   (𝜃 → 𝐴 ∈ ℕ0)    &   (𝜃 → 𝐵 ∈ ℕ0)    &   (𝜃 → 𝑊 ∈ ℕ)    &   (𝜃 → [𝑦 / 𝑟]𝜑)    &   (𝜃 → 𝑦 ∈ ℕ0)    &   (𝜃 → [𝑊 / 𝑟]𝜑)    ⇒   (𝜃 → [(𝑦 mod 𝑊) / 𝑟]𝜑)
 
3-Jan-2022bezoutlemex 10390 Lemma for Bézout's identity. Existence of a number which we will later show to be the greater common divisor and its decomposition into cofactors. (Contributed by Mario Carneiro and Jim Kingdon, 3-Jan-2022.)
((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → ∃𝑑 ∈ ℕ0 (∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑑 → (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)) ∧ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑑 = ((𝐴 · 𝑥) + (𝐵 · 𝑦))))
 
3-Jan-2022bezoutlemstep 10386 Lemma for Bézout's identity. This is the induction step for the proof by induction. (Contributed by Jim Kingdon, 3-Jan-2022.)
(𝜑 ↔ ∃𝑠 ∈ ℤ ∃𝑡 ∈ ℤ 𝑟 = ((𝐴 · 𝑠) + (𝐵 · 𝑡)))    &   (𝜃 → 𝐴 ∈ ℕ0)    &   (𝜃 → 𝐵 ∈ ℕ0)    &   (𝜃 → 𝑊 ∈ ℕ)    &   (𝜃 → [𝑦 / 𝑟]𝜑)    &   (𝜃 → 𝑦 ∈ ℕ0)    &   (𝜃 → [𝑊 / 𝑟]𝜑)    &   (𝜓 ↔ ∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 𝑥 ∧ 𝑧 ∥ 𝑦)))    &   ((𝜃 ∧ [(𝑦 mod 𝑊) / 𝑟]𝜑) → ∃𝑟 ∈ ℕ0 ([(𝑦 mod 𝑊) / 𝑥][𝑊 / 𝑦]𝜓 ∧ 𝜑))    &   Ⅎ𝑥𝜃    &   Ⅎ𝑟𝜃    ⇒   (𝜃 → ∃𝑟 ∈ ℕ0 ([𝑊 / 𝑥]𝜓 ∧ 𝜑))
 
1-Jan-2022fvifdc 5217 Move a conditional outside of a function. (Contributed by Jim Kingdon, 1-Jan-2022.)
(DECID 𝜑 → (𝐹‘if(𝜑, 𝐴, 𝐵)) = if(𝜑, (𝐹‘𝐴), (𝐹‘𝐵)))
 
1-Jan-2022ifeq1dadc 3379 Conditional equality. (Contributed by Jim Kingdon, 1-Jan-2022.)
((𝜑 ∧ 𝜓) → 𝐴 = 𝐵)    &   (𝜑 → DECID 𝜓)    ⇒   (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
 
1-Jan-2022ifsbdc 3363 Distribute a function over an if-clause. (Contributed by Jim Kingdon, 1-Jan-2022.)
(if(𝜑, 𝐴, 𝐵) = 𝐴 → 𝐶 = 𝐷)    &   (if(𝜑, 𝐴, 𝐵) = 𝐵 → 𝐶 = 𝐸)    ⇒   (DECID 𝜑 → 𝐶 = if(𝜑, 𝐷, 𝐸))
 
31-Dec-2021dfgcd3 10399 Alternate definition of the gcd operator. (Contributed by Jim Kingdon, 31-Dec-2021.)
((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) = (℩𝑑 ∈ ℕ0 ∀𝑧 ∈ ℤ (𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁))))
 
30-Dec-2021bezoutlemb 10389 Lemma for Bézout's identity. The is-bezout condition is satisfied by 𝐵. (Contributed by Jim Kingdon, 30-Dec-2021.)
(𝜑 ↔ ∃𝑠 ∈ ℤ ∃𝑡 ∈ ℤ 𝑟 = ((𝐴 · 𝑠) + (𝐵 · 𝑡)))    &   (𝜃 → 𝐴 ∈ ℕ0)    &   (𝜃 → 𝐵 ∈ ℕ0)    ⇒   (𝜃 → [𝐵 / 𝑟]𝜑)
 
30-Dec-2021bezoutlema 10388 Lemma for Bézout's identity. The is-bezout condition is satisfied by 𝐴. (Contributed by Jim Kingdon, 30-Dec-2021.)
(𝜑 ↔ ∃𝑠 ∈ ℤ ∃𝑡 ∈ ℤ 𝑟 = ((𝐴 · 𝑠) + (𝐵 · 𝑡)))    &   (𝜃 → 𝐴 ∈ ℕ0)    &   (𝜃 → 𝐵 ∈ ℕ0)    ⇒   (𝜃 → [𝐴 / 𝑟]𝜑)
 
30-Dec-2021bezoutlemmain 10387 Lemma for Bézout's identity. This is the main result which we prove by induction and which represents the application of the Extended Euclidean algorithm. (Contributed by Jim Kingdon, 30-Dec-2021.)
(𝜑 ↔ ∃𝑠 ∈ ℤ ∃𝑡 ∈ ℤ 𝑟 = ((𝐴 · 𝑠) + (𝐵 · 𝑡)))    &   (𝜓 ↔ ∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 𝑥 ∧ 𝑧 ∥ 𝑦)))    &   (𝜃 → 𝐴 ∈ ℕ0)    &   (𝜃 → 𝐵 ∈ ℕ0)    ⇒   (𝜃 → ∀𝑥 ∈ ℕ0 ([𝑥 / 𝑟]𝜑 → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 (𝜓 ∧ 𝜑))))
 
22-Dec-2021maxleast 10099 The maximum of two reals is a least upper bound. Lemma 3.11 of [Geuvers], p. 10. (Contributed by Jim Kingdon, 22-Dec-2021.)
(((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≤ 𝐶 ∧ 𝐵 ≤ 𝐶)) → sup({𝐴, 𝐵}, ℝ, < ) ≤ 𝐶)
 
22-Dec-2021maxcl 10096 The maximum of two real numbers is a real number. (Contributed by Jim Kingdon, 22-Dec-2021.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → sup({𝐴, 𝐵}, ℝ, < ) ∈ ℝ)
 
22-Dec-2021maxabslemval 10094 Lemma for maxabs 10095. Value of the supremum. (Contributed by Jim Kingdon, 22-Dec-2021.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((((𝐴 + 𝐵) + (abs‘(𝐴 − 𝐵))) / 2) ∈ ℝ ∧ ∀𝑥 ∈ {𝐴, 𝐵} ¬ (((𝐴 + 𝐵) + (abs‘(𝐴 − 𝐵))) / 2) < 𝑥 ∧ ∀𝑥 ∈ ℝ (𝑥 < (((𝐴 + 𝐵) + (abs‘(𝐴 − 𝐵))) / 2) → ∃𝑧 ∈ {𝐴, 𝐵}𝑥 < 𝑧)))
 
21-Dec-2021dfabsmax 10103 Absolute value of a real number in terms of maximum. Definition 3.13 of [Geuvers], p. 11. (Contributed by BJ and Jim Kingdon, 21-Dec-2021.)
(𝐴 ∈ ℝ → (abs‘𝐴) = sup({𝐴, -𝐴}, ℝ, < ))
 
21-Dec-2021maxleb 10102 Equivalence of ≤ and being equal to the maximum of two reals. Lemma 3.12 of [Geuvers], p. 10. (Contributed by Jim Kingdon, 21-Dec-2021.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ sup({𝐴, 𝐵}, ℝ, < ) = 𝐵))
 
21-Dec-2021maxle2 10098 The maximum of two reals is no smaller than the second real. Lemma 3.10 of [Geuvers], p. 10. (Contributed by Jim Kingdon, 21-Dec-2021.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐵 ≤ sup({𝐴, 𝐵}, ℝ, < ))
 
21-Dec-2021maxle1 10097 The maximum of two reals is no smaller than the first real. Lemma 3.10 of [Geuvers], p. 10. (Contributed by Jim Kingdon, 21-Dec-2021.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐴 ≤ sup({𝐴, 𝐵}, ℝ, < ))
 
21-Dec-2021maxabslemab 10092 Lemma for maxabs 10095. A variation of maxleim 10091- that is, if we know which of two real numbers is larger, we know the maximum of the two. (Contributed by Jim Kingdon, 21-Dec-2021.)
(𝜑 → 𝐴 ∈ ℝ)    &   (𝜑 → 𝐵 ∈ ℝ)    &   (𝜑 → 𝐴 < 𝐵)    ⇒   (𝜑 → (((𝐴 + 𝐵) + (abs‘(𝐴 − 𝐵))) / 2) = 𝐵)
 
21-Dec-2021maxleim 10091 Value of maximum when we know which number is larger. (Contributed by Jim Kingdon, 21-Dec-2021.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 → sup({𝐴, 𝐵}, ℝ, < ) = 𝐵))
 
21-Dec-2021maxcom 10089 The maximum of two reals is commutative. Lemma 3.9 of [Geuvers], p. 10. (Contributed by Jim Kingdon, 21-Dec-2021.)
sup({𝐴, 𝐵}, ℝ, < ) = sup({𝐵, 𝐴}, ℝ, < )
 
20-Dec-2021maxabs 10095 Maximum of two real numbers in terms of absolute value. (Contributed by Jim Kingdon, 20-Dec-2021.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → sup({𝐴, 𝐵}, ℝ, < ) = (((𝐴 + 𝐵) + (abs‘(𝐴 − 𝐵))) / 2))
 
20-Dec-2021maxabslemlub 10093 Lemma for maxabs 10095. A least upper bound for {𝐴, 𝐵}. (Contributed by Jim Kingdon, 20-Dec-2021.)
(𝜑 → 𝐴 ∈ ℝ)    &   (𝜑 → 𝐵 ∈ ℝ)    &   (𝜑 → 𝐶 ∈ ℝ)    &   (𝜑 → 𝐶 < (((𝐴 + 𝐵) + (abs‘(𝐴 − 𝐵))) / 2))    ⇒   (𝜑 → (𝐶 < 𝐴 ∨ 𝐶 < 𝐵))
 
20-Dec-2021maxabsle 10090 An upper bound for {𝐴, 𝐵}. (Contributed by Jim Kingdon, 20-Dec-2021.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐴 ≤ (((𝐴 + 𝐵) + (abs‘(𝐴 − 𝐵))) / 2))
 
20-Dec-2021suprzclex 8445 The supremum of a set of integers is an element of the set. (Contributed by Jim Kingdon, 20-Dec-2021.)
(𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)))    &   (𝜑 → 𝐴 ⊆ ℤ)    ⇒   (𝜑 → sup(𝐴, ℝ, < ) ∈ 𝐴)
 
20-Dec-2021r19.12sn 3458 Special case of r19.12 2466 where its converse holds. (Contributed by NM, 19-May-2008.) (Revised by Mario Carneiro, 23-Apr-2015.) (Revised by BJ, 20-Dec-2021.)
(𝐴 ∈ 𝑉 → (∃𝑥 ∈ {𝐴}∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ {𝐴}𝜑))
 
19-Dec-2021infisoti 6445 Image of an infimum under an isomorphism. (Contributed by Jim Kingdon, 19-Dec-2021.)
(𝜑 → 𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵))    &   (𝜑 → 𝐶 ⊆ 𝐴)    &   (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐶 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐶 𝑧𝑅𝑦)))    &   ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢)))    ⇒   (𝜑 → inf((𝐹 “ 𝐶), 𝐵, 𝑆) = (𝐹‘inf(𝐶, 𝐴, 𝑅)))
 
19-Dec-2021infsnti 6443 The infimum of a singleton. (Contributed by Jim Kingdon, 19-Dec-2021.)
((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢)))    &   (𝜑 → 𝐵 ∈ 𝐴)    ⇒   (𝜑 → inf({𝐵}, 𝐴, 𝑅) = 𝐵)
 
19-Dec-2021infeuti 6442 An infimum is unique. (Contributed by Jim Kingdon, 19-Dec-2021.)
((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢)))    &   (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦)))    ⇒   (𝜑 → ∃!𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦)))
 
18-Dec-2021infmoti 6441 Any class 𝐵 has at most one infimum in 𝐴 (where 𝑅 is interpreted as 'less than'). (Contributed by Jim Kingdon, 18-Dec-2021.)
((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢)))    ⇒   (𝜑 → ∃*𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦)))
 
18-Dec-2021infminti 6440 The smallest element of a set is its infimum. Note that the converse is not true; the infimum might not be an element of the set considered. (Contributed by Jim Kingdon, 18-Dec-2021.)
((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢)))    &   (𝜑 → 𝐶 ∈ 𝐴)    &   (𝜑 → 𝐶 ∈ 𝐵)    &   ((𝜑 ∧ 𝑦 ∈ 𝐵) → ¬ 𝑦𝑅𝐶)    ⇒   (𝜑 → inf(𝐵, 𝐴, 𝑅) = 𝐶)
 
18-Dec-2021infnlbti 6439 A lower bound is not greater than the infimum. (Contributed by Jim Kingdon, 18-Dec-2021.)
((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢)))    &   (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦)))    ⇒   (𝜑 → ((𝐶 ∈ 𝐴 ∧ ∀𝑧 ∈ 𝐵 ¬ 𝑧𝑅𝐶) → ¬ inf(𝐵, 𝐴, 𝑅)𝑅𝐶))
 
18-Dec-2021infglbti 6438 An infimum is the greatest lower bound. See also infclti 6436 and inflbti 6437. (Contributed by Jim Kingdon, 18-Dec-2021.)
((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢)))    &   (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦)))    ⇒   (𝜑 → ((𝐶 ∈ 𝐴 ∧ inf(𝐵, 𝐴, 𝑅)𝑅𝐶) → ∃𝑧 ∈ 𝐵 𝑧𝑅𝐶))
 
18-Dec-2021inflbti 6437 An infimum is a lower bound. See also infclti 6436 and infglbti 6438. (Contributed by Jim Kingdon, 18-Dec-2021.)
((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢)))    &   (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦)))    ⇒   (𝜑 → (𝐶 ∈ 𝐵 → ¬ 𝐶𝑅inf(𝐵, 𝐴, 𝑅)))
 
17-Dec-2021infclti 6436 An infimum belongs to its base class (closure law). See also inflbti 6437 and infglbti 6438. (Contributed by Jim Kingdon, 17-Dec-2021.)
((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢)))    &   (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦)))    ⇒   (𝜑 → inf(𝐵, 𝐴, 𝑅) ∈ 𝐴)
 
17-Dec-2021infvalti 6435 Alternate expression for the infimum. (Contributed by Jim Kingdon, 17-Dec-2021.)
((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢)))    &   (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦)))    ⇒   (𝜑 → inf(𝐵, 𝐴, 𝑅) = (℩𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))))
 
17-Dec-2021cnvti 6432 If a relation satisfies a condition corresponding to tightness of an apartness generated by an order, so does its converse. (Contributed by Jim Kingdon, 17-Dec-2021.)
((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢)))    ⇒   ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢◡𝑅𝑣 ∧ ¬ 𝑣◡𝑅𝑢)))
 
17-Dec-2021cnvinfex 6431 Two ways of expressing existence of an infimum (one in terms of converse). (Contributed by Jim Kingdon, 17-Dec-2021.)
(𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦)))    ⇒   (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥◡𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦◡𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦◡𝑅𝑧)))
 
16-Dec-2021eqinftid 6434 Sufficient condition for an element to be equal to the infimum. (Contributed by Jim Kingdon, 16-Dec-2021.)
((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢)))    &   (𝜑 → 𝐶 ∈ 𝐴)    &   ((𝜑 ∧ 𝑦 ∈ 𝐵) → ¬ 𝑦𝑅𝐶)    &   ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝐶𝑅𝑦)) → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦)    ⇒   (𝜑 → inf(𝐵, 𝐴, 𝑅) = 𝐶)
 
16-Dec-2021eqinfti 6433 Sufficient condition for an element to be equal to the infimum. (Contributed by Jim Kingdon, 16-Dec-2021.)
((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢)))    ⇒   (𝜑 → ((𝐶 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝐶 ∧ ∀𝑦 ∈ 𝐴 (𝐶𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦)) → inf(𝐵, 𝐴, 𝑅) = 𝐶))
 
13-Dec-2021orandc 880 Disjunction in terms of conjunction (De Morgan's law), for decidable propositions. Compare Theorem *4.57 of [WhiteheadRussell] p. 120. (Contributed by Jim Kingdon, 13-Dec-2021.)
((DECID 𝜑 ∧ DECID 𝜓) → ((𝜑 ∨ 𝜓) ↔ ¬ (¬ 𝜑 ∧ ¬ 𝜓)))
 
12-Dec-2021gcdsupex 10349 Existence of the supremum used in defining gcd. (Contributed by Jim Kingdon, 12-Dec-2021.)
(((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ ¬ (𝑋 = 0 ∧ 𝑌 = 0)) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑋 ∧ 𝑛 ∥ 𝑌)} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑋 ∧ 𝑛 ∥ 𝑌)}𝑦 < 𝑧)))
 
12-Dec-2021gcdmndc 10340 Decidablity lemma used in various proofs related to gcd. (Contributed by Jim Kingdon, 12-Dec-2021.)
((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → DECID (𝑀 = 0 ∧ 𝑁 = 0))
 
12-Dec-2021ddifstab 3104 A class is equal to its double complement if and only if it is stable (that is, membership in it is a stable property). (Contributed by BJ, 12-Dec-2021.)
((V ∖ (V ∖ 𝐴)) = 𝐴 ↔ ∀𝑥STAB 𝑥 ∈ 𝐴)
 
11-Dec-2021gcdsupcl 10350 Closure of the supremum used in defining gcd. A lemma for gcdval 10351 and gcdn0cl 10354. (Contributed by Jim Kingdon, 11-Dec-2021.)
(((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ ¬ (𝑋 = 0 ∧ 𝑌 = 0)) → sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑋 ∧ 𝑛 ∥ 𝑌)}, ℝ, < ) ∈ ℕ)
 
11-Dec-2021dvdsbnd 10348 There is an upper bound to the divisors of a nonzero integer. (Contributed by Jim Kingdon, 11-Dec-2021.)
((𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) → ∃𝑛 ∈ ℕ ∀𝑚 ∈ (ℤ≥‘𝑛) ¬ 𝑚 ∥ 𝐴)
 
7-Dec-2021zsupcl 10343 Closure of supremum for decidable integer properties. The property which defines the set we are taking the supremum of must (a) be true at 𝑀 (which corresponds to the non-empty condition of classical supremum theorems), (b) decidable at each value after 𝑀, and (c) be false after 𝑗 (which corresponds to the upper bound condition found in classical supremum theorems). (Contributed by Jim Kingdon, 7-Dec-2021.)
(𝜑 → 𝑀 ∈ ℤ)    &   (𝑛 = 𝑀 → (𝜓 ↔ 𝜒))    &   (𝜑 → 𝜒)    &   ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → DECID 𝜓)    &   (𝜑 → ∃𝑗 ∈ (ℤ≥‘𝑀)∀𝑛 ∈ (ℤ≥‘𝑗) ¬ 𝜓)    ⇒   (𝜑 → sup({𝑛 ∈ ℤ ∣ 𝜓}, ℝ, < ) ∈ (ℤ≥‘𝑀))
 
7-Dec-2021zsupcllemex 10342 Lemma for zsupcl 10343. Existence of the supremum. (Contributed by Jim Kingdon, 7-Dec-2021.)
(𝜑 → 𝑀 ∈ ℤ)    &   (𝑛 = 𝑀 → (𝜓 ↔ 𝜒))    &   (𝜑 → 𝜒)    &   ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → DECID 𝜓)    &   (𝜑 → ∃𝑗 ∈ (ℤ≥‘𝑀)∀𝑛 ∈ (ℤ≥‘𝑗) ¬ 𝜓)    ⇒   (𝜑 → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧)))
 
7-Dec-2021zsupcllemstep 10341 Lemma for zsupcl 10343. Induction step. (Contributed by Jim Kingdon, 7-Dec-2021.)
((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → DECID 𝜓)    ⇒   (𝐾 ∈ (ℤ≥‘𝑀) → (((𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘𝐾) ¬ 𝜓) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧))) → ((𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘(𝐾 + 1)) ¬ 𝜓) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧)))))
 
5-Dec-2021divalglemqt 10319 Lemma for divalg 10324. The 𝑄 = 𝑇 case involved in showing uniqueness. (Contributed by Jim Kingdon, 5-Dec-2021.)
(𝜑 → 𝐷 ∈ ℤ)    &   (𝜑 → 𝑅 ∈ ℤ)    &   (𝜑 → 𝑆 ∈ ℤ)    &   (𝜑 → 𝑄 ∈ ℤ)    &   (𝜑 → 𝑇 ∈ ℤ)    &   (𝜑 → 𝑄 = 𝑇)    &   (𝜑 → ((𝑄 · 𝐷) + 𝑅) = ((𝑇 · 𝐷) + 𝑆))    ⇒   (𝜑 → 𝑅 = 𝑆)
 
4-Dec-2021divalglemeuneg 10323 Lemma for divalg 10324. Uniqueness for a negative denominator. (Contributed by Jim Kingdon, 4-Dec-2021.)
((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) → ∃!𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)))
 
4-Dec-2021divalglemeunn 10321 Lemma for divalg 10324. Uniqueness for a positive denominator. (Contributed by Jim Kingdon, 4-Dec-2021.)
((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → ∃!𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)))
 
4-Dec-2021divalglemnqt 10320 Lemma for divalg 10324. The 𝑄 < 𝑇 case involved in showing uniqueness. (Contributed by Jim Kingdon, 4-Dec-2021.)
(𝜑 → 𝐷 ∈ ℕ)    &   (𝜑 → 𝑅 ∈ ℤ)    &   (𝜑 → 𝑆 ∈ ℤ)    &   (𝜑 → 𝑄 ∈ ℤ)    &   (𝜑 → 𝑇 ∈ ℤ)    &   (𝜑 → 0 ≤ 𝑆)    &   (𝜑 → 𝑅 < 𝐷)    &   (𝜑 → ((𝑄 · 𝐷) + 𝑅) = ((𝑇 · 𝐷) + 𝑆))    ⇒   (𝜑 → ¬ 𝑄 < 𝑇)
 
2-Dec-2021rspc2gv 2712 Restricted specialization with two quantifiers, using implicit substitution. (Contributed by BJ, 2-Dec-2021.)
((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓))    ⇒   ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑊 𝜑 → 𝜓))
  Copyright terms: Public domain W3C HTML validation [external]