Theorem resqcld 14166

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2143  (class class class)co 7410  ℝcr 11103  2c2 12299  ↑cexp 14102

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-cnex 11160  ax-resscn 11161  ax-1cn 11162  ax-icn 11163  ax-addcl 11164  ax-addrcl 11165  ax-mulcl 11166  ax-mulrcl 11167  ax-mulcom 11168  ax-addass 11169  ax-mulass 11170  ax-distr 11171  ax-i2m1 11172  ax-1ne0 11173  ax-1rid 11174  ax-rnegex 11175  ax-rrecex 11176  ax-cnre 11177  ax-pre-lttri 11178  ax-pre-lttrn 11179  ax-pre-ltadd 11180  ax-pre-mulgt0 11181

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-iun 4958  df-br 5110  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5556  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-we 5616  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-pred 6302  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-om 7859  df-2nd 7983  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-rdg 8393  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11249  df-mnf 11250  df-xr 11251  df-ltxr 11252  df-le 11253  df-sub 11447  df-neg 11448  df-nn 12238  df-2 12307  df-n0 12509  df-z 12596  df-uz 12867  df-seq 14043  df-exp 14103

This theorem is used by:  zzlesq  14247  cjmulge0  15202  01sqrexlem1  15298  01sqrexlem6  15303  01sqrexlem7  15304  absrele  15364  abstri  15387  amgm2  15426  sinbnd  16240  cosbnd  16241  cos01bnd  16246  cos01gt0  16251  absefi  16256  pythagtriplem10  16884  pockthg  16970  prmreclem1  16980  4sqlem12  17020  4sqlem15  17023  4sqlem16  17024  prmlem1  17171  prmlem2  17184  cphnmf  25363  reipcl  25365  ipcau2  25402  csbren  25567  trirn  25568  rrxmval  25573  rrxmet  25576  rrxdstprj1  25577  rrxdsfi  25579  ehl1eudis  25588  ehl2eudis  25590  minveclem2  25594  minveclem3b  25596  minveclem3  25597  minveclem4  25600  minveclem6  25602  minveclem7  25603  pjthlem1  25605  itgabs  26003  dveflem  26147  tangtx  26679  tanregt0  26713  cxpsqrt  26877  lawcoslem1  26989  birthdaylem3  27127  cxp2limlem  27149  basellem8  27261  bposlem6  27462  2sqblem  27604  2sqmod  27609  2sqreulem1  27619  2sqreunnlem1  27622  rplogsumlem2  27658  logdivsum  27706  mulog2sumlem1  27707  mulog2sumlem2  27708  vmalogdivsum2  27711  log2sumbnd  27717  selberglem2  27719  logdivbnd  27729  pntpbnd1a  27758  pntlemb  27770  pntlemr  27775  pntlemk  27779  pntlemo  27780  eqeelen  29263  brbtwn2  29264  colinearalglem4  29268  axcgrid  29275  axsegconlem2  29277  axsegconlem3  29278  axsegconlem9  29284  ax5seglem1  29287  ax5seglem2  29288  ax5seglem3  29290  ax5seg  29297  ipval2lem2  31065  minvecolem2  31236  minvecolem3  31237  minvecolem4  31241  minvecolem5  31242  minvecolem6  31243  minvecolem7  31244  normpyc  31507  pjhthlem1  31752  chscllem2  31999  pjssposi  32533  hstle1  32587  hst1h  32588  hstle  32591  hstoh  32593  strlem3a  32613  receqid  33098  expevenpos  33188  cos9thpiminplylem1  34181  sqsscirc1  34307  hgt750lemf  35049  hgt750leme  35054  tgoldbachgtde  35056  sinccvglem  36172  itgabsnc  38368  dvasin  38383  areacirclem1  38387  areacirclem2  38388  areacirclem4  38390  areacirc  38392  cntotbnd  38475  rrnmet  38508  rrndstprj1  38509  rrndstprj2  38510  3lexlogpow2ineq2  42854  aks4d1p1p2  42865  aks4d1p1p4  42866  aks4d1p1p6  42868  aks4d1p1p7  42869  aks4d1p1p5  42870  aks4d1p1  42871  aks4d1p9  42883  aks6d1c3  42918  aks6d1c7lem1  42975  readvrec2  43150  3cubeslem1  43443  3cubeslem2  43444  pellexlem2  43585  pellexlem6  43589  pell14qrgt0  43614  pell1qrgaplem  43628  rmspecnonsq  43662  rmspecpos  43671  jm3.1lem2  43773  sqrtcval  44395  sqrlearg  46297  dvdivbd  46665  stirlinglem10  46825  fourierdlem56  46904  fourierdlem57  46905  rrxtopnfi  47029  rrndistlt  47032  hoiqssbllem2  47365  smfmullem1  47533  requad01  48414  requad1  48415  requad2  48416  resum2sqcl  49514  resum2sqgt0  49515  2sphere  49557  itsclc0lem3  49566  itscnhlc0yqe  49567  itsclc0yqsollem2  49571  itsclc0yqsol  49572  itscnhlc0xyqsol  49573  itschlc0xyqsol1  49574  itsclquadb  49584  2itscp  49589  itscnhlinecirc02plem1  49590  itscnhlinecirc02plem3  49592  itscnhlinecirc02p  49593