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

Theorem cnegexlem2 8133
Description: Existence of a real number which produces a real number when multiplied by i. (Hint: zero is such a number, although we don't need to prove that yet). Lemma for cnegex 8135. (Contributed by Eric Schmidt, 22-May-2007.)
Assertion
Ref Expression
cnegexlem2 โˆƒ๐‘ฆ โˆˆ โ„ (i ยท ๐‘ฆ) โˆˆ โ„

Proof of Theorem cnegexlem2
Dummy variables ๐‘ฅ ๐‘ง are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 0cn 7949 . 2 0 โˆˆ โ„‚
2 cnre 7953 . 2 (0 โˆˆ โ„‚ โ†’ โˆƒ๐‘ฅ โˆˆ โ„ โˆƒ๐‘ฆ โˆˆ โ„ 0 = (๐‘ฅ + (i ยท ๐‘ฆ)))
3 ax-rnegex 7920 . . . . . 6 (๐‘ฅ โˆˆ โ„ โ†’ โˆƒ๐‘ง โˆˆ โ„ (๐‘ฅ + ๐‘ง) = 0)
43adantr 276 . . . . 5 ((๐‘ฅ โˆˆ โ„ โˆง ๐‘ฆ โˆˆ โ„) โ†’ โˆƒ๐‘ง โˆˆ โ„ (๐‘ฅ + ๐‘ง) = 0)
5 recn 7944 . . . . . . . . . . 11 (๐‘ฅ โˆˆ โ„ โ†’ ๐‘ฅ โˆˆ โ„‚)
6 ax-icn 7906 . . . . . . . . . . . 12 i โˆˆ โ„‚
7 recn 7944 . . . . . . . . . . . 12 (๐‘ฆ โˆˆ โ„ โ†’ ๐‘ฆ โˆˆ โ„‚)
8 mulcl 7938 . . . . . . . . . . . 12 ((i โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‚) โ†’ (i ยท ๐‘ฆ) โˆˆ โ„‚)
96, 7, 8sylancr 414 . . . . . . . . . . 11 (๐‘ฆ โˆˆ โ„ โ†’ (i ยท ๐‘ฆ) โˆˆ โ„‚)
10 recn 7944 . . . . . . . . . . 11 (๐‘ง โˆˆ โ„ โ†’ ๐‘ง โˆˆ โ„‚)
11 addlid 8096 . . . . . . . . . . . . . . 15 (๐‘ง โˆˆ โ„‚ โ†’ (0 + ๐‘ง) = ๐‘ง)
12113ad2ant3 1020 . . . . . . . . . . . . . 14 ((๐‘ฅ โˆˆ โ„‚ โˆง (i ยท ๐‘ฆ) โˆˆ โ„‚ โˆง ๐‘ง โˆˆ โ„‚) โ†’ (0 + ๐‘ง) = ๐‘ง)
1312adantr 276 . . . . . . . . . . . . 13 (((๐‘ฅ โˆˆ โ„‚ โˆง (i ยท ๐‘ฆ) โˆˆ โ„‚ โˆง ๐‘ง โˆˆ โ„‚) โˆง ((๐‘ฅ + ๐‘ง) = 0 โˆง 0 = (๐‘ฅ + (i ยท ๐‘ฆ)))) โ†’ (0 + ๐‘ง) = ๐‘ง)
14 oveq1 5882 . . . . . . . . . . . . . . 15 ((๐‘ฅ + ๐‘ง) = 0 โ†’ ((๐‘ฅ + ๐‘ง) + (i ยท ๐‘ฆ)) = (0 + (i ยท ๐‘ฆ)))
1514ad2antrl 490 . . . . . . . . . . . . . 14 (((๐‘ฅ โˆˆ โ„‚ โˆง (i ยท ๐‘ฆ) โˆˆ โ„‚ โˆง ๐‘ง โˆˆ โ„‚) โˆง ((๐‘ฅ + ๐‘ง) = 0 โˆง 0 = (๐‘ฅ + (i ยท ๐‘ฆ)))) โ†’ ((๐‘ฅ + ๐‘ง) + (i ยท ๐‘ฆ)) = (0 + (i ยท ๐‘ฆ)))
16 add32 8116 . . . . . . . . . . . . . . . . 17 ((๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ง โˆˆ โ„‚ โˆง (i ยท ๐‘ฆ) โˆˆ โ„‚) โ†’ ((๐‘ฅ + ๐‘ง) + (i ยท ๐‘ฆ)) = ((๐‘ฅ + (i ยท ๐‘ฆ)) + ๐‘ง))
17163com23 1209 . . . . . . . . . . . . . . . 16 ((๐‘ฅ โˆˆ โ„‚ โˆง (i ยท ๐‘ฆ) โˆˆ โ„‚ โˆง ๐‘ง โˆˆ โ„‚) โ†’ ((๐‘ฅ + ๐‘ง) + (i ยท ๐‘ฆ)) = ((๐‘ฅ + (i ยท ๐‘ฆ)) + ๐‘ง))
18 oveq1 5882 . . . . . . . . . . . . . . . . 17 (0 = (๐‘ฅ + (i ยท ๐‘ฆ)) โ†’ (0 + ๐‘ง) = ((๐‘ฅ + (i ยท ๐‘ฆ)) + ๐‘ง))
1918eqcomd 2183 . . . . . . . . . . . . . . . 16 (0 = (๐‘ฅ + (i ยท ๐‘ฆ)) โ†’ ((๐‘ฅ + (i ยท ๐‘ฆ)) + ๐‘ง) = (0 + ๐‘ง))
2017, 19sylan9eq 2230 . . . . . . . . . . . . . . 15 (((๐‘ฅ โˆˆ โ„‚ โˆง (i ยท ๐‘ฆ) โˆˆ โ„‚ โˆง ๐‘ง โˆˆ โ„‚) โˆง 0 = (๐‘ฅ + (i ยท ๐‘ฆ))) โ†’ ((๐‘ฅ + ๐‘ง) + (i ยท ๐‘ฆ)) = (0 + ๐‘ง))
2120adantrl 478 . . . . . . . . . . . . . 14 (((๐‘ฅ โˆˆ โ„‚ โˆง (i ยท ๐‘ฆ) โˆˆ โ„‚ โˆง ๐‘ง โˆˆ โ„‚) โˆง ((๐‘ฅ + ๐‘ง) = 0 โˆง 0 = (๐‘ฅ + (i ยท ๐‘ฆ)))) โ†’ ((๐‘ฅ + ๐‘ง) + (i ยท ๐‘ฆ)) = (0 + ๐‘ง))
22 addlid 8096 . . . . . . . . . . . . . . . 16 ((i ยท ๐‘ฆ) โˆˆ โ„‚ โ†’ (0 + (i ยท ๐‘ฆ)) = (i ยท ๐‘ฆ))
23223ad2ant2 1019 . . . . . . . . . . . . . . 15 ((๐‘ฅ โˆˆ โ„‚ โˆง (i ยท ๐‘ฆ) โˆˆ โ„‚ โˆง ๐‘ง โˆˆ โ„‚) โ†’ (0 + (i ยท ๐‘ฆ)) = (i ยท ๐‘ฆ))
2423adantr 276 . . . . . . . . . . . . . 14 (((๐‘ฅ โˆˆ โ„‚ โˆง (i ยท ๐‘ฆ) โˆˆ โ„‚ โˆง ๐‘ง โˆˆ โ„‚) โˆง ((๐‘ฅ + ๐‘ง) = 0 โˆง 0 = (๐‘ฅ + (i ยท ๐‘ฆ)))) โ†’ (0 + (i ยท ๐‘ฆ)) = (i ยท ๐‘ฆ))
2515, 21, 243eqtr3d 2218 . . . . . . . . . . . . 13 (((๐‘ฅ โˆˆ โ„‚ โˆง (i ยท ๐‘ฆ) โˆˆ โ„‚ โˆง ๐‘ง โˆˆ โ„‚) โˆง ((๐‘ฅ + ๐‘ง) = 0 โˆง 0 = (๐‘ฅ + (i ยท ๐‘ฆ)))) โ†’ (0 + ๐‘ง) = (i ยท ๐‘ฆ))
2613, 25eqtr3d 2212 . . . . . . . . . . . 12 (((๐‘ฅ โˆˆ โ„‚ โˆง (i ยท ๐‘ฆ) โˆˆ โ„‚ โˆง ๐‘ง โˆˆ โ„‚) โˆง ((๐‘ฅ + ๐‘ง) = 0 โˆง 0 = (๐‘ฅ + (i ยท ๐‘ฆ)))) โ†’ ๐‘ง = (i ยท ๐‘ฆ))
2726ex 115 . . . . . . . . . . 11 ((๐‘ฅ โˆˆ โ„‚ โˆง (i ยท ๐‘ฆ) โˆˆ โ„‚ โˆง ๐‘ง โˆˆ โ„‚) โ†’ (((๐‘ฅ + ๐‘ง) = 0 โˆง 0 = (๐‘ฅ + (i ยท ๐‘ฆ))) โ†’ ๐‘ง = (i ยท ๐‘ฆ)))
285, 9, 10, 27syl3an 1280 . . . . . . . . . 10 ((๐‘ฅ โˆˆ โ„ โˆง ๐‘ฆ โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„) โ†’ (((๐‘ฅ + ๐‘ง) = 0 โˆง 0 = (๐‘ฅ + (i ยท ๐‘ฆ))) โ†’ ๐‘ง = (i ยท ๐‘ฆ)))
29283expa 1203 . . . . . . . . 9 (((๐‘ฅ โˆˆ โ„ โˆง ๐‘ฆ โˆˆ โ„) โˆง ๐‘ง โˆˆ โ„) โ†’ (((๐‘ฅ + ๐‘ง) = 0 โˆง 0 = (๐‘ฅ + (i ยท ๐‘ฆ))) โ†’ ๐‘ง = (i ยท ๐‘ฆ)))
3029imp 124 . . . . . . . 8 ((((๐‘ฅ โˆˆ โ„ โˆง ๐‘ฆ โˆˆ โ„) โˆง ๐‘ง โˆˆ โ„) โˆง ((๐‘ฅ + ๐‘ง) = 0 โˆง 0 = (๐‘ฅ + (i ยท ๐‘ฆ)))) โ†’ ๐‘ง = (i ยท ๐‘ฆ))
31 simplr 528 . . . . . . . 8 ((((๐‘ฅ โˆˆ โ„ โˆง ๐‘ฆ โˆˆ โ„) โˆง ๐‘ง โˆˆ โ„) โˆง ((๐‘ฅ + ๐‘ง) = 0 โˆง 0 = (๐‘ฅ + (i ยท ๐‘ฆ)))) โ†’ ๐‘ง โˆˆ โ„)
3230, 31eqeltrrd 2255 . . . . . . 7 ((((๐‘ฅ โˆˆ โ„ โˆง ๐‘ฆ โˆˆ โ„) โˆง ๐‘ง โˆˆ โ„) โˆง ((๐‘ฅ + ๐‘ง) = 0 โˆง 0 = (๐‘ฅ + (i ยท ๐‘ฆ)))) โ†’ (i ยท ๐‘ฆ) โˆˆ โ„)
3332exp32 365 . . . . . 6 (((๐‘ฅ โˆˆ โ„ โˆง ๐‘ฆ โˆˆ โ„) โˆง ๐‘ง โˆˆ โ„) โ†’ ((๐‘ฅ + ๐‘ง) = 0 โ†’ (0 = (๐‘ฅ + (i ยท ๐‘ฆ)) โ†’ (i ยท ๐‘ฆ) โˆˆ โ„)))
3433rexlimdva 2594 . . . . 5 ((๐‘ฅ โˆˆ โ„ โˆง ๐‘ฆ โˆˆ โ„) โ†’ (โˆƒ๐‘ง โˆˆ โ„ (๐‘ฅ + ๐‘ง) = 0 โ†’ (0 = (๐‘ฅ + (i ยท ๐‘ฆ)) โ†’ (i ยท ๐‘ฆ) โˆˆ โ„)))
354, 34mpd 13 . . . 4 ((๐‘ฅ โˆˆ โ„ โˆง ๐‘ฆ โˆˆ โ„) โ†’ (0 = (๐‘ฅ + (i ยท ๐‘ฆ)) โ†’ (i ยท ๐‘ฆ) โˆˆ โ„))
3635reximdva 2579 . . 3 (๐‘ฅ โˆˆ โ„ โ†’ (โˆƒ๐‘ฆ โˆˆ โ„ 0 = (๐‘ฅ + (i ยท ๐‘ฆ)) โ†’ โˆƒ๐‘ฆ โˆˆ โ„ (i ยท ๐‘ฆ) โˆˆ โ„))
3736rexlimiv 2588 . 2 (โˆƒ๐‘ฅ โˆˆ โ„ โˆƒ๐‘ฆ โˆˆ โ„ 0 = (๐‘ฅ + (i ยท ๐‘ฆ)) โ†’ โˆƒ๐‘ฆ โˆˆ โ„ (i ยท ๐‘ฆ) โˆˆ โ„)
381, 2, 37mp2b 8 1 โˆƒ๐‘ฆ โˆˆ โ„ (i ยท ๐‘ฆ) โˆˆ โ„
Colors of variables: wff set class
Syntax hints:   โ†’ wi 4   โˆง wa 104   โˆง w3a 978   = wceq 1353   โˆˆ wcel 2148  โˆƒwrex 2456  (class class class)co 5875  โ„‚cc 7809  โ„cr 7810  0cc0 7811  ici 7813   + caddc 7814   ยท cmul 7816
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 7903  ax-1cn 7904  ax-icn 7906  ax-addcl 7907  ax-mulcl 7909  ax-addcom 7911  ax-addass 7913  ax-i2m1 7916  ax-0id 7919  ax-rnegex 7920  ax-cnre 7922
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 2740  df-un 3134  df-in 3136  df-ss 3143  df-sn 3599  df-pr 3600  df-op 3602  df-uni 3811  df-br 4005  df-iota 5179  df-fv 5225  df-ov 5878
This theorem is referenced by:  cnegex  8135
  Copyright terms: Public domain W3C validator