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

Axiom ax-cnre 7921
Description: A complex number can be expressed in terms of two reals. Definition 10-1.1(v) of [Gleason] p. 130. Axiom for real and complex numbers, justified by Theorem axcnre 7879. For naming consistency, use cnre 7952 for new proofs. (New usage is discouraged.) (Contributed by NM, 9-May-1999.)
Assertion
Ref Expression
ax-cnre (๐ด โˆˆ โ„‚ โ†’ โˆƒ๐‘ฅ โˆˆ โ„ โˆƒ๐‘ฆ โˆˆ โ„ ๐ด = (๐‘ฅ + (i ยท ๐‘ฆ)))
Distinct variable group:   ๐‘ฅ,๐‘ฆ,๐ด

Detailed syntax breakdown of Axiom ax-cnre
StepHypRef Expression
1 cA . . 3 class ๐ด
2 cc 7808 . . 3 class โ„‚
31, 2wcel 2148 . 2 wff ๐ด โˆˆ โ„‚
4 vx . . . . . . 7 setvar ๐‘ฅ
54cv 1352 . . . . . 6 class ๐‘ฅ
6 ci 7812 . . . . . . 7 class i
7 vy . . . . . . . 8 setvar ๐‘ฆ
87cv 1352 . . . . . . 7 class ๐‘ฆ
9 cmul 7815 . . . . . . 7 class ยท
106, 8, 9co 5874 . . . . . 6 class (i ยท ๐‘ฆ)
11 caddc 7813 . . . . . 6 class +
125, 10, 11co 5874 . . . . 5 class (๐‘ฅ + (i ยท ๐‘ฆ))
131, 12wceq 1353 . . . 4 wff ๐ด = (๐‘ฅ + (i ยท ๐‘ฆ))
14 cr 7809 . . . 4 class โ„
1513, 7, 14wrex 2456 . . 3 wff โˆƒ๐‘ฆ โˆˆ โ„ ๐ด = (๐‘ฅ + (i ยท ๐‘ฆ))
1615, 4, 14wrex 2456 . 2 wff โˆƒ๐‘ฅ โˆˆ โ„ โˆƒ๐‘ฆ โˆˆ โ„ ๐ด = (๐‘ฅ + (i ยท ๐‘ฆ))
173, 16wi 4 1 wff (๐ด โˆˆ โ„‚ โ†’ โˆƒ๐‘ฅ โˆˆ โ„ โˆƒ๐‘ฆ โˆˆ โ„ ๐ด = (๐‘ฅ + (i ยท ๐‘ฆ)))
Colors of variables: wff set class
This axiom is referenced by:  cnre  7952
  Copyright terms: Public domain W3C validator