HomeHome Intuitionistic Logic Explorer
Theorem List (p. 106 of 114)
< 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 - 10501-10600   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremsqr11d 10501 The square root function is one-to-one. (Contributed by Mario Carneiro, 29-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑 → 0 ≤ 𝐴)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑 → 0 ≤ 𝐵)    &   (𝜑 → (√‘𝐴) = (√‘𝐵))       (𝜑𝐴 = 𝐵)
 
Theoremabsltd 10502 Absolute value and 'less than' relation. (Contributed by Mario Carneiro, 29-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)       (𝜑 → ((abs‘𝐴) < 𝐵 ↔ (-𝐵 < 𝐴𝐴 < 𝐵)))
 
Theoremabsled 10503 Absolute value and 'less than or equal to' relation. (Contributed by Mario Carneiro, 29-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)       (𝜑 → ((abs‘𝐴) ≤ 𝐵 ↔ (-𝐵𝐴𝐴𝐵)))
 
Theoremabssubge0d 10504 Absolute value of a nonnegative difference. (Contributed by Mario Carneiro, 29-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐴𝐵)       (𝜑 → (abs‘(𝐵𝐴)) = (𝐵𝐴))
 
Theoremabssuble0d 10505 Absolute value of a nonpositive difference. (Contributed by Mario Carneiro, 29-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐴𝐵)       (𝜑 → (abs‘(𝐴𝐵)) = (𝐵𝐴))
 
Theoremabsdifltd 10506 The absolute value of a difference and 'less than' relation. (Contributed by Mario Carneiro, 29-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐶 ∈ ℝ)       (𝜑 → ((abs‘(𝐴𝐵)) < 𝐶 ↔ ((𝐵𝐶) < 𝐴𝐴 < (𝐵 + 𝐶))))
 
Theoremabsdifled 10507 The absolute value of a difference and 'less than or equal to' relation. (Contributed by Mario Carneiro, 29-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐶 ∈ ℝ)       (𝜑 → ((abs‘(𝐴𝐵)) ≤ 𝐶 ↔ ((𝐵𝐶) ≤ 𝐴𝐴 ≤ (𝐵 + 𝐶))))
 
Theoremicodiamlt 10508 Two elements in a half-open interval have separation strictly less than the difference between the endpoints. (Contributed by Stefan O'Rear, 12-Sep-2014.)
(((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ (𝐴[,)𝐵) ∧ 𝐷 ∈ (𝐴[,)𝐵))) → (abs‘(𝐶𝐷)) < (𝐵𝐴))
 
Theoremabscld 10509 Real closure of absolute value. (Contributed by Mario Carneiro, 29-May-2016.)
(𝜑𝐴 ∈ ℂ)       (𝜑 → (abs‘𝐴) ∈ ℝ)
 
Theoremabsvalsqd 10510 Square of value of absolute value function. (Contributed by Mario Carneiro, 29-May-2016.)
(𝜑𝐴 ∈ ℂ)       (𝜑 → ((abs‘𝐴)↑2) = (𝐴 · (∗‘𝐴)))
 
Theoremabsvalsq2d 10511 Square of value of absolute value function. (Contributed by Mario Carneiro, 29-May-2016.)
(𝜑𝐴 ∈ ℂ)       (𝜑 → ((abs‘𝐴)↑2) = (((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2)))
 
Theoremabsge0d 10512 Absolute value is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.)
(𝜑𝐴 ∈ ℂ)       (𝜑 → 0 ≤ (abs‘𝐴))
 
Theoremabsval2d 10513 Value of absolute value function. Definition 10.36 of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
(𝜑𝐴 ∈ ℂ)       (𝜑 → (abs‘𝐴) = (√‘(((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2))))
 
Theoremabs00d 10514 The absolute value of a number is zero iff the number is zero. Proposition 10-3.7(c) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑 → (abs‘𝐴) = 0)       (𝜑𝐴 = 0)
 
Theoremabsne0d 10515 The absolute value of a number is zero iff the number is zero. Proposition 10-3.7(c) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐴 ≠ 0)       (𝜑 → (abs‘𝐴) ≠ 0)
 
