Home Intuitionistic Logic ExplorerTheorem List (p. 101 of 105) < 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 - 10001-10100   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremclim0c 10001* Express the predicate 𝐹 converges to 0. (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝐹𝑉)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) = 𝐵)    &   ((𝜑𝑘𝑍) → 𝐵 ∈ ℂ)       (𝜑 → (𝐹 ⇝ 0 ↔ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘𝐵) < 𝑥))

Theoremclimi 10002* Convergence of a sequence of complex numbers. (Contributed by NM, 11-Jan-2007.) (Revised by Mario Carneiro, 31-Jan-2014.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝐶 ∈ ℝ+)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) = 𝐵)    &   (𝜑𝐹𝐴)       (𝜑 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐵 ∈ ℂ ∧ (abs‘(𝐵𝐴)) < 𝐶))

Theoremclimi2 10003* Convergence of a sequence of complex numbers. (Contributed by NM, 11-Jan-2007.) (Revised by Mario Carneiro, 31-Jan-2014.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝐶 ∈ ℝ+)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) = 𝐵)    &   (𝜑𝐹𝐴)       (𝜑 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘(𝐵𝐴)) < 𝐶)

Theoremclimi0 10004* Convergence of a sequence of complex numbers to zero. (Contributed by NM, 11-Jan-2007.) (Revised by Mario Carneiro, 31-Jan-2014.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝐶 ∈ ℝ+)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) = 𝐵)    &   (𝜑𝐹 ⇝ 0)       (𝜑 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘𝐵) < 𝐶)

Theoremclimconst 10005* An (eventually) constant sequence converges to its value. (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 31-Jan-2014.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝐹𝑉)    &   (𝜑𝐴 ∈ ℂ)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) = 𝐴)       (𝜑𝐹𝐴)

Theoremclimconst2 10006 A constant sequence converges to its value. (Contributed by NM, 6-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)
(ℤ𝑀) ⊆ 𝑍    &   𝑍 ∈ V       ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℤ) → (𝑍 × {𝐴}) ⇝ 𝐴)

Theoremclimz 10007 The zero sequence converges to zero. (Contributed by NM, 2-Oct-1999.) (Revised by Mario Carneiro, 31-Jan-2014.)
(ℤ × {0}) ⇝ 0

Theoremclimuni 10008 An infinite sequence of complex numbers converges to at most one limit. (Contributed by NM, 2-Oct-1999.) (Proof shortened by Mario Carneiro, 31-Jan-2014.)
((𝐹𝐴𝐹𝐵) → 𝐴 = 𝐵)

Theoremfclim 10009 The limit relation is function-like, and with range the complex numbers. (Contributed by Mario Carneiro, 31-Jan-2014.)
⇝ :dom ⇝ ⟶ℂ

Theoremclimdm 10010 Two ways to express that a function has a limit. (The expression ( ⇝ ‘𝐹) is sometimes useful as a shorthand for "the unique limit of the function 𝐹"). (Contributed by Mario Carneiro, 18-Mar-2014.)
(𝐹 ∈ dom ⇝ ↔ 𝐹 ⇝ ( ⇝ ‘𝐹))

Theoremclimeu 10011* An infinite sequence of complex numbers converges to at most one limit. (Contributed by NM, 25-Dec-2005.)
(𝐹𝐴 → ∃!𝑥 𝐹𝑥)

Theoremclimreu 10012* An infinite sequence of complex numbers converges to at most one limit. (Contributed by NM, 25-Dec-2005.)
(𝐹𝐴 → ∃!𝑥 ∈ ℂ 𝐹𝑥)

Theoremclimmo 10013* An infinite sequence of complex numbers converges to at most one limit. (Contributed by Mario Carneiro, 13-Jul-2013.)
∃*𝑥 𝐹𝑥

Theoremclimeq 10014* Two functions that are eventually equal to one another have the same limit. (Contributed by Mario Carneiro, 5-Nov-2013.) (Revised by Mario Carneiro, 31-Jan-2014.)
𝑍 = (ℤ𝑀)    &   (𝜑𝐹𝑉)    &   (𝜑𝐺𝑊)    &   (𝜑𝑀 ∈ ℤ)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) = (𝐺𝑘))       (𝜑 → (𝐹𝐴𝐺𝐴))

