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

Theorem cnegexlem2 7249
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 7251. (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 7076 . 2 0 ∈ ℂ
2 cnre 7080 . 2 (0 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 0 = (𝑥 + (i · 𝑦)))
3 ax-rnegex 7050 . . . . . 6 (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0)
43adantr 265 . . . . 5 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0)
5 recn 7071 . . . . . . . . . . 11 (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
6 ax-icn 7036 . . . . . . . . . . . 12 i ∈ ℂ
7 recn 7071 . . . . . . . . . . . 12 (𝑦 ∈ ℝ → 𝑦 ∈ ℂ)
8 mulcl 7065 . . . . . . . . . . . 12 ((i ∈ ℂ ∧ 𝑦 ∈ ℂ) → (i · 𝑦) ∈ ℂ)
96, 7, 8sylancr 399 . . . . . . . . . . 11 (𝑦 ∈ ℝ → (i · 𝑦) ∈ ℂ)
10 recn 7071 . . . . . . . . . . 11 (𝑧 ∈ ℝ → 𝑧 ∈ ℂ)
11 addid2 7212 . . . . . . . . . . . . . . 15 (𝑧 ∈ ℂ → (0 + 𝑧) = 𝑧)
12113ad2ant3 938 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℂ ∧ (i · 𝑦) ∈ ℂ ∧ 𝑧 ∈ ℂ) → (0 + 𝑧) = 𝑧)
1312adantr 265 . . . . . . . . . . . . 13 (((𝑥 ∈ ℂ ∧ (i · 𝑦) ∈ ℂ ∧ 𝑧 ∈ ℂ) ∧ ((𝑥 + 𝑧) = 0 ∧ 0 = (𝑥 + (i · 𝑦)))) → (0 + 𝑧) = 𝑧)
14 oveq1 5546 . . . . . . . . . . . . . . 15 ((𝑥 + 𝑧) = 0 → ((𝑥 + 𝑧) + (i · 𝑦)) = (0 + (i · 𝑦)))
1514ad2antrl 467 . . . . . . . . . . . . . 14 (((𝑥 ∈ ℂ ∧ (i · 𝑦) ∈ ℂ ∧ 𝑧 ∈ ℂ) ∧ ((𝑥 + 𝑧) = 0 ∧ 0 = (𝑥 + (i · 𝑦)))) → ((𝑥 + 𝑧) + (i · 𝑦)) = (0 + (i · 𝑦)))
16 add32 7232 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ (i · 𝑦) ∈ ℂ) → ((𝑥 + 𝑧) + (i · 𝑦)) = ((𝑥 + (i · 𝑦)) + 𝑧))
17163com23 1121 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℂ ∧ (i · 𝑦) ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝑥 + 𝑧) + (i · 𝑦)) = ((𝑥 + (i · 𝑦)) + 𝑧))
18 oveq1 5546 . . . . . . . . . . . . . . . . 17 (0 = (𝑥 + (i · 𝑦)) → (0 + 𝑧) = ((𝑥 + (i · 𝑦)) + 𝑧))
1918eqcomd 2061 . . . . . . . . . . . . . . . 16 (0 = (𝑥 + (i · 𝑦)) → ((𝑥 + (i · 𝑦)) + 𝑧) = (0 + 𝑧))
2017, 19sylan9eq 2108 . . . . . . . . . . . . . . 15 (((𝑥 ∈ ℂ ∧ (i · 𝑦) ∈ ℂ ∧ 𝑧 ∈ ℂ) ∧ 0 = (𝑥 + (i · 𝑦))) → ((𝑥 + 𝑧) + (i · 𝑦)) = (0 + 𝑧))
2120adantrl 455 . . . . . . . . . . . . . 14 (((𝑥 ∈ ℂ ∧ (i · 𝑦) ∈ ℂ ∧ 𝑧 ∈ ℂ) ∧ ((𝑥 + 𝑧) = 0 ∧ 0 = (𝑥 + (i · 𝑦)))) → ((𝑥 + 𝑧) + (i · 𝑦)) = (0 + 𝑧))
22 addid2 7212 . . . . . . . . . . . . . . . 16 ((i · 𝑦) ∈ ℂ → (0 + (i · 𝑦)) = (i · 𝑦))
23223ad2ant2 937 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℂ ∧ (i · 𝑦) ∈ ℂ ∧ 𝑧 ∈ ℂ) → (0 + (i · 𝑦)) = (i · 𝑦))
2423adantr 265 . . . . . . . . . . . . . 14 (((𝑥 ∈ ℂ ∧ (i · 𝑦) ∈ ℂ ∧ 𝑧 ∈ ℂ) ∧ ((𝑥 + 𝑧) = 0 ∧ 0 = (𝑥 + (i · 𝑦)))) → (0 + (i · 𝑦)) = (i · 𝑦))
2515, 21, 243eqtr3d 2096 . . . . . . . . . . . . 13 (((𝑥 ∈ ℂ ∧ (i · 𝑦) ∈ ℂ ∧ 𝑧 ∈ ℂ) ∧ ((𝑥 + 𝑧) = 0 ∧ 0 = (𝑥 + (i · 𝑦)))) → (0 + 𝑧) = (i · 𝑦))
2613, 25eqtr3d 2090 . . . . . . . . . . . 12 (((𝑥 ∈ ℂ ∧ (i · 𝑦) ∈ ℂ ∧ 𝑧 ∈ ℂ) ∧ ((𝑥 + 𝑧) = 0 ∧ 0 = (𝑥 + (i · 𝑦)))) → 𝑧 = (i · 𝑦))
2726ex 112 . . . . . . . . . . 11 ((𝑥 ∈ ℂ ∧ (i · 𝑦) ∈ ℂ ∧ 𝑧 ∈ ℂ) → (((𝑥 + 𝑧) = 0 ∧ 0 = (𝑥 + (i · 𝑦))) → 𝑧 = (i · 𝑦)))
285, 9, 10, 27syl3an 1188 . . . . . . . . . 10 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (((𝑥 + 𝑧) = 0 ∧ 0 = (𝑥 + (i · 𝑦))) → 𝑧 = (i · 𝑦)))
29283expa 1115 . . . . . . . . 9 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ ℝ) → (((𝑥 + 𝑧) = 0 ∧ 0 = (𝑥 + (i · 𝑦))) → 𝑧 = (i · 𝑦)))
3029imp 119 . . . . . . . 8 ((((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ ℝ) ∧ ((𝑥 + 𝑧) = 0 ∧ 0 = (𝑥 + (i · 𝑦)))) → 𝑧 = (i · 𝑦))
31 simplr 490 . . . . . . . 8 ((((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ ℝ) ∧ ((𝑥 + 𝑧) = 0 ∧ 0 = (𝑥 + (i · 𝑦)))) → 𝑧 ∈ ℝ)
3230, 31eqeltrrd 2131 . . . . . . 7 ((((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ ℝ) ∧ ((𝑥 + 𝑧) = 0 ∧ 0 = (𝑥 + (i · 𝑦)))) → (i · 𝑦) ∈ ℝ)
3332exp32 351 . . . . . 6 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ ℝ) → ((𝑥 + 𝑧) = 0 → (0 = (𝑥 + (i · 𝑦)) → (i · 𝑦) ∈ ℝ)))
3433rexlimdva 2450 . . . . 5 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0 → (0 = (𝑥 + (i · 𝑦)) → (i · 𝑦) ∈ ℝ)))
354, 34mpd 13 . . . 4 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (0 = (𝑥 + (i · 𝑦)) → (i · 𝑦) ∈ ℝ))
3635reximdva 2438 . . 3 (𝑥 ∈ ℝ → (∃𝑦 ∈ ℝ 0 = (𝑥 + (i · 𝑦)) → ∃𝑦 ∈ ℝ (i · 𝑦) ∈ ℝ))
3736rexlimiv 2444 . 2 (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 0 = (𝑥 + (i · 𝑦)) → ∃𝑦 ∈ ℝ (i · 𝑦) ∈ ℝ)
381, 2, 37mp2b 8 1 𝑦 ∈ ℝ (i · 𝑦) ∈ ℝ
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101  w3a 896   = wceq 1259  wcel 1409  wrex 2324  (class class class)co 5539  cc 6944  cr 6945  0cc0 6946  ici 6948   + caddc 6949   · cmul 6951
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038  ax-resscn 7033  ax-1cn 7034  ax-icn 7036  ax-addcl 7037  ax-mulcl 7039  ax-addcom 7041  ax-addass 7043  ax-i2m1 7046  ax-0id 7049  ax-rnegex 7050  ax-cnre 7052
This theorem depends on definitions:  df-bi 114  df-3an 898  df-tru 1262  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-ral 2328  df-rex 2329  df-v 2576  df-un 2949  df-in 2951  df-ss 2958  df-sn 3408  df-pr 3409  df-op 3411  df-uni 3608  df-br 3792  df-iota 4894  df-fv 4937  df-ov 5542
This theorem is referenced by:  cnegex  7251
  Copyright terms: Public domain W3C validator