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

Theorem cju 8918
Description: The complex conjugate of a complex number is unique. (Contributed by Mario Carneiro, 6-Nov-2013.)
Assertion
Ref Expression
cju (๐ด โˆˆ โ„‚ โ†’ โˆƒ!๐‘ฅ โˆˆ โ„‚ ((๐ด + ๐‘ฅ) โˆˆ โ„ โˆง (i ยท (๐ด โˆ’ ๐‘ฅ)) โˆˆ โ„))
Distinct variable group:   ๐‘ฅ,๐ด

Proof of Theorem cju
Dummy variables ๐‘ฆ ๐‘ง are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cnre 7953 . . 3 (๐ด โˆˆ โ„‚ โ†’ โˆƒ๐‘ฆ โˆˆ โ„ โˆƒ๐‘ง โˆˆ โ„ ๐ด = (๐‘ฆ + (i ยท ๐‘ง)))
2 recn 7944 . . . . . . 7 (๐‘ฆ โˆˆ โ„ โ†’ ๐‘ฆ โˆˆ โ„‚)
3 ax-icn 7906 . . . . . . . 8 i โˆˆ โ„‚
4 recn 7944 . . . . . . . 8 (๐‘ง โˆˆ โ„ โ†’ ๐‘ง โˆˆ โ„‚)
5 mulcl 7938 . . . . . . . 8 ((i โˆˆ โ„‚ โˆง ๐‘ง โˆˆ โ„‚) โ†’ (i ยท ๐‘ง) โˆˆ โ„‚)
63, 4, 5sylancr 414 . . . . . . 7 (๐‘ง โˆˆ โ„ โ†’ (i ยท ๐‘ง) โˆˆ โ„‚)
7 subcl 8156 . . . . . . 7 ((๐‘ฆ โˆˆ โ„‚ โˆง (i ยท ๐‘ง) โˆˆ โ„‚) โ†’ (๐‘ฆ โˆ’ (i ยท ๐‘ง)) โˆˆ โ„‚)
82, 6, 7syl2an 289 . . . . . 6 ((๐‘ฆ โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„) โ†’ (๐‘ฆ โˆ’ (i ยท ๐‘ง)) โˆˆ โ„‚)
92adantr 276 . . . . . . . 8 ((๐‘ฆ โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„) โ†’ ๐‘ฆ โˆˆ โ„‚)
106adantl 277 . . . . . . . 8 ((๐‘ฆ โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„) โ†’ (i ยท ๐‘ง) โˆˆ โ„‚)
119, 10, 9ppncand 8308 . . . . . . 7 ((๐‘ฆ โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„) โ†’ ((๐‘ฆ + (i ยท ๐‘ง)) + (๐‘ฆ โˆ’ (i ยท ๐‘ง))) = (๐‘ฆ + ๐‘ฆ))
12 readdcl 7937 . . . . . . . . 9 ((๐‘ฆ โˆˆ โ„ โˆง ๐‘ฆ โˆˆ โ„) โ†’ (๐‘ฆ + ๐‘ฆ) โˆˆ โ„)
1312anidms 397 . . . . . . . 8 (๐‘ฆ โˆˆ โ„ โ†’ (๐‘ฆ + ๐‘ฆ) โˆˆ โ„)
1413adantr 276 . . . . . . 7 ((๐‘ฆ โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„) โ†’ (๐‘ฆ + ๐‘ฆ) โˆˆ โ„)
1511, 14eqeltrd 2254 . . . . . 6 ((๐‘ฆ โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„) โ†’ ((๐‘ฆ + (i ยท ๐‘ง)) + (๐‘ฆ โˆ’ (i ยท ๐‘ง))) โˆˆ โ„)
169, 10, 10pnncand 8307 . . . . . . . . . 10 ((๐‘ฆ โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„) โ†’ ((๐‘ฆ + (i ยท ๐‘ง)) โˆ’ (๐‘ฆ โˆ’ (i ยท ๐‘ง))) = ((i ยท ๐‘ง) + (i ยท ๐‘ง)))
173a1i 9 . . . . . . . . . . 11 ((๐‘ฆ โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„) โ†’ i โˆˆ โ„‚)
184adantl 277 . . . . . . . . . . 11 ((๐‘ฆ โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„) โ†’ ๐‘ง โˆˆ โ„‚)
1917, 18, 18adddid 7982 . . . . . . . . . 10 ((๐‘ฆ โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„) โ†’ (i ยท (๐‘ง + ๐‘ง)) = ((i ยท ๐‘ง) + (i ยท ๐‘ง)))
2016, 19eqtr4d 2213 . . . . . . . . 9 ((๐‘ฆ โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„) โ†’ ((๐‘ฆ + (i ยท ๐‘ง)) โˆ’ (๐‘ฆ โˆ’ (i ยท ๐‘ง))) = (i ยท (๐‘ง + ๐‘ง)))
2120oveq2d 5891 . . . . . . . 8 ((๐‘ฆ โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„) โ†’ (i ยท ((๐‘ฆ + (i ยท ๐‘ง)) โˆ’ (๐‘ฆ โˆ’ (i ยท ๐‘ง)))) = (i ยท (i ยท (๐‘ง + ๐‘ง))))
2218, 18addcld 7977 . . . . . . . . 9 ((๐‘ฆ โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„) โ†’ (๐‘ง + ๐‘ง) โˆˆ โ„‚)
23 mulass 7942 . . . . . . . . . 10 ((i โˆˆ โ„‚ โˆง i โˆˆ โ„‚ โˆง (๐‘ง + ๐‘ง) โˆˆ โ„‚) โ†’ ((i ยท i) ยท (๐‘ง + ๐‘ง)) = (i ยท (i ยท (๐‘ง + ๐‘ง))))
243, 3, 23mp3an12 1327 . . . . . . . . 9 ((๐‘ง + ๐‘ง) โˆˆ โ„‚ โ†’ ((i ยท i) ยท (๐‘ง + ๐‘ง)) = (i ยท (i ยท (๐‘ง + ๐‘ง))))
2522, 24syl 14 . . . . . . . 8 ((๐‘ฆ โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„) โ†’ ((i ยท i) ยท (๐‘ง + ๐‘ง)) = (i ยท (i ยท (๐‘ง + ๐‘ง))))
2621, 25eqtr4d 2213 . . . . . . 7 ((๐‘ฆ โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„) โ†’ (i ยท ((๐‘ฆ + (i ยท ๐‘ง)) โˆ’ (๐‘ฆ โˆ’ (i ยท ๐‘ง)))) = ((i ยท i) ยท (๐‘ง + ๐‘ง)))
27 ixi 8540 . . . . . . . . 9 (i ยท i) = -1
28 1re 7956 . . . . . . . . . 10 1 โˆˆ โ„
2928renegcli 8219 . . . . . . . . 9 -1 โˆˆ โ„
3027, 29eqeltri 2250 . . . . . . . 8 (i ยท i) โˆˆ โ„
31 simpr 110 . . . . . . . . 9 ((๐‘ฆ โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„) โ†’ ๐‘ง โˆˆ โ„)
3231, 31readdcld 7987 . . . . . . . 8 ((๐‘ฆ โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„) โ†’ (๐‘ง + ๐‘ง) โˆˆ โ„)
33 remulcl 7939 . . . . . . . 8 (((i ยท i) โˆˆ โ„ โˆง (๐‘ง + ๐‘ง) โˆˆ โ„) โ†’ ((i ยท i) ยท (๐‘ง + ๐‘ง)) โˆˆ โ„)
3430, 32, 33sylancr 414 . . . . . . 7 ((๐‘ฆ โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„) โ†’ ((i ยท i) ยท (๐‘ง + ๐‘ง)) โˆˆ โ„)
3526, 34eqeltrd 2254 . . . . . 6 ((๐‘ฆ โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„) โ†’ (i ยท ((๐‘ฆ + (i ยท ๐‘ง)) โˆ’ (๐‘ฆ โˆ’ (i ยท ๐‘ง)))) โˆˆ โ„)
36 oveq2 5883 . . . . . . . . 9 (๐‘ฅ = (๐‘ฆ โˆ’ (i ยท ๐‘ง)) โ†’ ((๐‘ฆ + (i ยท ๐‘ง)) + ๐‘ฅ) = ((๐‘ฆ + (i ยท ๐‘ง)) + (๐‘ฆ โˆ’ (i ยท ๐‘ง))))
3736eleq1d 2246 . . . . . . . 8 (๐‘ฅ = (๐‘ฆ โˆ’ (i ยท ๐‘ง)) โ†’ (((๐‘ฆ + (i ยท ๐‘ง)) + ๐‘ฅ) โˆˆ โ„ โ†” ((๐‘ฆ + (i ยท ๐‘ง)) + (๐‘ฆ โˆ’ (i ยท ๐‘ง))) โˆˆ โ„))
38 oveq2 5883 . . . . . . . . . 10 (๐‘ฅ = (๐‘ฆ โˆ’ (i ยท ๐‘ง)) โ†’ ((๐‘ฆ + (i ยท ๐‘ง)) โˆ’ ๐‘ฅ) = ((๐‘ฆ + (i ยท ๐‘ง)) โˆ’ (๐‘ฆ โˆ’ (i ยท ๐‘ง))))
3938oveq2d 5891 . . . . . . . . 9 (๐‘ฅ = (๐‘ฆ โˆ’ (i ยท ๐‘ง)) โ†’ (i ยท ((๐‘ฆ + (i ยท ๐‘ง)) โˆ’ ๐‘ฅ)) = (i ยท ((๐‘ฆ + (i ยท ๐‘ง)) โˆ’ (๐‘ฆ โˆ’ (i ยท ๐‘ง)))))
4039eleq1d 2246 . . . . . . . 8 (๐‘ฅ = (๐‘ฆ โˆ’ (i ยท ๐‘ง)) โ†’ ((i ยท ((๐‘ฆ + (i ยท ๐‘ง)) โˆ’ ๐‘ฅ)) โˆˆ โ„ โ†” (i ยท ((๐‘ฆ + (i ยท ๐‘ง)) โˆ’ (๐‘ฆ โˆ’ (i ยท ๐‘ง)))) โˆˆ โ„))
4137, 40anbi12d 473 . . . . . . 7 (๐‘ฅ = (๐‘ฆ โˆ’ (i ยท ๐‘ง)) โ†’ ((((๐‘ฆ + (i ยท ๐‘ง)) + ๐‘ฅ) โˆˆ โ„ โˆง (i ยท ((๐‘ฆ + (i ยท ๐‘ง)) โˆ’ ๐‘ฅ)) โˆˆ โ„) โ†” (((๐‘ฆ + (i ยท ๐‘ง)) + (๐‘ฆ โˆ’ (i ยท ๐‘ง))) โˆˆ โ„ โˆง (i ยท ((๐‘ฆ + (i ยท ๐‘ง)) โˆ’ (๐‘ฆ โˆ’ (i ยท ๐‘ง)))) โˆˆ โ„)))
4241rspcev 2842 . . . . . 6 (((๐‘ฆ โˆ’ (i ยท ๐‘ง)) โˆˆ โ„‚ โˆง (((๐‘ฆ + (i ยท ๐‘ง)) + (๐‘ฆ โˆ’ (i ยท ๐‘ง))) โˆˆ โ„ โˆง (i ยท ((๐‘ฆ + (i ยท ๐‘ง)) โˆ’ (๐‘ฆ โˆ’ (i ยท ๐‘ง)))) โˆˆ โ„)) โ†’ โˆƒ๐‘ฅ โˆˆ โ„‚ (((๐‘ฆ + (i ยท ๐‘ง)) + ๐‘ฅ) โˆˆ โ„ โˆง (i ยท ((๐‘ฆ + (i ยท ๐‘ง)) โˆ’ ๐‘ฅ)) โˆˆ โ„))
438, 15, 35, 42syl12anc 1236 . . . . 5 ((๐‘ฆ โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„) โ†’ โˆƒ๐‘ฅ โˆˆ โ„‚ (((๐‘ฆ + (i ยท ๐‘ง)) + ๐‘ฅ) โˆˆ โ„ โˆง (i ยท ((๐‘ฆ + (i ยท ๐‘ง)) โˆ’ ๐‘ฅ)) โˆˆ โ„))
44 oveq1 5882 . . . . . . . 8 (๐ด = (๐‘ฆ + (i ยท ๐‘ง)) โ†’ (๐ด + ๐‘ฅ) = ((๐‘ฆ + (i ยท ๐‘ง)) + ๐‘ฅ))
4544eleq1d 2246 . . . . . . 7 (๐ด = (๐‘ฆ + (i ยท ๐‘ง)) โ†’ ((๐ด + ๐‘ฅ) โˆˆ โ„ โ†” ((๐‘ฆ + (i ยท ๐‘ง)) + ๐‘ฅ) โˆˆ โ„))
46 oveq1 5882 . . . . . . . . 9 (๐ด = (๐‘ฆ + (i ยท ๐‘ง)) โ†’ (๐ด โˆ’ ๐‘ฅ) = ((๐‘ฆ + (i ยท ๐‘ง)) โˆ’ ๐‘ฅ))
4746oveq2d 5891 . . . . . . . 8 (๐ด = (๐‘ฆ + (i ยท ๐‘ง)) โ†’ (i ยท (๐ด โˆ’ ๐‘ฅ)) = (i ยท ((๐‘ฆ + (i ยท ๐‘ง)) โˆ’ ๐‘ฅ)))
4847eleq1d 2246 . . . . . . 7 (๐ด = (๐‘ฆ + (i ยท ๐‘ง)) โ†’ ((i ยท (๐ด โˆ’ ๐‘ฅ)) โˆˆ โ„ โ†” (i ยท ((๐‘ฆ + (i ยท ๐‘ง)) โˆ’ ๐‘ฅ)) โˆˆ โ„))
4945, 48anbi12d 473 . . . . . 6 (๐ด = (๐‘ฆ + (i ยท ๐‘ง)) โ†’ (((๐ด + ๐‘ฅ) โˆˆ โ„ โˆง (i ยท (๐ด โˆ’ ๐‘ฅ)) โˆˆ โ„) โ†” (((๐‘ฆ + (i ยท ๐‘ง)) + ๐‘ฅ) โˆˆ โ„ โˆง (i ยท ((๐‘ฆ + (i ยท ๐‘ง)) โˆ’ ๐‘ฅ)) โˆˆ โ„)))
5049rexbidv 2478 . . . . 5 (๐ด = (๐‘ฆ + (i ยท ๐‘ง)) โ†’ (โˆƒ๐‘ฅ โˆˆ โ„‚ ((๐ด + ๐‘ฅ) โˆˆ โ„ โˆง (i ยท (๐ด โˆ’ ๐‘ฅ)) โˆˆ โ„) โ†” โˆƒ๐‘ฅ โˆˆ โ„‚ (((๐‘ฆ + (i ยท ๐‘ง)) + ๐‘ฅ) โˆˆ โ„ โˆง (i ยท ((๐‘ฆ + (i ยท ๐‘ง)) โˆ’ ๐‘ฅ)) โˆˆ โ„)))
5143, 50syl5ibrcom 157 . . . 4 ((๐‘ฆ โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„) โ†’ (๐ด = (๐‘ฆ + (i ยท ๐‘ง)) โ†’ โˆƒ๐‘ฅ โˆˆ โ„‚ ((๐ด + ๐‘ฅ) โˆˆ โ„ โˆง (i ยท (๐ด โˆ’ ๐‘ฅ)) โˆˆ โ„)))
5251rexlimivv 2600 . . 3 (โˆƒ๐‘ฆ โˆˆ โ„ โˆƒ๐‘ง โˆˆ โ„ ๐ด = (๐‘ฆ + (i ยท ๐‘ง)) โ†’ โˆƒ๐‘ฅ โˆˆ โ„‚ ((๐ด + ๐‘ฅ) โˆˆ โ„ โˆง (i ยท (๐ด โˆ’ ๐‘ฅ)) โˆˆ โ„))
531, 52syl 14 . 2 (๐ด โˆˆ โ„‚ โ†’ โˆƒ๐‘ฅ โˆˆ โ„‚ ((๐ด + ๐‘ฅ) โˆˆ โ„ โˆง (i ยท (๐ด โˆ’ ๐‘ฅ)) โˆˆ โ„))
54 an4 586 . . . 4 ((((๐ด + ๐‘ฅ) โˆˆ โ„ โˆง (i ยท (๐ด โˆ’ ๐‘ฅ)) โˆˆ โ„) โˆง ((๐ด + ๐‘ฆ) โˆˆ โ„ โˆง (i ยท (๐ด โˆ’ ๐‘ฆ)) โˆˆ โ„)) โ†” (((๐ด + ๐‘ฅ) โˆˆ โ„ โˆง (๐ด + ๐‘ฆ) โˆˆ โ„) โˆง ((i ยท (๐ด โˆ’ ๐‘ฅ)) โˆˆ โ„ โˆง (i ยท (๐ด โˆ’ ๐‘ฆ)) โˆˆ โ„)))
55 resubcl 8221 . . . . . . 7 (((๐ด + ๐‘ฅ) โˆˆ โ„ โˆง (๐ด + ๐‘ฆ) โˆˆ โ„) โ†’ ((๐ด + ๐‘ฅ) โˆ’ (๐ด + ๐‘ฆ)) โˆˆ โ„)
56 pnpcan 8196 . . . . . . . . 9 ((๐ด โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‚) โ†’ ((๐ด + ๐‘ฅ) โˆ’ (๐ด + ๐‘ฆ)) = (๐‘ฅ โˆ’ ๐‘ฆ))
57563expb 1204 . . . . . . . 8 ((๐ด โˆˆ โ„‚ โˆง (๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‚)) โ†’ ((๐ด + ๐‘ฅ) โˆ’ (๐ด + ๐‘ฆ)) = (๐‘ฅ โˆ’ ๐‘ฆ))
5857eleq1d 2246 . . . . . . 7 ((๐ด โˆˆ โ„‚ โˆง (๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‚)) โ†’ (((๐ด + ๐‘ฅ) โˆ’ (๐ด + ๐‘ฆ)) โˆˆ โ„ โ†” (๐‘ฅ โˆ’ ๐‘ฆ) โˆˆ โ„))
5955, 58imbitrid 154 . . . . . 6 ((๐ด โˆˆ โ„‚ โˆง (๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‚)) โ†’ (((๐ด + ๐‘ฅ) โˆˆ โ„ โˆง (๐ด + ๐‘ฆ) โˆˆ โ„) โ†’ (๐‘ฅ โˆ’ ๐‘ฆ) โˆˆ โ„))
60 resubcl 8221 . . . . . . . 8 (((i ยท (๐ด โˆ’ ๐‘ฆ)) โˆˆ โ„ โˆง (i ยท (๐ด โˆ’ ๐‘ฅ)) โˆˆ โ„) โ†’ ((i ยท (๐ด โˆ’ ๐‘ฆ)) โˆ’ (i ยท (๐ด โˆ’ ๐‘ฅ))) โˆˆ โ„)
6160ancoms 268 . . . . . . 7 (((i ยท (๐ด โˆ’ ๐‘ฅ)) โˆˆ โ„ โˆง (i ยท (๐ด โˆ’ ๐‘ฆ)) โˆˆ โ„) โ†’ ((i ยท (๐ด โˆ’ ๐‘ฆ)) โˆ’ (i ยท (๐ด โˆ’ ๐‘ฅ))) โˆˆ โ„)
623a1i 9 . . . . . . . . . 10 ((๐ด โˆˆ โ„‚ โˆง (๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‚)) โ†’ i โˆˆ โ„‚)
63 subcl 8156 . . . . . . . . . . 11 ((๐ด โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‚) โ†’ (๐ด โˆ’ ๐‘ฆ) โˆˆ โ„‚)
6463adantrl 478 . . . . . . . . . 10 ((๐ด โˆˆ โ„‚ โˆง (๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‚)) โ†’ (๐ด โˆ’ ๐‘ฆ) โˆˆ โ„‚)
65 subcl 8156 . . . . . . . . . . 11 ((๐ด โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ โ„‚) โ†’ (๐ด โˆ’ ๐‘ฅ) โˆˆ โ„‚)
6665adantrr 479 . . . . . . . . . 10 ((๐ด โˆˆ โ„‚ โˆง (๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‚)) โ†’ (๐ด โˆ’ ๐‘ฅ) โˆˆ โ„‚)
6762, 64, 66subdid 8371 . . . . . . . . 9 ((๐ด โˆˆ โ„‚ โˆง (๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‚)) โ†’ (i ยท ((๐ด โˆ’ ๐‘ฆ) โˆ’ (๐ด โˆ’ ๐‘ฅ))) = ((i ยท (๐ด โˆ’ ๐‘ฆ)) โˆ’ (i ยท (๐ด โˆ’ ๐‘ฅ))))
68 nnncan1 8193 . . . . . . . . . . . 12 ((๐ด โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ โ„‚) โ†’ ((๐ด โˆ’ ๐‘ฆ) โˆ’ (๐ด โˆ’ ๐‘ฅ)) = (๐‘ฅ โˆ’ ๐‘ฆ))
69683com23 1209 . . . . . . . . . . 11 ((๐ด โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‚) โ†’ ((๐ด โˆ’ ๐‘ฆ) โˆ’ (๐ด โˆ’ ๐‘ฅ)) = (๐‘ฅ โˆ’ ๐‘ฆ))
70693expb 1204 . . . . . . . . . 10 ((๐ด โˆˆ โ„‚ โˆง (๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‚)) โ†’ ((๐ด โˆ’ ๐‘ฆ) โˆ’ (๐ด โˆ’ ๐‘ฅ)) = (๐‘ฅ โˆ’ ๐‘ฆ))
7170oveq2d 5891 . . . . . . . . 9 ((๐ด โˆˆ โ„‚ โˆง (๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‚)) โ†’ (i ยท ((๐ด โˆ’ ๐‘ฆ) โˆ’ (๐ด โˆ’ ๐‘ฅ))) = (i ยท (๐‘ฅ โˆ’ ๐‘ฆ)))
7267, 71eqtr3d 2212 . . . . . . . 8 ((๐ด โˆˆ โ„‚ โˆง (๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‚)) โ†’ ((i ยท (๐ด โˆ’ ๐‘ฆ)) โˆ’ (i ยท (๐ด โˆ’ ๐‘ฅ))) = (i ยท (๐‘ฅ โˆ’ ๐‘ฆ)))
7372eleq1d 2246 . . . . . . 7 ((๐ด โˆˆ โ„‚ โˆง (๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‚)) โ†’ (((i ยท (๐ด โˆ’ ๐‘ฆ)) โˆ’ (i ยท (๐ด โˆ’ ๐‘ฅ))) โˆˆ โ„ โ†” (i ยท (๐‘ฅ โˆ’ ๐‘ฆ)) โˆˆ โ„))
7461, 73imbitrid 154 . . . . . 6 ((๐ด โˆˆ โ„‚ โˆง (๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‚)) โ†’ (((i ยท (๐ด โˆ’ ๐‘ฅ)) โˆˆ โ„ โˆง (i ยท (๐ด โˆ’ ๐‘ฆ)) โˆˆ โ„) โ†’ (i ยท (๐‘ฅ โˆ’ ๐‘ฆ)) โˆˆ โ„))
7559, 74anim12d 335 . . . . 5 ((๐ด โˆˆ โ„‚ โˆง (๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‚)) โ†’ ((((๐ด + ๐‘ฅ) โˆˆ โ„ โˆง (๐ด + ๐‘ฆ) โˆˆ โ„) โˆง ((i ยท (๐ด โˆ’ ๐‘ฅ)) โˆˆ โ„ โˆง (i ยท (๐ด โˆ’ ๐‘ฆ)) โˆˆ โ„)) โ†’ ((๐‘ฅ โˆ’ ๐‘ฆ) โˆˆ โ„ โˆง (i ยท (๐‘ฅ โˆ’ ๐‘ฆ)) โˆˆ โ„)))
76 rimul 8542 . . . . . 6 (((๐‘ฅ โˆ’ ๐‘ฆ) โˆˆ โ„ โˆง (i ยท (๐‘ฅ โˆ’ ๐‘ฆ)) โˆˆ โ„) โ†’ (๐‘ฅ โˆ’ ๐‘ฆ) = 0)
7776a1i 9 . . . . 5 ((๐ด โˆˆ โ„‚ โˆง (๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‚)) โ†’ (((๐‘ฅ โˆ’ ๐‘ฆ) โˆˆ โ„ โˆง (i ยท (๐‘ฅ โˆ’ ๐‘ฆ)) โˆˆ โ„) โ†’ (๐‘ฅ โˆ’ ๐‘ฆ) = 0))
78 subeq0 8183 . . . . . . 7 ((๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‚) โ†’ ((๐‘ฅ โˆ’ ๐‘ฆ) = 0 โ†” ๐‘ฅ = ๐‘ฆ))
7978biimpd 144 . . . . . 6 ((๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‚) โ†’ ((๐‘ฅ โˆ’ ๐‘ฆ) = 0 โ†’ ๐‘ฅ = ๐‘ฆ))
8079adantl 277 . . . . 5 ((๐ด โˆˆ โ„‚ โˆง (๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‚)) โ†’ ((๐‘ฅ โˆ’ ๐‘ฆ) = 0 โ†’ ๐‘ฅ = ๐‘ฆ))
8175, 77, 803syld 57 . . . 4 ((๐ด โˆˆ โ„‚ โˆง (๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‚)) โ†’ ((((๐ด + ๐‘ฅ) โˆˆ โ„ โˆง (๐ด + ๐‘ฆ) โˆˆ โ„) โˆง ((i ยท (๐ด โˆ’ ๐‘ฅ)) โˆˆ โ„ โˆง (i ยท (๐ด โˆ’ ๐‘ฆ)) โˆˆ โ„)) โ†’ ๐‘ฅ = ๐‘ฆ))
8254, 81biimtrid 152 . . 3 ((๐ด โˆˆ โ„‚ โˆง (๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‚)) โ†’ ((((๐ด + ๐‘ฅ) โˆˆ โ„ โˆง (i ยท (๐ด โˆ’ ๐‘ฅ)) โˆˆ โ„) โˆง ((๐ด + ๐‘ฆ) โˆˆ โ„ โˆง (i ยท (๐ด โˆ’ ๐‘ฆ)) โˆˆ โ„)) โ†’ ๐‘ฅ = ๐‘ฆ))
8382ralrimivva 2559 . 2 (๐ด โˆˆ โ„‚ โ†’ โˆ€๐‘ฅ โˆˆ โ„‚ โˆ€๐‘ฆ โˆˆ โ„‚ ((((๐ด + ๐‘ฅ) โˆˆ โ„ โˆง (i ยท (๐ด โˆ’ ๐‘ฅ)) โˆˆ โ„) โˆง ((๐ด + ๐‘ฆ) โˆˆ โ„ โˆง (i ยท (๐ด โˆ’ ๐‘ฆ)) โˆˆ โ„)) โ†’ ๐‘ฅ = ๐‘ฆ))
84 oveq2 5883 . . . . 5 (๐‘ฅ = ๐‘ฆ โ†’ (๐ด + ๐‘ฅ) = (๐ด + ๐‘ฆ))
8584eleq1d 2246 . . . 4 (๐‘ฅ = ๐‘ฆ โ†’ ((๐ด + ๐‘ฅ) โˆˆ โ„ โ†” (๐ด + ๐‘ฆ) โˆˆ โ„))
86 oveq2 5883 . . . . . 6 (๐‘ฅ = ๐‘ฆ โ†’ (๐ด โˆ’ ๐‘ฅ) = (๐ด โˆ’ ๐‘ฆ))
8786oveq2d 5891 . . . . 5 (๐‘ฅ = ๐‘ฆ โ†’ (i ยท (๐ด โˆ’ ๐‘ฅ)) = (i ยท (๐ด โˆ’ ๐‘ฆ)))
8887eleq1d 2246 . . . 4 (๐‘ฅ = ๐‘ฆ โ†’ ((i ยท (๐ด โˆ’ ๐‘ฅ)) โˆˆ โ„ โ†” (i ยท (๐ด โˆ’ ๐‘ฆ)) โˆˆ โ„))
8985, 88anbi12d 473 . . 3 (๐‘ฅ = ๐‘ฆ โ†’ (((๐ด + ๐‘ฅ) โˆˆ โ„ โˆง (i ยท (๐ด โˆ’ ๐‘ฅ)) โˆˆ โ„) โ†” ((๐ด + ๐‘ฆ) โˆˆ โ„ โˆง (i ยท (๐ด โˆ’ ๐‘ฆ)) โˆˆ โ„)))
9089reu4 2932 . 2 (โˆƒ!๐‘ฅ โˆˆ โ„‚ ((๐ด + ๐‘ฅ) โˆˆ โ„ โˆง (i ยท (๐ด โˆ’ ๐‘ฅ)) โˆˆ โ„) โ†” (โˆƒ๐‘ฅ โˆˆ โ„‚ ((๐ด + ๐‘ฅ) โˆˆ โ„ โˆง (i ยท (๐ด โˆ’ ๐‘ฅ)) โˆˆ โ„) โˆง โˆ€๐‘ฅ โˆˆ โ„‚ โˆ€๐‘ฆ โˆˆ โ„‚ ((((๐ด + ๐‘ฅ) โˆˆ โ„ โˆง (i ยท (๐ด โˆ’ ๐‘ฅ)) โˆˆ โ„) โˆง ((๐ด + ๐‘ฆ) โˆˆ โ„ โˆง (i ยท (๐ด โˆ’ ๐‘ฆ)) โˆˆ โ„)) โ†’ ๐‘ฅ = ๐‘ฆ)))
9153, 83, 90sylanbrc 417 1 (๐ด โˆˆ โ„‚ โ†’ โˆƒ!๐‘ฅ โˆˆ โ„‚ ((๐ด + ๐‘ฅ) โˆˆ โ„ โˆง (i ยท (๐ด โˆ’ ๐‘ฅ)) โˆˆ โ„))
Colors of variables: wff set class
Syntax hints:   โ†’ wi 4   โˆง wa 104   = wceq 1353   โˆˆ wcel 2148  โˆ€wral 2455  โˆƒwrex 2456  โˆƒ!wreu 2457  (class class class)co 5875  โ„‚cc 7809  โ„cr 7810  0cc0 7811  1c1 7812  ici 7813   + caddc 7814   ยท cmul 7816   โˆ’ cmin 8128  -cneg 8129
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-in1 614  ax-in2 615  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-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4122  ax-pow 4175  ax-pr 4210  ax-un 4434  ax-setind 4537  ax-cnex 7902  ax-resscn 7903  ax-1cn 7904  ax-1re 7905  ax-icn 7906  ax-addcl 7907  ax-addrcl 7908  ax-mulcl 7909  ax-mulrcl 7910  ax-addcom 7911  ax-mulcom 7912  ax-addass 7913  ax-mulass 7914  ax-distr 7915  ax-i2m1 7916  ax-0lt1 7917  ax-1rid 7918  ax-0id 7919  ax-rnegex 7920  ax-precex 7921  ax-cnre 7922  ax-pre-ltirr 7923  ax-pre-lttrn 7925  ax-pre-apti 7926  ax-pre-ltadd 7927  ax-pre-mulgt0 7928
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-reu 2462  df-rmo 2463  df-rab 2464  df-v 2740  df-sbc 2964  df-dif 3132  df-un 3134  df-in 3136  df-ss 3143  df-pw 3578  df-sn 3599  df-pr 3600  df-op 3602  df-uni 3811  df-br 4005  df-opab 4066  df-id 4294  df-xp 4633  df-rel 4634  df-cnv 4635  df-co 4636  df-dm 4637  df-iota 5179  df-fun 5219  df-fv 5225  df-riota 5831  df-ov 5878  df-oprab 5879  df-mpo 5880  df-pnf 7994  df-mnf 7995  df-ltxr 7997  df-sub 8130  df-neg 8131  df-reap 8532
This theorem is referenced by:  cjval  10854  cjth  10855  cjf  10856  remim  10869
  Copyright terms: Public domain W3C validator