HomeHome Intuitionistic Logic Explorer
Theorem List (p. 96 of 106)
< 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 - 9501-9600   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremsqeq0i 9501 A number is zero iff its square is zero. (Contributed by NM, 2-Oct-1999.)
𝐴 ∈ ℂ       ((𝐴↑2) = 0 ↔ 𝐴 = 0)
 
Theoremsqmuli 9502 Distribution of square over multiplication. (Contributed by NM, 3-Sep-1999.)
𝐴 ∈ ℂ    &   𝐵 ∈ ℂ       ((𝐴 · 𝐵)↑2) = ((𝐴↑2) · (𝐵↑2))
 
Theoremsqdivapi 9503 Distribution of square over division. (Contributed by Jim Kingdon, 12-Jun-2020.)
𝐴 ∈ ℂ    &   𝐵 ∈ ℂ    &   𝐵 # 0       ((𝐴 / 𝐵)↑2) = ((𝐴↑2) / (𝐵↑2))
 
Theoremresqcli 9504 Closure of square in reals. (Contributed by NM, 2-Aug-1999.)
𝐴 ∈ ℝ       (𝐴↑2) ∈ ℝ
 
Theoremsqgt0api 9505 The square of a nonzero real is positive. (Contributed by Jim Kingdon, 12-Jun-2020.)
𝐴 ∈ ℝ       (𝐴 # 0 → 0 < (𝐴↑2))
 
Theoremsqge0i 9506 A square of a real is nonnegative. (Contributed by NM, 3-Aug-1999.)
𝐴 ∈ ℝ       0 ≤ (𝐴↑2)
 
Theoremlt2sqi 9507 The square function on nonnegative reals is strictly monotonic. (Contributed by NM, 12-Sep-1999.)
𝐴 ∈ ℝ    &   𝐵 ∈ ℝ       ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → (𝐴 < 𝐵 ↔ (𝐴↑2) < (𝐵↑2)))
 
Theoremle2sqi 9508 The square function on nonnegative reals is monotonic. (Contributed by NM, 12-Sep-1999.)
𝐴 ∈ ℝ    &   𝐵 ∈ ℝ       ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → (𝐴𝐵 ↔ (𝐴↑2) ≤ (𝐵↑2)))
 
Theoremsq11i 9509 The square function is one-to-one for nonnegative reals. (Contributed by NM, 27-Oct-1999.)
𝐴 ∈ ℝ    &   𝐵 ∈ ℝ       ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → ((𝐴↑2) = (𝐵↑2) ↔ 𝐴 = 𝐵))
 
Theoremsq0 9510 The square of 0 is 0. (Contributed by NM, 6-Jun-2006.)
(0↑2) = 0
 
Theoremsq0i 9511 If a number is zero, its square is zero. (Contributed by FL, 10-Dec-2006.)
(𝐴 = 0 → (𝐴↑2) = 0)
 
Theoremsq0id 9512 If a number is zero, its square is zero. Deduction form of sq0i 9511. Converse of sqeq0d 9548. (Contributed by David Moews, 28-Feb-2017.)
(𝜑𝐴 = 0)       (𝜑 → (𝐴↑2) = 0)
 
Theoremsq1 9513 The square of 1 is 1. (Contributed by NM, 22-Aug-1999.)
(1↑2) = 1
 
Theoremneg1sqe1 9514 -1 squared is 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
(-1↑2) = 1
 
Theoremsq2 9515 The square of 2 is 4. (Contributed by NM, 22-Aug-1999.)
(2↑2) = 4
 
Theoremsq3 9516 The square of 3 is 9. (Contributed by NM, 26-Apr-2006.)
(3↑2) = 9
 
Theoremcu2 9517 The cube of 2 is 8. (Contributed by NM, 2-Aug-2004.)
(2↑3) = 8
 
Theoremirec 9518 The reciprocal of i. (Contributed by NM, 11-Oct-1999.)
(1 / i) = -i
 
Theoremi2 9519 i squared. (Contributed by NM, 6-May-1999.)
(i↑2) = -1
 
Theoremi3 9520 i cubed. (Contributed by NM, 31-Jan-2007.)
(i↑3) = -i
 
Theoremi4 9521 i to the fourth power. (Contributed by NM, 31-Jan-2007.)
(i↑4) = 1
 
