Theorem resqcld 12435

Description: Closure of square in reals. (Contributed by Mario Carneiro, 28-May-2016.)

Hypothesis

Ref	Expression
resqcld.1	|- ( ph -> A e. RR )

Assertion

Ref	Expression
resqcld	|- ( ph -> ( A ^ 2 ) e. RR )

Proof of Theorem resqcld

Step	Hyp	Ref	Expression
1		resqcld.1	. 2 |- ( ph -> A e. RR )
2		resqcl 12335	. 2 |- ( A e. RR -> ( A ^ 2 ) e. RR )
3	1, 2	syl 17	1 |- ( ph -> ( A ^ 2 ) e. RR )

Syntax hints:   -> wi 4   e. wcel 1890  (class class class)co 6275   RRcr 9524   2c2 10647   ^cexp 12265

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1672  ax-4 1685  ax-5 1761  ax-6 1808  ax-7 1854  ax-8 1892  ax-9 1899  ax-10 1918  ax-11 1923  ax-12 1936  ax-13 2091  ax-ext 2431  ax-sep 4496  ax-nul 4505  ax-pow 4553  ax-pr 4611  ax-un 6570  ax-cnex 9581  ax-resscn 9582  ax-1cn 9583  ax-icn 9584  ax-addcl 9585  ax-addrcl 9586  ax-mulcl 9587  ax-mulrcl 9588  ax-mulcom 9589  ax-addass 9590  ax-mulass 9591  ax-distr 9592  ax-i2m1 9593  ax-1ne0 9594  ax-1rid 9595  ax-rnegex 9596  ax-rrecex 9597  ax-cnre 9598  ax-pre-lttri 9599  ax-pre-lttrn 9600  ax-pre-ltadd 9601  ax-pre-mulgt0 9602

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 987  df-3an 988  df-tru 1450  df-ex 1667  df-nf 1671  df-sb 1801  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2623  df-nel 2624  df-ral 2741  df-rex 2742  df-reu 2743  df-rab 2745  df-v 3014  df-sbc 3235  df-csb 3331  df-dif 3374  df-un 3376  df-in 3378  df-ss 3385  df-pss 3387  df-nul 3699  df-if 3849  df-pw 3920  df-sn 3936  df-pr 3938  df-tp 3940  df-op 3942  df-uni 4168  df-iun 4249  df-br 4374  df-opab 4433  df-mpt 4434  df-tr 4469  df-eprel 4722  df-id 4726  df-po 4732  df-so 4733  df-fr 4770  df-we 4772  df-xp 4817  df-rel 4818  df-cnv 4819  df-co 4820  df-dm 4821  df-rn 4822  df-res 4823  df-ima 4824  df-pred 5358  df-ord 5404  df-on 5405  df-lim 5406  df-suc 5407  df-iota 5524  df-fun 5562  df-fn 5563  df-f 5564  df-f1 5565  df-fo 5566  df-f1o 5567  df-fv 5568  df-riota 6237  df-ov 6278  df-oprab 6279  df-mpt2 6280  df-om 6680  df-2nd 6781  df-wrecs 7014  df-recs 7076  df-rdg 7114  df-er 7349  df-en 7556  df-dom 7557  df-sdom 7558  df-pnf 9663  df-mnf 9664  df-xr 9665  df-ltxr 9666  df-le 9667  df-sub 9848  df-neg 9849  df-nn 10598  df-2 10656  df-n0 10859  df-z 10927  df-uz 11149  df-seq 12207  df-exp 12266

This theorem is referenced by:  cjmulge0  13219  sqrlem1  13316  sqrlem6  13321  sqrlem7  13322  absrele  13381  abstri  13403  amgm2  13442  sinbnd  14244  cosbnd  14245  cos01bnd  14250  cos01gt0  14255  absefi  14260  pythagtriplem10  14780  pockthg  14860  prmreclem1  14870  4sqlem12  14910  4sqlem15OLD  14913  4sqlem16OLD  14914  4sqlem15  14919  4sqlem16  14920  prmlem1  15089  prmlem2  15101  cphnmf  22183  reipcl  22185  ipcau2  22218  csbren  22363  trirn  22364  rrxmval  22369  rrxmet  22372  rrxdstprj1  22373  minveclem2  22378  minveclem3b  22380  minveclem3  22381  minveclem4  22384  minveclem6  22386  minveclem7  22387  minveclem2OLD  22390  minveclem3bOLD  22392  minveclem3OLD  22393  minveclem4OLD  22396  minveclem6OLD  22398  minveclem7OLD  22399  pjthlem1  22401  itgabs  22803  dveflem  22942  tangtx  23471  tanregt0  23499  cxpsqrt  23659  lawcoslem1  23755  birthdaylem3  23890  cxp2limlem  23912  basellem8  24025  bposlem6  24228  2sqblem  24316  rplogsumlem2  24334  logdivsum  24382  mulog2sumlem1  24383  mulog2sumlem2  24384  vmalogdivsum2  24387  log2sumbnd  24393  selberglem2  24395  logdivbnd  24405  pntpbnd1a  24434  pntlemb  24446  pntlemr  24451  pntlemk  24455  pntlemo  24456  eqeelen  24945  brbtwn2  24946  colinearalglem4  24950  axcgrid  24957  axsegconlem2  24959  axsegconlem3  24960  axsegconlem9  24966  ax5seglem1  24969  ax5seglem2  24970  ax5seglem3  24972  ax5seg  24979  ipval2lem2  26351  ipval2lem5  26357  minvecolem2  26528  minvecolem3  26529  minvecolem4  26533  minvecolem5  26534  minvecolem6  26535  minvecolem7  26536  minvecolem2OLD  26538  minvecolem3OLD  26539  minvecolem4OLD  26543  minvecolem5OLD  26544  minvecolem6OLD  26545  minvecolem7OLD  26546  normpyc  26810  pjhthlem1  27055  chscllem2  27302  pjssposi  27836  hstle1  27890  hst1h  27891  hstle  27894  hstoh  27896  strlem3a  27916  2sqmod  28416  sqsscirc1  28720  sinccvglem  30321  itgabsnc  32012  dvasin  32029  areacirclem1  32033  areacirclem2  32034  areacirclem4  32036  areacirc  32038  cntotbnd  32129  rrnmet  32162  rrndstprj1  32163  rrndstprj2  32164  pellexlem2  35675  pellexlem6  35679  pell14qrgt0  35706  pell1qrgaplem  35720  rmspecnonsq  35756  rmspecpos  35765  jm3.1lem2  35874  dvdivbd  37836  stirlinglem10  38001  fourierdlem56  38082  fourierdlem57  38083  rrxdsfi  38210  rrxtopnfi  38211  rrndistlt  38215  hoiqssbllem2  38507