Step | Hyp | Ref
| Expression |
1 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑛 = 𝑀 → (𝑃‘𝑛) = (𝑃‘𝑀)) |
2 | 1 | fveq1d 6193 |
. . . . . 6
⊢ (𝑛 = 𝑀 → ((𝑃‘𝑛)‘𝑦) = ((𝑃‘𝑀)‘𝑦)) |
3 | | eqid 2622 |
. . . . . 6
⊢ (𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑦)) = (𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑦)) |
4 | | fvex 6201 |
. . . . . 6
⊢ ((𝑃‘𝑀)‘𝑦) ∈ V |
5 | 2, 3, 4 | fvmpt 6282 |
. . . . 5
⊢ (𝑀 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑦))‘𝑀) = ((𝑃‘𝑀)‘𝑦)) |
6 | 5 | ad2antlr 763 |
. . . 4
⊢ (((𝜑 ∧ 𝑀 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → ((𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑦))‘𝑀) = ((𝑃‘𝑀)‘𝑦)) |
7 | | nnuz 11723 |
. . . . 5
⊢ ℕ =
(ℤ≥‘1) |
8 | | simplr 792 |
. . . . 5
⊢ (((𝜑 ∧ 𝑀 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → 𝑀 ∈ ℕ) |
9 | | itg2i1fseq.5 |
. . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)) |
10 | | fveq2 6191 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → ((𝑃‘𝑛)‘𝑥) = ((𝑃‘𝑛)‘𝑦)) |
11 | 10 | mpteq2dv 4745 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑦))) |
12 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝐹‘𝑥) = (𝐹‘𝑦)) |
13 | 11, 12 | breq12d 4666 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → ((𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥) ↔ (𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑦)) ⇝ (𝐹‘𝑦))) |
14 | 13 | rspccva 3308 |
. . . . . . 7
⊢
((∀𝑥 ∈
ℝ (𝑛 ∈ ℕ
↦ ((𝑃‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥) ∧ 𝑦 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑦)) ⇝ (𝐹‘𝑦)) |
15 | 9, 14 | sylan 488 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑦)) ⇝ (𝐹‘𝑦)) |
16 | 15 | adantlr 751 |
. . . . 5
⊢ (((𝜑 ∧ 𝑀 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑦)) ⇝ (𝐹‘𝑦)) |
17 | | fveq2 6191 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑘 → (𝑃‘𝑛) = (𝑃‘𝑘)) |
18 | 17 | fveq1d 6193 |
. . . . . . . . 9
⊢ (𝑛 = 𝑘 → ((𝑃‘𝑛)‘𝑦) = ((𝑃‘𝑘)‘𝑦)) |
19 | | fvex 6201 |
. . . . . . . . 9
⊢ ((𝑃‘𝑘)‘𝑦) ∈ V |
20 | 18, 3, 19 | fvmpt 6282 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑦))‘𝑘) = ((𝑃‘𝑘)‘𝑦)) |
21 | 20 | adantl 482 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑦))‘𝑘) = ((𝑃‘𝑘)‘𝑦)) |
22 | | itg2i1fseq.3 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑃:ℕ⟶dom
∫1) |
23 | 22 | ffvelrnda 6359 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑃‘𝑘) ∈ dom
∫1) |
24 | | i1ff 23443 |
. . . . . . . . . 10
⊢ ((𝑃‘𝑘) ∈ dom ∫1 → (𝑃‘𝑘):ℝ⟶ℝ) |
25 | 23, 24 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑃‘𝑘):ℝ⟶ℝ) |
26 | 25 | ffvelrnda 6359 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → ((𝑃‘𝑘)‘𝑦) ∈ ℝ) |
27 | 26 | an32s 846 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑘 ∈ ℕ) → ((𝑃‘𝑘)‘𝑦) ∈ ℝ) |
28 | 21, 27 | eqeltrd 2701 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑦))‘𝑘) ∈ ℝ) |
29 | 28 | adantllr 755 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑀 ∈ ℕ) ∧ 𝑦 ∈ ℝ) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑦))‘𝑘) ∈ ℝ) |
30 | | itg2i1fseq.4 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑛 ∈ ℕ (0𝑝
∘𝑟 ≤ (𝑃‘𝑛) ∧ (𝑃‘𝑛) ∘𝑟 ≤ (𝑃‘(𝑛 + 1)))) |
31 | | simpr 477 |
. . . . . . . . . . . . 13
⊢
((0𝑝 ∘𝑟 ≤ (𝑃‘𝑛) ∧ (𝑃‘𝑛) ∘𝑟 ≤ (𝑃‘(𝑛 + 1))) → (𝑃‘𝑛) ∘𝑟 ≤ (𝑃‘(𝑛 + 1))) |
32 | 31 | ralimi 2952 |
. . . . . . . . . . . 12
⊢
(∀𝑛 ∈
ℕ (0𝑝 ∘𝑟 ≤ (𝑃‘𝑛) ∧ (𝑃‘𝑛) ∘𝑟 ≤ (𝑃‘(𝑛 + 1))) → ∀𝑛 ∈ ℕ (𝑃‘𝑛) ∘𝑟 ≤ (𝑃‘(𝑛 + 1))) |
33 | 30, 32 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑛 ∈ ℕ (𝑃‘𝑛) ∘𝑟 ≤ (𝑃‘(𝑛 + 1))) |
34 | | oveq1 6657 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑘 → (𝑛 + 1) = (𝑘 + 1)) |
35 | 34 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑘 → (𝑃‘(𝑛 + 1)) = (𝑃‘(𝑘 + 1))) |
36 | 17, 35 | breq12d 4666 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑘 → ((𝑃‘𝑛) ∘𝑟 ≤ (𝑃‘(𝑛 + 1)) ↔ (𝑃‘𝑘) ∘𝑟 ≤ (𝑃‘(𝑘 + 1)))) |
37 | 36 | rspccva 3308 |
. . . . . . . . . . 11
⊢
((∀𝑛 ∈
ℕ (𝑃‘𝑛) ∘𝑟
≤ (𝑃‘(𝑛 + 1)) ∧ 𝑘 ∈ ℕ) → (𝑃‘𝑘) ∘𝑟 ≤ (𝑃‘(𝑘 + 1))) |
38 | 33, 37 | sylan 488 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑃‘𝑘) ∘𝑟 ≤ (𝑃‘(𝑘 + 1))) |
39 | | ffn 6045 |
. . . . . . . . . . . 12
⊢ ((𝑃‘𝑘):ℝ⟶ℝ → (𝑃‘𝑘) Fn ℝ) |
40 | 23, 24, 39 | 3syl 18 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑃‘𝑘) Fn ℝ) |
41 | | peano2nn 11032 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈
ℕ) |
42 | | ffvelrn 6357 |
. . . . . . . . . . . . 13
⊢ ((𝑃:ℕ⟶dom
∫1 ∧ (𝑘
+ 1) ∈ ℕ) → (𝑃‘(𝑘 + 1)) ∈ dom
∫1) |
43 | 22, 41, 42 | syl2an 494 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑃‘(𝑘 + 1)) ∈ dom
∫1) |
44 | | i1ff 23443 |
. . . . . . . . . . . 12
⊢ ((𝑃‘(𝑘 + 1)) ∈ dom ∫1 →
(𝑃‘(𝑘 +
1)):ℝ⟶ℝ) |
45 | | ffn 6045 |
. . . . . . . . . . . 12
⊢ ((𝑃‘(𝑘 + 1)):ℝ⟶ℝ → (𝑃‘(𝑘 + 1)) Fn ℝ) |
46 | 43, 44, 45 | 3syl 18 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑃‘(𝑘 + 1)) Fn ℝ) |
47 | | reex 10027 |
. . . . . . . . . . . 12
⊢ ℝ
∈ V |
48 | 47 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ℝ ∈
V) |
49 | | inidm 3822 |
. . . . . . . . . . 11
⊢ (ℝ
∩ ℝ) = ℝ |
50 | | eqidd 2623 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → ((𝑃‘𝑘)‘𝑦) = ((𝑃‘𝑘)‘𝑦)) |
51 | | eqidd 2623 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → ((𝑃‘(𝑘 + 1))‘𝑦) = ((𝑃‘(𝑘 + 1))‘𝑦)) |
52 | 40, 46, 48, 48, 49, 50, 51 | ofrfval 6905 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑃‘𝑘) ∘𝑟 ≤ (𝑃‘(𝑘 + 1)) ↔ ∀𝑦 ∈ ℝ ((𝑃‘𝑘)‘𝑦) ≤ ((𝑃‘(𝑘 + 1))‘𝑦))) |
53 | 38, 52 | mpbid 222 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ∀𝑦 ∈ ℝ ((𝑃‘𝑘)‘𝑦) ≤ ((𝑃‘(𝑘 + 1))‘𝑦)) |
54 | 53 | r19.21bi 2932 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → ((𝑃‘𝑘)‘𝑦) ≤ ((𝑃‘(𝑘 + 1))‘𝑦)) |
55 | 54 | an32s 846 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑘 ∈ ℕ) → ((𝑃‘𝑘)‘𝑦) ≤ ((𝑃‘(𝑘 + 1))‘𝑦)) |
56 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑛 = (𝑘 + 1) → (𝑃‘𝑛) = (𝑃‘(𝑘 + 1))) |
57 | 56 | fveq1d 6193 |
. . . . . . . . . 10
⊢ (𝑛 = (𝑘 + 1) → ((𝑃‘𝑛)‘𝑦) = ((𝑃‘(𝑘 + 1))‘𝑦)) |
58 | | fvex 6201 |
. . . . . . . . . 10
⊢ ((𝑃‘(𝑘 + 1))‘𝑦) ∈ V |
59 | 57, 3, 58 | fvmpt 6282 |
. . . . . . . . 9
⊢ ((𝑘 + 1) ∈ ℕ →
((𝑛 ∈ ℕ ↦
((𝑃‘𝑛)‘𝑦))‘(𝑘 + 1)) = ((𝑃‘(𝑘 + 1))‘𝑦)) |
60 | 41, 59 | syl 17 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑦))‘(𝑘 + 1)) = ((𝑃‘(𝑘 + 1))‘𝑦)) |
61 | 60 | adantl 482 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑦))‘(𝑘 + 1)) = ((𝑃‘(𝑘 + 1))‘𝑦)) |
62 | 55, 21, 61 | 3brtr4d 4685 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑦))‘𝑘) ≤ ((𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑦))‘(𝑘 + 1))) |
63 | 62 | adantllr 755 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑀 ∈ ℕ) ∧ 𝑦 ∈ ℝ) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑦))‘𝑘) ≤ ((𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑦))‘(𝑘 + 1))) |
64 | 7, 8, 16, 29, 63 | climub 14392 |
. . . 4
⊢ (((𝜑 ∧ 𝑀 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → ((𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑦))‘𝑀) ≤ (𝐹‘𝑦)) |
65 | 6, 64 | eqbrtrrd 4677 |
. . 3
⊢ (((𝜑 ∧ 𝑀 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → ((𝑃‘𝑀)‘𝑦) ≤ (𝐹‘𝑦)) |
66 | 65 | ralrimiva 2966 |
. 2
⊢ ((𝜑 ∧ 𝑀 ∈ ℕ) → ∀𝑦 ∈ ℝ ((𝑃‘𝑀)‘𝑦) ≤ (𝐹‘𝑦)) |
67 | 22 | ffvelrnda 6359 |
. . . 4
⊢ ((𝜑 ∧ 𝑀 ∈ ℕ) → (𝑃‘𝑀) ∈ dom
∫1) |
68 | | i1ff 23443 |
. . . 4
⊢ ((𝑃‘𝑀) ∈ dom ∫1 → (𝑃‘𝑀):ℝ⟶ℝ) |
69 | | ffn 6045 |
. . . 4
⊢ ((𝑃‘𝑀):ℝ⟶ℝ → (𝑃‘𝑀) Fn ℝ) |
70 | 67, 68, 69 | 3syl 18 |
. . 3
⊢ ((𝜑 ∧ 𝑀 ∈ ℕ) → (𝑃‘𝑀) Fn ℝ) |
71 | | itg2i1fseq.2 |
. . . . . 6
⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞)) |
72 | | icossicc 12260 |
. . . . . 6
⊢
(0[,)+∞) ⊆ (0[,]+∞) |
73 | | fss 6056 |
. . . . . 6
⊢ ((𝐹:ℝ⟶(0[,)+∞)
∧ (0[,)+∞) ⊆ (0[,]+∞)) → 𝐹:ℝ⟶(0[,]+∞)) |
74 | 71, 72, 73 | sylancl 694 |
. . . . 5
⊢ (𝜑 → 𝐹:ℝ⟶(0[,]+∞)) |
75 | | ffn 6045 |
. . . . 5
⊢ (𝐹:ℝ⟶(0[,]+∞)
→ 𝐹 Fn
ℝ) |
76 | 74, 75 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐹 Fn ℝ) |
77 | 76 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ 𝑀 ∈ ℕ) → 𝐹 Fn ℝ) |
78 | 47 | a1i 11 |
. . 3
⊢ ((𝜑 ∧ 𝑀 ∈ ℕ) → ℝ ∈
V) |
79 | | eqidd 2623 |
. . 3
⊢ (((𝜑 ∧ 𝑀 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → ((𝑃‘𝑀)‘𝑦) = ((𝑃‘𝑀)‘𝑦)) |
80 | | eqidd 2623 |
. . 3
⊢ (((𝜑 ∧ 𝑀 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (𝐹‘𝑦) = (𝐹‘𝑦)) |
81 | 70, 77, 78, 78, 49, 79, 80 | ofrfval 6905 |
. 2
⊢ ((𝜑 ∧ 𝑀 ∈ ℕ) → ((𝑃‘𝑀) ∘𝑟 ≤ 𝐹 ↔ ∀𝑦 ∈ ℝ ((𝑃‘𝑀)‘𝑦) ≤ (𝐹‘𝑦))) |
82 | 66, 81 | mpbird 247 |
1
⊢ ((𝜑 ∧ 𝑀 ∈ ℕ) → (𝑃‘𝑀) ∘𝑟 ≤ 𝐹) |