Theorem sq1 14156

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

Syntax hints:   = wceq 1533   ∈ wcel 2098  (class class class)co 7401  1c1 11107  2c2 12264  ℤcz 12555  ↑cexp 14024

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-iun 4989  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7357  df-ov 7404  df-oprab 7405  df-mpo 7406  df-om 7849  df-2nd 7969  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-er 8699  df-en 8936  df-dom 8937  df-sdom 8938  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11443  df-neg 11444  df-div 11869  df-nn 12210  df-2 12272  df-n0 12470  df-z 12556  df-uz 12820  df-seq 13964  df-exp 14025

This theorem is referenced by:  neg1sqe1  14157  binom21  14179  binom2sub1  14181  sq01  14185  01sqrexlem1  15186  sqrt1  15215  sinbnd  16120  cosbnd  16121  cos1bnd  16127  cos2bnd  16128  cos01gt0  16131  sqnprm  16636  numdensq  16689  zsqrtelqelz  16693  prmreclem1  16848  prmreclem2  16849  4sqlem13  16889  4sqlem19  16895  odadd  19760  abvneg  20667  gzrngunitlem  21294  gzrngunit  21295  zringunit  21321  sinhalfpilem  26315  cos2pi  26328  tangtx  26357  coskpi  26374  tanregt0  26390  efif1olem3  26395  root1id  26605  root1cj  26607  isosctrlem2  26667  asin1  26742  efiatan2  26765  bndatandm  26777  atans2  26779  wilthlem1  26916  dchrinv  27110  sum2dchr  27123  lgslem1  27146  lgsne0  27184  lgssq  27186  lgssq2  27187  1lgs  27189  lgs1  27190  lgsdinn0  27194  lgsquad2lem2  27234  lgsquad3  27236  2lgsoddprmlem3a  27259  2sqlem9  27276  2sqlem10  27277  2sqlem11  27278  2sqblem  27280  2sqb  27281  2sq2  27282  addsqn2reu  27290  addsqrexnreu  27291  addsq2nreurex  27293  mulog2sumlem2  27384  pntlemb  27446  axlowdimlem16  28684  ex-pr  30152  normlem1  30832  kbpj  31678  hstnmoc  31945  hstle1  31948  hst1h  31949  hstle  31952  strlem3a  31974  strlem4  31976  strlem5  31977  jplem1  31990  dvasin  37062  dvacos  37063  areacirclem1  37066  areacirc  37071  cntotbnd  37154  3cubeslem1  41911  3cubeslem2  41912  3cubeslem3r  41914  pell1qrge1  42097  pell1qr1  42098  pell1qrgaplem  42100  pell14qrgapw  42103  pellqrex  42106  rmspecnonsq  42134  rmspecfund  42136  rmspecpos  42144  sqrtcval  42881  stoweidlem1  45202  wallispi2lem2  45273  stirlinglem10  45284  lighneallem2  46759  onetansqsecsq  47994  cotsqcscsq  47995