Step | Hyp | Ref
| Expression |
1 | | itg2mono.6 |
. . 3
β’ π = sup(ran (π β β β¦
(β«2β(πΉβπ))), β*, <
) |
2 | | itg2mono.3 |
. . . . . . . 8
β’ ((π β§ π β β) β (πΉβπ):ββΆ(0[,)+β)) |
3 | | icossicc 13362 |
. . . . . . . 8
β’
(0[,)+β) β (0[,]+β) |
4 | | fss 6689 |
. . . . . . . 8
β’ (((πΉβπ):ββΆ(0[,)+β) β§
(0[,)+β) β (0[,]+β)) β (πΉβπ):ββΆ(0[,]+β)) |
5 | 2, 3, 4 | sylancl 587 |
. . . . . . 7
β’ ((π β§ π β β) β (πΉβπ):ββΆ(0[,]+β)) |
6 | | itg2cl 25120 |
. . . . . . 7
β’ ((πΉβπ):ββΆ(0[,]+β) β
(β«2β(πΉβπ)) β
β*) |
7 | 5, 6 | syl 17 |
. . . . . 6
β’ ((π β§ π β β) β
(β«2β(πΉβπ)) β
β*) |
8 | 7 | fmpttd 7067 |
. . . . 5
β’ (π β (π β β β¦
(β«2β(πΉβπ))):ββΆβ*) |
9 | 8 | frnd 6680 |
. . . 4
β’ (π β ran (π β β β¦
(β«2β(πΉβπ))) β
β*) |
10 | | supxrcl 13243 |
. . . 4
β’ (ran
(π β β β¦
(β«2β(πΉβπ))) β β* β
sup(ran (π β β
β¦ (β«2β(πΉβπ))), β*, < ) β
β*) |
11 | 9, 10 | syl 17 |
. . 3
β’ (π β sup(ran (π β β β¦
(β«2β(πΉβπ))), β*, < ) β
β*) |
12 | 1, 11 | eqeltrid 2838 |
. 2
β’ (π β π β
β*) |
13 | | itg2monolem2.7 |
. . 3
β’ (π β π β dom
β«1) |
14 | | itg1cl 25072 |
. . 3
β’ (π β dom β«1
β (β«1βπ) β β) |
15 | 13, 14 | syl 17 |
. 2
β’ (π β
(β«1βπ)
β β) |
16 | | mnfxr 11220 |
. . . 4
β’ -β
β β* |
17 | 16 | a1i 11 |
. . 3
β’ (π β -β β
β*) |
18 | | fveq2 6846 |
. . . . . 6
β’ (π = 1 β (πΉβπ) = (πΉβ1)) |
19 | 18 | feq1d 6657 |
. . . . 5
β’ (π = 1 β ((πΉβπ):ββΆ(0[,]+β) β (πΉβ1):ββΆ(0[,]+β))) |
20 | 5 | ralrimiva 3140 |
. . . . 5
β’ (π β βπ β β (πΉβπ):ββΆ(0[,]+β)) |
21 | | 1nn 12172 |
. . . . . 6
β’ 1 β
β |
22 | 21 | a1i 11 |
. . . . 5
β’ (π β 1 β
β) |
23 | 19, 20, 22 | rspcdva 3584 |
. . . 4
β’ (π β (πΉβ1):ββΆ(0[,]+β)) |
24 | | itg2cl 25120 |
. . . 4
β’ ((πΉβ1):ββΆ(0[,]+β)
β (β«2β(πΉβ1)) β
β*) |
25 | 23, 24 | syl 17 |
. . 3
β’ (π β
(β«2β(πΉβ1)) β
β*) |
26 | | itg2ge0 25123 |
. . . . 5
β’ ((πΉβ1):ββΆ(0[,]+β)
β 0 β€ (β«2β(πΉβ1))) |
27 | 23, 26 | syl 17 |
. . . 4
β’ (π β 0 β€
(β«2β(πΉβ1))) |
28 | | mnflt0 13054 |
. . . . 5
β’ -β
< 0 |
29 | | 0xr 11210 |
. . . . . 6
β’ 0 β
β* |
30 | | xrltletr 13085 |
. . . . . 6
β’
((-β β β* β§ 0 β β*
β§ (β«2β(πΉβ1)) β β*)
β ((-β < 0 β§ 0 β€ (β«2β(πΉβ1))) β -β <
(β«2β(πΉβ1)))) |
31 | 16, 29, 25, 30 | mp3an12i 1466 |
. . . . 5
β’ (π β ((-β < 0 β§ 0
β€ (β«2β(πΉβ1))) β -β <
(β«2β(πΉβ1)))) |
32 | 28, 31 | mpani 695 |
. . . 4
β’ (π β (0 β€
(β«2β(πΉβ1)) β -β <
(β«2β(πΉβ1)))) |
33 | 27, 32 | mpd 15 |
. . 3
β’ (π β -β <
(β«2β(πΉβ1))) |
34 | | 2fveq3 6851 |
. . . . . . . 8
β’ (π = 1 β
(β«2β(πΉβπ)) = (β«2β(πΉβ1))) |
35 | | eqid 2733 |
. . . . . . . 8
β’ (π β β β¦
(β«2β(πΉβπ))) = (π β β β¦
(β«2β(πΉβπ))) |
36 | | fvex 6859 |
. . . . . . . 8
β’
(β«2β(πΉβ1)) β V |
37 | 34, 35, 36 | fvmpt 6952 |
. . . . . . 7
β’ (1 β
β β ((π β
β β¦ (β«2β(πΉβπ)))β1) =
(β«2β(πΉβ1))) |
38 | 21, 37 | ax-mp 5 |
. . . . . 6
β’ ((π β β β¦
(β«2β(πΉβπ)))β1) =
(β«2β(πΉβ1)) |
39 | 8 | ffnd 6673 |
. . . . . . 7
β’ (π β (π β β β¦
(β«2β(πΉβπ))) Fn β) |
40 | | fnfvelrn 7035 |
. . . . . . 7
β’ (((π β β β¦
(β«2β(πΉβπ))) Fn β β§ 1 β β) β
((π β β β¦
(β«2β(πΉβπ)))β1) β ran (π β β β¦
(β«2β(πΉβπ)))) |
41 | 39, 21, 40 | sylancl 587 |
. . . . . 6
β’ (π β ((π β β β¦
(β«2β(πΉβπ)))β1) β ran (π β β β¦
(β«2β(πΉβπ)))) |
42 | 38, 41 | eqeltrrid 2839 |
. . . . 5
β’ (π β
(β«2β(πΉβ1)) β ran (π β β β¦
(β«2β(πΉβπ)))) |
43 | | supxrub 13252 |
. . . . 5
β’ ((ran
(π β β β¦
(β«2β(πΉβπ))) β β* β§
(β«2β(πΉβ1)) β ran (π β β β¦
(β«2β(πΉβπ)))) β (β«2β(πΉβ1)) β€ sup(ran (π β β β¦
(β«2β(πΉβπ))), β*, <
)) |
44 | 9, 42, 43 | syl2anc 585 |
. . . 4
β’ (π β
(β«2β(πΉβ1)) β€ sup(ran (π β β β¦
(β«2β(πΉβπ))), β*, <
)) |
45 | 44, 1 | breqtrrdi 5151 |
. . 3
β’ (π β
(β«2β(πΉβ1)) β€ π) |
46 | 17, 25, 12, 33, 45 | xrltletrd 13089 |
. 2
β’ (π β -β < π) |
47 | 15 | rexrd 11213 |
. . 3
β’ (π β
(β«1βπ)
β β*) |
48 | | itg2monolem2.9 |
. . . 4
β’ (π β Β¬
(β«1βπ)
β€ π) |
49 | | xrltnle 11230 |
. . . . 5
β’ ((π β β*
β§ (β«1βπ) β β*) β (π <
(β«1βπ)
β Β¬ (β«1βπ) β€ π)) |
50 | 12, 47, 49 | syl2anc 585 |
. . . 4
β’ (π β (π < (β«1βπ) β Β¬
(β«1βπ)
β€ π)) |
51 | 48, 50 | mpbird 257 |
. . 3
β’ (π β π < (β«1βπ)) |
52 | 12, 47, 51 | xrltled 13078 |
. 2
β’ (π β π β€ (β«1βπ)) |
53 | | xrre 13097 |
. 2
β’ (((π β β*
β§ (β«1βπ) β β) β§ (-β < π β§ π β€ (β«1βπ))) β π β β) |
54 | 12, 15, 46, 52, 53 | syl22anc 838 |
1
β’ (π β π β β) |