Theoremclimmpt 10015* Exhibit a function 𝐺 with the same convergence properties as the not-quite-function 𝐹. (Contributed by Mario Carneiro, 31-Jan-2014.)
𝑍 = (ℤ𝑀)    &   𝐺 = (𝑘𝑍 ↦ (𝐹𝑘))       ((𝑀 ∈ ℤ ∧ 𝐹𝑉) → (𝐹𝐴𝐺𝐴))

Theorem2clim 10016* If two sequences converge to each other, they converge to the same limit. (Contributed by NM, 24-Dec-2005.) (Proof shortened by Mario Carneiro, 31-Jan-2014.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝐺𝑉)    &   ((𝜑𝑘𝑍) → (𝐺𝑘) ∈ ℂ)    &   (𝜑 → ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘((𝐹𝑘) − (𝐺𝑘))) < 𝑥)    &   (𝜑𝐹𝐴)       (𝜑𝐺𝐴)

Theoremclimshftlemg 10017 A shifted function converges if the original function converges. (Contributed by Mario Carneiro, 5-Nov-2013.)
((𝑀 ∈ ℤ ∧ 𝐹𝑉) → (𝐹𝐴 → (𝐹 shift 𝑀) ⇝ 𝐴))

Theoremclimres 10018 A function restricted to upper integers converges iff the original function converges. (Contributed by Mario Carneiro, 13-Jul-2013.) (Revised by Mario Carneiro, 31-Jan-2014.)
((𝑀 ∈ ℤ ∧ 𝐹𝑉) → ((𝐹 ↾ (ℤ𝑀)) ⇝ 𝐴𝐹𝐴))

Theoremclimshft 10019 A shifted function converges iff the original function converges. (Contributed by NM, 16-Aug-2005.) (Revised by Mario Carneiro, 31-Jan-2014.)
((𝑀 ∈ ℤ ∧ 𝐹𝑉) → ((𝐹 shift 𝑀) ⇝ 𝐴𝐹𝐴))

Theoremiserclim0 10020 The zero series converges to zero. (Contributed by Jim Kingdon, 19-Aug-2021.)
(𝑀 ∈ ℤ → seq𝑀( + , ((ℤ𝑀) × {0}), ℂ) ⇝ 0)

Theoremclimshft2 10021* A shifted function converges iff the original function converges. (Contributed by Paul Chapman, 21-Nov-2007.) (Revised by Mario Carneiro, 6-Feb-2014.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝐾 ∈ ℤ)    &   (𝜑𝐹𝑊)    &   (𝜑𝐺𝑋)    &   ((𝜑𝑘𝑍) → (𝐺‘(𝑘 + 𝐾)) = (𝐹𝑘))       (𝜑 → (𝐹𝐴𝐺𝐴))

