Step | Hyp | Ref
| Expression |
1 | | itg2add.f1 |
. . . 4
⊢ (𝜑 → 𝐹 ∈ MblFn) |
2 | | itg2add.g1 |
. . . 4
⊢ (𝜑 → 𝐺 ∈ MblFn) |
3 | 1, 2 | mbfadd 24558 |
. . 3
⊢ (𝜑 → (𝐹 ∘f + 𝐺) ∈ MblFn) |
4 | | ge0addcl 13048 |
. . . . 5
⊢ ((𝑦 ∈ (0[,)+∞) ∧
𝑧 ∈ (0[,)+∞))
→ (𝑦 + 𝑧) ∈
(0[,)+∞)) |
5 | 4 | adantl 485 |
. . . 4
⊢ ((𝜑 ∧ (𝑦 ∈ (0[,)+∞) ∧ 𝑧 ∈ (0[,)+∞))) →
(𝑦 + 𝑧) ∈ (0[,)+∞)) |
6 | | itg2add.f2 |
. . . 4
⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞)) |
7 | | itg2add.g2 |
. . . 4
⊢ (𝜑 → 𝐺:ℝ⟶(0[,)+∞)) |
8 | | reex 10820 |
. . . . 5
⊢ ℝ
∈ V |
9 | 8 | a1i 11 |
. . . 4
⊢ (𝜑 → ℝ ∈
V) |
10 | | inidm 4133 |
. . . 4
⊢ (ℝ
∩ ℝ) = ℝ |
11 | 5, 6, 7, 9, 9, 10 | off 7486 |
. . 3
⊢ (𝜑 → (𝐹 ∘f + 𝐺):ℝ⟶(0[,)+∞)) |
12 | | simpl 486 |
. . . . . 6
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → 𝑓
∈ dom ∫1) |
13 | | simpr 488 |
. . . . . 6
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → 𝑔
∈ dom ∫1) |
14 | 12, 13 | i1fadd 24592 |
. . . . 5
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (𝑓 ∘f + 𝑔) ∈ dom
∫1) |
15 | 14 | adantl 485 |
. . . 4
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ (𝑓
∘f + 𝑔)
∈ dom ∫1) |
16 | | itg2add.p1 |
. . . 4
⊢ (𝜑 → 𝑃:ℕ⟶dom
∫1) |
17 | | itg2add.q1 |
. . . 4
⊢ (𝜑 → 𝑄:ℕ⟶dom
∫1) |
18 | | nnex 11836 |
. . . . 5
⊢ ℕ
∈ V |
19 | 18 | a1i 11 |
. . . 4
⊢ (𝜑 → ℕ ∈
V) |
20 | | inidm 4133 |
. . . 4
⊢ (ℕ
∩ ℕ) = ℕ |
21 | 15, 16, 17, 19, 19, 20 | off 7486 |
. . 3
⊢ (𝜑 → (𝑃 ∘f ∘f +
𝑄):ℕ⟶dom
∫1) |
22 | | ge0addcl 13048 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ (0[,)+∞) ∧
𝑔 ∈ (0[,)+∞))
→ (𝑓 + 𝑔) ∈
(0[,)+∞)) |
23 | 22 | adantl 485 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓 ∈ (0[,)+∞) ∧ 𝑔 ∈ (0[,)+∞))) →
(𝑓 + 𝑔) ∈ (0[,)+∞)) |
24 | 16 | ffvelrnda 6904 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑃‘𝑚) ∈ dom
∫1) |
25 | | itg2add.p2 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑛 ∈ ℕ (0𝑝
∘r ≤ (𝑃‘𝑛) ∧ (𝑃‘𝑛) ∘r ≤ (𝑃‘(𝑛 + 1)))) |
26 | | fveq2 6717 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑚 → (𝑃‘𝑛) = (𝑃‘𝑚)) |
27 | 26 | breq2d 5065 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑚 → (0𝑝
∘r ≤ (𝑃‘𝑛) ↔ 0𝑝
∘r ≤ (𝑃‘𝑚))) |
28 | | fvoveq1 7236 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑚 → (𝑃‘(𝑛 + 1)) = (𝑃‘(𝑚 + 1))) |
29 | 26, 28 | breq12d 5066 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑚 → ((𝑃‘𝑛) ∘r ≤ (𝑃‘(𝑛 + 1)) ↔ (𝑃‘𝑚) ∘r ≤ (𝑃‘(𝑚 + 1)))) |
30 | 27, 29 | anbi12d 634 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑚 → ((0𝑝
∘r ≤ (𝑃‘𝑛) ∧ (𝑃‘𝑛) ∘r ≤ (𝑃‘(𝑛 + 1))) ↔ (0𝑝
∘r ≤ (𝑃‘𝑚) ∧ (𝑃‘𝑚) ∘r ≤ (𝑃‘(𝑚 + 1))))) |
31 | 30 | rspccva 3536 |
. . . . . . . . . . . 12
⊢
((∀𝑛 ∈
ℕ (0𝑝 ∘r ≤ (𝑃‘𝑛) ∧ (𝑃‘𝑛) ∘r ≤ (𝑃‘(𝑛 + 1))) ∧ 𝑚 ∈ ℕ) →
(0𝑝 ∘r ≤ (𝑃‘𝑚) ∧ (𝑃‘𝑚) ∘r ≤ (𝑃‘(𝑚 + 1)))) |
32 | 25, 31 | sylan 583 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) →
(0𝑝 ∘r ≤ (𝑃‘𝑚) ∧ (𝑃‘𝑚) ∘r ≤ (𝑃‘(𝑚 + 1)))) |
33 | 32 | simpld 498 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 0𝑝
∘r ≤ (𝑃‘𝑚)) |
34 | | breq2 5057 |
. . . . . . . . . . . 12
⊢ (𝑓 = (𝑃‘𝑚) → (0𝑝
∘r ≤ 𝑓
↔ 0𝑝 ∘r ≤ (𝑃‘𝑚))) |
35 | | feq1 6526 |
. . . . . . . . . . . 12
⊢ (𝑓 = (𝑃‘𝑚) → (𝑓:ℝ⟶(0[,)+∞) ↔ (𝑃‘𝑚):ℝ⟶(0[,)+∞))) |
36 | 34, 35 | imbi12d 348 |
. . . . . . . . . . 11
⊢ (𝑓 = (𝑃‘𝑚) → ((0𝑝
∘r ≤ 𝑓
→ 𝑓:ℝ⟶(0[,)+∞)) ↔
(0𝑝 ∘r ≤ (𝑃‘𝑚) → (𝑃‘𝑚):ℝ⟶(0[,)+∞)))) |
37 | | i1ff 24573 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 ∈ dom ∫1
→ 𝑓:ℝ⟶ℝ) |
38 | 37 | ffnd 6546 |
. . . . . . . . . . . . . 14
⊢ (𝑓 ∈ dom ∫1
→ 𝑓 Fn
ℝ) |
39 | 38 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝑓 ∈ dom ∫1
∧ 0𝑝 ∘r ≤ 𝑓) → 𝑓 Fn ℝ) |
40 | | 0cn 10825 |
. . . . . . . . . . . . . . . . . . 19
⊢ 0 ∈
ℂ |
41 | | fnconstg 6607 |
. . . . . . . . . . . . . . . . . . 19
⊢ (0 ∈
ℂ → (ℂ × {0}) Fn ℂ) |
42 | 40, 41 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢ (ℂ
× {0}) Fn ℂ |
43 | | df-0p 24567 |
. . . . . . . . . . . . . . . . . . 19
⊢
0𝑝 = (ℂ × {0}) |
44 | 43 | fneq1i 6476 |
. . . . . . . . . . . . . . . . . 18
⊢
(0𝑝 Fn ℂ ↔ (ℂ × {0}) Fn
ℂ) |
45 | 42, 44 | mpbir 234 |
. . . . . . . . . . . . . . . . 17
⊢
0𝑝 Fn ℂ |
46 | 45 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 ∈ dom ∫1
→ 0𝑝 Fn ℂ) |
47 | | cnex 10810 |
. . . . . . . . . . . . . . . . 17
⊢ ℂ
∈ V |
48 | 47 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 ∈ dom ∫1
→ ℂ ∈ V) |
49 | 8 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 ∈ dom ∫1
→ ℝ ∈ V) |
50 | | ax-resscn 10786 |
. . . . . . . . . . . . . . . . 17
⊢ ℝ
⊆ ℂ |
51 | | sseqin2 4130 |
. . . . . . . . . . . . . . . . 17
⊢ (ℝ
⊆ ℂ ↔ (ℂ ∩ ℝ) = ℝ) |
52 | 50, 51 | mpbi 233 |
. . . . . . . . . . . . . . . 16
⊢ (ℂ
∩ ℝ) = ℝ |
53 | | 0pval 24568 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℂ →
(0𝑝‘𝑥) = 0) |
54 | 53 | adantl 485 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑥 ∈ ℂ)
→ (0𝑝‘𝑥) = 0) |
55 | | eqidd 2738 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ (𝑓‘𝑥) = (𝑓‘𝑥)) |
56 | 46, 38, 48, 49, 52, 54, 55 | ofrfval 7478 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 ∈ dom ∫1
→ (0𝑝 ∘r ≤ 𝑓 ↔ ∀𝑥 ∈ ℝ 0 ≤ (𝑓‘𝑥))) |
57 | 56 | biimpa 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∈ dom ∫1
∧ 0𝑝 ∘r ≤ 𝑓) → ∀𝑥 ∈ ℝ 0 ≤ (𝑓‘𝑥)) |
58 | 37 | ffvelrnda 6904 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ (𝑓‘𝑥) ∈
ℝ) |
59 | | elrege0 13042 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓‘𝑥) ∈ (0[,)+∞) ↔ ((𝑓‘𝑥) ∈ ℝ ∧ 0 ≤ (𝑓‘𝑥))) |
60 | 59 | simplbi2 504 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓‘𝑥) ∈ ℝ → (0 ≤ (𝑓‘𝑥) → (𝑓‘𝑥) ∈ (0[,)+∞))) |
61 | 58, 60 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ (0 ≤ (𝑓‘𝑥) → (𝑓‘𝑥) ∈ (0[,)+∞))) |
62 | 61 | ralimdva 3100 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 ∈ dom ∫1
→ (∀𝑥 ∈
ℝ 0 ≤ (𝑓‘𝑥) → ∀𝑥 ∈ ℝ (𝑓‘𝑥) ∈ (0[,)+∞))) |
63 | 62 | imp 410 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∈ dom ∫1
∧ ∀𝑥 ∈
ℝ 0 ≤ (𝑓‘𝑥)) → ∀𝑥 ∈ ℝ (𝑓‘𝑥) ∈ (0[,)+∞)) |
64 | 57, 63 | syldan 594 |
. . . . . . . . . . . . 13
⊢ ((𝑓 ∈ dom ∫1
∧ 0𝑝 ∘r ≤ 𝑓) → ∀𝑥 ∈ ℝ (𝑓‘𝑥) ∈ (0[,)+∞)) |
65 | | ffnfv 6935 |
. . . . . . . . . . . . 13
⊢ (𝑓:ℝ⟶(0[,)+∞)
↔ (𝑓 Fn ℝ ∧
∀𝑥 ∈ ℝ
(𝑓‘𝑥) ∈ (0[,)+∞))) |
66 | 39, 64, 65 | sylanbrc 586 |
. . . . . . . . . . . 12
⊢ ((𝑓 ∈ dom ∫1
∧ 0𝑝 ∘r ≤ 𝑓) → 𝑓:ℝ⟶(0[,)+∞)) |
67 | 66 | ex 416 |
. . . . . . . . . . 11
⊢ (𝑓 ∈ dom ∫1
→ (0𝑝 ∘r ≤ 𝑓 → 𝑓:ℝ⟶(0[,)+∞))) |
68 | 36, 67 | vtoclga 3489 |
. . . . . . . . . 10
⊢ ((𝑃‘𝑚) ∈ dom ∫1 →
(0𝑝 ∘r ≤ (𝑃‘𝑚) → (𝑃‘𝑚):ℝ⟶(0[,)+∞))) |
69 | 24, 33, 68 | sylc 65 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑃‘𝑚):ℝ⟶(0[,)+∞)) |
70 | 17 | ffvelrnda 6904 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑄‘𝑚) ∈ dom
∫1) |
71 | | itg2add.q2 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑛 ∈ ℕ (0𝑝
∘r ≤ (𝑄‘𝑛) ∧ (𝑄‘𝑛) ∘r ≤ (𝑄‘(𝑛 + 1)))) |
72 | | fveq2 6717 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑚 → (𝑄‘𝑛) = (𝑄‘𝑚)) |
73 | 72 | breq2d 5065 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑚 → (0𝑝
∘r ≤ (𝑄‘𝑛) ↔ 0𝑝
∘r ≤ (𝑄‘𝑚))) |
74 | | fvoveq1 7236 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑚 → (𝑄‘(𝑛 + 1)) = (𝑄‘(𝑚 + 1))) |
75 | 72, 74 | breq12d 5066 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑚 → ((𝑄‘𝑛) ∘r ≤ (𝑄‘(𝑛 + 1)) ↔ (𝑄‘𝑚) ∘r ≤ (𝑄‘(𝑚 + 1)))) |
76 | 73, 75 | anbi12d 634 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑚 → ((0𝑝
∘r ≤ (𝑄‘𝑛) ∧ (𝑄‘𝑛) ∘r ≤ (𝑄‘(𝑛 + 1))) ↔ (0𝑝
∘r ≤ (𝑄‘𝑚) ∧ (𝑄‘𝑚) ∘r ≤ (𝑄‘(𝑚 + 1))))) |
77 | 76 | rspccva 3536 |
. . . . . . . . . . . 12
⊢
((∀𝑛 ∈
ℕ (0𝑝 ∘r ≤ (𝑄‘𝑛) ∧ (𝑄‘𝑛) ∘r ≤ (𝑄‘(𝑛 + 1))) ∧ 𝑚 ∈ ℕ) →
(0𝑝 ∘r ≤ (𝑄‘𝑚) ∧ (𝑄‘𝑚) ∘r ≤ (𝑄‘(𝑚 + 1)))) |
78 | 71, 77 | sylan 583 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) →
(0𝑝 ∘r ≤ (𝑄‘𝑚) ∧ (𝑄‘𝑚) ∘r ≤ (𝑄‘(𝑚 + 1)))) |
79 | 78 | simpld 498 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 0𝑝
∘r ≤ (𝑄‘𝑚)) |
80 | | breq2 5057 |
. . . . . . . . . . . 12
⊢ (𝑓 = (𝑄‘𝑚) → (0𝑝
∘r ≤ 𝑓
↔ 0𝑝 ∘r ≤ (𝑄‘𝑚))) |
81 | | feq1 6526 |
. . . . . . . . . . . 12
⊢ (𝑓 = (𝑄‘𝑚) → (𝑓:ℝ⟶(0[,)+∞) ↔ (𝑄‘𝑚):ℝ⟶(0[,)+∞))) |
82 | 80, 81 | imbi12d 348 |
. . . . . . . . . . 11
⊢ (𝑓 = (𝑄‘𝑚) → ((0𝑝
∘r ≤ 𝑓
→ 𝑓:ℝ⟶(0[,)+∞)) ↔
(0𝑝 ∘r ≤ (𝑄‘𝑚) → (𝑄‘𝑚):ℝ⟶(0[,)+∞)))) |
83 | 82, 67 | vtoclga 3489 |
. . . . . . . . . 10
⊢ ((𝑄‘𝑚) ∈ dom ∫1 →
(0𝑝 ∘r ≤ (𝑄‘𝑚) → (𝑄‘𝑚):ℝ⟶(0[,)+∞))) |
84 | 70, 79, 83 | sylc 65 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑄‘𝑚):ℝ⟶(0[,)+∞)) |
85 | 8 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ℝ ∈
V) |
86 | 23, 69, 84, 85, 85, 10 | off 7486 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑃‘𝑚) ∘f + (𝑄‘𝑚)):ℝ⟶(0[,)+∞)) |
87 | | 0plef 24569 |
. . . . . . . 8
⊢ (((𝑃‘𝑚) ∘f + (𝑄‘𝑚)):ℝ⟶(0[,)+∞) ↔
(((𝑃‘𝑚) ∘f + (𝑄‘𝑚)):ℝ⟶ℝ ∧
0𝑝 ∘r ≤ ((𝑃‘𝑚) ∘f + (𝑄‘𝑚)))) |
88 | 86, 87 | sylib 221 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (((𝑃‘𝑚) ∘f + (𝑄‘𝑚)):ℝ⟶ℝ ∧
0𝑝 ∘r ≤ ((𝑃‘𝑚) ∘f + (𝑄‘𝑚)))) |
89 | 88 | simprd 499 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 0𝑝
∘r ≤ ((𝑃‘𝑚) ∘f + (𝑄‘𝑚))) |
90 | 16 | ffnd 6546 |
. . . . . . 7
⊢ (𝜑 → 𝑃 Fn ℕ) |
91 | 17 | ffnd 6546 |
. . . . . . 7
⊢ (𝜑 → 𝑄 Fn ℕ) |
92 | | eqidd 2738 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑃‘𝑚) = (𝑃‘𝑚)) |
93 | | eqidd 2738 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑄‘𝑚) = (𝑄‘𝑚)) |
94 | 90, 91, 19, 19, 20, 92, 93 | ofval 7479 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑃 ∘f ∘f +
𝑄)‘𝑚) = ((𝑃‘𝑚) ∘f + (𝑄‘𝑚))) |
95 | 89, 94 | breqtrrd 5081 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 0𝑝
∘r ≤ ((𝑃 ∘f ∘f +
𝑄)‘𝑚)) |
96 | | i1ff 24573 |
. . . . . . . . . . 11
⊢ ((𝑃‘𝑚) ∈ dom ∫1 → (𝑃‘𝑚):ℝ⟶ℝ) |
97 | 24, 96 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑃‘𝑚):ℝ⟶ℝ) |
98 | 97 | ffvelrnda 6904 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → ((𝑃‘𝑚)‘𝑦) ∈ ℝ) |
99 | | i1ff 24573 |
. . . . . . . . . . 11
⊢ ((𝑄‘𝑚) ∈ dom ∫1 → (𝑄‘𝑚):ℝ⟶ℝ) |
100 | 70, 99 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑄‘𝑚):ℝ⟶ℝ) |
101 | 100 | ffvelrnda 6904 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → ((𝑄‘𝑚)‘𝑦) ∈ ℝ) |
102 | | peano2nn 11842 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ ℕ → (𝑚 + 1) ∈
ℕ) |
103 | | ffvelrn 6902 |
. . . . . . . . . . . 12
⊢ ((𝑃:ℕ⟶dom
∫1 ∧ (𝑚
+ 1) ∈ ℕ) → (𝑃‘(𝑚 + 1)) ∈ dom
∫1) |
104 | 16, 102, 103 | syl2an 599 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑃‘(𝑚 + 1)) ∈ dom
∫1) |
105 | | i1ff 24573 |
. . . . . . . . . . 11
⊢ ((𝑃‘(𝑚 + 1)) ∈ dom ∫1 →
(𝑃‘(𝑚 +
1)):ℝ⟶ℝ) |
106 | 104, 105 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑃‘(𝑚 +
1)):ℝ⟶ℝ) |
107 | 106 | ffvelrnda 6904 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → ((𝑃‘(𝑚 + 1))‘𝑦) ∈ ℝ) |
108 | | ffvelrn 6902 |
. . . . . . . . . . . 12
⊢ ((𝑄:ℕ⟶dom
∫1 ∧ (𝑚
+ 1) ∈ ℕ) → (𝑄‘(𝑚 + 1)) ∈ dom
∫1) |
109 | 17, 102, 108 | syl2an 599 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑄‘(𝑚 + 1)) ∈ dom
∫1) |
110 | | i1ff 24573 |
. . . . . . . . . . 11
⊢ ((𝑄‘(𝑚 + 1)) ∈ dom ∫1 →
(𝑄‘(𝑚 +
1)):ℝ⟶ℝ) |
111 | 109, 110 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑄‘(𝑚 +
1)):ℝ⟶ℝ) |
112 | 111 | ffvelrnda 6904 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → ((𝑄‘(𝑚 + 1))‘𝑦) ∈ ℝ) |
113 | 32 | simprd 499 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑃‘𝑚) ∘r ≤ (𝑃‘(𝑚 + 1))) |
114 | 97 | ffnd 6546 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑃‘𝑚) Fn ℝ) |
115 | 106 | ffnd 6546 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑃‘(𝑚 + 1)) Fn ℝ) |
116 | | eqidd 2738 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → ((𝑃‘𝑚)‘𝑦) = ((𝑃‘𝑚)‘𝑦)) |
117 | | eqidd 2738 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → ((𝑃‘(𝑚 + 1))‘𝑦) = ((𝑃‘(𝑚 + 1))‘𝑦)) |
118 | 114, 115,
85, 85, 10, 116, 117 | ofrfval 7478 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑃‘𝑚) ∘r ≤ (𝑃‘(𝑚 + 1)) ↔ ∀𝑦 ∈ ℝ ((𝑃‘𝑚)‘𝑦) ≤ ((𝑃‘(𝑚 + 1))‘𝑦))) |
119 | 113, 118 | mpbid 235 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ∀𝑦 ∈ ℝ ((𝑃‘𝑚)‘𝑦) ≤ ((𝑃‘(𝑚 + 1))‘𝑦)) |
120 | 119 | r19.21bi 3130 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → ((𝑃‘𝑚)‘𝑦) ≤ ((𝑃‘(𝑚 + 1))‘𝑦)) |
121 | 78 | simprd 499 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑄‘𝑚) ∘r ≤ (𝑄‘(𝑚 + 1))) |
122 | 100 | ffnd 6546 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑄‘𝑚) Fn ℝ) |
123 | 111 | ffnd 6546 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑄‘(𝑚 + 1)) Fn ℝ) |
124 | | eqidd 2738 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → ((𝑄‘𝑚)‘𝑦) = ((𝑄‘𝑚)‘𝑦)) |
125 | | eqidd 2738 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → ((𝑄‘(𝑚 + 1))‘𝑦) = ((𝑄‘(𝑚 + 1))‘𝑦)) |
126 | 122, 123,
85, 85, 10, 124, 125 | ofrfval 7478 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑄‘𝑚) ∘r ≤ (𝑄‘(𝑚 + 1)) ↔ ∀𝑦 ∈ ℝ ((𝑄‘𝑚)‘𝑦) ≤ ((𝑄‘(𝑚 + 1))‘𝑦))) |
127 | 121, 126 | mpbid 235 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ∀𝑦 ∈ ℝ ((𝑄‘𝑚)‘𝑦) ≤ ((𝑄‘(𝑚 + 1))‘𝑦)) |
128 | 127 | r19.21bi 3130 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → ((𝑄‘𝑚)‘𝑦) ≤ ((𝑄‘(𝑚 + 1))‘𝑦)) |
129 | 98, 101, 107, 112, 120, 128 | le2addd 11451 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (((𝑃‘𝑚)‘𝑦) + ((𝑄‘𝑚)‘𝑦)) ≤ (((𝑃‘(𝑚 + 1))‘𝑦) + ((𝑄‘(𝑚 + 1))‘𝑦))) |
130 | 129 | ralrimiva 3105 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ∀𝑦 ∈ ℝ (((𝑃‘𝑚)‘𝑦) + ((𝑄‘𝑚)‘𝑦)) ≤ (((𝑃‘(𝑚 + 1))‘𝑦) + ((𝑄‘(𝑚 + 1))‘𝑦))) |
131 | 24, 70 | i1fadd 24592 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑃‘𝑚) ∘f + (𝑄‘𝑚)) ∈ dom
∫1) |
132 | | i1ff 24573 |
. . . . . . . . 9
⊢ (((𝑃‘𝑚) ∘f + (𝑄‘𝑚)) ∈ dom ∫1 →
((𝑃‘𝑚) ∘f + (𝑄‘𝑚)):ℝ⟶ℝ) |
133 | | ffn 6545 |
. . . . . . . . 9
⊢ (((𝑃‘𝑚) ∘f + (𝑄‘𝑚)):ℝ⟶ℝ → ((𝑃‘𝑚) ∘f + (𝑄‘𝑚)) Fn ℝ) |
134 | 131, 132,
133 | 3syl 18 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑃‘𝑚) ∘f + (𝑄‘𝑚)) Fn ℝ) |
135 | 104, 109 | i1fadd 24592 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑃‘(𝑚 + 1)) ∘f + (𝑄‘(𝑚 + 1))) ∈ dom
∫1) |
136 | | i1ff 24573 |
. . . . . . . . . 10
⊢ (((𝑃‘(𝑚 + 1)) ∘f + (𝑄‘(𝑚 + 1))) ∈ dom ∫1 →
((𝑃‘(𝑚 + 1)) ∘f +
(𝑄‘(𝑚 +
1))):ℝ⟶ℝ) |
137 | 135, 136 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑃‘(𝑚 + 1)) ∘f + (𝑄‘(𝑚 +
1))):ℝ⟶ℝ) |
138 | 137 | ffnd 6546 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑃‘(𝑚 + 1)) ∘f + (𝑄‘(𝑚 + 1))) Fn ℝ) |
139 | 114, 122,
85, 85, 10, 116, 124 | ofval 7479 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (((𝑃‘𝑚) ∘f + (𝑄‘𝑚))‘𝑦) = (((𝑃‘𝑚)‘𝑦) + ((𝑄‘𝑚)‘𝑦))) |
140 | 115, 123,
85, 85, 10, 117, 125 | ofval 7479 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (((𝑃‘(𝑚 + 1)) ∘f + (𝑄‘(𝑚 + 1)))‘𝑦) = (((𝑃‘(𝑚 + 1))‘𝑦) + ((𝑄‘(𝑚 + 1))‘𝑦))) |
141 | 134, 138,
85, 85, 10, 139, 140 | ofrfval 7478 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (((𝑃‘𝑚) ∘f + (𝑄‘𝑚)) ∘r ≤ ((𝑃‘(𝑚 + 1)) ∘f + (𝑄‘(𝑚 + 1))) ↔ ∀𝑦 ∈ ℝ (((𝑃‘𝑚)‘𝑦) + ((𝑄‘𝑚)‘𝑦)) ≤ (((𝑃‘(𝑚 + 1))‘𝑦) + ((𝑄‘(𝑚 + 1))‘𝑦)))) |
142 | 130, 141 | mpbird 260 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑃‘𝑚) ∘f + (𝑄‘𝑚)) ∘r ≤ ((𝑃‘(𝑚 + 1)) ∘f + (𝑄‘(𝑚 + 1)))) |
143 | | eqidd 2738 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑚 + 1) ∈ ℕ) → (𝑃‘(𝑚 + 1)) = (𝑃‘(𝑚 + 1))) |
144 | | eqidd 2738 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑚 + 1) ∈ ℕ) → (𝑄‘(𝑚 + 1)) = (𝑄‘(𝑚 + 1))) |
145 | 90, 91, 19, 19, 20, 143, 144 | ofval 7479 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 + 1) ∈ ℕ) → ((𝑃 ∘f
∘f + 𝑄)‘(𝑚 + 1)) = ((𝑃‘(𝑚 + 1)) ∘f + (𝑄‘(𝑚 + 1)))) |
146 | 102, 145 | sylan2 596 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑃 ∘f ∘f +
𝑄)‘(𝑚 + 1)) = ((𝑃‘(𝑚 + 1)) ∘f + (𝑄‘(𝑚 + 1)))) |
147 | 142, 94, 146 | 3brtr4d 5085 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑃 ∘f ∘f +
𝑄)‘𝑚) ∘r ≤ ((𝑃 ∘f
∘f + 𝑄)‘(𝑚 + 1))) |
148 | 95, 147 | jca 515 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) →
(0𝑝 ∘r ≤ ((𝑃 ∘f ∘f +
𝑄)‘𝑚) ∧ ((𝑃 ∘f ∘f +
𝑄)‘𝑚) ∘r ≤ ((𝑃 ∘f
∘f + 𝑄)‘(𝑚 + 1)))) |
149 | 148 | ralrimiva 3105 |
. . 3
⊢ (𝜑 → ∀𝑚 ∈ ℕ (0𝑝
∘r ≤ ((𝑃 ∘f ∘f +
𝑄)‘𝑚) ∧ ((𝑃 ∘f ∘f +
𝑄)‘𝑚) ∘r ≤ ((𝑃 ∘f
∘f + 𝑄)‘(𝑚 + 1)))) |
150 | | fveq2 6717 |
. . . . . . . 8
⊢ (𝑛 = 𝑚 → ((𝑃 ∘f ∘f +
𝑄)‘𝑛) = ((𝑃 ∘f ∘f +
𝑄)‘𝑚)) |
151 | 150 | fveq1d 6719 |
. . . . . . 7
⊢ (𝑛 = 𝑚 → (((𝑃 ∘f ∘f +
𝑄)‘𝑛)‘𝑦) = (((𝑃 ∘f ∘f +
𝑄)‘𝑚)‘𝑦)) |
152 | 151 | cbvmptv 5158 |
. . . . . 6
⊢ (𝑛 ∈ ℕ ↦ (((𝑃 ∘f
∘f + 𝑄)‘𝑛)‘𝑦)) = (𝑚 ∈ ℕ ↦ (((𝑃 ∘f ∘f +
𝑄)‘𝑚)‘𝑦)) |
153 | | nnuz 12477 |
. . . . . . 7
⊢ ℕ =
(ℤ≥‘1) |
154 | | 1zzd 12208 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 1 ∈
ℤ) |
155 | | itg2add.p3 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)) |
156 | | fveq2 6717 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → ((𝑃‘𝑛)‘𝑥) = ((𝑃‘𝑛)‘𝑦)) |
157 | 156 | mpteq2dv 5151 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑦))) |
158 | | fveq2 6717 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝐹‘𝑥) = (𝐹‘𝑦)) |
159 | 157, 158 | breq12d 5066 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → ((𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥) ↔ (𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑦)) ⇝ (𝐹‘𝑦))) |
160 | 159 | rspccva 3536 |
. . . . . . . 8
⊢
((∀𝑥 ∈
ℝ (𝑛 ∈ ℕ
↦ ((𝑃‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥) ∧ 𝑦 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑦)) ⇝ (𝐹‘𝑦)) |
161 | 155, 160 | sylan 583 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑦)) ⇝ (𝐹‘𝑦)) |
162 | 18 | mptex 7039 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ ↦ (((𝑃 ∘f
∘f + 𝑄)‘𝑛)‘𝑦)) ∈ V |
163 | 162 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑛 ∈ ℕ ↦ (((𝑃 ∘f ∘f +
𝑄)‘𝑛)‘𝑦)) ∈ V) |
164 | | itg2add.q3 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑄‘𝑛)‘𝑥)) ⇝ (𝐺‘𝑥)) |
165 | | fveq2 6717 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → ((𝑄‘𝑛)‘𝑥) = ((𝑄‘𝑛)‘𝑦)) |
166 | 165 | mpteq2dv 5151 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑛 ∈ ℕ ↦ ((𝑄‘𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ ((𝑄‘𝑛)‘𝑦))) |
167 | | fveq2 6717 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝐺‘𝑥) = (𝐺‘𝑦)) |
168 | 166, 167 | breq12d 5066 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → ((𝑛 ∈ ℕ ↦ ((𝑄‘𝑛)‘𝑥)) ⇝ (𝐺‘𝑥) ↔ (𝑛 ∈ ℕ ↦ ((𝑄‘𝑛)‘𝑦)) ⇝ (𝐺‘𝑦))) |
169 | 168 | rspccva 3536 |
. . . . . . . 8
⊢
((∀𝑥 ∈
ℝ (𝑛 ∈ ℕ
↦ ((𝑄‘𝑛)‘𝑥)) ⇝ (𝐺‘𝑥) ∧ 𝑦 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((𝑄‘𝑛)‘𝑦)) ⇝ (𝐺‘𝑦)) |
170 | 164, 169 | sylan 583 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((𝑄‘𝑛)‘𝑦)) ⇝ (𝐺‘𝑦)) |
171 | 26 | fveq1d 6719 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑚 → ((𝑃‘𝑛)‘𝑦) = ((𝑃‘𝑚)‘𝑦)) |
172 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑦)) = (𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑦)) |
173 | | fvex 6730 |
. . . . . . . . . . 11
⊢ ((𝑃‘𝑚)‘𝑦) ∈ V |
174 | 171, 172,
173 | fvmpt 6818 |
. . . . . . . . . 10
⊢ (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑦))‘𝑚) = ((𝑃‘𝑚)‘𝑦)) |
175 | 174 | adantl 485 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑦))‘𝑚) = ((𝑃‘𝑚)‘𝑦)) |
176 | 98 | an32s 652 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → ((𝑃‘𝑚)‘𝑦) ∈ ℝ) |
177 | 175, 176 | eqeltrd 2838 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑦))‘𝑚) ∈ ℝ) |
178 | 177 | recnd 10861 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑦))‘𝑚) ∈ ℂ) |
179 | 72 | fveq1d 6719 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑚 → ((𝑄‘𝑛)‘𝑦) = ((𝑄‘𝑚)‘𝑦)) |
180 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ ↦ ((𝑄‘𝑛)‘𝑦)) = (𝑛 ∈ ℕ ↦ ((𝑄‘𝑛)‘𝑦)) |
181 | | fvex 6730 |
. . . . . . . . . . 11
⊢ ((𝑄‘𝑚)‘𝑦) ∈ V |
182 | 179, 180,
181 | fvmpt 6818 |
. . . . . . . . . 10
⊢ (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((𝑄‘𝑛)‘𝑦))‘𝑚) = ((𝑄‘𝑚)‘𝑦)) |
183 | 182 | adantl 485 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝑄‘𝑛)‘𝑦))‘𝑚) = ((𝑄‘𝑚)‘𝑦)) |
184 | 101 | an32s 652 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → ((𝑄‘𝑚)‘𝑦) ∈ ℝ) |
185 | 183, 184 | eqeltrd 2838 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝑄‘𝑛)‘𝑦))‘𝑚) ∈ ℝ) |
186 | 185 | recnd 10861 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝑄‘𝑛)‘𝑦))‘𝑚) ∈ ℂ) |
187 | 94 | fveq1d 6719 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (((𝑃 ∘f ∘f +
𝑄)‘𝑚)‘𝑦) = (((𝑃‘𝑚) ∘f + (𝑄‘𝑚))‘𝑦)) |
188 | 187 | adantr 484 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (((𝑃 ∘f ∘f +
𝑄)‘𝑚)‘𝑦) = (((𝑃‘𝑚) ∘f + (𝑄‘𝑚))‘𝑦)) |
189 | 188, 139 | eqtrd 2777 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (((𝑃 ∘f ∘f +
𝑄)‘𝑚)‘𝑦) = (((𝑃‘𝑚)‘𝑦) + ((𝑄‘𝑚)‘𝑦))) |
190 | 189 | an32s 652 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → (((𝑃 ∘f ∘f +
𝑄)‘𝑚)‘𝑦) = (((𝑃‘𝑚)‘𝑦) + ((𝑄‘𝑚)‘𝑦))) |
191 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ ↦ (((𝑃 ∘f
∘f + 𝑄)‘𝑛)‘𝑦)) = (𝑛 ∈ ℕ ↦ (((𝑃 ∘f ∘f +
𝑄)‘𝑛)‘𝑦)) |
192 | | fvex 6730 |
. . . . . . . . . 10
⊢ (((𝑃 ∘f
∘f + 𝑄)‘𝑚)‘𝑦) ∈ V |
193 | 151, 191,
192 | fvmpt 6818 |
. . . . . . . . 9
⊢ (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (((𝑃 ∘f
∘f + 𝑄)‘𝑛)‘𝑦))‘𝑚) = (((𝑃 ∘f ∘f +
𝑄)‘𝑚)‘𝑦)) |
194 | 193 | adantl 485 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (((𝑃 ∘f ∘f +
𝑄)‘𝑛)‘𝑦))‘𝑚) = (((𝑃 ∘f ∘f +
𝑄)‘𝑚)‘𝑦)) |
195 | 175, 183 | oveq12d 7231 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → (((𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑦))‘𝑚) + ((𝑛 ∈ ℕ ↦ ((𝑄‘𝑛)‘𝑦))‘𝑚)) = (((𝑃‘𝑚)‘𝑦) + ((𝑄‘𝑚)‘𝑦))) |
196 | 190, 194,
195 | 3eqtr4d 2787 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (((𝑃 ∘f ∘f +
𝑄)‘𝑛)‘𝑦))‘𝑚) = (((𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑦))‘𝑚) + ((𝑛 ∈ ℕ ↦ ((𝑄‘𝑛)‘𝑦))‘𝑚))) |
197 | 153, 154,
161, 163, 170, 178, 186, 196 | climadd 15193 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑛 ∈ ℕ ↦ (((𝑃 ∘f ∘f +
𝑄)‘𝑛)‘𝑦)) ⇝ ((𝐹‘𝑦) + (𝐺‘𝑦))) |
198 | 152, 197 | eqbrtrrid 5089 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑚 ∈ ℕ ↦ (((𝑃 ∘f ∘f +
𝑄)‘𝑚)‘𝑦)) ⇝ ((𝐹‘𝑦) + (𝐺‘𝑦))) |
199 | 6 | ffnd 6546 |
. . . . . 6
⊢ (𝜑 → 𝐹 Fn ℝ) |
200 | 7 | ffnd 6546 |
. . . . . 6
⊢ (𝜑 → 𝐺 Fn ℝ) |
201 | | eqidd 2738 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐹‘𝑦) = (𝐹‘𝑦)) |
202 | | eqidd 2738 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐺‘𝑦) = (𝐺‘𝑦)) |
203 | 199, 200,
9, 9, 10, 201, 202 | ofval 7479 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((𝐹 ∘f + 𝐺)‘𝑦) = ((𝐹‘𝑦) + (𝐺‘𝑦))) |
204 | 198, 203 | breqtrrd 5081 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑚 ∈ ℕ ↦ (((𝑃 ∘f ∘f +
𝑄)‘𝑚)‘𝑦)) ⇝ ((𝐹 ∘f + 𝐺)‘𝑦)) |
205 | 204 | ralrimiva 3105 |
. . 3
⊢ (𝜑 → ∀𝑦 ∈ ℝ (𝑚 ∈ ℕ ↦ (((𝑃 ∘f ∘f +
𝑄)‘𝑚)‘𝑦)) ⇝ ((𝐹 ∘f + 𝐺)‘𝑦)) |
206 | | 2fveq3 6722 |
. . . 4
⊢ (𝑛 = 𝑗 → (∫1‘((𝑃 ∘f
∘f + 𝑄)‘𝑛)) = (∫1‘((𝑃 ∘f
∘f + 𝑄)‘𝑗))) |
207 | 206 | cbvmptv 5158 |
. . 3
⊢ (𝑛 ∈ ℕ ↦
(∫1‘((𝑃 ∘f ∘f +
𝑄)‘𝑛))) = (𝑗 ∈ ℕ ↦
(∫1‘((𝑃 ∘f ∘f +
𝑄)‘𝑗))) |
208 | | itg2add.f3 |
. . . 4
⊢ (𝜑 →
(∫2‘𝐹)
∈ ℝ) |
209 | | itg2add.g3 |
. . . 4
⊢ (𝜑 →
(∫2‘𝐺)
∈ ℝ) |
210 | 208, 209 | readdcld 10862 |
. . 3
⊢ (𝜑 →
((∫2‘𝐹) + (∫2‘𝐺)) ∈
ℝ) |
211 | 94 | fveq2d 6721 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) →
(∫1‘((𝑃 ∘f ∘f +
𝑄)‘𝑚)) = (∫1‘((𝑃‘𝑚) ∘f + (𝑄‘𝑚)))) |
212 | 24, 70 | itg1add 24599 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) →
(∫1‘((𝑃‘𝑚) ∘f + (𝑄‘𝑚))) = ((∫1‘(𝑃‘𝑚)) + (∫1‘(𝑄‘𝑚)))) |
213 | 211, 212 | eqtrd 2777 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) →
(∫1‘((𝑃 ∘f ∘f +
𝑄)‘𝑚)) = ((∫1‘(𝑃‘𝑚)) + (∫1‘(𝑄‘𝑚)))) |
214 | | itg1cl 24582 |
. . . . . . . 8
⊢ ((𝑃‘𝑚) ∈ dom ∫1 →
(∫1‘(𝑃‘𝑚)) ∈ ℝ) |
215 | 24, 214 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) →
(∫1‘(𝑃‘𝑚)) ∈ ℝ) |
216 | | itg1cl 24582 |
. . . . . . . 8
⊢ ((𝑄‘𝑚) ∈ dom ∫1 →
(∫1‘(𝑄‘𝑚)) ∈ ℝ) |
217 | 70, 216 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) →
(∫1‘(𝑄‘𝑚)) ∈ ℝ) |
218 | 208 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) →
(∫2‘𝐹)
∈ ℝ) |
219 | 209 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) →
(∫2‘𝐺)
∈ ℝ) |
220 | 6 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝐹:ℝ⟶(0[,)+∞)) |
221 | | icossicc 13024 |
. . . . . . . . 9
⊢
(0[,)+∞) ⊆ (0[,]+∞) |
222 | | fss 6562 |
. . . . . . . . 9
⊢ ((𝐹:ℝ⟶(0[,)+∞)
∧ (0[,)+∞) ⊆ (0[,]+∞)) → 𝐹:ℝ⟶(0[,]+∞)) |
223 | 220, 221,
222 | sylancl 589 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝐹:ℝ⟶(0[,]+∞)) |
224 | 1, 6, 16, 25, 155 | itg2i1fseqle 24652 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑃‘𝑚) ∘r ≤ 𝐹) |
225 | | itg2ub 24631 |
. . . . . . . 8
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ (𝑃‘𝑚) ∈ dom ∫1
∧ (𝑃‘𝑚) ∘r ≤ 𝐹) →
(∫1‘(𝑃‘𝑚)) ≤ (∫2‘𝐹)) |
226 | 223, 24, 224, 225 | syl3anc 1373 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) →
(∫1‘(𝑃‘𝑚)) ≤ (∫2‘𝐹)) |
227 | 7 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝐺:ℝ⟶(0[,)+∞)) |
228 | | fss 6562 |
. . . . . . . . 9
⊢ ((𝐺:ℝ⟶(0[,)+∞)
∧ (0[,)+∞) ⊆ (0[,]+∞)) → 𝐺:ℝ⟶(0[,]+∞)) |
229 | 227, 221,
228 | sylancl 589 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝐺:ℝ⟶(0[,]+∞)) |
230 | 2, 7, 17, 71, 164 | itg2i1fseqle 24652 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑄‘𝑚) ∘r ≤ 𝐺) |
231 | | itg2ub 24631 |
. . . . . . . 8
⊢ ((𝐺:ℝ⟶(0[,]+∞)
∧ (𝑄‘𝑚) ∈ dom ∫1
∧ (𝑄‘𝑚) ∘r ≤ 𝐺) →
(∫1‘(𝑄‘𝑚)) ≤ (∫2‘𝐺)) |
232 | 229, 70, 230, 231 | syl3anc 1373 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) →
(∫1‘(𝑄‘𝑚)) ≤ (∫2‘𝐺)) |
233 | 215, 217,
218, 219, 226, 232 | le2addd 11451 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) →
((∫1‘(𝑃‘𝑚)) + (∫1‘(𝑄‘𝑚))) ≤ ((∫2‘𝐹) +
(∫2‘𝐺))) |
234 | 213, 233 | eqbrtrd 5075 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) →
(∫1‘((𝑃 ∘f ∘f +
𝑄)‘𝑚)) ≤ ((∫2‘𝐹) +
(∫2‘𝐺))) |
235 | 234 | ralrimiva 3105 |
. . . 4
⊢ (𝜑 → ∀𝑚 ∈ ℕ
(∫1‘((𝑃 ∘f ∘f +
𝑄)‘𝑚)) ≤ ((∫2‘𝐹) +
(∫2‘𝐺))) |
236 | | 2fveq3 6722 |
. . . . . 6
⊢ (𝑚 = 𝑘 → (∫1‘((𝑃 ∘f
∘f + 𝑄)‘𝑚)) = (∫1‘((𝑃 ∘f
∘f + 𝑄)‘𝑘))) |
237 | 236 | breq1d 5063 |
. . . . 5
⊢ (𝑚 = 𝑘 → ((∫1‘((𝑃 ∘f
∘f + 𝑄)‘𝑚)) ≤ ((∫2‘𝐹) +
(∫2‘𝐺)) ↔ (∫1‘((𝑃 ∘f
∘f + 𝑄)‘𝑘)) ≤ ((∫2‘𝐹) +
(∫2‘𝐺)))) |
238 | 237 | rspccva 3536 |
. . . 4
⊢
((∀𝑚 ∈
ℕ (∫1‘((𝑃 ∘f ∘f +
𝑄)‘𝑚)) ≤ ((∫2‘𝐹) +
(∫2‘𝐺)) ∧ 𝑘 ∈ ℕ) →
(∫1‘((𝑃 ∘f ∘f +
𝑄)‘𝑘)) ≤ ((∫2‘𝐹) +
(∫2‘𝐺))) |
239 | 235, 238 | sylan 583 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) →
(∫1‘((𝑃 ∘f ∘f +
𝑄)‘𝑘)) ≤ ((∫2‘𝐹) +
(∫2‘𝐺))) |
240 | 3, 11, 21, 149, 205, 207, 210, 239 | itg2i1fseq2 24654 |
. 2
⊢ (𝜑 → (𝑛 ∈ ℕ ↦
(∫1‘((𝑃 ∘f ∘f +
𝑄)‘𝑛))) ⇝ (∫2‘(𝐹 ∘f + 𝐺))) |
241 | | 1zzd 12208 |
. . 3
⊢ (𝜑 → 1 ∈
ℤ) |
242 | | eqid 2737 |
. . . 4
⊢ (𝑘 ∈ ℕ ↦
(∫1‘(𝑃‘𝑘))) = (𝑘 ∈ ℕ ↦
(∫1‘(𝑃‘𝑘))) |
243 | 1, 6, 16, 25, 155, 242, 208 | itg2i1fseq3 24655 |
. . 3
⊢ (𝜑 → (𝑘 ∈ ℕ ↦
(∫1‘(𝑃‘𝑘))) ⇝ (∫2‘𝐹)) |
244 | 18 | mptex 7039 |
. . . 4
⊢ (𝑛 ∈ ℕ ↦
(∫1‘((𝑃 ∘f ∘f +
𝑄)‘𝑛))) ∈ V |
245 | 244 | a1i 11 |
. . 3
⊢ (𝜑 → (𝑛 ∈ ℕ ↦
(∫1‘((𝑃 ∘f ∘f +
𝑄)‘𝑛))) ∈ V) |
246 | | eqid 2737 |
. . . 4
⊢ (𝑘 ∈ ℕ ↦
(∫1‘(𝑄‘𝑘))) = (𝑘 ∈ ℕ ↦
(∫1‘(𝑄‘𝑘))) |
247 | 2, 7, 17, 71, 164, 246, 209 | itg2i1fseq3 24655 |
. . 3
⊢ (𝜑 → (𝑘 ∈ ℕ ↦
(∫1‘(𝑄‘𝑘))) ⇝ (∫2‘𝐺)) |
248 | | 2fveq3 6722 |
. . . . . 6
⊢ (𝑘 = 𝑚 → (∫1‘(𝑃‘𝑘)) = (∫1‘(𝑃‘𝑚))) |
249 | | fvex 6730 |
. . . . . 6
⊢
(∫1‘(𝑃‘𝑚)) ∈ V |
250 | 248, 242,
249 | fvmpt 6818 |
. . . . 5
⊢ (𝑚 ∈ ℕ → ((𝑘 ∈ ℕ ↦
(∫1‘(𝑃‘𝑘)))‘𝑚) = (∫1‘(𝑃‘𝑚))) |
251 | 250 | adantl 485 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑘 ∈ ℕ ↦
(∫1‘(𝑃‘𝑘)))‘𝑚) = (∫1‘(𝑃‘𝑚))) |
252 | 215 | recnd 10861 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) →
(∫1‘(𝑃‘𝑚)) ∈ ℂ) |
253 | 251, 252 | eqeltrd 2838 |
. . 3
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑘 ∈ ℕ ↦
(∫1‘(𝑃‘𝑘)))‘𝑚) ∈ ℂ) |
254 | | 2fveq3 6722 |
. . . . . 6
⊢ (𝑘 = 𝑚 → (∫1‘(𝑄‘𝑘)) = (∫1‘(𝑄‘𝑚))) |
255 | | fvex 6730 |
. . . . . 6
⊢
(∫1‘(𝑄‘𝑚)) ∈ V |
256 | 254, 246,
255 | fvmpt 6818 |
. . . . 5
⊢ (𝑚 ∈ ℕ → ((𝑘 ∈ ℕ ↦
(∫1‘(𝑄‘𝑘)))‘𝑚) = (∫1‘(𝑄‘𝑚))) |
257 | 256 | adantl 485 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑘 ∈ ℕ ↦
(∫1‘(𝑄‘𝑘)))‘𝑚) = (∫1‘(𝑄‘𝑚))) |
258 | 217 | recnd 10861 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) →
(∫1‘(𝑄‘𝑚)) ∈ ℂ) |
259 | 257, 258 | eqeltrd 2838 |
. . 3
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑘 ∈ ℕ ↦
(∫1‘(𝑄‘𝑘)))‘𝑚) ∈ ℂ) |
260 | | 2fveq3 6722 |
. . . . . 6
⊢ (𝑗 = 𝑚 → (∫1‘((𝑃 ∘f
∘f + 𝑄)‘𝑗)) = (∫1‘((𝑃 ∘f
∘f + 𝑄)‘𝑚))) |
261 | | fvex 6730 |
. . . . . 6
⊢
(∫1‘((𝑃 ∘f ∘f +
𝑄)‘𝑚)) ∈ V |
262 | 260, 207,
261 | fvmpt 6818 |
. . . . 5
⊢ (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦
(∫1‘((𝑃 ∘f ∘f +
𝑄)‘𝑛)))‘𝑚) = (∫1‘((𝑃 ∘f
∘f + 𝑄)‘𝑚))) |
263 | 262 | adantl 485 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦
(∫1‘((𝑃 ∘f ∘f +
𝑄)‘𝑛)))‘𝑚) = (∫1‘((𝑃 ∘f
∘f + 𝑄)‘𝑚))) |
264 | 251, 257 | oveq12d 7231 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (((𝑘 ∈ ℕ ↦
(∫1‘(𝑃‘𝑘)))‘𝑚) + ((𝑘 ∈ ℕ ↦
(∫1‘(𝑄‘𝑘)))‘𝑚)) = ((∫1‘(𝑃‘𝑚)) + (∫1‘(𝑄‘𝑚)))) |
265 | 213, 263,
264 | 3eqtr4d 2787 |
. . 3
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦
(∫1‘((𝑃 ∘f ∘f +
𝑄)‘𝑛)))‘𝑚) = (((𝑘 ∈ ℕ ↦
(∫1‘(𝑃‘𝑘)))‘𝑚) + ((𝑘 ∈ ℕ ↦
(∫1‘(𝑄‘𝑘)))‘𝑚))) |
266 | 153, 241,
243, 245, 247, 253, 259, 265 | climadd 15193 |
. 2
⊢ (𝜑 → (𝑛 ∈ ℕ ↦
(∫1‘((𝑃 ∘f ∘f +
𝑄)‘𝑛))) ⇝ ((∫2‘𝐹) +
(∫2‘𝐺))) |
267 | | climuni 15113 |
. 2
⊢ (((𝑛 ∈ ℕ ↦
(∫1‘((𝑃 ∘f ∘f +
𝑄)‘𝑛))) ⇝ (∫2‘(𝐹 ∘f + 𝐺)) ∧ (𝑛 ∈ ℕ ↦
(∫1‘((𝑃 ∘f ∘f +
𝑄)‘𝑛))) ⇝ ((∫2‘𝐹) +
(∫2‘𝐺))) → (∫2‘(𝐹 ∘f + 𝐺)) =
((∫2‘𝐹) + (∫2‘𝐺))) |
268 | 240, 266,
267 | syl2anc 587 |
1
⊢ (𝜑 →
(∫2‘(𝐹
∘f + 𝐺)) =
((∫2‘𝐹) + (∫2‘𝐺))) |