Intuitionistic Logic Explorer Home Intuitionistic Logic Explorer
Most Recent Proofs 		 
Mirrors  >  Home  >  ILE Home  >  Th. List  >  Recent MPE Most Recent             Other  >  MM 100
Most recent proofs    These are the 100 (Unicode, GIF) or 1000 (Unicode, GIF) most recent proofs in the iset.mm database for the Intuitionistic Logic Explorer. The iset.mm database is maintained on GitHub with master (stable) and develop (development) versions. This page was created from the commit given on the MPE Most Recent Proofs page. The database from that commit is also available here: iset.mm.

See the MPE Most Recent Proofs page for news and some useful links.

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

Last updated on 21-Dec-2024 at 6:47 AM ET.
Recent Additions to the Intuitionistic Logic Explorer
DateLabelDescription
Theorem
 
9-Dec-2024nninfwlpoim 7154 Decidable equality for ℕ∞ implies the Weak Limited Principle of Omniscience (WLPO). (Contributed by Jim Kingdon, 9-Dec-2024.)
(∀𝑥 ∈ ℕ∞ ∀𝑦 ∈ ℕ∞ DECID 𝑥 = 𝑦 → ω ∈ WOmni)
 
8-Dec-2024nninfwlpoimlemdc 7153 Lemma for nninfwlpoim 7154. (Contributed by Jim Kingdon, 8-Dec-2024.)
(𝜑 → 𝐹:ω⟶2o)    &   𝐺 = (𝑖 ∈ ω ↦ if(∃𝑥 ∈ suc 𝑖(𝐹‘𝑥) = ∅, ∅, 1o))    &   (𝜑 → ∀𝑥 ∈ ℕ∞ ∀𝑦 ∈ ℕ∞ DECID 𝑥 = 𝑦)    ⇒   (𝜑 → DECID ∀𝑛 ∈ ω (𝐹‘𝑛) = 1o)
 
8-Dec-2024nninfwlpoimlemginf 7152 Lemma for nninfwlpoim 7154. (Contributed by Jim Kingdon, 8-Dec-2024.)
(𝜑 → 𝐹:ω⟶2o)    &   𝐺 = (𝑖 ∈ ω ↦ if(∃𝑥 ∈ suc 𝑖(𝐹‘𝑥) = ∅, ∅, 1o))    ⇒   (𝜑 → (𝐺 = (𝑖 ∈ ω ↦ 1o) ↔ ∀𝑛 ∈ ω (𝐹‘𝑛) = 1o))
 
8-Dec-2024nninfwlpoimlemg 7151 Lemma for nninfwlpoim 7154. (Contributed by Jim Kingdon, 8-Dec-2024.)
(𝜑 → 𝐹:ω⟶2o)    &   𝐺 = (𝑖 ∈ ω ↦ if(∃𝑥 ∈ suc 𝑖(𝐹‘𝑥) = ∅, ∅, 1o))    ⇒   (𝜑 → 𝐺 ∈ ℕ∞)
 
7-Dec-2024nninfwlpor 7150 The Weak Limited Principle of Omniscience (WLPO) implies that equality for ℕ∞ is decidable. (Contributed by Jim Kingdon, 7-Dec-2024.)
(ω ∈ WOmni → ∀𝑥 ∈ ℕ∞ ∀𝑦 ∈ ℕ∞ DECID 𝑥 = 𝑦)
 
7-Dec-2024nninfwlporlem 7149 Lemma for nninfwlpor 7150. The result. (Contributed by Jim Kingdon, 7-Dec-2024.)
(𝜑 → 𝑋:ω⟶2o)    &   (𝜑 → 𝑌:ω⟶2o)    &   𝐷 = (𝑖 ∈ ω ↦ if((𝑋‘𝑖) = (𝑌‘𝑖), 1o, ∅))    &   (𝜑 → ω ∈ WOmni)    ⇒   (𝜑 → DECID 𝑋 = 𝑌)
 
6-Dec-2024nninfwlporlemd 7148 Given two countably infinite sequences of zeroes and ones, they are equal if and only if a sequence formed by pointwise comparing them is all ones. (Contributed by Jim Kingdon, 6-Dec-2024.)
(𝜑 → 𝑋:ω⟶2o)    &   (𝜑 → 𝑌:ω⟶2o)    &   𝐷 = (𝑖 ∈ ω ↦ if((𝑋‘𝑖) = (𝑌‘𝑖), 1o, ∅))    ⇒   (𝜑 → (𝑋 = 𝑌 ↔ 𝐷 = (𝑖 ∈ ω ↦ 1o)))
 
3-Dec-2024nninfwlpo 7155 Decidability of equality for ℕ∞ is equivalent to the Weak Limited Principle of Omniscience (WLPO). (Contributed by Jim Kingdon, 3-Dec-2024.)
(∀𝑥 ∈ ℕ∞ ∀𝑦 ∈ ℕ∞ DECID 𝑥 = 𝑦 ↔ ω ∈ WOmni)
 
3-Dec-2024nninfdcinf 7147 The Weak Limited Principle of Omniscience (WLPO) implies that it is decidable whether an element of ℕ∞ equals the point at infinity. (Contributed by Jim Kingdon, 3-Dec-2024.)
(𝜑 → ω ∈ WOmni)    &   (𝜑 → 𝑁 ∈ ℕ∞)    ⇒   (𝜑 → DECID 𝑁 = (𝑖 ∈ ω ↦ 1o))
 
28-Nov-2024basmexd 12475 A structure whose base is inhabited is a set. (Contributed by Jim Kingdon, 28-Nov-2024.)
(𝜑 → 𝐵 = (Base‘𝐺))    &   (𝜑 → 𝐴 ∈ 𝐵)    ⇒   (𝜑 → 𝐺 ∈ V)
 
