MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  itg1mulc Structured version   Visualization version   GIF version

Theorem itg1mulc 23516
Description: The integral of a constant times a simple function is the constant times the original integral. (Contributed by Mario Carneiro, 25-Jun-2014.)
Hypotheses
Ref Expression
i1fmulc.2 (𝜑𝐹 ∈ dom ∫1)
i1fmulc.3 (𝜑𝐴 ∈ ℝ)
Assertion
Ref Expression
itg1mulc (𝜑 → (∫1‘((ℝ × {𝐴}) ∘𝑓 · 𝐹)) = (𝐴 · (∫1𝐹)))

Proof of Theorem itg1mulc
Dummy variables 𝑘 𝑚 𝑛 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 itg10 23500 . . 3 (∫1‘(ℝ × {0})) = 0
2 reex 10065 . . . . . 6 ℝ ∈ V
32a1i 11 . . . . 5 ((𝜑𝐴 = 0) → ℝ ∈ V)
4 i1fmulc.2 . . . . . . 7 (𝜑𝐹 ∈ dom ∫1)
5 i1ff 23488 . . . . . . 7 (𝐹 ∈ dom ∫1𝐹:ℝ⟶ℝ)
64, 5syl 17 . . . . . 6 (𝜑𝐹:ℝ⟶ℝ)
76adantr 480 . . . . 5 ((𝜑𝐴 = 0) → 𝐹:ℝ⟶ℝ)
8 i1fmulc.3 . . . . . 6 (𝜑𝐴 ∈ ℝ)
98adantr 480 . . . . 5 ((𝜑𝐴 = 0) → 𝐴 ∈ ℝ)
10 0red 10079 . . . . 5 ((𝜑𝐴 = 0) → 0 ∈ ℝ)
11 simplr 807 . . . . . . 7 (((𝜑𝐴 = 0) ∧ 𝑥 ∈ ℝ) → 𝐴 = 0)
1211oveq1d 6705 . . . . . 6 (((𝜑𝐴 = 0) ∧ 𝑥 ∈ ℝ) → (𝐴 · 𝑥) = (0 · 𝑥))
13 mul02lem2 10251 . . . . . . 7 (𝑥 ∈ ℝ → (0 · 𝑥) = 0)
1413adantl 481 . . . . . 6 (((𝜑𝐴 = 0) ∧ 𝑥 ∈ ℝ) → (0 · 𝑥) = 0)
1512, 14eqtrd 2685 . . . . 5 (((𝜑𝐴 = 0) ∧ 𝑥 ∈ ℝ) → (𝐴 · 𝑥) = 0)
163, 7, 9, 10, 15caofid2 6970 . . . 4 ((𝜑𝐴 = 0) → ((ℝ × {𝐴}) ∘𝑓 · 𝐹) = (ℝ × {0}))
1716fveq2d 6233 . . 3 ((𝜑𝐴 = 0) → (∫1‘((ℝ × {𝐴}) ∘𝑓 · 𝐹)) = (∫1‘(ℝ × {0})))
18 simpr 476 . . . . 5 ((𝜑𝐴 = 0) → 𝐴 = 0)
1918oveq1d 6705 . . . 4 ((𝜑𝐴 = 0) → (𝐴 · (∫1𝐹)) = (0 · (∫1𝐹)))
20 itg1cl 23497 . . . . . . . 8 (𝐹 ∈ dom ∫1 → (∫1𝐹) ∈ ℝ)
214, 20syl 17 . . . . . . 7 (𝜑 → (∫1𝐹) ∈ ℝ)
2221recnd 10106 . . . . . 6 (𝜑 → (∫1𝐹) ∈ ℂ)
2322mul02d 10272 . . . . 5 (𝜑 → (0 · (∫1𝐹)) = 0)
2423adantr 480 . . . 4 ((𝜑𝐴 = 0) → (0 · (∫1𝐹)) = 0)
2519, 24eqtrd 2685 . . 3 ((𝜑𝐴 = 0) → (𝐴 · (∫1𝐹)) = 0)
261, 17, 253eqtr4a 2711 . 2 ((𝜑𝐴 = 0) → (∫1‘((ℝ × {𝐴}) ∘𝑓 · 𝐹)) = (𝐴 · (∫1𝐹)))
274, 8i1fmulc 23515 . . . . . . . . . . . . . 14 (𝜑 → ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∈ dom ∫1)
2827adantr 480 . . . . . . . . . . . . 13 ((𝜑𝐴 ≠ 0) → ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∈ dom ∫1)
29 i1ff 23488 . . . . . . . . . . . . 13 (((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∈ dom ∫1 → ((ℝ × {𝐴}) ∘𝑓 · 𝐹):ℝ⟶ℝ)
3028, 29syl 17 . . . . . . . . . . . 12 ((𝜑𝐴 ≠ 0) → ((ℝ × {𝐴}) ∘𝑓 · 𝐹):ℝ⟶ℝ)
31 frn 6091 . . . . . . . . . . . 12 (((ℝ × {𝐴}) ∘𝑓 · 𝐹):ℝ⟶ℝ → ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ⊆ ℝ)
3230, 31syl 17 . . . . . . . . . . 11 ((𝜑𝐴 ≠ 0) → ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ⊆ ℝ)
3332ssdifssd 3781 . . . . . . . . . 10 ((𝜑𝐴 ≠ 0) → (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0}) ⊆ ℝ)
3433sselda 3636 . . . . . . . . 9 (((𝜑𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → 𝑚 ∈ ℝ)
3534recnd 10106 . . . . . . . 8 (((𝜑𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → 𝑚 ∈ ℂ)
368adantr 480 . . . . . . . . . 10 ((𝜑𝐴 ≠ 0) → 𝐴 ∈ ℝ)
3736recnd 10106 . . . . . . . . 9 ((𝜑𝐴 ≠ 0) → 𝐴 ∈ ℂ)
3837adantr 480 . . . . . . . 8 (((𝜑𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → 𝐴 ∈ ℂ)
39 simplr 807 . . . . . . . 8 (((𝜑𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → 𝐴 ≠ 0)
4035, 38, 39divcan2d 10841 . . . . . . 7 (((𝜑𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → (𝐴 · (𝑚 / 𝐴)) = 𝑚)
414, 8i1fmulclem 23514 . . . . . . . . . 10 (((𝜑𝐴 ≠ 0) ∧ 𝑚 ∈ ℝ) → (((ℝ × {𝐴}) ∘𝑓 · 𝐹) “ {𝑚}) = (𝐹 “ {(𝑚 / 𝐴)}))
4234, 41syldan 486 . . . . . . . . 9 (((𝜑𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → (((ℝ × {𝐴}) ∘𝑓 · 𝐹) “ {𝑚}) = (𝐹 “ {(𝑚 / 𝐴)}))
4342fveq2d 6233 . . . . . . . 8 (((𝜑𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → (vol‘(((ℝ × {𝐴}) ∘𝑓 · 𝐹) “ {𝑚})) = (vol‘(𝐹 “ {(𝑚 / 𝐴)})))
4443eqcomd 2657 . . . . . . 7 (((𝜑𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → (vol‘(𝐹 “ {(𝑚 / 𝐴)})) = (vol‘(((ℝ × {𝐴}) ∘𝑓 · 𝐹) “ {𝑚})))
4540, 44oveq12d 6708 . . . . . 6 (((𝜑𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → ((𝐴 · (𝑚 / 𝐴)) · (vol‘(𝐹 “ {(𝑚 / 𝐴)}))) = (𝑚 · (vol‘(((ℝ × {𝐴}) ∘𝑓 · 𝐹) “ {𝑚}))))
468ad2antrr 762 . . . . . . . . 9 (((𝜑𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → 𝐴 ∈ ℝ)
4734, 46, 39redivcld 10891 . . . . . . . 8 (((𝜑𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → (𝑚 / 𝐴) ∈ ℝ)
4847recnd 10106 . . . . . . 7 (((𝜑𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → (𝑚 / 𝐴) ∈ ℂ)
494ad2antrr 762 . . . . . . . . 9 (((𝜑𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → 𝐹 ∈ dom ∫1)
5046recnd 10106 . . . . . . . . . . 11 (((𝜑𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → 𝐴 ∈ ℂ)
51 eldifsni 4353 . . . . . . . . . . . 12 (𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0}) → 𝑚 ≠ 0)
5251adantl 481 . . . . . . . . . . 11 (((𝜑𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → 𝑚 ≠ 0)
5335, 50, 52, 39divne0d 10855 . . . . . . . . . 10 (((𝜑𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → (𝑚 / 𝐴) ≠ 0)
54 eldifsn 4350 . . . . . . . . . 10 ((𝑚 / 𝐴) ∈ (ℝ ∖ {0}) ↔ ((𝑚 / 𝐴) ∈ ℝ ∧ (𝑚 / 𝐴) ≠ 0))
5547, 53, 54sylanbrc 699 . . . . . . . . 9 (((𝜑𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → (𝑚 / 𝐴) ∈ (ℝ ∖ {0}))
56 i1fima2sn 23492 . . . . . . . . 9 ((𝐹 ∈ dom ∫1 ∧ (𝑚 / 𝐴) ∈ (ℝ ∖ {0})) → (vol‘(𝐹 “ {(𝑚 / 𝐴)})) ∈ ℝ)
5749, 55, 56syl2anc 694 . . . . . . . 8 (((𝜑𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → (vol‘(𝐹 “ {(𝑚 / 𝐴)})) ∈ ℝ)
5857recnd 10106 . . . . . . 7 (((𝜑𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → (vol‘(𝐹 “ {(𝑚 / 𝐴)})) ∈ ℂ)
5938, 48, 58mulassd 10101 . . . . . 6 (((𝜑𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → ((𝐴 · (𝑚 / 𝐴)) · (vol‘(𝐹 “ {(𝑚 / 𝐴)}))) = (𝐴 · ((𝑚 / 𝐴) · (vol‘(𝐹 “ {(𝑚 / 𝐴)})))))
6045, 59eqtr3d 2687 . . . . 5 (((𝜑𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → (𝑚 · (vol‘(((ℝ × {𝐴}) ∘𝑓 · 𝐹) “ {𝑚}))) = (𝐴 · ((𝑚 / 𝐴) · (vol‘(𝐹 “ {(𝑚 / 𝐴)})))))
6160sumeq2dv 14477 . . . 4 ((𝜑𝐴 ≠ 0) → Σ𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})(𝑚 · (vol‘(((ℝ × {𝐴}) ∘𝑓 · 𝐹) “ {𝑚}))) = Σ𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})(𝐴 · ((𝑚 / 𝐴) · (vol‘(𝐹 “ {(𝑚 / 𝐴)})))))
62 i1frn 23489 . . . . . . 7 (((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∈ dom ∫1 → ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∈ Fin)
6328, 62syl 17 . . . . . 6 ((𝜑𝐴 ≠ 0) → ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∈ Fin)
64 difss 3770 . . . . . 6 (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0}) ⊆ ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹)
65 ssfi 8221 . . . . . 6 ((ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∈ Fin ∧ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0}) ⊆ ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹)) → (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0}) ∈ Fin)
6663, 64, 65sylancl 695 . . . . 5 ((𝜑𝐴 ≠ 0) → (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0}) ∈ Fin)
6748, 58mulcld 10098 . . . . 5 (((𝜑𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → ((𝑚 / 𝐴) · (vol‘(𝐹 “ {(𝑚 / 𝐴)}))) ∈ ℂ)
6866, 37, 67fsummulc2 14560 . . . 4 ((𝜑𝐴 ≠ 0) → (𝐴 · Σ𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})((𝑚 / 𝐴) · (vol‘(𝐹 “ {(𝑚 / 𝐴)})))) = Σ𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})(𝐴 · ((𝑚 / 𝐴) · (vol‘(𝐹 “ {(𝑚 / 𝐴)})))))
6961, 68eqtr4d 2688 . . 3 ((𝜑𝐴 ≠ 0) → Σ𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})(𝑚 · (vol‘(((ℝ × {𝐴}) ∘𝑓 · 𝐹) “ {𝑚}))) = (𝐴 · Σ𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})((𝑚 / 𝐴) · (vol‘(𝐹 “ {(𝑚 / 𝐴)})))))
70 itg1val 23495 . . . 4 (((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∈ dom ∫1 → (∫1‘((ℝ × {𝐴}) ∘𝑓 · 𝐹)) = Σ𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})(𝑚 · (vol‘(((ℝ × {𝐴}) ∘𝑓 · 𝐹) “ {𝑚}))))
7128, 70syl 17 . . 3 ((𝜑𝐴 ≠ 0) → (∫1‘((ℝ × {𝐴}) ∘𝑓 · 𝐹)) = Σ𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})(𝑚 · (vol‘(((ℝ × {𝐴}) ∘𝑓 · 𝐹) “ {𝑚}))))
724adantr 480 . . . . . 6 ((𝜑𝐴 ≠ 0) → 𝐹 ∈ dom ∫1)
73 itg1val 23495 . . . . . 6 (𝐹 ∈ dom ∫1 → (∫1𝐹) = Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘(𝐹 “ {𝑘}))))
7472, 73syl 17 . . . . 5 ((𝜑𝐴 ≠ 0) → (∫1𝐹) = Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘(𝐹 “ {𝑘}))))
75 id 22 . . . . . . 7 (𝑘 = (𝑚 / 𝐴) → 𝑘 = (𝑚 / 𝐴))
76 sneq 4220 . . . . . . . . 9 (𝑘 = (𝑚 / 𝐴) → {𝑘} = {(𝑚 / 𝐴)})
7776imaeq2d 5501 . . . . . . . 8 (𝑘 = (𝑚 / 𝐴) → (𝐹 “ {𝑘}) = (𝐹 “ {(𝑚 / 𝐴)}))
7877fveq2d 6233 . . . . . . 7 (𝑘 = (𝑚 / 𝐴) → (vol‘(𝐹 “ {𝑘})) = (vol‘(𝐹 “ {(𝑚 / 𝐴)})))
7975, 78oveq12d 6708 . . . . . 6 (𝑘 = (𝑚 / 𝐴) → (𝑘 · (vol‘(𝐹 “ {𝑘}))) = ((𝑚 / 𝐴) · (vol‘(𝐹 “ {(𝑚 / 𝐴)}))))
80 eqid 2651 . . . . . . 7 (𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0}) ↦ (𝑛 / 𝐴)) = (𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0}) ↦ (𝑛 / 𝐴))
81 eldifi 3765 . . . . . . . . 9 (𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0}) → 𝑛 ∈ ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹))
822a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → ℝ ∈ V)
83 ffn 6083 . . . . . . . . . . . . . . . . . 18 (𝐹:ℝ⟶ℝ → 𝐹 Fn ℝ)
846, 83syl 17 . . . . . . . . . . . . . . . . 17 (𝜑𝐹 Fn ℝ)
85 eqidd 2652 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ ℝ) → (𝐹𝑦) = (𝐹𝑦))
8682, 8, 84, 85ofc1 6962 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ ℝ) → (((ℝ × {𝐴}) ∘𝑓 · 𝐹)‘𝑦) = (𝐴 · (𝐹𝑦)))
8786adantlr 751 . . . . . . . . . . . . . . 15 (((𝜑𝐴 ≠ 0) ∧ 𝑦 ∈ ℝ) → (((ℝ × {𝐴}) ∘𝑓 · 𝐹)‘𝑦) = (𝐴 · (𝐹𝑦)))
8887oveq1d 6705 . . . . . . . . . . . . . 14 (((𝜑𝐴 ≠ 0) ∧ 𝑦 ∈ ℝ) → ((((ℝ × {𝐴}) ∘𝑓 · 𝐹)‘𝑦) / 𝐴) = ((𝐴 · (𝐹𝑦)) / 𝐴))
896adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝐴 ≠ 0) → 𝐹:ℝ⟶ℝ)
9089ffvelrnda 6399 . . . . . . . . . . . . . . . 16 (((𝜑𝐴 ≠ 0) ∧ 𝑦 ∈ ℝ) → (𝐹𝑦) ∈ ℝ)
9190recnd 10106 . . . . . . . . . . . . . . 15 (((𝜑𝐴 ≠ 0) ∧ 𝑦 ∈ ℝ) → (𝐹𝑦) ∈ ℂ)
9237adantr 480 . . . . . . . . . . . . . . 15 (((𝜑𝐴 ≠ 0) ∧ 𝑦 ∈ ℝ) → 𝐴 ∈ ℂ)
93 simplr 807 . . . . . . . . . . . . . . 15 (((𝜑𝐴 ≠ 0) ∧ 𝑦 ∈ ℝ) → 𝐴 ≠ 0)
9491, 92, 93divcan3d 10844 . . . . . . . . . . . . . 14 (((𝜑𝐴 ≠ 0) ∧ 𝑦 ∈ ℝ) → ((𝐴 · (𝐹𝑦)) / 𝐴) = (𝐹𝑦))
9588, 94eqtrd 2685 . . . . . . . . . . . . 13 (((𝜑𝐴 ≠ 0) ∧ 𝑦 ∈ ℝ) → ((((ℝ × {𝐴}) ∘𝑓 · 𝐹)‘𝑦) / 𝐴) = (𝐹𝑦))
9689, 83syl 17 . . . . . . . . . . . . . 14 ((𝜑𝐴 ≠ 0) → 𝐹 Fn ℝ)
97 fnfvelrn 6396 . . . . . . . . . . . . . 14 ((𝐹 Fn ℝ ∧ 𝑦 ∈ ℝ) → (𝐹𝑦) ∈ ran 𝐹)
9896, 97sylan 487 . . . . . . . . . . . . 13 (((𝜑𝐴 ≠ 0) ∧ 𝑦 ∈ ℝ) → (𝐹𝑦) ∈ ran 𝐹)
9995, 98eqeltrd 2730 . . . . . . . . . . . 12 (((𝜑𝐴 ≠ 0) ∧ 𝑦 ∈ ℝ) → ((((ℝ × {𝐴}) ∘𝑓 · 𝐹)‘𝑦) / 𝐴) ∈ ran 𝐹)
10099ralrimiva 2995 . . . . . . . . . . 11 ((𝜑𝐴 ≠ 0) → ∀𝑦 ∈ ℝ ((((ℝ × {𝐴}) ∘𝑓 · 𝐹)‘𝑦) / 𝐴) ∈ ran 𝐹)
101 ffn 6083 . . . . . . . . . . . . 13 (((ℝ × {𝐴}) ∘𝑓 · 𝐹):ℝ⟶ℝ → ((ℝ × {𝐴}) ∘𝑓 · 𝐹) Fn ℝ)
10230, 101syl 17 . . . . . . . . . . . 12 ((𝜑𝐴 ≠ 0) → ((ℝ × {𝐴}) ∘𝑓 · 𝐹) Fn ℝ)
103 oveq1 6697 . . . . . . . . . . . . . 14 (𝑛 = (((ℝ × {𝐴}) ∘𝑓 · 𝐹)‘𝑦) → (𝑛 / 𝐴) = ((((ℝ × {𝐴}) ∘𝑓 · 𝐹)‘𝑦) / 𝐴))
104103eleq1d 2715 . . . . . . . . . . . . 13 (𝑛 = (((ℝ × {𝐴}) ∘𝑓 · 𝐹)‘𝑦) → ((𝑛 / 𝐴) ∈ ran 𝐹 ↔ ((((ℝ × {𝐴}) ∘𝑓 · 𝐹)‘𝑦) / 𝐴) ∈ ran 𝐹))
105104ralrn 6402 . . . . . . . . . . . 12 (((ℝ × {𝐴}) ∘𝑓 · 𝐹) Fn ℝ → (∀𝑛 ∈ ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹)(𝑛 / 𝐴) ∈ ran 𝐹 ↔ ∀𝑦 ∈ ℝ ((((ℝ × {𝐴}) ∘𝑓 · 𝐹)‘𝑦) / 𝐴) ∈ ran 𝐹))
106102, 105syl 17 . . . . . . . . . . 11 ((𝜑𝐴 ≠ 0) → (∀𝑛 ∈ ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹)(𝑛 / 𝐴) ∈ ran 𝐹 ↔ ∀𝑦 ∈ ℝ ((((ℝ × {𝐴}) ∘𝑓 · 𝐹)‘𝑦) / 𝐴) ∈ ran 𝐹))
107100, 106mpbird 247 . . . . . . . . . 10 ((𝜑𝐴 ≠ 0) → ∀𝑛 ∈ ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹)(𝑛 / 𝐴) ∈ ran 𝐹)
108107r19.21bi 2961 . . . . . . . . 9 (((𝜑𝐴 ≠ 0) ∧ 𝑛 ∈ ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹)) → (𝑛 / 𝐴) ∈ ran 𝐹)
10981, 108sylan2 490 . . . . . . . 8 (((𝜑𝐴 ≠ 0) ∧ 𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → (𝑛 / 𝐴) ∈ ran 𝐹)
11033sselda 3636 . . . . . . . . . 10 (((𝜑𝐴 ≠ 0) ∧ 𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → 𝑛 ∈ ℝ)
111110recnd 10106 . . . . . . . . 9 (((𝜑𝐴 ≠ 0) ∧ 𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → 𝑛 ∈ ℂ)
11237adantr 480 . . . . . . . . 9 (((𝜑𝐴 ≠ 0) ∧ 𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → 𝐴 ∈ ℂ)
113 eldifsni 4353 . . . . . . . . . 10 (𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0}) → 𝑛 ≠ 0)
114113adantl 481 . . . . . . . . 9 (((𝜑𝐴 ≠ 0) ∧ 𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → 𝑛 ≠ 0)
115 simplr 807 . . . . . . . . 9 (((𝜑𝐴 ≠ 0) ∧ 𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → 𝐴 ≠ 0)
116111, 112, 114, 115divne0d 10855 . . . . . . . 8 (((𝜑𝐴 ≠ 0) ∧ 𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → (𝑛 / 𝐴) ≠ 0)
117 eldifsn 4350 . . . . . . . 8 ((𝑛 / 𝐴) ∈ (ran 𝐹 ∖ {0}) ↔ ((𝑛 / 𝐴) ∈ ran 𝐹 ∧ (𝑛 / 𝐴) ≠ 0))
118109, 116, 117sylanbrc 699 . . . . . . 7 (((𝜑𝐴 ≠ 0) ∧ 𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → (𝑛 / 𝐴) ∈ (ran 𝐹 ∖ {0}))
119 eldifi 3765 . . . . . . . . 9 (𝑘 ∈ (ran 𝐹 ∖ {0}) → 𝑘 ∈ ran 𝐹)
120 fnfvelrn 6396 . . . . . . . . . . . . . 14 ((((ℝ × {𝐴}) ∘𝑓 · 𝐹) Fn ℝ ∧ 𝑦 ∈ ℝ) → (((ℝ × {𝐴}) ∘𝑓 · 𝐹)‘𝑦) ∈ ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹))
121102, 120sylan 487 . . . . . . . . . . . . 13 (((𝜑𝐴 ≠ 0) ∧ 𝑦 ∈ ℝ) → (((ℝ × {𝐴}) ∘𝑓 · 𝐹)‘𝑦) ∈ ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹))
12287, 121eqeltrrd 2731 . . . . . . . . . . . 12 (((𝜑𝐴 ≠ 0) ∧ 𝑦 ∈ ℝ) → (𝐴 · (𝐹𝑦)) ∈ ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹))
123122ralrimiva 2995 . . . . . . . . . . 11 ((𝜑𝐴 ≠ 0) → ∀𝑦 ∈ ℝ (𝐴 · (𝐹𝑦)) ∈ ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹))
124 oveq2 6698 . . . . . . . . . . . . . 14 (𝑘 = (𝐹𝑦) → (𝐴 · 𝑘) = (𝐴 · (𝐹𝑦)))
125124eleq1d 2715 . . . . . . . . . . . . 13 (𝑘 = (𝐹𝑦) → ((𝐴 · 𝑘) ∈ ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ↔ (𝐴 · (𝐹𝑦)) ∈ ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹)))
126125ralrn 6402 . . . . . . . . . . . 12 (𝐹 Fn ℝ → (∀𝑘 ∈ ran 𝐹(𝐴 · 𝑘) ∈ ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ↔ ∀𝑦 ∈ ℝ (𝐴 · (𝐹𝑦)) ∈ ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹)))
12796, 126syl 17 . . . . . . . . . . 11 ((𝜑𝐴 ≠ 0) → (∀𝑘 ∈ ran 𝐹(𝐴 · 𝑘) ∈ ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ↔ ∀𝑦 ∈ ℝ (𝐴 · (𝐹𝑦)) ∈ ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹)))
128123, 127mpbird 247 . . . . . . . . . 10 ((𝜑𝐴 ≠ 0) → ∀𝑘 ∈ ran 𝐹(𝐴 · 𝑘) ∈ ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹))
129128r19.21bi 2961 . . . . . . . . 9 (((𝜑𝐴 ≠ 0) ∧ 𝑘 ∈ ran 𝐹) → (𝐴 · 𝑘) ∈ ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹))
130119, 129sylan2 490 . . . . . . . 8 (((𝜑𝐴 ≠ 0) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝐴 · 𝑘) ∈ ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹))
13137adantr 480 . . . . . . . . 9 (((𝜑𝐴 ≠ 0) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → 𝐴 ∈ ℂ)
132 frn 6091 . . . . . . . . . . . . 13 (𝐹:ℝ⟶ℝ → ran 𝐹 ⊆ ℝ)
13389, 132syl 17 . . . . . . . . . . . 12 ((𝜑𝐴 ≠ 0) → ran 𝐹 ⊆ ℝ)
134133ssdifssd 3781 . . . . . . . . . . 11 ((𝜑𝐴 ≠ 0) → (ran 𝐹 ∖ {0}) ⊆ ℝ)
135134sselda 3636 . . . . . . . . . 10 (((𝜑𝐴 ≠ 0) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → 𝑘 ∈ ℝ)
136135recnd 10106 . . . . . . . . 9 (((𝜑𝐴 ≠ 0) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → 𝑘 ∈ ℂ)
137 simplr 807 . . . . . . . . 9 (((𝜑𝐴 ≠ 0) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → 𝐴 ≠ 0)
138 eldifsni 4353 . . . . . . . . . 10 (𝑘 ∈ (ran 𝐹 ∖ {0}) → 𝑘 ≠ 0)
139138adantl 481 . . . . . . . . 9 (((𝜑𝐴 ≠ 0) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → 𝑘 ≠ 0)
140131, 136, 137, 139mulne0d 10717 . . . . . . . 8 (((𝜑𝐴 ≠ 0) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝐴 · 𝑘) ≠ 0)
141 eldifsn 4350 . . . . . . . 8 ((𝐴 · 𝑘) ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0}) ↔ ((𝐴 · 𝑘) ∈ ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∧ (𝐴 · 𝑘) ≠ 0))
142130, 140, 141sylanbrc 699 . . . . . . 7 (((𝜑𝐴 ≠ 0) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝐴 · 𝑘) ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0}))
143 simpl 472 . . . . . . . . . . . 12 ((𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0}) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → 𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0}))
144 ssel2 3631 . . . . . . . . . . . 12 (((ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0}) ⊆ ℝ ∧ 𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → 𝑛 ∈ ℝ)
14533, 143, 144syl2an 493 . . . . . . . . . . 11 (((𝜑𝐴 ≠ 0) ∧ (𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0}) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0}))) → 𝑛 ∈ ℝ)
146145recnd 10106 . . . . . . . . . 10 (((𝜑𝐴 ≠ 0) ∧ (𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0}) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0}))) → 𝑛 ∈ ℂ)
1478ad2antrr 762 . . . . . . . . . . 11 (((𝜑𝐴 ≠ 0) ∧ (𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0}) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0}))) → 𝐴 ∈ ℝ)
148147recnd 10106 . . . . . . . . . 10 (((𝜑𝐴 ≠ 0) ∧ (𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0}) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0}))) → 𝐴 ∈ ℂ)
149135adantrl 752 . . . . . . . . . . 11 (((𝜑𝐴 ≠ 0) ∧ (𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0}) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0}))) → 𝑘 ∈ ℝ)
150149recnd 10106 . . . . . . . . . 10 (((𝜑𝐴 ≠ 0) ∧ (𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0}) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0}))) → 𝑘 ∈ ℂ)
151 simplr 807 . . . . . . . . . 10 (((𝜑𝐴 ≠ 0) ∧ (𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0}) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0}))) → 𝐴 ≠ 0)
152146, 148, 150, 151divmuld 10861 . . . . . . . . 9 (((𝜑𝐴 ≠ 0) ∧ (𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0}) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0}))) → ((𝑛 / 𝐴) = 𝑘 ↔ (𝐴 · 𝑘) = 𝑛))
153152bicomd 213 . . . . . . . 8 (((𝜑𝐴 ≠ 0) ∧ (𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0}) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0}))) → ((𝐴 · 𝑘) = 𝑛 ↔ (𝑛 / 𝐴) = 𝑘))
154 eqcom 2658 . . . . . . . 8 (𝑛 = (𝐴 · 𝑘) ↔ (𝐴 · 𝑘) = 𝑛)
155 eqcom 2658 . . . . . . . 8 (𝑘 = (𝑛 / 𝐴) ↔ (𝑛 / 𝐴) = 𝑘)
156153, 154, 1553bitr4g 303 . . . . . . 7 (((𝜑𝐴 ≠ 0) ∧ (𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0}) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0}))) → (𝑛 = (𝐴 · 𝑘) ↔ 𝑘 = (𝑛 / 𝐴)))
15780, 118, 142, 156f1o2d 6929 . . . . . 6 ((𝜑𝐴 ≠ 0) → (𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0}) ↦ (𝑛 / 𝐴)):(ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})–1-1-onto→(ran 𝐹 ∖ {0}))
158 oveq1 6697 . . . . . . . 8 (𝑛 = 𝑚 → (𝑛 / 𝐴) = (𝑚 / 𝐴))
159 ovex 6718 . . . . . . . 8 (𝑚 / 𝐴) ∈ V
160158, 80, 159fvmpt 6321 . . . . . . 7 (𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0}) → ((𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0}) ↦ (𝑛 / 𝐴))‘𝑚) = (𝑚 / 𝐴))
161160adantl 481 . . . . . 6 (((𝜑𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → ((𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0}) ↦ (𝑛 / 𝐴))‘𝑚) = (𝑚 / 𝐴))
162 i1fima2sn 23492 . . . . . . . . 9 ((𝐹 ∈ dom ∫1𝑘 ∈ (ran 𝐹 ∖ {0})) → (vol‘(𝐹 “ {𝑘})) ∈ ℝ)
16372, 162sylan 487 . . . . . . . 8 (((𝜑𝐴 ≠ 0) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (vol‘(𝐹 “ {𝑘})) ∈ ℝ)
164135, 163remulcld 10108 . . . . . . 7 (((𝜑𝐴 ≠ 0) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑘 · (vol‘(𝐹 “ {𝑘}))) ∈ ℝ)
165164recnd 10106 . . . . . 6 (((𝜑𝐴 ≠ 0) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑘 · (vol‘(𝐹 “ {𝑘}))) ∈ ℂ)
16679, 66, 157, 161, 165fsumf1o 14498 . . . . 5 ((𝜑𝐴 ≠ 0) → Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘(𝐹 “ {𝑘}))) = Σ𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})((𝑚 / 𝐴) · (vol‘(𝐹 “ {(𝑚 / 𝐴)}))))
16774, 166eqtrd 2685 . . . 4 ((𝜑𝐴 ≠ 0) → (∫1𝐹) = Σ𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})((𝑚 / 𝐴) · (vol‘(𝐹 “ {(𝑚 / 𝐴)}))))
168167oveq2d 6706 . . 3 ((𝜑𝐴 ≠ 0) → (𝐴 · (∫1𝐹)) = (𝐴 · Σ𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})((𝑚 / 𝐴) · (vol‘(𝐹 “ {(𝑚 / 𝐴)})))))
16969, 71, 1683eqtr4d 2695 . 2 ((𝜑𝐴 ≠ 0) → (∫1‘((ℝ × {𝐴}) ∘𝑓 · 𝐹)) = (𝐴 · (∫1𝐹)))
17026, 169pm2.61dane 2910 1 (𝜑 → (∫1‘((ℝ × {𝐴}) ∘𝑓 · 𝐹)) = (𝐴 · (∫1𝐹)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1523  wcel 2030  wne 2823  wral 2941  Vcvv 3231  cdif 3604  wss 3607  {csn 4210  cmpt 4762   × cxp 5141  ccnv 5142  dom cdm 5143  ran crn 5144  cima 5146   Fn wfn 5921  wf 5922  cfv 5926  (class class class)co 6690  𝑓 cof 6937  Fincfn 7997  cc 9972  cr 9973  0cc0 9974   · cmul 9979   / cdiv 10722  Σcsu 14460  volcvol 23278  1citg1 23429
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-of 6939  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-er 7787  df-map 7901  df-pm 7902  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-sup 8389  df-inf 8390  df-oi 8456  df-card 8803  df-cda 9028  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-n0 11331  df-z 11416  df-uz 11726  df-q 11827  df-rp 11871  df-xadd 11985  df-ioo 12217  df-ico 12219  df-icc 12220  df-fz 12365  df-fzo 12505  df-fl 12633  df-seq 12842  df-exp 12901  df-hash 13158  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-clim 14263  df-sum 14461  df-xmet 19787  df-met 19788  df-ovol 23279  df-vol 23280  df-mbf 23433  df-itg1 23434
This theorem is referenced by:  itg1sub  23521  itg2const  23552  itg2mulclem  23558  itg2monolem1  23562  itg2addnclem  33591
  Copyright terms: Public domain W3C validator