HomeHome Intuitionistic Logic Explorer
Theorem List (p. 109 of 149)
< Previous  Next >
Bad symbols? Try the
GIF version.

Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 10801-10900   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremhashfzo 10801 Cardinality of a half-open set of integers. (Contributed by Stefan O'Rear, 15-Aug-2015.)
(𝐡 ∈ (β„€β‰₯β€˜π΄) β†’ (β™―β€˜(𝐴..^𝐡)) = (𝐡 βˆ’ 𝐴))
 
Theoremhashfzo0 10802 Cardinality of a half-open set of integers based at zero. (Contributed by Stefan O'Rear, 15-Aug-2015.)
(𝐡 ∈ β„•0 β†’ (β™―β€˜(0..^𝐡)) = 𝐡)
 
Theoremhashfzp1 10803 Value of the numeric cardinality of a (possibly empty) integer range. (Contributed by AV, 19-Jun-2021.)
(𝐡 ∈ (β„€β‰₯β€˜π΄) β†’ (β™―β€˜((𝐴 + 1)...𝐡)) = (𝐡 βˆ’ 𝐴))
 
Theoremhashfz0 10804 Value of the numeric cardinality of a nonempty range of nonnegative integers. (Contributed by Alexander van der Vekens, 21-Jul-2018.)
(𝐡 ∈ β„•0 β†’ (β™―β€˜(0...𝐡)) = (𝐡 + 1))
 
Theoremhashxp 10805 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) β†’ (β™―β€˜(𝐴 Γ— 𝐡)) = ((β™―β€˜π΄) Β· (β™―β€˜π΅)))
 
Theoremfimaxq 10806* A finite set of rational numbers has a maximum. (Contributed by Jim Kingdon, 6-Sep-2022.)
((𝐴 βŠ† β„š ∧ 𝐴 ∈ Fin ∧ 𝐴 β‰  βˆ…) β†’ βˆƒπ‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 𝑦 ≀ π‘₯)
 
Theoremfiubm 10807* Lemma for fiubz 10808 and fiubnn 10809. A general form of those theorems. (Contributed by Jim Kingdon, 29-Oct-2024.)
(πœ‘ β†’ 𝐴 βŠ† 𝐡)    &   (πœ‘ β†’ 𝐡 βŠ† β„š)    &   (πœ‘ β†’ 𝐢 ∈ 𝐡)    &   (πœ‘ β†’ 𝐴 ∈ Fin)    β‡’   (πœ‘ β†’ βˆƒπ‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐴 𝑦 ≀ π‘₯)
 
Theoremfiubz 10808* A finite set of integers has an upper bound which is an integer. (Contributed by Jim Kingdon, 29-Oct-2024.)
((𝐴 βŠ† β„€ ∧ 𝐴 ∈ Fin) β†’ βˆƒπ‘₯ ∈ β„€ βˆ€π‘¦ ∈ 𝐴 𝑦 ≀ π‘₯)
 
Theoremfiubnn 10809* A finite set of natural numbers has an upper bound which is a a natural number. (Contributed by Jim Kingdon, 29-Oct-2024.)
((𝐴 βŠ† β„• ∧ 𝐴 ∈ Fin) β†’ βˆƒπ‘₯ ∈ β„• βˆ€π‘¦ ∈ 𝐴 𝑦 ≀ π‘₯)
 
Theoremresunimafz0 10810 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..^𝑁))) βˆͺ {⟨(πΉβ€˜π‘), (πΌβ€˜(πΉβ€˜π‘))⟩}))
 
Theoremfnfz0hash 10811 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))
 
Theoremffz0hash 10812 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))
 
Theoremffzo0hash 10813 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..^𝑁)) β†’ (β™―β€˜πΉ) = 𝑁)
 
Theoremfnfzo0hash 10814 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..^𝑁)⟢𝐡) β†’ (β™―β€˜πΉ) = 𝑁)
 
Theoremhashfacen 10815* The number of bijections between two sets is a cardinal invariant. (Contributed by Mario Carneiro, 21-Jan-2015.)
((𝐴 β‰ˆ 𝐡 ∧ 𝐢 β‰ˆ 𝐷) β†’ {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐢} β‰ˆ {𝑓 ∣ 𝑓:𝐡–1-1-onto→𝐷})
 