22-Nov-2024eliotaeu 5187 An inhabited iota expression has a unique value. (Contributed by Jim Kingdon, 22-Nov-2024.)
(𝐴 ∈ (℩𝑥𝜑) → ∃!𝑥𝜑)
 
22-Nov-2024eliota 5186 An element of an iota expression. (Contributed by Jim Kingdon, 22-Nov-2024.)
(𝐴 ∈ (℩𝑥𝜑) ↔ ∃𝑦(𝐴 ∈ 𝑦 ∧ ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)))
 
18-Nov-2024basmex 12474 A structure whose base is inhabited is a set. (Contributed by Jim Kingdon, 18-Nov-2024.)
𝐵 = (Base‘𝐺)    ⇒   (𝐴 ∈ 𝐵 → 𝐺 ∈ V)
 
11-Nov-2024bj-con1st 13786 Contraposition when the antecedent is a negated stable proposition. See con1dc 851. (Contributed by BJ, 11-Nov-2024.)
(STAB 𝜑 → ((¬ 𝜑 → 𝜓) → (¬ 𝜓 → 𝜑)))
 
11-Nov-2024const 847 Contraposition when the antecedent is a negated stable proposition. See comment of condc 848. (Contributed by BJ, 18-Nov-2023.) (Proof shortened by BJ, 11-Nov-2024.)
(STAB 𝜑 → ((¬ 𝜑 → ¬ 𝜓) → (𝜓 → 𝜑)))
 
4-Nov-2024lgsfvalg 13700 Value of the function 𝐹 which defines the Legendre symbol at the primes. (Contributed by Mario Carneiro, 4-Feb-2015.) (Revised by Jim Kingdon, 4-Nov-2024.)
𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑁)), 1))    ⇒   ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (𝐹‘𝑀) = if(𝑀 ∈ ℙ, (if(𝑀 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑀 − 1) / 2)) + 1) mod 𝑀) − 1))↑(𝑀 pCnt 𝑁)), 1))
 