Theoremabsrpclapd 10516 The absolute value of a complex number apart from zero is a positive real. (Contributed by Jim Kingdon, 13-Aug-2021.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐴 # 0)       (𝜑 → (abs‘𝐴) ∈ ℝ+)
 
Theoremabsnegd 10517 Absolute value of negative. (Contributed by Mario Carneiro, 29-May-2016.)
(𝜑𝐴 ∈ ℂ)       (𝜑 → (abs‘-𝐴) = (abs‘𝐴))
 
Theoremabscjd 10518 The absolute value of a number and its conjugate are the same. Proposition 10-3.7(b) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
(𝜑𝐴 ∈ ℂ)       (𝜑 → (abs‘(∗‘𝐴)) = (abs‘𝐴))
 
Theoremreleabsd 10519 The real part of a number is less than or equal to its absolute value. Proposition 10-3.7(d) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
(𝜑𝐴 ∈ ℂ)       (𝜑 → (ℜ‘𝐴) ≤ (abs‘𝐴))
 
Theoremabsexpd 10520 Absolute value of positive integer exponentiation. (Contributed by Mario Carneiro, 29-May-2016.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝑁 ∈ ℕ0)       (𝜑 → (abs‘(𝐴𝑁)) = ((abs‘𝐴)↑𝑁))
 
Theoremabssubd 10521 Swapping order of subtraction doesn't change the absolute value. Example of [Apostol] p. 363. (Contributed by Mario Carneiro, 29-May-2016.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐵 ∈ ℂ)       (𝜑 → (abs‘(𝐴𝐵)) = (abs‘(𝐵𝐴)))
 
Theoremabsmuld 10522 Absolute value distributes over multiplication. Proposition 10-3.7(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐵 ∈ ℂ)       (𝜑 → (abs‘(𝐴 · 𝐵)) = ((abs‘𝐴) · (abs‘𝐵)))
 
Theoremabsdivapd 10523 Absolute value distributes over division. (Contributed by Jim Kingdon, 13-Aug-2021.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐵 ∈ ℂ)    &   (𝜑𝐵 # 0)       (𝜑 → (abs‘(𝐴 / 𝐵)) = ((abs‘𝐴) / (abs‘𝐵)))
 
Theoremabstrid 10524 Triangle inequality for absolute value. Proposition 10-3.7(h) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐵 ∈ ℂ)       (𝜑 → (abs‘(𝐴 + 𝐵)) ≤ ((abs‘𝐴) + (abs‘𝐵)))
 
Theoremabs2difd 10525 Difference of absolute values. (Contributed by Mario Carneiro, 29-May-2016.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐵 ∈ ℂ)       (𝜑 → ((abs‘𝐴) − (abs‘𝐵)) ≤ (abs‘(𝐴𝐵)))
 
Theoremabs2dif2d 10526 Difference of absolute values. (Contributed by Mario Carneiro, 29-May-2016.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐵 ∈ ℂ)       (𝜑 → (abs‘(𝐴𝐵)) ≤ ((abs‘𝐴) + (abs‘𝐵)))
 
Theoremabs2difabsd 10527 Absolute value of difference of absolute values. (Contributed by Mario Carneiro, 29-May-2016.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐵 ∈ ℂ)       (𝜑 → (abs‘((abs‘𝐴) − (abs‘𝐵))) ≤ (abs‘(𝐴𝐵)))
 
Theoremabs3difd 10528 Absolute value of differences around common element. (Contributed by Mario Carneiro, 29-May-2016.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐵 ∈ ℂ)    &   (𝜑𝐶 ∈ ℂ)       (𝜑 → (abs‘(𝐴𝐵)) ≤ ((abs‘(𝐴𝐶)) + (abs‘(𝐶𝐵))))
 
Theoremabs3lemd 10529 Lemma involving absolute value of differences. (Contributed by Mario Carneiro, 29-May-2016.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐵 ∈ ℂ)    &   (𝜑𝐶 ∈ ℂ)    &   (𝜑𝐷 ∈ ℝ)    &   (𝜑 → (abs‘(𝐴𝐶)) < (𝐷 / 2))    &   (𝜑 → (abs‘(𝐶𝐵)) < (𝐷 / 2))       (𝜑 → (abs‘(𝐴𝐵)) < 𝐷)
 
Theoremqdenre 10530* The rational numbers are dense in : any real number can be approximated with arbitrary precision by a rational number. For order theoretic density, see qbtwnre 9596. (Contributed by BJ, 15-Oct-2021.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → ∃𝑥 ∈ ℚ (abs‘(𝑥𝐴)) < 𝐵)
 
3.7.5  The maximum of two real numbers
 
Theoremmaxcom 10531 The maximum of two reals is commutative. Lemma 3.9 of [Geuvers], p. 10. (Contributed by Jim Kingdon, 21-Dec-2021.)
sup({𝐴, 𝐵}, ℝ, < ) = sup({𝐵, 𝐴}, ℝ, < )
 
Theoremmaxabsle 10532 An upper bound for {𝐴, 𝐵}. (Contributed by Jim Kingdon, 20-Dec-2021.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐴 ≤ (((𝐴 + 𝐵) + (abs‘(𝐴𝐵))) / 2))
 
Theoremmaxleim 10533 Value of maximum when we know which number is larger. (Contributed by Jim Kingdon, 21-Dec-2021.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴𝐵 → sup({𝐴, 𝐵}, ℝ, < ) = 𝐵))
 
