Theorem rpcnne0 13031

Description: A positive real is a nonzero complex number. (Contributed by NM, 11-Nov-2008.)

Assertion

Ref	Expression
rpcnne0	⊢ (𝐴 ∈ ℝ+ → (𝐴 ∈ ℂ ∧ 𝐴 ≠ 0))

Proof of Theorem rpcnne0

Step	Hyp	Ref	Expression
1		rpcn 13023	. 2 ⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℂ)
2		rpne0 13029	. 2 ⊢ (𝐴 ∈ ℝ+ → 𝐴 ≠ 0)
3	1, 2	jca 520	1 ⊢ (𝐴 ∈ ℝ+ → (𝐴 ∈ ℂ ∧ 𝐴 ≠ 0))

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2149   ≠ wne 2964  ℂcc 11094  0cc0 11096  ℝ⁺crp 13012

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5258  ax-nul 5268  ax-pow 5334  ax-pr 5402  ax-un 7730  ax-resscn 11153  ax-1cn 11154  ax-addrcl 11157  ax-rnegex 11167  ax-cnre 11169  ax-pre-lttri 11170  ax-pre-lttrn 11171

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5554  df-po 5567  df-so 5568  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11241  df-mnf 11242  df-ltxr 11244  df-rp 13013

This theorem is referenced by:  rpcndif0  13033  mod0  13905  modlt  13909  modcyc  13935  modmuladdnn0  13947  moddi  13971  modirr  13974  icchmeo  25065  aaliou3lem3  26470  aaliou3lem8  26471  reeff1o  26572  reeflog  26707  relogeftb  26711  rpcxpcl  26803  relogbcxp  26912  rlimcnp  27092  rlimcnp2  27093  divsqrtsumlem  27106  harmonicbnd4  27137  logfacrlim  27350  logexprlim  27351  vmadivsum  27608  dchrmusum2  27620  dchrvmasumlem2  27624  dchrvmasumiflem1  27627  dchrisum0lem2a  27643  mudivsum  27656  mulogsumlem  27657  mulog2sumlem2  27661  selberglem2  27672  selberg2lem  27676  selberg2  27677  pntrsumo1  27691  selbergr  27694  pntibndlem2  27717  pntibndlem3  27718  pntlemb  27723  pntlemr  27728  pntlemf  27731  blocnilem  31093  minvecolem3  31165  itg2addnclem2  38206  fllogbd  49218