P. 483 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 48201-48300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ldepsprlem 48201	Lemma for ldepspr 48202. (Contributed by AV, 16-Apr-2019.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑅 = (Scalar‘𝑀)    &   ⊢ 𝑆 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑍 = (0g‘𝑀)    &   ⊢ · = ( ·𝑠 ‘𝑀)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝑁 = (invg‘𝑅)    ⇒   ⊢ ((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝐴 ∈ 𝑆)) → (𝑋 = (𝐴 · 𝑌) → (( 1 · 𝑋)(+g‘𝑀)((𝑁‘𝐴) · 𝑌)) = 𝑍))
Theorem	ldepspr 48202	If a vector is a scalar multiple of another vector, the (unordered pair containing the) two vectors are linearly dependent. (Contributed by AV, 16-Apr-2019.) (Revised by AV, 27-Apr-2019.) (Proof shortened by AV, 30-Jul-2019.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑅 = (Scalar‘𝑀)    &   ⊢ 𝑆 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑍 = (0g‘𝑀)    &   ⊢ · = ( ·𝑠 ‘𝑀)    ⇒   ⊢ ((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌)) → ((𝐴 ∈ 𝑆 ∧ 𝑋 = (𝐴 · 𝑌)) → {𝑋, 𝑌} linDepS 𝑀))
Theorem	lincresunit3lem3 48203	Lemma 3 for lincresunit3 48210. (Contributed by AV, 18-May-2019.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑅 = (Scalar‘𝑀)    &   ⊢ 𝐸 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝑁 = (invg‘𝑅)    &   ⊢ · = ( ·𝑠 ‘𝑀)    ⇒   ⊢ (((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝐴 ∈ 𝑈) → (((𝑁‘𝐴) · 𝑋) = ((𝑁‘𝐴) · 𝑌) ↔ 𝑋 = 𝑌))
Theorem	lincresunitlem1 48204	Lemma 1 for properties of a specially modified restriction of a linear combination containing a unit as scalar. (Contributed by AV, 18-May-2019.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑅 = (Scalar‘𝑀)    &   ⊢ 𝐸 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑍 = (0g‘𝑀)    &   ⊢ 𝑁 = (invg‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝐺 = (𝑠 ∈ (𝑆 ∖ {𝑋}) ↦ ((𝐼‘(𝑁‘(𝐹‘𝑋))) · (𝐹‘𝑠)))    ⇒   ⊢ (((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) ∧ (𝐹 ∈ (𝐸 ↑m 𝑆) ∧ (𝐹‘𝑋) ∈ 𝑈)) → (𝐼‘(𝑁‘(𝐹‘𝑋))) ∈ 𝐸)
Theorem	lincresunitlem2 48205	Lemma for properties of a specially modified restriction of a linear combination containing a unit as scalar. (Contributed by AV, 18-May-2019.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑅 = (Scalar‘𝑀)    &   ⊢ 𝐸 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑍 = (0g‘𝑀)    &   ⊢ 𝑁 = (invg‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝐺 = (𝑠 ∈ (𝑆 ∖ {𝑋}) ↦ ((𝐼‘(𝑁‘(𝐹‘𝑋))) · (𝐹‘𝑠)))    ⇒   ⊢ ((((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) ∧ (𝐹 ∈ (𝐸 ↑m 𝑆) ∧ (𝐹‘𝑋) ∈ 𝑈)) ∧ 𝑌 ∈ 𝑆) → ((𝐼‘(𝑁‘(𝐹‘𝑋))) · (𝐹‘𝑌)) ∈ 𝐸)
Theorem	lincresunit1 48206*	Property 1 of a specially modified restriction of a linear combination containing a unit as scalar. (Contributed by AV, 18-May-2019.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑅 = (Scalar‘𝑀)    &   ⊢ 𝐸 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑍 = (0g‘𝑀)    &   ⊢ 𝑁 = (invg‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝐺 = (𝑠 ∈ (𝑆 ∖ {𝑋}) ↦ ((𝐼‘(𝑁‘(𝐹‘𝑋))) · (𝐹‘𝑠)))    ⇒   ⊢ (((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) ∧ (𝐹 ∈ (𝐸 ↑m 𝑆) ∧ (𝐹‘𝑋) ∈ 𝑈)) → 𝐺 ∈ (𝐸 ↑m (𝑆 ∖ {𝑋})))
Theorem	lincresunit2 48207*	Property 2 of a specially modified restriction of a linear combination containing a unit as scalar. (Contributed by AV, 18-May-2019.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑅 = (Scalar‘𝑀)    &   ⊢ 𝐸 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑍 = (0g‘𝑀)    &   ⊢ 𝑁 = (invg‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝐺 = (𝑠 ∈ (𝑆 ∖ {𝑋}) ↦ ((𝐼‘(𝑁‘(𝐹‘𝑋))) · (𝐹‘𝑠)))    ⇒   ⊢ (((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) ∧ (𝐹 ∈ (𝐸 ↑m 𝑆) ∧ (𝐹‘𝑋) ∈ 𝑈 ∧ 𝐹 finSupp 0 )) → 𝐺 finSupp 0 )
Theorem	lincresunit3lem1 48208*	Lemma 1 for lincresunit3 48210. (Contributed by AV, 17-May-2019.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑅 = (Scalar‘𝑀)    &   ⊢ 𝐸 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑍 = (0g‘𝑀)    &   ⊢ 𝑁 = (invg‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝐺 = (𝑠 ∈ (𝑆 ∖ {𝑋}) ↦ ((𝐼‘(𝑁‘(𝐹‘𝑋))) · (𝐹‘𝑠)))    ⇒   ⊢ (((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) ∧ (𝐹 ∈ (𝐸 ↑m 𝑆) ∧ (𝐹‘𝑋) ∈ 𝑈 ∧ 𝑧 ∈ (𝑆 ∖ {𝑋}))) → ((𝑁‘(𝐹‘𝑋))( ·𝑠 ‘𝑀)((𝐺‘𝑧)( ·𝑠 ‘𝑀)𝑧)) = ((𝐹‘𝑧)( ·𝑠 ‘𝑀)𝑧))
Theorem	lincresunit3lem2 48209*	Lemma 2 for lincresunit3 48210. (Contributed by AV, 18-May-2019.) (Proof shortened by AV, 30-Jul-2019.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑅 = (Scalar‘𝑀)    &   ⊢ 𝐸 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑍 = (0g‘𝑀)    &   ⊢ 𝑁 = (invg‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝐺 = (𝑠 ∈ (𝑆 ∖ {𝑋}) ↦ ((𝐼‘(𝑁‘(𝐹‘𝑋))) · (𝐹‘𝑠)))    ⇒   ⊢ (((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) ∧ (𝐹 ∈ (𝐸 ↑m 𝑆) ∧ (𝐹‘𝑋) ∈ 𝑈 ∧ 𝐹 finSupp 0 )) → ((𝑁‘(𝐹‘𝑋))( ·𝑠 ‘𝑀)(𝑀 Σg (𝑧 ∈ (𝑆 ∖ {𝑋}) ↦ ((𝐺‘𝑧)( ·𝑠 ‘𝑀)𝑧)))) = ((𝐹 ↾ (𝑆 ∖ {𝑋}))( linC ‘𝑀)(𝑆 ∖ {𝑋})))
Theorem	lincresunit3 48210*	Property 3 of a specially modified restriction of a linear combination in a vector space. (Contributed by AV, 18-May-2019.) (Proof shortened by AV, 30-Jul-2019.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑅 = (Scalar‘𝑀)    &   ⊢ 𝐸 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑍 = (0g‘𝑀)    &   ⊢ 𝑁 = (invg‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝐺 = (𝑠 ∈ (𝑆 ∖ {𝑋}) ↦ ((𝐼‘(𝑁‘(𝐹‘𝑋))) · (𝐹‘𝑠)))    ⇒   ⊢ (((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) ∧ (𝐹 ∈ (𝐸 ↑m 𝑆) ∧ (𝐹‘𝑋) ∈ 𝑈 ∧ 𝐹 finSupp 0 ) ∧ (𝐹( linC ‘𝑀)𝑆) = 𝑍) → (𝐺( linC ‘𝑀)(𝑆 ∖ {𝑋})) = 𝑋)
Theorem	lincreslvec3 48211*	Property 3 of a specially modified restriction of a linear combination in a vector space. (Contributed by AV, 18-May-2019.) (Proof shortened by AV, 30-Jul-2019.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑅 = (Scalar‘𝑀)    &   ⊢ 𝐸 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑍 = (0g‘𝑀)    &   ⊢ 𝑁 = (invg‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝐺 = (𝑠 ∈ (𝑆 ∖ {𝑋}) ↦ ((𝐼‘(𝑁‘(𝐹‘𝑋))) · (𝐹‘𝑠)))    ⇒   ⊢ (((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LVec ∧ 𝑋 ∈ 𝑆) ∧ (𝐹 ∈ (𝐸 ↑m 𝑆) ∧ (𝐹‘𝑋) ≠ 0 ∧ 𝐹 finSupp 0 ) ∧ (𝐹( linC ‘𝑀)𝑆) = 𝑍) → (𝐺( linC ‘𝑀)(𝑆 ∖ {𝑋})) = 𝑋)
Theorem	islindeps2 48212*	Conditions for being a linearly dependent subset of a (left) module over a nonzero ring. (Contributed by AV, 29-Apr-2019.) (Proof shortened by AV, 30-Jul-2019.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑍 = (0g‘𝑀)    &   ⊢ 𝑅 = (Scalar‘𝑀)    &   ⊢ 𝐸 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ∧ 𝑅 ∈ NzRing) → (∃𝑠 ∈ 𝑆 ∃𝑓 ∈ (𝐸 ↑m (𝑆 ∖ {𝑠}))(𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)(𝑆 ∖ {𝑠})) = 𝑠) → 𝑆 linDepS 𝑀))
Theorem	islininds2 48213*	Implication of being a linearly independent subset of a (left) module over a nonzero ring. (Contributed by AV, 29-Apr-2019.) (Proof shortened by AV, 30-Jul-2019.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑍 = (0g‘𝑀)    &   ⊢ 𝑅 = (Scalar‘𝑀)    &   ⊢ 𝐸 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ∧ 𝑅 ∈ NzRing) → (𝑆 linIndS 𝑀 → ∀𝑠 ∈ 𝑆 ∀𝑓 ∈ (𝐸 ↑m (𝑆 ∖ {𝑠}))(¬ 𝑓 finSupp 0 ∨ (𝑓( linC ‘𝑀)(𝑆 ∖ {𝑠})) ≠ 𝑠)))
Theorem	isldepslvec2 48214*	Alternative definition of being a linearly dependent subset of a (left) vector space. In this case, the reverse implication of islindeps2 48212 holds, so that both definitions are equivalent (see theorem 1.6 in [Roman] p. 46 and the note in [Roman] p. 112: if a nontrivial linear combination of elements (where not all of the coefficients are 0) in an R-vector space is 0, then and only then each of the elements is a linear combination of the others. (Contributed by AV, 30-Apr-2019.) (Proof shortened by AV, 30-Jul-2019.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑍 = (0g‘𝑀)    &   ⊢ 𝑅 = (Scalar‘𝑀)    &   ⊢ 𝐸 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑀 ∈ LVec ∧ 𝑆 ∈ 𝒫 𝐵) → (∃𝑠 ∈ 𝑆 ∃𝑓 ∈ (𝐸 ↑m (𝑆 ∖ {𝑠}))(𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)(𝑆 ∖ {𝑠})) = 𝑠) ↔ 𝑆 linDepS 𝑀))
Theorem	lindssnlvec 48215	A singleton not containing the zero element of a vector space is always linearly independent. (Contributed by AV, 16-Apr-2019.) (Revised by AV, 28-Apr-2019.)
⊢ ((𝑀 ∈ LVec ∧ 𝑆 ∈ (Base‘𝑀) ∧ 𝑆 ≠ (0g‘𝑀)) → {𝑆} linIndS 𝑀)
21.48.20.4  Simple left modules and the ` ZZ `-module
Theorem	lmod1lem1 48216*	Lemma 1 for lmod1 48221. (Contributed by AV, 28-Apr-2019.)
⊢ 𝑀 = ({⟨(Base‘ndx), {𝐼}⟩, ⟨(+g‘ndx), {⟨⟨𝐼, 𝐼⟩, 𝐼⟩}⟩, ⟨(Scalar‘ndx), 𝑅⟩} ∪ {⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ {𝐼} ↦ 𝑦)⟩})    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ∧ 𝑟 ∈ (Base‘𝑅)) → (𝑟( ·𝑠 ‘𝑀)𝐼) ∈ {𝐼})
Theorem	lmod1lem2 48217*	Lemma 2 for lmod1 48221. (Contributed by AV, 28-Apr-2019.)
⊢ 𝑀 = ({⟨(Base‘ndx), {𝐼}⟩, ⟨(+g‘ndx), {⟨⟨𝐼, 𝐼⟩, 𝐼⟩}⟩, ⟨(Scalar‘ndx), 𝑅⟩} ∪ {⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ {𝐼} ↦ 𝑦)⟩})    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ∧ 𝑟 ∈ (Base‘𝑅)) → (𝑟( ·𝑠 ‘𝑀)(𝐼(+g‘𝑀)𝐼)) = ((𝑟( ·𝑠 ‘𝑀)𝐼)(+g‘𝑀)(𝑟( ·𝑠 ‘𝑀)𝐼)))
Theorem	lmod1lem3 48218*	Lemma 3 for lmod1 48221. (Contributed by AV, 29-Apr-2019.)
⊢ 𝑀 = ({⟨(Base‘ndx), {𝐼}⟩, ⟨(+g‘ndx), {⟨⟨𝐼, 𝐼⟩, 𝐼⟩}⟩, ⟨(Scalar‘ndx), 𝑅⟩} ∪ {⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ {𝐼} ↦ 𝑦)⟩})    ⇒   ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) ∧ (𝑞 ∈ (Base‘𝑅) ∧ 𝑟 ∈ (Base‘𝑅))) → ((𝑞(+g‘(Scalar‘𝑀))𝑟)( ·𝑠 ‘𝑀)𝐼) = ((𝑞( ·𝑠 ‘𝑀)𝐼)(+g‘𝑀)(𝑟( ·𝑠 ‘𝑀)𝐼)))
Theorem	lmod1lem4 48219*	Lemma 4 for lmod1 48221. (Contributed by AV, 29-Apr-2019.)
⊢ 𝑀 = ({⟨(Base‘ndx), {𝐼}⟩, ⟨(+g‘ndx), {⟨⟨𝐼, 𝐼⟩, 𝐼⟩}⟩, ⟨(Scalar‘ndx), 𝑅⟩} ∪ {⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ {𝐼} ↦ 𝑦)⟩})    ⇒   ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) ∧ (𝑞 ∈ (Base‘𝑅) ∧ 𝑟 ∈ (Base‘𝑅))) → ((𝑞(.r‘(Scalar‘𝑀))𝑟)( ·𝑠 ‘𝑀)𝐼) = (𝑞( ·𝑠 ‘𝑀)(𝑟( ·𝑠 ‘𝑀)𝐼)))
Theorem	lmod1lem5 48220*	Lemma 5 for lmod1 48221. (Contributed by AV, 28-Apr-2019.)
⊢ 𝑀 = ({⟨(Base‘ndx), {𝐼}⟩, ⟨(+g‘ndx), {⟨⟨𝐼, 𝐼⟩, 𝐼⟩}⟩, ⟨(Scalar‘ndx), 𝑅⟩} ∪ {⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ {𝐼} ↦ 𝑦)⟩})    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) → ((1r‘(Scalar‘𝑀))( ·𝑠 ‘𝑀)𝐼) = 𝐼)
Theorem	lmod1 48221*	The (smallest) structure representing a zero module over an arbitrary ring. (Contributed by AV, 29-Apr-2019.)
⊢ 𝑀 = ({⟨(Base‘ndx), {𝐼}⟩, ⟨(+g‘ndx), {⟨⟨𝐼, 𝐼⟩, 𝐼⟩}⟩, ⟨(Scalar‘ndx), 𝑅⟩} ∪ {⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ {𝐼} ↦ 𝑦)⟩})    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) → 𝑀 ∈ LMod)
Theorem	lmod1zr 48222	The (smallest) structure representing a zero module over a zero ring. (Contributed by AV, 29-Apr-2019.)
⊢ 𝑅 = {⟨(Base‘ndx), {𝑍}⟩, ⟨(+g‘ndx), {⟨⟨𝑍, 𝑍⟩, 𝑍⟩}⟩, ⟨(.r‘ndx), {⟨⟨𝑍, 𝑍⟩, 𝑍⟩}⟩}    &   ⊢ 𝑀 = ({⟨(Base‘ndx), {𝐼}⟩, ⟨(+g‘ndx), {⟨⟨𝐼, 𝐼⟩, 𝐼⟩}⟩, ⟨(Scalar‘ndx), 𝑅⟩} ∪ {⟨( ·𝑠 ‘ndx), {⟨⟨𝑍, 𝐼⟩, 𝐼⟩}⟩})    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → 𝑀 ∈ LMod)
Theorem	lmod1zrnlvec 48223	There is a (left) module (a zero module) which is not a (left) vector space. (Contributed by AV, 29-Apr-2019.)
⊢ 𝑅 = {⟨(Base‘ndx), {𝑍}⟩, ⟨(+g‘ndx), {⟨⟨𝑍, 𝑍⟩, 𝑍⟩}⟩, ⟨(.r‘ndx), {⟨⟨𝑍, 𝑍⟩, 𝑍⟩}⟩}    &   ⊢ 𝑀 = ({⟨(Base‘ndx), {𝐼}⟩, ⟨(+g‘ndx), {⟨⟨𝐼, 𝐼⟩, 𝐼⟩}⟩, ⟨(Scalar‘ndx), 𝑅⟩} ∪ {⟨( ·𝑠 ‘ndx), {⟨⟨𝑍, 𝐼⟩, 𝐼⟩}⟩})    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → 𝑀 ∉ LVec)
Theorem	lmodn0 48224	Left modules exist. (Contributed by AV, 29-Apr-2019.)
⊢ LMod ≠ ∅
Theorem	zlmodzxzequa 48225	Example of an equation within the ℤ-module ℤ × ℤ (see example in [Roman] p. 112 for a linearly dependent set). (Contributed by AV, 22-May-2019.) (Revised by AV, 10-Jun-2019.)
⊢ 𝑍 = (ℤring freeLMod {0, 1})    &   ⊢ 0 = {⟨0, 0⟩, ⟨1, 0⟩}    &   ⊢ ∙ = ( ·𝑠 ‘𝑍)    &   ⊢ − = (-g‘𝑍)    &   ⊢ 𝐴 = {⟨0, 3⟩, ⟨1, 6⟩}    &   ⊢ 𝐵 = {⟨0, 2⟩, ⟨1, 4⟩}    ⇒   ⊢ ((2 ∙ 𝐴) − (3 ∙ 𝐵)) = 0
Theorem	zlmodzxznm 48226	Example of a linearly dependent set whose elements are not linear combinations of the others, see note in [Roman] p. 112). (Contributed by AV, 23-May-2019.) (Revised by AV, 10-Jun-2019.)
⊢ 𝑍 = (ℤring freeLMod {0, 1})    &   ⊢ 0 = {⟨0, 0⟩, ⟨1, 0⟩}    &   ⊢ ∙ = ( ·𝑠 ‘𝑍)    &   ⊢ − = (-g‘𝑍)    &   ⊢ 𝐴 = {⟨0, 3⟩, ⟨1, 6⟩}    &   ⊢ 𝐵 = {⟨0, 2⟩, ⟨1, 4⟩}    ⇒   ⊢ ∀𝑖 ∈ ℤ ((𝑖 ∙ 𝐴) ≠ 𝐵 ∧ (𝑖 ∙ 𝐵) ≠ 𝐴)
Theorem	zlmodzxzldeplem 48227	A and B are not equal. (Contributed by AV, 24-May-2019.) (Revised by AV, 10-Jun-2019.)
⊢ 𝑍 = (ℤring freeLMod {0, 1})    &   ⊢ 𝐴 = {⟨0, 3⟩, ⟨1, 6⟩}    &   ⊢ 𝐵 = {⟨0, 2⟩, ⟨1, 4⟩}    ⇒   ⊢ 𝐴 ≠ 𝐵
Theorem	zlmodzxzequap 48228	Example of an equation within the ℤ-module ℤ × ℤ (see example in [Roman] p. 112 for a linearly dependent set), written as a sum. (Contributed by AV, 24-May-2019.) (Revised by AV, 10-Jun-2019.)
⊢ 𝑍 = (ℤring freeLMod {0, 1})    &   ⊢ 𝐴 = {⟨0, 3⟩, ⟨1, 6⟩}    &   ⊢ 𝐵 = {⟨0, 2⟩, ⟨1, 4⟩}    &   ⊢ 0 = {⟨0, 0⟩, ⟨1, 0⟩}    &   ⊢ + = (+g‘𝑍)    &   ⊢ ∙ = ( ·𝑠 ‘𝑍)    ⇒   ⊢ ((2 ∙ 𝐴) + (-3 ∙ 𝐵)) = 0
Theorem	zlmodzxzldeplem1 48229	Lemma 1 for zlmodzxzldep 48233. (Contributed by AV, 24-May-2019.) (Revised by AV, 10-Jun-2019.)
⊢ 𝑍 = (ℤring freeLMod {0, 1})    &   ⊢ 𝐴 = {⟨0, 3⟩, ⟨1, 6⟩}    &   ⊢ 𝐵 = {⟨0, 2⟩, ⟨1, 4⟩}    &   ⊢ 𝐹 = {⟨𝐴, 2⟩, ⟨𝐵, -3⟩}    ⇒   ⊢ 𝐹 ∈ (ℤ ↑m {𝐴, 𝐵})
Theorem	zlmodzxzldeplem2 48230	Lemma 2 for zlmodzxzldep 48233. (Contributed by AV, 24-May-2019.) (Revised by AV, 30-Jul-2019.)
⊢ 𝑍 = (ℤring freeLMod {0, 1})    &   ⊢ 𝐴 = {⟨0, 3⟩, ⟨1, 6⟩}    &   ⊢ 𝐵 = {⟨0, 2⟩, ⟨1, 4⟩}    &   ⊢ 𝐹 = {⟨𝐴, 2⟩, ⟨𝐵, -3⟩}    ⇒   ⊢ 𝐹 finSupp 0
Theorem	zlmodzxzldeplem3 48231	Lemma 3 for zlmodzxzldep 48233. (Contributed by AV, 24-May-2019.) (Revised by AV, 10-Jun-2019.)
⊢ 𝑍 = (ℤring freeLMod {0, 1})    &   ⊢ 𝐴 = {⟨0, 3⟩, ⟨1, 6⟩}    &   ⊢ 𝐵 = {⟨0, 2⟩, ⟨1, 4⟩}    &   ⊢ 𝐹 = {⟨𝐴, 2⟩, ⟨𝐵, -3⟩}    ⇒   ⊢ (𝐹( linC ‘𝑍){𝐴, 𝐵}) = (0g‘𝑍)
Theorem	zlmodzxzldeplem4 48232*	Lemma 4 for zlmodzxzldep 48233. (Contributed by AV, 24-May-2019.) (Revised by AV, 10-Jun-2019.)
⊢ 𝑍 = (ℤring freeLMod {0, 1})    &   ⊢ 𝐴 = {⟨0, 3⟩, ⟨1, 6⟩}    &   ⊢ 𝐵 = {⟨0, 2⟩, ⟨1, 4⟩}    &   ⊢ 𝐹 = {⟨𝐴, 2⟩, ⟨𝐵, -3⟩}    ⇒   ⊢ ∃𝑦 ∈ {𝐴, 𝐵} (𝐹‘𝑦) ≠ 0
Theorem	zlmodzxzldep 48233	{ A , B } is a linearly dependent set within the ℤ-module ℤ × ℤ (see example in [Roman] p. 112). (Contributed by AV, 22-May-2019.) (Revised by AV, 10-Jun-2019.)
⊢ 𝑍 = (ℤring freeLMod {0, 1})    &   ⊢ 𝐴 = {⟨0, 3⟩, ⟨1, 6⟩}    &   ⊢ 𝐵 = {⟨0, 2⟩, ⟨1, 4⟩}    ⇒   ⊢ {𝐴, 𝐵} linDepS 𝑍
Theorem	ldepsnlinclem1 48234	Lemma 1 for ldepsnlinc 48237. (Contributed by AV, 25-May-2019.) (Revised by AV, 10-Jun-2019.)
⊢ 𝑍 = (ℤring freeLMod {0, 1})    &   ⊢ 𝐴 = {⟨0, 3⟩, ⟨1, 6⟩}    &   ⊢ 𝐵 = {⟨0, 2⟩, ⟨1, 4⟩}    ⇒   ⊢ (𝐹 ∈ ((Base‘ℤring) ↑m {𝐵}) → (𝐹( linC ‘𝑍){𝐵}) ≠ 𝐴)
Theorem	ldepsnlinclem2 48235	Lemma 2 for ldepsnlinc 48237. (Contributed by AV, 25-May-2019.) (Revised by AV, 10-Jun-2019.)
⊢ 𝑍 = (ℤring freeLMod {0, 1})    &   ⊢ 𝐴 = {⟨0, 3⟩, ⟨1, 6⟩}    &   ⊢ 𝐵 = {⟨0, 2⟩, ⟨1, 4⟩}    ⇒   ⊢ (𝐹 ∈ ((Base‘ℤring) ↑m {𝐴}) → (𝐹( linC ‘𝑍){𝐴}) ≠ 𝐵)
21.48.20.5  Differences between (left) modules and (left) vector spaces
Theorem	lvecpsslmod 48236	The class of all (left) vector spaces is a proper subclass of the class of all (left) modules. Although it is obvious (and proven by lveclmod 21128) that every left vector space is a left module, there is (at least) one left module which is no left vector space, for example the zero module over the zero ring, see lmod1zrnlvec 48223. (Contributed by AV, 29-Apr-2019.)
⊢ LVec ⊊ LMod
Theorem	ldepsnlinc 48237*	The reverse implication of islindeps2 48212 does not hold for arbitrary (left) modules, see note in [Roman] p. 112: "... if a nontrivial linear combination of the elements ... in an R-module M is 0, ... where not all of the coefficients are 0, then we cannot conclude ... that one of the elements ... is a linear combination of the others." This means that there is at least one left module having a linearly dependent subset in which there is at least one element which is not a linear combination of the other elements of this subset. Such a left module can be constructed by using zlmodzxzequa 48225 and zlmodzxznm 48226. (Contributed by AV, 25-May-2019.) (Revised by AV, 30-Jul-2019.)
⊢ ∃𝑚 ∈ LMod ∃𝑠 ∈ 𝒫 (Base‘𝑚)(𝑠 linDepS 𝑚 ∧ ∀𝑣 ∈ 𝑠 ∀𝑓 ∈ ((Base‘(Scalar‘𝑚)) ↑m (𝑠 ∖ {𝑣}))(𝑓 finSupp (0g‘(Scalar‘𝑚)) → (𝑓( linC ‘𝑚)(𝑠 ∖ {𝑣})) ≠ 𝑣))
Theorem	ldepslinc 48238*	For (left) vector spaces, isldepslvec2 48214 provides an alternative definition of being a linearly dependent subset, whereas ldepsnlinc 48237 indicates that there is not an analogous alternative definition for arbitrary (left) modules. (Contributed by AV, 25-May-2019.) (Revised by AV, 30-Jul-2019.)
⊢ (∀𝑚 ∈ LVec ∀𝑠 ∈ 𝒫 (Base‘𝑚)(𝑠 linDepS 𝑚 ↔ ∃𝑣 ∈ 𝑠 ∃𝑓 ∈ ((Base‘(Scalar‘𝑚)) ↑m (𝑠 ∖ {𝑣}))(𝑓 finSupp (0g‘(Scalar‘𝑚)) ∧ (𝑓( linC ‘𝑚)(𝑠 ∖ {𝑣})) = 𝑣)) ∧ ¬ ∀𝑚 ∈ LMod ∀𝑠 ∈ 𝒫 (Base‘𝑚)(𝑠 linDepS 𝑚 ↔ ∃𝑣 ∈ 𝑠 ∃𝑓 ∈ ((Base‘(Scalar‘𝑚)) ↑m (𝑠 ∖ {𝑣}))(𝑓 finSupp (0g‘(Scalar‘𝑚)) ∧ (𝑓( linC ‘𝑚)(𝑠 ∖ {𝑣})) = 𝑣)))
21.48.21  Complexity theory
21.48.21.1  Auxiliary theorems
Theorem	suppdm 48239	If the range of a function does not contain the zero, the support of the function equals its domain. (Contributed by AV, 20-May-2020.)
⊢ (((Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ 𝑍 ∉ ran 𝐹) → (𝐹 supp 𝑍) = dom 𝐹)
Theorem	eluz2cnn0n1 48240	An integer greater than 1 is a complex number not equal to 0 or 1. (Contributed by AV, 23-May-2020.)
⊢ (𝐵 ∈ (ℤ≥‘2) → 𝐵 ∈ (ℂ ∖ {0, 1}))
Theorem	divge1b 48241	The ratio of a real number to a positive real number is greater than or equal to 1 iff the divisor (the positive real number) is less than or equal to the dividend (the real number). (Contributed by AV, 26-May-2020.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ 1 ≤ (𝐵 / 𝐴)))
Theorem	divgt1b 48242	The ratio of a real number to a positive real number is greater than 1 iff the divisor (the positive real number) is less than the dividend (the real number). (Contributed by AV, 30-May-2020.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 1 < (𝐵 / 𝐴)))
Theorem	ltsubaddb 48243	Equivalence for the "less than" relation between differences and sums. (Contributed by AV, 6-Jun-2020.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 − 𝐶) < (𝐵 − 𝐷) ↔ (𝐴 + 𝐷) < (𝐵 + 𝐶)))
Theorem	ltsubsubb 48244	Equivalence for the "less than" relation between differences. (Contributed by AV, 6-Jun-2020.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 − 𝐶) < (𝐵 − 𝐷) ↔ (𝐴 − 𝐵) < (𝐶 − 𝐷)))
Theorem	ltsubadd2b 48245	Equivalence for the "less than" relation between differences and sums. (Contributed by AV, 6-Jun-2020.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐷 − 𝐶) < (𝐵 − 𝐴) ↔ (𝐴 + 𝐷) < (𝐵 + 𝐶)))
Theorem	divsub1dir 48246	Distribution of division over subtraction by 1. (Contributed by AV, 6-Jun-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → ((𝐴 / 𝐵) − 1) = ((𝐴 − 𝐵) / 𝐵))
Theorem	expnegico01 48247	An integer greater than 1 to the power of a negative integer is in the closed-below, open-above interval between 0 and 1. (Contributed by AV, 24-May-2020.)
⊢ ((𝐵 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝑁 < 0) → (𝐵↑𝑁) ∈ (0[,)1))
Theorem	elfzolborelfzop1 48248	An element of a half-open integer interval is either equal to the left bound of the interval or an element of a half-open integer interval with a lower bound increased by 1. (Contributed by AV, 2-Jun-2020.)
⊢ (𝐾 ∈ (𝑀..^𝑁) → (𝐾 = 𝑀 ∨ 𝐾 ∈ ((𝑀 + 1)..^𝑁)))
Theorem	pw2m1lepw2m1 48249	2 to the power of a positive integer decreased by 1 is less than or equal to 2 to the power of the integer minus 1. (Contributed by AV, 30-May-2020.)
⊢ (𝐼 ∈ ℕ → (2↑(𝐼 − 1)) ≤ ((2↑𝐼) − 1))
Theorem	zgtp1leeq 48250	If an integer is between another integer and its predecessor, the integer is equal to the other integer. (Contributed by AV, 7-Jun-2020.)
⊢ ((𝐼 ∈ ℤ ∧ 𝐴 ∈ ℤ) → (((𝐴 − 1) < 𝐼 ∧ 𝐼 ≤ 𝐴) → 𝐼 = 𝐴))
Theorem	flsubz 48251	An integer can be moved in and out of the floor of a difference. (Contributed by AV, 29-May-2020.)
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ) → (⌊‘(𝐴 − 𝑁)) = ((⌊‘𝐴) − 𝑁))
21.48.21.2  The modulo (remainder) operation (extension)
Theorem	fldivmod 48252	Expressing the floor of a division by the modulo operator. (Contributed by AV, 6-Jun-2020.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (⌊‘(𝐴 / 𝐵)) = ((𝐴 − (𝐴 mod 𝐵)) / 𝐵))
Theorem	mod0mul 48253*	If an integer is 0 modulo a positive integer, this integer must be the product of another integer and the modulus. (Contributed by AV, 7-Jun-2020.)
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝐴 mod 𝑁) = 0 → ∃𝑥 ∈ ℤ 𝐴 = (𝑥 · 𝑁)))
Theorem	modn0mul 48254*	If an integer is not 0 modulo a positive integer, this integer must be the sum of the product of another integer and the modulus and a positive integer less than the modulus. (Contributed by AV, 7-Jun-2020.)
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝐴 mod 𝑁) ≠ 0 → ∃𝑥 ∈ ℤ ∃𝑦 ∈ (1..^𝑁)𝐴 = ((𝑥 · 𝑁) + 𝑦)))
Theorem	m1modmmod 48255	An integer decreased by 1 modulo a positive integer minus the integer modulo the same modulus is either -1 or the modulus minus 1. (Contributed by AV, 7-Jun-2020.)
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝐴 − 1) mod 𝑁) − (𝐴 mod 𝑁)) = if((𝐴 mod 𝑁) = 0, (𝑁 − 1), -1))
Theorem	difmodm1lt 48256	The difference between an integer modulo a positive integer and the integer decreased by 1 modulo the same modulus is less than the modulus decreased by 1 (if the modulus is greater than 2). This theorem would not be valid for an odd 𝐴 and 𝑁 = 2, since ((𝐴 mod 𝑁) − ((𝐴 − 1) mod 𝑁)) would be (1 − 0) = 1 which is not less than (𝑁 − 1) = 1. (Contributed by AV, 6-Jun-2012.)
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁) → ((𝐴 mod 𝑁) − ((𝐴 − 1) mod 𝑁)) < (𝑁 − 1))
21.48.21.3  Even and odd integers
Theorem	nn0onn0ex 48257*	For each odd nonnegative integer there is a nonnegative integer which, multiplied by 2 and increased by 1, results in the odd nonnegative integer. (Contributed by AV, 30-May-2020.)
⊢ ((𝑁 ∈ ℕ0 ∧ ((𝑁 + 1) / 2) ∈ ℕ0) → ∃𝑚 ∈ ℕ0 𝑁 = ((2 · 𝑚) + 1))
Theorem	nn0enn0ex 48258*	For each even nonnegative integer there is a nonnegative integer which, multiplied by 2, results in the even nonnegative integer. (Contributed by AV, 30-May-2020.)
⊢ ((𝑁 ∈ ℕ0 ∧ (𝑁 / 2) ∈ ℕ0) → ∃𝑚 ∈ ℕ0 𝑁 = (2 · 𝑚))
Theorem	nnennex 48259*	For each even positive integer there is a positive integer which, multiplied by 2, results in the even positive integer. (Contributed by AV, 5-Jun-2023.)
⊢ ((𝑁 ∈ ℕ ∧ (𝑁 / 2) ∈ ℕ) → ∃𝑚 ∈ ℕ 𝑁 = (2 · 𝑚))
Theorem	nneop 48260	A positive integer is even or odd. (Contributed by AV, 30-May-2020.)
⊢ (𝑁 ∈ ℕ → ((𝑁 / 2) ∈ ℕ ∨ ((𝑁 + 1) / 2) ∈ ℕ))
Theorem	nneom 48261	A positive integer is even or odd. (Contributed by AV, 30-May-2020.)
⊢ (𝑁 ∈ ℕ → ((𝑁 / 2) ∈ ℕ ∨ ((𝑁 − 1) / 2) ∈ ℕ0))
Theorem	nn0eo 48262	A nonnegative integer is even or odd. (Contributed by AV, 27-May-2020.)
⊢ (𝑁 ∈ ℕ0 → ((𝑁 / 2) ∈ ℕ0 ∨ ((𝑁 + 1) / 2) ∈ ℕ0))
Theorem	nnpw2even 48263	2 to the power of a positive integer is even. (Contributed by AV, 2-Jun-2020.)
⊢ (𝑁 ∈ ℕ → ((2↑𝑁) / 2) ∈ ℕ)
Theorem	zefldiv2 48264	The floor of an even integer divided by 2 is equal to the integer divided by 2. (Contributed by AV, 7-Jun-2020.)
⊢ ((𝑁 ∈ ℤ ∧ (𝑁 / 2) ∈ ℤ) → (⌊‘(𝑁 / 2)) = (𝑁 / 2))
Theorem	zofldiv2 48265	The floor of an odd integer divided by 2 is equal to the integer first decreased by 1 and then divided by 2. (Contributed by AV, 7-Jun-2020.)
⊢ ((𝑁 ∈ ℤ ∧ ((𝑁 + 1) / 2) ∈ ℤ) → (⌊‘(𝑁 / 2)) = ((𝑁 − 1) / 2))
Theorem	nn0ofldiv2 48266	The floor of an odd nonnegative integer divided by 2 is equal to the integer first decreased by 1 and then divided by 2. (Contributed by AV, 1-Jun-2020.) (Proof shortened by AV, 7-Jun-2020.)
⊢ ((𝑁 ∈ ℕ0 ∧ ((𝑁 + 1) / 2) ∈ ℕ0) → (⌊‘(𝑁 / 2)) = ((𝑁 − 1) / 2))
Theorem	flnn0div2ge 48267	The floor of a positive integer divided by 2 is greater than or equal to the integer decreased by 1 and then divided by 2. (Contributed by AV, 1-Jun-2020.)
⊢ (𝑁 ∈ ℕ0 → ((𝑁 − 1) / 2) ≤ (⌊‘(𝑁 / 2)))
Theorem	flnn0ohalf 48268	The floor of the half of an odd positive integer is equal to the floor of the half of the integer decreased by 1. (Contributed by AV, 5-Jun-2012.)
⊢ ((𝑁 ∈ ℕ0 ∧ ((𝑁 + 1) / 2) ∈ ℕ0) → (⌊‘(𝑁 / 2)) = (⌊‘((𝑁 − 1) / 2)))
21.48.21.4  The natural logarithm on complex numbers (extension)
Theorem	logcxp0 48269	Logarithm of a complex power. Generalization of logcxp 26729. (Contributed by AV, 22-May-2020.)
⊢ ((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℂ ∧ (𝐵 · (log‘𝐴)) ∈ ran log) → (log‘(𝐴↑𝑐𝐵)) = (𝐵 · (log‘𝐴)))
Theorem	regt1loggt0 48270	The natural logarithm for a real number greater than 1 is greater than 0. (Contributed by AV, 25-May-2020.)
⊢ (𝐵 ∈ (1(,)+∞) → 0 < (log‘𝐵))
21.48.21.5  Division of functions
Syntax	cfdiv 48271	Extend class notation with the division operator of two functions.
class /f
Definition	df-fdiv 48272*	Define the division of two functions into the complex numbers. (Contributed by AV, 15-May-2020.)
⊢ /f = (𝑓 ∈ V, 𝑔 ∈ V ↦ ((𝑓 ∘f / 𝑔) ↾ (𝑔 supp 0)))
Theorem	fdivval 48273	The quotient of two functions into the complex numbers. (Contributed by AV, 15-May-2020.)
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → (𝐹 /f 𝐺) = ((𝐹 ∘f / 𝐺) ↾ (𝐺 supp 0)))
Theorem	fdivmpt 48274*	The quotient of two functions into the complex numbers as mapping. (Contributed by AV, 16-May-2020.)
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐺:𝐴⟶ℂ ∧ 𝐴 ∈ 𝑉) → (𝐹 /f 𝐺) = (𝑥 ∈ (𝐺 supp 0) ↦ ((𝐹‘𝑥) / (𝐺‘𝑥))))
Theorem	fdivmptf 48275	The quotient of two functions into the complex numbers is a function into the complex numbers. (Contributed by AV, 16-May-2020.)
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐺:𝐴⟶ℂ ∧ 𝐴 ∈ 𝑉) → (𝐹 /f 𝐺):(𝐺 supp 0)⟶ℂ)
Theorem	refdivmptf 48276	The quotient of two functions into the real numbers is a function into the real numbers. (Contributed by AV, 16-May-2020.)
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐺:𝐴⟶ℝ ∧ 𝐴 ∈ 𝑉) → (𝐹 /f 𝐺):(𝐺 supp 0)⟶ℝ)
Theorem	fdivpm 48277	The quotient of two functions into the complex numbers is a partial function. (Contributed by AV, 16-May-2020.)
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐺:𝐴⟶ℂ ∧ 𝐴 ∈ 𝑉) → (𝐹 /f 𝐺) ∈ (ℂ ↑pm 𝐴))
Theorem	refdivpm 48278	The quotient of two functions into the real numbers is a partial function. (Contributed by AV, 16-May-2020.)
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐺:𝐴⟶ℝ ∧ 𝐴 ∈ 𝑉) → (𝐹 /f 𝐺) ∈ (ℝ ↑pm 𝐴))
Theorem	fdivmptfv 48279	The function value of a quotient of two functions into the complex numbers. (Contributed by AV, 19-May-2020.)
⊢ (((𝐹:𝐴⟶ℂ ∧ 𝐺:𝐴⟶ℂ ∧ 𝐴 ∈ 𝑉) ∧ 𝑋 ∈ (𝐺 supp 0)) → ((𝐹 /f 𝐺)‘𝑋) = ((𝐹‘𝑋) / (𝐺‘𝑋)))
Theorem	refdivmptfv 48280	The function value of a quotient of two functions into the real numbers. (Contributed by AV, 19-May-2020.)
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐺:𝐴⟶ℝ ∧ 𝐴 ∈ 𝑉) ∧ 𝑋 ∈ (𝐺 supp 0)) → ((𝐹 /f 𝐺)‘𝑋) = ((𝐹‘𝑋) / (𝐺‘𝑋)))
21.48.21.6  Upper bounds
Syntax	cbigo 48281	Extend class notation with the class of the "big-O" function.
class Ο
Definition	df-bigo 48282*	Define the function "big-O", mapping a real function g to the set of real functions "of order g(x)". Definition in section 1.1 of [AhoHopUll] p. 2. This is a generalization of "big-O of one", see df-o1 15536 and df-lo1 15537. As explained in the comment of df-o1 , any big-O can be represented in terms of 𝑂(1) and division, see elbigolo1 48291. (Contributed by AV, 15-May-2020.)
⊢ Ο = (𝑔 ∈ (ℝ ↑pm ℝ) ↦ {𝑓 ∈ (ℝ ↑pm ℝ) ∣ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓‘𝑦) ≤ (𝑚 · (𝑔‘𝑦))})
Theorem	bigoval 48283*	Set of functions of order G(x). (Contributed by AV, 15-May-2020.)
⊢ (𝐺 ∈ (ℝ ↑pm ℝ) → (Ο‘𝐺) = {𝑓 ∈ (ℝ ↑pm ℝ) ∣ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓‘𝑦) ≤ (𝑚 · (𝐺‘𝑦))})
Theorem	elbigofrcl 48284	Reverse closure of the "big-O" function. (Contributed by AV, 16-May-2020.)
⊢ (𝐹 ∈ (Ο‘𝐺) → 𝐺 ∈ (ℝ ↑pm ℝ))
Theorem	elbigo 48285*	Properties of a function of order G(x). (Contributed by AV, 16-May-2020.)
⊢ (𝐹 ∈ (Ο‘𝐺) ↔ (𝐹 ∈ (ℝ ↑pm ℝ) ∧ 𝐺 ∈ (ℝ ↑pm ℝ) ∧ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝐹 ∩ (𝑥[,)+∞))(𝐹‘𝑦) ≤ (𝑚 · (𝐺‘𝑦))))
Theorem	elbigo2 48286*	Properties of a function of order G(x) under certain assumptions. (Contributed by AV, 17-May-2020.)
⊢ (((𝐺:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ (𝐹:𝐵⟶ℝ ∧ 𝐵 ⊆ 𝐴)) → (𝐹 ∈ (Ο‘𝐺) ↔ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝑚 · (𝐺‘𝑦)))))
Theorem	elbigo2r 48287*	Sufficient condition for a function to be of order G(x). (Contributed by AV, 18-May-2020.)
⊢ (((𝐺:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ (𝐹:𝐵⟶ℝ ∧ 𝐵 ⊆ 𝐴) ∧ (𝐶 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝐶 ≤ 𝑥 → (𝐹‘𝑥) ≤ (𝑀 · (𝐺‘𝑥))))) → 𝐹 ∈ (Ο‘𝐺))
Theorem	elbigof 48288	A function of order G(x) is a function. (Contributed by AV, 18-May-2020.)
⊢ (𝐹 ∈ (Ο‘𝐺) → 𝐹:dom 𝐹⟶ℝ)
Theorem	elbigodm 48289	The domain of a function of order G(x) is a subset of the reals. (Contributed by AV, 18-May-2020.)
⊢ (𝐹 ∈ (Ο‘𝐺) → dom 𝐹 ⊆ ℝ)
Theorem	elbigoimp 48290*	The defining property of a function of order G(x). (Contributed by AV, 18-May-2020.)
⊢ ((𝐹 ∈ (Ο‘𝐺) ∧ 𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ dom 𝐺) → ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝑚 · (𝐺‘𝑦))))
Theorem	elbigolo1 48291	A function (into the positive reals) is of order G(x) iff the quotient of the function and G(x) (also a function into the positive reals) is an eventually upper bounded function. (Contributed by AV, 20-May-2020.) (Proof shortened by II, 16-Feb-2023.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) → (𝐹 ∈ (Ο‘𝐺) ↔ (𝐹 /f 𝐺) ∈ ≤𝑂(1)))
21.48.21.7  Logarithm to an arbitrary base (extension)
Theorem	rege1logbrege0 48292	The general logarithm, with a real base greater than 1, for a real number greater than or equal to 1 is greater than or equal to 0. (Contributed by AV, 25-May-2020.)
⊢ ((𝐵 ∈ (1(,)+∞) ∧ 𝑋 ∈ (1[,)+∞)) → 0 ≤ (𝐵 logb 𝑋))
Theorem	rege1logbzge0 48293	The general logarithm, with an integer base greater than 1, for a real number greater than or equal to 1 is greater than or equal to 0. (Contributed by AV, 25-May-2020.)
⊢ ((𝐵 ∈ (ℤ≥‘2) ∧ 𝑋 ∈ (1[,)+∞)) → 0 ≤ (𝐵 logb 𝑋))
Theorem	fllogbd 48294	A real number is between the base of a logarithm to the power of the floor of the logarithm of the number and the base of the logarithm to the power of the floor of the logarithm of the number plus one. (Contributed by AV, 23-May-2020.)
⊢ (𝜑 → 𝐵 ∈ (ℤ≥‘2))    &   ⊢ (𝜑 → 𝑋 ∈ ℝ+)    &   ⊢ 𝐸 = (⌊‘(𝐵 logb 𝑋))    ⇒   ⊢ (𝜑 → ((𝐵↑𝐸) ≤ 𝑋 ∧ 𝑋 < (𝐵↑(𝐸 + 1))))
Theorem	relogbmulbexp 48295	The logarithm of the product of a positive real number and the base to the power of a real number is the logarithm of the positive real number plus the real number. (Contributed by AV, 29-May-2020.)
⊢ ((𝐵 ∈ (ℝ+ ∖ {1}) ∧ (𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ)) → (𝐵 logb (𝐴 · (𝐵↑𝑐𝐶))) = ((𝐵 logb 𝐴) + 𝐶))
Theorem	relogbdivb 48296	The logarithm of the quotient of a positive real number and the base is the logarithm of the number minus 1. (Contributed by AV, 29-May-2020.)
⊢ ((𝐵 ∈ (ℝ+ ∖ {1}) ∧ 𝐴 ∈ ℝ+) → (𝐵 logb (𝐴 / 𝐵)) = ((𝐵 logb 𝐴) − 1))
Theorem	logbge0b 48297	The logarithm of a number is nonnegative iff the number is greater than or equal to 1. (Contributed by AV, 30-May-2020.)
⊢ ((𝐵 ∈ (ℤ≥‘2) ∧ 𝑋 ∈ ℝ+) → (0 ≤ (𝐵 logb 𝑋) ↔ 1 ≤ 𝑋))
Theorem	logblt1b 48298	The logarithm of a number is less than 1 iff the number is less than the base of the logarithm. (Contributed by AV, 30-May-2020.)
⊢ ((𝐵 ∈ (ℤ≥‘2) ∧ 𝑋 ∈ ℝ+) → ((𝐵 logb 𝑋) < 1 ↔ 𝑋 < 𝐵))
21.48.21.8  The binary logarithm If the binary logarithm is used more often, a separate symbol/definition could be provided for it, e.g., log2 = (𝑥 ∈ (ℂ ∖ {0}) ↦ (2 logb 𝑋)). Then we can write "( log2 ` x )" (analogous to (log𝑥) for the natural logarithm) instead of (2 logb 𝑥).
Theorem	fldivexpfllog2 48299	The floor of a positive real number divided by 2 to the power of the floor of the logarithm to base 2 of the number is 1. (Contributed by AV, 26-May-2020.)
⊢ (𝑋 ∈ ℝ+ → (⌊‘(𝑋 / (2↑(⌊‘(2 logb 𝑋))))) = 1)
Theorem	nnlog2ge0lt1 48300	A positive integer is 1 iff its binary logarithm is between 0 and 1. (Contributed by AV, 30-May-2020.)
⊢ (𝑁 ∈ ℕ → (𝑁 = 1 ↔ (0 ≤ (2 logb 𝑁) ∧ (2 logb 𝑁) < 1)))