| Step | Hyp | Ref
| Expression |
| 1 | | itg2mulc.2 |
. . . . 5
⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞)) |
| 2 | 1 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 0 < 𝐴) → 𝐹:ℝ⟶(0[,)+∞)) |
| 3 | | itg2mulc.3 |
. . . . 5
⊢ (𝜑 →
(∫2‘𝐹)
∈ ℝ) |
| 4 | 3 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 0 < 𝐴) → (∫2‘𝐹) ∈
ℝ) |
| 5 | | itg2mulc.4 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ (0[,)+∞)) |
| 6 | | elrege0 13494 |
. . . . . . . 8
⊢ (𝐴 ∈ (0[,)+∞) ↔
(𝐴 ∈ ℝ ∧ 0
≤ 𝐴)) |
| 7 | 5, 6 | sylib 218 |
. . . . . . 7
⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴)) |
| 8 | 7 | simpld 494 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ ℝ) |
| 9 | 8 | anim1i 615 |
. . . . 5
⊢ ((𝜑 ∧ 0 < 𝐴) → (𝐴 ∈ ℝ ∧ 0 < 𝐴)) |
| 10 | | elrp 13036 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
↔ (𝐴 ∈ ℝ
∧ 0 < 𝐴)) |
| 11 | 9, 10 | sylibr 234 |
. . . 4
⊢ ((𝜑 ∧ 0 < 𝐴) → 𝐴 ∈
ℝ+) |
| 12 | 2, 4, 11 | itg2mulclem 25781 |
. . 3
⊢ ((𝜑 ∧ 0 < 𝐴) → (∫2‘((ℝ
× {𝐴})
∘f · 𝐹)) ≤ (𝐴 · (∫2‘𝐹))) |
| 13 | | ge0mulcl 13501 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (0[,)+∞) ∧
𝑦 ∈ (0[,)+∞))
→ (𝑥 · 𝑦) ∈
(0[,)+∞)) |
| 14 | 13 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (0[,)+∞) ∧ 𝑦 ∈ (0[,)+∞))) →
(𝑥 · 𝑦) ∈
(0[,)+∞)) |
| 15 | | fconst6g 6797 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0[,)+∞) →
(ℝ × {𝐴}):ℝ⟶(0[,)+∞)) |
| 16 | 5, 15 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (ℝ × {𝐴}):ℝ⟶(0[,)+∞)) |
| 17 | | reex 11246 |
. . . . . . . . 9
⊢ ℝ
∈ V |
| 18 | 17 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → ℝ ∈
V) |
| 19 | | inidm 4227 |
. . . . . . . 8
⊢ (ℝ
∩ ℝ) = ℝ |
| 20 | 14, 16, 1, 18, 18, 19 | off 7715 |
. . . . . . 7
⊢ (𝜑 → ((ℝ × {𝐴}) ∘f ·
𝐹):ℝ⟶(0[,)+∞)) |
| 21 | 20 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 0 < 𝐴) → ((ℝ × {𝐴}) ∘f ·
𝐹):ℝ⟶(0[,)+∞)) |
| 22 | | icossicc 13476 |
. . . . . . . . 9
⊢
(0[,)+∞) ⊆ (0[,]+∞) |
| 23 | | fss 6752 |
. . . . . . . . 9
⊢
((((ℝ × {𝐴}) ∘f · 𝐹):ℝ⟶(0[,)+∞)
∧ (0[,)+∞) ⊆ (0[,]+∞)) → ((ℝ × {𝐴}) ∘f ·
𝐹):ℝ⟶(0[,]+∞)) |
| 24 | 20, 22, 23 | sylancl 586 |
. . . . . . . 8
⊢ (𝜑 → ((ℝ × {𝐴}) ∘f ·
𝐹):ℝ⟶(0[,]+∞)) |
| 25 | 24 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 0 < 𝐴) → ((ℝ × {𝐴}) ∘f ·
𝐹):ℝ⟶(0[,]+∞)) |
| 26 | 8, 3 | remulcld 11291 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 · (∫2‘𝐹)) ∈
ℝ) |
| 27 | 26 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 0 < 𝐴) → (𝐴 · (∫2‘𝐹)) ∈
ℝ) |
| 28 | | itg2lecl 25773 |
. . . . . . 7
⊢
((((ℝ × {𝐴}) ∘f · 𝐹):ℝ⟶(0[,]+∞)
∧ (𝐴 ·
(∫2‘𝐹)) ∈ ℝ ∧
(∫2‘((ℝ × {𝐴}) ∘f · 𝐹)) ≤ (𝐴 · (∫2‘𝐹))) →
(∫2‘((ℝ × {𝐴}) ∘f · 𝐹)) ∈
ℝ) |
| 29 | 25, 27, 12, 28 | syl3anc 1373 |
. . . . . 6
⊢ ((𝜑 ∧ 0 < 𝐴) → (∫2‘((ℝ
× {𝐴})
∘f · 𝐹)) ∈ ℝ) |
| 30 | 11 | rpreccld 13087 |
. . . . . 6
⊢ ((𝜑 ∧ 0 < 𝐴) → (1 / 𝐴) ∈
ℝ+) |
| 31 | 21, 29, 30 | itg2mulclem 25781 |
. . . . 5
⊢ ((𝜑 ∧ 0 < 𝐴) → (∫2‘((ℝ
× {(1 / 𝐴)})
∘f · ((ℝ × {𝐴}) ∘f · 𝐹))) ≤ ((1 / 𝐴) ·
(∫2‘((ℝ × {𝐴}) ∘f · 𝐹)))) |
| 32 | 2 | feqmptd 6977 |
. . . . . . . 8
⊢ ((𝜑 ∧ 0 < 𝐴) → 𝐹 = (𝑦 ∈ ℝ ↦ (𝐹‘𝑦))) |
| 33 | | rge0ssre 13496 |
. . . . . . . . . . . . . 14
⊢
(0[,)+∞) ⊆ ℝ |
| 34 | | ax-resscn 11212 |
. . . . . . . . . . . . . 14
⊢ ℝ
⊆ ℂ |
| 35 | 33, 34 | sstri 3993 |
. . . . . . . . . . . . 13
⊢
(0[,)+∞) ⊆ ℂ |
| 36 | | fss 6752 |
. . . . . . . . . . . . 13
⊢ ((𝐹:ℝ⟶(0[,)+∞)
∧ (0[,)+∞) ⊆ ℂ) → 𝐹:ℝ⟶ℂ) |
| 37 | 1, 35, 36 | sylancl 586 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹:ℝ⟶ℂ) |
| 38 | 37 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 0 < 𝐴) → 𝐹:ℝ⟶ℂ) |
| 39 | 38 | ffvelcdmda 7104 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 0 < 𝐴) ∧ 𝑦 ∈ ℝ) → (𝐹‘𝑦) ∈ ℂ) |
| 40 | 39 | mullidd 11279 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 0 < 𝐴) ∧ 𝑦 ∈ ℝ) → (1 · (𝐹‘𝑦)) = (𝐹‘𝑦)) |
| 41 | 40 | mpteq2dva 5242 |
. . . . . . . 8
⊢ ((𝜑 ∧ 0 < 𝐴) → (𝑦 ∈ ℝ ↦ (1 · (𝐹‘𝑦))) = (𝑦 ∈ ℝ ↦ (𝐹‘𝑦))) |
| 42 | 32, 41 | eqtr4d 2780 |
. . . . . . 7
⊢ ((𝜑 ∧ 0 < 𝐴) → 𝐹 = (𝑦 ∈ ℝ ↦ (1 · (𝐹‘𝑦)))) |
| 43 | 17 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 0 < 𝐴) → ℝ ∈ V) |
| 44 | | 1red 11262 |
. . . . . . . 8
⊢ (((𝜑 ∧ 0 < 𝐴) ∧ 𝑦 ∈ ℝ) → 1 ∈
ℝ) |
| 45 | 43, 30, 11 | ofc12 7727 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 0 < 𝐴) → ((ℝ × {(1 / 𝐴)}) ∘f ·
(ℝ × {𝐴})) =
(ℝ × {((1 / 𝐴)
· 𝐴)})) |
| 46 | | fconstmpt 5747 |
. . . . . . . . . 10
⊢ (ℝ
× {((1 / 𝐴) ·
𝐴)}) = (𝑦 ∈ ℝ ↦ ((1 / 𝐴) · 𝐴)) |
| 47 | 45, 46 | eqtrdi 2793 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 0 < 𝐴) → ((ℝ × {(1 / 𝐴)}) ∘f ·
(ℝ × {𝐴})) =
(𝑦 ∈ ℝ ↦
((1 / 𝐴) · 𝐴))) |
| 48 | 8 | recnd 11289 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ ℂ) |
| 49 | 48 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 0 < 𝐴) → 𝐴 ∈ ℂ) |
| 50 | 11 | rpne0d 13082 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 0 < 𝐴) → 𝐴 ≠ 0) |
| 51 | 49, 50 | recid2d 12039 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 0 < 𝐴) → ((1 / 𝐴) · 𝐴) = 1) |
| 52 | 51 | mpteq2dv 5244 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 0 < 𝐴) → (𝑦 ∈ ℝ ↦ ((1 / 𝐴) · 𝐴)) = (𝑦 ∈ ℝ ↦ 1)) |
| 53 | 47, 52 | eqtrd 2777 |
. . . . . . . 8
⊢ ((𝜑 ∧ 0 < 𝐴) → ((ℝ × {(1 / 𝐴)}) ∘f ·
(ℝ × {𝐴})) =
(𝑦 ∈ ℝ ↦
1)) |
| 54 | 43, 44, 39, 53, 32 | offval2 7717 |
. . . . . . 7
⊢ ((𝜑 ∧ 0 < 𝐴) → (((ℝ × {(1 / 𝐴)}) ∘f ·
(ℝ × {𝐴}))
∘f · 𝐹) = (𝑦 ∈ ℝ ↦ (1 · (𝐹‘𝑦)))) |
| 55 | 30 | rpcnd 13079 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 0 < 𝐴) → (1 / 𝐴) ∈ ℂ) |
| 56 | | fconst6g 6797 |
. . . . . . . . 9
⊢ ((1 /
𝐴) ∈ ℂ →
(ℝ × {(1 / 𝐴)}):ℝ⟶ℂ) |
| 57 | 55, 56 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 0 < 𝐴) → (ℝ × {(1 / 𝐴)}):ℝ⟶ℂ) |
| 58 | | fconst6g 6797 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (ℝ
× {𝐴}):ℝ⟶ℂ) |
| 59 | 49, 58 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 0 < 𝐴) → (ℝ × {𝐴}):ℝ⟶ℂ) |
| 60 | | mulass 11243 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝑥 · 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧))) |
| 61 | 60 | adantl 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 0 < 𝐴) ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ)) → ((𝑥 · 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧))) |
| 62 | 43, 57, 59, 38, 61 | caofass 7737 |
. . . . . . 7
⊢ ((𝜑 ∧ 0 < 𝐴) → (((ℝ × {(1 / 𝐴)}) ∘f ·
(ℝ × {𝐴}))
∘f · 𝐹) = ((ℝ × {(1 / 𝐴)}) ∘f ·
((ℝ × {𝐴})
∘f · 𝐹))) |
| 63 | 42, 54, 62 | 3eqtr2d 2783 |
. . . . . 6
⊢ ((𝜑 ∧ 0 < 𝐴) → 𝐹 = ((ℝ × {(1 / 𝐴)}) ∘f · ((ℝ
× {𝐴})
∘f · 𝐹))) |
| 64 | 63 | fveq2d 6910 |
. . . . 5
⊢ ((𝜑 ∧ 0 < 𝐴) → (∫2‘𝐹) =
(∫2‘((ℝ × {(1 / 𝐴)}) ∘f · ((ℝ
× {𝐴})
∘f · 𝐹)))) |
| 65 | 29 | recnd 11289 |
. . . . . 6
⊢ ((𝜑 ∧ 0 < 𝐴) → (∫2‘((ℝ
× {𝐴})
∘f · 𝐹)) ∈ ℂ) |
| 66 | 65, 49, 50 | divrec2d 12047 |
. . . . 5
⊢ ((𝜑 ∧ 0 < 𝐴) → ((∫2‘((ℝ
× {𝐴})
∘f · 𝐹)) / 𝐴) = ((1 / 𝐴) ·
(∫2‘((ℝ × {𝐴}) ∘f · 𝐹)))) |
| 67 | 31, 64, 66 | 3brtr4d 5175 |
. . . 4
⊢ ((𝜑 ∧ 0 < 𝐴) → (∫2‘𝐹) ≤
((∫2‘((ℝ × {𝐴}) ∘f · 𝐹)) / 𝐴)) |
| 68 | 4, 29, 11 | lemuldiv2d 13127 |
. . . 4
⊢ ((𝜑 ∧ 0 < 𝐴) → ((𝐴 · (∫2‘𝐹)) ≤
(∫2‘((ℝ × {𝐴}) ∘f · 𝐹)) ↔
(∫2‘𝐹)
≤ ((∫2‘((ℝ × {𝐴}) ∘f · 𝐹)) / 𝐴))) |
| 69 | 67, 68 | mpbird 257 |
. . 3
⊢ ((𝜑 ∧ 0 < 𝐴) → (𝐴 · (∫2‘𝐹)) ≤
(∫2‘((ℝ × {𝐴}) ∘f · 𝐹))) |
| 70 | | itg2cl 25767 |
. . . . . 6
⊢
(((ℝ × {𝐴}) ∘f · 𝐹):ℝ⟶(0[,]+∞)
→ (∫2‘((ℝ × {𝐴}) ∘f · 𝐹)) ∈
ℝ*) |
| 71 | 24, 70 | syl 17 |
. . . . 5
⊢ (𝜑 →
(∫2‘((ℝ × {𝐴}) ∘f · 𝐹)) ∈
ℝ*) |
| 72 | 26 | rexrd 11311 |
. . . . 5
⊢ (𝜑 → (𝐴 · (∫2‘𝐹)) ∈
ℝ*) |
| 73 | | xrletri3 13196 |
. . . . 5
⊢
(((∫2‘((ℝ × {𝐴}) ∘f · 𝐹)) ∈ ℝ*
∧ (𝐴 ·
(∫2‘𝐹)) ∈ ℝ*) →
((∫2‘((ℝ × {𝐴}) ∘f · 𝐹)) = (𝐴 · (∫2‘𝐹)) ↔
((∫2‘((ℝ × {𝐴}) ∘f · 𝐹)) ≤ (𝐴 · (∫2‘𝐹)) ∧ (𝐴 · (∫2‘𝐹)) ≤
(∫2‘((ℝ × {𝐴}) ∘f · 𝐹))))) |
| 74 | 71, 72, 73 | syl2anc 584 |
. . . 4
⊢ (𝜑 →
((∫2‘((ℝ × {𝐴}) ∘f · 𝐹)) = (𝐴 · (∫2‘𝐹)) ↔
((∫2‘((ℝ × {𝐴}) ∘f · 𝐹)) ≤ (𝐴 · (∫2‘𝐹)) ∧ (𝐴 · (∫2‘𝐹)) ≤
(∫2‘((ℝ × {𝐴}) ∘f · 𝐹))))) |
| 75 | 74 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 0 < 𝐴) → ((∫2‘((ℝ
× {𝐴})
∘f · 𝐹)) = (𝐴 · (∫2‘𝐹)) ↔
((∫2‘((ℝ × {𝐴}) ∘f · 𝐹)) ≤ (𝐴 · (∫2‘𝐹)) ∧ (𝐴 · (∫2‘𝐹)) ≤
(∫2‘((ℝ × {𝐴}) ∘f · 𝐹))))) |
| 76 | 12, 69, 75 | mpbir2and 713 |
. 2
⊢ ((𝜑 ∧ 0 < 𝐴) → (∫2‘((ℝ
× {𝐴})
∘f · 𝐹)) = (𝐴 · (∫2‘𝐹))) |
| 77 | 17 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 0 = 𝐴) → ℝ ∈ V) |
| 78 | 37 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 0 = 𝐴) → 𝐹:ℝ⟶ℂ) |
| 79 | 8 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 0 = 𝐴) → 𝐴 ∈ ℝ) |
| 80 | | 0re 11263 |
. . . . . . 7
⊢ 0 ∈
ℝ |
| 81 | 80 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 0 = 𝐴) → 0 ∈ ℝ) |
| 82 | | simplr 769 |
. . . . . . . 8
⊢ (((𝜑 ∧ 0 = 𝐴) ∧ 𝑥 ∈ ℂ) → 0 = 𝐴) |
| 83 | 82 | oveq1d 7446 |
. . . . . . 7
⊢ (((𝜑 ∧ 0 = 𝐴) ∧ 𝑥 ∈ ℂ) → (0 · 𝑥) = (𝐴 · 𝑥)) |
| 84 | | mul02 11439 |
. . . . . . . 8
⊢ (𝑥 ∈ ℂ → (0
· 𝑥) =
0) |
| 85 | 84 | adantl 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 0 = 𝐴) ∧ 𝑥 ∈ ℂ) → (0 · 𝑥) = 0) |
| 86 | 83, 85 | eqtr3d 2779 |
. . . . . 6
⊢ (((𝜑 ∧ 0 = 𝐴) ∧ 𝑥 ∈ ℂ) → (𝐴 · 𝑥) = 0) |
| 87 | 77, 78, 79, 81, 86 | caofid2 7733 |
. . . . 5
⊢ ((𝜑 ∧ 0 = 𝐴) → ((ℝ × {𝐴}) ∘f ·
𝐹) = (ℝ ×
{0})) |
| 88 | 87 | fveq2d 6910 |
. . . 4
⊢ ((𝜑 ∧ 0 = 𝐴) → (∫2‘((ℝ
× {𝐴})
∘f · 𝐹)) = (∫2‘(ℝ
× {0}))) |
| 89 | | itg20 25772 |
. . . 4
⊢
(∫2‘(ℝ × {0})) = 0 |
| 90 | 88, 89 | eqtrdi 2793 |
. . 3
⊢ ((𝜑 ∧ 0 = 𝐴) → (∫2‘((ℝ
× {𝐴})
∘f · 𝐹)) = 0) |
| 91 | 3 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 0 = 𝐴) → (∫2‘𝐹) ∈
ℝ) |
| 92 | 91 | recnd 11289 |
. . . 4
⊢ ((𝜑 ∧ 0 = 𝐴) → (∫2‘𝐹) ∈
ℂ) |
| 93 | 92 | mul02d 11459 |
. . 3
⊢ ((𝜑 ∧ 0 = 𝐴) → (0 ·
(∫2‘𝐹)) = 0) |
| 94 | | simpr 484 |
. . . 4
⊢ ((𝜑 ∧ 0 = 𝐴) → 0 = 𝐴) |
| 95 | 94 | oveq1d 7446 |
. . 3
⊢ ((𝜑 ∧ 0 = 𝐴) → (0 ·
(∫2‘𝐹)) = (𝐴 · (∫2‘𝐹))) |
| 96 | 90, 93, 95 | 3eqtr2d 2783 |
. 2
⊢ ((𝜑 ∧ 0 = 𝐴) → (∫2‘((ℝ
× {𝐴})
∘f · 𝐹)) = (𝐴 · (∫2‘𝐹))) |
| 97 | 7 | simprd 495 |
. . 3
⊢ (𝜑 → 0 ≤ 𝐴) |
| 98 | | leloe 11347 |
. . . 4
⊢ ((0
∈ ℝ ∧ 𝐴
∈ ℝ) → (0 ≤ 𝐴 ↔ (0 < 𝐴 ∨ 0 = 𝐴))) |
| 99 | 80, 8, 98 | sylancr 587 |
. . 3
⊢ (𝜑 → (0 ≤ 𝐴 ↔ (0 < 𝐴 ∨ 0 = 𝐴))) |
| 100 | 97, 99 | mpbid 232 |
. 2
⊢ (𝜑 → (0 < 𝐴 ∨ 0 = 𝐴)) |
| 101 | 76, 96, 100 | mpjaodan 961 |
1
⊢ (𝜑 →
(∫2‘((ℝ × {𝐴}) ∘f · 𝐹)) = (𝐴 · (∫2‘𝐹))) |