HomeHome Intuitionistic Logic Explorer
Theorem List (p. 99 of 101)
< Previous  Next >
Bad symbols? Try the
GIF version.

Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 9801-9900   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremclimabs0 9801* Convergence to zero of the absolute value is equivalent to convergence to zero. (Contributed by NM, 8-Jul-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝐹𝑉)    &   (𝜑𝐺𝑊)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℂ)    &   ((𝜑𝑘𝑍) → (𝐺𝑘) = (abs‘(𝐹𝑘)))       (𝜑 → (𝐹 ⇝ 0 ↔ 𝐺 ⇝ 0))
 
Theoremclimcn1 9802* Image of a limit under a continuous map. (Contributed by Mario Carneiro, 31-Jan-2014.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝐴𝐵)    &   ((𝜑𝑧𝐵) → (𝐹𝑧) ∈ ℂ)    &   (𝜑𝐺𝐴)    &   (𝜑𝐻𝑊)    &   ((𝜑𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℝ+𝑧𝐵 ((abs‘(𝑧𝐴)) < 𝑦 → (abs‘((𝐹𝑧) − (𝐹𝐴))) < 𝑥))    &   ((𝜑𝑘𝑍) → (𝐺𝑘) ∈ 𝐵)    &   ((𝜑𝑘𝑍) → (𝐻𝑘) = (𝐹‘(𝐺𝑘)))       (𝜑𝐻 ⇝ (𝐹𝐴))
 
Theoremclimcn2 9803* Image of a limit under a continuous map, two-arg version. (Contributed by Mario Carneiro, 31-Jan-2014.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝐴𝐶)    &   (𝜑𝐵𝐷)    &   ((𝜑 ∧ (𝑢𝐶𝑣𝐷)) → (𝑢𝐹𝑣) ∈ ℂ)    &   (𝜑𝐺𝐴)    &   (𝜑𝐻𝐵)    &   (𝜑𝐾𝑊)    &   ((𝜑𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑢𝐶𝑣𝐷 (((abs‘(𝑢𝐴)) < 𝑦 ∧ (abs‘(𝑣𝐵)) < 𝑧) → (abs‘((𝑢𝐹𝑣) − (𝐴𝐹𝐵))) < 𝑥))    &   ((𝜑𝑘𝑍) → (𝐺𝑘) ∈ 𝐶)    &   ((𝜑𝑘𝑍) → (𝐻𝑘) ∈ 𝐷)    &   ((𝜑𝑘𝑍) → (𝐾𝑘) = ((𝐺𝑘)𝐹(𝐻𝑘)))       (𝜑𝐾 ⇝ (𝐴𝐹𝐵))
 
Theoremaddcn2 9804* Complex number addition is a continuous function. Part of Proposition 14-4.16 of [Gleason] p. 243. (We write out the definition directly because df-cn and df-cncf are not yet available to us. See addcn for the abbreviated version.) (Contributed by Mario Carneiro, 31-Jan-2014.)
((𝐴 ∈ ℝ+𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ∃𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑢 ∈ ℂ ∀𝑣 ∈ ℂ (((abs‘(𝑢𝐵)) < 𝑦 ∧ (abs‘(𝑣𝐶)) < 𝑧) → (abs‘((𝑢 + 𝑣) − (𝐵 + 𝐶))) < 𝐴))
 
Theoremsubcn2 9805* Complex number subtraction is a continuous function. Part of Proposition 14-4.16 of [Gleason] p. 243. (Contributed by Mario Carneiro, 31-Jan-2014.)
((𝐴 ∈ ℝ+𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ∃𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑢 ∈ ℂ ∀𝑣 ∈ ℂ (((abs‘(𝑢𝐵)) < 𝑦 ∧ (abs‘(𝑣𝐶)) < 𝑧) → (abs‘((𝑢𝑣) − (𝐵𝐶))) < 𝐴))
 
Theoremmulcn2 9806* Complex number multiplication is a continuous function. Part of Proposition 14-4.16 of [Gleason] p. 243. (Contributed by Mario Carneiro, 31-Jan-2014.)
((𝐴 ∈ ℝ+𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ∃𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑢 ∈ ℂ ∀𝑣 ∈ ℂ (((abs‘(𝑢𝐵)) < 𝑦 ∧ (abs‘(𝑣𝐶)) < 𝑧) → (abs‘((𝑢 · 𝑣) − (𝐵 · 𝐶))) < 𝐴))
 
Theoremcn1lem 9807* A sufficient condition for a function to be continuous. (Contributed by Mario Carneiro, 9-Feb-2014.)
𝐹:ℂ⟶ℂ    &   ((𝑧 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (abs‘((𝐹𝑧) − (𝐹𝐴))) ≤ (abs‘(𝑧𝐴)))       ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℝ+𝑧 ∈ ℂ ((abs‘(𝑧𝐴)) < 𝑦 → (abs‘((𝐹𝑧) − (𝐹𝐴))) < 𝑥))
 
Theoremabscn2 9808* The absolute value function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.)
((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℝ+𝑧 ∈ ℂ ((abs‘(𝑧𝐴)) < 𝑦 → (abs‘((abs‘𝑧) − (abs‘𝐴))) < 𝑥))
 
Theoremcjcn2 9809* The complex conjugate function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.)
((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℝ+𝑧 ∈ ℂ ((abs‘(𝑧𝐴)) < 𝑦 → (abs‘((∗‘𝑧) − (∗‘𝐴))) < 𝑥))
 
Theoremrecn2 9810* The real part function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.)
((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℝ+𝑧 ∈ ℂ ((abs‘(𝑧𝐴)) < 𝑦 → (abs‘((ℜ‘𝑧) − (ℜ‘𝐴))) < 𝑥))
 
Theoremimcn2 9811* The imaginary part function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.)
((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℝ+𝑧 ∈ ℂ ((abs‘(𝑧𝐴)) < 𝑦 → (abs‘((ℑ‘𝑧) − (ℑ‘𝐴))) < 𝑥))
 
Theoremclimcn1lem 9812* The limit of a continuous function, theorem form. (Contributed by Mario Carneiro, 9-Feb-2014.)
𝑍 = (ℤ𝑀)    &   (𝜑𝐹𝐴)    &   (𝜑𝐺𝑊)    &   (𝜑𝑀 ∈ ℤ)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℂ)    &   𝐻:ℂ⟶ℂ    &   ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℝ+𝑧 ∈ ℂ ((abs‘(𝑧𝐴)) < 𝑦 → (abs‘((𝐻𝑧) − (𝐻𝐴))) < 𝑥))    &   ((𝜑𝑘𝑍) → (𝐺𝑘) = (𝐻‘(𝐹𝑘)))       (𝜑𝐺 ⇝ (𝐻𝐴))
 
Theoremclimabs 9813* Limit of the absolute value of a sequence. Proposition 12-2.4(c) of [Gleason] p. 172. (Contributed by NM, 7-Jun-2006.) (Revised by Mario Carneiro, 9-Feb-2014.)
𝑍 = (ℤ𝑀)    &   (𝜑𝐹𝐴)    &   (𝜑𝐺𝑊)    &   (𝜑𝑀 ∈ ℤ)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℂ)    &   ((𝜑𝑘𝑍) → (𝐺𝑘) = (abs‘(𝐹𝑘)))       (𝜑𝐺 ⇝ (abs‘𝐴))
 
Theoremclimcj 9814* Limit of the complex conjugate of a sequence. Proposition 12-2.4(c) of [Gleason] p. 172. (Contributed by NM, 7-Jun-2006.) (Revised by Mario Carneiro, 9-Feb-2014.)
𝑍 = (ℤ𝑀)    &   (𝜑𝐹𝐴)    &   (𝜑𝐺𝑊)    &   (𝜑𝑀 ∈ ℤ)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℂ)    &   ((𝜑𝑘𝑍) → (𝐺𝑘) = (∗‘(𝐹𝑘)))       (𝜑𝐺 ⇝ (∗‘𝐴))
 
Theoremclimre 9815* Limit of the real part of a sequence. Proposition 12-2.4(c) of [Gleason] p. 172. (Contributed by NM, 7-Jun-2006.) (Revised by Mario Carneiro, 9-Feb-2014.)
𝑍 = (ℤ𝑀)    &   (𝜑𝐹𝐴)    &   (𝜑𝐺𝑊)    &   (𝜑𝑀 ∈ ℤ)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℂ)    &   ((𝜑𝑘𝑍) → (𝐺𝑘) = (ℜ‘(𝐹𝑘)))       (𝜑𝐺 ⇝ (ℜ‘𝐴))
 
