vonicc - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > vonicc		Structured version Visualization version GIF version

Theorem vonicc 47037

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 6649	. . . . . . 7 ⊢ (𝑋 = ∅ → (𝐴:𝑋⟶ℝ ↔ 𝐴:∅⟶ℝ))
5	4	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 = ∅) → (𝐴:𝑋⟶ℝ ↔ 𝐴:∅⟶ℝ))
6	3, 5	mpbid 232	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 = ∅) → 𝐴:∅⟶ℝ)
7		vonicc.b	. . . . . . 7 ⊢ (𝜑 → 𝐵:𝑋⟶ℝ)
8	7	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 = ∅) → 𝐵:𝑋⟶ℝ)
9		feq2 6649	. . . . . . 7 ⊢ (𝑋 = ∅ → (𝐵:𝑋⟶ℝ ↔ 𝐵:∅⟶ℝ))
10	9	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 = ∅) → (𝐵:𝑋⟶ℝ ↔ 𝐵:∅⟶ℝ))
11	8, 10	mpbid 232	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 = ∅) → 𝐵:∅⟶ℝ)
12	1, 6, 11	hoidmv0val 46935	. . . 4 ⊢ ((𝜑 ∧ 𝑋 = ∅) → (𝐴(𝐿‘∅)𝐵) = 0)
13	12	eqcomd 2743	. . 3 ⊢ ((𝜑 ∧ 𝑋 = ∅) → 0 = (𝐴(𝐿‘∅)𝐵))
14		fveq2 6842	. . . . . 6 ⊢ (𝑋 = ∅ → (voln‘𝑋) = (voln‘∅))
15		vonicc.i	. . . . . . . 8 ⊢ 𝐼 = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐵‘𝑘))
16	15	a1i 11	. . . . . . 7 ⊢ (𝑋 = ∅ → 𝐼 = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐵‘𝑘)))
17		ixpeq1 8858	. . . . . . 7 ⊢ (𝑋 = ∅ → X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐵‘𝑘)) = X𝑘 ∈ ∅ ((𝐴‘𝑘)[,](𝐵‘𝑘)))
18	16, 17	eqtrd 2772	. . . . . 6 ⊢ (𝑋 = ∅ → 𝐼 = X𝑘 ∈ ∅ ((𝐴‘𝑘)[,](𝐵‘𝑘)))
19	14, 18	fveq12d 6849	. . . . 5 ⊢ (𝑋 = ∅ → ((voln‘𝑋)‘𝐼) = ((voln‘∅)‘X𝑘 ∈ ∅ ((𝐴‘𝑘)[,](𝐵‘𝑘))))
20	19	adantl 481	. . . 4 ⊢ ((𝜑 ∧ 𝑋 = ∅) → ((voln‘𝑋)‘𝐼) = ((voln‘∅)‘X𝑘 ∈ ∅ ((𝐴‘𝑘)[,](𝐵‘𝑘))))
21		0fi 8991	. . . . . . 7 ⊢ ∅ ∈ Fin
22	21	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 = ∅) → ∅ ∈ Fin)
23		eqid 2737	. . . . . 6 ⊢ dom (voln‘∅) = dom (voln‘∅)
24	22, 23, 6, 11	iccvonmbl 47031	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 = ∅) → X𝑘 ∈ ∅ ((𝐴‘𝑘)[,](𝐵‘𝑘)) ∈ dom (voln‘∅))
25	24	von0val 47023	. . . 4 ⊢ ((𝜑 ∧ 𝑋 = ∅) → ((voln‘∅)‘X𝑘 ∈ ∅ ((𝐴‘𝑘)[,](𝐵‘𝑘))) = 0)
26	20, 25	eqtrd 2772	. . 3 ⊢ ((𝜑 ∧ 𝑋 = ∅) → ((voln‘𝑋)‘𝐼) = 0)
27		fveq2 6842	. . . . 5 ⊢ (𝑋 = ∅ → (𝐿‘𝑋) = (𝐿‘∅))
28	27	oveqd 7385	. . . 4 ⊢ (𝑋 = ∅ → (𝐴(𝐿‘𝑋)𝐵) = (𝐴(𝐿‘∅)𝐵))
29	28	adantl 481	. . 3 ⊢ ((𝜑 ∧ 𝑋 = ∅) → (𝐴(𝐿‘𝑋)𝐵) = (𝐴(𝐿‘∅)𝐵))
30	13, 26, 29	3eqtr4d 2782	. 2 ⊢ ((𝜑 ∧ 𝑋 = ∅) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵))
31		neqne 2941	. . . 4 ⊢ (¬ 𝑋 = ∅ → 𝑋 ≠ ∅)
32	31	adantl 481	. . 3 ⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → 𝑋 ≠ ∅)
33		nfv 1916	. . . . . . . . 9 ⊢ Ⅎ𝑘(𝜑 ∧ 𝑋 ≠ ∅)
34		nfra1 3262	. . . . . . . . 9 ⊢ Ⅎ𝑘∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)
35	33, 34	nfan 1901	. . . . . . . 8 ⊢ Ⅎ𝑘((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘))
36	2	ffvelcdmda 7038	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈ ℝ)
37	7	ffvelcdmda 7038	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈ ℝ)
38		volico2 46993	. . . . . . . . . . . 12 ⊢ (((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = if((𝐴‘𝑘) ≤ (𝐵‘𝑘), ((𝐵‘𝑘) − (𝐴‘𝑘)), 0))
39	36, 37, 38	syl2anc 585	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = if((𝐴‘𝑘) ≤ (𝐵‘𝑘), ((𝐵‘𝑘) − (𝐴‘𝑘)), 0))
40	39	ad4ant14 753	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = if((𝐴‘𝑘) ≤ (𝐵‘𝑘), ((𝐵‘𝑘) − (𝐴‘𝑘)), 0))
41		rspa 3227	. . . . . . . . . . . 12 ⊢ ((∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘) ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ≤ (𝐵‘𝑘))
42	41	iftrued 4489	. . . . . . . . . . 11 ⊢ ((∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘) ∧ 𝑘 ∈ 𝑋) → if((𝐴‘𝑘) ≤ (𝐵‘𝑘), ((𝐵‘𝑘) − (𝐴‘𝑘)), 0) = ((𝐵‘𝑘) − (𝐴‘𝑘)))
43	42	adantll 715	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) ∧ 𝑘 ∈ 𝑋) → if((𝐴‘𝑘) ≤ (𝐵‘𝑘), ((𝐵‘𝑘) − (𝐴‘𝑘)), 0) = ((𝐵‘𝑘) − (𝐴‘𝑘)))
44	40, 43	eqtrd 2772	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = ((𝐵‘𝑘) − (𝐴‘𝑘)))
45	44	ex 412	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → (𝑘 ∈ 𝑋 → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = ((𝐵‘𝑘) − (𝐴‘𝑘))))
46	35, 45	ralrimi 3236	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → ∀𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = ((𝐵‘𝑘) − (𝐴‘𝑘)))
47	46	prodeq2d 15856	. . . . . 6 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − (𝐴‘𝑘)))
48	47	eqcomd 2743	. . . . 5 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − (𝐴‘𝑘)) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
49		fveq2 6842	. . . . . . . . . 10 ⊢ (𝑘 = 𝑗 → (𝐴‘𝑘) = (𝐴‘𝑗))
50		fveq2 6842	. . . . . . . . . 10 ⊢ (𝑘 = 𝑗 → (𝐵‘𝑘) = (𝐵‘𝑗))
51	49, 50	breq12d 5113	. . . . . . . . 9 ⊢ (𝑘 = 𝑗 → ((𝐴‘𝑘) ≤ (𝐵‘𝑘) ↔ (𝐴‘𝑗) ≤ (𝐵‘𝑗)))
52	51	cbvralvw 3216	. . . . . . . 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 583	. . . . . . . 8 ⊢ ((∀𝑗 ∈ 𝑋 (𝐴‘𝑗) ≤ (𝐵‘𝑗) ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ≤ (𝐵‘𝑘))
65	64	adantll 715	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑗 ∈ 𝑋 (𝐴‘𝑗) ≤ (𝐵‘𝑗)) ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ≤ (𝐵‘𝑘))
66		fveq2 6842	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑘 → (𝐵‘𝑗) = (𝐵‘𝑘))
67	66	oveq1d 7383	. . . . . . . . . 10 ⊢ (𝑗 = 𝑘 → ((𝐵‘𝑗) + (1 / 𝑚)) = ((𝐵‘𝑘) + (1 / 𝑚)))
68	67	cbvmptv 5204	. . . . . . . . 9 ⊢ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚))) = (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑚)))
69	68	mpteq2i 5196	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚)))) = (𝑚 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑚))))
70		oveq2 7376	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑛 → (1 / 𝑚) = (1 / 𝑛))
71	70	oveq2d 7384	. . . . . . . . . 10 ⊢ (𝑚 = 𝑛 → ((𝐵‘𝑘) + (1 / 𝑚)) = ((𝐵‘𝑘) + (1 / 𝑛)))
72	71	mpteq2dv 5194	. . . . . . . . 9 ⊢ (𝑚 = 𝑛 → (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑚))) = (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑛))))
73	72	cbvmptv 5204	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑚)))) = (𝑛 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑛))))
74	69, 73	eqtri 2760	. . . . . . 7 ⊢ (𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚)))) = (𝑛 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑛))))
75		fveq2 6842	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑛 → ((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚))))‘𝑖) = ((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚))))‘𝑛))
76	75	fveq1d 6844	. . . . . . . . . 10 ⊢ (𝑖 = 𝑛 → (((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚))))‘𝑖)‘𝑘) = (((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚))))‘𝑛)‘𝑘))
77	76	oveq2d 7384	. . . . . . . . 9 ⊢ (𝑖 = 𝑛 → ((𝐴‘𝑘)[,)(((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚))))‘𝑖)‘𝑘)) = ((𝐴‘𝑘)[,)(((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚))))‘𝑛)‘𝑘)))
78	77	ixpeq2dv 8863	. . . . . . . 8 ⊢ (𝑖 = 𝑛 → X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚))))‘𝑖)‘𝑘)) = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚))))‘𝑛)‘𝑘)))
79	78	cbvmptv 5204	. . . . . . 7 ⊢ (𝑖 ∈ ℕ ↦ X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚))))‘𝑖)‘𝑘))) = (𝑛 ∈ ℕ ↦ X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚))))‘𝑛)‘𝑘)))
80	57, 59, 61, 63, 65, 15, 74, 79	vonicclem2 47036	. . . . . 6 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑗 ∈ 𝑋 (𝐴‘𝑗) ≤ (𝐵‘𝑗)) → ((voln‘𝑋)‘𝐼) = ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − (𝐴‘𝑘)))
81	54, 80	syldan 592	. . . . 5 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → ((voln‘𝑋)‘𝐼) = ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − (𝐴‘𝑘)))
82	1, 56, 62, 58, 60	hoidmvn0val 46936	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → (𝐴(𝐿‘𝑋)𝐵) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
83	82	adantr 480	. . . . 5 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → (𝐴(𝐿‘𝑋)𝐵) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
84	48, 81, 83	3eqtr4d 2782	. . . 4 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵))
85		rexnal 3090	. . . . . . . . . 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 11292	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ ¬ (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → ((𝐵‘𝑘) < (𝐴‘𝑘) ↔ ¬ (𝐴‘𝑘) ≤ (𝐵‘𝑘)))
93	89, 92	mpbird 257	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ ¬ (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → (𝐵‘𝑘) < (𝐴‘𝑘))
94	93	ex 412	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (¬ (𝐴‘𝑘) ≤ (𝐵‘𝑘) → (𝐵‘𝑘) < (𝐴‘𝑘)))
95	94	reximdva 3151	. . . . . . . 8 ⊢ (𝜑 → (∃𝑘 ∈ 𝑋 ¬ (𝐴‘𝑘) ≤ (𝐵‘𝑘) → ∃𝑘 ∈ 𝑋 (𝐵‘𝑘) < (𝐴‘𝑘)))
96	95	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → (∃𝑘 ∈ 𝑋 ¬ (𝐴‘𝑘) ≤ (𝐵‘𝑘) → ∃𝑘 ∈ 𝑋 (𝐵‘𝑘) < (𝐴‘𝑘)))
97	88, 96	mpd 15	. . . . . 6 ⊢ ((𝜑 ∧ ¬ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → ∃𝑘 ∈ 𝑋 (𝐵‘𝑘) < (𝐴‘𝑘))
98	97	adantlr 716	. . . . 5 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ¬ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → ∃𝑘 ∈ 𝑋 (𝐵‘𝑘) < (𝐴‘𝑘))
99		nfcv 2899	. . . . . . . . 9 ⊢ Ⅎ𝑘(voln‘𝑋)
100		nfixp1 8868	. . . . . . . . . 10 ⊢ Ⅎ𝑘X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐵‘𝑘))
101	15, 100	nfcxfr 2897	. . . . . . . . 9 ⊢ Ⅎ𝑘𝐼
102	99, 101	nffv 6852	. . . . . . . 8 ⊢ Ⅎ𝑘((voln‘𝑋)‘𝐼)
103		nfcv 2899	. . . . . . . . 9 ⊢ Ⅎ𝑘𝐴
104		nfcv 2899	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘Fin
105		nfcv 2899	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘(ℝ ↑_m 𝑥)
106		nfv 1916	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘 𝑥 = ∅
107		nfcv 2899	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘0
108		nfcv 2899	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘𝑥
109	108	nfcprod1 15843	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))
110	106, 107, 109	nfif 4512	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))
111	105, 105, 110	nfmpo 7450	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘(𝑎 ∈ (ℝ ↑_m 𝑥), 𝑏 ∈ (ℝ ↑_m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))
112	104, 111	nfmpt 5198	. . . . . . . . . . 11 ⊢ Ⅎ𝑘(𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑_m 𝑥), 𝑏 ∈ (ℝ ↑_m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))))
113	1, 112	nfcxfr 2897	. . . . . . . . . 10 ⊢ Ⅎ𝑘𝐿
114		nfcv 2899	. . . . . . . . . 10 ⊢ Ⅎ𝑘𝑋
115	113, 114	nffv 6852	. . . . . . . . 9 ⊢ Ⅎ𝑘(𝐿‘𝑋)
116		nfcv 2899	. . . . . . . . 9 ⊢ Ⅎ𝑘𝐵
117	103, 115, 116	nfov 7398	. . . . . . . 8 ⊢ Ⅎ𝑘(𝐴(𝐿‘𝑋)𝐵)
118	102, 117	nfeq 2913	. . . . . . 7 ⊢ Ⅎ𝑘((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵)
119	55	vonmea 46926	. . . . . . . . . . . 12 ⊢ (𝜑 → (voln‘𝑋) ∈ Meas)
120	119	mea0 46806	. . . . . . . . . . 11 ⊢ (𝜑 → ((voln‘𝑋)‘∅) = 0)
121	120	3ad2ant1 1134	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → ((voln‘𝑋)‘∅) = 0)
122	15	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → 𝐼 = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐵‘𝑘)))
123		simp2 1138	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → 𝑘 ∈ 𝑋)
124		simp3 1139	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → (𝐵‘𝑘) < (𝐴‘𝑘))
125		ressxr 11188	. . . . . . . . . . . . . . . . . 18 ⊢ ℝ ⊆ ℝ^*
126	125, 36	sselid 3933	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈ ℝ^*)
127	125, 37	sselid 3933	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈ ℝ^*)
128		icc0 13321	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴‘𝑘) ∈ ℝ^* ∧ (𝐵‘𝑘) ∈ ℝ^*) → (((𝐴‘𝑘)[,](𝐵‘𝑘)) = ∅ ↔ (𝐵‘𝑘) < (𝐴‘𝑘)))
129	126, 127, 128	syl2anc 585	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (((𝐴‘𝑘)[,](𝐵‘𝑘)) = ∅ ↔ (𝐵‘𝑘) < (𝐴‘𝑘)))
130	129	3adant3 1133	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → (((𝐴‘𝑘)[,](𝐵‘𝑘)) = ∅ ↔ (𝐵‘𝑘) < (𝐴‘𝑘)))
131	124, 130	mpbird 257	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → ((𝐴‘𝑘)[,](𝐵‘𝑘)) = ∅)
132		rspe 3228	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ 𝑋 ∧ ((𝐴‘𝑘)[,](𝐵‘𝑘)) = ∅) → ∃𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐵‘𝑘)) = ∅)
133	123, 131, 132	syl2anc 585	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → ∃𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐵‘𝑘)) = ∅)
134		ixp0 8881	. . . . . . . . . . . . 13 ⊢ (∃𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐵‘𝑘)) = ∅ → X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐵‘𝑘)) = ∅)
135	133, 134	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐵‘𝑘)) = ∅)
136	122, 135	eqtrd 2772	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → 𝐼 = ∅)
137	136	fveq2d 6846	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → ((voln‘𝑋)‘𝐼) = ((voln‘𝑋)‘∅))
138		ne0i 4295	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ 𝑋 → 𝑋 ≠ ∅)
139	138	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝑋 ≠ ∅)
140	139, 82	syldan 592	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴(𝐿‘𝑋)𝐵) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
141	140	3adant3 1133	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → (𝐴(𝐿‘𝑋)𝐵) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
142		eleq1w 2820	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑘 → (𝑗 ∈ 𝑋 ↔ 𝑘 ∈ 𝑋))
143		fveq2 6842	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝑘 → (𝐴‘𝑗) = (𝐴‘𝑘))
144	66, 143	breq12d 5113	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑘 → ((𝐵‘𝑗) < (𝐴‘𝑗) ↔ (𝐵‘𝑘) < (𝐴‘𝑘)))
145	142, 144	3anbi23d 1442	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑘 → ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) ↔ (𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘))))
146	145	imbi1d 341	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑘 → (((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = 0) ↔ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = 0)))
147		nfv 1916	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘(𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗))
148	55	3ad2ant1 1134	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) → 𝑋 ∈ Fin)
149		volicore 46933	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℝ)
150	36, 37, 149	syl2anc 585	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℝ)
151	150	recnd 11172	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℂ)
152	151	3ad2antl1 1187	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℂ)
153		simp2 1138	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) → 𝑗 ∈ 𝑋)
154	49, 50	oveq12d 7386	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑗 → ((𝐴‘𝑘)[,)(𝐵‘𝑘)) = ((𝐴‘𝑗)[,)(𝐵‘𝑗)))
155	154	fveq2d 6846	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑗 → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = (vol‘((𝐴‘𝑗)[,)(𝐵‘𝑗))))
156	155	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) ∧ 𝑘 = 𝑗) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = (vol‘((𝐴‘𝑗)[,)(𝐵‘𝑗))))
157	2	ffvelcdmda 7038	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋) → (𝐴‘𝑗) ∈ ℝ)
158	7	ffvelcdmda 7038	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋) → (𝐵‘𝑗) ∈ ℝ)
159		volico2 46993	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴‘𝑗) ∈ ℝ ∧ (𝐵‘𝑗) ∈ ℝ) → (vol‘((𝐴‘𝑗)[,)(𝐵‘𝑗))) = if((𝐴‘𝑗) ≤ (𝐵‘𝑗), ((𝐵‘𝑗) − (𝐴‘𝑗)), 0))
160	157, 158, 159	syl2anc 585	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋) → (vol‘((𝐴‘𝑗)[,)(𝐵‘𝑗))) = if((𝐴‘𝑗) ≤ (𝐵‘𝑗), ((𝐵‘𝑗) − (𝐴‘𝑗)), 0))
161	160	3adant3 1133	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) → (vol‘((𝐴‘𝑗)[,)(𝐵‘𝑗))) = if((𝐴‘𝑗) ≤ (𝐵‘𝑗), ((𝐵‘𝑗) − (𝐴‘𝑗)), 0))
162		simp3 1139	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) → (𝐵‘𝑗) < (𝐴‘𝑗))
163	158, 157	ltnled 11292	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋) → ((𝐵‘𝑗) < (𝐴‘𝑗) ↔ ¬ (𝐴‘𝑗) ≤ (𝐵‘𝑗)))
164	163	3adant3 1133	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) → ((𝐵‘𝑗) < (𝐴‘𝑗) ↔ ¬ (𝐴‘𝑗) ≤ (𝐵‘𝑗)))
165	162, 164	mpbid 232	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) → ¬ (𝐴‘𝑗) ≤ (𝐵‘𝑗))
166	165	iffalsed 4492	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) → if((𝐴‘𝑗) ≤ (𝐵‘𝑗), ((𝐵‘𝑗) − (𝐴‘𝑗)), 0) = 0)
167	161, 166	eqtrd 2772	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) → (vol‘((𝐴‘𝑗)[,)(𝐵‘𝑗))) = 0)
168	167	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) ∧ 𝑘 = 𝑗) → (vol‘((𝐴‘𝑗)[,)(𝐵‘𝑗))) = 0)
169	156, 168	eqtrd 2772	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) ∧ 𝑘 = 𝑗) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = 0)
170	147, 148, 152, 153, 169	fprodeq0g 15929	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = 0)
171	146, 170	chvarvv 1991	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = 0)
172	141, 171	eqtrd 2772	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → (𝐴(𝐿‘𝑋)𝐵) = 0)
173	121, 137, 172	3eqtr4d 2782	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵))
174	173	3exp 1120	. . . . . . . 8 ⊢ (𝜑 → (𝑘 ∈ 𝑋 → ((𝐵‘𝑘) < (𝐴‘𝑘) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵))))
175	174	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → (𝑘 ∈ 𝑋 → ((𝐵‘𝑘) < (𝐴‘𝑘) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵))))
176	33, 118, 175	rexlimd 3245	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → (∃𝑘 ∈ 𝑋 (𝐵‘𝑘) < (𝐴‘𝑘) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵)))
177	176	imp 406	. . . . 5 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∃𝑘 ∈ 𝑋 (𝐵‘𝑘) < (𝐴‘𝑘)) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵))
178	98, 177	syldan 592	. . . 4 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ¬ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵))
179	84, 178	pm2.61dan 813	. . 3 ⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵))
180	32, 179	syldan 592	. 2 ⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵))
181	30, 180	pm2.61dan 813	1 ⊢ (𝜑 → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ≠ wne 2933 ∀wral 3052 ∃wrex 3062 ∅c0 4287 ifcif 4481 class class class wbr 5100 ↦ cmpt 5181 dom cdm 5632 ⟶wf 6496 ‘cfv 6500 (class class class)co 7368 ∈ cmpo 7370 ↑_m cmap 8775 Xcixp 8847 Fincfn 8895 ℂcc 11036 ℝcr 11037 0cc0 11038 1c1 11039 + caddc 11041 ℝ^*cxr 11177 < clt 11178 ≤ cle 11179 − cmin 11376 / cdiv 11806 ℕcn 12157 [,)cico 13275 [,]cicc 13276 ∏cprod 15838 volcvol 25432 volncvoln 46890

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5226 ax-sep 5243 ax-nul 5253 ax-pow 5312 ax-pr 5379 ax-un 7690 ax-inf2 9562 ax-cc 10357 ax-ac2 10385 ax-cnex 11094 ax-resscn 11095 ax-1cn 11096 ax-icn 11097 ax-addcl 11098 ax-addrcl 11099 ax-mulcl 11100 ax-mulrcl 11101 ax-mulcom 11102 ax-addass 11103 ax-mulass 11104 ax-distr 11105 ax-i2m1 11106 ax-1ne0 11107 ax-1rid 11108 ax-rnegex 11109 ax-rrecex 11110 ax-cnre 11111 ax-pre-lttri 11112 ax-pre-lttrn 11113 ax-pre-ltadd 11114 ax-pre-mulgt0 11115 ax-pre-sup 11116 ax-addf 11117 ax-mulf 11118

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3352 df-reu 3353 df-rab 3402 df-v 3444 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4288 df-if 4482 df-pw 4558 df-sn 4583 df-pr 4585 df-tp 4587 df-op 4589 df-uni 4866 df-int 4905 df-iun 4950 df-iin 4951 df-disj 5068 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5527 df-eprel 5532 df-po 5540 df-so 5541 df-fr 5585 df-se 5586 df-we 5587 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-res 5644 df-ima 5645 df-pred 6267 df-ord 6328 df-on 6329 df-lim 6330 df-suc 6331 df-iota 6456 df-fun 6502 df-fn 6503 df-f 6504 df-f1 6505 df-fo 6506 df-f1o 6507 df-fv 6508 df-isom 6509 df-riota 7325 df-ov 7371 df-oprab 7372 df-mpo 7373 df-of 7632 df-om 7819 df-1st 7943 df-2nd 7944 df-supp 8113 df-tpos 8178 df-frecs 8233 df-wrecs 8264 df-recs 8313 df-rdg 8351 df-1o 8407 df-2o 8408 df-oadd 8411 df-omul 8412 df-er 8645 df-map 8777 df-pm 8778 df-ixp 8848 df-en 8896 df-dom 8897 df-sdom 8898 df-fin 8899 df-fsupp 9277 df-fi 9326 df-sup 9357 df-inf 9358 df-oi 9427 df-dju 9825 df-card 9863 df-acn 9866 df-ac 10038 df-pnf 11180 df-mnf 11181 df-xr 11182 df-ltxr 11183 df-le 11184 df-sub 11378 df-neg 11379 df-div 11807 df-nn 12158 df-2 12220 df-3 12221 df-4 12222 df-5 12223 df-6 12224 df-7 12225 df-8 12226 df-9 12227 df-n0 12414 df-z 12501 df-dec 12620 df-uz 12764 df-q 12874 df-rp 12918 df-xneg 13038 df-xadd 13039 df-xmul 13040 df-ioo 13277 df-ico 13279 df-icc 13280 df-fz 13436 df-fzo 13583 df-fl 13724 df-seq 13937 df-exp 13997 df-hash 14266 df-cj 15034 df-re 15035 df-im 15036 df-sqrt 15170 df-abs 15171 df-clim 15423 df-rlim 15424 df-sum 15622 df-prod 15839 df-struct 17086 df-sets 17103 df-slot 17121 df-ndx 17133 df-base 17149 df-ress 17170 df-plusg 17202 df-mulr 17203 df-starv 17204 df-sca 17205 df-vsca 17206 df-ip 17207 df-tset 17208 df-ple 17209 df-ds 17211 df-unif 17212 df-hom 17213 df-cco 17214 df-rest 17354 df-topn 17355 df-0g 17373 df-gsum 17374 df-topgen 17375 df-pt 17376 df-prds 17379 df-pws 17381 df-xrs 17435 df-qtop 17440 df-imas 17441 df-xps 17443 df-mre 17517 df-mrc 17518 df-acs 17520 df-mgm 18577 df-sgrp 18656 df-mnd 18672 df-mhm 18720 df-submnd 18721 df-grp 18878 df-minusg 18879 df-sbg 18880 df-mulg 19010 df-subg 19065 df-ghm 19154 df-cntz 19258 df-cmn 19723 df-abl 19724 df-mgp 20088 df-rng 20100 df-ur 20129 df-ring 20182 df-cring 20183 df-oppr 20285 df-dvdsr 20305 df-unit 20306 df-invr 20336 df-dvr 20349 df-rhm 20420 df-subrng 20491 df-subrg 20515 df-drng 20676 df-field 20677 df-abv 20754 df-staf 20784 df-srng 20785 df-lmod 20825 df-lss 20895 df-lmhm 20986 df-lvec 21067 df-sra 21137 df-rgmod 21138 df-psmet 21313 df-xmet 21314 df-met 21315 df-bl 21316 df-mopn 21317 df-cnfld 21322 df-refld 21572 df-phl 21593 df-dsmm 21699 df-frlm 21714 df-top 22850 df-topon 22867 df-topsp 22889 df-bases 22902 df-cn 23183 df-cnp 23184 df-cmp 23343 df-tx 23518 df-hmeo 23711 df-xms 24276 df-ms 24277 df-tms 24278 df-nm 24538 df-ngp 24539 df-tng 24540 df-nrg 24541 df-nlm 24542 df-cncf 24839 df-clm 25031 df-cph 25136 df-tcph 25137 df-rrx 25353 df-ovol 25433 df-vol 25434 df-salg 46661 df-sumge0 46715 df-mea 46802 df-ome 46842 df-caragen 46844 df-ovoln 46889 df-voln 46891

This theorem is referenced by: vonn0icc 47040

W3C validator