P. 117 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 11601-11700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cjmulval 11601	A complex number times its conjugate. (Contributed by NM, 1-Feb-2007.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ (𝐴 ∈ ℂ → (𝐴 · (∗‘𝐴)) = (((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2)))
Theorem	cjmulge0 11602	A complex number times its conjugate is nonnegative. (Contributed by NM, 26-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ (𝐴 ∈ ℂ → 0 ≤ (𝐴 · (∗‘𝐴)))
Theorem	cjneg 11603	Complex conjugate of negative. (Contributed by NM, 27-Feb-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ (𝐴 ∈ ℂ → (∗‘-𝐴) = -(∗‘𝐴))
Theorem	addcj 11604	A number plus its conjugate is twice its real part. Compare Proposition 10-3.4(h) of [Gleason] p. 133. (Contributed by NM, 21-Jan-2007.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ (𝐴 ∈ ℂ → (𝐴 + (∗‘𝐴)) = (2 · (ℜ‘𝐴)))
Theorem	cjsub 11605	Complex conjugate distributes over subtraction. (Contributed by NM, 28-Apr-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (∗‘(𝐴 − 𝐵)) = ((∗‘𝐴) − (∗‘𝐵)))
Theorem	cjexp 11606	Complex conjugate of positive integer exponentiation. (Contributed by NM, 7-Jun-2006.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (∗‘(𝐴↑𝑁)) = ((∗‘𝐴)↑𝑁))
Theorem	imval2 11607	The imaginary part of a number in terms of complex conjugate. (Contributed by NM, 30-Apr-2005.)
⊢ (𝐴 ∈ ℂ → (ℑ‘𝐴) = ((𝐴 − (∗‘𝐴)) / (2 · i)))
Theorem	re0 11608	The real part of zero. (Contributed by NM, 27-Jul-1999.)
⊢ (ℜ‘0) = 0
Theorem	im0 11609	The imaginary part of zero. (Contributed by NM, 27-Jul-1999.)
⊢ (ℑ‘0) = 0
Theorem	re1 11610	The real part of one. (Contributed by Scott Fenton, 9-Jun-2006.)
⊢ (ℜ‘1) = 1
Theorem	im1 11611	The imaginary part of one. (Contributed by Scott Fenton, 9-Jun-2006.)
⊢ (ℑ‘1) = 0
Theorem	rei 11612	The real part of i. (Contributed by Scott Fenton, 9-Jun-2006.)
⊢ (ℜ‘i) = 0
Theorem	imi 11613	The imaginary part of i. (Contributed by Scott Fenton, 9-Jun-2006.)
⊢ (ℑ‘i) = 1
Theorem	cj0 11614	The conjugate of zero. (Contributed by NM, 27-Jul-1999.)
⊢ (∗‘0) = 0
Theorem	cji 11615	The complex conjugate of the imaginary unit. (Contributed by NM, 26-Mar-2005.)
⊢ (∗‘i) = -i
Theorem	cjreim 11616	The conjugate of a representation of a complex number in terms of real and imaginary parts. (Contributed by NM, 1-Jul-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (∗‘(𝐴 + (i · 𝐵))) = (𝐴 − (i · 𝐵)))
Theorem	cjreim2 11617	The conjugate of the representation of a complex number in terms of real and imaginary parts. (Contributed by NM, 1-Jul-2005.) (Proof shortened by Mario Carneiro, 29-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (∗‘(𝐴 − (i · 𝐵))) = (𝐴 + (i · 𝐵)))
Theorem	cj11 11618	Complex conjugate is a one-to-one function. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Eric Schmidt, 2-Jul-2009.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((∗‘𝐴) = (∗‘𝐵) ↔ 𝐴 = 𝐵))
Theorem	cjap 11619	Complex conjugate and apartness. (Contributed by Jim Kingdon, 14-Jun-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((∗‘𝐴) # (∗‘𝐵) ↔ 𝐴 # 𝐵))
Theorem	cjap0 11620	A number is apart from zero iff its complex conjugate is apart from zero. (Contributed by Jim Kingdon, 14-Jun-2020.)
⊢ (𝐴 ∈ ℂ → (𝐴 # 0 ↔ (∗‘𝐴) # 0))
Theorem	cjne0 11621	A number is nonzero iff its complex conjugate is nonzero. Also see cjap0 11620 which is similar but for apartness. (Contributed by NM, 29-Apr-2005.)
⊢ (𝐴 ∈ ℂ → (𝐴 ≠ 0 ↔ (∗‘𝐴) ≠ 0))
Theorem	cjdivap 11622	Complex conjugate distributes over division. (Contributed by Jim Kingdon, 14-Jun-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → (∗‘(𝐴 / 𝐵)) = ((∗‘𝐴) / (∗‘𝐵)))
Theorem	cnrecnv 11623*	The inverse to the canonical bijection from (ℝ × ℝ) to ℂ from cnref1o 10004. (Contributed by Mario Carneiro, 25-Aug-2014.)
⊢ 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + (i · 𝑦)))    ⇒   ⊢ ◡𝐹 = (𝑧 ∈ ℂ ↦ ⟨(ℜ‘𝑧), (ℑ‘𝑧)⟩)
Theorem	recli 11624	The real part of a complex number is real (closure law). (Contributed by NM, 11-May-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (ℜ‘𝐴) ∈ ℝ
Theorem	imcli 11625	The imaginary part of a complex number is real (closure law). (Contributed by NM, 11-May-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (ℑ‘𝐴) ∈ ℝ
Theorem	cjcli 11626	Closure law for complex conjugate. (Contributed by NM, 11-May-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (∗‘𝐴) ∈ ℂ
Theorem	replimi 11627	Construct a complex number from its real and imaginary parts. (Contributed by NM, 1-Oct-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ 𝐴 = ((ℜ‘𝐴) + (i · (ℑ‘𝐴)))
Theorem	cjcji 11628	The conjugate of the conjugate is the original complex number. Proposition 10-3.4(e) of [Gleason] p. 133. (Contributed by NM, 11-May-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (∗‘(∗‘𝐴)) = 𝐴
Theorem	reim0bi 11629	A number is real iff its imaginary part is 0. (Contributed by NM, 29-May-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 ∈ ℝ ↔ (ℑ‘𝐴) = 0)
Theorem	rerebi 11630	A real number equals its real part. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by NM, 27-Oct-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 ∈ ℝ ↔ (ℜ‘𝐴) = 𝐴)
Theorem	cjrebi 11631	A number is real iff it equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by NM, 11-Oct-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 ∈ ℝ ↔ (∗‘𝐴) = 𝐴)
Theorem	recji 11632	Real part of a complex conjugate. (Contributed by NM, 2-Oct-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (ℜ‘(∗‘𝐴)) = (ℜ‘𝐴)
Theorem	imcji 11633	Imaginary part of a complex conjugate. (Contributed by NM, 2-Oct-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (ℑ‘(∗‘𝐴)) = -(ℑ‘𝐴)
Theorem	cjmulrcli 11634	A complex number times its conjugate is real. (Contributed by NM, 11-May-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 · (∗‘𝐴)) ∈ ℝ
Theorem	cjmulvali 11635	A complex number times its conjugate. (Contributed by NM, 2-Oct-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 · (∗‘𝐴)) = (((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2))
Theorem	cjmulge0i 11636	A complex number times its conjugate is nonnegative. (Contributed by NM, 28-May-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ 0 ≤ (𝐴 · (∗‘𝐴))
Theorem	renegi 11637	Real part of negative. (Contributed by NM, 2-Aug-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (ℜ‘-𝐴) = -(ℜ‘𝐴)
Theorem	imnegi 11638	Imaginary part of negative. (Contributed by NM, 2-Aug-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (ℑ‘-𝐴) = -(ℑ‘𝐴)
Theorem	cjnegi 11639	Complex conjugate of negative. (Contributed by NM, 2-Aug-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (∗‘-𝐴) = -(∗‘𝐴)
Theorem	addcji 11640	A number plus its conjugate is twice its real part. Compare Proposition 10-3.4(h) of [Gleason] p. 133. (Contributed by NM, 2-Oct-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 + (∗‘𝐴)) = (2 · (ℜ‘𝐴))
Theorem	readdi 11641	Real part distributes over addition. (Contributed by NM, 28-Jul-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (ℜ‘(𝐴 + 𝐵)) = ((ℜ‘𝐴) + (ℜ‘𝐵))
Theorem	imaddi 11642	Imaginary part distributes over addition. (Contributed by NM, 28-Jul-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (ℑ‘(𝐴 + 𝐵)) = ((ℑ‘𝐴) + (ℑ‘𝐵))
Theorem	remuli 11643	Real part of a product. (Contributed by NM, 28-Jul-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (ℜ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℜ‘𝐵)) − ((ℑ‘𝐴) · (ℑ‘𝐵)))
Theorem	immuli 11644	Imaginary part of a product. (Contributed by NM, 28-Jul-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (ℑ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℑ‘𝐵)) + ((ℑ‘𝐴) · (ℜ‘𝐵)))
Theorem	cjaddi 11645	Complex conjugate distributes over addition. Proposition 10-3.4(a) of [Gleason] p. 133. (Contributed by NM, 28-Jul-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (∗‘(𝐴 + 𝐵)) = ((∗‘𝐴) + (∗‘𝐵))
Theorem	cjmuli 11646	Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of [Gleason] p. 133. (Contributed by NM, 28-Jul-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (∗‘(𝐴 · 𝐵)) = ((∗‘𝐴) · (∗‘𝐵))
Theorem	ipcni 11647	Standard inner product on complex numbers. (Contributed by NM, 2-Oct-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (ℜ‘(𝐴 · (∗‘𝐵))) = (((ℜ‘𝐴) · (ℜ‘𝐵)) + ((ℑ‘𝐴) · (ℑ‘𝐵)))
Theorem	cjdivapi 11648	Complex conjugate distributes over division. (Contributed by Jim Kingdon, 14-Jun-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐵 # 0 → (∗‘(𝐴 / 𝐵)) = ((∗‘𝐴) / (∗‘𝐵)))
Theorem	crrei 11649	The real part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by NM, 10-May-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (ℜ‘(𝐴 + (i · 𝐵))) = 𝐴
Theorem	crimi 11650	The imaginary part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by NM, 10-May-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (ℑ‘(𝐴 + (i · 𝐵))) = 𝐵
Theorem	recld 11651	The real part of a complex number is real (closure law). (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℜ‘𝐴) ∈ ℝ)
Theorem	imcld 11652	The imaginary part of a complex number is real (closure law). (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℑ‘𝐴) ∈ ℝ)
Theorem	cjcld 11653	Closure law for complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (∗‘𝐴) ∈ ℂ)
Theorem	replimd 11654	Construct a complex number from its real and imaginary parts. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → 𝐴 = ((ℜ‘𝐴) + (i · (ℑ‘𝐴))))
Theorem	remimd 11655	Value of the conjugate of a complex number. The value is the real part minus i times the imaginary part. Definition 10-3.2 of [Gleason] p. 132. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (∗‘𝐴) = ((ℜ‘𝐴) − (i · (ℑ‘𝐴))))
Theorem	cjcjd 11656	The conjugate of the conjugate is the original complex number. Proposition 10-3.4(e) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (∗‘(∗‘𝐴)) = 𝐴)
Theorem	reim0bd 11657	A number is real iff its imaginary part is 0. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → (ℑ‘𝐴) = 0)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℝ)
Theorem	rerebd 11658	A real number equals its real part. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → (ℜ‘𝐴) = 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℝ)
Theorem	cjrebd 11659	A number is real iff it equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → (∗‘𝐴) = 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℝ)
Theorem	cjne0d 11660	A number which is nonzero has a complex conjugate which is nonzero. Also see cjap0d 11661 which is similar but for apartness. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → (∗‘𝐴) ≠ 0)
Theorem	cjap0d 11661	A number which is apart from zero has a complex conjugate which is apart from zero. (Contributed by Jim Kingdon, 11-Aug-2021.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 0)    ⇒   ⊢ (𝜑 → (∗‘𝐴) # 0)
Theorem	recjd 11662	Real part of a complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℜ‘(∗‘𝐴)) = (ℜ‘𝐴))
Theorem	imcjd 11663	Imaginary part of a complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℑ‘(∗‘𝐴)) = -(ℑ‘𝐴))
Theorem	cjmulrcld 11664	A complex number times its conjugate is real. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 · (∗‘𝐴)) ∈ ℝ)
Theorem	cjmulvald 11665	A complex number times its conjugate. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 · (∗‘𝐴)) = (((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2)))
Theorem	cjmulge0d 11666	A complex number times its conjugate is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → 0 ≤ (𝐴 · (∗‘𝐴)))
Theorem	renegd 11667	Real part of negative. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℜ‘-𝐴) = -(ℜ‘𝐴))
Theorem	imnegd 11668	Imaginary part of negative. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℑ‘-𝐴) = -(ℑ‘𝐴))
Theorem	cjnegd 11669	Complex conjugate of negative. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (∗‘-𝐴) = -(∗‘𝐴))
Theorem	addcjd 11670	A number plus its conjugate is twice its real part. Compare Proposition 10-3.4(h) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 + (∗‘𝐴)) = (2 · (ℜ‘𝐴)))
Theorem	cjexpd 11671	Complex conjugate of positive integer exponentiation. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (∗‘(𝐴↑𝑁)) = ((∗‘𝐴)↑𝑁))
Theorem	readdd 11672	Real part distributes over addition. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℜ‘(𝐴 + 𝐵)) = ((ℜ‘𝐴) + (ℜ‘𝐵)))
Theorem	imaddd 11673	Imaginary part distributes over addition. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℑ‘(𝐴 + 𝐵)) = ((ℑ‘𝐴) + (ℑ‘𝐵)))
Theorem	resubd 11674	Real part distributes over subtraction. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℜ‘(𝐴 − 𝐵)) = ((ℜ‘𝐴) − (ℜ‘𝐵)))
Theorem	imsubd 11675	Imaginary part distributes over subtraction. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℑ‘(𝐴 − 𝐵)) = ((ℑ‘𝐴) − (ℑ‘𝐵)))
Theorem	remuld 11676	Real part of a product. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℜ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℜ‘𝐵)) − ((ℑ‘𝐴) · (ℑ‘𝐵))))
Theorem	immuld 11677	Imaginary part of a product. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℑ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℑ‘𝐵)) + ((ℑ‘𝐴) · (ℜ‘𝐵))))
Theorem	cjaddd 11678	Complex conjugate distributes over addition. Proposition 10-3.4(a) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (∗‘(𝐴 + 𝐵)) = ((∗‘𝐴) + (∗‘𝐵)))
Theorem	cjmuld 11679	Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (∗‘(𝐴 · 𝐵)) = ((∗‘𝐴) · (∗‘𝐵)))
Theorem	ipcnd 11680	Standard inner product on complex numbers. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℜ‘(𝐴 · (∗‘𝐵))) = (((ℜ‘𝐴) · (ℜ‘𝐵)) + ((ℑ‘𝐴) · (ℑ‘𝐵))))
Theorem	cjdivapd 11681	Complex conjugate distributes over division. (Contributed by Jim Kingdon, 15-Jun-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → (∗‘(𝐴 / 𝐵)) = ((∗‘𝐴) / (∗‘𝐵)))
Theorem	rered 11682	A real number equals its real part. One direction of Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (ℜ‘𝐴) = 𝐴)
Theorem	reim0d 11683	The imaginary part of a real number is 0. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (ℑ‘𝐴) = 0)
Theorem	cjred 11684	A real number equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (∗‘𝐴) = 𝐴)
Theorem	remul2d 11685	Real part of a product. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℜ‘(𝐴 · 𝐵)) = (𝐴 · (ℜ‘𝐵)))
Theorem	immul2d 11686	Imaginary part of a product. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℑ‘(𝐴 · 𝐵)) = (𝐴 · (ℑ‘𝐵)))
Theorem	redivapd 11687	Real part of a division. Related to remul2 11586. (Contributed by Jim Kingdon, 15-Jun-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 0)    ⇒   ⊢ (𝜑 → (ℜ‘(𝐵 / 𝐴)) = ((ℜ‘𝐵) / 𝐴))
Theorem	imdivapd 11688	Imaginary part of a division. Related to remul2 11586. (Contributed by Jim Kingdon, 15-Jun-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 0)    ⇒   ⊢ (𝜑 → (ℑ‘(𝐵 / 𝐴)) = ((ℑ‘𝐵) / 𝐴))
Theorem	crred 11689	The real part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (ℜ‘(𝐴 + (i · 𝐵))) = 𝐴)
Theorem	crimd 11690	The imaginary part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (ℑ‘(𝐴 + (i · 𝐵))) = 𝐵)
Theorem	cnreim 11691	Complex apartness in terms of real and imaginary parts. See also apreim 8895 which is similar but with different notation. (Contributed by Jim Kingdon, 16-Dec-2023.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 # 𝐵 ↔ ((ℜ‘𝐴) # (ℜ‘𝐵) ∨ (ℑ‘𝐴) # (ℑ‘𝐵))))
4.8.3  Sequence convergence
Theorem	caucvgrelemrec 11692*	Two ways to express a reciprocal. (Contributed by Jim Kingdon, 20-Jul-2021.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 # 0) → (℩𝑟 ∈ ℝ (𝐴 · 𝑟) = 1) = (1 / 𝐴))
Theorem	caucvgrelemcau 11693*	Lemma for caucvgre 11694. Converting the Cauchy condition. (Contributed by Jim Kingdon, 20-Jul-2021.)
⊢ (𝜑 → 𝐹:ℕ⟶ℝ)    &   ⊢ (𝜑 → ∀𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)((𝐹‘𝑛) < ((𝐹‘𝑘) + (1 / 𝑛)) ∧ (𝐹‘𝑘) < ((𝐹‘𝑛) + (1 / 𝑛))))    ⇒   ⊢ (𝜑 → ∀𝑛 ∈ ℕ ∀𝑘 ∈ ℕ (𝑛 <ℝ 𝑘 → ((𝐹‘𝑛) <ℝ ((𝐹‘𝑘) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)) ∧ (𝐹‘𝑘) <ℝ ((𝐹‘𝑛) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)))))
Theorem	caucvgre 11694*	Convergence of real sequences. A Cauchy sequence (as defined here, which has a rate of convergence built in) of real numbers converges to a real number. Specifically on rate of convergence, all terms after the nth term must be within 1 / 𝑛 of the nth term. (Contributed by Jim Kingdon, 19-Jul-2021.)
⊢ (𝜑 → 𝐹:ℕ⟶ℝ)    &   ⊢ (𝜑 → ∀𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)((𝐹‘𝑛) < ((𝐹‘𝑘) + (1 / 𝑛)) ∧ (𝐹‘𝑘) < ((𝐹‘𝑛) + (1 / 𝑛))))    ⇒   ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ≥‘𝑗)((𝐹‘𝑖) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹‘𝑖) + 𝑥)))
Theorem	cvg1nlemcxze 11695	Lemma for cvg1n 11699. Rearranging an expression related to the rate of convergence. (Contributed by Jim Kingdon, 6-Aug-2021.)
⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑍 ∈ ℕ)    &   ⊢ (𝜑 → 𝐸 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → ((((𝐶 · 2) / 𝑋) / 𝑍) + 𝐴) < 𝐸)    ⇒   ⊢ (𝜑 → (𝐶 / (𝐸 · 𝑍)) < (𝑋 / 2))
Theorem	cvg1nlemf 11696*	Lemma for cvg1n 11699. The modified sequence 𝐺 is a sequence. (Contributed by Jim Kingdon, 1-Aug-2021.)
⊢ (𝜑 → 𝐹:ℕ⟶ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → ∀𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)((𝐹‘𝑛) < ((𝐹‘𝑘) + (𝐶 / 𝑛)) ∧ (𝐹‘𝑘) < ((𝐹‘𝑛) + (𝐶 / 𝑛))))    &   ⊢ 𝐺 = (𝑗 ∈ ℕ ↦ (𝐹‘(𝑗 · 𝑍)))    &   ⊢ (𝜑 → 𝑍 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 < 𝑍)    ⇒   ⊢ (𝜑 → 𝐺:ℕ⟶ℝ)
Theorem	cvg1nlemcau 11697*	Lemma for cvg1n 11699. By selecting spaced out terms for the modified sequence 𝐺, the terms are within 1 / 𝑛 (without the constant 𝐶). (Contributed by Jim Kingdon, 1-Aug-2021.)
⊢ (𝜑 → 𝐹:ℕ⟶ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → ∀𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)((𝐹‘𝑛) < ((𝐹‘𝑘) + (𝐶 / 𝑛)) ∧ (𝐹‘𝑘) < ((𝐹‘𝑛) + (𝐶 / 𝑛))))    &   ⊢ 𝐺 = (𝑗 ∈ ℕ ↦ (𝐹‘(𝑗 · 𝑍)))    &   ⊢ (𝜑 → 𝑍 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 < 𝑍)    ⇒   ⊢ (𝜑 → ∀𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)((𝐺‘𝑛) < ((𝐺‘𝑘) + (1 / 𝑛)) ∧ (𝐺‘𝑘) < ((𝐺‘𝑛) + (1 / 𝑛))))
Theorem	cvg1nlemres 11698*	Lemma for cvg1n 11699. The original sequence 𝐹 has a limit (turns out it is the same as the limit of the modified sequence 𝐺). (Contributed by Jim Kingdon, 1-Aug-2021.)
⊢ (𝜑 → 𝐹:ℕ⟶ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → ∀𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)((𝐹‘𝑛) < ((𝐹‘𝑘) + (𝐶 / 𝑛)) ∧ (𝐹‘𝑘) < ((𝐹‘𝑛) + (𝐶 / 𝑛))))    &   ⊢ 𝐺 = (𝑗 ∈ ℕ ↦ (𝐹‘(𝑗 · 𝑍)))    &   ⊢ (𝜑 → 𝑍 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 < 𝑍)    ⇒   ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ≥‘𝑗)((𝐹‘𝑖) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹‘𝑖) + 𝑥)))
Theorem	cvg1n 11699*	Convergence of real sequences. This is a version of caucvgre 11694 with a constant multiplier 𝐶 on the rate of convergence. That is, all terms after the nth term must be within 𝐶 / 𝑛 of the nth term. (Contributed by Jim Kingdon, 1-Aug-2021.)
⊢ (𝜑 → 𝐹:ℕ⟶ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → ∀𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)((𝐹‘𝑛) < ((𝐹‘𝑘) + (𝐶 / 𝑛)) ∧ (𝐹‘𝑘) < ((𝐹‘𝑛) + (𝐶 / 𝑛))))    ⇒   ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ≥‘𝑗)((𝐹‘𝑖) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹‘𝑖) + 𝑥)))
Theorem	uzin2 11700	The upper integers are closed under intersection. (Contributed by Mario Carneiro, 24-Dec-2013.)
⊢ ((𝐴 ∈ ran ℤ≥ ∧ 𝐵 ∈ ran ℤ≥) → (𝐴 ∩ 𝐵) ∈ ran ℤ≥)