Theorem List for Intuitionistic Logic Explorer - 10701-10800 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | fihashss 10701 |
The size of a subset is less than or equal to the size of its superset.
(Contributed by Alexander van der Vekens, 14-Jul-2018.)
|
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → (♯‘𝐵) ≤ (♯‘𝐴)) |
|
Theorem | fiprsshashgt1 10702 |
The size of a superset of a proper unordered pair is greater than 1.
(Contributed by AV, 6-Feb-2021.)
|
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ 𝐶 ∈ Fin) → ({𝐴, 𝐵} ⊆ 𝐶 → 2 ≤ (♯‘𝐶))) |
|
Theorem | fihashssdif 10703 |
The size of the difference of a finite set and a finite subset is the
set's size minus the subset's. (Contributed by Jim Kingdon,
31-May-2022.)
|
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → (♯‘(𝐴 ∖ 𝐵)) = ((♯‘𝐴) − (♯‘𝐵))) |
|
Theorem | hashdifsn 10704 |
The size of the difference of a finite set and a singleton subset is the
set's size minus 1. (Contributed by Alexander van der Vekens,
6-Jan-2018.)
|
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝐴) → (♯‘(𝐴 ∖ {𝐵})) = ((♯‘𝐴) − 1)) |
|
Theorem | hashdifpr 10705 |
The size of the difference of a finite set and a proper ordered pair
subset is the set's size minus 2. (Contributed by AV, 16-Dec-2020.)
|
⊢ ((𝐴 ∈ Fin ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐵 ≠ 𝐶)) → (♯‘(𝐴 ∖ {𝐵, 𝐶})) = ((♯‘𝐴) − 2)) |
|
Theorem | hashfz 10706 |
Value of the numeric cardinality of a nonempty integer range.
(Contributed by Stefan O'Rear, 12-Sep-2014.) (Proof shortened by Mario
Carneiro, 15-Apr-2015.)
|
⊢ (𝐵 ∈ (ℤ≥‘𝐴) → (♯‘(𝐴...𝐵)) = ((𝐵 − 𝐴) + 1)) |
|
Theorem | hashfzo 10707 |
Cardinality of a half-open set of integers. (Contributed by Stefan
O'Rear, 15-Aug-2015.)
|
⊢ (𝐵 ∈ (ℤ≥‘𝐴) → (♯‘(𝐴..^𝐵)) = (𝐵 − 𝐴)) |
|
Theorem | hashfzo0 10708 |
Cardinality of a half-open set of integers based at zero. (Contributed by
Stefan O'Rear, 15-Aug-2015.)
|
⊢ (𝐵 ∈ ℕ0 →
(♯‘(0..^𝐵)) =
𝐵) |
|
Theorem | hashfzp1 10709 |
Value of the numeric cardinality of a (possibly empty) integer range.
(Contributed by AV, 19-Jun-2021.)
|
⊢ (𝐵 ∈ (ℤ≥‘𝐴) → (♯‘((𝐴 + 1)...𝐵)) = (𝐵 − 𝐴)) |
|
Theorem | hashfz0 10710 |
Value of the numeric cardinality of a nonempty range of nonnegative
integers. (Contributed by Alexander van der Vekens, 21-Jul-2018.)
|
⊢ (𝐵 ∈ ℕ0 →
(♯‘(0...𝐵)) =
(𝐵 + 1)) |
|
Theorem | hashxp 10711 |
The size of the Cartesian product of two finite sets is the product of
their sizes. (Contributed by Paul Chapman, 30-Nov-2012.)
|
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (♯‘(𝐴 × 𝐵)) = ((♯‘𝐴) · (♯‘𝐵))) |
|
Theorem | fimaxq 10712* |
A finite set of rational numbers has a maximum. (Contributed by Jim
Kingdon, 6-Sep-2022.)
|
⊢ ((𝐴 ⊆ ℚ ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) |
|
Theorem | resunimafz0 10713 |
The union of a restriction by an image over an open range of nonnegative
integers and a singleton of an ordered pair is a restriction by an image
over an interval of nonnegative integers. (Contributed by Mario
Carneiro, 8-Apr-2015.) (Revised by AV, 20-Feb-2021.)
|
⊢ (𝜑 → Fun 𝐼)
& ⊢ (𝜑 → 𝐹:(0..^(♯‘𝐹))⟶dom 𝐼)
& ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹)))
⇒ ⊢ (𝜑 → (𝐼 ↾ (𝐹 “ (0...𝑁))) = ((𝐼 ↾ (𝐹 “ (0..^𝑁))) ∪ {〈(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))〉})) |
|
Theorem | fnfz0hash 10714 |
The size of a function on a finite set of sequential nonnegative integers.
(Contributed by Alexander van der Vekens, 25-Jun-2018.)
|
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹 Fn (0...𝑁)) → (♯‘𝐹) = (𝑁 + 1)) |
|
Theorem | ffz0hash 10715 |
The size of a function on a finite set of sequential nonnegative integers
equals the upper bound of the sequence increased by 1. (Contributed by
Alexander van der Vekens, 15-Mar-2018.) (Proof shortened by AV,
11-Apr-2021.)
|
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹:(0...𝑁)⟶𝐵) → (♯‘𝐹) = (𝑁 + 1)) |
|
Theorem | ffzo0hash 10716 |
The size of a function on a half-open range of nonnegative integers.
(Contributed by Alexander van der Vekens, 25-Mar-2018.)
|
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹 Fn (0..^𝑁)) → (♯‘𝐹) = 𝑁) |
|
Theorem | fnfzo0hash 10717 |
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 10718* |
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 10719 |
Version of isorel 5760 for strictly increasing functions on the
reals.
(Contributed by Mario Carneiro, 6-Apr-2015.) (Revised by Mario Carneiro,
9-Sep-2015.)
|
⊢ ((𝐹 Isom < , < (𝐴, 𝐵) ∧ (𝐴 ⊆ ℝ* ∧ 𝐵 ⊆ ℝ*)
∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → (𝐶 ≤ 𝐷 ↔ (𝐹‘𝐶) ≤ (𝐹‘𝐷))) |
|
Theorem | zfz1isolemsplit 10720 |
Lemma for zfz1iso 10723. Removing one element from an integer
range.
(Contributed by Jim Kingdon, 8-Sep-2022.)
|
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑀 ∈ 𝑋) ⇒ ⊢ (𝜑 → (1...(♯‘𝑋)) =
((1...(♯‘(𝑋
∖ {𝑀}))) ∪
{(♯‘𝑋)})) |
|
Theorem | zfz1isolemiso 10721* |
Lemma for zfz1iso 10723. Adding one element to the order
isomorphism.
(Contributed by Jim Kingdon, 8-Sep-2022.)
|
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑋 ⊆ ℤ) & ⊢ (𝜑 → 𝑀 ∈ 𝑋)
& ⊢ (𝜑 → ∀𝑧 ∈ 𝑋 𝑧 ≤ 𝑀)
& ⊢ (𝜑 → 𝐺 Isom < , <
((1...(♯‘(𝑋
∖ {𝑀}))), (𝑋 ∖ {𝑀}))) & ⊢ (𝜑 → 𝐴 ∈ (1...(♯‘𝑋))) & ⊢ (𝜑 → 𝐵 ∈ (1...(♯‘𝑋)))
⇒ ⊢ (𝜑 → (𝐴 < 𝐵 ↔ ((𝐺 ∪ {〈(♯‘𝑋), 𝑀〉})‘𝐴) < ((𝐺 ∪ {〈(♯‘𝑋), 𝑀〉})‘𝐵))) |
|
Theorem | zfz1isolem1 10722* |
Lemma for zfz1iso 10723. 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 10723* |
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 | seq3coll 10724* |
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.) (Revised by Jim
Kingdon, 9-Apr-2023.)
|
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑆) → (𝑍 + 𝑘) = 𝑘)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑆) → (𝑘 + 𝑍) = 𝑘)
& ⊢ ((𝜑 ∧ (𝑘 ∈ 𝑆 ∧ 𝑛 ∈ 𝑆)) → (𝑘 + 𝑛) ∈ 𝑆)
& ⊢ (𝜑 → 𝑍 ∈ 𝑆)
& ⊢ (𝜑 → 𝐺 Isom < , <
((1...(♯‘𝐴)),
𝐴)) & ⊢ (𝜑 → 𝑁 ∈ (1...(♯‘𝐴))) & ⊢ (𝜑 → 𝐴 ⊆
(ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) ∈ 𝑆)
& ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1))
→ (𝐻‘𝑘) ∈ 𝑆)
& ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀...(𝐺‘(♯‘𝐴))) ∖ 𝐴)) → (𝐹‘𝑘) = 𝑍)
& ⊢ ((𝜑 ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (𝐻‘𝑛) = (𝐹‘(𝐺‘𝑛))) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘(𝐺‘𝑁)) = (seq1( + , 𝐻)‘𝑁)) |
|
4.7 Elementary real and complex
functions
|
|
4.7.1 The "shift" operation
|
|
Syntax | cshi 10725 |
Extend class notation with function shifter.
|
class shift |
|
Definition | df-shft 10726* |
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 10736 for its value. (Contributed by NM,
20-Jul-2005.)
|
⊢ shift = (𝑓 ∈ V, 𝑥 ∈ ℂ ↦ {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ ℂ ∧ (𝑦 − 𝑥)𝑓𝑧)}) |
|
Theorem | shftlem 10727* |
Two ways to write a shifted set (𝐵 + 𝐴). (Contributed by Mario
Carneiro, 3-Nov-2013.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ⊆ ℂ) → {𝑥 ∈ ℂ ∣ (𝑥 − 𝐴) ∈ 𝐵} = {𝑥 ∣ ∃𝑦 ∈ 𝐵 𝑥 = (𝑦 + 𝐴)}) |
|
Theorem | shftuz 10728* |
A shift of the upper integers. (Contributed by Mario Carneiro,
5-Nov-2013.)
|
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → {𝑥 ∈ ℂ ∣ (𝑥 − 𝐴) ∈
(ℤ≥‘𝐵)} = (ℤ≥‘(𝐵 + 𝐴))) |
|
Theorem | shftfvalg 10729* |
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 10730 |
Existence of the result of applying shift. (Contributed by Jim Kingdon,
15-Aug-2021.)
|
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐴 ∈ ℂ) → (𝐹 shift 𝐴) ∈ V) |
|
Theorem | shftfibg 10731 |
Value of a fiber of the relation 𝐹. (Contributed by Jim Kingdon,
15-Aug-2021.)
|
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift 𝐴) “ {𝐵}) = (𝐹 “ {(𝐵 − 𝐴)})) |
|
Theorem | shftfval 10732* |
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 10733* |
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 10734 |
Value of a fiber of the relation 𝐹. (Contributed by Mario
Carneiro, 4-Nov-2013.)
|
⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift 𝐴) “ {𝐵}) = (𝐹 “ {(𝐵 − 𝐴)})) |
|
Theorem | shftfn 10735* |
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 10736 |
Value of a sequence shifted by 𝐴. (Contributed by NM,
20-Jul-2005.) (Revised by Mario Carneiro, 4-Nov-2013.)
|
⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift 𝐴)‘𝐵) = (𝐹‘(𝐵 − 𝐴))) |
|
Theorem | shftval2 10737 |
Value of a sequence shifted by 𝐴 − 𝐵. (Contributed by NM,
20-Jul-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
|
⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐹 shift (𝐴 − 𝐵))‘(𝐴 + 𝐶)) = (𝐹‘(𝐵 + 𝐶))) |
|
Theorem | shftval3 10738 |
Value of a sequence shifted by 𝐴 − 𝐵. (Contributed by NM,
20-Jul-2005.)
|
⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift (𝐴 − 𝐵))‘𝐴) = (𝐹‘𝐵)) |
|
Theorem | shftval4 10739 |
Value of a sequence shifted by -𝐴. (Contributed by NM,
18-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
|
⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift -𝐴)‘𝐵) = (𝐹‘(𝐴 + 𝐵))) |
|
Theorem | shftval5 10740 |
Value of a shifted sequence. (Contributed by NM, 19-Aug-2005.)
(Revised by Mario Carneiro, 5-Nov-2013.)
|
⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift 𝐴)‘(𝐵 + 𝐴)) = (𝐹‘𝐵)) |
|
Theorem | shftf 10741* |
Functionality of a shifted sequence. (Contributed by NM, 19-Aug-2005.)
(Revised by Mario Carneiro, 5-Nov-2013.)
|
⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐴 ∈ ℂ) → (𝐹 shift 𝐴):{𝑥 ∈ ℂ ∣ (𝑥 − 𝐴) ∈ 𝐵}⟶𝐶) |
|
Theorem | 2shfti 10742 |
Composite shift operations. (Contributed by NM, 19-Aug-2005.) (Revised
by Mario Carneiro, 5-Nov-2013.)
|
⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift 𝐴) shift 𝐵) = (𝐹 shift (𝐴 + 𝐵))) |
|
Theorem | shftidt2 10743 |
Identity law for the shift operation. (Contributed by Mario Carneiro,
5-Nov-2013.)
|
⊢ 𝐹 ∈ V ⇒ ⊢ (𝐹 shift 0) = (𝐹 ↾ ℂ) |
|
Theorem | shftidt 10744 |
Identity law for the shift operation. (Contributed by NM, 19-Aug-2005.)
(Revised by Mario Carneiro, 5-Nov-2013.)
|
⊢ 𝐹 ∈ V ⇒ ⊢ (𝐴 ∈ ℂ → ((𝐹 shift 0)‘𝐴) = (𝐹‘𝐴)) |
|
Theorem | shftcan1 10745 |
Cancellation law for the shift operation. (Contributed by NM,
4-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
|
⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐹 shift 𝐴) shift -𝐴)‘𝐵) = (𝐹‘𝐵)) |
|
Theorem | shftcan2 10746 |
Cancellation law for the shift operation. (Contributed by NM,
4-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
|
⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐹 shift -𝐴) shift 𝐴)‘𝐵) = (𝐹‘𝐵)) |
|
Theorem | shftvalg 10747 |
Value of a sequence shifted by 𝐴. (Contributed by Scott Fenton,
16-Dec-2017.)
|
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift 𝐴)‘𝐵) = (𝐹‘(𝐵 − 𝐴))) |
|
Theorem | shftval4g 10748 |
Value of a sequence shifted by -𝐴. (Contributed by Jim Kingdon,
19-Aug-2021.)
|
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift -𝐴)‘𝐵) = (𝐹‘(𝐴 + 𝐵))) |
|
Theorem | seq3shft 10749* |
Shifting the index set of a sequence. (Contributed by NM, 17-Mar-2005.)
(Revised by Jim Kingdon, 17-Oct-2022.)
|
⊢ (𝜑 → 𝐹 ∈ 𝑉)
& ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 − 𝑁))) → (𝐹‘𝑥) ∈ 𝑆)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) ⇒ ⊢ (𝜑 → seq𝑀( + , (𝐹 shift 𝑁)) = (seq(𝑀 − 𝑁)( + , 𝐹) shift 𝑁)) |
|
4.7.2 Real and imaginary parts;
conjugate
|
|
Syntax | ccj 10750 |
Extend class notation to include complex conjugate function.
|
class ∗ |
|
Syntax | cre 10751 |
Extend class notation to include real part of a complex number.
|
class ℜ |
|
Syntax | cim 10752 |
Extend class notation to include imaginary part of a complex number.
|
class ℑ |
|
Definition | df-cj 10753* |
Define the complex conjugate function. See cjcli 10824 for its closure and
cjval 10756 for its value. (Contributed by NM,
9-May-1999.) (Revised by
Mario Carneiro, 6-Nov-2013.)
|
⊢ ∗ = (𝑥 ∈ ℂ ↦ (℩𝑦 ∈ ℂ ((𝑥 + 𝑦) ∈ ℝ ∧ (i · (𝑥 − 𝑦)) ∈ ℝ))) |
|
Definition | df-re 10754 |
Define a function whose value is the real part of a complex number. See
reval 10760 for its value, recli 10822 for its closure, and replim 10770 for its use
in decomposing a complex number. (Contributed by NM, 9-May-1999.)
|
⊢ ℜ = (𝑥 ∈ ℂ ↦ ((𝑥 + (∗‘𝑥)) / 2)) |
|
Definition | df-im 10755 |
Define a function whose value is the imaginary part of a complex number.
See imval 10761 for its value, imcli 10823 for its closure, and replim 10770 for its
use in decomposing a complex number. (Contributed by NM,
9-May-1999.)
|
⊢ ℑ = (𝑥 ∈ ℂ ↦ (ℜ‘(𝑥 / i))) |
|
Theorem | cjval 10756* |
The value of the conjugate of a complex number. (Contributed by Mario
Carneiro, 6-Nov-2013.)
|
⊢ (𝐴 ∈ ℂ →
(∗‘𝐴) =
(℩𝑥 ∈
ℂ ((𝐴 + 𝑥) ∈ ℝ ∧ (i
· (𝐴 − 𝑥)) ∈
ℝ))) |
|
Theorem | cjth 10757 |
The defining property of the complex conjugate. (Contributed by Mario
Carneiro, 6-Nov-2013.)
|
⊢ (𝐴 ∈ ℂ → ((𝐴 + (∗‘𝐴)) ∈ ℝ ∧ (i · (𝐴 − (∗‘𝐴))) ∈
ℝ)) |
|
Theorem | cjf 10758 |
Domain and codomain of the conjugate function. (Contributed by Mario
Carneiro, 6-Nov-2013.)
|
⊢
∗:ℂ⟶ℂ |
|
Theorem | cjcl 10759 |
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 10760 |
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 10761 |
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 10762 |
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 10763 |
The real part of a complex number in terms of the imaginary part
function. (Contributed by Mario Carneiro, 31-Mar-2015.)
|
⊢ (𝐴 ∈ ℂ → (ℜ‘𝐴) = (ℑ‘(i ·
𝐴))) |
|
Theorem | recl 10764 |
The real part of a complex number is real. (Contributed by NM,
9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
|
⊢ (𝐴 ∈ ℂ → (ℜ‘𝐴) ∈
ℝ) |
|
Theorem | imcl 10765 |
The imaginary part of a complex number is real. (Contributed by NM,
9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
|
⊢ (𝐴 ∈ ℂ → (ℑ‘𝐴) ∈
ℝ) |
|
Theorem | ref 10766 |
Domain and codomain of the real part function. (Contributed by Paul
Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 6-Nov-2013.)
|
⊢
ℜ:ℂ⟶ℝ |
|
Theorem | imf 10767 |
Domain and codomain of the imaginary part function. (Contributed by
Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 6-Nov-2013.)
|
⊢
ℑ:ℂ⟶ℝ |
|
Theorem | crre 10768 |
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 10769 |
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 10770 |
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 10771 |
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 10772 |
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 10773 |
A number is real iff its imaginary part is 0. (Contributed by NM,
26-Sep-2005.)
|
⊢ (𝐴 ∈ ℂ → (𝐴 ∈ ℝ ↔ (ℑ‘𝐴) = 0)) |
|
Theorem | rereb 10774 |
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 10775 |
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 10776 |
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 10777 |
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 10778 |
Real part of a complex conjugate. (Contributed by Mario Carneiro,
14-Jul-2014.)
|
⊢ (𝐴 ∈ ℂ →
(ℜ‘(∗‘𝐴)) = (ℜ‘𝐴)) |
|
Theorem | reneg 10779 |
Real part of negative. (Contributed by NM, 17-Mar-2005.) (Revised by
Mario Carneiro, 14-Jul-2014.)
|
⊢ (𝐴 ∈ ℂ → (ℜ‘-𝐴) = -(ℜ‘𝐴)) |
|
Theorem | readd 10780 |
Real part distributes over addition. (Contributed by NM, 17-Mar-2005.)
(Revised by Mario Carneiro, 14-Jul-2014.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(ℜ‘(𝐴 + 𝐵)) = ((ℜ‘𝐴) + (ℜ‘𝐵))) |
|
Theorem | resub 10781 |
Real part distributes over subtraction. (Contributed by NM,
17-Mar-2005.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(ℜ‘(𝐴 −
𝐵)) = ((ℜ‘𝐴) − (ℜ‘𝐵))) |
|
Theorem | remullem 10782 |
Lemma for remul 10783, immul 10790, and cjmul 10796. (Contributed by NM,
28-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((ℜ‘(𝐴 ·
𝐵)) =
(((ℜ‘𝐴)
· (ℜ‘𝐵))
− ((ℑ‘𝐴)
· (ℑ‘𝐵))) ∧ (ℑ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℑ‘𝐵)) + ((ℑ‘𝐴) · (ℜ‘𝐵))) ∧ (∗‘(𝐴 · 𝐵)) = ((∗‘𝐴) · (∗‘𝐵)))) |
|
Theorem | remul 10783 |
Real part of a product. (Contributed by NM, 28-Jul-1999.) (Revised by
Mario Carneiro, 14-Jul-2014.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(ℜ‘(𝐴 ·
𝐵)) =
(((ℜ‘𝐴)
· (ℜ‘𝐵))
− ((ℑ‘𝐴)
· (ℑ‘𝐵)))) |
|
Theorem | remul2 10784 |
Real part of a product. (Contributed by Mario Carneiro, 2-Aug-2014.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℂ) →
(ℜ‘(𝐴 ·
𝐵)) = (𝐴 · (ℜ‘𝐵))) |
|
Theorem | redivap 10785 |
Real part of a division. Related to remul2 10784. (Contributed by Jim
Kingdon, 14-Jun-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ∧ 𝐵 # 0) → (ℜ‘(𝐴 / 𝐵)) = ((ℜ‘𝐴) / 𝐵)) |
|
Theorem | imcj 10786 |
Imaginary part of a complex conjugate. (Contributed by NM, 18-Mar-2005.)
(Revised by Mario Carneiro, 14-Jul-2014.)
|
⊢ (𝐴 ∈ ℂ →
(ℑ‘(∗‘𝐴)) = -(ℑ‘𝐴)) |
|
Theorem | imneg 10787 |
The imaginary part of a negative number. (Contributed by NM,
18-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
|
⊢ (𝐴 ∈ ℂ →
(ℑ‘-𝐴) =
-(ℑ‘𝐴)) |
|
Theorem | imadd 10788 |
Imaginary part distributes over addition. (Contributed by NM,
18-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(ℑ‘(𝐴 + 𝐵)) = ((ℑ‘𝐴) + (ℑ‘𝐵))) |
|
Theorem | imsub 10789 |
Imaginary part distributes over subtraction. (Contributed by NM,
18-Mar-2005.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(ℑ‘(𝐴 −
𝐵)) =
((ℑ‘𝐴) −
(ℑ‘𝐵))) |
|
Theorem | immul 10790 |
Imaginary part of a product. (Contributed by NM, 28-Jul-1999.) (Revised
by Mario Carneiro, 14-Jul-2014.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(ℑ‘(𝐴 ·
𝐵)) =
(((ℜ‘𝐴)
· (ℑ‘𝐵)) + ((ℑ‘𝐴) · (ℜ‘𝐵)))) |
|
Theorem | immul2 10791 |
Imaginary part of a product. (Contributed by Mario Carneiro,
2-Aug-2014.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℂ) →
(ℑ‘(𝐴 ·
𝐵)) = (𝐴 · (ℑ‘𝐵))) |
|
Theorem | imdivap 10792 |
Imaginary part of a division. Related to immul2 10791. (Contributed by Jim
Kingdon, 14-Jun-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ∧ 𝐵 # 0) → (ℑ‘(𝐴 / 𝐵)) = ((ℑ‘𝐴) / 𝐵)) |
|
Theorem | cjre 10793 |
A real number equals its complex conjugate. Proposition 10-3.4(f) of
[Gleason] p. 133. (Contributed by NM,
8-Oct-1999.)
|
⊢ (𝐴 ∈ ℝ →
(∗‘𝐴) = 𝐴) |
|
Theorem | cjcj 10794 |
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 10795 |
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 10796 |
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 10797 |
Standard inner product on complex numbers. (Contributed by NM,
29-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(ℜ‘(𝐴 ·
(∗‘𝐵))) =
(((ℜ‘𝐴)
· (ℜ‘𝐵))
+ ((ℑ‘𝐴)
· (ℑ‘𝐵)))) |
|
Theorem | cjmulrcl 10798 |
A complex number times its conjugate is real. (Contributed by NM,
26-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
|
⊢ (𝐴 ∈ ℂ → (𝐴 · (∗‘𝐴)) ∈ ℝ) |
|
Theorem | cjmulval 10799 |
A complex number times its conjugate. (Contributed by NM, 1-Feb-2007.)
(Revised by Mario Carneiro, 14-Jul-2014.)
|
⊢ (𝐴 ∈ ℂ → (𝐴 · (∗‘𝐴)) = (((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2))) |
|
Theorem | cjmulge0 10800 |
A complex number times its conjugate is nonnegative. (Contributed by NM,
26-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
|
⊢ (𝐴 ∈ ℂ → 0 ≤ (𝐴 · (∗‘𝐴))) |