Theoremmaxabslemab 10534 Lemma for maxabs 10537. A variation of maxleim 10533- that is, if we know which of two real numbers is larger, we know the maximum of the two. (Contributed by Jim Kingdon, 21-Dec-2021.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐴 < 𝐵)       (𝜑 → (((𝐴 + 𝐵) + (abs‘(𝐴𝐵))) / 2) = 𝐵)
 
Theoremmaxabslemlub 10535 Lemma for maxabs 10537. A least upper bound for {𝐴, 𝐵}. (Contributed by Jim Kingdon, 20-Dec-2021.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐶 ∈ ℝ)    &   (𝜑𝐶 < (((𝐴 + 𝐵) + (abs‘(𝐴𝐵))) / 2))       (𝜑 → (𝐶 < 𝐴𝐶 < 𝐵))
 
Theoremmaxabslemval 10536* Lemma for maxabs 10537. Value of the supremum. (Contributed by Jim Kingdon, 22-Dec-2021.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((((𝐴 + 𝐵) + (abs‘(𝐴𝐵))) / 2) ∈ ℝ ∧ ∀𝑥 ∈ {𝐴, 𝐵} ¬ (((𝐴 + 𝐵) + (abs‘(𝐴𝐵))) / 2) < 𝑥 ∧ ∀𝑥 ∈ ℝ (𝑥 < (((𝐴 + 𝐵) + (abs‘(𝐴𝐵))) / 2) → ∃𝑧 ∈ {𝐴, 𝐵}𝑥 < 𝑧)))
 
Theoremmaxabs 10537 Maximum of two real numbers in terms of absolute value. (Contributed by Jim Kingdon, 20-Dec-2021.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → sup({𝐴, 𝐵}, ℝ, < ) = (((𝐴 + 𝐵) + (abs‘(𝐴𝐵))) / 2))
 
Theoremmaxcl 10538 The maximum of two real numbers is a real number. (Contributed by Jim Kingdon, 22-Dec-2021.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → sup({𝐴, 𝐵}, ℝ, < ) ∈ ℝ)
 
Theoremmaxle1 10539 The maximum of two reals is no smaller than the first real. Lemma 3.10 of [Geuvers], p. 10. (Contributed by Jim Kingdon, 21-Dec-2021.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐴 ≤ sup({𝐴, 𝐵}, ℝ, < ))
 
Theoremmaxle2 10540 The maximum of two reals is no smaller than the second real. Lemma 3.10 of [Geuvers], p. 10. (Contributed by Jim Kingdon, 21-Dec-2021.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐵 ≤ sup({𝐴, 𝐵}, ℝ, < ))
 
Theoremmaxleast 10541 The maximum of two reals is a least upper bound. Lemma 3.11 of [Geuvers], p. 10. (Contributed by Jim Kingdon, 22-Dec-2021.)
(((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴𝐶𝐵𝐶)) → sup({𝐴, 𝐵}, ℝ, < ) ≤ 𝐶)
 
Theoremmaxleastb 10542 Two ways of saying the maximum of two numbers is less than or equal to a third. (Contributed by Jim Kingdon, 31-Jan-2022.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (sup({𝐴, 𝐵}, ℝ, < ) ≤ 𝐶 ↔ (𝐴𝐶𝐵𝐶)))
 
