Theorem resqcld 14082

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

Syntax hints:   → wi 4   ∈ wcel 2121  (class class class)co 7360  ℝcr 11032  2c2 12231  ↑cexp 14018

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713  ax-sep 5221  ax-nul 5231  ax-pow 5297  ax-pr 5365  ax-un 7682  ax-cnex 11089  ax-resscn 11090  ax-1cn 11091  ax-icn 11092  ax-addcl 11093  ax-addrcl 11094  ax-mulcl 11095  ax-mulrcl 11096  ax-mulcom 11097  ax-addass 11098  ax-mulass 11099  ax-distr 11100  ax-i2m1 11101  ax-1ne0 11102  ax-1rid 11103  ax-rnegex 11104  ax-rrecex 11105  ax-cnre 11106  ax-pre-lttri 11107  ax-pre-lttrn 11108  ax-pre-ltadd 11109  ax-pre-mulgt0 11110

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3or 1094  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-ne 2937  df-nel 3041  df-ral 3056  df-rex 3066  df-reu 3347  df-rab 3394  df-v 3435  df-sbc 3726  df-csb 3834  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-pss 3905  df-nul 4265  df-if 4458  df-pw 4534  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4842  df-iun 4926  df-br 5076  df-opab 5138  df-mpt 5157  df-tr 5183  df-id 5516  df-eprel 5521  df-po 5529  df-so 5530  df-fr 5574  df-we 5576  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-pred 6256  df-ord 6317  df-on 6318  df-lim 6319  df-suc 6320  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-riota 7317  df-ov 7363  df-oprab 7364  df-mpo 7365  df-om 7811  df-2nd 7936  df-frecs 8225  df-wrecs 8256  df-recs 8305  df-rdg 8343  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  df-pnf 11176  df-mnf 11177  df-xr 11178  df-ltxr 11179  df-le 11180  df-sub 11374  df-neg 11375  df-nn 12170  df-2 12239  df-n0 12433  df-z 12520  df-uz 12784  df-seq 13959  df-exp 14019

This theorem is referenced by:  zzlesq  14163  cjmulge0  15103  01sqrexlem1  15199  01sqrexlem6  15204  01sqrexlem7  15205  absrele  15265  abstri  15288  amgm2  15327  sinbnd  16142  cosbnd  16143  cos01bnd  16148  cos01gt0  16153  absefi  16158  pythagtriplem10  16786  pockthg  16872  prmreclem1  16882  4sqlem12  16922  4sqlem15  16925  4sqlem16  16926  prmlem1  17073  prmlem2  17085  cphnmf  25184  reipcl  25186  ipcau2  25223  csbren  25388  trirn  25389  rrxmval  25394  rrxmet  25397  rrxdstprj1  25398  rrxdsfi  25400  ehl1eudis  25409  ehl2eudis  25411  minveclem2  25415  minveclem3b  25417  minveclem3  25418  minveclem4  25421  minveclem6  25423  minveclem7  25424  pjthlem1  25426  itgabs  25824  dveflem  25968  tangtx  26491  tanregt0  26525  cxpsqrt  26689  lawcoslem1  26801  birthdaylem3  26939  cxp2limlem  26961  basellem8  27073  bposlem6  27274  2sqblem  27416  2sqmod  27421  2sqreulem1  27431  2sqreunnlem1  27434  rplogsumlem2  27470  logdivsum  27518  mulog2sumlem1  27519  mulog2sumlem2  27520  vmalogdivsum2  27523  log2sumbnd  27529  selberglem2  27531  logdivbnd  27541  pntpbnd1a  27570  pntlemb  27582  pntlemr  27587  pntlemk  27591  pntlemo  27592  eqeelen  28995  brbtwn2  28996  colinearalglem4  29000  axcgrid  29007  axsegconlem2  29009  axsegconlem3  29010  axsegconlem9  29016  ax5seglem1  29019  ax5seglem2  29020  ax5seglem3  29022  ax5seg  29029  ipval2lem2  30797  minvecolem2  30968  minvecolem3  30969  minvecolem4  30973  minvecolem5  30974  minvecolem6  30975  minvecolem7  30976  normpyc  31239  pjhthlem1  31484  chscllem2  31731  pjssposi  32265  hstle1  32319  hst1h  32320  hstle  32323  hstoh  32325  strlem3a  32345  receqid  32840  expevenpos  32942  cos9thpiminplylem1  33978  sqsscirc1  34104  hgt750lemf  34849  hgt750leme  34854  tgoldbachgtde  34856  sinccvglem  35915  itgabsnc  38071  dvasin  38086  areacirclem1  38090  areacirclem2  38091  areacirclem4  38093  areacirc  38095  cntotbnd  38178  rrnmet  38211  rrndstprj1  38212  rrndstprj2  38213  3lexlogpow2ineq2  42559  aks4d1p1p2  42570  aks4d1p1p4  42571  aks4d1p1p6  42573  aks4d1p1p7  42574  aks4d1p1p5  42575  aks4d1p1  42576  aks4d1p9  42588  aks6d1c3  42623  aks6d1c7lem1  42680  readvrec2  42853  3cubeslem1  43148  3cubeslem2  43149  pellexlem2  43290  pellexlem6  43294  pell14qrgt0  43319  pell1qrgaplem  43333  rmspecnonsq  43367  rmspecpos  43376  jm3.1lem2  43478  sqrtcval  44100  sqrlearg  46012  dvdivbd  46380  stirlinglem10  46540  fourierdlem56  46619  fourierdlem57  46620  rrxtopnfi  46744  rrndistlt  46747  hoiqssbllem2  47080  smfmullem1  47248  requad01  48126  requad1  48127  requad2  48128  resum2sqcl  49211  resum2sqgt0  49212  2sphere  49254  itsclc0lem3  49263  itscnhlc0yqe  49264  itsclc0yqsollem2  49268  itsclc0yqsol  49269  itscnhlc0xyqsol  49270  itschlc0xyqsol1  49271  itsclquadb  49281  2itscp  49286  itscnhlinecirc02plem1  49287  itscnhlinecirc02plem3  49289  itscnhlinecirc02p  49290