Theoremleisorel 10816 Version of isorel 5808 for strictly increasing functions on the reals. (Contributed by Mario Carneiro, 6-Apr-2015.) (Revised by Mario Carneiro, 9-Sep-2015.)
((𝐹 Isom < , < (𝐴, 𝐡) ∧ (𝐴 βŠ† ℝ* ∧ 𝐡 βŠ† ℝ*) ∧ (𝐢 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) β†’ (𝐢 ≀ 𝐷 ↔ (πΉβ€˜πΆ) ≀ (πΉβ€˜π·)))
 
Theoremzfz1isolemsplit 10817 Lemma for zfz1iso 10820. Removing one element from an integer range. (Contributed by Jim Kingdon, 8-Sep-2022.)
(πœ‘ β†’ 𝑋 ∈ Fin)    &   (πœ‘ β†’ 𝑀 ∈ 𝑋)    β‡’   (πœ‘ β†’ (1...(β™―β€˜π‘‹)) = ((1...(β™―β€˜(𝑋 βˆ– {𝑀}))) βˆͺ {(β™―β€˜π‘‹)}))
 
Theoremzfz1isolemiso 10818* Lemma for zfz1iso 10820. Adding one element to the order isomorphism. (Contributed by Jim Kingdon, 8-Sep-2022.)
(πœ‘ β†’ 𝑋 ∈ Fin)    &   (πœ‘ β†’ 𝑋 βŠ† β„€)    &   (πœ‘ β†’ 𝑀 ∈ 𝑋)    &   (πœ‘ β†’ βˆ€π‘§ ∈ 𝑋 𝑧 ≀ 𝑀)    &   (πœ‘ β†’ 𝐺 Isom < , < ((1...(β™―β€˜(𝑋 βˆ– {𝑀}))), (𝑋 βˆ– {𝑀})))    &   (πœ‘ β†’ 𝐴 ∈ (1...(β™―β€˜π‘‹)))    &   (πœ‘ β†’ 𝐡 ∈ (1...(β™―β€˜π‘‹)))    β‡’   (πœ‘ β†’ (𝐴 < 𝐡 ↔ ((𝐺 βˆͺ {⟨(β™―β€˜π‘‹), π‘€βŸ©})β€˜π΄) < ((𝐺 βˆͺ {⟨(β™―β€˜π‘‹), π‘€βŸ©})β€˜π΅)))
 
Theoremzfz1isolem1 10819* Lemma for zfz1iso 10820. 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...(β™―β€˜π‘‹)), 𝑋))
 
Theoremzfz1iso 10820* 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...(β™―β€˜π΄)), 𝐴))
 
Theoremseq3coll 10821* 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
 
Syntaxcshi 10822 Extend class notation with function shifter.
class shift
 
Definitiondf-shft 10823* 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 10833 for its value. (Contributed by NM, 20-Jul-2005.)
shift = (𝑓 ∈ V, π‘₯ ∈ β„‚ ↦ {βŸ¨π‘¦, π‘§βŸ© ∣ (𝑦 ∈ β„‚ ∧ (𝑦 βˆ’ π‘₯)𝑓𝑧)})
 
Theoremshftlem 10824* Two ways to write a shifted set (𝐡 + 𝐴). (Contributed by Mario Carneiro, 3-Nov-2013.)
((𝐴 ∈ β„‚ ∧ 𝐡 βŠ† β„‚) β†’ {π‘₯ ∈ β„‚ ∣ (π‘₯ βˆ’ 𝐴) ∈ 𝐡} = {π‘₯ ∣ βˆƒπ‘¦ ∈ 𝐡 π‘₯ = (𝑦 + 𝐴)})
 
Theoremshftuz 10825* A shift of the upper integers. (Contributed by Mario Carneiro, 5-Nov-2013.)
((𝐴 ∈ β„€ ∧ 𝐡 ∈ β„€) β†’ {π‘₯ ∈ β„‚ ∣ (π‘₯ βˆ’ 𝐴) ∈ (β„€β‰₯β€˜π΅)} = (β„€β‰₯β€˜(𝐡 + 𝐴)))
 
Theoremshftfvalg 10826* 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 𝐴) = {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ β„‚ ∧ (π‘₯ βˆ’ 𝐴)𝐹𝑦)})
 
