Theorem sq2 14370

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

Assertion

Ref	Expression
sq2	⊢ (2↑2) = 4

Proof of Theorem sq2

Step	Hyp	Ref	Expression
1		2cn 12448	. . 3 ⊢ 2 ∈ ℂ
2	1	sqvali 14353	. 2 ⊢ (2↑2) = (2 · 2)
3		2t2e4 12536	. 2 ⊢ (2 · 2) = 4
4	2, 3	eqtri 2786	1 ⊢ (2↑2) = 4

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7446   · cmul 11235  2c2 12427  4c4 12429  ↑cexp 14234

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5253  ax-nul 5264  ax-pow 5332  ax-pr 5396  ax-un 7778  ax-cnex 11286  ax-resscn 11287  ax-1cn 11288  ax-icn 11289  ax-addcl 11290  ax-addrcl 11291  ax-mulcl 11292  ax-mulrcl 11293  ax-mulcom 11294  ax-addass 11295  ax-mulass 11296  ax-distr 11297  ax-i2m1 11298  ax-1ne0 11299  ax-1rid 11300  ax-rnegex 11301  ax-rrecex 11302  ax-cnre 11303  ax-pre-lttri 11304  ax-pre-lttrn 11305  ax-pre-ltadd 11306  ax-pre-mulgt0 11307

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-iun 4956  df-br 5107  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5551  df-eprel 5556  df-po 5564  df-so 5565  df-fr 5609  df-we 5611  df-xp 5662  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-rn 5667  df-res 5668  df-ima 5669  df-pred 6325  df-ord 6386  df-on 6387  df-lim 6388  df-suc 6389  df-iota 6515  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7403  df-ov 7449  df-oprab 7450  df-mpo 7451  df-om 7905  df-2nd 8029  df-frecs 8330  df-wrecs 8361  df-recs 8410  df-rdg 8449  df-er 8748  df-en 9005  df-dom 9006  df-sdom 9007  df-pnf 11375  df-mnf 11376  df-xr 11377  df-ltxr 11378  df-le 11379  df-sub 11573  df-neg 11574  df-nn 12366  df-2 12435  df-3 12436  df-4 12437  df-n0 12637  df-z 12724  df-uz 12996  df-seq 14175  df-exp 14235

This theorem is used by:  sq4e2t8  14372  cu2  14373  sqoddm1div8  14417  faclbnd2  14465  sqrt4  15471  amgm2  15569  ef01bndlem  16384  cos2bnd  16388  pythagtriplem1  17026  4sqlem12  17166  2exp4  17294  2exp5  17295  efmnd2hash  19122  lt6abl  20142  csbren  25753  minveclem2  25780  sincos6thpi  26877  heron  27199  quad2  27200  dcubic2  27205  mcubic  27208  dquartlem2  27213  dquart  27214  quart1  27217  quartlem1  27218  chtublem  27571  chtub  27572  bclbnd  27640  bposlem6  27649  bposlem8  27651  addsqnreup  27803  addsq2nreurex  27804  chebbnd1lem3  27831  chebbnd1  27832  fltoprmlem2  28027  ipidsq  31345  minvecolem2  31510  normpar2i  31791  iconstr  34481  constrresqrtcl  34492  cos9thpiminplylem1  34497  sqsscirc1  34623  lcmineqlem21  43302  aks4d1p1p7  43327  aks4d1p1p5  43328  wallispi2lem1  47296  stirlinglem3  47301  stirlinglem10  47308  fmtno1  48841  fmtno2  48850  fmtnofac1  48870  m2prm  48891  lighneallem2  48906  lighneallem4a  48908  nprmdvdsfacm1lem2  48921  exple2lt6  49691  ackval3  50010  ackval42  50023  ackval42a  50024  itsclc0yqsollem1  50089  itscnhlinecirc02plem1  50109