1-Nov-2024qsqeqor 10586 The squares of two rational numbers are equal iff one number equals the other or its negative. (Contributed by Jim Kingdon, 1-Nov-2024.)
((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → ((𝐴↑2) = (𝐵↑2) ↔ (𝐴 = 𝐵 ∨ 𝐴 = -𝐵)))
 
29-Oct-2024fiubnn 10765 A finite set of natural numbers has an upper bound which is a a natural number. (Contributed by Jim Kingdon, 29-Oct-2024.)
((𝐴 ⊆ ℕ ∧ 𝐴 ∈ Fin) → ∃𝑥 ∈ ℕ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)
 
29-Oct-2024fiubz 10764 A finite set of integers has an upper bound which is an integer. (Contributed by Jim Kingdon, 29-Oct-2024.)
((𝐴 ⊆ ℤ ∧ 𝐴 ∈ Fin) → ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)
 
29-Oct-2024fiubm 10763 Lemma for fiubz 10764 and fiubnn 10765. A general form of those theorems. (Contributed by Jim Kingdon, 29-Oct-2024.)
(𝜑 → 𝐴 ⊆ 𝐵)    &   (𝜑 → 𝐵 ⊆ ℚ)    &   (𝜑 → 𝐶 ∈ 𝐵)    &   (𝜑 → 𝐴 ∈ Fin)    ⇒   (𝜑 → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)
 
27-Oct-2024bj-nnst 13778 Double negation of stability of a formula. Intuitionistic logic refutes unstability (but does not prove stability) of any formula. This theorem can also be proved in classical refutability calculus (see https://us.metamath.org/mpeuni/bj-peircestab.html) but not in minimal calculus (see https://us.metamath.org/mpeuni/bj-stabpeirce.html). See nnnotnotr 14025 for the version not using the definition of stability. (Contributed by BJ, 9-Oct-2019.) Prove it in ( → , ¬ ) -intuitionistic calculus with definitions (uses of ax-ia1 105, ax-ia2 106, ax-ia3 107 are via sylibr 133, necessary for definition unpackaging), and in ( → , ↔ , ¬ )-intuitionistic calculus, following a discussion with Jim Kingdon. (Revised by BJ, 27-Oct-2024.)
¬ ¬ STAB 𝜑
 
27-Oct-2024bj-imnimnn 13773 If a formula is implied by both a formula and its negation, then it is not refutable. There is another proof using the inference associated with bj-nnclavius 13772 as its last step. (Contributed by BJ, 27-Oct-2024.)
(𝜑 → 𝜓)    &   (¬ 𝜑 → 𝜓)    ⇒    ¬ ¬ 𝜓
 
25-Oct-2024nnwosdc 11994 Well-ordering principle: any inhabited decidable set of positive integers has a least element (schema form). (Contributed by NM, 17-Aug-2001.) (Revised by Jim Kingdon, 25-Oct-2024.)
(𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ((∃𝑥 ∈ ℕ 𝜑 ∧ ∀𝑥 ∈ ℕ DECID 𝜑) → ∃𝑥 ∈ ℕ (𝜑 ∧ ∀𝑦 ∈ ℕ (𝜓 → 𝑥 ≤ 𝑦)))
 
23-Oct-2024nnwodc 11991 Well-ordering principle: any inhabited decidable set of positive integers has a least element. Theorem I.37 (well-ordering principle) of [Apostol] p. 34. (Contributed by NM, 17-Aug-2001.) (Revised by Jim Kingdon, 23-Oct-2024.)
((𝐴 ⊆ ℕ ∧ ∃𝑤 𝑤 ∈ 𝐴 ∧ ∀𝑗 ∈ ℕ DECID 𝑗 ∈ 𝐴) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦)
 
22-Oct-2024uzwodc 11992 Well-ordering principle: any inhabited decidable subset of an upper set of integers has a least element. (Contributed by NM, 8-Oct-2005.) (Revised by Jim Kingdon, 22-Oct-2024.)
((𝑆 ⊆ (ℤ≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ≥‘𝑀)DECID 𝑥 ∈ 𝑆) → ∃𝑗 ∈ 𝑆 ∀𝑘 ∈ 𝑆 𝑗 ≤ 𝑘)
 
21-Oct-2024nnnotnotr 14025 Double negation of double negation elimination. Suggested by an online post by Martin Escardo. Although this statement resembles nnexmid 845, it can be proved with reference only to implication and negation (that is, without use of disjunction). (Contributed by Jim Kingdon, 21-Oct-2024.)
¬ ¬ (¬ ¬ 𝜑 → 𝜑)
 
20-Oct-2024isprm5lem 12095 Lemma for isprm5 12096. The interesting direction (showing that one only needs to check prime divisors up to the square root of 𝑃). (Contributed by Jim Kingdon, 20-Oct-2024.)
(𝜑 → 𝑃 ∈ (ℤ≥‘2))    &   (𝜑 → ∀𝑧 ∈ ℙ ((𝑧↑2) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃))    &   (𝜑 → 𝑋 ∈ (2...(𝑃 − 1)))    ⇒   (𝜑 → ¬ 𝑋 ∥ 𝑃)
 
17-Oct-2024elnndc 9571 Membership of an integer in ℕ is decidable. (Contributed by Jim Kingdon, 17-Oct-2024.)
(𝑁 ∈ ℤ → DECID 𝑁 ∈ ℕ)
 
14-Oct-20242zinfmin 11206 Two ways to express the minimum of two integers. Because order of integers is decidable, we have more flexibility than for real numbers. (Contributed by Jim Kingdon, 14-Oct-2024.)
((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → inf({𝐴, 𝐵}, ℝ, < ) = if(𝐴 ≤ 𝐵, 𝐴, 𝐵))
 
14-Oct-2024mingeb 11205 Equivalence of ≤ and being equal to the minimum of two reals. (Contributed by Jim Kingdon, 14-Oct-2024.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ inf({𝐴, 𝐵}, ℝ, < ) = 𝐴))
 
13-Oct-2024pcxnn0cl 12264 Extended nonnegative integer closure of the general prime count function. (Contributed by Jim Kingdon, 13-Oct-2024.)
((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → (𝑃 pCnt 𝑁) ∈ ℕ0*)
 
13-Oct-2024xnn0letri 9760 Dichotomy for extended nonnegative integers. (Contributed by Jim Kingdon, 13-Oct-2024.)
((𝐴 ∈ ℕ0* ∧ 𝐵 ∈ ℕ0*) → (𝐴 ≤ 𝐵 ∨ 𝐵 ≤ 𝐴))
 
13-Oct-2024xnn0dcle 9759 Decidability of ≤ for extended nonnegative integers. (Contributed by Jim Kingdon, 13-Oct-2024.)
((𝐴 ∈ ℕ0* ∧ 𝐵 ∈ ℕ0*) → DECID 𝐴 ≤ 𝐵)
 
9-Oct-2024nn0leexp2 10645 Ordering law for exponentiation. (Contributed by Jim Kingdon, 9-Oct-2024.)
(((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 1 < 𝐴) → (𝑀 ≤ 𝑁 ↔ (𝐴↑𝑀) ≤ (𝐴↑𝑁)))
 
8-Oct-2024pclemdc 12242 Lemma for the prime power pre-function's properties. (Contributed by Jim Kingdon, 8-Oct-2024.)
𝐴 = {𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑁}    ⇒   ((𝑃 ∈ (ℤ≥‘2) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → ∀𝑥 ∈ ℤ DECID 𝑥 ∈ 𝐴)
 
8-Oct-2024elnn0dc 9570 Membership of an integer in ℕ0 is decidable. (Contributed by Jim Kingdon, 8-Oct-2024.)
(𝑁 ∈ ℤ → DECID 𝑁 ∈ ℕ0)
 
7-Oct-2024pclemub 12241 Lemma for the prime power pre-function's properties. (Contributed by Mario Carneiro, 23-Feb-2014.) (Revised by Jim Kingdon, 7-Oct-2024.)
𝐴 = {𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑁}    ⇒   ((𝑃 ∈ (ℤ≥‘2) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)
 
7-Oct-2024pclem0 12240 Lemma for the prime power pre-function's properties. (Contributed by Mario Carneiro, 23-Feb-2014.) (Revised by Jim Kingdon, 7-Oct-2024.)
𝐴 = {𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑁}    ⇒   ((𝑃 ∈ (ℤ≥‘2) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → 0 ∈ 𝐴)
 
7-Oct-2024nn0ltexp2 10644 Special case of ltexp2 13654 which we use here because we haven't yet defined df-rpcxp 13574 which is used in the current proof of ltexp2 13654. (Contributed by Jim Kingdon, 7-Oct-2024.)
(((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 1 < 𝐴) → (𝑀 < 𝑁 ↔ (𝐴↑𝑀) < (𝐴↑𝑁)))
 
6-Oct-2024suprzcl2dc 11910 The supremum of a bounded-above decidable set of integers is a member of the set. (This theorem avoids ax-pre-suploc 7895.) (Contributed by Mario Carneiro, 21-Apr-2015.) (Revised by Jim Kingdon, 6-Oct-2024.)
(𝜑 → 𝐴 ⊆ ℤ)    &   (𝜑 → ∀𝑥 ∈ ℤ DECID 𝑥 ∈ 𝐴)    &   (𝜑 → ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)    &   (𝜑 → ∃𝑥 𝑥 ∈ 𝐴)    ⇒   (𝜑 → sup(𝐴, ℝ, < ) ∈ 𝐴)
 
5-Oct-2024zsupssdc 11909 An inhabited decidable bounded subset of integers has a supremum in the set. (The proof does not use ax-pre-suploc 7895.) (Contributed by Mario Carneiro, 21-Apr-2015.) (Revised by Jim Kingdon, 5-Oct-2024.)
(𝜑 → 𝐴 ⊆ ℤ)    &   (𝜑 → ∃𝑥 𝑥 ∈ 𝐴)    &   (𝜑 → ∀𝑥 ∈ ℤ DECID 𝑥 ∈ 𝐴)    &   (𝜑 → ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)    ⇒   (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ 𝐵 (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)))
 
5-Oct-2024suprzubdc 11907 The supremum of a bounded-above decidable set of integers is greater than any member of the set. (Contributed by Mario Carneiro, 21-Apr-2015.) (Revised by Jim Kingdon, 5-Oct-2024.)
(𝜑 → 𝐴 ⊆ ℤ)    &   (𝜑 → ∀𝑥 ∈ ℤ DECID 𝑥 ∈ 𝐴)    &   (𝜑 → ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)    &   (𝜑 → 𝐵 ∈ 𝐴)    ⇒   (𝜑 → 𝐵 ≤ sup(𝐴, ℝ, < ))
 
1-Oct-2024infex2g 7011 Existence of infimum. (Contributed by Jim Kingdon, 1-Oct-2024.)
(𝐴 ∈ 𝐶 → inf(𝐵, 𝐴, 𝑅) ∈ V)
 
30-Sep-2024unbendc 12409 An unbounded decidable set of positive integers is infinite. (Contributed by NM, 5-May-2005.) (Revised by Jim Kingdon, 30-Sep-2024.)
((𝐴 ⊆ ℕ ∧ ∀𝑥 ∈ ℕ DECID 𝑥 ∈ 𝐴 ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝐴 𝑚 < 𝑛) → 𝐴 ≈ ℕ)
 
30-Sep-2024prmdc 12084 Primality is decidable. (Contributed by Jim Kingdon, 30-Sep-2024.)
(𝑁 ∈ ℕ → DECID 𝑁 ∈ ℙ)
 
30-Sep-2024dcfi 6958 Decidability of a family of propositions indexed by a finite set. (Contributed by Jim Kingdon, 30-Sep-2024.)
((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 DECID 𝜑) → DECID ∀𝑥 ∈ 𝐴 𝜑)
 
29-Sep-2024ssnnct 12402 A decidable subset of ℕ is countable. (Contributed by Jim Kingdon, 29-Sep-2024.)
((𝐴 ⊆ ℕ ∧ ∀𝑥 ∈ ℕ DECID 𝑥 ∈ 𝐴) → ∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o))
 
29-Sep-2024ssnnctlemct 12401 Lemma for ssnnct 12402. The result. (Contributed by Jim Kingdon, 29-Sep-2024.)
𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 1)    ⇒   ((𝐴 ⊆ ℕ ∧ ∀𝑥 ∈ ℕ DECID 𝑥 ∈ 𝐴) → ∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o))
 
28-Sep-2024nninfdcex 11908 A decidable set of natural numbers has an infimum. (Contributed by Jim Kingdon, 28-Sep-2024.)
(𝜑 → 𝐴 ⊆ ℕ)    &   (𝜑 → ∀𝑥 ∈ ℕ DECID 𝑥 ∈ 𝐴)    &   (𝜑 → ∃𝑦 𝑦 ∈ 𝐴)    ⇒   (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))
 
27-Sep-2024infregelbex 9557 Any lower bound of a set of real numbers with an infimum is less than or equal to the infimum. (Contributed by Jim Kingdon, 27-Sep-2024.)
(𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))    &   (𝜑 → 𝐴 ⊆ ℝ)    &   (𝜑 → 𝐵 ∈ ℝ)    ⇒   (𝜑 → (𝐵 ≤ inf(𝐴, ℝ, < ) ↔ ∀𝑧 ∈ 𝐴 𝐵 ≤ 𝑧))
 
26-Sep-2024nninfdclemp1 12405 Lemma for nninfdc 12408. Each element of the sequence 𝐹 is greater than the previous element. (Contributed by Jim Kingdon, 26-Sep-2024.)
(𝜑 → 𝐴 ⊆ ℕ)    &   (𝜑 → ∀𝑥 ∈ ℕ DECID 𝑥 ∈ 𝐴)    &   (𝜑 → ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝐴 𝑚 < 𝑛)    &   (𝜑 → (𝐽 ∈ 𝐴 ∧ 1 < 𝐽))    &   𝐹 = seq1((𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ≥‘(𝑦 + 1))), ℝ, < )), (𝑖 ∈ ℕ ↦ 𝐽))    &   (𝜑 → 𝑈 ∈ ℕ)    ⇒   (𝜑 → (𝐹‘𝑈) < (𝐹‘(𝑈 + 1)))
 