Theoremovshftex 10827 Existence of the result of applying shift. (Contributed by Jim Kingdon, 15-Aug-2021.)
((𝐹 ∈ 𝑉 ∧ 𝐴 ∈ β„‚) β†’ (𝐹 shift 𝐴) ∈ V)
 
Theoremshftfibg 10828 Value of a fiber of the relation 𝐹. (Contributed by Jim Kingdon, 15-Aug-2021.)
((𝐹 ∈ 𝑉 ∧ 𝐴 ∈ β„‚ ∧ 𝐡 ∈ β„‚) β†’ ((𝐹 shift 𝐴) β€œ {𝐡}) = (𝐹 β€œ {(𝐡 βˆ’ 𝐴)}))
 
Theoremshftfval 10829* 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 𝐴) = {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ β„‚ ∧ (π‘₯ βˆ’ 𝐴)𝐹𝑦)})
 
Theoremshftdm 10830* 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 𝐹})
 
Theoremshftfib 10831 Value of a fiber of the relation 𝐹. (Contributed by Mario Carneiro, 4-Nov-2013.)
𝐹 ∈ V    β‡’   ((𝐴 ∈ β„‚ ∧ 𝐡 ∈ β„‚) β†’ ((𝐹 shift 𝐴) β€œ {𝐡}) = (𝐹 β€œ {(𝐡 βˆ’ 𝐴)}))
 
Theoremshftfn 10832* 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 {π‘₯ ∈ β„‚ ∣ (π‘₯ βˆ’ 𝐴) ∈ 𝐡})
 
Theoremshftval 10833 Value of a sequence shifted by 𝐴. (Contributed by NM, 20-Jul-2005.) (Revised by Mario Carneiro, 4-Nov-2013.)
𝐹 ∈ V    β‡’   ((𝐴 ∈ β„‚ ∧ 𝐡 ∈ β„‚) β†’ ((𝐹 shift 𝐴)β€˜π΅) = (πΉβ€˜(𝐡 βˆ’ 𝐴)))
 