Theoremnnlesq 9522 A positive integer is less than or equal to its square. (Contributed by NM, 15-Sep-1999.) (Revised by Mario Carneiro, 12-Sep-2015.)
(𝑁 ∈ ℕ → 𝑁 ≤ (𝑁↑2))
 
Theoremiexpcyc 9523 Taking i to the 𝐾-th power is the same as using the 𝐾 mod 4 -th power instead, by i4 9521. (Contributed by Mario Carneiro, 7-Jul-2014.)
(𝐾 ∈ ℤ → (i↑(𝐾 mod 4)) = (i↑𝐾))
 
Theoremexpnass 9524 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))
 
Theoremsubsq 9525 Factor the difference of two squares. (Contributed by NM, 21-Feb-2008.)
((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑2) − (𝐵↑2)) = ((𝐴 + 𝐵) · (𝐴𝐵)))
 
Theoremsubsq2 9526 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 · 𝐵) · (𝐴𝐵))))
 
Theorembinom2i 9527 The square of a binomial. (Contributed by NM, 11-Aug-1999.)
𝐴 ∈ ℂ    &   𝐵 ∈ ℂ       ((𝐴 + 𝐵)↑2) = (((𝐴↑2) + (2 · (𝐴 · 𝐵))) + (𝐵↑2))
 
Theoremsubsqi 9528 Factor the difference of two squares. (Contributed by NM, 7-Feb-2005.)
𝐴 ∈ ℂ    &   𝐵 ∈ ℂ       ((𝐴↑2) − (𝐵↑2)) = ((𝐴 + 𝐵) · (𝐴𝐵))
 
Theorembinom2 9529 The square of a binomial. (Contributed by FL, 10-Dec-2006.)
((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵)↑2) = (((𝐴↑2) + (2 · (𝐴 · 𝐵))) + (𝐵↑2)))
 
Theorembinom21 9530 Special case of binom2 9529 where 𝐵 = 1. (Contributed by Scott Fenton, 11-May-2014.)
(𝐴 ∈ ℂ → ((𝐴 + 1)↑2) = (((𝐴↑2) + (2 · 𝐴)) + 1))
 
Theorembinom2sub 9531 Expand the square of a subtraction. (Contributed by Scott Fenton, 10-Jun-2013.)
((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴𝐵)↑2) = (((𝐴↑2) − (2 · (𝐴 · 𝐵))) + (𝐵↑2)))
 
Theorembinom2subi 9532 Expand the square of a subtraction. (Contributed by Scott Fenton, 13-Jun-2013.)
𝐴 ∈ ℂ    &   𝐵 ∈ ℂ       ((𝐴𝐵)↑2) = (((𝐴↑2) − (2 · (𝐴 · 𝐵))) + (𝐵↑2))
 
Theoremmulbinom2 9533 The square of a binomial with factor. (Contributed by AV, 19-Jul-2021.)
((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (((𝐶 · 𝐴) + 𝐵)↑2) = ((((𝐶 · 𝐴)↑2) + ((2 · 𝐶) · (𝐴 · 𝐵))) + (𝐵↑2)))
 
Theorembinom3 9534 The cube of a binomial. (Contributed by Mario Carneiro, 24-Apr-2015.)
((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵)↑3) = (((𝐴↑3) + (3 · ((𝐴↑2) · 𝐵))) + ((3 · (𝐴 · (𝐵↑2))) + (𝐵↑3))))
 
Theoremzesq 9535 An integer is even iff its square is even. (Contributed by Mario Carneiro, 12-Sep-2015.)
(𝑁 ∈ ℤ → ((𝑁 / 2) ∈ ℤ ↔ ((𝑁↑2) / 2) ∈ ℤ))
 
Theoremnnesq 9536 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) ∈ ℕ))
 
Theorembernneq 9537 Bernoulli's inequality, due to Johan Bernoulli (1667-1748). (Contributed by NM, 21-Feb-2005.)
((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ -1 ≤ 𝐴) → (1 + (𝐴 · 𝑁)) ≤ ((1 + 𝐴)↑𝑁))
 
Theorembernneq2 9538 Variation of Bernoulli's inequality bernneq 9537. (Contributed by NM, 18-Oct-2007.)
((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ 0 ≤ 𝐴) → (((𝐴 − 1) · 𝑁) + 1) ≤ (𝐴𝑁))
 