26-Sep-2024nnminle 11990 The infimum of a decidable subset of the natural numbers is less than an element of the set. The infimum is also a minimum as shown at nnmindc 11989. (Contributed by Jim Kingdon, 26-Sep-2024.)
((𝐴 ⊆ ℕ ∧ ∀𝑥 ∈ ℕ DECID 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐴) → inf(𝐴, ℝ, < ) ≤ 𝐵)
 
25-Sep-2024nninfdclemcl 12403 Lemma for nninfdc 12408. (Contributed by Jim Kingdon, 25-Sep-2024.)
(𝜑 → 𝐴 ⊆ ℕ)    &   (𝜑 → ∀𝑥 ∈ ℕ DECID 𝑥 ∈ 𝐴)    &   (𝜑 → ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝐴 𝑚 < 𝑛)    &   (𝜑 → 𝑃 ∈ 𝐴)    &   (𝜑 → 𝑄 ∈ 𝐴)    ⇒   (𝜑 → (𝑃(𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ≥‘(𝑦 + 1))), ℝ, < ))𝑄) ∈ 𝐴)
 
24-Sep-2024nninfdclemlt 12406 Lemma for nninfdc 12408. The function from nninfdclemf 12404 is strictly monotonic. (Contributed by Jim Kingdon, 24-Sep-2024.)
(𝜑 → 𝐴 ⊆ ℕ)    &   (𝜑 → ∀𝑥 ∈ ℕ DECID 𝑥 ∈ 𝐴)    &   (𝜑 → ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝐴 𝑚 < 𝑛)    &   (𝜑 → (𝐽 ∈ 𝐴 ∧ 1 < 𝐽))    &   𝐹 = seq1((𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ≥‘(𝑦 + 1))), ℝ, < )), (𝑖 ∈ ℕ ↦ 𝐽))    &   (𝜑 → 𝑈 ∈ ℕ)    &   (𝜑 → 𝑉 ∈ ℕ)    &   (𝜑 → 𝑈 < 𝑉)    ⇒   (𝜑 → (𝐹‘𝑈) < (𝐹‘𝑉))
 