Theoremshftval2 10834 Value of a sequence shifted by 𝐴 βˆ’ 𝐡. (Contributed by NM, 20-Jul-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
𝐹 ∈ V    β‡’   ((𝐴 ∈ β„‚ ∧ 𝐡 ∈ β„‚ ∧ 𝐢 ∈ β„‚) β†’ ((𝐹 shift (𝐴 βˆ’ 𝐡))β€˜(𝐴 + 𝐢)) = (πΉβ€˜(𝐡 + 𝐢)))
 
Theoremshftval3 10835 Value of a sequence shifted by 𝐴 βˆ’ 𝐡. (Contributed by NM, 20-Jul-2005.)
𝐹 ∈ V    β‡’   ((𝐴 ∈ β„‚ ∧ 𝐡 ∈ β„‚) β†’ ((𝐹 shift (𝐴 βˆ’ 𝐡))β€˜π΄) = (πΉβ€˜π΅))
 
Theoremshftval4 10836 Value of a sequence shifted by -𝐴. (Contributed by NM, 18-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
𝐹 ∈ V    β‡’   ((𝐴 ∈ β„‚ ∧ 𝐡 ∈ β„‚) β†’ ((𝐹 shift -𝐴)β€˜π΅) = (πΉβ€˜(𝐴 + 𝐡)))
 
Theoremshftval5 10837 Value of a shifted sequence. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
𝐹 ∈ V    β‡’   ((𝐴 ∈ β„‚ ∧ 𝐡 ∈ β„‚) β†’ ((𝐹 shift 𝐴)β€˜(𝐡 + 𝐴)) = (πΉβ€˜π΅))
 
Theoremshftf 10838* Functionality of a shifted sequence. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
𝐹 ∈ V    β‡’   ((𝐹:𝐡⟢𝐢 ∧ 𝐴 ∈ β„‚) β†’ (𝐹 shift 𝐴):{π‘₯ ∈ β„‚ ∣ (π‘₯ βˆ’ 𝐴) ∈ 𝐡}⟢𝐢)
 
Theorem2shfti 10839 Composite shift operations. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
𝐹 ∈ V    β‡’   ((𝐴 ∈ β„‚ ∧ 𝐡 ∈ β„‚) β†’ ((𝐹 shift 𝐴) shift 𝐡) = (𝐹 shift (𝐴 + 𝐡)))
 
Theoremshftidt2 10840 Identity law for the shift operation. (Contributed by Mario Carneiro, 5-Nov-2013.)
𝐹 ∈ V    β‡’   (𝐹 shift 0) = (𝐹 β†Ύ β„‚)
 
Theoremshftidt 10841 Identity law for the shift operation. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
𝐹 ∈ V    β‡’   (𝐴 ∈ β„‚ β†’ ((𝐹 shift 0)β€˜π΄) = (πΉβ€˜π΄))
 
Theoremshftcan1 10842 Cancellation law for the shift operation. (Contributed by NM, 4-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
𝐹 ∈ V    β‡’   ((𝐴 ∈ β„‚ ∧ 𝐡 ∈ β„‚) β†’ (((𝐹 shift 𝐴) shift -𝐴)β€˜π΅) = (πΉβ€˜π΅))
 
Theoremshftcan2 10843 Cancellation law for the shift operation. (Contributed by NM, 4-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
𝐹 ∈ V    β‡’   ((𝐴 ∈ β„‚ ∧ 𝐡 ∈ β„‚) β†’ (((𝐹 shift -𝐴) shift 𝐴)β€˜π΅) = (πΉβ€˜π΅))
 
Theoremshftvalg 10844 Value of a sequence shifted by 𝐴. (Contributed by Scott Fenton, 16-Dec-2017.)
((𝐹 ∈ 𝑉 ∧ 𝐴 ∈ β„‚ ∧ 𝐡 ∈ β„‚) β†’ ((𝐹 shift 𝐴)β€˜π΅) = (πΉβ€˜(𝐡 βˆ’ 𝐴)))
 
Theoremshftval4g 10845 Value of a sequence shifted by -𝐴. (Contributed by Jim Kingdon, 19-Aug-2021.)
((𝐹 ∈ 𝑉 ∧ 𝐴 ∈ β„‚ ∧ 𝐡 ∈ β„‚) β†’ ((𝐹 shift -𝐴)β€˜π΅) = (πΉβ€˜(𝐴 + 𝐡)))
 
Theoremseq3shft 10846* 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
 
Syntaxccj 10847 Extend class notation to include complex conjugate function.
class βˆ—
 
Syntaxcre 10848 Extend class notation to include real part of a complex number.
class β„œ
 
Syntaxcim 10849 Extend class notation to include imaginary part of a complex number.
class β„‘
 
Definitiondf-cj 10850* Define the complex conjugate function. See cjcli 10921 for its closure and cjval 10853 for its value. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
βˆ— = (π‘₯ ∈ β„‚ ↦ (℩𝑦 ∈ β„‚ ((π‘₯ + 𝑦) ∈ ℝ ∧ (i Β· (π‘₯ βˆ’ 𝑦)) ∈ ℝ)))
 
Definitiondf-re 10851 Define a function whose value is the real part of a complex number. See reval 10857 for its value, recli 10919 for its closure, and replim 10867 for its use in decomposing a complex number. (Contributed by NM, 9-May-1999.)
β„œ = (π‘₯ ∈ β„‚ ↦ ((π‘₯ + (βˆ—β€˜π‘₯)) / 2))
 
Definitiondf-im 10852 Define a function whose value is the imaginary part of a complex number. See imval 10858 for its value, imcli 10920 for its closure, and replim 10867 for its use in decomposing a complex number. (Contributed by NM, 9-May-1999.)
β„‘ = (π‘₯ ∈ β„‚ ↦ (β„œβ€˜(π‘₯ / i)))
 
Theoremcjval 10853* The value of the conjugate of a complex number. (Contributed by Mario Carneiro, 6-Nov-2013.)
(𝐴 ∈ β„‚ β†’ (βˆ—β€˜π΄) = (β„©π‘₯ ∈ β„‚ ((𝐴 + π‘₯) ∈ ℝ ∧ (i Β· (𝐴 βˆ’ π‘₯)) ∈ ℝ)))
 
Theoremcjth 10854 The defining property of the complex conjugate. (Contributed by Mario Carneiro, 6-Nov-2013.)
(𝐴 ∈ β„‚ β†’ ((𝐴 + (βˆ—β€˜π΄)) ∈ ℝ ∧ (i Β· (𝐴 βˆ’ (βˆ—β€˜π΄))) ∈ ℝ))
 
Theoremcjf 10855 Domain and codomain of the conjugate function. (Contributed by Mario Carneiro, 6-Nov-2013.)
βˆ—:β„‚βŸΆβ„‚
 
Theoremcjcl 10856 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.)
(𝐴 ∈ β„‚ β†’ (βˆ—β€˜π΄) ∈ β„‚)
 
Theoremreval 10857 The value of the real part of a complex number. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
(𝐴 ∈ β„‚ β†’ (β„œβ€˜π΄) = ((𝐴 + (βˆ—β€˜π΄)) / 2))
 
Theoremimval 10858 The value of the imaginary part of a complex number. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
(𝐴 ∈ β„‚ β†’ (β„‘β€˜π΄) = (β„œβ€˜(𝐴 / i)))
 
Theoremimre 10859 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 Β· 𝐴)))
 
