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

Theorem cnegexlem2 7950
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 7952. (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 7770 . 2 0 ∈ ℂ
2 cnre 7774 . 2 (0 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 0 = (𝑥 + (i · 𝑦)))
3 ax-rnegex 7741 . . . . . 6 (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0)
43adantr 274 . . . . 5 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0)
5 recn 7765 . . . . . . . . . . 11 (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
6 ax-icn 7727 . . . . . . . . . . . 12 i ∈ ℂ
7 recn 7765 . . . . . . . . . . . 12 (𝑦 ∈ ℝ → 𝑦 ∈ ℂ)
8 mulcl 7759 . . . . . . . . . . . 12 ((i ∈ ℂ ∧ 𝑦 ∈ ℂ) → (i · 𝑦) ∈ ℂ)
96, 7, 8sylancr 410 . . . . . . . . . . 11 (𝑦 ∈ ℝ → (i · 𝑦) ∈ ℂ)
10 recn 7765 . . . . . . . . . . 11 (𝑧 ∈ ℝ → 𝑧 ∈ ℂ)
11 addid2 7913 . . . . . . . . . . . . . . 15 (𝑧 ∈ ℂ → (0 + 𝑧) = 𝑧)
12113ad2ant3 1004 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℂ ∧ (i · 𝑦) ∈ ℂ ∧ 𝑧 ∈ ℂ) → (0 + 𝑧) = 𝑧)
1312adantr 274 . . . . . . . . . . . . 13 (((𝑥 ∈ ℂ ∧ (i · 𝑦) ∈ ℂ ∧ 𝑧 ∈ ℂ) ∧ ((𝑥 + 𝑧) = 0 ∧ 0 = (𝑥 + (i · 𝑦)))) → (0 + 𝑧) = 𝑧)
14 oveq1 5781 . . . . . . . . . . . . . . 15 ((𝑥 + 𝑧) = 0 → ((𝑥 + 𝑧) + (i · 𝑦)) = (0 + (i · 𝑦)))
1514ad2antrl 481 . . . . . . . . . . . . . 14 (((𝑥 ∈ ℂ ∧ (i · 𝑦) ∈ ℂ ∧ 𝑧 ∈ ℂ) ∧ ((𝑥 + 𝑧) = 0 ∧ 0 = (𝑥 + (i · 𝑦)))) → ((𝑥 + 𝑧) + (i · 𝑦)) = (0 + (i · 𝑦)))
16 add32 7933 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ (i · 𝑦) ∈ ℂ) → ((𝑥 + 𝑧) + (i · 𝑦)) = ((𝑥 + (i · 𝑦)) + 𝑧))
17163com23 1187 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℂ ∧ (i · 𝑦) ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝑥 + 𝑧) + (i · 𝑦)) = ((𝑥 + (i · 𝑦)) + 𝑧))
18 oveq1 5781 . . . . . . . . . . . . . . . . 17 (0 = (𝑥 + (i · 𝑦)) → (0 + 𝑧) = ((𝑥 + (i · 𝑦)) + 𝑧))
1918eqcomd 2145 . . . . . . . . . . . . . . . 16 (0 = (𝑥 + (i · 𝑦)) → ((𝑥 + (i · 𝑦)) + 𝑧) = (0 + 𝑧))
2017, 19sylan9eq 2192 . . . . . . . . . . . . . . 15 (((𝑥 ∈ ℂ ∧ (i · 𝑦) ∈ ℂ ∧ 𝑧 ∈ ℂ) ∧ 0 = (𝑥 + (i · 𝑦))) → ((𝑥 + 𝑧) + (i · 𝑦)) = (0 + 𝑧))
2120adantrl 469 . . . . . . . . . . . . . 14 (((𝑥 ∈ ℂ ∧ (i · 𝑦) ∈ ℂ ∧ 𝑧 ∈ ℂ) ∧ ((𝑥 + 𝑧) = 0 ∧ 0 = (𝑥 + (i · 𝑦)))) → ((𝑥 + 𝑧) + (i · 𝑦)) = (0 + 𝑧))
22 addid2 7913 . . . . . . . . . . . . . . . 16 ((i · 𝑦) ∈ ℂ → (0 + (i · 𝑦)) = (i · 𝑦))
23223ad2ant2 1003 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℂ ∧ (i · 𝑦) ∈ ℂ ∧ 𝑧 ∈ ℂ) → (0 + (i · 𝑦)) = (i · 𝑦))
2423adantr 274 . . . . . . . . . . . . . 14 (((𝑥 ∈ ℂ ∧ (i · 𝑦) ∈ ℂ ∧ 𝑧 ∈ ℂ) ∧ ((𝑥 + 𝑧) = 0 ∧ 0 = (𝑥 + (i · 𝑦)))) → (0 + (i · 𝑦)) = (i · 𝑦))
2515, 21, 243eqtr3d 2180 . . . . . . . . . . . . 13 (((𝑥 ∈ ℂ ∧ (i · 𝑦) ∈ ℂ ∧ 𝑧 ∈ ℂ) ∧ ((𝑥 + 𝑧) = 0 ∧ 0 = (𝑥 + (i · 𝑦)))) → (0 + 𝑧) = (i · 𝑦))
2613, 25eqtr3d 2174 . . . . . . . . . . . 12 (((𝑥 ∈ ℂ ∧ (i · 𝑦) ∈ ℂ ∧ 𝑧 ∈ ℂ) ∧ ((𝑥 + 𝑧) = 0 ∧ 0 = (𝑥 + (i · 𝑦)))) → 𝑧 = (i · 𝑦))
2726ex 114 . . . . . . . . . . 11 ((𝑥 ∈ ℂ ∧ (i · 𝑦) ∈ ℂ ∧ 𝑧 ∈ ℂ) → (((𝑥 + 𝑧) = 0 ∧ 0 = (𝑥 + (i · 𝑦))) → 𝑧 = (i · 𝑦)))
285, 9, 10, 27syl3an 1258 . . . . . . . . . 10 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (((𝑥 + 𝑧) = 0 ∧ 0 = (𝑥 + (i · 𝑦))) → 𝑧 = (i · 𝑦)))
29283expa 1181 . . . . . . . . 9 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ ℝ) → (((𝑥 + 𝑧) = 0 ∧ 0 = (𝑥 + (i · 𝑦))) → 𝑧 = (i · 𝑦)))
3029imp 123 . . . . . . . 8 ((((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ ℝ) ∧ ((𝑥 + 𝑧) = 0 ∧ 0 = (𝑥 + (i · 𝑦)))) → 𝑧 = (i · 𝑦))
31 simplr 519 . . . . . . . 8 ((((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ ℝ) ∧ ((𝑥 + 𝑧) = 0 ∧ 0 = (𝑥 + (i · 𝑦)))) → 𝑧 ∈ ℝ)
3230, 31eqeltrrd 2217 . . . . . . 7 ((((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ ℝ) ∧ ((𝑥 + 𝑧) = 0 ∧ 0 = (𝑥 + (i · 𝑦)))) → (i · 𝑦) ∈ ℝ)
3332exp32 362 . . . . . 6 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ ℝ) → ((𝑥 + 𝑧) = 0 → (0 = (𝑥 + (i · 𝑦)) → (i · 𝑦) ∈ ℝ)))
3433rexlimdva 2549 . . . . 5 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0 → (0 = (𝑥 + (i · 𝑦)) → (i · 𝑦) ∈ ℝ)))
354, 34mpd 13 . . . 4 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (0 = (𝑥 + (i · 𝑦)) → (i · 𝑦) ∈ ℝ))
3635reximdva 2534 . . 3 (𝑥 ∈ ℝ → (∃𝑦 ∈ ℝ 0 = (𝑥 + (i · 𝑦)) → ∃𝑦 ∈ ℝ (i · 𝑦) ∈ ℝ))
3736rexlimiv 2543 . 2 (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 0 = (𝑥 + (i · 𝑦)) → ∃𝑦 ∈ ℝ (i · 𝑦) ∈ ℝ)
381, 2, 37mp2b 8 1 𝑦 ∈ ℝ (i · 𝑦) ∈ ℝ
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 962   = wceq 1331  wcel 1480  wrex 2417  (class class class)co 5774  cc 7630  cr 7631  0cc0 7632  ici 7634   + caddc 7635   · cmul 7637
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-resscn 7724  ax-1cn 7725  ax-icn 7727  ax-addcl 7728  ax-mulcl 7730  ax-addcom 7732  ax-addass 7734  ax-i2m1 7737  ax-0id 7740  ax-rnegex 7741  ax-cnre 7743
This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ral 2421  df-rex 2422  df-v 2688  df-un 3075  df-in 3077  df-ss 3084  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-br 3930  df-iota 5088  df-fv 5131  df-ov 5777
This theorem is referenced by:  cnegex  7952
  Copyright terms: Public domain W3C validator