HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
GIF version
Theorem axaddass 5269
Description: Addition of complex numbers is associative. This theorem transfers the associative laws for the real and imaginary signed real components of complex number pairs, to complex number addition itself. Axiom 11 of 25 for real and complex numbers, derived from ZF set theory.
Assertion
Ref Expression
axaddass ⊢ ((A ∈ ℂ ⋀ B ∈ ℂ ⋀ C ∈ ℂ) → ((A + B) + C) = (A + (B + C)))
Proof of Theorem axaddass
StepHypRef Expression
1 dfcnqs 5254 . 2 ⊢ ℂ = ((R × R) / ◡E)
2 addcnsrec 5255 . 2 ⊢ (((x ∈ R ⋀ y ∈ R) ⋀ (z ∈ R ⋀ w ∈ R)) → ([⟨x, y⟩]◡E + [⟨z, w⟩]◡E) = [⟨(x +R z), (y +R w)⟩]◡E)
3 addcnsrec 5255 . 2 ⊢ (((z ∈ R ⋀ w ∈ R) ⋀ (v ∈ R ⋀ u ∈ R)) → ([⟨z, w⟩]◡E + [⟨v, u⟩]◡E) = [⟨(z +R v), (w +R u)⟩]◡E)
4 addcnsrec 5255 . 2 ⊢ ((((x +R z) ∈ R ⋀ (y +R w) ∈ R) ⋀ (v ∈ R ⋀ u ∈ R)) → ([⟨(x +R z), (y +R w)⟩]◡E + [⟨v, u⟩]◡E) = [⟨((x +R z) +R v), ((y +R w) +R u)⟩]◡E)
5 addcnsrec 5255 . 2 ⊢ (((x ∈ R ⋀ y ∈ R) ⋀ ((z +R v) ∈ R ⋀ (w +R u) ∈ R)) → ([⟨x, y⟩]◡E + [⟨(z +R v), (w +R u)⟩]◡E) = [⟨(x +R (z +R v)), (y +R (w +R u))⟩]◡E)
6 addclsr 5184 . . . 4 ⊢ ((x ∈ R ⋀ z ∈ R) → (x +R z) ∈ R)
7 addclsr 5184 . . . 4 ⊢ ((y ∈ R ⋀ w ∈ R) → (y +R w) ∈ R)
86, 7anim12i 333 . . 3 ⊢ (((x ∈ R ⋀ z ∈ R) ⋀ (y ∈ R ⋀ w ∈ R)) → ((x +R z) ∈ R ⋀ (y +R w) ∈ R))
98an4s 508 . 2 ⊢ (((x ∈ R ⋀ y ∈ R) ⋀ (z ∈ R ⋀ w ∈ R)) → ((x +R z) ∈ R ⋀ (y +R w) ∈ R))
10 addclsr 5184 . . . 4 ⊢ ((z ∈ R ⋀ v ∈ R) → (z +R v) ∈ R)
11 addclsr 5184 . . . 4 ⊢ ((w ∈ R ⋀ u ∈ R) → (w +R u) ∈ R)
1210, 11anim12i 333 . . 3 ⊢ (((z ∈ R ⋀ v ∈ R) ⋀ (w ∈ R ⋀ u ∈ R)) → ((z +R v) ∈ R ⋀ (w +R u) ∈ R))
1312an4s 508 . 2 ⊢ (((z ∈ R ⋀ w ∈ R) ⋀ (v ∈ R ⋀ u ∈ R)) → ((z +R v) ∈ R ⋀ (w +R u) ∈ R))
14 visset 1809 . . 3 ⊢ z ∈ V
15 visset 1809 . . 3 ⊢ v ∈ V
1614, 15addasssr 5189 . 2 ⊢ ((x +R z) +R v) = (x +R (z +R v))
17 visset 1809 . . 3 ⊢ w ∈ V
18 visset 1809 . . 3 ⊢ u ∈ V
1917, 18addasssr 5189 . 2 ⊢ ((y +R w) +R u) = (y +R (w +R u))
201, 2, 3, 4, 5, 9, 13, 16, 19ecoprass 4321 1 ⊢ ((A ∈ ℂ ⋀ B ∈ ℂ ⋀ C ∈ ℂ) → ((A + B) + C) = (A + (B + C)))
Colors of variables: wff set class
Syntax hints:   → wi 3   ⋀ wa 223   ⋀ w3a 774   = wceq 954   ∈ wcel 956  Ecep 2827  ◡ccnv 3169  (class class class)co 3965  Rcnr 4985   +R cplr 4989  ℂcc 5224   + caddc 5229
This theorem is referenced by:  addasst 5299  addass 5316  add12t 5328  add23t 5329  add4t 5330  cnegextlem1 5337  cnegext 5340  addcan 5343  negeu 5347  addsubasst 5375  muladdt 5413  nnaddclt 5908  nneo 6164  uzaddclt 6401  expaddt 6547  bernneq 6603  ser1absdiflem 6886  faclbnd6 6911  fsum1ps 6976  fsum3 6982  fsum4 6983  binomlem5 7028  bcxmaslem2 7033  bcxmas 7034  ser1cmp2 7133  cvgratlem1ALT 7202  cvgratlem1 7205  fsum0diaglem2 7212  efi4pt 7397  efivalt 7409  cnaddabl 8091  stadd3 10148  golem1 10171  mslb1 10545  2wsms 10546
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-9 963  ax-10 964  ax-11 965  ax-12 966  ax-13 967  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-rep 2689  ax-sep 2699  ax-nul 2706  ax-pow 2738  ax-pr 2775  ax-un 2865  ax-inf2 4617
This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 775  df-3an 776  df-ex 979  df-sb 1170  df-eu 1380  df-mo 1381  df-clab 1462  df-cleq 1467  df-clel 1470  df-ne 1584  df-ral 1646  df-rex 1647  df-reu 1648  df-rab 1649  df-v 1808  df-sbc 1938  df-csb 1998  df-dif 2045  df-un 2046  df-in 2047  df-ss 2049  df-pss 2051  df-nul 2277  df-if 2358  df-pw 2398  df-sn 2408  df-pr 2409  df-tp 2411  df-op 2412  df-uni 2500  df-int 2530  df-iun 2564  df-br 2616  df-opab 2663  df-tr 2677  df-eprel 2829  df-id 2832  df-po 2839  df-so 2849  df-fr 2916  df-we 2933  df-ord 2950  df-on 2951  df-lim 2952  df-suc 2953  df-om 3132  df-xp 3184  df-rel 3185  df-cnv 3186  df-co 3187  df-dm 3188  df-rn 3189  df-res 3190  df-ima 3191  df-fun 3192  df-fn 3193  df-f 3194  df-fv 3198  df-rdg 3934  df-opr 3967  df-oprab 3968  df-1st 4080  df-2nd 4081  df-1o 4134  df-oadd 4136  df-omul 4137  df-er 4262  df-ec 4264  df-qs 4267  df-ni 4992  df-pli 4993  df-mi 4994  df-lti 4995  df-plpq 5027  df-mpq 5028  df-enq 5029  df-nq 5030  df-plq 5031  df-mq 5032  df-rq 5033  df-ltq 5034  df-1q 5035  df-np 5078  df-plp 5080  df-ltp 5082  df-plpr 5156  df-enr 5158  df-nr 5159  df-plr 5160  df-c 5232  df-plus 5237
Copyright terms: Public domain