Theoremreim 10860 The real part of a complex number in terms of the imaginary part function. (Contributed by Mario Carneiro, 31-Mar-2015.)
(𝐴 ∈ β„‚ β†’ (β„œβ€˜π΄) = (β„‘β€˜(i Β· 𝐴)))
 
Theoremrecl 10861 The real part of a complex number is real. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
(𝐴 ∈ β„‚ β†’ (β„œβ€˜π΄) ∈ ℝ)
 
Theoremimcl 10862 The imaginary part of a complex number is real. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
(𝐴 ∈ β„‚ β†’ (β„‘β€˜π΄) ∈ ℝ)
 
Theoremref 10863 Domain and codomain of the real part function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 6-Nov-2013.)
β„œ:β„‚βŸΆβ„
 
Theoremimf 10864 Domain and codomain of the imaginary part function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 6-Nov-2013.)
β„‘:β„‚βŸΆβ„
 
Theoremcrre 10865 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 Β· 𝐡))) = 𝐴)
 
Theoremcrim 10866 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 Β· 𝐡))) = 𝐡)
 
Theoremreplim 10867 Reconstruct a complex number from its real and imaginary parts. (Contributed by NM, 10-May-1999.) (Revised by Mario Carneiro, 7-Nov-2013.)
(𝐴 ∈ β„‚ β†’ 𝐴 = ((β„œβ€˜π΄) + (i Β· (β„‘β€˜π΄))))
 
Theoremremim 10868 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 Β· (β„‘β€˜π΄))))
 
Theoremreim0 10869 The imaginary part of a real number is 0. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 7-Nov-2013.)
(𝐴 ∈ ℝ β†’ (β„‘β€˜π΄) = 0)
 
Theoremreim0b 10870 A number is real iff its imaginary part is 0. (Contributed by NM, 26-Sep-2005.)
(𝐴 ∈ β„‚ β†’ (𝐴 ∈ ℝ ↔ (β„‘β€˜π΄) = 0))
 
Theoremrereb 10871 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.)
(𝐴 ∈ β„‚ β†’ (𝐴 ∈ ℝ ↔ (β„œβ€˜π΄) = 𝐴))
 
Theoremmulreap 10872 A product with a real multiplier apart from zero is real iff the multiplicand is real. (Contributed by Jim Kingdon, 14-Jun-2020.)
((𝐴 ∈ β„‚ ∧ 𝐡 ∈ ℝ ∧ 𝐡 # 0) β†’ (𝐴 ∈ ℝ ↔ (𝐡 Β· 𝐴) ∈ ℝ))
 
Theoremrere 10873 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.)
(𝐴 ∈ ℝ β†’ (β„œβ€˜π΄) = 𝐴)
 
Theoremcjreb 10874 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.)
(𝐴 ∈ β„‚ β†’ (𝐴 ∈ ℝ ↔ (βˆ—β€˜π΄) = 𝐴))
 
Theoremrecj 10875 Real part of a complex conjugate. (Contributed by Mario Carneiro, 14-Jul-2014.)
(𝐴 ∈ β„‚ β†’ (β„œβ€˜(βˆ—β€˜π΄)) = (β„œβ€˜π΄))
 
