Proof of Theorem itg2monolem2
Step | Hyp | Ref
| Expression |
1 | | itg2mono.6 |
. . 3
⊢ 𝑆 = sup(ran (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))), ℝ*, <
) |
2 | | itg2mono.3 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛):ℝ⟶(0[,)+∞)) |
3 | | icossicc 12260 |
. . . . . . . 8
⊢
(0[,)+∞) ⊆ (0[,]+∞) |
4 | | fss 6056 |
. . . . . . . 8
⊢ (((𝐹‘𝑛):ℝ⟶(0[,)+∞) ∧
(0[,)+∞) ⊆ (0[,]+∞)) → (𝐹‘𝑛):ℝ⟶(0[,]+∞)) |
5 | 2, 3, 4 | sylancl 694 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛):ℝ⟶(0[,]+∞)) |
6 | | itg2cl 23499 |
. . . . . . 7
⊢ ((𝐹‘𝑛):ℝ⟶(0[,]+∞) →
(∫2‘(𝐹‘𝑛)) ∈
ℝ*) |
7 | 5, 6 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) →
(∫2‘(𝐹‘𝑛)) ∈
ℝ*) |
8 | | eqid 2622 |
. . . . . 6
⊢ (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))) = (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))) |
9 | 7, 8 | fmptd 6385 |
. . . . 5
⊢ (𝜑 → (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))):ℕ⟶ℝ*) |
10 | | frn 6053 |
. . . . 5
⊢ ((𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))):ℕ⟶ℝ* →
ran (𝑛 ∈ ℕ
↦ (∫2‘(𝐹‘𝑛))) ⊆
ℝ*) |
11 | 9, 10 | syl 17 |
. . . 4
⊢ (𝜑 → ran (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))) ⊆
ℝ*) |
12 | | supxrcl 12145 |
. . . 4
⊢ (ran
(𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))) ⊆ ℝ* →
sup(ran (𝑛 ∈ ℕ
↦ (∫2‘(𝐹‘𝑛))), ℝ*, < ) ∈
ℝ*) |
13 | 11, 12 | syl 17 |
. . 3
⊢ (𝜑 → sup(ran (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))), ℝ*, < ) ∈
ℝ*) |
14 | 1, 13 | syl5eqel 2705 |
. 2
⊢ (𝜑 → 𝑆 ∈
ℝ*) |
15 | | itg2monolem2.7 |
. . 3
⊢ (𝜑 → 𝑃 ∈ dom
∫1) |
16 | | itg1cl 23452 |
. . 3
⊢ (𝑃 ∈ dom ∫1
→ (∫1‘𝑃) ∈ ℝ) |
17 | 15, 16 | syl 17 |
. 2
⊢ (𝜑 →
(∫1‘𝑃)
∈ ℝ) |
18 | | mnfxr 10096 |
. . . 4
⊢ -∞
∈ ℝ* |
19 | 18 | a1i 11 |
. . 3
⊢ (𝜑 → -∞ ∈
ℝ*) |
20 | | 1nn 11031 |
. . . . 5
⊢ 1 ∈
ℕ |
21 | 5 | ralrimiva 2966 |
. . . . 5
⊢ (𝜑 → ∀𝑛 ∈ ℕ (𝐹‘𝑛):ℝ⟶(0[,]+∞)) |
22 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑛 = 1 → (𝐹‘𝑛) = (𝐹‘1)) |
23 | 22 | feq1d 6030 |
. . . . . 6
⊢ (𝑛 = 1 → ((𝐹‘𝑛):ℝ⟶(0[,]+∞) ↔ (𝐹‘1):ℝ⟶(0[,]+∞))) |
24 | 23 | rspcv 3305 |
. . . . 5
⊢ (1 ∈
ℕ → (∀𝑛
∈ ℕ (𝐹‘𝑛):ℝ⟶(0[,]+∞) → (𝐹‘1):ℝ⟶(0[,]+∞))) |
25 | 20, 21, 24 | mpsyl 68 |
. . . 4
⊢ (𝜑 → (𝐹‘1):ℝ⟶(0[,]+∞)) |
26 | | itg2cl 23499 |
. . . 4
⊢ ((𝐹‘1):ℝ⟶(0[,]+∞)
→ (∫2‘(𝐹‘1)) ∈
ℝ*) |
27 | 25, 26 | syl 17 |
. . 3
⊢ (𝜑 →
(∫2‘(𝐹‘1)) ∈
ℝ*) |
28 | | itg2ge0 23502 |
. . . . 5
⊢ ((𝐹‘1):ℝ⟶(0[,]+∞)
→ 0 ≤ (∫2‘(𝐹‘1))) |
29 | 25, 28 | syl 17 |
. . . 4
⊢ (𝜑 → 0 ≤
(∫2‘(𝐹‘1))) |
30 | | mnflt0 11959 |
. . . . 5
⊢ -∞
< 0 |
31 | | 0xr 10086 |
. . . . . . 7
⊢ 0 ∈
ℝ* |
32 | | xrltletr 11988 |
. . . . . . 7
⊢
((-∞ ∈ ℝ* ∧ 0 ∈ ℝ*
∧ (∫2‘(𝐹‘1)) ∈ ℝ*)
→ ((-∞ < 0 ∧ 0 ≤ (∫2‘(𝐹‘1))) → -∞ <
(∫2‘(𝐹‘1)))) |
33 | 18, 31, 32 | mp3an12 1414 |
. . . . . 6
⊢
((∫2‘(𝐹‘1)) ∈ ℝ* →
((-∞ < 0 ∧ 0 ≤ (∫2‘(𝐹‘1))) → -∞ <
(∫2‘(𝐹‘1)))) |
34 | 27, 33 | syl 17 |
. . . . 5
⊢ (𝜑 → ((-∞ < 0 ∧ 0
≤ (∫2‘(𝐹‘1))) → -∞ <
(∫2‘(𝐹‘1)))) |
35 | 30, 34 | mpani 712 |
. . . 4
⊢ (𝜑 → (0 ≤
(∫2‘(𝐹‘1)) → -∞ <
(∫2‘(𝐹‘1)))) |
36 | 29, 35 | mpd 15 |
. . 3
⊢ (𝜑 → -∞ <
(∫2‘(𝐹‘1))) |
37 | 22 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝑛 = 1 →
(∫2‘(𝐹‘𝑛)) = (∫2‘(𝐹‘1))) |
38 | | fvex 6201 |
. . . . . . . 8
⊢
(∫2‘(𝐹‘1)) ∈ V |
39 | 37, 8, 38 | fvmpt 6282 |
. . . . . . 7
⊢ (1 ∈
ℕ → ((𝑛 ∈
ℕ ↦ (∫2‘(𝐹‘𝑛)))‘1) =
(∫2‘(𝐹‘1))) |
40 | 20, 39 | ax-mp 5 |
. . . . . 6
⊢ ((𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛)))‘1) =
(∫2‘(𝐹‘1)) |
41 | | ffn 6045 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))):ℕ⟶ℝ* →
(𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))) Fn ℕ) |
42 | 9, 41 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))) Fn ℕ) |
43 | | fnfvelrn 6356 |
. . . . . . 7
⊢ (((𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))) Fn ℕ ∧ 1 ∈ ℕ) →
((𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛)))‘1) ∈ ran (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛)))) |
44 | 42, 20, 43 | sylancl 694 |
. . . . . 6
⊢ (𝜑 → ((𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛)))‘1) ∈ ran (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛)))) |
45 | 40, 44 | syl5eqelr 2706 |
. . . . 5
⊢ (𝜑 →
(∫2‘(𝐹‘1)) ∈ ran (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛)))) |
46 | | supxrub 12154 |
. . . . 5
⊢ ((ran
(𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))) ⊆ ℝ* ∧
(∫2‘(𝐹‘1)) ∈ ran (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛)))) → (∫2‘(𝐹‘1)) ≤ sup(ran (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))), ℝ*, <
)) |
47 | 11, 45, 46 | syl2anc 693 |
. . . 4
⊢ (𝜑 →
(∫2‘(𝐹‘1)) ≤ sup(ran (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))), ℝ*, <
)) |
48 | 47, 1 | syl6breqr 4695 |
. . 3
⊢ (𝜑 →
(∫2‘(𝐹‘1)) ≤ 𝑆) |
49 | 19, 27, 14, 36, 48 | xrltletrd 11992 |
. 2
⊢ (𝜑 → -∞ < 𝑆) |
50 | | itg2monolem2.9 |
. . . 4
⊢ (𝜑 → ¬
(∫1‘𝑃)
≤ 𝑆) |
51 | 17 | rexrd 10089 |
. . . . 5
⊢ (𝜑 →
(∫1‘𝑃)
∈ ℝ*) |
52 | | xrltnle 10105 |
. . . . 5
⊢ ((𝑆 ∈ ℝ*
∧ (∫1‘𝑃) ∈ ℝ*) → (𝑆 <
(∫1‘𝑃)
↔ ¬ (∫1‘𝑃) ≤ 𝑆)) |
53 | 14, 51, 52 | syl2anc 693 |
. . . 4
⊢ (𝜑 → (𝑆 < (∫1‘𝑃) ↔ ¬
(∫1‘𝑃)
≤ 𝑆)) |
54 | 50, 53 | mpbird 247 |
. . 3
⊢ (𝜑 → 𝑆 < (∫1‘𝑃)) |
55 | | xrltle 11982 |
. . . 4
⊢ ((𝑆 ∈ ℝ*
∧ (∫1‘𝑃) ∈ ℝ*) → (𝑆 <
(∫1‘𝑃)
→ 𝑆 ≤
(∫1‘𝑃))) |
56 | 14, 51, 55 | syl2anc 693 |
. . 3
⊢ (𝜑 → (𝑆 < (∫1‘𝑃) → 𝑆 ≤ (∫1‘𝑃))) |
57 | 54, 56 | mpd 15 |
. 2
⊢ (𝜑 → 𝑆 ≤ (∫1‘𝑃)) |
58 | | xrre 12000 |
. 2
⊢ (((𝑆 ∈ ℝ*
∧ (∫1‘𝑃) ∈ ℝ) ∧ (-∞ < 𝑆 ∧ 𝑆 ≤ (∫1‘𝑃))) → 𝑆 ∈ ℝ) |
59 | 14, 17, 49, 57, 58 | syl22anc 1327 |
1
⊢ (𝜑 → 𝑆 ∈ ℝ) |