Theoremmaxleastlt 10543 The maximum as a least upper bound, in terms of less than. (Contributed by Jim Kingdon, 9-Feb-2022.)
(((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐶 < sup({𝐴, 𝐵}, ℝ, < ))) → (𝐶 < 𝐴𝐶 < 𝐵))
 
Theoremmaxleb 10544 Equivalence of and being equal to the maximum of two reals. Lemma 3.12 of [Geuvers], p. 10. (Contributed by Jim Kingdon, 21-Dec-2021.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴𝐵 ↔ sup({𝐴, 𝐵}, ℝ, < ) = 𝐵))
 
Theoremdfabsmax 10545 Absolute value of a real number in terms of maximum. Definition 3.13 of [Geuvers], p. 11. (Contributed by BJ and Jim Kingdon, 21-Dec-2021.)
(𝐴 ∈ ℝ → (abs‘𝐴) = sup({𝐴, -𝐴}, ℝ, < ))
 
Theoremmaxltsup 10546 Two ways of saying the maximum of two numbers is less than a third. (Contributed by Jim Kingdon, 10-Feb-2022.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (sup({𝐴, 𝐵}, ℝ, < ) < 𝐶 ↔ (𝐴 < 𝐶𝐵 < 𝐶)))
 
Theoremmax0addsup 10547 The sum of the positive and negative part functions is the absolute value function over the reals. (Contributed by Jim Kingdon, 30-Jan-2022.)
(𝐴 ∈ ℝ → (sup({𝐴, 0}, ℝ, < ) + sup({-𝐴, 0}, ℝ, < )) = (abs‘𝐴))
 
Theoremrexanre 10548* Combine two different upper real properties into one. (Contributed by Mario Carneiro, 8-May-2016.)
(𝐴 ⊆ ℝ → (∃𝑗 ∈ ℝ ∀𝑘𝐴 (𝑗𝑘 → (𝜑𝜓)) ↔ (∃𝑗 ∈ ℝ ∀𝑘𝐴 (𝑗𝑘𝜑) ∧ ∃𝑗 ∈ ℝ ∀𝑘𝐴 (𝑗𝑘𝜓))))
 
Theoremrexico 10549* Restrict the base of an upper real quantifier to an upper real set. (Contributed by Mario Carneiro, 12-May-2016.)
((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) → (∃𝑗 ∈ (𝐵[,)+∞)∀𝑘𝐴 (𝑗𝑘𝜑) ↔ ∃𝑗 ∈ ℝ ∀𝑘𝐴 (𝑗𝑘𝜑)))
 
Theoremmaxclpr 10550 The maximum of two real numbers is one of those numbers if and only if dichotomy (𝐴𝐵𝐵𝐴) holds. For example, this can be combined with zletric 8727 if one is dealing with integers, but real number dichotomy in general does not follow from our axioms. (Contributed by Jim Kingdon, 1-Feb-2022.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (sup({𝐴, 𝐵}, ℝ, < ) ∈ {𝐴, 𝐵} ↔ (𝐴𝐵𝐵𝐴)))
 
Theoremfimaxre2 10551* A nonempty finite set of real numbers has an upper bound. (Contributed by Jeff Madsen, 27-May-2011.) (Revised by Mario Carneiro, 13-Feb-2014.)
((𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin) → ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦𝑥)
 
Theoremnegfi 10552* The negation of a finite set of real numbers is finite. (Contributed by AV, 9-Aug-2020.)
((𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin) → {𝑛 ∈ ℝ ∣ -𝑛𝐴} ∈ Fin)
 
3.7.6  The minimum of two real numbers
 
Theoremmincom 10553 The minimum of two reals is commutative. (Contributed by Jim Kingdon, 8-Feb-2021.)
inf({𝐴, 𝐵}, ℝ, < ) = inf({𝐵, 𝐴}, ℝ, < )
 
Theoremminmax 10554 Minimum expressed in terms of maximum. (Contributed by Jim Kingdon, 8-Feb-2021.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → inf({𝐴, 𝐵}, ℝ, < ) = -sup({-𝐴, -𝐵}, ℝ, < ))
 
