Theorem resqcld 13610

Description: Closure of square in reals. (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 13489	. 2 ⊢ (𝐴 ∈ ℝ → (𝐴↑2) ∈ ℝ)
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴↑2) ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2110  (class class class)co 7155  ℝcr 10535  2c2 11691  ↑cexp 13428

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5202  ax-nul 5209  ax-pow 5265  ax-pr 5329  ax-un 7460  ax-cnex 10592  ax-resscn 10593  ax-1cn 10594  ax-icn 10595  ax-addcl 10596  ax-addrcl 10597  ax-mulcl 10598  ax-mulrcl 10599  ax-mulcom 10600  ax-addass 10601  ax-mulass 10602  ax-distr 10603  ax-i2m1 10604  ax-1ne0 10605  ax-1rid 10606  ax-rnegex 10607  ax-rrecex 10608  ax-cnre 10609  ax-pre-lttri 10610  ax-pre-lttrn 10611  ax-pre-ltadd 10612  ax-pre-mulgt0 10613

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4567  df-pr 4569  df-tp 4571  df-op 4573  df-uni 4838  df-iun 4920  df-br 5066  df-opab 5128  df-mpt 5146  df-tr 5172  df-id 5459  df-eprel 5464  df-po 5473  df-so 5474  df-fr 5513  df-we 5515  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-pred 6147  df-ord 6193  df-on 6194  df-lim 6195  df-suc 6196  df-iota 6313  df-fun 6356  df-fn 6357  df-f 6358  df-f1 6359  df-fo 6360  df-f1o 6361  df-fv 6362  df-riota 7113  df-ov 7158  df-oprab 7159  df-mpo 7160  df-om 7580  df-2nd 7689  df-wrecs 7946  df-recs 8007  df-rdg 8045  df-er 8288  df-en 8509  df-dom 8510  df-sdom 8511  df-pnf 10676  df-mnf 10677  df-xr 10678  df-ltxr 10679  df-le 10680  df-sub 10871  df-neg 10872  df-nn 11638  df-2 11699  df-n0 11897  df-z 11981  df-uz 12243  df-seq 13369  df-exp 13429

This theorem is referenced by:  cjmulge0  14504  sqrlem1  14601  sqrlem6  14606  sqrlem7  14607  absrele  14667  abstri  14689  amgm2  14728  sinbnd  15532  cosbnd  15533  cos01bnd  15538  cos01gt0  15543  absefi  15548  pythagtriplem10  16156  pockthg  16241  prmreclem1  16251  4sqlem12  16291  4sqlem15  16294  4sqlem16  16295  prmlem1  16440  prmlem2  16452  cphnmf  23798  reipcl  23800  ipcau2  23836  csbren  24001  trirn  24002  rrxmval  24007  rrxmet  24010  rrxdstprj1  24011  rrxdsfi  24013  ehl1eudis  24022  ehl2eudis  24024  minveclem2  24028  minveclem3b  24030  minveclem3  24031  minveclem4  24034  minveclem6  24036  minveclem7  24037  pjthlem1  24039  itgabs  24434  dveflem  24575  tangtx  25090  tanregt0  25122  cxpsqrt  25285  lawcoslem1  25392  birthdaylem3  25530  cxp2limlem  25552  basellem8  25664  bposlem6  25864  2sqblem  26006  2sqmod  26011  2sqreulem1  26021  2sqreunnlem1  26024  rplogsumlem2  26060  logdivsum  26108  mulog2sumlem1  26109  mulog2sumlem2  26110  vmalogdivsum2  26113  log2sumbnd  26119  selberglem2  26121  logdivbnd  26131  pntpbnd1a  26160  pntlemb  26172  pntlemr  26177  pntlemk  26181  pntlemo  26182  eqeelen  26689  brbtwn2  26690  colinearalglem4  26694  axcgrid  26701  axsegconlem2  26703  axsegconlem3  26704  axsegconlem9  26710  ax5seglem1  26713  ax5seglem2  26714  ax5seglem3  26716  ax5seg  26723  ipval2lem2  28480  minvecolem2  28651  minvecolem3  28652  minvecolem4  28656  minvecolem5  28657  minvecolem6  28658  minvecolem7  28659  normpyc  28922  pjhthlem1  29167  chscllem2  29414  pjssposi  29948  hstle1  30002  hst1h  30003  hstle  30006  hstoh  30008  strlem3a  30028  sqsscirc1  31151  hgt750lemf  31924  hgt750leme  31929  tgoldbachgtde  31931  sinccvglem  32915  itgabsnc  34960  dvasin  34977  areacirclem1  34981  areacirclem2  34982  areacirclem4  34984  areacirc  34986  cntotbnd  35073  rrnmet  35106  rrndstprj1  35107  rrndstprj2  35108  3cubeslem1  39279  3cubeslem2  39280  pellexlem2  39425  pellexlem6  39429  pell14qrgt0  39454  pell1qrgaplem  39468  rmspecnonsq  39502  rmspecpos  39511  jm3.1lem2  39613  sqrlearg  41827  dvdivbd  42206  stirlinglem10  42367  fourierdlem56  42446  fourierdlem57  42447  rrxtopnfi  42571  rrndistlt  42574  hoiqssbllem2  42904  smfmullem1  43065  requad01  43785  requad1  43786  requad2  43787  resum2sqcl  44692  resum2sqgt0  44693  2sphere  44735  itsclc0lem3  44744  itscnhlc0yqe  44745  itsclc0yqsollem2  44749  itsclc0yqsol  44750  itscnhlc0xyqsol  44751  itschlc0xyqsol1  44752  itsclquadb  44762  2itscp  44767  itscnhlinecirc02plem1  44768  itscnhlinecirc02plem3  44770  itscnhlinecirc02p  44771