Step | Hyp | Ref
| Expression |
1 | | itg2add.f1 |
. . . 4
⊢ (𝜑 → 𝐹 ∈ MblFn) |
2 | | itg2add.g1 |
. . . 4
⊢ (𝜑 → 𝐺 ∈ MblFn) |
3 | 1, 2 | mbfadd 23234 |
. . 3
⊢ (𝜑 → (𝐹 ∘𝑓 + 𝐺) ∈ MblFn) |
4 | | ge0addcl 12155 |
. . . . 5
⊢ ((𝑦 ∈ (0[,)+∞) ∧
𝑧 ∈ (0[,)+∞))
→ (𝑦 + 𝑧) ∈
(0[,)+∞)) |
5 | 4 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ (𝑦 ∈ (0[,)+∞) ∧ 𝑧 ∈ (0[,)+∞))) →
(𝑦 + 𝑧) ∈ (0[,)+∞)) |
6 | | itg2add.f2 |
. . . 4
⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞)) |
7 | | itg2add.g2 |
. . . 4
⊢ (𝜑 → 𝐺:ℝ⟶(0[,)+∞)) |
8 | | reex 9906 |
. . . . 5
⊢ ℝ
∈ V |
9 | 8 | a1i 11 |
. . . 4
⊢ (𝜑 → ℝ ∈
V) |
10 | | inidm 3784 |
. . . 4
⊢ (ℝ
∩ ℝ) = ℝ |
11 | 5, 6, 7, 9, 9, 10 | off 6810 |
. . 3
⊢ (𝜑 → (𝐹 ∘𝑓 + 𝐺):ℝ⟶(0[,)+∞)) |
12 | | simpl 472 |
. . . . . 6
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → 𝑓
∈ dom ∫1) |
13 | | simpr 476 |
. . . . . 6
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → 𝑔
∈ dom ∫1) |
14 | 12, 13 | i1fadd 23268 |
. . . . 5
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (𝑓 ∘𝑓 + 𝑔) ∈ dom
∫1) |
15 | 14 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ (𝑓
∘𝑓 + 𝑔) ∈ dom
∫1) |
16 | | itg2add.p1 |
. . . 4
⊢ (𝜑 → 𝑃:ℕ⟶dom
∫1) |
17 | | itg2add.q1 |
. . . 4
⊢ (𝜑 → 𝑄:ℕ⟶dom
∫1) |
18 | | nnex 10903 |
. . . . 5
⊢ ℕ
∈ V |
19 | 18 | a1i 11 |
. . . 4
⊢ (𝜑 → ℕ ∈
V) |
20 | | inidm 3784 |
. . . 4
⊢ (ℕ
∩ ℕ) = ℕ |
21 | 15, 16, 17, 19, 19, 20 | off 6810 |
. . 3
⊢ (𝜑 → (𝑃 ∘𝑓
∘𝑓 + 𝑄):ℕ⟶dom
∫1) |
22 | | ge0addcl 12155 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ (0[,)+∞) ∧
𝑔 ∈ (0[,)+∞))
→ (𝑓 + 𝑔) ∈
(0[,)+∞)) |
23 | 22 | adantl 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓 ∈ (0[,)+∞) ∧ 𝑔 ∈ (0[,)+∞))) →
(𝑓 + 𝑔) ∈ (0[,)+∞)) |
24 | 16 | ffvelrnda 6267 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑃‘𝑚) ∈ dom
∫1) |
25 | | itg2add.p2 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑛 ∈ ℕ (0𝑝
∘𝑟 ≤ (𝑃‘𝑛) ∧ (𝑃‘𝑛) ∘𝑟 ≤ (𝑃‘(𝑛 + 1)))) |
26 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑚 → (𝑃‘𝑛) = (𝑃‘𝑚)) |
27 | 26 | breq2d 4595 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑚 → (0𝑝
∘𝑟 ≤ (𝑃‘𝑛) ↔ 0𝑝
∘𝑟 ≤ (𝑃‘𝑚))) |
28 | | oveq1 6556 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑚 → (𝑛 + 1) = (𝑚 + 1)) |
29 | 28 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑚 → (𝑃‘(𝑛 + 1)) = (𝑃‘(𝑚 + 1))) |
30 | 26, 29 | breq12d 4596 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑚 → ((𝑃‘𝑛) ∘𝑟 ≤ (𝑃‘(𝑛 + 1)) ↔ (𝑃‘𝑚) ∘𝑟 ≤ (𝑃‘(𝑚 + 1)))) |
31 | 27, 30 | anbi12d 743 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑚 → ((0𝑝
∘𝑟 ≤ (𝑃‘𝑛) ∧ (𝑃‘𝑛) ∘𝑟 ≤ (𝑃‘(𝑛 + 1))) ↔ (0𝑝
∘𝑟 ≤ (𝑃‘𝑚) ∧ (𝑃‘𝑚) ∘𝑟 ≤ (𝑃‘(𝑚 + 1))))) |
32 | 31 | rspccva 3281 |
. . . . . . . . . . . 12
⊢
((∀𝑛 ∈
ℕ (0𝑝 ∘𝑟 ≤ (𝑃‘𝑛) ∧ (𝑃‘𝑛) ∘𝑟 ≤ (𝑃‘(𝑛 + 1))) ∧ 𝑚 ∈ ℕ) →
(0𝑝 ∘𝑟 ≤ (𝑃‘𝑚) ∧ (𝑃‘𝑚) ∘𝑟 ≤ (𝑃‘(𝑚 + 1)))) |
33 | 25, 32 | sylan 487 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) →
(0𝑝 ∘𝑟 ≤ (𝑃‘𝑚) ∧ (𝑃‘𝑚) ∘𝑟 ≤ (𝑃‘(𝑚 + 1)))) |
34 | 33 | simpld 474 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 0𝑝
∘𝑟 ≤ (𝑃‘𝑚)) |
35 | | breq2 4587 |
. . . . . . . . . . . 12
⊢ (𝑓 = (𝑃‘𝑚) → (0𝑝
∘𝑟 ≤ 𝑓 ↔ 0𝑝
∘𝑟 ≤ (𝑃‘𝑚))) |
36 | | feq1 5939 |
. . . . . . . . . . . 12
⊢ (𝑓 = (𝑃‘𝑚) → (𝑓:ℝ⟶(0[,)+∞) ↔ (𝑃‘𝑚):ℝ⟶(0[,)+∞))) |
37 | 35, 36 | imbi12d 333 |
. . . . . . . . . . 11
⊢ (𝑓 = (𝑃‘𝑚) → ((0𝑝
∘𝑟 ≤ 𝑓 → 𝑓:ℝ⟶(0[,)+∞)) ↔
(0𝑝 ∘𝑟 ≤ (𝑃‘𝑚) → (𝑃‘𝑚):ℝ⟶(0[,)+∞)))) |
38 | | i1ff 23249 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 ∈ dom ∫1
→ 𝑓:ℝ⟶ℝ) |
39 | | ffn 5958 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:ℝ⟶ℝ →
𝑓 Fn
ℝ) |
40 | 38, 39 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑓 ∈ dom ∫1
→ 𝑓 Fn
ℝ) |
41 | 40 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑓 ∈ dom ∫1
∧ 0𝑝 ∘𝑟 ≤ 𝑓) → 𝑓 Fn ℝ) |
42 | | 0cn 9911 |
. . . . . . . . . . . . . . . . . . 19
⊢ 0 ∈
ℂ |
43 | | fnconstg 6006 |
. . . . . . . . . . . . . . . . . . 19
⊢ (0 ∈
ℂ → (ℂ × {0}) Fn ℂ) |
44 | 42, 43 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢ (ℂ
× {0}) Fn ℂ |
45 | | df-0p 23243 |
. . . . . . . . . . . . . . . . . . 19
⊢
0𝑝 = (ℂ × {0}) |
46 | 45 | fneq1i 5899 |
. . . . . . . . . . . . . . . . . 18
⊢
(0𝑝 Fn ℂ ↔ (ℂ × {0}) Fn
ℂ) |
47 | 44, 46 | mpbir 220 |
. . . . . . . . . . . . . . . . 17
⊢
0𝑝 Fn ℂ |
48 | 47 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 ∈ dom ∫1
→ 0𝑝 Fn ℂ) |
49 | | cnex 9896 |
. . . . . . . . . . . . . . . . 17
⊢ ℂ
∈ V |
50 | 49 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 ∈ dom ∫1
→ ℂ ∈ V) |
51 | 8 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 ∈ dom ∫1
→ ℝ ∈ V) |
52 | | ax-resscn 9872 |
. . . . . . . . . . . . . . . . 17
⊢ ℝ
⊆ ℂ |
53 | | sseqin2 3779 |
. . . . . . . . . . . . . . . . 17
⊢ (ℝ
⊆ ℂ ↔ (ℂ ∩ ℝ) = ℝ) |
54 | 52, 53 | mpbi 219 |
. . . . . . . . . . . . . . . 16
⊢ (ℂ
∩ ℝ) = ℝ |
55 | | 0pval 23244 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℂ →
(0𝑝‘𝑥) = 0) |
56 | 55 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑥 ∈ ℂ)
→ (0𝑝‘𝑥) = 0) |
57 | | eqidd 2611 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ (𝑓‘𝑥) = (𝑓‘𝑥)) |
58 | 48, 40, 50, 51, 54, 56, 57 | ofrfval 6803 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 ∈ dom ∫1
→ (0𝑝 ∘𝑟 ≤ 𝑓 ↔ ∀𝑥 ∈ ℝ 0 ≤ (𝑓‘𝑥))) |
59 | 58 | biimpa 500 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∈ dom ∫1
∧ 0𝑝 ∘𝑟 ≤ 𝑓) → ∀𝑥 ∈ ℝ 0 ≤ (𝑓‘𝑥)) |
60 | 38 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ (𝑓‘𝑥) ∈
ℝ) |
61 | | elrege0 12149 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓‘𝑥) ∈ (0[,)+∞) ↔ ((𝑓‘𝑥) ∈ ℝ ∧ 0 ≤ (𝑓‘𝑥))) |
62 | 61 | simplbi2 653 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓‘𝑥) ∈ ℝ → (0 ≤ (𝑓‘𝑥) → (𝑓‘𝑥) ∈ (0[,)+∞))) |
63 | 60, 62 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ (0 ≤ (𝑓‘𝑥) → (𝑓‘𝑥) ∈ (0[,)+∞))) |
64 | 63 | ralimdva 2945 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 ∈ dom ∫1
→ (∀𝑥 ∈
ℝ 0 ≤ (𝑓‘𝑥) → ∀𝑥 ∈ ℝ (𝑓‘𝑥) ∈ (0[,)+∞))) |
65 | 64 | imp 444 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∈ dom ∫1
∧ ∀𝑥 ∈
ℝ 0 ≤ (𝑓‘𝑥)) → ∀𝑥 ∈ ℝ (𝑓‘𝑥) ∈ (0[,)+∞)) |
66 | 59, 65 | syldan 486 |
. . . . . . . . . . . . 13
⊢ ((𝑓 ∈ dom ∫1
∧ 0𝑝 ∘𝑟 ≤ 𝑓) → ∀𝑥 ∈ ℝ (𝑓‘𝑥) ∈ (0[,)+∞)) |
67 | | ffnfv 6295 |
. . . . . . . . . . . . 13
⊢ (𝑓:ℝ⟶(0[,)+∞)
↔ (𝑓 Fn ℝ ∧
∀𝑥 ∈ ℝ
(𝑓‘𝑥) ∈ (0[,)+∞))) |
68 | 41, 66, 67 | sylanbrc 695 |
. . . . . . . . . . . 12
⊢ ((𝑓 ∈ dom ∫1
∧ 0𝑝 ∘𝑟 ≤ 𝑓) → 𝑓:ℝ⟶(0[,)+∞)) |
69 | 68 | ex 449 |
. . . . . . . . . . 11
⊢ (𝑓 ∈ dom ∫1
→ (0𝑝 ∘𝑟 ≤ 𝑓 → 𝑓:ℝ⟶(0[,)+∞))) |
70 | 37, 69 | vtoclga 3245 |
. . . . . . . . . 10
⊢ ((𝑃‘𝑚) ∈ dom ∫1 →
(0𝑝 ∘𝑟 ≤ (𝑃‘𝑚) → (𝑃‘𝑚):ℝ⟶(0[,)+∞))) |
71 | 24, 34, 70 | sylc 63 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑃‘𝑚):ℝ⟶(0[,)+∞)) |
72 | 17 | ffvelrnda 6267 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑄‘𝑚) ∈ dom
∫1) |
73 | | itg2add.q2 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑛 ∈ ℕ (0𝑝
∘𝑟 ≤ (𝑄‘𝑛) ∧ (𝑄‘𝑛) ∘𝑟 ≤ (𝑄‘(𝑛 + 1)))) |
74 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑚 → (𝑄‘𝑛) = (𝑄‘𝑚)) |
75 | 74 | breq2d 4595 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑚 → (0𝑝
∘𝑟 ≤ (𝑄‘𝑛) ↔ 0𝑝
∘𝑟 ≤ (𝑄‘𝑚))) |
76 | 28 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑚 → (𝑄‘(𝑛 + 1)) = (𝑄‘(𝑚 + 1))) |
77 | 74, 76 | breq12d 4596 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑚 → ((𝑄‘𝑛) ∘𝑟 ≤ (𝑄‘(𝑛 + 1)) ↔ (𝑄‘𝑚) ∘𝑟 ≤ (𝑄‘(𝑚 + 1)))) |
78 | 75, 77 | anbi12d 743 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑚 → ((0𝑝
∘𝑟 ≤ (𝑄‘𝑛) ∧ (𝑄‘𝑛) ∘𝑟 ≤ (𝑄‘(𝑛 + 1))) ↔ (0𝑝
∘𝑟 ≤ (𝑄‘𝑚) ∧ (𝑄‘𝑚) ∘𝑟 ≤ (𝑄‘(𝑚 + 1))))) |
79 | 78 | rspccva 3281 |
. . . . . . . . . . . 12
⊢
((∀𝑛 ∈
ℕ (0𝑝 ∘𝑟 ≤ (𝑄‘𝑛) ∧ (𝑄‘𝑛) ∘𝑟 ≤ (𝑄‘(𝑛 + 1))) ∧ 𝑚 ∈ ℕ) →
(0𝑝 ∘𝑟 ≤ (𝑄‘𝑚) ∧ (𝑄‘𝑚) ∘𝑟 ≤ (𝑄‘(𝑚 + 1)))) |
80 | 73, 79 | sylan 487 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) →
(0𝑝 ∘𝑟 ≤ (𝑄‘𝑚) ∧ (𝑄‘𝑚) ∘𝑟 ≤ (𝑄‘(𝑚 + 1)))) |
81 | 80 | simpld 474 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 0𝑝
∘𝑟 ≤ (𝑄‘𝑚)) |
82 | | breq2 4587 |
. . . . . . . . . . . 12
⊢ (𝑓 = (𝑄‘𝑚) → (0𝑝
∘𝑟 ≤ 𝑓 ↔ 0𝑝
∘𝑟 ≤ (𝑄‘𝑚))) |
83 | | feq1 5939 |
. . . . . . . . . . . 12
⊢ (𝑓 = (𝑄‘𝑚) → (𝑓:ℝ⟶(0[,)+∞) ↔ (𝑄‘𝑚):ℝ⟶(0[,)+∞))) |
84 | 82, 83 | imbi12d 333 |
. . . . . . . . . . 11
⊢ (𝑓 = (𝑄‘𝑚) → ((0𝑝
∘𝑟 ≤ 𝑓 → 𝑓:ℝ⟶(0[,)+∞)) ↔
(0𝑝 ∘𝑟 ≤ (𝑄‘𝑚) → (𝑄‘𝑚):ℝ⟶(0[,)+∞)))) |
85 | 84, 69 | vtoclga 3245 |
. . . . . . . . . 10
⊢ ((𝑄‘𝑚) ∈ dom ∫1 →
(0𝑝 ∘𝑟 ≤ (𝑄‘𝑚) → (𝑄‘𝑚):ℝ⟶(0[,)+∞))) |
86 | 72, 81, 85 | sylc 63 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑄‘𝑚):ℝ⟶(0[,)+∞)) |
87 | 8 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ℝ ∈
V) |
88 | 23, 71, 86, 87, 87, 10 | off 6810 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑃‘𝑚) ∘𝑓 + (𝑄‘𝑚)):ℝ⟶(0[,)+∞)) |
89 | | 0plef 23245 |
. . . . . . . 8
⊢ (((𝑃‘𝑚) ∘𝑓 + (𝑄‘𝑚)):ℝ⟶(0[,)+∞) ↔
(((𝑃‘𝑚) ∘𝑓 +
(𝑄‘𝑚)):ℝ⟶ℝ ∧
0𝑝 ∘𝑟 ≤ ((𝑃‘𝑚) ∘𝑓 + (𝑄‘𝑚)))) |
90 | 88, 89 | sylib 207 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (((𝑃‘𝑚) ∘𝑓 + (𝑄‘𝑚)):ℝ⟶ℝ ∧
0𝑝 ∘𝑟 ≤ ((𝑃‘𝑚) ∘𝑓 + (𝑄‘𝑚)))) |
91 | 90 | simprd 478 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 0𝑝
∘𝑟 ≤ ((𝑃‘𝑚) ∘𝑓 + (𝑄‘𝑚))) |
92 | | ffn 5958 |
. . . . . . . 8
⊢ (𝑃:ℕ⟶dom
∫1 → 𝑃
Fn ℕ) |
93 | 16, 92 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑃 Fn ℕ) |
94 | | ffn 5958 |
. . . . . . . 8
⊢ (𝑄:ℕ⟶dom
∫1 → 𝑄
Fn ℕ) |
95 | 17, 94 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑄 Fn ℕ) |
96 | | eqidd 2611 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑃‘𝑚) = (𝑃‘𝑚)) |
97 | | eqidd 2611 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑄‘𝑚) = (𝑄‘𝑚)) |
98 | 93, 95, 19, 19, 20, 96, 97 | ofval 6804 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑚) = ((𝑃‘𝑚) ∘𝑓 + (𝑄‘𝑚))) |
99 | 91, 98 | breqtrrd 4611 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 0𝑝
∘𝑟 ≤ ((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑚)) |
100 | | i1ff 23249 |
. . . . . . . . . . 11
⊢ ((𝑃‘𝑚) ∈ dom ∫1 → (𝑃‘𝑚):ℝ⟶ℝ) |
101 | 24, 100 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑃‘𝑚):ℝ⟶ℝ) |
102 | 101 | ffvelrnda 6267 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → ((𝑃‘𝑚)‘𝑦) ∈ ℝ) |
103 | | i1ff 23249 |
. . . . . . . . . . 11
⊢ ((𝑄‘𝑚) ∈ dom ∫1 → (𝑄‘𝑚):ℝ⟶ℝ) |
104 | 72, 103 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑄‘𝑚):ℝ⟶ℝ) |
105 | 104 | ffvelrnda 6267 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → ((𝑄‘𝑚)‘𝑦) ∈ ℝ) |
106 | | peano2nn 10909 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ ℕ → (𝑚 + 1) ∈
ℕ) |
107 | | ffvelrn 6265 |
. . . . . . . . . . . 12
⊢ ((𝑃:ℕ⟶dom
∫1 ∧ (𝑚
+ 1) ∈ ℕ) → (𝑃‘(𝑚 + 1)) ∈ dom
∫1) |
108 | 16, 106, 107 | syl2an 493 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑃‘(𝑚 + 1)) ∈ dom
∫1) |
109 | | i1ff 23249 |
. . . . . . . . . . 11
⊢ ((𝑃‘(𝑚 + 1)) ∈ dom ∫1 →
(𝑃‘(𝑚 +
1)):ℝ⟶ℝ) |
110 | 108, 109 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑃‘(𝑚 +
1)):ℝ⟶ℝ) |
111 | 110 | ffvelrnda 6267 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → ((𝑃‘(𝑚 + 1))‘𝑦) ∈ ℝ) |
112 | | ffvelrn 6265 |
. . . . . . . . . . . 12
⊢ ((𝑄:ℕ⟶dom
∫1 ∧ (𝑚
+ 1) ∈ ℕ) → (𝑄‘(𝑚 + 1)) ∈ dom
∫1) |
113 | 17, 106, 112 | syl2an 493 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑄‘(𝑚 + 1)) ∈ dom
∫1) |
114 | | i1ff 23249 |
. . . . . . . . . . 11
⊢ ((𝑄‘(𝑚 + 1)) ∈ dom ∫1 →
(𝑄‘(𝑚 +
1)):ℝ⟶ℝ) |
115 | 113, 114 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑄‘(𝑚 +
1)):ℝ⟶ℝ) |
116 | 115 | ffvelrnda 6267 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → ((𝑄‘(𝑚 + 1))‘𝑦) ∈ ℝ) |
117 | 33 | simprd 478 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑃‘𝑚) ∘𝑟 ≤ (𝑃‘(𝑚 + 1))) |
118 | | ffn 5958 |
. . . . . . . . . . . . 13
⊢ ((𝑃‘𝑚):ℝ⟶ℝ → (𝑃‘𝑚) Fn ℝ) |
119 | 101, 118 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑃‘𝑚) Fn ℝ) |
120 | | ffn 5958 |
. . . . . . . . . . . . 13
⊢ ((𝑃‘(𝑚 + 1)):ℝ⟶ℝ → (𝑃‘(𝑚 + 1)) Fn ℝ) |
121 | 110, 120 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑃‘(𝑚 + 1)) Fn ℝ) |
122 | | eqidd 2611 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → ((𝑃‘𝑚)‘𝑦) = ((𝑃‘𝑚)‘𝑦)) |
123 | | eqidd 2611 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → ((𝑃‘(𝑚 + 1))‘𝑦) = ((𝑃‘(𝑚 + 1))‘𝑦)) |
124 | 119, 121,
87, 87, 10, 122, 123 | ofrfval 6803 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑃‘𝑚) ∘𝑟 ≤ (𝑃‘(𝑚 + 1)) ↔ ∀𝑦 ∈ ℝ ((𝑃‘𝑚)‘𝑦) ≤ ((𝑃‘(𝑚 + 1))‘𝑦))) |
125 | 117, 124 | mpbid 221 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ∀𝑦 ∈ ℝ ((𝑃‘𝑚)‘𝑦) ≤ ((𝑃‘(𝑚 + 1))‘𝑦)) |
126 | 125 | r19.21bi 2916 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → ((𝑃‘𝑚)‘𝑦) ≤ ((𝑃‘(𝑚 + 1))‘𝑦)) |
127 | 80 | simprd 478 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑄‘𝑚) ∘𝑟 ≤ (𝑄‘(𝑚 + 1))) |
128 | | ffn 5958 |
. . . . . . . . . . . . 13
⊢ ((𝑄‘𝑚):ℝ⟶ℝ → (𝑄‘𝑚) Fn ℝ) |
129 | 104, 128 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑄‘𝑚) Fn ℝ) |
130 | | ffn 5958 |
. . . . . . . . . . . . 13
⊢ ((𝑄‘(𝑚 + 1)):ℝ⟶ℝ → (𝑄‘(𝑚 + 1)) Fn ℝ) |
131 | 115, 130 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑄‘(𝑚 + 1)) Fn ℝ) |
132 | | eqidd 2611 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → ((𝑄‘𝑚)‘𝑦) = ((𝑄‘𝑚)‘𝑦)) |
133 | | eqidd 2611 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → ((𝑄‘(𝑚 + 1))‘𝑦) = ((𝑄‘(𝑚 + 1))‘𝑦)) |
134 | 129, 131,
87, 87, 10, 132, 133 | ofrfval 6803 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑄‘𝑚) ∘𝑟 ≤ (𝑄‘(𝑚 + 1)) ↔ ∀𝑦 ∈ ℝ ((𝑄‘𝑚)‘𝑦) ≤ ((𝑄‘(𝑚 + 1))‘𝑦))) |
135 | 127, 134 | mpbid 221 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ∀𝑦 ∈ ℝ ((𝑄‘𝑚)‘𝑦) ≤ ((𝑄‘(𝑚 + 1))‘𝑦)) |
136 | 135 | r19.21bi 2916 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → ((𝑄‘𝑚)‘𝑦) ≤ ((𝑄‘(𝑚 + 1))‘𝑦)) |
137 | 102, 105,
111, 116, 126, 136 | le2addd 10525 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (((𝑃‘𝑚)‘𝑦) + ((𝑄‘𝑚)‘𝑦)) ≤ (((𝑃‘(𝑚 + 1))‘𝑦) + ((𝑄‘(𝑚 + 1))‘𝑦))) |
138 | 137 | ralrimiva 2949 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ∀𝑦 ∈ ℝ (((𝑃‘𝑚)‘𝑦) + ((𝑄‘𝑚)‘𝑦)) ≤ (((𝑃‘(𝑚 + 1))‘𝑦) + ((𝑄‘(𝑚 + 1))‘𝑦))) |
139 | 24, 72 | i1fadd 23268 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑃‘𝑚) ∘𝑓 + (𝑄‘𝑚)) ∈ dom
∫1) |
140 | | i1ff 23249 |
. . . . . . . . 9
⊢ (((𝑃‘𝑚) ∘𝑓 + (𝑄‘𝑚)) ∈ dom ∫1 →
((𝑃‘𝑚) ∘𝑓 +
(𝑄‘𝑚)):ℝ⟶ℝ) |
141 | | ffn 5958 |
. . . . . . . . 9
⊢ (((𝑃‘𝑚) ∘𝑓 + (𝑄‘𝑚)):ℝ⟶ℝ → ((𝑃‘𝑚) ∘𝑓 + (𝑄‘𝑚)) Fn ℝ) |
142 | 139, 140,
141 | 3syl 18 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑃‘𝑚) ∘𝑓 + (𝑄‘𝑚)) Fn ℝ) |
143 | 108, 113 | i1fadd 23268 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑃‘(𝑚 + 1)) ∘𝑓 + (𝑄‘(𝑚 + 1))) ∈ dom
∫1) |
144 | | i1ff 23249 |
. . . . . . . . . 10
⊢ (((𝑃‘(𝑚 + 1)) ∘𝑓 + (𝑄‘(𝑚 + 1))) ∈ dom ∫1 →
((𝑃‘(𝑚 + 1))
∘𝑓 + (𝑄‘(𝑚 +
1))):ℝ⟶ℝ) |
145 | 143, 144 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑃‘(𝑚 + 1)) ∘𝑓 + (𝑄‘(𝑚 +
1))):ℝ⟶ℝ) |
146 | | ffn 5958 |
. . . . . . . . 9
⊢ (((𝑃‘(𝑚 + 1)) ∘𝑓 + (𝑄‘(𝑚 + 1))):ℝ⟶ℝ → ((𝑃‘(𝑚 + 1)) ∘𝑓 + (𝑄‘(𝑚 + 1))) Fn ℝ) |
147 | 145, 146 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑃‘(𝑚 + 1)) ∘𝑓 + (𝑄‘(𝑚 + 1))) Fn ℝ) |
148 | 119, 129,
87, 87, 10, 122, 132 | ofval 6804 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (((𝑃‘𝑚) ∘𝑓 + (𝑄‘𝑚))‘𝑦) = (((𝑃‘𝑚)‘𝑦) + ((𝑄‘𝑚)‘𝑦))) |
149 | 121, 131,
87, 87, 10, 123, 133 | ofval 6804 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (((𝑃‘(𝑚 + 1)) ∘𝑓 + (𝑄‘(𝑚 + 1)))‘𝑦) = (((𝑃‘(𝑚 + 1))‘𝑦) + ((𝑄‘(𝑚 + 1))‘𝑦))) |
150 | 142, 147,
87, 87, 10, 148, 149 | ofrfval 6803 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (((𝑃‘𝑚) ∘𝑓 + (𝑄‘𝑚)) ∘𝑟 ≤ ((𝑃‘(𝑚 + 1)) ∘𝑓 + (𝑄‘(𝑚 + 1))) ↔ ∀𝑦 ∈ ℝ (((𝑃‘𝑚)‘𝑦) + ((𝑄‘𝑚)‘𝑦)) ≤ (((𝑃‘(𝑚 + 1))‘𝑦) + ((𝑄‘(𝑚 + 1))‘𝑦)))) |
151 | 138, 150 | mpbird 246 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑃‘𝑚) ∘𝑓 + (𝑄‘𝑚)) ∘𝑟 ≤ ((𝑃‘(𝑚 + 1)) ∘𝑓 + (𝑄‘(𝑚 + 1)))) |
152 | | eqidd 2611 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑚 + 1) ∈ ℕ) → (𝑃‘(𝑚 + 1)) = (𝑃‘(𝑚 + 1))) |
153 | | eqidd 2611 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑚 + 1) ∈ ℕ) → (𝑄‘(𝑚 + 1)) = (𝑄‘(𝑚 + 1))) |
154 | 93, 95, 19, 19, 20, 152, 153 | ofval 6804 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 + 1) ∈ ℕ) → ((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘(𝑚 + 1)) = ((𝑃‘(𝑚 + 1)) ∘𝑓 + (𝑄‘(𝑚 + 1)))) |
155 | 106, 154 | sylan2 490 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘(𝑚 + 1)) = ((𝑃‘(𝑚 + 1)) ∘𝑓 + (𝑄‘(𝑚 + 1)))) |
156 | 151, 98, 155 | 3brtr4d 4615 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑚) ∘𝑟 ≤ ((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘(𝑚 + 1))) |
157 | 99, 156 | jca 553 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) →
(0𝑝 ∘𝑟 ≤ ((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑚) ∧ ((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑚) ∘𝑟 ≤ ((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘(𝑚 + 1)))) |
158 | 157 | ralrimiva 2949 |
. . 3
⊢ (𝜑 → ∀𝑚 ∈ ℕ (0𝑝
∘𝑟 ≤ ((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑚) ∧ ((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑚) ∘𝑟 ≤ ((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘(𝑚 + 1)))) |
159 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑛 = 𝑚 → ((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑛) = ((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑚)) |
160 | 159 | fveq1d 6105 |
. . . . . . 7
⊢ (𝑛 = 𝑚 → (((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑛)‘𝑦) = (((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑚)‘𝑦)) |
161 | 160 | cbvmptv 4678 |
. . . . . 6
⊢ (𝑛 ∈ ℕ ↦ (((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑛)‘𝑦)) = (𝑚 ∈ ℕ ↦ (((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑚)‘𝑦)) |
162 | | nnuz 11599 |
. . . . . . 7
⊢ ℕ =
(ℤ≥‘1) |
163 | | 1zzd 11285 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 1 ∈
ℤ) |
164 | | itg2add.p3 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)) |
165 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → ((𝑃‘𝑛)‘𝑥) = ((𝑃‘𝑛)‘𝑦)) |
166 | 165 | mpteq2dv 4673 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑦))) |
167 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝐹‘𝑥) = (𝐹‘𝑦)) |
168 | 166, 167 | breq12d 4596 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → ((𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥) ↔ (𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑦)) ⇝ (𝐹‘𝑦))) |
169 | 168 | rspccva 3281 |
. . . . . . . 8
⊢
((∀𝑥 ∈
ℝ (𝑛 ∈ ℕ
↦ ((𝑃‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥) ∧ 𝑦 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑦)) ⇝ (𝐹‘𝑦)) |
170 | 164, 169 | sylan 487 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑦)) ⇝ (𝐹‘𝑦)) |
171 | 18 | mptex 6390 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ ↦ (((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑛)‘𝑦)) ∈ V |
172 | 171 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑛 ∈ ℕ ↦ (((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑛)‘𝑦)) ∈ V) |
173 | | itg2add.q3 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑄‘𝑛)‘𝑥)) ⇝ (𝐺‘𝑥)) |
174 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → ((𝑄‘𝑛)‘𝑥) = ((𝑄‘𝑛)‘𝑦)) |
175 | 174 | mpteq2dv 4673 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑛 ∈ ℕ ↦ ((𝑄‘𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ ((𝑄‘𝑛)‘𝑦))) |
176 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝐺‘𝑥) = (𝐺‘𝑦)) |
177 | 175, 176 | breq12d 4596 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → ((𝑛 ∈ ℕ ↦ ((𝑄‘𝑛)‘𝑥)) ⇝ (𝐺‘𝑥) ↔ (𝑛 ∈ ℕ ↦ ((𝑄‘𝑛)‘𝑦)) ⇝ (𝐺‘𝑦))) |
178 | 177 | rspccva 3281 |
. . . . . . . 8
⊢
((∀𝑥 ∈
ℝ (𝑛 ∈ ℕ
↦ ((𝑄‘𝑛)‘𝑥)) ⇝ (𝐺‘𝑥) ∧ 𝑦 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((𝑄‘𝑛)‘𝑦)) ⇝ (𝐺‘𝑦)) |
179 | 173, 178 | sylan 487 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((𝑄‘𝑛)‘𝑦)) ⇝ (𝐺‘𝑦)) |
180 | 26 | fveq1d 6105 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑚 → ((𝑃‘𝑛)‘𝑦) = ((𝑃‘𝑚)‘𝑦)) |
181 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑦)) = (𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑦)) |
182 | | fvex 6113 |
. . . . . . . . . . 11
⊢ ((𝑃‘𝑚)‘𝑦) ∈ V |
183 | 180, 181,
182 | fvmpt 6191 |
. . . . . . . . . 10
⊢ (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑦))‘𝑚) = ((𝑃‘𝑚)‘𝑦)) |
184 | 183 | adantl 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑦))‘𝑚) = ((𝑃‘𝑚)‘𝑦)) |
185 | 102 | an32s 842 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → ((𝑃‘𝑚)‘𝑦) ∈ ℝ) |
186 | 184, 185 | eqeltrd 2688 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑦))‘𝑚) ∈ ℝ) |
187 | 186 | recnd 9947 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑦))‘𝑚) ∈ ℂ) |
188 | 74 | fveq1d 6105 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑚 → ((𝑄‘𝑛)‘𝑦) = ((𝑄‘𝑚)‘𝑦)) |
189 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ ↦ ((𝑄‘𝑛)‘𝑦)) = (𝑛 ∈ ℕ ↦ ((𝑄‘𝑛)‘𝑦)) |
190 | | fvex 6113 |
. . . . . . . . . . 11
⊢ ((𝑄‘𝑚)‘𝑦) ∈ V |
191 | 188, 189,
190 | fvmpt 6191 |
. . . . . . . . . 10
⊢ (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((𝑄‘𝑛)‘𝑦))‘𝑚) = ((𝑄‘𝑚)‘𝑦)) |
192 | 191 | adantl 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝑄‘𝑛)‘𝑦))‘𝑚) = ((𝑄‘𝑚)‘𝑦)) |
193 | 105 | an32s 842 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → ((𝑄‘𝑚)‘𝑦) ∈ ℝ) |
194 | 192, 193 | eqeltrd 2688 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝑄‘𝑛)‘𝑦))‘𝑚) ∈ ℝ) |
195 | 194 | recnd 9947 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝑄‘𝑛)‘𝑦))‘𝑚) ∈ ℂ) |
196 | 98 | fveq1d 6105 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑚)‘𝑦) = (((𝑃‘𝑚) ∘𝑓 + (𝑄‘𝑚))‘𝑦)) |
197 | 196 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑚)‘𝑦) = (((𝑃‘𝑚) ∘𝑓 + (𝑄‘𝑚))‘𝑦)) |
198 | 197, 148 | eqtrd 2644 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑚)‘𝑦) = (((𝑃‘𝑚)‘𝑦) + ((𝑄‘𝑚)‘𝑦))) |
199 | 198 | an32s 842 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → (((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑚)‘𝑦) = (((𝑃‘𝑚)‘𝑦) + ((𝑄‘𝑚)‘𝑦))) |
200 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ ↦ (((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑛)‘𝑦)) = (𝑛 ∈ ℕ ↦ (((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑛)‘𝑦)) |
201 | | fvex 6113 |
. . . . . . . . . 10
⊢ (((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑚)‘𝑦) ∈ V |
202 | 160, 200,
201 | fvmpt 6191 |
. . . . . . . . 9
⊢ (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑛)‘𝑦))‘𝑚) = (((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑚)‘𝑦)) |
203 | 202 | adantl 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑛)‘𝑦))‘𝑚) = (((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑚)‘𝑦)) |
204 | 184, 192 | oveq12d 6567 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → (((𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑦))‘𝑚) + ((𝑛 ∈ ℕ ↦ ((𝑄‘𝑛)‘𝑦))‘𝑚)) = (((𝑃‘𝑚)‘𝑦) + ((𝑄‘𝑚)‘𝑦))) |
205 | 199, 203,
204 | 3eqtr4d 2654 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑛)‘𝑦))‘𝑚) = (((𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑦))‘𝑚) + ((𝑛 ∈ ℕ ↦ ((𝑄‘𝑛)‘𝑦))‘𝑚))) |
206 | 162, 163,
170, 172, 179, 187, 195, 205 | climadd 14210 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑛 ∈ ℕ ↦ (((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑛)‘𝑦)) ⇝ ((𝐹‘𝑦) + (𝐺‘𝑦))) |
207 | 161, 206 | syl5eqbrr 4619 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑚 ∈ ℕ ↦ (((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑚)‘𝑦)) ⇝ ((𝐹‘𝑦) + (𝐺‘𝑦))) |
208 | | ffn 5958 |
. . . . . . 7
⊢ (𝐹:ℝ⟶(0[,)+∞)
→ 𝐹 Fn
ℝ) |
209 | 6, 208 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐹 Fn ℝ) |
210 | | ffn 5958 |
. . . . . . 7
⊢ (𝐺:ℝ⟶(0[,)+∞)
→ 𝐺 Fn
ℝ) |
211 | 7, 210 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐺 Fn ℝ) |
212 | | eqidd 2611 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐹‘𝑦) = (𝐹‘𝑦)) |
213 | | eqidd 2611 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐺‘𝑦) = (𝐺‘𝑦)) |
214 | 209, 211,
9, 9, 10, 212, 213 | ofval 6804 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((𝐹 ∘𝑓 + 𝐺)‘𝑦) = ((𝐹‘𝑦) + (𝐺‘𝑦))) |
215 | 207, 214 | breqtrrd 4611 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑚 ∈ ℕ ↦ (((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑚)‘𝑦)) ⇝ ((𝐹 ∘𝑓 + 𝐺)‘𝑦)) |
216 | 215 | ralrimiva 2949 |
. . 3
⊢ (𝜑 → ∀𝑦 ∈ ℝ (𝑚 ∈ ℕ ↦ (((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑚)‘𝑦)) ⇝ ((𝐹 ∘𝑓 + 𝐺)‘𝑦)) |
217 | | fveq2 6103 |
. . . . 5
⊢ (𝑛 = 𝑗 → ((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑛) = ((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑗)) |
218 | 217 | fveq2d 6107 |
. . . 4
⊢ (𝑛 = 𝑗 → (∫1‘((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑛)) = (∫1‘((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑗))) |
219 | 218 | cbvmptv 4678 |
. . 3
⊢ (𝑛 ∈ ℕ ↦
(∫1‘((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑛))) = (𝑗 ∈ ℕ ↦
(∫1‘((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑗))) |
220 | | itg2add.f3 |
. . . 4
⊢ (𝜑 →
(∫2‘𝐹)
∈ ℝ) |
221 | | itg2add.g3 |
. . . 4
⊢ (𝜑 →
(∫2‘𝐺)
∈ ℝ) |
222 | 220, 221 | readdcld 9948 |
. . 3
⊢ (𝜑 →
((∫2‘𝐹) + (∫2‘𝐺)) ∈
ℝ) |
223 | 98 | fveq2d 6107 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) →
(∫1‘((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑚)) = (∫1‘((𝑃‘𝑚) ∘𝑓 + (𝑄‘𝑚)))) |
224 | 24, 72 | itg1add 23274 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) →
(∫1‘((𝑃‘𝑚) ∘𝑓 + (𝑄‘𝑚))) = ((∫1‘(𝑃‘𝑚)) + (∫1‘(𝑄‘𝑚)))) |
225 | 223, 224 | eqtrd 2644 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) →
(∫1‘((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑚)) = ((∫1‘(𝑃‘𝑚)) + (∫1‘(𝑄‘𝑚)))) |
226 | | itg1cl 23258 |
. . . . . . . 8
⊢ ((𝑃‘𝑚) ∈ dom ∫1 →
(∫1‘(𝑃‘𝑚)) ∈ ℝ) |
227 | 24, 226 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) →
(∫1‘(𝑃‘𝑚)) ∈ ℝ) |
228 | | itg1cl 23258 |
. . . . . . . 8
⊢ ((𝑄‘𝑚) ∈ dom ∫1 →
(∫1‘(𝑄‘𝑚)) ∈ ℝ) |
229 | 72, 228 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) →
(∫1‘(𝑄‘𝑚)) ∈ ℝ) |
230 | 220 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) →
(∫2‘𝐹)
∈ ℝ) |
231 | 221 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) →
(∫2‘𝐺)
∈ ℝ) |
232 | 6 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝐹:ℝ⟶(0[,)+∞)) |
233 | | icossicc 12131 |
. . . . . . . . 9
⊢
(0[,)+∞) ⊆ (0[,]+∞) |
234 | | fss 5969 |
. . . . . . . . 9
⊢ ((𝐹:ℝ⟶(0[,)+∞)
∧ (0[,)+∞) ⊆ (0[,]+∞)) → 𝐹:ℝ⟶(0[,]+∞)) |
235 | 232, 233,
234 | sylancl 693 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝐹:ℝ⟶(0[,]+∞)) |
236 | 1, 6, 16, 25, 164 | itg2i1fseqle 23327 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑃‘𝑚) ∘𝑟 ≤ 𝐹) |
237 | | itg2ub 23306 |
. . . . . . . 8
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ (𝑃‘𝑚) ∈ dom ∫1
∧ (𝑃‘𝑚) ∘𝑟
≤ 𝐹) →
(∫1‘(𝑃‘𝑚)) ≤ (∫2‘𝐹)) |
238 | 235, 24, 236, 237 | syl3anc 1318 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) →
(∫1‘(𝑃‘𝑚)) ≤ (∫2‘𝐹)) |
239 | 7 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝐺:ℝ⟶(0[,)+∞)) |
240 | | fss 5969 |
. . . . . . . . 9
⊢ ((𝐺:ℝ⟶(0[,)+∞)
∧ (0[,)+∞) ⊆ (0[,]+∞)) → 𝐺:ℝ⟶(0[,]+∞)) |
241 | 239, 233,
240 | sylancl 693 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝐺:ℝ⟶(0[,]+∞)) |
242 | 2, 7, 17, 73, 173 | itg2i1fseqle 23327 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑄‘𝑚) ∘𝑟 ≤ 𝐺) |
243 | | itg2ub 23306 |
. . . . . . . 8
⊢ ((𝐺:ℝ⟶(0[,]+∞)
∧ (𝑄‘𝑚) ∈ dom ∫1
∧ (𝑄‘𝑚) ∘𝑟
≤ 𝐺) →
(∫1‘(𝑄‘𝑚)) ≤ (∫2‘𝐺)) |
244 | 241, 72, 242, 243 | syl3anc 1318 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) →
(∫1‘(𝑄‘𝑚)) ≤ (∫2‘𝐺)) |
245 | 227, 229,
230, 231, 238, 244 | le2addd 10525 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) →
((∫1‘(𝑃‘𝑚)) + (∫1‘(𝑄‘𝑚))) ≤ ((∫2‘𝐹) +
(∫2‘𝐺))) |
246 | 225, 245 | eqbrtrd 4605 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) →
(∫1‘((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑚)) ≤ ((∫2‘𝐹) +
(∫2‘𝐺))) |
247 | 246 | ralrimiva 2949 |
. . . 4
⊢ (𝜑 → ∀𝑚 ∈ ℕ
(∫1‘((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑚)) ≤ ((∫2‘𝐹) +
(∫2‘𝐺))) |
248 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑚 = 𝑘 → ((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑚) = ((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑘)) |
249 | 248 | fveq2d 6107 |
. . . . . 6
⊢ (𝑚 = 𝑘 → (∫1‘((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑚)) = (∫1‘((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑘))) |
250 | 249 | breq1d 4593 |
. . . . 5
⊢ (𝑚 = 𝑘 → ((∫1‘((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑚)) ≤ ((∫2‘𝐹) +
(∫2‘𝐺)) ↔ (∫1‘((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑘)) ≤ ((∫2‘𝐹) +
(∫2‘𝐺)))) |
251 | 250 | rspccva 3281 |
. . . 4
⊢
((∀𝑚 ∈
ℕ (∫1‘((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑚)) ≤ ((∫2‘𝐹) +
(∫2‘𝐺)) ∧ 𝑘 ∈ ℕ) →
(∫1‘((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑘)) ≤ ((∫2‘𝐹) +
(∫2‘𝐺))) |
252 | 247, 251 | sylan 487 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) →
(∫1‘((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑘)) ≤ ((∫2‘𝐹) +
(∫2‘𝐺))) |
253 | 3, 11, 21, 158, 216, 219, 222, 252 | itg2i1fseq2 23329 |
. 2
⊢ (𝜑 → (𝑛 ∈ ℕ ↦
(∫1‘((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑛))) ⇝ (∫2‘(𝐹 ∘𝑓 +
𝐺))) |
254 | | 1zzd 11285 |
. . 3
⊢ (𝜑 → 1 ∈
ℤ) |
255 | | eqid 2610 |
. . . 4
⊢ (𝑘 ∈ ℕ ↦
(∫1‘(𝑃‘𝑘))) = (𝑘 ∈ ℕ ↦
(∫1‘(𝑃‘𝑘))) |
256 | 1, 6, 16, 25, 164, 255, 220 | itg2i1fseq3 23330 |
. . 3
⊢ (𝜑 → (𝑘 ∈ ℕ ↦
(∫1‘(𝑃‘𝑘))) ⇝ (∫2‘𝐹)) |
257 | 18 | mptex 6390 |
. . . 4
⊢ (𝑛 ∈ ℕ ↦
(∫1‘((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑛))) ∈ V |
258 | 257 | a1i 11 |
. . 3
⊢ (𝜑 → (𝑛 ∈ ℕ ↦
(∫1‘((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑛))) ∈ V) |
259 | | eqid 2610 |
. . . 4
⊢ (𝑘 ∈ ℕ ↦
(∫1‘(𝑄‘𝑘))) = (𝑘 ∈ ℕ ↦
(∫1‘(𝑄‘𝑘))) |
260 | 2, 7, 17, 73, 173, 259, 221 | itg2i1fseq3 23330 |
. . 3
⊢ (𝜑 → (𝑘 ∈ ℕ ↦
(∫1‘(𝑄‘𝑘))) ⇝ (∫2‘𝐺)) |
261 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑘 = 𝑚 → (𝑃‘𝑘) = (𝑃‘𝑚)) |
262 | 261 | fveq2d 6107 |
. . . . . 6
⊢ (𝑘 = 𝑚 → (∫1‘(𝑃‘𝑘)) = (∫1‘(𝑃‘𝑚))) |
263 | | fvex 6113 |
. . . . . 6
⊢
(∫1‘(𝑃‘𝑚)) ∈ V |
264 | 262, 255,
263 | fvmpt 6191 |
. . . . 5
⊢ (𝑚 ∈ ℕ → ((𝑘 ∈ ℕ ↦
(∫1‘(𝑃‘𝑘)))‘𝑚) = (∫1‘(𝑃‘𝑚))) |
265 | 264 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑘 ∈ ℕ ↦
(∫1‘(𝑃‘𝑘)))‘𝑚) = (∫1‘(𝑃‘𝑚))) |
266 | 227 | recnd 9947 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) →
(∫1‘(𝑃‘𝑚)) ∈ ℂ) |
267 | 265, 266 | eqeltrd 2688 |
. . 3
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑘 ∈ ℕ ↦
(∫1‘(𝑃‘𝑘)))‘𝑚) ∈ ℂ) |
268 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑘 = 𝑚 → (𝑄‘𝑘) = (𝑄‘𝑚)) |
269 | 268 | fveq2d 6107 |
. . . . . 6
⊢ (𝑘 = 𝑚 → (∫1‘(𝑄‘𝑘)) = (∫1‘(𝑄‘𝑚))) |
270 | | fvex 6113 |
. . . . . 6
⊢
(∫1‘(𝑄‘𝑚)) ∈ V |
271 | 269, 259,
270 | fvmpt 6191 |
. . . . 5
⊢ (𝑚 ∈ ℕ → ((𝑘 ∈ ℕ ↦
(∫1‘(𝑄‘𝑘)))‘𝑚) = (∫1‘(𝑄‘𝑚))) |
272 | 271 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑘 ∈ ℕ ↦
(∫1‘(𝑄‘𝑘)))‘𝑚) = (∫1‘(𝑄‘𝑚))) |
273 | 229 | recnd 9947 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) →
(∫1‘(𝑄‘𝑚)) ∈ ℂ) |
274 | 272, 273 | eqeltrd 2688 |
. . 3
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑘 ∈ ℕ ↦
(∫1‘(𝑄‘𝑘)))‘𝑚) ∈ ℂ) |
275 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑗 = 𝑚 → ((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑗) = ((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑚)) |
276 | 275 | fveq2d 6107 |
. . . . . 6
⊢ (𝑗 = 𝑚 → (∫1‘((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑗)) = (∫1‘((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑚))) |
277 | | fvex 6113 |
. . . . . 6
⊢
(∫1‘((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑚)) ∈ V |
278 | 276, 219,
277 | fvmpt 6191 |
. . . . 5
⊢ (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦
(∫1‘((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑛)))‘𝑚) = (∫1‘((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑚))) |
279 | 278 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦
(∫1‘((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑛)))‘𝑚) = (∫1‘((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑚))) |
280 | 265, 272 | oveq12d 6567 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (((𝑘 ∈ ℕ ↦
(∫1‘(𝑃‘𝑘)))‘𝑚) + ((𝑘 ∈ ℕ ↦
(∫1‘(𝑄‘𝑘)))‘𝑚)) = ((∫1‘(𝑃‘𝑚)) + (∫1‘(𝑄‘𝑚)))) |
281 | 225, 279,
280 | 3eqtr4d 2654 |
. . 3
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦
(∫1‘((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑛)))‘𝑚) = (((𝑘 ∈ ℕ ↦
(∫1‘(𝑃‘𝑘)))‘𝑚) + ((𝑘 ∈ ℕ ↦
(∫1‘(𝑄‘𝑘)))‘𝑚))) |
282 | 162, 254,
256, 258, 260, 267, 274, 281 | climadd 14210 |
. 2
⊢ (𝜑 → (𝑛 ∈ ℕ ↦
(∫1‘((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑛))) ⇝ ((∫2‘𝐹) +
(∫2‘𝐺))) |
283 | | climuni 14131 |
. 2
⊢ (((𝑛 ∈ ℕ ↦
(∫1‘((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑛))) ⇝ (∫2‘(𝐹 ∘𝑓 +
𝐺)) ∧ (𝑛 ∈ ℕ ↦
(∫1‘((𝑃 ∘𝑓
∘𝑓 + 𝑄)‘𝑛))) ⇝ ((∫2‘𝐹) +
(∫2‘𝐺))) → (∫2‘(𝐹 ∘𝑓 +
𝐺)) =
((∫2‘𝐹) + (∫2‘𝐺))) |
284 | 253, 282,
283 | syl2anc 691 |
1
⊢ (𝜑 →
(∫2‘(𝐹
∘𝑓 + 𝐺)) = ((∫2‘𝐹) +
(∫2‘𝐺))) |