HomeHome Intuitionistic Logic Explorer
Theorem List (p. 107 of 152) 		< 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 - 10601-10700   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremresqcl 10601 Closure of the square of a real number. (Contributed by NM, 18-Oct-1999.)
(𝐴 ∈ ℝ β†’ (𝐴↑2) ∈ ℝ)
 
Theoremsqgt0ap 10602 The square of a nonzero real is positive. (Contributed by Jim Kingdon, 11-Jun-2020.)
((𝐴 ∈ ℝ ∧ 𝐴 # 0) β†’ 0 < (𝐴↑2))
 
Theoremnnsqcl 10603 The naturals are closed under squaring. (Contributed by Scott Fenton, 29-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
(𝐴 ∈ β„• β†’ (𝐴↑2) ∈ β„•)
 
Theoremzsqcl 10604 Integers are closed under squaring. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
(𝐴 ∈ β„€ β†’ (𝐴↑2) ∈ β„€)
 
Theoremqsqcl 10605 The square of a rational is rational. (Contributed by Stefan O'Rear, 15-Sep-2014.)
(𝐴 ∈ β„š β†’ (𝐴↑2) ∈ β„š)
 
Theoremsq11 10606 The square function is one-to-one for nonnegative reals. Also see sq11ap 10701 which would easily follow from this given excluded middle, but which for us is proved another way. (Contributed by NM, 8-Apr-2001.) (Proof shortened by Mario Carneiro, 28-May-2016.)
(((𝐴 ∈ ℝ ∧ 0 ≀ 𝐴) ∧ (𝐡 ∈ ℝ ∧ 0 ≀ 𝐡)) β†’ ((𝐴↑2) = (𝐡↑2) ↔ 𝐴 = 𝐡))
 
Theoremlt2sq 10607 The square function on nonnegative reals is strictly monotonic. (Contributed by NM, 24-Feb-2006.)
(((𝐴 ∈ ℝ ∧ 0 ≀ 𝐴) ∧ (𝐡 ∈ ℝ ∧ 0 ≀ 𝐡)) β†’ (𝐴 < 𝐡 ↔ (𝐴↑2) < (𝐡↑2)))
 
Theoremle2sq 10608 The square function on nonnegative reals is monotonic. (Contributed by NM, 18-Oct-1999.)
(((𝐴 ∈ ℝ ∧ 0 ≀ 𝐴) ∧ (𝐡 ∈ ℝ ∧ 0 ≀ 𝐡)) β†’ (𝐴 ≀ 𝐡 ↔ (𝐴↑2) ≀ (𝐡↑2)))
 
Theoremle2sq2 10609 The square of a 'less than or equal to' ordering. (Contributed by NM, 21-Mar-2008.)
(((𝐴 ∈ ℝ ∧ 0 ≀ 𝐴) ∧ (𝐡 ∈ ℝ ∧ 𝐴 ≀ 𝐡)) β†’ (𝐴↑2) ≀ (𝐡↑2))
 
Theoremsqge0 10610 A square of a real is nonnegative. (Contributed by NM, 18-Oct-1999.)
(𝐴 ∈ ℝ β†’ 0 ≀ (𝐴↑2))
 
Theoremzsqcl2 10611 The square of an integer is a nonnegative integer. (Contributed by Mario Carneiro, 18-Apr-2014.) (Revised by Mario Carneiro, 14-Jul-2014.)
(𝐴 ∈ β„€ β†’ (𝐴↑2) ∈ β„•0)
 
Theoremsumsqeq0 10612 Two real numbers are equal to 0 iff their Euclidean norm is. (Contributed by NM, 29-Apr-2005.) (Revised by Stefan O'Rear, 5-Oct-2014.) (Proof shortened by Mario Carneiro, 28-May-2016.)
((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ) β†’ ((𝐴 = 0 ∧ 𝐡 = 0) ↔ ((𝐴↑2) + (𝐡↑2)) = 0))
 
Theoremsqvali 10613 Value of square. Inference version. (Contributed by NM, 1-Aug-1999.)
𝐴 ∈ β„‚    β‡’   (𝐴↑2) = (𝐴 Β· 𝐴)
 
Theoremsqcli 10614 Closure of square. (Contributed by NM, 2-Aug-1999.)
𝐴 ∈ β„‚    β‡’   (𝐴↑2) ∈ β„‚
 
Theoremsqeq0i 10615 A number is zero iff its square is zero. (Contributed by NM, 2-Oct-1999.)
𝐴 ∈ β„‚    β‡’   ((𝐴↑2) = 0 ↔ 𝐴 = 0)
 
Theoremsqmuli 10616 Distribution of square over multiplication. (Contributed by NM, 3-Sep-1999.)
𝐴 ∈ β„‚    &   π΅ ∈ β„‚    β‡’   ((𝐴 Β· 𝐡)↑2) = ((𝐴↑2) Β· (𝐡↑2))
 
Theoremsqdivapi 10617 Distribution of square over division. (Contributed by Jim Kingdon, 12-Jun-2020.)
𝐴 ∈ β„‚    &   π΅ ∈ β„‚    &   π΅ # 0    β‡’   ((𝐴 / 𝐡)↑2) = ((𝐴↑2) / (𝐡↑2))
 
Theoremresqcli 10618 Closure of square in reals. (Contributed by NM, 2-Aug-1999.)
𝐴 ∈ ℝ    β‡’   (𝐴↑2) ∈ ℝ
 
Theoremsqgt0api 10619 The square of a nonzero real is positive. (Contributed by Jim Kingdon, 12-Jun-2020.)
𝐴 ∈ ℝ    β‡’   (𝐴 # 0 β†’ 0 < (𝐴↑2))
 
Theoremsqge0i 10620 A square of a real is nonnegative. (Contributed by NM, 3-Aug-1999.)
𝐴 ∈ ℝ    β‡’   0 ≀ (𝐴↑2)
 
Theoremlt2sqi 10621 The square function on nonnegative reals is strictly monotonic. (Contributed by NM, 12-Sep-1999.)
𝐴 ∈ ℝ    &   π΅ ∈ ℝ    β‡’   ((0 ≀ 𝐴 ∧ 0 ≀ 𝐡) β†’ (𝐴 < 𝐡 ↔ (𝐴↑2) < (𝐡↑2)))
 
Theoremle2sqi 10622 The square function on nonnegative reals is monotonic. (Contributed by NM, 12-Sep-1999.)
𝐴 ∈ ℝ    &   π΅ ∈ ℝ    β‡’   ((0 ≀ 𝐴 ∧ 0 ≀ 𝐡) β†’ (𝐴 ≀ 𝐡 ↔ (𝐴↑2) ≀ (𝐡↑2)))
 
Theoremsq11i 10623 The square function is one-to-one for nonnegative reals. (Contributed by NM, 27-Oct-1999.)
𝐴 ∈ ℝ    &   π΅ ∈ ℝ    β‡’   ((0 ≀ 𝐴 ∧ 0 ≀ 𝐡) β†’ ((𝐴↑2) = (𝐡↑2) ↔ 𝐴 = 𝐡))
 
Theoremsq0 10624 The square of 0 is 0. (Contributed by NM, 6-Jun-2006.)
(0↑2) = 0
 
Theoremsq0i 10625 If a number is zero, its square is zero. (Contributed by FL, 10-Dec-2006.)
(𝐴 = 0 β†’ (𝐴↑2) = 0)
 
Theoremsq0id 10626 If a number is zero, its square is zero. Deduction form of sq0i 10625. Converse of sqeq0d 10666. (Contributed by David Moews, 28-Feb-2017.)
(πœ‘ β†’ 𝐴 = 0)    β‡’   (πœ‘ β†’ (𝐴↑2) = 0)
 
Theoremsq1 10627 The square of 1 is 1. (Contributed by NM, 22-Aug-1999.)
(1↑2) = 1
 
Theoremneg1sqe1 10628 -1 squared is 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
(-1↑2) = 1
 
Theoremsq2 10629 The square of 2 is 4. (Contributed by NM, 22-Aug-1999.)
(2↑2) = 4
 
Theoremsq3 10630 The square of 3 is 9. (Contributed by NM, 26-Apr-2006.)
(3↑2) = 9
 
Theoremsq4e2t8 10631 The square of 4 is 2 times 8. (Contributed by AV, 20-Jul-2021.)
(4↑2) = (2 Β· 8)
 
Theoremcu2 10632 The cube of 2 is 8. (Contributed by NM, 2-Aug-2004.)
(2↑3) = 8
 
Theoremirec 10633 The reciprocal of i. (Contributed by NM, 11-Oct-1999.)
(1 / i) = -i
 
Theoremi2 10634 i squared. (Contributed by NM, 6-May-1999.)
(i↑2) = -1
 
Theoremi3 10635 i cubed. (Contributed by NM, 31-Jan-2007.)
(i↑3) = -i
 
Theoremi4 10636 i to the fourth power. (Contributed by NM, 31-Jan-2007.)
(i↑4) = 1
 
Theoremnnlesq 10637 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 10638 Taking i to the 𝐾-th power is the same as using the 𝐾 mod 4 -th power instead, by i4 10636. (Contributed by Mario Carneiro, 7-Jul-2014.)
(𝐾 ∈ β„€ β†’ (i↑(𝐾 mod 4)) = (i↑𝐾))
 
Theoremexpnass 10639 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 10640 Factor the difference of two squares. (Contributed by NM, 21-Feb-2008.)
((𝐴 ∈ β„‚ ∧ 𝐡 ∈ β„‚) β†’ ((𝐴↑2) βˆ’ (𝐡↑2)) = ((𝐴 + 𝐡) Β· (𝐴 βˆ’ 𝐡)))
 
Theoremsubsq2 10641 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 10642 The square of a binomial. (Contributed by NM, 11-Aug-1999.)
𝐴 ∈ β„‚    &   π΅ ∈ β„‚    β‡’   ((𝐴 + 𝐡)↑2) = (((𝐴↑2) + (2 Β· (𝐴 Β· 𝐡))) + (𝐡↑2))
 
Theoremsubsqi 10643 Factor the difference of two squares. (Contributed by NM, 7-Feb-2005.)
𝐴 ∈ β„‚    &   π΅ ∈ β„‚    β‡’   ((𝐴↑2) βˆ’ (𝐡↑2)) = ((𝐴 + 𝐡) Β· (𝐴 βˆ’ 𝐡))
 
Theoremqsqeqor 10644 The squares of two rational numbers are equal iff one number equals the other or its negative. (Contributed by Jim Kingdon, 1-Nov-2024.)
((𝐴 ∈ β„š ∧ 𝐡 ∈ β„š) β†’ ((𝐴↑2) = (𝐡↑2) ↔ (𝐴 = 𝐡 ∨ 𝐴 = -𝐡)))
 
Theorembinom2 10645 The square of a binomial. (Contributed by FL, 10-Dec-2006.)
((𝐴 ∈ β„‚ ∧ 𝐡 ∈ β„‚) β†’ ((𝐴 + 𝐡)↑2) = (((𝐴↑2) + (2 Β· (𝐴 Β· 𝐡))) + (𝐡↑2)))
 
Theorembinom21 10646 Special case of binom2 10645 where 𝐡 = 1. (Contributed by Scott Fenton, 11-May-2014.)
(𝐴 ∈ β„‚ β†’ ((𝐴 + 1)↑2) = (((𝐴↑2) + (2 Β· 𝐴)) + 1))
 
Theorembinom2sub 10647 Expand the square of a subtraction. (Contributed by Scott Fenton, 10-Jun-2013.)
((𝐴 ∈ β„‚ ∧ 𝐡 ∈ β„‚) β†’ ((𝐴 βˆ’ 𝐡)↑2) = (((𝐴↑2) βˆ’ (2 Β· (𝐴 Β· 𝐡))) + (𝐡↑2)))
 
Theorembinom2sub1 10648 Special case of binom2sub 10647 where 𝐡 = 1. (Contributed by AV, 2-Aug-2021.)
(𝐴 ∈ β„‚ β†’ ((𝐴 βˆ’ 1)↑2) = (((𝐴↑2) βˆ’ (2 Β· 𝐴)) + 1))
 
Theorembinom2subi 10649 Expand the square of a subtraction. (Contributed by Scott Fenton, 13-Jun-2013.)
𝐴 ∈ β„‚    &   π΅ ∈ β„‚    β‡’   ((𝐴 βˆ’ 𝐡)↑2) = (((𝐴↑2) βˆ’ (2 Β· (𝐴 Β· 𝐡))) + (𝐡↑2))
 
Theoremmulbinom2 10650 The square of a binomial with factor. (Contributed by AV, 19-Jul-2021.)
((𝐴 ∈ β„‚ ∧ 𝐡 ∈ β„‚ ∧ 𝐢 ∈ β„‚) β†’ (((𝐢 Β· 𝐴) + 𝐡)↑2) = ((((𝐢 Β· 𝐴)↑2) + ((2 Β· 𝐢) Β· (𝐴 Β· 𝐡))) + (𝐡↑2)))
 
Theorembinom3 10651 The cube of a binomial. (Contributed by Mario Carneiro, 24-Apr-2015.)
((𝐴 ∈ β„‚ ∧ 𝐡 ∈ β„‚) β†’ ((𝐴 + 𝐡)↑3) = (((𝐴↑3) + (3 Β· ((𝐴↑2) Β· 𝐡))) + ((3 Β· (𝐴 Β· (𝐡↑2))) + (𝐡↑3))))
 
Theoremzesq 10652 An integer is even iff its square is even. (Contributed by Mario Carneiro, 12-Sep-2015.)
(𝑁 ∈ β„€ β†’ ((𝑁 / 2) ∈ β„€ ↔ ((𝑁↑2) / 2) ∈ β„€))
 
Theoremnnesq 10653 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 10654 Bernoulli's inequality, due to Johan Bernoulli (1667-1748). (Contributed by NM, 21-Feb-2005.)
((𝐴 ∈ ℝ ∧ 𝑁 ∈ β„•0 ∧ -1 ≀ 𝐴) β†’ (1 + (𝐴 Β· 𝑁)) ≀ ((1 + 𝐴)↑𝑁))
 
Theorembernneq2 10655 Variation of Bernoulli's inequality bernneq 10654. (Contributed by NM, 18-Oct-2007.)
((𝐴 ∈ ℝ ∧ 𝑁 ∈ β„•0 ∧ 0 ≀ 𝐴) β†’ (((𝐴 βˆ’ 1) Β· 𝑁) + 1) ≀ (𝐴↑𝑁))
 
Theorembernneq3 10656 A corollary of bernneq 10654. (Contributed by Mario Carneiro, 11-Mar-2014.)
((𝑃 ∈ (β„€β‰₯β€˜2) ∧ 𝑁 ∈ β„•0) β†’ 𝑁 < (𝑃↑𝑁))
 
Theoremexpnbnd 10657* Exponentiation with a base greater than 1 has no upper bound. (Contributed by NM, 20-Oct-2007.)
((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ ∧ 1 < 𝐡) β†’ βˆƒπ‘˜ ∈ β„• 𝐴 < (π΅β†‘π‘˜))
 
Theoremexpnlbnd 10658* The reciprocal of exponentiation with a base greater than 1 has no positive lower bound. (Contributed by NM, 18-Jul-2008.)
((𝐴 ∈ ℝ+ ∧ 𝐡 ∈ ℝ ∧ 1 < 𝐡) β†’ βˆƒπ‘˜ ∈ β„• (1 / (π΅β†‘π‘˜)) < 𝐴)
 
Theoremexpnlbnd2 10659* 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 / (π΅β†‘π‘˜)) < 𝐴)
 
Theoremmodqexp 10660 Exponentiation property of the modulo operation, see theorem 5.2(c) in [ApostolNT] p. 107. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 7-Sep-2024.)
(πœ‘ β†’ 𝐴 ∈ β„€)    &   (πœ‘ β†’ 𝐡 ∈ β„€)    &   (πœ‘ β†’ 𝐢 ∈ β„•0)    &   (πœ‘ β†’ 𝐷 ∈ β„š)    &   (πœ‘ β†’ 0 < 𝐷)    &   (πœ‘ β†’ (𝐴 mod 𝐷) = (𝐡 mod 𝐷))    β‡’   (πœ‘ β†’ ((𝐴↑𝐢) mod 𝐷) = ((𝐡↑𝐢) mod 𝐷))
 
Theoremexp0d 10661 Value of a complex number raised to the 0th power. (Contributed by Mario Carneiro, 28-May-2016.)
(πœ‘ β†’ 𝐴 ∈ β„‚)    β‡’   (πœ‘ β†’ (𝐴↑0) = 1)
 
Theoremexp1d 10662 Value of a complex number raised to the first power. (Contributed by Mario Carneiro, 28-May-2016.)
(πœ‘ β†’ 𝐴 ∈ β„‚)    β‡’   (πœ‘ β†’ (𝐴↑1) = 𝐴)
 
Theoremexpeq0d 10663 Positive integer exponentiation is 0 iff its base is 0. (Contributed by Mario Carneiro, 28-May-2016.)
(πœ‘ β†’ 𝐴 ∈ β„‚)    &   (πœ‘ β†’ 𝑁 ∈ β„•)    &   (πœ‘ β†’ (𝐴↑𝑁) = 0)    β‡’   (πœ‘ β†’ 𝐴 = 0)
 
Theoremsqvald 10664 Value of square. Inference version. (Contributed by Mario Carneiro, 28-May-2016.)
(πœ‘ β†’ 𝐴 ∈ β„‚)    β‡’   (πœ‘ β†’ (𝐴↑2) = (𝐴 Β· 𝐴))
 
Theoremsqcld 10665 Closure of square. (Contributed by Mario Carneiro, 28-May-2016.)
(πœ‘ β†’ 𝐴 ∈ β„‚)    β‡’   (πœ‘ β†’ (𝐴↑2) ∈ β„‚)
 
Theoremsqeq0d 10666 A number is zero iff its square is zero. (Contributed by Mario Carneiro, 28-May-2016.)
(πœ‘ β†’ 𝐴 ∈ β„‚)    &   (πœ‘ β†’ (𝐴↑2) = 0)    β‡’   (πœ‘ β†’ 𝐴 = 0)
 
Theoremexpcld 10667 Closure law for nonnegative integer exponentiation. (Contributed by Mario Carneiro, 28-May-2016.)
(πœ‘ β†’ 𝐴 ∈ β„‚)    &   (πœ‘ β†’ 𝑁 ∈ β„•0)    β‡’   (πœ‘ β†’ (𝐴↑𝑁) ∈ β„‚)
 
Theoremexpp1d 10668 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 10669 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 10670 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 10671 Square of reciprocal. (Contributed by Jim Kingdon, 12-Jun-2020.)
(πœ‘ β†’ 𝐴 ∈ β„‚)    &   (πœ‘ β†’ 𝐴 # 0)    β‡’   (πœ‘ β†’ ((1 / 𝐴)↑2) = (1 / (𝐴↑2)))
 
Theoremexpclzapd 10672 Closure law for integer exponentiation. (Contributed by Jim Kingdon, 12-Jun-2020.)
(πœ‘ β†’ 𝐴 ∈ β„‚)    &   (πœ‘ β†’ 𝐴 # 0)    &   (πœ‘ β†’ 𝑁 ∈ β„€)    β‡’   (πœ‘ β†’ (𝐴↑𝑁) ∈ β„‚)
 
Theoremexpap0d 10673 Nonnegative integer exponentiation is nonzero if its base is nonzero. (Contributed by Jim Kingdon, 12-Jun-2020.)
(πœ‘ β†’ 𝐴 ∈ β„‚)    &   (πœ‘ β†’ 𝐴 # 0)    &   (πœ‘ β†’ 𝑁 ∈ β„€)    β‡’   (πœ‘ β†’ (𝐴↑𝑁) # 0)
 
Theoremexpnegapd 10674 Value of a complex number raised to a negative power. (Contributed by Jim Kingdon, 12-Jun-2020.)
(πœ‘ β†’ 𝐴 ∈ β„‚)    &   (πœ‘ β†’ 𝐴 # 0)    &   (πœ‘ β†’ 𝑁 ∈ β„€)    β‡’   (πœ‘ β†’ (𝐴↑-𝑁) = (1 / (𝐴↑𝑁)))
 
Theoremexprecapd 10675 Nonnegative integer exponentiation of a reciprocal. (Contributed by Jim Kingdon, 12-Jun-2020.)
(πœ‘ β†’ 𝐴 ∈ β„‚)    &   (πœ‘ β†’ 𝐴 # 0)    &   (πœ‘ β†’ 𝑁 ∈ β„€)    β‡’   (πœ‘ β†’ ((1 / 𝐴)↑𝑁) = (1 / (𝐴↑𝑁)))
 
Theoremexpp1zapd 10676 Value of a nonzero complex number raised to an integer power plus one. (Contributed by Jim Kingdon, 12-Jun-2020.)
(πœ‘ β†’ 𝐴 ∈ β„‚)    &   (πœ‘ β†’ 𝐴 # 0)    &   (πœ‘ β†’ 𝑁 ∈ β„€)    β‡’   (πœ‘ β†’ (𝐴↑(𝑁 + 1)) = ((𝐴↑𝑁) Β· 𝐴))
 
Theoremexpm1apd 10677 Value of a complex number raised to an integer power minus one. (Contributed by Jim Kingdon, 12-Jun-2020.)
(πœ‘ β†’ 𝐴 ∈ β„‚)    &   (πœ‘ β†’ 𝐴 # 0)    &   (πœ‘ β†’ 𝑁 ∈ β„€)    β‡’   (πœ‘ β†’ (𝐴↑(𝑁 βˆ’ 1)) = ((𝐴↑𝑁) / 𝐴))
 
Theoremexpsubapd 10678 Exponent subtraction law for nonnegative integer exponentiation. (Contributed by Jim Kingdon, 12-Jun-2020.)
(πœ‘ β†’ 𝐴 ∈ β„‚)    &   (πœ‘ β†’ 𝐴 # 0)    &   (πœ‘ β†’ 𝑁 ∈ β„€)    &   (πœ‘ β†’ 𝑀 ∈ β„€)    β‡’   (πœ‘ β†’ (𝐴↑(𝑀 βˆ’ 𝑁)) = ((𝐴↑𝑀) / (𝐴↑𝑁)))
 
Theoremsqmuld 10679 Distribution of square over multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
(πœ‘ β†’ 𝐴 ∈ β„‚)    &   (πœ‘ β†’ 𝐡 ∈ β„‚)    β‡’   (πœ‘ β†’ ((𝐴 Β· 𝐡)↑2) = ((𝐴↑2) Β· (𝐡↑2)))
 
Theoremsqdivapd 10680 Distribution of square over division. (Contributed by Jim Kingdon, 13-Jun-2020.)
(πœ‘ β†’ 𝐴 ∈ β„‚)    &   (πœ‘ β†’ 𝐡 ∈ β„‚)    &   (πœ‘ β†’ 𝐡 # 0)    β‡’   (πœ‘ β†’ ((𝐴 / 𝐡)↑2) = ((𝐴↑2) / (𝐡↑2)))
 
Theoremexpdivapd 10681 Nonnegative integer exponentiation of a quotient. (Contributed by Jim Kingdon, 13-Jun-2020.)
(πœ‘ β†’ 𝐴 ∈ β„‚)    &   (πœ‘ β†’ 𝐡 ∈ β„‚)    &   (πœ‘ β†’ 𝐡 # 0)    &   (πœ‘ β†’ 𝑁 ∈ β„•0)    β‡’   (πœ‘ β†’ ((𝐴 / 𝐡)↑𝑁) = ((𝐴↑𝑁) / (𝐡↑𝑁)))
 
Theoremmulexpd 10682 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 10683 Value of zero raised to a positive integer power. (Contributed by Mario Carneiro, 28-May-2016.)
(πœ‘ β†’ 𝑁 ∈ β„•)    β‡’   (πœ‘ β†’ (0↑𝑁) = 0)
 
Theoremreexpcld 10684 Closure of exponentiation of reals. (Contributed by Mario Carneiro, 28-May-2016.)
(πœ‘ β†’ 𝐴 ∈ ℝ)    &   (πœ‘ β†’ 𝑁 ∈ β„•0)    β‡’   (πœ‘ β†’ (𝐴↑𝑁) ∈ ℝ)
 
Theoremexpge0d 10685 A nonnegative real raised to a nonnegative integer is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)
(πœ‘ β†’ 𝐴 ∈ ℝ)    &   (πœ‘ β†’ 𝑁 ∈ β„•0)    &   (πœ‘ β†’ 0 ≀ 𝐴)    β‡’   (πœ‘ β†’ 0 ≀ (𝐴↑𝑁))
 
Theoremexpge1d 10686 A real greater than or equal to 1 raised to a nonnegative integer is greater than or equal to 1. (Contributed by Mario Carneiro, 28-May-2016.)
(πœ‘ β†’ 𝐴 ∈ ℝ)    &   (πœ‘ β†’ 𝑁 ∈ β„•0)    &   (πœ‘ β†’ 1 ≀ 𝐴)    β‡’   (πœ‘ β†’ 1 ≀ (𝐴↑𝑁))
 
Theoremsqoddm1div8 10687 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 10688 The naturals are closed under squaring. (Contributed by Mario Carneiro, 28-May-2016.)
(πœ‘ β†’ 𝐴 ∈ β„•)    β‡’   (πœ‘ β†’ (𝐴↑2) ∈ β„•)
 
Theoremnnexpcld 10689 Closure of exponentiation of nonnegative integers. (Contributed by Mario Carneiro, 28-May-2016.)
(πœ‘ β†’ 𝐴 ∈ β„•)    &   (πœ‘ β†’ 𝑁 ∈ β„•0)    β‡’   (πœ‘ β†’ (𝐴↑𝑁) ∈ β„•)
 
Theoremnn0expcld 10690 Closure of exponentiation of nonnegative integers. (Contributed by Mario Carneiro, 28-May-2016.)
(πœ‘ β†’ 𝐴 ∈ β„•0)    &   (πœ‘ β†’ 𝑁 ∈ β„•0)    β‡’   (πœ‘ β†’ (𝐴↑𝑁) ∈ β„•0)
 
Theoremrpexpcld 10691 Closure law for exponentiation of positive reals. (Contributed by Mario Carneiro, 28-May-2016.)
(πœ‘ β†’ 𝐴 ∈ ℝ+)    &   (πœ‘ β†’ 𝑁 ∈ β„€)    β‡’   (πœ‘ β†’ (𝐴↑𝑁) ∈ ℝ+)
 
Theoremreexpclzapd 10692 Closure of exponentiation of reals. (Contributed by Jim Kingdon, 13-Jun-2020.)
(πœ‘ β†’ 𝐴 ∈ ℝ)    &   (πœ‘ β†’ 𝐴 # 0)    &   (πœ‘ β†’ 𝑁 ∈ β„€)    β‡’   (πœ‘ β†’ (𝐴↑𝑁) ∈ ℝ)
 
Theoremresqcld 10693 Closure of square in reals. (Contributed by Mario Carneiro, 28-May-2016.)
(πœ‘ β†’ 𝐴 ∈ ℝ)    β‡’   (πœ‘ β†’ (𝐴↑2) ∈ ℝ)
 
Theoremsqge0d 10694 A square of a real is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)
(πœ‘ β†’ 𝐴 ∈ ℝ)    β‡’   (πœ‘ β†’ 0 ≀ (𝐴↑2))
 
Theoremsqgt0apd 10695 The square of a real apart from zero is positive. (Contributed by Jim Kingdon, 13-Jun-2020.)
(πœ‘ β†’ 𝐴 ∈ ℝ)    &   (πœ‘ β†’ 𝐴 # 0)    β‡’   (πœ‘ β†’ 0 < (𝐴↑2))
 
Theoremleexp2ad 10696 Ordering relationship for exponentiation. (Contributed by Mario Carneiro, 28-May-2016.)
(πœ‘ β†’ 𝐴 ∈ ℝ)    &   (πœ‘ β†’ 1 ≀ 𝐴)    &   (πœ‘ β†’ 𝑁 ∈ (β„€β‰₯β€˜π‘€))    β‡’   (πœ‘ β†’ (𝐴↑𝑀) ≀ (𝐴↑𝑁))
 
Theoremleexp2rd 10697 Ordering relationship for exponentiation. (Contributed by Mario Carneiro, 28-May-2016.)
(πœ‘ β†’ 𝐴 ∈ ℝ)    &   (πœ‘ β†’ 𝑀 ∈ β„•0)    &   (πœ‘ β†’ 𝑁 ∈ (β„€β‰₯β€˜π‘€))    &   (πœ‘ β†’ 0 ≀ 𝐴)    &   (πœ‘ β†’ 𝐴 ≀ 1)    β‡’   (πœ‘ β†’ (𝐴↑𝑁) ≀ (𝐴↑𝑀))
 
Theoremlt2sqd 10698 The square function on nonnegative reals is strictly monotonic. (Contributed by Mario Carneiro, 28-May-2016.)
(πœ‘ β†’ 𝐴 ∈ ℝ)    &   (πœ‘ β†’ 𝐡 ∈ ℝ)    &   (πœ‘ β†’ 0 ≀ 𝐴)    &   (πœ‘ β†’ 0 ≀ 𝐡)    β‡’   (πœ‘ β†’ (𝐴 < 𝐡 ↔ (𝐴↑2) < (𝐡↑2)))
 
Theoremle2sqd 10699 The square function on nonnegative reals is monotonic. (Contributed by Mario Carneiro, 28-May-2016.)
(πœ‘ β†’ 𝐴 ∈ ℝ)    &   (πœ‘ β†’ 𝐡 ∈ ℝ)    &   (πœ‘ β†’ 0 ≀ 𝐴)    &   (πœ‘ β†’ 0 ≀ 𝐡)    β‡’   (πœ‘ β†’ (𝐴 ≀ 𝐡 ↔ (𝐴↑2) ≀ (𝐡↑2)))
 
Theoremsq11d 10700 The square function is one-to-one for nonnegative reals. (Contributed by Mario Carneiro, 28-May-2016.)
(πœ‘ β†’ 𝐴 ∈ ℝ)    &   (πœ‘ β†’ 𝐡 ∈ ℝ)    &   (πœ‘ β†’ 0 ≀ 𝐴)    &   (πœ‘ β†’ 0 ≀ 𝐡)    &   (πœ‘ β†’ (𝐴↑2) = (𝐡↑2))    β‡’   (πœ‘ β†’ 𝐴 = 𝐡)
    < 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-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13700 138 13701-13800 139 13801-13900 140 13901-14000 141 14001-14100 142 14101-14200 143 14201-14300 144 14301-14400 145 14401-14500 146 14501-14600 147 14601-14700 148 14701-14800 149 14801-14900 150 14901-15000 151 15001-15100 152 15101-15104
  Copyright terms: Public domain < Previous  Next >