Step | Hyp | Ref
| Expression |
1 | | esumcst.1 |
. . . . 5
β’
β²ππ΄ |
2 | 1 | nfel1 2924 |
. . . 4
β’
β²π π΄ β π |
3 | | esumcst.2 |
. . . . 5
β’
β²ππ΅ |
4 | 3 | nfel1 2924 |
. . . 4
β’
β²π π΅ β
(0[,]+β) |
5 | 2, 4 | nfan 1903 |
. . 3
β’
β²π(π΄ β π β§ π΅ β (0[,]+β)) |
6 | | simpl 484 |
. . 3
β’ ((π΄ β π β§ π΅ β (0[,]+β)) β π΄ β π) |
7 | | simplr 768 |
. . 3
β’ (((π΄ β π β§ π΅ β (0[,]+β)) β§ π β π΄) β π΅ β (0[,]+β)) |
8 | | xrge0tmd 32566 |
. . . . . . 7
β’
(β*π βΎs
(0[,]+β)) β TopMnd |
9 | | tmdmnd 23442 |
. . . . . . 7
β’
((β*π βΎs
(0[,]+β)) β TopMnd β (β*π
βΎs (0[,]+β)) β Mnd) |
10 | 8, 9 | ax-mp 5 |
. . . . . 6
β’
(β*π βΎs
(0[,]+β)) β Mnd |
11 | 10 | a1i 11 |
. . . . 5
β’ (((π΄ β π β§ π΅ β (0[,]+β)) β§ π₯ β (π« π΄ β© Fin)) β
(β*π βΎs (0[,]+β))
β Mnd) |
12 | | inss2 4194 |
. . . . . 6
β’
(π« π΄ β©
Fin) β Fin |
13 | | simpr 486 |
. . . . . 6
β’ (((π΄ β π β§ π΅ β (0[,]+β)) β§ π₯ β (π« π΄ β© Fin)) β π₯ β (π« π΄ β© Fin)) |
14 | 12, 13 | sselid 3947 |
. . . . 5
β’ (((π΄ β π β§ π΅ β (0[,]+β)) β§ π₯ β (π« π΄ β© Fin)) β π₯ β Fin) |
15 | | simplr 768 |
. . . . 5
β’ (((π΄ β π β§ π΅ β (0[,]+β)) β§ π₯ β (π« π΄ β© Fin)) β π΅ β
(0[,]+β)) |
16 | | xrge0base 31918 |
. . . . . 6
β’
(0[,]+β) = (Baseβ(β*π
βΎs (0[,]+β))) |
17 | | eqid 2737 |
. . . . . 6
β’
(.gβ(β*π
βΎs (0[,]+β))) =
(.gβ(β*π
βΎs (0[,]+β))) |
18 | 3, 16, 17 | gsumconstf 19719 |
. . . . 5
β’
(((β*π βΎs
(0[,]+β)) β Mnd β§ π₯ β Fin β§ π΅ β (0[,]+β)) β
((β*π βΎs (0[,]+β))
Ξ£g (π β π₯ β¦ π΅)) = ((β―βπ₯)(.gβ(β*π
βΎs (0[,]+β)))π΅)) |
19 | 11, 14, 15, 18 | syl3anc 1372 |
. . . 4
β’ (((π΄ β π β§ π΅ β (0[,]+β)) β§ π₯ β (π« π΄ β© Fin)) β
((β*π βΎs (0[,]+β))
Ξ£g (π β π₯ β¦ π΅)) = ((β―βπ₯)(.gβ(β*π
βΎs (0[,]+β)))π΅)) |
20 | | hashcl 14263 |
. . . . . 6
β’ (π₯ β Fin β
(β―βπ₯) β
β0) |
21 | 14, 20 | syl 17 |
. . . . 5
β’ (((π΄ β π β§ π΅ β (0[,]+β)) β§ π₯ β (π« π΄ β© Fin)) β
(β―βπ₯) β
β0) |
22 | | xrge0mulgnn0 31922 |
. . . . 5
β’
(((β―βπ₯)
β β0 β§ π΅ β (0[,]+β)) β
((β―βπ₯)(.gβ(β*π
βΎs (0[,]+β)))π΅) =
((β―βπ₯) Β·e
π΅)) |
23 | 21, 15, 22 | syl2anc 585 |
. . . 4
β’ (((π΄ β π β§ π΅ β (0[,]+β)) β§ π₯ β (π« π΄ β© Fin)) β
((β―βπ₯)(.gβ(β*π
βΎs (0[,]+β)))π΅) =
((β―βπ₯) Β·e
π΅)) |
24 | 19, 23 | eqtrd 2777 |
. . 3
β’ (((π΄ β π β§ π΅ β (0[,]+β)) β§ π₯ β (π« π΄ β© Fin)) β
((β*π βΎs (0[,]+β))
Ξ£g (π β π₯ β¦ π΅)) = ((β―βπ₯) Β·e π΅)) |
25 | 5, 1, 6, 7, 24 | esumval 32685 |
. 2
β’ ((π΄ β π β§ π΅ β (0[,]+β)) β
Ξ£*π β
π΄π΅ = sup(ran (π₯ β (π« π΄ β© Fin) β¦ ((β―βπ₯) Β·e π΅)), β*, <
)) |
26 | | nn0ssre 12424 |
. . . . . . . . . 10
β’
β0 β β |
27 | | ressxr 11206 |
. . . . . . . . . 10
β’ β
β β* |
28 | 26, 27 | sstri 3958 |
. . . . . . . . 9
β’
β0 β β* |
29 | | pnfxr 11216 |
. . . . . . . . . 10
β’ +β
β β* |
30 | | snssi 4773 |
. . . . . . . . . 10
β’ (+β
β β* β {+β} β
β*) |
31 | 29, 30 | ax-mp 5 |
. . . . . . . . 9
β’
{+β} β β* |
32 | 28, 31 | unssi 4150 |
. . . . . . . 8
β’
(β0 βͺ {+β}) β
β* |
33 | | hashf 14245 |
. . . . . . . . 9
β’
β―:VβΆ(β0 βͺ {+β}) |
34 | | vex 3452 |
. . . . . . . . 9
β’ π₯ β V |
35 | | ffvelcdm 7037 |
. . . . . . . . 9
β’
((β―:VβΆ(β0 βͺ {+β}) β§ π₯ β V) β
(β―βπ₯) β
(β0 βͺ {+β})) |
36 | 33, 34, 35 | mp2an 691 |
. . . . . . . 8
β’
(β―βπ₯)
β (β0 βͺ {+β}) |
37 | 32, 36 | sselii 3946 |
. . . . . . 7
β’
(β―βπ₯)
β β* |
38 | 37 | a1i 11 |
. . . . . 6
β’ (((π΄ β π β§ π΅ β (0[,]+β)) β§ π₯ β (π« π΄ β© Fin)) β
(β―βπ₯) β
β*) |
39 | | iccssxr 13354 |
. . . . . . . 8
β’
(0[,]+β) β β* |
40 | | simpr 486 |
. . . . . . . 8
β’ ((π΄ β π β§ π΅ β (0[,]+β)) β π΅ β
(0[,]+β)) |
41 | 39, 40 | sselid 3947 |
. . . . . . 7
β’ ((π΄ β π β§ π΅ β (0[,]+β)) β π΅ β
β*) |
42 | 41 | adantr 482 |
. . . . . 6
β’ (((π΄ β π β§ π΅ β (0[,]+β)) β§ π₯ β (π« π΄ β© Fin)) β π΅ β
β*) |
43 | 38, 42 | xmulcld 13228 |
. . . . 5
β’ (((π΄ β π β§ π΅ β (0[,]+β)) β§ π₯ β (π« π΄ β© Fin)) β
((β―βπ₯)
Β·e π΅)
β β*) |
44 | 43 | fmpttd 7068 |
. . . 4
β’ ((π΄ β π β§ π΅ β (0[,]+β)) β (π₯ β (π« π΄ β© Fin) β¦
((β―βπ₯)
Β·e π΅)):(π« π΄ β©
Fin)βΆβ*) |
45 | 44 | frnd 6681 |
. . 3
β’ ((π΄ β π β§ π΅ β (0[,]+β)) β ran (π₯ β (π« π΄ β© Fin) β¦
((β―βπ₯)
Β·e π΅))
β β*) |
46 | | hashxrcl 14264 |
. . . . 5
β’ (π΄ β π β (β―βπ΄) β
β*) |
47 | 46 | adantr 482 |
. . . 4
β’ ((π΄ β π β§ π΅ β (0[,]+β)) β
(β―βπ΄) β
β*) |
48 | 47, 41 | xmulcld 13228 |
. . 3
β’ ((π΄ β π β§ π΅ β (0[,]+β)) β
((β―βπ΄)
Β·e π΅)
β β*) |
49 | | vex 3452 |
. . . . . . . 8
β’ π¦ β V |
50 | | eqid 2737 |
. . . . . . . . 9
β’ (π₯ β (π« π΄ β© Fin) β¦
((β―βπ₯)
Β·e π΅)) =
(π₯ β (π« π΄ β© Fin) β¦
((β―βπ₯)
Β·e π΅)) |
51 | 50 | elrnmpt 5916 |
. . . . . . . 8
β’ (π¦ β V β (π¦ β ran (π₯ β (π« π΄ β© Fin) β¦ ((β―βπ₯) Β·e π΅)) β βπ₯ β (π« π΄ β© Fin)π¦ = ((β―βπ₯) Β·e π΅))) |
52 | 49, 51 | ax-mp 5 |
. . . . . . 7
β’ (π¦ β ran (π₯ β (π« π΄ β© Fin) β¦ ((β―βπ₯) Β·e π΅)) β βπ₯ β (π« π΄ β© Fin)π¦ = ((β―βπ₯) Β·e π΅)) |
53 | 52 | biimpi 215 |
. . . . . 6
β’ (π¦ β ran (π₯ β (π« π΄ β© Fin) β¦ ((β―βπ₯) Β·e π΅)) β βπ₯ β (π« π΄ β© Fin)π¦ = ((β―βπ₯) Β·e π΅)) |
54 | 47 | adantr 482 |
. . . . . . . 8
β’ (((π΄ β π β§ π΅ β (0[,]+β)) β§ π₯ β (π« π΄ β© Fin)) β
(β―βπ΄) β
β*) |
55 | | 0xr 11209 |
. . . . . . . . . . 11
β’ 0 β
β* |
56 | 55 | a1i 11 |
. . . . . . . . . 10
β’ (((π΄ β π β§ π΅ β (0[,]+β)) β§ π₯ β (π« π΄ β© Fin)) β 0 β
β*) |
57 | 29 | a1i 11 |
. . . . . . . . . 10
β’ (((π΄ β π β§ π΅ β (0[,]+β)) β§ π₯ β (π« π΄ β© Fin)) β +β
β β*) |
58 | | iccgelb 13327 |
. . . . . . . . . 10
β’ ((0
β β* β§ +β β β* β§
π΅ β (0[,]+β))
β 0 β€ π΅) |
59 | 56, 57, 15, 58 | syl3anc 1372 |
. . . . . . . . 9
β’ (((π΄ β π β§ π΅ β (0[,]+β)) β§ π₯ β (π« π΄ β© Fin)) β 0 β€ π΅) |
60 | 42, 59 | jca 513 |
. . . . . . . 8
β’ (((π΄ β π β§ π΅ β (0[,]+β)) β§ π₯ β (π« π΄ β© Fin)) β (π΅ β β*
β§ 0 β€ π΅)) |
61 | 6 | adantr 482 |
. . . . . . . . . 10
β’ (((π΄ β π β§ π΅ β (0[,]+β)) β§ π₯ β (π« π΄ β© Fin)) β π΄ β π) |
62 | | inss1 4193 |
. . . . . . . . . . . 12
β’
(π« π΄ β©
Fin) β π« π΄ |
63 | 62 | sseli 3945 |
. . . . . . . . . . 11
β’ (π₯ β (π« π΄ β© Fin) β π₯ β π« π΄) |
64 | | elpwi 4572 |
. . . . . . . . . . 11
β’ (π₯ β π« π΄ β π₯ β π΄) |
65 | 13, 63, 64 | 3syl 18 |
. . . . . . . . . 10
β’ (((π΄ β π β§ π΅ β (0[,]+β)) β§ π₯ β (π« π΄ β© Fin)) β π₯ β π΄) |
66 | | ssdomg 8947 |
. . . . . . . . . 10
β’ (π΄ β π β (π₯ β π΄ β π₯ βΌ π΄)) |
67 | 61, 65, 66 | sylc 65 |
. . . . . . . . 9
β’ (((π΄ β π β§ π΅ β (0[,]+β)) β§ π₯ β (π« π΄ β© Fin)) β π₯ βΌ π΄) |
68 | | hashdomi 14287 |
. . . . . . . . 9
β’ (π₯ βΌ π΄ β (β―βπ₯) β€ (β―βπ΄)) |
69 | 67, 68 | syl 17 |
. . . . . . . 8
β’ (((π΄ β π β§ π΅ β (0[,]+β)) β§ π₯ β (π« π΄ β© Fin)) β
(β―βπ₯) β€
(β―βπ΄)) |
70 | | xlemul1a 13214 |
. . . . . . . 8
β’
((((β―βπ₯)
β β* β§ (β―βπ΄) β β* β§ (π΅ β β*
β§ 0 β€ π΅)) β§
(β―βπ₯) β€
(β―βπ΄)) β
((β―βπ₯)
Β·e π΅)
β€ ((β―βπ΄)
Β·e π΅)) |
71 | 38, 54, 60, 69, 70 | syl31anc 1374 |
. . . . . . 7
β’ (((π΄ β π β§ π΅ β (0[,]+β)) β§ π₯ β (π« π΄ β© Fin)) β
((β―βπ₯)
Β·e π΅)
β€ ((β―βπ΄)
Β·e π΅)) |
72 | 71 | ralrimiva 3144 |
. . . . . 6
β’ ((π΄ β π β§ π΅ β (0[,]+β)) β βπ₯ β (π« π΄ β© Fin)((β―βπ₯) Β·e π΅) β€ ((β―βπ΄) Β·e π΅)) |
73 | | r19.29r 3120 |
. . . . . 6
β’
((βπ₯ β
(π« π΄ β©
Fin)π¦ =
((β―βπ₯)
Β·e π΅)
β§ βπ₯ β
(π« π΄ β©
Fin)((β―βπ₯)
Β·e π΅)
β€ ((β―βπ΄)
Β·e π΅))
β βπ₯ β
(π« π΄ β©
Fin)(π¦ =
((β―βπ₯)
Β·e π΅)
β§ ((β―βπ₯)
Β·e π΅)
β€ ((β―βπ΄)
Β·e π΅))) |
74 | 53, 72, 73 | syl2anr 598 |
. . . . 5
β’ (((π΄ β π β§ π΅ β (0[,]+β)) β§ π¦ β ran (π₯ β (π« π΄ β© Fin) β¦ ((β―βπ₯) Β·e π΅))) β βπ₯ β (π« π΄ β© Fin)(π¦ = ((β―βπ₯) Β·e π΅) β§ ((β―βπ₯) Β·e π΅) β€ ((β―βπ΄) Β·e π΅))) |
75 | | simpl 484 |
. . . . . . 7
β’ ((π¦ = ((β―βπ₯) Β·e π΅) β§ ((β―βπ₯) Β·e π΅) β€ ((β―βπ΄) Β·e π΅)) β π¦ = ((β―βπ₯) Β·e π΅)) |
76 | | simpr 486 |
. . . . . . 7
β’ ((π¦ = ((β―βπ₯) Β·e π΅) β§ ((β―βπ₯) Β·e π΅) β€ ((β―βπ΄) Β·e π΅)) β ((β―βπ₯) Β·e π΅) β€ ((β―βπ΄) Β·e π΅)) |
77 | 75, 76 | eqbrtrd 5132 |
. . . . . 6
β’ ((π¦ = ((β―βπ₯) Β·e π΅) β§ ((β―βπ₯) Β·e π΅) β€ ((β―βπ΄) Β·e π΅)) β π¦ β€ ((β―βπ΄) Β·e π΅)) |
78 | 77 | rexlimivw 3149 |
. . . . 5
β’
(βπ₯ β
(π« π΄ β©
Fin)(π¦ =
((β―βπ₯)
Β·e π΅)
β§ ((β―βπ₯)
Β·e π΅)
β€ ((β―βπ΄)
Β·e π΅))
β π¦ β€
((β―βπ΄)
Β·e π΅)) |
79 | 74, 78 | syl 17 |
. . . 4
β’ (((π΄ β π β§ π΅ β (0[,]+β)) β§ π¦ β ran (π₯ β (π« π΄ β© Fin) β¦ ((β―βπ₯) Β·e π΅))) β π¦ β€ ((β―βπ΄) Β·e π΅)) |
80 | 79 | ralrimiva 3144 |
. . 3
β’ ((π΄ β π β§ π΅ β (0[,]+β)) β βπ¦ β ran (π₯ β (π« π΄ β© Fin) β¦ ((β―βπ₯) Β·e π΅))π¦ β€ ((β―βπ΄) Β·e π΅)) |
81 | | pwidg 4585 |
. . . . . . . . . . 11
β’ (π΄ β Fin β π΄ β π« π΄) |
82 | 81 | ancri 551 |
. . . . . . . . . 10
β’ (π΄ β Fin β (π΄ β π« π΄ β§ π΄ β Fin)) |
83 | | elin 3931 |
. . . . . . . . . 10
β’ (π΄ β (π« π΄ β© Fin) β (π΄ β π« π΄ β§ π΄ β Fin)) |
84 | 82, 83 | sylibr 233 |
. . . . . . . . 9
β’ (π΄ β Fin β π΄ β (π« π΄ β© Fin)) |
85 | | eqid 2737 |
. . . . . . . . . . 11
β’
((β―βπ΄)
Β·e π΅) =
((β―βπ΄)
Β·e π΅) |
86 | | fveq2 6847 |
. . . . . . . . . . . . 13
β’ (π₯ = π΄ β (β―βπ₯) = (β―βπ΄)) |
87 | 86 | oveq1d 7377 |
. . . . . . . . . . . 12
β’ (π₯ = π΄ β ((β―βπ₯) Β·e π΅) = ((β―βπ΄) Β·e π΅)) |
88 | 87 | rspceeqv 3600 |
. . . . . . . . . . 11
β’ ((π΄ β (π« π΄ β© Fin) β§
((β―βπ΄)
Β·e π΅) =
((β―βπ΄)
Β·e π΅))
β βπ₯ β
(π« π΄ β©
Fin)((β―βπ΄)
Β·e π΅) =
((β―βπ₯)
Β·e π΅)) |
89 | 85, 88 | mpan2 690 |
. . . . . . . . . 10
β’ (π΄ β (π« π΄ β© Fin) β βπ₯ β (π« π΄ β© Fin)((β―βπ΄) Β·e π΅) = ((β―βπ₯) Β·e π΅)) |
90 | | ovex 7395 |
. . . . . . . . . . 11
β’
((β―βπ΄)
Β·e π΅)
β V |
91 | 50 | elrnmpt 5916 |
. . . . . . . . . . 11
β’
(((β―βπ΄)
Β·e π΅)
β V β (((β―βπ΄) Β·e π΅) β ran (π₯ β (π« π΄ β© Fin) β¦ ((β―βπ₯) Β·e π΅)) β βπ₯ β (π« π΄ β© Fin)((β―βπ΄) Β·e π΅) = ((β―βπ₯) Β·e π΅))) |
92 | 90, 91 | ax-mp 5 |
. . . . . . . . . 10
β’
(((β―βπ΄)
Β·e π΅)
β ran (π₯ β
(π« π΄ β© Fin)
β¦ ((β―βπ₯)
Β·e π΅))
β βπ₯ β
(π« π΄ β©
Fin)((β―βπ΄)
Β·e π΅) =
((β―βπ₯)
Β·e π΅)) |
93 | 89, 92 | sylibr 233 |
. . . . . . . . 9
β’ (π΄ β (π« π΄ β© Fin) β
((β―βπ΄)
Β·e π΅)
β ran (π₯ β
(π« π΄ β© Fin)
β¦ ((β―βπ₯)
Β·e π΅))) |
94 | 84, 93 | syl 17 |
. . . . . . . 8
β’ (π΄ β Fin β
((β―βπ΄)
Β·e π΅)
β ran (π₯ β
(π« π΄ β© Fin)
β¦ ((β―βπ₯)
Β·e π΅))) |
95 | 94 | adantl 483 |
. . . . . . 7
β’
(((((π΄ β π β§ π΅ β (0[,]+β)) β§ π¦ β β) β§ π¦ < ((β―βπ΄) Β·e π΅)) β§ π΄ β Fin) β ((β―βπ΄) Β·e π΅) β ran (π₯ β (π« π΄ β© Fin) β¦ ((β―βπ₯) Β·e π΅))) |
96 | | simplr 768 |
. . . . . . 7
β’
(((((π΄ β π β§ π΅ β (0[,]+β)) β§ π¦ β β) β§ π¦ < ((β―βπ΄) Β·e π΅)) β§ π΄ β Fin) β π¦ < ((β―βπ΄) Β·e π΅)) |
97 | | breq2 5114 |
. . . . . . . 8
β’ (π§ = ((β―βπ΄) Β·e π΅) β (π¦ < π§ β π¦ < ((β―βπ΄) Β·e π΅))) |
98 | 97 | rspcev 3584 |
. . . . . . 7
β’
((((β―βπ΄)
Β·e π΅)
β ran (π₯ β
(π« π΄ β© Fin)
β¦ ((β―βπ₯)
Β·e π΅))
β§ π¦ <
((β―βπ΄)
Β·e π΅))
β βπ§ β ran
(π₯ β (π« π΄ β© Fin) β¦
((β―βπ₯)
Β·e π΅))π¦ < π§) |
99 | 95, 96, 98 | syl2anc 585 |
. . . . . 6
β’
(((((π΄ β π β§ π΅ β (0[,]+β)) β§ π¦ β β) β§ π¦ < ((β―βπ΄) Β·e π΅)) β§ π΄ β Fin) β βπ§ β ran (π₯ β (π« π΄ β© Fin) β¦ ((β―βπ₯) Β·e π΅))π¦ < π§) |
100 | | 0elpw 5316 |
. . . . . . . . . . . 12
β’ β
β π« π΄ |
101 | | 0fin 9122 |
. . . . . . . . . . . 12
β’ β
β Fin |
102 | | elin 3931 |
. . . . . . . . . . . 12
β’ (β
β (π« π΄ β©
Fin) β (β
β π« π΄ β§ β
β Fin)) |
103 | 100, 101,
102 | mpbir2an 710 |
. . . . . . . . . . 11
β’ β
β (π« π΄ β©
Fin) |
104 | 103 | a1i 11 |
. . . . . . . . . 10
β’
((((((π΄ β π β§ π΅ β (0[,]+β)) β§ π¦ β β) β§ π¦ < ((β―βπ΄) Β·e π΅)) β§ Β¬ π΄ β Fin) β§ π΅ = 0) β β
β (π« π΄ β© Fin)) |
105 | | simpr 486 |
. . . . . . . . . . . 12
β’
((((((π΄ β π β§ π΅ β (0[,]+β)) β§ π¦ β β) β§ π¦ < ((β―βπ΄) Β·e π΅)) β§ Β¬ π΄ β Fin) β§ π΅ = 0) β π΅ = 0) |
106 | 105 | oveq2d 7378 |
. . . . . . . . . . 11
β’
((((((π΄ β π β§ π΅ β (0[,]+β)) β§ π¦ β β) β§ π¦ < ((β―βπ΄) Β·e π΅)) β§ Β¬ π΄ β Fin) β§ π΅ = 0) β ((β―ββ
)
Β·e π΅) =
((β―ββ
) Β·e 0)) |
107 | | hash0 14274 |
. . . . . . . . . . . . 13
β’
(β―ββ
) = 0 |
108 | 107, 55 | eqeltri 2834 |
. . . . . . . . . . . 12
β’
(β―ββ
) β β* |
109 | | xmul01 13193 |
. . . . . . . . . . . 12
β’
((β―ββ
) β β* β
((β―ββ
) Β·e 0) = 0) |
110 | 108, 109 | ax-mp 5 |
. . . . . . . . . . 11
β’
((β―ββ
) Β·e 0) = 0 |
111 | 106, 110 | eqtr2di 2794 |
. . . . . . . . . 10
β’
((((((π΄ β π β§ π΅ β (0[,]+β)) β§ π¦ β β) β§ π¦ < ((β―βπ΄) Β·e π΅)) β§ Β¬ π΄ β Fin) β§ π΅ = 0) β 0 = ((β―ββ
)
Β·e π΅)) |
112 | | fveq2 6847 |
. . . . . . . . . . . 12
β’ (π₯ = β
β
(β―βπ₯) =
(β―ββ
)) |
113 | 112 | oveq1d 7377 |
. . . . . . . . . . 11
β’ (π₯ = β
β
((β―βπ₯)
Β·e π΅) =
((β―ββ
) Β·e π΅)) |
114 | 113 | rspceeqv 3600 |
. . . . . . . . . 10
β’ ((β
β (π« π΄ β©
Fin) β§ 0 = ((β―ββ
) Β·e π΅)) β βπ₯ β (π« π΄ β© Fin)0 = ((β―βπ₯) Β·e π΅)) |
115 | 104, 111,
114 | syl2anc 585 |
. . . . . . . . 9
β’
((((((π΄ β π β§ π΅ β (0[,]+β)) β§ π¦ β β) β§ π¦ < ((β―βπ΄) Β·e π΅)) β§ Β¬ π΄ β Fin) β§ π΅ = 0) β βπ₯ β (π« π΄ β© Fin)0 = ((β―βπ₯) Β·e π΅)) |
116 | | ovex 7395 |
. . . . . . . . . 10
β’
((β―βπ₯)
Β·e π΅)
β V |
117 | 50, 116 | elrnmpti 5920 |
. . . . . . . . 9
β’ (0 β
ran (π₯ β (π«
π΄ β© Fin) β¦
((β―βπ₯)
Β·e π΅))
β βπ₯ β
(π« π΄ β© Fin)0 =
((β―βπ₯)
Β·e π΅)) |
118 | 115, 117 | sylibr 233 |
. . . . . . . 8
β’
((((((π΄ β π β§ π΅ β (0[,]+β)) β§ π¦ β β) β§ π¦ < ((β―βπ΄) Β·e π΅)) β§ Β¬ π΄ β Fin) β§ π΅ = 0) β 0 β ran (π₯ β (π« π΄ β© Fin) β¦
((β―βπ₯)
Β·e π΅))) |
119 | | simpllr 775 |
. . . . . . . . 9
β’
((((((π΄ β π β§ π΅ β (0[,]+β)) β§ π¦ β β) β§ π¦ < ((β―βπ΄) Β·e π΅)) β§ Β¬ π΄ β Fin) β§ π΅ = 0) β π¦ < ((β―βπ΄) Β·e π΅)) |
120 | 105 | oveq2d 7378 |
. . . . . . . . . 10
β’
((((((π΄ β π β§ π΅ β (0[,]+β)) β§ π¦ β β) β§ π¦ < ((β―βπ΄) Β·e π΅)) β§ Β¬ π΄ β Fin) β§ π΅ = 0) β ((β―βπ΄) Β·e π΅) = ((β―βπ΄) Β·e
0)) |
121 | 47 | ad4antr 731 |
. . . . . . . . . . 11
β’
((((((π΄ β π β§ π΅ β (0[,]+β)) β§ π¦ β β) β§ π¦ < ((β―βπ΄) Β·e π΅)) β§ Β¬ π΄ β Fin) β§ π΅ = 0) β (β―βπ΄) β
β*) |
122 | | xmul01 13193 |
. . . . . . . . . . 11
β’
((β―βπ΄)
β β* β ((β―βπ΄) Β·e 0) =
0) |
123 | 121, 122 | syl 17 |
. . . . . . . . . 10
β’
((((((π΄ β π β§ π΅ β (0[,]+β)) β§ π¦ β β) β§ π¦ < ((β―βπ΄) Β·e π΅)) β§ Β¬ π΄ β Fin) β§ π΅ = 0) β ((β―βπ΄) Β·e 0) =
0) |
124 | 120, 123 | eqtrd 2777 |
. . . . . . . . 9
β’
((((((π΄ β π β§ π΅ β (0[,]+β)) β§ π¦ β β) β§ π¦ < ((β―βπ΄) Β·e π΅)) β§ Β¬ π΄ β Fin) β§ π΅ = 0) β ((β―βπ΄) Β·e π΅) = 0) |
125 | 119, 124 | breqtrd 5136 |
. . . . . . . 8
β’
((((((π΄ β π β§ π΅ β (0[,]+β)) β§ π¦ β β) β§ π¦ < ((β―βπ΄) Β·e π΅)) β§ Β¬ π΄ β Fin) β§ π΅ = 0) β π¦ < 0) |
126 | | breq2 5114 |
. . . . . . . . 9
β’ (π§ = 0 β (π¦ < π§ β π¦ < 0)) |
127 | 126 | rspcev 3584 |
. . . . . . . 8
β’ ((0
β ran (π₯ β
(π« π΄ β© Fin)
β¦ ((β―βπ₯)
Β·e π΅))
β§ π¦ < 0) β
βπ§ β ran (π₯ β (π« π΄ β© Fin) β¦
((β―βπ₯)
Β·e π΅))π¦ < π§) |
128 | 118, 125,
127 | syl2anc 585 |
. . . . . . 7
β’
((((((π΄ β π β§ π΅ β (0[,]+β)) β§ π¦ β β) β§ π¦ < ((β―βπ΄) Β·e π΅)) β§ Β¬ π΄ β Fin) β§ π΅ = 0) β βπ§ β ran (π₯ β (π« π΄ β© Fin) β¦ ((β―βπ₯) Β·e π΅))π¦ < π§) |
129 | | simplr 768 |
. . . . . . . . . . . . . 14
β’
((((((((((π΄ β
π β§ π΅ β (0[,]+β)) β§ π¦ β β) β§ π¦ < ((β―βπ΄) Β·e π΅)) β§ Β¬ π΄ β Fin) β§ π΅ β β+) β§ π β β) β§ (π¦ / π΅) < π) β§ π β π« π΄) β§ (β―βπ) = π) β π β π« π΄) |
130 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’
((((((((((π΄ β
π β§ π΅ β (0[,]+β)) β§ π¦ β β) β§ π¦ < ((β―βπ΄) Β·e π΅)) β§ Β¬ π΄ β Fin) β§ π΅ β β+) β§ π β β) β§ (π¦ / π΅) < π) β§ π β π« π΄) β§ (β―βπ) = π) β (β―βπ) = π) |
131 | | simp-4r 783 |
. . . . . . . . . . . . . . . 16
β’
((((((((((π΄ β
π β§ π΅ β (0[,]+β)) β§ π¦ β β) β§ π¦ < ((β―βπ΄) Β·e π΅)) β§ Β¬ π΄ β Fin) β§ π΅ β β+) β§ π β β) β§ (π¦ / π΅) < π) β§ π β π« π΄) β§ (β―βπ) = π) β π β β) |
132 | 130, 131 | eqeltrd 2838 |
. . . . . . . . . . . . . . 15
β’
((((((((((π΄ β
π β§ π΅ β (0[,]+β)) β§ π¦ β β) β§ π¦ < ((β―βπ΄) Β·e π΅)) β§ Β¬ π΄ β Fin) β§ π΅ β β+) β§ π β β) β§ (π¦ / π΅) < π) β§ π β π« π΄) β§ (β―βπ) = π) β (β―βπ) β β) |
133 | | nnnn0 12427 |
. . . . . . . . . . . . . . . 16
β’
((β―βπ)
β β β (β―βπ) β
β0) |
134 | | vex 3452 |
. . . . . . . . . . . . . . . . 17
β’ π β V |
135 | | hashclb 14265 |
. . . . . . . . . . . . . . . . 17
β’ (π β V β (π β Fin β
(β―βπ) β
β0)) |
136 | 134, 135 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
β’ (π β Fin β
(β―βπ) β
β0) |
137 | 133, 136 | sylibr 233 |
. . . . . . . . . . . . . . 15
β’
((β―βπ)
β β β π
β Fin) |
138 | 132, 137 | syl 17 |
. . . . . . . . . . . . . 14
β’
((((((((((π΄ β
π β§ π΅ β (0[,]+β)) β§ π¦ β β) β§ π¦ < ((β―βπ΄) Β·e π΅)) β§ Β¬ π΄ β Fin) β§ π΅ β β+) β§ π β β) β§ (π¦ / π΅) < π) β§ π β π« π΄) β§ (β―βπ) = π) β π β Fin) |
139 | 129, 138 | elind 4159 |
. . . . . . . . . . . . 13
β’
((((((((((π΄ β
π β§ π΅ β (0[,]+β)) β§ π¦ β β) β§ π¦ < ((β―βπ΄) Β·e π΅)) β§ Β¬ π΄ β Fin) β§ π΅ β β+) β§ π β β) β§ (π¦ / π΅) < π) β§ π β π« π΄) β§ (β―βπ) = π) β π β (π« π΄ β© Fin)) |
140 | | eqidd 2738 |
. . . . . . . . . . . . 13
β’
((((((((((π΄ β
π β§ π΅ β (0[,]+β)) β§ π¦ β β) β§ π¦ < ((β―βπ΄) Β·e π΅)) β§ Β¬ π΄ β Fin) β§ π΅ β β+) β§ π β β) β§ (π¦ / π΅) < π) β§ π β π« π΄) β§ (β―βπ) = π) β ((β―βπ) Β·e π΅) = ((β―βπ) Β·e π΅)) |
141 | | fveq2 6847 |
. . . . . . . . . . . . . . 15
β’ (π₯ = π β (β―βπ₯) = (β―βπ)) |
142 | 141 | oveq1d 7377 |
. . . . . . . . . . . . . 14
β’ (π₯ = π β ((β―βπ₯) Β·e π΅) = ((β―βπ) Β·e π΅)) |
143 | 142 | rspceeqv 3600 |
. . . . . . . . . . . . 13
β’ ((π β (π« π΄ β© Fin) β§
((β―βπ)
Β·e π΅) =
((β―βπ)
Β·e π΅))
β βπ₯ β
(π« π΄ β©
Fin)((β―βπ)
Β·e π΅) =
((β―βπ₯)
Β·e π΅)) |
144 | 139, 140,
143 | syl2anc 585 |
. . . . . . . . . . . 12
β’
((((((((((π΄ β
π β§ π΅ β (0[,]+β)) β§ π¦ β β) β§ π¦ < ((β―βπ΄) Β·e π΅)) β§ Β¬ π΄ β Fin) β§ π΅ β β+) β§ π β β) β§ (π¦ / π΅) < π) β§ π β π« π΄) β§ (β―βπ) = π) β βπ₯ β (π« π΄ β© Fin)((β―βπ) Β·e π΅) = ((β―βπ₯) Β·e π΅)) |
145 | 50, 116 | elrnmpti 5920 |
. . . . . . . . . . . 12
β’
(((β―βπ)
Β·e π΅)
β ran (π₯ β
(π« π΄ β© Fin)
β¦ ((β―βπ₯)
Β·e π΅))
β βπ₯ β
(π« π΄ β©
Fin)((β―βπ)
Β·e π΅) =
((β―βπ₯)
Β·e π΅)) |
146 | 144, 145 | sylibr 233 |
. . . . . . . . . . 11
β’
((((((((((π΄ β
π β§ π΅ β (0[,]+β)) β§ π¦ β β) β§ π¦ < ((β―βπ΄) Β·e π΅)) β§ Β¬ π΄ β Fin) β§ π΅ β β+) β§ π β β) β§ (π¦ / π΅) < π) β§ π β π« π΄) β§ (β―βπ) = π) β ((β―βπ) Β·e π΅) β ran (π₯ β (π« π΄ β© Fin) β¦ ((β―βπ₯) Β·e π΅))) |
147 | | simpllr 775 |
. . . . . . . . . . . . 13
β’
((((((((((π΄ β
π β§ π΅ β (0[,]+β)) β§ π¦ β β) β§ π¦ < ((β―βπ΄) Β·e π΅)) β§ Β¬ π΄ β Fin) β§ π΅ β β+) β§ π β β) β§ (π¦ / π΅) < π) β§ π β π« π΄) β§ (β―βπ) = π) β (π¦ / π΅) < π) |
148 | | simp-8r 791 |
. . . . . . . . . . . . . 14
β’
((((((((((π΄ β
π β§ π΅ β (0[,]+β)) β§ π¦ β β) β§ π¦ < ((β―βπ΄) Β·e π΅)) β§ Β¬ π΄ β Fin) β§ π΅ β β+) β§ π β β) β§ (π¦ / π΅) < π) β§ π β π« π΄) β§ (β―βπ) = π) β π¦ β β) |
149 | 131 | nnred 12175 |
. . . . . . . . . . . . . 14
β’
((((((((((π΄ β
π β§ π΅ β (0[,]+β)) β§ π¦ β β) β§ π¦ < ((β―βπ΄) Β·e π΅)) β§ Β¬ π΄ β Fin) β§ π΅ β β+) β§ π β β) β§ (π¦ / π΅) < π) β§ π β π« π΄) β§ (β―βπ) = π) β π β β) |
150 | | simp-5r 785 |
. . . . . . . . . . . . . 14
β’
((((((((((π΄ β
π β§ π΅ β (0[,]+β)) β§ π¦ β β) β§ π¦ < ((β―βπ΄) Β·e π΅)) β§ Β¬ π΄ β Fin) β§ π΅ β β+) β§ π β β) β§ (π¦ / π΅) < π) β§ π β π« π΄) β§ (β―βπ) = π) β π΅ β
β+) |
151 | 148, 149,
150 | ltdivmul2d 13016 |
. . . . . . . . . . . . 13
β’
((((((((((π΄ β
π β§ π΅ β (0[,]+β)) β§ π¦ β β) β§ π¦ < ((β―βπ΄) Β·e π΅)) β§ Β¬ π΄ β Fin) β§ π΅ β β+) β§ π β β) β§ (π¦ / π΅) < π) β§ π β π« π΄) β§ (β―βπ) = π) β ((π¦ / π΅) < π β π¦ < (π Β· π΅))) |
152 | 147, 151 | mpbid 231 |
. . . . . . . . . . . 12
β’
((((((((((π΄ β
π β§ π΅ β (0[,]+β)) β§ π¦ β β) β§ π¦ < ((β―βπ΄) Β·e π΅)) β§ Β¬ π΄ β Fin) β§ π΅ β β+) β§ π β β) β§ (π¦ / π΅) < π) β§ π β π« π΄) β§ (β―βπ) = π) β π¦ < (π Β· π΅)) |
153 | 130 | oveq1d 7377 |
. . . . . . . . . . . . 13
β’
((((((((((π΄ β
π β§ π΅ β (0[,]+β)) β§ π¦ β β) β§ π¦ < ((β―βπ΄) Β·e π΅)) β§ Β¬ π΄ β Fin) β§ π΅ β β+) β§ π β β) β§ (π¦ / π΅) < π) β§ π β π« π΄) β§ (β―βπ) = π) β ((β―βπ) Β·e π΅) = (π Β·e π΅)) |
154 | 150 | rpred 12964 |
. . . . . . . . . . . . . 14
β’
((((((((((π΄ β
π β§ π΅ β (0[,]+β)) β§ π¦ β β) β§ π¦ < ((β―βπ΄) Β·e π΅)) β§ Β¬ π΄ β Fin) β§ π΅ β β+) β§ π β β) β§ (π¦ / π΅) < π) β§ π β π« π΄) β§ (β―βπ) = π) β π΅ β β) |
155 | | rexmul 13197 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ π΅ β β) β (π Β·e π΅) = (π Β· π΅)) |
156 | 149, 154,
155 | syl2anc 585 |
. . . . . . . . . . . . 13
β’
((((((((((π΄ β
π β§ π΅ β (0[,]+β)) β§ π¦ β β) β§ π¦ < ((β―βπ΄) Β·e π΅)) β§ Β¬ π΄ β Fin) β§ π΅ β β+) β§ π β β) β§ (π¦ / π΅) < π) β§ π β π« π΄) β§ (β―βπ) = π) β (π Β·e π΅) = (π Β· π΅)) |
157 | 153, 156 | eqtrd 2777 |
. . . . . . . . . . . 12
β’
((((((((((π΄ β
π β§ π΅ β (0[,]+β)) β§ π¦ β β) β§ π¦ < ((β―βπ΄) Β·e π΅)) β§ Β¬ π΄ β Fin) β§ π΅ β β+) β§ π β β) β§ (π¦ / π΅) < π) β§ π β π« π΄) β§ (β―βπ) = π) β ((β―βπ) Β·e π΅) = (π Β· π΅)) |
158 | 152, 157 | breqtrrd 5138 |
. . . . . . . . . . 11
β’
((((((((((π΄ β
π β§ π΅ β (0[,]+β)) β§ π¦ β β) β§ π¦ < ((β―βπ΄) Β·e π΅)) β§ Β¬ π΄ β Fin) β§ π΅ β β+) β§ π β β) β§ (π¦ / π΅) < π) β§ π β π« π΄) β§ (β―βπ) = π) β π¦ < ((β―βπ) Β·e π΅)) |
159 | | breq2 5114 |
. . . . . . . . . . . 12
β’ (π§ = ((β―βπ) Β·e π΅) β (π¦ < π§ β π¦ < ((β―βπ) Β·e π΅))) |
160 | 159 | rspcev 3584 |
. . . . . . . . . . 11
β’
((((β―βπ)
Β·e π΅)
β ran (π₯ β
(π« π΄ β© Fin)
β¦ ((β―βπ₯)
Β·e π΅))
β§ π¦ <
((β―βπ)
Β·e π΅))
β βπ§ β ran
(π₯ β (π« π΄ β© Fin) β¦
((β―βπ₯)
Β·e π΅))π¦ < π§) |
161 | 146, 158,
160 | syl2anc 585 |
. . . . . . . . . 10
β’
((((((((((π΄ β
π β§ π΅ β (0[,]+β)) β§ π¦ β β) β§ π¦ < ((β―βπ΄) Β·e π΅)) β§ Β¬ π΄ β Fin) β§ π΅ β β+) β§ π β β) β§ (π¦ / π΅) < π) β§ π β π« π΄) β§ (β―βπ) = π) β βπ§ β ran (π₯ β (π« π΄ β© Fin) β¦ ((β―βπ₯) Β·e π΅))π¦ < π§) |
162 | 161 | rexlimdva2 3155 |
. . . . . . . . 9
β’
((((((((π΄ β
π β§ π΅ β (0[,]+β)) β§ π¦ β β) β§ π¦ < ((β―βπ΄) Β·e π΅)) β§ Β¬ π΄ β Fin) β§ π΅ β β+) β§ π β β) β§ (π¦ / π΅) < π) β (βπ β π« π΄(β―βπ) = π β βπ§ β ran (π₯ β (π« π΄ β© Fin) β¦ ((β―βπ₯) Β·e π΅))π¦ < π§)) |
163 | 162 | impr 456 |
. . . . . . . 8
β’
((((((((π΄ β
π β§ π΅ β (0[,]+β)) β§ π¦ β β) β§ π¦ < ((β―βπ΄) Β·e π΅)) β§ Β¬ π΄ β Fin) β§ π΅ β β+) β§ π β β) β§ ((π¦ / π΅) < π β§ βπ β π« π΄(β―βπ) = π)) β βπ§ β ran (π₯ β (π« π΄ β© Fin) β¦ ((β―βπ₯) Β·e π΅))π¦ < π§) |
164 | | simp-4r 783 |
. . . . . . . . . . 11
β’
((((((π΄ β π β§ π΅ β (0[,]+β)) β§ π¦ β β) β§ π¦ < ((β―βπ΄) Β·e π΅)) β§ Β¬ π΄ β Fin) β§ π΅ β β+) β π¦ β
β) |
165 | | simpr 486 |
. . . . . . . . . . 11
β’
((((((π΄ β π β§ π΅ β (0[,]+β)) β§ π¦ β β) β§ π¦ < ((β―βπ΄) Β·e π΅)) β§ Β¬ π΄ β Fin) β§ π΅ β β+) β π΅ β
β+) |
166 | 164, 165 | rerpdivcld 12995 |
. . . . . . . . . 10
β’
((((((π΄ β π β§ π΅ β (0[,]+β)) β§ π¦ β β) β§ π¦ < ((β―βπ΄) Β·e π΅)) β§ Β¬ π΄ β Fin) β§ π΅ β β+) β (π¦ / π΅) β β) |
167 | | arch 12417 |
. . . . . . . . . 10
β’ ((π¦ / π΅) β β β βπ β β (π¦ / π΅) < π) |
168 | 166, 167 | syl 17 |
. . . . . . . . 9
β’
((((((π΄ β π β§ π΅ β (0[,]+β)) β§ π¦ β β) β§ π¦ < ((β―βπ΄) Β·e π΅)) β§ Β¬ π΄ β Fin) β§ π΅ β β+) β
βπ β β
(π¦ / π΅) < π) |
169 | | ishashinf 14369 |
. . . . . . . . . 10
β’ (Β¬
π΄ β Fin β
βπ β β
βπ β π«
π΄(β―βπ) = π) |
170 | 169 | ad2antlr 726 |
. . . . . . . . 9
β’
((((((π΄ β π β§ π΅ β (0[,]+β)) β§ π¦ β β) β§ π¦ < ((β―βπ΄) Β·e π΅)) β§ Β¬ π΄ β Fin) β§ π΅ β β+) β
βπ β β
βπ β π«
π΄(β―βπ) = π) |
171 | | r19.29r 3120 |
. . . . . . . . 9
β’
((βπ β
β (π¦ / π΅) < π β§ βπ β β βπ β π« π΄(β―βπ) = π) β βπ β β ((π¦ / π΅) < π β§ βπ β π« π΄(β―βπ) = π)) |
172 | 168, 170,
171 | syl2anc 585 |
. . . . . . . 8
β’
((((((π΄ β π β§ π΅ β (0[,]+β)) β§ π¦ β β) β§ π¦ < ((β―βπ΄) Β·e π΅)) β§ Β¬ π΄ β Fin) β§ π΅ β β+) β
βπ β β
((π¦ / π΅) < π β§ βπ β π« π΄(β―βπ) = π)) |
173 | 163, 172 | r19.29a 3160 |
. . . . . . 7
β’
((((((π΄ β π β§ π΅ β (0[,]+β)) β§ π¦ β β) β§ π¦ < ((β―βπ΄) Β·e π΅)) β§ Β¬ π΄ β Fin) β§ π΅ β β+) β
βπ§ β ran (π₯ β (π« π΄ β© Fin) β¦
((β―βπ₯)
Β·e π΅))π¦ < π§) |
174 | | nfielex 9224 |
. . . . . . . . . . . 12
β’ (Β¬
π΄ β Fin β
βπ π β π΄) |
175 | 174 | adantr 482 |
. . . . . . . . . . 11
β’ ((Β¬
π΄ β Fin β§ π΅ = +β) β βπ π β π΄) |
176 | | snelpwi 5405 |
. . . . . . . . . . . . . . 15
β’ (π β π΄ β {π} β π« π΄) |
177 | | snfi 8995 |
. . . . . . . . . . . . . . 15
β’ {π} β Fin |
178 | 176, 177 | jctir 522 |
. . . . . . . . . . . . . 14
β’ (π β π΄ β ({π} β π« π΄ β§ {π} β Fin)) |
179 | | elin 3931 |
. . . . . . . . . . . . . 14
β’ ({π} β (π« π΄ β© Fin) β ({π} β π« π΄ β§ {π} β Fin)) |
180 | 178, 179 | sylibr 233 |
. . . . . . . . . . . . 13
β’ (π β π΄ β {π} β (π« π΄ β© Fin)) |
181 | 180 | adantl 483 |
. . . . . . . . . . . 12
β’ (((Β¬
π΄ β Fin β§ π΅ = +β) β§ π β π΄) β {π} β (π« π΄ β© Fin)) |
182 | | simplr 768 |
. . . . . . . . . . . . . 14
β’ (((Β¬
π΄ β Fin β§ π΅ = +β) β§ π β π΄) β π΅ = +β) |
183 | 182 | oveq2d 7378 |
. . . . . . . . . . . . 13
β’ (((Β¬
π΄ β Fin β§ π΅ = +β) β§ π β π΄) β ((β―β{π}) Β·e π΅) = ((β―β{π}) Β·e
+β)) |
184 | | hashsng 14276 |
. . . . . . . . . . . . . . . 16
β’ (π β π΄ β (β―β{π}) = 1) |
185 | | 1re 11162 |
. . . . . . . . . . . . . . . . 17
β’ 1 β
β |
186 | 27, 185 | sselii 3946 |
. . . . . . . . . . . . . . . 16
β’ 1 β
β* |
187 | 184, 186 | eqeltrdi 2846 |
. . . . . . . . . . . . . . 15
β’ (π β π΄ β (β―β{π}) β
β*) |
188 | | 0lt1 11684 |
. . . . . . . . . . . . . . . 16
β’ 0 <
1 |
189 | 188, 184 | breqtrrid 5148 |
. . . . . . . . . . . . . . 15
β’ (π β π΄ β 0 < (β―β{π})) |
190 | | xmulpnf1 13200 |
. . . . . . . . . . . . . . 15
β’
(((β―β{π}) β β* β§ 0 <
(β―β{π})) β
((β―β{π})
Β·e +β) = +β) |
191 | 187, 189,
190 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (π β π΄ β ((β―β{π}) Β·e +β) =
+β) |
192 | 191 | adantl 483 |
. . . . . . . . . . . . 13
β’ (((Β¬
π΄ β Fin β§ π΅ = +β) β§ π β π΄) β ((β―β{π}) Β·e +β) =
+β) |
193 | 183, 192 | eqtr2d 2778 |
. . . . . . . . . . . 12
β’ (((Β¬
π΄ β Fin β§ π΅ = +β) β§ π β π΄) β +β = ((β―β{π}) Β·e π΅)) |
194 | | fveq2 6847 |
. . . . . . . . . . . . . 14
β’ (π₯ = {π} β (β―βπ₯) = (β―β{π})) |
195 | 194 | oveq1d 7377 |
. . . . . . . . . . . . 13
β’ (π₯ = {π} β ((β―βπ₯) Β·e π΅) = ((β―β{π}) Β·e π΅)) |
196 | 195 | rspceeqv 3600 |
. . . . . . . . . . . 12
β’ (({π} β (π« π΄ β© Fin) β§ +β =
((β―β{π})
Β·e π΅))
β βπ₯ β
(π« π΄ β©
Fin)+β = ((β―βπ₯) Β·e π΅)) |
197 | 181, 193,
196 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((Β¬
π΄ β Fin β§ π΅ = +β) β§ π β π΄) β βπ₯ β (π« π΄ β© Fin)+β = ((β―βπ₯) Β·e π΅)) |
198 | 175, 197 | exlimddv 1939 |
. . . . . . . . . 10
β’ ((Β¬
π΄ β Fin β§ π΅ = +β) β βπ₯ β (π« π΄ β© Fin)+β =
((β―βπ₯)
Β·e π΅)) |
199 | 198 | adantll 713 |
. . . . . . . . 9
β’
((((((π΄ β π β§ π΅ β (0[,]+β)) β§ π¦ β β) β§ π¦ < ((β―βπ΄) Β·e π΅)) β§ Β¬ π΄ β Fin) β§ π΅ = +β) β βπ₯ β (π« π΄ β© Fin)+β =
((β―βπ₯)
Β·e π΅)) |
200 | 50, 116 | elrnmpti 5920 |
. . . . . . . . 9
β’ (+β
β ran (π₯ β
(π« π΄ β© Fin)
β¦ ((β―βπ₯)
Β·e π΅))
β βπ₯ β
(π« π΄ β©
Fin)+β = ((β―βπ₯) Β·e π΅)) |
201 | 199, 200 | sylibr 233 |
. . . . . . . 8
β’
((((((π΄ β π β§ π΅ β (0[,]+β)) β§ π¦ β β) β§ π¦ < ((β―βπ΄) Β·e π΅)) β§ Β¬ π΄ β Fin) β§ π΅ = +β) β +β β ran
(π₯ β (π« π΄ β© Fin) β¦
((β―βπ₯)
Β·e π΅))) |
202 | | simp-4r 783 |
. . . . . . . . 9
β’
((((((π΄ β π β§ π΅ β (0[,]+β)) β§ π¦ β β) β§ π¦ < ((β―βπ΄) Β·e π΅)) β§ Β¬ π΄ β Fin) β§ π΅ = +β) β π¦ β β) |
203 | | ltpnf 13048 |
. . . . . . . . 9
β’ (π¦ β β β π¦ < +β) |
204 | 202, 203 | syl 17 |
. . . . . . . 8
β’
((((((π΄ β π β§ π΅ β (0[,]+β)) β§ π¦ β β) β§ π¦ < ((β―βπ΄) Β·e π΅)) β§ Β¬ π΄ β Fin) β§ π΅ = +β) β π¦ < +β) |
205 | | breq2 5114 |
. . . . . . . . 9
β’ (π§ = +β β (π¦ < π§ β π¦ < +β)) |
206 | 205 | rspcev 3584 |
. . . . . . . 8
β’
((+β β ran (π₯ β (π« π΄ β© Fin) β¦ ((β―βπ₯) Β·e π΅)) β§ π¦ < +β) β βπ§ β ran (π₯ β (π« π΄ β© Fin) β¦ ((β―βπ₯) Β·e π΅))π¦ < π§) |
207 | 201, 204,
206 | syl2anc 585 |
. . . . . . 7
β’
((((((π΄ β π β§ π΅ β (0[,]+β)) β§ π¦ β β) β§ π¦ < ((β―βπ΄) Β·e π΅)) β§ Β¬ π΄ β Fin) β§ π΅ = +β) β βπ§ β ran (π₯ β (π« π΄ β© Fin) β¦ ((β―βπ₯) Β·e π΅))π¦ < π§) |
208 | | simp-4r 783 |
. . . . . . . 8
β’
(((((π΄ β π β§ π΅ β (0[,]+β)) β§ π¦ β β) β§ π¦ < ((β―βπ΄) Β·e π΅)) β§ Β¬ π΄ β Fin) β π΅ β (0[,]+β)) |
209 | | elxrge02 31830 |
. . . . . . . 8
β’ (π΅ β (0[,]+β) β
(π΅ = 0 β¨ π΅ β β+ β¨
π΅ =
+β)) |
210 | 208, 209 | sylib 217 |
. . . . . . 7
β’
(((((π΄ β π β§ π΅ β (0[,]+β)) β§ π¦ β β) β§ π¦ < ((β―βπ΄) Β·e π΅)) β§ Β¬ π΄ β Fin) β (π΅ = 0 β¨ π΅ β β+ β¨ π΅ = +β)) |
211 | 128, 173,
207, 210 | mpjao3dan 1432 |
. . . . . 6
β’
(((((π΄ β π β§ π΅ β (0[,]+β)) β§ π¦ β β) β§ π¦ < ((β―βπ΄) Β·e π΅)) β§ Β¬ π΄ β Fin) β βπ§ β ran (π₯ β (π« π΄ β© Fin) β¦ ((β―βπ₯) Β·e π΅))π¦ < π§) |
212 | 99, 211 | pm2.61dan 812 |
. . . . 5
β’ ((((π΄ β π β§ π΅ β (0[,]+β)) β§ π¦ β β) β§ π¦ < ((β―βπ΄) Β·e π΅)) β βπ§ β ran (π₯ β (π« π΄ β© Fin) β¦ ((β―βπ₯) Β·e π΅))π¦ < π§) |
213 | 212 | ex 414 |
. . . 4
β’ (((π΄ β π β§ π΅ β (0[,]+β)) β§ π¦ β β) β (π¦ < ((β―βπ΄) Β·e π΅) β βπ§ β ran (π₯ β (π« π΄ β© Fin) β¦ ((β―βπ₯) Β·e π΅))π¦ < π§)) |
214 | 213 | ralrimiva 3144 |
. . 3
β’ ((π΄ β π β§ π΅ β (0[,]+β)) β βπ¦ β β (π¦ < ((β―βπ΄) Β·e π΅) β βπ§ β ran (π₯ β (π« π΄ β© Fin) β¦ ((β―βπ₯) Β·e π΅))π¦ < π§)) |
215 | | supxr2 13240 |
. . 3
β’ (((ran
(π₯ β (π« π΄ β© Fin) β¦
((β―βπ₯)
Β·e π΅))
β β* β§ ((β―βπ΄) Β·e π΅) β β*) β§
(βπ¦ β ran
(π₯ β (π« π΄ β© Fin) β¦
((β―βπ₯)
Β·e π΅))π¦ β€ ((β―βπ΄) Β·e π΅) β§ βπ¦ β β (π¦ < ((β―βπ΄) Β·e π΅) β βπ§ β ran (π₯ β (π« π΄ β© Fin) β¦ ((β―βπ₯) Β·e π΅))π¦ < π§))) β sup(ran (π₯ β (π« π΄ β© Fin) β¦ ((β―βπ₯) Β·e π΅)), β*, < )
= ((β―βπ΄)
Β·e π΅)) |
216 | 45, 48, 80, 214, 215 | syl22anc 838 |
. 2
β’ ((π΄ β π β§ π΅ β (0[,]+β)) β sup(ran
(π₯ β (π« π΄ β© Fin) β¦
((β―βπ₯)
Β·e π΅)),
β*, < ) = ((β―βπ΄) Β·e π΅)) |
217 | 25, 216 | eqtrd 2777 |
1
β’ ((π΄ β π β§ π΅ β (0[,]+β)) β
Ξ£*π β
π΄π΅ = ((β―βπ΄) Β·e π΅)) |