Theorem rpcnne0d 13166

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 13159	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
3	1	rpne0d 13162	. 2 ⊢ (𝜑 → 𝐴 ≠ 0)
4	2, 3	jca 521	1 ⊢ (𝜑 → (𝐴 ∈ ℂ ∧ 𝐴 ≠ 0))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145   ≠ wne 2956  ℂcc 11191  0cc0 11193  ℝ⁺crp 13113

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7749  ax-resscn 11250  ax-1cn 11251  ax-addrcl 11254  ax-rnegex 11264  ax-cnre 11266  ax-pre-lttri 11267  ax-pre-lttrn 11268

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-po 5559  df-so 5560  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-er 8710  df-en 8967  df-dom 8968  df-sdom 8969  df-pnf 11338  df-mnf 11339  df-ltxr 11341  df-rp 13114

This theorem is used by:  expcnv  16026  mertenslem1  16046  divgcdcoprm0  16833  ovolscalem1  25827  aalioulem2  26653  aalioulem3  26654  dvsqrt  27063  cxpcn3lem  27068  relogbval  27093  relogbcl  27094  nnlogbexp  27102  divsqrtsumlem  27300  logexprlim  27545  2lgslem3b  27717  2lgslem3c  27718  2lgslem3d  27719  chebbnd1lem3  27791  chebbnd1  27792  chtppilimlem1  27793  chtppilimlem2  27794  chebbnd2  27797  chpchtlim  27799  chpo1ub  27800  rplogsumlem1  27804  rplogsumlem2  27805  rpvmasumlem  27807  dchrvmasumlem1  27815  dchrvmasum2lem  27816  dchrvmasumlem2  27818  dchrisum0fno1  27831  dchrisum0lem1b  27835  dchrisum0lem1  27836  dchrisum0lem2a  27837  dchrisum0lem2  27838  dchrisum0lem3  27839  rplogsum  27847  mulogsum  27852  mulog2sumlem1  27854  selberglem1  27865  pntrmax  27884  pntpbnd1a  27905  pntibndlem2  27911  pntlemc  27915  pntlemb  27917  pntlemn  27920  pntlemr  27922  pntlemj  27923  pntlemf  27925  pntlemk  27926  pntlemo  27927  pnt2  27933  bcm1n  33380  jm2.21  43980  stoweidlem25  47004  stoweidlem42  47021  wallispilem4  47047  stirlinglem10  47062  fourierdlem39  47125  lighneallem3  48661  dignn0flhalflem1  49696  dignn0flhalflem2  49697  itschlc0xyqsol1  49847