Theorem resqcld 14097

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

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7390  ℝcr 11074  2c2 12248  ↑cexp 14033

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-cnex 11131  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151  ax-pre-mulgt0 11152

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-pred 6277  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-riota 7347  df-ov 7393  df-oprab 7394  df-mpo 7395  df-om 7846  df-2nd 7972  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-rdg 8381  df-er 8674  df-en 8922  df-dom 8923  df-sdom 8924  df-pnf 11217  df-mnf 11218  df-xr 11219  df-ltxr 11220  df-le 11221  df-sub 11414  df-neg 11415  df-nn 12194  df-2 12256  df-n0 12450  df-z 12537  df-uz 12801  df-seq 13974  df-exp 14034

This theorem is referenced by:  zzlesq  14178  cjmulge0  15119  01sqrexlem1  15215  01sqrexlem6  15220  01sqrexlem7  15221  absrele  15281  abstri  15304  amgm2  15343  sinbnd  16155  cosbnd  16156  cos01bnd  16161  cos01gt0  16166  absefi  16171  pythagtriplem10  16798  pockthg  16884  prmreclem1  16894  4sqlem12  16934  4sqlem15  16937  4sqlem16  16938  prmlem1  17085  prmlem2  17097  cphnmf  25102  reipcl  25104  ipcau2  25141  csbren  25306  trirn  25307  rrxmval  25312  rrxmet  25315  rrxdstprj1  25316  rrxdsfi  25318  ehl1eudis  25327  ehl2eudis  25329  minveclem2  25333  minveclem3b  25335  minveclem3  25336  minveclem4  25339  minveclem6  25341  minveclem7  25342  pjthlem1  25344  itgabs  25743  dveflem  25890  tangtx  26421  tanregt0  26455  cxpsqrt  26619  lawcoslem1  26732  birthdaylem3  26870  cxp2limlem  26893  basellem8  27005  bposlem6  27207  2sqblem  27349  2sqmod  27354  2sqreulem1  27364  2sqreunnlem1  27367  rplogsumlem2  27403  logdivsum  27451  mulog2sumlem1  27452  mulog2sumlem2  27453  vmalogdivsum2  27456  log2sumbnd  27462  selberglem2  27464  logdivbnd  27474  pntpbnd1a  27503  pntlemb  27515  pntlemr  27520  pntlemk  27524  pntlemo  27525  eqeelen  28838  brbtwn2  28839  colinearalglem4  28843  axcgrid  28850  axsegconlem2  28852  axsegconlem3  28853  axsegconlem9  28859  ax5seglem1  28862  ax5seglem2  28863  ax5seglem3  28865  ax5seg  28872  ipval2lem2  30640  minvecolem2  30811  minvecolem3  30812  minvecolem4  30816  minvecolem5  30817  minvecolem6  30818  minvecolem7  30819  normpyc  31082  pjhthlem1  31327  chscllem2  31574  pjssposi  32108  hstle1  32162  hst1h  32163  hstle  32166  hstoh  32168  strlem3a  32188  receqid  32675  expevenpos  32778  cos9thpiminplylem1  33779  sqsscirc1  33905  hgt750lemf  34651  hgt750leme  34656  tgoldbachgtde  34658  sinccvglem  35666  itgabsnc  37690  dvasin  37705  areacirclem1  37709  areacirclem2  37710  areacirclem4  37712  areacirc  37714  cntotbnd  37797  rrnmet  37830  rrndstprj1  37831  rrndstprj2  37832  3lexlogpow2ineq2  42054  aks4d1p1p2  42065  aks4d1p1p4  42066  aks4d1p1p6  42068  aks4d1p1p7  42069  aks4d1p1p5  42070  aks4d1p1  42071  aks4d1p9  42083  aks6d1c3  42118  aks6d1c7lem1  42175  readvrec2  42356  3cubeslem1  42679  3cubeslem2  42680  pellexlem2  42825  pellexlem6  42829  pell14qrgt0  42854  pell1qrgaplem  42868  rmspecnonsq  42902  rmspecpos  42912  jm3.1lem2  43014  sqrtcval  43637  sqrlearg  45558  dvdivbd  45928  stirlinglem10  46088  fourierdlem56  46167  fourierdlem57  46168  rrxtopnfi  46292  rrndistlt  46295  hoiqssbllem2  46628  smfmullem1  46796  requad01  47626  requad1  47627  requad2  47628  resum2sqcl  48699  resum2sqgt0  48700  2sphere  48742  itsclc0lem3  48751  itscnhlc0yqe  48752  itsclc0yqsollem2  48756  itsclc0yqsol  48757  itscnhlc0xyqsol  48758  itschlc0xyqsol1  48759  itsclquadb  48769  2itscp  48774  itscnhlinecirc02plem1  48775  itscnhlinecirc02plem3  48777  itscnhlinecirc02p  48778