Theorem resqcld 14268

Description: Closure of squaring in reals, deduction form. (Contributed by Mario Carneiro, 28-May-2016.)

Hypothesis

Ref	Expression
resqcld.1	⊢ (𝜑 → 𝐴 ∈ ℝ)

Assertion

Ref	Expression
resqcld	⊢ (𝜑 → (𝐴↑2) ∈ ℝ)

Proof of Theorem resqcld

Step	Hyp	Ref	Expression
1		resqcld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2		resqcl 14267	. 2 ⊢ (𝐴 ∈ ℝ → (𝐴↑2) ∈ ℝ)
3	1, 2	syl 18	1 ⊢ (𝜑 → (𝐴↑2) ∈ ℝ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  (class class class)co 7420  ℝcr 11199  2c2 12397  ↑cexp 14204

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-cnex 11256  ax-resscn 11257  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-addrcl 11261  ax-mulcl 11262  ax-mulrcl 11263  ax-mulcom 11264  ax-addass 11265  ax-mulass 11266  ax-distr 11267  ax-i2m1 11268  ax-1ne0 11269  ax-1rid 11270  ax-rnegex 11271  ax-rrecex 11272  ax-cnre 11273  ax-pre-lttri 11274  ax-pre-lttrn 11275  ax-pre-ltadd 11276  ax-pre-mulgt0 11277

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7377  df-ov 7423  df-oprab 7424  df-mpo 7425  df-om 7878  df-2nd 8002  df-frecs 8299  df-wrecs 8330  df-recs 8379  df-rdg 8418  df-er 8717  df-en 8974  df-dom 8975  df-sdom 8976  df-pnf 11345  df-mnf 11346  df-xr 11347  df-ltxr 11348  df-le 11349  df-sub 11543  df-neg 11544  df-nn 12336  df-2 12405  df-n0 12607  df-z 12694  df-uz 12966  df-seq 14145  df-exp 14205

This theorem is used by:  zzlesq  14350  cjmulge0  15313  01sqrexlem1  15409  01sqrexlem6  15414  01sqrexlem7  15415  absrele  15475  abstri  15498  amgm2  15537  sinbnd  16348  cosbnd  16349  cos01bnd  16354  cos01gt0  16359  absefi  16364  pythagtriplem10  16998  pockthg  17084  prmreclem1  17094  4sqlem12  17134  4sqlem15  17137  4sqlem16  17138  prmlem1  17285  prmlem2  17298  cphnmf  25516  reipcl  25518  ipcau2  25555  csbren  25720  trirn  25721  rrxmval  25726  rrxmet  25729  rrxdstprj1  25730  rrxdsfi  25732  ehl1eudis  25741  ehl2eudis  25743  minveclem2  25747  minveclem3b  25749  minveclem3  25750  minveclem4  25753  minveclem6  25755  minveclem7  25756  pjthlem1  25758  itgabs  26155  dveflem  26299  tangtx  26834  tanregt0  26867  cxpsqrt  27031  lawcoslem1  27143  birthdaylem3  27281  cxp2limlem  27303  basellem8  27415  bposlem6  27616  2sqblem  27758  2sqmod  27763  2sqreulem1  27773  2sqreunnlem1  27776  rplogsumlem2  27812  logdivsum  27860  mulog2sumlem1  27861  mulog2sumlem2  27862  vmalogdivsum2  27865  log2sumbnd  27871  selberglem2  27873  logdivbnd  27883  pntpbnd1a  27912  pntlemb  27924  pntlemr  27929  pntlemk  27933  pntlemo  27934  eqeelen  29482  brbtwn2  29483  colinearalglem4  29487  axcgrid  29494  axsegconlem2  29496  axsegconlem3  29497  axsegconlem9  29503  ax5seglem1  29506  ax5seglem2  29507  ax5seglem3  29509  ax5seg  29516  ipval2lem2  31306  minvecolem2  31477  minvecolem3  31478  minvecolem4  31482  minvecolem5  31483  minvecolem6  31484  minvecolem7  31485  normpyc  31748  pjhthlem1  31993  chscllem2  32240  pjssposi  32774  hstle1  32828  hst1h  32829  hstle  32832  hstoh  32834  strlem3a  32854  receqid  33336  expevenpos  33426  cos9thpiminplylem1  34414  sqsscirc1  34540  hgt750lemf  35282  hgt750leme  35287  tgoldbachgtde  35289  sinccvglem  36437  itgabsnc  38608  dvasin  38623  areacirclem1  38627  areacirclem2  38628  areacirclem4  38630  areacirc  38632  cntotbnd  38731  rrnmet  38764  rrndstprj1  38765  rrndstprj2  38766  3lexlogpow2ineq2  43110  aks4d1p1p2  43121  aks4d1p1p4  43122  aks4d1p1p6  43124  aks4d1p1p7  43125  aks4d1p1p5  43126  aks4d1p1  43127  aks4d1p9  43139  aks6d1c3  43174  aks6d1c7lem1  43231  readvrec2  43413  3cubeslem1  43695  3cubeslem2  43696  pellexlem2  43837  pellexlem6  43841  pell14qrgt0  43866  pell1qrgaplem  43880  rmspecnonsq  43914  rmspecpos  43923  jm3.1lem2  44025  sqrtcval  44641  sqrlearg  46565  dvdivbd  46933  stirlinglem10  47093  fourierdlem56  47172  fourierdlem57  47173  rrxtopnfi  47297  rrndistlt  47300  hoiqssbllem2  47633  smfmullem1  47801  requad01  48719  requad1  48720  requad2  48721  resum2sqcl  49818  resum2sqgt0  49819  2sphere  49861  itsclc0lem3  49870  itscnhlc0yqe  49871  itsclc0yqsollem2  49875  itsclc0yqsol  49876  itscnhlc0xyqsol  49877  itschlc0xyqsol1  49878  itsclquadb  49888  2itscp  49893  itscnhlinecirc02plem1  49894  itscnhlinecirc02plem3  49896  itscnhlinecirc02p  49897  veronesefvcl  50972  veronesev1lem  50973  veronesev2lem  50974  veronesev3lem  50975  veroquadgsumlem  50983