Theorem resqcld 14076

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

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7356  ℝcr 11026  2c2 12225  ↑cexp 14012

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2184  ax-ext 2707  ax-sep 5220  ax-nul 5230  ax-pow 5296  ax-pr 5364  ax-un 7678  ax-cnex 11083  ax-resscn 11084  ax-1cn 11085  ax-icn 11086  ax-addcl 11087  ax-addrcl 11088  ax-mulcl 11089  ax-mulrcl 11090  ax-mulcom 11091  ax-addass 11092  ax-mulass 11093  ax-distr 11094  ax-i2m1 11095  ax-1ne0 11096  ax-1rid 11097  ax-rnegex 11098  ax-rrecex 11099  ax-cnre 11100  ax-pre-lttri 11101  ax-pre-lttrn 11102  ax-pre-ltadd 11103  ax-pre-mulgt0 11104

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2538  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2810  df-nfc 2884  df-ne 2931  df-nel 3035  df-ral 3050  df-rex 3060  df-reu 3341  df-rab 3388  df-v 3429  df-sbc 3726  df-csb 3834  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-pss 3905  df-nul 4264  df-if 4457  df-pw 4533  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4841  df-iun 4925  df-br 5075  df-opab 5137  df-mpt 5156  df-tr 5182  df-id 5515  df-eprel 5520  df-po 5528  df-so 5529  df-fr 5573  df-we 5575  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-pred 6254  df-ord 6315  df-on 6316  df-lim 6317  df-suc 6318  df-iota 6443  df-fun 6489  df-fn 6490  df-f 6491  df-f1 6492  df-fo 6493  df-f1o 6494  df-fv 6495  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-om 7807  df-2nd 7932  df-frecs 8220  df-wrecs 8251  df-recs 8300  df-rdg 8338  df-er 8632  df-en 8883  df-dom 8884  df-sdom 8885  df-pnf 11170  df-mnf 11171  df-xr 11172  df-ltxr 11173  df-le 11174  df-sub 11368  df-neg 11369  df-nn 12164  df-2 12233  df-n0 12427  df-z 12514  df-uz 12778  df-seq 13953  df-exp 14013

This theorem is referenced by:  zzlesq  14157  cjmulge0  15097  01sqrexlem1  15193  01sqrexlem6  15198  01sqrexlem7  15199  absrele  15259  abstri  15282  amgm2  15321  sinbnd  16136  cosbnd  16137  cos01bnd  16142  cos01gt0  16147  absefi  16152  pythagtriplem10  16780  pockthg  16866  prmreclem1  16876  4sqlem12  16916  4sqlem15  16919  4sqlem16  16920  prmlem1  17067  prmlem2  17079  cphnmf  25150  reipcl  25152  ipcau2  25189  csbren  25354  trirn  25355  rrxmval  25360  rrxmet  25363  rrxdstprj1  25364  rrxdsfi  25366  ehl1eudis  25375  ehl2eudis  25377  minveclem2  25381  minveclem3b  25383  minveclem3  25384  minveclem4  25387  minveclem6  25389  minveclem7  25390  pjthlem1  25392  itgabs  25790  dveflem  25934  tangtx  26457  tanregt0  26491  cxpsqrt  26655  lawcoslem1  26767  birthdaylem3  26905  cxp2limlem  26927  basellem8  27039  bposlem6  27240  2sqblem  27382  2sqmod  27387  2sqreulem1  27397  2sqreunnlem1  27400  rplogsumlem2  27436  logdivsum  27484  mulog2sumlem1  27485  mulog2sumlem2  27486  vmalogdivsum2  27489  log2sumbnd  27495  selberglem2  27497  logdivbnd  27507  pntpbnd1a  27536  pntlemb  27548  pntlemr  27553  pntlemk  27557  pntlemo  27558  eqeelen  28961  brbtwn2  28962  colinearalglem4  28966  axcgrid  28973  axsegconlem2  28975  axsegconlem3  28976  axsegconlem9  28982  ax5seglem1  28985  ax5seglem2  28986  ax5seglem3  28988  ax5seg  28995  ipval2lem2  30763  minvecolem2  30934  minvecolem3  30935  minvecolem4  30939  minvecolem5  30940  minvecolem6  30941  minvecolem7  30942  normpyc  31205  pjhthlem1  31450  chscllem2  31697  pjssposi  32231  hstle1  32285  hst1h  32286  hstle  32289  hstoh  32291  strlem3a  32311  receqid  32805  expevenpos  32907  cos9thpiminplylem1  33914  sqsscirc1  34040  hgt750lemf  34785  hgt750leme  34790  tgoldbachgtde  34792  sinccvglem  35842  itgabsnc  37998  dvasin  38013  areacirclem1  38017  areacirclem2  38018  areacirclem4  38020  areacirc  38022  cntotbnd  38105  rrnmet  38138  rrndstprj1  38139  rrndstprj2  38140  3lexlogpow2ineq2  42486  aks4d1p1p2  42497  aks4d1p1p4  42498  aks4d1p1p6  42500  aks4d1p1p7  42501  aks4d1p1p5  42502  aks4d1p1  42503  aks4d1p9  42515  aks6d1c3  42550  aks6d1c7lem1  42607  readvrec2  42781  3cubeslem1  43104  3cubeslem2  43105  pellexlem2  43246  pellexlem6  43250  pell14qrgt0  43275  pell1qrgaplem  43289  rmspecnonsq  43323  rmspecpos  43332  jm3.1lem2  43434  sqrtcval  44056  sqrlearg  45971  dvdivbd  46339  stirlinglem10  46499  fourierdlem56  46578  fourierdlem57  46579  rrxtopnfi  46703  rrndistlt  46706  hoiqssbllem2  47039  smfmullem1  47207  requad01  48085  requad1  48086  requad2  48087  resum2sqcl  49170  resum2sqgt0  49171  2sphere  49213  itsclc0lem3  49222  itscnhlc0yqe  49223  itsclc0yqsollem2  49227  itsclc0yqsol  49228  itscnhlc0xyqsol  49229  itschlc0xyqsol1  49230  itsclquadb  49240  2itscp  49245  itscnhlinecirc02plem1  49246  itscnhlinecirc02plem3  49248  itscnhlinecirc02p  49249