Theoremclimabs0 10022* 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 10023* Image of a limit under a continuous map. (Contributed by Mario Carneiro, 31-Jan-2014.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝐴𝐵)    &   ((𝜑𝑧𝐵) → (𝐹𝑧) ∈ ℂ)    &   (𝜑𝐺𝐴)    &   (𝜑𝐻𝑊)    &   ((𝜑𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℝ+𝑧𝐵 ((abs‘(𝑧𝐴)) < 𝑦 → (abs‘((𝐹𝑧) − (𝐹𝐴))) < 𝑥))    &   ((𝜑𝑘𝑍) → (𝐺𝑘) ∈ 𝐵)    &   ((𝜑𝑘𝑍) → (𝐻𝑘) = (𝐹‘(𝐺𝑘)))       (𝜑𝐻 ⇝ (𝐹𝐴))

Theoremclimcn2 10024* Image of a limit under a continuous map, two-arg version. (Contributed by Mario Carneiro, 31-Jan-2014.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝐴𝐶)    &   (𝜑𝐵𝐷)    &   ((𝜑 ∧ (𝑢𝐶𝑣𝐷)) → (𝑢𝐹𝑣) ∈ ℂ)    &   (𝜑𝐺𝐴)    &   (𝜑𝐻𝐵)    &   (𝜑𝐾𝑊)    &   ((𝜑𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑢𝐶𝑣𝐷 (((abs‘(𝑢𝐴)) < 𝑦 ∧ (abs‘(𝑣𝐵)) < 𝑧) → (abs‘((𝑢𝐹𝑣) − (𝐴𝐹𝐵))) < 𝑥))    &   ((𝜑𝑘𝑍) → (𝐺𝑘) ∈ 𝐶)    &   ((𝜑𝑘𝑍) → (𝐻𝑘) ∈ 𝐷)    &   ((𝜑𝑘𝑍) → (𝐾𝑘) = ((𝐺𝑘)𝐹(𝐻𝑘)))       (𝜑𝐾 ⇝ (𝐴𝐹𝐵))

Theoremaddcn2 10025* 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 10026* 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 10027* 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 10028* A sufficient condition for a function to be continuous. (Contributed by Mario Carneiro, 9-Feb-2014.)
𝐹:ℂ⟶ℂ    &   ((𝑧 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (abs‘((𝐹𝑧) − (𝐹𝐴))) ≤ (abs‘(𝑧𝐴)))       ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℝ+𝑧 ∈ ℂ ((abs‘(𝑧𝐴)) < 𝑦 → (abs‘((𝐹𝑧) − (𝐹𝐴))) < 𝑥))

Theoremabscn2 10029* The absolute value function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.)
((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℝ+𝑧 ∈ ℂ ((abs‘(𝑧𝐴)) < 𝑦 → (abs‘((abs‘𝑧) − (abs‘𝐴))) < 𝑥))

Theoremcjcn2 10030* The complex conjugate function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.)
((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℝ+𝑧 ∈ ℂ ((abs‘(𝑧𝐴)) < 𝑦 → (abs‘((∗‘𝑧) − (∗‘𝐴))) < 𝑥))

Theoremrecn2 10031* The real part function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.)
((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℝ+𝑧 ∈ ℂ ((abs‘(𝑧𝐴)) < 𝑦 → (abs‘((ℜ‘𝑧) − (ℜ‘𝐴))) < 𝑥))

Theoremimcn2 10032* The imaginary part function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.)
((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℝ+𝑧 ∈ ℂ ((abs‘(𝑧𝐴)) < 𝑦 → (abs‘((ℑ‘𝑧) − (ℑ‘𝐴))) < 𝑥))

Theoremclimcn1lem 10033* The limit of a continuous function, theorem form. (Contributed by Mario Carneiro, 9-Feb-2014.)
𝑍 = (ℤ𝑀)    &   (𝜑𝐹𝐴)    &   (𝜑𝐺𝑊)    &   (𝜑𝑀 ∈ ℤ)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℂ)    &   𝐻:ℂ⟶ℂ    &   ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℝ+𝑧 ∈ ℂ ((abs‘(𝑧𝐴)) < 𝑦 → (abs‘((𝐻𝑧) − (𝐻𝐴))) < 𝑥))    &   ((𝜑𝑘𝑍) → (𝐺𝑘) = (𝐻‘(𝐹𝑘)))       (𝜑𝐺 ⇝ (𝐻𝐴))

Theoremclimabs 10034* 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 10035* 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 10036* 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 10037* 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 10038* The limit of a convergent real sequence is real. Corollary 12-2.5 of [Gleason] p. 172. (Contributed by NM, 10-Sep-2005.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝐹𝐴)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℝ)       (𝜑𝐴 ∈ ℝ)

Theoremclimge0 10039* A nonnegative sequence converges to a nonnegative number. (Contributed by NM, 11-Sep-2005.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝐹𝐴)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℝ)    &   ((𝜑𝑘𝑍) → 0 ≤ (𝐹𝑘))       (𝜑 → 0 ≤ 𝐴)

Theoremclimadd 10040* 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 10041* 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 10042* 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 10043* 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 10044* 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 10045* 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 10046* Limit of a constant 𝐶 subtracted from each term of a sequence. (Contributed by Mario Carneiro, 9-Feb-2014.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝐹𝐴)    &   (𝜑𝐶 ∈ ℂ)    &   (𝜑𝐺𝑊)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℂ)    &   ((𝜑𝑘𝑍) → (𝐺𝑘) = ((𝐹𝑘) − 𝐶))       (𝜑𝐺 ⇝ (𝐴𝐶))

