Step | Hyp | Ref
| Expression |
1 | | remulcl 10021 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 · 𝑦) ∈ ℝ) |
2 | 1 | adantl 482 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑥 · 𝑦) ∈ ℝ) |
3 | | mbfmulc2re.2 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ ℝ) |
4 | | fconst6g 6094 |
. . . . . 6
⊢ (𝐵 ∈ ℝ → (𝐴 × {𝐵}):𝐴⟶ℝ) |
5 | 3, 4 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝐴 × {𝐵}):𝐴⟶ℝ) |
6 | | mbfmulc2lem.3 |
. . . . 5
⊢ (𝜑 → 𝐹:𝐴⟶ℝ) |
7 | | fdm 6051 |
. . . . . . 7
⊢ (𝐹:𝐴⟶ℝ → dom 𝐹 = 𝐴) |
8 | 6, 7 | syl 17 |
. . . . . 6
⊢ (𝜑 → dom 𝐹 = 𝐴) |
9 | | mbfmulc2re.1 |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈ MblFn) |
10 | | mbfdm 23395 |
. . . . . . 7
⊢ (𝐹 ∈ MblFn → dom 𝐹 ∈ dom
vol) |
11 | 9, 10 | syl 17 |
. . . . . 6
⊢ (𝜑 → dom 𝐹 ∈ dom vol) |
12 | 8, 11 | eqeltrrd 2702 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ dom vol) |
13 | | inidm 3822 |
. . . . 5
⊢ (𝐴 ∩ 𝐴) = 𝐴 |
14 | 2, 5, 6, 12, 12, 13 | off 6912 |
. . . 4
⊢ (𝜑 → ((𝐴 × {𝐵}) ∘𝑓 ·
𝐹):𝐴⟶ℝ) |
15 | 14 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ 𝐵 < 0) → ((𝐴 × {𝐵}) ∘𝑓 ·
𝐹):𝐴⟶ℝ) |
16 | 12 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ 𝐵 < 0) → 𝐴 ∈ dom vol) |
17 | | simprl 794 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → 𝑦 ∈ ℝ) |
18 | 17 | rexrd 10089 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → 𝑦 ∈ ℝ*) |
19 | | elioopnf 12267 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℝ*
→ ((((𝐴 × {𝐵}) ∘𝑓
· 𝐹)‘𝑧) ∈ (𝑦(,)+∞) ↔ ((((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧) ∈ ℝ ∧ 𝑦 < (((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧)))) |
20 | 18, 19 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → ((((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧) ∈ (𝑦(,)+∞) ↔ ((((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧) ∈ ℝ ∧ 𝑦 < (((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧)))) |
21 | 14 | ffvelrnda 6359 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧) ∈ ℝ) |
22 | 21 | ad2ant2rl 785 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → (((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧) ∈ ℝ) |
23 | 22 | biantrurd 529 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → (𝑦 < (((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧) ↔ ((((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧) ∈ ℝ ∧ 𝑦 < (((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧)))) |
24 | 6 | ffvelrnda 6359 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ ℝ) |
25 | 24 | ad2ant2rl 785 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → (𝐹‘𝑧) ∈ ℝ) |
26 | 25 | biantrurd 529 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → ((𝐹‘𝑧) < (𝑦 / 𝐵) ↔ ((𝐹‘𝑧) ∈ ℝ ∧ (𝐹‘𝑧) < (𝑦 / 𝐵)))) |
27 | | simprr 796 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → 𝑧 ∈ 𝐴) |
28 | 12 | ad2antrr 762 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → 𝐴 ∈ dom vol) |
29 | 3 | ad2antrr 762 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → 𝐵 ∈ ℝ) |
30 | 6 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → 𝐹:𝐴⟶ℝ) |
31 | | ffn 6045 |
. . . . . . . . . . . . . . 15
⊢ (𝐹:𝐴⟶ℝ → 𝐹 Fn 𝐴) |
32 | 30, 31 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → 𝐹 Fn 𝐴) |
33 | | eqidd 2623 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) = (𝐹‘𝑧)) |
34 | 28, 29, 32, 33 | ofc1 6920 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) ∧ 𝑧 ∈ 𝐴) → (((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧) = (𝐵 · (𝐹‘𝑧))) |
35 | 27, 34 | mpdan 702 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → (((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧) = (𝐵 · (𝐹‘𝑧))) |
36 | 35 | breq2d 4665 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → (𝑦 < (((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧) ↔ 𝑦 < (𝐵 · (𝐹‘𝑧)))) |
37 | 17 | renegcld 10457 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → -𝑦 ∈ ℝ) |
38 | 29 | renegcld 10457 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → -𝐵 ∈ ℝ) |
39 | | simplr 792 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → 𝐵 < 0) |
40 | 29 | lt0neg1d 10597 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → (𝐵 < 0 ↔ 0 < -𝐵)) |
41 | 39, 40 | mpbid 222 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → 0 < -𝐵) |
42 | | ltmuldiv2 10897 |
. . . . . . . . . . . . 13
⊢ (((𝐹‘𝑧) ∈ ℝ ∧ -𝑦 ∈ ℝ ∧ (-𝐵 ∈ ℝ ∧ 0 < -𝐵)) → ((-𝐵 · (𝐹‘𝑧)) < -𝑦 ↔ (𝐹‘𝑧) < (-𝑦 / -𝐵))) |
43 | 25, 37, 38, 41, 42 | syl112anc 1330 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → ((-𝐵 · (𝐹‘𝑧)) < -𝑦 ↔ (𝐹‘𝑧) < (-𝑦 / -𝐵))) |
44 | 29 | recnd 10068 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → 𝐵 ∈ ℂ) |
45 | 25 | recnd 10068 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → (𝐹‘𝑧) ∈ ℂ) |
46 | 44, 45 | mulneg1d 10483 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → (-𝐵 · (𝐹‘𝑧)) = -(𝐵 · (𝐹‘𝑧))) |
47 | 46 | breq1d 4663 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → ((-𝐵 · (𝐹‘𝑧)) < -𝑦 ↔ -(𝐵 · (𝐹‘𝑧)) < -𝑦)) |
48 | 35, 22 | eqeltrrd 2702 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → (𝐵 · (𝐹‘𝑧)) ∈ ℝ) |
49 | 17, 48 | ltnegd 10605 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → (𝑦 < (𝐵 · (𝐹‘𝑧)) ↔ -(𝐵 · (𝐹‘𝑧)) < -𝑦)) |
50 | 47, 49 | bitr4d 271 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → ((-𝐵 · (𝐹‘𝑧)) < -𝑦 ↔ 𝑦 < (𝐵 · (𝐹‘𝑧)))) |
51 | 43, 50 | bitr3d 270 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → ((𝐹‘𝑧) < (-𝑦 / -𝐵) ↔ 𝑦 < (𝐵 · (𝐹‘𝑧)))) |
52 | 17 | recnd 10068 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → 𝑦 ∈ ℂ) |
53 | 39 | lt0ne0d 10593 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → 𝐵 ≠ 0) |
54 | 52, 44, 53 | div2negd 10816 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → (-𝑦 / -𝐵) = (𝑦 / 𝐵)) |
55 | 54 | breq2d 4665 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → ((𝐹‘𝑧) < (-𝑦 / -𝐵) ↔ (𝐹‘𝑧) < (𝑦 / 𝐵))) |
56 | 36, 51, 55 | 3bitr2d 296 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → (𝑦 < (((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧) ↔ (𝐹‘𝑧) < (𝑦 / 𝐵))) |
57 | 17, 29, 53 | redivcld 10853 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → (𝑦 / 𝐵) ∈ ℝ) |
58 | 57 | rexrd 10089 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → (𝑦 / 𝐵) ∈
ℝ*) |
59 | | elioomnf 12268 |
. . . . . . . . . . 11
⊢ ((𝑦 / 𝐵) ∈ ℝ* → ((𝐹‘𝑧) ∈ (-∞(,)(𝑦 / 𝐵)) ↔ ((𝐹‘𝑧) ∈ ℝ ∧ (𝐹‘𝑧) < (𝑦 / 𝐵)))) |
60 | 58, 59 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → ((𝐹‘𝑧) ∈ (-∞(,)(𝑦 / 𝐵)) ↔ ((𝐹‘𝑧) ∈ ℝ ∧ (𝐹‘𝑧) < (𝑦 / 𝐵)))) |
61 | 26, 56, 60 | 3bitr4d 300 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → (𝑦 < (((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧) ↔ (𝐹‘𝑧) ∈ (-∞(,)(𝑦 / 𝐵)))) |
62 | 20, 23, 61 | 3bitr2d 296 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → ((((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧) ∈ (𝑦(,)+∞) ↔ (𝐹‘𝑧) ∈ (-∞(,)(𝑦 / 𝐵)))) |
63 | 62 | anassrs 680 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐵 < 0) ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → ((((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧) ∈ (𝑦(,)+∞) ↔ (𝐹‘𝑧) ∈ (-∞(,)(𝑦 / 𝐵)))) |
64 | 63 | pm5.32da 673 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ 𝑦 ∈ ℝ) → ((𝑧 ∈ 𝐴 ∧ (((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧) ∈ (𝑦(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (-∞(,)(𝑦 / 𝐵))))) |
65 | | ffn 6045 |
. . . . . . . . 9
⊢ (((𝐴 × {𝐵}) ∘𝑓 ·
𝐹):𝐴⟶ℝ → ((𝐴 × {𝐵}) ∘𝑓 ·
𝐹) Fn 𝐴) |
66 | 14, 65 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴 × {𝐵}) ∘𝑓 ·
𝐹) Fn 𝐴) |
67 | 66 | ad2antrr 762 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ 𝑦 ∈ ℝ) → ((𝐴 × {𝐵}) ∘𝑓 ·
𝐹) Fn 𝐴) |
68 | | elpreima 6337 |
. . . . . . 7
⊢ (((𝐴 × {𝐵}) ∘𝑓 ·
𝐹) Fn 𝐴 → (𝑧 ∈ (◡((𝐴 × {𝐵}) ∘𝑓 ·
𝐹) “ (𝑦(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧) ∈ (𝑦(,)+∞)))) |
69 | 67, 68 | syl 17 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ 𝑦 ∈ ℝ) → (𝑧 ∈ (◡((𝐴 × {𝐵}) ∘𝑓 ·
𝐹) “ (𝑦(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧) ∈ (𝑦(,)+∞)))) |
70 | 6, 31 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 Fn 𝐴) |
71 | 70 | ad2antrr 762 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ 𝑦 ∈ ℝ) → 𝐹 Fn 𝐴) |
72 | | elpreima 6337 |
. . . . . . 7
⊢ (𝐹 Fn 𝐴 → (𝑧 ∈ (◡𝐹 “ (-∞(,)(𝑦 / 𝐵))) ↔ (𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (-∞(,)(𝑦 / 𝐵))))) |
73 | 71, 72 | syl 17 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ 𝑦 ∈ ℝ) → (𝑧 ∈ (◡𝐹 “ (-∞(,)(𝑦 / 𝐵))) ↔ (𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (-∞(,)(𝑦 / 𝐵))))) |
74 | 64, 69, 73 | 3bitr4d 300 |
. . . . 5
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ 𝑦 ∈ ℝ) → (𝑧 ∈ (◡((𝐴 × {𝐵}) ∘𝑓 ·
𝐹) “ (𝑦(,)+∞)) ↔ 𝑧 ∈ (◡𝐹 “ (-∞(,)(𝑦 / 𝐵))))) |
75 | 74 | eqrdv 2620 |
. . . 4
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ 𝑦 ∈ ℝ) → (◡((𝐴 × {𝐵}) ∘𝑓 ·
𝐹) “ (𝑦(,)+∞)) = (◡𝐹 “ (-∞(,)(𝑦 / 𝐵)))) |
76 | | mbfima 23399 |
. . . . . 6
⊢ ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶ℝ) → (◡𝐹 “ (-∞(,)(𝑦 / 𝐵))) ∈ dom vol) |
77 | 9, 6, 76 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → (◡𝐹 “ (-∞(,)(𝑦 / 𝐵))) ∈ dom vol) |
78 | 77 | ad2antrr 762 |
. . . 4
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ 𝑦 ∈ ℝ) → (◡𝐹 “ (-∞(,)(𝑦 / 𝐵))) ∈ dom vol) |
79 | 75, 78 | eqeltrd 2701 |
. . 3
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ 𝑦 ∈ ℝ) → (◡((𝐴 × {𝐵}) ∘𝑓 ·
𝐹) “ (𝑦(,)+∞)) ∈ dom
vol) |
80 | | elioomnf 12268 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℝ*
→ ((((𝐴 × {𝐵}) ∘𝑓
· 𝐹)‘𝑧) ∈ (-∞(,)𝑦) ↔ ((((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧) ∈ ℝ ∧ (((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧) < 𝑦))) |
81 | 18, 80 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → ((((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧) ∈ (-∞(,)𝑦) ↔ ((((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧) ∈ ℝ ∧ (((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧) < 𝑦))) |
82 | 22 | biantrurd 529 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → ((((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧) < 𝑦 ↔ ((((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧) ∈ ℝ ∧ (((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧) < 𝑦))) |
83 | 25 | biantrurd 529 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → ((𝑦 / 𝐵) < (𝐹‘𝑧) ↔ ((𝐹‘𝑧) ∈ ℝ ∧ (𝑦 / 𝐵) < (𝐹‘𝑧)))) |
84 | 35 | breq1d 4663 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → ((((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧) < 𝑦 ↔ (𝐵 · (𝐹‘𝑧)) < 𝑦)) |
85 | 46 | breq2d 4665 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → (-𝑦 < (-𝐵 · (𝐹‘𝑧)) ↔ -𝑦 < -(𝐵 · (𝐹‘𝑧)))) |
86 | 54 | breq1d 4663 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → ((-𝑦 / -𝐵) < (𝐹‘𝑧) ↔ (𝑦 / 𝐵) < (𝐹‘𝑧))) |
87 | | ltdivmul 10898 |
. . . . . . . . . . . . . 14
⊢ ((-𝑦 ∈ ℝ ∧ (𝐹‘𝑧) ∈ ℝ ∧ (-𝐵 ∈ ℝ ∧ 0 < -𝐵)) → ((-𝑦 / -𝐵) < (𝐹‘𝑧) ↔ -𝑦 < (-𝐵 · (𝐹‘𝑧)))) |
88 | 37, 25, 38, 41, 87 | syl112anc 1330 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → ((-𝑦 / -𝐵) < (𝐹‘𝑧) ↔ -𝑦 < (-𝐵 · (𝐹‘𝑧)))) |
89 | 86, 88 | bitr3d 270 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → ((𝑦 / 𝐵) < (𝐹‘𝑧) ↔ -𝑦 < (-𝐵 · (𝐹‘𝑧)))) |
90 | 48, 17 | ltnegd 10605 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → ((𝐵 · (𝐹‘𝑧)) < 𝑦 ↔ -𝑦 < -(𝐵 · (𝐹‘𝑧)))) |
91 | 85, 89, 90 | 3bitr4d 300 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → ((𝑦 / 𝐵) < (𝐹‘𝑧) ↔ (𝐵 · (𝐹‘𝑧)) < 𝑦)) |
92 | 84, 91 | bitr4d 271 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → ((((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧) < 𝑦 ↔ (𝑦 / 𝐵) < (𝐹‘𝑧))) |
93 | | elioopnf 12267 |
. . . . . . . . . . 11
⊢ ((𝑦 / 𝐵) ∈ ℝ* → ((𝐹‘𝑧) ∈ ((𝑦 / 𝐵)(,)+∞) ↔ ((𝐹‘𝑧) ∈ ℝ ∧ (𝑦 / 𝐵) < (𝐹‘𝑧)))) |
94 | 58, 93 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → ((𝐹‘𝑧) ∈ ((𝑦 / 𝐵)(,)+∞) ↔ ((𝐹‘𝑧) ∈ ℝ ∧ (𝑦 / 𝐵) < (𝐹‘𝑧)))) |
95 | 83, 92, 94 | 3bitr4d 300 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → ((((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧) < 𝑦 ↔ (𝐹‘𝑧) ∈ ((𝑦 / 𝐵)(,)+∞))) |
96 | 81, 82, 95 | 3bitr2d 296 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → ((((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧) ∈ (-∞(,)𝑦) ↔ (𝐹‘𝑧) ∈ ((𝑦 / 𝐵)(,)+∞))) |
97 | 96 | anassrs 680 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐵 < 0) ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → ((((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧) ∈ (-∞(,)𝑦) ↔ (𝐹‘𝑧) ∈ ((𝑦 / 𝐵)(,)+∞))) |
98 | 97 | pm5.32da 673 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ 𝑦 ∈ ℝ) → ((𝑧 ∈ 𝐴 ∧ (((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧) ∈ (-∞(,)𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ ((𝑦 / 𝐵)(,)+∞)))) |
99 | | elpreima 6337 |
. . . . . . 7
⊢ (((𝐴 × {𝐵}) ∘𝑓 ·
𝐹) Fn 𝐴 → (𝑧 ∈ (◡((𝐴 × {𝐵}) ∘𝑓 ·
𝐹) “
(-∞(,)𝑦)) ↔
(𝑧 ∈ 𝐴 ∧ (((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧) ∈ (-∞(,)𝑦)))) |
100 | 67, 99 | syl 17 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ 𝑦 ∈ ℝ) → (𝑧 ∈ (◡((𝐴 × {𝐵}) ∘𝑓 ·
𝐹) “
(-∞(,)𝑦)) ↔
(𝑧 ∈ 𝐴 ∧ (((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧) ∈ (-∞(,)𝑦)))) |
101 | | elpreima 6337 |
. . . . . . 7
⊢ (𝐹 Fn 𝐴 → (𝑧 ∈ (◡𝐹 “ ((𝑦 / 𝐵)(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ ((𝑦 / 𝐵)(,)+∞)))) |
102 | 71, 101 | syl 17 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ 𝑦 ∈ ℝ) → (𝑧 ∈ (◡𝐹 “ ((𝑦 / 𝐵)(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ ((𝑦 / 𝐵)(,)+∞)))) |
103 | 98, 100, 102 | 3bitr4d 300 |
. . . . 5
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ 𝑦 ∈ ℝ) → (𝑧 ∈ (◡((𝐴 × {𝐵}) ∘𝑓 ·
𝐹) “
(-∞(,)𝑦)) ↔
𝑧 ∈ (◡𝐹 “ ((𝑦 / 𝐵)(,)+∞)))) |
104 | 103 | eqrdv 2620 |
. . . 4
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ 𝑦 ∈ ℝ) → (◡((𝐴 × {𝐵}) ∘𝑓 ·
𝐹) “
(-∞(,)𝑦)) = (◡𝐹 “ ((𝑦 / 𝐵)(,)+∞))) |
105 | | mbfima 23399 |
. . . . . 6
⊢ ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶ℝ) → (◡𝐹 “ ((𝑦 / 𝐵)(,)+∞)) ∈ dom
vol) |
106 | 9, 6, 105 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → (◡𝐹 “ ((𝑦 / 𝐵)(,)+∞)) ∈ dom
vol) |
107 | 106 | ad2antrr 762 |
. . . 4
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ 𝑦 ∈ ℝ) → (◡𝐹 “ ((𝑦 / 𝐵)(,)+∞)) ∈ dom
vol) |
108 | 104, 107 | eqeltrd 2701 |
. . 3
⊢ (((𝜑 ∧ 𝐵 < 0) ∧ 𝑦 ∈ ℝ) → (◡((𝐴 × {𝐵}) ∘𝑓 ·
𝐹) “
(-∞(,)𝑦)) ∈ dom
vol) |
109 | 15, 16, 79, 108 | ismbf2d 23408 |
. 2
⊢ ((𝜑 ∧ 𝐵 < 0) → ((𝐴 × {𝐵}) ∘𝑓 ·
𝐹) ∈
MblFn) |
110 | 12 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 = 0) → 𝐴 ∈ dom vol) |
111 | 6 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 = 0) → 𝐹:𝐴⟶ℝ) |
112 | | simpr 477 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 = 0) → 𝐵 = 0) |
113 | | 0cn 10032 |
. . . . 5
⊢ 0 ∈
ℂ |
114 | 112, 113 | syl6eqel 2709 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 = 0) → 𝐵 ∈ ℂ) |
115 | | 0cnd 10033 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 = 0) → 0 ∈
ℂ) |
116 | | simplr 792 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵 = 0) ∧ 𝑥 ∈ ℝ) → 𝐵 = 0) |
117 | 116 | oveq1d 6665 |
. . . . 5
⊢ (((𝜑 ∧ 𝐵 = 0) ∧ 𝑥 ∈ ℝ) → (𝐵 · 𝑥) = (0 · 𝑥)) |
118 | | mul02lem2 10213 |
. . . . . 6
⊢ (𝑥 ∈ ℝ → (0
· 𝑥) =
0) |
119 | 118 | adantl 482 |
. . . . 5
⊢ (((𝜑 ∧ 𝐵 = 0) ∧ 𝑥 ∈ ℝ) → (0 · 𝑥) = 0) |
120 | 117, 119 | eqtrd 2656 |
. . . 4
⊢ (((𝜑 ∧ 𝐵 = 0) ∧ 𝑥 ∈ ℝ) → (𝐵 · 𝑥) = 0) |
121 | 110, 111,
114, 115, 120 | caofid2 6928 |
. . 3
⊢ ((𝜑 ∧ 𝐵 = 0) → ((𝐴 × {𝐵}) ∘𝑓 ·
𝐹) = (𝐴 × {0})) |
122 | | mbfconst 23402 |
. . . 4
⊢ ((𝐴 ∈ dom vol ∧ 0 ∈
ℂ) → (𝐴 ×
{0}) ∈ MblFn) |
123 | 110, 113,
122 | sylancl 694 |
. . 3
⊢ ((𝜑 ∧ 𝐵 = 0) → (𝐴 × {0}) ∈ MblFn) |
124 | 121, 123 | eqeltrd 2701 |
. 2
⊢ ((𝜑 ∧ 𝐵 = 0) → ((𝐴 × {𝐵}) ∘𝑓 ·
𝐹) ∈
MblFn) |
125 | 14 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ 0 < 𝐵) → ((𝐴 × {𝐵}) ∘𝑓 ·
𝐹):𝐴⟶ℝ) |
126 | 12 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ 0 < 𝐵) → 𝐴 ∈ dom vol) |
127 | | simprl 794 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 0 < 𝐵) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → 𝑦 ∈ ℝ) |
128 | 127 | rexrd 10089 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 0 < 𝐵) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → 𝑦 ∈ ℝ*) |
129 | 128, 19 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 0 < 𝐵) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → ((((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧) ∈ (𝑦(,)+∞) ↔ ((((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧) ∈ ℝ ∧ 𝑦 < (((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧)))) |
130 | 21 | ad2ant2rl 785 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 0 < 𝐵) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → (((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧) ∈ ℝ) |
131 | 130 | biantrurd 529 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 0 < 𝐵) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → (𝑦 < (((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧) ↔ ((((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧) ∈ ℝ ∧ 𝑦 < (((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧)))) |
132 | 24 | ad2ant2rl 785 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 0 < 𝐵) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → (𝐹‘𝑧) ∈ ℝ) |
133 | 132 | biantrurd 529 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 0 < 𝐵) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → ((𝑦 / 𝐵) < (𝐹‘𝑧) ↔ ((𝐹‘𝑧) ∈ ℝ ∧ (𝑦 / 𝐵) < (𝐹‘𝑧)))) |
134 | | eqidd 2623 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) = (𝐹‘𝑧)) |
135 | 12, 3, 70, 134 | ofc1 6920 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧) = (𝐵 · (𝐹‘𝑧))) |
136 | 135 | ad2ant2rl 785 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 0 < 𝐵) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → (((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧) = (𝐵 · (𝐹‘𝑧))) |
137 | 136 | breq2d 4665 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 0 < 𝐵) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → (𝑦 < (((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧) ↔ 𝑦 < (𝐵 · (𝐹‘𝑧)))) |
138 | 3 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 0 < 𝐵) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → 𝐵 ∈ ℝ) |
139 | | simplr 792 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 0 < 𝐵) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → 0 < 𝐵) |
140 | | ltdivmul 10898 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℝ ∧ (𝐹‘𝑧) ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → ((𝑦 / 𝐵) < (𝐹‘𝑧) ↔ 𝑦 < (𝐵 · (𝐹‘𝑧)))) |
141 | 127, 132,
138, 139, 140 | syl112anc 1330 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 0 < 𝐵) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → ((𝑦 / 𝐵) < (𝐹‘𝑧) ↔ 𝑦 < (𝐵 · (𝐹‘𝑧)))) |
142 | 137, 141 | bitr4d 271 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 0 < 𝐵) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → (𝑦 < (((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧) ↔ (𝑦 / 𝐵) < (𝐹‘𝑧))) |
143 | 138, 139 | elrpd 11869 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 0 < 𝐵) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → 𝐵 ∈
ℝ+) |
144 | 127, 143 | rerpdivcld 11903 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 0 < 𝐵) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → (𝑦 / 𝐵) ∈ ℝ) |
145 | 144 | rexrd 10089 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 0 < 𝐵) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → (𝑦 / 𝐵) ∈
ℝ*) |
146 | 145, 93 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 0 < 𝐵) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → ((𝐹‘𝑧) ∈ ((𝑦 / 𝐵)(,)+∞) ↔ ((𝐹‘𝑧) ∈ ℝ ∧ (𝑦 / 𝐵) < (𝐹‘𝑧)))) |
147 | 133, 142,
146 | 3bitr4d 300 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 0 < 𝐵) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → (𝑦 < (((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧) ↔ (𝐹‘𝑧) ∈ ((𝑦 / 𝐵)(,)+∞))) |
148 | 129, 131,
147 | 3bitr2d 296 |
. . . . . . . 8
⊢ (((𝜑 ∧ 0 < 𝐵) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → ((((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧) ∈ (𝑦(,)+∞) ↔ (𝐹‘𝑧) ∈ ((𝑦 / 𝐵)(,)+∞))) |
149 | 148 | anassrs 680 |
. . . . . . 7
⊢ ((((𝜑 ∧ 0 < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → ((((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧) ∈ (𝑦(,)+∞) ↔ (𝐹‘𝑧) ∈ ((𝑦 / 𝐵)(,)+∞))) |
150 | 149 | pm5.32da 673 |
. . . . . 6
⊢ (((𝜑 ∧ 0 < 𝐵) ∧ 𝑦 ∈ ℝ) → ((𝑧 ∈ 𝐴 ∧ (((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧) ∈ (𝑦(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ ((𝑦 / 𝐵)(,)+∞)))) |
151 | 66 | ad2antrr 762 |
. . . . . . 7
⊢ (((𝜑 ∧ 0 < 𝐵) ∧ 𝑦 ∈ ℝ) → ((𝐴 × {𝐵}) ∘𝑓 ·
𝐹) Fn 𝐴) |
152 | 151, 68 | syl 17 |
. . . . . 6
⊢ (((𝜑 ∧ 0 < 𝐵) ∧ 𝑦 ∈ ℝ) → (𝑧 ∈ (◡((𝐴 × {𝐵}) ∘𝑓 ·
𝐹) “ (𝑦(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧) ∈ (𝑦(,)+∞)))) |
153 | 70 | ad2antrr 762 |
. . . . . . 7
⊢ (((𝜑 ∧ 0 < 𝐵) ∧ 𝑦 ∈ ℝ) → 𝐹 Fn 𝐴) |
154 | 153, 101 | syl 17 |
. . . . . 6
⊢ (((𝜑 ∧ 0 < 𝐵) ∧ 𝑦 ∈ ℝ) → (𝑧 ∈ (◡𝐹 “ ((𝑦 / 𝐵)(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ ((𝑦 / 𝐵)(,)+∞)))) |
155 | 150, 152,
154 | 3bitr4d 300 |
. . . . 5
⊢ (((𝜑 ∧ 0 < 𝐵) ∧ 𝑦 ∈ ℝ) → (𝑧 ∈ (◡((𝐴 × {𝐵}) ∘𝑓 ·
𝐹) “ (𝑦(,)+∞)) ↔ 𝑧 ∈ (◡𝐹 “ ((𝑦 / 𝐵)(,)+∞)))) |
156 | 155 | eqrdv 2620 |
. . . 4
⊢ (((𝜑 ∧ 0 < 𝐵) ∧ 𝑦 ∈ ℝ) → (◡((𝐴 × {𝐵}) ∘𝑓 ·
𝐹) “ (𝑦(,)+∞)) = (◡𝐹 “ ((𝑦 / 𝐵)(,)+∞))) |
157 | 106 | ad2antrr 762 |
. . . 4
⊢ (((𝜑 ∧ 0 < 𝐵) ∧ 𝑦 ∈ ℝ) → (◡𝐹 “ ((𝑦 / 𝐵)(,)+∞)) ∈ dom
vol) |
158 | 156, 157 | eqeltrd 2701 |
. . 3
⊢ (((𝜑 ∧ 0 < 𝐵) ∧ 𝑦 ∈ ℝ) → (◡((𝐴 × {𝐵}) ∘𝑓 ·
𝐹) “ (𝑦(,)+∞)) ∈ dom
vol) |
159 | 128, 80 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 0 < 𝐵) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → ((((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧) ∈ (-∞(,)𝑦) ↔ ((((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧) ∈ ℝ ∧ (((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧) < 𝑦))) |
160 | 130 | biantrurd 529 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 0 < 𝐵) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → ((((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧) < 𝑦 ↔ ((((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧) ∈ ℝ ∧ (((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧) < 𝑦))) |
161 | | ltmuldiv2 10897 |
. . . . . . . . . . 11
⊢ (((𝐹‘𝑧) ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → ((𝐵 · (𝐹‘𝑧)) < 𝑦 ↔ (𝐹‘𝑧) < (𝑦 / 𝐵))) |
162 | 132, 127,
138, 139, 161 | syl112anc 1330 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 0 < 𝐵) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → ((𝐵 · (𝐹‘𝑧)) < 𝑦 ↔ (𝐹‘𝑧) < (𝑦 / 𝐵))) |
163 | 136 | breq1d 4663 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 0 < 𝐵) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → ((((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧) < 𝑦 ↔ (𝐵 · (𝐹‘𝑧)) < 𝑦)) |
164 | 145, 59 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 0 < 𝐵) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → ((𝐹‘𝑧) ∈ (-∞(,)(𝑦 / 𝐵)) ↔ ((𝐹‘𝑧) ∈ ℝ ∧ (𝐹‘𝑧) < (𝑦 / 𝐵)))) |
165 | 132 | biantrurd 529 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 0 < 𝐵) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → ((𝐹‘𝑧) < (𝑦 / 𝐵) ↔ ((𝐹‘𝑧) ∈ ℝ ∧ (𝐹‘𝑧) < (𝑦 / 𝐵)))) |
166 | 164, 165 | bitr4d 271 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 0 < 𝐵) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → ((𝐹‘𝑧) ∈ (-∞(,)(𝑦 / 𝐵)) ↔ (𝐹‘𝑧) < (𝑦 / 𝐵))) |
167 | 162, 163,
166 | 3bitr4d 300 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 0 < 𝐵) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → ((((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧) < 𝑦 ↔ (𝐹‘𝑧) ∈ (-∞(,)(𝑦 / 𝐵)))) |
168 | 159, 160,
167 | 3bitr2d 296 |
. . . . . . . 8
⊢ (((𝜑 ∧ 0 < 𝐵) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) → ((((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧) ∈ (-∞(,)𝑦) ↔ (𝐹‘𝑧) ∈ (-∞(,)(𝑦 / 𝐵)))) |
169 | 168 | anassrs 680 |
. . . . . . 7
⊢ ((((𝜑 ∧ 0 < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → ((((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧) ∈ (-∞(,)𝑦) ↔ (𝐹‘𝑧) ∈ (-∞(,)(𝑦 / 𝐵)))) |
170 | 169 | pm5.32da 673 |
. . . . . 6
⊢ (((𝜑 ∧ 0 < 𝐵) ∧ 𝑦 ∈ ℝ) → ((𝑧 ∈ 𝐴 ∧ (((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧) ∈ (-∞(,)𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (-∞(,)(𝑦 / 𝐵))))) |
171 | 151, 99 | syl 17 |
. . . . . 6
⊢ (((𝜑 ∧ 0 < 𝐵) ∧ 𝑦 ∈ ℝ) → (𝑧 ∈ (◡((𝐴 × {𝐵}) ∘𝑓 ·
𝐹) “
(-∞(,)𝑦)) ↔
(𝑧 ∈ 𝐴 ∧ (((𝐴 × {𝐵}) ∘𝑓 ·
𝐹)‘𝑧) ∈ (-∞(,)𝑦)))) |
172 | 153, 72 | syl 17 |
. . . . . 6
⊢ (((𝜑 ∧ 0 < 𝐵) ∧ 𝑦 ∈ ℝ) → (𝑧 ∈ (◡𝐹 “ (-∞(,)(𝑦 / 𝐵))) ↔ (𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) ∈ (-∞(,)(𝑦 / 𝐵))))) |
173 | 170, 171,
172 | 3bitr4d 300 |
. . . . 5
⊢ (((𝜑 ∧ 0 < 𝐵) ∧ 𝑦 ∈ ℝ) → (𝑧 ∈ (◡((𝐴 × {𝐵}) ∘𝑓 ·
𝐹) “
(-∞(,)𝑦)) ↔
𝑧 ∈ (◡𝐹 “ (-∞(,)(𝑦 / 𝐵))))) |
174 | 173 | eqrdv 2620 |
. . . 4
⊢ (((𝜑 ∧ 0 < 𝐵) ∧ 𝑦 ∈ ℝ) → (◡((𝐴 × {𝐵}) ∘𝑓 ·
𝐹) “
(-∞(,)𝑦)) = (◡𝐹 “ (-∞(,)(𝑦 / 𝐵)))) |
175 | 77 | ad2antrr 762 |
. . . 4
⊢ (((𝜑 ∧ 0 < 𝐵) ∧ 𝑦 ∈ ℝ) → (◡𝐹 “ (-∞(,)(𝑦 / 𝐵))) ∈ dom vol) |
176 | 174, 175 | eqeltrd 2701 |
. . 3
⊢ (((𝜑 ∧ 0 < 𝐵) ∧ 𝑦 ∈ ℝ) → (◡((𝐴 × {𝐵}) ∘𝑓 ·
𝐹) “
(-∞(,)𝑦)) ∈ dom
vol) |
177 | 125, 126,
158, 176 | ismbf2d 23408 |
. 2
⊢ ((𝜑 ∧ 0 < 𝐵) → ((𝐴 × {𝐵}) ∘𝑓 ·
𝐹) ∈
MblFn) |
178 | | 0re 10040 |
. . 3
⊢ 0 ∈
ℝ |
179 | | lttri4 10122 |
. . 3
⊢ ((𝐵 ∈ ℝ ∧ 0 ∈
ℝ) → (𝐵 < 0
∨ 𝐵 = 0 ∨ 0 <
𝐵)) |
180 | 3, 178, 179 | sylancl 694 |
. 2
⊢ (𝜑 → (𝐵 < 0 ∨ 𝐵 = 0 ∨ 0 < 𝐵)) |
181 | 109, 124,
177, 180 | mpjao3dan 1395 |
1
⊢ (𝜑 → ((𝐴 × {𝐵}) ∘𝑓 ·
𝐹) ∈
MblFn) |