P. 104 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 10301-10400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	fnfzo0hash 10301	The size of a function on a half-open range of nonnegative integers equals the upper bound of this range. (Contributed by Alexander van der Vekens, 26-Jan-2018.) (Proof shortened by AV, 11-Apr-2021.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹:(0..^𝑁)⟶𝐵) → (♯‘𝐹) = 𝑁)
Theorem	hashfacen 10302*	The number of bijections between two sets is a cardinal invariant. (Contributed by Mario Carneiro, 21-Jan-2015.)
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷) → {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐶} ≈ {𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐷})
Theorem	leisorel 10303	Version of isorel 5601 for strictly increasing functions on the reals. (Contributed by Mario Carneiro, 6-Apr-2015.) (Revised by Mario Carneiro, 9-Sep-2015.)
⊢ ((𝐹 Isom < , < (𝐴, 𝐵) ∧ (𝐴 ⊆ ℝ* ∧ 𝐵 ⊆ ℝ*) ∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → (𝐶 ≤ 𝐷 ↔ (𝐹‘𝐶) ≤ (𝐹‘𝐷)))
Theorem	zfz1isolemsplit 10304	Lemma for zfz1iso 10307. Removing one element from an integer range. (Contributed by Jim Kingdon, 8-Sep-2022.)
⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑋)    ⇒   ⊢ (𝜑 → (1...(♯‘𝑋)) = ((1...(♯‘(𝑋 ∖ {𝑀}))) ∪ {(♯‘𝑋)}))
Theorem	zfz1isolemiso 10305*	Lemma for zfz1iso 10307. Adding one element to the order isomorphism. (Contributed by Jim Kingdon, 8-Sep-2022.)
⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝑋 ⊆ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑋)    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑋 𝑧 ≤ 𝑀)    &   ⊢ (𝜑 → 𝐺 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀})))    &   ⊢ (𝜑 → 𝐴 ∈ (1...(♯‘𝑋)))    &   ⊢ (𝜑 → 𝐵 ∈ (1...(♯‘𝑋)))    ⇒   ⊢ (𝜑 → (𝐴 < 𝐵 ↔ ((𝐺 ∪ {⟨(♯‘𝑋), 𝑀⟩})‘𝐴) < ((𝐺 ∪ {⟨(♯‘𝑋), 𝑀⟩})‘𝐵)))
Theorem	zfz1isolem1 10306*	Lemma for zfz1iso 10307. Existence of an order isomorphism given the existence of shorter isomorphisms. (Contributed by Jim Kingdon, 7-Sep-2022.)
⊢ (𝜑 → 𝐾 ∈ ω)    &   ⊢ (𝜑 → ∀𝑦(((𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑦 ≈ 𝐾) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑦)), 𝑦)))    &   ⊢ (𝜑 → 𝑋 ⊆ ℤ)    &   ⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝑋 ≈ suc 𝐾)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑋)    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑋 𝑧 ≤ 𝑀)    ⇒   ⊢ (𝜑 → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑋)), 𝑋))
Theorem	zfz1iso 10307*	A finite set of integers has an order isomorphism to a one-based finite sequence. (Contributed by Jim Kingdon, 3-Sep-2022.)
⊢ ((𝐴 ⊆ ℤ ∧ 𝐴 ∈ Fin) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝐴)), 𝐴))
Theorem	iseqcoll 10308*	The function 𝐹 contains a sparse set of nonzero values to be summed. The function 𝐺 is an order isomorphism from the set of nonzero values of 𝐹 to a 1-based finite sequence, and 𝐻 collects these nonzero values together. Under these conditions, the sum over the values in 𝐻 yields the same result as the sum over the original set 𝐹. (Contributed by Mario Carneiro, 2-Apr-2014.)
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑆) → (𝑍 + 𝑘) = 𝑘)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑆) → (𝑘 + 𝑍) = 𝑘)    &   ⊢ ((𝜑 ∧ (𝑘 ∈ 𝑆 ∧ 𝑛 ∈ 𝑆)) → (𝑘 + 𝑛) ∈ 𝑆)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴))    &   ⊢ (𝜑 → 𝑁 ∈ (1...(♯‘𝐴)))    &   ⊢ (𝜑 → 𝐴 ⊆ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1)) → (𝐻‘𝑘) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀...(𝐺‘(♯‘𝐴))) ∖ 𝐴)) → (𝐹‘𝑘) = 𝑍)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (𝐻‘𝑛) = (𝐹‘(𝐺‘𝑛)))    ⇒   ⊢ (𝜑 → (seq𝑀( + , 𝐹, 𝑆)‘(𝐺‘𝑁)) = (seq1( + , 𝐻, 𝑆)‘𝑁))
3.7  Elementary real and complex functions
3.7.1  The "shift" operation
Syntax	cshi 10309	Extend class notation with function shifter.
class shift
Definition	df-shft 10310*	Define a function shifter. This operation offsets the value argument of a function (ordinarily on a subset of ℂ) and produces a new function on ℂ. See shftval 10320 for its value. (Contributed by NM, 20-Jul-2005.)
⊢ shift = (𝑓 ∈ V, 𝑥 ∈ ℂ ↦ {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ ℂ ∧ (𝑦 − 𝑥)𝑓𝑧)})
Theorem	shftlem 10311*	Two ways to write a shifted set (𝐵 + 𝐴). (Contributed by Mario Carneiro, 3-Nov-2013.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ⊆ ℂ) → {𝑥 ∈ ℂ ∣ (𝑥 − 𝐴) ∈ 𝐵} = {𝑥 ∣ ∃𝑦 ∈ 𝐵 𝑥 = (𝑦 + 𝐴)})
Theorem	shftuz 10312*	A shift of the upper integers. (Contributed by Mario Carneiro, 5-Nov-2013.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → {𝑥 ∈ ℂ ∣ (𝑥 − 𝐴) ∈ (ℤ≥‘𝐵)} = (ℤ≥‘(𝐵 + 𝐴)))
Theorem	shftfvalg 10313*	The value of the sequence shifter operation is a function on ℂ. 𝐴 is ordinarily an integer. (Contributed by NM, 20-Jul-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐹 ∈ 𝑉) → (𝐹 shift 𝐴) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦)})
Theorem	ovshftex 10314	Existence of the result of applying shift. (Contributed by Jim Kingdon, 15-Aug-2021.)
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐴 ∈ ℂ) → (𝐹 shift 𝐴) ∈ V)
Theorem	shftfibg 10315	Value of a fiber of the relation 𝐹. (Contributed by Jim Kingdon, 15-Aug-2021.)
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift 𝐴) “ {𝐵}) = (𝐹 “ {(𝐵 − 𝐴)}))
Theorem	shftfval 10316*	The value of the sequence shifter operation is a function on ℂ. 𝐴 is ordinarily an integer. (Contributed by NM, 20-Jul-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
⊢ 𝐹 ∈ V    ⇒   ⊢ (𝐴 ∈ ℂ → (𝐹 shift 𝐴) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦)})
Theorem	shftdm 10317*	Domain of a relation shifted by 𝐴. The set on the right is more commonly notated as (dom 𝐹 + 𝐴) (meaning add 𝐴 to every element of dom 𝐹). (Contributed by Mario Carneiro, 3-Nov-2013.)
⊢ 𝐹 ∈ V    ⇒   ⊢ (𝐴 ∈ ℂ → dom (𝐹 shift 𝐴) = {𝑥 ∈ ℂ ∣ (𝑥 − 𝐴) ∈ dom 𝐹})
Theorem	shftfib 10318	Value of a fiber of the relation 𝐹. (Contributed by Mario Carneiro, 4-Nov-2013.)
⊢ 𝐹 ∈ V    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift 𝐴) “ {𝐵}) = (𝐹 “ {(𝐵 − 𝐴)}))
Theorem	shftfn 10319*	Functionality and domain of a sequence shifted by 𝐴. (Contributed by NM, 20-Jul-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
⊢ 𝐹 ∈ V    ⇒   ⊢ ((𝐹 Fn 𝐵 ∧ 𝐴 ∈ ℂ) → (𝐹 shift 𝐴) Fn {𝑥 ∈ ℂ ∣ (𝑥 − 𝐴) ∈ 𝐵})
Theorem	shftval 10320	Value of a sequence shifted by 𝐴. (Contributed by NM, 20-Jul-2005.) (Revised by Mario Carneiro, 4-Nov-2013.)
⊢ 𝐹 ∈ V    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift 𝐴)‘𝐵) = (𝐹‘(𝐵 − 𝐴)))
Theorem	shftval2 10321	Value of a sequence shifted by 𝐴 − 𝐵. (Contributed by NM, 20-Jul-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
⊢ 𝐹 ∈ V    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐹 shift (𝐴 − 𝐵))‘(𝐴 + 𝐶)) = (𝐹‘(𝐵 + 𝐶)))
Theorem	shftval3 10322	Value of a sequence shifted by 𝐴 − 𝐵. (Contributed by NM, 20-Jul-2005.)
⊢ 𝐹 ∈ V    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift (𝐴 − 𝐵))‘𝐴) = (𝐹‘𝐵))
Theorem	shftval4 10323	Value of a sequence shifted by -𝐴. (Contributed by NM, 18-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
⊢ 𝐹 ∈ V    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift -𝐴)‘𝐵) = (𝐹‘(𝐴 + 𝐵)))
Theorem	shftval5 10324	Value of a shifted sequence. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
⊢ 𝐹 ∈ V    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift 𝐴)‘(𝐵 + 𝐴)) = (𝐹‘𝐵))
Theorem	shftf 10325*	Functionality of a shifted sequence. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
⊢ 𝐹 ∈ V    ⇒   ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐴 ∈ ℂ) → (𝐹 shift 𝐴):{𝑥 ∈ ℂ ∣ (𝑥 − 𝐴) ∈ 𝐵}⟶𝐶)
Theorem	2shfti 10326	Composite shift operations. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
⊢ 𝐹 ∈ V    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift 𝐴) shift 𝐵) = (𝐹 shift (𝐴 + 𝐵)))
Theorem	shftidt2 10327	Identity law for the shift operation. (Contributed by Mario Carneiro, 5-Nov-2013.)
⊢ 𝐹 ∈ V    ⇒   ⊢ (𝐹 shift 0) = (𝐹 ↾ ℂ)
Theorem	shftidt 10328	Identity law for the shift operation. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
⊢ 𝐹 ∈ V    ⇒   ⊢ (𝐴 ∈ ℂ → ((𝐹 shift 0)‘𝐴) = (𝐹‘𝐴))
Theorem	shftcan1 10329	Cancellation law for the shift operation. (Contributed by NM, 4-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
⊢ 𝐹 ∈ V    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐹 shift 𝐴) shift -𝐴)‘𝐵) = (𝐹‘𝐵))
Theorem	shftcan2 10330	Cancellation law for the shift operation. (Contributed by NM, 4-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
⊢ 𝐹 ∈ V    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐹 shift -𝐴) shift 𝐴)‘𝐵) = (𝐹‘𝐵))
Theorem	shftvalg 10331	Value of a sequence shifted by 𝐴. (Contributed by Scott Fenton, 16-Dec-2017.)
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift 𝐴)‘𝐵) = (𝐹‘(𝐵 − 𝐴)))
Theorem	shftval4g 10332	Value of a sequence shifted by -𝐴. (Contributed by Jim Kingdon, 19-Aug-2021.)
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift -𝐴)‘𝐵) = (𝐹‘(𝐴 + 𝐵)))
Theorem	seq3shft 10333*	Shifting the index set of a sequence. (Contributed by NM, 17-Mar-2005.) (Revised by Jim Kingdon, 17-Oct-2022.)
⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 − 𝑁))) → (𝐹‘𝑥) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)    ⇒   ⊢ (𝜑 → seq𝑀( + , (𝐹 shift 𝑁)) = (seq(𝑀 − 𝑁)( + , 𝐹) shift 𝑁))
3.7.2  Real and imaginary parts; conjugate
Syntax	ccj 10334	Extend class notation to include complex conjugate function.
class ∗
Syntax	cre 10335	Extend class notation to include real part of a complex number.
class ℜ
Syntax	cim 10336	Extend class notation to include imaginary part of a complex number.
class ℑ
Definition	df-cj 10337*	Define the complex conjugate function. See cjcli 10408 for its closure and cjval 10340 for its value. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
⊢ ∗ = (𝑥 ∈ ℂ ↦ (℩𝑦 ∈ ℂ ((𝑥 + 𝑦) ∈ ℝ ∧ (i · (𝑥 − 𝑦)) ∈ ℝ)))
Definition	df-re 10338	Define a function whose value is the real part of a complex number. See reval 10344 for its value, recli 10406 for its closure, and replim 10354 for its use in decomposing a complex number. (Contributed by NM, 9-May-1999.)
⊢ ℜ = (𝑥 ∈ ℂ ↦ ((𝑥 + (∗‘𝑥)) / 2))
Definition	df-im 10339	Define a function whose value is the imaginary part of a complex number. See imval 10345 for its value, imcli 10407 for its closure, and replim 10354 for its use in decomposing a complex number. (Contributed by NM, 9-May-1999.)
⊢ ℑ = (𝑥 ∈ ℂ ↦ (ℜ‘(𝑥 / i)))
Theorem	cjval 10340*	The value of the conjugate of a complex number. (Contributed by Mario Carneiro, 6-Nov-2013.)
⊢ (𝐴 ∈ ℂ → (∗‘𝐴) = (℩𝑥 ∈ ℂ ((𝐴 + 𝑥) ∈ ℝ ∧ (i · (𝐴 − 𝑥)) ∈ ℝ)))
Theorem	cjth 10341	The defining property of the complex conjugate. (Contributed by Mario Carneiro, 6-Nov-2013.)
⊢ (𝐴 ∈ ℂ → ((𝐴 + (∗‘𝐴)) ∈ ℝ ∧ (i · (𝐴 − (∗‘𝐴))) ∈ ℝ))
Theorem	cjf 10342	Domain and codomain of the conjugate function. (Contributed by Mario Carneiro, 6-Nov-2013.)
⊢ ∗:ℂ⟶ℂ
Theorem	cjcl 10343	The conjugate of a complex number is a complex number (closure law). (Contributed by NM, 10-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
⊢ (𝐴 ∈ ℂ → (∗‘𝐴) ∈ ℂ)
Theorem	reval 10344	The value of the real part of a complex number. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
⊢ (𝐴 ∈ ℂ → (ℜ‘𝐴) = ((𝐴 + (∗‘𝐴)) / 2))
Theorem	imval 10345	The value of the imaginary part of a complex number. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
⊢ (𝐴 ∈ ℂ → (ℑ‘𝐴) = (ℜ‘(𝐴 / i)))
Theorem	imre 10346	The imaginary part of a complex number in terms of the real part function. (Contributed by NM, 12-May-2005.) (Revised by Mario Carneiro, 6-Nov-2013.)
⊢ (𝐴 ∈ ℂ → (ℑ‘𝐴) = (ℜ‘(-i · 𝐴)))
Theorem	reim 10347	The real part of a complex number in terms of the imaginary part function. (Contributed by Mario Carneiro, 31-Mar-2015.)
⊢ (𝐴 ∈ ℂ → (ℜ‘𝐴) = (ℑ‘(i · 𝐴)))
Theorem	recl 10348	The real part of a complex number is real. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
⊢ (𝐴 ∈ ℂ → (ℜ‘𝐴) ∈ ℝ)
Theorem	imcl 10349	The imaginary part of a complex number is real. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
⊢ (𝐴 ∈ ℂ → (ℑ‘𝐴) ∈ ℝ)
Theorem	ref 10350	Domain and codomain of the real part function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 6-Nov-2013.)
⊢ ℜ:ℂ⟶ℝ
Theorem	imf 10351	Domain and codomain of the imaginary part function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 6-Nov-2013.)
⊢ ℑ:ℂ⟶ℝ
Theorem	crre 10352	The real part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by NM, 12-May-2005.) (Revised by Mario Carneiro, 7-Nov-2013.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (ℜ‘(𝐴 + (i · 𝐵))) = 𝐴)
Theorem	crim 10353	The real part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by NM, 12-May-2005.) (Revised by Mario Carneiro, 7-Nov-2013.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (ℑ‘(𝐴 + (i · 𝐵))) = 𝐵)
Theorem	replim 10354	Reconstruct a complex number from its real and imaginary parts. (Contributed by NM, 10-May-1999.) (Revised by Mario Carneiro, 7-Nov-2013.)
⊢ (𝐴 ∈ ℂ → 𝐴 = ((ℜ‘𝐴) + (i · (ℑ‘𝐴))))
Theorem	remim 10355	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 NM, 10-May-1999.) (Revised by Mario Carneiro, 7-Nov-2013.)
⊢ (𝐴 ∈ ℂ → (∗‘𝐴) = ((ℜ‘𝐴) − (i · (ℑ‘𝐴))))
Theorem	reim0 10356	The imaginary part of a real number is 0. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 7-Nov-2013.)
⊢ (𝐴 ∈ ℝ → (ℑ‘𝐴) = 0)
Theorem	reim0b 10357	A number is real iff its imaginary part is 0. (Contributed by NM, 26-Sep-2005.)
⊢ (𝐴 ∈ ℂ → (𝐴 ∈ ℝ ↔ (ℑ‘𝐴) = 0))
Theorem	rereb 10358	A number is real iff it equals its real part. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by NM, 20-Aug-2008.)
⊢ (𝐴 ∈ ℂ → (𝐴 ∈ ℝ ↔ (ℜ‘𝐴) = 𝐴))
Theorem	mulreap 10359	A product with a real multiplier apart from zero is real iff the multiplicand is real. (Contributed by Jim Kingdon, 14-Jun-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ∧ 𝐵 # 0) → (𝐴 ∈ ℝ ↔ (𝐵 · 𝐴) ∈ ℝ))
Theorem	rere 10360	A real number equals its real part. One direction of Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by Paul Chapman, 7-Sep-2007.)
⊢ (𝐴 ∈ ℝ → (ℜ‘𝐴) = 𝐴)
Theorem	cjreb 10361	A number is real iff it equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by NM, 2-Jul-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ (𝐴 ∈ ℂ → (𝐴 ∈ ℝ ↔ (∗‘𝐴) = 𝐴))
Theorem	recj 10362	Real part of a complex conjugate. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ (𝐴 ∈ ℂ → (ℜ‘(∗‘𝐴)) = (ℜ‘𝐴))
Theorem	reneg 10363	Real part of negative. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ (𝐴 ∈ ℂ → (ℜ‘-𝐴) = -(ℜ‘𝐴))
Theorem	readd 10364	Real part distributes over addition. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (ℜ‘(𝐴 + 𝐵)) = ((ℜ‘𝐴) + (ℜ‘𝐵)))
Theorem	resub 10365	Real part distributes over subtraction. (Contributed by NM, 17-Mar-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (ℜ‘(𝐴 − 𝐵)) = ((ℜ‘𝐴) − (ℜ‘𝐵)))
Theorem	remullem 10366	Lemma for remul 10367, immul 10374, and cjmul 10380. (Contributed by NM, 28-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((ℜ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℜ‘𝐵)) − ((ℑ‘𝐴) · (ℑ‘𝐵))) ∧ (ℑ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℑ‘𝐵)) + ((ℑ‘𝐴) · (ℜ‘𝐵))) ∧ (∗‘(𝐴 · 𝐵)) = ((∗‘𝐴) · (∗‘𝐵))))
Theorem	remul 10367	Real part of a product. (Contributed by NM, 28-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (ℜ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℜ‘𝐵)) − ((ℑ‘𝐴) · (ℑ‘𝐵))))
Theorem	remul2 10368	Real part of a product. (Contributed by Mario Carneiro, 2-Aug-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℂ) → (ℜ‘(𝐴 · 𝐵)) = (𝐴 · (ℜ‘𝐵)))
Theorem	redivap 10369	Real part of a division. Related to remul2 10368. (Contributed by Jim Kingdon, 14-Jun-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ∧ 𝐵 # 0) → (ℜ‘(𝐴 / 𝐵)) = ((ℜ‘𝐴) / 𝐵))
Theorem	imcj 10370	Imaginary part of a complex conjugate. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ (𝐴 ∈ ℂ → (ℑ‘(∗‘𝐴)) = -(ℑ‘𝐴))
Theorem	imneg 10371	The imaginary part of a negative number. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ (𝐴 ∈ ℂ → (ℑ‘-𝐴) = -(ℑ‘𝐴))
Theorem	imadd 10372	Imaginary part distributes over addition. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (ℑ‘(𝐴 + 𝐵)) = ((ℑ‘𝐴) + (ℑ‘𝐵)))
Theorem	imsub 10373	Imaginary part distributes over subtraction. (Contributed by NM, 18-Mar-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (ℑ‘(𝐴 − 𝐵)) = ((ℑ‘𝐴) − (ℑ‘𝐵)))
Theorem	immul 10374	Imaginary part of a product. (Contributed by NM, 28-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (ℑ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℑ‘𝐵)) + ((ℑ‘𝐴) · (ℜ‘𝐵))))
Theorem	immul2 10375	Imaginary part of a product. (Contributed by Mario Carneiro, 2-Aug-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℂ) → (ℑ‘(𝐴 · 𝐵)) = (𝐴 · (ℑ‘𝐵)))
Theorem	imdivap 10376	Imaginary part of a division. Related to immul2 10375. (Contributed by Jim Kingdon, 14-Jun-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ∧ 𝐵 # 0) → (ℑ‘(𝐴 / 𝐵)) = ((ℑ‘𝐴) / 𝐵))
Theorem	cjre 10377	A real number equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by NM, 8-Oct-1999.)
⊢ (𝐴 ∈ ℝ → (∗‘𝐴) = 𝐴)
Theorem	cjcj 10378	The conjugate of the conjugate is the original complex number. Proposition 10-3.4(e) of [Gleason] p. 133. (Contributed by NM, 29-Jul-1999.) (Proof shortened by Mario Carneiro, 14-Jul-2014.)
⊢ (𝐴 ∈ ℂ → (∗‘(∗‘𝐴)) = 𝐴)
Theorem	cjadd 10379	Complex conjugate distributes over addition. Proposition 10-3.4(a) of [Gleason] p. 133. (Contributed by NM, 31-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (∗‘(𝐴 + 𝐵)) = ((∗‘𝐴) + (∗‘𝐵)))
Theorem	cjmul 10380	Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of [Gleason] p. 133. (Contributed by NM, 29-Jul-1999.) (Proof shortened by Mario Carneiro, 14-Jul-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (∗‘(𝐴 · 𝐵)) = ((∗‘𝐴) · (∗‘𝐵)))
Theorem	ipcnval 10381	Standard inner product on complex numbers. (Contributed by NM, 29-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (ℜ‘(𝐴 · (∗‘𝐵))) = (((ℜ‘𝐴) · (ℜ‘𝐵)) + ((ℑ‘𝐴) · (ℑ‘𝐵))))
Theorem	cjmulrcl 10382	A complex number times its conjugate is real. (Contributed by NM, 26-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ (𝐴 ∈ ℂ → (𝐴 · (∗‘𝐴)) ∈ ℝ)
Theorem	cjmulval 10383	A complex number times its conjugate. (Contributed by NM, 1-Feb-2007.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ (𝐴 ∈ ℂ → (𝐴 · (∗‘𝐴)) = (((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2)))
Theorem	cjmulge0 10384	A complex number times its conjugate is nonnegative. (Contributed by NM, 26-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ (𝐴 ∈ ℂ → 0 ≤ (𝐴 · (∗‘𝐴)))
Theorem	cjneg 10385	Complex conjugate of negative. (Contributed by NM, 27-Feb-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ (𝐴 ∈ ℂ → (∗‘-𝐴) = -(∗‘𝐴))
Theorem	addcj 10386	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 10387	Complex conjugate distributes over subtraction. (Contributed by NM, 28-Apr-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (∗‘(𝐴 − 𝐵)) = ((∗‘𝐴) − (∗‘𝐵)))
Theorem	cjexp 10388	Complex conjugate of positive integer exponentiation. (Contributed by NM, 7-Jun-2006.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (∗‘(𝐴↑𝑁)) = ((∗‘𝐴)↑𝑁))
Theorem	imval2 10389	The imaginary part of a number in terms of complex conjugate. (Contributed by NM, 30-Apr-2005.)
⊢ (𝐴 ∈ ℂ → (ℑ‘𝐴) = ((𝐴 − (∗‘𝐴)) / (2 · i)))
Theorem	re0 10390	The real part of zero. (Contributed by NM, 27-Jul-1999.)
⊢ (ℜ‘0) = 0
Theorem	im0 10391	The imaginary part of zero. (Contributed by NM, 27-Jul-1999.)
⊢ (ℑ‘0) = 0
Theorem	re1 10392	The real part of one. (Contributed by Scott Fenton, 9-Jun-2006.)
⊢ (ℜ‘1) = 1
Theorem	im1 10393	The imaginary part of one. (Contributed by Scott Fenton, 9-Jun-2006.)
⊢ (ℑ‘1) = 0
Theorem	rei 10394	The real part of i. (Contributed by Scott Fenton, 9-Jun-2006.)
⊢ (ℜ‘i) = 0
Theorem	imi 10395	The imaginary part of i. (Contributed by Scott Fenton, 9-Jun-2006.)
⊢ (ℑ‘i) = 1
Theorem	cj0 10396	The conjugate of zero. (Contributed by NM, 27-Jul-1999.)
⊢ (∗‘0) = 0
Theorem	cji 10397	The complex conjugate of the imaginary unit. (Contributed by NM, 26-Mar-2005.)
⊢ (∗‘i) = -i
Theorem	cjreim 10398	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 10399	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 10400	Complex conjugate is a one-to-one function. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Eric Schmidt, 2-Jul-2009.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((∗‘𝐴) = (∗‘𝐵) ↔ 𝐴 = 𝐵))