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

Theorem cnegex 6966
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 6801 . 2 (A ℂ → 𝑎 𝑏 A = (𝑎 + (i · 𝑏)))
2 cnegexlem2 6964 . . . . 5 y ℝ (i · y)
3 cnegexlem3 6965 . . . . . . . 8 ((𝑏 y ℝ) → 𝑐 ℝ (𝑏 + 𝑐) = y)
43ad2ant2lr 479 . . . . . . 7 (((𝑎 𝑏 ℝ) (y (i · y) ℝ)) → 𝑐 ℝ (𝑏 + 𝑐) = y)
5 ax-icn 6758 . . . . . . . . . . . . . 14 i
6 recn 6792 . . . . . . . . . . . . . 14 (𝑐 ℝ → 𝑐 ℂ)
7 mulcl 6786 . . . . . . . . . . . . . 14 ((i 𝑐 ℂ) → (i · 𝑐) ℂ)
85, 6, 7sylancr 393 . . . . . . . . . . . . 13 (𝑐 ℝ → (i · 𝑐) ℂ)
9 recn 6792 . . . . . . . . . . . . 13 (𝑑 ℝ → 𝑑 ℂ)
10 addcl 6784 . . . . . . . . . . . . 13 (((i · 𝑐) 𝑑 ℂ) → ((i · 𝑐) + 𝑑) ℂ)
118, 9, 10syl2an 273 . . . . . . . . . . . 12 ((𝑐 𝑑 ℝ) → ((i · 𝑐) + 𝑑) ℂ)
1211adantlr 446 . . . . . . . . . . 11 (((𝑐 (𝑏 + 𝑐) = y) 𝑑 ℝ) → ((i · 𝑐) + 𝑑) ℂ)
1312adantll 445 . . . . . . . . . 10 (((((𝑎 𝑏 ℝ) (y (i · y) ℝ)) (𝑐 (𝑏 + 𝑐) = y)) 𝑑 ℝ) → ((i · 𝑐) + 𝑑) ℂ)
1413adantr 261 . . . . . . . . 9 ((((((𝑎 𝑏 ℝ) (y (i · y) ℝ)) (𝑐 (𝑏 + 𝑐) = y)) 𝑑 ℝ) ((𝑎 + (i · y)) + 𝑑) = 0) → ((i · 𝑐) + 𝑑) ℂ)
15 recn 6792 . . . . . . . . . . . . . . . . 17 (𝑎 ℝ → 𝑎 ℂ)
16 recn 6792 . . . . . . . . . . . . . . . . 17 (𝑏 ℝ → 𝑏 ℂ)
1715, 16anim12i 321 . . . . . . . . . . . . . . . 16 ((𝑎 𝑏 ℝ) → (𝑎 𝑏 ℂ))
1817, 6anim12i 321 . . . . . . . . . . . . . . 15 (((𝑎 𝑏 ℝ) 𝑐 ℝ) → ((𝑎 𝑏 ℂ) 𝑐 ℂ))
19 mulcl 6786 . . . . . . . . . . . . . . . . . . . 20 ((i 𝑏 ℂ) → (i · 𝑏) ℂ)
205, 19mpan 400 . . . . . . . . . . . . . . . . . . 19 (𝑏 ℂ → (i · 𝑏) ℂ)
21 addcl 6784 . . . . . . . . . . . . . . . . . . 19 ((𝑎 (i · 𝑏) ℂ) → (𝑎 + (i · 𝑏)) ℂ)
2220, 21sylan2 270 . . . . . . . . . . . . . . . . . 18 ((𝑎 𝑏 ℂ) → (𝑎 + (i · 𝑏)) ℂ)
2322ad2antrr 457 . . . . . . . . . . . . . . . . 17 ((((𝑎 𝑏 ℂ) 𝑐 ℂ) 𝑑 ℂ) → (𝑎 + (i · 𝑏)) ℂ)
245, 7mpan 400 . . . . . . . . . . . . . . . . . 18 (𝑐 ℂ → (i · 𝑐) ℂ)
2524ad2antlr 458 . . . . . . . . . . . . . . . . 17 ((((𝑎 𝑏 ℂ) 𝑐 ℂ) 𝑑 ℂ) → (i · 𝑐) ℂ)
26 simpr 103 . . . . . . . . . . . . . . . . 17 ((((𝑎 𝑏 ℂ) 𝑐 ℂ) 𝑑 ℂ) → 𝑑 ℂ)
2723, 25, 26addassd 6827 . . . . . . . . . . . . . . . 16 ((((𝑎 𝑏 ℂ) 𝑐 ℂ) 𝑑 ℂ) → (((𝑎 + (i · 𝑏)) + (i · 𝑐)) + 𝑑) = ((𝑎 + (i · 𝑏)) + ((i · 𝑐) + 𝑑)))
28 simpll 481 . . . . . . . . . . . . . . . . . . . 20 (((𝑎 𝑏 ℂ) 𝑐 ℂ) → 𝑎 ℂ)
2920ad2antlr 458 . . . . . . . . . . . . . . . . . . . 20 (((𝑎 𝑏 ℂ) 𝑐 ℂ) → (i · 𝑏) ℂ)
3024adantl 262 . . . . . . . . . . . . . . . . . . . 20 (((𝑎 𝑏 ℂ) 𝑐 ℂ) → (i · 𝑐) ℂ)
3128, 29, 30addassd 6827 . . . . . . . . . . . . . . . . . . 19 (((𝑎 𝑏 ℂ) 𝑐 ℂ) → ((𝑎 + (i · 𝑏)) + (i · 𝑐)) = (𝑎 + ((i · 𝑏) + (i · 𝑐))))
32 adddi 6791 . . . . . . . . . . . . . . . . . . . . . 22 ((i 𝑏 𝑐 ℂ) → (i · (𝑏 + 𝑐)) = ((i · 𝑏) + (i · 𝑐)))
335, 32mp3an1 1218 . . . . . . . . . . . . . . . . . . . . 21 ((𝑏 𝑐 ℂ) → (i · (𝑏 + 𝑐)) = ((i · 𝑏) + (i · 𝑐)))
3433adantll 445 . . . . . . . . . . . . . . . . . . . 20 (((𝑎 𝑏 ℂ) 𝑐 ℂ) → (i · (𝑏 + 𝑐)) = ((i · 𝑏) + (i · 𝑐)))
3534oveq2d 5471 . . . . . . . . . . . . . . . . . . 19 (((𝑎 𝑏 ℂ) 𝑐 ℂ) → (𝑎 + (i · (𝑏 + 𝑐))) = (𝑎 + ((i · 𝑏) + (i · 𝑐))))
3631, 35eqtr4d 2072 . . . . . . . . . . . . . . . . . 18 (((𝑎 𝑏 ℂ) 𝑐 ℂ) → ((𝑎 + (i · 𝑏)) + (i · 𝑐)) = (𝑎 + (i · (𝑏 + 𝑐))))
3736adantr 261 . . . . . . . . . . . . . . . . 17 ((((𝑎 𝑏 ℂ) 𝑐 ℂ) 𝑑 ℂ) → ((𝑎 + (i · 𝑏)) + (i · 𝑐)) = (𝑎 + (i · (𝑏 + 𝑐))))
3837oveq1d 5470 . . . . . . . . . . . . . . . 16 ((((𝑎 𝑏 ℂ) 𝑐 ℂ) 𝑑 ℂ) → (((𝑎 + (i · 𝑏)) + (i · 𝑐)) + 𝑑) = ((𝑎 + (i · (𝑏 + 𝑐))) + 𝑑))
3927, 38eqtr3d 2071 . . . . . . . . . . . . . . 15 ((((𝑎 𝑏 ℂ) 𝑐 ℂ) 𝑑 ℂ) → ((𝑎 + (i · 𝑏)) + ((i · 𝑐) + 𝑑)) = ((𝑎 + (i · (𝑏 + 𝑐))) + 𝑑))
4018, 9, 39syl2an 273 . . . . . . . . . . . . . 14 ((((𝑎 𝑏 ℝ) 𝑐 ℝ) 𝑑 ℝ) → ((𝑎 + (i · 𝑏)) + ((i · 𝑐) + 𝑑)) = ((𝑎 + (i · (𝑏 + 𝑐))) + 𝑑))
4140adantlrr 452 . . . . . . . . . . . . 13 ((((𝑎 𝑏 ℝ) (𝑐 (𝑏 + 𝑐) = y)) 𝑑 ℝ) → ((𝑎 + (i · 𝑏)) + ((i · 𝑐) + 𝑑)) = ((𝑎 + (i · (𝑏 + 𝑐))) + 𝑑))
42 oveq2 5463 . . . . . . . . . . . . . . . . 17 ((𝑏 + 𝑐) = y → (i · (𝑏 + 𝑐)) = (i · y))
4342oveq2d 5471 . . . . . . . . . . . . . . . 16 ((𝑏 + 𝑐) = y → (𝑎 + (i · (𝑏 + 𝑐))) = (𝑎 + (i · y)))
4443oveq1d 5470 . . . . . . . . . . . . . . 15 ((𝑏 + 𝑐) = y → ((𝑎 + (i · (𝑏 + 𝑐))) + 𝑑) = ((𝑎 + (i · y)) + 𝑑))
4544adantl 262 . . . . . . . . . . . . . 14 ((𝑐 (𝑏 + 𝑐) = y) → ((𝑎 + (i · (𝑏 + 𝑐))) + 𝑑) = ((𝑎 + (i · y)) + 𝑑))
4645ad2antlr 458 . . . . . . . . . . . . 13 ((((𝑎 𝑏 ℝ) (𝑐 (𝑏 + 𝑐) = y)) 𝑑 ℝ) → ((𝑎 + (i · (𝑏 + 𝑐))) + 𝑑) = ((𝑎 + (i · y)) + 𝑑))
4741, 46eqtr2d 2070 . . . . . . . . . . . 12 ((((𝑎 𝑏 ℝ) (𝑐 (𝑏 + 𝑐) = y)) 𝑑 ℝ) → ((𝑎 + (i · y)) + 𝑑) = ((𝑎 + (i · 𝑏)) + ((i · 𝑐) + 𝑑)))
4847adantllr 450 . . . . . . . . . . 11 (((((𝑎 𝑏 ℝ) (y (i · y) ℝ)) (𝑐 (𝑏 + 𝑐) = y)) 𝑑 ℝ) → ((𝑎 + (i · y)) + 𝑑) = ((𝑎 + (i · 𝑏)) + ((i · 𝑐) + 𝑑)))
4948eqeq1d 2045 . . . . . . . . . 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 5463 . . . . . . . . . . 11 (x = ((i · 𝑐) + 𝑑) → ((𝑎 + (i · 𝑏)) + x) = ((𝑎 + (i · 𝑏)) + ((i · 𝑐) + 𝑑)))
5251eqeq1d 2045 . . . . . . . . . 10 (x = ((i · 𝑐) + 𝑑) → (((𝑎 + (i · 𝑏)) + x) = 0 ↔ ((𝑎 + (i · 𝑏)) + ((i · 𝑐) + 𝑑)) = 0))
5352rspcev 2650 . . . . . . . . 9 ((((i · 𝑐) + 𝑑) ((𝑎 + (i · 𝑏)) + ((i · 𝑐) + 𝑑)) = 0) → x ℂ ((𝑎 + (i · 𝑏)) + x) = 0)
5414, 50, 53syl2anc 391 . . . . . . . 8 ((((((𝑎 𝑏 ℝ) (y (i · y) ℝ)) (𝑐 (𝑏 + 𝑐) = y)) 𝑑 ℝ) ((𝑎 + (i · y)) + 𝑑) = 0) → x ℂ ((𝑎 + (i · 𝑏)) + x) = 0)
55 readdcl 6785 . . . . . . . . . . 11 ((𝑎 (i · y) ℝ) → (𝑎 + (i · y)) ℝ)
56 ax-rnegex 6772 . . . . . . . . . . 11 ((𝑎 + (i · y)) ℝ → 𝑑 ℝ ((𝑎 + (i · y)) + 𝑑) = 0)
5755, 56syl 14 . . . . . . . . . 10 ((𝑎 (i · y) ℝ) → 𝑑 ℝ ((𝑎 + (i · y)) + 𝑑) = 0)
5857ad2ant2rl 480 . . . . . . . . 9 (((𝑎 𝑏 ℝ) (y (i · y) ℝ)) → 𝑑 ℝ ((𝑎 + (i · y)) + 𝑑) = 0)
5958adantr 261 . . . . . . . 8 ((((𝑎 𝑏 ℝ) (y (i · y) ℝ)) (𝑐 (𝑏 + 𝑐) = y)) → 𝑑 ℝ ((𝑎 + (i · y)) + 𝑑) = 0)
6054, 59r19.29a 2448 . . . . . . 7 ((((𝑎 𝑏 ℝ) (y (i · y) ℝ)) (𝑐 (𝑏 + 𝑐) = y)) → x ℂ ((𝑎 + (i · 𝑏)) + x) = 0)
614, 60rexlimddv 2431 . . . . . 6 (((𝑎 𝑏 ℝ) (y (i · y) ℝ)) → x ℂ ((𝑎 + (i · 𝑏)) + x) = 0)
6261rexlimdvaa 2428 . . . . 5 ((𝑎 𝑏 ℝ) → (y ℝ (i · y) ℝ → x ℂ ((𝑎 + (i · 𝑏)) + x) = 0))
632, 62mpi 15 . . . 4 ((𝑎 𝑏 ℝ) → x ℂ ((𝑎 + (i · 𝑏)) + x) = 0)
64 oveq1 5462 . . . . . 6 (A = (𝑎 + (i · 𝑏)) → (A + x) = ((𝑎 + (i · 𝑏)) + x))
6564eqeq1d 2045 . . . . 5 (A = (𝑎 + (i · 𝑏)) → ((A + x) = 0 ↔ ((𝑎 + (i · 𝑏)) + x) = 0))
6665rexbidv 2321 . . . 4 (A = (𝑎 + (i · 𝑏)) → (x ℂ (A + x) = 0 ↔ x ℂ ((𝑎 + (i · 𝑏)) + x) = 0))
6763, 66syl5ibrcom 146 . . 3 ((𝑎 𝑏 ℝ) → (A = (𝑎 + (i · 𝑏)) → x ℂ (A + x) = 0))
6867rexlimivv 2432 . 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 1242   wcel 1390  wrex 2301  (class class class)co 5455  cc 6689  cr 6690  0cc0 6691  ici 6693   + caddc 6694   · cmul 6696
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 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-resscn 6755  ax-1cn 6756  ax-icn 6758  ax-addcl 6759  ax-addrcl 6760  ax-mulcl 6761  ax-addcom 6763  ax-addass 6765  ax-distr 6767  ax-i2m1 6768  ax-0id 6771  ax-rnegex 6772  ax-cnre 6774
This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-v 2553  df-un 2916  df-in 2918  df-ss 2925  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-br 3756  df-iota 4810  df-fv 4853  df-ov 5458
This theorem is referenced by:  cnegex2  6967  addcan2  6969  0cnALT  6978  negeu  6979
  Copyright terms: Public domain W3C validator