Proof of Theorem itg2monolem2
Step | Hyp | Ref
| Expression |
1 | | itg2mono.6 |
. . 3
⊢ 𝑆 = sup(ran (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))), ℝ*, <
) |
2 | | itg2mono.3 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛):ℝ⟶(0[,)+∞)) |
3 | | icossicc 12131 |
. . . . . . . 8
⊢
(0[,)+∞) ⊆ (0[,]+∞) |
4 | | fss 5969 |
. . . . . . . 8
⊢ (((𝐹‘𝑛):ℝ⟶(0[,)+∞) ∧
(0[,)+∞) ⊆ (0[,]+∞)) → (𝐹‘𝑛):ℝ⟶(0[,]+∞)) |
5 | 2, 3, 4 | sylancl 693 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛):ℝ⟶(0[,]+∞)) |
6 | | itg2cl 23305 |
. . . . . . 7
⊢ ((𝐹‘𝑛):ℝ⟶(0[,]+∞) →
(∫2‘(𝐹‘𝑛)) ∈
ℝ*) |
7 | 5, 6 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) →
(∫2‘(𝐹‘𝑛)) ∈
ℝ*) |
8 | | eqid 2610 |
. . . . . 6
⊢ (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))) = (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))) |
9 | 7, 8 | fmptd 6292 |
. . . . 5
⊢ (𝜑 → (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))):ℕ⟶ℝ*) |
10 | | frn 5966 |
. . . . 5
⊢ ((𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))):ℕ⟶ℝ* →
ran (𝑛 ∈ ℕ
↦ (∫2‘(𝐹‘𝑛))) ⊆
ℝ*) |
11 | 9, 10 | syl 17 |
. . . 4
⊢ (𝜑 → ran (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))) ⊆
ℝ*) |
12 | | supxrcl 12017 |
. . . 4
⊢ (ran
(𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))) ⊆ ℝ* →
sup(ran (𝑛 ∈ ℕ
↦ (∫2‘(𝐹‘𝑛))), ℝ*, < ) ∈
ℝ*) |
13 | 11, 12 | syl 17 |
. . 3
⊢ (𝜑 → sup(ran (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))), ℝ*, < ) ∈
ℝ*) |
14 | 1, 13 | syl5eqel 2692 |
. 2
⊢ (𝜑 → 𝑆 ∈
ℝ*) |
15 | | itg2monolem2.7 |
. . 3
⊢ (𝜑 → 𝑃 ∈ dom
∫1) |
16 | | itg1cl 23258 |
. . 3
⊢ (𝑃 ∈ dom ∫1
→ (∫1‘𝑃) ∈ ℝ) |
17 | 15, 16 | syl 17 |
. 2
⊢ (𝜑 →
(∫1‘𝑃)
∈ ℝ) |
18 | | mnfxr 9975 |
. . . 4
⊢ -∞
∈ ℝ* |
19 | 18 | a1i 11 |
. . 3
⊢ (𝜑 → -∞ ∈
ℝ*) |
20 | | 1nn 10908 |
. . . . 5
⊢ 1 ∈
ℕ |
21 | 5 | ralrimiva 2949 |
. . . . 5
⊢ (𝜑 → ∀𝑛 ∈ ℕ (𝐹‘𝑛):ℝ⟶(0[,]+∞)) |
22 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑛 = 1 → (𝐹‘𝑛) = (𝐹‘1)) |
23 | 22 | feq1d 5943 |
. . . . . 6
⊢ (𝑛 = 1 → ((𝐹‘𝑛):ℝ⟶(0[,]+∞) ↔ (𝐹‘1):ℝ⟶(0[,]+∞))) |
24 | 23 | rspcv 3278 |
. . . . 5
⊢ (1 ∈
ℕ → (∀𝑛
∈ ℕ (𝐹‘𝑛):ℝ⟶(0[,]+∞) → (𝐹‘1):ℝ⟶(0[,]+∞))) |
25 | 20, 21, 24 | mpsyl 66 |
. . . 4
⊢ (𝜑 → (𝐹‘1):ℝ⟶(0[,]+∞)) |
26 | | itg2cl 23305 |
. . . 4
⊢ ((𝐹‘1):ℝ⟶(0[,]+∞)
→ (∫2‘(𝐹‘1)) ∈
ℝ*) |
27 | 25, 26 | syl 17 |
. . 3
⊢ (𝜑 →
(∫2‘(𝐹‘1)) ∈
ℝ*) |
28 | | itg2ge0 23308 |
. . . . 5
⊢ ((𝐹‘1):ℝ⟶(0[,]+∞)
→ 0 ≤ (∫2‘(𝐹‘1))) |
29 | 25, 28 | syl 17 |
. . . 4
⊢ (𝜑 → 0 ≤
(∫2‘(𝐹‘1))) |
30 | | mnflt0 11835 |
. . . . 5
⊢ -∞
< 0 |
31 | | 0xr 9965 |
. . . . . . 7
⊢ 0 ∈
ℝ* |
32 | | xrltletr 11864 |
. . . . . . 7
⊢
((-∞ ∈ ℝ* ∧ 0 ∈ ℝ*
∧ (∫2‘(𝐹‘1)) ∈ ℝ*)
→ ((-∞ < 0 ∧ 0 ≤ (∫2‘(𝐹‘1))) → -∞ <
(∫2‘(𝐹‘1)))) |
33 | 18, 31, 32 | mp3an12 1406 |
. . . . . 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 708 |
. . . 4
⊢ (𝜑 → (0 ≤
(∫2‘(𝐹‘1)) → -∞ <
(∫2‘(𝐹‘1)))) |
36 | 29, 35 | mpd 15 |
. . 3
⊢ (𝜑 → -∞ <
(∫2‘(𝐹‘1))) |
37 | 22 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑛 = 1 →
(∫2‘(𝐹‘𝑛)) = (∫2‘(𝐹‘1))) |
38 | | fvex 6113 |
. . . . . . . 8
⊢
(∫2‘(𝐹‘1)) ∈ V |
39 | 37, 8, 38 | fvmpt 6191 |
. . . . . . 7
⊢ (1 ∈
ℕ → ((𝑛 ∈
ℕ ↦ (∫2‘(𝐹‘𝑛)))‘1) =
(∫2‘(𝐹‘1))) |
40 | 20, 39 | ax-mp 5 |
. . . . . 6
⊢ ((𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛)))‘1) =
(∫2‘(𝐹‘1)) |
41 | | ffn 5958 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))):ℕ⟶ℝ* →
(𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))) Fn ℕ) |
42 | 9, 41 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))) Fn ℕ) |
43 | | fnfvelrn 6264 |
. . . . . . 7
⊢ (((𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))) Fn ℕ ∧ 1 ∈ ℕ) →
((𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛)))‘1) ∈ ran (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛)))) |
44 | 42, 20, 43 | sylancl 693 |
. . . . . 6
⊢ (𝜑 → ((𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛)))‘1) ∈ ran (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛)))) |
45 | 40, 44 | syl5eqelr 2693 |
. . . . 5
⊢ (𝜑 →
(∫2‘(𝐹‘1)) ∈ ran (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛)))) |
46 | | supxrub 12026 |
. . . . 5
⊢ ((ran
(𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))) ⊆ ℝ* ∧
(∫2‘(𝐹‘1)) ∈ ran (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛)))) → (∫2‘(𝐹‘1)) ≤ sup(ran (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))), ℝ*, <
)) |
47 | 11, 45, 46 | syl2anc 691 |
. . . 4
⊢ (𝜑 →
(∫2‘(𝐹‘1)) ≤ sup(ran (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))), ℝ*, <
)) |
48 | 47, 1 | syl6breqr 4625 |
. . 3
⊢ (𝜑 →
(∫2‘(𝐹‘1)) ≤ 𝑆) |
49 | 19, 27, 14, 36, 48 | xrltletrd 11868 |
. 2
⊢ (𝜑 → -∞ < 𝑆) |
50 | | itg2monolem2.9 |
. . . 4
⊢ (𝜑 → ¬
(∫1‘𝑃)
≤ 𝑆) |
51 | 17 | rexrd 9968 |
. . . . 5
⊢ (𝜑 →
(∫1‘𝑃)
∈ ℝ*) |
52 | | xrltnle 9984 |
. . . . 5
⊢ ((𝑆 ∈ ℝ*
∧ (∫1‘𝑃) ∈ ℝ*) → (𝑆 <
(∫1‘𝑃)
↔ ¬ (∫1‘𝑃) ≤ 𝑆)) |
53 | 14, 51, 52 | syl2anc 691 |
. . . 4
⊢ (𝜑 → (𝑆 < (∫1‘𝑃) ↔ ¬
(∫1‘𝑃)
≤ 𝑆)) |
54 | 50, 53 | mpbird 246 |
. . 3
⊢ (𝜑 → 𝑆 < (∫1‘𝑃)) |
55 | | xrltle 11858 |
. . . 4
⊢ ((𝑆 ∈ ℝ*
∧ (∫1‘𝑃) ∈ ℝ*) → (𝑆 <
(∫1‘𝑃)
→ 𝑆 ≤
(∫1‘𝑃))) |
56 | 14, 51, 55 | syl2anc 691 |
. . 3
⊢ (𝜑 → (𝑆 < (∫1‘𝑃) → 𝑆 ≤ (∫1‘𝑃))) |
57 | 54, 56 | mpd 15 |
. 2
⊢ (𝜑 → 𝑆 ≤ (∫1‘𝑃)) |
58 | | xrre 11874 |
. 2
⊢ (((𝑆 ∈ ℝ*
∧ (∫1‘𝑃) ∈ ℝ) ∧ (-∞ < 𝑆 ∧ 𝑆 ≤ (∫1‘𝑃))) → 𝑆 ∈ ℝ) |
59 | 14, 17, 49, 57, 58 | syl22anc 1319 |
1
⊢ (𝜑 → 𝑆 ∈ ℝ) |