![]() |
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 13296 | . 2 ⊢ (𝐴 ∈ ℂ → (𝐴↑2) = (𝐴 · 𝐴)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → (𝐴↑2) = (𝐴 · 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1507 ∈ wcel 2050 (class class class)co 6976 ℂcc 10333 · cmul 10340 2c2 11495 ↑cexp 13244 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 ax-ext 2750 ax-sep 5060 ax-nul 5067 ax-pow 5119 ax-pr 5186 ax-un 7279 ax-cnex 10391 ax-resscn 10392 ax-1cn 10393 ax-icn 10394 ax-addcl 10395 ax-addrcl 10396 ax-mulcl 10397 ax-mulrcl 10398 ax-mulcom 10399 ax-addass 10400 ax-mulass 10401 ax-distr 10402 ax-i2m1 10403 ax-1ne0 10404 ax-1rid 10405 ax-rnegex 10406 ax-rrecex 10407 ax-cnre 10408 ax-pre-lttri 10409 ax-pre-lttrn 10410 ax-pre-ltadd 10411 ax-pre-mulgt0 10412 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3or 1069 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2584 df-clab 2759 df-cleq 2771 df-clel 2846 df-nfc 2918 df-ne 2968 df-nel 3074 df-ral 3093 df-rex 3094 df-reu 3095 df-rab 3097 df-v 3417 df-sbc 3682 df-csb 3787 df-dif 3832 df-un 3834 df-in 3836 df-ss 3843 df-pss 3845 df-nul 4179 df-if 4351 df-pw 4424 df-sn 4442 df-pr 4444 df-tp 4446 df-op 4448 df-uni 4713 df-iun 4794 df-br 4930 df-opab 4992 df-mpt 5009 df-tr 5031 df-id 5312 df-eprel 5317 df-po 5326 df-so 5327 df-fr 5366 df-we 5368 df-xp 5413 df-rel 5414 df-cnv 5415 df-co 5416 df-dm 5417 df-rn 5418 df-res 5419 df-ima 5420 df-pred 5986 df-ord 6032 df-on 6033 df-lim 6034 df-suc 6035 df-iota 6152 df-fun 6190 df-fn 6191 df-f 6192 df-f1 6193 df-fo 6194 df-f1o 6195 df-fv 6196 df-riota 6937 df-ov 6979 df-oprab 6980 df-mpo 6981 df-om 7397 df-2nd 7502 df-wrecs 7750 df-recs 7812 df-rdg 7850 df-er 8089 df-en 8307 df-dom 8308 df-sdom 8309 df-pnf 10476 df-mnf 10477 df-xr 10478 df-ltxr 10479 df-le 10480 df-sub 10672 df-neg 10673 df-nn 11440 df-2 11503 df-n0 11708 df-z 11794 df-uz 12059 df-seq 13185 df-exp 13245 |
This theorem is referenced by: sqoddm1div8 13419 cjmulval 14365 sqrlem5 14467 sqrlem6 14468 sqrlem7 14469 remsqsqrt 14477 sqrtmsq 14491 absid 14517 absre 14522 absresq 14523 abs1m 14556 abslem2 14560 sqreulem 14580 msqsqrtd 14661 tanval3 15347 sincossq 15389 cos2t 15391 sqrt2irrlem 15461 sqnprm 15902 isprm5 15907 coprimeprodsq 16001 pockthg 16098 4sqlem7 16136 4sqlem10 16139 mul4sqlem 16145 4sqlem12 16148 4sqlem15 16151 4sqlem16 16152 4sqlem17 16153 odadd2 18725 abvneg 19327 zringunit 20337 cphsubrglem 23484 rrxnm 23697 pjthlem1 23743 itgabs 24138 dvrec 24255 dvmptdiv 24274 dveflem 24279 tangtx 24794 tanregt0 24824 tanarg 24903 cxpsqrt 24987 lawcoslem1 25094 chordthmlem4 25114 heron 25117 quad2 25118 dcubic1lem 25122 dcubic1 25124 dcubic 25125 cubic2 25127 binom4 25129 dquartlem1 25130 dquartlem2 25131 dquart 25132 quart1lem 25134 asinsin 25171 cxp2limlem 25255 lgamgulmlem3 25310 wilthlem1 25347 basellem8 25367 chpub 25498 bposlem2 25563 lgssq 25615 lgssq2 25616 lgsquad3 25665 2sqlem3 25698 2sqlem8 25704 2sqmod 25714 chtppilimlem1 25751 rplogsumlem2 25763 dchrisum0lem1a 25764 dchrisum0lem1 25794 dchrisum0lem3 25797 mulog2sumlem1 25812 vmalogdivsum2 25816 logsqvma 25820 logdivbnd 25834 pntpbnd1a 25863 pntlemr 25880 pntlemf 25883 pntlemk 25884 pntlemo 25885 brbtwn2 26394 colinearalglem4 26398 htthlem 28473 pjhthlem1 28949 cnlnadjlem7 29631 branmfn 29663 leopnmid 29696 hgt750lemf 31578 hgt750leme 31583 pdivsq 32507 dvtan 34389 itgabsnc 34408 ftc1anclem3 34416 areacirclem1 34429 irrapxlem5 38825 pellexlem2 38829 pellexlem6 38833 rmxdbl 38938 jm2.18 38987 jm2.19lem1 38988 jm2.20nn 38996 jm2.25 38998 jm2.27c 39006 jm3.1lem2 39017 int-sqdefd 39905 int-sqgeq0d 39910 sqrlearg 41266 dvdivf 41643 wallispi2lem1 41793 stirlinglem1 41796 stirlinglem3 41798 stirlinglem10 41805 smfmullem1 42503 fmtnorec2lem 43078 fmtnorec3 43084 modexp2m1d 43151 itschlc0yqe 44121 itscnhlc0xyqsol 44126 itschlc0xyqsol1 44127 itschlc0xyqsol 44128 itsclc0xyqsolr 44130 |
Copyright terms: Public domain | W3C validator |