23-Sep-2024nninfdc 12408 An unbounded decidable set of positive integers is infinite. (Contributed by Jim Kingdon, 23-Sep-2024.)
((𝐴 ⊆ ℕ ∧ ∀𝑥 ∈ ℕ DECID 𝑥 ∈ 𝐴 ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝐴 𝑚 < 𝑛) → ω ≼ 𝐴)
 
23-Sep-2024nninfdclemf1 12407 Lemma for nninfdc 12408. The function from nninfdclemf 12404 is one-to-one. (Contributed by Jim Kingdon, 23-Sep-2024.)
(𝜑 → 𝐴 ⊆ ℕ)    &   (𝜑 → ∀𝑥 ∈ ℕ DECID 𝑥 ∈ 𝐴)    &   (𝜑 → ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝐴 𝑚 < 𝑛)    &   (𝜑 → (𝐽 ∈ 𝐴 ∧ 1 < 𝐽))    &   𝐹 = seq1((𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ≥‘(𝑦 + 1))), ℝ, < )), (𝑖 ∈ ℕ ↦ 𝐽))    ⇒   (𝜑 → 𝐹:ℕ–1-1→𝐴)
 
23-Sep-2024nninfdclemf 12404 Lemma for nninfdc 12408. A function from the natural numbers into 𝐴. (Contributed by Jim Kingdon, 23-Sep-2024.)
(𝜑 → 𝐴 ⊆ ℕ)    &   (𝜑 → ∀𝑥 ∈ ℕ DECID 𝑥 ∈ 𝐴)    &   (𝜑 → ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝐴 𝑚 < 𝑛)    &   (𝜑 → (𝐽 ∈ 𝐴 ∧ 1 < 𝐽))    &   𝐹 = seq1((𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ≥‘(𝑦 + 1))), ℝ, < )), (𝑖 ∈ ℕ ↦ 𝐽))    ⇒   (𝜑 → 𝐹:ℕ⟶𝐴)
 
23-Sep-2024nnmindc 11989 An inhabited decidable subset of the natural numbers has a minimum. (Contributed by Jim Kingdon, 23-Sep-2024.)
((𝐴 ⊆ ℕ ∧ ∀𝑥 ∈ ℕ DECID 𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ 𝐴) → inf(𝐴, ℝ, < ) ∈ 𝐴)
 
19-Sep-2024ssomct 12400 A decidable subset of ω is countable. (Contributed by Jim Kingdon, 19-Sep-2024.)
((𝐴 ⊆ ω ∧ ∀𝑥 ∈ ω DECID 𝑥 ∈ 𝐴) → ∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o))
 
14-Sep-2024nnpredlt 4608 The predecessor (see nnpredcl 4607) of a nonzero natural number is less than (see df-iord 4351) that number. (Contributed by Jim Kingdon, 14-Sep-2024.)
((𝐴 ∈ ω ∧ 𝐴 ≠ ∅) → ∪ 𝐴 ∈ 𝐴)
 
