Theorem vonicc 46606

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 6729	. . . . . . 7 ⊢ (𝑋 = ∅ → (𝐴:𝑋⟶ℝ ↔ 𝐴:∅⟶ℝ))
5	4	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 = ∅) → (𝐴:𝑋⟶ℝ ↔ 𝐴:∅⟶ℝ))
6	3, 5	mpbid 232	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 = ∅) → 𝐴:∅⟶ℝ)
7		vonicc.b	. . . . . . 7 ⊢ (𝜑 → 𝐵:𝑋⟶ℝ)
8	7	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 = ∅) → 𝐵:𝑋⟶ℝ)
9		feq2 6729	. . . . . . 7 ⊢ (𝑋 = ∅ → (𝐵:𝑋⟶ℝ ↔ 𝐵:∅⟶ℝ))
10	9	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 = ∅) → (𝐵:𝑋⟶ℝ ↔ 𝐵:∅⟶ℝ))
11	8, 10	mpbid 232	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 = ∅) → 𝐵:∅⟶ℝ)
12	1, 6, 11	hoidmv0val 46504	. . . 4 ⊢ ((𝜑 ∧ 𝑋 = ∅) → (𝐴(𝐿‘∅)𝐵) = 0)
13	12	eqcomd 2746	. . 3 ⊢ ((𝜑 ∧ 𝑋 = ∅) → 0 = (𝐴(𝐿‘∅)𝐵))
14		fveq2 6920	. . . . . 6 ⊢ (𝑋 = ∅ → (voln‘𝑋) = (voln‘∅))
15		vonicc.i	. . . . . . . 8 ⊢ 𝐼 = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐵‘𝑘))
16	15	a1i 11	. . . . . . 7 ⊢ (𝑋 = ∅ → 𝐼 = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐵‘𝑘)))
17		ixpeq1 8966	. . . . . . 7 ⊢ (𝑋 = ∅ → X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐵‘𝑘)) = X𝑘 ∈ ∅ ((𝐴‘𝑘)[,](𝐵‘𝑘)))
18	16, 17	eqtrd 2780	. . . . . 6 ⊢ (𝑋 = ∅ → 𝐼 = X𝑘 ∈ ∅ ((𝐴‘𝑘)[,](𝐵‘𝑘)))
19	14, 18	fveq12d 6927	. . . . 5 ⊢ (𝑋 = ∅ → ((voln‘𝑋)‘𝐼) = ((voln‘∅)‘X𝑘 ∈ ∅ ((𝐴‘𝑘)[,](𝐵‘𝑘))))
20	19	adantl 481	. . . 4 ⊢ ((𝜑 ∧ 𝑋 = ∅) → ((voln‘𝑋)‘𝐼) = ((voln‘∅)‘X𝑘 ∈ ∅ ((𝐴‘𝑘)[,](𝐵‘𝑘))))
21		0fi 9108	. . . . . . 7 ⊢ ∅ ∈ Fin
22	21	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 = ∅) → ∅ ∈ Fin)
23		eqid 2740	. . . . . 6 ⊢ dom (voln‘∅) = dom (voln‘∅)
24	22, 23, 6, 11	iccvonmbl 46600	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 = ∅) → X𝑘 ∈ ∅ ((𝐴‘𝑘)[,](𝐵‘𝑘)) ∈ dom (voln‘∅))
25	24	von0val 46592	. . . 4 ⊢ ((𝜑 ∧ 𝑋 = ∅) → ((voln‘∅)‘X𝑘 ∈ ∅ ((𝐴‘𝑘)[,](𝐵‘𝑘))) = 0)
26	20, 25	eqtrd 2780	. . 3 ⊢ ((𝜑 ∧ 𝑋 = ∅) → ((voln‘𝑋)‘𝐼) = 0)
27		fveq2 6920	. . . . 5 ⊢ (𝑋 = ∅ → (𝐿‘𝑋) = (𝐿‘∅))
28	27	oveqd 7465	. . . 4 ⊢ (𝑋 = ∅ → (𝐴(𝐿‘𝑋)𝐵) = (𝐴(𝐿‘∅)𝐵))
29	28	adantl 481	. . 3 ⊢ ((𝜑 ∧ 𝑋 = ∅) → (𝐴(𝐿‘𝑋)𝐵) = (𝐴(𝐿‘∅)𝐵))
30	13, 26, 29	3eqtr4d 2790	. 2 ⊢ ((𝜑 ∧ 𝑋 = ∅) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵))
31		neqne 2954	. . . 4 ⊢ (¬ 𝑋 = ∅ → 𝑋 ≠ ∅)
32	31	adantl 481	. . 3 ⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → 𝑋 ≠ ∅)
33		nfv 1913	. . . . . . . . 9 ⊢ Ⅎ𝑘(𝜑 ∧ 𝑋 ≠ ∅)
34		nfra1 3290	. . . . . . . . 9 ⊢ Ⅎ𝑘∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)
35	33, 34	nfan 1898	. . . . . . . 8 ⊢ Ⅎ𝑘((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘))
36	2	ffvelcdmda 7118	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈ ℝ)
37	7	ffvelcdmda 7118	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈ ℝ)
38		volico2 46562	. . . . . . . . . . . 12 ⊢ (((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = if((𝐴‘𝑘) ≤ (𝐵‘𝑘), ((𝐵‘𝑘) − (𝐴‘𝑘)), 0))
39	36, 37, 38	syl2anc 583	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = if((𝐴‘𝑘) ≤ (𝐵‘𝑘), ((𝐵‘𝑘) − (𝐴‘𝑘)), 0))
40	39	ad4ant14 751	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = if((𝐴‘𝑘) ≤ (𝐵‘𝑘), ((𝐵‘𝑘) − (𝐴‘𝑘)), 0))
41		rspa 3254	. . . . . . . . . . . 12 ⊢ ((∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘) ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ≤ (𝐵‘𝑘))
42	41	iftrued 4556	. . . . . . . . . . 11 ⊢ ((∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘) ∧ 𝑘 ∈ 𝑋) → if((𝐴‘𝑘) ≤ (𝐵‘𝑘), ((𝐵‘𝑘) − (𝐴‘𝑘)), 0) = ((𝐵‘𝑘) − (𝐴‘𝑘)))
43	42	adantll 713	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) ∧ 𝑘 ∈ 𝑋) → if((𝐴‘𝑘) ≤ (𝐵‘𝑘), ((𝐵‘𝑘) − (𝐴‘𝑘)), 0) = ((𝐵‘𝑘) − (𝐴‘𝑘)))
44	40, 43	eqtrd 2780	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = ((𝐵‘𝑘) − (𝐴‘𝑘)))
45	44	ex 412	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → (𝑘 ∈ 𝑋 → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = ((𝐵‘𝑘) − (𝐴‘𝑘))))
46	35, 45	ralrimi 3263	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → ∀𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = ((𝐵‘𝑘) − (𝐴‘𝑘)))
47	46	prodeq2d 15969	. . . . . 6 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − (𝐴‘𝑘)))
48	47	eqcomd 2746	. . . . 5 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − (𝐴‘𝑘)) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
49		fveq2 6920	. . . . . . . . . 10 ⊢ (𝑘 = 𝑗 → (𝐴‘𝑘) = (𝐴‘𝑗))
50		fveq2 6920	. . . . . . . . . 10 ⊢ (𝑘 = 𝑗 → (𝐵‘𝑘) = (𝐵‘𝑗))
51	49, 50	breq12d 5179	. . . . . . . . 9 ⊢ (𝑘 = 𝑗 → ((𝐴‘𝑘) ≤ (𝐵‘𝑘) ↔ (𝐴‘𝑗) ≤ (𝐵‘𝑗)))
52	51	cbvralvw 3243	. . . . . . . 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 581	. . . . . . . 8 ⊢ ((∀𝑗 ∈ 𝑋 (𝐴‘𝑗) ≤ (𝐵‘𝑗) ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ≤ (𝐵‘𝑘))
65	64	adantll 713	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑗 ∈ 𝑋 (𝐴‘𝑗) ≤ (𝐵‘𝑗)) ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ≤ (𝐵‘𝑘))
66		fveq2 6920	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑘 → (𝐵‘𝑗) = (𝐵‘𝑘))
67	66	oveq1d 7463	. . . . . . . . . 10 ⊢ (𝑗 = 𝑘 → ((𝐵‘𝑗) + (1 / 𝑚)) = ((𝐵‘𝑘) + (1 / 𝑚)))
68	67	cbvmptv 5279	. . . . . . . . 9 ⊢ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚))) = (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑚)))
69	68	mpteq2i 5271	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚)))) = (𝑚 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑚))))
70		oveq2 7456	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑛 → (1 / 𝑚) = (1 / 𝑛))
71	70	oveq2d 7464	. . . . . . . . . 10 ⊢ (𝑚 = 𝑛 → ((𝐵‘𝑘) + (1 / 𝑚)) = ((𝐵‘𝑘) + (1 / 𝑛)))
72	71	mpteq2dv 5268	. . . . . . . . 9 ⊢ (𝑚 = 𝑛 → (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑚))) = (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑛))))
73	72	cbvmptv 5279	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑚)))) = (𝑛 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑛))))
74	69, 73	eqtri 2768	. . . . . . 7 ⊢ (𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚)))) = (𝑛 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑛))))
75		fveq2 6920	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑛 → ((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚))))‘𝑖) = ((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚))))‘𝑛))
76	75	fveq1d 6922	. . . . . . . . . 10 ⊢ (𝑖 = 𝑛 → (((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚))))‘𝑖)‘𝑘) = (((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚))))‘𝑛)‘𝑘))
77	76	oveq2d 7464	. . . . . . . . 9 ⊢ (𝑖 = 𝑛 → ((𝐴‘𝑘)[,)(((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚))))‘𝑖)‘𝑘)) = ((𝐴‘𝑘)[,)(((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚))))‘𝑛)‘𝑘)))
78	77	ixpeq2dv 8971	. . . . . . . 8 ⊢ (𝑖 = 𝑛 → X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚))))‘𝑖)‘𝑘)) = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚))))‘𝑛)‘𝑘)))
79	78	cbvmptv 5279	. . . . . . 7 ⊢ (𝑖 ∈ ℕ ↦ X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚))))‘𝑖)‘𝑘))) = (𝑛 ∈ ℕ ↦ X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚))))‘𝑛)‘𝑘)))
80	57, 59, 61, 63, 65, 15, 74, 79	vonicclem2 46605	. . . . . 6 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑗 ∈ 𝑋 (𝐴‘𝑗) ≤ (𝐵‘𝑗)) → ((voln‘𝑋)‘𝐼) = ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − (𝐴‘𝑘)))
81	54, 80	syldan 590	. . . . 5 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → ((voln‘𝑋)‘𝐼) = ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − (𝐴‘𝑘)))
82	1, 56, 62, 58, 60	hoidmvn0val 46505	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → (𝐴(𝐿‘𝑋)𝐵) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
83	82	adantr 480	. . . . 5 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → (𝐴(𝐿‘𝑋)𝐵) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
84	48, 81, 83	3eqtr4d 2790	. . . 4 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵))
85		rexnal 3106	. . . . . . . . . 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 11437	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ ¬ (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → ((𝐵‘𝑘) < (𝐴‘𝑘) ↔ ¬ (𝐴‘𝑘) ≤ (𝐵‘𝑘)))
93	89, 92	mpbird 257	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ ¬ (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → (𝐵‘𝑘) < (𝐴‘𝑘))
94	93	ex 412	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (¬ (𝐴‘𝑘) ≤ (𝐵‘𝑘) → (𝐵‘𝑘) < (𝐴‘𝑘)))
95	94	reximdva 3174	. . . . . . . 8 ⊢ (𝜑 → (∃𝑘 ∈ 𝑋 ¬ (𝐴‘𝑘) ≤ (𝐵‘𝑘) → ∃𝑘 ∈ 𝑋 (𝐵‘𝑘) < (𝐴‘𝑘)))
96	95	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → (∃𝑘 ∈ 𝑋 ¬ (𝐴‘𝑘) ≤ (𝐵‘𝑘) → ∃𝑘 ∈ 𝑋 (𝐵‘𝑘) < (𝐴‘𝑘)))
97	88, 96	mpd 15	. . . . . 6 ⊢ ((𝜑 ∧ ¬ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → ∃𝑘 ∈ 𝑋 (𝐵‘𝑘) < (𝐴‘𝑘))
98	97	adantlr 714	. . . . 5 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ¬ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → ∃𝑘 ∈ 𝑋 (𝐵‘𝑘) < (𝐴‘𝑘))
99		nfcv 2908	. . . . . . . . 9 ⊢ Ⅎ𝑘(voln‘𝑋)
100		nfixp1 8976	. . . . . . . . . 10 ⊢ Ⅎ𝑘X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐵‘𝑘))
101	15, 100	nfcxfr 2906	. . . . . . . . 9 ⊢ Ⅎ𝑘𝐼
102	99, 101	nffv 6930	. . . . . . . 8 ⊢ Ⅎ𝑘((voln‘𝑋)‘𝐼)
103		nfcv 2908	. . . . . . . . 9 ⊢ Ⅎ𝑘𝐴
104		nfcv 2908	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘Fin
105		nfcv 2908	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘(ℝ ↑m 𝑥)
106		nfv 1913	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘 𝑥 = ∅
107		nfcv 2908	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘0
108		nfcv 2908	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘𝑥
109	108	nfcprod1 15956	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))
110	106, 107, 109	nfif 4578	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))
111	105, 105, 110	nfmpo 7532	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘(𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))
112	104, 111	nfmpt 5273	. . . . . . . . . . 11 ⊢ Ⅎ𝑘(𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))))
113	1, 112	nfcxfr 2906	. . . . . . . . . 10 ⊢ Ⅎ𝑘𝐿
114		nfcv 2908	. . . . . . . . . 10 ⊢ Ⅎ𝑘𝑋
115	113, 114	nffv 6930	. . . . . . . . 9 ⊢ Ⅎ𝑘(𝐿‘𝑋)
116		nfcv 2908	. . . . . . . . 9 ⊢ Ⅎ𝑘𝐵
117	103, 115, 116	nfov 7478	. . . . . . . 8 ⊢ Ⅎ𝑘(𝐴(𝐿‘𝑋)𝐵)
118	102, 117	nfeq 2922	. . . . . . 7 ⊢ Ⅎ𝑘((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵)
119	55	vonmea 46495	. . . . . . . . . . . 12 ⊢ (𝜑 → (voln‘𝑋) ∈ Meas)
120	119	mea0 46375	. . . . . . . . . . 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 11334	. . . . . . . . . . . . . . . . . 18 ⊢ ℝ ⊆ ℝ*
126	125, 36	sselid 4006	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈ ℝ*)
127	125, 37	sselid 4006	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈ ℝ*)
128		icc0 13455	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴‘𝑘) ∈ ℝ* ∧ (𝐵‘𝑘) ∈ ℝ*) → (((𝐴‘𝑘)[,](𝐵‘𝑘)) = ∅ ↔ (𝐵‘𝑘) < (𝐴‘𝑘)))
129	126, 127, 128	syl2anc 583	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (((𝐴‘𝑘)[,](𝐵‘𝑘)) = ∅ ↔ (𝐵‘𝑘) < (𝐴‘𝑘)))
130	129	3adant3 1132	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → (((𝐴‘𝑘)[,](𝐵‘𝑘)) = ∅ ↔ (𝐵‘𝑘) < (𝐴‘𝑘)))
131	124, 130	mpbird 257	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → ((𝐴‘𝑘)[,](𝐵‘𝑘)) = ∅)
132		rspe 3255	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ 𝑋 ∧ ((𝐴‘𝑘)[,](𝐵‘𝑘)) = ∅) → ∃𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐵‘𝑘)) = ∅)
133	123, 131, 132	syl2anc 583	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → ∃𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐵‘𝑘)) = ∅)
134		ixp0 8989	. . . . . . . . . . . . 13 ⊢ (∃𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐵‘𝑘)) = ∅ → X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐵‘𝑘)) = ∅)
135	133, 134	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐵‘𝑘)) = ∅)
136	122, 135	eqtrd 2780	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → 𝐼 = ∅)
137	136	fveq2d 6924	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → ((voln‘𝑋)‘𝐼) = ((voln‘𝑋)‘∅))
138		ne0i 4364	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ 𝑋 → 𝑋 ≠ ∅)
139	138	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝑋 ≠ ∅)
140	139, 82	syldan 590	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴(𝐿‘𝑋)𝐵) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
141	140	3adant3 1132	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → (𝐴(𝐿‘𝑋)𝐵) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
142		eleq1w 2827	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑘 → (𝑗 ∈ 𝑋 ↔ 𝑘 ∈ 𝑋))
143		fveq2 6920	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝑘 → (𝐴‘𝑗) = (𝐴‘𝑘))
144	66, 143	breq12d 5179	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑘 → ((𝐵‘𝑗) < (𝐴‘𝑗) ↔ (𝐵‘𝑘) < (𝐴‘𝑘)))
145	142, 144	3anbi23d 1439	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑘 → ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) ↔ (𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘))))
146	145	imbi1d 341	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑘 → (((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = 0) ↔ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = 0)))
147		nfv 1913	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘(𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗))
148	55	3ad2ant1 1133	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) → 𝑋 ∈ Fin)
149		volicore 46502	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℝ)
150	36, 37, 149	syl2anc 583	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℝ)
151	150	recnd 11318	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℂ)
152	151	3ad2antl1 1185	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℂ)
153		simp2 1137	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) → 𝑗 ∈ 𝑋)
154	49, 50	oveq12d 7466	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑗 → ((𝐴‘𝑘)[,)(𝐵‘𝑘)) = ((𝐴‘𝑗)[,)(𝐵‘𝑗)))
155	154	fveq2d 6924	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑗 → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = (vol‘((𝐴‘𝑗)[,)(𝐵‘𝑗))))
156	155	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) ∧ 𝑘 = 𝑗) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = (vol‘((𝐴‘𝑗)[,)(𝐵‘𝑗))))
157	2	ffvelcdmda 7118	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋) → (𝐴‘𝑗) ∈ ℝ)
158	7	ffvelcdmda 7118	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋) → (𝐵‘𝑗) ∈ ℝ)
159		volico2 46562	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴‘𝑗) ∈ ℝ ∧ (𝐵‘𝑗) ∈ ℝ) → (vol‘((𝐴‘𝑗)[,)(𝐵‘𝑗))) = if((𝐴‘𝑗) ≤ (𝐵‘𝑗), ((𝐵‘𝑗) − (𝐴‘𝑗)), 0))
160	157, 158, 159	syl2anc 583	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋) → (vol‘((𝐴‘𝑗)[,)(𝐵‘𝑗))) = if((𝐴‘𝑗) ≤ (𝐵‘𝑗), ((𝐵‘𝑗) − (𝐴‘𝑗)), 0))
161	160	3adant3 1132	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) → (vol‘((𝐴‘𝑗)[,)(𝐵‘𝑗))) = if((𝐴‘𝑗) ≤ (𝐵‘𝑗), ((𝐵‘𝑗) − (𝐴‘𝑗)), 0))
162		simp3 1138	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) → (𝐵‘𝑗) < (𝐴‘𝑗))
163	158, 157	ltnled 11437	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋) → ((𝐵‘𝑗) < (𝐴‘𝑗) ↔ ¬ (𝐴‘𝑗) ≤ (𝐵‘𝑗)))
164	163	3adant3 1132	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) → ((𝐵‘𝑗) < (𝐴‘𝑗) ↔ ¬ (𝐴‘𝑗) ≤ (𝐵‘𝑗)))
165	162, 164	mpbid 232	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) → ¬ (𝐴‘𝑗) ≤ (𝐵‘𝑗))
166	165	iffalsed 4559	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) → if((𝐴‘𝑗) ≤ (𝐵‘𝑗), ((𝐵‘𝑗) − (𝐴‘𝑗)), 0) = 0)
167	161, 166	eqtrd 2780	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) → (vol‘((𝐴‘𝑗)[,)(𝐵‘𝑗))) = 0)
168	167	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) ∧ 𝑘 = 𝑗) → (vol‘((𝐴‘𝑗)[,)(𝐵‘𝑗))) = 0)
169	156, 168	eqtrd 2780	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) ∧ 𝑘 = 𝑗) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = 0)
170	147, 148, 152, 153, 169	fprodeq0g 16042	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = 0)
171	146, 170	chvarvv 1998	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = 0)
172	141, 171	eqtrd 2780	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → (𝐴(𝐿‘𝑋)𝐵) = 0)
173	121, 137, 172	3eqtr4d 2790	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵))
174	173	3exp 1119	. . . . . . . 8 ⊢ (𝜑 → (𝑘 ∈ 𝑋 → ((𝐵‘𝑘) < (𝐴‘𝑘) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵))))
175	174	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → (𝑘 ∈ 𝑋 → ((𝐵‘𝑘) < (𝐴‘𝑘) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵))))
176	33, 118, 175	rexlimd 3272	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → (∃𝑘 ∈ 𝑋 (𝐵‘𝑘) < (𝐴‘𝑘) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵)))
177	176	imp 406	. . . . 5 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∃𝑘 ∈ 𝑋 (𝐵‘𝑘) < (𝐴‘𝑘)) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵))
178	98, 177	syldan 590	. . . 4 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ¬ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵))
179	84, 178	pm2.61dan 812	. . 3 ⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵))
180	32, 179	syldan 590	. 2 ⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵))
181	30, 180	pm2.61dan 812	1 ⊢ (𝜑 → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1537   ∈ wcel 2108   ≠ wne 2946  ∀wral 3067  ∃wrex 3076  ∅c0 4352  ifcif 4548   class class class wbr 5166   ↦ cmpt 5249  dom cdm 5700  ⟶wf 6569  ‘cfv 6573  (class class class)co 7448   ∈ cmpo 7450   ↑_m cmap 8884  Xcixp 8955  Fincfn 9003  ℂcc 11182  ℝcr 11183  0cc0 11184  1c1 11185   + caddc 11187  ℝ^*cxr 11323   < clt 11324   ≤ cle 11325   − cmin 11520   / cdiv 11947  ℕcn 12293  [,)cico 13409  [,]cicc 13410  ∏cprod 15951  volcvol 25517  volncvoln 46459

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-rep 5303  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-inf2 9710  ax-cc 10504  ax-ac2 10532  ax-cnex 11240  ax-resscn 11241  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-mulcom 11248  ax-addass 11249  ax-mulass 11250  ax-distr 11251  ax-i2m1 11252  ax-1ne0 11253  ax-1rid 11254  ax-rnegex 11255  ax-rrecex 11256  ax-cnre 11257  ax-pre-lttri 11258  ax-pre-lttrn 11259  ax-pre-ltadd 11260  ax-pre-mulgt0 11261  ax-pre-sup 11262  ax-addf 11263  ax-mulf 11264

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-tp 4653  df-op 4655  df-uni 4932  df-int 4971  df-iun 5017  df-iin 5018  df-disj 5134  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-se 5653  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-isom 6582  df-riota 7404  df-ov 7451  df-oprab 7452  df-mpo 7453  df-of 7714  df-om 7904  df-1st 8030  df-2nd 8031  df-supp 8202  df-tpos 8267  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-1o 8522  df-2o 8523  df-oadd 8526  df-omul 8527  df-er 8763  df-map 8886  df-pm 8887  df-ixp 8956  df-en 9004  df-dom 9005  df-sdom 9006  df-fin 9007  df-fsupp 9432  df-fi 9480  df-sup 9511  df-inf 9512  df-oi 9579  df-dju 9970  df-card 10008  df-acn 10011  df-ac 10185  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-sub 11522  df-neg 11523  df-div 11948  df-nn 12294  df-2 12356  df-3 12357  df-4 12358  df-5 12359  df-6 12360  df-7 12361  df-8 12362  df-9 12363  df-n0 12554  df-z 12640  df-dec 12759  df-uz 12904  df-q 13014  df-rp 13058  df-xneg 13175  df-xadd 13176  df-xmul 13177  df-ioo 13411  df-ico 13413  df-icc 13414  df-fz 13568  df-fzo 13712  df-fl 13843  df-seq 14053  df-exp 14113  df-hash 14380  df-cj 15148  df-re 15149  df-im 15150  df-sqrt 15284  df-abs 15285  df-clim 15534  df-rlim 15535  df-sum 15735  df-prod 15952  df-struct 17194  df-sets 17211  df-slot 17229  df-ndx 17241  df-base 17259  df-ress 17288  df-plusg 17324  df-mulr 17325  df-starv 17326  df-sca 17327  df-vsca 17328  df-ip 17329  df-tset 17330  df-ple 17331  df-ds 17333  df-unif 17334  df-hom 17335  df-cco 17336  df-rest 17482  df-topn 17483  df-0g 17501  df-gsum 17502  df-topgen 17503  df-pt 17504  df-prds 17507  df-pws 17509  df-xrs 17562  df-qtop 17567  df-imas 17568  df-xps 17570  df-mre 17644  df-mrc 17645  df-acs 17647  df-mgm 18678  df-sgrp 18757  df-mnd 18773  df-mhm 18818  df-submnd 18819  df-grp 18976  df-minusg 18977  df-sbg 18978  df-mulg 19108  df-subg 19163  df-ghm 19253  df-cntz 19357  df-cmn 19824  df-abl 19825  df-mgp 20162  df-rng 20180  df-ur 20209  df-ring 20262  df-cring 20263  df-oppr 20360  df-dvdsr 20383  df-unit 20384  df-invr 20414  df-dvr 20427  df-rhm 20498  df-subrng 20572  df-subrg 20597  df-drng 20753  df-field 20754  df-abv 20832  df-staf 20862  df-srng 20863  df-lmod 20882  df-lss 20953  df-lmhm 21044  df-lvec 21125  df-sra 21195  df-rgmod 21196  df-psmet 21379  df-xmet 21380  df-met 21381  df-bl 21382  df-mopn 21383  df-cnfld 21388  df-refld 21646  df-phl 21667  df-dsmm 21775  df-frlm 21790  df-top 22921  df-topon 22938  df-topsp 22960  df-bases 22974  df-cn 23256  df-cnp 23257  df-cmp 23416  df-tx 23591  df-hmeo 23784  df-xms 24351  df-ms 24352  df-tms 24353  df-nm 24616  df-ngp 24617  df-tng 24618  df-nrg 24619  df-nlm 24620  df-cncf 24923  df-clm 25115  df-cph 25221  df-tcph 25222  df-rrx 25438  df-ovol 25518  df-vol 25519  df-salg 46230  df-sumge0 46284  df-mea 46371  df-ome 46411  df-caragen 46413  df-ovoln 46458  df-voln 46460

This theorem is referenced by:  vonn0icc  46609