Theorem resqcld 14084

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

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7364  ℝcr 11034  2c2 12233  ↑cexp 14020

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 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pow 5306  ax-pr 5374  ax-un 7686  ax-cnex 11091  ax-resscn 11092  ax-1cn 11093  ax-icn 11094  ax-addcl 11095  ax-addrcl 11096  ax-mulcl 11097  ax-mulrcl 11098  ax-mulcom 11099  ax-addass 11100  ax-mulass 11101  ax-distr 11102  ax-i2m1 11103  ax-1ne0 11104  ax-1rid 11105  ax-rnegex 11106  ax-rrecex 11107  ax-cnre 11108  ax-pre-lttri 11109  ax-pre-lttrn 11110  ax-pre-ltadd 11111  ax-pre-mulgt0 11112

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 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5523  df-eprel 5528  df-po 5536  df-so 5537  df-fr 5581  df-we 5583  df-xp 5634  df-rel 5635  df-cnv 5636  df-co 5637  df-dm 5638  df-rn 5639  df-res 5640  df-ima 5641  df-pred 6263  df-ord 6324  df-on 6325  df-lim 6326  df-suc 6327  df-iota 6452  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7321  df-ov 7367  df-oprab 7368  df-mpo 7369  df-om 7815  df-2nd 7940  df-frecs 8228  df-wrecs 8259  df-recs 8308  df-rdg 8346  df-er 8640  df-en 8891  df-dom 8892  df-sdom 8893  df-pnf 11178  df-mnf 11179  df-xr 11180  df-ltxr 11181  df-le 11182  df-sub 11376  df-neg 11377  df-nn 12172  df-2 12241  df-n0 12435  df-z 12522  df-uz 12786  df-seq 13961  df-exp 14021

This theorem is referenced by:  zzlesq  14165  cjmulge0  15105  01sqrexlem1  15201  01sqrexlem6  15206  01sqrexlem7  15207  absrele  15267  abstri  15290  amgm2  15329  sinbnd  16144  cosbnd  16145  cos01bnd  16150  cos01gt0  16155  absefi  16160  pythagtriplem10  16788  pockthg  16874  prmreclem1  16884  4sqlem12  16924  4sqlem15  16927  4sqlem16  16928  prmlem1  17075  prmlem2  17087  cphnmf  25178  reipcl  25180  ipcau2  25217  csbren  25382  trirn  25383  rrxmval  25388  rrxmet  25391  rrxdstprj1  25392  rrxdsfi  25394  ehl1eudis  25403  ehl2eudis  25405  minveclem2  25409  minveclem3b  25411  minveclem3  25412  minveclem4  25415  minveclem6  25417  minveclem7  25418  pjthlem1  25420  itgabs  25818  dveflem  25962  tangtx  26488  tanregt0  26522  cxpsqrt  26686  lawcoslem1  26798  birthdaylem3  26936  cxp2limlem  26959  basellem8  27071  bposlem6  27272  2sqblem  27414  2sqmod  27419  2sqreulem1  27429  2sqreunnlem1  27432  rplogsumlem2  27468  logdivsum  27516  mulog2sumlem1  27517  mulog2sumlem2  27518  vmalogdivsum2  27521  log2sumbnd  27527  selberglem2  27529  logdivbnd  27539  pntpbnd1a  27568  pntlemb  27580  pntlemr  27585  pntlemk  27589  pntlemo  27590  eqeelen  28993  brbtwn2  28994  colinearalglem4  28998  axcgrid  29005  axsegconlem2  29007  axsegconlem3  29008  axsegconlem9  29014  ax5seglem1  29017  ax5seglem2  29018  ax5seglem3  29020  ax5seg  29027  ipval2lem2  30796  minvecolem2  30967  minvecolem3  30968  minvecolem4  30972  minvecolem5  30973  minvecolem6  30974  minvecolem7  30975  normpyc  31238  pjhthlem1  31483  chscllem2  31730  pjssposi  32264  hstle1  32318  hst1h  32319  hstle  32322  hstoh  32324  strlem3a  32344  receqid  32838  expevenpos  32940  cos9thpiminplylem1  33948  sqsscirc1  34074  hgt750lemf  34819  hgt750leme  34824  tgoldbachgtde  34826  sinccvglem  35876  itgabsnc  38032  dvasin  38047  areacirclem1  38051  areacirclem2  38052  areacirclem4  38054  areacirc  38056  cntotbnd  38139  rrnmet  38172  rrndstprj1  38173  rrndstprj2  38174  3lexlogpow2ineq2  42520  aks4d1p1p2  42531  aks4d1p1p4  42532  aks4d1p1p6  42534  aks4d1p1p7  42535  aks4d1p1p5  42536  aks4d1p1  42537  aks4d1p9  42549  aks6d1c3  42584  aks6d1c7lem1  42641  readvrec2  42815  3cubeslem1  43138  3cubeslem2  43139  pellexlem2  43284  pellexlem6  43288  pell14qrgt0  43313  pell1qrgaplem  43327  rmspecnonsq  43361  rmspecpos  43370  jm3.1lem2  43472  sqrtcval  44094  sqrlearg  46009  dvdivbd  46377  stirlinglem10  46537  fourierdlem56  46616  fourierdlem57  46617  rrxtopnfi  46741  rrndistlt  46744  hoiqssbllem2  47077  smfmullem1  47245  requad01  48117  requad1  48118  requad2  48119  resum2sqcl  49202  resum2sqgt0  49203  2sphere  49245  itsclc0lem3  49254  itscnhlc0yqe  49255  itsclc0yqsollem2  49259  itsclc0yqsol  49260  itscnhlc0xyqsol  49261  itschlc0xyqsol1  49262  itsclquadb  49272  2itscp  49277  itscnhlinecirc02plem1  49278  itscnhlinecirc02plem3  49280  itscnhlinecirc02p  49281