Theoremclimim 9816* Limit of the imaginary part of a sequence. Proposition 12-2.4(c) of [Gleason] p. 172. (Contributed by NM, 7-Jun-2006.) (Revised by Mario Carneiro, 9-Feb-2014.)
𝑍 = (ℤ𝑀)    &   (𝜑𝐹𝐴)    &   (𝜑𝐺𝑊)    &   (𝜑𝑀 ∈ ℤ)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℂ)    &   ((𝜑𝑘𝑍) → (𝐺𝑘) = (ℑ‘(𝐹𝑘)))       (𝜑𝐺 ⇝ (ℑ‘𝐴))
 
Theoremclimrecl 9817* The limit of a convergent real sequence is real. Corollary 12-2.5 of [Gleason] p. 172. (Contributed by NM, 10-Sep-2005.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝐹𝐴)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℝ)       (𝜑𝐴 ∈ ℝ)
 
Theoremclimge0 9818* A nonnegative sequence converges to a nonnegative number. (Contributed by NM, 11-Sep-2005.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝐹𝐴)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℝ)    &   ((𝜑𝑘𝑍) → 0 ≤ (𝐹𝑘))       (𝜑 → 0 ≤ 𝐴)
 
Theoremclimadd 9819* Limit of the sum of two converging sequences. Proposition 12-2.1(a) of [Gleason] p. 168. (Contributed by NM, 24-Sep-2005.) (Proof shortened by Mario Carneiro, 31-Jan-2014.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝐹𝐴)    &   (𝜑𝐻𝑋)    &   (𝜑𝐺𝐵)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℂ)    &   ((𝜑𝑘𝑍) → (𝐺𝑘) ∈ ℂ)    &   ((𝜑𝑘𝑍) → (𝐻𝑘) = ((𝐹𝑘) + (𝐺𝑘)))       (𝜑𝐻 ⇝ (𝐴 + 𝐵))
 
Theoremclimmul 9820* Limit of the product of two converging sequences. Proposition 12-2.1(c) of [Gleason] p. 168. (Contributed by NM, 27-Dec-2005.) (Proof shortened by Mario Carneiro, 1-Feb-2014.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝐹𝐴)    &   (𝜑𝐻𝑋)    &   (𝜑𝐺𝐵)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℂ)    &   ((𝜑𝑘𝑍) → (𝐺𝑘) ∈ ℂ)    &   ((𝜑𝑘𝑍) → (𝐻𝑘) = ((𝐹𝑘) · (𝐺𝑘)))       (𝜑𝐻 ⇝ (𝐴 · 𝐵))
 
Theoremclimsub 9821* Limit of the difference of two converging sequences. Proposition 12-2.1(b) of [Gleason] p. 168. (Contributed by NM, 4-Aug-2007.) (Proof shortened by Mario Carneiro, 1-Feb-2014.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝐹𝐴)    &   (𝜑𝐻𝑋)    &   (𝜑𝐺𝐵)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℂ)    &   ((𝜑𝑘𝑍) → (𝐺𝑘) ∈ ℂ)    &   ((𝜑𝑘𝑍) → (𝐻𝑘) = ((𝐹𝑘) − (𝐺𝑘)))       (𝜑𝐻 ⇝ (𝐴𝐵))
 
Theoremclimaddc1 9822* Limit of a constant 𝐶 added to each term of a sequence. (Contributed by NM, 24-Sep-2005.) (Revised by Mario Carneiro, 3-Feb-2014.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝐹𝐴)    &   (𝜑𝐶 ∈ ℂ)    &   (𝜑𝐺𝑊)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℂ)    &   ((𝜑𝑘𝑍) → (𝐺𝑘) = ((𝐹𝑘) + 𝐶))       (𝜑𝐺 ⇝ (𝐴 + 𝐶))
 
Theoremclimaddc2 9823* Limit of a constant 𝐶 added to each term of a sequence. (Contributed by NM, 24-Sep-2005.) (Revised by Mario Carneiro, 3-Feb-2014.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝐹𝐴)    &   (𝜑𝐶 ∈ ℂ)    &   (𝜑𝐺𝑊)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℂ)    &   ((𝜑𝑘𝑍) → (𝐺𝑘) = (𝐶 + (𝐹𝑘)))       (𝜑𝐺 ⇝ (𝐶 + 𝐴))
 
Theoremclimmulc2 9824* Limit of a sequence multiplied by a constant 𝐶. Corollary 12-2.2 of [Gleason] p. 171. (Contributed by NM, 24-Sep-2005.) (Revised by Mario Carneiro, 3-Feb-2014.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝐹𝐴)    &   (𝜑𝐶 ∈ ℂ)    &   (𝜑𝐺𝑊)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℂ)    &   ((𝜑𝑘𝑍) → (𝐺𝑘) = (𝐶 · (𝐹𝑘)))       (𝜑𝐺 ⇝ (𝐶 · 𝐴))
 
