Step | Hyp | Ref
| Expression |
1 | | itg2mono.1 |
. . . . . . . 8
⊢ 𝐺 = (𝑥 ∈ ℝ ↦ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < )) |
2 | | itg2mono.2 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ MblFn) |
3 | 2 | adantlr 747 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐺) ∧ ¬
(∫1‘𝑓)
≤ 𝑆)) ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ MblFn) |
4 | | itg2mono.3 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛):ℝ⟶(0[,)+∞)) |
5 | 4 | adantlr 747 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐺) ∧ ¬
(∫1‘𝑓)
≤ 𝑆)) ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛):ℝ⟶(0[,)+∞)) |
6 | | itg2mono.4 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∘𝑟 ≤ (𝐹‘(𝑛 + 1))) |
7 | 6 | adantlr 747 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐺) ∧ ¬
(∫1‘𝑓)
≤ 𝑆)) ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∘𝑟 ≤ (𝐹‘(𝑛 + 1))) |
8 | | itg2mono.5 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ ℕ ((𝐹‘𝑛)‘𝑥) ≤ 𝑦) |
9 | 8 | adantlr 747 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐺) ∧ ¬
(∫1‘𝑓)
≤ 𝑆)) ∧ 𝑥 ∈ ℝ) →
∃𝑦 ∈ ℝ
∀𝑛 ∈ ℕ
((𝐹‘𝑛)‘𝑥) ≤ 𝑦) |
10 | | itg2mono.6 |
. . . . . . . 8
⊢ 𝑆 = sup(ran (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))), ℝ*, <
) |
11 | | simprll 798 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐺) ∧ ¬
(∫1‘𝑓)
≤ 𝑆)) → 𝑓 ∈ dom
∫1) |
12 | | simprlr 799 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐺) ∧ ¬
(∫1‘𝑓)
≤ 𝑆)) → 𝑓 ∘𝑟
≤ 𝐺) |
13 | | simprr 792 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐺) ∧ ¬
(∫1‘𝑓)
≤ 𝑆)) → ¬
(∫1‘𝑓)
≤ 𝑆) |
14 | 1, 3, 5, 7, 9, 10,
11, 12, 13 | itg2monolem3 23325 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐺) ∧ ¬
(∫1‘𝑓)
≤ 𝑆)) →
(∫1‘𝑓)
≤ 𝑆) |
15 | 14 | expr 641 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐺)) → (¬
(∫1‘𝑓)
≤ 𝑆 →
(∫1‘𝑓)
≤ 𝑆)) |
16 | 15 | pm2.18d 123 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐺)) →
(∫1‘𝑓)
≤ 𝑆) |
17 | 16 | expr 641 |
. . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → (𝑓 ∘𝑟
≤ 𝐺 →
(∫1‘𝑓)
≤ 𝑆)) |
18 | 17 | ralrimiva 2949 |
. . 3
⊢ (𝜑 → ∀𝑓 ∈ dom ∫1(𝑓 ∘𝑟
≤ 𝐺 →
(∫1‘𝑓)
≤ 𝑆)) |
19 | | rge0ssre 12151 |
. . . . . . . . . . . . 13
⊢
(0[,)+∞) ⊆ ℝ |
20 | | fss 5969 |
. . . . . . . . . . . . 13
⊢ (((𝐹‘𝑛):ℝ⟶(0[,)+∞) ∧
(0[,)+∞) ⊆ ℝ) → (𝐹‘𝑛):ℝ⟶ℝ) |
21 | 4, 19, 20 | sylancl 693 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛):ℝ⟶ℝ) |
22 | 21 | ffvelrnda 6267 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑛)‘𝑥) ∈ ℝ) |
23 | 22 | an32s 842 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℕ) → ((𝐹‘𝑛)‘𝑥) ∈ ℝ) |
24 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) |
25 | 23, 24 | fmptd 6292 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)):ℕ⟶ℝ) |
26 | | frn 5966 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)):ℕ⟶ℝ → ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) ⊆ ℝ) |
27 | 25, 26 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) ⊆ ℝ) |
28 | | 1nn 10908 |
. . . . . . . . . . 11
⊢ 1 ∈
ℕ |
29 | 24, 23 | dmmptd 5937 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → dom (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) = ℕ) |
30 | 28, 29 | syl5eleqr 2695 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 1 ∈ dom (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))) |
31 | | ne0i 3880 |
. . . . . . . . . 10
⊢ (1 ∈
dom (𝑛 ∈ ℕ
↦ ((𝐹‘𝑛)‘𝑥)) → dom (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) ≠ ∅) |
32 | 30, 31 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → dom (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) ≠ ∅) |
33 | | dm0rn0 5263 |
. . . . . . . . . 10
⊢ (dom
(𝑛 ∈ ℕ ↦
((𝐹‘𝑛)‘𝑥)) = ∅ ↔ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) = ∅) |
34 | 33 | necon3bii 2834 |
. . . . . . . . 9
⊢ (dom
(𝑛 ∈ ℕ ↦
((𝐹‘𝑛)‘𝑥)) ≠ ∅ ↔ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) ≠ ∅) |
35 | 32, 34 | sylib 207 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) ≠ ∅) |
36 | | ffn 5958 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)):ℕ⟶ℝ → (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) Fn ℕ) |
37 | 25, 36 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) Fn ℕ) |
38 | | breq1 4586 |
. . . . . . . . . . . . 13
⊢ (𝑧 = ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑚) → (𝑧 ≤ 𝑦 ↔ ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑚) ≤ 𝑦)) |
39 | 38 | ralrn 6270 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) Fn ℕ → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))𝑧 ≤ 𝑦 ↔ ∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑚) ≤ 𝑦)) |
40 | 37, 39 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))𝑧 ≤ 𝑦 ↔ ∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑚) ≤ 𝑦)) |
41 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑚 → (𝐹‘𝑛) = (𝐹‘𝑚)) |
42 | 41 | fveq1d 6105 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑚 → ((𝐹‘𝑛)‘𝑥) = ((𝐹‘𝑚)‘𝑥)) |
43 | | fvex 6113 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹‘𝑚)‘𝑥) ∈ V |
44 | 42, 24, 43 | fvmpt 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑚) = ((𝐹‘𝑚)‘𝑥)) |
45 | 44 | breq1d 4593 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ ℕ → (((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑚) ≤ 𝑦 ↔ ((𝐹‘𝑚)‘𝑥) ≤ 𝑦)) |
46 | 45 | ralbiia 2962 |
. . . . . . . . . . . 12
⊢
(∀𝑚 ∈
ℕ ((𝑛 ∈ ℕ
↦ ((𝐹‘𝑛)‘𝑥))‘𝑚) ≤ 𝑦 ↔ ∀𝑚 ∈ ℕ ((𝐹‘𝑚)‘𝑥) ≤ 𝑦) |
47 | 42 | breq1d 4593 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑚 → (((𝐹‘𝑛)‘𝑥) ≤ 𝑦 ↔ ((𝐹‘𝑚)‘𝑥) ≤ 𝑦)) |
48 | 47 | cbvralv 3147 |
. . . . . . . . . . . 12
⊢
(∀𝑛 ∈
ℕ ((𝐹‘𝑛)‘𝑥) ≤ 𝑦 ↔ ∀𝑚 ∈ ℕ ((𝐹‘𝑚)‘𝑥) ≤ 𝑦) |
49 | 46, 48 | bitr4i 266 |
. . . . . . . . . . 11
⊢
(∀𝑚 ∈
ℕ ((𝑛 ∈ ℕ
↦ ((𝐹‘𝑛)‘𝑥))‘𝑚) ≤ 𝑦 ↔ ∀𝑛 ∈ ℕ ((𝐹‘𝑛)‘𝑥) ≤ 𝑦) |
50 | 40, 49 | syl6bb 275 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))𝑧 ≤ 𝑦 ↔ ∀𝑛 ∈ ℕ ((𝐹‘𝑛)‘𝑥) ≤ 𝑦)) |
51 | 50 | rexbidv 3034 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))𝑧 ≤ 𝑦 ↔ ∃𝑦 ∈ ℝ ∀𝑛 ∈ ℕ ((𝐹‘𝑛)‘𝑥) ≤ 𝑦)) |
52 | 8, 51 | mpbird 246 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))𝑧 ≤ 𝑦) |
53 | | suprcl 10862 |
. . . . . . . 8
⊢ ((ran
(𝑛 ∈ ℕ ↦
((𝐹‘𝑛)‘𝑥)) ⊆ ℝ ∧ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))𝑧 ≤ 𝑦) → sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ) ∈
ℝ) |
54 | 27, 35, 52, 53 | syl3anc 1318 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ) ∈
ℝ) |
55 | 54 | rexrd 9968 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ) ∈
ℝ*) |
56 | | 0red 9920 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 0 ∈
ℝ) |
57 | 4 | ralrimiva 2949 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑛 ∈ ℕ (𝐹‘𝑛):ℝ⟶(0[,)+∞)) |
58 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 1 → (𝐹‘𝑛) = (𝐹‘1)) |
59 | 58 | feq1d 5943 |
. . . . . . . . . . . 12
⊢ (𝑛 = 1 → ((𝐹‘𝑛):ℝ⟶(0[,)+∞) ↔ (𝐹‘1):ℝ⟶(0[,)+∞))) |
60 | 59 | rspcv 3278 |
. . . . . . . . . . 11
⊢ (1 ∈
ℕ → (∀𝑛
∈ ℕ (𝐹‘𝑛):ℝ⟶(0[,)+∞) → (𝐹‘1):ℝ⟶(0[,)+∞))) |
61 | 28, 57, 60 | mpsyl 66 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹‘1):ℝ⟶(0[,)+∞)) |
62 | 61 | ffvelrnda 6267 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐹‘1)‘𝑥) ∈ (0[,)+∞)) |
63 | | elrege0 12149 |
. . . . . . . . 9
⊢ (((𝐹‘1)‘𝑥) ∈ (0[,)+∞) ↔
(((𝐹‘1)‘𝑥) ∈ ℝ ∧ 0 ≤
((𝐹‘1)‘𝑥))) |
64 | 62, 63 | sylib 207 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((𝐹‘1)‘𝑥) ∈ ℝ ∧ 0 ≤ ((𝐹‘1)‘𝑥))) |
65 | 64 | simpld 474 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐹‘1)‘𝑥) ∈ ℝ) |
66 | 64 | simprd 478 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 0 ≤ ((𝐹‘1)‘𝑥)) |
67 | 58 | fveq1d 6105 |
. . . . . . . . . . 11
⊢ (𝑛 = 1 → ((𝐹‘𝑛)‘𝑥) = ((𝐹‘1)‘𝑥)) |
68 | | fvex 6113 |
. . . . . . . . . . 11
⊢ ((𝐹‘1)‘𝑥) ∈ V |
69 | 67, 24, 68 | fvmpt 6191 |
. . . . . . . . . 10
⊢ (1 ∈
ℕ → ((𝑛 ∈
ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘1) = ((𝐹‘1)‘𝑥)) |
70 | 28, 69 | ax-mp 5 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘1) = ((𝐹‘1)‘𝑥) |
71 | | fnfvelrn 6264 |
. . . . . . . . . 10
⊢ (((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) Fn ℕ ∧ 1 ∈ ℕ) →
((𝑛 ∈ ℕ ↦
((𝐹‘𝑛)‘𝑥))‘1) ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))) |
72 | 37, 28, 71 | sylancl 693 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘1) ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))) |
73 | 70, 72 | syl5eqelr 2693 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐹‘1)‘𝑥) ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))) |
74 | | suprub 10863 |
. . . . . . . 8
⊢ (((ran
(𝑛 ∈ ℕ ↦
((𝐹‘𝑛)‘𝑥)) ⊆ ℝ ∧ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))𝑧 ≤ 𝑦) ∧ ((𝐹‘1)‘𝑥) ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))) → ((𝐹‘1)‘𝑥) ≤ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < )) |
75 | 27, 35, 52, 73, 74 | syl31anc 1321 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐹‘1)‘𝑥) ≤ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < )) |
76 | 56, 65, 54, 66, 75 | letrd 10073 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 0 ≤ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < )) |
77 | | elxrge0 12152 |
. . . . . 6
⊢ (sup(ran
(𝑛 ∈ ℕ ↦
((𝐹‘𝑛)‘𝑥)), ℝ, < ) ∈ (0[,]+∞)
↔ (sup(ran (𝑛 ∈
ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ) ∈
ℝ* ∧ 0 ≤ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ))) |
78 | 55, 76, 77 | sylanbrc 695 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ) ∈
(0[,]+∞)) |
79 | 78, 1 | fmptd 6292 |
. . . 4
⊢ (𝜑 → 𝐺:ℝ⟶(0[,]+∞)) |
80 | | icossicc 12131 |
. . . . . . . . . 10
⊢
(0[,)+∞) ⊆ (0[,]+∞) |
81 | | fss 5969 |
. . . . . . . . . 10
⊢ (((𝐹‘𝑛):ℝ⟶(0[,)+∞) ∧
(0[,)+∞) ⊆ (0[,]+∞)) → (𝐹‘𝑛):ℝ⟶(0[,]+∞)) |
82 | 4, 80, 81 | sylancl 693 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛):ℝ⟶(0[,]+∞)) |
83 | | itg2cl 23305 |
. . . . . . . . 9
⊢ ((𝐹‘𝑛):ℝ⟶(0[,]+∞) →
(∫2‘(𝐹‘𝑛)) ∈
ℝ*) |
84 | 82, 83 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) →
(∫2‘(𝐹‘𝑛)) ∈
ℝ*) |
85 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))) = (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))) |
86 | 84, 85 | fmptd 6292 |
. . . . . . 7
⊢ (𝜑 → (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))):ℕ⟶ℝ*) |
87 | | frn 5966 |
. . . . . . 7
⊢ ((𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))):ℕ⟶ℝ* →
ran (𝑛 ∈ ℕ
↦ (∫2‘(𝐹‘𝑛))) ⊆
ℝ*) |
88 | 86, 87 | syl 17 |
. . . . . 6
⊢ (𝜑 → ran (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))) ⊆
ℝ*) |
89 | | supxrcl 12017 |
. . . . . 6
⊢ (ran
(𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))) ⊆ ℝ* →
sup(ran (𝑛 ∈ ℕ
↦ (∫2‘(𝐹‘𝑛))), ℝ*, < ) ∈
ℝ*) |
90 | 88, 89 | syl 17 |
. . . . 5
⊢ (𝜑 → sup(ran (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))), ℝ*, < ) ∈
ℝ*) |
91 | 10, 90 | syl5eqel 2692 |
. . . 4
⊢ (𝜑 → 𝑆 ∈
ℝ*) |
92 | | itg2leub 23307 |
. . . 4
⊢ ((𝐺:ℝ⟶(0[,]+∞)
∧ 𝑆 ∈
ℝ*) → ((∫2‘𝐺) ≤ 𝑆 ↔ ∀𝑓 ∈ dom ∫1(𝑓 ∘𝑟
≤ 𝐺 →
(∫1‘𝑓)
≤ 𝑆))) |
93 | 79, 91, 92 | syl2anc 691 |
. . 3
⊢ (𝜑 →
((∫2‘𝐺) ≤ 𝑆 ↔ ∀𝑓 ∈ dom ∫1(𝑓 ∘𝑟
≤ 𝐺 →
(∫1‘𝑓)
≤ 𝑆))) |
94 | 18, 93 | mpbird 246 |
. 2
⊢ (𝜑 →
(∫2‘𝐺)
≤ 𝑆) |
95 | 41 | feq1d 5943 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑚 → ((𝐹‘𝑛):ℝ⟶(0[,)+∞) ↔ (𝐹‘𝑚):ℝ⟶(0[,)+∞))) |
96 | 95 | cbvralv 3147 |
. . . . . . . . . 10
⊢
(∀𝑛 ∈
ℕ (𝐹‘𝑛):ℝ⟶(0[,)+∞)
↔ ∀𝑚 ∈
ℕ (𝐹‘𝑚):ℝ⟶(0[,)+∞)) |
97 | 57, 96 | sylib 207 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑚 ∈ ℕ (𝐹‘𝑚):ℝ⟶(0[,)+∞)) |
98 | 97 | r19.21bi 2916 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐹‘𝑚):ℝ⟶(0[,)+∞)) |
99 | | fss 5969 |
. . . . . . . 8
⊢ (((𝐹‘𝑚):ℝ⟶(0[,)+∞) ∧
(0[,)+∞) ⊆ (0[,]+∞)) → (𝐹‘𝑚):ℝ⟶(0[,]+∞)) |
100 | 98, 80, 99 | sylancl 693 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐹‘𝑚):ℝ⟶(0[,]+∞)) |
101 | 79 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝐺:ℝ⟶(0[,]+∞)) |
102 | 27, 35, 52 | 3jca 1235 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) ⊆ ℝ ∧ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))𝑧 ≤ 𝑦)) |
103 | 102 | adantlr 747 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) ⊆ ℝ ∧ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))𝑧 ≤ 𝑦)) |
104 | 44 | ad2antlr 759 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑚) = ((𝐹‘𝑚)‘𝑥)) |
105 | 37 | adantlr 747 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) Fn ℕ) |
106 | | simplr 788 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝑚 ∈ ℕ) |
107 | | fnfvelrn 6264 |
. . . . . . . . . . . . . 14
⊢ (((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) Fn ℕ ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑚) ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))) |
108 | 105, 106,
107 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑚) ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))) |
109 | 104, 108 | eqeltrrd 2689 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑚)‘𝑥) ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))) |
110 | | suprub 10863 |
. . . . . . . . . . . 12
⊢ (((ran
(𝑛 ∈ ℕ ↦
((𝐹‘𝑛)‘𝑥)) ⊆ ℝ ∧ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))𝑧 ≤ 𝑦) ∧ ((𝐹‘𝑚)‘𝑥) ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))) → ((𝐹‘𝑚)‘𝑥) ≤ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < )) |
111 | 103, 109,
110 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑚)‘𝑥) ≤ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < )) |
112 | | simpr 476 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ) |
113 | | ltso 9997 |
. . . . . . . . . . . . 13
⊢ < Or
ℝ |
114 | 113 | supex 8252 |
. . . . . . . . . . . 12
⊢ sup(ran
(𝑛 ∈ ℕ ↦
((𝐹‘𝑛)‘𝑥)), ℝ, < ) ∈ V |
115 | 1 | fvmpt2 6200 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ ∧ sup(ran
(𝑛 ∈ ℕ ↦
((𝐹‘𝑛)‘𝑥)), ℝ, < ) ∈ V) → (𝐺‘𝑥) = sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < )) |
116 | 112, 114,
115 | sylancl 693 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐺‘𝑥) = sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < )) |
117 | 111, 116 | breqtrrd 4611 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑚)‘𝑥) ≤ (𝐺‘𝑥)) |
118 | 117 | ralrimiva 2949 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ∀𝑥 ∈ ℝ ((𝐹‘𝑚)‘𝑥) ≤ (𝐺‘𝑥)) |
119 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → ((𝐹‘𝑚)‘𝑥) = ((𝐹‘𝑚)‘𝑧)) |
120 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → (𝐺‘𝑥) = (𝐺‘𝑧)) |
121 | 119, 120 | breq12d 4596 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑧 → (((𝐹‘𝑚)‘𝑥) ≤ (𝐺‘𝑥) ↔ ((𝐹‘𝑚)‘𝑧) ≤ (𝐺‘𝑧))) |
122 | 121 | cbvralv 3147 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
ℝ ((𝐹‘𝑚)‘𝑥) ≤ (𝐺‘𝑥) ↔ ∀𝑧 ∈ ℝ ((𝐹‘𝑚)‘𝑧) ≤ (𝐺‘𝑧)) |
123 | 118, 122 | sylib 207 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ∀𝑧 ∈ ℝ ((𝐹‘𝑚)‘𝑧) ≤ (𝐺‘𝑧)) |
124 | | ffn 5958 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑚):ℝ⟶(0[,]+∞) → (𝐹‘𝑚) Fn ℝ) |
125 | 100, 124 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐹‘𝑚) Fn ℝ) |
126 | 54, 1 | fmptd 6292 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺:ℝ⟶ℝ) |
127 | | ffn 5958 |
. . . . . . . . . . 11
⊢ (𝐺:ℝ⟶ℝ →
𝐺 Fn
ℝ) |
128 | 126, 127 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 Fn ℝ) |
129 | 128 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝐺 Fn ℝ) |
130 | | reex 9906 |
. . . . . . . . . 10
⊢ ℝ
∈ V |
131 | 130 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ℝ ∈
V) |
132 | | inidm 3784 |
. . . . . . . . 9
⊢ (ℝ
∩ ℝ) = ℝ |
133 | | eqidd 2611 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑧 ∈ ℝ) → ((𝐹‘𝑚)‘𝑧) = ((𝐹‘𝑚)‘𝑧)) |
134 | | eqidd 2611 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑧 ∈ ℝ) → (𝐺‘𝑧) = (𝐺‘𝑧)) |
135 | 125, 129,
131, 131, 132, 133, 134 | ofrfval 6803 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝐹‘𝑚) ∘𝑟 ≤ 𝐺 ↔ ∀𝑧 ∈ ℝ ((𝐹‘𝑚)‘𝑧) ≤ (𝐺‘𝑧))) |
136 | 123, 135 | mpbird 246 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐹‘𝑚) ∘𝑟 ≤ 𝐺) |
137 | | itg2le 23312 |
. . . . . . 7
⊢ (((𝐹‘𝑚):ℝ⟶(0[,]+∞) ∧ 𝐺:ℝ⟶(0[,]+∞)
∧ (𝐹‘𝑚) ∘𝑟
≤ 𝐺) →
(∫2‘(𝐹‘𝑚)) ≤ (∫2‘𝐺)) |
138 | 100, 101,
136, 137 | syl3anc 1318 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) →
(∫2‘(𝐹‘𝑚)) ≤ (∫2‘𝐺)) |
139 | 138 | ralrimiva 2949 |
. . . . 5
⊢ (𝜑 → ∀𝑚 ∈ ℕ
(∫2‘(𝐹‘𝑚)) ≤ (∫2‘𝐺)) |
140 | | ffn 5958 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))):ℕ⟶ℝ* →
(𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))) Fn ℕ) |
141 | 86, 140 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))) Fn ℕ) |
142 | | breq1 4586 |
. . . . . . . 8
⊢ (𝑧 = ((𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛)))‘𝑚) → (𝑧 ≤ (∫2‘𝐺) ↔ ((𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛)))‘𝑚) ≤ (∫2‘𝐺))) |
143 | 142 | ralrn 6270 |
. . . . . . 7
⊢ ((𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))) Fn ℕ → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛)))𝑧 ≤ (∫2‘𝐺) ↔ ∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛)))‘𝑚) ≤ (∫2‘𝐺))) |
144 | 141, 143 | syl 17 |
. . . . . 6
⊢ (𝜑 → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛)))𝑧 ≤ (∫2‘𝐺) ↔ ∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛)))‘𝑚) ≤ (∫2‘𝐺))) |
145 | 41 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝑛 = 𝑚 → (∫2‘(𝐹‘𝑛)) = (∫2‘(𝐹‘𝑚))) |
146 | | fvex 6113 |
. . . . . . . . 9
⊢
(∫2‘(𝐹‘𝑚)) ∈ V |
147 | 145, 85, 146 | fvmpt 6191 |
. . . . . . . 8
⊢ (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛)))‘𝑚) = (∫2‘(𝐹‘𝑚))) |
148 | 147 | breq1d 4593 |
. . . . . . 7
⊢ (𝑚 ∈ ℕ → (((𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛)))‘𝑚) ≤ (∫2‘𝐺) ↔
(∫2‘(𝐹‘𝑚)) ≤ (∫2‘𝐺))) |
149 | 148 | ralbiia 2962 |
. . . . . 6
⊢
(∀𝑚 ∈
ℕ ((𝑛 ∈ ℕ
↦ (∫2‘(𝐹‘𝑛)))‘𝑚) ≤ (∫2‘𝐺) ↔ ∀𝑚 ∈ ℕ
(∫2‘(𝐹‘𝑚)) ≤ (∫2‘𝐺)) |
150 | 144, 149 | syl6bb 275 |
. . . . 5
⊢ (𝜑 → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛)))𝑧 ≤ (∫2‘𝐺) ↔ ∀𝑚 ∈ ℕ
(∫2‘(𝐹‘𝑚)) ≤ (∫2‘𝐺))) |
151 | 139, 150 | mpbird 246 |
. . . 4
⊢ (𝜑 → ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛)))𝑧 ≤ (∫2‘𝐺)) |
152 | | itg2cl 23305 |
. . . . . 6
⊢ (𝐺:ℝ⟶(0[,]+∞)
→ (∫2‘𝐺) ∈
ℝ*) |
153 | 79, 152 | syl 17 |
. . . . 5
⊢ (𝜑 →
(∫2‘𝐺)
∈ ℝ*) |
154 | | supxrleub 12028 |
. . . . 5
⊢ ((ran
(𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))) ⊆ ℝ* ∧
(∫2‘𝐺)
∈ ℝ*) → (sup(ran (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))), ℝ*, < ) ≤
(∫2‘𝐺)
↔ ∀𝑧 ∈ ran
(𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛)))𝑧 ≤ (∫2‘𝐺))) |
155 | 88, 153, 154 | syl2anc 691 |
. . . 4
⊢ (𝜑 → (sup(ran (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))), ℝ*, < ) ≤
(∫2‘𝐺)
↔ ∀𝑧 ∈ ran
(𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛)))𝑧 ≤ (∫2‘𝐺))) |
156 | 151, 155 | mpbird 246 |
. . 3
⊢ (𝜑 → sup(ran (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))), ℝ*, < ) ≤
(∫2‘𝐺)) |
157 | 10, 156 | syl5eqbr 4618 |
. 2
⊢ (𝜑 → 𝑆 ≤ (∫2‘𝐺)) |
158 | | xrletri3 11861 |
. . 3
⊢
(((∫2‘𝐺) ∈ ℝ* ∧ 𝑆 ∈ ℝ*)
→ ((∫2‘𝐺) = 𝑆 ↔ ((∫2‘𝐺) ≤ 𝑆 ∧ 𝑆 ≤ (∫2‘𝐺)))) |
159 | 153, 91, 158 | syl2anc 691 |
. 2
⊢ (𝜑 →
((∫2‘𝐺) = 𝑆 ↔ ((∫2‘𝐺) ≤ 𝑆 ∧ 𝑆 ≤ (∫2‘𝐺)))) |
160 | 94, 157, 159 | mpbir2and 959 |
1
⊢ (𝜑 →
(∫2‘𝐺)
= 𝑆) |