P. 386 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 38501-38600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	sin2h 38501	Half-angle rule for sine. (Contributed by Brendan Leahy, 3-Aug-2018.)
⊢ (𝐴 ∈ (0[,](2 · π)) → (sin‘(𝐴 / 2)) = (√‘((1 − (cos‘𝐴)) / 2)))
Theorem	cos2h 38502	Half-angle rule for cosine. (Contributed by Brendan Leahy, 4-Aug-2018.)
⊢ (𝐴 ∈ (-π[,]π) → (cos‘(𝐴 / 2)) = (√‘((1 + (cos‘𝐴)) / 2)))
Theorem	tan2h 38503	Half-angle rule for tangent. (Contributed by Brendan Leahy, 4-Aug-2018.)
⊢ (𝐴 ∈ (0[,)π) → (tan‘(𝐴 / 2)) = (√‘((1 − (cos‘𝐴)) / (1 + (cos‘𝐴)))))
Theorem	lindsadd 38504	In a vector space, the union of an independent set and a vector not in its span is an independent set. (Contributed by Brendan Leahy, 4-Mar-2023.)
⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → (𝐹 ∪ {𝑋}) ∈ (LIndS‘𝑊))
Theorem	ptrest 38505*	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 38506*	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 38507*	Lemma for poimir 38539- 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)) / 𝑗⦌(𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))))    &   ⊢ (𝜑 → 𝑇:(1...𝑁)⟶ℤ)    &   ⊢ (𝜑 → 𝑈:(1...𝑁)–1-1-onto→(1...𝑁))    &   ⊢ (𝜑 → 𝑀 ∈ (1...(𝑁 − 1)))    ⇒   ⊢ (𝜑 → ¬ ∃*𝑛 ∈ (1...𝑁)((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛))
Theorem	poimirlem2 38508*	Lemma for poimir 38539- consecutive vertices differ in at most one dimension. (Contributed by Brendan Leahy, 21-Aug-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))))    &   ⊢ (𝜑 → 𝑇:(1...𝑁)⟶ℤ)    &   ⊢ (𝜑 → 𝑈:(1...𝑁)–1-1-onto→(1...𝑁))    &   ⊢ (𝜑 → 𝑉 ∈ (1...(𝑁 − 1)))    &   ⊢ (𝜑 → 𝑀 ∈ ((0...𝑁) ∖ {𝑉}))    ⇒   ⊢ (𝜑 → ∃*𝑛 ∈ (1...𝑁)((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛))
Theorem	poimirlem3 38509*	Lemma for poimir 38539 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...𝑀)𝑖 = ⦋((𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) / 𝑝⦌𝐵 → (⟨(𝑇 ∪ {⟨(𝑀 + 1), 0⟩}), (𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩})⟩ ∈ (((0..^𝐾) ↑m (1...(𝑀 + 1))) × {𝑓 ∣ 𝑓:(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1))}) ∧ (∀𝑖 ∈ (0...𝑀)∃𝑗 ∈ (0...𝑀)𝑖 = ⦋(((𝑇 ∪ {⟨(𝑀 + 1), 0⟩}) ∘f + ((((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) / 𝑝⦌𝐵 ∧ ((𝑇 ∪ {⟨(𝑀 + 1), 0⟩})‘(𝑀 + 1)) = 0 ∧ ((𝑈 ∪ {⟨(𝑀 + 1), (𝑀 + 1)⟩})‘(𝑀 + 1)) = (𝑀 + 1)))))
Theorem	poimirlem4 38510*	Lemma for poimir 38539 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..^𝐾) ↑m (1...𝑀)) × {𝑓 ∣ 𝑓:(1...𝑀)–1-1-onto→(1...𝑀)}) ∣ ∀𝑖 ∈ (0...𝑀)∃𝑗 ∈ (0...𝑀)𝑖 = ⦋(((1st ‘𝑠) ∘f + ((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd ‘𝑠) “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) / 𝑝⦌𝐵} ≈ {𝑠 ∈ (((0..^𝐾) ↑m (1...(𝑀 + 1))) × {𝑓 ∣ 𝑓:(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1))}) ∣ (∀𝑖 ∈ (0...𝑀)∃𝑗 ∈ (0...𝑀)𝑖 = ⦋(((1st ‘𝑠) ∘f + ((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd ‘𝑠) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) / 𝑝⦌𝐵 ∧ ((1st ‘𝑠)‘(𝑀 + 1)) = 0 ∧ ((2nd ‘𝑠)‘(𝑀 + 1)) = (𝑀 + 1))})
Theorem	poimirlem5 38511*	Lemma for poimir 38539 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..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘f + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → 0 < (2nd ‘𝑇))    ⇒   ⊢ (𝜑 → (𝐹‘0) = (1st ‘(1st ‘𝑇)))
Theorem	poimirlem6 38512*	Lemma for poimir 38539 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..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘f + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → (2nd ‘𝑇) ∈ (1...(𝑁 − 1)))    &   ⊢ (𝜑 → 𝑀 ∈ (1...((2nd ‘𝑇) − 1)))    ⇒   ⊢ (𝜑 → (℩𝑛 ∈ (1...𝑁)((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛)) = ((2nd ‘(1st ‘𝑇))‘𝑀))
Theorem	poimirlem7 38513*	Lemma for poimir 38539, similar to poimirlem6 38512, but for vertices after the opposite vertex. (Contributed by Brendan Leahy, 21-Aug-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘f + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → (2nd ‘𝑇) ∈ (1...(𝑁 − 1)))    &   ⊢ (𝜑 → 𝑀 ∈ ((((2nd ‘𝑇) + 1) + 1)...𝑁))    ⇒   ⊢ (𝜑 → (℩𝑛 ∈ (1...𝑁)((𝐹‘(𝑀 − 2))‘𝑛) ≠ ((𝐹‘(𝑀 − 1))‘𝑛)) = ((2nd ‘(1st ‘𝑇))‘𝑀))
Theorem	poimirlem8 38514*	Lemma for poimir 38539, establishing that away from the opposite vertex the walks in poimirlem9 38515 yield the same vertices. (Contributed by Brendan Leahy, 21-Aug-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘f + ((((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 38515*	Lemma for poimir 38539, 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..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘f + ((((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 38516*	Lemma for poimir 38539 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..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘f + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}    &   ⊢ (𝜑 → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑m (1...𝑁)))    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → (2nd ‘𝑇) = 0)    ⇒   ⊢ (𝜑 → ((𝐹‘(𝑁 − 1)) ∘f − ((1...𝑁) × {1})) = (1st ‘(1st ‘𝑇)))
Theorem	poimirlem11 38517*	Lemma for poimir 38539 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..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘f + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}    &   ⊢ (𝜑 → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑m (1...𝑁)))    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → (2nd ‘𝑇) = 0)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → (2nd ‘𝑈) = 0)    &   ⊢ (𝜑 → 𝑀 ∈ (1...𝑁))    ⇒   ⊢ (𝜑 → ((2nd ‘(1st ‘𝑇)) “ (1...𝑀)) ⊆ ((2nd ‘(1st ‘𝑈)) “ (1...𝑀)))
Theorem	poimirlem12 38518*	Lemma for poimir 38539 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..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘f + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}    &   ⊢ (𝜑 → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑m (1...𝑁)))    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → (2nd ‘𝑇) = 𝑁)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → (2nd ‘𝑈) = 𝑁)    &   ⊢ (𝜑 → 𝑀 ∈ (0...(𝑁 − 1)))    ⇒   ⊢ (𝜑 → ((2nd ‘(1st ‘𝑇)) “ (1...𝑀)) ⊆ ((2nd ‘(1st ‘𝑈)) “ (1...𝑀)))
Theorem	poimirlem13 38519*	Lemma for poimir 38539- 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..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘f + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}    &   ⊢ (𝜑 → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑m (1...𝑁)))    ⇒   ⊢ (𝜑 → ∃*𝑧 ∈ 𝑆 (2nd ‘𝑧) = 0)
Theorem	poimirlem14 38520*	Lemma for poimir 38539- 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..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘f + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}    &   ⊢ (𝜑 → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑m (1...𝑁)))    ⇒   ⊢ (𝜑 → ∃*𝑧 ∈ 𝑆 (2nd ‘𝑧) = 𝑁)
Theorem	poimirlem15 38521*	Lemma for poimir 38539, that the face in poimirlem22 38528 is a face. (Contributed by Brendan Leahy, 21-Aug-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘f + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}    &   ⊢ (𝜑 → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑m (1...𝑁)))    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → (2nd ‘𝑇) ∈ (1...(𝑁 − 1)))    ⇒   ⊢ (𝜑 → ⟨⟨(1st ‘(1st ‘𝑇)), ((2nd ‘(1st ‘𝑇)) ∘ ({⟨(2nd ‘𝑇), ((2nd ‘𝑇) + 1)⟩, ⟨((2nd ‘𝑇) + 1), (2nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}))))⟩, (2nd ‘𝑇)⟩ ∈ 𝑆)
Theorem	poimirlem16 38522*	Lemma for poimir 38539 establishing the vertices of the simplex of poimirlem17 38523. (Contributed by Brendan Leahy, 21-Aug-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘f + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}    &   ⊢ (𝜑 → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑m (1...𝑁)))    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 𝐾)    &   ⊢ (𝜑 → (2nd ‘𝑇) = 0)    ⇒   ⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ((𝑛 ∈ (1...𝑁) ↦ (((1st ‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st ‘𝑇))‘1), 1, 0))) ∘f + (((((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0})))))
Theorem	poimirlem17 38523*	Lemma for poimir 38539 establishing existence for poimirlem18 38524. (Contributed by Brendan Leahy, 21-Aug-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘f + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}    &   ⊢ (𝜑 → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑m (1...𝑁)))    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 𝐾)    &   ⊢ (𝜑 → (2nd ‘𝑇) = 0)    ⇒   ⊢ (𝜑 → ∃𝑧 ∈ 𝑆 𝑧 ≠ 𝑇)
Theorem	poimirlem18 38524*	Lemma for poimir 38539 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..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘f + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}    &   ⊢ (𝜑 → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑m (1...𝑁)))    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 𝐾)    &   ⊢ (𝜑 → (2nd ‘𝑇) = 0)    ⇒   ⊢ (𝜑 → ∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇)
Theorem	poimirlem19 38525*	Lemma for poimir 38539 establishing the vertices of the simplex in poimirlem20 38526. (Contributed by Brendan Leahy, 21-Aug-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘f + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}    &   ⊢ (𝜑 → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑m (1...𝑁)))    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 0)    &   ⊢ (𝜑 → (2nd ‘𝑇) = 𝑁)    ⇒   ⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ((𝑛 ∈ (1...𝑁) ↦ (((1st ‘(1st ‘𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st ‘𝑇))‘𝑁), 1, 0))) ∘f + (((((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0})))))
Theorem	poimirlem20 38526*	Lemma for poimir 38539 establishing existence for poimirlem21 38527. (Contributed by Brendan Leahy, 21-Aug-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘f + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}    &   ⊢ (𝜑 → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑m (1...𝑁)))    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 0)    &   ⊢ (𝜑 → (2nd ‘𝑇) = 𝑁)    ⇒   ⊢ (𝜑 → ∃𝑧 ∈ 𝑆 𝑧 ≠ 𝑇)
Theorem	poimirlem21 38527*	Lemma for poimir 38539 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..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘f + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}    &   ⊢ (𝜑 → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑m (1...𝑁)))    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 0)    &   ⊢ (𝜑 → (2nd ‘𝑇) = 𝑁)    ⇒   ⊢ (𝜑 → ∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇)
Theorem	poimirlem22 38528*	Lemma for poimir 38539, 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..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘f + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}    &   ⊢ (𝜑 → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑m (1...𝑁)))    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 0)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 𝐾)    ⇒   ⊢ (𝜑 → ∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇)
Theorem	poimirlem23 38529*	Lemma for poimir 38539, 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)) / 𝑗⦌(𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))(𝑝‘𝑁) ≠ 0 ↔ ¬ (𝑉 = 𝑁 ∧ ((𝑇‘𝑁) = 0 ∧ (𝑈‘𝑁) = 𝑁))))
Theorem	poimirlem24 38530*	Lemma for poimir 38539, 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 ‘𝑠) ∘f + ((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd ‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → 𝐵 = 𝐶)    &   ⊢ ((𝜑 ∧ 𝑝:(1...𝑁)⟶(0...𝐾)) → 𝐵 ∈ (0...𝑁))    &   ⊢ (𝜑 → 𝑇:(1...𝑁)⟶(0..^𝐾))    &   ⊢ (𝜑 → 𝑈:(1...𝑁)–1-1-onto→(1...𝑁))    &   ⊢ (𝜑 → 𝑉 ∈ (0...𝑁))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ (((0...𝐾) ↑m (1...𝑁)) ↑m (0...(𝑁 − 1)))(𝑥 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ∧ ((0...(𝑁 − 1)) ⊆ ran (𝑝 ∈ ran 𝑥 ↦ 𝐵) ∧ ∃𝑝 ∈ ran 𝑥(𝑝‘𝑁) ≠ 0)) ↔ (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑉})𝑖 = ⦋⟨𝑇, 𝑈⟩ / 𝑠⦌𝐶 ∧ ¬ (𝑉 = 𝑁 ∧ ((𝑇‘𝑁) = 0 ∧ (𝑈‘𝑁) = 𝑁)))))
Theorem	poimirlem25 38531*	Lemma for poimir 38539 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 ‘𝑠) ∘f + ((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd ‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → 𝐵 = 𝐶)    &   ⊢ ((𝜑 ∧ 𝑝:(1...𝑁)⟶(0...𝐾)) → 𝐵 ∈ (0...𝑁))    &   ⊢ (𝜑 → 𝑇:(1...𝑁)⟶(0..^𝐾))    &   ⊢ (𝜑 → 𝑈:(1...𝑁)–1-1-onto→(1...𝑁))    &   ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝑁 ≠ ⦋⟨𝑇, 𝑈⟩ / 𝑠⦌𝐶)    ⇒   ⊢ (𝜑 → 2 ∥ (♯‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = ⦋⟨𝑇, 𝑈⟩ / 𝑠⦌𝐶}))
Theorem	poimirlem26 38532*	Lemma for poimir 38539 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 ‘𝑠) ∘f + ((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd ‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → 𝐵 = 𝐶)    &   ⊢ ((𝜑 ∧ 𝑝:(1...𝑁)⟶(0...𝐾)) → 𝐵 ∈ (0...𝑁))    ⇒   ⊢ (𝜑 → 2 ∥ ((♯‘{𝑡 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {(2nd ‘𝑡)})𝑖 = ⦋(1st ‘𝑡) / 𝑠⦌𝐶}) − (♯‘{𝑠 ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∣ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = 𝐶})))
Theorem	poimirlem27 38533*	Lemma for poimir 38539 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 ‘𝑠) ∘f + ((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd ‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → 𝐵 = 𝐶)    &   ⊢ ((𝜑 ∧ 𝑝:(1...𝑁)⟶(0...𝐾)) → 𝐵 ∈ (0...𝑁))    &   ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝐾) ∧ (𝑝‘𝑛) = 0)) → 𝐵 < 𝑛)    &   ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝐾) ∧ (𝑝‘𝑛) = 𝐾)) → 𝐵 ≠ (𝑛 − 1))    ⇒   ⊢ (𝜑 → 2 ∥ ((♯‘{𝑡 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {(2nd ‘𝑡)})𝑖 = ⦋(1st ‘𝑡) / 𝑠⦌𝐶}) − (♯‘{𝑠 ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∣ (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ (0...(𝑁 − 1))𝑖 = 𝐶 ∧ ((1st ‘𝑠)‘𝑁) = 0 ∧ ((2nd ‘𝑠)‘𝑁) = 𝑁)})))
Theorem	poimirlem28 38534*	Lemma for poimir 38539, a variant of Sperner's lemma. (Contributed by Brendan Leahy, 21-Aug-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝑝 = ((1st ‘𝑠) ∘f + ((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd ‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → 𝐵 = 𝐶)    &   ⊢ ((𝜑 ∧ 𝑝:(1...𝑁)⟶(0...𝐾)) → 𝐵 ∈ (0...𝑁))    &   ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝐾) ∧ (𝑝‘𝑛) = 0)) → 𝐵 < 𝑛)    &   ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝐾) ∧ (𝑝‘𝑛) = 𝐾)) → 𝐵 ≠ (𝑛 − 1))    &   ⊢ (𝜑 → 𝐾 ∈ ℕ)    ⇒   ⊢ (𝜑 → ∃𝑠 ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = 𝐶)
Theorem	poimirlem29 38535*	Lemma for poimir 38539 connecting cubes of the tessellation to neighborhoods. (Contributed by Brendan Leahy, 21-Aug-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐼 = ((0[,]1) ↑m (1...𝑁))    &   ⊢ 𝑅 = (∏t‘((1...𝑁) × {(topGen‘ran (,))}))    &   ⊢ (𝜑 → 𝐹 ∈ ((𝑅 ↾t 𝐼) Cn 𝑅))    &   ⊢ 𝑋 = ((𝐹‘(((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑛)    &   ⊢ (𝜑 → 𝐺:ℕ⟶((ℕ0 ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ran (1st ‘(𝐺‘𝑘)) ⊆ (0..^𝑘))    &   ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁) ∧ 𝑟 ∈ { ≤ , ◡ ≤ })) → ∃𝑗 ∈ (0...𝑁)0𝑟𝑋)    ⇒   ⊢ (𝜑 → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → ∀𝑛 ∈ (1...𝑁)∀𝑣 ∈ (𝑅 ↾t 𝐼)(𝐶 ∈ 𝑣 → ∀𝑟 ∈ { ≤ , ◡ ≤ }∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛))))
Theorem	poimirlem30 38536*	Lemma for poimir 38539 combining poimirlem29 38535 with bwth 23708. (Contributed by Brendan Leahy, 21-Aug-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐼 = ((0[,]1) ↑m (1...𝑁))    &   ⊢ 𝑅 = (∏t‘((1...𝑁) × {(topGen‘ran (,))}))    &   ⊢ (𝜑 → 𝐹 ∈ ((𝑅 ↾t 𝐼) Cn 𝑅))    &   ⊢ 𝑋 = ((𝐹‘(((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑛)    &   ⊢ (𝜑 → 𝐺:ℕ⟶((ℕ0 ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ran (1st ‘(𝐺‘𝑘)) ⊆ (0..^𝑘))    &   ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁) ∧ 𝑟 ∈ { ≤ , ◡ ≤ })) → ∃𝑗 ∈ (0...𝑁)0𝑟𝑋)    ⇒   ⊢ (𝜑 → ∃𝑐 ∈ 𝐼 ∀𝑛 ∈ (1...𝑁)∀𝑣 ∈ (𝑅 ↾t 𝐼)(𝑐 ∈ 𝑣 → ∀𝑟 ∈ { ≤ , ◡ ≤ }∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛)))
Theorem	poimirlem31 38537*	Lemma for poimir 38539, assigning values to the vertices of the tessellation that meet the hypotheses of both poimirlem30 38536 and poimirlem28 38534. Equation (2) of [Kulpa] p. 547. (Contributed by Brendan Leahy, 21-Aug-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐼 = ((0[,]1) ↑m (1...𝑁))    &   ⊢ 𝑅 = (∏t‘((1...𝑁) × {(topGen‘ran (,))}))    &   ⊢ (𝜑 → 𝐹 ∈ ((𝑅 ↾t 𝐼) Cn 𝑅))    &   ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 0)) → ((𝐹‘𝑧)‘𝑛) ≤ 0)    &   ⊢ 𝑃 = ((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))    &   ⊢ (𝜑 → 𝐺:ℕ⟶((ℕ0 ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ran (1st ‘(𝐺‘𝑘)) ⊆ (0..^𝑘))    &   ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑖 ∈ (0...𝑁))) → ∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ))    ⇒   ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁) ∧ 𝑟 ∈ { ≤ , ◡ ≤ })) → ∃𝑗 ∈ (0...𝑁)0𝑟((𝐹‘(𝑃 ∘f / ((1...𝑁) × {𝑘})))‘𝑛))
Theorem	poimirlem32 38538*	Lemma for poimir 38539, combining poimirlem28 38534, poimirlem30 38536, and poimirlem31 38537 to get Equation (1) of [Kulpa] p. 547. (Contributed by Brendan Leahy, 21-Aug-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐼 = ((0[,]1) ↑m (1...𝑁))    &   ⊢ 𝑅 = (∏t‘((1...𝑁) × {(topGen‘ran (,))}))    &   ⊢ (𝜑 → 𝐹 ∈ ((𝑅 ↾t 𝐼) Cn 𝑅))    &   ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 0)) → ((𝐹‘𝑧)‘𝑛) ≤ 0)    &   ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 1)) → 0 ≤ ((𝐹‘𝑧)‘𝑛))    ⇒   ⊢ (𝜑 → ∃𝑐 ∈ 𝐼 ∀𝑛 ∈ (1...𝑁)∀𝑣 ∈ (𝑅 ↾t 𝐼)(𝑐 ∈ 𝑣 → ∀𝑟 ∈ { ≤ , ◡ ≤ }∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛)))
Theorem	poimir 38539*	Poincare-Miranda theorem. Theorem on [Kulpa] p. 547. (Contributed by Brendan Leahy, 21-Aug-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐼 = ((0[,]1) ↑m (1...𝑁))    &   ⊢ 𝑅 = (∏t‘((1...𝑁) × {(topGen‘ran (,))}))    &   ⊢ (𝜑 → 𝐹 ∈ ((𝑅 ↾t 𝐼) Cn 𝑅))    &   ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 0)) → ((𝐹‘𝑧)‘𝑛) ≤ 0)    &   ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 1)) → 0 ≤ ((𝐹‘𝑧)‘𝑛))    ⇒   ⊢ (𝜑 → ∃𝑐 ∈ 𝐼 (𝐹‘𝑐) = ((1...𝑁) × {0}))
Theorem	broucube 38540*	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) ↑m (1...𝑁))    &   ⊢ 𝑅 = (∏t‘((1...𝑁) × {(topGen‘ran (,))}))    &   ⊢ (𝜑 → 𝐹 ∈ ((𝑅 ↾t 𝐼) Cn (𝑅 ↾t 𝐼)))    ⇒   ⊢ (𝜑 → ∃𝑐 ∈ 𝐼 𝑐 = (𝐹‘𝑐))
Theorem	heicant 38541	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 38542*	Lemma for ismblfin 38547; could also be used to shorten proof of opnmbllem 25902. (Contributed by Brendan Leahy, 13-Jul-2018.)
⊢ (𝐴 ∈ (topGen‘ran (,)) → ∪ ([,] “ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴}) = 𝐴)
Theorem	mblfinlem1 38543*	Lemma for ismblfin 38547, 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 38544*	Lemma for ismblfin 38547, effectively one direction of the same fact for open sets, made necessary by Viaclovsky's slightly different definition 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 38545*	The difference between two sets measurable by the criterion in ismblfin 38547 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 38546*	Backward direction of ismblfin 38547. (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 38547*	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 38548*	ovoliun 25806 is incompatible with the Feferman-Levy model. (Contributed by Brendan Leahy, 21-Nov-2017.)
⊢ ((𝑓 Fn ℕ ∧ ∀𝑛 ∈ ℕ ((𝑓‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑓‘𝑛)) ∈ ℝ)) → (vol*‘∪ 𝑚 ∈ ℕ (𝑓‘𝑚)) ≤ sup(ran seq1( + , (𝑚 ∈ ℕ ↦ (vol*‘(𝑓‘𝑚)))), ℝ*, < ))    ⇒   ⊢ ((𝐴 ≼ ℕ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) → ∪ 𝐴 ≠ ℝ)
Theorem	ex-ovoliunnfl 38549*	Demonstration of ovoliunnfl 38548. (Contributed by Brendan Leahy, 21-Nov-2017.)
⊢ ((𝐴 ≼ ℕ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) → ∪ 𝐴 ≠ ℝ)
Theorem	voliunnfl 38550*	voliun 25855 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 38551*	volsup 25857 is incompatible with the Feferman-Levy model. (Contributed by Brendan Leahy, 2-Jan-2018.)
⊢ ((𝑓:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ⊆ (𝑓‘(𝑛 + 1))) → (vol‘∪ ran 𝑓) = sup((vol “ ran 𝑓), ℝ*, < ))    ⇒   ⊢ ((𝐴 ≼ ℕ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) → ∪ 𝐴 ≠ ℝ)
Theorem	mbfresfi 38552*	Measurability of a piecewise function across arbitrarily many subsets. (Contributed by Brendan Leahy, 31-Mar-2018.)
⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝑆 ∈ Fin)    &   ⊢ (𝜑 → ∀𝑠 ∈ 𝑆 (𝐹 ↾ 𝑠) ∈ MblFn)    &   ⊢ (𝜑 → ∪ 𝑆 = 𝐴)    ⇒   ⊢ (𝜑 → 𝐹 ∈ MblFn)
Theorem	mbfposadd 38553*	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 38554	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 38555	Lemma for dvtan 38556- 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 38556	Derivative of tangent. (Contributed by Brendan Leahy, 7-Aug-2018.)
⊢ (ℂ D tan) = (𝑥 ∈ dom tan ↦ ((cos‘𝑥)↑-2))
Theorem	itg2addnclem 38557*	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, ((𝑔‘𝑧) + 𝑦))) ∘r ≤ 𝐹 ∧ 𝑥 = (∫1‘𝑔))}    ⇒   ⊢ (𝐹:ℝ⟶(0[,]+∞) → (∫2‘𝐹) = sup(𝐿, ℝ*, < ))
Theorem	itg2addnclem2 38558*	Lemma for itg2addnc 38560. 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 38559*	Lemma incomprehensible in isolation split off to shorten proof of itg2addnc 38560. (Contributed by Brendan Leahy, 11-Mar-2018.)
⊢ (𝜑 → 𝐹 ∈ MblFn)    &   ⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞))    &   ⊢ (𝜑 → (∫2‘𝐹) ∈ ℝ)    &   ⊢ (𝜑 → 𝐺:ℝ⟶(0[,)+∞))    &   ⊢ (𝜑 → (∫2‘𝐺) ∈ ℝ)    ⇒   ⊢ (𝜑 → (∃ℎ ∈ dom ∫1(∃𝑦 ∈ ℝ+ (𝑧 ∈ ℝ ↦ if((ℎ‘𝑧) = 0, 0, ((ℎ‘𝑧) + 𝑦))) ∘r ≤ (𝐹 ∘f + 𝐺) ∧ 𝑠 = (∫1‘ℎ)) → ∃𝑡∃𝑢(∃𝑓 ∈ dom ∫1∃𝑔 ∈ dom ∫1((∃𝑐 ∈ ℝ+ (𝑧 ∈ ℝ ↦ if((𝑓‘𝑧) = 0, 0, ((𝑓‘𝑧) + 𝑐))) ∘r ≤ 𝐹 ∧ 𝑡 = (∫1‘𝑓)) ∧ (∃𝑑 ∈ ℝ+ (𝑧 ∈ ℝ ↦ if((𝑔‘𝑧) = 0, 0, ((𝑔‘𝑧) + 𝑑))) ∘r ≤ 𝐺 ∧ 𝑢 = (∫1‘𝑔))) ∧ 𝑠 = (𝑡 + 𝑢))))
Theorem	itg2addnc 38560	Alternate proof of itg2add 26060 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 26009, 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 10494, 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‘(𝐹 ∘f + 𝐺)) = ((∫2‘𝐹) + (∫2‘𝐺)))
Theorem	itg2gt0cn 38561*	itg2gt0 26061 holds on functions continuous on an open interval in the absence of ax-cc 10494. The fourth hypothesis is made unnecessary by the continuity hypothesis. (Contributed by Brendan Leahy, 16-Nov-2017.)
⊢ (𝜑 → 𝑋 < 𝑌)    &   ⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 0 < (𝐹‘𝑥))    &   ⊢ (𝜑 → (𝐹 ↾ (𝑋(,)𝑌)) ∈ ((𝑋(,)𝑌)–cn→ℂ))    ⇒   ⊢ (𝜑 → 0 < (∫2‘𝐹))
Theorem	ibladdnclem 38562*	Lemma for ibladdnc 38563; cf ibladdlem 26120, whose fifth hypothesis is rendered unnecessary by the weakened hypotheses of itg2addnc 38560. (Contributed by Brendan Leahy, 31-Oct-2017.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐷 = (𝐵 + 𝐶))    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn)    &   ⊢ (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))) ∈ ℝ)    &   ⊢ (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0))) ∈ ℝ)    ⇒   ⊢ (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0))) ∈ ℝ)
Theorem	ibladdnc 38563*	Choice-free analogue of itgadd 26125. A measurability hypothesis is necessitated by the loss of mbfadd 25962; 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 38564*	Lemma for itgaddnc 38566; cf. itgaddlem1 26123. (Contributed by Brendan Leahy, 7-Nov-2017.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∈ MblFn)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ 𝐶)    ⇒   ⊢ (𝜑 → ∫𝐴(𝐵 + 𝐶) d𝑥 = (∫𝐴𝐵 d𝑥 + ∫𝐴𝐶 d𝑥))
Theorem	itgaddnclem2 38565*	Lemma for itgaddnc 38566; cf. itgaddlem2 26124. (Contributed by Brendan Leahy, 10-Nov-2017.) (Revised by Brendan Leahy, 3-Apr-2018.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∈ MblFn)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → ∫𝐴(𝐵 + 𝐶) d𝑥 = (∫𝐴𝐵 d𝑥 + ∫𝐴𝐶 d𝑥))
Theorem	itgaddnc 38566*	Choice-free analogue of itgadd 26125. (Contributed by Brendan Leahy, 11-Nov-2017.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∈ MblFn)    ⇒   ⊢ (𝜑 → ∫𝐴(𝐵 + 𝐶) d𝑥 = (∫𝐴𝐵 d𝑥 + ∫𝐴𝐶 d𝑥))
Theorem	iblsubnc 38567*	Choice-free analogue of iblsub 26122. (Contributed by Brendan Leahy, 11-Nov-2017.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 − 𝐶)) ∈ MblFn)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 − 𝐶)) ∈ 𝐿1)
Theorem	itgsubnc 38568*	Choice-free analogue of itgsub 26126. (Contributed by Brendan Leahy, 11-Nov-2017.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 − 𝐶)) ∈ MblFn)    ⇒   ⊢ (𝜑 → ∫𝐴(𝐵 − 𝐶) d𝑥 = (∫𝐴𝐵 d𝑥 − ∫𝐴𝐶 d𝑥))
Theorem	iblabsnclem 38569*	Lemma for iblabsnc 38570; cf. iblabslem 26128. (Contributed by Brendan Leahy, 7-Nov-2017.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    &   ⊢ 𝐺 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(𝐹‘𝐵)), 0))    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐹‘𝐵)) ∈ 𝐿1)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝐵) ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐺 ∈ MblFn ∧ (∫2‘𝐺) ∈ ℝ))
Theorem	iblabsnc 38570*	Choice-free analogue of iblabs 26129. As with ibladdnc 38563, a measurability hypothesis is needed. (Contributed by Brendan Leahy, 7-Nov-2017.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (abs‘𝐵)) ∈ MblFn)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (abs‘𝐵)) ∈ 𝐿1)
Theorem	iblmulc2nc 38571*	Choice-free analogue of iblmulc2 26131. (Contributed by Brendan Leahy, 17-Nov-2017.)
⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ MblFn)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ 𝐿1)
Theorem	itgmulc2nclem1 38572*	Lemma for itgmulc2nc 38574; cf. itgmulc2lem1 26132. (Contributed by Brendan Leahy, 17-Nov-2017.)
⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ MblFn)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 · ∫𝐴𝐵 d𝑥) = ∫𝐴(𝐶 · 𝐵) d𝑥)
Theorem	itgmulc2nclem2 38573*	Lemma for itgmulc2nc 38574; cf. itgmulc2lem2 26133. (Contributed by Brendan Leahy, 19-Nov-2017.)
⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ MblFn)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐶 · ∫𝐴𝐵 d𝑥) = ∫𝐴(𝐶 · 𝐵) d𝑥)
Theorem	itgmulc2nc 38574*	Choice-free analogue of itgmulc2 26134. (Contributed by Brendan Leahy, 19-Nov-2017.)
⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ MblFn)    ⇒   ⊢ (𝜑 → (𝐶 · ∫𝐴𝐵 d𝑥) = ∫𝐴(𝐶 · 𝐵) d𝑥)
Theorem	itgabsnc 38575*	Choice-free analogue of itgabs 26135. (Contributed by Brendan Leahy, 19-Nov-2017.) (Revised by Brendan Leahy, 19-Jun-2018.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (abs‘𝐵)) ∈ MblFn)    &   ⊢ (𝜑 → (𝑦 ∈ 𝐴 ↦ ((∗‘∫𝐴𝐵 d𝑥) · ⦋𝑦 / 𝑥⦌𝐵)) ∈ MblFn)    ⇒   ⊢ (𝜑 → (abs‘∫𝐴𝐵 d𝑥) ≤ ∫𝐴(abs‘𝐵) d𝑥)
Theorem	itggt0cn 38576*	itggt0 26144 holds for continuous functions in the absence of ax-cc 10494. (Contributed by Brendan Leahy, 16-Nov-2017.)
⊢ (𝜑 → 𝑋 < 𝑌)    &   ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ 𝐿1)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ ((𝑋(,)𝑌)–cn→ℂ))    ⇒   ⊢ (𝜑 → 0 < ∫(𝑋(,)𝑌)𝐵 d𝑥)
Theorem	ftc1cnnclem 38577*	Lemma for ftc1cnnc 38578; cf. ftc1lem4 26339. The stronger assumptions of ftc1cn 26343 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 38578*	Choice-free proof of ftc1cn 26343. (Contributed by Brendan Leahy, 20-Nov-2017.)
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐿1)    ⇒   ⊢ (𝜑 → (ℝ D 𝐺) = 𝐹)
Theorem	ftc1anclem1 38579	Lemma for ftc1anc 38587- the absolute value of a real-valued measurable function is measurable. Would be trivial with cncombf 25959, but this proof avoids ax-cc 10494. (Contributed by Brendan Leahy, 18-Jun-2018.)
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐹 ∈ MblFn) → (abs ∘ 𝐹) ∈ MblFn)
Theorem	ftc1anclem2 38580*	Lemma for ftc1anc 38587- 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 38581	Lemma for ftc1anc 38587- 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 ∘ (𝐹 ∘f + ((ℝ × {i}) ∘f · 𝐺))) ∈ dom ∫1)
Theorem	ftc1anclem4 38582*	Lemma for ftc1anc 38587. (Contributed by Brendan Leahy, 17-Jun-2018.)
⊢ ((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ 𝐿1 ∧ 𝐺:ℝ⟶ℝ) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((𝐺‘𝑡) − (𝐹‘𝑡))))) ∈ ℝ)
Theorem	ftc1anclem5 38583*	Lemma for ftc1anc 38587, 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 38584*	Lemma for ftc1anc 38587- 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 38585*	Lemma for ftc1anc 38587. (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 38586*	Lemma for ftc1anc 38587. (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 38587*	ftc1a 26337 holds for functions that obey the triangle inequality in the absence of ax-cc 10494. Theorem 565Ma of [Fremlin5] p. 220. (Contributed by Brendan Leahy, 11-May-2018.)
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐷 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐿1)    &   ⊢ (𝜑 → 𝐹:𝐷⟶ℂ)    &   ⊢ (𝜑 → ∀𝑠 ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵)))(abs‘∫𝑠(𝐹‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝑠, (abs‘(𝐹‘𝑡)), 0))))    ⇒   ⊢ (𝜑 → 𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ))
Theorem	ftc2nc 38588*	Choice-free proof of ftc2 26344. (Contributed by Brendan Leahy, 19-Jun-2018.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → (ℝ D 𝐹) ∈ ((𝐴(,)𝐵)–cn→ℂ))    &   ⊢ (𝜑 → (ℝ D 𝐹) ∈ 𝐿1)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ))    ⇒   ⊢ (𝜑 → ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 = ((𝐹‘𝐵) − (𝐹‘𝐴)))
Theorem	asindmre 38589	Real part of domain of differentiability of arcsine. (Contributed by Brendan Leahy, 19-Dec-2018.)
⊢ 𝐷 = (ℂ ∖ ((-∞(,]-1) ∪ (1[,)+∞)))    ⇒   ⊢ (𝐷 ∩ ℝ) = (-1(,)1)
Theorem	dvasin 38590*	Derivative of arcsine. (Contributed by Brendan Leahy, 18-Dec-2018.)
⊢ 𝐷 = (ℂ ∖ ((-∞(,]-1) ∪ (1[,)+∞)))    ⇒   ⊢ (ℂ D (arcsin ↾ 𝐷)) = (𝑥 ∈ 𝐷 ↦ (1 / (√‘(1 − (𝑥↑2)))))
Theorem	dvacos 38591*	Derivative of arccosine. (Contributed by Brendan Leahy, 18-Dec-2018.)
⊢ 𝐷 = (ℂ ∖ ((-∞(,]-1) ∪ (1[,)+∞)))    ⇒   ⊢ (ℂ D (arccos ↾ 𝐷)) = (𝑥 ∈ 𝐷 ↦ (-1 / (√‘(1 − (𝑥↑2)))))
Theorem	dvreasin 38592	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 38593	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 38594*	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))))))
Theorem	areacirclem2 38595*	Endpoint-inclusive continuity of Cartesian ordinate of circle. (Contributed by Brendan Leahy, 29-Aug-2017.) (Revised by Brendan Leahy, 11-Jul-2018.)
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑡↑2)))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
Theorem	areacirclem3 38596*	Integrability of cross-section of circle. (Contributed by Brendan Leahy, 26-Aug-2017.) (Revised by Brendan Leahy, 11-Jul-2018.)
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑡↑2))))) ∈ 𝐿1)
Theorem	areacirclem4 38597*	Endpoint-inclusive continuity of antiderivative of cross-section of circle. (Contributed by Brendan Leahy, 31-Aug-2017.) (Revised by Brendan Leahy, 11-Jul-2018.)
⊢ (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑡 / 𝑅)) + ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2))))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
Theorem	areacirclem5 38598*	Finding the cross-section of a circle. (Contributed by Brendan Leahy, 31-Aug-2017.) (Revised by Brendan Leahy, 22-Sep-2017.) (Revised by Brendan Leahy, 11-Jul-2018.)
⊢ 𝑆 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ((𝑥↑2) + (𝑦↑2)) ≤ (𝑅↑2))}    ⇒   ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (𝑆 “ {𝑡}) = if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))
Theorem	areacirc 38599*	The area of a circle of radius 𝑅 is π · 𝑅↑2. This is Metamath 100 proof #9. (Contributed by Brendan Leahy, 31-Aug-2017.) (Revised by Brendan Leahy, 22-Sep-2017.) (Revised by Brendan Leahy, 11-Jul-2018.)
⊢ 𝑆 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ((𝑥↑2) + (𝑦↑2)) ≤ (𝑅↑2))}    ⇒   ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (area‘𝑆) = (π · (𝑅↑2)))
21.24  Mathbox for Thomas van Maaren
Theorem	findcard4 38600*	Schema for strong induction on the cardinality of a finite set. The inductive hypothesis is that the result is true on any set with less elements. The result is then proven to be true for all finite sets. (Contributed by Thomas van Maaren, 14-Aug-2026.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))    &   ⊢ (𝑦 ∈ Fin → (∀𝑥((♯‘𝑥) < (♯‘𝑦) → 𝜑) → 𝜒))    ⇒   ⊢ (𝐴 ∈ Fin → 𝜏)