Theorem sq1 14218

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 12629	. 2 ⊢ 2 ∈ ℤ
2		1exp 14114	. 2 ⊢ (2 ∈ ℤ → (1↑2) = 1)
3	1, 2	ax-mp 5	1 ⊢ (1↑2) = 1

Syntax hints:   = wceq 1540   ∈ wcel 2109  (class class class)co 7410  1c1 11135  2c2 12300  ℤcz 12593  ↑cexp 14084

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pow 5340  ax-pr 5407  ax-un 7734  ax-cnex 11190  ax-resscn 11191  ax-1cn 11192  ax-icn 11193  ax-addcl 11194  ax-addrcl 11195  ax-mulcl 11196  ax-mulrcl 11197  ax-mulcom 11198  ax-addass 11199  ax-mulass 11200  ax-distr 11201  ax-i2m1 11202  ax-1ne0 11203  ax-1rid 11204  ax-rnegex 11205  ax-rrecex 11206  ax-cnre 11207  ax-pre-lttri 11208  ax-pre-lttrn 11209  ax-pre-ltadd 11210  ax-pre-mulgt0 11211

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3062  df-rmo 3364  df-reu 3365  df-rab 3421  df-v 3466  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-pss 3951  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-iun 4974  df-br 5125  df-opab 5187  df-mpt 5207  df-tr 5235  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6295  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-om 7867  df-2nd 7994  df-frecs 8285  df-wrecs 8316  df-recs 8390  df-rdg 8429  df-er 8724  df-en 8965  df-dom 8966  df-sdom 8967  df-pnf 11276  df-mnf 11277  df-xr 11278  df-ltxr 11279  df-le 11280  df-sub 11473  df-neg 11474  df-div 11900  df-nn 12246  df-2 12308  df-n0 12507  df-z 12594  df-uz 12858  df-seq 14025  df-exp 14085

This theorem is referenced by:  neg1sqe1  14219  binom21  14242  binom2sub1  14244  sq01  14248  01sqrexlem1  15266  sqrt1  15295  sinbnd  16203  cosbnd  16204  cos1bnd  16210  cos2bnd  16211  cos01gt0  16214  sqnprm  16726  numdensq  16778  zsqrtelqelz  16782  prmreclem1  16941  prmreclem2  16942  4sqlem13  16982  4sqlem19  16988  odadd  19836  abvneg  20791  gzrngunitlem  21405  gzrngunit  21406  zringunit  21432  sinhalfpilem  26429  cos2pi  26442  tangtx  26471  coskpi  26489  tanregt0  26505  efif1olem3  26510  root1id  26721  root1cj  26723  isosctrlem2  26786  asin1  26861  efiatan2  26884  bndatandm  26896  atans2  26898  wilthlem1  27035  dchrinv  27229  sum2dchr  27242  lgslem1  27265  lgsne0  27303  lgssq  27305  lgssq2  27306  1lgs  27308  lgs1  27309  lgsdinn0  27313  lgsquad2lem2  27353  lgsquad3  27355  2lgsoddprmlem3a  27378  2sqlem9  27395  2sqlem10  27396  2sqlem11  27397  2sqblem  27399  2sqb  27400  2sq2  27401  addsqn2reu  27409  addsqrexnreu  27410  addsq2nreurex  27412  mulog2sumlem2  27503  pntlemb  27565  axlowdimlem16  28941  ex-pr  30416  normlem1  31096  kbpj  31942  hstnmoc  32209  hstle1  32212  hst1h  32213  hstle  32216  strlem3a  32238  strlem4  32240  strlem5  32241  jplem1  32254  iconstr  33805  cos9thpiminplylem1  33821  cos9thpinconstrlem1  33828  dvasin  37733  dvacos  37734  areacirclem1  37737  areacirc  37742  cntotbnd  37825  3cubeslem1  42674  3cubeslem2  42675  3cubeslem3r  42677  pell1qrge1  42860  pell1qr1  42861  pell1qrgaplem  42863  pell14qrgapw  42866  pellqrex  42869  rmspecnonsq  42897  rmspecfund  42899  rmspecpos  42907  sqrtcval  43632  stoweidlem1  45997  wallispi2lem2  46068  stirlinglem10  46079  lighneallem2  47587  onetansqsecsq  49592  cotsqcscsq  49593