Step | Hyp | Ref
| Expression |
1 | | iunin2 5036 |
. . . . 5
β’ βͺ π β β (πΈ β© π΄) = (πΈ β© βͺ
π β β π΄) |
2 | 1 | fveq2i 6850 |
. . . 4
β’ (πββͺ π β β (πΈ β© π΄)) = (πβ(πΈ β© βͺ
π β β π΄)) |
3 | | iccssxr 13354 |
. . . . 5
β’
(0[,]+β) β β* |
4 | | carsgval.2 |
. . . . . 6
β’ (π β π:π« πβΆ(0[,]+β)) |
5 | | nnex 12166 |
. . . . . . . 8
β’ β
β V |
6 | 5 | a1i 11 |
. . . . . . 7
β’ (π β β β
V) |
7 | | carsgclctunlem2.3 |
. . . . . . . . 9
β’ (π β πΈ β π« π) |
8 | 7 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β β) β πΈ β π« π) |
9 | 8 | elpwincl1 31495 |
. . . . . . 7
β’ ((π β§ π β β) β (πΈ β© π΄) β π« π) |
10 | 6, 9 | elpwiuncl 31497 |
. . . . . 6
β’ (π β βͺ π β β (πΈ β© π΄) β π« π) |
11 | 4, 10 | ffvelcdmd 7041 |
. . . . 5
β’ (π β (πββͺ
π β β (πΈ β© π΄)) β (0[,]+β)) |
12 | 3, 11 | sselid 3947 |
. . . 4
β’ (π β (πββͺ
π β β (πΈ β© π΄)) β
β*) |
13 | 2, 12 | eqeltrrid 2843 |
. . 3
β’ (π β (πβ(πΈ β© βͺ
π β β π΄)) β
β*) |
14 | 4, 7 | ffvelcdmd 7041 |
. . . . 5
β’ (π β (πβπΈ) β (0[,]+β)) |
15 | 3, 14 | sselid 3947 |
. . . 4
β’ (π β (πβπΈ) β
β*) |
16 | 7 | elpwdifcl 31496 |
. . . . . . 7
β’ (π β (πΈ β βͺ
π β β π΄) β π« π) |
17 | 4, 16 | ffvelcdmd 7041 |
. . . . . 6
β’ (π β (πβ(πΈ β βͺ
π β β π΄)) β
(0[,]+β)) |
18 | 3, 17 | sselid 3947 |
. . . . 5
β’ (π β (πβ(πΈ β βͺ
π β β π΄)) β
β*) |
19 | 18 | xnegcld 13226 |
. . . 4
β’ (π β
-π(πβ(πΈ β βͺ
π β β π΄)) β
β*) |
20 | 15, 19 | xaddcld 13227 |
. . 3
β’ (π β ((πβπΈ) +π
-π(πβ(πΈ β βͺ
π β β π΄))) β
β*) |
21 | 4 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β β) β π:π« πβΆ(0[,]+β)) |
22 | 21, 9 | ffvelcdmd 7041 |
. . . . . . . 8
β’ ((π β§ π β β) β (πβ(πΈ β© π΄)) β (0[,]+β)) |
23 | 22 | ralrimiva 3144 |
. . . . . . 7
β’ (π β βπ β β (πβ(πΈ β© π΄)) β (0[,]+β)) |
24 | | nfcv 2908 |
. . . . . . . 8
β’
β²πβ |
25 | 24 | esumcl 32669 |
. . . . . . 7
β’ ((β
β V β§ βπ
β β (πβ(πΈ β© π΄)) β (0[,]+β)) β
Ξ£*π β
β(πβ(πΈ β© π΄)) β (0[,]+β)) |
26 | 6, 23, 25 | syl2anc 585 |
. . . . . 6
β’ (π β Ξ£*π β β(πβ(πΈ β© π΄)) β (0[,]+β)) |
27 | 3, 26 | sselid 3947 |
. . . . 5
β’ (π β Ξ£*π β β(πβ(πΈ β© π΄)) β
β*) |
28 | 9 | ralrimiva 3144 |
. . . . . . . . 9
β’ (π β βπ β β (πΈ β© π΄) β π« π) |
29 | | dfiun3g 5924 |
. . . . . . . . 9
β’
(βπ β
β (πΈ β© π΄) β π« π β βͺ π β β (πΈ β© π΄) = βͺ ran (π β β β¦ (πΈ β© π΄))) |
30 | 28, 29 | syl 17 |
. . . . . . . 8
β’ (π β βͺ π β β (πΈ β© π΄) = βͺ ran (π β β β¦ (πΈ β© π΄))) |
31 | 30 | fveq2d 6851 |
. . . . . . 7
β’ (π β (πββͺ
π β β (πΈ β© π΄)) = (πββͺ ran
(π β β β¦
(πΈ β© π΄)))) |
32 | | nnct 13893 |
. . . . . . . . . 10
β’ β
βΌ Ο |
33 | | mptct 10481 |
. . . . . . . . . 10
β’ (β
βΌ Ο β (π
β β β¦ (πΈ
β© π΄)) βΌ
Ο) |
34 | | rnct 10468 |
. . . . . . . . . 10
β’ ((π β β β¦ (πΈ β© π΄)) βΌ Ο β ran (π β β β¦ (πΈ β© π΄)) βΌ Ο) |
35 | 32, 33, 34 | mp2b 10 |
. . . . . . . . 9
β’ ran
(π β β β¦
(πΈ β© π΄)) βΌ Ο |
36 | 35 | a1i 11 |
. . . . . . . 8
β’ (π β ran (π β β β¦ (πΈ β© π΄)) βΌ Ο) |
37 | | eqid 2737 |
. . . . . . . . . 10
β’ (π β β β¦ (πΈ β© π΄)) = (π β β β¦ (πΈ β© π΄)) |
38 | 37 | rnmptss 7075 |
. . . . . . . . 9
β’
(βπ β
β (πΈ β© π΄) β π« π β ran (π β β β¦ (πΈ β© π΄)) β π« π) |
39 | 28, 38 | syl 17 |
. . . . . . . 8
β’ (π β ran (π β β β¦ (πΈ β© π΄)) β π« π) |
40 | | mptexg 7176 |
. . . . . . . . . 10
β’ (β
β V β (π β
β β¦ (πΈ β©
π΄)) β
V) |
41 | | rnexg 7846 |
. . . . . . . . . 10
β’ ((π β β β¦ (πΈ β© π΄)) β V β ran (π β β β¦ (πΈ β© π΄)) β V) |
42 | 5, 40, 41 | mp2b 10 |
. . . . . . . . 9
β’ ran
(π β β β¦
(πΈ β© π΄)) β V |
43 | | breq1 5113 |
. . . . . . . . . . . 12
β’ (π₯ = ran (π β β β¦ (πΈ β© π΄)) β (π₯ βΌ Ο β ran (π β β β¦ (πΈ β© π΄)) βΌ Ο)) |
44 | | sseq1 3974 |
. . . . . . . . . . . 12
β’ (π₯ = ran (π β β β¦ (πΈ β© π΄)) β (π₯ β π« π β ran (π β β β¦ (πΈ β© π΄)) β π« π)) |
45 | 43, 44 | 3anbi23d 1440 |
. . . . . . . . . . 11
β’ (π₯ = ran (π β β β¦ (πΈ β© π΄)) β ((π β§ π₯ βΌ Ο β§ π₯ β π« π) β (π β§ ran (π β β β¦ (πΈ β© π΄)) βΌ Ο β§ ran (π β β β¦ (πΈ β© π΄)) β π« π))) |
46 | | unieq 4881 |
. . . . . . . . . . . . 13
β’ (π₯ = ran (π β β β¦ (πΈ β© π΄)) β βͺ π₯ = βͺ
ran (π β β
β¦ (πΈ β© π΄))) |
47 | 46 | fveq2d 6851 |
. . . . . . . . . . . 12
β’ (π₯ = ran (π β β β¦ (πΈ β© π΄)) β (πββͺ π₯) = (πββͺ ran
(π β β β¦
(πΈ β© π΄)))) |
48 | | esumeq1 32673 |
. . . . . . . . . . . 12
β’ (π₯ = ran (π β β β¦ (πΈ β© π΄)) β Ξ£*π¦ β π₯(πβπ¦) = Ξ£*π¦ β ran (π β β β¦ (πΈ β© π΄))(πβπ¦)) |
49 | 47, 48 | breq12d 5123 |
. . . . . . . . . . 11
β’ (π₯ = ran (π β β β¦ (πΈ β© π΄)) β ((πββͺ π₯) β€ Ξ£*π¦ β π₯(πβπ¦) β (πββͺ ran
(π β β β¦
(πΈ β© π΄))) β€ Ξ£*π¦ β ran (π β β β¦ (πΈ β© π΄))(πβπ¦))) |
50 | 45, 49 | imbi12d 345 |
. . . . . . . . . 10
β’ (π₯ = ran (π β β β¦ (πΈ β© π΄)) β (((π β§ π₯ βΌ Ο β§ π₯ β π« π) β (πββͺ π₯) β€ Ξ£*π¦ β π₯(πβπ¦)) β ((π β§ ran (π β β β¦ (πΈ β© π΄)) βΌ Ο β§ ran (π β β β¦ (πΈ β© π΄)) β π« π) β (πββͺ ran
(π β β β¦
(πΈ β© π΄))) β€ Ξ£*π¦ β ran (π β β β¦ (πΈ β© π΄))(πβπ¦)))) |
51 | | carsgsiga.2 |
. . . . . . . . . 10
β’ ((π β§ π₯ βΌ Ο β§ π₯ β π« π) β (πββͺ π₯) β€ Ξ£*π¦ β π₯(πβπ¦)) |
52 | 50, 51 | vtoclg 3528 |
. . . . . . . . 9
β’ (ran
(π β β β¦
(πΈ β© π΄)) β V β ((π β§ ran (π β β β¦ (πΈ β© π΄)) βΌ Ο β§ ran (π β β β¦ (πΈ β© π΄)) β π« π) β (πββͺ ran
(π β β β¦
(πΈ β© π΄))) β€ Ξ£*π¦ β ran (π β β β¦ (πΈ β© π΄))(πβπ¦))) |
53 | 42, 52 | ax-mp 5 |
. . . . . . . 8
β’ ((π β§ ran (π β β β¦ (πΈ β© π΄)) βΌ Ο β§ ran (π β β β¦ (πΈ β© π΄)) β π« π) β (πββͺ ran
(π β β β¦
(πΈ β© π΄))) β€ Ξ£*π¦ β ran (π β β β¦ (πΈ β© π΄))(πβπ¦)) |
54 | 36, 39, 53 | mpd3an23 1464 |
. . . . . . 7
β’ (π β (πββͺ ran
(π β β β¦
(πΈ β© π΄))) β€ Ξ£*π¦ β ran (π β β β¦ (πΈ β© π΄))(πβπ¦)) |
55 | 31, 54 | eqbrtrd 5132 |
. . . . . 6
β’ (π β (πββͺ
π β β (πΈ β© π΄)) β€ Ξ£*π¦ β ran (π β β β¦ (πΈ β© π΄))(πβπ¦)) |
56 | | fveq2 6847 |
. . . . . . 7
β’ (π¦ = (πΈ β© π΄) β (πβπ¦) = (πβ(πΈ β© π΄))) |
57 | | simpr 486 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ (πΈ β© π΄) = β
) β (πΈ β© π΄) = β
) |
58 | 57 | fveq2d 6851 |
. . . . . . . 8
β’ (((π β§ π β β) β§ (πΈ β© π΄) = β
) β (πβ(πΈ β© π΄)) = (πββ
)) |
59 | | carsgsiga.1 |
. . . . . . . . 9
β’ (π β (πββ
) = 0) |
60 | 59 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π β β) β§ (πΈ β© π΄) = β
) β (πββ
) = 0) |
61 | 58, 60 | eqtrd 2777 |
. . . . . . 7
β’ (((π β§ π β β) β§ (πΈ β© π΄) = β
) β (πβ(πΈ β© π΄)) = 0) |
62 | | carsgclctunlem2.1 |
. . . . . . . . 9
β’ (π β Disj π β β π΄) |
63 | | disjin 31546 |
. . . . . . . . 9
β’
(Disj π
β β π΄ β
Disj π β
β (π΄ β© πΈ)) |
64 | 62, 63 | syl 17 |
. . . . . . . 8
β’ (π β Disj π β β (π΄ β© πΈ)) |
65 | | incom 4166 |
. . . . . . . . . 10
β’ (π΄ β© πΈ) = (πΈ β© π΄) |
66 | 65 | rgenw 3069 |
. . . . . . . . 9
β’
βπ β
β (π΄ β© πΈ) = (πΈ β© π΄) |
67 | | disjeq2 5079 |
. . . . . . . . 9
β’
(βπ β
β (π΄ β© πΈ) = (πΈ β© π΄) β (Disj π β β (π΄ β© πΈ) β Disj π β β (πΈ β© π΄))) |
68 | 66, 67 | ax-mp 5 |
. . . . . . . 8
β’
(Disj π
β β (π΄ β©
πΈ) β Disj π β β (πΈ β© π΄)) |
69 | 64, 68 | sylib 217 |
. . . . . . 7
β’ (π β Disj π β β (πΈ β© π΄)) |
70 | 56, 6, 22, 9, 61, 69 | esumrnmpt2 32707 |
. . . . . 6
β’ (π β Ξ£*π¦ β ran (π β β β¦ (πΈ β© π΄))(πβπ¦) = Ξ£*π β β(πβ(πΈ β© π΄))) |
71 | 55, 70 | breqtrd 5136 |
. . . . 5
β’ (π β (πββͺ
π β β (πΈ β© π΄)) β€ Ξ£*π β β(πβ(πΈ β© π΄))) |
72 | | carsgval.1 |
. . . . . . . 8
β’ (π β π β π) |
73 | | difssd 4097 |
. . . . . . . 8
β’ (π β (πΈ β βͺ
π β β π΄) β πΈ) |
74 | | carsgsiga.3 |
. . . . . . . 8
β’ ((π β§ π₯ β π¦ β§ π¦ β π« π) β (πβπ₯) β€ (πβπ¦)) |
75 | 72, 4, 73, 7, 74 | carsgmon 32954 |
. . . . . . 7
β’ (π β (πβ(πΈ β βͺ
π β β π΄)) β€ (πβπΈ)) |
76 | 14, 17, 75 | xrge0subcld 31710 |
. . . . . 6
β’ (π β ((πβπΈ) +π
-π(πβ(πΈ β βͺ
π β β π΄))) β
(0[,]+β)) |
77 | 4 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β π:π« πβΆ(0[,]+β)) |
78 | 7 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β πΈ β π« π) |
79 | 78 | elpwincl1 31495 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (πΈ β© βͺ
π β (1...π)π΄) β π« π) |
80 | 77, 79 | ffvelcdmd 7041 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (πβ(πΈ β© βͺ
π β (1...π)π΄)) β (0[,]+β)) |
81 | 3, 80 | sselid 3947 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (πβ(πΈ β© βͺ
π β (1...π)π΄)) β
β*) |
82 | | xrge0neqmnf 13376 |
. . . . . . . . . . 11
β’ ((πβ(πΈ β© βͺ
π β (1...π)π΄)) β (0[,]+β) β (πβ(πΈ β© βͺ
π β (1...π)π΄)) β -β) |
83 | 80, 82 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (πβ(πΈ β© βͺ
π β (1...π)π΄)) β -β) |
84 | 78 | elpwdifcl 31496 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (πΈ β βͺ
π β (1...π)π΄) β π« π) |
85 | 77, 84 | ffvelcdmd 7041 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (πβ(πΈ β βͺ
π β (1...π)π΄)) β (0[,]+β)) |
86 | 3, 85 | sselid 3947 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (πβ(πΈ β βͺ
π β (1...π)π΄)) β
β*) |
87 | | xrge0neqmnf 13376 |
. . . . . . . . . . 11
β’ ((πβ(πΈ β βͺ
π β (1...π)π΄)) β (0[,]+β) β (πβ(πΈ β βͺ
π β (1...π)π΄)) β -β) |
88 | 85, 87 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (πβ(πΈ β βͺ
π β (1...π)π΄)) β -β) |
89 | 86 | xnegcld 13226 |
. . . . . . . . . 10
β’ ((π β§ π β β) β
-π(πβ(πΈ β βͺ
π β (1...π)π΄)) β
β*) |
90 | | xnegneg 13140 |
. . . . . . . . . . . . . . . . 17
β’ ((πβ(πΈ β βͺ
π β (1...π)π΄)) β β* β
-π-π(πβ(πΈ β βͺ
π β (1...π)π΄)) = (πβ(πΈ β βͺ
π β (1...π)π΄))) |
91 | 86, 90 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β
-π-π(πβ(πΈ β βͺ
π β (1...π)π΄)) = (πβ(πΈ β βͺ
π β (1...π)π΄))) |
92 | 91 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β) β§
-π(πβ(πΈ β βͺ
π β (1...π)π΄)) = -β) β
-π-π(πβ(πΈ β βͺ
π β (1...π)π΄)) = (πβ(πΈ β βͺ
π β (1...π)π΄))) |
93 | | xnegeq 13133 |
. . . . . . . . . . . . . . . . 17
β’
(-π(πβ(πΈ β βͺ
π β (1...π)π΄)) = -β β
-π-π(πβ(πΈ β βͺ
π β (1...π)π΄)) =
-π-β) |
94 | 93 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β) β§
-π(πβ(πΈ β βͺ
π β (1...π)π΄)) = -β) β
-π-π(πβ(πΈ β βͺ
π β (1...π)π΄)) =
-π-β) |
95 | | xnegmnf 13136 |
. . . . . . . . . . . . . . . 16
β’
-π-β = +β |
96 | 94, 95 | eqtrdi 2793 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β) β§
-π(πβ(πΈ β βͺ
π β (1...π)π΄)) = -β) β
-π-π(πβ(πΈ β βͺ
π β (1...π)π΄)) = +β) |
97 | 92, 96 | eqtr3d 2779 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β) β§
-π(πβ(πΈ β βͺ
π β (1...π)π΄)) = -β) β (πβ(πΈ β βͺ
π β (1...π)π΄)) = +β) |
98 | 97 | oveq2d 7378 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β) β§
-π(πβ(πΈ β βͺ
π β (1...π)π΄)) = -β) β ((πβ(πΈ β© βͺ
π β (1...π)π΄)) +π (πβ(πΈ β βͺ
π β (1...π)π΄))) = ((πβ(πΈ β© βͺ
π β (1...π)π΄)) +π
+β)) |
99 | | simpll 766 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β β) β§ π β (1...π)) β π) |
100 | | fz1ssnn 13479 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(1...π) β
β |
101 | 100 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β β) β (1...π) β
β) |
102 | 101 | sselda 3949 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β β) β§ π β (1...π)) β π β β) |
103 | | carsgclctunlem2.2 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β β) β π΄ β (toCaraSigaβπ)) |
104 | 99, 102, 103 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β β) β§ π β (1...π)) β π΄ β (toCaraSigaβπ)) |
105 | 104 | ralrimiva 3144 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β β) β βπ β (1...π)π΄ β (toCaraSigaβπ)) |
106 | | dfiun3g 5924 |
. . . . . . . . . . . . . . . . . . 19
β’
(βπ β
(1...π)π΄ β (toCaraSigaβπ) β βͺ
π β (1...π)π΄ = βͺ ran (π β (1...π) β¦ π΄)) |
107 | 105, 106 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β β) β βͺ π β (1...π)π΄ = βͺ ran (π β (1...π) β¦ π΄)) |
108 | 72 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β β) β π β π) |
109 | 59 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β β) β (πββ
) = 0) |
110 | 51 | 3adant1r 1178 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β β) β§ π₯ βΌ Ο β§ π₯ β π« π) β (πββͺ π₯) β€ Ξ£*π¦ β π₯(πβπ¦)) |
111 | | fzfi 13884 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(1...π) β
Fin |
112 | | mptfi 9302 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((1...π) β Fin
β (π β (1...π) β¦ π΄) β Fin) |
113 | | rnfi 9286 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β (1...π) β¦ π΄) β Fin β ran (π β (1...π) β¦ π΄) β Fin) |
114 | 111, 112,
113 | mp2b 10 |
. . . . . . . . . . . . . . . . . . . 20
β’ ran
(π β (1...π) β¦ π΄) β Fin |
115 | 114 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β β) β ran (π β (1...π) β¦ π΄) β Fin) |
116 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (1...π) β¦ π΄) = (π β (1...π) β¦ π΄) |
117 | 116 | rnmptss 7075 |
. . . . . . . . . . . . . . . . . . . 20
β’
(βπ β
(1...π)π΄ β (toCaraSigaβπ) β ran (π β (1...π) β¦ π΄) β (toCaraSigaβπ)) |
118 | 105, 117 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β β) β ran (π β (1...π) β¦ π΄) β (toCaraSigaβπ)) |
119 | 108, 77, 109, 110, 115, 118 | fiunelcarsg 32956 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β β) β βͺ ran (π β (1...π) β¦ π΄) β (toCaraSigaβπ)) |
120 | 107, 119 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β) β βͺ π β (1...π)π΄ β (toCaraSigaβπ)) |
121 | 108, 77 | elcarsg 32945 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β) β (βͺ π β (1...π)π΄ β (toCaraSigaβπ) β (βͺ π β (1...π)π΄ β π β§ βπ β π« π((πβ(π β© βͺ
π β (1...π)π΄)) +π (πβ(π β βͺ
π β (1...π)π΄))) = (πβπ)))) |
122 | 120, 121 | mpbid 231 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β (βͺ π β (1...π)π΄ β π β§ βπ β π« π((πβ(π β© βͺ
π β (1...π)π΄)) +π (πβ(π β βͺ
π β (1...π)π΄))) = (πβπ))) |
123 | 122 | simprd 497 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β βπ β π« π((πβ(π β© βͺ
π β (1...π)π΄)) +π (πβ(π β βͺ
π β (1...π)π΄))) = (πβπ)) |
124 | | ineq1 4170 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = πΈ β (π β© βͺ
π β (1...π)π΄) = (πΈ β© βͺ
π β (1...π)π΄)) |
125 | 124 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . 18
β’ (π = πΈ β (πβ(π β© βͺ
π β (1...π)π΄)) = (πβ(πΈ β© βͺ
π β (1...π)π΄))) |
126 | | difeq1 4080 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = πΈ β (π β βͺ
π β (1...π)π΄) = (πΈ β βͺ
π β (1...π)π΄)) |
127 | 126 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . 18
β’ (π = πΈ β (πβ(π β βͺ
π β (1...π)π΄)) = (πβ(πΈ β βͺ
π β (1...π)π΄))) |
128 | 125, 127 | oveq12d 7380 |
. . . . . . . . . . . . . . . . 17
β’ (π = πΈ β ((πβ(π β© βͺ
π β (1...π)π΄)) +π (πβ(π β βͺ
π β (1...π)π΄))) = ((πβ(πΈ β© βͺ
π β (1...π)π΄)) +π (πβ(πΈ β βͺ
π β (1...π)π΄)))) |
129 | | fveq2 6847 |
. . . . . . . . . . . . . . . . 17
β’ (π = πΈ β (πβπ) = (πβπΈ)) |
130 | 128, 129 | eqeq12d 2753 |
. . . . . . . . . . . . . . . 16
β’ (π = πΈ β (((πβ(π β© βͺ
π β (1...π)π΄)) +π (πβ(π β βͺ
π β (1...π)π΄))) = (πβπ) β ((πβ(πΈ β© βͺ
π β (1...π)π΄)) +π (πβ(πΈ β βͺ
π β (1...π)π΄))) = (πβπΈ))) |
131 | 130 | rspcv 3580 |
. . . . . . . . . . . . . . 15
β’ (πΈ β π« π β (βπ β π« π((πβ(π β© βͺ
π β (1...π)π΄)) +π (πβ(π β βͺ
π β (1...π)π΄))) = (πβπ) β ((πβ(πΈ β© βͺ
π β (1...π)π΄)) +π (πβ(πΈ β βͺ
π β (1...π)π΄))) = (πβπΈ))) |
132 | 78, 123, 131 | sylc 65 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β ((πβ(πΈ β© βͺ
π β (1...π)π΄)) +π (πβ(πΈ β βͺ
π β (1...π)π΄))) = (πβπΈ)) |
133 | 132 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β) β§
-π(πβ(πΈ β βͺ
π β (1...π)π΄)) = -β) β ((πβ(πΈ β© βͺ
π β (1...π)π΄)) +π (πβ(πΈ β βͺ
π β (1...π)π΄))) = (πβπΈ)) |
134 | | xaddpnf1 13152 |
. . . . . . . . . . . . . . 15
β’ (((πβ(πΈ β© βͺ
π β (1...π)π΄)) β β* β§ (πβ(πΈ β© βͺ
π β (1...π)π΄)) β -β) β ((πβ(πΈ β© βͺ
π β (1...π)π΄)) +π +β) =
+β) |
135 | 81, 83, 134 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β ((πβ(πΈ β© βͺ
π β (1...π)π΄)) +π +β) =
+β) |
136 | 135 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β) β§
-π(πβ(πΈ β βͺ
π β (1...π)π΄)) = -β) β ((πβ(πΈ β© βͺ
π β (1...π)π΄)) +π +β) =
+β) |
137 | 98, 133, 136 | 3eqtr3d 2785 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§
-π(πβ(πΈ β βͺ
π β (1...π)π΄)) = -β) β (πβπΈ) = +β) |
138 | | carsgclctunlem2.4 |
. . . . . . . . . . . . . 14
β’ (π β (πβπΈ) β +β) |
139 | 138 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β) β§
-π(πβ(πΈ β βͺ
π β (1...π)π΄)) = -β) β (πβπΈ) β +β) |
140 | 139 | neneqd 2949 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§
-π(πβ(πΈ β βͺ
π β (1...π)π΄)) = -β) β Β¬ (πβπΈ) = +β) |
141 | 137, 140 | pm2.65da 816 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β Β¬
-π(πβ(πΈ β βͺ
π β (1...π)π΄)) = -β) |
142 | 141 | neqned 2951 |
. . . . . . . . . 10
β’ ((π β§ π β β) β
-π(πβ(πΈ β βͺ
π β (1...π)π΄)) β -β) |
143 | | xaddass 13175 |
. . . . . . . . . 10
β’ ((((πβ(πΈ β© βͺ
π β (1...π)π΄)) β β* β§ (πβ(πΈ β© βͺ
π β (1...π)π΄)) β -β) β§ ((πβ(πΈ β βͺ
π β (1...π)π΄)) β β* β§ (πβ(πΈ β βͺ
π β (1...π)π΄)) β -β) β§
(-π(πβ(πΈ β βͺ
π β (1...π)π΄)) β β* β§
-π(πβ(πΈ β βͺ
π β (1...π)π΄)) β -β)) β (((πβ(πΈ β© βͺ
π β (1...π)π΄)) +π (πβ(πΈ β βͺ
π β (1...π)π΄))) +π
-π(πβ(πΈ β βͺ
π β (1...π)π΄))) = ((πβ(πΈ β© βͺ
π β (1...π)π΄)) +π ((πβ(πΈ β βͺ
π β (1...π)π΄)) +π
-π(πβ(πΈ β βͺ
π β (1...π)π΄))))) |
144 | 81, 83, 86, 88, 89, 142, 143 | syl222anc 1387 |
. . . . . . . . 9
β’ ((π β§ π β β) β (((πβ(πΈ β© βͺ
π β (1...π)π΄)) +π (πβ(πΈ β βͺ
π β (1...π)π΄))) +π
-π(πβ(πΈ β βͺ
π β (1...π)π΄))) = ((πβ(πΈ β© βͺ
π β (1...π)π΄)) +π ((πβ(πΈ β βͺ
π β (1...π)π΄)) +π
-π(πβ(πΈ β βͺ
π β (1...π)π΄))))) |
145 | | xnegid 13164 |
. . . . . . . . . . 11
β’ ((πβ(πΈ β βͺ
π β (1...π)π΄)) β β* β ((πβ(πΈ β βͺ
π β (1...π)π΄)) +π
-π(πβ(πΈ β βͺ
π β (1...π)π΄))) = 0) |
146 | 86, 145 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π β β) β ((πβ(πΈ β βͺ
π β (1...π)π΄)) +π
-π(πβ(πΈ β βͺ
π β (1...π)π΄))) = 0) |
147 | 146 | oveq2d 7378 |
. . . . . . . . 9
β’ ((π β§ π β β) β ((πβ(πΈ β© βͺ
π β (1...π)π΄)) +π ((πβ(πΈ β βͺ
π β (1...π)π΄)) +π
-π(πβ(πΈ β βͺ
π β (1...π)π΄)))) = ((πβ(πΈ β© βͺ
π β (1...π)π΄)) +π
0)) |
148 | | xaddid1 13167 |
. . . . . . . . . 10
β’ ((πβ(πΈ β© βͺ
π β (1...π)π΄)) β β* β ((πβ(πΈ β© βͺ
π β (1...π)π΄)) +π 0) = (πβ(πΈ β© βͺ
π β (1...π)π΄))) |
149 | 81, 148 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π β β) β ((πβ(πΈ β© βͺ
π β (1...π)π΄)) +π 0) = (πβ(πΈ β© βͺ
π β (1...π)π΄))) |
150 | 144, 147,
149 | 3eqtrd 2781 |
. . . . . . . 8
β’ ((π β§ π β β) β (((πβ(πΈ β© βͺ
π β (1...π)π΄)) +π (πβ(πΈ β βͺ
π β (1...π)π΄))) +π
-π(πβ(πΈ β βͺ
π β (1...π)π΄))) = (πβ(πΈ β© βͺ
π β (1...π)π΄))) |
151 | 132 | oveq1d 7377 |
. . . . . . . 8
β’ ((π β§ π β β) β (((πβ(πΈ β© βͺ
π β (1...π)π΄)) +π (πβ(πΈ β βͺ
π β (1...π)π΄))) +π
-π(πβ(πΈ β βͺ
π β (1...π)π΄))) = ((πβπΈ) +π
-π(πβ(πΈ β βͺ
π β (1...π)π΄)))) |
152 | 107 | ineq2d 4177 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (πΈ β© βͺ
π β (1...π)π΄) = (πΈ β© βͺ ran
(π β (1...π) β¦ π΄))) |
153 | 152 | fveq2d 6851 |
. . . . . . . . 9
β’ ((π β§ π β β) β (πβ(πΈ β© βͺ
π β (1...π)π΄)) = (πβ(πΈ β© βͺ ran
(π β (1...π) β¦ π΄)))) |
154 | | mptss 6001 |
. . . . . . . . . . . . 13
β’
((1...π) β
β β (π β
(1...π) β¦ π΄) β (π β β β¦ π΄)) |
155 | | rnss 5899 |
. . . . . . . . . . . . 13
β’ ((π β (1...π) β¦ π΄) β (π β β β¦ π΄) β ran (π β (1...π) β¦ π΄) β ran (π β β β¦ π΄)) |
156 | 100, 154,
155 | mp2b 10 |
. . . . . . . . . . . 12
β’ ran
(π β (1...π) β¦ π΄) β ran (π β β β¦ π΄) |
157 | 156 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β ran (π β (1...π) β¦ π΄) β ran (π β β β¦ π΄)) |
158 | | disjrnmpt 31545 |
. . . . . . . . . . . . 13
β’
(Disj π
β β π΄ β
Disj π¦ β ran
(π β β β¦
π΄)π¦) |
159 | 62, 158 | syl 17 |
. . . . . . . . . . . 12
β’ (π β Disj π¦ β ran (π β β β¦ π΄)π¦) |
160 | 159 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β Disj π¦ β ran (π β β β¦ π΄)π¦) |
161 | | disjss1 5081 |
. . . . . . . . . . 11
β’ (ran
(π β (1...π) β¦ π΄) β ran (π β β β¦ π΄) β (Disj π¦ β ran (π β β β¦ π΄)π¦ β Disj π¦ β ran (π β (1...π) β¦ π΄)π¦)) |
162 | 157, 160,
161 | sylc 65 |
. . . . . . . . . 10
β’ ((π β§ π β β) β Disj π¦ β ran (π β (1...π) β¦ π΄)π¦) |
163 | 108, 77, 109, 110, 115, 118, 162, 78 | carsgclctunlem1 32957 |
. . . . . . . . 9
β’ ((π β§ π β β) β (πβ(πΈ β© βͺ ran
(π β (1...π) β¦ π΄))) = Ξ£*π¦ β ran (π β (1...π) β¦ π΄)(πβ(πΈ β© π¦))) |
164 | | ineq2 4171 |
. . . . . . . . . . 11
β’ (π¦ = π΄ β (πΈ β© π¦) = (πΈ β© π΄)) |
165 | 164 | fveq2d 6851 |
. . . . . . . . . 10
β’ (π¦ = π΄ β (πβ(πΈ β© π¦)) = (πβ(πΈ β© π΄))) |
166 | 111 | elexi 3467 |
. . . . . . . . . . 11
β’
(1...π) β
V |
167 | 166 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (1...π) β V) |
168 | 99, 102, 22 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β (1...π)) β (πβ(πΈ β© π΄)) β (0[,]+β)) |
169 | | inss2 4194 |
. . . . . . . . . . . . . . 15
β’ (πΈ β© π΄) β π΄ |
170 | | sseq2 3975 |
. . . . . . . . . . . . . . 15
β’ (π΄ = β
β ((πΈ β© π΄) β π΄ β (πΈ β© π΄) β β
)) |
171 | 169, 170 | mpbii 232 |
. . . . . . . . . . . . . 14
β’ (π΄ = β
β (πΈ β© π΄) β β
) |
172 | | ss0 4363 |
. . . . . . . . . . . . . 14
β’ ((πΈ β© π΄) β β
β (πΈ β© π΄) = β
) |
173 | 171, 172 | syl 17 |
. . . . . . . . . . . . 13
β’ (π΄ = β
β (πΈ β© π΄) = β
) |
174 | 173 | adantl 483 |
. . . . . . . . . . . 12
β’ ((((π β§ π β β) β§ π β (1...π)) β§ π΄ = β
) β (πΈ β© π΄) = β
) |
175 | 174 | fveq2d 6851 |
. . . . . . . . . . 11
β’ ((((π β§ π β β) β§ π β (1...π)) β§ π΄ = β
) β (πβ(πΈ β© π΄)) = (πββ
)) |
176 | 109 | ad2antrr 725 |
. . . . . . . . . . 11
β’ ((((π β§ π β β) β§ π β (1...π)) β§ π΄ = β
) β (πββ
) = 0) |
177 | 175, 176 | eqtrd 2777 |
. . . . . . . . . 10
β’ ((((π β§ π β β) β§ π β (1...π)) β§ π΄ = β
) β (πβ(πΈ β© π΄)) = 0) |
178 | 62 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β Disj π β β π΄) |
179 | | disjss1 5081 |
. . . . . . . . . . 11
β’
((1...π) β
β β (Disj π β β π΄ β Disj π β (1...π)π΄)) |
180 | 101, 178,
179 | sylc 65 |
. . . . . . . . . 10
β’ ((π β§ π β β) β Disj π β (1...π)π΄) |
181 | 165, 167,
168, 104, 177, 180 | esumrnmpt2 32707 |
. . . . . . . . 9
β’ ((π β§ π β β) β
Ξ£*π¦ β
ran (π β (1...π) β¦ π΄)(πβ(πΈ β© π¦)) = Ξ£*π β (1...π)(πβ(πΈ β© π΄))) |
182 | 153, 163,
181 | 3eqtrd 2781 |
. . . . . . . 8
β’ ((π β§ π β β) β (πβ(πΈ β© βͺ
π β (1...π)π΄)) = Ξ£*π β (1...π)(πβ(πΈ β© π΄))) |
183 | 150, 151,
182 | 3eqtr3rd 2786 |
. . . . . . 7
β’ ((π β§ π β β) β
Ξ£*π β
(1...π)(πβ(πΈ β© π΄)) = ((πβπΈ) +π
-π(πβ(πΈ β βͺ
π β (1...π)π΄)))) |
184 | 17 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (πβ(πΈ β βͺ
π β β π΄)) β
(0[,]+β)) |
185 | 3, 184 | sselid 3947 |
. . . . . . . . 9
β’ ((π β§ π β β) β (πβ(πΈ β βͺ
π β β π΄)) β
β*) |
186 | 185 | xnegcld 13226 |
. . . . . . . 8
β’ ((π β§ π β β) β
-π(πβ(πΈ β βͺ
π β β π΄)) β
β*) |
187 | 15 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β β) β (πβπΈ) β
β*) |
188 | | iunss1 4973 |
. . . . . . . . . . . 12
β’
((1...π) β
β β βͺ π β (1...π)π΄ β βͺ
π β β π΄) |
189 | 100, 188 | mp1i 13 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β βͺ π β (1...π)π΄ β βͺ
π β β π΄) |
190 | 189 | sscond 4106 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (πΈ β βͺ
π β β π΄) β (πΈ β βͺ
π β (1...π)π΄)) |
191 | 74 | 3adant1r 1178 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π₯ β π¦ β§ π¦ β π« π) β (πβπ₯) β€ (πβπ¦)) |
192 | 108, 77, 190, 84, 191 | carsgmon 32954 |
. . . . . . . . 9
β’ ((π β§ π β β) β (πβ(πΈ β βͺ
π β β π΄)) β€ (πβ(πΈ β βͺ
π β (1...π)π΄))) |
193 | | xleneg 13144 |
. . . . . . . . . 10
β’ (((πβ(πΈ β βͺ
π β β π΄)) β β*
β§ (πβ(πΈ β βͺ π β (1...π)π΄)) β β*) β
((πβ(πΈ β βͺ π β β π΄)) β€ (πβ(πΈ β βͺ
π β (1...π)π΄)) β -π(πβ(πΈ β βͺ
π β (1...π)π΄)) β€ -π(πβ(πΈ β βͺ
π β β π΄)))) |
194 | 193 | biimpa 478 |
. . . . . . . . 9
β’ ((((πβ(πΈ β βͺ
π β β π΄)) β β*
β§ (πβ(πΈ β βͺ π β (1...π)π΄)) β β*) β§ (πβ(πΈ β βͺ
π β β π΄)) β€ (πβ(πΈ β βͺ
π β (1...π)π΄))) β -π(πβ(πΈ β βͺ
π β (1...π)π΄)) β€ -π(πβ(πΈ β βͺ
π β β π΄))) |
195 | 185, 86, 192, 194 | syl21anc 837 |
. . . . . . . 8
β’ ((π β§ π β β) β
-π(πβ(πΈ β βͺ
π β (1...π)π΄)) β€ -π(πβ(πΈ β βͺ
π β β π΄))) |
196 | | xleadd2a 13180 |
. . . . . . . 8
β’
(((-π(πβ(πΈ β βͺ
π β (1...π)π΄)) β β* β§
-π(πβ(πΈ β βͺ
π β β π΄)) β β*
β§ (πβπΈ) β β*)
β§ -π(πβ(πΈ β βͺ
π β (1...π)π΄)) β€ -π(πβ(πΈ β βͺ
π β β π΄))) β ((πβπΈ) +π
-π(πβ(πΈ β βͺ
π β (1...π)π΄))) β€ ((πβπΈ) +π
-π(πβ(πΈ β βͺ
π β β π΄)))) |
197 | 89, 186, 187, 195, 196 | syl31anc 1374 |
. . . . . . 7
β’ ((π β§ π β β) β ((πβπΈ) +π
-π(πβ(πΈ β βͺ
π β (1...π)π΄))) β€ ((πβπΈ) +π
-π(πβ(πΈ β βͺ
π β β π΄)))) |
198 | 183, 197 | eqbrtrd 5132 |
. . . . . 6
β’ ((π β§ π β β) β
Ξ£*π β
(1...π)(πβ(πΈ β© π΄)) β€ ((πβπΈ) +π
-π(πβ(πΈ β βͺ
π β β π΄)))) |
199 | 76, 22, 198 | esumgect 32729 |
. . . . 5
β’ (π β Ξ£*π β β(πβ(πΈ β© π΄)) β€ ((πβπΈ) +π
-π(πβ(πΈ β βͺ
π β β π΄)))) |
200 | 12, 27, 20, 71, 199 | xrletrd 13088 |
. . . 4
β’ (π β (πββͺ
π β β (πΈ β© π΄)) β€ ((πβπΈ) +π
-π(πβ(πΈ β βͺ
π β β π΄)))) |
201 | 2, 200 | eqbrtrrid 5146 |
. . 3
β’ (π β (πβ(πΈ β© βͺ
π β β π΄)) β€ ((πβπΈ) +π
-π(πβ(πΈ β βͺ
π β β π΄)))) |
202 | | xleadd1a 13179 |
. . 3
β’ ((((πβ(πΈ β© βͺ
π β β π΄)) β β*
β§ ((πβπΈ) +π
-π(πβ(πΈ β βͺ
π β β π΄))) β β*
β§ (πβ(πΈ β βͺ π β β π΄)) β β*) β§ (πβ(πΈ β© βͺ
π β β π΄)) β€ ((πβπΈ) +π
-π(πβ(πΈ β βͺ
π β β π΄)))) β ((πβ(πΈ β© βͺ
π β β π΄)) +π (πβ(πΈ β βͺ
π β β π΄))) β€ (((πβπΈ) +π
-π(πβ(πΈ β βͺ
π β β π΄))) +π (πβ(πΈ β βͺ
π β β π΄)))) |
203 | 13, 20, 18, 201, 202 | syl31anc 1374 |
. 2
β’ (π β ((πβ(πΈ β© βͺ
π β β π΄)) +π (πβ(πΈ β βͺ
π β β π΄))) β€ (((πβπΈ) +π
-π(πβ(πΈ β βͺ
π β β π΄))) +π (πβ(πΈ β βͺ
π β β π΄)))) |
204 | | xrge0npcan 31927 |
. . 3
β’ (((πβπΈ) β (0[,]+β) β§ (πβ(πΈ β βͺ
π β β π΄)) β (0[,]+β) β§
(πβ(πΈ β βͺ
π β β π΄)) β€ (πβπΈ)) β (((πβπΈ) +π
-π(πβ(πΈ β βͺ
π β β π΄))) +π (πβ(πΈ β βͺ
π β β π΄))) = (πβπΈ)) |
205 | 14, 17, 75, 204 | syl3anc 1372 |
. 2
β’ (π β (((πβπΈ) +π
-π(πβ(πΈ β βͺ
π β β π΄))) +π (πβ(πΈ β βͺ
π β β π΄))) = (πβπΈ)) |
206 | 203, 205 | breqtrd 5136 |
1
β’ (π β ((πβ(πΈ β© βͺ
π β β π΄)) +π (πβ(πΈ β βͺ
π β β π΄))) β€ (πβπΈ)) |