Theoremclimsubc2 10047* Limit of a constant 𝐶 minus each term of a sequence. (Contributed by NM, 24-Sep-2005.) (Revised by Mario Carneiro, 9-Feb-2014.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝐹𝐴)    &   (𝜑𝐶 ∈ ℂ)    &   (𝜑𝐺𝑊)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℂ)    &   ((𝜑𝑘𝑍) → (𝐺𝑘) = (𝐶 − (𝐹𝑘)))       (𝜑𝐺 ⇝ (𝐶𝐴))

Theoremclimle 10048* Comparison of the limits of two sequences. (Contributed by Paul Chapman, 10-Sep-2007.) (Revised by Mario Carneiro, 1-Feb-2014.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝐹𝐴)    &   (𝜑𝐺𝐵)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℝ)    &   ((𝜑𝑘𝑍) → (𝐺𝑘) ∈ ℝ)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) ≤ (𝐺𝑘))       (𝜑𝐴𝐵)

Theoremclimsqz 10049* 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 10050* 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 10051* The limit of an infinite series with an initial segment removed. (Contributed by Jim Kingdon, 20-Aug-2021.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑁𝑍)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℂ)    &   (𝜑 → seq𝑀( + , 𝐹, ℂ) ⇝ 𝐴)       (𝜑 → seq(𝑁 + 1)( + , 𝐹, ℂ) ⇝ (𝐴 − (seq𝑀( + , 𝐹, ℂ)‘𝑁)))

Theoremclim2iser2 10052* The limit of an infinite series with an initial segment added. (Contributed by Jim Kingdon, 21-Aug-2021.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑁𝑍)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℂ)    &   (𝜑 → seq(𝑁 + 1)( + , 𝐹, ℂ) ⇝ 𝐴)       (𝜑 → seq𝑀( + , 𝐹, ℂ) ⇝ (𝐴 + (seq𝑀( + , 𝐹, ℂ)‘𝑁)))

Theoremiiserex 10053* 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 10054* 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 10055* Comparison of a constant to the limit of a sequence. (Contributed by NM, 28-Feb-2008.) (Revised by Mario Carneiro, 1-Feb-2014.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝐴 ∈ ℝ)    &   (𝜑𝐹𝐵)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℝ)    &   ((𝜑𝑘𝑍) → 𝐴 ≤ (𝐹𝑘))       (𝜑𝐴𝐵)

Theoremiserile 10056* Comparison of the limits of two infinite series. (Contributed by Jim Kingdon, 22-Aug-2021.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑 → seq𝑀( + , 𝐹, ℂ) ⇝ 𝐴)    &   (𝜑 → seq𝑀( + , 𝐺, ℂ) ⇝ 𝐵)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℝ)    &   ((𝜑𝑘𝑍) → (𝐺𝑘) ∈ ℝ)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) ≤ (𝐺𝑘))       (𝜑𝐴𝐵)

Theoremiserige0 10057* The limit of an infinite series of nonnegative reals is nonnegative. (Contributed by Jim Kingdon, 22-Aug-2021.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑 → seq𝑀( + , 𝐹, ℂ) ⇝ 𝐴)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℝ)    &   ((𝜑𝑘𝑍) → 0 ≤ (𝐹𝑘))       (𝜑 → 0 ≤ 𝐴)

Theoremclimub 10058* 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 10059* 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 10060* 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 10063). 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 10061* 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 10062* Lemma for climcvg1n 10063. 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 10063* 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 10064* A converging sequence of complex numbers is a Cauchy sequence. This is like climcau 10060 but adds the part that (𝐹𝑘) is complex. (Contributed by Jim Kingdon, 24-Aug-2021.)
𝑍 = (ℤ𝑀)       ((𝑀 ∈ ℤ ∧ 𝐹 ∈ dom ⇝ ) → ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)((𝐹𝑘) ∈ ℂ ∧ (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑥))

Theoremserif0 10065* 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 10066 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 10067* 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 10068 Equality theorem for a sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.)
(𝐴 = 𝐵 → Σ𝑘𝐴 𝐶 = Σ𝑘𝐵 𝐶)

