Step | Hyp | Ref
| Expression |
1 | | sge0seq.z |
. . . . . . 7
β’ π =
(β€β₯βπ) |
2 | | sge0seq.m |
. . . . . . 7
β’ (π β π β β€) |
3 | | rge0ssre 13433 |
. . . . . . . 8
β’
(0[,)+β) β β |
4 | | sge0seq.f |
. . . . . . . . 9
β’ (π β πΉ:πβΆ(0[,)+β)) |
5 | 4 | ffvelcdmda 7087 |
. . . . . . . 8
β’ ((π β§ π β π) β (πΉβπ) β (0[,)+β)) |
6 | 3, 5 | sselid 3981 |
. . . . . . 7
β’ ((π β§ π β π) β (πΉβπ) β β) |
7 | | readdcl 11193 |
. . . . . . . 8
β’ ((π β β β§ π β β) β (π + π) β β) |
8 | 7 | adantl 483 |
. . . . . . 7
β’ ((π β§ (π β β β§ π β β)) β (π + π) β β) |
9 | 1, 2, 6, 8 | seqf 13989 |
. . . . . 6
β’ (π β seqπ( + , πΉ):πβΆβ) |
10 | | sge0seq.g |
. . . . . . . 8
β’ πΊ = seqπ( + , πΉ) |
11 | 10 | a1i 11 |
. . . . . . 7
β’ (π β πΊ = seqπ( + , πΉ)) |
12 | 11 | feq1d 6703 |
. . . . . 6
β’ (π β (πΊ:πβΆβ β seqπ( + , πΉ):πβΆβ)) |
13 | 9, 12 | mpbird 257 |
. . . . 5
β’ (π β πΊ:πβΆβ) |
14 | 13 | frnd 6726 |
. . . 4
β’ (π β ran πΊ β β) |
15 | | ressxr 11258 |
. . . . 5
β’ β
β β* |
16 | 15 | a1i 11 |
. . . 4
β’ (π β β β
β*) |
17 | 14, 16 | sstrd 3993 |
. . 3
β’ (π β ran πΊ β
β*) |
18 | 1 | fvexi 6906 |
. . . . 5
β’ π β V |
19 | 18 | a1i 11 |
. . . 4
β’ (π β π β V) |
20 | | icossicc 13413 |
. . . . . 6
β’
(0[,)+β) β (0[,]+β) |
21 | 20 | a1i 11 |
. . . . 5
β’ (π β (0[,)+β) β
(0[,]+β)) |
22 | 4, 21 | fssd 6736 |
. . . 4
β’ (π β πΉ:πβΆ(0[,]+β)) |
23 | 19, 22 | sge0xrcl 45101 |
. . 3
β’ (π β
(Ξ£^βπΉ) β
β*) |
24 | | simpr 486 |
. . . . . 6
β’ ((π β§ π§ β ran πΊ) β π§ β ran πΊ) |
25 | 13 | ffnd 6719 |
. . . . . . . 8
β’ (π β πΊ Fn π) |
26 | | fvelrnb 6953 |
. . . . . . . 8
β’ (πΊ Fn π β (π§ β ran πΊ β βπ β π (πΊβπ) = π§)) |
27 | 25, 26 | syl 17 |
. . . . . . 7
β’ (π β (π§ β ran πΊ β βπ β π (πΊβπ) = π§)) |
28 | 27 | adantr 482 |
. . . . . 6
β’ ((π β§ π§ β ran πΊ) β (π§ β ran πΊ β βπ β π (πΊβπ) = π§)) |
29 | 24, 28 | mpbid 231 |
. . . . 5
β’ ((π β§ π§ β ran πΊ) β βπ β π (πΊβπ) = π§) |
30 | 20, 5 | sselid 3981 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β (πΉβπ) β (0[,]+β)) |
31 | | elfzuz 13497 |
. . . . . . . . . . . . . 14
β’ (π β (π...π) β π β (β€β₯βπ)) |
32 | 31, 1 | eleqtrrdi 2845 |
. . . . . . . . . . . . 13
β’ (π β (π...π) β π β π) |
33 | 32 | ssriv 3987 |
. . . . . . . . . . . 12
β’ (π...π) β π |
34 | 33 | a1i 11 |
. . . . . . . . . . 11
β’ (π β (π...π) β π) |
35 | 19, 30, 34 | sge0lessmpt 45115 |
. . . . . . . . . 10
β’ (π β
(Ξ£^β(π β (π...π) β¦ (πΉβπ))) β€
(Ξ£^β(π β π β¦ (πΉβπ)))) |
36 | 35 | 3ad2ant1 1134 |
. . . . . . . . 9
β’ ((π β§ π β π β§ (πΊβπ) = π§) β
(Ξ£^β(π β (π...π) β¦ (πΉβπ))) β€
(Ξ£^β(π β π β¦ (πΉβπ)))) |
37 | | fzfid 13938 |
. . . . . . . . . . . . . 14
β’ (π β (π...π) β Fin) |
38 | 32, 5 | sylan2 594 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (π...π)) β (πΉβπ) β (0[,)+β)) |
39 | 37, 38 | sge0fsummpt 45106 |
. . . . . . . . . . . . 13
β’ (π β
(Ξ£^β(π β (π...π) β¦ (πΉβπ))) = Ξ£π β (π...π)(πΉβπ)) |
40 | 39 | 3ad2ant1 1134 |
. . . . . . . . . . . 12
β’ ((π β§ π β π β§ (πΊβπ) = π§) β
(Ξ£^β(π β (π...π) β¦ (πΉβπ))) = Ξ£π β (π...π)(πΉβπ)) |
41 | | simpll 766 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β π) β§ π β (π...π)) β π) |
42 | 32 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β π) β§ π β (π...π)) β π β π) |
43 | | eqidd 2734 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π) β (πΉβπ) = (πΉβπ)) |
44 | 41, 42, 43 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π) β§ π β (π...π)) β (πΉβπ) = (πΉβπ)) |
45 | 1 | eleq2i 2826 |
. . . . . . . . . . . . . . . 16
β’ (π β π β π β (β€β₯βπ)) |
46 | 45 | biimpi 215 |
. . . . . . . . . . . . . . 15
β’ (π β π β π β (β€β₯βπ)) |
47 | 46 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π) β π β (β€β₯βπ)) |
48 | 6 | recnd 11242 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π) β (πΉβπ) β β) |
49 | 41, 42, 48 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π) β§ π β (π...π)) β (πΉβπ) β β) |
50 | 44, 47, 49 | fsumser 15676 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π) β Ξ£π β (π...π)(πΉβπ) = (seqπ( + , πΉ)βπ)) |
51 | 50 | 3adant3 1133 |
. . . . . . . . . . . 12
β’ ((π β§ π β π β§ (πΊβπ) = π§) β Ξ£π β (π...π)(πΉβπ) = (seqπ( + , πΉ)βπ)) |
52 | 40, 51 | eqtrd 2773 |
. . . . . . . . . . 11
β’ ((π β§ π β π β§ (πΊβπ) = π§) β
(Ξ£^β(π β (π...π) β¦ (πΉβπ))) = (seqπ( + , πΉ)βπ)) |
53 | 10 | eqcomi 2742 |
. . . . . . . . . . . . 13
β’ seqπ( + , πΉ) = πΊ |
54 | 53 | fveq1i 6893 |
. . . . . . . . . . . 12
β’ (seqπ( + , πΉ)βπ) = (πΊβπ) |
55 | 54 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β§ π β π β§ (πΊβπ) = π§) β (seqπ( + , πΉ)βπ) = (πΊβπ)) |
56 | | simp3 1139 |
. . . . . . . . . . 11
β’ ((π β§ π β π β§ (πΊβπ) = π§) β (πΊβπ) = π§) |
57 | 52, 55, 56 | 3eqtrrd 2778 |
. . . . . . . . . 10
β’ ((π β§ π β π β§ (πΊβπ) = π§) β π§ =
(Ξ£^β(π β (π...π) β¦ (πΉβπ)))) |
58 | 4 | feqmptd 6961 |
. . . . . . . . . . . 12
β’ (π β πΉ = (π β π β¦ (πΉβπ))) |
59 | 58 | fveq2d 6896 |
. . . . . . . . . . 11
β’ (π β
(Ξ£^βπΉ) =
(Ξ£^β(π β π β¦ (πΉβπ)))) |
60 | 59 | 3ad2ant1 1134 |
. . . . . . . . . 10
β’ ((π β§ π β π β§ (πΊβπ) = π§) β
(Ξ£^βπΉ) =
(Ξ£^β(π β π β¦ (πΉβπ)))) |
61 | 57, 60 | breq12d 5162 |
. . . . . . . . 9
β’ ((π β§ π β π β§ (πΊβπ) = π§) β (π§ β€
(Ξ£^βπΉ) β
(Ξ£^β(π β (π...π) β¦ (πΉβπ))) β€
(Ξ£^β(π β π β¦ (πΉβπ))))) |
62 | 36, 61 | mpbird 257 |
. . . . . . . 8
β’ ((π β§ π β π β§ (πΊβπ) = π§) β π§ β€
(Ξ£^βπΉ)) |
63 | 62 | 3exp 1120 |
. . . . . . 7
β’ (π β (π β π β ((πΊβπ) = π§ β π§ β€
(Ξ£^βπΉ)))) |
64 | 63 | adantr 482 |
. . . . . 6
β’ ((π β§ π§ β ran πΊ) β (π β π β ((πΊβπ) = π§ β π§ β€
(Ξ£^βπΉ)))) |
65 | 64 | rexlimdv 3154 |
. . . . 5
β’ ((π β§ π§ β ran πΊ) β (βπ β π (πΊβπ) = π§ β π§ β€
(Ξ£^βπΉ))) |
66 | 29, 65 | mpd 15 |
. . . 4
β’ ((π β§ π§ β ran πΊ) β π§ β€
(Ξ£^βπΉ)) |
67 | 66 | ralrimiva 3147 |
. . 3
β’ (π β βπ§ β ran πΊ π§ β€
(Ξ£^βπΉ)) |
68 | | nfv 1918 |
. . . . . . . 8
β’
β²π((π β§ π§ β β) β§ π§ <
(Ξ£^βπΉ)) |
69 | 18 | a1i 11 |
. . . . . . . 8
β’ (((π β§ π§ β β) β§ π§ <
(Ξ£^βπΉ)) β π β V) |
70 | 5 | ad4ant14 751 |
. . . . . . . 8
β’ ((((π β§ π§ β β) β§ π§ <
(Ξ£^βπΉ)) β§ π β π) β (πΉβπ) β (0[,)+β)) |
71 | | simplr 768 |
. . . . . . . 8
β’ (((π β§ π§ β β) β§ π§ <
(Ξ£^βπΉ)) β π§ β β) |
72 | | simpr 486 |
. . . . . . . . . 10
β’ ((π β§ π§ <
(Ξ£^βπΉ)) β π§ <
(Ξ£^βπΉ)) |
73 | 59 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π§ <
(Ξ£^βπΉ)) β
(Ξ£^βπΉ) =
(Ξ£^β(π β π β¦ (πΉβπ)))) |
74 | 72, 73 | breqtrd 5175 |
. . . . . . . . 9
β’ ((π β§ π§ <
(Ξ£^βπΉ)) β π§ <
(Ξ£^β(π β π β¦ (πΉβπ)))) |
75 | 74 | adantlr 714 |
. . . . . . . 8
β’ (((π β§ π§ β β) β§ π§ <
(Ξ£^βπΉ)) β π§ <
(Ξ£^β(π β π β¦ (πΉβπ)))) |
76 | 68, 69, 70, 71, 75 | sge0gtfsumgt 45159 |
. . . . . . 7
β’ (((π β§ π§ β β) β§ π§ <
(Ξ£^βπΉ)) β βπ€ β (π« π β© Fin)π§ < Ξ£π β π€ (πΉβπ)) |
77 | 2 | 3ad2ant1 1134 |
. . . . . . . . . . . . 13
β’ ((π β§ π€ β (π« π β© Fin) β§ π§ < Ξ£π β π€ (πΉβπ)) β π β β€) |
78 | | elpwinss 43736 |
. . . . . . . . . . . . . 14
β’ (π€ β (π« π β© Fin) β π€ β π) |
79 | 78 | 3ad2ant2 1135 |
. . . . . . . . . . . . 13
β’ ((π β§ π€ β (π« π β© Fin) β§ π§ < Ξ£π β π€ (πΉβπ)) β π€ β π) |
80 | | elinel2 4197 |
. . . . . . . . . . . . . 14
β’ (π€ β (π« π β© Fin) β π€ β Fin) |
81 | 80 | 3ad2ant2 1135 |
. . . . . . . . . . . . 13
β’ ((π β§ π€ β (π« π β© Fin) β§ π§ < Ξ£π β π€ (πΉβπ)) β π€ β Fin) |
82 | 77, 1, 79, 81 | uzfissfz 44036 |
. . . . . . . . . . . 12
β’ ((π β§ π€ β (π« π β© Fin) β§ π§ < Ξ£π β π€ (πΉβπ)) β βπ β π π€ β (π...π)) |
83 | 82 | 3adant1r 1178 |
. . . . . . . . . . 11
β’ (((π β§ π§ β β) β§ π€ β (π« π β© Fin) β§ π§ < Ξ£π β π€ (πΉβπ)) β βπ β π π€ β (π...π)) |
84 | | simpl1r 1226 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π§ β β) β§ π€ β (π« π β© Fin) β§ π§ < Ξ£π β π€ (πΉβπ)) β§ π€ β (π...π)) β π§ β β) |
85 | 80 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π€ β (π« π β© Fin)) β π€ β Fin) |
86 | 58, 6 | fmpt3d 7116 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β πΉ:πβΆβ) |
87 | 86 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π€ β (π« π β© Fin)) β§ π β π€) β πΉ:πβΆβ) |
88 | 78 | sselda 3983 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π€ β (π« π β© Fin) β§ π β π€) β π β π) |
89 | 88 | adantll 713 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π€ β (π« π β© Fin)) β§ π β π€) β π β π) |
90 | 87, 89 | ffvelcdmd 7088 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π€ β (π« π β© Fin)) β§ π β π€) β (πΉβπ) β β) |
91 | 85, 90 | fsumrecl 15680 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π€ β (π« π β© Fin)) β Ξ£π β π€ (πΉβπ) β β) |
92 | 91 | ad4ant13 750 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π§ β β) β§ π€ β (π« π β© Fin)) β§ π€ β (π...π)) β Ξ£π β π€ (πΉβπ) β β) |
93 | 92 | 3adantl3 1169 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π§ β β) β§ π€ β (π« π β© Fin) β§ π§ < Ξ£π β π€ (πΉβπ)) β§ π€ β (π...π)) β Ξ£π β π€ (πΉβπ) β β) |
94 | 32, 6 | sylan2 594 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (π...π)) β (πΉβπ) β β) |
95 | 37, 94 | fsumrecl 15680 |
. . . . . . . . . . . . . . . 16
β’ (π β Ξ£π β (π...π)(πΉβπ) β β) |
96 | 95 | ad3antrrr 729 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π§ β β) β§ π€ β (π« π β© Fin)) β§ π€ β (π...π)) β Ξ£π β (π...π)(πΉβπ) β β) |
97 | 96 | 3adantl3 1169 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π§ β β) β§ π€ β (π« π β© Fin) β§ π§ < Ξ£π β π€ (πΉβπ)) β§ π€ β (π...π)) β Ξ£π β (π...π)(πΉβπ) β β) |
98 | | simpl3 1194 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π§ β β) β§ π€ β (π« π β© Fin) β§ π§ < Ξ£π β π€ (πΉβπ)) β§ π€ β (π...π)) β π§ < Ξ£π β π€ (πΉβπ)) |
99 | 37 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π€ β (π...π)) β (π...π) β Fin) |
100 | 94 | adantlr 714 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π€ β (π...π)) β§ π β (π...π)) β (πΉβπ) β β) |
101 | | 0xr 11261 |
. . . . . . . . . . . . . . . . . . . . 21
β’ 0 β
β* |
102 | 101 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β π) β 0 β
β*) |
103 | | pnfxr 11268 |
. . . . . . . . . . . . . . . . . . . . 21
β’ +β
β β* |
104 | 103 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β π) β +β β
β*) |
105 | | icogelb 13375 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((0
β β* β§ +β β β* β§
(πΉβπ) β (0[,)+β)) β 0 β€ (πΉβπ)) |
106 | 102, 104,
5, 105 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β π) β 0 β€ (πΉβπ)) |
107 | 32, 106 | sylan2 594 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (π...π)) β 0 β€ (πΉβπ)) |
108 | 107 | adantlr 714 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π€ β (π...π)) β§ π β (π...π)) β 0 β€ (πΉβπ)) |
109 | | simpr 486 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π€ β (π...π)) β π€ β (π...π)) |
110 | 99, 100, 108, 109 | fsumless 15742 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π€ β (π...π)) β Ξ£π β π€ (πΉβπ) β€ Ξ£π β (π...π)(πΉβπ)) |
111 | 110 | adantlr 714 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π§ β β) β§ π€ β (π...π)) β Ξ£π β π€ (πΉβπ) β€ Ξ£π β (π...π)(πΉβπ)) |
112 | 111 | 3ad2antl1 1186 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π§ β β) β§ π€ β (π« π β© Fin) β§ π§ < Ξ£π β π€ (πΉβπ)) β§ π€ β (π...π)) β Ξ£π β π€ (πΉβπ) β€ Ξ£π β (π...π)(πΉβπ)) |
113 | 84, 93, 97, 98, 112 | ltletrd 11374 |
. . . . . . . . . . . . 13
β’ ((((π β§ π§ β β) β§ π€ β (π« π β© Fin) β§ π§ < Ξ£π β π€ (πΉβπ)) β§ π€ β (π...π)) β π§ < Ξ£π β (π...π)(πΉβπ)) |
114 | 113 | ex 414 |
. . . . . . . . . . . 12
β’ (((π β§ π§ β β) β§ π€ β (π« π β© Fin) β§ π§ < Ξ£π β π€ (πΉβπ)) β (π€ β (π...π) β π§ < Ξ£π β (π...π)(πΉβπ))) |
115 | 114 | reximdv 3171 |
. . . . . . . . . . 11
β’ (((π β§ π§ β β) β§ π€ β (π« π β© Fin) β§ π§ < Ξ£π β π€ (πΉβπ)) β (βπ β π π€ β (π...π) β βπ β π π§ < Ξ£π β (π...π)(πΉβπ))) |
116 | 83, 115 | mpd 15 |
. . . . . . . . . 10
β’ (((π β§ π§ β β) β§ π€ β (π« π β© Fin) β§ π§ < Ξ£π β π€ (πΉβπ)) β βπ β π π§ < Ξ£π β (π...π)(πΉβπ)) |
117 | 116 | 3exp 1120 |
. . . . . . . . 9
β’ ((π β§ π§ β β) β (π€ β (π« π β© Fin) β (π§ < Ξ£π β π€ (πΉβπ) β βπ β π π§ < Ξ£π β (π...π)(πΉβπ)))) |
118 | 117 | adantr 482 |
. . . . . . . 8
β’ (((π β§ π§ β β) β§ π§ <
(Ξ£^βπΉ)) β (π€ β (π« π β© Fin) β (π§ < Ξ£π β π€ (πΉβπ) β βπ β π π§ < Ξ£π β (π...π)(πΉβπ)))) |
119 | 118 | rexlimdv 3154 |
. . . . . . 7
β’ (((π β§ π§ β β) β§ π§ <
(Ξ£^βπΉ)) β (βπ€ β (π« π β© Fin)π§ < Ξ£π β π€ (πΉβπ) β βπ β π π§ < Ξ£π β (π...π)(πΉβπ))) |
120 | 76, 119 | mpd 15 |
. . . . . 6
β’ (((π β§ π§ β β) β§ π§ <
(Ξ£^βπΉ)) β βπ β π π§ < Ξ£π β (π...π)(πΉβπ)) |
121 | 9 | ffnd 6719 |
. . . . . . . . . . . . . . 15
β’ (π β seqπ( + , πΉ) Fn π) |
122 | 121 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π) β seqπ( + , πΉ) Fn π) |
123 | 47, 45 | sylibr 233 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π) β π β π) |
124 | | fnfvelrn 7083 |
. . . . . . . . . . . . . 14
β’
((seqπ( + , πΉ) Fn π β§ π β π) β (seqπ( + , πΉ)βπ) β ran seqπ( + , πΉ)) |
125 | 122, 123,
124 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π) β (seqπ( + , πΉ)βπ) β ran seqπ( + , πΉ)) |
126 | 10 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π) β πΊ = seqπ( + , πΉ)) |
127 | 126 | rneqd 5938 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π) β ran πΊ = ran seqπ( + , πΉ)) |
128 | 50, 127 | eleq12d 2828 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π) β (Ξ£π β (π...π)(πΉβπ) β ran πΊ β (seqπ( + , πΉ)βπ) β ran seqπ( + , πΉ))) |
129 | 125, 128 | mpbird 257 |
. . . . . . . . . . . 12
β’ ((π β§ π β π) β Ξ£π β (π...π)(πΉβπ) β ran πΊ) |
130 | 129 | adantlr 714 |
. . . . . . . . . . 11
β’ (((π β§ π§ β β) β§ π β π) β Ξ£π β (π...π)(πΉβπ) β ran πΊ) |
131 | 130 | 3adant3 1133 |
. . . . . . . . . 10
β’ (((π β§ π§ β β) β§ π β π β§ π§ < Ξ£π β (π...π)(πΉβπ)) β Ξ£π β (π...π)(πΉβπ) β ran πΊ) |
132 | | simp3 1139 |
. . . . . . . . . 10
β’ (((π β§ π§ β β) β§ π β π β§ π§ < Ξ£π β (π...π)(πΉβπ)) β π§ < Ξ£π β (π...π)(πΉβπ)) |
133 | | breq2 5153 |
. . . . . . . . . . 11
β’ (π¦ = Ξ£π β (π...π)(πΉβπ) β (π§ < π¦ β π§ < Ξ£π β (π...π)(πΉβπ))) |
134 | 133 | rspcev 3613 |
. . . . . . . . . 10
β’
((Ξ£π β
(π...π)(πΉβπ) β ran πΊ β§ π§ < Ξ£π β (π...π)(πΉβπ)) β βπ¦ β ran πΊ π§ < π¦) |
135 | 131, 132,
134 | syl2anc 585 |
. . . . . . . . 9
β’ (((π β§ π§ β β) β§ π β π β§ π§ < Ξ£π β (π...π)(πΉβπ)) β βπ¦ β ran πΊ π§ < π¦) |
136 | 135 | 3exp 1120 |
. . . . . . . 8
β’ ((π β§ π§ β β) β (π β π β (π§ < Ξ£π β (π...π)(πΉβπ) β βπ¦ β ran πΊ π§ < π¦))) |
137 | 136 | rexlimdv 3154 |
. . . . . . 7
β’ ((π β§ π§ β β) β (βπ β π π§ < Ξ£π β (π...π)(πΉβπ) β βπ¦ β ran πΊ π§ < π¦)) |
138 | 137 | adantr 482 |
. . . . . 6
β’ (((π β§ π§ β β) β§ π§ <
(Ξ£^βπΉ)) β (βπ β π π§ < Ξ£π β (π...π)(πΉβπ) β βπ¦ β ran πΊ π§ < π¦)) |
139 | 120, 138 | mpd 15 |
. . . . 5
β’ (((π β§ π§ β β) β§ π§ <
(Ξ£^βπΉ)) β βπ¦ β ran πΊ π§ < π¦) |
140 | 139 | ex 414 |
. . . 4
β’ ((π β§ π§ β β) β (π§ <
(Ξ£^βπΉ) β βπ¦ β ran πΊ π§ < π¦)) |
141 | 140 | ralrimiva 3147 |
. . 3
β’ (π β βπ§ β β (π§ <
(Ξ£^βπΉ) β βπ¦ β ran πΊ π§ < π¦)) |
142 | | supxr2 13293 |
. . 3
β’ (((ran
πΊ β
β* β§ (Ξ£^βπΉ) β β*)
β§ (βπ§ β ran
πΊ π§ β€
(Ξ£^βπΉ) β§ βπ§ β β (π§ <
(Ξ£^βπΉ) β βπ¦ β ran πΊ π§ < π¦))) β sup(ran πΊ, β*, < ) =
(Ξ£^βπΉ)) |
143 | 17, 23, 67, 141, 142 | syl22anc 838 |
. 2
β’ (π β sup(ran πΊ, β*, < ) =
(Ξ£^βπΉ)) |
144 | 143 | eqcomd 2739 |
1
β’ (π β
(Ξ£^βπΉ) = sup(ran πΊ, β*, <
)) |