Theorembernneq3 9539 A corollary of bernneq 9537. (Contributed by Mario Carneiro, 11-Mar-2014.)
((𝑃 ∈ (ℤ‘2) ∧ 𝑁 ∈ ℕ0) → 𝑁 < (𝑃𝑁))
 
Theoremexpnbnd 9540* Exponentiation with a mantissa greater than 1 has no upper bound. (Contributed by NM, 20-Oct-2007.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → ∃𝑘 ∈ ℕ 𝐴 < (𝐵𝑘))
 
Theoremexpnlbnd 9541* The reciprocal of exponentiation with a mantissa greater than 1 has no lower bound. (Contributed by NM, 18-Jul-2008.)
((𝐴 ∈ ℝ+𝐵 ∈ ℝ ∧ 1 < 𝐵) → ∃𝑘 ∈ ℕ (1 / (𝐵𝑘)) < 𝐴)
 
Theoremexpnlbnd2 9542* The reciprocal of exponentiation with a mantissa greater than 1 has no lower bound. (Contributed by NM, 18-Jul-2008.) (Proof shortened by Mario Carneiro, 5-Jun-2014.)
((𝐴 ∈ ℝ+𝐵 ∈ ℝ ∧ 1 < 𝐵) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(1 / (𝐵𝑘)) < 𝐴)
 
Theoremexp0d 9543 Value of a complex number raised to the 0th power. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℂ)       (𝜑 → (𝐴↑0) = 1)
 
Theoremexp1d 9544 Value of a complex number raised to the first power. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℂ)       (𝜑 → (𝐴↑1) = 𝐴)
 
Theoremexpeq0d 9545 Positive integer exponentiation is 0 iff its mantissa is 0. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝑁 ∈ ℕ)    &   (𝜑 → (𝐴𝑁) = 0)       (𝜑𝐴 = 0)
 
Theoremsqvald 9546 Value of square. Inference version. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℂ)       (𝜑 → (𝐴↑2) = (𝐴 · 𝐴))
 
Theoremsqcld 9547 Closure of square. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℂ)       (𝜑 → (𝐴↑2) ∈ ℂ)
 
Theoremsqeq0d 9548 A number is zero iff its square is zero. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑 → (𝐴↑2) = 0)       (𝜑𝐴 = 0)
 
Theoremexpcld 9549 Closure law for nonnegative integer exponentiation. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝑁 ∈ ℕ0)       (𝜑 → (𝐴𝑁) ∈ ℂ)
 
Theoremexpp1d 9550 Value of a complex number raised to a nonnegative integer power plus one. Part of Definition 10-4.1 of [Gleason] p. 134. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝑁 ∈ ℕ0)       (𝜑 → (𝐴↑(𝑁 + 1)) = ((𝐴𝑁) · 𝐴))
 
Theoremexpaddd 9551 Sum of exponents law for nonnegative integer exponentiation. Proposition 10-4.2(a) of [Gleason] p. 135. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝑁 ∈ ℕ0)    &   (𝜑𝑀 ∈ ℕ0)       (𝜑 → (𝐴↑(𝑀 + 𝑁)) = ((𝐴𝑀) · (𝐴𝑁)))
 
Theoremexpmuld 9552 Product of exponents law for positive integer exponentiation. Proposition 10-4.2(b) of [Gleason] p. 135, restricted to nonnegative integer exponents. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝑁 ∈ ℕ0)    &   (𝜑𝑀 ∈ ℕ0)       (𝜑 → (𝐴↑(𝑀 · 𝑁)) = ((𝐴𝑀)↑𝑁))
 