13-Sep-2024nninfisollemeq 7108 Lemma for nninfisol 7109. The case where 𝑁 is a successor and 𝑁 and 𝑋 are equal. (Contributed by Jim Kingdon, 13-Sep-2024.)
(𝜑 → 𝑋 ∈ ℕ∞)    &   (𝜑 → (𝑋‘𝑁) = ∅)    &   (𝜑 → 𝑁 ∈ ω)    &   (𝜑 → 𝑁 ≠ ∅)    &   (𝜑 → (𝑋‘∪ 𝑁) = 1o)    ⇒   (𝜑 → DECID (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋)
 
13-Sep-2024nninfisollemne 7107 Lemma for nninfisol 7109. A case where 𝑁 is a successor and 𝑁 and 𝑋 are not equal. (Contributed by Jim Kingdon, 13-Sep-2024.)
(𝜑 → 𝑋 ∈ ℕ∞)    &   (𝜑 → (𝑋‘𝑁) = ∅)    &   (𝜑 → 𝑁 ∈ ω)    &   (𝜑 → 𝑁 ≠ ∅)    &   (𝜑 → (𝑋‘∪ 𝑁) = ∅)    ⇒   (𝜑 → DECID (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋)
 
13-Sep-2024nninfisollem0 7106 Lemma for nninfisol 7109. The case where 𝑁 is zero. (Contributed by Jim Kingdon, 13-Sep-2024.)
(𝜑 → 𝑋 ∈ ℕ∞)    &   (𝜑 → (𝑋‘𝑁) = ∅)    &   (𝜑 → 𝑁 ∈ ω)    &   (𝜑 → 𝑁 = ∅)    ⇒   (𝜑 → DECID (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋)
 
12-Sep-2024nninfisol 7109 Finite elements of ℕ∞ are isolated. That is, given a natural number and any element of ℕ∞, it is decidable whether the natural number (when converted to an element of ℕ∞) is equal to the given element of ℕ∞. Stated in an online post by Martin Escardo. One way to understand this theorem is that you do not need to look at an unbounded number of elements of the sequence 𝑋 to decide whether it is equal to 𝑁 (in fact, you only need to look at two elements and 𝑁 tells you where to look). (Contributed by BJ and Jim Kingdon, 12-Sep-2024.)
((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) → DECID (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋)
 
7-Sep-2024eulerthlemfi 12182 Lemma for eulerth 12187. The set 𝑆 is finite. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 7-Sep-2024.)
(𝜑 → (𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1))    &   𝑆 = {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1}    ⇒   (𝜑 → 𝑆 ∈ Fin)
 
7-Sep-2024modqexp 10602 Exponentiation property of the modulo operation, see theorem 5.2(c) in [ApostolNT] p. 107. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 7-Sep-2024.)
(𝜑 → 𝐴 ∈ ℤ)    &   (𝜑 → 𝐵 ∈ ℤ)    &   (𝜑 → 𝐶 ∈ ℕ0)    &   (𝜑 → 𝐷 ∈ ℚ)    &   (𝜑 → 0 < 𝐷)    &   (𝜑 → (𝐴 mod 𝐷) = (𝐵 mod 𝐷))    ⇒   (𝜑 → ((𝐴↑𝐶) mod 𝐷) = ((𝐵↑𝐶) mod 𝐷))
 
5-Sep-2024eulerthlemh 12185 Lemma for eulerth 12187. A permutation of (1...(ϕ‘𝑁)). (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 5-Sep-2024.)
(𝜑 → (𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1))    &   𝑆 = {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1}    &   (𝜑 → 𝐹:(1...(ϕ‘𝑁))–1-1-onto→𝑆)    &   𝐻 = (◡𝐹 ∘ (𝑦 ∈ (1...(ϕ‘𝑁)) ↦ ((𝐴 · (𝐹‘𝑦)) mod 𝑁)))    ⇒   (𝜑 → 𝐻:(1...(ϕ‘𝑁))–1-1-onto→(1...(ϕ‘𝑁)))
 
2-Sep-2024eulerthlemth 12186 Lemma for eulerth 12187. The result. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 2-Sep-2024.)
(𝜑 → (𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1))    &   𝑆 = {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1}    &   (𝜑 → 𝐹:(1...(ϕ‘𝑁))–1-1-onto→𝑆)    ⇒   (𝜑 → ((𝐴↑(ϕ‘𝑁)) mod 𝑁) = (1 mod 𝑁))
 
2-Sep-2024eulerthlema 12184 Lemma for eulerth 12187. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 2-Sep-2024.)
(𝜑 → (𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1))    &   𝑆 = {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1}    &   (𝜑 → 𝐹:(1...(ϕ‘𝑁))–1-1-onto→𝑆)    ⇒   (𝜑 → (((𝐴↑(ϕ‘𝑁)) · ∏𝑥 ∈ (1...(ϕ‘𝑁))(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...(ϕ‘𝑁))((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁))
 
2-Sep-2024eulerthlemrprm 12183 Lemma for eulerth 12187. 𝑁 and ∏𝑥 ∈ (1...(ϕ‘𝑁))(𝐹‘𝑥) are relatively prime. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 2-Sep-2024.)
(𝜑 → (𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1))    &   𝑆 = {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1}    &   (𝜑 → 𝐹:(1...(ϕ‘𝑁))–1-1-onto→𝑆)    ⇒   (𝜑 → (𝑁 gcd ∏𝑥 ∈ (1...(ϕ‘𝑁))(𝐹‘𝑥)) = 1)
 
30-Aug-2024fprodap0f 11599 A finite product of terms apart from zero is apart from zero. A version of fprodap0 11584 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.) (Revised by Jim Kingdon, 30-Aug-2024.)
Ⅎ𝑘𝜑    &   (𝜑 → 𝐴 ∈ Fin)    &   ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 # 0)    ⇒   (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 # 0)
 
28-Aug-2024fprodrec 11592 The finite product of reciprocals is the reciprocal of the product. (Contributed by Jim Kingdon, 28-Aug-2024.)
(𝜑 → 𝐴 ∈ Fin)    &   ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 # 0)    ⇒   (𝜑 → ∏𝑘 ∈ 𝐴 (1 / 𝐵) = (1 / ∏𝑘 ∈ 𝐴 𝐵))
 
26-Aug-2024exmidontri2or 7220 Ordinal trichotomy is equivalent to excluded middle. (Contributed by Jim Kingdon, 26-Aug-2024.)
(EXMID ↔ ∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥))
 
26-Aug-2024exmidontri 7216 Ordinal trichotomy is equivalent to excluded middle. (Contributed by Jim Kingdon, 26-Aug-2024.)
(EXMID ↔ ∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥))
 
26-Aug-2024ontri2orexmidim 4556 Ordinal trichotomy implies excluded middle. Closed form of ordtri2or2exmid 4555. (Contributed by Jim Kingdon, 26-Aug-2024.)
(∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥) → DECID 𝜑)
 
26-Aug-2024ontriexmidim 4506 Ordinal trichotomy implies excluded middle. Closed form of ordtriexmid 4505. (Contributed by Jim Kingdon, 26-Aug-2024.)
(∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) → DECID 𝜑)
 