Theoremclimsubc1 9825* Limit of a constant 𝐶 subtracted from each term of a sequence. (Contributed by Mario Carneiro, 9-Feb-2014.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝐹𝐴)    &   (𝜑𝐶 ∈ ℂ)    &   (𝜑𝐺𝑊)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℂ)    &   ((𝜑𝑘𝑍) → (𝐺𝑘) = ((𝐹𝑘) − 𝐶))       (𝜑𝐺 ⇝ (𝐴𝐶))
 
Theoremclimsubc2 9826* Limit of a constant 𝐶 minus each term of a sequence. (Contributed by NM, 24-Sep-2005.) (Revised by Mario Carneiro, 9-Feb-2014.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝐹𝐴)    &   (𝜑𝐶 ∈ ℂ)    &   (𝜑𝐺𝑊)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℂ)    &   ((𝜑𝑘𝑍) → (𝐺𝑘) = (𝐶 − (𝐹𝑘)))       (𝜑𝐺 ⇝ (𝐶𝐴))
 
Theoremclimle 9827* Comparison of the limits of two sequences. (Contributed by Paul Chapman, 10-Sep-2007.) (Revised by Mario Carneiro, 1-Feb-2014.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝐹𝐴)    &   (𝜑𝐺𝐵)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℝ)    &   ((𝜑𝑘𝑍) → (𝐺𝑘) ∈ ℝ)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) ≤ (𝐺𝑘))       (𝜑𝐴𝐵)
 
Theoremclimsqz 9828* Convergence of a sequence sandwiched between another converging sequence and its limit. (Contributed by NM, 6-Feb-2008.) (Revised by Mario Carneiro, 3-Feb-2014.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝐹𝐴)    &   (𝜑𝐺𝑊)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℝ)    &   ((𝜑𝑘𝑍) → (𝐺𝑘) ∈ ℝ)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) ≤ (𝐺𝑘))    &   ((𝜑𝑘𝑍) → (𝐺𝑘) ≤ 𝐴)       (𝜑𝐺𝐴)
 
Theoremclimsqz2 9829* Convergence of a sequence sandwiched between another converging sequence and its limit. (Contributed by NM, 14-Feb-2008.) (Revised by Mario Carneiro, 3-Feb-2014.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝐹𝐴)    &   (𝜑𝐺𝑊)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℝ)    &   ((𝜑𝑘𝑍) → (𝐺𝑘) ∈ ℝ)    &   ((𝜑𝑘𝑍) → (𝐺𝑘) ≤ (𝐹𝑘))    &   ((𝜑𝑘𝑍) → 𝐴 ≤ (𝐺𝑘))       (𝜑𝐺𝐴)
 
Theoremclim2iser 9830* The limit of an infinite series with an initial segment removed. (Contributed by Jim Kingdon, 20-Aug-2021.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑁𝑍)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℂ)    &   (𝜑 → seq𝑀( + , 𝐹, ℂ) ⇝ 𝐴)       (𝜑 → seq(𝑁 + 1)( + , 𝐹, ℂ) ⇝ (𝐴 − (seq𝑀( + , 𝐹, ℂ)‘𝑁)))
 
Theoremclim2iser2 9831* The limit of an infinite series with an initial segment added. (Contributed by Jim Kingdon, 21-Aug-2021.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑁𝑍)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℂ)    &   (𝜑 → seq(𝑁 + 1)( + , 𝐹, ℂ) ⇝ 𝐴)       (𝜑 → seq𝑀( + , 𝐹, ℂ) ⇝ (𝐴 + (seq𝑀( + , 𝐹, ℂ)‘𝑁)))
 
Theoremiiserex 9832* An infinite series converges, if and only if the series does with initial terms removed. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Mario Carneiro, 27-Apr-2014.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑁𝑍)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℂ)       (𝜑 → (seq𝑀( + , 𝐹, ℂ) ∈ dom ⇝ ↔ seq𝑁( + , 𝐹, ℂ) ∈ dom ⇝ ))
 
Theoremiisermulc2 9833* Multiplication of an infinite series by a constant. (Contributed by Paul Chapman, 14-Nov-2007.) (Revised by Mario Carneiro, 1-Feb-2014.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝐶 ∈ ℂ)    &   (𝜑 → seq𝑀( + , 𝐹, ℂ) ⇝ 𝐴)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℂ)    &   ((𝜑𝑘𝑍) → (𝐺𝑘) = (𝐶 · (𝐹𝑘)))       (𝜑 → seq𝑀( + , 𝐺, ℂ) ⇝ (𝐶 · 𝐴))
 
Theoremclimlec2 9834* Comparison of a constant to the limit of a sequence. (Contributed by NM, 28-Feb-2008.) (Revised by Mario Carneiro, 1-Feb-2014.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝐴 ∈ ℝ)    &   (𝜑𝐹𝐵)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℝ)    &   ((𝜑𝑘𝑍) → 𝐴 ≤ (𝐹𝑘))       (𝜑𝐴𝐵)
 
Theoremiserile 9835* Comparison of the limits of two infinite series. (Contributed by Jim Kingdon, 22-Aug-2021.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑 → seq𝑀( + , 𝐹, ℂ) ⇝ 𝐴)    &   (𝜑 → seq𝑀( + , 𝐺, ℂ) ⇝ 𝐵)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℝ)    &   ((𝜑𝑘𝑍) → (𝐺𝑘) ∈ ℝ)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) ≤ (𝐺𝑘))       (𝜑𝐴𝐵)
 
Theoremiserige0 9836* The limit of an infinite series of nonnegative reals is nonnegative. (Contributed by Jim Kingdon, 22-Aug-2021.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑 → seq𝑀( + , 𝐹, ℂ) ⇝ 𝐴)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℝ)    &   ((𝜑𝑘𝑍) → 0 ≤ (𝐹𝑘))       (𝜑 → 0 ≤ 𝐴)
 
Theoremclimub 9837* The limit of a monotonic sequence is an upper bound. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 10-Feb-2014.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑁𝑍)    &   (𝜑𝐹𝐴)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℝ)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) ≤ (𝐹‘(𝑘 + 1)))       (𝜑 → (𝐹𝑁) ≤ 𝐴)
 
Theoremclimserile 9838* The partial sums of a converging infinite series with nonnegative terms are bounded by its limit. (Contributed by Jim Kingdon, 22-Aug-2021.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑁𝑍)    &   (𝜑 → seq𝑀( + , 𝐹, ℂ) ⇝ 𝐴)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℝ)    &   ((𝜑𝑘𝑍) → 0 ≤ (𝐹𝑘))       (𝜑 → (seq𝑀( + , 𝐹, ℂ)‘𝑁) ≤ 𝐴)
 