Theoremmin1inf 10555 The minimum of two numbers is less than or equal to the first. (Contributed by Jim Kingdon, 8-Feb-2021.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → inf({𝐴, 𝐵}, ℝ, < ) ≤ 𝐴)
 
Theoremmin2inf 10556 The minimum of two numbers is less than or equal to the second. (Contributed by Jim Kingdon, 9-Feb-2021.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → inf({𝐴, 𝐵}, ℝ, < ) ≤ 𝐵)
 
Theoremlemininf 10557 Two ways of saying a number is less than or equal to the minimum of two others. (Contributed by NM, 3-Aug-2007.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 ≤ inf({𝐵, 𝐶}, ℝ, < ) ↔ (𝐴𝐵𝐴𝐶)))
 
Theoremltmininf 10558 Two ways of saying a number is less than the minimum of two others. (Contributed by Jim Kingdon, 10-Feb-2022.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < inf({𝐵, 𝐶}, ℝ, < ) ↔ (𝐴 < 𝐵𝐴 < 𝐶)))
 
3.8  Elementary limits and convergence
 
3.8.1  Limits
 
Syntaxcli 10559 Extend class notation with convergence relation for limits.
class
 
Definitiondf-clim 10560* Define the limit relation for complex number sequences. See clim 10562 for its relational expression. (Contributed by NM, 28-Aug-2005.)
⇝ = {⟨𝑓, 𝑦⟩ ∣ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)((𝑓𝑘) ∈ ℂ ∧ (abs‘((𝑓𝑘) − 𝑦)) < 𝑥))}
 
Theoremclimrel 10561 The limit relation is a relation. (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 31-Jan-2014.)
Rel ⇝
 
Theoremclim 10562* Express the predicate: The limit of complex number sequence 𝐹 is 𝐴, or 𝐹 converges to 𝐴. This means that for any real 𝑥, no matter how small, there always exists an integer 𝑗 such that the absolute difference of any later complex number in the sequence and the limit is less than 𝑥. (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
(𝜑𝐹𝑉)    &   ((𝜑𝑘 ∈ ℤ) → (𝐹𝑘) = 𝐵)       (𝜑 → (𝐹𝐴 ↔ (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)(𝐵 ∈ ℂ ∧ (abs‘(𝐵𝐴)) < 𝑥))))
 
Theoremclimcl 10563 Closure of the limit of a sequence of complex numbers. (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
(𝐹𝐴𝐴 ∈ ℂ)
 
Theoremclim2 10564* Express the predicate: The limit of complex number sequence 𝐹 is 𝐴, or 𝐹 converges to 𝐴, with more general quantifier restrictions than clim 10562. (Contributed by NM, 6-Jan-2007.) (Revised by Mario Carneiro, 31-Jan-2014.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝐹𝑉)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) = 𝐵)       (𝜑 → (𝐹𝐴 ↔ (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐵 ∈ ℂ ∧ (abs‘(𝐵𝐴)) < 𝑥))))
 
Theoremclim2c 10565* Express the predicate 𝐹 converges to 𝐴. (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝐹𝑉)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) = 𝐵)    &   (𝜑𝐴 ∈ ℂ)    &   ((𝜑𝑘𝑍) → 𝐵 ∈ ℂ)       (𝜑 → (𝐹𝐴 ↔ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘(𝐵𝐴)) < 𝑥))
 
Theoremclim0 10566* Express the predicate 𝐹 converges to 0. (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝐹𝑉)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) = 𝐵)       (𝜑 → (𝐹 ⇝ 0 ↔ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐵 ∈ ℂ ∧ (abs‘𝐵) < 𝑥)))
 
Theoremclim0c 10567* Express the predicate 𝐹 converges to 0. (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝐹𝑉)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) = 𝐵)    &   ((𝜑𝑘𝑍) → 𝐵 ∈ ℂ)       (𝜑 → (𝐹 ⇝ 0 ↔ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘𝐵) < 𝑥))
 
Theoremclimi 10568* Convergence of a sequence of complex numbers. (Contributed by NM, 11-Jan-2007.) (Revised by Mario Carneiro, 31-Jan-2014.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝐶 ∈ ℝ+)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) = 𝐵)    &   (𝜑𝐹𝐴)       (𝜑 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐵 ∈ ℂ ∧ (abs‘(𝐵𝐴)) < 𝐶))
 
