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

Theorem cnegexlem2 6964
 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 6966. (Contributed by Eric Schmidt, 22-May-2007.)
Assertion
Ref Expression
cnegexlem2 y ℝ (i · y)

Proof of Theorem cnegexlem2
Dummy variables x z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 0cn 6797 . 2 0
2 cnre 6801 . 2 (0 ℂ → x y ℝ 0 = (x + (i · y)))
3 ax-rnegex 6772 . . . . . 6 (x ℝ → z ℝ (x + z) = 0)
43adantr 261 . . . . 5 ((x y ℝ) → z ℝ (x + z) = 0)
5 recn 6792 . . . . . . . . . . 11 (x ℝ → x ℂ)
6 ax-icn 6758 . . . . . . . . . . . 12 i
7 recn 6792 . . . . . . . . . . . 12 (y ℝ → y ℂ)
8 mulcl 6786 . . . . . . . . . . . 12 ((i y ℂ) → (i · y) ℂ)
96, 7, 8sylancr 393 . . . . . . . . . . 11 (y ℝ → (i · y) ℂ)
10 recn 6792 . . . . . . . . . . 11 (z ℝ → z ℂ)
11 addid2 6929 . . . . . . . . . . . . . . 15 (z ℂ → (0 + z) = z)
12113ad2ant3 926 . . . . . . . . . . . . . 14 ((x (i · y) z ℂ) → (0 + z) = z)
1312adantr 261 . . . . . . . . . . . . 13 (((x (i · y) z ℂ) ((x + z) = 0 0 = (x + (i · y)))) → (0 + z) = z)
14 oveq1 5462 . . . . . . . . . . . . . . 15 ((x + z) = 0 → ((x + z) + (i · y)) = (0 + (i · y)))
1514ad2antrl 459 . . . . . . . . . . . . . 14 (((x (i · y) z ℂ) ((x + z) = 0 0 = (x + (i · y)))) → ((x + z) + (i · y)) = (0 + (i · y)))
16 add32 6947 . . . . . . . . . . . . . . . . 17 ((x z (i · y) ℂ) → ((x + z) + (i · y)) = ((x + (i · y)) + z))
17163com23 1109 . . . . . . . . . . . . . . . 16 ((x (i · y) z ℂ) → ((x + z) + (i · y)) = ((x + (i · y)) + z))
18 oveq1 5462 . . . . . . . . . . . . . . . . 17 (0 = (x + (i · y)) → (0 + z) = ((x + (i · y)) + z))
1918eqcomd 2042 . . . . . . . . . . . . . . . 16 (0 = (x + (i · y)) → ((x + (i · y)) + z) = (0 + z))
2017, 19sylan9eq 2089 . . . . . . . . . . . . . . 15 (((x (i · y) z ℂ) 0 = (x + (i · y))) → ((x + z) + (i · y)) = (0 + z))
2120adantrl 447 . . . . . . . . . . . . . 14 (((x (i · y) z ℂ) ((x + z) = 0 0 = (x + (i · y)))) → ((x + z) + (i · y)) = (0 + z))
22 addid2 6929 . . . . . . . . . . . . . . . 16 ((i · y) ℂ → (0 + (i · y)) = (i · y))
23223ad2ant2 925 . . . . . . . . . . . . . . 15 ((x (i · y) z ℂ) → (0 + (i · y)) = (i · y))
2423adantr 261 . . . . . . . . . . . . . 14 (((x (i · y) z ℂ) ((x + z) = 0 0 = (x + (i · y)))) → (0 + (i · y)) = (i · y))
2515, 21, 243eqtr3d 2077 . . . . . . . . . . . . 13 (((x (i · y) z ℂ) ((x + z) = 0 0 = (x + (i · y)))) → (0 + z) = (i · y))
2613, 25eqtr3d 2071 . . . . . . . . . . . 12 (((x (i · y) z ℂ) ((x + z) = 0 0 = (x + (i · y)))) → z = (i · y))
2726ex 108 . . . . . . . . . . 11 ((x (i · y) z ℂ) → (((x + z) = 0 0 = (x + (i · y))) → z = (i · y)))
285, 9, 10, 27syl3an 1176 . . . . . . . . . 10 ((x y z ℝ) → (((x + z) = 0 0 = (x + (i · y))) → z = (i · y)))
29283expa 1103 . . . . . . . . 9 (((x y ℝ) z ℝ) → (((x + z) = 0 0 = (x + (i · y))) → z = (i · y)))
3029imp 115 . . . . . . . 8 ((((x y ℝ) z ℝ) ((x + z) = 0 0 = (x + (i · y)))) → z = (i · y))
31 simplr 482 . . . . . . . 8 ((((x y ℝ) z ℝ) ((x + z) = 0 0 = (x + (i · y)))) → z ℝ)
3230, 31eqeltrrd 2112 . . . . . . 7 ((((x y ℝ) z ℝ) ((x + z) = 0 0 = (x + (i · y)))) → (i · y) ℝ)
3332exp32 347 . . . . . 6 (((x y ℝ) z ℝ) → ((x + z) = 0 → (0 = (x + (i · y)) → (i · y) ℝ)))
3433rexlimdva 2427 . . . . 5 ((x y ℝ) → (z ℝ (x + z) = 0 → (0 = (x + (i · y)) → (i · y) ℝ)))
354, 34mpd 13 . . . 4 ((x y ℝ) → (0 = (x + (i · y)) → (i · y) ℝ))
3635reximdva 2415 . . 3 (x ℝ → (y ℝ 0 = (x + (i · y)) → y ℝ (i · y) ℝ))
3736rexlimiv 2421 . 2 (x y ℝ 0 = (x + (i · y)) → y ℝ (i · y) ℝ)
381, 2, 37mp2b 8 1 y ℝ (i · y)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ∧ w3a 884   = 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-mulcl 6761  ax-addcom 6763  ax-addass 6765  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:  cnegex  6966
 Copyright terms: Public domain W3C validator