Theoremclimcau 9839* A converging sequence of complex numbers is a Cauchy sequence. The converse would require excluded middle or a different definition of Cauchy sequence (for example, fixing a rate of convergence as in climcvg1n 9842). Theorem 12-5.3 of [Gleason] p. 180 (necessity part). (Contributed by NM, 16-Apr-2005.) (Revised by Mario Carneiro, 26-Apr-2014.)
𝑍 = (ℤ𝑀)       ((𝑀 ∈ ℤ ∧ 𝐹 ∈ dom ⇝ ) → ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑥)
 
Theoremclimrecvg1n 9840* A Cauchy sequence of real numbers converges, existence version. The rate of convergence is fixed: all terms after the nth term must be within 𝐶 / 𝑛 of the nth term, where 𝐶 is a constant multiplier. (Contributed by Jim Kingdon, 23-Aug-2021.)
(𝜑𝐹:ℕ⟶ℝ)    &   (𝜑𝐶 ∈ ℝ+)    &   (𝜑 → ∀𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ𝑛)(abs‘((𝐹𝑘) − (𝐹𝑛))) < (𝐶 / 𝑛))       (𝜑𝐹 ∈ dom ⇝ )
 
Theoremclimcvg1nlem 9841* Lemma for climcvg1n 9842. We construct sequences of the real and imaginary parts of each term of 𝐹, show those converge, and use that to show that 𝐹 converges. (Contributed by Jim Kingdon, 24-Aug-2021.)
(𝜑𝐹:ℕ⟶ℂ)    &   (𝜑𝐶 ∈ ℝ+)    &   (𝜑 → ∀𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ𝑛)(abs‘((𝐹𝑘) − (𝐹𝑛))) < (𝐶 / 𝑛))    &   𝐺 = (𝑥 ∈ ℕ ↦ (ℜ‘(𝐹𝑥)))    &   𝐻 = (𝑥 ∈ ℕ ↦ (ℑ‘(𝐹𝑥)))    &   𝐽 = (𝑥 ∈ ℕ ↦ (i · (𝐻𝑥)))       (𝜑𝐹 ∈ dom ⇝ )
 
Theoremclimcvg1n 9842* A Cauchy sequence of complex numbers converges, existence version. The rate of convergence is fixed: all terms after the nth term must be within 𝐶 / 𝑛 of the nth term, where 𝐶 is a constant multiplier. (Contributed by Jim Kingdon, 23-Aug-2021.)
(𝜑𝐹:ℕ⟶ℂ)    &   (𝜑𝐶 ∈ ℝ+)    &   (𝜑 → ∀𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ𝑛)(abs‘((𝐹𝑘) − (𝐹𝑛))) < (𝐶 / 𝑛))       (𝜑𝐹 ∈ dom ⇝ )
 
Theoremclimcaucn 9843* A converging sequence of complex numbers is a Cauchy sequence. This is like climcau 9839 but adds the part that (𝐹𝑘) is complex. (Contributed by Jim Kingdon, 24-Aug-2021.)
𝑍 = (ℤ𝑀)       ((𝑀 ∈ ℤ ∧ 𝐹 ∈ dom ⇝ ) → ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)((𝐹𝑘) ∈ ℂ ∧ (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑥))
 
Theoremserif0 9844* If an infinite series converges, its underlying sequence converges to zero. (Contributed by NM, 2-Sep-2005.) (Revised by Mario Carneiro, 16-Feb-2014.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝐹𝑉)    &   (𝜑 → seq𝑀( + , 𝐹, ℂ) ∈ dom ⇝ )    &   ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℂ)       (𝜑𝐹 ⇝ 0)
 
3.8.2  Finite and infinite sums
 
Syntaxcsu 9845 Extend class notation to include finite summations. (An underscore was added to the ASCII token in order to facilitate set.mm text searches, since "sum" is a commonly used word in comments.)
class Σ𝑘𝐴 𝐵
 
Definitiondf-sum 9846* Define the sum of a series with an index set of integers 𝐴. 𝑘 is normally a free variable in 𝐵, i.e. 𝐵 can be thought of as 𝐵(𝑘). This definition is the result of a collection of discussions over the most general definition for a sum that does not need the index set to have a specified ordering. This definition is in two parts, one for finite sums and one for subsets of the upper integers. When summing over a subset of the upper integers, we extend the index set to the upper integers by adding zero outside the domain, and then sum the set in order, setting the result to the limit of the partial sums, if it exists. This means that conditionally convergent sums can be evaluated meaningfully. For finite sums, we are explicitly order-independent, by picking any bijection to a 1-based finite sequence and summing in the induced order. These two methods of summation produce the same result on their common region of definition (i.e. finite subsets of the upper integers). Examples: Σ𝑘 ∈ {1, 2, 4} 𝑘 means 1 + 2 + 4 = 7, and Σ𝑘 ∈ ℕ (1 / (2↑𝑘)) = 1 means 1/2 + 1/4 + 1/8 + ... = 1. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.)
Σ𝑘𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0)), ℂ) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵), ℂ)‘𝑚))))
 
Theoremsumeq1 9847 Equality theorem for a sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.)
(𝐴 = 𝐵 → Σ𝑘𝐴 𝐶 = Σ𝑘𝐵 𝐶)
 
Theoremnfsum1 9848 Bound-variable hypothesis builder for sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.)
𝑘𝐴       𝑘Σ𝑘𝐴 𝐵
 
Theoremnfsum 9849 Bound-variable hypothesis builder for sum: if 𝑥 is (effectively) not free in 𝐴 and 𝐵, it is not free in Σ𝑘𝐴𝐵. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.)
𝑥𝐴    &   𝑥𝐵       𝑥Σ𝑘𝐴 𝐵
 
PART 4  ELEMENTARY NUMBER THEORY

Here we introduce elementary number theory, in particular the elementary properties of divisibility and elementary prime number theory.

 
4.1  Elementary properties of divisibility
 
4.1.1  Rationality of square root of 2
 
Theoremsqr2irrlem 9850 Lemma concerning rationality of square root of 2. The core of the proof - if 𝐴 / 𝐵 = √(2), then 𝐴 and 𝐵 are even, so 𝐴 / 2 and 𝐵 / 2 are smaller representatives, which is absurd by the method of infinite descent (here implemented by strong induction). (Contributed by NM, 20-Aug-2001.) (Revised by Mario Carneiro, 12-Sep-2015.)
(𝜑𝐴 ∈ ℤ)    &   (𝜑𝐵 ∈ ℕ)    &   (𝜑 → (√‘2) = (𝐴 / 𝐵))       (𝜑 → ((𝐴 / 2) ∈ ℤ ∧ (𝐵 / 2) ∈ ℕ))
 