Theoremclimi2 10569* Convergence of a sequence of complex numbers. (Contributed by NM, 11-Jan-2007.) (Revised by Mario Carneiro, 31-Jan-2014.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝐶 ∈ ℝ+)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) = 𝐵)    &   (𝜑𝐹𝐴)       (𝜑 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘(𝐵𝐴)) < 𝐶)
 
Theoremclimi0 10570* 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 10571* An (eventually) constant sequence converges to its value. (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 31-Jan-2014.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝐹𝑉)    &   (𝜑𝐴 ∈ ℂ)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) = 𝐴)       (𝜑𝐹𝐴)
 
Theoremclimconst2 10572 A constant sequence converges to its value. (Contributed by NM, 6-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)
(ℤ𝑀) ⊆ 𝑍    &   𝑍 ∈ V       ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℤ) → (𝑍 × {𝐴}) ⇝ 𝐴)
 
Theoremclimz 10573 The zero sequence converges to zero. (Contributed by NM, 2-Oct-1999.) (Revised by Mario Carneiro, 31-Jan-2014.)
(ℤ × {0}) ⇝ 0
 
Theoremclimuni 10574 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 10575 The limit relation is function-like, and with range the complex numbers. (Contributed by Mario Carneiro, 31-Jan-2014.)
⇝ :dom ⇝ ⟶ℂ
 
Theoremclimdm 10576 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 10577* An infinite sequence of complex numbers converges to at most one limit. (Contributed by NM, 25-Dec-2005.)
(𝐹𝐴 → ∃!𝑥 𝐹𝑥)
 
Theoremclimreu 10578* An infinite sequence of complex numbers converges to at most one limit. (Contributed by NM, 25-Dec-2005.)
(𝐹𝐴 → ∃!𝑥 ∈ ℂ 𝐹𝑥)
 
Theoremclimmo 10579* An infinite sequence of complex numbers converges to at most one limit. (Contributed by Mario Carneiro, 13-Jul-2013.)
∃*𝑥 𝐹𝑥
 
Theoremclimeq 10580* 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 10581* Exhibit a function 𝐺 with the same convergence properties as the not-quite-function 𝐹. (Contributed by Mario Carneiro, 31-Jan-2014.)
𝑍 = (ℤ𝑀)    &   𝐺 = (𝑘𝑍 ↦ (𝐹𝑘))       ((𝑀 ∈ ℤ ∧ 𝐹𝑉) → (𝐹𝐴𝐺𝐴))
 
Theorem2clim 10582* 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 10583 A shifted function converges if the original function converges. (Contributed by Mario Carneiro, 5-Nov-2013.)
((𝑀 ∈ ℤ ∧ 𝐹𝑉) → (𝐹𝐴 → (𝐹 shift 𝑀) ⇝ 𝐴))
 
Theoremclimres 10584 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 10585 A shifted function converges iff the original function converges. (Contributed by NM, 16-Aug-2005.) (Revised by Mario Carneiro, 31-Jan-2014.)
((𝑀 ∈ ℤ ∧ 𝐹𝑉) → ((𝐹 shift 𝑀) ⇝ 𝐴𝐹𝐴))
 
Theoremiserclim0 10586 The zero series converges to zero. (Contributed by Jim Kingdon, 19-Aug-2021.)
(𝑀 ∈ ℤ → seq𝑀( + , ((ℤ𝑀) × {0}), ℂ) ⇝ 0)
 
Theoremclimshft2 10587* A shifted function converges iff the original function converges. (Contributed by Paul Chapman, 21-Nov-2007.) (Revised by Mario Carneiro, 6-Feb-2014.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝐾 ∈ ℤ)    &   (𝜑𝐹𝑊)    &   (𝜑𝐺𝑋)    &   ((𝜑𝑘𝑍) → (𝐺‘(𝑘 + 𝐾)) = (𝐹𝑘))       (𝜑 → (𝐹𝐴𝐺𝐴))
 
