Step | Hyp | Ref
| Expression |
1 | | dvadd.bg |
. . . 4
β’ (π β πΆ(π D πΊ)πΏ) |
2 | | eqid 2177 |
. . . . 5
β’ (π½ βΎt π) = (π½ βΎt π) |
3 | | dvaddcntop.j |
. . . . 5
β’ π½ = (MetOpenβ(abs β
β )) |
4 | | eqid 2177 |
. . . . 5
β’ (π§ β {π€ β π β£ π€ # πΆ} β¦ (((πΊβπ§) β (πΊβπΆ)) / (π§ β πΆ))) = (π§ β {π€ β π β£ π€ # πΆ} β¦ (((πΊβπ§) β (πΊβπΆ)) / (π§ β πΆ))) |
5 | | dvaddbr.s |
. . . . 5
β’ (π β π β β) |
6 | | dvaddxx.g |
. . . . 5
β’ (π β πΊ:πβΆβ) |
7 | | dvadd.x |
. . . . 5
β’ (π β π β π) |
8 | 2, 3, 4, 5, 6, 7 | eldvap 14087 |
. . . 4
β’ (π β (πΆ(π D πΊ)πΏ β (πΆ β ((intβ(π½ βΎt π))βπ) β§ πΏ β ((π§ β {π€ β π β£ π€ # πΆ} β¦ (((πΊβπ§) β (πΊβπΆ)) / (π§ β πΆ))) limβ πΆ)))) |
9 | 1, 8 | mpbid 147 |
. . 3
β’ (π β (πΆ β ((intβ(π½ βΎt π))βπ) β§ πΏ β ((π§ β {π€ β π β£ π€ # πΆ} β¦ (((πΊβπ§) β (πΊβπΆ)) / (π§ β πΆ))) limβ πΆ))) |
10 | 9 | simpld 112 |
. 2
β’ (π β πΆ β ((intβ(π½ βΎt π))βπ)) |
11 | | dvadd.f |
. . . . 5
β’ (π β πΉ:πβΆβ) |
12 | 7, 5 | sstrd 3165 |
. . . . 5
β’ (π β π β β) |
13 | 3 | cntoptopon 13968 |
. . . . . . . . 9
β’ π½ β
(TopOnββ) |
14 | | resttopon 13607 |
. . . . . . . . 9
β’ ((π½ β (TopOnββ)
β§ π β β)
β (π½
βΎt π)
β (TopOnβπ)) |
15 | 13, 5, 14 | sylancr 414 |
. . . . . . . 8
β’ (π β (π½ βΎt π) β (TopOnβπ)) |
16 | | topontop 13450 |
. . . . . . . 8
β’ ((π½ βΎt π) β (TopOnβπ) β (π½ βΎt π) β Top) |
17 | 15, 16 | syl 14 |
. . . . . . 7
β’ (π β (π½ βΎt π) β Top) |
18 | | toponuni 13451 |
. . . . . . . . 9
β’ ((π½ βΎt π) β (TopOnβπ) β π = βͺ (π½ βΎt π)) |
19 | 15, 18 | syl 14 |
. . . . . . . 8
β’ (π β π = βͺ (π½ βΎt π)) |
20 | 7, 19 | sseqtrd 3193 |
. . . . . . 7
β’ (π β π β βͺ (π½ βΎt π)) |
21 | | eqid 2177 |
. . . . . . . 8
β’ βͺ (π½
βΎt π) =
βͺ (π½ βΎt π) |
22 | 21 | ntrss2 13557 |
. . . . . . 7
β’ (((π½ βΎt π) β Top β§ π β βͺ (π½
βΎt π))
β ((intβ(π½
βΎt π))βπ) β π) |
23 | 17, 20, 22 | syl2anc 411 |
. . . . . 6
β’ (π β ((intβ(π½ βΎt π))βπ) β π) |
24 | | dvadd.bf |
. . . . . . . 8
β’ (π β πΆ(π D πΉ)πΎ) |
25 | | eqid 2177 |
. . . . . . . . 9
β’ (π§ β {π€ β π β£ π€ # πΆ} β¦ (((πΉβπ§) β (πΉβπΆ)) / (π§ β πΆ))) = (π§ β {π€ β π β£ π€ # πΆ} β¦ (((πΉβπ§) β (πΉβπΆ)) / (π§ β πΆ))) |
26 | 2, 3, 25, 5, 11, 7 | eldvap 14087 |
. . . . . . . 8
β’ (π β (πΆ(π D πΉ)πΎ β (πΆ β ((intβ(π½ βΎt π))βπ) β§ πΎ β ((π§ β {π€ β π β£ π€ # πΆ} β¦ (((πΉβπ§) β (πΉβπΆ)) / (π§ β πΆ))) limβ πΆ)))) |
27 | 24, 26 | mpbid 147 |
. . . . . . 7
β’ (π β (πΆ β ((intβ(π½ βΎt π))βπ) β§ πΎ β ((π§ β {π€ β π β£ π€ # πΆ} β¦ (((πΉβπ§) β (πΉβπΆ)) / (π§ β πΆ))) limβ πΆ))) |
28 | 27 | simpld 112 |
. . . . . 6
β’ (π β πΆ β ((intβ(π½ βΎt π))βπ)) |
29 | 23, 28 | sseldd 3156 |
. . . . 5
β’ (π β πΆ β π) |
30 | 11, 12, 29 | dvlemap 14085 |
. . . 4
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β (((πΉβπ§) β (πΉβπΆ)) / (π§ β πΆ)) β β) |
31 | 6, 12, 29 | dvlemap 14085 |
. . . 4
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β (((πΊβπ§) β (πΊβπΆ)) / (π§ β πΆ)) β β) |
32 | | ssidd 3176 |
. . . 4
β’ (π β β β
β) |
33 | | txtopon 13698 |
. . . . . 6
β’ ((π½ β (TopOnββ)
β§ π½ β
(TopOnββ)) β (π½ Γt π½) β (TopOnβ(β Γ
β))) |
34 | 13, 13, 33 | mp2an 426 |
. . . . 5
β’ (π½ Γt π½) β (TopOnβ(β
Γ β)) |
35 | 34 | toponrestid 13457 |
. . . 4
β’ (π½ Γt π½) = ((π½ Γt π½) βΎt (β Γ
β)) |
36 | 27 | simprd 114 |
. . . 4
β’ (π β πΎ β ((π§ β {π€ β π β£ π€ # πΆ} β¦ (((πΉβπ§) β (πΉβπΆ)) / (π§ β πΆ))) limβ πΆ)) |
37 | 9 | simprd 114 |
. . . 4
β’ (π β πΏ β ((π§ β {π€ β π β£ π€ # πΆ} β¦ (((πΊβπ§) β (πΊβπΆ)) / (π§ β πΆ))) limβ πΆ)) |
38 | 3 | addcncntop 13988 |
. . . . 5
β’ + β
((π½ Γt
π½) Cn π½) |
39 | 5, 11, 7 | dvcl 14088 |
. . . . . . 7
β’ ((π β§ πΆ(π D πΉ)πΎ) β πΎ β β) |
40 | 24, 39 | mpdan 421 |
. . . . . 6
β’ (π β πΎ β β) |
41 | 5, 6, 7 | dvcl 14088 |
. . . . . . 7
β’ ((π β§ πΆ(π D πΊ)πΏ) β πΏ β β) |
42 | 1, 41 | mpdan 421 |
. . . . . 6
β’ (π β πΏ β β) |
43 | 40, 42 | opelxpd 4659 |
. . . . 5
β’ (π β β¨πΎ, πΏβ© β (β Γ
β)) |
44 | 34 | toponunii 13453 |
. . . . . 6
β’ (β
Γ β) = βͺ (π½ Γt π½) |
45 | 44 | cncnpi 13664 |
. . . . 5
β’ (( +
β ((π½
Γt π½) Cn
π½) β§ β¨πΎ, πΏβ© β (β Γ β))
β + β (((π½
Γt π½) CnP
π½)ββ¨πΎ, πΏβ©)) |
46 | 38, 43, 45 | sylancr 414 |
. . . 4
β’ (π β + β (((π½ Γt π½) CnP π½)ββ¨πΎ, πΏβ©)) |
47 | 30, 31, 32, 32, 3, 35, 36, 37, 46 | limccnp2cntop 14082 |
. . 3
β’ (π β (πΎ + πΏ) β ((π§ β {π€ β π β£ π€ # πΆ} β¦ ((((πΉβπ§) β (πΉβπΆ)) / (π§ β πΆ)) + (((πΊβπ§) β (πΊβπΆ)) / (π§ β πΆ)))) limβ πΆ)) |
48 | | elrabi 2890 |
. . . . . . . . . . 11
β’ (π§ β {π€ β π β£ π€ # πΆ} β π§ β π) |
49 | 48 | adantl 277 |
. . . . . . . . . 10
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β π§ β π) |
50 | 11 | ffnd 5366 |
. . . . . . . . . . . 12
β’ (π β πΉ Fn π) |
51 | 50 | adantr 276 |
. . . . . . . . . . 11
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β πΉ Fn π) |
52 | 6 | ffnd 5366 |
. . . . . . . . . . . 12
β’ (π β πΊ Fn π) |
53 | 52 | adantr 276 |
. . . . . . . . . . 11
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β πΊ Fn π) |
54 | | cnex 7934 |
. . . . . . . . . . . . 13
β’ β
β V |
55 | | ssexg 4142 |
. . . . . . . . . . . . 13
β’ ((π β β β§ β
β V) β π β
V) |
56 | 12, 54, 55 | sylancl 413 |
. . . . . . . . . . . 12
β’ (π β π β V) |
57 | 56 | adantr 276 |
. . . . . . . . . . 11
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β π β V) |
58 | | inidm 3344 |
. . . . . . . . . . 11
β’ (π β© π) = π |
59 | | eqidd 2178 |
. . . . . . . . . . 11
β’ (((π β§ π§ β {π€ β π β£ π€ # πΆ}) β§ π§ β π) β (πΉβπ§) = (πΉβπ§)) |
60 | | eqidd 2178 |
. . . . . . . . . . 11
β’ (((π β§ π§ β {π€ β π β£ π€ # πΆ}) β§ π§ β π) β (πΊβπ§) = (πΊβπ§)) |
61 | 11 | adantr 276 |
. . . . . . . . . . . . 13
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β πΉ:πβΆβ) |
62 | 61 | ffvelcdmda 5651 |
. . . . . . . . . . . 12
β’ (((π β§ π§ β {π€ β π β£ π€ # πΆ}) β§ π§ β π) β (πΉβπ§) β β) |
63 | 6 | adantr 276 |
. . . . . . . . . . . . 13
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β πΊ:πβΆβ) |
64 | 63 | ffvelcdmda 5651 |
. . . . . . . . . . . 12
β’ (((π β§ π§ β {π€ β π β£ π€ # πΆ}) β§ π§ β π) β (πΊβπ§) β β) |
65 | 62, 64 | addcld 7976 |
. . . . . . . . . . 11
β’ (((π β§ π§ β {π€ β π β£ π€ # πΆ}) β§ π§ β π) β ((πΉβπ§) + (πΊβπ§)) β β) |
66 | 51, 53, 57, 57, 58, 59, 60, 65 | ofvalg 6091 |
. . . . . . . . . 10
β’ (((π β§ π§ β {π€ β π β£ π€ # πΆ}) β§ π§ β π) β ((πΉ βπ + πΊ)βπ§) = ((πΉβπ§) + (πΊβπ§))) |
67 | 49, 66 | mpdan 421 |
. . . . . . . . 9
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β ((πΉ βπ + πΊ)βπ§) = ((πΉβπ§) + (πΊβπ§))) |
68 | | eqidd 2178 |
. . . . . . . . . . 11
β’ (((π β§ π§ β {π€ β π β£ π€ # πΆ}) β§ πΆ β π) β (πΉβπΆ) = (πΉβπΆ)) |
69 | | eqidd 2178 |
. . . . . . . . . . 11
β’ (((π β§ π§ β {π€ β π β£ π€ # πΆ}) β§ πΆ β π) β (πΊβπΆ) = (πΊβπΆ)) |
70 | 61 | ffvelcdmda 5651 |
. . . . . . . . . . . 12
β’ (((π β§ π§ β {π€ β π β£ π€ # πΆ}) β§ πΆ β π) β (πΉβπΆ) β β) |
71 | 63 | ffvelcdmda 5651 |
. . . . . . . . . . . 12
β’ (((π β§ π§ β {π€ β π β£ π€ # πΆ}) β§ πΆ β π) β (πΊβπΆ) β β) |
72 | 70, 71 | addcld 7976 |
. . . . . . . . . . 11
β’ (((π β§ π§ β {π€ β π β£ π€ # πΆ}) β§ πΆ β π) β ((πΉβπΆ) + (πΊβπΆ)) β β) |
73 | 51, 53, 57, 57, 58, 68, 69, 72 | ofvalg 6091 |
. . . . . . . . . 10
β’ (((π β§ π§ β {π€ β π β£ π€ # πΆ}) β§ πΆ β π) β ((πΉ βπ + πΊ)βπΆ) = ((πΉβπΆ) + (πΊβπΆ))) |
74 | 29, 73 | mpidan 423 |
. . . . . . . . 9
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β ((πΉ βπ + πΊ)βπΆ) = ((πΉβπΆ) + (πΊβπΆ))) |
75 | 67, 74 | oveq12d 5892 |
. . . . . . . 8
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β (((πΉ βπ + πΊ)βπ§) β ((πΉ βπ + πΊ)βπΆ)) = (((πΉβπ§) + (πΊβπ§)) β ((πΉβπΆ) + (πΊβπΆ)))) |
76 | | ffvelcdm 5649 |
. . . . . . . . . 10
β’ ((πΉ:πβΆβ β§ π§ β π) β (πΉβπ§) β β) |
77 | 11, 48, 76 | syl2an 289 |
. . . . . . . . 9
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β (πΉβπ§) β β) |
78 | 63, 49 | ffvelcdmd 5652 |
. . . . . . . . 9
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β (πΊβπ§) β β) |
79 | 11, 29 | ffvelcdmd 5652 |
. . . . . . . . . 10
β’ (π β (πΉβπΆ) β β) |
80 | 79 | adantr 276 |
. . . . . . . . 9
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β (πΉβπΆ) β β) |
81 | 6, 29 | ffvelcdmd 5652 |
. . . . . . . . . 10
β’ (π β (πΊβπΆ) β β) |
82 | 81 | adantr 276 |
. . . . . . . . 9
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β (πΊβπΆ) β β) |
83 | 77, 78, 80, 82 | addsub4d 8314 |
. . . . . . . 8
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β (((πΉβπ§) + (πΊβπ§)) β ((πΉβπΆ) + (πΊβπΆ))) = (((πΉβπ§) β (πΉβπΆ)) + ((πΊβπ§) β (πΊβπΆ)))) |
84 | 75, 83 | eqtrd 2210 |
. . . . . . 7
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β (((πΉ βπ + πΊ)βπ§) β ((πΉ βπ + πΊ)βπΆ)) = (((πΉβπ§) β (πΉβπΆ)) + ((πΊβπ§) β (πΊβπΆ)))) |
85 | 84 | oveq1d 5889 |
. . . . . 6
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β ((((πΉ βπ + πΊ)βπ§) β ((πΉ βπ + πΊ)βπΆ)) / (π§ β πΆ)) = ((((πΉβπ§) β (πΉβπΆ)) + ((πΊβπ§) β (πΊβπΆ))) / (π§ β πΆ))) |
86 | 61, 49 | ffvelcdmd 5652 |
. . . . . . . 8
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β (πΉβπ§) β β) |
87 | 86, 80 | subcld 8267 |
. . . . . . 7
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β ((πΉβπ§) β (πΉβπΆ)) β β) |
88 | 78, 82 | subcld 8267 |
. . . . . . 7
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β ((πΊβπ§) β (πΊβπΆ)) β β) |
89 | | ssrab2 3240 |
. . . . . . . . . 10
β’ {π€ β π β£ π€ # πΆ} β π |
90 | 89, 12 | sstrid 3166 |
. . . . . . . . 9
β’ (π β {π€ β π β£ π€ # πΆ} β β) |
91 | 90 | sselda 3155 |
. . . . . . . 8
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β π§ β β) |
92 | 12, 29 | sseldd 3156 |
. . . . . . . . 9
β’ (π β πΆ β β) |
93 | 92 | adantr 276 |
. . . . . . . 8
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β πΆ β β) |
94 | 91, 93 | subcld 8267 |
. . . . . . 7
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β (π§ β πΆ) β β) |
95 | | breq1 4006 |
. . . . . . . . . . 11
β’ (π€ = π§ β (π€ # πΆ β π§ # πΆ)) |
96 | 95 | elrab 2893 |
. . . . . . . . . 10
β’ (π§ β {π€ β π β£ π€ # πΆ} β (π§ β π β§ π§ # πΆ)) |
97 | 96 | simprbi 275 |
. . . . . . . . 9
β’ (π§ β {π€ β π β£ π€ # πΆ} β π§ # πΆ) |
98 | 97 | adantl 277 |
. . . . . . . 8
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β π§ # πΆ) |
99 | 91, 93, 98 | subap0d 8600 |
. . . . . . 7
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β (π§ β πΆ) # 0) |
100 | 87, 88, 94, 99 | divdirapd 8785 |
. . . . . 6
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β ((((πΉβπ§) β (πΉβπΆ)) + ((πΊβπ§) β (πΊβπΆ))) / (π§ β πΆ)) = ((((πΉβπ§) β (πΉβπΆ)) / (π§ β πΆ)) + (((πΊβπ§) β (πΊβπΆ)) / (π§ β πΆ)))) |
101 | 85, 100 | eqtrd 2210 |
. . . . 5
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β ((((πΉ βπ + πΊ)βπ§) β ((πΉ βπ + πΊ)βπΆ)) / (π§ β πΆ)) = ((((πΉβπ§) β (πΉβπΆ)) / (π§ β πΆ)) + (((πΊβπ§) β (πΊβπΆ)) / (π§ β πΆ)))) |
102 | 101 | mpteq2dva 4093 |
. . . 4
β’ (π β (π§ β {π€ β π β£ π€ # πΆ} β¦ ((((πΉ βπ + πΊ)βπ§) β ((πΉ βπ + πΊ)βπΆ)) / (π§ β πΆ))) = (π§ β {π€ β π β£ π€ # πΆ} β¦ ((((πΉβπ§) β (πΉβπΆ)) / (π§ β πΆ)) + (((πΊβπ§) β (πΊβπΆ)) / (π§ β πΆ))))) |
103 | 102 | oveq1d 5889 |
. . 3
β’ (π β ((π§ β {π€ β π β£ π€ # πΆ} β¦ ((((πΉ βπ + πΊ)βπ§) β ((πΉ βπ + πΊ)βπΆ)) / (π§ β πΆ))) limβ πΆ) = ((π§ β {π€ β π β£ π€ # πΆ} β¦ ((((πΉβπ§) β (πΉβπΆ)) / (π§ β πΆ)) + (((πΊβπ§) β (πΊβπΆ)) / (π§ β πΆ)))) limβ πΆ)) |
104 | 47, 103 | eleqtrrd 2257 |
. 2
β’ (π β (πΎ + πΏ) β ((π§ β {π€ β π β£ π€ # πΆ} β¦ ((((πΉ βπ + πΊ)βπ§) β ((πΉ βπ + πΊ)βπΆ)) / (π§ β πΆ))) limβ πΆ)) |
105 | | eqid 2177 |
. . 3
β’ (π§ β {π€ β π β£ π€ # πΆ} β¦ ((((πΉ βπ + πΊ)βπ§) β ((πΉ βπ + πΊ)βπΆ)) / (π§ β πΆ))) = (π§ β {π€ β π β£ π€ # πΆ} β¦ ((((πΉ βπ + πΊ)βπ§) β ((πΉ βπ + πΊ)βπΆ)) / (π§ β πΆ))) |
106 | | addcl 7935 |
. . . . 5
β’ ((π₯ β β β§ π¦ β β) β (π₯ + π¦) β β) |
107 | 106 | adantl 277 |
. . . 4
β’ ((π β§ (π₯ β β β§ π¦ β β)) β (π₯ + π¦) β β) |
108 | 107, 11, 6, 56, 56, 58 | off 6094 |
. . 3
β’ (π β (πΉ βπ + πΊ):πβΆβ) |
109 | 2, 3, 105, 5, 108, 7 | eldvap 14087 |
. 2
β’ (π β (πΆ(π D (πΉ βπ + πΊ))(πΎ + πΏ) β (πΆ β ((intβ(π½ βΎt π))βπ) β§ (πΎ + πΏ) β ((π§ β {π€ β π β£ π€ # πΆ} β¦ ((((πΉ βπ + πΊ)βπ§) β ((πΉ βπ + πΊ)βπΆ)) / (π§ β πΆ))) limβ πΆ)))) |
110 | 10, 104, 109 | mpbir2and 944 |
1
β’ (π β πΆ(π D (πΉ βπ + πΊ))(πΎ + πΏ)) |