25-Aug-2024onntri2or 7223 Double negated ordinal trichotomy. (Contributed by Jim Kingdon, 25-Aug-2024.)
(¬ ¬ EXMID ↔ ∀𝑥 ∈ On ∀𝑦 ∈ On ¬ ¬ (𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥))
 
25-Aug-2024onntri3or 7222 Double negated ordinal trichotomy. (Contributed by Jim Kingdon, 25-Aug-2024.)
(¬ ¬ EXMID ↔ ∀𝑥 ∈ On ∀𝑦 ∈ On ¬ ¬ (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥))
 
25-Aug-2024csbcow 3060 Composition law for chained substitutions into a class. Version of csbco 3059 with a disjoint variable condition, which requires fewer axioms. (Contributed by NM, 10-Nov-2005.) (Revised by Gino Giotto, 25-Aug-2024.)
⦋𝐴 / 𝑦⦌⦋𝑦 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵
 
25-Aug-2024cbvreuvw 2702 Version of cbvreuv 2698 with a disjoint variable condition. (Contributed by Gino Giotto, 10-Jan-2024.) Reduce axiom usage. (Revised by Gino Giotto, 25-Aug-2024.)
(𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑦 ∈ 𝐴 𝜓)
 
25-Aug-2024cbvrexvw 2701 Version of cbvrexv 2697 with a disjoint variable condition. (Contributed by Gino Giotto, 10-Jan-2024.) Reduce axiom usage. (Revised by Gino Giotto, 25-Aug-2024.)
(𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)
 
25-Aug-2024cbvralvw 2700 Version of cbvralv 2696 with a disjoint variable condition. (Contributed by Gino Giotto, 10-Jan-2024.) Reduce axiom usage. (Revised by Gino Giotto, 25-Aug-2024.)
(𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)
 
25-Aug-2024cbvabw 2293 Version of cbvab 2294 with a disjoint variable condition. (Contributed by Gino Giotto, 10-Jan-2024.) Reduce axiom usage. (Revised by Gino Giotto, 25-Aug-2024.)
Ⅎ𝑦𝜑    &   Ⅎ𝑥𝜓    &   (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓}
 
25-Aug-2024nfsbv 1940 If 𝑧 is not free in 𝜑, it is not free in [𝑦 / 𝑥]𝜑 when 𝑧 is distinct from 𝑥 and 𝑦. Version of nfsb 1939 requiring more disjoint variables. (Contributed by Wolf Lammen, 7-Feb-2023.) Remove disjoint variable condition on 𝑥, 𝑦. (Revised by Steven Nguyen, 13-Aug-2023.) Reduce axiom usage. (Revised by Gino Giotto, 25-Aug-2024.)
Ⅎ𝑧𝜑    ⇒   Ⅎ𝑧[𝑦 / 𝑥]𝜑
 
25-Aug-2024cbvexvw 1913 Change bound variable. See cbvexv 1911 for a version with fewer disjoint variable conditions. (Contributed by NM, 19-Apr-2017.) Avoid ax-7 1441. (Revised by Gino Giotto, 25-Aug-2024.)
(𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   (∃𝑥𝜑 ↔ ∃𝑦𝜓)
 
25-Aug-2024cbvalvw 1912 Change bound variable. See cbvalv 1910 for a version with fewer disjoint variable conditions. (Contributed by NM, 9-Apr-2017.) Avoid ax-7 1441. (Revised by Gino Giotto, 25-Aug-2024.)
(𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   (∀𝑥𝜑 ↔ ∀𝑦𝜓)
 
25-Aug-2024nfal 1569 If 𝑥 is not free in 𝜑, it is not free in ∀𝑦𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.) Remove dependency on ax-4 1503. (Revised by Gino Giotto, 25-Aug-2024.)
Ⅎ𝑥𝜑    ⇒   Ⅎ𝑥∀𝑦𝜑
 
24-Aug-2024gcdcomd 11929 The gcd operator is commutative, deduction version. (Contributed by SN, 24-Aug-2024.)
(𝜑 → 𝑀 ∈ ℤ)    &   (𝜑 → 𝑁 ∈ ℤ)    ⇒   (𝜑 → (𝑀 gcd 𝑁) = (𝑁 gcd 𝑀))
 
21-Aug-2024dvds2addd 11791 Deduction form of dvds2add 11787. (Contributed by SN, 21-Aug-2024.)
(𝜑 → 𝐾 ∈ ℤ)    &   (𝜑 → 𝑀 ∈ ℤ)    &   (𝜑 → 𝑁 ∈ ℤ)    &   (𝜑 → 𝐾 ∥ 𝑀)    &   (𝜑 → 𝐾 ∥ 𝑁)    ⇒   (𝜑 → 𝐾 ∥ (𝑀 + 𝑁))
 
17-Aug-2024fprodcl2lem 11568 Finite product closure lemma. (Contributed by Scott Fenton, 14-Dec-2017.) (Revised by Jim Kingdon, 17-Aug-2024.)
(𝜑 → 𝑆 ⊆ ℂ)    &   ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 · 𝑦) ∈ 𝑆)    &   (𝜑 → 𝐴 ∈ Fin)    &   ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ 𝑆)    &   (𝜑 → 𝐴 ≠ ∅)    ⇒   (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 ∈ 𝑆)
 
16-Aug-2024if0ab 13840 Expression of a conditional class as a class abstraction when the False alternative is the empty class: in that case, the conditional class is the extension, in the True alternative, of the condition.

Remark: a consequence which could be formalized is the inclusion if(𝜑, 𝐴, ∅) ⊆ 𝐴 and therefore, using elpwg 3574, (𝐴 ∈ 𝑉 → if(𝜑, 𝐴, ∅) ∈ 𝒫 𝐴), from which fmelpw1o 13841 could be derived, yielding an alternative proof. (Contributed by BJ, 16-Aug-2024.)

