Step | Hyp | Ref
| Expression |
1 | | xrofsup.5 |
. . 3
β’ (π β π = ( +π β (π Γ π))) |
2 | | xrofsup.1 |
. . . . . . . . . 10
β’ (π β π β
β*) |
3 | 2 | sseld 3982 |
. . . . . . . . 9
β’ (π β (π₯ β π β π₯ β
β*)) |
4 | | xrofsup.2 |
. . . . . . . . . 10
β’ (π β π β
β*) |
5 | 4 | sseld 3982 |
. . . . . . . . 9
β’ (π β (π¦ β π β π¦ β
β*)) |
6 | 3, 5 | anim12d 610 |
. . . . . . . 8
β’ (π β ((π₯ β π β§ π¦ β π) β (π₯ β β* β§ π¦ β
β*))) |
7 | 6 | imp 408 |
. . . . . . 7
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ β β* β§ π¦ β
β*)) |
8 | | xaddcl 13218 |
. . . . . . 7
β’ ((π₯ β β*
β§ π¦ β
β*) β (π₯ +π π¦) β
β*) |
9 | 7, 8 | syl 17 |
. . . . . 6
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ +π π¦) β
β*) |
10 | 9 | ralrimivva 3201 |
. . . . 5
β’ (π β βπ₯ β π βπ¦ β π (π₯ +π π¦) β
β*) |
11 | | fveq2 6892 |
. . . . . . . 8
β’ (π’ = β¨π₯, π¦β© β ( +π
βπ’) = (
+π ββ¨π₯, π¦β©)) |
12 | | df-ov 7412 |
. . . . . . . 8
β’ (π₯ +π π¦) = ( +π
ββ¨π₯, π¦β©) |
13 | 11, 12 | eqtr4di 2791 |
. . . . . . 7
β’ (π’ = β¨π₯, π¦β© β ( +π
βπ’) = (π₯ +π π¦)) |
14 | 13 | eleq1d 2819 |
. . . . . 6
β’ (π’ = β¨π₯, π¦β© β (( +π
βπ’) β
β* β (π₯ +π π¦) β
β*)) |
15 | 14 | ralxp 5842 |
. . . . 5
β’
(βπ’ β
(π Γ π)( +π
βπ’) β
β* β βπ₯ β π βπ¦ β π (π₯ +π π¦) β
β*) |
16 | 10, 15 | sylibr 233 |
. . . 4
β’ (π β βπ’ β (π Γ π)( +π βπ’) β
β*) |
17 | | xaddf 13203 |
. . . . . 6
β’
+π :(β* Γ
β*)βΆβ* |
18 | | ffun 6721 |
. . . . . 6
β’ (
+π :(β* Γ
β*)βΆβ* β Fun
+π ) |
19 | 17, 18 | ax-mp 5 |
. . . . 5
β’ Fun
+π |
20 | | xpss12 5692 |
. . . . . . 7
β’ ((π β β*
β§ π β
β*) β (π Γ π) β (β* Γ
β*)) |
21 | 2, 4, 20 | syl2anc 585 |
. . . . . 6
β’ (π β (π Γ π) β (β* Γ
β*)) |
22 | 17 | fdmi 6730 |
. . . . . 6
β’ dom
+π = (β* Γ
β*) |
23 | 21, 22 | sseqtrrdi 4034 |
. . . . 5
β’ (π β (π Γ π) β dom +π
) |
24 | | funimass4 6957 |
. . . . 5
β’ ((Fun
+π β§ (π Γ π) β dom +π ) β
(( +π β (π Γ π)) β β* β
βπ’ β (π Γ π)( +π βπ’) β
β*)) |
25 | 19, 23, 24 | sylancr 588 |
. . . 4
β’ (π β (( +π
β (π Γ π)) β β*
β βπ’ β
(π Γ π)( +π
βπ’) β
β*)) |
26 | 16, 25 | mpbird 257 |
. . 3
β’ (π β ( +π
β (π Γ π)) β
β*) |
27 | 1, 26 | eqsstrd 4021 |
. 2
β’ (π β π β
β*) |
28 | | supxrcl 13294 |
. . . 4
β’ (π β β*
β sup(π,
β*, < ) β β*) |
29 | 2, 28 | syl 17 |
. . 3
β’ (π β sup(π, β*, < ) β
β*) |
30 | | supxrcl 13294 |
. . . 4
β’ (π β β*
β sup(π,
β*, < ) β β*) |
31 | 4, 30 | syl 17 |
. . 3
β’ (π β sup(π, β*, < ) β
β*) |
32 | 29, 31 | xaddcld 13280 |
. 2
β’ (π β (sup(π, β*, < )
+π sup(π, β*, < )) β
β*) |
33 | 1 | eleq2d 2820 |
. . . . 5
β’ (π β (π§ β π β π§ β ( +π β
(π Γ π)))) |
34 | 33 | pm5.32i 576 |
. . . 4
β’ ((π β§ π§ β π) β (π β§ π§ β ( +π β
(π Γ π)))) |
35 | | nfvd 1919 |
. . . . 5
β’ ((π β§ π§ β ( +π β
(π Γ π))) β β²π₯ π§ β€ (sup(π, β*, < )
+π sup(π, β*, <
))) |
36 | | nfvd 1919 |
. . . . 5
β’ ((π β§ π§ β ( +π β
(π Γ π))) β β²π¦ π§ β€ (sup(π, β*, < )
+π sup(π, β*, <
))) |
37 | 2 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π§ β ( +π β
(π Γ π))) β§ (π₯ β π β§ π¦ β π)) β π β
β*) |
38 | | simprl 770 |
. . . . . . . . . . 11
β’ (((π β§ π§ β ( +π β
(π Γ π))) β§ (π₯ β π β§ π¦ β π)) β π₯ β π) |
39 | | supxrub 13303 |
. . . . . . . . . . 11
β’ ((π β β*
β§ π₯ β π) β π₯ β€ sup(π, β*, <
)) |
40 | 37, 38, 39 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π β§ π§ β ( +π β
(π Γ π))) β§ (π₯ β π β§ π¦ β π)) β π₯ β€ sup(π, β*, <
)) |
41 | 4 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π§ β ( +π β
(π Γ π))) β§ (π₯ β π β§ π¦ β π)) β π β
β*) |
42 | | simprr 772 |
. . . . . . . . . . 11
β’ (((π β§ π§ β ( +π β
(π Γ π))) β§ (π₯ β π β§ π¦ β π)) β π¦ β π) |
43 | | supxrub 13303 |
. . . . . . . . . . 11
β’ ((π β β*
β§ π¦ β π) β π¦ β€ sup(π, β*, <
)) |
44 | 41, 42, 43 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π β§ π§ β ( +π β
(π Γ π))) β§ (π₯ β π β§ π¦ β π)) β π¦ β€ sup(π, β*, <
)) |
45 | 37, 38 | sseldd 3984 |
. . . . . . . . . . 11
β’ (((π β§ π§ β ( +π β
(π Γ π))) β§ (π₯ β π β§ π¦ β π)) β π₯ β β*) |
46 | 41, 42 | sseldd 3984 |
. . . . . . . . . . 11
β’ (((π β§ π§ β ( +π β
(π Γ π))) β§ (π₯ β π β§ π¦ β π)) β π¦ β β*) |
47 | 37, 28 | syl 17 |
. . . . . . . . . . 11
β’ (((π β§ π§ β ( +π β
(π Γ π))) β§ (π₯ β π β§ π¦ β π)) β sup(π, β*, < ) β
β*) |
48 | 41, 30 | syl 17 |
. . . . . . . . . . 11
β’ (((π β§ π§ β ( +π β
(π Γ π))) β§ (π₯ β π β§ π¦ β π)) β sup(π, β*, < ) β
β*) |
49 | | xle2add 13238 |
. . . . . . . . . . 11
β’ (((π₯ β β*
β§ π¦ β
β*) β§ (sup(π, β*, < ) β
β* β§ sup(π, β*, < ) β
β*)) β ((π₯ β€ sup(π, β*, < ) β§ π¦ β€ sup(π, β*, < )) β (π₯ +π π¦) β€ (sup(π, β*, < )
+π sup(π, β*, <
)))) |
50 | 45, 46, 47, 48, 49 | syl22anc 838 |
. . . . . . . . . 10
β’ (((π β§ π§ β ( +π β
(π Γ π))) β§ (π₯ β π β§ π¦ β π)) β ((π₯ β€ sup(π, β*, < ) β§ π¦ β€ sup(π, β*, < )) β (π₯ +π π¦) β€ (sup(π, β*, < )
+π sup(π, β*, <
)))) |
51 | 40, 44, 50 | mp2and 698 |
. . . . . . . . 9
β’ (((π β§ π§ β ( +π β
(π Γ π))) β§ (π₯ β π β§ π¦ β π)) β (π₯ +π π¦) β€ (sup(π, β*, < )
+π sup(π, β*, <
))) |
52 | 51 | ralrimivva 3201 |
. . . . . . . 8
β’ ((π β§ π§ β ( +π β
(π Γ π))) β βπ₯ β π βπ¦ β π (π₯ +π π¦) β€ (sup(π, β*, < )
+π sup(π, β*, <
))) |
53 | | fvelima 6958 |
. . . . . . . . . . 11
β’ ((Fun
+π β§ π§ β ( +π β
(π Γ π))) β βπ’ β (π Γ π)( +π βπ’) = π§) |
54 | 19, 53 | mpan 689 |
. . . . . . . . . 10
β’ (π§ β ( +π
β (π Γ π)) β βπ’ β (π Γ π)( +π βπ’) = π§) |
55 | 54 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π§ β ( +π β
(π Γ π))) β βπ’ β (π Γ π)( +π βπ’) = π§) |
56 | 13 | eqeq1d 2735 |
. . . . . . . . . 10
β’ (π’ = β¨π₯, π¦β© β (( +π
βπ’) = π§ β (π₯ +π π¦) = π§)) |
57 | 56 | rexxp 5843 |
. . . . . . . . 9
β’
(βπ’ β
(π Γ π)( +π
βπ’) = π§ β βπ₯ β π βπ¦ β π (π₯ +π π¦) = π§) |
58 | 55, 57 | sylib 217 |
. . . . . . . 8
β’ ((π β§ π§ β ( +π β
(π Γ π))) β βπ₯ β π βπ¦ β π (π₯ +π π¦) = π§) |
59 | 52, 58 | r19.29d2r 3141 |
. . . . . . 7
β’ ((π β§ π§ β ( +π β
(π Γ π))) β βπ₯ β π βπ¦ β π ((π₯ +π π¦) β€ (sup(π, β*, < )
+π sup(π, β*, < )) β§ (π₯ +π π¦) = π§)) |
60 | | ancom 462 |
. . . . . . . 8
β’ (((π₯ +π π¦) β€ (sup(π, β*, < )
+π sup(π, β*, < )) β§ (π₯ +π π¦) = π§) β ((π₯ +π π¦) = π§ β§ (π₯ +π π¦) β€ (sup(π, β*, < )
+π sup(π, β*, <
)))) |
61 | 60 | 2rexbii 3130 |
. . . . . . 7
β’
(βπ₯ β
π βπ¦ β π ((π₯ +π π¦) β€ (sup(π, β*, < )
+π sup(π, β*, < )) β§ (π₯ +π π¦) = π§) β βπ₯ β π βπ¦ β π ((π₯ +π π¦) = π§ β§ (π₯ +π π¦) β€ (sup(π, β*, < )
+π sup(π, β*, <
)))) |
62 | 59, 61 | sylib 217 |
. . . . . 6
β’ ((π β§ π§ β ( +π β
(π Γ π))) β βπ₯ β π βπ¦ β π ((π₯ +π π¦) = π§ β§ (π₯ +π π¦) β€ (sup(π, β*, < )
+π sup(π, β*, <
)))) |
63 | | breq1 5152 |
. . . . . . . . 9
β’ ((π₯ +π π¦) = π§ β ((π₯ +π π¦) β€ (sup(π, β*, < )
+π sup(π, β*, < )) β π§ β€ (sup(π, β*, < )
+π sup(π, β*, <
)))) |
64 | 63 | biimpa 478 |
. . . . . . . 8
β’ (((π₯ +π π¦) = π§ β§ (π₯ +π π¦) β€ (sup(π, β*, < )
+π sup(π, β*, < ))) β π§ β€ (sup(π, β*, < )
+π sup(π, β*, <
))) |
65 | 64 | reximi 3085 |
. . . . . . 7
β’
(βπ¦ β
π ((π₯ +π π¦) = π§ β§ (π₯ +π π¦) β€ (sup(π, β*, < )
+π sup(π, β*, < ))) β
βπ¦ β π π§ β€ (sup(π, β*, < )
+π sup(π, β*, <
))) |
66 | 65 | reximi 3085 |
. . . . . 6
β’
(βπ₯ β
π βπ¦ β π ((π₯ +π π¦) = π§ β§ (π₯ +π π¦) β€ (sup(π, β*, < )
+π sup(π, β*, < ))) β
βπ₯ β π βπ¦ β π π§ β€ (sup(π, β*, < )
+π sup(π, β*, <
))) |
67 | 62, 66 | syl 17 |
. . . . 5
β’ ((π β§ π§ β ( +π β
(π Γ π))) β βπ₯ β π βπ¦ β π π§ β€ (sup(π, β*, < )
+π sup(π, β*, <
))) |
68 | 35, 36, 67 | 19.9d2r 31712 |
. . . 4
β’ ((π β§ π§ β ( +π β
(π Γ π))) β π§ β€ (sup(π, β*, < )
+π sup(π, β*, <
))) |
69 | 34, 68 | sylbi 216 |
. . 3
β’ ((π β§ π§ β π) β π§ β€ (sup(π, β*, < )
+π sup(π, β*, <
))) |
70 | 69 | ralrimiva 3147 |
. 2
β’ (π β βπ§ β π π§ β€ (sup(π, β*, < )
+π sup(π, β*, <
))) |
71 | 2 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π§ β β) β§ π§ < (sup(π, β*, < )
+π sup(π, β*, < ))) β π β
β*) |
72 | 4 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π§ β β) β§ π§ < (sup(π, β*, < )
+π sup(π, β*, < ))) β π β
β*) |
73 | | simplr 768 |
. . . . . . 7
β’ (((π β§ π§ β β) β§ π§ < (sup(π, β*, < )
+π sup(π, β*, < ))) β π§ β
β) |
74 | 29 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π§ β β) β§ π§ < (sup(π, β*, < )
+π sup(π, β*, < ))) β
sup(π, β*,
< ) β β*) |
75 | 31 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π§ β β) β§ π§ < (sup(π, β*, < )
+π sup(π, β*, < ))) β
sup(π, β*,
< ) β β*) |
76 | | xrofsup.3 |
. . . . . . . 8
β’ (π β sup(π, β*, < ) β
-β) |
77 | 76 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π§ β β) β§ π§ < (sup(π, β*, < )
+π sup(π, β*, < ))) β
sup(π, β*,
< ) β -β) |
78 | | xrofsup.4 |
. . . . . . . 8
β’ (π β sup(π, β*, < ) β
-β) |
79 | 78 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π§ β β) β§ π§ < (sup(π, β*, < )
+π sup(π, β*, < ))) β
sup(π, β*,
< ) β -β) |
80 | | simpr 486 |
. . . . . . 7
β’ (((π β§ π§ β β) β§ π§ < (sup(π, β*, < )
+π sup(π, β*, < ))) β π§ < (sup(π, β*, < )
+π sup(π, β*, <
))) |
81 | 73, 74, 75, 77, 79, 80 | xlt2addrd 31971 |
. . . . . 6
β’ (((π β§ π§ β β) β§ π§ < (sup(π, β*, < )
+π sup(π, β*, < ))) β
βπ β
β* βπ β β* (π§ = (π +π π) β§ π < sup(π, β*, < ) β§ π < sup(π, β*, <
))) |
82 | | nfv 1918 |
. . . . . . . 8
β’
β²π(π β β*
β§ π β
β*) |
83 | | nfcv 2904 |
. . . . . . . . 9
β’
β²πβ* |
84 | | nfre1 3283 |
. . . . . . . . 9
β’
β²πβπ β β*
(π§ = (π +π π) β§ π < sup(π, β*, < ) β§ π < sup(π, β*, <
)) |
85 | 83, 84 | nfrexw 3311 |
. . . . . . . 8
β’
β²πβπ β β*
βπ β
β* (π§ =
(π +π
π) β§ π < sup(π, β*, < ) β§ π < sup(π, β*, <
)) |
86 | 82, 85 | nfan 1903 |
. . . . . . 7
β’
β²π((π β β*
β§ π β
β*) β§ βπ β β* βπ β β*
(π§ = (π +π π) β§ π < sup(π, β*, < ) β§ π < sup(π, β*, <
))) |
87 | | nfvd 1919 |
. . . . . . 7
β’ (((π β β*
β§ π β
β*) β§ βπ β β* βπ β β*
(π§ = (π +π π) β§ π < sup(π, β*, < ) β§ π < sup(π, β*, < ))) β
β²πβπ£ β π βπ€ β π π§ < (π£ +π π€)) |
88 | | nfvd 1919 |
. . . . . . 7
β’ (((π β β*
β§ π β
β*) β§ βπ β β* βπ β β*
(π§ = (π +π π) β§ π < sup(π, β*, < ) β§ π < sup(π, β*, < ))) β
β²πβπ£ β π βπ€ β π π§ < (π£ +π π€)) |
89 | | id 22 |
. . . . . . . . . . . 12
β’ ((π β β*
β§ π β
β*) β (π β β* β§ π β
β*)) |
90 | 89 | ralrimivw 3151 |
. . . . . . . . . . 11
β’ ((π β β*
β§ π β
β*) β βπ β β* (π β β*
β§ π β
β*)) |
91 | 90 | ralrimivw 3151 |
. . . . . . . . . 10
β’ ((π β β*
β§ π β
β*) β βπ β β* βπ β β*
(π β
β* β§ π
β β*)) |
92 | 91 | adantr 482 |
. . . . . . . . 9
β’ (((π β β*
β§ π β
β*) β§ βπ β β* βπ β β*
(π§ = (π +π π) β§ π < sup(π, β*, < ) β§ π < sup(π, β*, < ))) β
βπ β
β* βπ β β* (π β β*
β§ π β
β*)) |
93 | | simpr 486 |
. . . . . . . . 9
β’ (((π β β*
β§ π β
β*) β§ βπ β β* βπ β β*
(π§ = (π +π π) β§ π < sup(π, β*, < ) β§ π < sup(π, β*, < ))) β
βπ β
β* βπ β β* (π§ = (π +π π) β§ π < sup(π, β*, < ) β§ π < sup(π, β*, <
))) |
94 | 92, 93 | r19.29d2r 3141 |
. . . . . . . 8
β’ (((π β β*
β§ π β
β*) β§ βπ β β* βπ β β*
(π§ = (π +π π) β§ π < sup(π, β*, < ) β§ π < sup(π, β*, < ))) β
βπ β
β* βπ β β* ((π β β*
β§ π β
β*) β§ (π§ = (π +π π) β§ π < sup(π, β*, < ) β§ π < sup(π, β*, <
)))) |
95 | | simplrr 777 |
. . . . . . . . . . . . . . 15
β’ ((((π β β*
β§ π β
β*) β§ ((π β β* β§ π β β*)
β§ (π§ = (π +π π) β§ π < sup(π, β*, < ) β§ π < sup(π, β*, < )))) β§
(π£ β π β§ π€ β π β§ (π < π£ β§ π < π€))) β (π§ = (π +π π) β§ π < sup(π, β*, < ) β§ π < sup(π, β*, <
))) |
96 | 95 | 3anassrs 1361 |
. . . . . . . . . . . . . 14
β’
((((((π β
β* β§ π
β β*) β§ ((π β β* β§ π β β*)
β§ (π§ = (π +π π) β§ π < sup(π, β*, < ) β§ π < sup(π, β*, < )))) β§ π£ β π) β§ π€ β π) β§ (π < π£ β§ π < π€)) β (π§ = (π +π π) β§ π < sup(π, β*, < ) β§ π < sup(π, β*, <
))) |
97 | 96 | simp1d 1143 |
. . . . . . . . . . . . 13
β’
((((((π β
β* β§ π
β β*) β§ ((π β β* β§ π β β*)
β§ (π§ = (π +π π) β§ π < sup(π, β*, < ) β§ π < sup(π, β*, < )))) β§ π£ β π) β§ π€ β π) β§ (π < π£ β§ π < π€)) β π§ = (π +π π)) |
98 | | simp-4l 782 |
. . . . . . . . . . . . . 14
β’
((((((π β
β* β§ π
β β*) β§ ((π β β* β§ π β β*)
β§ (π§ = (π +π π) β§ π < sup(π, β*, < ) β§ π < sup(π, β*, < )))) β§ π£ β π) β§ π€ β π) β§ (π < π£ β§ π < π€)) β (π β β* β§ π β
β*)) |
99 | | simplrl 776 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β β*
β§ π β
β*) β§ ((π β β* β§ π β β*)
β§ (π§ = (π +π π) β§ π < sup(π, β*, < ) β§ π < sup(π, β*, < )))) β§
(π£ β π β§ π€ β π β§ (π < π£ β§ π < π€))) β (π β β* β§ π β
β*)) |
100 | 99 | 3anassrs 1361 |
. . . . . . . . . . . . . . . 16
β’
((((((π β
β* β§ π
β β*) β§ ((π β β* β§ π β β*)
β§ (π§ = (π +π π) β§ π < sup(π, β*, < ) β§ π < sup(π, β*, < )))) β§ π£ β π) β§ π€ β π) β§ (π < π£ β§ π < π€)) β (π β β* β§ π β
β*)) |
101 | 100 | simpld 496 |
. . . . . . . . . . . . . . 15
β’
((((((π β
β* β§ π
β β*) β§ ((π β β* β§ π β β*)
β§ (π§ = (π +π π) β§ π < sup(π, β*, < ) β§ π < sup(π, β*, < )))) β§ π£ β π) β§ π€ β π) β§ (π < π£ β§ π < π€)) β π β
β*) |
102 | | simpllr 775 |
. . . . . . . . . . . . . . 15
β’
((((((π β
β* β§ π
β β*) β§ ((π β β* β§ π β β*)
β§ (π§ = (π +π π) β§ π < sup(π, β*, < ) β§ π < sup(π, β*, < )))) β§ π£ β π) β§ π€ β π) β§ (π < π£ β§ π < π€)) β π£ β π) |
103 | 101, 102 | sseldd 3984 |
. . . . . . . . . . . . . 14
β’
((((((π β
β* β§ π
β β*) β§ ((π β β* β§ π β β*)
β§ (π§ = (π +π π) β§ π < sup(π, β*, < ) β§ π < sup(π, β*, < )))) β§ π£ β π) β§ π€ β π) β§ (π < π£ β§ π < π€)) β π£ β β*) |
104 | 100 | simprd 497 |
. . . . . . . . . . . . . . 15
β’
((((((π β
β* β§ π
β β*) β§ ((π β β* β§ π β β*)
β§ (π§ = (π +π π) β§ π < sup(π, β*, < ) β§ π < sup(π, β*, < )))) β§ π£ β π) β§ π€ β π) β§ (π < π£ β§ π < π€)) β π β
β*) |
105 | | simplr 768 |
. . . . . . . . . . . . . . 15
β’
((((((π β
β* β§ π
β β*) β§ ((π β β* β§ π β β*)
β§ (π§ = (π +π π) β§ π < sup(π, β*, < ) β§ π < sup(π, β*, < )))) β§ π£ β π) β§ π€ β π) β§ (π < π£ β§ π < π€)) β π€ β π) |
106 | 104, 105 | sseldd 3984 |
. . . . . . . . . . . . . 14
β’
((((((π β
β* β§ π
β β*) β§ ((π β β* β§ π β β*)
β§ (π§ = (π +π π) β§ π < sup(π, β*, < ) β§ π < sup(π, β*, < )))) β§ π£ β π) β§ π€ β π) β§ (π < π£ β§ π < π€)) β π€ β β*) |
107 | 98, 103, 106 | jca32 517 |
. . . . . . . . . . . . 13
β’
((((((π β
β* β§ π
β β*) β§ ((π β β* β§ π β β*)
β§ (π§ = (π +π π) β§ π < sup(π, β*, < ) β§ π < sup(π, β*, < )))) β§ π£ β π) β§ π€ β π) β§ (π < π£ β§ π < π€)) β ((π β β* β§ π β β*)
β§ (π£ β
β* β§ π€
β β*))) |
108 | | simpr 486 |
. . . . . . . . . . . . 13
β’
((((((π β
β* β§ π
β β*) β§ ((π β β* β§ π β β*)
β§ (π§ = (π +π π) β§ π < sup(π, β*, < ) β§ π < sup(π, β*, < )))) β§ π£ β π) β§ π€ β π) β§ (π < π£ β§ π < π€)) β (π < π£ β§ π < π€)) |
109 | | xlt2add 13239 |
. . . . . . . . . . . . . . 15
β’ (((π β β*
β§ π β
β*) β§ (π£ β β* β§ π€ β β*))
β ((π < π£ β§ π < π€) β (π +π π) < (π£ +π π€))) |
110 | 109 | imp 408 |
. . . . . . . . . . . . . 14
β’ ((((π β β*
β§ π β
β*) β§ (π£ β β* β§ π€ β β*))
β§ (π < π£ β§ π < π€)) β (π +π π) < (π£ +π π€)) |
111 | | breq1 5152 |
. . . . . . . . . . . . . . 15
β’ (π§ = (π +π π) β (π§ < (π£ +π π€) β (π +π π) < (π£ +π π€))) |
112 | 111 | biimpar 479 |
. . . . . . . . . . . . . 14
β’ ((π§ = (π +π π) β§ (π +π π) < (π£ +π π€)) β π§ < (π£ +π π€)) |
113 | 110, 112 | sylan2 594 |
. . . . . . . . . . . . 13
β’ ((π§ = (π +π π) β§ (((π β β* β§ π β β*)
β§ (π£ β
β* β§ π€
β β*)) β§ (π < π£ β§ π < π€))) β π§ < (π£ +π π€)) |
114 | 97, 107, 108, 113 | syl12anc 836 |
. . . . . . . . . . . 12
β’
((((((π β
β* β§ π
β β*) β§ ((π β β* β§ π β β*)
β§ (π§ = (π +π π) β§ π < sup(π, β*, < ) β§ π < sup(π, β*, < )))) β§ π£ β π) β§ π€ β π) β§ (π < π£ β§ π < π€)) β π§ < (π£ +π π€)) |
115 | | simplll 774 |
. . . . . . . . . . . . . . 15
β’ ((((π β β*
β§ π β
β*) β§ (π§ = (π +π π) β§ π < sup(π, β*, < ) β§ π < sup(π, β*, < ))) β§ (π β β*
β§ π β
β*)) β π β
β*) |
116 | | simprl 770 |
. . . . . . . . . . . . . . 15
β’ ((((π β β*
β§ π β
β*) β§ (π§ = (π +π π) β§ π < sup(π, β*, < ) β§ π < sup(π, β*, < ))) β§ (π β β*
β§ π β
β*)) β π β β*) |
117 | | simplr2 1217 |
. . . . . . . . . . . . . . 15
β’ ((((π β β*
β§ π β
β*) β§ (π§ = (π +π π) β§ π < sup(π, β*, < ) β§ π < sup(π, β*, < ))) β§ (π β β*
β§ π β
β*)) β π < sup(π, β*, <
)) |
118 | | supxrlub 13304 |
. . . . . . . . . . . . . . . 16
β’ ((π β β*
β§ π β
β*) β (π < sup(π, β*, < ) β
βπ£ β π π < π£)) |
119 | 118 | biimpa 478 |
. . . . . . . . . . . . . . 15
β’ (((π β β*
β§ π β
β*) β§ π < sup(π, β*, < )) β
βπ£ β π π < π£) |
120 | 115, 116,
117, 119 | syl21anc 837 |
. . . . . . . . . . . . . 14
β’ ((((π β β*
β§ π β
β*) β§ (π§ = (π +π π) β§ π < sup(π, β*, < ) β§ π < sup(π, β*, < ))) β§ (π β β*
β§ π β
β*)) β βπ£ β π π < π£) |
121 | | simpllr 775 |
. . . . . . . . . . . . . . 15
β’ ((((π β β*
β§ π β
β*) β§ (π§ = (π +π π) β§ π < sup(π, β*, < ) β§ π < sup(π, β*, < ))) β§ (π β β*
β§ π β
β*)) β π β
β*) |
122 | | simprr 772 |
. . . . . . . . . . . . . . 15
β’ ((((π β β*
β§ π β
β*) β§ (π§ = (π +π π) β§ π < sup(π, β*, < ) β§ π < sup(π, β*, < ))) β§ (π β β*
β§ π β
β*)) β π β β*) |
123 | | simplr3 1218 |
. . . . . . . . . . . . . . 15
β’ ((((π β β*
β§ π β
β*) β§ (π§ = (π +π π) β§ π < sup(π, β*, < ) β§ π < sup(π, β*, < ))) β§ (π β β*
β§ π β
β*)) β π < sup(π, β*, <
)) |
124 | | supxrlub 13304 |
. . . . . . . . . . . . . . . 16
β’ ((π β β*
β§ π β
β*) β (π < sup(π, β*, < ) β
βπ€ β π π < π€)) |
125 | 124 | biimpa 478 |
. . . . . . . . . . . . . . 15
β’ (((π β β*
β§ π β
β*) β§ π < sup(π, β*, < )) β
βπ€ β π π < π€) |
126 | 121, 122,
123, 125 | syl21anc 837 |
. . . . . . . . . . . . . 14
β’ ((((π β β*
β§ π β
β*) β§ (π§ = (π +π π) β§ π < sup(π, β*, < ) β§ π < sup(π, β*, < ))) β§ (π β β*
β§ π β
β*)) β βπ€ β π π < π€) |
127 | | reeanv 3227 |
. . . . . . . . . . . . . 14
β’
(βπ£ β
π βπ€ β π (π < π£ β§ π < π€) β (βπ£ β π π < π£ β§ βπ€ β π π < π€)) |
128 | 120, 126,
127 | sylanbrc 584 |
. . . . . . . . . . . . 13
β’ ((((π β β*
β§ π β
β*) β§ (π§ = (π +π π) β§ π < sup(π, β*, < ) β§ π < sup(π, β*, < ))) β§ (π β β*
β§ π β
β*)) β βπ£ β π βπ€ β π (π < π£ β§ π < π€)) |
129 | 128 | ancoms 460 |
. . . . . . . . . . . 12
β’ (((π β β*
β§ π β
β*) β§ ((π β β* β§ π β β*)
β§ (π§ = (π +π π) β§ π < sup(π, β*, < ) β§ π < sup(π, β*, < )))) β
βπ£ β π βπ€ β π (π < π£ β§ π < π€)) |
130 | 114, 129 | reximddv2 3213 |
. . . . . . . . . . 11
β’ (((π β β*
β§ π β
β*) β§ ((π β β* β§ π β β*)
β§ (π§ = (π +π π) β§ π < sup(π, β*, < ) β§ π < sup(π, β*, < )))) β
βπ£ β π βπ€ β π π§ < (π£ +π π€)) |
131 | 130 | ex 414 |
. . . . . . . . . 10
β’ ((π β β*
β§ π β
β*) β (((π β β* β§ π β β*)
β§ (π§ = (π +π π) β§ π < sup(π, β*, < ) β§ π < sup(π, β*, < ))) β
βπ£ β π βπ€ β π π§ < (π£ +π π€))) |
132 | 131 | reximdva 3169 |
. . . . . . . . 9
β’ (π β β*
β (βπ β
β* ((π
β β* β§ π β β*) β§ (π§ = (π +π π) β§ π < sup(π, β*, < ) β§ π < sup(π, β*, < ))) β
βπ β
β* βπ£ β π βπ€ β π π§ < (π£ +π π€))) |
133 | 132 | reximia 3082 |
. . . . . . . 8
β’
(βπ β
β* βπ β β* ((π β β*
β§ π β
β*) β§ (π§ = (π +π π) β§ π < sup(π, β*, < ) β§ π < sup(π, β*, < ))) β
βπ β
β* βπ β β* βπ£ β π βπ€ β π π§ < (π£ +π π€)) |
134 | 94, 133 | syl 17 |
. . . . . . 7
β’ (((π β β*
β§ π β
β*) β§ βπ β β* βπ β β*
(π§ = (π +π π) β§ π < sup(π, β*, < ) β§ π < sup(π, β*, < ))) β
βπ β
β* βπ β β* βπ£ β π βπ€ β π π§ < (π£ +π π€)) |
135 | 86, 87, 88, 134 | 19.9d2rf 31711 |
. . . . . 6
β’ (((π β β*
β§ π β
β*) β§ βπ β β* βπ β β*
(π§ = (π +π π) β§ π < sup(π, β*, < ) β§ π < sup(π, β*, < ))) β
βπ£ β π βπ€ β π π§ < (π£ +π π€)) |
136 | 71, 72, 81, 135 | syl21anc 837 |
. . . . 5
β’ (((π β§ π§ β β) β§ π§ < (sup(π, β*, < )
+π sup(π, β*, < ))) β
βπ£ β π βπ€ β π π§ < (π£ +π π€)) |
137 | | simprl 770 |
. . . . . . . . . 10
β’ ((π β§ (π£ β π β§ π€ β π)) β π£ β π) |
138 | | simprr 772 |
. . . . . . . . . 10
β’ ((π β§ (π£ β π β§ π€ β π)) β π€ β π) |
139 | 19 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ (π£ β π β§ π€ β π)) β Fun +π
) |
140 | 23 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ (π£ β π β§ π€ β π)) β (π Γ π) β dom +π
) |
141 | 137, 138,
139, 140 | elovimad 7457 |
. . . . . . . . 9
β’ ((π β§ (π£ β π β§ π€ β π)) β (π£ +π π€) β ( +π β
(π Γ π))) |
142 | 1 | eleq2d 2820 |
. . . . . . . . . 10
β’ (π β ((π£ +π π€) β π β (π£ +π π€) β ( +π β
(π Γ π)))) |
143 | 142 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ (π£ β π β§ π€ β π)) β ((π£ +π π€) β π β (π£ +π π€) β ( +π β
(π Γ π)))) |
144 | 141, 143 | mpbird 257 |
. . . . . . . 8
β’ ((π β§ (π£ β π β§ π€ β π)) β (π£ +π π€) β π) |
145 | | simpr 486 |
. . . . . . . . 9
β’ (((π β§ (π£ β π β§ π€ β π)) β§ π = (π£ +π π€)) β π = (π£ +π π€)) |
146 | 145 | breq2d 5161 |
. . . . . . . 8
β’ (((π β§ (π£ β π β§ π€ β π)) β§ π = (π£ +π π€)) β (π§ < π β π§ < (π£ +π π€))) |
147 | 144, 146 | rspcedv 3606 |
. . . . . . 7
β’ ((π β§ (π£ β π β§ π€ β π)) β (π§ < (π£ +π π€) β βπ β π π§ < π)) |
148 | 147 | rexlimdvva 3212 |
. . . . . 6
β’ (π β (βπ£ β π βπ€ β π π§ < (π£ +π π€) β βπ β π π§ < π)) |
149 | 148 | ad2antrr 725 |
. . . . 5
β’ (((π β§ π§ β β) β§ π§ < (sup(π, β*, < )
+π sup(π, β*, < ))) β
(βπ£ β π βπ€ β π π§ < (π£ +π π€) β βπ β π π§ < π)) |
150 | 136, 149 | mpd 15 |
. . . 4
β’ (((π β§ π§ β β) β§ π§ < (sup(π, β*, < )
+π sup(π, β*, < ))) β
βπ β π π§ < π) |
151 | 150 | ex 414 |
. . 3
β’ ((π β§ π§ β β) β (π§ < (sup(π, β*, < )
+π sup(π, β*, < )) β
βπ β π π§ < π)) |
152 | 151 | ralrimiva 3147 |
. 2
β’ (π β βπ§ β β (π§ < (sup(π, β*, < )
+π sup(π, β*, < )) β
βπ β π π§ < π)) |
153 | | supxr2 13293 |
. 2
β’ (((π β β*
β§ (sup(π,
β*, < ) +π sup(π, β*, < )) β
β*) β§ (βπ§ β π π§ β€ (sup(π, β*, < )
+π sup(π, β*, < )) β§
βπ§ β β
(π§ < (sup(π, β*, < )
+π sup(π, β*, < )) β
βπ β π π§ < π))) β sup(π, β*, < ) = (sup(π, β*, < )
+π sup(π, β*, <
))) |
154 | 27, 32, 70, 152, 153 | syl22anc 838 |
1
β’ (π β sup(π, β*, < ) = (sup(π, β*, < )
+π sup(π, β*, <
))) |