Theoremnfsum1 10069 Bound-variable hypothesis builder for sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.)
𝑘𝐴       𝑘Σ𝑘𝐴 𝐵

Theoremnfsum 10070 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  The divides relation

Syntaxcdvds 10071 Extend the definition of a class to include the divides relation. See df-dvds 10072.
class

Definitiondf-dvds 10072* Define the divides relation, see definition in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.)
∥ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ ∃𝑛 ∈ ℤ (𝑛 · 𝑥) = 𝑦)}

Theoremdivides 10073* Define the divides relation. 𝑀𝑁 means 𝑀 divides into 𝑁 with no remainder. For example, 3 ∥ 6 (ex-dvds 10226). As proven in dvdsval3 10075, 𝑀𝑁 ↔ (𝑁 mod 𝑀) = 0. See divides 10073 and dvdsval2 10074 for other equivalent expressions. (Contributed by Paul Chapman, 21-Mar-2011.)
((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀𝑁 ↔ ∃𝑛 ∈ ℤ (𝑛 · 𝑀) = 𝑁))

Theoremdvdsval2 10074 One nonzero integer divides another integer if and only if their quotient is an integer. (Contributed by Jeff Hankins, 29-Sep-2013.)
((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝑀𝑁 ↔ (𝑁 / 𝑀) ∈ ℤ))

Theoremdvdsval3 10075 One nonzero integer divides another integer if and only if the remainder upon division is zero, see remark in [ApostolNT] p. 106. (Contributed by Mario Carneiro, 22-Feb-2014.) (Revised by Mario Carneiro, 15-Jul-2014.)
((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ) → (𝑀𝑁 ↔ (𝑁 mod 𝑀) = 0))

Theoremdvdszrcl 10076 Reverse closure for the divisibility relation. (Contributed by Stefan O'Rear, 5-Sep-2015.)
(𝑋𝑌 → (𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ))

Theoremnndivdvds 10077 Strong form of dvdsval2 10074 for positive integers. (Contributed by Stefan O'Rear, 13-Sep-2014.)
((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐵𝐴 ↔ (𝐴 / 𝐵) ∈ ℕ))

Theoremnndivides 10078* Definition of the divides relation for positive integers. (Contributed by AV, 26-Jul-2021.)
((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀𝑁 ↔ ∃𝑛 ∈ ℕ (𝑛 · 𝑀) = 𝑁))

Theoremdvdsdc 10079 Divisibility is decidable. (Contributed by Jim Kingdon, 14-Nov-2021.)
((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ) → DECID 𝑀𝑁)

Theoremmoddvds 10080 Two ways to say 𝐴𝐵 (mod 𝑁), see also definition in [ApostolNT] p. 106. (Contributed by Mario Carneiro, 18-Feb-2014.)
((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 mod 𝑁) = (𝐵 mod 𝑁) ↔ 𝑁 ∥ (𝐴𝐵)))

Theoremdvds0lem 10081 A lemma to assist theorems of with no antecedents. (Contributed by Paul Chapman, 21-Mar-2011.)
(((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 · 𝑀) = 𝑁) → 𝑀𝑁)

Theoremdvds1lem 10082* A lemma to assist theorems of with one antecedent. (Contributed by Paul Chapman, 21-Mar-2011.)
(𝜑 → (𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ))    &   (𝜑 → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))    &   ((𝜑𝑥 ∈ ℤ) → 𝑍 ∈ ℤ)    &   ((𝜑𝑥 ∈ ℤ) → ((𝑥 · 𝐽) = 𝐾 → (𝑍 · 𝑀) = 𝑁))       (𝜑 → (𝐽𝐾𝑀𝑁))

