Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 2halvesd | Structured version Visualization version GIF version |
Description: Two halves make a whole. (Contributed by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
2timesd.1 | ⊢ (𝜑 → 𝐴 ∈ ℂ) |
Ref | Expression |
---|---|
2halvesd | ⊢ (𝜑 → ((𝐴 / 2) + (𝐴 / 2)) = 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2timesd.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℂ) | |
2 | 2halves 12189 | . 2 ⊢ (𝐴 ∈ ℂ → ((𝐴 / 2) + (𝐴 / 2)) = 𝐴) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → ((𝐴 / 2) + (𝐴 / 2)) = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1539 ∈ wcel 2106 (class class class)co 7268 ℂcc 10857 + caddc 10862 / cdiv 11620 2c2 12016 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-sep 5222 ax-nul 5229 ax-pow 5287 ax-pr 5351 ax-un 7579 ax-resscn 10916 ax-1cn 10917 ax-icn 10918 ax-addcl 10919 ax-addrcl 10920 ax-mulcl 10921 ax-mulrcl 10922 ax-mulcom 10923 ax-addass 10924 ax-mulass 10925 ax-distr 10926 ax-i2m1 10927 ax-1ne0 10928 ax-1rid 10929 ax-rnegex 10930 ax-rrecex 10931 ax-cnre 10932 ax-pre-lttri 10933 ax-pre-lttrn 10934 ax-pre-ltadd 10935 ax-pre-mulgt0 10936 |
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 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-reu 3071 df-rmo 3072 df-rab 3073 df-v 3432 df-sbc 3717 df-csb 3833 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-nul 4258 df-if 4461 df-pw 4536 df-sn 4563 df-pr 4565 df-op 4569 df-uni 4841 df-br 5075 df-opab 5137 df-mpt 5158 df-id 5485 df-po 5499 df-so 5500 df-xp 5591 df-rel 5592 df-cnv 5593 df-co 5594 df-dm 5595 df-rn 5596 df-res 5597 df-ima 5598 df-iota 6385 df-fun 6429 df-fn 6430 df-f 6431 df-f1 6432 df-fo 6433 df-f1o 6434 df-fv 6435 df-riota 7225 df-ov 7271 df-oprab 7272 df-mpo 7273 df-er 8486 df-en 8722 df-dom 8723 df-sdom 8724 df-pnf 10999 df-mnf 11000 df-xr 11001 df-ltxr 11002 df-le 11003 df-sub 11195 df-neg 11196 df-div 11621 df-2 12024 |
This theorem is referenced by: reccn2 15294 mertenslem1 15584 sin01bnd 15882 prmreclem5 16609 4sqlem6 16632 4sqlem10 16636 4sqlem15 16648 4sqlem16 16649 blhalf 23546 methaus 23664 nrginvrcnlem 23843 opnreen 23982 iscau3 24430 ovollb2lem 24640 ovolunlem1a 24648 itg2cnlem2 24915 ulmcn 25546 ulmdvlem1 25547 cxpcn3lem 25888 chordthmlem4 25973 lgamgulmlem3 26168 ftalem2 26211 chtub 26348 lgsqrlem2 26483 lgseisenlem2 26512 lgsquadlem1 26516 2sqlem8 26562 mulog2sumlem1 26670 vmalogdivsum 26675 pntibndlem2 26727 lt2addrd 31060 le2halvesd 31064 dnizphlfeqhlf 34642 poimirlem29 35792 heicant 35798 mblfinlem4 35803 itg2addnclem 35814 ftc1anclem6 35841 ftc1anclem8 35843 heibor1lem 35953 aks4d1p1p4 40065 suplesup 42837 lptre2pt 43140 0ellimcdiv 43149 ioodvbdlimc1lem2 43432 ioodvbdlimc2lem 43434 dirkertrigeqlem2 43599 dirkercncflem1 43603 sge0xaddlem1 43930 hoiqssbllem2 44120 |
Copyright terms: Public domain | W3C validator |