Theoremsqrecapd 9553 Square of reciprocal. (Contributed by Jim Kingdon, 12-Jun-2020.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐴 # 0)       (𝜑 → ((1 / 𝐴)↑2) = (1 / (𝐴↑2)))
 
Theoremexpclzapd 9554 Closure law for integer exponentiation. (Contributed by Jim Kingdon, 12-Jun-2020.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐴 # 0)    &   (𝜑𝑁 ∈ ℤ)       (𝜑 → (𝐴𝑁) ∈ ℂ)
 
Theoremexpap0d 9555 Nonnegative integer exponentiation is nonzero if its mantissa is nonzero. (Contributed by Jim Kingdon, 12-Jun-2020.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐴 # 0)    &   (𝜑𝑁 ∈ ℤ)       (𝜑 → (𝐴𝑁) # 0)
 
Theoremexpnegapd 9556 Value of a complex number raised to a negative power. (Contributed by Jim Kingdon, 12-Jun-2020.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐴 # 0)    &   (𝜑𝑁 ∈ ℤ)       (𝜑 → (𝐴↑-𝑁) = (1 / (𝐴𝑁)))
 
Theoremexprecapd 9557 Nonnegative integer exponentiation of a reciprocal. (Contributed by Jim Kingdon, 12-Jun-2020.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐴 # 0)    &   (𝜑𝑁 ∈ ℤ)       (𝜑 → ((1 / 𝐴)↑𝑁) = (1 / (𝐴𝑁)))
 
Theoremexpp1zapd 9558 Value of a nonzero complex number raised to an integer power plus one. (Contributed by Jim Kingdon, 12-Jun-2020.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐴 # 0)    &   (𝜑𝑁 ∈ ℤ)       (𝜑 → (𝐴↑(𝑁 + 1)) = ((𝐴𝑁) · 𝐴))
 
Theoremexpm1apd 9559 Value of a complex number raised to an integer power minus one. (Contributed by Jim Kingdon, 12-Jun-2020.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐴 # 0)    &   (𝜑𝑁 ∈ ℤ)       (𝜑 → (𝐴↑(𝑁 − 1)) = ((𝐴𝑁) / 𝐴))
 
Theoremexpsubapd 9560 Exponent subtraction law for nonnegative integer exponentiation. (Contributed by Jim Kingdon, 12-Jun-2020.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐴 # 0)    &   (𝜑𝑁 ∈ ℤ)    &   (𝜑𝑀 ∈ ℤ)       (𝜑 → (𝐴↑(𝑀𝑁)) = ((𝐴𝑀) / (𝐴𝑁)))
 
Theoremsqmuld 9561 Distribution of square over multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐵 ∈ ℂ)       (𝜑 → ((𝐴 · 𝐵)↑2) = ((𝐴↑2) · (𝐵↑2)))
 
Theoremsqdivapd 9562 Distribution of square over division. (Contributed by Jim Kingdon, 13-Jun-2020.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐵 ∈ ℂ)    &   (𝜑𝐵 # 0)       (𝜑 → ((𝐴 / 𝐵)↑2) = ((𝐴↑2) / (𝐵↑2)))
 
Theoremexpdivapd 9563 Nonnegative integer exponentiation of a quotient. (Contributed by Jim Kingdon, 13-Jun-2020.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐵 ∈ ℂ)    &   (𝜑𝐵 # 0)    &   (𝜑𝑁 ∈ ℕ0)       (𝜑 → ((𝐴 / 𝐵)↑𝑁) = ((𝐴𝑁) / (𝐵𝑁)))
 
Theoremmulexpd 9564 Positive integer exponentiation of a product. Proposition 10-4.2(c) of [Gleason] p. 135, restricted to nonnegative integer exponents. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐵 ∈ ℂ)    &   (𝜑𝑁 ∈ ℕ0)       (𝜑 → ((𝐴 · 𝐵)↑𝑁) = ((𝐴𝑁) · (𝐵𝑁)))
 
Theorem0expd 9565 Value of zero raised to a positive integer power. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝑁 ∈ ℕ)       (𝜑 → (0↑𝑁) = 0)
 
Theoremreexpcld 9566 Closure of exponentiation of reals. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝑁 ∈ ℕ0)       (𝜑 → (𝐴𝑁) ∈ ℝ)
 
Theoremexpge0d 9567 Nonnegative integer exponentiation with a nonnegative mantissa is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝑁 ∈ ℕ0)    &   (𝜑 → 0 ≤ 𝐴)       (𝜑 → 0 ≤ (𝐴𝑁))
 
Theoremexpge1d 9568 Nonnegative integer exponentiation with a nonnegative mantissa is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝑁 ∈ ℕ0)    &   (𝜑 → 1 ≤ 𝐴)       (𝜑 → 1 ≤ (𝐴𝑁))
 
Theoremsqoddm1div8 9569 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))
 
Theoremnnsqcld 9570 The naturals are closed under squaring. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℕ)       (𝜑 → (𝐴↑2) ∈ ℕ)
 
Theoremnnexpcld 9571 Closure of exponentiation of nonnegative integers. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℕ)    &   (𝜑𝑁 ∈ ℕ0)       (𝜑 → (𝐴𝑁) ∈ ℕ)
 
