![]() |
Metamath
Proof Explorer Theorem List (p. 142 of 473) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-29807) |
![]() (29808-31330) |
![]() (31331-47223) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | sq3 14101 | The square of 3 is 9. (Contributed by NM, 26-Apr-2006.) |
⊢ (3↑2) = 9 | ||
Theorem | sq4e2t8 14102 | The square of 4 is 2 times 8. (Contributed by AV, 20-Jul-2021.) |
⊢ (4↑2) = (2 · 8) | ||
Theorem | cu2 14103 | The cube of 2 is 8. (Contributed by NM, 2-Aug-2004.) |
⊢ (2↑3) = 8 | ||
Theorem | irec 14104 | The reciprocal of i. (Contributed by NM, 11-Oct-1999.) |
⊢ (1 / i) = -i | ||
Theorem | i2 14105 | i squared. (Contributed by NM, 6-May-1999.) |
⊢ (i↑2) = -1 | ||
Theorem | i3 14106 | i cubed. (Contributed by NM, 31-Jan-2007.) |
⊢ (i↑3) = -i | ||
Theorem | i4 14107 | i to the fourth power. (Contributed by NM, 31-Jan-2007.) |
⊢ (i↑4) = 1 | ||
Theorem | nnlesq 14108 | A positive integer is less than or equal to its square. For general integers, see zzlesq 14109. (Contributed by NM, 15-Sep-1999.) (Revised by Mario Carneiro, 12-Sep-2015.) |
⊢ (𝑁 ∈ ℕ → 𝑁 ≤ (𝑁↑2)) | ||
Theorem | zzlesq 14109 | An integer is less than or equal to its square. (Contributed by BJ, 6-Feb-2025.) |
⊢ (𝑁 ∈ ℤ → 𝑁 ≤ (𝑁↑2)) | ||
Theorem | iexpcyc 14110 | Taking i to the 𝐾-th power is the same as using the 𝐾 mod 4 -th power instead, by i4 14107. (Contributed by Mario Carneiro, 7-Jul-2014.) |
⊢ (𝐾 ∈ ℤ → (i↑(𝐾 mod 4)) = (i↑𝐾)) | ||
Theorem | expnass 14111 | A counterexample showing that exponentiation is not associative. (Contributed by Stefan Allan and Gérard Lang, 21-Sep-2010.) |
⊢ ((3↑3)↑3) < (3↑(3↑3)) | ||
Theorem | sqlecan 14112 | Cancel one factor of a square in a ≤ comparison. Unlike lemul1 12006, the common factor 𝐴 may be zero. (Contributed by NM, 17-Jan-2008.) |
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((𝐴↑2) ≤ (𝐵 · 𝐴) ↔ 𝐴 ≤ 𝐵)) | ||
Theorem | subsq 14113 | Factor the difference of two squares. (Contributed by NM, 21-Feb-2008.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑2) − (𝐵↑2)) = ((𝐴 + 𝐵) · (𝐴 − 𝐵))) | ||
Theorem | subsq2 14114 | Express the difference of the squares of two numbers as a polynomial in the difference of the numbers. (Contributed by NM, 21-Feb-2008.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑2) − (𝐵↑2)) = (((𝐴 − 𝐵)↑2) + ((2 · 𝐵) · (𝐴 − 𝐵)))) | ||
Theorem | binom2i 14115 | The square of a binomial. (Contributed by NM, 11-Aug-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ ((𝐴 + 𝐵)↑2) = (((𝐴↑2) + (2 · (𝐴 · 𝐵))) + (𝐵↑2)) | ||
Theorem | subsqi 14116 | Factor the difference of two squares. (Contributed by NM, 7-Feb-2005.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ ((𝐴↑2) − (𝐵↑2)) = ((𝐴 + 𝐵) · (𝐴 − 𝐵)) | ||
Theorem | sqeqori 14117 | The squares of two complex numbers are equal iff one number equals the other or its negative. Lemma 15-4.7 of [Gleason] p. 311 and its converse. (Contributed by NM, 15-Jan-2006.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ ((𝐴↑2) = (𝐵↑2) ↔ (𝐴 = 𝐵 ∨ 𝐴 = -𝐵)) | ||
Theorem | subsq0i 14118 | The two solutions to the difference of squares set equal to zero. (Contributed by NM, 25-Apr-2006.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (((𝐴↑2) − (𝐵↑2)) = 0 ↔ (𝐴 = 𝐵 ∨ 𝐴 = -𝐵)) | ||
Theorem | sqeqor 14119 | The squares of two complex numbers are equal iff one number equals the other or its negative. Lemma 15-4.7 of [Gleason] p. 311 and its converse. (Contributed by Paul Chapman, 15-Mar-2008.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑2) = (𝐵↑2) ↔ (𝐴 = 𝐵 ∨ 𝐴 = -𝐵))) | ||
Theorem | binom2 14120 | The square of a binomial. (Contributed by FL, 10-Dec-2006.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵)↑2) = (((𝐴↑2) + (2 · (𝐴 · 𝐵))) + (𝐵↑2))) | ||
Theorem | binom21 14121 | Special case of binom2 14120 where 𝐵 = 1. (Contributed by Scott Fenton, 11-May-2014.) |
⊢ (𝐴 ∈ ℂ → ((𝐴 + 1)↑2) = (((𝐴↑2) + (2 · 𝐴)) + 1)) | ||
Theorem | binom2sub 14122 | Expand the square of a subtraction. (Contributed by Scott Fenton, 10-Jun-2013.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵)↑2) = (((𝐴↑2) − (2 · (𝐴 · 𝐵))) + (𝐵↑2))) | ||
Theorem | binom2sub1 14123 | Special case of binom2sub 14122 where 𝐵 = 1. (Contributed by AV, 2-Aug-2021.) |
⊢ (𝐴 ∈ ℂ → ((𝐴 − 1)↑2) = (((𝐴↑2) − (2 · 𝐴)) + 1)) | ||
Theorem | binom2subi 14124 | Expand the square of a subtraction. (Contributed by Scott Fenton, 13-Jun-2013.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ ((𝐴 − 𝐵)↑2) = (((𝐴↑2) − (2 · (𝐴 · 𝐵))) + (𝐵↑2)) | ||
Theorem | mulbinom2 14125 | The square of a binomial with factor. (Contributed by AV, 19-Jul-2021.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (((𝐶 · 𝐴) + 𝐵)↑2) = ((((𝐶 · 𝐴)↑2) + ((2 · 𝐶) · (𝐴 · 𝐵))) + (𝐵↑2))) | ||
Theorem | binom3 14126 | The cube of a binomial. (Contributed by Mario Carneiro, 24-Apr-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵)↑3) = (((𝐴↑3) + (3 · ((𝐴↑2) · 𝐵))) + ((3 · (𝐴 · (𝐵↑2))) + (𝐵↑3)))) | ||
Theorem | sq01 14127 | If a complex number equals its square, it must be 0 or 1. (Contributed by NM, 6-Jun-2006.) |
⊢ (𝐴 ∈ ℂ → ((𝐴↑2) = 𝐴 ↔ (𝐴 = 0 ∨ 𝐴 = 1))) | ||
Theorem | zesq 14128 | An integer is even iff its square is even. (Contributed by Mario Carneiro, 12-Sep-2015.) |
⊢ (𝑁 ∈ ℤ → ((𝑁 / 2) ∈ ℤ ↔ ((𝑁↑2) / 2) ∈ ℤ)) | ||
Theorem | nnesq 14129 | A positive integer is even iff its square is even. (Contributed by NM, 20-Aug-2001.) (Revised by Mario Carneiro, 12-Sep-2015.) |
⊢ (𝑁 ∈ ℕ → ((𝑁 / 2) ∈ ℕ ↔ ((𝑁↑2) / 2) ∈ ℕ)) | ||
Theorem | crreczi 14130 | Reciprocal of a complex number in terms of real and imaginary components. Remark in [Apostol] p. 361. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Jeff Hankins, 16-Dec-2013.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ ((𝐴 ≠ 0 ∨ 𝐵 ≠ 0) → (1 / (𝐴 + (i · 𝐵))) = ((𝐴 − (i · 𝐵)) / ((𝐴↑2) + (𝐵↑2)))) | ||
Theorem | bernneq 14131 | Bernoulli's inequality, due to Johan Bernoulli (1667-1748). (Contributed by NM, 21-Feb-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ -1 ≤ 𝐴) → (1 + (𝐴 · 𝑁)) ≤ ((1 + 𝐴)↑𝑁)) | ||
Theorem | bernneq2 14132 | Variation of Bernoulli's inequality bernneq 14131. (Contributed by NM, 18-Oct-2007.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ 0 ≤ 𝐴) → (((𝐴 − 1) · 𝑁) + 1) ≤ (𝐴↑𝑁)) | ||
Theorem | bernneq3 14133 | A corollary of bernneq 14131. (Contributed by Mario Carneiro, 11-Mar-2014.) |
⊢ ((𝑃 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ0) → 𝑁 < (𝑃↑𝑁)) | ||
Theorem | expnbnd 14134* | Exponentiation with a base greater than 1 has no upper bound. (Contributed by NM, 20-Oct-2007.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → ∃𝑘 ∈ ℕ 𝐴 < (𝐵↑𝑘)) | ||
Theorem | expnlbnd 14135* | The reciprocal of exponentiation with a base greater than 1 has no positive lower bound. (Contributed by NM, 18-Jul-2008.) |
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → ∃𝑘 ∈ ℕ (1 / (𝐵↑𝑘)) < 𝐴) | ||
Theorem | expnlbnd2 14136* | The reciprocal of exponentiation with a base greater than 1 has no positive lower bound. (Contributed by NM, 18-Jul-2008.) (Proof shortened by Mario Carneiro, 5-Jun-2014.) |
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(1 / (𝐵↑𝑘)) < 𝐴) | ||
Theorem | expmulnbnd 14137* | Exponentiation with a base greater than 1 is not bounded by any linear function. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → ∃𝑗 ∈ ℕ0 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐴 · 𝑘) < (𝐵↑𝑘)) | ||
Theorem | digit2 14138 | Two ways to express the 𝐾 th digit in the decimal (when base 𝐵 = 10) expansion of a number 𝐴. 𝐾 = 1 corresponds to the first digit after the decimal point. (Contributed by NM, 25-Dec-2008.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ) → ((⌊‘((𝐵↑𝐾) · 𝐴)) mod 𝐵) = ((⌊‘((𝐵↑𝐾) · 𝐴)) − (𝐵 · (⌊‘((𝐵↑(𝐾 − 1)) · 𝐴))))) | ||
Theorem | digit1 14139 | Two ways to express the 𝐾 th digit in the decimal expansion of a number 𝐴 (when base 𝐵 = 10). 𝐾 = 1 corresponds to the first digit after the decimal point. (Contributed by NM, 3-Jan-2009.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ) → ((⌊‘((𝐵↑𝐾) · 𝐴)) mod 𝐵) = (((⌊‘((𝐵↑𝐾) · 𝐴)) mod (𝐵↑𝐾)) − ((𝐵 · (⌊‘((𝐵↑(𝐾 − 1)) · 𝐴))) mod (𝐵↑𝐾)))) | ||
Theorem | modexp 14140 | Exponentiation property of the modulo operation, see theorem 5.2(c) in [ApostolNT] p. 107. (Contributed by Mario Carneiro, 28-Feb-2014.) |
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℝ+) ∧ (𝐴 mod 𝐷) = (𝐵 mod 𝐷)) → ((𝐴↑𝐶) mod 𝐷) = ((𝐵↑𝐶) mod 𝐷)) | ||
Theorem | discr1 14141* | A nonnegative quadratic form has nonnegative leading coefficient. (Contributed by Mario Carneiro, 4-Jun-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 0 ≤ (((𝐴 · (𝑥↑2)) + (𝐵 · 𝑥)) + 𝐶)) & ⊢ 𝑋 = if(1 ≤ (((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) + 1) / -𝐴), (((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) + 1) / -𝐴), 1) ⇒ ⊢ (𝜑 → 0 ≤ 𝐴) | ||
Theorem | discr 14142* | If a quadratic polynomial with real coefficients is nonnegative for all values, then its discriminant is nonpositive. (Contributed by NM, 10-Aug-1999.) (Revised by Mario Carneiro, 4-Jun-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 0 ≤ (((𝐴 · (𝑥↑2)) + (𝐵 · 𝑥)) + 𝐶)) ⇒ ⊢ (𝜑 → ((𝐵↑2) − (4 · (𝐴 · 𝐶))) ≤ 0) | ||
Theorem | expnngt1 14143 | If an integer power with a positive integer base is greater than 1, then the exponent is positive. (Contributed by AV, 28-Dec-2022.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ ∧ 1 < (𝐴↑𝐵)) → 𝐵 ∈ ℕ) | ||
Theorem | expnngt1b 14144 | An integer power with an integer base greater than 1 is greater than 1 iff the exponent is positive. (Contributed by AV, 28-Dec-2022.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ ℤ) → (1 < (𝐴↑𝐵) ↔ 𝐵 ∈ ℕ)) | ||
Theorem | sqoddm1div8 14145 | A squared odd number minus 1 divided by 8 is the odd number multiplied with its successor divided by 2. (Contributed by AV, 19-Jul-2021.) |
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 = ((2 · 𝑁) + 1)) → (((𝑀↑2) − 1) / 8) = ((𝑁 · (𝑁 + 1)) / 2)) | ||
Theorem | nnsqcld 14146 | The naturals are closed under squaring. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) ⇒ ⊢ (𝜑 → (𝐴↑2) ∈ ℕ) | ||
Theorem | nnexpcld 14147 | Closure of exponentiation of nonnegative integers. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝐴↑𝑁) ∈ ℕ) | ||
Theorem | nn0expcld 14148 | Closure of exponentiation of nonnegative integers. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℕ0) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝐴↑𝑁) ∈ ℕ0) | ||
Theorem | rpexpcld 14149 | Closure law for exponentiation of positive reals. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝑁 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝐴↑𝑁) ∈ ℝ+) | ||
Theorem | ltexp2rd 14150 | The power of a positive number smaller than 1 decreases as its exponent increases. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐴 < 1) ⇒ ⊢ (𝜑 → (𝑀 < 𝑁 ↔ (𝐴↑𝑁) < (𝐴↑𝑀))) | ||
Theorem | reexpclzd 14151 | Closure of exponentiation of reals. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝑁 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝐴↑𝑁) ∈ ℝ) | ||
Theorem | sqgt0d 14152 | The square of a nonzero real is positive. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≠ 0) ⇒ ⊢ (𝜑 → 0 < (𝐴↑2)) | ||
Theorem | ltexp2d 14153 | Ordering relationship for exponentiation. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 1 < 𝐴) ⇒ ⊢ (𝜑 → (𝑀 < 𝑁 ↔ (𝐴↑𝑀) < (𝐴↑𝑁))) | ||
Theorem | leexp2d 14154 | Ordering law for exponentiation. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 1 < 𝐴) ⇒ ⊢ (𝜑 → (𝑀 ≤ 𝑁 ↔ (𝐴↑𝑀) ≤ (𝐴↑𝑁))) | ||
Theorem | expcand 14155 | Ordering relationship for exponentiation. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 1 < 𝐴) & ⊢ (𝜑 → (𝐴↑𝑀) = (𝐴↑𝑁)) ⇒ ⊢ (𝜑 → 𝑀 = 𝑁) | ||
Theorem | leexp2ad 14156 | Ordering relationship for exponentiation. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 1 ≤ 𝐴) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) ⇒ ⊢ (𝜑 → (𝐴↑𝑀) ≤ (𝐴↑𝑁)) | ||
Theorem | leexp2rd 14157 | Ordering relationship for exponentiation. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐴 ≤ 1) ⇒ ⊢ (𝜑 → (𝐴↑𝑁) ≤ (𝐴↑𝑀)) | ||
Theorem | lt2sqd 14158 | The square function on nonnegative reals is strictly monotonic. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 0 ≤ 𝐵) ⇒ ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (𝐴↑2) < (𝐵↑2))) | ||
Theorem | le2sqd 14159 | The square function on nonnegative reals is monotonic. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 0 ≤ 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (𝐴↑2) ≤ (𝐵↑2))) | ||
Theorem | sq11d 14160 | The square function is one-to-one for nonnegative reals. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 0 ≤ 𝐵) & ⊢ (𝜑 → (𝐴↑2) = (𝐵↑2)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | mulsubdivbinom2 14161 | The square of a binomial with factor minus a number divided by a nonzero number. (Contributed by AV, 19-Jul-2021.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → (((((𝐶 · 𝐴) + 𝐵)↑2) − 𝐷) / 𝐶) = (((𝐶 · (𝐴↑2)) + (2 · (𝐴 · 𝐵))) + (((𝐵↑2) − 𝐷) / 𝐶))) | ||
Theorem | muldivbinom2 14162 | The square of a binomial with factor divided by a nonzero number. (Contributed by AV, 19-Jul-2021.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((((𝐶 · 𝐴) + 𝐵)↑2) / 𝐶) = (((𝐶 · (𝐴↑2)) + (2 · (𝐴 · 𝐵))) + ((𝐵↑2) / 𝐶))) | ||
Theorem | sq10 14163 | The square of 10 is 100. (Contributed by AV, 14-Jun-2021.) (Revised by AV, 1-Aug-2021.) |
⊢ (;10↑2) = ;;100 | ||
Theorem | sq10e99m1 14164 | The square of 10 is 99 plus 1. (Contributed by AV, 14-Jun-2021.) (Revised by AV, 1-Aug-2021.) |
⊢ (;10↑2) = (;99 + 1) | ||
Theorem | 3dec 14165 | A "decimal constructor" which is used to build up "decimal integers" or "numeric terms" in base 10 with 3 "digits". (Contributed by AV, 14-Jun-2021.) (Revised by AV, 1-Aug-2021.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 ⇒ ⊢ ;;𝐴𝐵𝐶 = ((((;10↑2) · 𝐴) + (;10 · 𝐵)) + 𝐶) | ||
Theorem | nn0le2msqi 14166 | The square function on nonnegative integers is monotonic. (Contributed by Raph Levien, 10-Dec-2002.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 ⇒ ⊢ (𝐴 ≤ 𝐵 ↔ (𝐴 · 𝐴) ≤ (𝐵 · 𝐵)) | ||
Theorem | nn0opthlem1 14167 | A rather pretty lemma for nn0opthi 14169. (Contributed by Raph Levien, 10-Dec-2002.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 ⇒ ⊢ (𝐴 < 𝐶 ↔ ((𝐴 · 𝐴) + (2 · 𝐴)) < (𝐶 · 𝐶)) | ||
Theorem | nn0opthlem2 14168 | Lemma for nn0opthi 14169. (Contributed by Raph Levien, 10-Dec-2002.) (Revised by Scott Fenton, 8-Sep-2010.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 ⇒ ⊢ ((𝐴 + 𝐵) < 𝐶 → ((𝐶 · 𝐶) + 𝐷) ≠ (((𝐴 + 𝐵) · (𝐴 + 𝐵)) + 𝐵)) | ||
Theorem | nn0opthi 14169 | An ordered pair theorem for nonnegative integers. Theorem 17.3 of [Quine] p. 124. We can represent an ordered pair of nonnegative integers 𝐴 and 𝐵 by (((𝐴 + 𝐵) · (𝐴 + 𝐵)) + 𝐵). If two such ordered pairs are equal, their first elements are equal and their second elements are equal. Contrast this ordered pair representation with the standard one df-op 4593 that works for any set. (Contributed by Raph Levien, 10-Dec-2002.) (Proof shortened by Scott Fenton, 8-Sep-2010.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 ⇒ ⊢ ((((𝐴 + 𝐵) · (𝐴 + 𝐵)) + 𝐵) = (((𝐶 + 𝐷) · (𝐶 + 𝐷)) + 𝐷) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) | ||
Theorem | nn0opth2i 14170 | An ordered pair theorem for nonnegative integers. Theorem 17.3 of [Quine] p. 124. See comments for nn0opthi 14169. (Contributed by NM, 22-Jul-2004.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 ⇒ ⊢ ((((𝐴 + 𝐵)↑2) + 𝐵) = (((𝐶 + 𝐷)↑2) + 𝐷) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) | ||
Theorem | nn0opth2 14171 | An ordered pair theorem for nonnegative integers. Theorem 17.3 of [Quine] p. 124. See nn0opthi 14169. (Contributed by NM, 22-Jul-2004.) |
⊢ (((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) ∧ (𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℕ0)) → ((((𝐴 + 𝐵)↑2) + 𝐵) = (((𝐶 + 𝐷)↑2) + 𝐷) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))) | ||
Syntax | cfa 14172 | Extend class notation to include the factorial of nonnegative integers. |
class ! | ||
Definition | df-fac 14173 | Define the factorial function on nonnegative integers. For example, (!‘5) = 120 because 1 · 2 · 3 · 4 · 5 = 120 (ex-fac 29342). In the literature, the factorial function is written as a postscript exclamation point. (Contributed by NM, 2-Dec-2004.) |
⊢ ! = ({〈0, 1〉} ∪ seq1( · , I )) | ||
Theorem | facnn 14174 | Value of the factorial function for positive integers. (Contributed by NM, 2-Dec-2004.) (Revised by Mario Carneiro, 13-Jul-2013.) |
⊢ (𝑁 ∈ ℕ → (!‘𝑁) = (seq1( · , I )‘𝑁)) | ||
Theorem | fac0 14175 | The factorial of 0. (Contributed by NM, 2-Dec-2004.) (Revised by Mario Carneiro, 13-Jul-2013.) |
⊢ (!‘0) = 1 | ||
Theorem | fac1 14176 | The factorial of 1. (Contributed by NM, 2-Dec-2004.) (Revised by Mario Carneiro, 13-Jul-2013.) |
⊢ (!‘1) = 1 | ||
Theorem | facp1 14177 | The factorial of a successor. (Contributed by NM, 2-Dec-2004.) (Revised by Mario Carneiro, 13-Jul-2013.) |
⊢ (𝑁 ∈ ℕ0 → (!‘(𝑁 + 1)) = ((!‘𝑁) · (𝑁 + 1))) | ||
Theorem | fac2 14178 | The factorial of 2. (Contributed by NM, 17-Mar-2005.) |
⊢ (!‘2) = 2 | ||
Theorem | fac3 14179 | The factorial of 3. (Contributed by NM, 17-Mar-2005.) |
⊢ (!‘3) = 6 | ||
Theorem | fac4 14180 | The factorial of 4. (Contributed by Mario Carneiro, 18-Jun-2015.) |
⊢ (!‘4) = ;24 | ||
Theorem | facnn2 14181 | Value of the factorial function expressed recursively. (Contributed by NM, 2-Dec-2004.) |
⊢ (𝑁 ∈ ℕ → (!‘𝑁) = ((!‘(𝑁 − 1)) · 𝑁)) | ||
Theorem | faccl 14182 | Closure of the factorial function. (Contributed by NM, 2-Dec-2004.) |
⊢ (𝑁 ∈ ℕ0 → (!‘𝑁) ∈ ℕ) | ||
Theorem | faccld 14183 | Closure of the factorial function, deduction version of faccl 14182. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (!‘𝑁) ∈ ℕ) | ||
Theorem | facmapnn 14184 | The factorial function restricted to positive integers is a mapping from the positive integers to the positive integers. (Contributed by AV, 8-Aug-2020.) |
⊢ (𝑛 ∈ ℕ ↦ (!‘𝑛)) ∈ (ℕ ↑m ℕ) | ||
Theorem | facne0 14185 | The factorial function is nonzero. (Contributed by NM, 26-Apr-2005.) |
⊢ (𝑁 ∈ ℕ0 → (!‘𝑁) ≠ 0) | ||
Theorem | facdiv 14186 | A positive integer divides the factorial of an equal or larger number. (Contributed by NM, 2-May-2005.) |
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝑁 ≤ 𝑀) → ((!‘𝑀) / 𝑁) ∈ ℕ) | ||
Theorem | facndiv 14187 | No positive integer (greater than one) divides the factorial plus one of an equal or larger number. (Contributed by NM, 3-May-2005.) |
⊢ (((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ) ∧ (1 < 𝑁 ∧ 𝑁 ≤ 𝑀)) → ¬ (((!‘𝑀) + 1) / 𝑁) ∈ ℤ) | ||
Theorem | facwordi 14188 | Ordering property of factorial. (Contributed by NM, 9-Dec-2005.) |
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁) → (!‘𝑀) ≤ (!‘𝑁)) | ||
Theorem | faclbnd 14189 | A lower bound for the factorial function. (Contributed by NM, 17-Dec-2005.) |
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀↑(𝑁 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑁))) | ||
Theorem | faclbnd2 14190 | A lower bound for the factorial function. (Contributed by NM, 17-Dec-2005.) |
⊢ (𝑁 ∈ ℕ0 → ((2↑𝑁) / 2) ≤ (!‘𝑁)) | ||
Theorem | faclbnd3 14191 | A lower bound for the factorial function. (Contributed by NM, 19-Dec-2005.) |
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀↑𝑁) ≤ ((𝑀↑𝑀) · (!‘𝑁))) | ||
Theorem | faclbnd4lem1 14192 | Lemma for faclbnd4 14196. Prepare the induction step. (Contributed by NM, 20-Dec-2005.) |
⊢ 𝑁 ∈ ℕ & ⊢ 𝐾 ∈ ℕ0 & ⊢ 𝑀 ∈ ℕ0 ⇒ ⊢ ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) → ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) ≤ (((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · (!‘𝑁))) | ||
Theorem | faclbnd4lem2 14193 | Lemma for faclbnd4 14196. Use the weak deduction theorem to convert the hypotheses of faclbnd4lem1 14192 to antecedents. (Contributed by NM, 23-Dec-2005.) |
⊢ ((𝑀 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ) → ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) → ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) ≤ (((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · (!‘𝑁)))) | ||
Theorem | faclbnd4lem3 14194 | Lemma for faclbnd4 14196. The 𝑁 = 0 case. (Contributed by NM, 23-Dec-2005.) |
⊢ (((𝑀 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0) ∧ 𝑁 = 0) → ((𝑁↑𝐾) · (𝑀↑𝑁)) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘𝑁))) | ||
Theorem | faclbnd4lem4 14195 | Lemma for faclbnd4 14196. Prove the 0 < 𝑁 case by induction on 𝐾. (Contributed by NM, 19-Dec-2005.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0) → ((𝑁↑𝐾) · (𝑀↑𝑁)) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘𝑁))) | ||
Theorem | faclbnd4 14196 | Variant of faclbnd5 14197 providing a non-strict lower bound. (Contributed by NM, 23-Dec-2005.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0) → ((𝑁↑𝐾) · (𝑀↑𝑁)) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘𝑁))) | ||
Theorem | faclbnd5 14197 | The factorial function grows faster than powers and exponentiations. If we consider 𝐾 and 𝑀 to be constants, the right-hand side of the inequality is a constant times 𝑁-factorial. (Contributed by NM, 24-Dec-2005.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ) → ((𝑁↑𝐾) · (𝑀↑𝑁)) < ((2 · ((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾)))) · (!‘𝑁))) | ||
Theorem | faclbnd6 14198 | Geometric lower bound for the factorial function, where N is usually held constant. (Contributed by Paul Chapman, 28-Dec-2007.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0) → ((!‘𝑁) · ((𝑁 + 1)↑𝑀)) ≤ (!‘(𝑁 + 𝑀))) | ||
Theorem | facubnd 14199 | An upper bound for the factorial function. (Contributed by Mario Carneiro, 15-Apr-2016.) |
⊢ (𝑁 ∈ ℕ0 → (!‘𝑁) ≤ (𝑁↑𝑁)) | ||
Theorem | facavg 14200 | The product of two factorials is greater than or equal to the factorial of (the floor of) their average. (Contributed by NM, 9-Dec-2005.) |
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (!‘(⌊‘((𝑀 + 𝑁) / 2))) ≤ ((!‘𝑀) · (!‘𝑁))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |