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 47135

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 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 = ∅) → 𝐴:𝑋⟶ℝ)
4		feq2 6641	. . . . . . 7 ⊢ (𝑋 = ∅ → (𝐴:𝑋⟶ℝ ↔ 𝐴:∅⟶ℝ))
5	4	adantl 482	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 = ∅) → (𝐴:𝑋⟶ℝ ↔ 𝐴:∅⟶ℝ))
6	3, 5	mpbid 233	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 = ∅) → 𝐴:∅⟶ℝ)
7		vonicc.b	. . . . . . 7 ⊢ (𝜑 → 𝐵:𝑋⟶ℝ)
8	7	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 = ∅) → 𝐵:𝑋⟶ℝ)
9		feq2 6641	. . . . . . 7 ⊢ (𝑋 = ∅ → (𝐵:𝑋⟶ℝ ↔ 𝐵:∅⟶ℝ))
10	9	adantl 482	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 = ∅) → (𝐵:𝑋⟶ℝ ↔ 𝐵:∅⟶ℝ))
11	8, 10	mpbid 233	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 = ∅) → 𝐵:∅⟶ℝ)
12	1, 6, 11	hoidmv0val 47033	. . . 4 ⊢ ((𝜑 ∧ 𝑋 = ∅) → (𝐴(𝐿‘∅)𝐵) = 0)
13	12	eqcomd 2746	. . 3 ⊢ ((𝜑 ∧ 𝑋 = ∅) → 0 = (𝐴(𝐿‘∅)𝐵))
14		fveq2 6834	. . . . . 6 ⊢ (𝑋 = ∅ → (voln‘𝑋) = (voln‘∅))
15		vonicc.i	. . . . . . . 8 ⊢ 𝐼 = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐵‘𝑘))
16	15	a1i 11	. . . . . . 7 ⊢ (𝑋 = ∅ → 𝐼 = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐵‘𝑘)))
17		ixpeq1 8853	. . . . . . 7 ⊢ (𝑋 = ∅ → X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐵‘𝑘)) = X𝑘 ∈ ∅ ((𝐴‘𝑘)[,](𝐵‘𝑘)))
18	16, 17	eqtrd 2775	. . . . . 6 ⊢ (𝑋 = ∅ → 𝐼 = X𝑘 ∈ ∅ ((𝐴‘𝑘)[,](𝐵‘𝑘)))
19	14, 18	fveq12d 6841	. . . . 5 ⊢ (𝑋 = ∅ → ((voln‘𝑋)‘𝐼) = ((voln‘∅)‘X𝑘 ∈ ∅ ((𝐴‘𝑘)[,](𝐵‘𝑘))))
20	19	adantl 482	. . . 4 ⊢ ((𝜑 ∧ 𝑋 = ∅) → ((voln‘𝑋)‘𝐼) = ((voln‘∅)‘X𝑘 ∈ ∅ ((𝐴‘𝑘)[,](𝐵‘𝑘))))
21		0fi 8986	. . . . . . 7 ⊢ ∅ ∈ Fin
22	21	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 = ∅) → ∅ ∈ Fin)
23		eqid 2740	. . . . . 6 ⊢ dom (voln‘∅) = dom (voln‘∅)
24	22, 23, 6, 11	iccvonmbl 47129	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 = ∅) → X𝑘 ∈ ∅ ((𝐴‘𝑘)[,](𝐵‘𝑘)) ∈ dom (voln‘∅))
25	24	von0val 47121	. . . 4 ⊢ ((𝜑 ∧ 𝑋 = ∅) → ((voln‘∅)‘X𝑘 ∈ ∅ ((𝐴‘𝑘)[,](𝐵‘𝑘))) = 0)
26	20, 25	eqtrd 2775	. . 3 ⊢ ((𝜑 ∧ 𝑋 = ∅) → ((voln‘𝑋)‘𝐼) = 0)
27		fveq2 6834	. . . . 5 ⊢ (𝑋 = ∅ → (𝐿‘𝑋) = (𝐿‘∅))
28	27	oveqd 7380	. . . 4 ⊢ (𝑋 = ∅ → (𝐴(𝐿‘𝑋)𝐵) = (𝐴(𝐿‘∅)𝐵))
29	28	adantl 482	. . 3 ⊢ ((𝜑 ∧ 𝑋 = ∅) → (𝐴(𝐿‘𝑋)𝐵) = (𝐴(𝐿‘∅)𝐵))
30	13, 26, 29	3eqtr4d 2785	. 2 ⊢ ((𝜑 ∧ 𝑋 = ∅) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵))
31		neqne 2943	. . . 4 ⊢ (¬ 𝑋 = ∅ → 𝑋 ≠ ∅)
32	31	adantl 482	. . 3 ⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → 𝑋 ≠ ∅)
33		nfv 1921	. . . . . . . . 9 ⊢ Ⅎ𝑘(𝜑 ∧ 𝑋 ≠ ∅)
34		nfra1 3264	. . . . . . . . 9 ⊢ Ⅎ𝑘∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)
35	33, 34	nfan 1906	. . . . . . . 8 ⊢ Ⅎ𝑘((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘))
36	2	ffvelcdmda 7032	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈ ℝ)
37	7	ffvelcdmda 7032	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈ ℝ)
38		volico2 47091	. . . . . . . . . . . 12 ⊢ (((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = if((𝐴‘𝑘) ≤ (𝐵‘𝑘), ((𝐵‘𝑘) − (𝐴‘𝑘)), 0))
39	36, 37, 38	syl2anc 590	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = if((𝐴‘𝑘) ≤ (𝐵‘𝑘), ((𝐵‘𝑘) − (𝐴‘𝑘)), 0))
40	39	ad4ant14 758	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = if((𝐴‘𝑘) ≤ (𝐵‘𝑘), ((𝐵‘𝑘) − (𝐴‘𝑘)), 0))
41		rspa 3229	. . . . . . . . . . . 12 ⊢ ((∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘) ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ≤ (𝐵‘𝑘))
42	41	iftrued 4469	. . . . . . . . . . 11 ⊢ ((∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘) ∧ 𝑘 ∈ 𝑋) → if((𝐴‘𝑘) ≤ (𝐵‘𝑘), ((𝐵‘𝑘) − (𝐴‘𝑘)), 0) = ((𝐵‘𝑘) − (𝐴‘𝑘)))
43	42	adantll 720	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) ∧ 𝑘 ∈ 𝑋) → if((𝐴‘𝑘) ≤ (𝐵‘𝑘), ((𝐵‘𝑘) − (𝐴‘𝑘)), 0) = ((𝐵‘𝑘) − (𝐴‘𝑘)))
44	40, 43	eqtrd 2775	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = ((𝐵‘𝑘) − (𝐴‘𝑘)))
45	44	ex 413	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → (𝑘 ∈ 𝑋 → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = ((𝐵‘𝑘) − (𝐴‘𝑘))))
46	35, 45	ralrimi 3238	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → ∀𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = ((𝐵‘𝑘) − (𝐴‘𝑘)))
47	46	prodeq2d 15884	. . . . . 6 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − (𝐴‘𝑘)))
48	47	eqcomd 2746	. . . . 5 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − (𝐴‘𝑘)) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
49		fveq2 6834	. . . . . . . . 9 ⊢ (𝑘 = 𝑗 → (𝐴‘𝑘) = (𝐴‘𝑗))
50		fveq2 6834	. . . . . . . . 9 ⊢ (𝑘 = 𝑗 → (𝐵‘𝑘) = (𝐵‘𝑗))
51	49, 50	breq12d 5092	. . . . . . . 8 ⊢ (𝑘 = 𝑗 → ((𝐴‘𝑘) ≤ (𝐵‘𝑘) ↔ (𝐴‘𝑗) ≤ (𝐵‘𝑗)))
52	51	cbvralvw 3218	. . . . . . 7 ⊢ (∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘) ↔ ∀𝑗 ∈ 𝑋 (𝐴‘𝑗) ≤ (𝐵‘𝑗))
53	52	bilani 505	. . . . . 6 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → ∀𝑗 ∈ 𝑋 (𝐴‘𝑗) ≤ (𝐵‘𝑗))
54		vonicc.x	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ∈ Fin)
55	54	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → 𝑋 ∈ Fin)
56	55	adantr 481	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑗 ∈ 𝑋 (𝐴‘𝑗) ≤ (𝐵‘𝑗)) → 𝑋 ∈ Fin)
57	2	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → 𝐴:𝑋⟶ℝ)
58	57	adantr 481	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑗 ∈ 𝑋 (𝐴‘𝑗) ≤ (𝐵‘𝑗)) → 𝐴:𝑋⟶ℝ)
59	7	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → 𝐵:𝑋⟶ℝ)
60	59	adantr 481	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑗 ∈ 𝑋 (𝐴‘𝑗) ≤ (𝐵‘𝑗)) → 𝐵:𝑋⟶ℝ)
61		simpr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → 𝑋 ≠ ∅)
62	61	adantr 481	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑗 ∈ 𝑋 (𝐴‘𝑗) ≤ (𝐵‘𝑗)) → 𝑋 ≠ ∅)
63	52, 41	sylanbr 588	. . . . . . . 8 ⊢ ((∀𝑗 ∈ 𝑋 (𝐴‘𝑗) ≤ (𝐵‘𝑗) ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ≤ (𝐵‘𝑘))
64	63	adantll 720	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑗 ∈ 𝑋 (𝐴‘𝑗) ≤ (𝐵‘𝑗)) ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ≤ (𝐵‘𝑘))
65		fveq2 6834	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑘 → (𝐵‘𝑗) = (𝐵‘𝑘))
66	65	oveq1d 7378	. . . . . . . . . 10 ⊢ (𝑗 = 𝑘 → ((𝐵‘𝑗) + (1 / 𝑚)) = ((𝐵‘𝑘) + (1 / 𝑚)))
67	66	cbvmptv 5183	. . . . . . . . 9 ⊢ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚))) = (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑚)))
68	67	mpteq2i 5175	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚)))) = (𝑚 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑚))))
69		oveq2 7371	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑛 → (1 / 𝑚) = (1 / 𝑛))
70	69	oveq2d 7379	. . . . . . . . . 10 ⊢ (𝑚 = 𝑛 → ((𝐵‘𝑘) + (1 / 𝑚)) = ((𝐵‘𝑘) + (1 / 𝑛)))
71	70	mpteq2dv 5173	. . . . . . . . 9 ⊢ (𝑚 = 𝑛 → (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑚))) = (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑛))))
72	71	cbvmptv 5183	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑚)))) = (𝑛 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑛))))
73	68, 72	eqtri 2763	. . . . . . 7 ⊢ (𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚)))) = (𝑛 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑛))))
74		fveq2 6834	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑛 → ((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚))))‘𝑖) = ((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚))))‘𝑛))
75	74	fveq1d 6836	. . . . . . . . . 10 ⊢ (𝑖 = 𝑛 → (((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚))))‘𝑖)‘𝑘) = (((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚))))‘𝑛)‘𝑘))
76	75	oveq2d 7379	. . . . . . . . 9 ⊢ (𝑖 = 𝑛 → ((𝐴‘𝑘)[,)(((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚))))‘𝑖)‘𝑘)) = ((𝐴‘𝑘)[,)(((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚))))‘𝑛)‘𝑘)))
77	76	ixpeq2dv 8858	. . . . . . . 8 ⊢ (𝑖 = 𝑛 → X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚))))‘𝑖)‘𝑘)) = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚))))‘𝑛)‘𝑘)))
78	77	cbvmptv 5183	. . . . . . 7 ⊢ (𝑖 ∈ ℕ ↦ X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚))))‘𝑖)‘𝑘))) = (𝑛 ∈ ℕ ↦ X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚))))‘𝑛)‘𝑘)))
79	56, 58, 60, 62, 64, 15, 73, 78	vonicclem2 47134	. . . . . 6 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑗 ∈ 𝑋 (𝐴‘𝑗) ≤ (𝐵‘𝑗)) → ((voln‘𝑋)‘𝐼) = ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − (𝐴‘𝑘)))
80	53, 79	syldan 597	. . . . 5 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → ((voln‘𝑋)‘𝐼) = ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − (𝐴‘𝑘)))
81	1, 55, 61, 57, 59	hoidmvn0val 47034	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → (𝐴(𝐿‘𝑋)𝐵) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
82	81	adantr 481	. . . . 5 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → (𝐴(𝐿‘𝑋)𝐵) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
83	48, 80, 82	3eqtr4d 2785	. . . 4 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵))
84		rexnal 3092	. . . . . . . 8 ⊢ (∃𝑘 ∈ 𝑋 ¬ (𝐴‘𝑘) ≤ (𝐵‘𝑘) ↔ ¬ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘))
85	84	bilanri 507	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → ∃𝑘 ∈ 𝑋 ¬ (𝐴‘𝑘) ≤ (𝐵‘𝑘))
86		simpr 485	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ ¬ (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → ¬ (𝐴‘𝑘) ≤ (𝐵‘𝑘))
87	37	adantr 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ ¬ (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → (𝐵‘𝑘) ∈ ℝ)
88	36	adantr 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ ¬ (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → (𝐴‘𝑘) ∈ ℝ)
89	87, 88	ltnled 11291	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ ¬ (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → ((𝐵‘𝑘) < (𝐴‘𝑘) ↔ ¬ (𝐴‘𝑘) ≤ (𝐵‘𝑘)))
90	86, 89	mpbird 258	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ ¬ (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → (𝐵‘𝑘) < (𝐴‘𝑘))
91	90	ex 413	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (¬ (𝐴‘𝑘) ≤ (𝐵‘𝑘) → (𝐵‘𝑘) < (𝐴‘𝑘)))
92	91	reximdva 3153	. . . . . . . 8 ⊢ (𝜑 → (∃𝑘 ∈ 𝑋 ¬ (𝐴‘𝑘) ≤ (𝐵‘𝑘) → ∃𝑘 ∈ 𝑋 (𝐵‘𝑘) < (𝐴‘𝑘)))
93	92	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → (∃𝑘 ∈ 𝑋 ¬ (𝐴‘𝑘) ≤ (𝐵‘𝑘) → ∃𝑘 ∈ 𝑋 (𝐵‘𝑘) < (𝐴‘𝑘)))
94	85, 93	mpd 15	. . . . . 6 ⊢ ((𝜑 ∧ ¬ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → ∃𝑘 ∈ 𝑋 (𝐵‘𝑘) < (𝐴‘𝑘))
95	94	adantlr 721	. . . . 5 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ¬ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → ∃𝑘 ∈ 𝑋 (𝐵‘𝑘) < (𝐴‘𝑘))
96		nfcv 2902	. . . . . . . . 9 ⊢ Ⅎ𝑘(voln‘𝑋)
97		nfixp1 8863	. . . . . . . . . 10 ⊢ Ⅎ𝑘X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐵‘𝑘))
98	15, 97	nfcxfr 2900	. . . . . . . . 9 ⊢ Ⅎ𝑘𝐼
99	96, 98	nffv 6844	. . . . . . . 8 ⊢ Ⅎ𝑘((voln‘𝑋)‘𝐼)
100		nfcv 2902	. . . . . . . . 9 ⊢ Ⅎ𝑘𝐴
101		nfcv 2902	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘Fin
102		nfcv 2902	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘(ℝ ↑_m 𝑥)
103		nfv 1921	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘 𝑥 = ∅
104		nfcv 2902	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘0
105		nfcv 2902	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘𝑥
106	105	nfcprod1 15871	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))
107	103, 104, 106	nfif 4492	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))
108	102, 102, 107	nfmpo 7445	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘(𝑎 ∈ (ℝ ↑_m 𝑥), 𝑏 ∈ (ℝ ↑_m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))
109	101, 108	nfmpt 5177	. . . . . . . . . . 11 ⊢ Ⅎ𝑘(𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑_m 𝑥), 𝑏 ∈ (ℝ ↑_m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))))
110	1, 109	nfcxfr 2900	. . . . . . . . . 10 ⊢ Ⅎ𝑘𝐿
111		nfcv 2902	. . . . . . . . . 10 ⊢ Ⅎ𝑘𝑋
112	110, 111	nffv 6844	. . . . . . . . 9 ⊢ Ⅎ𝑘(𝐿‘𝑋)
113		nfcv 2902	. . . . . . . . 9 ⊢ Ⅎ𝑘𝐵
114	100, 112, 113	nfov 7393	. . . . . . . 8 ⊢ Ⅎ𝑘(𝐴(𝐿‘𝑋)𝐵)
115	99, 114	nfeq 2915	. . . . . . 7 ⊢ Ⅎ𝑘((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵)
116	54	vonmea 47024	. . . . . . . . . . . 12 ⊢ (𝜑 → (voln‘𝑋) ∈ Meas)
117	116	mea0 46904	. . . . . . . . . . 11 ⊢ (𝜑 → ((voln‘𝑋)‘∅) = 0)
118	117	3ad2ant1 1139	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → ((voln‘𝑋)‘∅) = 0)
119	15	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → 𝐼 = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐵‘𝑘)))
120		simp2 1143	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → 𝑘 ∈ 𝑋)
121		simp3 1144	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → (𝐵‘𝑘) < (𝐴‘𝑘))
122		ressxr 11187	. . . . . . . . . . . . . . . . . 18 ⊢ ℝ ⊆ ℝ^*
123	122, 36	sselid 3920	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈ ℝ^*)
124	122, 37	sselid 3920	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈ ℝ^*)
125		icc0 13344	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴‘𝑘) ∈ ℝ^* ∧ (𝐵‘𝑘) ∈ ℝ^*) → (((𝐴‘𝑘)[,](𝐵‘𝑘)) = ∅ ↔ (𝐵‘𝑘) < (𝐴‘𝑘)))
126	123, 124, 125	syl2anc 590	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (((𝐴‘𝑘)[,](𝐵‘𝑘)) = ∅ ↔ (𝐵‘𝑘) < (𝐴‘𝑘)))
127	126	3adant3 1138	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → (((𝐴‘𝑘)[,](𝐵‘𝑘)) = ∅ ↔ (𝐵‘𝑘) < (𝐴‘𝑘)))
128	121, 127	mpbird 258	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → ((𝐴‘𝑘)[,](𝐵‘𝑘)) = ∅)
129		rspe 3230	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ 𝑋 ∧ ((𝐴‘𝑘)[,](𝐵‘𝑘)) = ∅) → ∃𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐵‘𝑘)) = ∅)
130	120, 128, 129	syl2anc 590	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → ∃𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐵‘𝑘)) = ∅)
131		ixp0 8876	. . . . . . . . . . . . 13 ⊢ (∃𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐵‘𝑘)) = ∅ → X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐵‘𝑘)) = ∅)
132	130, 131	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐵‘𝑘)) = ∅)
133	119, 132	eqtrd 2775	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → 𝐼 = ∅)
134	133	fveq2d 6838	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → ((voln‘𝑋)‘𝐼) = ((voln‘𝑋)‘∅))
135		ne0i 4276	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ 𝑋 → 𝑋 ≠ ∅)
136	135	adantl 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝑋 ≠ ∅)
137	136, 81	syldan 597	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴(𝐿‘𝑋)𝐵) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
138	137	3adant3 1138	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → (𝐴(𝐿‘𝑋)𝐵) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
139		eleq1w 2823	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑘 → (𝑗 ∈ 𝑋 ↔ 𝑘 ∈ 𝑋))
140		fveq2 6834	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝑘 → (𝐴‘𝑗) = (𝐴‘𝑘))
141	65, 140	breq12d 5092	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑘 → ((𝐵‘𝑗) < (𝐴‘𝑗) ↔ (𝐵‘𝑘) < (𝐴‘𝑘)))
142	139, 141	3anbi23d 1447	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑘 → ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) ↔ (𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘))))
143	142	imbi1d 342	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑘 → (((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = 0) ↔ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = 0)))
144		nfv 1921	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘(𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗))
145	54	3ad2ant1 1139	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) → 𝑋 ∈ Fin)
146		volicore 47031	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℝ)
147	36, 37, 146	syl2anc 590	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℝ)
148	147	recnd 11171	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℂ)
149	148	3ad2antl1 1192	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℂ)
150		simp2 1143	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) → 𝑗 ∈ 𝑋)
151	49, 50	oveq12d 7381	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑗 → ((𝐴‘𝑘)[,)(𝐵‘𝑘)) = ((𝐴‘𝑗)[,)(𝐵‘𝑗)))
152	151	fveq2d 6838	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑗 → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = (vol‘((𝐴‘𝑗)[,)(𝐵‘𝑗))))
153	152	adantl 482	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) ∧ 𝑘 = 𝑗) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = (vol‘((𝐴‘𝑗)[,)(𝐵‘𝑗))))
154	2	ffvelcdmda 7032	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋) → (𝐴‘𝑗) ∈ ℝ)
155	7	ffvelcdmda 7032	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋) → (𝐵‘𝑗) ∈ ℝ)
156		volico2 47091	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴‘𝑗) ∈ ℝ ∧ (𝐵‘𝑗) ∈ ℝ) → (vol‘((𝐴‘𝑗)[,)(𝐵‘𝑗))) = if((𝐴‘𝑗) ≤ (𝐵‘𝑗), ((𝐵‘𝑗) − (𝐴‘𝑗)), 0))
157	154, 155, 156	syl2anc 590	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋) → (vol‘((𝐴‘𝑗)[,)(𝐵‘𝑗))) = if((𝐴‘𝑗) ≤ (𝐵‘𝑗), ((𝐵‘𝑗) − (𝐴‘𝑗)), 0))
158	157	3adant3 1138	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) → (vol‘((𝐴‘𝑗)[,)(𝐵‘𝑗))) = if((𝐴‘𝑗) ≤ (𝐵‘𝑗), ((𝐵‘𝑗) − (𝐴‘𝑗)), 0))
159		simp3 1144	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) → (𝐵‘𝑗) < (𝐴‘𝑗))
160	155, 154	ltnled 11291	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋) → ((𝐵‘𝑗) < (𝐴‘𝑗) ↔ ¬ (𝐴‘𝑗) ≤ (𝐵‘𝑗)))
161	160	3adant3 1138	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) → ((𝐵‘𝑗) < (𝐴‘𝑗) ↔ ¬ (𝐴‘𝑗) ≤ (𝐵‘𝑗)))
162	159, 161	mpbid 233	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) → ¬ (𝐴‘𝑗) ≤ (𝐵‘𝑗))
163	162	iffalsed 4472	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) → if((𝐴‘𝑗) ≤ (𝐵‘𝑗), ((𝐵‘𝑗) − (𝐴‘𝑗)), 0) = 0)
164	158, 163	eqtrd 2775	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) → (vol‘((𝐴‘𝑗)[,)(𝐵‘𝑗))) = 0)
165	164	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) ∧ 𝑘 = 𝑗) → (vol‘((𝐴‘𝑗)[,)(𝐵‘𝑗))) = 0)
166	153, 165	eqtrd 2775	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) ∧ 𝑘 = 𝑗) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = 0)
167	144, 145, 149, 150, 166	fprodeq0g 15957	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = 0)
168	143, 167	chvarvv 1996	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = 0)
169	138, 168	eqtrd 2775	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → (𝐴(𝐿‘𝑋)𝐵) = 0)
170	118, 134, 169	3eqtr4d 2785	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵))
171	170	3exp 1125	. . . . . . . 8 ⊢ (𝜑 → (𝑘 ∈ 𝑋 → ((𝐵‘𝑘) < (𝐴‘𝑘) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵))))
172	171	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → (𝑘 ∈ 𝑋 → ((𝐵‘𝑘) < (𝐴‘𝑘) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵))))
173	33, 115, 172	rexlimd 3247	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → (∃𝑘 ∈ 𝑋 (𝐵‘𝑘) < (𝐴‘𝑘) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵)))
174	173	imp 407	. . . . 5 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∃𝑘 ∈ 𝑋 (𝐵‘𝑘) < (𝐴‘𝑘)) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵))
175	95, 174	syldan 597	. . . 4 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ¬ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵))
176	83, 175	pm2.61dan 818	. . 3 ⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵))
177	32, 176	syldan 597	. 2 ⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵))
178	30, 177	pm2.61dan 818	1 ⊢ (𝜑 → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 ∧ wa 396 ∧ w3a 1092 = wceq 1547 ∈ wcel 2119 ≠ wne 2935 ∀wral 3054 ∃wrex 3064 ∅c0 4268 ifcif 4461 class class class wbr 5079 ↦ cmpt 5160 dom cdm 5625 ⟶wf 6488 ‘cfv 6492 (class class class)co 7363 ∈ cmpo 7365 ↑_m cmap 8770 Xcixp 8842 Fincfn 8890 ℂcc 11034 ℝcr 11035 0cc0 11036 1c1 11037 + caddc 11039 ℝ^*cxr 11176 < clt 11177 ≤ cle 11178 − cmin 11375 / cdiv 11805 ℕcn 12172 [,)cico 13298 [,]cicc 13299 ∏cprod 15866 volcvol 25455 volncvoln 46988

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-11 2168 ax-12 2189 ax-ext 2712 ax-rep 5206 ax-sep 5225 ax-nul 5235 ax-pow 5301 ax-pr 5369 ax-un 7685 ax-inf2 9560 ax-cc 10355 ax-ac2 10383 ax-cnex 11092 ax-resscn 11093 ax-1cn 11094 ax-icn 11095 ax-addcl 11096 ax-addrcl 11097 ax-mulcl 11098 ax-mulrcl 11099 ax-mulcom 11100 ax-addass 11101 ax-mulass 11102 ax-distr 11103 ax-i2m1 11104 ax-1ne0 11105 ax-1rid 11106 ax-rnegex 11107 ax-rrecex 11108 ax-cnre 11109 ax-pre-lttri 11110 ax-pre-lttrn 11111 ax-pre-ltadd 11112 ax-pre-mulgt0 11113 ax-pre-sup 11114 ax-addf 11115 ax-mulf 11116

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3or 1093 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2719 df-cleq 2732 df-clel 2815 df-nfc 2889 df-ne 2936 df-nel 3040 df-ral 3055 df-rex 3065 df-rmo 3345 df-reu 3346 df-rab 3393 df-v 3434 df-sbc 3731 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4269 df-if 4462 df-pw 4538 df-sn 4563 df-pr 4565 df-tp 4567 df-op 4569 df-uni 4846 df-int 4885 df-iun 4930 df-iin 4931 df-disj 5047 df-br 5080 df-opab 5142 df-mpt 5161 df-tr 5187 df-id 5520 df-eprel 5525 df-po 5533 df-so 5534 df-fr 5578 df-se 5579 df-we 5580 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-res 5637 df-ima 5638 df-pred 6259 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-isom 6501 df-riota 7320 df-ov 7366 df-oprab 7367 df-mpo 7368 df-of 7627 df-om 7814 df-1st 7938 df-2nd 7939 df-supp 8108 df-tpos 8173 df-frecs 8228 df-wrecs 8259 df-recs 8308 df-rdg 8346 df-1o 8402 df-2o 8403 df-oadd 8406 df-omul 8407 df-er 8640 df-map 8772 df-pm 8773 df-ixp 8843 df-en 8891 df-dom 8892 df-sdom 8893 df-fin 8894 df-fsupp 9272 df-fi 9321 df-sup 9352 df-inf 9353 df-oi 9422 df-dju 9823 df-card 9861 df-acn 9864 df-ac 10036 df-pnf 11179 df-mnf 11180 df-xr 11181 df-ltxr 11182 df-le 11183 df-sub 11377 df-neg 11378 df-div 11806 df-nn 12173 df-2 12242 df-3 12243 df-4 12244 df-5 12245 df-6 12246 df-7 12247 df-8 12248 df-9 12249 df-n0 12436 df-z 12523 df-dec 12643 df-uz 12787 df-q 12897 df-rp 12941 df-xneg 13061 df-xadd 13062 df-xmul 13063 df-ioo 13300 df-ico 13302 df-icc 13303 df-fz 13460 df-fzo 13607 df-fl 13749 df-seq 13962 df-exp 14022 df-hash 14291 df-cj 15059 df-re 15060 df-im 15061 df-sqrt 15195 df-abs 15196 df-clim 15448 df-rlim 15449 df-sum 15647 df-prod 15867 df-struct 17115 df-sets 17132 df-slot 17150 df-ndx 17162 df-base 17178 df-ress 17199 df-plusg 17231 df-mulr 17232 df-starv 17233 df-sca 17234 df-vsca 17235 df-ip 17236 df-tset 17237 df-ple 17238 df-ds 17240 df-unif 17241 df-hom 17242 df-cco 17243 df-rest 17383 df-topn 17384 df-0g 17402 df-gsum 17403 df-topgen 17404 df-pt 17405 df-prds 17408 df-pws 17410 df-xrs 17464 df-qtop 17469 df-imas 17470 df-xps 17472 df-mre 17546 df-mrc 17547 df-acs 17549 df-mgm 18606 df-sgrp 18685 df-mnd 18701 df-mhm 18749 df-submnd 18750 df-grp 18910 df-minusg 18911 df-sbg 18912 df-mulg 19042 df-subg 19097 df-ghm 19186 df-cntz 19290 df-cmn 19755 df-abl 19756 df-mgp 20120 df-rng 20132 df-ur 20161 df-ring 20214 df-cring 20215 df-oppr 20315 df-dvdsr 20335 df-unit 20336 df-invr 20366 df-dvr 20379 df-rhm 20450 df-subrng 20525 df-subrg 20549 df-drng 20710 df-field 20711 df-abv 20788 df-staf 20818 df-srng 20819 df-lmod 20859 df-lss 20929 df-lmhm 21019 df-lvec 21100 df-sra 21170 df-rgmod 21171 df-psmet 21346 df-xmet 21347 df-met 21348 df-bl 21349 df-mopn 21350 df-cnfld 21355 df-refld 21587 df-phl 21608 df-dsmm 21714 df-frlm 21729 df-top 22884 df-topon 22901 df-topsp 22923 df-bases 22936 df-cn 23217 df-cnp 23218 df-cmp 23377 df-tx 23552 df-hmeo 23745 df-xms 24310 df-ms 24311 df-tms 24312 df-nm 24572 df-ngp 24573 df-tng 24574 df-nrg 24575 df-nlm 24576 df-cncf 24870 df-clm 25055 df-cph 25160 df-tcph 25161 df-rrx 25377 df-ovol 25456 df-vol 25457 df-salg 46759 df-sumge0 46813 df-mea 46900 df-ome 46940 df-caragen 46942 df-ovoln 46987 df-voln 46989

This theorem is referenced by: vonn0icc 47138

W3C validator