Step | Hyp | Ref
| Expression |
1 | | iccssxr 13354 |
. . . . . . 7
β’
(0[,]+β) β β* |
2 | | carsgval.2 |
. . . . . . . 8
β’ (π β π:π« πβΆ(0[,]+β)) |
3 | | carsgclctunlem3.1 |
. . . . . . . . 9
β’ (π β πΈ β π« π) |
4 | 3 | elpwincl1 31495 |
. . . . . . . 8
β’ (π β (πΈ β© βͺ π΄) β π« π) |
5 | 2, 4 | ffvelcdmd 7041 |
. . . . . . 7
β’ (π β (πβ(πΈ β© βͺ π΄)) β
(0[,]+β)) |
6 | 1, 5 | sselid 3947 |
. . . . . 6
β’ (π β (πβ(πΈ β© βͺ π΄)) β
β*) |
7 | 3 | elpwdifcl 31496 |
. . . . . . . 8
β’ (π β (πΈ β βͺ π΄) β π« π) |
8 | 2, 7 | ffvelcdmd 7041 |
. . . . . . 7
β’ (π β (πβ(πΈ β βͺ π΄)) β
(0[,]+β)) |
9 | 1, 8 | sselid 3947 |
. . . . . 6
β’ (π β (πβ(πΈ β βͺ π΄)) β
β*) |
10 | 6, 9 | xaddcld 13227 |
. . . . 5
β’ (π β ((πβ(πΈ β© βͺ π΄)) +π (πβ(πΈ β βͺ π΄))) β
β*) |
11 | 10 | adantr 482 |
. . . 4
β’ ((π β§ (πβπΈ) = +β) β ((πβ(πΈ β© βͺ π΄)) +π (πβ(πΈ β βͺ π΄))) β
β*) |
12 | | pnfge 13058 |
. . . 4
β’ (((πβ(πΈ β© βͺ π΄)) +π (πβ(πΈ β βͺ π΄))) β β*
β ((πβ(πΈ β© βͺ π΄))
+π (πβ(πΈ β βͺ π΄))) β€
+β) |
13 | 11, 12 | syl 17 |
. . 3
β’ ((π β§ (πβπΈ) = +β) β ((πβ(πΈ β© βͺ π΄)) +π (πβ(πΈ β βͺ π΄))) β€
+β) |
14 | | simpr 486 |
. . 3
β’ ((π β§ (πβπΈ) = +β) β (πβπΈ) = +β) |
15 | 13, 14 | breqtrrd 5138 |
. 2
β’ ((π β§ (πβπΈ) = +β) β ((πβ(πΈ β© βͺ π΄)) +π (πβ(πΈ β βͺ π΄))) β€ (πβπΈ)) |
16 | | unieq 4881 |
. . . . . . . . . . . . 13
β’ (π΄ = β
β βͺ π΄ =
βͺ β
) |
17 | | uni0 4901 |
. . . . . . . . . . . . 13
β’ βͺ β
= β
|
18 | 16, 17 | eqtrdi 2793 |
. . . . . . . . . . . 12
β’ (π΄ = β
β βͺ π΄ =
β
) |
19 | 18 | ineq2d 4177 |
. . . . . . . . . . 11
β’ (π΄ = β
β (πΈ β© βͺ π΄) =
(πΈ β©
β
)) |
20 | | in0 4356 |
. . . . . . . . . . 11
β’ (πΈ β© β
) =
β
|
21 | 19, 20 | eqtrdi 2793 |
. . . . . . . . . 10
β’ (π΄ = β
β (πΈ β© βͺ π΄) =
β
) |
22 | 21 | fveq2d 6851 |
. . . . . . . . 9
β’ (π΄ = β
β (πβ(πΈ β© βͺ π΄)) = (πββ
)) |
23 | 18 | difeq2d 4087 |
. . . . . . . . . . 11
β’ (π΄ = β
β (πΈ β βͺ π΄) =
(πΈ β
β
)) |
24 | | dif0 4337 |
. . . . . . . . . . 11
β’ (πΈ β β
) = πΈ |
25 | 23, 24 | eqtrdi 2793 |
. . . . . . . . . 10
β’ (π΄ = β
β (πΈ β βͺ π΄) =
πΈ) |
26 | 25 | fveq2d 6851 |
. . . . . . . . 9
β’ (π΄ = β
β (πβ(πΈ β βͺ π΄)) = (πβπΈ)) |
27 | 22, 26 | oveq12d 7380 |
. . . . . . . 8
β’ (π΄ = β
β ((πβ(πΈ β© βͺ π΄)) +π (πβ(πΈ β βͺ π΄))) = ((πββ
) +π (πβπΈ))) |
28 | 27 | adantl 483 |
. . . . . . 7
β’ ((π β§ π΄ = β
) β ((πβ(πΈ β© βͺ π΄)) +π (πβ(πΈ β βͺ π΄))) = ((πββ
) +π (πβπΈ))) |
29 | | carsgsiga.1 |
. . . . . . . . 9
β’ (π β (πββ
) = 0) |
30 | 29 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π΄ = β
) β (πββ
) = 0) |
31 | 30 | oveq1d 7377 |
. . . . . . 7
β’ ((π β§ π΄ = β
) β ((πββ
) +π (πβπΈ)) = (0 +π (πβπΈ))) |
32 | 2, 3 | ffvelcdmd 7041 |
. . . . . . . . . 10
β’ (π β (πβπΈ) β (0[,]+β)) |
33 | 1, 32 | sselid 3947 |
. . . . . . . . 9
β’ (π β (πβπΈ) β
β*) |
34 | 33 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π΄ = β
) β (πβπΈ) β
β*) |
35 | | xaddid2 13168 |
. . . . . . . 8
β’ ((πβπΈ) β β* β (0
+π (πβπΈ)) = (πβπΈ)) |
36 | 34, 35 | syl 17 |
. . . . . . 7
β’ ((π β§ π΄ = β
) β (0 +π
(πβπΈ)) = (πβπΈ)) |
37 | 28, 31, 36 | 3eqtrd 2781 |
. . . . . 6
β’ ((π β§ π΄ = β
) β ((πβ(πΈ β© βͺ π΄)) +π (πβ(πΈ β βͺ π΄))) = (πβπΈ)) |
38 | 37, 34 | eqeltrd 2838 |
. . . . . . 7
β’ ((π β§ π΄ = β
) β ((πβ(πΈ β© βͺ π΄)) +π (πβ(πΈ β βͺ π΄))) β
β*) |
39 | | xeqlelt 31721 |
. . . . . . 7
β’ ((((πβ(πΈ β© βͺ π΄)) +π (πβ(πΈ β βͺ π΄))) β β*
β§ (πβπΈ) β β*)
β (((πβ(πΈ β© βͺ π΄))
+π (πβ(πΈ β βͺ π΄))) = (πβπΈ) β (((πβ(πΈ β© βͺ π΄)) +π (πβ(πΈ β βͺ π΄))) β€ (πβπΈ) β§ Β¬ ((πβ(πΈ β© βͺ π΄)) +π (πβ(πΈ β βͺ π΄))) < (πβπΈ)))) |
40 | 38, 34, 39 | syl2anc 585 |
. . . . . 6
β’ ((π β§ π΄ = β
) β (((πβ(πΈ β© βͺ π΄)) +π (πβ(πΈ β βͺ π΄))) = (πβπΈ) β (((πβ(πΈ β© βͺ π΄)) +π (πβ(πΈ β βͺ π΄))) β€ (πβπΈ) β§ Β¬ ((πβ(πΈ β© βͺ π΄)) +π (πβ(πΈ β βͺ π΄))) < (πβπΈ)))) |
41 | 37, 40 | mpbid 231 |
. . . . 5
β’ ((π β§ π΄ = β
) β (((πβ(πΈ β© βͺ π΄)) +π (πβ(πΈ β βͺ π΄))) β€ (πβπΈ) β§ Β¬ ((πβ(πΈ β© βͺ π΄)) +π (πβ(πΈ β βͺ π΄))) < (πβπΈ))) |
42 | 41 | simpld 496 |
. . . 4
β’ ((π β§ π΄ = β
) β ((πβ(πΈ β© βͺ π΄)) +π (πβ(πΈ β βͺ π΄))) β€ (πβπΈ)) |
43 | 42 | adantlr 714 |
. . 3
β’ (((π β§ (πβπΈ) β +β) β§ π΄ = β
) β ((πβ(πΈ β© βͺ π΄)) +π (πβ(πΈ β βͺ π΄))) β€ (πβπΈ)) |
44 | | carsgclctun.2 |
. . . . . . . 8
β’ (π β π΄ β (toCaraSigaβπ)) |
45 | | fvex 6860 |
. . . . . . . . 9
β’
(toCaraSigaβπ)
β V |
46 | 45 | ssex 5283 |
. . . . . . . 8
β’ (π΄ β (toCaraSigaβπ) β π΄ β V) |
47 | | 0sdomg 9055 |
. . . . . . . 8
β’ (π΄ β V β (β
βΊ π΄ β π΄ β β
)) |
48 | 44, 46, 47 | 3syl 18 |
. . . . . . 7
β’ (π β (β
βΊ π΄ β π΄ β β
)) |
49 | 48 | biimpar 479 |
. . . . . 6
β’ ((π β§ π΄ β β
) β β
βΊ π΄) |
50 | 49 | adantlr 714 |
. . . . 5
β’ (((π β§ (πβπΈ) β +β) β§ π΄ β β
) β β
βΊ π΄) |
51 | | carsgclctun.1 |
. . . . . . 7
β’ (π β π΄ βΌ Ο) |
52 | | nnenom 13892 |
. . . . . . . 8
β’ β
β Ο |
53 | 52 | ensymi 8951 |
. . . . . . 7
β’ Ο
β β |
54 | | domentr 8960 |
. . . . . . 7
β’ ((π΄ βΌ Ο β§ Ο
β β) β π΄
βΌ β) |
55 | 51, 53, 54 | sylancl 587 |
. . . . . 6
β’ (π β π΄ βΌ β) |
56 | 55 | ad2antrr 725 |
. . . . 5
β’ (((π β§ (πβπΈ) β +β) β§ π΄ β β
) β π΄ βΌ β) |
57 | | fodomr 9079 |
. . . . 5
β’ ((β
βΊ π΄ β§ π΄ βΌ β) β
βπ π:ββontoβπ΄) |
58 | 50, 56, 57 | syl2anc 585 |
. . . 4
β’ (((π β§ (πβπΈ) β +β) β§ π΄ β β
) β βπ π:ββontoβπ΄) |
59 | | fveq2 6847 |
. . . . . . . . . 10
β’ (π = π β (πβπ) = (πβπ)) |
60 | 59 | iundisj 24928 |
. . . . . . . . 9
β’ βͺ π β β (πβπ) = βͺ π β β ((πβπ) β βͺ
π β (1..^π)(πβπ)) |
61 | | fofn 6763 |
. . . . . . . . . . . 12
β’ (π:ββontoβπ΄ β π Fn β) |
62 | | fniunfv 7199 |
. . . . . . . . . . . 12
β’ (π Fn β β βͺ π β β (πβπ) = βͺ ran π) |
63 | 61, 62 | syl 17 |
. . . . . . . . . . 11
β’ (π:ββontoβπ΄ β βͺ
π β β (πβπ) = βͺ ran π) |
64 | | forn 6764 |
. . . . . . . . . . . 12
β’ (π:ββontoβπ΄ β ran π = π΄) |
65 | 64 | unieqd 4884 |
. . . . . . . . . . 11
β’ (π:ββontoβπ΄ β βͺ ran
π = βͺ π΄) |
66 | 63, 65 | eqtrd 2777 |
. . . . . . . . . 10
β’ (π:ββontoβπ΄ β βͺ
π β β (πβπ) = βͺ π΄) |
67 | 66 | adantl 483 |
. . . . . . . . 9
β’ ((((π β§ (πβπΈ) β +β) β§ π΄ β β
) β§ π:ββontoβπ΄) β βͺ
π β β (πβπ) = βͺ π΄) |
68 | 60, 67 | eqtr3id 2791 |
. . . . . . . 8
β’ ((((π β§ (πβπΈ) β +β) β§ π΄ β β
) β§ π:ββontoβπ΄) β βͺ
π β β ((πβπ) β βͺ
π β (1..^π)(πβπ)) = βͺ π΄) |
69 | 68 | ineq2d 4177 |
. . . . . . 7
β’ ((((π β§ (πβπΈ) β +β) β§ π΄ β β
) β§ π:ββontoβπ΄) β (πΈ β© βͺ
π β β ((πβπ) β βͺ
π β (1..^π)(πβπ))) = (πΈ β© βͺ π΄)) |
70 | 69 | fveq2d 6851 |
. . . . . 6
β’ ((((π β§ (πβπΈ) β +β) β§ π΄ β β
) β§ π:ββontoβπ΄) β (πβ(πΈ β© βͺ
π β β ((πβπ) β βͺ
π β (1..^π)(πβπ)))) = (πβ(πΈ β© βͺ π΄))) |
71 | 68 | difeq2d 4087 |
. . . . . . 7
β’ ((((π β§ (πβπΈ) β +β) β§ π΄ β β
) β§ π:ββontoβπ΄) β (πΈ β βͺ
π β β ((πβπ) β βͺ
π β (1..^π)(πβπ))) = (πΈ β βͺ π΄)) |
72 | 71 | fveq2d 6851 |
. . . . . 6
β’ ((((π β§ (πβπΈ) β +β) β§ π΄ β β
) β§ π:ββontoβπ΄) β (πβ(πΈ β βͺ
π β β ((πβπ) β βͺ
π β (1..^π)(πβπ)))) = (πβ(πΈ β βͺ π΄))) |
73 | 70, 72 | oveq12d 7380 |
. . . . 5
β’ ((((π β§ (πβπΈ) β +β) β§ π΄ β β
) β§ π:ββontoβπ΄) β ((πβ(πΈ β© βͺ
π β β ((πβπ) β βͺ
π β (1..^π)(πβπ)))) +π (πβ(πΈ β βͺ
π β β ((πβπ) β βͺ
π β (1..^π)(πβπ))))) = ((πβ(πΈ β© βͺ π΄)) +π (πβ(πΈ β βͺ π΄)))) |
74 | | carsgval.1 |
. . . . . . 7
β’ (π β π β π) |
75 | 74 | ad3antrrr 729 |
. . . . . 6
β’ ((((π β§ (πβπΈ) β +β) β§ π΄ β β
) β§ π:ββontoβπ΄) β π β π) |
76 | 2 | ad3antrrr 729 |
. . . . . 6
β’ ((((π β§ (πβπΈ) β +β) β§ π΄ β β
) β§ π:ββontoβπ΄) β π:π« πβΆ(0[,]+β)) |
77 | 29 | ad3antrrr 729 |
. . . . . 6
β’ ((((π β§ (πβπΈ) β +β) β§ π΄ β β
) β§ π:ββontoβπ΄) β (πββ
) = 0) |
78 | | carsgsiga.2 |
. . . . . . . . 9
β’ ((π β§ π₯ βΌ Ο β§ π₯ β π« π) β (πββͺ π₯) β€ Ξ£*π¦ β π₯(πβπ¦)) |
79 | 78 | 3adant1r 1178 |
. . . . . . . 8
β’ (((π β§ (πβπΈ) β +β) β§ π₯ βΌ Ο β§ π₯ β π« π) β (πββͺ π₯) β€ Ξ£*π¦ β π₯(πβπ¦)) |
80 | 79 | 3adant1r 1178 |
. . . . . . 7
β’ ((((π β§ (πβπΈ) β +β) β§ π΄ β β
) β§ π₯ βΌ Ο β§ π₯ β π« π) β (πββͺ π₯) β€ Ξ£*π¦ β π₯(πβπ¦)) |
81 | 80 | 3adant1r 1178 |
. . . . . 6
β’
(((((π β§ (πβπΈ) β +β) β§ π΄ β β
) β§ π:ββontoβπ΄) β§ π₯ βΌ Ο β§ π₯ β π« π) β (πββͺ π₯) β€ Ξ£*π¦ β π₯(πβπ¦)) |
82 | | carsgsiga.3 |
. . . . . . . . 9
β’ ((π β§ π₯ β π¦ β§ π¦ β π« π) β (πβπ₯) β€ (πβπ¦)) |
83 | 82 | 3adant1r 1178 |
. . . . . . . 8
β’ (((π β§ (πβπΈ) β +β) β§ π₯ β π¦ β§ π¦ β π« π) β (πβπ₯) β€ (πβπ¦)) |
84 | 83 | 3adant1r 1178 |
. . . . . . 7
β’ ((((π β§ (πβπΈ) β +β) β§ π΄ β β
) β§ π₯ β π¦ β§ π¦ β π« π) β (πβπ₯) β€ (πβπ¦)) |
85 | 84 | 3adant1r 1178 |
. . . . . 6
β’
(((((π β§ (πβπΈ) β +β) β§ π΄ β β
) β§ π:ββontoβπ΄) β§ π₯ β π¦ β§ π¦ β π« π) β (πβπ₯) β€ (πβπ¦)) |
86 | 59 | iundisj2 24929 |
. . . . . . 7
β’
Disj π β
β ((πβπ) β βͺ π β (1..^π)(πβπ)) |
87 | 86 | a1i 11 |
. . . . . 6
β’ ((((π β§ (πβπΈ) β +β) β§ π΄ β β
) β§ π:ββontoβπ΄) β Disj π β β ((πβπ) β βͺ
π β (1..^π)(πβπ))) |
88 | 75 | adantr 482 |
. . . . . . 7
β’
(((((π β§ (πβπΈ) β +β) β§ π΄ β β
) β§ π:ββontoβπ΄) β§ π β β) β π β π) |
89 | 76 | adantr 482 |
. . . . . . 7
β’
(((((π β§ (πβπΈ) β +β) β§ π΄ β β
) β§ π:ββontoβπ΄) β§ π β β) β π:π« πβΆ(0[,]+β)) |
90 | 44 | ad4antr 731 |
. . . . . . . 8
β’
(((((π β§ (πβπΈ) β +β) β§ π΄ β β
) β§ π:ββontoβπ΄) β§ π β β) β π΄ β (toCaraSigaβπ)) |
91 | | fof 6761 |
. . . . . . . . . 10
β’ (π:ββontoβπ΄ β π:ββΆπ΄) |
92 | 91 | ad2antlr 726 |
. . . . . . . . 9
β’
(((((π β§ (πβπΈ) β +β) β§ π΄ β β
) β§ π:ββontoβπ΄) β§ π β β) β π:ββΆπ΄) |
93 | | simpr 486 |
. . . . . . . . 9
β’
(((((π β§ (πβπΈ) β +β) β§ π΄ β β
) β§ π:ββontoβπ΄) β§ π β β) β π β β) |
94 | 92, 93 | ffvelcdmd 7041 |
. . . . . . . 8
β’
(((((π β§ (πβπΈ) β +β) β§ π΄ β β
) β§ π:ββontoβπ΄) β§ π β β) β (πβπ) β π΄) |
95 | 90, 94 | sseldd 3950 |
. . . . . . 7
β’
(((((π β§ (πβπΈ) β +β) β§ π΄ β β
) β§ π:ββontoβπ΄) β§ π β β) β (πβπ) β (toCaraSigaβπ)) |
96 | 77 | adantr 482 |
. . . . . . . 8
β’
(((((π β§ (πβπΈ) β +β) β§ π΄ β β
) β§ π:ββontoβπ΄) β§ π β β) β (πββ
) = 0) |
97 | 81 | 3adant1r 1178 |
. . . . . . . 8
β’
((((((π β§ (πβπΈ) β +β) β§ π΄ β β
) β§ π:ββontoβπ΄) β§ π β β) β§ π₯ βΌ Ο β§ π₯ β π« π) β (πββͺ π₯) β€ Ξ£*π¦ β π₯(πβπ¦)) |
98 | 88, 89, 96, 97 | carsgsigalem 32955 |
. . . . . . 7
β’
((((((π β§ (πβπΈ) β +β) β§ π΄ β β
) β§ π:ββontoβπ΄) β§ π β β) β§ π β π« π β§ π β π« π) β (πβ(π βͺ π)) β€ ((πβπ) +π (πβπ))) |
99 | 91 | ad3antlr 730 |
. . . . . . . . . . 11
β’
((((((π β§ (πβπΈ) β +β) β§ π΄ β β
) β§ π:ββontoβπ΄) β§ π β β) β§ π β (1..^π)) β π:ββΆπ΄) |
100 | | fzossnn 13628 |
. . . . . . . . . . . . 13
β’
(1..^π) β
β |
101 | 100 | a1i 11 |
. . . . . . . . . . . 12
β’
(((((π β§ (πβπΈ) β +β) β§ π΄ β β
) β§ π:ββontoβπ΄) β§ π β β) β (1..^π) β
β) |
102 | 101 | sselda 3949 |
. . . . . . . . . . 11
β’
((((((π β§ (πβπΈ) β +β) β§ π΄ β β
) β§ π:ββontoβπ΄) β§ π β β) β§ π β (1..^π)) β π β β) |
103 | 99, 102 | ffvelcdmd 7041 |
. . . . . . . . . 10
β’
((((((π β§ (πβπΈ) β +β) β§ π΄ β β
) β§ π:ββontoβπ΄) β§ π β β) β§ π β (1..^π)) β (πβπ) β π΄) |
104 | 103 | ralrimiva 3144 |
. . . . . . . . 9
β’
(((((π β§ (πβπΈ) β +β) β§ π΄ β β
) β§ π:ββontoβπ΄) β§ π β β) β βπ β (1..^π)(πβπ) β π΄) |
105 | | dfiun2g 4995 |
. . . . . . . . 9
β’
(βπ β
(1..^π)(πβπ) β π΄ β βͺ
π β (1..^π)(πβπ) = βͺ {π§ β£ βπ β (1..^π)π§ = (πβπ)}) |
106 | 104, 105 | syl 17 |
. . . . . . . 8
β’
(((((π β§ (πβπΈ) β +β) β§ π΄ β β
) β§ π:ββontoβπ΄) β§ π β β) β βͺ π β (1..^π)(πβπ) = βͺ {π§ β£ βπ β (1..^π)π§ = (πβπ)}) |
107 | | eqid 2737 |
. . . . . . . . . . . 12
β’ (π β (1..^π) β¦ (πβπ)) = (π β (1..^π) β¦ (πβπ)) |
108 | 107 | rnmpt 5915 |
. . . . . . . . . . 11
β’ ran
(π β (1..^π) β¦ (πβπ)) = {π§ β£ βπ β (1..^π)π§ = (πβπ)} |
109 | | fzofi 13886 |
. . . . . . . . . . . 12
β’
(1..^π) β
Fin |
110 | | mptfi 9302 |
. . . . . . . . . . . 12
β’
((1..^π) β Fin
β (π β (1..^π) β¦ (πβπ)) β Fin) |
111 | | rnfi 9286 |
. . . . . . . . . . . 12
β’ ((π β (1..^π) β¦ (πβπ)) β Fin β ran (π β (1..^π) β¦ (πβπ)) β Fin) |
112 | 109, 110,
111 | mp2b 10 |
. . . . . . . . . . 11
β’ ran
(π β (1..^π) β¦ (πβπ)) β Fin |
113 | 108, 112 | eqeltrri 2835 |
. . . . . . . . . 10
β’ {π§ β£ βπ β (1..^π)π§ = (πβπ)} β Fin |
114 | 113 | a1i 11 |
. . . . . . . . 9
β’
(((((π β§ (πβπΈ) β +β) β§ π΄ β β
) β§ π:ββontoβπ΄) β§ π β β) β {π§ β£ βπ β (1..^π)π§ = (πβπ)} β Fin) |
115 | 90 | adantr 482 |
. . . . . . . . . . . . 13
β’
((((((π β§ (πβπΈ) β +β) β§ π΄ β β
) β§ π:ββontoβπ΄) β§ π β β) β§ π β (1..^π)) β π΄ β (toCaraSigaβπ)) |
116 | 115, 103 | sseldd 3950 |
. . . . . . . . . . . 12
β’
((((((π β§ (πβπΈ) β +β) β§ π΄ β β
) β§ π:ββontoβπ΄) β§ π β β) β§ π β (1..^π)) β (πβπ) β (toCaraSigaβπ)) |
117 | 116 | ralrimiva 3144 |
. . . . . . . . . . 11
β’
(((((π β§ (πβπΈ) β +β) β§ π΄ β β
) β§ π:ββontoβπ΄) β§ π β β) β βπ β (1..^π)(πβπ) β (toCaraSigaβπ)) |
118 | 107 | rnmptss 7075 |
. . . . . . . . . . 11
β’
(βπ β
(1..^π)(πβπ) β (toCaraSigaβπ) β ran (π β (1..^π) β¦ (πβπ)) β (toCaraSigaβπ)) |
119 | 117, 118 | syl 17 |
. . . . . . . . . 10
β’
(((((π β§ (πβπΈ) β +β) β§ π΄ β β
) β§ π:ββontoβπ΄) β§ π β β) β ran (π β (1..^π) β¦ (πβπ)) β (toCaraSigaβπ)) |
120 | 108, 119 | eqsstrrid 3998 |
. . . . . . . . 9
β’
(((((π β§ (πβπΈ) β +β) β§ π΄ β β
) β§ π:ββontoβπ΄) β§ π β β) β {π§ β£ βπ β (1..^π)π§ = (πβπ)} β (toCaraSigaβπ)) |
121 | 88, 89, 96, 97, 114, 120 | fiunelcarsg 32956 |
. . . . . . . 8
β’
(((((π β§ (πβπΈ) β +β) β§ π΄ β β
) β§ π:ββontoβπ΄) β§ π β β) β βͺ {π§
β£ βπ β
(1..^π)π§ = (πβπ)} β (toCaraSigaβπ)) |
122 | 106, 121 | eqeltrd 2838 |
. . . . . . 7
β’
(((((π β§ (πβπΈ) β +β) β§ π΄ β β
) β§ π:ββontoβπ΄) β§ π β β) β βͺ π β (1..^π)(πβπ) β (toCaraSigaβπ)) |
123 | 88, 89, 95, 98, 122 | difelcarsg2 32953 |
. . . . . 6
β’
(((((π β§ (πβπΈ) β +β) β§ π΄ β β
) β§ π:ββontoβπ΄) β§ π β β) β ((πβπ) β βͺ
π β (1..^π)(πβπ)) β (toCaraSigaβπ)) |
124 | 3 | ad3antrrr 729 |
. . . . . 6
β’ ((((π β§ (πβπΈ) β +β) β§ π΄ β β
) β§ π:ββontoβπ΄) β πΈ β π« π) |
125 | | simpllr 775 |
. . . . . 6
β’ ((((π β§ (πβπΈ) β +β) β§ π΄ β β
) β§ π:ββontoβπ΄) β (πβπΈ) β +β) |
126 | 75, 76, 77, 81, 85, 87, 123, 124, 125 | carsgclctunlem2 32959 |
. . . . 5
β’ ((((π β§ (πβπΈ) β +β) β§ π΄ β β
) β§ π:ββontoβπ΄) β ((πβ(πΈ β© βͺ
π β β ((πβπ) β βͺ
π β (1..^π)(πβπ)))) +π (πβ(πΈ β βͺ
π β β ((πβπ) β βͺ
π β (1..^π)(πβπ))))) β€ (πβπΈ)) |
127 | 73, 126 | eqbrtrrd 5134 |
. . . 4
β’ ((((π β§ (πβπΈ) β +β) β§ π΄ β β
) β§ π:ββontoβπ΄) β ((πβ(πΈ β© βͺ π΄)) +π (πβ(πΈ β βͺ π΄))) β€ (πβπΈ)) |
128 | 58, 127 | exlimddv 1939 |
. . 3
β’ (((π β§ (πβπΈ) β +β) β§ π΄ β β
) β ((πβ(πΈ β© βͺ π΄)) +π (πβ(πΈ β βͺ π΄))) β€ (πβπΈ)) |
129 | 43, 128 | pm2.61dane 3033 |
. 2
β’ ((π β§ (πβπΈ) β +β) β ((πβ(πΈ β© βͺ π΄)) +π (πβ(πΈ β βͺ π΄))) β€ (πβπΈ)) |
130 | 15, 129 | pm2.61dane 3033 |
1
β’ (π β ((πβ(πΈ β© βͺ π΄)) +π (πβ(πΈ β βͺ π΄))) β€ (πβπΈ)) |