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 47521

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 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 = ∅) → 𝐴:𝑋⟶ℝ)
4		feq2 6685	. . . . . . 7 ⊢ (𝑋 = ∅ → (𝐴:𝑋⟶ℝ ↔ 𝐴:∅⟶ℝ))
5	4	adantl 487	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 = ∅) → (𝐴:𝑋⟶ℝ ↔ 𝐴:∅⟶ℝ))
6	3, 5	mpbid 235	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 = ∅) → 𝐴:∅⟶ℝ)
7		vonicc.b	. . . . . . 7 ⊢ (𝜑 → 𝐵:𝑋⟶ℝ)
8	7	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 = ∅) → 𝐵:𝑋⟶ℝ)
9		feq2 6685	. . . . . . 7 ⊢ (𝑋 = ∅ → (𝐵:𝑋⟶ℝ ↔ 𝐵:∅⟶ℝ))
10	9	adantl 487	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 = ∅) → (𝐵:𝑋⟶ℝ ↔ 𝐵:∅⟶ℝ))
11	8, 10	mpbid 235	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 = ∅) → 𝐵:∅⟶ℝ)
12	1, 6, 11	hoidmv0val 47419	. . . 4 ⊢ ((𝜑 ∧ 𝑋 = ∅) → (𝐴(𝐿‘∅)𝐵) = 0)
13	12	eqcomd 2768	. . 3 ⊢ ((𝜑 ∧ 𝑋 = ∅) → 0 = (𝐴(𝐿‘∅)𝐵))
14		fveq2 6882	. . . . . 6 ⊢ (𝑋 = ∅ → (voln‘𝑋) = (voln‘∅))
15		vonicc.i	. . . . . . . 8 ⊢ 𝐼 = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐵‘𝑘))
16	15	a1i 11	. . . . . . 7 ⊢ (𝑋 = ∅ → 𝐼 = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐵‘𝑘)))
17		ixpeq1 8919	. . . . . . 7 ⊢ (𝑋 = ∅ → X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐵‘𝑘)) = X𝑘 ∈ ∅ ((𝐴‘𝑘)[,](𝐵‘𝑘)))
18	16, 17	eqtrd 2797	. . . . . 6 ⊢ (𝑋 = ∅ → 𝐼 = X𝑘 ∈ ∅ ((𝐴‘𝑘)[,](𝐵‘𝑘)))
19	14, 18	fveq12d 6889	. . . . 5 ⊢ (𝑋 = ∅ → ((voln‘𝑋)‘𝐼) = ((voln‘∅)‘X𝑘 ∈ ∅ ((𝐴‘𝑘)[,](𝐵‘𝑘))))
20	19	adantl 487	. . . 4 ⊢ ((𝜑 ∧ 𝑋 = ∅) → ((voln‘𝑋)‘𝐼) = ((voln‘∅)‘X𝑘 ∈ ∅ ((𝐴‘𝑘)[,](𝐵‘𝑘))))
21		0fi 9053	. . . . . . 7 ⊢ ∅ ∈ Fin
22	21	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 = ∅) → ∅ ∈ Fin)
23		eqid 2762	. . . . . 6 ⊢ dom (voln‘∅) = dom (voln‘∅)
24	22, 23, 6, 11	iccvonmbl 47515	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 = ∅) → X𝑘 ∈ ∅ ((𝐴‘𝑘)[,](𝐵‘𝑘)) ∈ dom (voln‘∅))
25	24	von0val 47507	. . . 4 ⊢ ((𝜑 ∧ 𝑋 = ∅) → ((voln‘∅)‘X𝑘 ∈ ∅ ((𝐴‘𝑘)[,](𝐵‘𝑘))) = 0)
26	20, 25	eqtrd 2797	. . 3 ⊢ ((𝜑 ∧ 𝑋 = ∅) → ((voln‘𝑋)‘𝐼) = 0)
27		fveq2 6882	. . . . 5 ⊢ (𝑋 = ∅ → (𝐿‘𝑋) = (𝐿‘∅))
28	27	oveqd 7434	. . . 4 ⊢ (𝑋 = ∅ → (𝐴(𝐿‘𝑋)𝐵) = (𝐴(𝐿‘∅)𝐵))
29	28	adantl 487	. . 3 ⊢ ((𝜑 ∧ 𝑋 = ∅) → (𝐴(𝐿‘𝑋)𝐵) = (𝐴(𝐿‘∅)𝐵))
30	13, 26, 29	3eqtr4d 2807	. 2 ⊢ ((𝜑 ∧ 𝑋 = ∅) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵))
31		neqne 2965	. . . 4 ⊢ (¬ 𝑋 = ∅ → 𝑋 ≠ ∅)
32	31	adantl 487	. . 3 ⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → 𝑋 ≠ ∅)
33		nfv 1947	. . . . . . . . 9 ⊢ Ⅎ𝑘(𝜑 ∧ 𝑋 ≠ ∅)
34		nfra1 3288	. . . . . . . . 9 ⊢ Ⅎ𝑘∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)
35	33, 34	nfan 1932	. . . . . . . 8 ⊢ Ⅎ𝑘((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘))
36	2	ffvelcdmda 7081	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈ ℝ)
37	7	ffvelcdmda 7081	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈ ℝ)
38		volico2 47477	. . . . . . . . . . . 12 ⊢ (((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = if((𝐴‘𝑘) ≤ (𝐵‘𝑘), ((𝐵‘𝑘) − (𝐴‘𝑘)), 0))
39	36, 37, 38	syl2anc 596	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = if((𝐴‘𝑘) ≤ (𝐵‘𝑘), ((𝐵‘𝑘) − (𝐴‘𝑘)), 0))
40	39	ad4ant14 765	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = if((𝐴‘𝑘) ≤ (𝐵‘𝑘), ((𝐵‘𝑘) − (𝐴‘𝑘)), 0))
41		rspa 3253	. . . . . . . . . . . 12 ⊢ ((∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘) ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ≤ (𝐵‘𝑘))
42	41	iftrued 4493	. . . . . . . . . . 11 ⊢ ((∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘) ∧ 𝑘 ∈ 𝑋) → if((𝐴‘𝑘) ≤ (𝐵‘𝑘), ((𝐵‘𝑘) − (𝐴‘𝑘)), 0) = ((𝐵‘𝑘) − (𝐴‘𝑘)))
43	42	adantll 727	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) ∧ 𝑘 ∈ 𝑋) → if((𝐴‘𝑘) ≤ (𝐵‘𝑘), ((𝐵‘𝑘) − (𝐴‘𝑘)), 0) = ((𝐵‘𝑘) − (𝐴‘𝑘)))
44	40, 43	eqtrd 2797	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = ((𝐵‘𝑘) − (𝐴‘𝑘)))
45	44	ex 418	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → (𝑘 ∈ 𝑋 → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = ((𝐵‘𝑘) − (𝐴‘𝑘))))
46	35, 45	ralrimi 3262	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → ∀𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = ((𝐵‘𝑘) − (𝐴‘𝑘)))
47	46	prodeq2d 16014	. . . . . 6 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − (𝐴‘𝑘)))
48	47	eqcomd 2768	. . . . 5 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − (𝐴‘𝑘)) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
49		fveq2 6882	. . . . . . . . 9 ⊢ (𝑘 = 𝑗 → (𝐴‘𝑘) = (𝐴‘𝑗))
50		fveq2 6882	. . . . . . . . 9 ⊢ (𝑘 = 𝑗 → (𝐵‘𝑘) = (𝐵‘𝑗))
51	49, 50	breq12d 5120	. . . . . . . 8 ⊢ (𝑘 = 𝑗 → ((𝐴‘𝑘) ≤ (𝐵‘𝑘) ↔ (𝐴‘𝑗) ≤ (𝐵‘𝑗)))
52	51	cbvralvw 3242	. . . . . . 7 ⊢ (∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘) ↔ ∀𝑗 ∈ 𝑋 (𝐴‘𝑗) ≤ (𝐵‘𝑗))
53	52	bilani 510	. . . . . 6 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → ∀𝑗 ∈ 𝑋 (𝐴‘𝑗) ≤ (𝐵‘𝑗))
54		vonicc.x	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ∈ Fin)
55	54	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → 𝑋 ∈ Fin)
56	55	adantr 486	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑗 ∈ 𝑋 (𝐴‘𝑗) ≤ (𝐵‘𝑗)) → 𝑋 ∈ Fin)
57	2	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → 𝐴:𝑋⟶ℝ)
58	57	adantr 486	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑗 ∈ 𝑋 (𝐴‘𝑗) ≤ (𝐵‘𝑗)) → 𝐴:𝑋⟶ℝ)
59	7	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → 𝐵:𝑋⟶ℝ)
60	59	adantr 486	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑗 ∈ 𝑋 (𝐴‘𝑗) ≤ (𝐵‘𝑗)) → 𝐵:𝑋⟶ℝ)
61		simpr 490	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → 𝑋 ≠ ∅)
62	61	adantr 486	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑗 ∈ 𝑋 (𝐴‘𝑗) ≤ (𝐵‘𝑗)) → 𝑋 ≠ ∅)
63	52, 41	sylanbr 594	. . . . . . . 8 ⊢ ((∀𝑗 ∈ 𝑋 (𝐴‘𝑗) ≤ (𝐵‘𝑗) ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ≤ (𝐵‘𝑘))
64	63	adantll 727	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑗 ∈ 𝑋 (𝐴‘𝑗) ≤ (𝐵‘𝑗)) ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ≤ (𝐵‘𝑘))
65		fveq2 6882	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑘 → (𝐵‘𝑗) = (𝐵‘𝑘))
66	65	oveq1d 7432	. . . . . . . . . 10 ⊢ (𝑗 = 𝑘 → ((𝐵‘𝑗) + (1 / 𝑚)) = ((𝐵‘𝑘) + (1 / 𝑚)))
67	66	cbvmptv 5213	. . . . . . . . 9 ⊢ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚))) = (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑚)))
68	67	mpteq2i 5205	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚)))) = (𝑚 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑚))))
69		oveq2 7425	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑛 → (1 / 𝑚) = (1 / 𝑛))
70	69	oveq2d 7433	. . . . . . . . . 10 ⊢ (𝑚 = 𝑛 → ((𝐵‘𝑘) + (1 / 𝑚)) = ((𝐵‘𝑘) + (1 / 𝑛)))
71	70	mpteq2dv 5203	. . . . . . . . 9 ⊢ (𝑚 = 𝑛 → (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑚))) = (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑛))))
72	71	cbvmptv 5213	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑚)))) = (𝑛 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑛))))
73	68, 72	eqtri 2785	. . . . . . 7 ⊢ (𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚)))) = (𝑛 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑛))))
74		fveq2 6882	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑛 → ((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚))))‘𝑖) = ((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚))))‘𝑛))
75	74	fveq1d 6884	. . . . . . . . . 10 ⊢ (𝑖 = 𝑛 → (((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚))))‘𝑖)‘𝑘) = (((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚))))‘𝑛)‘𝑘))
76	75	oveq2d 7433	. . . . . . . . 9 ⊢ (𝑖 = 𝑛 → ((𝐴‘𝑘)[,)(((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚))))‘𝑖)‘𝑘)) = ((𝐴‘𝑘)[,)(((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚))))‘𝑛)‘𝑘)))
77	76	ixpeq2dv 8924	. . . . . . . 8 ⊢ (𝑖 = 𝑛 → X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚))))‘𝑖)‘𝑘)) = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚))))‘𝑛)‘𝑘)))
78	77	cbvmptv 5213	. . . . . . 7 ⊢ (𝑖 ∈ ℕ ↦ X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚))))‘𝑖)‘𝑘))) = (𝑛 ∈ ℕ ↦ X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) + (1 / 𝑚))))‘𝑛)‘𝑘)))
79	56, 58, 60, 62, 64, 15, 73, 78	vonicclem2 47520	. . . . . 6 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑗 ∈ 𝑋 (𝐴‘𝑗) ≤ (𝐵‘𝑗)) → ((voln‘𝑋)‘𝐼) = ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − (𝐴‘𝑘)))
80	53, 79	syldan 603	. . . . 5 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → ((voln‘𝑋)‘𝐼) = ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − (𝐴‘𝑘)))
81	1, 55, 61, 57, 59	hoidmvn0val 47420	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → (𝐴(𝐿‘𝑋)𝐵) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
82	81	adantr 486	. . . . 5 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → (𝐴(𝐿‘𝑋)𝐵) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
83	48, 80, 82	3eqtr4d 2807	. . . 4 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵))
84		rexnal 3116	. . . . . . . 8 ⊢ (∃𝑘 ∈ 𝑋 ¬ (𝐴‘𝑘) ≤ (𝐵‘𝑘) ↔ ¬ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘))
85	84	bilanri 512	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → ∃𝑘 ∈ 𝑋 ¬ (𝐴‘𝑘) ≤ (𝐵‘𝑘))
86		simpr 490	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ ¬ (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → ¬ (𝐴‘𝑘) ≤ (𝐵‘𝑘))
87	37	adantr 486	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ ¬ (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → (𝐵‘𝑘) ∈ ℝ)
88	36	adantr 486	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ ¬ (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → (𝐴‘𝑘) ∈ ℝ)
89	87, 88	ltnled 11385	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ ¬ (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → ((𝐵‘𝑘) < (𝐴‘𝑘) ↔ ¬ (𝐴‘𝑘) ≤ (𝐵‘𝑘)))
90	86, 89	mpbird 260	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ ¬ (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → (𝐵‘𝑘) < (𝐴‘𝑘))
91	90	ex 418	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (¬ (𝐴‘𝑘) ≤ (𝐵‘𝑘) → (𝐵‘𝑘) < (𝐴‘𝑘)))
92	91	reximdva 3177	. . . . . . . 8 ⊢ (𝜑 → (∃𝑘 ∈ 𝑋 ¬ (𝐴‘𝑘) ≤ (𝐵‘𝑘) → ∃𝑘 ∈ 𝑋 (𝐵‘𝑘) < (𝐴‘𝑘)))
93	92	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → (∃𝑘 ∈ 𝑋 ¬ (𝐴‘𝑘) ≤ (𝐵‘𝑘) → ∃𝑘 ∈ 𝑋 (𝐵‘𝑘) < (𝐴‘𝑘)))
94	85, 93	mpd 16	. . . . . 6 ⊢ ((𝜑 ∧ ¬ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → ∃𝑘 ∈ 𝑋 (𝐵‘𝑘) < (𝐴‘𝑘))
95	94	adantlr 728	. . . . 5 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ¬ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → ∃𝑘 ∈ 𝑋 (𝐵‘𝑘) < (𝐴‘𝑘))
96		nfcv 2924	. . . . . . . . 9 ⊢ Ⅎ𝑘(voln‘𝑋)
97		nfixp1 8929	. . . . . . . . . 10 ⊢ Ⅎ𝑘X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐵‘𝑘))
98	15, 97	nfcxfr 2922	. . . . . . . . 9 ⊢ Ⅎ𝑘𝐼
99	96, 98	nffv 6892	. . . . . . . 8 ⊢ Ⅎ𝑘((voln‘𝑋)‘𝐼)
100		nfcv 2924	. . . . . . . . 9 ⊢ Ⅎ𝑘𝐴
101		nfcv 2924	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘Fin
102		nfcv 2924	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘(ℝ ↑_m 𝑥)
103		nfv 1947	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘 𝑥 = ∅
104		nfcv 2924	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘0
105		nfcv 2924	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘𝑥
106	105	nfcprod1 16001	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))
107	103, 104, 106	nfif 4516	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))
108	102, 102, 107	nfmpo 7499	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘(𝑎 ∈ (ℝ ↑_m 𝑥), 𝑏 ∈ (ℝ ↑_m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))
109	101, 108	nfmpt 5207	. . . . . . . . . . 11 ⊢ Ⅎ𝑘(𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑_m 𝑥), 𝑏 ∈ (ℝ ↑_m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))))
110	1, 109	nfcxfr 2922	. . . . . . . . . 10 ⊢ Ⅎ𝑘𝐿
111		nfcv 2924	. . . . . . . . . 10 ⊢ Ⅎ𝑘𝑋
112	110, 111	nffv 6892	. . . . . . . . 9 ⊢ Ⅎ𝑘(𝐿‘𝑋)
113		nfcv 2924	. . . . . . . . 9 ⊢ Ⅎ𝑘𝐵
114	100, 112, 113	nfov 7447	. . . . . . . 8 ⊢ Ⅎ𝑘(𝐴(𝐿‘𝑋)𝐵)
115	99, 114	nfeq 2937	. . . . . . 7 ⊢ Ⅎ𝑘((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵)
116	54	vonmea 47410	. . . . . . . . . . . 12 ⊢ (𝜑 → (voln‘𝑋) ∈ Meas)
117	116	mea0 47290	. . . . . . . . . . 11 ⊢ (𝜑 → ((voln‘𝑋)‘∅) = 0)
118	117	3ad2ant1 1151	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → ((voln‘𝑋)‘∅) = 0)
119	15	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → 𝐼 = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐵‘𝑘)))
120		simp2 1155	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → 𝑘 ∈ 𝑋)
121		simp3 1156	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → (𝐵‘𝑘) < (𝐴‘𝑘))
122		ressxr 11281	. . . . . . . . . . . . . . . . . 18 ⊢ ℝ ⊆ ℝ^*
123	122, 36	sselid 3932	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈ ℝ^*)
124	122, 37	sselid 3932	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈ ℝ^*)
125		icc0 13450	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴‘𝑘) ∈ ℝ^* ∧ (𝐵‘𝑘) ∈ ℝ^*) → (((𝐴‘𝑘)[,](𝐵‘𝑘)) = ∅ ↔ (𝐵‘𝑘) < (𝐴‘𝑘)))
126	123, 124, 125	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (((𝐴‘𝑘)[,](𝐵‘𝑘)) = ∅ ↔ (𝐵‘𝑘) < (𝐴‘𝑘)))
127	126	3adant3 1150	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → (((𝐴‘𝑘)[,](𝐵‘𝑘)) = ∅ ↔ (𝐵‘𝑘) < (𝐴‘𝑘)))
128	121, 127	mpbird 260	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → ((𝐴‘𝑘)[,](𝐵‘𝑘)) = ∅)
129		rspe 3254	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ 𝑋 ∧ ((𝐴‘𝑘)[,](𝐵‘𝑘)) = ∅) → ∃𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐵‘𝑘)) = ∅)
130	120, 128, 129	syl2anc 596	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → ∃𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐵‘𝑘)) = ∅)
131		ixp0 8942	. . . . . . . . . . . . 13 ⊢ (∃𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐵‘𝑘)) = ∅ → X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐵‘𝑘)) = ∅)
132	130, 131	syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐵‘𝑘)) = ∅)
133	119, 132	eqtrd 2797	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → 𝐼 = ∅)
134	133	fveq2d 6886	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → ((voln‘𝑋)‘𝐼) = ((voln‘𝑋)‘∅))
135		ne0i 4290	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ 𝑋 → 𝑋 ≠ ∅)
136	135	adantl 487	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝑋 ≠ ∅)
137	136, 81	syldan 603	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴(𝐿‘𝑋)𝐵) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
138	137	3adant3 1150	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → (𝐴(𝐿‘𝑋)𝐵) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
139		eleq1w 2845	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑘 → (𝑗 ∈ 𝑋 ↔ 𝑘 ∈ 𝑋))
140		fveq2 6882	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝑘 → (𝐴‘𝑗) = (𝐴‘𝑘))
141	65, 140	breq12d 5120	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑘 → ((𝐵‘𝑗) < (𝐴‘𝑗) ↔ (𝐵‘𝑘) < (𝐴‘𝑘)))
142	139, 141	3anbi23d 1467	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑘 → ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) ↔ (𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘))))
143	142	imbi1d 344	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑘 → (((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = 0) ↔ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = 0)))
144		nfv 1947	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘(𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗))
145	54	3ad2ant1 1151	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) → 𝑋 ∈ Fin)
146		volicore 47417	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℝ)
147	36, 37, 146	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℝ)
148	147	recnd 11265	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℂ)
149	148	3ad2antl1 1204	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℂ)
150		simp2 1155	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) → 𝑗 ∈ 𝑋)
151	49, 50	oveq12d 7435	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑗 → ((𝐴‘𝑘)[,)(𝐵‘𝑘)) = ((𝐴‘𝑗)[,)(𝐵‘𝑗)))
152	151	fveq2d 6886	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑗 → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = (vol‘((𝐴‘𝑗)[,)(𝐵‘𝑗))))
153	152	adantl 487	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) ∧ 𝑘 = 𝑗) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = (vol‘((𝐴‘𝑗)[,)(𝐵‘𝑗))))
154	2	ffvelcdmda 7081	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋) → (𝐴‘𝑗) ∈ ℝ)
155	7	ffvelcdmda 7081	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋) → (𝐵‘𝑗) ∈ ℝ)
156		volico2 47477	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴‘𝑗) ∈ ℝ ∧ (𝐵‘𝑗) ∈ ℝ) → (vol‘((𝐴‘𝑗)[,)(𝐵‘𝑗))) = if((𝐴‘𝑗) ≤ (𝐵‘𝑗), ((𝐵‘𝑗) − (𝐴‘𝑗)), 0))
157	154, 155, 156	syl2anc 596	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋) → (vol‘((𝐴‘𝑗)[,)(𝐵‘𝑗))) = if((𝐴‘𝑗) ≤ (𝐵‘𝑗), ((𝐵‘𝑗) − (𝐴‘𝑗)), 0))
158	157	3adant3 1150	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) → (vol‘((𝐴‘𝑗)[,)(𝐵‘𝑗))) = if((𝐴‘𝑗) ≤ (𝐵‘𝑗), ((𝐵‘𝑗) − (𝐴‘𝑗)), 0))
159		simp3 1156	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) → (𝐵‘𝑗) < (𝐴‘𝑗))
160	155, 154	ltnled 11385	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋) → ((𝐵‘𝑗) < (𝐴‘𝑗) ↔ ¬ (𝐴‘𝑗) ≤ (𝐵‘𝑗)))
161	160	3adant3 1150	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) → ((𝐵‘𝑗) < (𝐴‘𝑗) ↔ ¬ (𝐴‘𝑗) ≤ (𝐵‘𝑗)))
162	159, 161	mpbid 235	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) → ¬ (𝐴‘𝑗) ≤ (𝐵‘𝑗))
163	162	iffalsed 4496	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) → if((𝐴‘𝑗) ≤ (𝐵‘𝑗), ((𝐵‘𝑗) − (𝐴‘𝑗)), 0) = 0)
164	158, 163	eqtrd 2797	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) → (vol‘((𝐴‘𝑗)[,)(𝐵‘𝑗))) = 0)
165	164	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) ∧ 𝑘 = 𝑗) → (vol‘((𝐴‘𝑗)[,)(𝐵‘𝑗))) = 0)
166	153, 165	eqtrd 2797	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) ∧ 𝑘 = 𝑗) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = 0)
167	144, 145, 149, 150, 166	fprodeq0g 16087	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) < (𝐴‘𝑗)) → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = 0)
168	143, 167	chvarvv 2022	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = 0)
169	138, 168	eqtrd 2797	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → (𝐴(𝐿‘𝑋)𝐵) = 0)
170	118, 134, 169	3eqtr4d 2807	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) < (𝐴‘𝑘)) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵))
171	170	3exp 1137	. . . . . . . 8 ⊢ (𝜑 → (𝑘 ∈ 𝑋 → ((𝐵‘𝑘) < (𝐴‘𝑘) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵))))
172	171	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → (𝑘 ∈ 𝑋 → ((𝐵‘𝑘) < (𝐴‘𝑘) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵))))
173	33, 115, 172	rexlimd 3271	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → (∃𝑘 ∈ 𝑋 (𝐵‘𝑘) < (𝐴‘𝑘) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵)))
174	173	imp 412	. . . . 5 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∃𝑘 ∈ 𝑋 (𝐵‘𝑘) < (𝐴‘𝑘)) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵))
175	95, 174	syldan 603	. . . 4 ⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ¬ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) ≤ (𝐵‘𝑘)) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵))
176	83, 175	pm2.61dan 825	. . 3 ⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵))
177	32, 176	syldan 603	. 2 ⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵))
178	30, 177	pm2.61dan 825	1 ⊢ (𝜑 → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 ≠ wne 2957 ∀wral 3078 ∃wrex 3088 ∅c0 4282 ifcif 4485 class class class wbr 5107 ↦ cmpt 5190 dom cdm 5659 ⟶wf 6533 ‘cfv 6537 (class class class)co 7417 ∈ cmpo 7419 ↑_m cmap 8830 Xcixp 8908 Fincfn 8956 ℂcc 11126 ℝcr 11127 0cc0 11128 1c1 11129 + caddc 11131 ℝ^*cxr 11270 < clt 11271 ≤ cle 11272 − cmin 11469 / cdiv 11899 ℕcn 12261 [,)cico 13404 [,]cicc 13405 ∏cprod 15996 volcvol 25697 volncvoln 47374

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2734 ax-rep 5236 ax-sep 5255 ax-nul 5267 ax-pow 5334 ax-pr 5402 ax-un 7740 ax-inf2 9624 ax-cc 10441 ax-cnex 11184 ax-resscn 11185 ax-1cn 11186 ax-icn 11187 ax-addcl 11188 ax-addrcl 11189 ax-mulcl 11190 ax-mulrcl 11191 ax-mulcom 11192 ax-addass 11193 ax-mulass 11194 ax-distr 11195 ax-i2m1 11196 ax-1ne0 11197 ax-1rid 11198 ax-rnegex 11199 ax-rrecex 11200 ax-cnre 11201 ax-pre-lttri 11202 ax-pre-lttrn 11203 ax-pre-ltadd 11204 ax-pre-mulgt0 11205 ax-pre-sup 11206 ax-addf 11207 ax-mulf 11208

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4283 df-if 4486 df-pw 4562 df-sn 4588 df-pr 4590 df-tp 4592 df-op 4594 df-uni 4871 df-int 4911 df-iun 4956 df-iin 4957 df-disj 5075 df-br 5108 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5554 df-eprel 5559 df-po 5567 df-so 5568 df-fr 5612 df-se 5613 df-we 5614 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-isom 6546 df-riota 7374 df-ov 7420 df-oprab 7421 df-mpo 7422 df-of 7682 df-om 7867 df-1st 7990 df-2nd 7991 df-supp 8163 df-tpos 8228 df-frecs 8284 df-wrecs 8315 df-recs 8364 df-rdg 8403 df-1o 8459 df-2o 8460 df-oadd 8463 df-omul 8464 df-er 8700 df-map 8832 df-pm 8833 df-ixp 8909 df-en 8957 df-dom 8958 df-sdom 8959 df-fin 8960 df-fsupp 9336 df-fi 9385 df-sup 9416 df-inf 9417 df-oi 9486 df-dju 9910 df-card 9948 df-acn 9951 df-pnf 11273 df-mnf 11274 df-xr 11275 df-ltxr 11276 df-le 11277 df-sub 11471 df-neg 11472 df-div 11900 df-nn 12262 df-2 12331 df-3 12332 df-4 12333 df-5 12334 df-6 12335 df-7 12336 df-8 12337 df-9 12338 df-n0 12533 df-z 12620 df-dec 12741 df-uz 12892 df-q 13002 df-rp 13047 df-xneg 13167 df-xadd 13168 df-xmul 13169 df-ioo 13406 df-ico 13408 df-icc 13409 df-fz 13566 df-fzo 13714 df-fl 13857 df-seq 14070 df-exp 14130 df-hash 14399 df-cj 15190 df-re 15191 df-im 15192 df-sqrt 15326 df-abs 15327 df-clim 15579 df-rlim 15580 df-sum 15778 df-prod 15997 df-struct 17245 df-sets 17262 df-slot 17280 df-ndx 17292 df-base 17308 df-ress 17329 df-plusg 17361 df-mulr 17362 df-starv 17363 df-sca 17364 df-vsca 17365 df-ip 17366 df-tset 17367 df-ple 17368 df-ds 17370 df-unif 17371 df-hom 17372 df-cco 17373 df-rest 17513 df-topn 17514 df-0g 17532 df-gsum 17533 df-topgen 17534 df-pt 17535 df-prds 17538 df-pws 17540 df-xrs 17594 df-qtop 17599 df-imas 17600 df-xps 17602 df-mre 17676 df-mrc 17677 df-acs 17679 df-mgm 18736 df-sgrp 18827 df-mnd 18843 df-mhm 18897 df-submnd 18898 df-grp 19066 df-minusg 19067 df-sbg 19068 df-mulg 19197 df-subg 19252 df-ghm 19347 df-cntz 19450 df-cmn 19915 df-abl 19916 df-mgp 20280 df-rng 20294 df-ur 20327 df-ring 20380 df-cring 20381 df-oppr 20484 df-dvdsr 20504 df-unit 20505 df-invr 20535 df-dvr 20548 df-rhm 20619 df-subrng 20714 df-subrg 20738 df-drng 20898 df-field 20899 df-abv 20981 df-staf 21011 df-srng 21012 df-lmod 21052 df-lss 21122 df-lmhm 21212 df-lvec 21293 df-sra 21363 df-rgmod 21364 df-psmet 21583 df-xmet 21584 df-met 21585 df-bl 21586 df-mopn 21587 df-cnfld 21592 df-refld 21824 df-phl 21845 df-dsmm 21951 df-frlm 21966 df-top 23125 df-topon 23142 df-topsp 23164 df-bases 23177 df-cn 23458 df-cnp 23459 df-cmp 23618 df-tx 23794 df-hmeo 23987 df-xms 24552 df-ms 24553 df-tms 24554 df-nm 24814 df-ngp 24815 df-tng 24816 df-nrg 24817 df-nlm 24818 df-cncf 25112 df-clm 25297 df-cph 25402 df-tcph 25403 df-rrx 25619 df-ovol 25698 df-vol 25699 df-salg 47145 df-sumge0 47199 df-mea 47286 df-ome 47326 df-caragen 47328 df-ovoln 47373 df-voln 47375

This theorem is used by: vonn0icc 47524

W3C validator