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

Theorem cnegex 8134
Description: Existence of the negative of a complex number. (Contributed by Eric Schmidt, 21-May-2007.)
Assertion
Ref Expression
cnegex (๐ด โˆˆ โ„‚ โ†’ โˆƒ๐‘ฅ โˆˆ โ„‚ (๐ด + ๐‘ฅ) = 0)
Distinct variable group:   ๐‘ฅ,๐ด

Proof of Theorem cnegex
Dummy variables ๐‘Ž ๐‘ ๐‘ ๐‘‘ ๐‘ฆ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cnre 7952 . 2 (๐ด โˆˆ โ„‚ โ†’ โˆƒ๐‘Ž โˆˆ โ„ โˆƒ๐‘ โˆˆ โ„ ๐ด = (๐‘Ž + (i ยท ๐‘)))
2 cnegexlem2 8132 . . . . 5 โˆƒ๐‘ฆ โˆˆ โ„ (i ยท ๐‘ฆ) โˆˆ โ„
3 cnegexlem3 8133 . . . . . . . 8 ((๐‘ โˆˆ โ„ โˆง ๐‘ฆ โˆˆ โ„) โ†’ โˆƒ๐‘ โˆˆ โ„ (๐‘ + ๐‘) = ๐‘ฆ)
43ad2ant2lr 510 . . . . . . 7 (((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (๐‘ฆ โˆˆ โ„ โˆง (i ยท ๐‘ฆ) โˆˆ โ„)) โ†’ โˆƒ๐‘ โˆˆ โ„ (๐‘ + ๐‘) = ๐‘ฆ)
5 ax-icn 7905 . . . . . . . . . . . . . 14 i โˆˆ โ„‚
6 recn 7943 . . . . . . . . . . . . . 14 (๐‘ โˆˆ โ„ โ†’ ๐‘ โˆˆ โ„‚)
7 mulcl 7937 . . . . . . . . . . . . . 14 ((i โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„‚) โ†’ (i ยท ๐‘) โˆˆ โ„‚)
85, 6, 7sylancr 414 . . . . . . . . . . . . 13 (๐‘ โˆˆ โ„ โ†’ (i ยท ๐‘) โˆˆ โ„‚)
9 recn 7943 . . . . . . . . . . . . 13 (๐‘‘ โˆˆ โ„ โ†’ ๐‘‘ โˆˆ โ„‚)
10 addcl 7935 . . . . . . . . . . . . 13 (((i ยท ๐‘) โˆˆ โ„‚ โˆง ๐‘‘ โˆˆ โ„‚) โ†’ ((i ยท ๐‘) + ๐‘‘) โˆˆ โ„‚)
118, 9, 10syl2an 289 . . . . . . . . . . . 12 ((๐‘ โˆˆ โ„ โˆง ๐‘‘ โˆˆ โ„) โ†’ ((i ยท ๐‘) + ๐‘‘) โˆˆ โ„‚)
1211adantlr 477 . . . . . . . . . . 11 (((๐‘ โˆˆ โ„ โˆง (๐‘ + ๐‘) = ๐‘ฆ) โˆง ๐‘‘ โˆˆ โ„) โ†’ ((i ยท ๐‘) + ๐‘‘) โˆˆ โ„‚)
1312adantll 476 . . . . . . . . . 10 (((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (๐‘ฆ โˆˆ โ„ โˆง (i ยท ๐‘ฆ) โˆˆ โ„)) โˆง (๐‘ โˆˆ โ„ โˆง (๐‘ + ๐‘) = ๐‘ฆ)) โˆง ๐‘‘ โˆˆ โ„) โ†’ ((i ยท ๐‘) + ๐‘‘) โˆˆ โ„‚)
1413adantr 276 . . . . . . . . 9 ((((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (๐‘ฆ โˆˆ โ„ โˆง (i ยท ๐‘ฆ) โˆˆ โ„)) โˆง (๐‘ โˆˆ โ„ โˆง (๐‘ + ๐‘) = ๐‘ฆ)) โˆง ๐‘‘ โˆˆ โ„) โˆง ((๐‘Ž + (i ยท ๐‘ฆ)) + ๐‘‘) = 0) โ†’ ((i ยท ๐‘) + ๐‘‘) โˆˆ โ„‚)
15 recn 7943 . . . . . . . . . . . . . . . . 17 (๐‘Ž โˆˆ โ„ โ†’ ๐‘Ž โˆˆ โ„‚)
16 recn 7943 . . . . . . . . . . . . . . . . 17 (๐‘ โˆˆ โ„ โ†’ ๐‘ โˆˆ โ„‚)
1715, 16anim12i 338 . . . . . . . . . . . . . . . 16 ((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โ†’ (๐‘Ž โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„‚))
1817, 6anim12i 338 . . . . . . . . . . . . . . 15 (((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง ๐‘ โˆˆ โ„) โ†’ ((๐‘Ž โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„‚) โˆง ๐‘ โˆˆ โ„‚))
19 mulcl 7937 . . . . . . . . . . . . . . . . . . . 20 ((i โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„‚) โ†’ (i ยท ๐‘) โˆˆ โ„‚)
205, 19mpan 424 . . . . . . . . . . . . . . . . . . 19 (๐‘ โˆˆ โ„‚ โ†’ (i ยท ๐‘) โˆˆ โ„‚)
21 addcl 7935 . . . . . . . . . . . . . . . . . . 19 ((๐‘Ž โˆˆ โ„‚ โˆง (i ยท ๐‘) โˆˆ โ„‚) โ†’ (๐‘Ž + (i ยท ๐‘)) โˆˆ โ„‚)
2220, 21sylan2 286 . . . . . . . . . . . . . . . . . 18 ((๐‘Ž โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„‚) โ†’ (๐‘Ž + (i ยท ๐‘)) โˆˆ โ„‚)
2322ad2antrr 488 . . . . . . . . . . . . . . . . 17 ((((๐‘Ž โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„‚) โˆง ๐‘ โˆˆ โ„‚) โˆง ๐‘‘ โˆˆ โ„‚) โ†’ (๐‘Ž + (i ยท ๐‘)) โˆˆ โ„‚)
245, 7mpan 424 . . . . . . . . . . . . . . . . . 18 (๐‘ โˆˆ โ„‚ โ†’ (i ยท ๐‘) โˆˆ โ„‚)
2524ad2antlr 489 . . . . . . . . . . . . . . . . 17 ((((๐‘Ž โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„‚) โˆง ๐‘ โˆˆ โ„‚) โˆง ๐‘‘ โˆˆ โ„‚) โ†’ (i ยท ๐‘) โˆˆ โ„‚)
26 simpr 110 . . . . . . . . . . . . . . . . 17 ((((๐‘Ž โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„‚) โˆง ๐‘ โˆˆ โ„‚) โˆง ๐‘‘ โˆˆ โ„‚) โ†’ ๐‘‘ โˆˆ โ„‚)
2723, 25, 26addassd 7979 . . . . . . . . . . . . . . . 16 ((((๐‘Ž โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„‚) โˆง ๐‘ โˆˆ โ„‚) โˆง ๐‘‘ โˆˆ โ„‚) โ†’ (((๐‘Ž + (i ยท ๐‘)) + (i ยท ๐‘)) + ๐‘‘) = ((๐‘Ž + (i ยท ๐‘)) + ((i ยท ๐‘) + ๐‘‘)))
28 simpll 527 . . . . . . . . . . . . . . . . . . . 20 (((๐‘Ž โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„‚) โˆง ๐‘ โˆˆ โ„‚) โ†’ ๐‘Ž โˆˆ โ„‚)
2920ad2antlr 489 . . . . . . . . . . . . . . . . . . . 20 (((๐‘Ž โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„‚) โˆง ๐‘ โˆˆ โ„‚) โ†’ (i ยท ๐‘) โˆˆ โ„‚)
3024adantl 277 . . . . . . . . . . . . . . . . . . . 20 (((๐‘Ž โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„‚) โˆง ๐‘ โˆˆ โ„‚) โ†’ (i ยท ๐‘) โˆˆ โ„‚)
3128, 29, 30addassd 7979 . . . . . . . . . . . . . . . . . . 19 (((๐‘Ž โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„‚) โˆง ๐‘ โˆˆ โ„‚) โ†’ ((๐‘Ž + (i ยท ๐‘)) + (i ยท ๐‘)) = (๐‘Ž + ((i ยท ๐‘) + (i ยท ๐‘))))
32 adddi 7942 . . . . . . . . . . . . . . . . . . . . . 22 ((i โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„‚) โ†’ (i ยท (๐‘ + ๐‘)) = ((i ยท ๐‘) + (i ยท ๐‘)))
335, 32mp3an1 1324 . . . . . . . . . . . . . . . . . . . . 21 ((๐‘ โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„‚) โ†’ (i ยท (๐‘ + ๐‘)) = ((i ยท ๐‘) + (i ยท ๐‘)))
3433adantll 476 . . . . . . . . . . . . . . . . . . . 20 (((๐‘Ž โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„‚) โˆง ๐‘ โˆˆ โ„‚) โ†’ (i ยท (๐‘ + ๐‘)) = ((i ยท ๐‘) + (i ยท ๐‘)))
3534oveq2d 5890 . . . . . . . . . . . . . . . . . . 19 (((๐‘Ž โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„‚) โˆง ๐‘ โˆˆ โ„‚) โ†’ (๐‘Ž + (i ยท (๐‘ + ๐‘))) = (๐‘Ž + ((i ยท ๐‘) + (i ยท ๐‘))))
3631, 35eqtr4d 2213 . . . . . . . . . . . . . . . . . 18 (((๐‘Ž โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„‚) โˆง ๐‘ โˆˆ โ„‚) โ†’ ((๐‘Ž + (i ยท ๐‘)) + (i ยท ๐‘)) = (๐‘Ž + (i ยท (๐‘ + ๐‘))))
3736adantr 276 . . . . . . . . . . . . . . . . 17 ((((๐‘Ž โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„‚) โˆง ๐‘ โˆˆ โ„‚) โˆง ๐‘‘ โˆˆ โ„‚) โ†’ ((๐‘Ž + (i ยท ๐‘)) + (i ยท ๐‘)) = (๐‘Ž + (i ยท (๐‘ + ๐‘))))
3837oveq1d 5889 . . . . . . . . . . . . . . . 16 ((((๐‘Ž โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„‚) โˆง ๐‘ โˆˆ โ„‚) โˆง ๐‘‘ โˆˆ โ„‚) โ†’ (((๐‘Ž + (i ยท ๐‘)) + (i ยท ๐‘)) + ๐‘‘) = ((๐‘Ž + (i ยท (๐‘ + ๐‘))) + ๐‘‘))
3927, 38eqtr3d 2212 . . . . . . . . . . . . . . 15 ((((๐‘Ž โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„‚) โˆง ๐‘ โˆˆ โ„‚) โˆง ๐‘‘ โˆˆ โ„‚) โ†’ ((๐‘Ž + (i ยท ๐‘)) + ((i ยท ๐‘) + ๐‘‘)) = ((๐‘Ž + (i ยท (๐‘ + ๐‘))) + ๐‘‘))
4018, 9, 39syl2an 289 . . . . . . . . . . . . . 14 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง ๐‘ โˆˆ โ„) โˆง ๐‘‘ โˆˆ โ„) โ†’ ((๐‘Ž + (i ยท ๐‘)) + ((i ยท ๐‘) + ๐‘‘)) = ((๐‘Ž + (i ยท (๐‘ + ๐‘))) + ๐‘‘))
4140adantlrr 483 . . . . . . . . . . . . 13 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (๐‘ โˆˆ โ„ โˆง (๐‘ + ๐‘) = ๐‘ฆ)) โˆง ๐‘‘ โˆˆ โ„) โ†’ ((๐‘Ž + (i ยท ๐‘)) + ((i ยท ๐‘) + ๐‘‘)) = ((๐‘Ž + (i ยท (๐‘ + ๐‘))) + ๐‘‘))
42 oveq2 5882 . . . . . . . . . . . . . . . . 17 ((๐‘ + ๐‘) = ๐‘ฆ โ†’ (i ยท (๐‘ + ๐‘)) = (i ยท ๐‘ฆ))
4342oveq2d 5890 . . . . . . . . . . . . . . . 16 ((๐‘ + ๐‘) = ๐‘ฆ โ†’ (๐‘Ž + (i ยท (๐‘ + ๐‘))) = (๐‘Ž + (i ยท ๐‘ฆ)))
4443oveq1d 5889 . . . . . . . . . . . . . . 15 ((๐‘ + ๐‘) = ๐‘ฆ โ†’ ((๐‘Ž + (i ยท (๐‘ + ๐‘))) + ๐‘‘) = ((๐‘Ž + (i ยท ๐‘ฆ)) + ๐‘‘))
4544adantl 277 . . . . . . . . . . . . . 14 ((๐‘ โˆˆ โ„ โˆง (๐‘ + ๐‘) = ๐‘ฆ) โ†’ ((๐‘Ž + (i ยท (๐‘ + ๐‘))) + ๐‘‘) = ((๐‘Ž + (i ยท ๐‘ฆ)) + ๐‘‘))
4645ad2antlr 489 . . . . . . . . . . . . 13 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (๐‘ โˆˆ โ„ โˆง (๐‘ + ๐‘) = ๐‘ฆ)) โˆง ๐‘‘ โˆˆ โ„) โ†’ ((๐‘Ž + (i ยท (๐‘ + ๐‘))) + ๐‘‘) = ((๐‘Ž + (i ยท ๐‘ฆ)) + ๐‘‘))
4741, 46eqtr2d 2211 . . . . . . . . . . . 12 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (๐‘ โˆˆ โ„ โˆง (๐‘ + ๐‘) = ๐‘ฆ)) โˆง ๐‘‘ โˆˆ โ„) โ†’ ((๐‘Ž + (i ยท ๐‘ฆ)) + ๐‘‘) = ((๐‘Ž + (i ยท ๐‘)) + ((i ยท ๐‘) + ๐‘‘)))
4847adantllr 481 . . . . . . . . . . 11 (((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (๐‘ฆ โˆˆ โ„ โˆง (i ยท ๐‘ฆ) โˆˆ โ„)) โˆง (๐‘ โˆˆ โ„ โˆง (๐‘ + ๐‘) = ๐‘ฆ)) โˆง ๐‘‘ โˆˆ โ„) โ†’ ((๐‘Ž + (i ยท ๐‘ฆ)) + ๐‘‘) = ((๐‘Ž + (i ยท ๐‘)) + ((i ยท ๐‘) + ๐‘‘)))
4948eqeq1d 2186 . . . . . . . . . 10 (((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (๐‘ฆ โˆˆ โ„ โˆง (i ยท ๐‘ฆ) โˆˆ โ„)) โˆง (๐‘ โˆˆ โ„ โˆง (๐‘ + ๐‘) = ๐‘ฆ)) โˆง ๐‘‘ โˆˆ โ„) โ†’ (((๐‘Ž + (i ยท ๐‘ฆ)) + ๐‘‘) = 0 โ†” ((๐‘Ž + (i ยท ๐‘)) + ((i ยท ๐‘) + ๐‘‘)) = 0))
5049biimpa 296 . . . . . . . . 9 ((((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (๐‘ฆ โˆˆ โ„ โˆง (i ยท ๐‘ฆ) โˆˆ โ„)) โˆง (๐‘ โˆˆ โ„ โˆง (๐‘ + ๐‘) = ๐‘ฆ)) โˆง ๐‘‘ โˆˆ โ„) โˆง ((๐‘Ž + (i ยท ๐‘ฆ)) + ๐‘‘) = 0) โ†’ ((๐‘Ž + (i ยท ๐‘)) + ((i ยท ๐‘) + ๐‘‘)) = 0)
51 oveq2 5882 . . . . . . . . . . 11 (๐‘ฅ = ((i ยท ๐‘) + ๐‘‘) โ†’ ((๐‘Ž + (i ยท ๐‘)) + ๐‘ฅ) = ((๐‘Ž + (i ยท ๐‘)) + ((i ยท ๐‘) + ๐‘‘)))
5251eqeq1d 2186 . . . . . . . . . 10 (๐‘ฅ = ((i ยท ๐‘) + ๐‘‘) โ†’ (((๐‘Ž + (i ยท ๐‘)) + ๐‘ฅ) = 0 โ†” ((๐‘Ž + (i ยท ๐‘)) + ((i ยท ๐‘) + ๐‘‘)) = 0))
5352rspcev 2841 . . . . . . . . 9 ((((i ยท ๐‘) + ๐‘‘) โˆˆ โ„‚ โˆง ((๐‘Ž + (i ยท ๐‘)) + ((i ยท ๐‘) + ๐‘‘)) = 0) โ†’ โˆƒ๐‘ฅ โˆˆ โ„‚ ((๐‘Ž + (i ยท ๐‘)) + ๐‘ฅ) = 0)
5414, 50, 53syl2anc 411 . . . . . . . 8 ((((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (๐‘ฆ โˆˆ โ„ โˆง (i ยท ๐‘ฆ) โˆˆ โ„)) โˆง (๐‘ โˆˆ โ„ โˆง (๐‘ + ๐‘) = ๐‘ฆ)) โˆง ๐‘‘ โˆˆ โ„) โˆง ((๐‘Ž + (i ยท ๐‘ฆ)) + ๐‘‘) = 0) โ†’ โˆƒ๐‘ฅ โˆˆ โ„‚ ((๐‘Ž + (i ยท ๐‘)) + ๐‘ฅ) = 0)
55 readdcl 7936 . . . . . . . . . . 11 ((๐‘Ž โˆˆ โ„ โˆง (i ยท ๐‘ฆ) โˆˆ โ„) โ†’ (๐‘Ž + (i ยท ๐‘ฆ)) โˆˆ โ„)
56 ax-rnegex 7919 . . . . . . . . . . 11 ((๐‘Ž + (i ยท ๐‘ฆ)) โˆˆ โ„ โ†’ โˆƒ๐‘‘ โˆˆ โ„ ((๐‘Ž + (i ยท ๐‘ฆ)) + ๐‘‘) = 0)
5755, 56syl 14 . . . . . . . . . 10 ((๐‘Ž โˆˆ โ„ โˆง (i ยท ๐‘ฆ) โˆˆ โ„) โ†’ โˆƒ๐‘‘ โˆˆ โ„ ((๐‘Ž + (i ยท ๐‘ฆ)) + ๐‘‘) = 0)
5857ad2ant2rl 511 . . . . . . . . 9 (((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (๐‘ฆ โˆˆ โ„ โˆง (i ยท ๐‘ฆ) โˆˆ โ„)) โ†’ โˆƒ๐‘‘ โˆˆ โ„ ((๐‘Ž + (i ยท ๐‘ฆ)) + ๐‘‘) = 0)
5958adantr 276 . . . . . . . 8 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (๐‘ฆ โˆˆ โ„ โˆง (i ยท ๐‘ฆ) โˆˆ โ„)) โˆง (๐‘ โˆˆ โ„ โˆง (๐‘ + ๐‘) = ๐‘ฆ)) โ†’ โˆƒ๐‘‘ โˆˆ โ„ ((๐‘Ž + (i ยท ๐‘ฆ)) + ๐‘‘) = 0)
6054, 59r19.29a 2620 . . . . . . 7 ((((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (๐‘ฆ โˆˆ โ„ โˆง (i ยท ๐‘ฆ) โˆˆ โ„)) โˆง (๐‘ โˆˆ โ„ โˆง (๐‘ + ๐‘) = ๐‘ฆ)) โ†’ โˆƒ๐‘ฅ โˆˆ โ„‚ ((๐‘Ž + (i ยท ๐‘)) + ๐‘ฅ) = 0)
614, 60rexlimddv 2599 . . . . . 6 (((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง (๐‘ฆ โˆˆ โ„ โˆง (i ยท ๐‘ฆ) โˆˆ โ„)) โ†’ โˆƒ๐‘ฅ โˆˆ โ„‚ ((๐‘Ž + (i ยท ๐‘)) + ๐‘ฅ) = 0)
6261rexlimdvaa 2595 . . . . 5 ((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โ†’ (โˆƒ๐‘ฆ โˆˆ โ„ (i ยท ๐‘ฆ) โˆˆ โ„ โ†’ โˆƒ๐‘ฅ โˆˆ โ„‚ ((๐‘Ž + (i ยท ๐‘)) + ๐‘ฅ) = 0))
632, 62mpi 15 . . . 4 ((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โ†’ โˆƒ๐‘ฅ โˆˆ โ„‚ ((๐‘Ž + (i ยท ๐‘)) + ๐‘ฅ) = 0)
64 oveq1 5881 . . . . . 6 (๐ด = (๐‘Ž + (i ยท ๐‘)) โ†’ (๐ด + ๐‘ฅ) = ((๐‘Ž + (i ยท ๐‘)) + ๐‘ฅ))
6564eqeq1d 2186 . . . . 5 (๐ด = (๐‘Ž + (i ยท ๐‘)) โ†’ ((๐ด + ๐‘ฅ) = 0 โ†” ((๐‘Ž + (i ยท ๐‘)) + ๐‘ฅ) = 0))
6665rexbidv 2478 . . . 4 (๐ด = (๐‘Ž + (i ยท ๐‘)) โ†’ (โˆƒ๐‘ฅ โˆˆ โ„‚ (๐ด + ๐‘ฅ) = 0 โ†” โˆƒ๐‘ฅ โˆˆ โ„‚ ((๐‘Ž + (i ยท ๐‘)) + ๐‘ฅ) = 0))
6763, 66syl5ibrcom 157 . . 3 ((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โ†’ (๐ด = (๐‘Ž + (i ยท ๐‘)) โ†’ โˆƒ๐‘ฅ โˆˆ โ„‚ (๐ด + ๐‘ฅ) = 0))
6867rexlimivv 2600 . 2 (โˆƒ๐‘Ž โˆˆ โ„ โˆƒ๐‘ โˆˆ โ„ ๐ด = (๐‘Ž + (i ยท ๐‘)) โ†’ โˆƒ๐‘ฅ โˆˆ โ„‚ (๐ด + ๐‘ฅ) = 0)
691, 68syl 14 1 (๐ด โˆˆ โ„‚ โ†’ โˆƒ๐‘ฅ โˆˆ โ„‚ (๐ด + ๐‘ฅ) = 0)
Colors of variables: wff set class
Syntax hints:   โ†’ wi 4   โˆง wa 104   = wceq 1353   โˆˆ wcel 2148  โˆƒwrex 2456  (class class class)co 5874  โ„‚cc 7808  โ„cr 7809  0cc0 7810  ici 7812   + caddc 7813   ยท cmul 7815
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-resscn 7902  ax-1cn 7903  ax-icn 7905  ax-addcl 7906  ax-addrcl 7907  ax-mulcl 7908  ax-addcom 7910  ax-addass 7912  ax-distr 7914  ax-i2m1 7915  ax-0id 7918  ax-rnegex 7919  ax-cnre 7921
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2739  df-un 3133  df-in 3135  df-ss 3142  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-br 4004  df-iota 5178  df-fv 5224  df-ov 5877
This theorem is referenced by:  cnegex2  8135  addcan2  8137  0cnALT  8146  negeu  8147
  Copyright terms: Public domain W3C validator