![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sqvali | Structured version Visualization version GIF version |
Description: Value of square. Inference version. (Contributed by NM, 1-Aug-1999.) |
Ref | Expression |
---|---|
sqval.1 | ⊢ 𝐴 ∈ ℂ |
Ref | Expression |
---|---|
sqvali | ⊢ (𝐴↑2) = (𝐴 · 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sqval.1 | . 2 ⊢ 𝐴 ∈ ℂ | |
2 | sqval 13516 | . 2 ⊢ (𝐴 ∈ ℂ → (𝐴↑2) = (𝐴 · 𝐴)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴↑2) = (𝐴 · 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1539 ∈ wcel 2112 (class class class)co 7143 ℂcc 10558 · cmul 10565 2c2 11714 ↑cexp 13464 |
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 1912 ax-6 1971 ax-7 2016 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2159 ax-12 2176 ax-ext 2730 ax-sep 5162 ax-nul 5169 ax-pow 5227 ax-pr 5291 ax-un 7452 ax-cnex 10616 ax-resscn 10617 ax-1cn 10618 ax-icn 10619 ax-addcl 10620 ax-addrcl 10621 ax-mulcl 10622 ax-mulrcl 10623 ax-mulcom 10624 ax-addass 10625 ax-mulass 10626 ax-distr 10627 ax-i2m1 10628 ax-1ne0 10629 ax-1rid 10630 ax-rnegex 10631 ax-rrecex 10632 ax-cnre 10633 ax-pre-lttri 10634 ax-pre-lttrn 10635 ax-pre-ltadd 10636 ax-pre-mulgt0 10637 |
This theorem depends on definitions: df-bi 210 df-an 401 df-or 846 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2071 df-mo 2558 df-eu 2589 df-clab 2737 df-cleq 2751 df-clel 2831 df-nfc 2899 df-ne 2950 df-nel 3054 df-ral 3073 df-rex 3074 df-reu 3075 df-rab 3077 df-v 3409 df-sbc 3694 df-csb 3802 df-dif 3857 df-un 3859 df-in 3861 df-ss 3871 df-pss 3873 df-nul 4222 df-if 4414 df-pw 4489 df-sn 4516 df-pr 4518 df-tp 4520 df-op 4522 df-uni 4792 df-iun 4878 df-br 5026 df-opab 5088 df-mpt 5106 df-tr 5132 df-id 5423 df-eprel 5428 df-po 5436 df-so 5437 df-fr 5476 df-we 5478 df-xp 5523 df-rel 5524 df-cnv 5525 df-co 5526 df-dm 5527 df-rn 5528 df-res 5529 df-ima 5530 df-pred 6119 df-ord 6165 df-on 6166 df-lim 6167 df-suc 6168 df-iota 6287 df-fun 6330 df-fn 6331 df-f 6332 df-f1 6333 df-fo 6334 df-f1o 6335 df-fv 6336 df-riota 7101 df-ov 7146 df-oprab 7147 df-mpo 7148 df-om 7573 df-2nd 7687 df-wrecs 7950 df-recs 8011 df-rdg 8049 df-er 8292 df-en 8521 df-dom 8522 df-sdom 8523 df-pnf 10700 df-mnf 10701 df-xr 10702 df-ltxr 10703 df-le 10704 df-sub 10895 df-neg 10896 df-nn 11660 df-2 11722 df-n0 11920 df-z 12006 df-uz 12268 df-seq 13404 df-exp 13465 |
This theorem is referenced by: sqrecii 13581 sqdivi 13583 sqge0i 13586 lt2sqi 13587 le2sqi 13588 sq11i 13589 sq2 13595 sq3 13596 sq4e2t8 13597 i2 13600 expnass 13605 binom2i 13609 sq10 13659 3dec 13661 nn0le2msqi 13662 nn0opthlem1 13663 nn0opth2i 13666 faclbnd4lem1 13688 sqrtmsq2i 14780 pythagtriplem12 16203 pythagtriplem14 16205 prmlem1 16484 prmlem2 16496 4001prm 16521 mcubic 25517 dquartlem1 25521 quart1lem 25525 quart1 25526 log2ublem3 25618 birthday 25624 bposlem7 25958 bposlem8 25959 bposlem9 25960 ax5seglem7 26813 normlem1 28977 nmopcoadji 29968 dpmul4 30697 hgt750lem2 32136 quad3 33129 cntotbnd 35499 3lexlogpow5ineq1 39606 3lexlogpow5ineq5 39612 flt4lem5e 39970 resqrtvalex 40703 imsqrtvalex 40704 fmtno5lem4 44426 flsqrt5 44464 lighneallem4a 44478 |
Copyright terms: Public domain | W3C validator |