ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-re Structured version   Unicode version

Definition df-re 9071
Description: Define a function whose value is the real part of a complex number. See reval 9077 for its value, recli 9139 for its closure, and replim 9087 for its use in decomposing a complex number. (Contributed by NM, 9-May-1999.)
Assertion
Ref Expression
df-re  Re  CC  |->  +  * `  2

Detailed syntax breakdown of Definition df-re
StepHypRef Expression
1 cre 9068 . 2  Re
2 vx . . 3  setvar
3 cc 6709 . . 3  CC
42cv 1241 . . . . 5
5 ccj 9067 . . . . . 6  *
64, 5cfv 4845 . . . . 5  * `
7 caddc 6714 . . . . 5  +
84, 6, 7co 5455 . . . 4  +  * `
9 c2 7744 . . . 4  2
10 cdiv 7433 . . . 4
118, 9, 10co 5455 . . 3  +  * `
 2
122, 3, 11cmpt 3809 . 2  CC  |->  +  * `
 2
131, 12wceq 1242 1  Re  CC  |->  +  * `  2
Colors of variables: wff set class
This definition is referenced by:  reval  9077  ref  9083
  Copyright terms: Public domain W3C validator