ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  cnegex Structured version   GIF version

Theorem cnegex 6791
Description: Existence of the negative of a complex number. (Contributed by Eric Schmidt, 21-May-2007.)
Assertion
Ref Expression
cnegex (A ℂ → x ℂ (A + x) = 0)
Distinct variable group:   x,A

Proof of Theorem cnegex
Dummy variables 𝑎 𝑏 𝑐 𝑑 y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cnre 6626 . 2 (A ℂ → 𝑎 𝑏 A = (𝑎 + (i · 𝑏)))
2 cnegexlem2 6789 . . . . 5 y ℝ (i · y)
3 cnegexlem3 6790 . . . . . . . 8 ((𝑏 y ℝ) → 𝑐 ℝ (𝑏 + 𝑐) = y)
43ad2ant2lr 467 . . . . . . 7 (((𝑎 𝑏 ℝ) (y (i · y) ℝ)) → 𝑐 ℝ (𝑏 + 𝑐) = y)
5 ax-icn 6585 . . . . . . . . . . . . . 14 i
6 recn 6617 . . . . . . . . . . . . . 14 (𝑐 ℝ → 𝑐 ℂ)
7 mulcl 6611 . . . . . . . . . . . . . 14 ((i 𝑐 ℂ) → (i · 𝑐) ℂ)
85, 6, 7sylancr 395 . . . . . . . . . . . . 13 (𝑐 ℝ → (i · 𝑐) ℂ)
9 recn 6617 . . . . . . . . . . . . 13 (𝑑 ℝ → 𝑑 ℂ)
10 addcl 6609 . . . . . . . . . . . . 13 (((i · 𝑐) 𝑑 ℂ) → ((i · 𝑐) + 𝑑) ℂ)
118, 9, 10syl2an 273 . . . . . . . . . . . 12 ((𝑐 𝑑 ℝ) → ((i · 𝑐) + 𝑑) ℂ)
1211adantlr 449 . . . . . . . . . . 11 (((𝑐 (𝑏 + 𝑐) = y) 𝑑 ℝ) → ((i · 𝑐) + 𝑑) ℂ)
1312adantll 448 . . . . . . . . . 10 (((((𝑎 𝑏 ℝ) (y (i · y) ℝ)) (𝑐 (𝑏 + 𝑐) = y)) 𝑑 ℝ) → ((i · 𝑐) + 𝑑) ℂ)
1413adantr 261 . . . . . . . . 9 ((((((𝑎 𝑏 ℝ) (y (i · y) ℝ)) (𝑐 (𝑏 + 𝑐) = y)) 𝑑 ℝ) ((𝑎 + (i · y)) + 𝑑) = 0) → ((i · 𝑐) + 𝑑) ℂ)
15 recn 6617 . . . . . . . . . . . . . . . . 17 (𝑎 ℝ → 𝑎 ℂ)
16 recn 6617 . . . . . . . . . . . . . . . . 17 (𝑏 ℝ → 𝑏 ℂ)
1715, 16anim12i 321 . . . . . . . . . . . . . . . 16 ((𝑎 𝑏 ℝ) → (𝑎 𝑏 ℂ))
1817, 6anim12i 321 . . . . . . . . . . . . . . 15 (((𝑎 𝑏 ℝ) 𝑐 ℝ) → ((𝑎 𝑏 ℂ) 𝑐 ℂ))
19 mulcl 6611 . . . . . . . . . . . . . . . . . . . 20 ((i 𝑏 ℂ) → (i · 𝑏) ℂ)
205, 19mpan 402 . . . . . . . . . . . . . . . . . . 19 (𝑏 ℂ → (i · 𝑏) ℂ)
21 addcl 6609 . . . . . . . . . . . . . . . . . . 19 ((𝑎 (i · 𝑏) ℂ) → (𝑎 + (i · 𝑏)) ℂ)
2220, 21sylan2 270 . . . . . . . . . . . . . . . . . 18 ((𝑎 𝑏 ℂ) → (𝑎 + (i · 𝑏)) ℂ)
2322ad2antrr 460 . . . . . . . . . . . . . . . . 17 ((((𝑎 𝑏 ℂ) 𝑐 ℂ) 𝑑 ℂ) → (𝑎 + (i · 𝑏)) ℂ)
245, 7mpan 402 . . . . . . . . . . . . . . . . . 18 (𝑐 ℂ → (i · 𝑐) ℂ)
2524ad2antlr 462 . . . . . . . . . . . . . . . . 17 ((((𝑎 𝑏 ℂ) 𝑐 ℂ) 𝑑 ℂ) → (i · 𝑐) ℂ)
26 simpr 103 . . . . . . . . . . . . . . . . 17 ((((𝑎 𝑏 ℂ) 𝑐 ℂ) 𝑑 ℂ) → 𝑑 ℂ)
2723, 25, 26addassd 6652 . . . . . . . . . . . . . . . 16 ((((𝑎 𝑏 ℂ) 𝑐 ℂ) 𝑑 ℂ) → (((𝑎 + (i · 𝑏)) + (i · 𝑐)) + 𝑑) = ((𝑎 + (i · 𝑏)) + ((i · 𝑐) + 𝑑)))
28 simpll 469 . . . . . . . . . . . . . . . . . . . 20 (((𝑎 𝑏 ℂ) 𝑐 ℂ) → 𝑎 ℂ)
2920ad2antlr 462 . . . . . . . . . . . . . . . . . . . 20 (((𝑎 𝑏 ℂ) 𝑐 ℂ) → (i · 𝑏) ℂ)
3024adantl 262 . . . . . . . . . . . . . . . . . . . 20 (((𝑎 𝑏 ℂ) 𝑐 ℂ) → (i · 𝑐) ℂ)
3128, 29, 30addassd 6652 . . . . . . . . . . . . . . . . . . 19 (((𝑎 𝑏 ℂ) 𝑐 ℂ) → ((𝑎 + (i · 𝑏)) + (i · 𝑐)) = (𝑎 + ((i · 𝑏) + (i · 𝑐))))
32 adddi 6616 . . . . . . . . . . . . . . . . . . . . . 22 ((i 𝑏 𝑐 ℂ) → (i · (𝑏 + 𝑐)) = ((i · 𝑏) + (i · 𝑐)))
335, 32mp3an1 1202 . . . . . . . . . . . . . . . . . . . . 21 ((𝑏 𝑐 ℂ) → (i · (𝑏 + 𝑐)) = ((i · 𝑏) + (i · 𝑐)))
3433adantll 448 . . . . . . . . . . . . . . . . . . . 20 (((𝑎 𝑏 ℂ) 𝑐 ℂ) → (i · (𝑏 + 𝑐)) = ((i · 𝑏) + (i · 𝑐)))
3534oveq2d 5448 . . . . . . . . . . . . . . . . . . 19 (((𝑎 𝑏 ℂ) 𝑐 ℂ) → (𝑎 + (i · (𝑏 + 𝑐))) = (𝑎 + ((i · 𝑏) + (i · 𝑐))))
3631, 35eqtr4d 2053 . . . . . . . . . . . . . . . . . 18 (((𝑎 𝑏 ℂ) 𝑐 ℂ) → ((𝑎 + (i · 𝑏)) + (i · 𝑐)) = (𝑎 + (i · (𝑏 + 𝑐))))
3736adantr 261 . . . . . . . . . . . . . . . . 17 ((((𝑎 𝑏 ℂ) 𝑐 ℂ) 𝑑 ℂ) → ((𝑎 + (i · 𝑏)) + (i · 𝑐)) = (𝑎 + (i · (𝑏 + 𝑐))))
3837oveq1d 5447 . . . . . . . . . . . . . . . 16 ((((𝑎 𝑏 ℂ) 𝑐 ℂ) 𝑑 ℂ) → (((𝑎 + (i · 𝑏)) + (i · 𝑐)) + 𝑑) = ((𝑎 + (i · (𝑏 + 𝑐))) + 𝑑))
3927, 38eqtr3d 2052 . . . . . . . . . . . . . . 15 ((((𝑎 𝑏 ℂ) 𝑐 ℂ) 𝑑 ℂ) → ((𝑎 + (i · 𝑏)) + ((i · 𝑐) + 𝑑)) = ((𝑎 + (i · (𝑏 + 𝑐))) + 𝑑))
4018, 9, 39syl2an 273 . . . . . . . . . . . . . 14 ((((𝑎 𝑏 ℝ) 𝑐 ℝ) 𝑑 ℝ) → ((𝑎 + (i · 𝑏)) + ((i · 𝑐) + 𝑑)) = ((𝑎 + (i · (𝑏 + 𝑐))) + 𝑑))
4140adantlrr 455 . . . . . . . . . . . . 13 ((((𝑎 𝑏 ℝ) (𝑐 (𝑏 + 𝑐) = y)) 𝑑 ℝ) → ((𝑎 + (i · 𝑏)) + ((i · 𝑐) + 𝑑)) = ((𝑎 + (i · (𝑏 + 𝑐))) + 𝑑))
42 oveq2 5440 . . . . . . . . . . . . . . . . 17 ((𝑏 + 𝑐) = y → (i · (𝑏 + 𝑐)) = (i · y))
4342oveq2d 5448 . . . . . . . . . . . . . . . 16 ((𝑏 + 𝑐) = y → (𝑎 + (i · (𝑏 + 𝑐))) = (𝑎 + (i · y)))
4443oveq1d 5447 . . . . . . . . . . . . . . 15 ((𝑏 + 𝑐) = y → ((𝑎 + (i · (𝑏 + 𝑐))) + 𝑑) = ((𝑎 + (i · y)) + 𝑑))
4544adantl 262 . . . . . . . . . . . . . 14 ((𝑐 (𝑏 + 𝑐) = y) → ((𝑎 + (i · (𝑏 + 𝑐))) + 𝑑) = ((𝑎 + (i · y)) + 𝑑))
4645ad2antlr 462 . . . . . . . . . . . . 13 ((((𝑎 𝑏 ℝ) (𝑐 (𝑏 + 𝑐) = y)) 𝑑 ℝ) → ((𝑎 + (i · (𝑏 + 𝑐))) + 𝑑) = ((𝑎 + (i · y)) + 𝑑))
4741, 46eqtr2d 2051 . . . . . . . . . . . 12 ((((𝑎 𝑏 ℝ) (𝑐 (𝑏 + 𝑐) = y)) 𝑑 ℝ) → ((𝑎 + (i · y)) + 𝑑) = ((𝑎 + (i · 𝑏)) + ((i · 𝑐) + 𝑑)))
4847adantllr 453 . . . . . . . . . . 11 (((((𝑎 𝑏 ℝ) (y (i · y) ℝ)) (𝑐 (𝑏 + 𝑐) = y)) 𝑑 ℝ) → ((𝑎 + (i · y)) + 𝑑) = ((𝑎 + (i · 𝑏)) + ((i · 𝑐) + 𝑑)))
4948eqeq1d 2026 . . . . . . . . . 10 (((((𝑎 𝑏 ℝ) (y (i · y) ℝ)) (𝑐 (𝑏 + 𝑐) = y)) 𝑑 ℝ) → (((𝑎 + (i · y)) + 𝑑) = 0 ↔ ((𝑎 + (i · 𝑏)) + ((i · 𝑐) + 𝑑)) = 0))
5049biimpa 280 . . . . . . . . 9 ((((((𝑎 𝑏 ℝ) (y (i · y) ℝ)) (𝑐 (𝑏 + 𝑐) = y)) 𝑑 ℝ) ((𝑎 + (i · y)) + 𝑑) = 0) → ((𝑎 + (i · 𝑏)) + ((i · 𝑐) + 𝑑)) = 0)
51 oveq2 5440 . . . . . . . . . . 11 (x = ((i · 𝑐) + 𝑑) → ((𝑎 + (i · 𝑏)) + x) = ((𝑎 + (i · 𝑏)) + ((i · 𝑐) + 𝑑)))
5251eqeq1d 2026 . . . . . . . . . 10 (x = ((i · 𝑐) + 𝑑) → (((𝑎 + (i · 𝑏)) + x) = 0 ↔ ((𝑎 + (i · 𝑏)) + ((i · 𝑐) + 𝑑)) = 0))
5352rspcev 2629 . . . . . . . . 9 ((((i · 𝑐) + 𝑑) ((𝑎 + (i · 𝑏)) + ((i · 𝑐) + 𝑑)) = 0) → x ℂ ((𝑎 + (i · 𝑏)) + x) = 0)
5414, 50, 53syl2anc 393 . . . . . . . 8 ((((((𝑎 𝑏 ℝ) (y (i · y) ℝ)) (𝑐 (𝑏 + 𝑐) = y)) 𝑑 ℝ) ((𝑎 + (i · y)) + 𝑑) = 0) → x ℂ ((𝑎 + (i · 𝑏)) + x) = 0)
55 readdcl 6610 . . . . . . . . . . 11 ((𝑎 (i · y) ℝ) → (𝑎 + (i · y)) ℝ)
56 ax-rnegex 6599 . . . . . . . . . . 11 ((𝑎 + (i · y)) ℝ → 𝑑 ℝ ((𝑎 + (i · y)) + 𝑑) = 0)
5755, 56syl 14 . . . . . . . . . 10 ((𝑎 (i · y) ℝ) → 𝑑 ℝ ((𝑎 + (i · y)) + 𝑑) = 0)
5857ad2ant2rl 468 . . . . . . . . 9 (((𝑎 𝑏 ℝ) (y (i · y) ℝ)) → 𝑑 ℝ ((𝑎 + (i · y)) + 𝑑) = 0)
5958adantr 261 . . . . . . . 8 ((((𝑎 𝑏 ℝ) (y (i · y) ℝ)) (𝑐 (𝑏 + 𝑐) = y)) → 𝑑 ℝ ((𝑎 + (i · y)) + 𝑑) = 0)
6054, 59r19.29a 2428 . . . . . . 7 ((((𝑎 𝑏 ℝ) (y (i · y) ℝ)) (𝑐 (𝑏 + 𝑐) = y)) → x ℂ ((𝑎 + (i · 𝑏)) + x) = 0)
614, 60rexlimddv 2411 . . . . . 6 (((𝑎 𝑏 ℝ) (y (i · y) ℝ)) → x ℂ ((𝑎 + (i · 𝑏)) + x) = 0)
6261rexlimdvaa 2408 . . . . 5 ((𝑎 𝑏 ℝ) → (y ℝ (i · y) ℝ → x ℂ ((𝑎 + (i · 𝑏)) + x) = 0))
632, 62mpi 15 . . . 4 ((𝑎 𝑏 ℝ) → x ℂ ((𝑎 + (i · 𝑏)) + x) = 0)
64 oveq1 5439 . . . . . 6 (A = (𝑎 + (i · 𝑏)) → (A + x) = ((𝑎 + (i · 𝑏)) + x))
6564eqeq1d 2026 . . . . 5 (A = (𝑎 + (i · 𝑏)) → ((A + x) = 0 ↔ ((𝑎 + (i · 𝑏)) + x) = 0))
6665rexbidv 2301 . . . 4 (A = (𝑎 + (i · 𝑏)) → (x ℂ (A + x) = 0 ↔ x ℂ ((𝑎 + (i · 𝑏)) + x) = 0))
6763, 66syl5ibrcom 146 . . 3 ((𝑎 𝑏 ℝ) → (A = (𝑎 + (i · 𝑏)) → x ℂ (A + x) = 0))
6867rexlimivv 2412 . 2 (𝑎 𝑏 A = (𝑎 + (i · 𝑏)) → x ℂ (A + x) = 0)
691, 68syl 14 1 (A ℂ → x ℂ (A + x) = 0)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97   = wceq 1226   wcel 1370  wrex 2281  (class class class)co 5432  cc 6522  cr 6523  0cc0 6524  ici 6526   + caddc 6527   · cmul 6529
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 617  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-8 1372  ax-10 1373  ax-11 1374  ax-i12 1375  ax-bnd 1376  ax-4 1377  ax-17 1396  ax-i9 1400  ax-ial 1405  ax-i5r 1406  ax-ext 2000  ax-resscn 6582  ax-1cn 6583  ax-icn 6585  ax-addcl 6586  ax-addrcl 6587  ax-mulcl 6588  ax-addcom 6590  ax-addass 6592  ax-distr 6594  ax-i2m1 6595  ax-0id 6598  ax-rnegex 6599  ax-cnre 6601
This theorem depends on definitions:  df-bi 110  df-3an 873  df-tru 1229  df-nf 1326  df-sb 1624  df-clab 2005  df-cleq 2011  df-clel 2014  df-nfc 2145  df-ral 2285  df-rex 2286  df-v 2533  df-un 2895  df-in 2897  df-ss 2904  df-sn 3352  df-pr 3353  df-op 3355  df-uni 3551  df-br 3735  df-iota 4790  df-fv 4833  df-ov 5435
This theorem is referenced by:  cnegex2  6792  addcan2  6794  0cnALT  6803  negeu  6804
  Copyright terms: Public domain W3C validator