Theoremsqrt2irr 9851 The square root of 2 is not rational. That is, for any rational number, (√‘2) does not equal it. However, if we were to say "the square root of 2 is irrational" that would mean something stronger: "for any rational number, (√‘2) is apart from it" (the two statements are equivalent given excluded middle). We do not prove irrationality in this stronger sense here.

The proof's core is proven in sqr2irrlem 9850, which shows that if 𝐴 / 𝐵 = √(2), then 𝐴 and 𝐵 are even, so 𝐴 / 2 and 𝐵 / 2 are smaller representatives, which is absurd. (Contributed by NM, 8-Jan-2002.) (Proof shortened by Mario Carneiro, 12-Sep-2015.)

(√‘2) ∉ ℚ
 
Theoremsqrt2re 9852 The square root of 2 exists and is a real number. (Contributed by NM, 3-Dec-2004.)
(√‘2) ∈ ℝ
 
4.1.2  Algorithms
 
Theoremnn0seqcvgd 9853* A strictly-decreasing nonnegative integer sequence with initial term 𝑁 reaches zero by the 𝑁 th term. Deduction version. (Contributed by Paul Chapman, 31-Mar-2011.)
(𝜑𝐹:ℕ0⟶ℕ0)    &   (𝜑𝑁 = (𝐹‘0))    &   ((𝜑𝑘 ∈ ℕ0) → ((𝐹‘(𝑘 + 1)) ≠ 0 → (𝐹‘(𝑘 + 1)) < (𝐹𝑘)))       (𝜑 → (𝐹𝑁) = 0)
 
Theoremialgrlem1st 9854 Lemma for ialgr0 9856. Expressing algrflemg 5851 in a form suitable for theorems such as iseq1 9196 or iseqfn 9195. (Contributed by Jim Kingdon, 22-Jul-2021.)
(𝜑𝐹:𝑆𝑆)       ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥(𝐹 ∘ 1st )𝑦) ∈ 𝑆)
 
Theoremialgrlemconst 9855 Lemma for ialgr0 9856. Closure of a constant function, in a form suitable for theorems such as iseq1 9196 or iseqfn 9195. (Contributed by Jim Kingdon, 22-Jul-2021.)
𝑍 = (ℤ𝑀)    &   (𝜑𝐴𝑆)       ((𝜑𝑥 ∈ (ℤ𝑀)) → ((𝑍 × {𝐴})‘𝑥) ∈ 𝑆)
 
Theoremialgr0 9856 The value of the algorithm iterator 𝑅 at 0 is the initial state 𝐴. (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Mario Carneiro, 28-May-2014.)
𝑍 = (ℤ𝑀)    &   𝑅 = seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}), 𝑆)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝐴𝑆)    &   (𝜑𝐹:𝑆𝑆)    &   (𝜑𝑆𝑉)       (𝜑 → (𝑅𝑀) = 𝐴)
 
Theoremialgrf 9857 An algorithm is a step function 𝐹:𝑆𝑆 on a state space 𝑆. An algorithm acts on an initial state 𝐴𝑆 by iteratively applying 𝐹 to give 𝐴, (𝐹𝐴), (𝐹‘(𝐹𝐴)) and so on. An algorithm is said to halt if a fixed point of 𝐹 is reached after a finite number of iterations.

The algorithm iterator 𝑅:ℕ0𝑆 "runs" the algorithm 𝐹 so that (𝑅𝑘) is the state after 𝑘 iterations of 𝐹 on the initial state 𝐴.

Domain and codomain of the algorithm iterator 𝑅. (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Mario Carneiro, 28-May-2014.)

𝑍 = (ℤ𝑀)    &   𝑅 = seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}), 𝑆)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝐴𝑆)    &   (𝜑𝐹:𝑆𝑆)    &   (𝜑𝑆𝑉)       (𝜑𝑅:𝑍𝑆)
 
Theoremialgrp1 9858 The value of the algorithm iterator 𝑅 at (𝐾 + 1). (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Mario Carneiro, 27-Dec-2014.)
𝑍 = (ℤ𝑀)    &   𝑅 = seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}), 𝑆)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝐴𝑆)    &   (𝜑𝐹:𝑆𝑆)    &   (𝜑𝑆𝑉)       ((𝜑𝐾𝑍) → (𝑅‘(𝐾 + 1)) = (𝐹‘(𝑅𝐾)))
 
Theoremialginv 9859* If 𝐼 is an invariant of 𝐹, its value is unchanged after any number of iterations of 𝐹. (Contributed by Paul Chapman, 31-Mar-2011.)
𝑅 = seq0((𝐹 ∘ 1st ), (ℕ0 × {𝐴}), 𝑆)    &   𝐹:𝑆𝑆    &   𝐼 Fn 𝑆    &   (𝑥𝑆 → (𝐼‘(𝐹𝑥)) = (𝐼𝑥))    &   𝑆𝑉       ((𝐴𝑆𝐾 ∈ ℕ0) → (𝐼‘(𝑅𝐾)) = (𝐼‘(𝑅‘0)))
 
Theoremialgcvg 9860* One way to prove that an algorithm halts is to construct a countdown function 𝐶:𝑆⟶ℕ0 whose value is guaranteed to decrease for each iteration of 𝐹 until it reaches 0. That is, if 𝑋𝑆 is not a fixed point of 𝐹, then (𝐶‘(𝐹𝑋)) < (𝐶𝑋).

If 𝐶 is a countdown function for algorithm 𝐹, the sequence (𝐶‘(𝑅𝑘)) reaches 0 after at most 𝑁 steps, where 𝑁 is the value of 𝐶 for the initial state 𝐴. (Contributed by Paul Chapman, 22-Jun-2011.)

𝐹:𝑆𝑆    &   𝑅 = seq0((𝐹 ∘ 1st ), (ℕ0 × {𝐴}), 𝑆)    &   𝐶:𝑆⟶ℕ0    &   (𝑧𝑆 → ((𝐶‘(𝐹𝑧)) ≠ 0 → (𝐶‘(𝐹𝑧)) < (𝐶𝑧)))    &   𝑁 = (𝐶𝐴)    &   𝑆𝑉       (𝐴𝑆 → (𝐶‘(𝑅𝑁)) = 0)
 