if(𝜑, 𝐴, ∅) = {𝑥 ∈ 𝐴 ∣ 𝜑}
 
16-Aug-2024fprodunsn 11567 Multiply in an additional term in a finite product. See also fprodsplitsn 11596 which is the same but with a Ⅎ𝑘𝜑 hypothesis in place of the distinct variable condition between 𝜑 and 𝑘. (Contributed by Jim Kingdon, 16-Aug-2024.)
Ⅎ𝑘𝐷    &   (𝜑 → 𝐴 ∈ Fin)    &   (𝜑 → 𝐵 ∈ 𝑉)    &   (𝜑 → ¬ 𝐵 ∈ 𝐴)    &   ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ)    &   (𝜑 → 𝐷 ∈ ℂ)    &   (𝑘 = 𝐵 → 𝐶 = 𝐷)    ⇒   (𝜑 → ∏𝑘 ∈ (𝐴 ∪ {𝐵})𝐶 = (∏𝑘 ∈ 𝐴 𝐶 · 𝐷))
 
15-Aug-2024bj-charfundcALT 13844 Alternate proof of bj-charfundc 13843. It was expected to be much shorter since it uses bj-charfun 13842 for the main part of the proof and the rest is basic computations, but these turn out to be lengthy, maybe because of the limited library of available lemmas. (Contributed by BJ, 15-Aug-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
(𝜑 → 𝐹 = (𝑥 ∈ 𝑋 ↦ if(𝑥 ∈ 𝐴, 1o, ∅)))    &   (𝜑 → ∀𝑥 ∈ 𝑋 DECID 𝑥 ∈ 𝐴)    ⇒   (𝜑 → (𝐹:𝑋⟶2o ∧ (∀𝑥 ∈ (𝑋 ∩ 𝐴)(𝐹‘𝑥) = 1o ∧ ∀𝑥 ∈ (𝑋 ∖ 𝐴)(𝐹‘𝑥) = ∅)))
 
15-Aug-2024bj-charfun 13842 Properties of the characteristic function on the class 𝑋 of the class 𝐴. (Contributed by BJ, 15-Aug-2024.)
(𝜑 → 𝐹 = (𝑥 ∈ 𝑋 ↦ if(𝑥 ∈ 𝐴, 1o, ∅)))    ⇒   (𝜑 → ((𝐹:𝑋⟶𝒫 1o ∧ (𝐹 ↾ ((𝑋 ∩ 𝐴) ∪ (𝑋 ∖ 𝐴))):((𝑋 ∩ 𝐴) ∪ (𝑋 ∖ 𝐴))⟶2o) ∧ (∀𝑥 ∈ (𝑋 ∩ 𝐴)(𝐹‘𝑥) = 1o ∧ ∀𝑥 ∈ (𝑋 ∖ 𝐴)(𝐹‘𝑥) = ∅)))
 
15-Aug-2024fmelpw1o 13841 With a formula 𝜑 one can associate an element of 𝒫 1o, which can therefore be thought of as the set of "truth values" (but recall that there are no other genuine truth values than ⊤ and ⊥, by nndc 846, which translate to 1o and ∅ respectively by iftrue 3531 and iffalse 3534, giving pwtrufal 14030).

As proved in if0ab 13840, the associated element of 𝒫 1o is the extension, in 𝒫 1o, of the formula 𝜑. (Contributed by BJ, 15-Aug-2024.)

if(𝜑, 1o, ∅) ∈ 𝒫 1o
 
15-Aug-2024cnstab 8564 Equality of complex numbers is stable. Stability here means ¬ ¬ 𝐴 = 𝐵 → 𝐴 = 𝐵 as defined at df-stab 826. This theorem for real numbers is Proposition 5.2 of [BauerHanson], p. 27. (Contributed by Jim Kingdon, 1-Aug-2023.) (Proof shortened by BJ, 15-Aug-2024.)
((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → STAB 𝐴 = 𝐵)
 
15-Aug-2024subap0d 8563 Two numbers apart from each other have difference apart from zero. (Contributed by Jim Kingdon, 12-Aug-2021.) (Proof shortened by BJ, 15-Aug-2024.)
(𝜑 → 𝐴 ∈ ℂ)    &   (𝜑 → 𝐵 ∈ ℂ)    &   (𝜑 → 𝐴 # 𝐵)    ⇒   (𝜑 → (𝐴 − 𝐵) # 0)
 
15-Aug-2024ifexd 4469 Existence of a conditional class (deduction form). (Contributed by BJ, 15-Aug-2024.)
(𝜑 → 𝐴 ∈ 𝑉)    &   (𝜑 → 𝐵 ∈ 𝑊)    ⇒   (𝜑 → if(𝜓, 𝐴, 𝐵) ∈ V)
 
15-Aug-2024ifelpwun 4468 Existence of a conditional class, quantitative version (inference form). (Contributed by BJ, 15-Aug-2024.)
𝐴 ∈ V    &   𝐵 ∈ V    ⇒   if(𝜑, 𝐴, 𝐵) ∈ 𝒫 (𝐴 ∪ 𝐵)
 
15-Aug-2024ifelpwund 4467 Existence of a conditional class, quantitative version (deduction form). (Contributed by BJ, 15-Aug-2024.)
(𝜑 → 𝐴 ∈ 𝑉)    &   (𝜑 → 𝐵 ∈ 𝑊)    ⇒   (𝜑 → if(𝜓, 𝐴, 𝐵) ∈ 𝒫 (𝐴 ∪ 𝐵))
  Copyright terms: Public domain W3C HTML validation [external]