Theorem vonicc 46808

Description: The n-dimensional Lebesgue measure of a closed interval. This is the second statement in Proposition 115G (d) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021.)

Hypotheses

Ref	Expression
vonicc.x	⊢ (𝜑 → 𝑋 ∈ Fin)
vonicc.a	⊢ (𝜑 → 𝐴:𝑋⟶ℝ)
vonicc.b	⊢ (𝜑 → 𝐵:𝑋⟶ℝ)
vonicc.i	⊢ 𝐼 = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐵‘𝑘))
vonicc.l	⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))))

Assertion

Ref	Expression
vonicc	⊢ (𝜑 → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵))

Distinct variable groups:   𝐴,𝑎,𝑏,𝑘   𝐵,𝑎,𝑏,𝑘   𝑋,𝑎,𝑏,𝑘,𝑥   𝜑,𝑎,𝑏,𝑘,𝑥

Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)   𝐼(𝑥,𝑘,𝑎,𝑏)   𝐿(𝑥,𝑘,𝑎,𝑏)

Proof of Theorem vonicc

Dummy variables 𝑖 𝑗 𝑛 𝑚 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vonicc.l	. . . . 5 ⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))))
2		vonicc.a	. . . . . . 7 ⊢ (𝜑 → 𝐴:𝑋⟶ℝ)
3	2	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 = ∅) → 𝐴:𝑋⟶ℝ)
4		feq2 6635	. . . . . . 7 ⊢ (𝑋 = ∅ → (𝐴:𝑋⟶ℝ ↔ 𝐴:∅⟶ℝ))
5	4	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 = ∅) → (𝐴:𝑋⟶ℝ ↔ 𝐴:∅⟶ℝ))
6	3, 5	mpbid 232	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 = ∅) → 𝐴:∅⟶ℝ)
7		vonicc.b	. . . . . . 7 ⊢ (𝜑 → 𝐵:𝑋⟶ℝ)
8	7	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 = ∅) → 𝐵:𝑋⟶ℝ)
9		feq2 6635	. . . . . . 7 ⊢ (𝑋 = ∅ → (𝐵:𝑋⟶ℝ ↔ 𝐵:∅⟶ℝ))
10	9	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 = ∅) → (𝐵:𝑋⟶ℝ ↔ 𝐵:∅⟶ℝ))
11	8, 10	mpbid 232	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 = ∅) → 𝐵:∅⟶ℝ)
12	1, 6, 11	hoidmv0val 46706	. . . 4 ⊢ ((𝜑 ∧ 𝑋 = ∅) → (𝐴(𝐿‘∅)𝐵) = 0)
13	12	eqcomd 2739	. . 3 ⊢ ((𝜑 ∧ 𝑋 = ∅) → 0 = (𝐴(𝐿‘∅)𝐵))
14		fveq2 6828	. . . . . 6 ⊢ (𝑋 = ∅ → (voln‘𝑋) = (voln‘∅))
15		vonicc.i	. . . . . . . 8 ⊢ 𝐼 = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐵‘𝑘))
16	15	a1i 11	. . . . . . 7 ⊢ (𝑋 = ∅ → 𝐼 = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐵‘𝑘)))
17		ixpeq1 8838	. . . . . . 7 ⊢ (𝑋 = ∅ → X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐵‘𝑘)) = X𝑘 ∈ ∅ ((𝐴‘𝑘)[,](𝐵‘𝑘)))
18	16, 17	eqtrd 2768	. . . . . 6 ⊢ (𝑋 = ∅ → 𝐼 = X𝑘 ∈ ∅ ((𝐴‘𝑘)[,](𝐵‘𝑘)))
19	14, 18	fveq12d 6835	. . . . 5 ⊢ (𝑋 = ∅ → ((voln‘𝑋)‘𝐼) = ((voln‘∅)‘X𝑘 ∈ ∅ ((𝐴‘𝑘)[,](𝐵‘𝑘))))
20	19	adantl 481	. . . 4 ⊢ ((𝜑 ∧ 𝑋 = ∅) → ((voln‘𝑋)‘𝐼) = ((voln‘∅)‘X𝑘 ∈ ∅ ((𝐴‘𝑘)[,](𝐵‘𝑘))))
21		0fi 8971	. . . . . . 7 ⊢ ∅ ∈ Fin
22	21	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 = ∅) → ∅ ∈ Fin)
23		eqid 2733	. . . . . 6 ⊢ dom (voln‘∅) = dom (voln‘∅)
24	22, 23, 6, 11	iccvonmbl 46802	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 = ∅) → X𝑘 ∈ ∅ ((𝐴‘𝑘)[,](𝐵‘𝑘)) ∈ dom (voln‘∅))
25	24	von0val 46794	. . . 4 ⊢ ((𝜑 ∧ 𝑋 = ∅) → ((voln‘∅)‘X𝑘 ∈ ∅ ((𝐴‘𝑘)[,](𝐵‘𝑘))) = 0)
26	20, 25	eqtrd 2768	. . 3 ⊢ ((𝜑 ∧ 𝑋 = ∅) → ((voln‘𝑋)‘𝐼) = 0)
27		fveq2 6828	. . . . 5 ⊢ (𝑋 = ∅ → (𝐿‘𝑋) = (𝐿‘∅))
28	27	oveqd 7369	. . . 4 ⊢ (𝑋 = ∅ → (𝐴(𝐿‘𝑋)𝐵) = (𝐴(𝐿‘∅)𝐵))
29	28	adantl 481	. . 3 ⊢ ((𝜑 ∧ 𝑋 = ∅) → (𝐴(𝐿‘𝑋)𝐵) = (𝐴(𝐿‘∅)𝐵))
30	13, 26, 29	3eqtr4d 2778	. 2 ⊢ ((𝜑 ∧ 𝑋 = ∅) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵))
31		neqne 2937	. . . 4 ⊢ (¬ 𝑋 = ∅ → 𝑋 ≠ ∅)
32	31	adantl 481	. . 3 ⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → 𝑋 ≠ ∅)
33		nfv 1915	. . . . . . . . 9 ⊢ Ⅎ𝑘(𝜑 ∧ 𝑋 ≠ ∅)
34		nfra1 3257	. . . . . . . . 9 ⊢ Ⅎ𝑘∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)
35	33, 34	nfan 1900	. . . . . . . 8 ⊢ Ⅎ𝑘((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘))
36	2	ffvelcdmda 7023	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈ ℝ)
37	7	ffvelcdmda 7023	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈ ℝ)
38		volico2 46764	. . . . . . . . . . . 12 ⊢ (((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = if((𝐴‘𝑘) ≤ (𝐵‘𝑘), ((𝐵‘𝑘) − (𝐴‘𝑘)), 0))
39	36, 37, 38	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = if((𝐴‘𝑘) ≤ (𝐵‘𝑘), ((𝐵‘𝑘) − (𝐴‘𝑘)), 0))
40	39	ad4ant14 752	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = if((𝐴‘𝑘) ≤ (𝐵‘𝑘), ((𝐵‘𝑘) − (𝐴‘𝑘)), 0))
41		rspa 3222	. . . . . . . . . . . 12 ⊢ ((∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘) ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ≤ (𝐵‘𝑘))
42	41	iftrued 4482	. . . . . . . . . . 11 ⊢ ((∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘) ∧ 𝑘 ∈ 𝑋) → if((𝐴‘𝑘) ≤ (𝐵‘𝑘), ((𝐵‘𝑘) − (𝐴‘𝑘)), 0) = ((𝐵‘𝑘) − (𝐴‘𝑘)))
43	42	adantll 714	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) ∧ 𝑘 ∈ 𝑋) → if((𝐴‘𝑘) ≤ (𝐵‘𝑘), ((𝐵‘𝑘) − (𝐴‘𝑘)), 0) = ((𝐵‘𝑘) − (𝐴‘𝑘)))
44	40, 43	eqtrd 2768	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = ((𝐵‘𝑘) − (𝐴‘𝑘)))
45	44	ex 412	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → (𝑘 ∈ 𝑋 → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = ((𝐵‘𝑘) − (𝐴‘𝑘))))
46	35, 45	ralrimi 3231	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → ∀𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = ((𝐵‘𝑘) − (𝐴‘𝑘)))
47	46	prodeq2d 15830	. . . . . 6 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − (𝐴‘𝑘)))
48	47	eqcomd 2739	. . . . 5 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − (𝐴‘𝑘)) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
49		fveq2 6828	. . . . . . . . . 10 ⊢ (𝑘 = 𝑗 → (𝐴‘𝑘) = (𝐴‘𝑗))
50		fveq2 6828	. . . . . . . . . 10 ⊢ (𝑘 = 𝑗 → (𝐵‘𝑘) = (𝐵‘𝑗))
51	49, 50	breq12d 5106	. . . . . . . . 9 ⊢ (𝑘 = 𝑗 → ((𝐴‘𝑘) ≤ (𝐵‘𝑘) ↔ (𝐴‘𝑗) ≤ (𝐵‘𝑗)))
52	51	cbvralvw 3211	. . . . . . . 8 ⊢ (∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘) ↔ ∀𝑗 ∈ 𝑋 (𝐴‘𝑗) ≤ (𝐵‘𝑗))
53	52	biimpi 216	. . . . . . 7 ⊢ (∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘) → ∀𝑗 ∈ 𝑋 (𝐴‘𝑗) ≤ (𝐵‘𝑗))
54	53	adantl 481	. . . . . 6 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → ∀𝑗 ∈ 𝑋 (𝐴‘𝑗) ≤ (𝐵‘𝑗))
55		vonicc.x	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ∈ Fin)
56	55	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → 𝑋 ∈ Fin)
57	56	adantr 480	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑗 ∈ 𝑋 (𝐴‘𝑗) ≤ (𝐵‘𝑗)) → 𝑋 ∈ Fin)
58	2	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → 𝐴:𝑋⟶ℝ)
59	58	adantr 480	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑗 ∈ 𝑋 (𝐴‘𝑗) ≤ (𝐵‘𝑗)) → 𝐴:𝑋⟶ℝ)
60	7	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → 𝐵:𝑋⟶ℝ)
61	60	adantr 480	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑗 ∈ 𝑋 (𝐴‘𝑗) ≤ (𝐵‘𝑗)) → 𝐵:𝑋⟶ℝ)
62		simpr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → 𝑋 ≠ ∅)
63	62	adantr 480	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑗 ∈ 𝑋 (𝐴‘𝑗) ≤ (𝐵‘𝑗)) → 𝑋 ≠ ∅)
64	52, 41	sylanbr 582	. . . . . . . 8 ⊢ ((∀𝑗 ∈ 𝑋 (𝐴‘𝑗) ≤ (𝐵‘𝑗) ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ≤ (𝐵‘𝑘))
65	64	adantll 714	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑗 ∈ 𝑋 (𝐴‘𝑗) ≤ (𝐵‘𝑗)) ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ≤ (𝐵‘𝑘))
66		fveq2 6828	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑘 → (𝐵‘𝑗) = (𝐵‘𝑘))
67	66	oveq1d 7367	. . . . . . . . . 10 ⊢ (𝑗 = 𝑘 → ((𝐵‘𝑗) + (1 / 𝑚)) = ((𝐵‘𝑘) + (1 / 𝑚)))
68	67	cbvmptv 5197	. . . . . . . . 9 ⊢ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚))) = (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑚)))
69	68	mpteq2i 5189	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚)))) = (𝑚 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑚))))
70		oveq2 7360	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑛 → (1 / 𝑚) = (1 / 𝑛))
71	70	oveq2d 7368	. . . . . . . . . 10 ⊢ (𝑚 = 𝑛 → ((𝐵‘𝑘) + (1 / 𝑚)) = ((𝐵‘𝑘) + (1 / 𝑛)))
72	71	mpteq2dv 5187	. . . . . . . . 9 ⊢ (𝑚 = 𝑛 → (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑚))) = (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑛))))
73	72	cbvmptv 5197	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑚)))) = (𝑛 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑛))))
74	69, 73	eqtri 2756	. . . . . . 7 ⊢ (𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚)))) = (𝑛 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑛))))
75		fveq2 6828	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑛 → ((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚))))‘𝑖) = ((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚))))‘𝑛))
76	75	fveq1d 6830	. . . . . . . . . 10 ⊢ (𝑖 = 𝑛 → (((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚))))‘𝑖)‘𝑘) = (((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚))))‘𝑛)‘𝑘))
77	76	oveq2d 7368	. . . . . . . . 9 ⊢ (𝑖 = 𝑛 → ((𝐴‘𝑘)[,)(((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚))))‘𝑖)‘𝑘)) = ((𝐴‘𝑘)[,)(((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚))))‘𝑛)‘𝑘)))
78	77	ixpeq2dv 8843	. . . . . . . 8 ⊢ (𝑖 = 𝑛 → X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚))))‘𝑖)‘𝑘)) = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚))))‘𝑛)‘𝑘)))
79	78	cbvmptv 5197	. . . . . . 7 ⊢ (𝑖 ∈ ℕ ↦ X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚))))‘𝑖)‘𝑘))) = (𝑛 ∈ ℕ ↦ X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚))))‘𝑛)‘𝑘)))
80	57, 59, 61, 63, 65, 15, 74, 79	vonicclem2 46807	. . . . . 6 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑗 ∈ 𝑋 (𝐴‘𝑗) ≤ (𝐵‘𝑗)) → ((voln‘𝑋)‘𝐼) = ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − (𝐴‘𝑘)))
81	54, 80	syldan 591	. . . . 5 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → ((voln‘𝑋)‘𝐼) = ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − (𝐴‘𝑘)))
82	1, 56, 62, 58, 60	hoidmvn0val 46707	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → (𝐴(𝐿‘𝑋)𝐵) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
83	82	adantr 480	. . . . 5 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → (𝐴(𝐿‘𝑋)𝐵) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
84	48, 81, 83	3eqtr4d 2778	. . . 4 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵))
85		rexnal 3085	. . . . . . . . . 10 ⊢ (∃𝑘 ∈ 𝑋 ¬ (𝐴‘𝑘) ≤ (𝐵‘𝑘) ↔ ¬ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘))
86	85	bicomi 224	. . . . . . . . 9 ⊢ (¬ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘) ↔ ∃𝑘 ∈ 𝑋 ¬ (𝐴‘𝑘) ≤ (𝐵‘𝑘))
87	86	biimpi 216	. . . . . . . 8 ⊢ (¬ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘) → ∃𝑘 ∈ 𝑋 ¬ (𝐴‘𝑘) ≤ (𝐵‘𝑘))
88	87	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → ∃𝑘 ∈ 𝑋 ¬ (𝐴‘𝑘) ≤ (𝐵‘𝑘))
89		simpr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ ¬ (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → ¬ (𝐴‘𝑘) ≤ (𝐵‘𝑘))
90	37	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ ¬ (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → (𝐵‘𝑘) ∈ ℝ)
91	36	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ ¬ (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → (𝐴‘𝑘) ∈ ℝ)
92	90, 91	ltnled 11267	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ ¬ (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → ((𝐵‘𝑘) < (𝐴‘𝑘) ↔ ¬ (𝐴‘𝑘) ≤ (𝐵‘𝑘)))
93	89, 92	mpbird 257	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ ¬ (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → (𝐵‘𝑘) < (𝐴‘𝑘))
94	93	ex 412	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (¬ (𝐴‘𝑘) ≤ (𝐵‘𝑘) → (𝐵‘𝑘) < (𝐴‘𝑘)))
95	94	reximdva 3146	. . . . . . . 8 ⊢ (𝜑 → (∃𝑘 ∈ 𝑋 ¬ (𝐴‘𝑘) ≤ (𝐵‘𝑘) → ∃𝑘 ∈ 𝑋 (𝐵‘𝑘) < (𝐴‘𝑘)))
96	95	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → (∃𝑘 ∈ 𝑋 ¬ (𝐴‘𝑘) ≤ (𝐵‘𝑘) → ∃𝑘 ∈ 𝑋 (𝐵‘𝑘) < (𝐴‘𝑘)))
97	88, 96	mpd 15	. . . . . 6 ⊢ ((𝜑 ∧ ¬ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → ∃𝑘 ∈ 𝑋 (𝐵‘𝑘) < (𝐴‘𝑘))
98	97	adantlr 715	. . . . 5 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ¬ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → ∃𝑘 ∈ 𝑋 (𝐵‘𝑘) < (𝐴‘𝑘))
99		nfcv 2895	. . . . . . . . 9 ⊢ Ⅎ𝑘(voln‘𝑋)
100		nfixp1 8848	. . . . . . . . . 10 ⊢ Ⅎ𝑘X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐵‘𝑘))
101	15, 100	nfcxfr 2893	. . . . . . . . 9 ⊢ Ⅎ𝑘𝐼
102	99, 101	nffv 6838	. . . . . . . 8 ⊢ Ⅎ𝑘((voln‘𝑋)‘𝐼)
103		nfcv 2895	. . . . . . . . 9 ⊢ Ⅎ𝑘𝐴
104		nfcv 2895	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘Fin
105		nfcv 2895	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘(ℝ ↑m 𝑥)
106		nfv 1915	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘 𝑥 = ∅
107		nfcv 2895	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘0
108		nfcv 2895	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘𝑥
109	108	nfcprod1 15817	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))
110	106, 107, 109	nfif 4505	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))
111	105, 105, 110	nfmpo 7434	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘(𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))
112	104, 111	nfmpt 5191	. . . . . . . . . . 11 ⊢ Ⅎ𝑘(𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))))
113	1, 112	nfcxfr 2893	. . . . . . . . . 10 ⊢ Ⅎ𝑘𝐿
114		nfcv 2895	. . . . . . . . . 10 ⊢ Ⅎ𝑘𝑋
115	113, 114	nffv 6838	. . . . . . . . 9 ⊢ Ⅎ𝑘(𝐿‘𝑋)
116		nfcv 2895	. . . . . . . . 9 ⊢ Ⅎ𝑘𝐵
117	103, 115, 116	nfov 7382	. . . . . . . 8 ⊢ Ⅎ𝑘(𝐴(𝐿‘𝑋)𝐵)
118	102, 117	nfeq 2909	. . . . . . 7 ⊢ Ⅎ𝑘((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵)
119	55	vonmea 46697	. . . . . . . . . . . 12 ⊢ (𝜑 → (voln‘𝑋) ∈ Meas)
120	119	mea0 46577	. . . . . . . . . . 11 ⊢ (𝜑 → ((voln‘𝑋)‘∅) = 0)
121	120	3ad2ant1 1133	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → ((voln‘𝑋)‘∅) = 0)
122	15	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → 𝐼 = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐵‘𝑘)))
123		simp2 1137	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → 𝑘 ∈ 𝑋)
124		simp3 1138	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → (𝐵‘𝑘) < (𝐴‘𝑘))
125		ressxr 11163	. . . . . . . . . . . . . . . . . 18 ⊢ ℝ ⊆ ℝ*
126	125, 36	sselid 3928	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈ ℝ*)
127	125, 37	sselid 3928	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈ ℝ*)
128		icc0 13295	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴‘𝑘) ∈ ℝ* ∧ (𝐵‘𝑘) ∈ ℝ*) → (((𝐴‘𝑘)[,](𝐵‘𝑘)) = ∅ ↔ (𝐵‘𝑘) < (𝐴‘𝑘)))
129	126, 127, 128	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (((𝐴‘𝑘)[,](𝐵‘𝑘)) = ∅ ↔ (𝐵‘𝑘) < (𝐴‘𝑘)))
130	129	3adant3 1132	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → (((𝐴‘𝑘)[,](𝐵‘𝑘)) = ∅ ↔ (𝐵‘𝑘) < (𝐴‘𝑘)))
131	124, 130	mpbird 257	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → ((𝐴‘𝑘)[,](𝐵‘𝑘)) = ∅)
132		rspe 3223	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ 𝑋 ∧ ((𝐴‘𝑘)[,](𝐵‘𝑘)) = ∅) → ∃𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐵‘𝑘)) = ∅)
133	123, 131, 132	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → ∃𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐵‘𝑘)) = ∅)
134		ixp0 8861	. . . . . . . . . . . . 13 ⊢ (∃𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐵‘𝑘)) = ∅ → X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐵‘𝑘)) = ∅)
135	133, 134	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐵‘𝑘)) = ∅)
136	122, 135	eqtrd 2768	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → 𝐼 = ∅)
137	136	fveq2d 6832	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → ((voln‘𝑋)‘𝐼) = ((voln‘𝑋)‘∅))
138		ne0i 4290	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ 𝑋 → 𝑋 ≠ ∅)
139	138	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝑋 ≠ ∅)
140	139, 82	syldan 591	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴(𝐿‘𝑋)𝐵) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
141	140	3adant3 1132	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → (𝐴(𝐿‘𝑋)𝐵) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
142		eleq1w 2816	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑘 → (𝑗 ∈ 𝑋 ↔ 𝑘 ∈ 𝑋))
143		fveq2 6828	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝑘 → (𝐴‘𝑗) = (𝐴‘𝑘))
144	66, 143	breq12d 5106	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑘 → ((𝐵‘𝑗) < (𝐴‘𝑗) ↔ (𝐵‘𝑘) < (𝐴‘𝑘)))
145	142, 144	3anbi23d 1441	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑘 → ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) ↔ (𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘))))
146	145	imbi1d 341	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑘 → (((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = 0) ↔ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = 0)))
147		nfv 1915	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘(𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗))
148	55	3ad2ant1 1133	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) → 𝑋 ∈ Fin)
149		volicore 46704	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℝ)
150	36, 37, 149	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℝ)
151	150	recnd 11147	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℂ)
152	151	3ad2antl1 1186	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℂ)
153		simp2 1137	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) → 𝑗 ∈ 𝑋)
154	49, 50	oveq12d 7370	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑗 → ((𝐴‘𝑘)[,)(𝐵‘𝑘)) = ((𝐴‘𝑗)[,)(𝐵‘𝑗)))
155	154	fveq2d 6832	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑗 → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = (vol‘((𝐴‘𝑗)[,)(𝐵‘𝑗))))
156	155	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) ∧ 𝑘 = 𝑗) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = (vol‘((𝐴‘𝑗)[,)(𝐵‘𝑗))))
157	2	ffvelcdmda 7023	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋) → (𝐴‘𝑗) ∈ ℝ)
158	7	ffvelcdmda 7023	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋) → (𝐵‘𝑗) ∈ ℝ)
159		volico2 46764	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴‘𝑗) ∈ ℝ ∧ (𝐵‘𝑗) ∈ ℝ) → (vol‘((𝐴‘𝑗)[,)(𝐵‘𝑗))) = if((𝐴‘𝑗) ≤ (𝐵‘𝑗), ((𝐵‘𝑗) − (𝐴‘𝑗)), 0))
160	157, 158, 159	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋) → (vol‘((𝐴‘𝑗)[,)(𝐵‘𝑗))) = if((𝐴‘𝑗) ≤ (𝐵‘𝑗), ((𝐵‘𝑗) − (𝐴‘𝑗)), 0))
161	160	3adant3 1132	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) → (vol‘((𝐴‘𝑗)[,)(𝐵‘𝑗))) = if((𝐴‘𝑗) ≤ (𝐵‘𝑗), ((𝐵‘𝑗) − (𝐴‘𝑗)), 0))
162		simp3 1138	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) → (𝐵‘𝑗) < (𝐴‘𝑗))
163	158, 157	ltnled 11267	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋) → ((𝐵‘𝑗) < (𝐴‘𝑗) ↔ ¬ (𝐴‘𝑗) ≤ (𝐵‘𝑗)))
164	163	3adant3 1132	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) → ((𝐵‘𝑗) < (𝐴‘𝑗) ↔ ¬ (𝐴‘𝑗) ≤ (𝐵‘𝑗)))
165	162, 164	mpbid 232	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) → ¬ (𝐴‘𝑗) ≤ (𝐵‘𝑗))
166	165	iffalsed 4485	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) → if((𝐴‘𝑗) ≤ (𝐵‘𝑗), ((𝐵‘𝑗) − (𝐴‘𝑗)), 0) = 0)
167	161, 166	eqtrd 2768	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) → (vol‘((𝐴‘𝑗)[,)(𝐵‘𝑗))) = 0)
168	167	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) ∧ 𝑘 = 𝑗) → (vol‘((𝐴‘𝑗)[,)(𝐵‘𝑗))) = 0)
169	156, 168	eqtrd 2768	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) ∧ 𝑘 = 𝑗) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = 0)
170	147, 148, 152, 153, 169	fprodeq0g 15903	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = 0)
171	146, 170	chvarvv 1990	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = 0)
172	141, 171	eqtrd 2768	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → (𝐴(𝐿‘𝑋)𝐵) = 0)
173	121, 137, 172	3eqtr4d 2778	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵))
174	173	3exp 1119	. . . . . . . 8 ⊢ (𝜑 → (𝑘 ∈ 𝑋 → ((𝐵‘𝑘) < (𝐴‘𝑘) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵))))
175	174	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → (𝑘 ∈ 𝑋 → ((𝐵‘𝑘) < (𝐴‘𝑘) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵))))
176	33, 118, 175	rexlimd 3240	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → (∃𝑘 ∈ 𝑋 (𝐵‘𝑘) < (𝐴‘𝑘) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵)))
177	176	imp 406	. . . . 5 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∃𝑘 ∈ 𝑋 (𝐵‘𝑘) < (𝐴‘𝑘)) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵))
178	98, 177	syldan 591	. . . 4 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ¬ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵))
179	84, 178	pm2.61dan 812	. . 3 ⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵))
180	32, 179	syldan 591	. 2 ⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵))
181	30, 180	pm2.61dan 812	1 ⊢ (𝜑 → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1541   ∈ wcel 2113   ≠ wne 2929  ∀wral 3048  ∃wrex 3057  ∅c0 4282  ifcif 4474   class class class wbr 5093   ↦ cmpt 5174  dom cdm 5619  ⟶wf 6482  ‘cfv 6486  (class class class)co 7352   ∈ cmpo 7354   ↑_m cmap 8756  Xcixp 8827  Fincfn 8875  ℂcc 11011  ℝcr 11012  0cc0 11013  1c1 11014   + caddc 11016  ℝ^*cxr 11152   < clt 11153   ≤ cle 11154   − cmin 11351   / cdiv 11781  ℕcn 12132  [,)cico 13249  [,]cicc 13250  ∏cprod 15812  volcvol 25392  volncvoln 46661

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-rep 5219  ax-sep 5236  ax-nul 5246  ax-pow 5305  ax-pr 5372  ax-un 7674  ax-inf2 9538  ax-cc 10333  ax-ac2 10361  ax-cnex 11069  ax-resscn 11070  ax-1cn 11071  ax-icn 11072  ax-addcl 11073  ax-addrcl 11074  ax-mulcl 11075  ax-mulrcl 11076  ax-mulcom 11077  ax-addass 11078  ax-mulass 11079  ax-distr 11080  ax-i2m1 11081  ax-1ne0 11082  ax-1rid 11083  ax-rnegex 11084  ax-rrecex 11085  ax-cnre 11086  ax-pre-lttri 11087  ax-pre-lttrn 11088  ax-pre-ltadd 11089  ax-pre-mulgt0 11090  ax-pre-sup 11091  ax-addf 11092  ax-mulf 11093

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-nel 3034  df-ral 3049  df-rex 3058  df-rmo 3347  df-reu 3348  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-tp 4580  df-op 4582  df-uni 4859  df-int 4898  df-iun 4943  df-iin 4944  df-disj 5061  df-br 5094  df-opab 5156  df-mpt 5175  df-tr 5201  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-se 5573  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-pred 6253  df-ord 6314  df-on 6315  df-lim 6316  df-suc 6317  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-isom 6495  df-riota 7309  df-ov 7355  df-oprab 7356  df-mpo 7357  df-of 7616  df-om 7803  df-1st 7927  df-2nd 7928  df-supp 8097  df-tpos 8162  df-frecs 8217  df-wrecs 8248  df-recs 8297  df-rdg 8335  df-1o 8391  df-2o 8392  df-oadd 8395  df-omul 8396  df-er 8628  df-map 8758  df-pm 8759  df-ixp 8828  df-en 8876  df-dom 8877  df-sdom 8878  df-fin 8879  df-fsupp 9253  df-fi 9302  df-sup 9333  df-inf 9334  df-oi 9403  df-dju 9801  df-card 9839  df-acn 9842  df-ac 10014  df-pnf 11155  df-mnf 11156  df-xr 11157  df-ltxr 11158  df-le 11159  df-sub 11353  df-neg 11354  df-div 11782  df-nn 12133  df-2 12195  df-3 12196  df-4 12197  df-5 12198  df-6 12199  df-7 12200  df-8 12201  df-9 12202  df-n0 12389  df-z 12476  df-dec 12595  df-uz 12739  df-q 12849  df-rp 12893  df-xneg 13013  df-xadd 13014  df-xmul 13015  df-ioo 13251  df-ico 13253  df-icc 13254  df-fz 13410  df-fzo 13557  df-fl 13698  df-seq 13911  df-exp 13971  df-hash 14240  df-cj 15008  df-re 15009  df-im 15010  df-sqrt 15144  df-abs 15145  df-clim 15397  df-rlim 15398  df-sum 15596  df-prod 15813  df-struct 17060  df-sets 17077  df-slot 17095  df-ndx 17107  df-base 17123  df-ress 17144  df-plusg 17176  df-mulr 17177  df-starv 17178  df-sca 17179  df-vsca 17180  df-ip 17181  df-tset 17182  df-ple 17183  df-ds 17185  df-unif 17186  df-hom 17187  df-cco 17188  df-rest 17328  df-topn 17329  df-0g 17347  df-gsum 17348  df-topgen 17349  df-pt 17350  df-prds 17353  df-pws 17355  df-xrs 17408  df-qtop 17413  df-imas 17414  df-xps 17416  df-mre 17490  df-mrc 17491  df-acs 17493  df-mgm 18550  df-sgrp 18629  df-mnd 18645  df-mhm 18693  df-submnd 18694  df-grp 18851  df-minusg 18852  df-sbg 18853  df-mulg 18983  df-subg 19038  df-ghm 19127  df-cntz 19231  df-cmn 19696  df-abl 19697  df-mgp 20061  df-rng 20073  df-ur 20102  df-ring 20155  df-cring 20156  df-oppr 20257  df-dvdsr 20277  df-unit 20278  df-invr 20308  df-dvr 20321  df-rhm 20392  df-subrng 20463  df-subrg 20487  df-drng 20648  df-field 20649  df-abv 20726  df-staf 20756  df-srng 20757  df-lmod 20797  df-lss 20867  df-lmhm 20958  df-lvec 21039  df-sra 21109  df-rgmod 21110  df-psmet 21285  df-xmet 21286  df-met 21287  df-bl 21288  df-mopn 21289  df-cnfld 21294  df-refld 21544  df-phl 21565  df-dsmm 21671  df-frlm 21686  df-top 22810  df-topon 22827  df-topsp 22849  df-bases 22862  df-cn 23143  df-cnp 23144  df-cmp 23303  df-tx 23478  df-hmeo 23671  df-xms 24236  df-ms 24237  df-tms 24238  df-nm 24498  df-ngp 24499  df-tng 24500  df-nrg 24501  df-nlm 24502  df-cncf 24799  df-clm 24991  df-cph 25096  df-tcph 25097  df-rrx 25313  df-ovol 25393  df-vol 25394  df-salg 46432  df-sumge0 46486  df-mea 46573  df-ome 46613  df-caragen 46615  df-ovoln 46660  df-voln 46662

This theorem is referenced by:  vonn0icc  46811