Theoremclimabs0 10588* 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 10589* Image of a limit under a continuous map. (Contributed by Mario Carneiro, 31-Jan-2014.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝐴𝐵)    &   ((𝜑𝑧𝐵) → (𝐹𝑧) ∈ ℂ)    &   (𝜑𝐺𝐴)    &   (𝜑𝐻𝑊)    &   ((𝜑𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℝ+𝑧𝐵 ((abs‘(𝑧𝐴)) < 𝑦 → (abs‘((𝐹𝑧) − (𝐹𝐴))) < 𝑥))    &   ((𝜑𝑘𝑍) → (𝐺𝑘) ∈ 𝐵)    &   ((𝜑𝑘𝑍) → (𝐻𝑘) = (𝐹‘(𝐺𝑘)))       (𝜑𝐻 ⇝ (𝐹𝐴))
 
Theoremclimcn2 10590* Image of a limit under a continuous map, two-arg version. (Contributed by Mario Carneiro, 31-Jan-2014.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝐴𝐶)    &   (𝜑𝐵𝐷)    &   ((𝜑 ∧ (𝑢𝐶𝑣𝐷)) → (𝑢𝐹𝑣) ∈ ℂ)    &   (𝜑𝐺𝐴)    &   (𝜑𝐻𝐵)    &   (𝜑𝐾𝑊)    &   ((𝜑𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑢𝐶𝑣𝐷 (((abs‘(𝑢𝐴)) < 𝑦 ∧ (abs‘(𝑣𝐵)) < 𝑧) → (abs‘((𝑢𝐹𝑣) − (𝐴𝐹𝐵))) < 𝑥))    &   ((𝜑𝑘𝑍) → (𝐺𝑘) ∈ 𝐶)    &   ((𝜑𝑘𝑍) → (𝐻𝑘) ∈ 𝐷)    &   ((𝜑𝑘𝑍) → (𝐾𝑘) = ((𝐺𝑘)𝐹(𝐻𝑘)))       (𝜑𝐾 ⇝ (𝐴𝐹𝐵))
 
Theoremaddcn2 10591* 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 10592* 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 10593* 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 10594* A sufficient condition for a function to be continuous. (Contributed by Mario Carneiro, 9-Feb-2014.)
𝐹:ℂ⟶ℂ    &   ((𝑧 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (abs‘((𝐹𝑧) − (𝐹𝐴))) ≤ (abs‘(𝑧𝐴)))       ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℝ+𝑧 ∈ ℂ ((abs‘(𝑧𝐴)) < 𝑦 → (abs‘((𝐹𝑧) − (𝐹𝐴))) < 𝑥))
 
Theoremabscn2 10595* The absolute value function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.)
((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℝ+𝑧 ∈ ℂ ((abs‘(𝑧𝐴)) < 𝑦 → (abs‘((abs‘𝑧) − (abs‘𝐴))) < 𝑥))
 
Theoremcjcn2 10596* The complex conjugate function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.)
((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℝ+𝑧 ∈ ℂ ((abs‘(𝑧𝐴)) < 𝑦 → (abs‘((∗‘𝑧) − (∗‘𝐴))) < 𝑥))
 
Theoremrecn2 10597* The real part function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.)
((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℝ+𝑧 ∈ ℂ ((abs‘(𝑧𝐴)) < 𝑦 → (abs‘((ℜ‘𝑧) − (ℜ‘𝐴))) < 𝑥))
 
Theoremimcn2 10598* The imaginary part function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.)
((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℝ+𝑧 ∈ ℂ ((abs‘(𝑧𝐴)) < 𝑦 → (abs‘((ℑ‘𝑧) − (ℑ‘𝐴))) < 𝑥))
 
Theoremclimcn1lem 10599* The limit of a continuous function, theorem form. (Contributed by Mario Carneiro, 9-Feb-2014.)
𝑍 = (ℤ𝑀)    &   (𝜑𝐹𝐴)    &   (𝜑𝐺𝑊)    &   (𝜑𝑀 ∈ ℤ)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℂ)    &   𝐻:ℂ⟶ℂ    &   ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℝ+𝑧 ∈ ℂ ((abs‘(𝑧𝐴)) < 𝑦 → (abs‘((𝐻𝑧) − (𝐻𝐴))) < 𝑥))    &   ((𝜑𝑘𝑍) → (𝐺𝑘) = (𝐻‘(𝐹𝑘)))       (𝜑𝐺 ⇝ (𝐻𝐴))
 
Theoremclimabs 10600* 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‘𝐴))
    < 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-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11363
  Copyright terms: Public domain < Previous  Next >