Theoremnn0expcld 9572 Closure of exponentiation of nonnegative integers. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℕ0)    &   (𝜑𝑁 ∈ ℕ0)       (𝜑 → (𝐴𝑁) ∈ ℕ0)
 
Theoremrpexpcld 9573 Closure law for exponentiation of positive reals. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ+)    &   (𝜑𝑁 ∈ ℤ)       (𝜑 → (𝐴𝑁) ∈ ℝ+)
 
Theoremreexpclzapd 9574 Closure of exponentiation of reals. (Contributed by Jim Kingdon, 13-Jun-2020.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐴 # 0)    &   (𝜑𝑁 ∈ ℤ)       (𝜑 → (𝐴𝑁) ∈ ℝ)
 
Theoremresqcld 9575 Closure of square in reals. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ)       (𝜑 → (𝐴↑2) ∈ ℝ)
 
Theoremsqge0d 9576 A square of a real is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ)       (𝜑 → 0 ≤ (𝐴↑2))
 
Theoremsqgt0apd 9577 The square of a real apart from zero is positive. (Contributed by Jim Kingdon, 13-Jun-2020.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐴 # 0)       (𝜑 → 0 < (𝐴↑2))
 
Theoremleexp2ad 9578 Ordering relationship for exponentiation. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑 → 1 ≤ 𝐴)    &   (𝜑𝑁 ∈ (ℤ𝑀))       (𝜑 → (𝐴𝑀) ≤ (𝐴𝑁))
 
Theoremleexp2rd 9579 Ordering relationship for exponentiation. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝑀 ∈ ℕ0)    &   (𝜑𝑁 ∈ (ℤ𝑀))    &   (𝜑 → 0 ≤ 𝐴)    &   (𝜑𝐴 ≤ 1)       (𝜑 → (𝐴𝑁) ≤ (𝐴𝑀))
 
Theoremlt2sqd 9580 The square function on nonnegative reals is strictly monotonic. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑 → 0 ≤ 𝐴)    &   (𝜑 → 0 ≤ 𝐵)       (𝜑 → (𝐴 < 𝐵 ↔ (𝐴↑2) < (𝐵↑2)))
 
Theoremle2sqd 9581 The square function on nonnegative reals is monotonic. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑 → 0 ≤ 𝐴)    &   (𝜑 → 0 ≤ 𝐵)       (𝜑 → (𝐴𝐵 ↔ (𝐴↑2) ≤ (𝐵↑2)))
 
Theoremsq11d 9582 The square function is one-to-one for nonnegative reals. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑 → 0 ≤ 𝐴)    &   (𝜑 → 0 ≤ 𝐵)    &   (𝜑 → (𝐴↑2) = (𝐵↑2))       (𝜑𝐴 = 𝐵)
 
