MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  addcomd Structured version   Visualization version   Unicode version
Theorem addcomd 10238
Description: Addition commutes. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.) (Revised by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
muld.1 |- ( ph -> A e. CC )
addcomd.2 |- ( ph -> B e. CC )
Assertion
Ref Expression
addcomd |- ( ph -> ( A + B ) = ( B + A ) )
Proof of Theorem addcomd
StepHypRef Expression
1 1cnd 10056 . . . . . . . 8 |- ( ph -> 1 e. CC )
21, 1addcld 10059 . . . . . . 7 |- ( ph -> ( 1 + 1 ) e. CC )
3 muld.1 . . . . . . 7 |- ( ph -> A e. CC )
4 addcomd.2 . . . . . . 7 |- ( ph -> B e. CC )
52, 3, 4adddid 10064 . . . . . 6 |- ( ph -> ( ( 1 + 1 ) x. ( A + B ) ) = ( ( ( 1 + 1 ) x. A ) + ( ( 1 + 1 ) x. B ) ) )
63, 4addcld 10059 . . . . . . 7 |- ( ph -> ( A + B ) e. CC )
7 1p1times 10207 . . . . . . 7 |- ( ( A + B ) e. CC -> ( ( 1 + 1 ) x. ( A + B ) ) = ( ( A + B ) + ( A + B ) ) )
86, 7syl 17 . . . . . 6 |- ( ph -> ( ( 1 + 1 ) x. ( A + B ) ) = ( ( A + B ) + ( A + B ) ) )
9 1p1times 10207 . . . . . . . 8 |- ( A e. CC -> ( ( 1 + 1 ) x. A ) = ( A + A ) )
103, 9syl 17 . . . . . . 7 |- ( ph -> ( ( 1 + 1 ) x. A ) = ( A + A ) )
11 1p1times 10207 . . . . . . . 8 |- ( B e. CC -> ( ( 1 + 1 ) x. B ) = ( B + B ) )
124, 11syl 17 . . . . . . 7 |- ( ph -> ( ( 1 + 1 ) x. B ) = ( B + B ) )
1310, 12oveq12d 6668 . . . . . 6 |- ( ph -> ( ( ( 1 + 1 ) x. A ) + ( ( 1 + 1 ) x. B ) ) = ( ( A + A ) + ( B + B ) ) )
145, 8, 133eqtr3rd 2665 . . . . 5 |- ( ph -> ( ( A + A ) + ( B + B ) ) = ( ( A + B ) + ( A + B ) ) )
153, 3addcld 10059 . . . . . 6 |- ( ph -> ( A + A ) e. CC )
1615, 4, 4addassd 10062 . . . . 5 |- ( ph -> ( ( ( A + A ) + B ) + B ) = ( ( A + A ) + ( B + B ) ) )
176, 3, 4addassd 10062 . . . . 5 |- ( ph -> ( ( ( A + B ) + A ) + B ) = ( ( A + B ) + ( A + B ) ) )
1814, 16, 173eqtr4d 2666 . . . 4 |- ( ph -> ( ( ( A + A ) + B ) + B ) = ( ( ( A + B ) + A ) + B ) )
1915, 4addcld 10059 . . . . 5 |- ( ph -> ( ( A + A ) + B ) e. CC )
206, 3addcld 10059 . . . . 5 |- ( ph -> ( ( A + B ) + A ) e. CC )
21 addcan2 10221 . . . . 5 |- ( ( ( ( A + A ) + B ) e. CC /\ ( ( A + B ) + A ) e. CC /\ B e. CC ) -> ( ( ( ( A + A ) + B ) + B ) = ( ( ( A + B ) + A ) + B ) <-> ( ( A + A ) + B ) = ( ( A + B ) + A ) ) )
2219, 20, 4, 21syl3anc 1326 . . . 4 |- ( ph -> ( ( ( ( A + A ) + B ) + B ) = ( ( ( A + B ) + A ) + B ) <-> ( ( A + A ) + B ) = ( ( A + B ) + A ) ) )
2318, 22mpbid 222 . . 3 |- ( ph -> ( ( A + A ) + B ) = ( ( A + B ) + A ) )
243, 3, 4addassd 10062 . . 3 |- ( ph -> ( ( A + A ) + B ) = ( A + ( A + B ) ) )
253, 4, 3addassd 10062 . . 3 |- ( ph -> ( ( A + B ) + A ) = ( A + ( B + A ) ) )
2623, 24, 253eqtr3d 2664 . 2 |- ( ph -> ( A + ( A + B ) ) = ( A + ( B + A ) ) )
274, 3addcld 10059 . . 3 |- ( ph -> ( B + A ) e. CC )
28 addcan 10220 . . 3 |- ( ( A e. CC /\ ( A + B ) e. CC /\ ( B + A ) e. CC ) -> ( ( A + ( A + B ) ) = ( A + ( B + A ) ) <-> ( A + B ) = ( B + A ) ) )
293, 6, 27, 28syl3anc 1326 . 2 |- ( ph -> ( ( A + ( A + B ) ) = ( A + ( B + A ) ) <-> ( A + B ) = ( B + A ) ) )
3026, 29mpbid 222 1 |- ( ph -> ( A + B ) = ( B + A ) )
Colors of variables: wff setvar class
Syntax hints:   -> wi 4   <-> wb 196   = wceq 1483   e. wcel 1990  (class class class)co 6650   CCcc 9934   1c1 9937   + caddc 9939   x. cmul 9941
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-po 5035  df-so 5036  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-ov 6653  df-er 7742  df-en 7956  df-dom 7957  df-sdom 7958  df-pnf 10076  df-mnf 10077  df-ltxr 10079
This theorem is referenced by:  muladd11r  10249  comraddd  10250  subadd2  10285  pncan  10287  npcan  10290  subcan  10336  subaddeqd  10446  addrsub  10448  ltadd1  10495  leadd2  10497  ltsubadd2  10499  lesubadd2  10501  lesub3d  10645  supadd  10991  ltaddrp2d  11906  lincmb01cmp  12315  iccf1o  12316  modaddabs  12708  muladdmodid  12710  negmod  12715  modadd2mod  12720  modadd12d  12726  modaddmulmod  12737  addmodlteq  12745  expaddz  12904  bcn2m1  13111  bcn2p1  13112  ccatrn  13372  addlenswrd  13438  spllen  13505  splfv2a  13507  relexpaddnn  13791  relexpaddg  13793  rtrclreclem3  13800  remullem  13868  sqreulem  14099  climaddc2  14366  clim2ser2  14386  iseraltlem2  14413  telfsumo  14534  fsumparts  14538  bcxmas  14567  bpoly4  14790  cosneg  14877  coshval  14885  sinadd  14894  sincossq  14906  cos2t  14908  absefi  14926  absefib  14928  dvdsaddre2b  15029  pwp1fsum  15114  sadadd2lem2  15172  bitsres  15195  bezoutlem2  15257  bezoutlem4  15259  pythagtrip  15539  pcadd2  15594  vdwapun  15678  vdwlem5  15689  vdwlem6  15690  vdwlem8  15692  gsumccat  17378  mulgnndir  17569  mulgnndirOLD  17570  mulgdirlem  17572  mulgdir  17573  sylow1lem1  18013  efgcpbllemb  18168  cygabl  18292  ablfacrp  18465  icccvx  22749  cnlmod  22940  cphipval  23042  pjthlem1  23208  ovolicc2lem4  23288  cmmbl  23302  voliunlem1  23318  itgmulc2  23600  dvle  23770  dvcvx  23783  dvfsumlem2  23790  dvfsumlem4  23792  dvfsum2  23797  ply1divex  23896  plymullem1  23970  coeeulem  23980  aaliou3lem6  24103  dvtaylp  24124  ulmcn  24153  abelthlem7  24192  pilem3  24207  rzgrp  24300  lawcos  24546  affineequiv  24553  heron  24565  quad2  24566  dcubic1lem  24570  dcubic2  24571  dcubic  24573  mcubic  24574  quart1lem  24582  quart1  24583  asinlem2  24596  asinsin  24619  cosasin  24631  atanlogaddlem  24640  atanlogadd  24641  cvxcl  24711  scvxcvx  24712  lgamgulmlem2  24756  lgamgulmlem3  24757  lgamcvg2  24781  lgam1  24790  bposlem9  25017  lgseisenlem1  25100  2sqlem3  25145  2sqblem  25156  dchrisumlem2  25179  selberg  25237  selberg2  25240  chpdifbndlem1  25242  selberg4  25250  pntrlog2bndlem1  25266  pntrlog2bndlem6  25272  pntibndlem2  25280  pntlemb  25286  pntlemf  25294  padicabv  25319  colinearalglem2  25787  axsegconlem9  25805  axeuclidlem  25842  eupth2lem3lem3  27090  numclwlk3lem3  27206  smcnlem  27552  ipval2  27562  hhph  28035  pjhthlem1  28250  golem1  29130  stcltrlem1  29135  bhmafibid2  29645  2sqmod  29648  omndmul2  29712  archirngz  29743  archiabllem1a  29745  archiabllem1  29747  archiabllem2c  29749  ballotlemsdom  30573  signshf  30665  fsum2dsub  30685  resconn  31228  iprodgam  31628  faclimlem1  31629  faclimlem3  31631  faclim  31632  iprodfac  31633  fwddifnp1  32272  dnibndlem7  32474  dnibndlem8  32475  knoppndvlem14  32516  bj-bary1  33162  dvtan  33460  itg2addnclem3  33463  itgaddnclem2  33469  itgmulc2nc  33478  ftc1anclem8  33492  dvasin  33496  areacirclem1  33500  pellexlem2  37394  pell14qrgt0  37423  rmxyadd  37486  rmxluc  37501  fzmaxdif  37548  acongeq  37550  jm2.19lem2  37557  jm2.26lem3  37568  areaquad  37802  int-addcomd  38476  int-leftdistd  38482  subadd4b  39494  sub31  39503  fsumsplit1  39804  coseq0  40075  coskpi2  40077  cosknegpi  40080  fperdvper  40133  dvbdfbdioolem2  40144  dvnmul  40158  dvmptfprodlem  40159  itgsincmulx  40190  itgsbtaddcnst  40198  stoweidlem11  40228  stirlinglem5  40295  stirlinglem7  40297  dirkertrigeqlem1  40315  dirkertrigeqlem2  40316  dirkertrigeqlem3  40317  dirkertrigeq  40318  dirkercncflem2  40321  fourierdlem4  40328  fourierdlem26  40350  fourierdlem40  40364  fourierdlem42  40366  fourierdlem47  40370  fourierdlem63  40386  fourierdlem64  40387  fourierdlem65  40388  fourierdlem74  40397  fourierdlem75  40398  fourierdlem78  40401  fourierdlem79  40402  fourierdlem84  40407  fourierdlem93  40416  fourierdlem103  40426  fourierdlem111  40434  fourierswlem  40447  fouriersw  40448  etransclem32  40483  etransclem46  40497  sge0gtfsumgt  40660  hoidmv1lelem2  40806  hoidmvlelem2  40810  hspmbllem1  40840  smfmullem1  40998  sigarperm  41049  2elfz2melfz  41328  fargshiftfo  41378  fmtnorec3  41460  2zrngacmnd  41942  2zrngagrp  41943  ply1mulgsumlem1  42174  m1modmmod  42316  onetansqsecsq  42502  mvlladdd  42513
  Copyright terms: Public domain W3C validator