Theorem sq1 14148

Description: The square of 1 is 1. (Contributed by NM, 22-Aug-1999.)

Assertion

Ref	Expression
sq1	⊢ (1↑2) = 1

Proof of Theorem sq1

Step	Hyp	Ref	Expression
1		2z 12550	. 2 ⊢ 2 ∈ ℤ
2		1exp 14044	. 2 ⊢ (2 ∈ ℤ → (1↑2) = 1)
3	1, 2	ax-mp 5	1 ⊢ (1↑2) = 1

Syntax hints:   = wceq 1547   ∈ wcel 2119  (class class class)co 7356  1c1 11030  2c2 12227  ℤcz 12515  ↑cexp 14014

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678  ax-cnex 11085  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105  ax-pre-mulgt0 11106

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-nel 3039  df-ral 3054  df-rex 3064  df-rmo 3344  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-iun 4923  df-br 5073  df-opab 5135  df-mpt 5154  df-tr 5180  df-id 5513  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5571  df-we 5573  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-pred 6252  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-om 7807  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-er 8633  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371  df-div 11799  df-nn 12166  df-2 12235  df-n0 12429  df-z 12516  df-uz 12780  df-seq 13955  df-exp 14015

This theorem is referenced by:  neg1sqe1  14149  binom21  14172  binom2sub1  14174  sq01  14178  01sqrexlem1  15195  sqrt1  15224  sinbnd  16138  cosbnd  16139  cos1bnd  16145  cos2bnd  16146  cos01gt0  16149  sqnprm  16663  numdensq  16715  zsqrtelqelz  16719  prmreclem1  16878  prmreclem2  16879  4sqlem13  16919  4sqlem19  16925  odadd  19816  abvneg  20798  gzrngunitlem  21407  gzrngunit  21408  zringunit  21441  sinhalfpilem  26445  cos2pi  26458  tangtx  26487  coskpi  26505  tanregt0  26521  efif1olem3  26526  root1id  26736  root1cj  26738  isosctrlem2  26801  asin1  26876  efiatan2  26899  bndatandm  26911  atans2  26913  wilthlem1  27049  dchrinv  27242  sum2dchr  27255  lgslem1  27278  lgsne0  27316  lgssq  27318  lgssq2  27319  1lgs  27321  lgs1  27322  lgsdinn0  27326  lgsquad2lem2  27366  lgsquad3  27368  2lgsoddprmlem3a  27391  2sqlem9  27408  2sqlem10  27409  2sqlem11  27410  2sqblem  27412  2sqb  27413  2sq2  27414  addsqn2reu  27422  addsqrexnreu  27423  addsq2nreurex  27425  mulog2sumlem2  27516  pntlemb  27578  axlowdimlem16  29044  ex-pr  30518  normlem1  31199  kbpj  32045  hstnmoc  32312  hstle1  32315  hst1h  32316  hstle  32319  strlem3a  32341  strlem4  32343  strlem5  32344  jplem1  32357  iconstr  33950  cos9thpiminplylem1  33966  cos9thpinconstrlem1  33973  dvasin  38071  dvacos  38072  areacirclem1  38075  areacirc  38080  cntotbnd  38163  3cubeslem1  43133  3cubeslem2  43134  3cubeslem3r  43136  pell1qrge1  43315  pell1qr1  43316  pell1qrgaplem  43318  pell14qrgapw  43321  pellqrex  43324  rmspecnonsq  43352  rmspecfund  43354  rmspecpos  43361  sqrtcval  44085  stoweidlem1  46444  wallispi2lem2  46515  stirlinglem10  46526  sin5tlem2  47337  lighneallem2  48084  onetansqsecsq  50251  cotsqcscsq  50252