Theoremreneg 10876 Real part of negative. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
(𝐴 ∈ β„‚ β†’ (β„œβ€˜-𝐴) = -(β„œβ€˜π΄))
 
Theoremreadd 10877 Real part distributes over addition. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
((𝐴 ∈ β„‚ ∧ 𝐡 ∈ β„‚) β†’ (β„œβ€˜(𝐴 + 𝐡)) = ((β„œβ€˜π΄) + (β„œβ€˜π΅)))
 
Theoremresub 10878 Real part distributes over subtraction. (Contributed by NM, 17-Mar-2005.)
((𝐴 ∈ β„‚ ∧ 𝐡 ∈ β„‚) β†’ (β„œβ€˜(𝐴 βˆ’ 𝐡)) = ((β„œβ€˜π΄) βˆ’ (β„œβ€˜π΅)))
 
Theoremremullem 10879 Lemma for remul 10880, immul 10887, and cjmul 10893. (Contributed by NM, 28-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.)
((𝐴 ∈ β„‚ ∧ 𝐡 ∈ β„‚) β†’ ((β„œβ€˜(𝐴 Β· 𝐡)) = (((β„œβ€˜π΄) Β· (β„œβ€˜π΅)) βˆ’ ((β„‘β€˜π΄) Β· (β„‘β€˜π΅))) ∧ (β„‘β€˜(𝐴 Β· 𝐡)) = (((β„œβ€˜π΄) Β· (β„‘β€˜π΅)) + ((β„‘β€˜π΄) Β· (β„œβ€˜π΅))) ∧ (βˆ—β€˜(𝐴 Β· 𝐡)) = ((βˆ—β€˜π΄) Β· (βˆ—β€˜π΅))))
 
Theoremremul 10880 Real part of a product. (Contributed by NM, 28-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.)
((𝐴 ∈ β„‚ ∧ 𝐡 ∈ β„‚) β†’ (β„œβ€˜(𝐴 Β· 𝐡)) = (((β„œβ€˜π΄) Β· (β„œβ€˜π΅)) βˆ’ ((β„‘β€˜π΄) Β· (β„‘β€˜π΅))))
 
Theoremremul2 10881 Real part of a product. (Contributed by Mario Carneiro, 2-Aug-2014.)
((𝐴 ∈ ℝ ∧ 𝐡 ∈ β„‚) β†’ (β„œβ€˜(𝐴 Β· 𝐡)) = (𝐴 Β· (β„œβ€˜π΅)))
 
