| Step | Hyp | Ref
| Expression |
|---|
| 1 | | dvcnp.g |
. 2
β’ πΊ = (π§ β π΄ β¦ if(π§ = π΅, ((π D πΉ)βπ΅), (((πΉβπ§) β (πΉβπ΅)) / (π§ β π΅)))) |
| 2 | | dvfg 25647 |
. . . . . . 7
β’ (π β {β, β}
β (π D πΉ):dom (π D πΉ)βΆβ) |
| 3 | 2 | 3ad2ant1 1133 |
. . . . . 6
β’ ((π β {β, β} β§
πΉ:π΄βΆβ β§ π΄ β π) β (π D πΉ):dom (π D πΉ)βΆβ) |
| 4 | | ffun 6720 |
. . . . . 6
β’ ((π D πΉ):dom (π D πΉ)βΆβ β Fun (π D πΉ)) |
| 5 | | funfvbrb 7052 |
. . . . . 6
β’ (Fun
(π D πΉ) β (π΅ β dom (π D πΉ) β π΅(π D πΉ)((π D πΉ)βπ΅))) |
| 6 | 3, 4, 5 | 3syl 18 |
. . . . 5
β’ ((π β {β, β} β§
πΉ:π΄βΆβ β§ π΄ β π) β (π΅ β dom (π D πΉ) β π΅(π D πΉ)((π D πΉ)βπ΅))) |
| 7 | | eqid 2732 |
. . . . . 6
β’ (πΎ βΎt π) = (πΎ βΎt π) |
| 8 | | dvcnp.k |
. . . . . 6
β’ πΎ =
(TopOpenββfld) |
| 9 | | eqid 2732 |
. . . . . 6
β’ (π§ β (π΄ β {π΅}) β¦ (((πΉβπ§) β (πΉβπ΅)) / (π§ β π΅))) = (π§ β (π΄ β {π΅}) β¦ (((πΉβπ§) β (πΉβπ΅)) / (π§ β π΅))) |
| 10 | | recnprss 25645 |
. . . . . . 7
β’ (π β {β, β}
β π β
β) |
| 11 | 10 | 3ad2ant1 1133 |
. . . . . 6
β’ ((π β {β, β} β§
πΉ:π΄βΆβ β§ π΄ β π) β π β β) |
| 12 | | simp2 1137 |
. . . . . 6
β’ ((π β {β, β} β§
πΉ:π΄βΆβ β§ π΄ β π) β πΉ:π΄βΆβ) |
| 13 | | simp3 1138 |
. . . . . 6
β’ ((π β {β, β} β§
πΉ:π΄βΆβ β§ π΄ β π) β π΄ β π) |
| 14 | 7, 8, 9, 11, 12, 13 | eldv 25639 |
. . . . 5
β’ ((π β {β, β} β§
πΉ:π΄βΆβ β§ π΄ β π) β (π΅(π D πΉ)((π D πΉ)βπ΅) β (π΅ β ((intβ(πΎ βΎt π))βπ΄) β§ ((π D πΉ)βπ΅) β ((π§ β (π΄ β {π΅}) β¦ (((πΉβπ§) β (πΉβπ΅)) / (π§ β π΅))) limβ π΅)))) |
| 15 | 6, 14 | bitrd 278 |
. . . 4
β’ ((π β {β, β} β§
πΉ:π΄βΆβ β§ π΄ β π) β (π΅ β dom (π D πΉ) β (π΅ β ((intβ(πΎ βΎt π))βπ΄) β§ ((π D πΉ)βπ΅) β ((π§ β (π΄ β {π΅}) β¦ (((πΉβπ§) β (πΉβπ΅)) / (π§ β π΅))) limβ π΅)))) |
| 16 | 15 | simplbda 500 |
. . 3
β’ (((π β {β, β} β§
πΉ:π΄βΆβ β§ π΄ β π) β§ π΅ β dom (π D πΉ)) β ((π D πΉ)βπ΅) β ((π§ β (π΄ β {π΅}) β¦ (((πΉβπ§) β (πΉβπ΅)) / (π§ β π΅))) limβ π΅)) |
| 17 | 13, 11 | sstrd 3992 |
. . . . 5
β’ ((π β {β, β} β§
πΉ:π΄βΆβ β§ π΄ β π) β π΄ β β) |
| 18 | 17 | adantr 481 |
. . . 4
β’ (((π β {β, β} β§
πΉ:π΄βΆβ β§ π΄ β π) β§ π΅ β dom (π D πΉ)) β π΄ β β) |
| 19 | 11, 12, 13 | dvbss 25642 |
. . . . 5
β’ ((π β {β, β} β§
πΉ:π΄βΆβ β§ π΄ β π) β dom (π D πΉ) β π΄) |
| 20 | 19 | sselda 3982 |
. . . 4
β’ (((π β {β, β} β§
πΉ:π΄βΆβ β§ π΄ β π) β§ π΅ β dom (π D πΉ)) β π΅ β π΄) |
| 21 | | eldifsn 4790 |
. . . . 5
β’ (π§ β (π΄ β {π΅}) β (π§ β π΄ β§ π§ β π΅)) |
| 22 | 12 | adantr 481 |
. . . . . 6
β’ (((π β {β, β} β§
πΉ:π΄βΆβ β§ π΄ β π) β§ π΅ β dom (π D πΉ)) β πΉ:π΄βΆβ) |
| 23 | 22, 18, 20 | dvlem 25637 |
. . . . 5
β’ ((((π β {β, β} β§
πΉ:π΄βΆβ β§ π΄ β π) β§ π΅ β dom (π D πΉ)) β§ π§ β (π΄ β {π΅})) β (((πΉβπ§) β (πΉβπ΅)) / (π§ β π΅)) β β) |
| 24 | 21, 23 | sylan2br 595 |
. . . 4
β’ ((((π β {β, β} β§
πΉ:π΄βΆβ β§ π΄ β π) β§ π΅ β dom (π D πΉ)) β§ (π§ β π΄ β§ π§ β π΅)) β (((πΉβπ§) β (πΉβπ΅)) / (π§ β π΅)) β β) |
| 25 | | dvcnp.j |
. . . 4
β’ π½ = (πΎ βΎt π΄) |
| 26 | 18, 20, 24, 25, 8 | limcmpt2 25625 |
. . 3
β’ (((π β {β, β} β§
πΉ:π΄βΆβ β§ π΄ β π) β§ π΅ β dom (π D πΉ)) β (((π D πΉ)βπ΅) β ((π§ β (π΄ β {π΅}) β¦ (((πΉβπ§) β (πΉβπ΅)) / (π§ β π΅))) limβ π΅) β (π§ β π΄ β¦ if(π§ = π΅, ((π D πΉ)βπ΅), (((πΉβπ§) β (πΉβπ΅)) / (π§ β π΅)))) β ((π½ CnP πΎ)βπ΅))) |
| 27 | 16, 26 | mpbid 231 |
. 2
β’ (((π β {β, β} β§
πΉ:π΄βΆβ β§ π΄ β π) β§ π΅ β dom (π D πΉ)) β (π§ β π΄ β¦ if(π§ = π΅, ((π D πΉ)βπ΅), (((πΉβπ§) β (πΉβπ΅)) / (π§ β π΅)))) β ((π½ CnP πΎ)βπ΅)) |
| 28 | 1, 27 | eqeltrid 2837 |
1
β’ (((π β {β, β} β§
πΉ:π΄βΆβ β§ π΄ β π) β§ π΅ β dom (π D πΉ)) β πΊ β ((π½ CnP πΎ)βπ΅)) |