Theoremdvds2lem 10083* A lemma to assist theorems of with two antecedents. (Contributed by Paul Chapman, 21-Mar-2011.)
(𝜑 → (𝐼 ∈ ℤ ∧ 𝐽 ∈ ℤ))    &   (𝜑 → (𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ))    &   (𝜑 → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))    &   ((𝜑 ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝑍 ∈ ℤ)    &   ((𝜑 ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (((𝑥 · 𝐼) = 𝐽 ∧ (𝑦 · 𝐾) = 𝐿) → (𝑍 · 𝑀) = 𝑁))       (𝜑 → ((𝐼𝐽𝐾𝐿) → 𝑀𝑁))

Theoremiddvds 10084 An integer divides itself. Theorem 1.1(a) in [ApostolNT] p. 14 (reflexive property of the divides relation). (Contributed by Paul Chapman, 21-Mar-2011.)
(𝑁 ∈ ℤ → 𝑁𝑁)

Theorem1dvds 10085 1 divides any integer. Theorem 1.1(f) in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.)
(𝑁 ∈ ℤ → 1 ∥ 𝑁)

Theoremdvds0 10086 Any integer divides 0. Theorem 1.1(g) in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.)
(𝑁 ∈ ℤ → 𝑁 ∥ 0)

Theoremnegdvdsb 10087 An integer divides another iff its negation does. (Contributed by Paul Chapman, 21-Mar-2011.)
((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀𝑁 ↔ -𝑀𝑁))

Theoremdvdsnegb 10088 An integer divides another iff it divides its negation. (Contributed by Paul Chapman, 21-Mar-2011.)
((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀𝑁𝑀 ∥ -𝑁))

Theoremabsdvdsb 10089 An integer divides another iff its absolute value does. (Contributed by Paul Chapman, 21-Mar-2011.)
((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀𝑁 ↔ (abs‘𝑀) ∥ 𝑁))

Theoremdvdsabsb 10090 An integer divides another iff it divides its absolute value. (Contributed by Paul Chapman, 21-Mar-2011.)
((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀𝑁𝑀 ∥ (abs‘𝑁)))

Theorem0dvds 10091 Only 0 is divisible by 0. Theorem 1.1(h) in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.)
(𝑁 ∈ ℤ → (0 ∥ 𝑁𝑁 = 0))

Theoremdvdsmul1 10092 An integer divides a multiple of itself. (Contributed by Paul Chapman, 21-Mar-2011.)
((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑀 ∥ (𝑀 · 𝑁))

Theoremdvdsmul2 10093 An integer divides a multiple of itself. (Contributed by Paul Chapman, 21-Mar-2011.)
((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∥ (𝑀 · 𝑁))

Theoremiddvdsexp 10094 An integer divides a positive integer power of itself. (Contributed by Paul Chapman, 26-Oct-2012.)
((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑀 ∥ (𝑀𝑁))

Theoremmuldvds1 10095 If a product divides an integer, so does one of its factors. (Contributed by Paul Chapman, 21-Mar-2011.)
((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 · 𝑀) ∥ 𝑁𝐾𝑁))

Theoremmuldvds2 10096 If a product divides an integer, so does one of its factors. (Contributed by Paul Chapman, 21-Mar-2011.)
((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 · 𝑀) ∥ 𝑁𝑀𝑁))

Theoremdvdscmul 10097 Multiplication by a constant maintains the divides relation. Theorem 1.1(d) in [ApostolNT] p. 14 (multiplication property of the divides relation). (Contributed by Paul Chapman, 21-Mar-2011.)
((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀𝑁 → (𝐾 · 𝑀) ∥ (𝐾 · 𝑁)))

Theoremdvdsmulc 10098 Multiplication by a constant maintains the divides relation. (Contributed by Paul Chapman, 21-Mar-2011.)
((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀𝑁 → (𝑀 · 𝐾) ∥ (𝑁 · 𝐾)))

Theoremdvdscmulr 10099 Cancellation law for the divides relation. Theorem 1.1(e) in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.)
((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐾 ∈ ℤ ∧ 𝐾 ≠ 0)) → ((𝐾 · 𝑀) ∥ (𝐾 · 𝑁) ↔ 𝑀𝑁))

Theoremdvdsmulcr 10100 Cancellation law for the divides relation. (Contributed by Paul Chapman, 21-Mar-2011.)
((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐾 ∈ ℤ ∧ 𝐾 ≠ 0)) → ((𝑀 · 𝐾) ∥ (𝑁 · 𝐾) ↔ 𝑀𝑁))

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-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10454
 Copyright terms: Public domain < Previous  Next >