![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sqmuld | Structured version Visualization version GIF version |
Description: Distribution of square over multiplication. (Contributed by Mario Carneiro, 28-May-2016.) |
Ref | Expression |
---|---|
expcld.1 | ⊢ (𝜑 → 𝐴 ∈ ℂ) |
mulexpd.2 | ⊢ (𝜑 → 𝐵 ∈ ℂ) |
Ref | Expression |
---|---|
sqmuld | ⊢ (𝜑 → ((𝐴 · 𝐵)↑2) = ((𝐴↑2) · (𝐵↑2))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | expcld.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℂ) | |
2 | mulexpd.2 | . 2 ⊢ (𝜑 → 𝐵 ∈ ℂ) | |
3 | sqmul 13118 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 · 𝐵)↑2) = ((𝐴↑2) · (𝐵↑2))) | |
4 | 1, 2, 3 | syl2anc 696 | 1 ⊢ (𝜑 → ((𝐴 · 𝐵)↑2) = ((𝐴↑2) · (𝐵↑2))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1630 ∈ wcel 2137 (class class class)co 6811 ℂcc 10124 · cmul 10131 2c2 11260 ↑cexp 13052 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1869 ax-4 1884 ax-5 1986 ax-6 2052 ax-7 2088 ax-8 2139 ax-9 2146 ax-10 2166 ax-11 2181 ax-12 2194 ax-13 2389 ax-ext 2738 ax-sep 4931 ax-nul 4939 ax-pow 4990 ax-pr 5053 ax-un 7112 ax-cnex 10182 ax-resscn 10183 ax-1cn 10184 ax-icn 10185 ax-addcl 10186 ax-addrcl 10187 ax-mulcl 10188 ax-mulrcl 10189 ax-mulcom 10190 ax-addass 10191 ax-mulass 10192 ax-distr 10193 ax-i2m1 10194 ax-1ne0 10195 ax-1rid 10196 ax-rnegex 10197 ax-rrecex 10198 ax-cnre 10199 ax-pre-lttri 10200 ax-pre-lttrn 10201 ax-pre-ltadd 10202 ax-pre-mulgt0 10203 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1073 df-3an 1074 df-tru 1633 df-ex 1852 df-nf 1857 df-sb 2045 df-eu 2609 df-mo 2610 df-clab 2745 df-cleq 2751 df-clel 2754 df-nfc 2889 df-ne 2931 df-nel 3034 df-ral 3053 df-rex 3054 df-reu 3055 df-rab 3057 df-v 3340 df-sbc 3575 df-csb 3673 df-dif 3716 df-un 3718 df-in 3720 df-ss 3727 df-pss 3729 df-nul 4057 df-if 4229 df-pw 4302 df-sn 4320 df-pr 4322 df-tp 4324 df-op 4326 df-uni 4587 df-iun 4672 df-br 4803 df-opab 4863 df-mpt 4880 df-tr 4903 df-id 5172 df-eprel 5177 df-po 5185 df-so 5186 df-fr 5223 df-we 5225 df-xp 5270 df-rel 5271 df-cnv 5272 df-co 5273 df-dm 5274 df-rn 5275 df-res 5276 df-ima 5277 df-pred 5839 df-ord 5885 df-on 5886 df-lim 5887 df-suc 5888 df-iota 6010 df-fun 6049 df-fn 6050 df-f 6051 df-f1 6052 df-fo 6053 df-f1o 6054 df-fv 6055 df-riota 6772 df-ov 6814 df-oprab 6815 df-mpt2 6816 df-om 7229 df-2nd 7332 df-wrecs 7574 df-recs 7635 df-rdg 7673 df-er 7909 df-en 8120 df-dom 8121 df-sdom 8122 df-pnf 10266 df-mnf 10267 df-xr 10268 df-ltxr 10269 df-le 10270 df-sub 10458 df-neg 10459 df-nn 11211 df-2 11269 df-n0 11483 df-z 11568 df-uz 11878 df-seq 12994 df-exp 13053 |
This theorem is referenced by: sqoddm1div8 13220 sqrtmul 14197 sqreulem 14296 pythagtriplem1 15721 prmreclem1 15820 ipcau2 23231 csbren 23380 chordthmlem4 24759 heron 24762 quad2 24763 dquart 24777 cxp2limlem 24899 basellem8 25011 lgsdir 25254 2sqlem3 25342 2sqlem4 25343 2sqlem8 25348 2sqblem 25353 axsegconlem9 26002 ax5seglem1 26005 ax5seglem2 26006 ax5seglem3 26008 bhmafibid1 29951 2sqmod 29955 rrndstprj2 33941 pellexlem6 37898 pell1234qrne0 37917 pell1234qrreccl 37918 pell1234qrmulcl 37919 pell14qrgt0 37923 pell14qrdich 37933 rmxyneg 37985 wallispi2lem1 40789 stirlinglem3 40794 stirlinglem10 40801 |
Copyright terms: Public domain | W3C validator |