Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > sqvald | Structured version Visualization version GIF version |
Description: Value of square. Inference version. (Contributed by Mario Carneiro, 28-May-2016.) |
Ref | Expression |
---|---|
expcld.1 | ⊢ (𝜑 → 𝐴 ∈ ℂ) |
Ref | Expression |
---|---|
sqvald | ⊢ (𝜑 → (𝐴↑2) = (𝐴 · 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | expcld.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℂ) | |
2 | sqval 13844 | . 2 ⊢ (𝐴 ∈ ℂ → (𝐴↑2) = (𝐴 · 𝐴)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → (𝐴↑2) = (𝐴 · 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1539 ∈ wcel 2107 (class class class)co 7284 ℂcc 10878 · cmul 10885 2c2 12037 ↑cexp 13791 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2710 ax-sep 5224 ax-nul 5231 ax-pow 5289 ax-pr 5353 ax-un 7597 ax-cnex 10936 ax-resscn 10937 ax-1cn 10938 ax-icn 10939 ax-addcl 10940 ax-addrcl 10941 ax-mulcl 10942 ax-mulrcl 10943 ax-mulcom 10944 ax-addass 10945 ax-mulass 10946 ax-distr 10947 ax-i2m1 10948 ax-1ne0 10949 ax-1rid 10950 ax-rnegex 10951 ax-rrecex 10952 ax-cnre 10953 ax-pre-lttri 10954 ax-pre-lttrn 10955 ax-pre-ltadd 10956 ax-pre-mulgt0 10957 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2541 df-eu 2570 df-clab 2717 df-cleq 2731 df-clel 2817 df-nfc 2890 df-ne 2945 df-nel 3051 df-ral 3070 df-rex 3071 df-reu 3073 df-rab 3074 df-v 3435 df-sbc 3718 df-csb 3834 df-dif 3891 df-un 3893 df-in 3895 df-ss 3905 df-pss 3907 df-nul 4258 df-if 4461 df-pw 4536 df-sn 4563 df-pr 4565 df-op 4569 df-uni 4841 df-iun 4927 df-br 5076 df-opab 5138 df-mpt 5159 df-tr 5193 df-id 5490 df-eprel 5496 df-po 5504 df-so 5505 df-fr 5545 df-we 5547 df-xp 5596 df-rel 5597 df-cnv 5598 df-co 5599 df-dm 5600 df-rn 5601 df-res 5602 df-ima 5603 df-pred 6206 df-ord 6273 df-on 6274 df-lim 6275 df-suc 6276 df-iota 6395 df-fun 6439 df-fn 6440 df-f 6441 df-f1 6442 df-fo 6443 df-f1o 6444 df-fv 6445 df-riota 7241 df-ov 7287 df-oprab 7288 df-mpo 7289 df-om 7722 df-2nd 7841 df-frecs 8106 df-wrecs 8137 df-recs 8211 df-rdg 8250 df-er 8507 df-en 8743 df-dom 8744 df-sdom 8745 df-pnf 11020 df-mnf 11021 df-xr 11022 df-ltxr 11023 df-le 11024 df-sub 11216 df-neg 11217 df-nn 11983 df-2 12045 df-n0 12243 df-z 12329 df-uz 12592 df-seq 13731 df-exp 13792 |
This theorem is referenced by: sqoddm1div8 13967 cjmulval 14865 sqrlem5 14967 sqrlem6 14968 sqrlem7 14969 remsqsqrt 14977 sqrtmsq 14991 absid 15017 absre 15022 absresq 15023 abs1m 15056 abslem2 15060 sqreulem 15080 msqsqrtd 15161 tanval3 15852 sincossq 15894 cos2t 15896 sqrt2irrlem 15966 sqnprm 16416 isprm5 16421 prmdvdssqOLD 16433 coprimeprodsq 16518 pockthg 16616 4sqlem7 16654 4sqlem10 16657 mul4sqlem 16663 4sqlem12 16666 4sqlem15 16669 4sqlem16 16670 4sqlem17 16671 odadd2 19459 abvneg 20103 zringunit 20697 cphsubrglem 24350 rrxnm 24564 pjthlem1 24610 itgabs 25008 dvrec 25128 dvmptdiv 25147 dveflem 25152 tangtx 25671 tanregt0 25704 tanarg 25783 cxpsqrt 25867 lawcoslem1 25974 chordthmlem4 25994 heron 25997 quad2 25998 dcubic1lem 26002 dcubic1 26004 dcubic 26005 cubic2 26007 binom4 26009 dquartlem1 26010 dquartlem2 26011 dquart 26012 quart1lem 26014 asinsin 26051 cxp2limlem 26134 lgamgulmlem3 26189 wilthlem1 26226 basellem8 26246 chpub 26377 bposlem2 26442 lgssq 26494 lgssq2 26495 lgsquad3 26544 2sqlem3 26577 2sqlem8 26583 2sqmod 26593 chtppilimlem1 26630 rplogsumlem2 26642 dchrisum0lem1a 26643 dchrisum0lem1 26673 dchrisum0lem3 26676 mulog2sumlem1 26691 vmalogdivsum2 26695 logsqvma 26699 logdivbnd 26713 pntpbnd1a 26742 pntlemr 26759 pntlemf 26762 pntlemk 26763 pntlemo 26764 brbtwn2 27282 colinearalglem4 27286 htthlem 29288 pjhthlem1 29762 cnlnadjlem7 30444 branmfn 30476 leopnmid 30509 hgt750lemf 32642 hgt750leme 32647 dvtan 35836 itgabsnc 35855 ftc1anclem3 35861 areacirclem1 35874 3lexlogpow2ineq2 40074 3cubeslem1 40513 3cubeslem2 40514 3cubeslem3l 40515 irrapxlem5 40655 pellexlem2 40659 pellexlem6 40663 rmxdbl 40768 jm2.18 40817 jm2.19lem1 40818 jm2.20nn 40826 jm2.25 40828 jm2.27c 40836 jm3.1lem2 40847 int-sqdefd 41799 int-sqgeq0d 41804 sqrlearg 43098 dvdivf 43470 wallispi2lem1 43619 stirlinglem1 43622 stirlinglem3 43624 stirlinglem10 43631 smfmullem1 44336 fmtnorec2lem 45005 fmtnorec3 45011 modexp2m1d 45075 itschlc0yqe 46117 itscnhlc0xyqsol 46122 itschlc0xyqsol1 46123 itschlc0xyqsol 46124 itsclc0xyqsolr 46126 |
Copyright terms: Public domain | W3C validator |