Theorem resqcld 14086

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 14085	. 2 ⊢ (𝐴 ∈ ℝ → (𝐴↑2) ∈ ℝ)
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴↑2) ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2106  (class class class)co 7405  ℝcr 11105  2c2 12263  ↑cexp 14023

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  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 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7852  df-2nd 7972  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-er 8699  df-en 8936  df-dom 8937  df-sdom 8938  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-nn 12209  df-2 12271  df-n0 12469  df-z 12555  df-uz 12819  df-seq 13963  df-exp 14024

This theorem is referenced by:  zzlesq  14166  cjmulge0  15089  01sqrexlem1  15185  01sqrexlem6  15190  01sqrexlem7  15191  absrele  15251  abstri  15273  amgm2  15312  sinbnd  16119  cosbnd  16120  cos01bnd  16125  cos01gt0  16130  absefi  16135  pythagtriplem10  16749  pockthg  16835  prmreclem1  16845  4sqlem12  16885  4sqlem15  16888  4sqlem16  16889  prmlem1  17037  prmlem2  17049  cphnmf  24703  reipcl  24705  ipcau2  24742  csbren  24907  trirn  24908  rrxmval  24913  rrxmet  24916  rrxdstprj1  24917  rrxdsfi  24919  ehl1eudis  24928  ehl2eudis  24930  minveclem2  24934  minveclem3b  24936  minveclem3  24937  minveclem4  24940  minveclem6  24942  minveclem7  24943  pjthlem1  24945  itgabs  25343  dveflem  25487  tangtx  26006  tanregt0  26039  cxpsqrt  26202  lawcoslem1  26309  birthdaylem3  26447  cxp2limlem  26469  basellem8  26581  bposlem6  26781  2sqblem  26923  2sqmod  26928  2sqreulem1  26938  2sqreunnlem1  26941  rplogsumlem2  26977  logdivsum  27025  mulog2sumlem1  27026  mulog2sumlem2  27027  vmalogdivsum2  27030  log2sumbnd  27036  selberglem2  27038  logdivbnd  27048  pntpbnd1a  27077  pntlemb  27089  pntlemr  27094  pntlemk  27098  pntlemo  27099  eqeelen  28151  brbtwn2  28152  colinearalglem4  28156  axcgrid  28163  axsegconlem2  28165  axsegconlem3  28166  axsegconlem9  28172  ax5seglem1  28175  ax5seglem2  28176  ax5seglem3  28178  ax5seg  28185  ipval2lem2  29944  minvecolem2  30115  minvecolem3  30116  minvecolem4  30120  minvecolem5  30121  minvecolem6  30122  minvecolem7  30123  normpyc  30386  pjhthlem1  30631  chscllem2  30878  pjssposi  31412  hstle1  31466  hst1h  31467  hstle  31470  hstoh  31472  strlem3a  31492  sqsscirc1  32876  hgt750lemf  33653  hgt750leme  33658  tgoldbachgtde  33660  sinccvglem  34645  itgabsnc  36545  dvasin  36560  areacirclem1  36564  areacirclem2  36565  areacirclem4  36567  areacirc  36569  cntotbnd  36652  rrnmet  36685  rrndstprj1  36686  rrndstprj2  36687  3lexlogpow2ineq2  40912  aks4d1p1p2  40923  aks4d1p1p4  40924  aks4d1p1p6  40926  aks4d1p1p7  40927  aks4d1p1p5  40928  aks4d1p1  40929  aks4d1p9  40941  3cubeslem1  41407  3cubeslem2  41408  pellexlem2  41553  pellexlem6  41557  pell14qrgt0  41582  pell1qrgaplem  41596  rmspecnonsq  41630  rmspecpos  41640  jm3.1lem2  41742  sqrtcval  42377  sqrlearg  44252  dvdivbd  44625  stirlinglem10  44785  fourierdlem56  44864  fourierdlem57  44865  rrxtopnfi  44989  rrndistlt  44992  hoiqssbllem2  45325  smfmullem1  45493  requad01  46275  requad1  46276  requad2  46277  resum2sqcl  47345  resum2sqgt0  47346  2sphere  47388  itsclc0lem3  47397  itscnhlc0yqe  47398  itsclc0yqsollem2  47402  itsclc0yqsol  47403  itscnhlc0xyqsol  47404  itschlc0xyqsol1  47405  itsclquadb  47415  2itscp  47420  itscnhlinecirc02plem1  47421  itscnhlinecirc02plem3  47423  itscnhlinecirc02p  47424