Step | Hyp | Ref
| Expression |
1 | | itg10 24609 |
. . 3
⊢
(∫1‘(ℝ × {0})) = 0 |
2 | | reex 10845 |
. . . . . 6
⊢ ℝ
∈ V |
3 | 2 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 = 0) → ℝ ∈
V) |
4 | | i1fmulc.2 |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈ dom
∫1) |
5 | | i1ff 24597 |
. . . . . . 7
⊢ (𝐹 ∈ dom ∫1
→ 𝐹:ℝ⟶ℝ) |
6 | 4, 5 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) |
7 | 6 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 = 0) → 𝐹:ℝ⟶ℝ) |
8 | | i1fmulc.3 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ ℝ) |
9 | 8 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 = 0) → 𝐴 ∈ ℝ) |
10 | | 0red 10861 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 = 0) → 0 ∈
ℝ) |
11 | | simplr 769 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 = 0) ∧ 𝑥 ∈ ℝ) → 𝐴 = 0) |
12 | 11 | oveq1d 7247 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 = 0) ∧ 𝑥 ∈ ℝ) → (𝐴 · 𝑥) = (0 · 𝑥)) |
13 | | mul02lem2 11034 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ → (0
· 𝑥) =
0) |
14 | 13 | adantl 485 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 = 0) ∧ 𝑥 ∈ ℝ) → (0 · 𝑥) = 0) |
15 | 12, 14 | eqtrd 2778 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 = 0) ∧ 𝑥 ∈ ℝ) → (𝐴 · 𝑥) = 0) |
16 | 3, 7, 9, 10, 15 | caofid2 7521 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 = 0) → ((ℝ × {𝐴}) ∘f ·
𝐹) = (ℝ ×
{0})) |
17 | 16 | fveq2d 6740 |
. . 3
⊢ ((𝜑 ∧ 𝐴 = 0) →
(∫1‘((ℝ × {𝐴}) ∘f · 𝐹)) =
(∫1‘(ℝ × {0}))) |
18 | | simpr 488 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 = 0) → 𝐴 = 0) |
19 | 18 | oveq1d 7247 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 = 0) → (𝐴 · (∫1‘𝐹)) = (0 ·
(∫1‘𝐹))) |
20 | | itg1cl 24606 |
. . . . . . . 8
⊢ (𝐹 ∈ dom ∫1
→ (∫1‘𝐹) ∈ ℝ) |
21 | 4, 20 | syl 17 |
. . . . . . 7
⊢ (𝜑 →
(∫1‘𝐹)
∈ ℝ) |
22 | 21 | recnd 10886 |
. . . . . 6
⊢ (𝜑 →
(∫1‘𝐹)
∈ ℂ) |
23 | 22 | mul02d 11055 |
. . . . 5
⊢ (𝜑 → (0 ·
(∫1‘𝐹)) = 0) |
24 | 23 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 = 0) → (0 ·
(∫1‘𝐹)) = 0) |
25 | 19, 24 | eqtrd 2778 |
. . 3
⊢ ((𝜑 ∧ 𝐴 = 0) → (𝐴 · (∫1‘𝐹)) = 0) |
26 | 1, 17, 25 | 3eqtr4a 2805 |
. 2
⊢ ((𝜑 ∧ 𝐴 = 0) →
(∫1‘((ℝ × {𝐴}) ∘f · 𝐹)) = (𝐴 · (∫1‘𝐹))) |
27 | 4, 8 | i1fmulc 24625 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((ℝ × {𝐴}) ∘f ·
𝐹) ∈ dom
∫1) |
28 | 27 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ((ℝ × {𝐴}) ∘f ·
𝐹) ∈ dom
∫1) |
29 | | i1ff 24597 |
. . . . . . . . . . . . 13
⊢
(((ℝ × {𝐴}) ∘f · 𝐹) ∈ dom ∫1
→ ((ℝ × {𝐴}) ∘f · 𝐹):ℝ⟶ℝ) |
30 | 28, 29 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ((ℝ × {𝐴}) ∘f ·
𝐹):ℝ⟶ℝ) |
31 | 30 | frnd 6572 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ran ((ℝ × {𝐴}) ∘f ·
𝐹) ⊆
ℝ) |
32 | 31 | ssdifssd 4072 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (ran ((ℝ ×
{𝐴}) ∘f
· 𝐹) ∖ {0})
⊆ ℝ) |
33 | 32 | sselda 3916 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})) →
𝑚 ∈
ℝ) |
34 | 33 | recnd 10886 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})) →
𝑚 ∈
ℂ) |
35 | 8 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → 𝐴 ∈ ℝ) |
36 | 35 | recnd 10886 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → 𝐴 ∈ ℂ) |
37 | 36 | adantr 484 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})) →
𝐴 ∈
ℂ) |
38 | | simplr 769 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})) →
𝐴 ≠ 0) |
39 | 34, 37, 38 | divcan2d 11635 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})) →
(𝐴 · (𝑚 / 𝐴)) = 𝑚) |
40 | 4, 8 | i1fmulclem 24624 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℝ) → (◡((ℝ × {𝐴}) ∘f · 𝐹) “ {𝑚}) = (◡𝐹 “ {(𝑚 / 𝐴)})) |
41 | 33, 40 | syldan 594 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})) →
(◡((ℝ × {𝐴}) ∘f · 𝐹) “ {𝑚}) = (◡𝐹 “ {(𝑚 / 𝐴)})) |
42 | 41 | fveq2d 6740 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})) →
(vol‘(◡((ℝ × {𝐴}) ∘f ·
𝐹) “ {𝑚})) = (vol‘(◡𝐹 “ {(𝑚 / 𝐴)}))) |
43 | 42 | eqcomd 2744 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})) →
(vol‘(◡𝐹 “ {(𝑚 / 𝐴)})) = (vol‘(◡((ℝ × {𝐴}) ∘f · 𝐹) “ {𝑚}))) |
44 | 39, 43 | oveq12d 7250 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})) →
((𝐴 · (𝑚 / 𝐴)) · (vol‘(◡𝐹 “ {(𝑚 / 𝐴)}))) = (𝑚 · (vol‘(◡((ℝ × {𝐴}) ∘f · 𝐹) “ {𝑚})))) |
45 | 8 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})) →
𝐴 ∈
ℝ) |
46 | 33, 45, 38 | redivcld 11685 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})) →
(𝑚 / 𝐴) ∈ ℝ) |
47 | 46 | recnd 10886 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})) →
(𝑚 / 𝐴) ∈ ℂ) |
48 | 4 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})) →
𝐹 ∈ dom
∫1) |
49 | 45 | recnd 10886 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})) →
𝐴 ∈
ℂ) |
50 | | eldifsni 4718 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ (ran ((ℝ ×
{𝐴}) ∘f
· 𝐹) ∖ {0})
→ 𝑚 ≠
0) |
51 | 50 | adantl 485 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})) →
𝑚 ≠ 0) |
52 | 34, 49, 51, 38 | divne0d 11649 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})) →
(𝑚 / 𝐴) ≠ 0) |
53 | | eldifsn 4715 |
. . . . . . . . . 10
⊢ ((𝑚 / 𝐴) ∈ (ℝ ∖ {0}) ↔
((𝑚 / 𝐴) ∈ ℝ ∧ (𝑚 / 𝐴) ≠ 0)) |
54 | 46, 52, 53 | sylanbrc 586 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})) →
(𝑚 / 𝐴) ∈ (ℝ ∖
{0})) |
55 | | i1fima2sn 24601 |
. . . . . . . . 9
⊢ ((𝐹 ∈ dom ∫1
∧ (𝑚 / 𝐴) ∈ (ℝ ∖ {0}))
→ (vol‘(◡𝐹 “ {(𝑚 / 𝐴)})) ∈ ℝ) |
56 | 48, 54, 55 | syl2anc 587 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})) →
(vol‘(◡𝐹 “ {(𝑚 / 𝐴)})) ∈ ℝ) |
57 | 56 | recnd 10886 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})) →
(vol‘(◡𝐹 “ {(𝑚 / 𝐴)})) ∈ ℂ) |
58 | 37, 47, 57 | mulassd 10881 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})) →
((𝐴 · (𝑚 / 𝐴)) · (vol‘(◡𝐹 “ {(𝑚 / 𝐴)}))) = (𝐴 · ((𝑚 / 𝐴) · (vol‘(◡𝐹 “ {(𝑚 / 𝐴)}))))) |
59 | 44, 58 | eqtr3d 2780 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})) →
(𝑚 ·
(vol‘(◡((ℝ × {𝐴}) ∘f ·
𝐹) “ {𝑚}))) = (𝐴 · ((𝑚 / 𝐴) · (vol‘(◡𝐹 “ {(𝑚 / 𝐴)}))))) |
60 | 59 | sumeq2dv 15292 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → Σ𝑚 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})(𝑚 · (vol‘(◡((ℝ × {𝐴}) ∘f · 𝐹) “ {𝑚}))) = Σ𝑚 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})(𝐴 · ((𝑚 / 𝐴) · (vol‘(◡𝐹 “ {(𝑚 / 𝐴)}))))) |
61 | | i1frn 24598 |
. . . . . . 7
⊢
(((ℝ × {𝐴}) ∘f · 𝐹) ∈ dom ∫1
→ ran ((ℝ × {𝐴}) ∘f · 𝐹) ∈ Fin) |
62 | 28, 61 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∈
Fin) |
63 | | difss 4061 |
. . . . . 6
⊢ (ran
((ℝ × {𝐴})
∘f · 𝐹) ∖ {0}) ⊆ ran ((ℝ ×
{𝐴}) ∘f
· 𝐹) |
64 | | ssfi 8874 |
. . . . . 6
⊢ ((ran
((ℝ × {𝐴})
∘f · 𝐹) ∈ Fin ∧ (ran ((ℝ ×
{𝐴}) ∘f
· 𝐹) ∖ {0})
⊆ ran ((ℝ × {𝐴}) ∘f · 𝐹)) → (ran ((ℝ ×
{𝐴}) ∘f
· 𝐹) ∖ {0})
∈ Fin) |
65 | 62, 63, 64 | sylancl 589 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (ran ((ℝ ×
{𝐴}) ∘f
· 𝐹) ∖ {0})
∈ Fin) |
66 | 47, 57 | mulcld 10878 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})) →
((𝑚 / 𝐴) · (vol‘(◡𝐹 “ {(𝑚 / 𝐴)}))) ∈ ℂ) |
67 | 65, 36, 66 | fsummulc2 15373 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (𝐴 · Σ𝑚 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})((𝑚 / 𝐴) · (vol‘(◡𝐹 “ {(𝑚 / 𝐴)})))) = Σ𝑚 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})(𝐴 · ((𝑚 / 𝐴) · (vol‘(◡𝐹 “ {(𝑚 / 𝐴)}))))) |
68 | 60, 67 | eqtr4d 2781 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → Σ𝑚 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})(𝑚 · (vol‘(◡((ℝ × {𝐴}) ∘f · 𝐹) “ {𝑚}))) = (𝐴 · Σ𝑚 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})((𝑚 / 𝐴) · (vol‘(◡𝐹 “ {(𝑚 / 𝐴)}))))) |
69 | | itg1val 24604 |
. . . 4
⊢
(((ℝ × {𝐴}) ∘f · 𝐹) ∈ dom ∫1
→ (∫1‘((ℝ × {𝐴}) ∘f · 𝐹)) = Σ𝑚 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})(𝑚 · (vol‘(◡((ℝ × {𝐴}) ∘f · 𝐹) “ {𝑚})))) |
70 | 28, 69 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ≠ 0) →
(∫1‘((ℝ × {𝐴}) ∘f · 𝐹)) = Σ𝑚 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})(𝑚 · (vol‘(◡((ℝ × {𝐴}) ∘f · 𝐹) “ {𝑚})))) |
71 | 4 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → 𝐹 ∈ dom
∫1) |
72 | | itg1val 24604 |
. . . . . 6
⊢ (𝐹 ∈ dom ∫1
→ (∫1‘𝐹) = Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘(◡𝐹 “ {𝑘})))) |
73 | 71, 72 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ≠ 0) →
(∫1‘𝐹)
= Σ𝑘 ∈ (ran
𝐹 ∖ {0})(𝑘 · (vol‘(◡𝐹 “ {𝑘})))) |
74 | | id 22 |
. . . . . . 7
⊢ (𝑘 = (𝑚 / 𝐴) → 𝑘 = (𝑚 / 𝐴)) |
75 | | sneq 4566 |
. . . . . . . . 9
⊢ (𝑘 = (𝑚 / 𝐴) → {𝑘} = {(𝑚 / 𝐴)}) |
76 | 75 | imaeq2d 5944 |
. . . . . . . 8
⊢ (𝑘 = (𝑚 / 𝐴) → (◡𝐹 “ {𝑘}) = (◡𝐹 “ {(𝑚 / 𝐴)})) |
77 | 76 | fveq2d 6740 |
. . . . . . 7
⊢ (𝑘 = (𝑚 / 𝐴) → (vol‘(◡𝐹 “ {𝑘})) = (vol‘(◡𝐹 “ {(𝑚 / 𝐴)}))) |
78 | 74, 77 | oveq12d 7250 |
. . . . . 6
⊢ (𝑘 = (𝑚 / 𝐴) → (𝑘 · (vol‘(◡𝐹 “ {𝑘}))) = ((𝑚 / 𝐴) · (vol‘(◡𝐹 “ {(𝑚 / 𝐴)})))) |
79 | | eqid 2738 |
. . . . . . 7
⊢ (𝑛 ∈ (ran ((ℝ ×
{𝐴}) ∘f
· 𝐹) ∖ {0})
↦ (𝑛 / 𝐴)) = (𝑛 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0}) ↦
(𝑛 / 𝐴)) |
80 | | eldifi 4056 |
. . . . . . . . 9
⊢ (𝑛 ∈ (ran ((ℝ ×
{𝐴}) ∘f
· 𝐹) ∖ {0})
→ 𝑛 ∈ ran
((ℝ × {𝐴})
∘f · 𝐹)) |
81 | 2 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ℝ ∈
V) |
82 | 6 | ffnd 6565 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐹 Fn ℝ) |
83 | | eqidd 2739 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐹‘𝑦) = (𝐹‘𝑦)) |
84 | 81, 8, 82, 83 | ofc1 7513 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (((ℝ ×
{𝐴}) ∘f
· 𝐹)‘𝑦) = (𝐴 · (𝐹‘𝑦))) |
85 | 84 | adantlr 715 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ ℝ) → (((ℝ ×
{𝐴}) ∘f
· 𝐹)‘𝑦) = (𝐴 · (𝐹‘𝑦))) |
86 | 85 | oveq1d 7247 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ ℝ) → ((((ℝ ×
{𝐴}) ∘f
· 𝐹)‘𝑦) / 𝐴) = ((𝐴 · (𝐹‘𝑦)) / 𝐴)) |
87 | 6 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → 𝐹:ℝ⟶ℝ) |
88 | 87 | ffvelrnda 6923 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ ℝ) → (𝐹‘𝑦) ∈ ℝ) |
89 | 88 | recnd 10886 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ ℝ) → (𝐹‘𝑦) ∈ ℂ) |
90 | 36 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ ℝ) → 𝐴 ∈ ℂ) |
91 | | simplr 769 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ ℝ) → 𝐴 ≠ 0) |
92 | 89, 90, 91 | divcan3d 11638 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ ℝ) → ((𝐴 · (𝐹‘𝑦)) / 𝐴) = (𝐹‘𝑦)) |
93 | 86, 92 | eqtrd 2778 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ ℝ) → ((((ℝ ×
{𝐴}) ∘f
· 𝐹)‘𝑦) / 𝐴) = (𝐹‘𝑦)) |
94 | 87 | ffnd 6565 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → 𝐹 Fn ℝ) |
95 | | fnfvelrn 6920 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 Fn ℝ ∧ 𝑦 ∈ ℝ) → (𝐹‘𝑦) ∈ ran 𝐹) |
96 | 94, 95 | sylan 583 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ ℝ) → (𝐹‘𝑦) ∈ ran 𝐹) |
97 | 93, 96 | eqeltrd 2839 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ ℝ) → ((((ℝ ×
{𝐴}) ∘f
· 𝐹)‘𝑦) / 𝐴) ∈ ran 𝐹) |
98 | 97 | ralrimiva 3106 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ∀𝑦 ∈ ℝ ((((ℝ × {𝐴}) ∘f ·
𝐹)‘𝑦) / 𝐴) ∈ ran 𝐹) |
99 | 30 | ffnd 6565 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ((ℝ × {𝐴}) ∘f ·
𝐹) Fn
ℝ) |
100 | | oveq1 7239 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = (((ℝ × {𝐴}) ∘f ·
𝐹)‘𝑦) → (𝑛 / 𝐴) = ((((ℝ × {𝐴}) ∘f · 𝐹)‘𝑦) / 𝐴)) |
101 | 100 | eleq1d 2823 |
. . . . . . . . . . . . 13
⊢ (𝑛 = (((ℝ × {𝐴}) ∘f ·
𝐹)‘𝑦) → ((𝑛 / 𝐴) ∈ ran 𝐹 ↔ ((((ℝ × {𝐴}) ∘f ·
𝐹)‘𝑦) / 𝐴) ∈ ran 𝐹)) |
102 | 101 | ralrn 6926 |
. . . . . . . . . . . 12
⊢
(((ℝ × {𝐴}) ∘f · 𝐹) Fn ℝ →
(∀𝑛 ∈ ran
((ℝ × {𝐴})
∘f · 𝐹)(𝑛 / 𝐴) ∈ ran 𝐹 ↔ ∀𝑦 ∈ ℝ ((((ℝ × {𝐴}) ∘f ·
𝐹)‘𝑦) / 𝐴) ∈ ran 𝐹)) |
103 | 99, 102 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (∀𝑛 ∈ ran ((ℝ × {𝐴}) ∘f ·
𝐹)(𝑛 / 𝐴) ∈ ran 𝐹 ↔ ∀𝑦 ∈ ℝ ((((ℝ × {𝐴}) ∘f ·
𝐹)‘𝑦) / 𝐴) ∈ ran 𝐹)) |
104 | 98, 103 | mpbird 260 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ∀𝑛 ∈ ran ((ℝ × {𝐴}) ∘f ·
𝐹)(𝑛 / 𝐴) ∈ ran 𝐹) |
105 | 104 | r19.21bi 3131 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑛 ∈ ran ((ℝ × {𝐴}) ∘f ·
𝐹)) → (𝑛 / 𝐴) ∈ ran 𝐹) |
106 | 80, 105 | sylan2 596 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑛 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})) →
(𝑛 / 𝐴) ∈ ran 𝐹) |
107 | 32 | sselda 3916 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑛 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})) →
𝑛 ∈
ℝ) |
108 | 107 | recnd 10886 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑛 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})) →
𝑛 ∈
ℂ) |
109 | 36 | adantr 484 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑛 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})) →
𝐴 ∈
ℂ) |
110 | | eldifsni 4718 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (ran ((ℝ ×
{𝐴}) ∘f
· 𝐹) ∖ {0})
→ 𝑛 ≠
0) |
111 | 110 | adantl 485 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑛 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})) →
𝑛 ≠ 0) |
112 | | simplr 769 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑛 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})) →
𝐴 ≠ 0) |
113 | 108, 109,
111, 112 | divne0d 11649 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑛 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})) →
(𝑛 / 𝐴) ≠ 0) |
114 | | eldifsn 4715 |
. . . . . . . 8
⊢ ((𝑛 / 𝐴) ∈ (ran 𝐹 ∖ {0}) ↔ ((𝑛 / 𝐴) ∈ ran 𝐹 ∧ (𝑛 / 𝐴) ≠ 0)) |
115 | 106, 113,
114 | sylanbrc 586 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑛 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})) →
(𝑛 / 𝐴) ∈ (ran 𝐹 ∖ {0})) |
116 | | eldifi 4056 |
. . . . . . . . 9
⊢ (𝑘 ∈ (ran 𝐹 ∖ {0}) → 𝑘 ∈ ran 𝐹) |
117 | | fnfvelrn 6920 |
. . . . . . . . . . . . . 14
⊢
((((ℝ × {𝐴}) ∘f · 𝐹) Fn ℝ ∧ 𝑦 ∈ ℝ) →
(((ℝ × {𝐴})
∘f · 𝐹)‘𝑦) ∈ ran ((ℝ × {𝐴}) ∘f ·
𝐹)) |
118 | 99, 117 | sylan 583 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ ℝ) → (((ℝ ×
{𝐴}) ∘f
· 𝐹)‘𝑦) ∈ ran ((ℝ ×
{𝐴}) ∘f
· 𝐹)) |
119 | 85, 118 | eqeltrrd 2840 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ ℝ) → (𝐴 · (𝐹‘𝑦)) ∈ ran ((ℝ × {𝐴}) ∘f ·
𝐹)) |
120 | 119 | ralrimiva 3106 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ∀𝑦 ∈ ℝ (𝐴 · (𝐹‘𝑦)) ∈ ran ((ℝ × {𝐴}) ∘f ·
𝐹)) |
121 | | oveq2 7240 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = (𝐹‘𝑦) → (𝐴 · 𝑘) = (𝐴 · (𝐹‘𝑦))) |
122 | 121 | eleq1d 2823 |
. . . . . . . . . . . . 13
⊢ (𝑘 = (𝐹‘𝑦) → ((𝐴 · 𝑘) ∈ ran ((ℝ × {𝐴}) ∘f ·
𝐹) ↔ (𝐴 · (𝐹‘𝑦)) ∈ ran ((ℝ × {𝐴}) ∘f ·
𝐹))) |
123 | 122 | ralrn 6926 |
. . . . . . . . . . . 12
⊢ (𝐹 Fn ℝ →
(∀𝑘 ∈ ran 𝐹(𝐴 · 𝑘) ∈ ran ((ℝ × {𝐴}) ∘f ·
𝐹) ↔ ∀𝑦 ∈ ℝ (𝐴 · (𝐹‘𝑦)) ∈ ran ((ℝ × {𝐴}) ∘f ·
𝐹))) |
124 | 94, 123 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (∀𝑘 ∈ ran 𝐹(𝐴 · 𝑘) ∈ ran ((ℝ × {𝐴}) ∘f ·
𝐹) ↔ ∀𝑦 ∈ ℝ (𝐴 · (𝐹‘𝑦)) ∈ ran ((ℝ × {𝐴}) ∘f ·
𝐹))) |
125 | 120, 124 | mpbird 260 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ∀𝑘 ∈ ran 𝐹(𝐴 · 𝑘) ∈ ran ((ℝ × {𝐴}) ∘f ·
𝐹)) |
126 | 125 | r19.21bi 3131 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑘 ∈ ran 𝐹) → (𝐴 · 𝑘) ∈ ran ((ℝ × {𝐴}) ∘f ·
𝐹)) |
127 | 116, 126 | sylan2 596 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝐴 · 𝑘) ∈ ran ((ℝ × {𝐴}) ∘f ·
𝐹)) |
128 | 36 | adantr 484 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → 𝐴 ∈ ℂ) |
129 | 87 | frnd 6572 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ran 𝐹 ⊆ ℝ) |
130 | 129 | ssdifssd 4072 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (ran 𝐹 ∖ {0}) ⊆
ℝ) |
131 | 130 | sselda 3916 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → 𝑘 ∈ ℝ) |
132 | 131 | recnd 10886 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → 𝑘 ∈ ℂ) |
133 | | simplr 769 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → 𝐴 ≠ 0) |
134 | | eldifsni 4718 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (ran 𝐹 ∖ {0}) → 𝑘 ≠ 0) |
135 | 134 | adantl 485 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → 𝑘 ≠ 0) |
136 | 128, 132,
133, 135 | mulne0d 11509 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝐴 · 𝑘) ≠ 0) |
137 | | eldifsn 4715 |
. . . . . . . 8
⊢ ((𝐴 · 𝑘) ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0}) ↔
((𝐴 · 𝑘) ∈ ran ((ℝ ×
{𝐴}) ∘f
· 𝐹) ∧ (𝐴 · 𝑘) ≠ 0)) |
138 | 127, 136,
137 | sylanbrc 586 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝐴 · 𝑘) ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖
{0})) |
139 | | simpl 486 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ (ran ((ℝ ×
{𝐴}) ∘f
· 𝐹) ∖ {0})
∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → 𝑛 ∈ (ran ((ℝ ×
{𝐴}) ∘f
· 𝐹) ∖
{0})) |
140 | | ssel2 3910 |
. . . . . . . . . . . 12
⊢ (((ran
((ℝ × {𝐴})
∘f · 𝐹) ∖ {0}) ⊆ ℝ ∧ 𝑛 ∈ (ran ((ℝ ×
{𝐴}) ∘f
· 𝐹) ∖ {0}))
→ 𝑛 ∈
ℝ) |
141 | 32, 139, 140 | syl2an 599 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ (𝑛 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0}) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0}))) → 𝑛 ∈ ℝ) |
142 | 141 | recnd 10886 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ (𝑛 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0}) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0}))) → 𝑛 ∈ ℂ) |
143 | 8 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ (𝑛 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0}) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0}))) → 𝐴 ∈ ℝ) |
144 | 143 | recnd 10886 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ (𝑛 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0}) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0}))) → 𝐴 ∈ ℂ) |
145 | 131 | adantrl 716 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ (𝑛 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0}) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0}))) → 𝑘 ∈ ℝ) |
146 | 145 | recnd 10886 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ (𝑛 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0}) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0}))) → 𝑘 ∈ ℂ) |
147 | | simplr 769 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ (𝑛 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0}) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0}))) → 𝐴 ≠ 0) |
148 | 142, 144,
146, 147 | divmuld 11655 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ (𝑛 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0}) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0}))) → ((𝑛 / 𝐴) = 𝑘 ↔ (𝐴 · 𝑘) = 𝑛)) |
149 | 148 | bicomd 226 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ (𝑛 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0}) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0}))) → ((𝐴 · 𝑘) = 𝑛 ↔ (𝑛 / 𝐴) = 𝑘)) |
150 | | eqcom 2745 |
. . . . . . . 8
⊢ (𝑛 = (𝐴 · 𝑘) ↔ (𝐴 · 𝑘) = 𝑛) |
151 | | eqcom 2745 |
. . . . . . . 8
⊢ (𝑘 = (𝑛 / 𝐴) ↔ (𝑛 / 𝐴) = 𝑘) |
152 | 149, 150,
151 | 3bitr4g 317 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ (𝑛 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0}) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0}))) → (𝑛 = (𝐴 · 𝑘) ↔ 𝑘 = (𝑛 / 𝐴))) |
153 | 79, 115, 138, 152 | f1o2d 7478 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (𝑛 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0}) ↦
(𝑛 / 𝐴)):(ran ((ℝ × {𝐴}) ∘f · 𝐹) ∖ {0})–1-1-onto→(ran 𝐹 ∖ {0})) |
154 | | oveq1 7239 |
. . . . . . . 8
⊢ (𝑛 = 𝑚 → (𝑛 / 𝐴) = (𝑚 / 𝐴)) |
155 | | ovex 7265 |
. . . . . . . 8
⊢ (𝑚 / 𝐴) ∈ V |
156 | 154, 79, 155 | fvmpt 6837 |
. . . . . . 7
⊢ (𝑚 ∈ (ran ((ℝ ×
{𝐴}) ∘f
· 𝐹) ∖ {0})
→ ((𝑛 ∈ (ran
((ℝ × {𝐴})
∘f · 𝐹) ∖ {0}) ↦ (𝑛 / 𝐴))‘𝑚) = (𝑚 / 𝐴)) |
157 | 156 | adantl 485 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})) →
((𝑛 ∈ (ran ((ℝ
× {𝐴})
∘f · 𝐹) ∖ {0}) ↦ (𝑛 / 𝐴))‘𝑚) = (𝑚 / 𝐴)) |
158 | | i1fima2sn 24601 |
. . . . . . . . 9
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) →
(vol‘(◡𝐹 “ {𝑘})) ∈ ℝ) |
159 | 71, 158 | sylan 583 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (vol‘(◡𝐹 “ {𝑘})) ∈ ℝ) |
160 | 131, 159 | remulcld 10888 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑘 · (vol‘(◡𝐹 “ {𝑘}))) ∈ ℝ) |
161 | 160 | recnd 10886 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑘 · (vol‘(◡𝐹 “ {𝑘}))) ∈ ℂ) |
162 | 78, 65, 153, 157, 161 | fsumf1o 15312 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘(◡𝐹 “ {𝑘}))) = Σ𝑚 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})((𝑚 / 𝐴) · (vol‘(◡𝐹 “ {(𝑚 / 𝐴)})))) |
163 | 73, 162 | eqtrd 2778 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ≠ 0) →
(∫1‘𝐹)
= Σ𝑚 ∈ (ran
((ℝ × {𝐴})
∘f · 𝐹) ∖ {0})((𝑚 / 𝐴) · (vol‘(◡𝐹 “ {(𝑚 / 𝐴)})))) |
164 | 163 | oveq2d 7248 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (𝐴 · (∫1‘𝐹)) = (𝐴 · Σ𝑚 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})((𝑚 / 𝐴) · (vol‘(◡𝐹 “ {(𝑚 / 𝐴)}))))) |
165 | 68, 70, 164 | 3eqtr4d 2788 |
. 2
⊢ ((𝜑 ∧ 𝐴 ≠ 0) →
(∫1‘((ℝ × {𝐴}) ∘f · 𝐹)) = (𝐴 · (∫1‘𝐹))) |
166 | 26, 165 | pm2.61dane 3030 |
1
⊢ (𝜑 →
(∫1‘((ℝ × {𝐴}) ∘f · 𝐹)) = (𝐴 · (∫1‘𝐹))) |