Theorem rpcnne0d 13064

Description: A positive real is a nonzero complex number. (Contributed by Mario Carneiro, 28-May-2016.)

Hypothesis

Ref	Expression
rpred.1	⊢ (𝜑 → 𝐴 ∈ ℝ+)

Assertion

Ref	Expression
rpcnne0d	⊢ (𝜑 → (𝐴 ∈ ℂ ∧ 𝐴 ≠ 0))

Proof of Theorem rpcnne0d

Step	Hyp	Ref	Expression
1		rpred.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ+)
2	1	rpcnd 13057	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
3	1	rpne0d 13060	. 2 ⊢ (𝜑 → 𝐴 ≠ 0)
4	2, 3	jca 520	1 ⊢ (𝜑 → (𝐴 ∈ ℂ ∧ 𝐴 ≠ 0))

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2143   ≠ wne 2958  ℂcc 11093  0cc0 11095  ℝ⁺crp 13011

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-resscn 11152  ax-1cn 11153  ax-addrcl 11156  ax-rnegex 11166  ax-cnre 11168  ax-pre-lttri 11169  ax-pre-lttrn 11170

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-po 5569  df-so 5570  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11240  df-mnf 11241  df-ltxr 11243  df-rp 13012

This theorem is referenced by:  expcnv  15914  mertenslem1  15934  divgcdcoprm0  16718  ovolscalem1  25672  aalioulem2  26496  aalioulem3  26497  dvsqrt  26907  cxpcn3lem  26912  relogbval  26937  relogbcl  26938  nnlogbexp  26946  divsqrtsumlem  27144  logexprlim  27389  2lgslem3b  27561  2lgslem3c  27562  2lgslem3d  27563  chebbnd1lem3  27635  chebbnd1  27636  chtppilimlem1  27637  chtppilimlem2  27638  chebbnd2  27641  chpchtlim  27643  chpo1ub  27644  rplogsumlem1  27648  rplogsumlem2  27649  rpvmasumlem  27651  dchrvmasumlem1  27659  dchrvmasum2lem  27660  dchrvmasumlem2  27662  dchrisum0fno1  27675  dchrisum0lem1b  27679  dchrisum0lem1  27680  dchrisum0lem2a  27681  dchrisum0lem2  27682  dchrisum0lem3  27683  rplogsum  27691  mulogsum  27696  mulog2sumlem1  27698  selberglem1  27709  pntrmax  27728  pntpbnd1a  27749  pntibndlem2  27755  pntlemc  27759  pntlemb  27761  pntlemn  27764  pntlemr  27766  pntlemj  27767  pntlemf  27769  pntlemk  27770  pntlemo  27771  pnt2  27777  bcm1n  33140  jm2.21  43721  stoweidlem25  46739  stoweidlem42  46756  wallispilem4  46782  stirlinglem10  46797  fourierdlem39  46860  lighneallem3  48359  dignn0flhalflem1  49395  dignn0flhalflem2  49396  itschlc0xyqsol1  49546