Step | Hyp | Ref
| Expression |
1 | | omeiunltfirp.z |
. . . . . 6
β’ π =
(β€β₯βπ) |
2 | 1 | fvexi 6861 |
. . . . 5
β’ π β V |
3 | 2 | a1i 11 |
. . . 4
β’ ((π β§
(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) = +β) β π β V) |
4 | | omeiunltfirp.o |
. . . . . . . 8
β’ (π β π β OutMeas) |
5 | 4 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β π) β π β OutMeas) |
6 | | omeiunltfirp.x |
. . . . . . 7
β’ π = βͺ
dom π |
7 | | omeiunltfirp.e |
. . . . . . . . 9
β’ (π β πΈ:πβΆπ« π) |
8 | 7 | ffvelcdmda 7040 |
. . . . . . . 8
β’ ((π β§ π β π) β (πΈβπ) β π« π) |
9 | | fvex 6860 |
. . . . . . . . 9
β’ (πΈβπ) β V |
10 | 9 | elpw 4569 |
. . . . . . . 8
β’ ((πΈβπ) β π« π β (πΈβπ) β π) |
11 | 8, 10 | sylib 217 |
. . . . . . 7
β’ ((π β§ π β π) β (πΈβπ) β π) |
12 | 5, 6, 11 | omecl 44818 |
. . . . . 6
β’ ((π β§ π β π) β (πβ(πΈβπ)) β (0[,]+β)) |
13 | | eqid 2737 |
. . . . . 6
β’ (π β π β¦ (πβ(πΈβπ))) = (π β π β¦ (πβ(πΈβπ))) |
14 | 12, 13 | fmptd 7067 |
. . . . 5
β’ (π β (π β π β¦ (πβ(πΈβπ))):πβΆ(0[,]+β)) |
15 | 14 | adantr 482 |
. . . 4
β’ ((π β§
(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) = +β) β (π β π β¦ (πβ(πΈβπ))):πβΆ(0[,]+β)) |
16 | | simpr 486 |
. . . 4
β’ ((π β§
(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) = +β) β
(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) = +β) |
17 | | omeiunltfirp.re |
. . . . 5
β’ (π β (πββͺ
π β π (πΈβπ)) β β) |
18 | 17 | adantr 482 |
. . . 4
β’ ((π β§
(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) = +β) β (πββͺ
π β π (πΈβπ)) β β) |
19 | 3, 15, 16, 18 | sge0pnffigt 44711 |
. . 3
β’ ((π β§
(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) = +β) β βπ§ β (π« π β© Fin)(πββͺ
π β π (πΈβπ)) <
(Ξ£^β((π β π β¦ (πβ(πΈβπ))) βΎ π§))) |
20 | | simpl 484 |
. . . . . . 7
β’ (((π β§ π§ β (π« π β© Fin)) β§ (πββͺ
π β π (πΈβπ)) <
(Ξ£^β((π β π β¦ (πβ(πΈβπ))) βΎ π§))) β (π β§ π§ β (π« π β© Fin))) |
21 | | simpr 486 |
. . . . . . . . 9
β’ ((π§ β (π« π β© Fin) β§ (πββͺ π β π (πΈβπ)) <
(Ξ£^β((π β π β¦ (πβ(πΈβπ))) βΎ π§))) β (πββͺ
π β π (πΈβπ)) <
(Ξ£^β((π β π β¦ (πβ(πΈβπ))) βΎ π§))) |
22 | | elpwinss 43331 |
. . . . . . . . . . . 12
β’ (π§ β (π« π β© Fin) β π§ β π) |
23 | 22 | resmptd 5999 |
. . . . . . . . . . 11
β’ (π§ β (π« π β© Fin) β ((π β π β¦ (πβ(πΈβπ))) βΎ π§) = (π β π§ β¦ (πβ(πΈβπ)))) |
24 | 23 | fveq2d 6851 |
. . . . . . . . . 10
β’ (π§ β (π« π β© Fin) β
(Ξ£^β((π β π β¦ (πβ(πΈβπ))) βΎ π§)) =
(Ξ£^β(π β π§ β¦ (πβ(πΈβπ))))) |
25 | 24 | adantr 482 |
. . . . . . . . 9
β’ ((π§ β (π« π β© Fin) β§ (πββͺ π β π (πΈβπ)) <
(Ξ£^β((π β π β¦ (πβ(πΈβπ))) βΎ π§))) β
(Ξ£^β((π β π β¦ (πβ(πΈβπ))) βΎ π§)) =
(Ξ£^β(π β π§ β¦ (πβ(πΈβπ))))) |
26 | 21, 25 | breqtrd 5136 |
. . . . . . . 8
β’ ((π§ β (π« π β© Fin) β§ (πββͺ π β π (πΈβπ)) <
(Ξ£^β((π β π β¦ (πβ(πΈβπ))) βΎ π§))) β (πββͺ
π β π (πΈβπ)) <
(Ξ£^β(π β π§ β¦ (πβ(πΈβπ))))) |
27 | 26 | adantll 713 |
. . . . . . 7
β’ (((π β§ π§ β (π« π β© Fin)) β§ (πββͺ
π β π (πΈβπ)) <
(Ξ£^β((π β π β¦ (πβ(πΈβπ))) βΎ π§))) β (πββͺ
π β π (πΈβπ)) <
(Ξ£^β(π β π§ β¦ (πβ(πΈβπ))))) |
28 | 17 | rexrd 11212 |
. . . . . . . . 9
β’ (π β (πββͺ
π β π (πΈβπ)) β
β*) |
29 | 28 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π§ β (π« π β© Fin)) β§ (πββͺ
π β π (πΈβπ)) <
(Ξ£^β(π β π§ β¦ (πβ(πΈβπ))))) β (πββͺ
π β π (πΈβπ)) β
β*) |
30 | | simpr 486 |
. . . . . . . . . 10
β’ ((π β§ π§ β (π« π β© Fin)) β π§ β (π« π β© Fin)) |
31 | 4 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ π§ β (π« π β© Fin)) β§ π β π§) β π β OutMeas) |
32 | 7 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ π§ β (π« π β© Fin)) β§ π β π§) β πΈ:πβΆπ« π) |
33 | 22 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π§ β (π« π β© Fin) β§ π β π§) β π§ β π) |
34 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’ ((π§ β (π« π β© Fin) β§ π β π§) β π β π§) |
35 | 33, 34 | sseldd 3950 |
. . . . . . . . . . . . . . 15
β’ ((π§ β (π« π β© Fin) β§ π β π§) β π β π) |
36 | 35 | adantll 713 |
. . . . . . . . . . . . . 14
β’ (((π β§ π§ β (π« π β© Fin)) β§ π β π§) β π β π) |
37 | 32, 36 | ffvelcdmd 7041 |
. . . . . . . . . . . . 13
β’ (((π β§ π§ β (π« π β© Fin)) β§ π β π§) β (πΈβπ) β π« π) |
38 | 37, 10 | sylib 217 |
. . . . . . . . . . . 12
β’ (((π β§ π§ β (π« π β© Fin)) β§ π β π§) β (πΈβπ) β π) |
39 | 31, 6, 38 | omecl 44818 |
. . . . . . . . . . 11
β’ (((π β§ π§ β (π« π β© Fin)) β§ π β π§) β (πβ(πΈβπ)) β (0[,]+β)) |
40 | | eqid 2737 |
. . . . . . . . . . 11
β’ (π β π§ β¦ (πβ(πΈβπ))) = (π β π§ β¦ (πβ(πΈβπ))) |
41 | 39, 40 | fmptd 7067 |
. . . . . . . . . 10
β’ ((π β§ π§ β (π« π β© Fin)) β (π β π§ β¦ (πβ(πΈβπ))):π§βΆ(0[,]+β)) |
42 | 30, 41 | sge0xrcl 44700 |
. . . . . . . . 9
β’ ((π β§ π§ β (π« π β© Fin)) β
(Ξ£^β(π β π§ β¦ (πβ(πΈβπ)))) β
β*) |
43 | 42 | adantr 482 |
. . . . . . . 8
β’ (((π β§ π§ β (π« π β© Fin)) β§ (πββͺ
π β π (πΈβπ)) <
(Ξ£^β(π β π§ β¦ (πβ(πΈβπ))))) β
(Ξ£^β(π β π§ β¦ (πβ(πΈβπ)))) β
β*) |
44 | | elinel2 4161 |
. . . . . . . . . . . . 13
β’ (π§ β (π« π β© Fin) β π§ β Fin) |
45 | 44 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β§ π§ β (π« π β© Fin)) β π§ β Fin) |
46 | | rge0ssre 13380 |
. . . . . . . . . . . . 13
β’
(0[,)+β) β β |
47 | | 0xr 11209 |
. . . . . . . . . . . . . . 15
β’ 0 β
β* |
48 | 47 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (((π β§ π§ β (π« π β© Fin)) β§ π β π§) β 0 β
β*) |
49 | | pnfxr 11216 |
. . . . . . . . . . . . . . 15
β’ +β
β β* |
50 | 49 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (((π β§ π§ β (π« π β© Fin)) β§ π β π§) β +β β
β*) |
51 | 31, 6, 38 | omexrcl 44822 |
. . . . . . . . . . . . . 14
β’ (((π β§ π§ β (π« π β© Fin)) β§ π β π§) β (πβ(πΈβπ)) β
β*) |
52 | | iccgelb 13327 |
. . . . . . . . . . . . . . 15
β’ ((0
β β* β§ +β β β* β§
(πβ(πΈβπ)) β (0[,]+β)) β 0 β€
(πβ(πΈβπ))) |
53 | 48, 50, 39, 52 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ (((π β§ π§ β (π« π β© Fin)) β§ π β π§) β 0 β€ (πβ(πΈβπ))) |
54 | 11 | ralrimiva 3144 |
. . . . . . . . . . . . . . . . . 18
β’ (π β βπ β π (πΈβπ) β π) |
55 | | iunss 5010 |
. . . . . . . . . . . . . . . . . 18
β’ (βͺ π β π (πΈβπ) β π β βπ β π (πΈβπ) β π) |
56 | 54, 55 | sylibr 233 |
. . . . . . . . . . . . . . . . 17
β’ (π β βͺ π β π (πΈβπ) β π) |
57 | 56 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π§ β (π« π β© Fin)) β§ π β π§) β βͺ
π β π (πΈβπ) β π) |
58 | 31, 6, 57 | omexrcl 44822 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π§ β (π« π β© Fin)) β§ π β π§) β (πββͺ
π β π (πΈβπ)) β
β*) |
59 | | ssiun2 5012 |
. . . . . . . . . . . . . . . . 17
β’ (π β π β (πΈβπ) β βͺ
π β π (πΈβπ)) |
60 | 36, 59 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π§ β (π« π β© Fin)) β§ π β π§) β (πΈβπ) β βͺ
π β π (πΈβπ)) |
61 | 31, 6, 57, 60 | omessle 44813 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π§ β (π« π β© Fin)) β§ π β π§) β (πβ(πΈβπ)) β€ (πββͺ
π β π (πΈβπ))) |
62 | 17 | ltpnfd 13049 |
. . . . . . . . . . . . . . . 16
β’ (π β (πββͺ
π β π (πΈβπ)) < +β) |
63 | 62 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π§ β (π« π β© Fin)) β§ π β π§) β (πββͺ
π β π (πΈβπ)) < +β) |
64 | 51, 58, 50, 61, 63 | xrlelttrd 13086 |
. . . . . . . . . . . . . 14
β’ (((π β§ π§ β (π« π β© Fin)) β§ π β π§) β (πβ(πΈβπ)) < +β) |
65 | 48, 50, 51, 53, 64 | elicod 13321 |
. . . . . . . . . . . . 13
β’ (((π β§ π§ β (π« π β© Fin)) β§ π β π§) β (πβ(πΈβπ)) β (0[,)+β)) |
66 | 46, 65 | sselid 3947 |
. . . . . . . . . . . 12
β’ (((π β§ π§ β (π« π β© Fin)) β§ π β π§) β (πβ(πΈβπ)) β β) |
67 | 45, 66 | fsumrecl 15626 |
. . . . . . . . . . 11
β’ ((π β§ π§ β (π« π β© Fin)) β Ξ£π β π§ (πβ(πΈβπ)) β β) |
68 | | omeiunltfirp.y |
. . . . . . . . . . . . 13
β’ (π β π β
β+) |
69 | 68 | rpred 12964 |
. . . . . . . . . . . 12
β’ (π β π β β) |
70 | 69 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π§ β (π« π β© Fin)) β π β β) |
71 | 67, 70 | readdcld 11191 |
. . . . . . . . . 10
β’ ((π β§ π§ β (π« π β© Fin)) β (Ξ£π β π§ (πβ(πΈβπ)) + π) β β) |
72 | 71 | rexrd 11212 |
. . . . . . . . 9
β’ ((π β§ π§ β (π« π β© Fin)) β (Ξ£π β π§ (πβ(πΈβπ)) + π) β
β*) |
73 | 72 | adantr 482 |
. . . . . . . 8
β’ (((π β§ π§ β (π« π β© Fin)) β§ (πββͺ
π β π (πΈβπ)) <
(Ξ£^β(π β π§ β¦ (πβ(πΈβπ))))) β (Ξ£π β π§ (πβ(πΈβπ)) + π) β
β*) |
74 | | simpr 486 |
. . . . . . . 8
β’ (((π β§ π§ β (π« π β© Fin)) β§ (πββͺ
π β π (πΈβπ)) <
(Ξ£^β(π β π§ β¦ (πβ(πΈβπ))))) β (πββͺ
π β π (πΈβπ)) <
(Ξ£^β(π β π§ β¦ (πβ(πΈβπ))))) |
75 | 65, 40 | fmptd 7067 |
. . . . . . . . . . . 12
β’ ((π β§ π§ β (π« π β© Fin)) β (π β π§ β¦ (πβ(πΈβπ))):π§βΆ(0[,)+β)) |
76 | 45, 75 | sge0fsum 44702 |
. . . . . . . . . . 11
β’ ((π β§ π§ β (π« π β© Fin)) β
(Ξ£^β(π β π§ β¦ (πβ(πΈβπ)))) = Ξ£π β π§ ((π β π§ β¦ (πβ(πΈβπ)))βπ)) |
77 | | eqidd 2738 |
. . . . . . . . . . . . 13
β’ (((π β§ π§ β (π« π β© Fin)) β§ π β π§) β (π β π§ β¦ (πβ(πΈβπ))) = (π β π§ β¦ (πβ(πΈβπ)))) |
78 | | 2fveq3 6852 |
. . . . . . . . . . . . . 14
β’ (π = π β (πβ(πΈβπ)) = (πβ(πΈβπ))) |
79 | 78 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((((π β§ π§ β (π« π β© Fin)) β§ π β π§) β§ π = π) β (πβ(πΈβπ)) = (πβ(πΈβπ))) |
80 | | simpr 486 |
. . . . . . . . . . . . 13
β’ (((π β§ π§ β (π« π β© Fin)) β§ π β π§) β π β π§) |
81 | | fvexd 6862 |
. . . . . . . . . . . . 13
β’ (((π β§ π§ β (π« π β© Fin)) β§ π β π§) β (πβ(πΈβπ)) β V) |
82 | 77, 79, 80, 81 | fvmptd 6960 |
. . . . . . . . . . . 12
β’ (((π β§ π§ β (π« π β© Fin)) β§ π β π§) β ((π β π§ β¦ (πβ(πΈβπ)))βπ) = (πβ(πΈβπ))) |
83 | 82 | sumeq2dv 15595 |
. . . . . . . . . . 11
β’ ((π β§ π§ β (π« π β© Fin)) β Ξ£π β π§ ((π β π§ β¦ (πβ(πΈβπ)))βπ) = Ξ£π β π§ (πβ(πΈβπ))) |
84 | | 2fveq3 6852 |
. . . . . . . . . . . . 13
β’ (π = π β (πβ(πΈβπ)) = (πβ(πΈβπ))) |
85 | 84 | cbvsumv 15588 |
. . . . . . . . . . . 12
β’
Ξ£π β
π§ (πβ(πΈβπ)) = Ξ£π β π§ (πβ(πΈβπ)) |
86 | 85 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β§ π§ β (π« π β© Fin)) β Ξ£π β π§ (πβ(πΈβπ)) = Ξ£π β π§ (πβ(πΈβπ))) |
87 | 76, 83, 86 | 3eqtrd 2781 |
. . . . . . . . . 10
β’ ((π β§ π§ β (π« π β© Fin)) β
(Ξ£^β(π β π§ β¦ (πβ(πΈβπ)))) = Ξ£π β π§ (πβ(πΈβπ))) |
88 | 68 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π§ β (π« π β© Fin)) β π β
β+) |
89 | 67, 88 | ltaddrpd 12997 |
. . . . . . . . . 10
β’ ((π β§ π§ β (π« π β© Fin)) β Ξ£π β π§ (πβ(πΈβπ)) < (Ξ£π β π§ (πβ(πΈβπ)) + π)) |
90 | 87, 89 | eqbrtrd 5132 |
. . . . . . . . 9
β’ ((π β§ π§ β (π« π β© Fin)) β
(Ξ£^β(π β π§ β¦ (πβ(πΈβπ)))) < (Ξ£π β π§ (πβ(πΈβπ)) + π)) |
91 | 90 | adantr 482 |
. . . . . . . 8
β’ (((π β§ π§ β (π« π β© Fin)) β§ (πββͺ
π β π (πΈβπ)) <
(Ξ£^β(π β π§ β¦ (πβ(πΈβπ))))) β
(Ξ£^β(π β π§ β¦ (πβ(πΈβπ)))) < (Ξ£π β π§ (πβ(πΈβπ)) + π)) |
92 | 29, 43, 73, 74, 91 | xrlttrd 13085 |
. . . . . . 7
β’ (((π β§ π§ β (π« π β© Fin)) β§ (πββͺ
π β π (πΈβπ)) <
(Ξ£^β(π β π§ β¦ (πβ(πΈβπ))))) β (πββͺ
π β π (πΈβπ)) < (Ξ£π β π§ (πβ(πΈβπ)) + π)) |
93 | 20, 27, 92 | syl2anc 585 |
. . . . . 6
β’ (((π β§ π§ β (π« π β© Fin)) β§ (πββͺ
π β π (πΈβπ)) <
(Ξ£^β((π β π β¦ (πβ(πΈβπ))) βΎ π§))) β (πββͺ
π β π (πΈβπ)) < (Ξ£π β π§ (πβ(πΈβπ)) + π)) |
94 | 93 | ex 414 |
. . . . 5
β’ ((π β§ π§ β (π« π β© Fin)) β ((πββͺ
π β π (πΈβπ)) <
(Ξ£^β((π β π β¦ (πβ(πΈβπ))) βΎ π§)) β (πββͺ
π β π (πΈβπ)) < (Ξ£π β π§ (πβ(πΈβπ)) + π))) |
95 | 94 | adantlr 714 |
. . . 4
β’ (((π β§
(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) = +β) β§ π§ β (π« π β© Fin)) β ((πββͺ
π β π (πΈβπ)) <
(Ξ£^β((π β π β¦ (πβ(πΈβπ))) βΎ π§)) β (πββͺ
π β π (πΈβπ)) < (Ξ£π β π§ (πβ(πΈβπ)) + π))) |
96 | 95 | reximdva 3166 |
. . 3
β’ ((π β§
(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) = +β) β (βπ§ β (π« π β© Fin)(πββͺ
π β π (πΈβπ)) <
(Ξ£^β((π β π β¦ (πβ(πΈβπ))) βΎ π§)) β βπ§ β (π« π β© Fin)(πββͺ
π β π (πΈβπ)) < (Ξ£π β π§ (πβ(πΈβπ)) + π))) |
97 | 19, 96 | mpd 15 |
. 2
β’ ((π β§
(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) = +β) β βπ§ β (π« π β© Fin)(πββͺ
π β π (πΈβπ)) < (Ξ£π β π§ (πβ(πΈβπ)) + π)) |
98 | | simpl 484 |
. . 3
β’ ((π β§ Β¬
(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) = +β) β π) |
99 | | simpr 486 |
. . . 4
β’ ((π β§ Β¬
(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) = +β) β Β¬
(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) = +β) |
100 | 2 | a1i 11 |
. . . . . 6
β’ (π β π β V) |
101 | 100, 14 | sge0repnf 44701 |
. . . . 5
β’ (π β
((Ξ£^β(π β π β¦ (πβ(πΈβπ)))) β β β Β¬
(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) = +β)) |
102 | 101 | adantr 482 |
. . . 4
β’ ((π β§ Β¬
(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) = +β) β
((Ξ£^β(π β π β¦ (πβ(πΈβπ)))) β β β Β¬
(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) = +β)) |
103 | 99, 102 | mpbird 257 |
. . 3
β’ ((π β§ Β¬
(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) = +β) β
(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) β β) |
104 | | nfv 1918 |
. . . . . 6
β’
β²ππ |
105 | | nfcv 2908 |
. . . . . . . 8
β’
β²πΞ£^ |
106 | | nfmpt1 5218 |
. . . . . . . 8
β’
β²π(π β π β¦ (πβ(πΈβπ))) |
107 | 105, 106 | nffv 6857 |
. . . . . . 7
β’
β²π(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) |
108 | | nfcv 2908 |
. . . . . . 7
β’
β²πβ |
109 | 107, 108 | nfel 2922 |
. . . . . 6
β’
β²π(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) β β |
110 | 104, 109 | nfan 1903 |
. . . . 5
β’
β²π(π β§
(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) β β) |
111 | 2 | a1i 11 |
. . . . 5
β’ ((π β§
(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) β β) β π β V) |
112 | 12 | adantlr 714 |
. . . . 5
β’ (((π β§
(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) β β) β§ π β π) β (πβ(πΈβπ)) β (0[,]+β)) |
113 | 68 | adantr 482 |
. . . . 5
β’ ((π β§
(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) β β) β π β
β+) |
114 | | simpr 486 |
. . . . 5
β’ ((π β§
(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) β β) β
(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) β β) |
115 | 110, 111,
112, 113, 114 | sge0ltfirpmpt 44723 |
. . . 4
β’ ((π β§
(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) β β) β βπ§ β (π« π β©
Fin)(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) <
((Ξ£^β(π β π§ β¦ (πβ(πΈβπ)))) + π)) |
116 | 17 | ad3antrrr 729 |
. . . . . . 7
β’ ((((π β§
(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) β β) β§ π§ β (π« π β© Fin)) β§
(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) <
((Ξ£^β(π β π§ β¦ (πβ(πΈβπ)))) + π)) β (πββͺ
π β π (πΈβπ)) β β) |
117 | 114 | ad2antrr 725 |
. . . . . . 7
β’ ((((π β§
(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) β β) β§ π§ β (π« π β© Fin)) β§
(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) <
((Ξ£^β(π β π§ β¦ (πβ(πΈβπ)))) + π)) β
(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) β β) |
118 | 71 | ad4ant13 750 |
. . . . . . 7
β’ ((((π β§
(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) β β) β§ π§ β (π« π β© Fin)) β§
(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) <
((Ξ£^β(π β π§ β¦ (πβ(πΈβπ)))) + π)) β (Ξ£π β π§ (πβ(πΈβπ)) + π) β β) |
119 | | nfcv 2908 |
. . . . . . . . 9
β’
β²ππΈ |
120 | 104, 119,
4, 6, 1, 7 | omeiunle 44832 |
. . . . . . . 8
β’ (π β (πββͺ
π β π (πΈβπ)) β€
(Ξ£^β(π β π β¦ (πβ(πΈβπ))))) |
121 | 120 | ad3antrrr 729 |
. . . . . . 7
β’ ((((π β§
(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) β β) β§ π§ β (π« π β© Fin)) β§
(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) <
((Ξ£^β(π β π§ β¦ (πβ(πΈβπ)))) + π)) β (πββͺ
π β π (πΈβπ)) β€
(Ξ£^β(π β π β¦ (πβ(πΈβπ))))) |
122 | | simpr 486 |
. . . . . . . 8
β’ ((((π β§
(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) β β) β§ π§ β (π« π β© Fin)) β§
(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) <
((Ξ£^β(π β π§ β¦ (πβ(πΈβπ)))) + π)) β
(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) <
((Ξ£^β(π β π§ β¦ (πβ(πΈβπ)))) + π)) |
123 | | simpll 766 |
. . . . . . . . . . 11
β’ (((π β§
(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) β β) β§ π§ β (π« π β© Fin)) β π) |
124 | | 2fveq3 6852 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (πβ(πΈβπ)) = (πβ(πΈβπ))) |
125 | 124 | cbvmptv 5223 |
. . . . . . . . . . . . . . 15
β’ (π β π β¦ (πβ(πΈβπ))) = (π β π β¦ (πβ(πΈβπ))) |
126 | 125 | fveq2i 6850 |
. . . . . . . . . . . . . 14
β’
(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) =
(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) |
127 | 126 | eleq1i 2829 |
. . . . . . . . . . . . 13
β’
((Ξ£^β(π β π β¦ (πβ(πΈβπ)))) β β β
(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) β β) |
128 | 127 | biimpi 215 |
. . . . . . . . . . . 12
β’
((Ξ£^β(π β π β¦ (πβ(πΈβπ)))) β β β
(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) β β) |
129 | 128 | ad2antlr 726 |
. . . . . . . . . . 11
β’ (((π β§
(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) β β) β§ π§ β (π« π β© Fin)) β
(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) β β) |
130 | | simpr 486 |
. . . . . . . . . . 11
β’ (((π β§
(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) β β) β§ π§ β (π« π β© Fin)) β π§ β (π« π β© Fin)) |
131 | 44 | adantl 483 |
. . . . . . . . . . . 12
β’ (((π β§
(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) β β) β§ π§ β (π« π β© Fin)) β π§ β Fin) |
132 | 65 | adantllr 718 |
. . . . . . . . . . . 12
β’ ((((π β§
(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) β β) β§ π§ β (π« π β© Fin)) β§ π β π§) β (πβ(πΈβπ)) β (0[,)+β)) |
133 | 131, 132 | sge0fsummpt 44705 |
. . . . . . . . . . 11
β’ (((π β§
(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) β β) β§ π§ β (π« π β© Fin)) β
(Ξ£^β(π β π§ β¦ (πβ(πΈβπ)))) = Ξ£π β π§ (πβ(πΈβπ))) |
134 | 123, 129,
130, 133 | syl21anc 837 |
. . . . . . . . . 10
β’ (((π β§
(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) β β) β§ π§ β (π« π β© Fin)) β
(Ξ£^β(π β π§ β¦ (πβ(πΈβπ)))) = Ξ£π β π§ (πβ(πΈβπ))) |
135 | 134 | oveq1d 7377 |
. . . . . . . . 9
β’ (((π β§
(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) β β) β§ π§ β (π« π β© Fin)) β
((Ξ£^β(π β π§ β¦ (πβ(πΈβπ)))) + π) = (Ξ£π β π§ (πβ(πΈβπ)) + π)) |
136 | 135 | adantr 482 |
. . . . . . . 8
β’ ((((π β§
(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) β β) β§ π§ β (π« π β© Fin)) β§
(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) <
((Ξ£^β(π β π§ β¦ (πβ(πΈβπ)))) + π)) β
((Ξ£^β(π β π§ β¦ (πβ(πΈβπ)))) + π) = (Ξ£π β π§ (πβ(πΈβπ)) + π)) |
137 | 122, 136 | breqtrd 5136 |
. . . . . . 7
β’ ((((π β§
(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) β β) β§ π§ β (π« π β© Fin)) β§
(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) <
((Ξ£^β(π β π§ β¦ (πβ(πΈβπ)))) + π)) β
(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) < (Ξ£π β π§ (πβ(πΈβπ)) + π)) |
138 | 116, 117,
118, 121, 137 | lelttrd 11320 |
. . . . . 6
β’ ((((π β§
(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) β β) β§ π§ β (π« π β© Fin)) β§
(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) <
((Ξ£^β(π β π§ β¦ (πβ(πΈβπ)))) + π)) β (πββͺ
π β π (πΈβπ)) < (Ξ£π β π§ (πβ(πΈβπ)) + π)) |
139 | 138 | ex 414 |
. . . . 5
β’ (((π β§
(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) β β) β§ π§ β (π« π β© Fin)) β
((Ξ£^β(π β π β¦ (πβ(πΈβπ)))) <
((Ξ£^β(π β π§ β¦ (πβ(πΈβπ)))) + π) β (πββͺ
π β π (πΈβπ)) < (Ξ£π β π§ (πβ(πΈβπ)) + π))) |
140 | 139 | reximdva 3166 |
. . . 4
β’ ((π β§
(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) β β) β (βπ§ β (π« π β©
Fin)(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) <
((Ξ£^β(π β π§ β¦ (πβ(πΈβπ)))) + π) β βπ§ β (π« π β© Fin)(πββͺ
π β π (πΈβπ)) < (Ξ£π β π§ (πβ(πΈβπ)) + π))) |
141 | 115, 140 | mpd 15 |
. . 3
β’ ((π β§
(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) β β) β βπ§ β (π« π β© Fin)(πββͺ
π β π (πΈβπ)) < (Ξ£π β π§ (πβ(πΈβπ)) + π)) |
142 | 98, 103, 141 | syl2anc 585 |
. 2
β’ ((π β§ Β¬
(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) = +β) β βπ§ β (π« π β© Fin)(πββͺ
π β π (πΈβπ)) < (Ξ£π β π§ (πβ(πΈβπ)) + π)) |
143 | 97, 142 | pm2.61dan 812 |
1
β’ (π β βπ§ β (π« π β© Fin)(πββͺ
π β π (πΈβπ)) < (Ξ£π β π§ (πβ(πΈβπ)) + π)) |