Theoremsq11ap 9583 Analogue to sq11 9492 but for apartness. (Contributed by Jim Kingdon, 12-Aug-2021.)
(((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((𝐴↑2) # (𝐵↑2) ↔ 𝐴 # 𝐵))
 
Theoremsq10 9584 The square of 10 is 100. (Contributed by AV, 14-Jun-2021.) (Revised by AV, 1-Aug-2021.)
(10↑2) = 100
 
Theoremsq10e99m1 9585 The square of 10 is 99 plus 1. (Contributed by AV, 14-Jun-2021.) (Revised by AV, 1-Aug-2021.)
(10↑2) = (99 + 1)
 
Theorem3dec 9586 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 · 𝐵)) + 𝐶)
 
3.6.6  Ordered pair theorem for nonnegative integers
 
Theoremnn0le2msqd 9587 The square function on nonnegative integers is monotonic. (Contributed by Jim Kingdon, 31-Oct-2021.)
(𝜑𝐴 ∈ ℕ0)    &   (𝜑𝐵 ∈ ℕ0)       (𝜑 → (𝐴𝐵 ↔ (𝐴 · 𝐴) ≤ (𝐵 · 𝐵)))
 
Theoremnn0opthlem1d 9588 A rather pretty lemma for nn0opth2 9592. (Contributed by Jim Kingdon, 31-Oct-2021.)
(𝜑𝐴 ∈ ℕ0)    &   (𝜑𝐶 ∈ ℕ0)       (𝜑 → (𝐴 < 𝐶 ↔ ((𝐴 · 𝐴) + (2 · 𝐴)) < (𝐶 · 𝐶)))
 
Theoremnn0opthlem2d 9589 Lemma for nn0opth2 9592. (Contributed by Jim Kingdon, 31-Oct-2021.)
(𝜑𝐴 ∈ ℕ0)    &   (𝜑𝐵 ∈ ℕ0)    &   (𝜑𝐶 ∈ ℕ0)    &   (𝜑𝐷 ∈ ℕ0)       (𝜑 → ((𝐴 + 𝐵) < 𝐶 → ((𝐶 · 𝐶) + 𝐷) ≠ (((𝐴 + 𝐵) · (𝐴 + 𝐵)) + 𝐵)))
 
Theoremnn0opthd 9590 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 3412 that works for any set. (Contributed by Jim Kingdon, 31-Oct-2021.)
(𝜑𝐴 ∈ ℕ0)    &   (𝜑𝐵 ∈ ℕ0)    &   (𝜑𝐶 ∈ ℕ0)    &   (𝜑𝐷 ∈ ℕ0)       (𝜑 → ((((𝐴 + 𝐵) · (𝐴 + 𝐵)) + 𝐵) = (((𝐶 + 𝐷) · (𝐶 + 𝐷)) + 𝐷) ↔ (𝐴 = 𝐶𝐵 = 𝐷)))
 
Theoremnn0opth2d 9591 An ordered pair theorem for nonnegative integers. Theorem 17.3 of [Quine] p. 124. See comments for nn0opthd 9590. (Contributed by Jim Kingdon, 31-Oct-2021.)
(𝜑𝐴 ∈ ℕ0)    &   (𝜑𝐵 ∈ ℕ0)    &   (𝜑𝐶 ∈ ℕ0)    &   (𝜑𝐷 ∈ ℕ0)       (𝜑 → ((((𝐴 + 𝐵)↑2) + 𝐵) = (((𝐶 + 𝐷)↑2) + 𝐷) ↔ (𝐴 = 𝐶𝐵 = 𝐷)))
 
Theoremnn0opth2 9592 An ordered pair theorem for nonnegative integers. Theorem 17.3 of [Quine] p. 124. See nn0opthd 9590. (Contributed by NM, 22-Jul-2004.)
(((𝐴 ∈ ℕ0𝐵 ∈ ℕ0) ∧ (𝐶 ∈ ℕ0𝐷 ∈ ℕ0)) → ((((𝐴 + 𝐵)↑2) + 𝐵) = (((𝐶 + 𝐷)↑2) + 𝐷) ↔ (𝐴 = 𝐶𝐵 = 𝐷)))
 
3.6.7  Factorial function
 
Syntaxcfa 9593 Extend class notation to include the factorial of nonnegative integers.
class !
 
Definitiondf-fac 9594 Define the factorial function on nonnegative integers. For example, (!‘5) = 120 because 1 · 2 · 3 · 4 · 5 = 120 (ex-fac 10281). In the literature, the factorial function is written as a postscript exclamation point. (Contributed by NM, 2-Dec-2004.)
! = ({⟨0, 1⟩} ∪ seq1( · , I , ℂ))
 
Theoremfacnn 9595 Value of the factorial function for positive integers. (Contributed by NM, 2-Dec-2004.) (Revised by Mario Carneiro, 13-Jul-2013.)
(𝑁 ∈ ℕ → (!‘𝑁) = (seq1( · , I , ℂ)‘𝑁))
 
Theoremfac0 9596 The factorial of 0. (Contributed by NM, 2-Dec-2004.) (Revised by Mario Carneiro, 13-Jul-2013.)
(!‘0) = 1
 
Theoremfac1 9597 The factorial of 1. (Contributed by NM, 2-Dec-2004.) (Revised by Mario Carneiro, 13-Jul-2013.)
(!‘1) = 1
 
Theoremfacp1 9598 The factorial of a successor. (Contributed by NM, 2-Dec-2004.) (Revised by Mario Carneiro, 13-Jul-2013.)
(𝑁 ∈ ℕ0 → (!‘(𝑁 + 1)) = ((!‘𝑁) · (𝑁 + 1)))
 
Theoremfac2 9599 The factorial of 2. (Contributed by NM, 17-Mar-2005.)
(!‘2) = 2
 
Theoremfac3 9600 The factorial of 3. (Contributed by NM, 17-Mar-2005.)
(!‘3) = 6
    < 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-10511
  Copyright terms: Public domain < Previous  Next >