Theoremredivap 10882 Real part of a division. Related to remul2 10881. (Contributed by Jim Kingdon, 14-Jun-2020.)
((𝐴 ∈ β„‚ ∧ 𝐡 ∈ ℝ ∧ 𝐡 # 0) β†’ (β„œβ€˜(𝐴 / 𝐡)) = ((β„œβ€˜π΄) / 𝐡))
 
Theoremimcj 10883 Imaginary part of a complex conjugate. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
(𝐴 ∈ β„‚ β†’ (β„‘β€˜(βˆ—β€˜π΄)) = -(β„‘β€˜π΄))
 
Theoremimneg 10884 The imaginary part of a negative number. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
(𝐴 ∈ β„‚ β†’ (β„‘β€˜-𝐴) = -(β„‘β€˜π΄))
 
Theoremimadd 10885 Imaginary part distributes over addition. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
((𝐴 ∈ β„‚ ∧ 𝐡 ∈ β„‚) β†’ (β„‘β€˜(𝐴 + 𝐡)) = ((β„‘β€˜π΄) + (β„‘β€˜π΅)))
 
Theoremimsub 10886 Imaginary part distributes over subtraction. (Contributed by NM, 18-Mar-2005.)
((𝐴 ∈ β„‚ ∧ 𝐡 ∈ β„‚) β†’ (β„‘β€˜(𝐴 βˆ’ 𝐡)) = ((β„‘β€˜π΄) βˆ’ (β„‘β€˜π΅)))
 
Theoremimmul 10887 Imaginary part of a product. (Contributed by NM, 28-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.)
((𝐴 ∈ β„‚ ∧ 𝐡 ∈ β„‚) β†’ (β„‘β€˜(𝐴 Β· 𝐡)) = (((β„œβ€˜π΄) Β· (β„‘β€˜π΅)) + ((β„‘β€˜π΄) Β· (β„œβ€˜π΅))))
 
Theoremimmul2 10888 Imaginary part of a product. (Contributed by Mario Carneiro, 2-Aug-2014.)
((𝐴 ∈ ℝ ∧ 𝐡 ∈ β„‚) β†’ (β„‘β€˜(𝐴 Β· 𝐡)) = (𝐴 Β· (β„‘β€˜π΅)))
 
Theoremimdivap 10889 Imaginary part of a division. Related to immul2 10888. (Contributed by Jim Kingdon, 14-Jun-2020.)
((𝐴 ∈ β„‚ ∧ 𝐡 ∈ ℝ ∧ 𝐡 # 0) β†’ (β„‘β€˜(𝐴 / 𝐡)) = ((β„‘β€˜π΄) / 𝐡))
 
Theoremcjre 10890 A real number equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by NM, 8-Oct-1999.)
(𝐴 ∈ ℝ β†’ (βˆ—β€˜π΄) = 𝐴)
 
Theoremcjcj 10891 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.)
(𝐴 ∈ β„‚ β†’ (βˆ—β€˜(βˆ—β€˜π΄)) = 𝐴)
 
Theoremcjadd 10892 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.)
((𝐴 ∈ β„‚ ∧ 𝐡 ∈ β„‚) β†’ (βˆ—β€˜(𝐴 + 𝐡)) = ((βˆ—β€˜π΄) + (βˆ—β€˜π΅)))
 
Theoremcjmul 10893 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.)
((𝐴 ∈ β„‚ ∧ 𝐡 ∈ β„‚) β†’ (βˆ—β€˜(𝐴 Β· 𝐡)) = ((βˆ—β€˜π΄) Β· (βˆ—β€˜π΅)))
 
Theoremipcnval 10894 Standard inner product on complex numbers. (Contributed by NM, 29-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.)
((𝐴 ∈ β„‚ ∧ 𝐡 ∈ β„‚) β†’ (β„œβ€˜(𝐴 Β· (βˆ—β€˜π΅))) = (((β„œβ€˜π΄) Β· (β„œβ€˜π΅)) + ((β„‘β€˜π΄) Β· (β„‘β€˜π΅))))
 
Theoremcjmulrcl 10895 A complex number times its conjugate is real. (Contributed by NM, 26-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
(𝐴 ∈ β„‚ β†’ (𝐴 Β· (βˆ—β€˜π΄)) ∈ ℝ)
 
Theoremcjmulval 10896 A complex number times its conjugate. (Contributed by NM, 1-Feb-2007.) (Revised by Mario Carneiro, 14-Jul-2014.)
(𝐴 ∈ β„‚ β†’ (𝐴 Β· (βˆ—β€˜π΄)) = (((β„œβ€˜π΄)↑2) + ((β„‘β€˜π΄)↑2)))
 
Theoremcjmulge0 10897 A complex number times its conjugate is nonnegative. (Contributed by NM, 26-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
(𝐴 ∈ β„‚ β†’ 0 ≀ (𝐴 Β· (βˆ—β€˜π΄)))
 
Theoremcjneg 10898 Complex conjugate of negative. (Contributed by NM, 27-Feb-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
(𝐴 ∈ β„‚ β†’ (βˆ—β€˜-𝐴) = -(βˆ—β€˜π΄))
 
Theoremaddcj 10899 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 Β· (β„œβ€˜π΄)))
 
Theoremcjsub 10900 Complex conjugate distributes over subtraction. (Contributed by NM, 28-Apr-2005.)
((𝐴 ∈ β„‚ ∧ 𝐡 ∈ β„‚) β†’ (βˆ—β€˜(𝐴 βˆ’ 𝐡)) = ((βˆ—β€˜π΄) βˆ’ (βˆ—β€˜π΅)))
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13700 138 13701-13800 139 13801-13900 140 13901-14000 141 14001-14100 142 14101-14200 143 14201-14300 144 14301-14400 145 14401-14500 146 14501-14600 147 14601-14700 148 14701-14800 149 14801-14801
  Copyright terms: Public domain < Previous  Next >