Theorem sq1 13209

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

Syntax hints:   = wceq 1653   ∈ wcel 2157  (class class class)co 6877  1c1 10224  2c2 11365  ℤcz 11663  ↑cexp 13111

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-8 2159  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2776  ax-sep 4974  ax-nul 4982  ax-pow 5034  ax-pr 5096  ax-un 7182  ax-cnex 10279  ax-resscn 10280  ax-1cn 10281  ax-icn 10282  ax-addcl 10283  ax-addrcl 10284  ax-mulcl 10285  ax-mulrcl 10286  ax-mulcom 10287  ax-addass 10288  ax-mulass 10289  ax-distr 10290  ax-i2m1 10291  ax-1ne0 10292  ax-1rid 10293  ax-rnegex 10294  ax-rrecex 10295  ax-cnre 10296  ax-pre-lttri 10297  ax-pre-lttrn 10298  ax-pre-ltadd 10299  ax-pre-mulgt0 10300

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3or 1109  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-mo 2591  df-eu 2609  df-clab 2785  df-cleq 2791  df-clel 2794  df-nfc 2929  df-ne 2971  df-nel 3074  df-ral 3093  df-rex 3094  df-reu 3095  df-rmo 3096  df-rab 3097  df-v 3386  df-sbc 3633  df-csb 3728  df-dif 3771  df-un 3773  df-in 3775  df-ss 3782  df-pss 3784  df-nul 4115  df-if 4277  df-pw 4350  df-sn 4368  df-pr 4370  df-tp 4372  df-op 4374  df-uni 4628  df-iun 4711  df-br 4843  df-opab 4905  df-mpt 4922  df-tr 4945  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5897  df-ord 5943  df-on 5944  df-lim 5945  df-suc 5946  df-iota 6063  df-fun 6102  df-fn 6103  df-f 6104  df-f1 6105  df-fo 6106  df-f1o 6107  df-fv 6108  df-riota 6838  df-ov 6880  df-oprab 6881  df-mpt2 6882  df-om 7299  df-2nd 7401  df-wrecs 7644  df-recs 7706  df-rdg 7744  df-er 7981  df-en 8195  df-dom 8196  df-sdom 8197  df-pnf 10364  df-mnf 10365  df-xr 10366  df-ltxr 10367  df-le 10368  df-sub 10557  df-neg 10558  df-div 10976  df-nn 11312  df-2 11373  df-n0 11578  df-z 11664  df-uz 11928  df-seq 13053  df-exp 13112

This theorem is referenced by:  neg1sqe1  13210  binom21  13231  binom2sub1  13233  sq01  13237  sqrlem1  14321  sqrt1  14350  sinbnd  15243  cosbnd  15244  cos1bnd  15250  cos2bnd  15251  cos01gt0  15254  sqnprm  15744  numdensq  15792  zsqrtelqelz  15796  prmreclem1  15950  prmreclem2  15951  4sqlem13  15991  4sqlem19  15997  odadd  18565  abvneg  19149  gzrngunitlem  20130  gzrngunit  20131  zringunit  20155  sinhalfpilem  24554  cos2pi  24567  tangtx  24596  coskpi  24611  tanregt0  24624  efif1olem3  24629  root1id  24836  root1cj  24838  isosctrlem2  24898  asin1  24970  efiatan2  24993  bndatandm  25005  atans2  25007  wilthlem1  25143  dchrinv  25335  sum2dchr  25348  lgslem1  25371  lgsne0  25409  lgssq  25411  lgssq2  25412  1lgs  25414  lgs1  25415  lgsdinn0  25419  lgsquad2lem2  25459  lgsquad3  25461  2lgsoddprmlem3a  25484  2sqlem9  25501  2sqlem10  25502  2sqlem11  25503  2sqblem  25505  2sqb  25506  mulog2sumlem2  25573  pntlemb  25635  axlowdimlem16  26187  ex-pr  27808  normlem1  28485  kbpj  29333  hstnmoc  29600  hstle1  29603  hst1h  29604  hstle  29607  strlem3a  29629  strlem4  29631  strlem5  29632  jplem1  29645  nn0sqeq1  30024  dvasin  33977  dvacos  33978  areacirclem1  33981  areacirc  33986  cntotbnd  34075  pell1qrge1  38209  pell1qr1  38210  pell1qrgaplem  38212  pell14qrgapw  38215  pellqrex  38218  rmspecnonsq  38246  rmspecfund  38248  rmspecpos  38255  stoweidlem1  40950  wallispi2lem2  41021  stirlinglem10  41032  lighneallem2  42294  onetansqsecsq  43293  cotsqcscsq  43294