Theoremalgcvgblem 9861 Lemma for algcvgb 9862. (Contributed by Paul Chapman, 31-Mar-2011.)
((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → ((𝑁 ≠ 0 → 𝑁 < 𝑀) ↔ ((𝑀 ≠ 0 → 𝑁 < 𝑀) ∧ (𝑀 = 0 → 𝑁 = 0))))
 
Theoremalgcvgb 9862 Two ways of expressing that 𝐶 is a countdown function for algorithm 𝐹. The first is used in these theorems. The second states the condition more intuitively as a conjunction: if the countdown function's value is currently nonzero, it must decrease at the next step; if it has reached zero, it must remain zero at the next step. (Contributed by Paul Chapman, 31-Mar-2011.)
𝐹:𝑆𝑆    &   𝐶:𝑆⟶ℕ0       (𝑋𝑆 → (((𝐶‘(𝐹𝑋)) ≠ 0 → (𝐶‘(𝐹𝑋)) < (𝐶𝑋)) ↔ (((𝐶𝑋) ≠ 0 → (𝐶‘(𝐹𝑋)) < (𝐶𝑋)) ∧ ((𝐶𝑋) = 0 → (𝐶‘(𝐹𝑋)) = 0))))
 
Theoremialgcvga 9863* The countdown function 𝐶 remains 0 after 𝑁 steps. (Contributed by Paul Chapman, 22-Jun-2011.)
𝐹:𝑆𝑆    &   𝑅 = seq0((𝐹 ∘ 1st ), (ℕ0 × {𝐴}), 𝑆)    &   𝐶:𝑆⟶ℕ0    &   (𝑧𝑆 → ((𝐶‘(𝐹𝑧)) ≠ 0 → (𝐶‘(𝐹𝑧)) < (𝐶𝑧)))    &   𝑁 = (𝐶𝐴)    &   𝑆𝑉       (𝐴𝑆 → (𝐾 ∈ (ℤ𝑁) → (𝐶‘(𝑅𝐾)) = 0))
 
Theoremialgfx 9864* If 𝐹 reaches a fixed point when the countdown function 𝐶 reaches 0, 𝐹 remains fixed after 𝑁 steps. (Contributed by Paul Chapman, 22-Jun-2011.)
𝐹:𝑆𝑆    &   𝑅 = seq0((𝐹 ∘ 1st ), (ℕ0 × {𝐴}), 𝑆)    &   𝐶:𝑆⟶ℕ0    &   (𝑧𝑆 → ((𝐶‘(𝐹𝑧)) ≠ 0 → (𝐶‘(𝐹𝑧)) < (𝐶𝑧)))    &   𝑁 = (𝐶𝐴)    &   𝑆𝑉    &   (𝑧𝑆 → ((𝐶𝑧) = 0 → (𝐹𝑧) = 𝑧))       (𝐴𝑆 → (𝐾 ∈ (ℤ𝑁) → (𝑅𝐾) = (𝑅𝑁)))
 
PART 5  GUIDES AND MISCELLANEA
 
5.1  Guides (conventions, explanations, and examples)
 
5.1.1  Conventions

This section describes the conventions we use. However, these conventions often refer to existing mathematical practices, which are discussed in more detail in other references. The following sources lay out how mathematics is developed without the law of the excluded middle. Of course, there are a greater number of sources which assume excluded middle and most of what is in them applies here too (especially in a treatment such as ours which is built on first order logic and set theory, rather than, say, type theory). Studying how a topic is treated in the Metamath Proof Explorer and the references therein is often a good place to start (and is easy to compare with the Intuitionistic Logic Explorer). The textbooks provide a motivation for what we are doing, whereas Metamath lets you see in detail all hidden and implicit steps. Most standard theorems are accompanied by citations. Some closely followed texts include the following:

  • Axioms of propositional calculus - Stanford Encyclopedia of Philosophy or [Heyting].
  • Axioms of predicate calculus - our axioms are adapted from the ones in the Metamath Proof Explorer.
  • Theorems of propositional calculus - [Heyting].
  • Theorems of pure predicate calculus - Metamath Proof Explorer.
  • Theorems of equality and substitution - Metamath Proof Explorer.
  • Axioms of set theory - [Crosilla].
  • Development of set theory - Chapter 10 of [HoTT].
  • Construction of real and complex numbers - Chapter 11 of [HoTT]; [BauerTaylor].
  • Theorems about real numbers - [Geuvers].
 
Theoremconventions 9865 Unless there is a reason to diverge, we follow the conventions of the Metamath Proof Explorer (aka "set.mm"). This list of conventions is intended to be read in conjunction with the corresponding conventions in the Metamath Proof Explorer, and only the differences are described below.

  • Minimizing axioms and the axiom of choice. We prefer proofs that depend on fewer and/or weaker axioms, even if the proofs are longer. In particular, our choice of IZF (Intuitionistic Zermelo-Fraenkel) over CZF (Constructive Zermelo-Fraenkel, a weaker system) was just an expedient choice because IZF is easier to formalize in metamath. You can find some development using CZF in BJ's mathbox starting at ax-bd0 9906 (and the section header just above it). As for the axiom of choice, the full axiom of choice implies excluded middle as seen at acexmid 5511, although some authors will use countable choice or dependent choice. For example, countable choice or excluded middle is needed to show that the Cauchy reals coincide with the Dedekind reals - Corollary 11.4.3 of [HoTT], p. (varies).
  • Junk/undefined results. Much of the discussion of this topic in the Metamath Proof Explorer applies except that certain techniques are not available to us. For example, the Metamath Proof Explorer will often say "if a function is evaluated within its domain, a certain result follows; if the function is evaluated outside its domain, the same result follows. Since the function must be evaluated within its domain or outside it, the result follows unconditionally" (the use of excluded middle in this argument is perhaps obvious when stated this way). For this reason, we generally need to prove we are evaluating functions within their domains and avoid the reverse closure theorems of the Metamath Proof Explorer.
  • Bibliography references. The bibliography for the Intuitionistic Logic Explorer is separate from the one for the Metamath Proof Explorer but feel free to copy-paste a citation in either direction in order to cite it.

Label naming conventions

Here are a few of the label naming conventions:

  • Suffixes. We follow the conventions of the Metamath Proof Explorer with a few additions. A biconditional in set.mm which is an implication in iset.mm should have a "r" (for the reverse direction), or "i"/"im" (for the forward direction) appended. A theorem in set.mm which has a decidability condition added should add "dc" to the theorem name. A theorem in set.mm where "nonempty class" is changed to "inhabited class" should add "m" (for member) to the theorem name.

The following table shows some commonly-used abbreviations in labels which are not found in the Metamath Proof Explorer, in alphabetical order. For each abbreviation we provide a mnenomic to help you remember it, the source theorem/assumption defining it, an expression showing what it looks like, whether or not it is a "syntax fragment" (an abbreviation that indicates a particular kind of syntax), and hyperlinks to label examples that use the abbreviation. The abbreviation is bolded if there is a df-NAME definition but the label fragment is not NAME.

AbbreviationMnenomicSource ExpressionSyntax?Example(s)
apapart df-ap 7571 Yes apadd1 7597, apne 7612

  • Community. The Metamath mailing list also covers the Intuitionistic Logic Explorer and is at: https://groups.google.com/forum/#!forum/metamath.
  • (Contributed by Jim Kingdon, 24-Feb-2020.)

    𝜑       𝜑
     
    5.1.2  Definitional examples
     
    Theoremex-or 9866 Example for ax-io 630. Example by David A. Wheeler. (Contributed by Mario Carneiro, 9-May-2015.)
    (2 = 3 ∨ 4 = 4)
     
    Theoremex-an 9867 Example for ax-ia1 99. Example by David A. Wheeler. (Contributed by Mario Carneiro, 9-May-2015.)
    (2 = 2 ∧ 3 = 3)
     
    Theoremex-fl 9868 Example for df-fl 9112. Example by David A. Wheeler. (Contributed by Mario Carneiro, 18-Jun-2015.)
    ((⌊‘(3 / 2)) = 1 ∧ (⌊‘-(3 / 2)) = -2)
     
    Theoremex-ceil 9869 Example for df-ceil 9113. (Contributed by AV, 4-Sep-2021.)
    ((⌈‘(3 / 2)) = 2 ∧ (⌈‘-(3 / 2)) = -1)
     
    PART 6  SUPPLEMENTARY MATERIAL (USER'S MATHBOXES)
     
    6.1  Mathboxes for user contributions
     
    6.1.1  Mathbox guidelines
     
    Theoremmathbox 9870 (This theorem is a dummy placeholder for these guidelines. The name of this theorem, "mathbox", is hard-coded into the Metamath program to identify the start of the mathbox section for web page generation.)

    A "mathbox" is a user-contributed section that is maintained by its contributor independently from the main part of set.mm.

    For contributors:

    By making a contribution, you agree to release it into the public domain, according to the statement at the beginning of set.mm.

    Mathboxes are provided to help keep your work synchronized with changes in set.mm, but they shouldn't be depended on as a permanent archive. If you want to preserve your original contribution, it is your responsibility to keep your own copy of it along with the version of set.mm that works with it.

    Guidelines:

    1. If at all possible, please use only 0-ary class constants for new definitions.

    2. Try to follow the style of the rest of set.mm. Each $p and $a statement must be immediately preceded with the comment that will be shown on its web page description. The metamath program command "write source set.mm /rewrap" will take care of wrapping comment lines and indentation conventions. All mathbox content will be on public display and should hopefully reflect the overall quality of the website.

    3. Before submitting a revised mathbox, please make sure it verifies against the current set.mm.

    4. Mathboxes should be independent i.e. the proofs should verify with all other mathboxes removed. If you need a theorem from another mathbox, that is fine (and encouraged), but let me know, so I can move the theorem to the main section. One way avoid undesired accidental use of other mathbox theorems is to develop your mathbox using a modified set.mm that has mathboxes removed.

    Notes:

    1. We may decide to move some theorems to the main part of set.mm for general use.

    2. We may make changes to mathboxes to maintain the overall quality of set.mm. Normally we will let you know if a change might impact what you are working on.

    3. If you use theorems from another user's mathbox, we don't provide assurance that they are based on correct or consistent $a statements. (If you find such a problem, please let us know so it can be corrected.) (Contributed by NM, 20-Feb-2007.) (New usage is discouraged.)

    𝜑       𝜑
     
    6.2  Mathbox for Mykola Mostovenko
     
    Theoremax1hfs 9871 Heyting's formal system Axiom #1 from [Heyting] p. 127. (Contributed by MM, 11-Aug-2018.)
    (𝜑 → (𝜑𝜑))
     
    6.3  Mathbox for BJ
     
    6.3.1  Propositional calculus
     
    Theoremnnexmid 9872 Double negation of excluded middle. Intuitionistic logic refutes the negation of excluded middle (but, of course, does not prove excluded middle) for any formula. (Contributed by BJ, 9-Oct-2019.)
    ¬ ¬ (𝜑 ∨ ¬ 𝜑)
     
    Theoremnndc 9873 Double negation of decidability of a formula. Intuitionistic logic refutes undecidability (but, of course, does not prove decidability) of any formula. (Contributed by BJ, 9-Oct-2019.)
    ¬ ¬ DECID 𝜑
     
    Theoremdcdc 9874 Decidability of a proposition is decidable if and only if that proposition is decidable. DECID is idempotent. (Contributed by BJ, 9-Oct-2019.)
    (DECID DECID 𝜑DECID 𝜑)
     
    6.3.2  Predicate calculus
     
    Theorembj-ex 9875* Existential generalization. (Contributed by BJ, 8-Dec-2019.) Proof modification is discouraged because there are shorter proofs, but using less basic results (like exlimiv 1489 and 19.9ht 1532 or 19.23ht 1386). (Proof modification is discouraged.)
    (∃𝑥𝜑𝜑)
     
    Theorembj-hbalt 9876 Closed form of hbal 1366 (copied from set.mm). (Contributed by BJ, 2-May-2019.)
    (∀𝑦(𝜑 → ∀𝑥𝜑) → (∀𝑦𝜑 → ∀𝑥𝑦𝜑))
     
    Theorembj-nfalt 9877 Closed form of nfal 1468 (copied from set.mm). (Contributed by BJ, 2-May-2019.)
    (∀𝑥𝑦𝜑 → Ⅎ𝑦𝑥𝜑)
     
    Theoremspimd 9878 Deduction form of spim 1626. (Contributed by BJ, 17-Oct-2019.)
    (𝜑 → Ⅎ𝑥𝜒)    &   (𝜑 → ∀𝑥(𝑥 = 𝑦 → (𝜓𝜒)))       (𝜑 → (∀𝑥𝜓𝜒))
     
    Theorem2spim 9879* Double substitution, as in spim 1626. (Contributed by BJ, 17-Oct-2019.)
    𝑥𝜒    &   𝑧𝜒    &   ((𝑥 = 𝑦𝑧 = 𝑡) → (𝜓𝜒))       (∀𝑧𝑥𝜓𝜒)
     
    Theoremch2var 9880* Implicit substitution of 𝑦 for 𝑥 and 𝑡 for 𝑧 into a theorem. (Contributed by BJ, 17-Oct-2019.)
    𝑥𝜓    &   𝑧𝜓    &   ((𝑥 = 𝑦𝑧 = 𝑡) → (𝜑𝜓))    &   𝜑       𝜓
     
    Theoremch2varv 9881* Version of ch2var 9880 with non-freeness hypotheses replaced by DV conditions. (Contributed by BJ, 17-Oct-2019.)
    ((𝑥 = 𝑦𝑧 = 𝑡) → (𝜑𝜓))    &   𝜑       𝜓
     
    Theorembj-exlimmp 9882 Lemma for bj-vtoclgf 9888. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.)
    𝑥𝜓    &   (𝜒𝜑)       (∀𝑥(𝜒 → (𝜑𝜓)) → (∃𝑥𝜒𝜓))
     
    Theorembj-exlimmpi 9883 Lemma for bj-vtoclgf 9888. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.)
    𝑥𝜓    &   (𝜒𝜑)    &   (𝜒 → (𝜑𝜓))       (∃𝑥𝜒𝜓)
     
    Theorembj-sbimedh 9884 A strengthening of sbiedh 1670 (same proof). (Contributed by BJ, 16-Dec-2019.)
    (𝜑 → ∀𝑥𝜑)    &   (𝜑 → (𝜒 → ∀𝑥𝜒))    &   (𝜑 → (𝑥 = 𝑦 → (𝜓𝜒)))       (𝜑 → ([𝑦 / 𝑥]𝜓𝜒))
     
    Theorembj-sbimeh 9885 A strengthening of sbieh 1673 (same proof). (Contributed by BJ, 16-Dec-2019.)
    (𝜓 → ∀𝑥𝜓)    &   (𝑥 = 𝑦 → (𝜑𝜓))       ([𝑦 / 𝑥]𝜑𝜓)
     
    Theorembj-sbime 9886 A strengthening of sbie 1674 (same proof). (Contributed by BJ, 16-Dec-2019.)
    𝑥𝜓    &   (𝑥 = 𝑦 → (𝜑𝜓))       ([𝑦 / 𝑥]𝜑𝜓)
     
    6.3.3  Extensionality

    Various utility theorems using FOL and extensionality.

     
    Theorembj-vtoclgft 9887 Weakening two hypotheses of vtoclgf 2612. (Contributed by BJ, 21-Nov-2019.)
    𝑥𝐴    &   𝑥𝜓    &   (𝑥 = 𝐴𝜑)       (∀𝑥(𝑥 = 𝐴 → (𝜑𝜓)) → (𝐴𝑉𝜓))
     
    Theorembj-vtoclgf 9888 Weakening two hypotheses of vtoclgf 2612. (Contributed by BJ, 21-Nov-2019.)
    𝑥𝐴    &   𝑥𝜓    &   (𝑥 = 𝐴𝜑)    &   (𝑥 = 𝐴 → (𝜑𝜓))       (𝐴𝑉𝜓)
     
    Theoremelabgf0 9889 Lemma for elabgf 2685. (Contributed by BJ, 21-Nov-2019.)
    (𝑥 = 𝐴 → (𝐴 ∈ {𝑥𝜑} ↔ 𝜑))
     
    Theoremelabgft1 9890 One implication of elabgf 2685, in closed form. (Contributed by BJ, 21-Nov-2019.)
    𝑥𝐴    &   𝑥𝜓       (∀𝑥(𝑥 = 𝐴 → (𝜑𝜓)) → (𝐴 ∈ {𝑥𝜑} → 𝜓))
     
    Theoremelabgf1 9891 One implication of elabgf 2685. (Contributed by BJ, 21-Nov-2019.)
    𝑥𝐴    &   𝑥𝜓    &   (𝑥 = 𝐴 → (𝜑𝜓))       (𝐴 ∈ {𝑥𝜑} → 𝜓)
     
    Theoremelabgf2 9892 One implication of elabgf 2685. (Contributed by BJ, 21-Nov-2019.)
    𝑥𝐴    &   𝑥𝜓    &   (𝑥 = 𝐴 → (𝜓𝜑))       (𝐴𝐵 → (𝜓𝐴 ∈ {𝑥𝜑}))
     
    Theoremelabf1 9893* One implication of elabf 2686. (Contributed by BJ, 21-Nov-2019.)
    𝑥𝜓    &   (𝑥 = 𝐴 → (𝜑𝜓))       (𝐴 ∈ {𝑥𝜑} → 𝜓)
     
    Theoremelabf2 9894* One implication of elabf 2686. (Contributed by BJ, 21-Nov-2019.)
    𝑥𝜓    &   𝐴 ∈ V    &   (𝑥 = 𝐴 → (𝜓𝜑))       (𝜓𝐴 ∈ {𝑥𝜑})
     
    Theoremelab1 9895* One implication of elab 2687. (Contributed by BJ, 21-Nov-2019.)
    (𝑥 = 𝐴 → (𝜑𝜓))       (𝐴 ∈ {𝑥𝜑} → 𝜓)
     
    Theoremelab2a 9896* One implication of elab 2687. (Contributed by BJ, 21-Nov-2019.)
    𝐴 ∈ V    &   (𝑥 = 𝐴 → (𝜓𝜑))       (𝜓𝐴 ∈ {𝑥𝜑})
     
    Theoremelabg2 9897* One implication of elabg 2688. (Contributed by BJ, 21-Nov-2019.)
    (𝑥 = 𝐴 → (𝜓𝜑))       (𝐴𝑉 → (𝜓𝐴 ∈ {𝑥𝜑}))
     
    Theorembj-rspgt 9898 Restricted specialization, generalized. Weakens a hypothesis of rspccv 2653 and seems to have a shorter proof. (Contributed by BJ, 21-Nov-2019.)
    𝑥𝐴    &   𝑥𝐵    &   𝑥𝜓       (∀𝑥(𝑥 = 𝐴 → (𝜑𝜓)) → (∀𝑥𝐵 𝜑 → (𝐴𝐵𝜓)))
     
    Theorembj-rspg 9899 Restricted specialization, generalized. Weakens a hypothesis of rspccv 2653 and seems to have a shorter proof. (Contributed by BJ, 21-Nov-2019.)
    𝑥𝐴    &   𝑥𝐵    &   𝑥𝜓    &   (𝑥 = 𝐴 → (𝜑𝜓))       (∀𝑥𝐵 𝜑 → (𝐴𝐵𝜓))
     
    Theoremcbvrald 9900* Rule used to change bound variables, using implicit substitution. (Contributed by BJ, 22-Nov-2019.)
    𝑥𝜑    &   𝑦𝜑    &   (𝜑 → Ⅎ𝑦𝜓)    &   (𝜑 → Ⅎ𝑥𝜒)    &   (𝜑 → (𝑥 = 𝑦 → (𝜓𝜒)))       (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑦𝐴 𝜒))
        < Previous  Next >

    Page List
    Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10095
      Copyright terms: Public domain < Previous  Next >