P. 335 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 33401-33500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	tan2h 33401	Half-angle rule for tangent. (Contributed by Brendan Leahy, 4-Aug-2018.)
⊢ (𝐴 ∈ (0[,)π) → (tan‘(𝐴 / 2)) = (√‘((1 − (cos‘𝐴)) / (1 + (cos‘𝐴)))))
Theorem	pigt3 33402	π is greater than 3. (Contributed by Brendan Leahy, 21-Aug-2020.)
⊢ 3 < π
Theorem	lindsdom 33403	A linearly independent set in a free linear module of finite dimension over a division ring is smaller than the dimension of the module. (Contributed by Brendan Leahy, 2-Jun-2021.)
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) → 𝑋 ≼ 𝐼)
Theorem	lindsenlbs 33404	A maximal linearly independent set in a free module of finite dimension over a division ring is a basis. (Contributed by Brendan Leahy, 2-Jun-2021.)
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ 𝑋 ≈ 𝐼) → 𝑋 ∈ (LBasis‘(𝑅 freeLMod 𝐼)))
Theorem	matunitlindflem1 33405	One direction of matunitlindf 33407. (Contributed by Brendan Leahy, 2-Jun-2021.)
⊢ (((𝑅 ∈ Field ∧ 𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝐼 ∈ (Fin ∖ {∅})) → (¬ curry 𝑀 LIndF (𝑅 freeLMod 𝐼) → ((𝐼 maDet 𝑅)‘𝑀) = (0g‘𝑅)))
Theorem	matunitlindflem2 33406	One direction of matunitlindf 33407. (Contributed by Brendan Leahy, 2-Jun-2021.)
⊢ ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅))
Theorem	matunitlindf 33407	A matrix over a field is invertible iff the rows are linearly independent. (Contributed by Brendan Leahy, 2-Jun-2021.)
⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (𝑀 ∈ (Unit‘(𝐼 Mat 𝑅)) ↔ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)))
Theorem	ptrest 33408*	Expressing a restriction of a product topology as a product topology. (Contributed by Brendan Leahy, 24-Mar-2019.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶Top)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑆 ∈ 𝑊)    ⇒   ⊢ (𝜑 → ((∏t‘𝐹) ↾t X𝑘 ∈ 𝐴 𝑆) = (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))))
Theorem	ptrecube 33409*	Any point in an open set of N-space is surrounded by an open cube within that set. (Contributed by Brendan Leahy, 21-Aug-2020.) (Proof shortened by AV, 28-Sep-2020.)
⊢ 𝑅 = (∏t‘((1...𝑁) × {(topGen‘ran (,))}))    &   ⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ))    ⇒   ⊢ ((𝑆 ∈ 𝑅 ∧ 𝑃 ∈ 𝑆) → ∃𝑑 ∈ ℝ+ X𝑛 ∈ (1...𝑁)((𝑃‘𝑛)(ball‘𝐷)𝑑) ⊆ 𝑆)
Theorem	poimirlem1 33410*	Lemma for poimir 33442- the vertices on either side of a skipped vertex differ in at least two dimensions. (Contributed by Brendan Leahy, 21-Aug-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))))    &   ⊢ (𝜑 → 𝑇:(1...𝑁)⟶ℤ)    &   ⊢ (𝜑 → 𝑈:(1...𝑁)–1-1-onto→(1...𝑁))    &   ⊢ (𝜑 → 𝑀 ∈ (1...(𝑁 − 1)))    ⇒   ⊢ (𝜑 → ¬ ∃*𝑛 ∈ (1...𝑁)((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛))
Theorem	poimirlem2 33411*	Lemma for poimir 33442- consecutive vertices differ in at most one dimension. (Contributed by Brendan Leahy, 21-Aug-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))))    &   ⊢ (𝜑 → 𝑇:(1...𝑁)⟶ℤ)    &   ⊢ (𝜑 → 𝑈:(1...𝑁)–1-1-onto→(1...𝑁))    &   ⊢ (𝜑 → 𝑉 ∈ (1...(𝑁 − 1)))    &   ⊢ (𝜑 → 𝑀 ∈ ((0...𝑁) ∖ {𝑉}))    ⇒   ⊢ (𝜑 → ∃*𝑛 ∈ (1...𝑁)((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛))
Theorem	poimirlem3 33412*	Lemma for poimir 33442 to add an interior point to an admissible face on the back face of the cube. (Contributed by Brendan Leahy, 21-Aug-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑀 < 𝑁)    &   ⊢ (𝜑 → 𝑇:(1...𝑀)⟶(0..^𝐾))    &   ⊢ (𝜑 → 𝑈:(1...𝑀)–1-1-onto→(1...𝑀))    ⇒   ⊢ (𝜑 → (∀𝑖 ∈ (0...𝑀)∃𝑗 ∈ (0...𝑀)𝑖 = ⦋((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) / 𝑝⦌𝐵 → (⟨(𝑇 ∪ {⟨(𝑀 + 1), 0⟩}), (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩})⟩ ∈ (((0..^𝐾) ↑𝑚 (1...(𝑀 + 1))) × {𝑓 ∣ 𝑓:(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1))}) ∧ (∀𝑖 ∈ (0...𝑀)∃𝑗 ∈ (0...𝑀)𝑖 = ⦋(((𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) ∘𝑓 + ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) / 𝑝⦌𝐵 ∧ ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘(𝑀 + 1)) = 0 ∧ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩})‘(𝑀 + 1)) = (𝑀 + 1)))))
Theorem	poimirlem4 33413*	Lemma for poimir 33442 connecting the admissible faces on the back face of the (𝑀 + 1)-cube to admissible simplices in the 𝑀-cube. (Contributed by Brendan Leahy, 21-Aug-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑀 < 𝑁)    ⇒   ⊢ (𝜑 → {𝑠 ∈ (((0..^𝐾) ↑𝑚 (1...𝑀)) × {𝑓 ∣ 𝑓:(1...𝑀)–1-1-onto→(1...𝑀)}) ∣ ∀𝑖 ∈ (0...𝑀)∃𝑗 ∈ (0...𝑀)𝑖 = ⦋(((1st ‘𝑠) ∘𝑓 + ((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd ‘𝑠) “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) / 𝑝⦌𝐵} ≈ {𝑠 ∈ (((0..^𝐾) ↑𝑚 (1...(𝑀 + 1))) × {𝑓 ∣ 𝑓:(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1))}) ∣ (∀𝑖 ∈ (0...𝑀)∃𝑗 ∈ (0...𝑀)𝑖 = ⦋(((1st ‘𝑠) ∘𝑓 + ((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd ‘𝑠) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) / 𝑝⦌𝐵 ∧ ((1st ‘𝑠)‘(𝑀 + 1)) = 0 ∧ ((2nd ‘𝑠)‘(𝑀 + 1)) = (𝑀 + 1))})
Theorem	poimirlem5 33414*	Lemma for poimir 33442 to establish that, for the simplices defined by a walk along the edges of an 𝑁-cube, if the starting vertex is not opposite a given face, it is the earliest vertex of the face on the walk. (Contributed by Brendan Leahy, 21-Aug-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘𝑓 + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → 0 < (2nd ‘𝑇))    ⇒   ⊢ (𝜑 → (𝐹‘0) = (1st ‘(1st ‘𝑇)))
Theorem	poimirlem6 33415*	Lemma for poimir 33442 establishing, for a face of a simplex defined by a walk along the edges of an 𝑁-cube, the single dimension in which successive vertices before the opposite vertex differ. (Contributed by Brendan Leahy, 21-Aug-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘𝑓 + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → (2nd ‘𝑇) ∈ (1...(𝑁 − 1)))    &   ⊢ (𝜑 → 𝑀 ∈ (1...((2nd ‘𝑇) − 1)))    ⇒   ⊢ (𝜑 → (℩𝑛 ∈ (1...𝑁)((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛)) = ((2nd ‘(1st ‘𝑇))‘𝑀))
Theorem	poimirlem7 33416*	Lemma for poimir 33442, similar to poimirlem6 33415, but for vertices after the opposite vertex. (Contributed by Brendan Leahy, 21-Aug-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘𝑓 + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → (2nd ‘𝑇) ∈ (1...(𝑁 − 1)))    &   ⊢ (𝜑 → 𝑀 ∈ ((((2nd ‘𝑇) + 1) + 1)...𝑁))    ⇒   ⊢ (𝜑 → (℩𝑛 ∈ (1...𝑁)((𝐹‘(𝑀 − 2))‘𝑛) ≠ ((𝐹‘(𝑀 − 1))‘𝑛)) = ((2nd ‘(1st ‘𝑇))‘𝑀))
Theorem	poimirlem8 33417*	Lemma for poimir 33442, establishing that away from the opposite vertex the walks in poimirlem9 33418 yield the same vertices. (Contributed by Brendan Leahy, 21-Aug-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘𝑓 + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → (2nd ‘𝑇) ∈ (1...(𝑁 − 1)))    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    ⇒   ⊢ (𝜑 → ((2nd ‘(1st ‘𝑈)) ↾ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})) = ((2nd ‘(1st ‘𝑇)) ↾ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})))
Theorem	poimirlem9 33418*	Lemma for poimir 33442, establishing the two walks that yield a given face when the opposite vertex is neither first nor last. (Contributed by Brendan Leahy, 21-Aug-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘𝑓 + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → (2nd ‘𝑇) ∈ (1...(𝑁 − 1)))    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → (2nd ‘(1st ‘𝑈)) ≠ (2nd ‘(1st ‘𝑇)))    ⇒   ⊢ (𝜑 → (2nd ‘(1st ‘𝑈)) = ((2nd ‘(1st ‘𝑇)) ∘ ({⟨(2nd ‘𝑇), ((2nd ‘𝑇) + 1)⟩, ⟨((2nd ‘𝑇) + 1), (2nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})))))
Theorem	poimirlem10 33419*	Lemma for poimir 33442 establishing the cube that yields the simplex that yields a face if the opposite vertex was first on the walk. (Contributed by Brendan Leahy, 21-Aug-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘𝑓 + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}    &   ⊢ (𝜑 → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑𝑚 (1...𝑁)))    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → (2nd ‘𝑇) = 0)    ⇒   ⊢ (𝜑 → ((𝐹‘(𝑁 − 1)) ∘𝑓 − ((1...𝑁) × {1})) = (1st ‘(1st ‘𝑇)))
Theorem	poimirlem11 33420*	Lemma for poimir 33442 connecting walks that could yield from a given cube a given face opposite the first vertex of the walk. (Contributed by Brendan Leahy, 21-Aug-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘𝑓 + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}    &   ⊢ (𝜑 → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑𝑚 (1...𝑁)))    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → (2nd ‘𝑇) = 0)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → (2nd ‘𝑈) = 0)    &   ⊢ (𝜑 → 𝑀 ∈ (1...𝑁))    ⇒   ⊢ (𝜑 → ((2nd ‘(1st ‘𝑇)) “ (1...𝑀)) ⊆ ((2nd ‘(1st ‘𝑈)) “ (1...𝑀)))
Theorem	poimirlem12 33421*	Lemma for poimir 33442 connecting walks that could yield from a given cube a given face opposite the final vertex of the walk. (Contributed by Brendan Leahy, 21-Aug-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘𝑓 + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}    &   ⊢ (𝜑 → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑𝑚 (1...𝑁)))    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → (2nd ‘𝑇) = 𝑁)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → (2nd ‘𝑈) = 𝑁)    &   ⊢ (𝜑 → 𝑀 ∈ (0...(𝑁 − 1)))    ⇒   ⊢ (𝜑 → ((2nd ‘(1st ‘𝑇)) “ (1...𝑀)) ⊆ ((2nd ‘(1st ‘𝑈)) “ (1...𝑀)))
Theorem	poimirlem13 33422*	Lemma for poimir 33442- for at most one simplex associated with a shared face is the opposite vertex first on the walk. (Contributed by Brendan Leahy, 21-Aug-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘𝑓 + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}    &   ⊢ (𝜑 → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑𝑚 (1...𝑁)))    ⇒   ⊢ (𝜑 → ∃*𝑧 ∈ 𝑆 (2nd ‘𝑧) = 0)
Theorem	poimirlem14 33423*	Lemma for poimir 33442- for at most one simplex associated with a shared face is the opposite vertex last on the walk. (Contributed by Brendan Leahy, 21-Aug-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘𝑓 + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}    &   ⊢ (𝜑 → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑𝑚 (1...𝑁)))    ⇒   ⊢ (𝜑 → ∃*𝑧 ∈ 𝑆 (2nd ‘𝑧) = 𝑁)
Theorem	poimirlem15 33424*	Lemma for poimir 33442, that the face in poimirlem22 33431 is a face. (Contributed by Brendan Leahy, 21-Aug-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘𝑓 + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}    &   ⊢ (𝜑 → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑𝑚 (1...𝑁)))    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → (2nd ‘𝑇) ∈ (1...(𝑁 − 1)))    ⇒   ⊢ (𝜑 → ⟨⟨(1st ‘(1st ‘𝑇)), ((2nd ‘(1st ‘𝑇)) ∘ ({⟨(2nd ‘𝑇), ((2nd ‘𝑇) + 1)⟩, ⟨((2nd ‘𝑇) + 1), (2nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}))))⟩, (2nd ‘𝑇)⟩ ∈ 𝑆)
Theorem	poimirlem16 33425*	Lemma for poimir 33442 establishing the vertices of the simplex of poimirlem17 33426. (Contributed by Brendan Leahy, 21-Aug-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘𝑓 + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}    &   ⊢ (𝜑 → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑𝑚 (1...𝑁)))    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 𝐾)    &   ⊢ (𝜑 → (2nd ‘𝑇) = 0)    ⇒   ⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ((𝑛 ∈ (1...𝑁) ↦ (((1st ‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st ‘𝑇))‘1), 1, 0))) ∘𝑓 + (((((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0})))))
Theorem	poimirlem17 33426*	Lemma for poimir 33442 establishing existence for poimirlem18 33427. (Contributed by Brendan Leahy, 21-Aug-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘𝑓 + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}    &   ⊢ (𝜑 → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑𝑚 (1...𝑁)))    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 𝐾)    &   ⊢ (𝜑 → (2nd ‘𝑇) = 0)    ⇒   ⊢ (𝜑 → ∃𝑧 ∈ 𝑆 𝑧 ≠ 𝑇)
Theorem	poimirlem18 33427*	Lemma for poimir 33442 stating that, given a face not on a front face of the main cube and a simplex in which it's opposite the first vertex on the walk, there exists exactly one other simplex containing it. (Contributed by Brendan Leahy, 21-Aug-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘𝑓 + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}    &   ⊢ (𝜑 → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑𝑚 (1...𝑁)))    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 𝐾)    &   ⊢ (𝜑 → (2nd ‘𝑇) = 0)    ⇒   ⊢ (𝜑 → ∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇)
Theorem	poimirlem19 33428*	Lemma for poimir 33442 establishing the vertices of the simplex in poimirlem20 33429. (Contributed by Brendan Leahy, 21-Aug-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘𝑓 + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}    &   ⊢ (𝜑 → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑𝑚 (1...𝑁)))    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 0)    &   ⊢ (𝜑 → (2nd ‘𝑇) = 𝑁)    ⇒   ⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ((𝑛 ∈ (1...𝑁) ↦ (((1st ‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st ‘𝑇))‘𝑁), 1, 0))) ∘𝑓 + (((((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0})))))
Theorem	poimirlem20 33429*	Lemma for poimir 33442 establishing existence for poimirlem21 33430. (Contributed by Brendan Leahy, 21-Aug-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘𝑓 + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}    &   ⊢ (𝜑 → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑𝑚 (1...𝑁)))    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 0)    &   ⊢ (𝜑 → (2nd ‘𝑇) = 𝑁)    ⇒   ⊢ (𝜑 → ∃𝑧 ∈ 𝑆 𝑧 ≠ 𝑇)
Theorem	poimirlem21 33430*	Lemma for poimir 33442 stating that, given a face not on a back face of the cube and a simplex in which it's opposite the final point of the walk, there exists exactly one other simplex containing it. (Contributed by Brendan Leahy, 21-Aug-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘𝑓 + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}    &   ⊢ (𝜑 → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑𝑚 (1...𝑁)))    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 0)    &   ⊢ (𝜑 → (2nd ‘𝑇) = 𝑁)    ⇒   ⊢ (𝜑 → ∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇)
Theorem	poimirlem22 33431*	Lemma for poimir 33442, that a given face belongs to exactly two simplices, provided it's not on the boundary of the cube. (Contributed by Brendan Leahy, 21-Aug-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘𝑓 + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}    &   ⊢ (𝜑 → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑𝑚 (1...𝑁)))    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 0)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 𝐾)    ⇒   ⊢ (𝜑 → ∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇)
Theorem	poimirlem23 33432*	Lemma for poimir 33442, two ways of expressing the property that a face is not on the back face of the cube. (Contributed by Brendan Leahy, 21-Aug-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑇:(1...𝑁)⟶(0..^𝐾))    &   ⊢ (𝜑 → 𝑈:(1...𝑁)–1-1-onto→(1...𝑁))    &   ⊢ (𝜑 → 𝑉 ∈ (0...𝑁))    ⇒   ⊢ (𝜑 → (∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))(𝑝‘𝑁) ≠ 0 ↔ ¬ (𝑉 = 𝑁 ∧ ((𝑇‘𝑁) = 0 ∧ (𝑈‘𝑁) = 𝑁))))
Theorem	poimirlem24 33433*	Lemma for poimir 33442, two ways of expressing that a simplex has an admissible face on the back face of the cube. (Contributed by Brendan Leahy, 21-Aug-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝑝 = ((1st ‘𝑠) ∘𝑓 + ((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd ‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → 𝐵 = 𝐶)    &   ⊢ ((𝜑 ∧ 𝑝:(1...𝑁)⟶(0...𝐾)) → 𝐵 ∈ (0...𝑁))    &   ⊢ (𝜑 → 𝑇:(1...𝑁)⟶(0..^𝐾))    &   ⊢ (𝜑 → 𝑈:(1...𝑁)–1-1-onto→(1...𝑁))    &   ⊢ (𝜑 → 𝑉 ∈ (0...𝑁))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ (((0...𝐾) ↑𝑚 (1...𝑁)) ↑𝑚 (0...(𝑁 − 1)))(𝑥 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ∧ ((0...(𝑁 − 1)) ⊆ ran (𝑝 ∈ ran 𝑥 ↦ 𝐵) ∧ ∃𝑝 ∈ ran 𝑥(𝑝‘𝑁) ≠ 0)) ↔ (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑉})𝑖 = ⦋⟨𝑇, 𝑈⟩ / 𝑠⦌𝐶 ∧ ¬ (𝑉 = 𝑁 ∧ ((𝑇‘𝑁) = 0 ∧ (𝑈‘𝑁) = 𝑁)))))
Theorem	poimirlem25 33434*	Lemma for poimir 33442 stating that for a given simplex such that no vertex maps to 𝑁, the number of admissible faces is even. (Contributed by Brendan Leahy, 21-Aug-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝑝 = ((1st ‘𝑠) ∘𝑓 + ((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd ‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → 𝐵 = 𝐶)    &   ⊢ ((𝜑 ∧ 𝑝:(1...𝑁)⟶(0...𝐾)) → 𝐵 ∈ (0...𝑁))    &   ⊢ (𝜑 → 𝑇:(1...𝑁)⟶(0..^𝐾))    &   ⊢ (𝜑 → 𝑈:(1...𝑁)–1-1-onto→(1...𝑁))    &   ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝑁 ≠ ⦋⟨𝑇, 𝑈⟩ / 𝑠⦌𝐶)    ⇒   ⊢ (𝜑 → 2 ∥ (#‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋⟨𝑇, 𝑈⟩ / 𝑠⦌𝐶}))
Theorem	poimirlem26 33435*	Lemma for poimir 33442 showing an even difference between the number of admissible faces and the number of admissible simplices. Equation (6) of [Kulpa] p. 548. (Contributed by Brendan Leahy, 21-Aug-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝑝 = ((1st ‘𝑠) ∘𝑓 + ((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd ‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → 𝐵 = 𝐶)    &   ⊢ ((𝜑 ∧ 𝑝:(1...𝑁)⟶(0...𝐾)) → 𝐵 ∈ (0...𝑁))    ⇒   ⊢ (𝜑 → 2 ∥ ((#‘{𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {(2nd ‘𝑡)})𝑖 = ⦋(1st ‘𝑡) / 𝑠⦌𝐶}) − (#‘{𝑠 ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∣ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = 𝐶})))
Theorem	poimirlem27 33436*	Lemma for poimir 33442 showing that the difference between admissible faces in the whole cube and admissible faces on the back face is even. Equation (7) of [Kulpa] p. 548. (Contributed by Brendan Leahy, 21-Aug-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝑝 = ((1st ‘𝑠) ∘𝑓 + ((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd ‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → 𝐵 = 𝐶)    &   ⊢ ((𝜑 ∧ 𝑝:(1...𝑁)⟶(0...𝐾)) → 𝐵 ∈ (0...𝑁))    &   ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝐾) ∧ (𝑝‘𝑛) = 0)) → 𝐵 < 𝑛)    &   ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝐾) ∧ (𝑝‘𝑛) = 𝐾)) → 𝐵 ≠ (𝑛 − 1))    ⇒   ⊢ (𝜑 → 2 ∥ ((#‘{𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {(2nd ‘𝑡)})𝑖 = ⦋(1st ‘𝑡) / 𝑠⦌𝐶}) − (#‘{𝑠 ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∣ (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ (0...(𝑁 − 1))𝑖 = 𝐶 ∧ ((1st ‘𝑠)‘𝑁) = 0 ∧ ((2nd ‘𝑠)‘𝑁) = 𝑁)})))
Theorem	poimirlem28 33437*	Lemma for poimir 33442, a variant of Sperner's lemma. (Contributed by Brendan Leahy, 21-Aug-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝑝 = ((1st ‘𝑠) ∘𝑓 + ((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd ‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → 𝐵 = 𝐶)    &   ⊢ ((𝜑 ∧ 𝑝:(1...𝑁)⟶(0...𝐾)) → 𝐵 ∈ (0...𝑁))    &   ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝐾) ∧ (𝑝‘𝑛) = 0)) → 𝐵 < 𝑛)    &   ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝐾) ∧ (𝑝‘𝑛) = 𝐾)) → 𝐵 ≠ (𝑛 − 1))    &   ⊢ (𝜑 → 𝐾 ∈ ℕ)    ⇒   ⊢ (𝜑 → ∃𝑠 ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = 𝐶)
Theorem	poimirlem29 33438*	Lemma for poimir 33442 connecting cubes of the tessellation to neighborhoods. (Contributed by Brendan Leahy, 21-Aug-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐼 = ((0[,]1) ↑𝑚 (1...𝑁))    &   ⊢ 𝑅 = (∏t‘((1...𝑁) × {(topGen‘ran (,))}))    &   ⊢ (𝜑 → 𝐹 ∈ ((𝑅 ↾t 𝐼) Cn 𝑅))    &   ⊢ 𝑋 = ((𝐹‘(((1st ‘(𝐺‘𝑘)) ∘𝑓 + ((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)    &   ⊢ (𝜑 → 𝐺:ℕ⟶((ℕ0 ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ran (1st ‘(𝐺‘𝑘)) ⊆ (0..^𝑘))    &   ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁) ∧ 𝑟 ∈ { ≤ , ◡ ≤ })) → ∃𝑗 ∈ (0...𝑁)0𝑟𝑋)    ⇒   ⊢ (𝜑 → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → ∀𝑛 ∈ (1...𝑁)∀𝑣 ∈ (𝑅 ↾t 𝐼)(𝐶 ∈ 𝑣 → ∀𝑟 ∈ { ≤ , ◡ ≤ }∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛))))
Theorem	poimirlem30 33439*	Lemma for poimir 33442 combining poimirlem29 33438 with bwth 21213. (Contributed by Brendan Leahy, 21-Aug-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐼 = ((0[,]1) ↑𝑚 (1...𝑁))    &   ⊢ 𝑅 = (∏t‘((1...𝑁) × {(topGen‘ran (,))}))    &   ⊢ (𝜑 → 𝐹 ∈ ((𝑅 ↾t 𝐼) Cn 𝑅))    &   ⊢ 𝑋 = ((𝐹‘(((1st ‘(𝐺‘𝑘)) ∘𝑓 + ((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)    &   ⊢ (𝜑 → 𝐺:ℕ⟶((ℕ0 ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ran (1st ‘(𝐺‘𝑘)) ⊆ (0..^𝑘))    &   ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁) ∧ 𝑟 ∈ { ≤ , ◡ ≤ })) → ∃𝑗 ∈ (0...𝑁)0𝑟𝑋)    ⇒   ⊢ (𝜑 → ∃𝑐 ∈ 𝐼 ∀𝑛 ∈ (1...𝑁)∀𝑣 ∈ (𝑅 ↾t 𝐼)(𝑐 ∈ 𝑣 → ∀𝑟 ∈ { ≤ , ◡ ≤ }∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛)))
Theorem	poimirlem31 33440*	Lemma for poimir 33442, assigning values to the vertices of the tessellation that meet the hypotheses of both poimirlem30 33439 and poimirlem28 33437. Equation (2) of [Kulpa] p. 547. (Contributed by Brendan Leahy, 21-Aug-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐼 = ((0[,]1) ↑𝑚 (1...𝑁))    &   ⊢ 𝑅 = (∏t‘((1...𝑁) × {(topGen‘ran (,))}))    &   ⊢ (𝜑 → 𝐹 ∈ ((𝑅 ↾t 𝐼) Cn 𝑅))    &   ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 0)) → ((𝐹‘𝑧)‘𝑛) ≤ 0)    &   ⊢ 𝑃 = ((1st ‘(𝐺‘𝑘)) ∘𝑓 + ((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))    &   ⊢ (𝜑 → 𝐺:ℕ⟶((ℕ0 ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ran (1st ‘(𝐺‘𝑘)) ⊆ (0..^𝑘))    &   ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑖 ∈ (0...𝑁))) → ∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ))    ⇒   ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁) ∧ 𝑟 ∈ { ≤ , ◡ ≤ })) → ∃𝑗 ∈ (0...𝑁)0𝑟((𝐹‘(𝑃 ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑛))
Theorem	poimirlem32 33441*	Lemma for poimir 33442, combining poimirlem28 33437, poimirlem30 33439, and poimirlem31 33440 to get Equation (1) of [Kulpa] p. 547. (Contributed by Brendan Leahy, 21-Aug-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐼 = ((0[,]1) ↑𝑚 (1...𝑁))    &   ⊢ 𝑅 = (∏t‘((1...𝑁) × {(topGen‘ran (,))}))    &   ⊢ (𝜑 → 𝐹 ∈ ((𝑅 ↾t 𝐼) Cn 𝑅))    &   ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 0)) → ((𝐹‘𝑧)‘𝑛) ≤ 0)    &   ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 1)) → 0 ≤ ((𝐹‘𝑧)‘𝑛))    ⇒   ⊢ (𝜑 → ∃𝑐 ∈ 𝐼 ∀𝑛 ∈ (1...𝑁)∀𝑣 ∈ (𝑅 ↾t 𝐼)(𝑐 ∈ 𝑣 → ∀𝑟 ∈ { ≤ , ◡ ≤ }∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛)))
Theorem	poimir 33442*	Poincare-Miranda theorem. Theorem on [Kulpa] p. 547. (Contributed by Brendan Leahy, 21-Aug-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐼 = ((0[,]1) ↑𝑚 (1...𝑁))    &   ⊢ 𝑅 = (∏t‘((1...𝑁) × {(topGen‘ran (,))}))    &   ⊢ (𝜑 → 𝐹 ∈ ((𝑅 ↾t 𝐼) Cn 𝑅))    &   ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 0)) → ((𝐹‘𝑧)‘𝑛) ≤ 0)    &   ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 1)) → 0 ≤ ((𝐹‘𝑧)‘𝑛))    ⇒   ⊢ (𝜑 → ∃𝑐 ∈ 𝐼 (𝐹‘𝑐) = ((1...𝑁) × {0}))
Theorem	broucube 33443*	Brouwer - or as Kulpa calls it, "Bohl-Brouwer" - fixed point theorem for the unit cube. Theorem on [Kulpa] p. 548. (Contributed by Brendan Leahy, 21-Aug-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐼 = ((0[,]1) ↑𝑚 (1...𝑁))    &   ⊢ 𝑅 = (∏t‘((1...𝑁) × {(topGen‘ran (,))}))    &   ⊢ (𝜑 → 𝐹 ∈ ((𝑅 ↾t 𝐼) Cn (𝑅 ↾t 𝐼)))    ⇒   ⊢ (𝜑 → ∃𝑐 ∈ 𝐼 𝑐 = (𝐹‘𝑐))
Theorem	heicant 33444	Heine-Cantor theorem: a continuous mapping between metric spaces whose domain is compact is uniformly continuous. Theorem on [Rosenlicht] p. 80. (Contributed by Brendan Leahy, 13-Aug-2018.) (Proof shortened by AV, 27-Sep-2020.)
⊢ (𝜑 → 𝐶 ∈ (∞Met‘𝑋))    &   ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑌))    &   ⊢ (𝜑 → (MetOpen‘𝐶) ∈ Comp)    &   ⊢ (𝜑 → 𝑋 ≠ ∅)    &   ⊢ (𝜑 → 𝑌 ≠ ∅)    ⇒   ⊢ (𝜑 → ((metUnif‘𝐶) Cnu(metUnif‘𝐷)) = ((MetOpen‘𝐶) Cn (MetOpen‘𝐷)))
Theorem	opnmbllem0 33445*	Lemma for ismblfin 33450; could also be used to shorten proof of opnmbllem 23369. (Contributed by Brendan Leahy, 13-Jul-2018.)
⊢ (𝐴 ∈ (topGen‘ran (,)) → ∪ ([,] “ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴}) = 𝐴)
Theorem	mblfinlem1 33446*	Lemma for ismblfin 33450, ordering the sets of dyadic intervals that are antichains under subset and whose unions are contained entirely in 𝐴. (Contributed by Brendan Leahy, 13-Jul-2018.)
⊢ ((𝐴 ∈ (topGen‘ran (,)) ∧ 𝐴 ≠ ∅) → ∃𝑓 𝑓:ℕ–1-1-onto→{𝑎 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} ∣ ∀𝑐 ∈ {𝑏 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑏) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑐) → 𝑎 = 𝑐)})
Theorem	mblfinlem2 33447*	Lemma for ismblfin 33450, effectively one direction of the same fact for open sets, made necessary by Viaclovsky's slightly different defintion of outer measure. Note that unlike the main theorem, this holds for sets of infinite measure. (Contributed by Brendan Leahy, 21-Feb-2018.) (Revised by Brendan Leahy, 13-Jul-2018.)
⊢ ((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑀 ∈ ℝ ∧ 𝑀 < (vol*‘𝐴)) → ∃𝑠 ∈ (Clsd‘(topGen‘ran (,)))(𝑠 ⊆ 𝐴 ∧ 𝑀 < (vol*‘𝑠)))
Theorem	mblfinlem3 33448*	The difference between two sets measurable by the criterion in ismblfin 33450 is itself measurable by the same. Corollary 0.3 of [Viaclovsky7] p. 3. (Contributed by Brendan Leahy, 25-Mar-2018.) (Revised by Brendan Leahy, 13-Jul-2018.)
⊢ (((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) ∈ ℝ) ∧ ((vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < ) ∧ (vol*‘𝐵) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐵 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < ))) → sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ (𝐴 ∖ 𝐵) ∧ 𝑦 = (vol‘𝑏))}, ℝ, < ) = (vol*‘(𝐴 ∖ 𝐵)))
Theorem	mblfinlem4 33449*	Backward direction of ismblfin 33450. (Contributed by Brendan Leahy, 28-Mar-2018.) (Revised by Brendan Leahy, 13-Jul-2018.)
⊢ (((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ 𝐴 ∈ dom vol) → (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < ))
Theorem	ismblfin 33450*	Measurability in terms of inner and outer measure. Proposition 7 of [Viaclovsky8] p. 3. (Contributed by Brendan Leahy, 4-Mar-2018.) (Revised by Brendan Leahy, 28-Mar-2018.)
⊢ ((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) → (𝐴 ∈ dom vol ↔ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )))
Theorem	ovoliunnfl 33451*	ovoliun 23273 is incompatible with the Feferman-Levy model. (Contributed by Brendan Leahy, 21-Nov-2017.)
⊢ ((𝑓 Fn ℕ ∧ ∀𝑛 ∈ ℕ ((𝑓‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑓‘𝑛)) ∈ ℝ)) → (vol*‘∪ 𝑚 ∈ ℕ (𝑓‘𝑚)) ≤ sup(ran seq1( + , (𝑚 ∈ ℕ ↦ (vol*‘(𝑓‘𝑚)))), ℝ*, < ))    ⇒   ⊢ ((𝐴 ≼ ℕ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) → ∪ 𝐴 ≠ ℝ)
Theorem	ex-ovoliunnfl 33452*	Demonstration of ovoliunnfl 33451. (Contributed by Brendan Leahy, 21-Nov-2017.)
⊢ ((𝐴 ≼ ℕ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) → ∪ 𝐴 ≠ ℝ)
Theorem	voliunnfl 33453*	voliun 23322 is incompatible with the Feferman-Levy model; in that model, therefore, the Lebesgue measure as we've defined it isn't actually a measure. (Contributed by Brendan Leahy, 16-Dec-2017.)
⊢ 𝑆 = seq1( + , 𝐺)    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛)))    &   ⊢ ((∀𝑛 ∈ ℕ ((𝑓‘𝑛) ∈ dom vol ∧ (vol‘(𝑓‘𝑛)) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ (𝑓‘𝑛)) → (vol‘∪ 𝑛 ∈ ℕ (𝑓‘𝑛)) = sup(ran 𝑆, ℝ*, < ))    ⇒   ⊢ ((𝐴 ≼ ℕ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) → ∪ 𝐴 ≠ ℝ)
Theorem	volsupnfl 33454*	volsup 23324 is incompatible with the Feferman-Levy model. (Contributed by Brendan Leahy, 2-Jan-2018.)
⊢ ((𝑓:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ⊆ (𝑓‘(𝑛 + 1))) → (vol‘∪ ran 𝑓) = sup((vol “ ran 𝑓), ℝ*, < ))    ⇒   ⊢ ((𝐴 ≼ ℕ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) → ∪ 𝐴 ≠ ℝ)
Theorem	0mbf 33455	The empty function is measurable. (Contributed by Brendan Leahy, 28-Mar-2018.)
⊢ ∅ ∈ MblFn
Theorem	mbfresfi 33456*	Measurability of a piecewise function across arbitrarily many subsets. (Contributed by Brendan Leahy, 31-Mar-2018.)
⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝑆 ∈ Fin)    &   ⊢ (𝜑 → ∀𝑠 ∈ 𝑆 (𝐹 ↾ 𝑠) ∈ MblFn)    &   ⊢ (𝜑 → ∪ 𝑆 = 𝐴)    ⇒   ⊢ (𝜑 → 𝐹 ∈ MblFn)
Theorem	mbfposadd 33457*	If the sum of two measurable functions is measurable, the sum of their nonnegative parts is measurable. (Contributed by Brendan Leahy, 2-Apr-2018.)
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∈ MblFn)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ∈ MblFn)
Theorem	cnambfre 33458	A real-valued, a.e. continuous function is measurable. (Contributed by Brendan Leahy, 4-Apr-2018.)
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol ∧ (vol*‘(𝐴 ∖ ((◡(((topGen‘ran (,)) ↾t 𝐴) CnP (topGen‘ran (,))) ∘ E ) “ {𝐹}))) = 0) → 𝐹 ∈ MblFn)
Theorem	dvtanlem 33459	Lemma for dvtan 33460- the domain of the tangent is open. (Contributed by Brendan Leahy, 8-Aug-2018.) (Proof shortened by OpenAI, 3-Jul-2020.)
⊢ (◡cos “ (ℂ ∖ {0})) ∈ (TopOpen‘ℂfld)
Theorem	dvtan 33460	Derivative of tangent. (Contributed by Brendan Leahy, 7-Aug-2018.)
⊢ (ℂ D tan) = (𝑥 ∈ dom tan ↦ ((cos‘𝑥)↑-2))
Theorem	itg2addnclem 33461*	An alternate expression for the ∫2 integral that includes an arbitrarily small but strictly positive "buffer zone" wherever the simple function is nonzero. (Contributed by Brendan Leahy, 10-Oct-2017.) (Revised by Brendan Leahy, 10-Mar-2018.)
⊢ 𝐿 = {𝑥 ∣ ∃𝑔 ∈ dom ∫1(∃𝑦 ∈ ℝ+ (𝑧 ∈ ℝ ↦ if((𝑔‘𝑧) = 0, 0, ((𝑔‘𝑧) + 𝑦))) ∘𝑟 ≤ 𝐹 ∧ 𝑥 = (∫1‘𝑔))}    ⇒   ⊢ (𝐹:ℝ⟶(0[,]+∞) → (∫2‘𝐹) = sup(𝐿, ℝ*, < ))
Theorem	itg2addnclem2 33462*	Lemma for itg2addnc 33464. The function described is a simple function. (Contributed by Brendan Leahy, 29-Oct-2017.)
⊢ (𝜑 → 𝐹 ∈ MblFn)    &   ⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞))    ⇒   ⊢ (((𝜑 ∧ ℎ ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹‘𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (ℎ‘𝑥) ∧ (ℎ‘𝑥) ≠ 0), (((⌊‘((𝐹‘𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (ℎ‘𝑥))) ∈ dom ∫1)
Theorem	itg2addnclem3 33463*	Lemma incomprehensible in isolation split off to shorten proof of itg2addnc 33464. (Contributed by Brendan Leahy, 11-Mar-2018.)
⊢ (𝜑 → 𝐹 ∈ MblFn)    &   ⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞))    &   ⊢ (𝜑 → (∫2‘𝐹) ∈ ℝ)    &   ⊢ (𝜑 → 𝐺:ℝ⟶(0[,)+∞))    &   ⊢ (𝜑 → (∫2‘𝐺) ∈ ℝ)    ⇒   ⊢ (𝜑 → (∃ℎ ∈ dom ∫1(∃𝑦 ∈ ℝ+ (𝑧 ∈ ℝ ↦ if((ℎ‘𝑧) = 0, 0, ((ℎ‘𝑧) + 𝑦))) ∘𝑟 ≤ (𝐹 ∘𝑓 + 𝐺) ∧ 𝑠 = (∫1‘ℎ)) → ∃𝑡∃𝑢(∃𝑓 ∈ dom ∫1∃𝑔 ∈ dom ∫1((∃𝑐 ∈ ℝ+ (𝑧 ∈ ℝ ↦ if((𝑓‘𝑧) = 0, 0, ((𝑓‘𝑧) + 𝑐))) ∘𝑟 ≤ 𝐹 ∧ 𝑡 = (∫1‘𝑓)) ∧ (∃𝑑 ∈ ℝ+ (𝑧 ∈ ℝ ↦ if((𝑔‘𝑧) = 0, 0, ((𝑔‘𝑧) + 𝑑))) ∘𝑟 ≤ 𝐺 ∧ 𝑢 = (∫1‘𝑔))) ∧ 𝑠 = (𝑡 + 𝑢))))
Theorem	itg2addnc 33464	Alternate proof of itg2add 23526 using the "buffer zone" definition from the first lemma, in which every simple function in the set is divided into to by dividing its buffer by a third and finding the largest allowable function locked to a grid laid out in increments of the new, smaller buffer up to the original simple function. The measurability of this function follows from that of the augend, and subtracting it from the original simple function yields another simple function by i1fsub 23475, which is allowable by the fact that the grid must have a mark between one third and two thirds the original buffer. This has two advantages over the current approach: first, eliminating ax-cc 9257, and second, weakening the measurability hypothesis to only the augend. (Contributed by Brendan Leahy, 31-Oct-2017.) (Revised by Brendan Leahy, 13-Mar-2018.)
⊢ (𝜑 → 𝐹 ∈ MblFn)    &   ⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞))    &   ⊢ (𝜑 → (∫2‘𝐹) ∈ ℝ)    &   ⊢ (𝜑 → 𝐺:ℝ⟶(0[,)+∞))    &   ⊢ (𝜑 → (∫2‘𝐺) ∈ ℝ)    ⇒   ⊢ (𝜑 → (∫2‘(𝐹 ∘𝑓 + 𝐺)) = ((∫2‘𝐹) + (∫2‘𝐺)))
Theorem	itg2gt0cn 33465*	itg2gt0 23527 holds on functions continuous on an open interval in the absence of ax-cc 9257. The fourth hypothesis is made unnecessary by the continuity hypothesis. (Contributed by Brendan Leahy, 16-Nov-2017.)
⊢ (𝜑 → 𝑋 < 𝑌)    &   ⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 0 < (𝐹‘𝑥))    &   ⊢ (𝜑 → (𝐹 ↾ (𝑋(,)𝑌)) ∈ ((𝑋(,)𝑌)–cn→ℂ))    ⇒   ⊢ (𝜑 → 0 < (∫2‘𝐹))
Theorem	ibladdnclem 33466*	Lemma for ibladdnc 33467; cf ibladdlem 23586, whose fifth hypothesis is rendered unnecessary by the weakened hypotheses of itg2addnc 33464. (Contributed by Brendan Leahy, 31-Oct-2017.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐷 = (𝐵 + 𝐶))    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn)    &   ⊢ (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))) ∈ ℝ)    &   ⊢ (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0))) ∈ ℝ)    ⇒   ⊢ (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0))) ∈ ℝ)
Theorem	ibladdnc 33467*	Choice-free analogue of itgadd 23591. A measurability hypothesis is necessitated by the loss of mbfadd 23428; for large classes of functions, such as continuous functions, it should be relatively easy to show. (Contributed by Brendan Leahy, 1-Nov-2017.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∈ MblFn)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∈ 𝐿1)
Theorem	itgaddnclem1 33468*	Lemma for itgaddnc 33470; cf. itgaddlem1 23589. (Contributed by Brendan Leahy, 7-Nov-2017.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∈ MblFn)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ 𝐶)    ⇒   ⊢ (𝜑 → ∫𝐴(𝐵 + 𝐶) d𝑥 = (∫𝐴𝐵 d𝑥 + ∫𝐴𝐶 d𝑥))
Theorem	itgaddnclem2 33469*	Lemma for itgaddnc 33470; cf. itgaddlem2 23590. (Contributed by Brendan Leahy, 10-Nov-2017.) (Revised by Brendan Leahy, 3-Apr-2018.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∈ MblFn)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → ∫𝐴(𝐵 + 𝐶) d𝑥 = (∫𝐴𝐵 d𝑥 + ∫𝐴𝐶 d𝑥))
Theorem	itgaddnc 33470*	Choice-free analogue of itgadd 23591. (Contributed by Brendan Leahy, 11-Nov-2017.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∈ MblFn)    ⇒   ⊢ (𝜑 → ∫𝐴(𝐵 + 𝐶) d𝑥 = (∫𝐴𝐵 d𝑥 + ∫𝐴𝐶 d𝑥))
Theorem	iblsubnc 33471*	Choice-free analogue of iblsub 23588. (Contributed by Brendan Leahy, 11-Nov-2017.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 − 𝐶)) ∈ MblFn)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 − 𝐶)) ∈ 𝐿1)
Theorem	itgsubnc 33472*	Choice-free analogue of itgsub 23592. (Contributed by Brendan Leahy, 11-Nov-2017.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 − 𝐶)) ∈ MblFn)    ⇒   ⊢ (𝜑 → ∫𝐴(𝐵 − 𝐶) d𝑥 = (∫𝐴𝐵 d𝑥 − ∫𝐴𝐶 d𝑥))
Theorem	iblabsnclem 33473*	Lemma for iblabsnc 33474; cf. iblabslem 23594. (Contributed by Brendan Leahy, 7-Nov-2017.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    &   ⊢ 𝐺 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(𝐹‘𝐵)), 0))    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐹‘𝐵)) ∈ 𝐿1)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝐵) ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐺 ∈ MblFn ∧ (∫2‘𝐺) ∈ ℝ))
Theorem	iblabsnc 33474*	Choice-free analogue of iblabs 23595. As with ibladdnc 33467, a measurability hypothesis is needed. (Contributed by Brendan Leahy, 7-Nov-2017.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (abs‘𝐵)) ∈ MblFn)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (abs‘𝐵)) ∈ 𝐿1)
Theorem	iblmulc2nc 33475*	Choice-free analogue of iblmulc2 23597. (Contributed by Brendan Leahy, 17-Nov-2017.)
⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ MblFn)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ 𝐿1)
Theorem	itgmulc2nclem1 33476*	Lemma for itgmulc2nc 33478; cf. itgmulc2lem1 23598. (Contributed by Brendan Leahy, 17-Nov-2017.)
⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ MblFn)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 · ∫𝐴𝐵 d𝑥) = ∫𝐴(𝐶 · 𝐵) d𝑥)
Theorem	itgmulc2nclem2 33477*	Lemma for itgmulc2nc 33478; cf. itgmulc2lem2 23599. (Contributed by Brendan Leahy, 19-Nov-2017.)
⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ MblFn)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐶 · ∫𝐴𝐵 d𝑥) = ∫𝐴(𝐶 · 𝐵) d𝑥)
Theorem	itgmulc2nc 33478*	Choice-free analogue of itgmulc2 23600. (Contributed by Brendan Leahy, 19-Nov-2017.)
⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ MblFn)    ⇒   ⊢ (𝜑 → (𝐶 · ∫𝐴𝐵 d𝑥) = ∫𝐴(𝐶 · 𝐵) d𝑥)
Theorem	itgabsnc 33479*	Choice-free analogue of itgabs 23601. (Contributed by Brendan Leahy, 19-Nov-2017.) (Revised by Brendan Leahy, 19-Jun-2018.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (abs‘𝐵)) ∈ MblFn)    &   ⊢ (𝜑 → (𝑦 ∈ 𝐴 ↦ ((∗‘∫𝐴𝐵 d𝑥) · ⦋𝑦 / 𝑥⦌𝐵)) ∈ MblFn)    ⇒   ⊢ (𝜑 → (abs‘∫𝐴𝐵 d𝑥) ≤ ∫𝐴(abs‘𝐵) d𝑥)
Theorem	bddiblnc 33480*	Choice-free proof of bddibl 23606. (Contributed by Brendan Leahy, 2-Nov-2017.) (Revised by Brendan Leahy, 6-Nov-2017.)
⊢ ((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) → 𝐹 ∈ 𝐿1)
Theorem	cnicciblnc 33481	Choice-free proof of cniccibl 23607. (Contributed by Brendan Leahy, 2-Nov-2017.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ)) → 𝐹 ∈ 𝐿1)
Theorem	itggt0cn 33482*	itggt0 23608 holds for continuous functions in the absence of ax-cc 9257. (Contributed by Brendan Leahy, 16-Nov-2017.)
⊢ (𝜑 → 𝑋 < 𝑌)    &   ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ 𝐿1)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ ((𝑋(,)𝑌)–cn→ℂ))    ⇒   ⊢ (𝜑 → 0 < ∫(𝑋(,)𝑌)𝐵 d𝑥)
Theorem	ftc1cnnclem 33483*	Lemma for ftc1cnnc 33484; cf. ftc1lem4 23802. The stronger assumptions of ftc1cn 23806 are exploited to make use of weaker theorems. (Contributed by Brendan Leahy, 19-Nov-2017.)
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐿1)    &   ⊢ (𝜑 → 𝑐 ∈ (𝐴(,)𝐵))    &   ⊢ 𝐻 = (𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑧) − (𝐺‘𝑐)) / (𝑧 − 𝑐)))    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑅 ∈ ℝ+)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → ((abs‘(𝑦 − 𝑐)) < 𝑅 → (abs‘((𝐹‘𝑦) − (𝐹‘𝑐))) < 𝐸))    &   ⊢ (𝜑 → 𝑋 ∈ (𝐴[,]𝐵))    &   ⊢ (𝜑 → (abs‘(𝑋 − 𝑐)) < 𝑅)    &   ⊢ (𝜑 → 𝑌 ∈ (𝐴[,]𝐵))    &   ⊢ (𝜑 → (abs‘(𝑌 − 𝑐)) < 𝑅)    ⇒   ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → (abs‘((((𝐺‘𝑌) − (𝐺‘𝑋)) / (𝑌 − 𝑋)) − (𝐹‘𝑐))) < 𝐸)
Theorem	ftc1cnnc 33484*	Choice-free proof of ftc1cn 23806. (Contributed by Brendan Leahy, 20-Nov-2017.)
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐿1)    ⇒   ⊢ (𝜑 → (ℝ D 𝐺) = 𝐹)
Theorem	ftc1anclem1 33485	Lemma for ftc1anc 33493- the absolute value of a real-valued measurable function is measurable. Would be trivial with cncombf 23425, but this proof avoids ax-cc 9257. (Contributed by Brendan Leahy, 18-Jun-2018.)
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐹 ∈ MblFn) → (abs ∘ 𝐹) ∈ MblFn)
Theorem	ftc1anclem2 33486*	Lemma for ftc1anc 33493- restriction of an integrable function to the absolute value of its real or imaginary part. (Contributed by Brendan Leahy, 19-Jun-2018.) (Revised by Brendan Leahy, 8-Aug-2018.)
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1 ∧ 𝐺 ∈ {ℜ, ℑ}) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐴, (abs‘(𝐺‘(𝐹‘𝑡))), 0))) ∈ ℝ)
Theorem	ftc1anclem3 33487	Lemma for ftc1anc 33493- the absolute value of the sum of a simple function and i times another simple function is itself a simple function. (Contributed by Brendan Leahy, 27-May-2018.)
⊢ ((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) → (abs ∘ (𝐹 ∘𝑓 + ((ℝ × {i}) ∘𝑓 · 𝐺))) ∈ dom ∫1)
Theorem	ftc1anclem4 33488*	Lemma for ftc1anc 33493. (Contributed by Brendan Leahy, 17-Jun-2018.)
⊢ ((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ 𝐿1 ∧ 𝐺:ℝ⟶ℝ) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((𝐺‘𝑡) − (𝐹‘𝑡))))) ∈ ℝ)
Theorem	ftc1anclem5 33489*	Lemma for ftc1anc 33493, the existence of a simple function the integral of whose pointwise difference from the function is less than a given positive real. (Contributed by Brendan Leahy, 17-Jun-2018.)
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐷 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐿1)    &   ⊢ (𝜑 → 𝐹:𝐷⟶ℂ)    ⇒   ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → ∃𝑓 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) < 𝑌)
Theorem	ftc1anclem6 33490*	Lemma for ftc1anc 33493- construction of simple functions within an arbitrary absolute distance of the given function. Similar to Lemma 565Ib of [Fremlin5] p. 218, but without Fremlin's additional step of converting the simple function into a continuous one, which is unnecessary to this lemma's use; also, two simple functions are used to allow for complex-valued 𝐹. (Contributed by Brendan Leahy, 31-May-2018.)
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐷 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐿1)    &   ⊢ (𝜑 → 𝐹:𝐷⟶ℂ)    ⇒   ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → ∃𝑓 ∈ dom ∫1∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < 𝑌)
Theorem	ftc1anclem7 33491*	Lemma for ftc1anc 33493. (Contributed by Brendan Leahy, 13-May-2018.)
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐷 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐿1)    &   ⊢ (𝜑 → 𝐹:𝐷⟶ℂ)    ⇒   ⊢ (((((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) ∧ (abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))) < ((𝑦 / 2) + (𝑦 / 2)))
Theorem	ftc1anclem8 33492*	Lemma for ftc1anc 33493. (Contributed by Brendan Leahy, 29-May-2018.)
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐷 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐿1)    &   ⊢ (𝜑 → 𝐹:𝐷⟶ℂ)    ⇒   ⊢ (((((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) ∧ (abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) < 𝑦)
Theorem	ftc1anc 33493*	ftc1a 23800 holds for functions that obey the triangle inequality in the absence of ax-cc 9257. Theorem 565Ma of [Fremlin5] p. 220. (Contributed by Brendan Leahy, 11-May-2018.)
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐷 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐿1)    &   ⊢ (𝜑 → 𝐹:𝐷⟶ℂ)    &   ⊢ (𝜑 → ∀𝑠 ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵)))(abs‘∫𝑠(𝐹‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝑠, (abs‘(𝐹‘𝑡)), 0))))    ⇒   ⊢ (𝜑 → 𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ))
Theorem	ftc2nc 33494*	Choice-free proof of ftc2 23807. (Contributed by Brendan Leahy, 19-Jun-2018.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → (ℝ D 𝐹) ∈ ((𝐴(,)𝐵)–cn→ℂ))    &   ⊢ (𝜑 → (ℝ D 𝐹) ∈ 𝐿1)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ))    ⇒   ⊢ (𝜑 → ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 = ((𝐹‘𝐵) − (𝐹‘𝐴)))
Theorem	asindmre 33495	Real part of domain of differentiability of arcsine. (Contributed by Brendan Leahy, 19-Dec-2018.)
⊢ 𝐷 = (ℂ ∖ ((-∞(,]-1) ∪ (1[,)+∞)))    ⇒   ⊢ (𝐷 ∩ ℝ) = (-1(,)1)
Theorem	dvasin 33496*	Derivative of arcsine. (Contributed by Brendan Leahy, 18-Dec-2018.)
⊢ 𝐷 = (ℂ ∖ ((-∞(,]-1) ∪ (1[,)+∞)))    ⇒   ⊢ (ℂ D (arcsin ↾ 𝐷)) = (𝑥 ∈ 𝐷 ↦ (1 / (√‘(1 − (𝑥↑2)))))
Theorem	dvacos 33497*	Derivative of arccosine. (Contributed by Brendan Leahy, 18-Dec-2018.)
⊢ 𝐷 = (ℂ ∖ ((-∞(,]-1) ∪ (1[,)+∞)))    ⇒   ⊢ (ℂ D (arccos ↾ 𝐷)) = (𝑥 ∈ 𝐷 ↦ (-1 / (√‘(1 − (𝑥↑2)))))
Theorem	dvreasin 33498	Real derivative of arcsine. (Contributed by Brendan Leahy, 3-Aug-2017.) (Proof shortened by Brendan Leahy, 18-Dec-2018.)
⊢ (ℝ D (arcsin ↾ (-1(,)1))) = (𝑥 ∈ (-1(,)1) ↦ (1 / (√‘(1 − (𝑥↑2)))))
Theorem	dvreacos 33499	Real derivative of arccosine. (Contributed by Brendan Leahy, 3-Aug-2017.) (Proof shortened by Brendan Leahy, 18-Dec-2018.)
⊢ (ℝ D (arccos ↾ (-1(,)1))) = (𝑥 ∈ (-1(,)1) ↦ (-1 / (√‘(1 − (𝑥↑2)))))
Theorem	areacirclem1 33500*	Antiderivative of cross-section of circle. (Contributed by Brendan Leahy, 28-Aug-2017.) (Revised by Brendan Leahy, 11-Jul-2018.)
⊢ (𝑅 ∈ ℝ+ → (ℝ D (𝑡 ∈ (-𝑅(,)𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑡 / 𝑅)) + ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2)))))))) = (𝑡 ∈ (-𝑅(,)𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑡↑2))))))