Step | Hyp | Ref
| Expression |
1 | | inss1 4192 |
. . . . . . . 8
β’ (π΅ β© (1[,)+β)) β
π΅ |
2 | | resmpt 5995 |
. . . . . . . 8
β’ ((π΅ β© (1[,)+β)) β
π΅ β ((π¦ β π΅ β¦ π) βΎ (π΅ β© (1[,)+β))) = (π¦ β (π΅ β© (1[,)+β)) β¦ π)) |
3 | 1, 2 | mp1i 13 |
. . . . . . 7
β’ (π β ((π¦ β π΅ β¦ π) βΎ (π΅ β© (1[,)+β))) = (π¦ β (π΅ β© (1[,)+β)) β¦ π)) |
4 | | 0xr 11210 |
. . . . . . . . . . 11
β’ 0 β
β* |
5 | | 0lt1 11685 |
. . . . . . . . . . 11
β’ 0 <
1 |
6 | | df-ioo 13277 |
. . . . . . . . . . . 12
β’ (,) =
(π₯ β
β*, π¦
β β* β¦ {π§ β β* β£ (π₯ < π§ β§ π§ < π¦)}) |
7 | | df-ico 13279 |
. . . . . . . . . . . 12
β’ [,) =
(π₯ β
β*, π¦
β β* β¦ {π§ β β* β£ (π₯ β€ π§ β§ π§ < π¦)}) |
8 | | xrltletr 13085 |
. . . . . . . . . . . 12
β’ ((0
β β* β§ 1 β β* β§ π€ β β*)
β ((0 < 1 β§ 1 β€ π€) β 0 < π€)) |
9 | 6, 7, 8 | ixxss1 13291 |
. . . . . . . . . . 11
β’ ((0
β β* β§ 0 < 1) β (1[,)+β) β
(0(,)+β)) |
10 | 4, 5, 9 | mp2an 691 |
. . . . . . . . . 10
β’
(1[,)+β) β (0(,)+β) |
11 | | ioorp 13351 |
. . . . . . . . . 10
β’
(0(,)+β) = β+ |
12 | 10, 11 | sseqtri 3984 |
. . . . . . . . 9
β’
(1[,)+β) β β+ |
13 | | sslin 4198 |
. . . . . . . . 9
β’
((1[,)+β) β β+ β (π΅ β© (1[,)+β)) β (π΅ β©
β+)) |
14 | 12, 13 | ax-mp 5 |
. . . . . . . 8
β’ (π΅ β© (1[,)+β)) β
(π΅ β©
β+) |
15 | | resmpt 5995 |
. . . . . . . 8
β’ ((π΅ β© (1[,)+β)) β
(π΅ β©
β+) β ((π¦ β (π΅ β© β+) β¦ π) βΎ (π΅ β© (1[,)+β))) = (π¦ β (π΅ β© (1[,)+β)) β¦ π)) |
16 | 14, 15 | mp1i 13 |
. . . . . . 7
β’ (π β ((π¦ β (π΅ β© β+) β¦ π) βΎ (π΅ β© (1[,)+β))) = (π¦ β (π΅ β© (1[,)+β)) β¦ π)) |
17 | 3, 16 | eqtr4d 2776 |
. . . . . 6
β’ (π β ((π¦ β π΅ β¦ π) βΎ (π΅ β© (1[,)+β))) = ((π¦ β (π΅ β© β+) β¦ π) βΎ (π΅ β© (1[,)+β)))) |
18 | | resres 5954 |
. . . . . 6
β’ (((π¦ β π΅ β¦ π) βΎ π΅) βΎ (1[,)+β)) = ((π¦ β π΅ β¦ π) βΎ (π΅ β© (1[,)+β))) |
19 | | resres 5954 |
. . . . . 6
β’ (((π¦ β (π΅ β© β+) β¦ π) βΎ π΅) βΎ (1[,)+β)) = ((π¦ β (π΅ β© β+) β¦ π) βΎ (π΅ β© (1[,)+β))) |
20 | 17, 18, 19 | 3eqtr4g 2798 |
. . . . 5
β’ (π β (((π¦ β π΅ β¦ π) βΎ π΅) βΎ (1[,)+β)) = (((π¦ β (π΅ β© β+) β¦ π) βΎ π΅) βΎ (1[,)+β))) |
21 | | rlimcnp2.r |
. . . . . . . . 9
β’ ((π β§ π¦ β π΅) β π β β) |
22 | 21 | fmpttd 7067 |
. . . . . . . 8
β’ (π β (π¦ β π΅ β¦ π):π΅βΆβ) |
23 | 22 | ffnd 6673 |
. . . . . . 7
β’ (π β (π¦ β π΅ β¦ π) Fn π΅) |
24 | | fnresdm 6624 |
. . . . . . 7
β’ ((π¦ β π΅ β¦ π) Fn π΅ β ((π¦ β π΅ β¦ π) βΎ π΅) = (π¦ β π΅ β¦ π)) |
25 | 23, 24 | syl 17 |
. . . . . 6
β’ (π β ((π¦ β π΅ β¦ π) βΎ π΅) = (π¦ β π΅ β¦ π)) |
26 | 25 | reseq1d 5940 |
. . . . 5
β’ (π β (((π¦ β π΅ β¦ π) βΎ π΅) βΎ (1[,)+β)) = ((π¦ β π΅ β¦ π) βΎ (1[,)+β))) |
27 | | elinel1 4159 |
. . . . . . . . . 10
β’ (π¦ β (π΅ β© β+) β π¦ β π΅) |
28 | 27, 21 | sylan2 594 |
. . . . . . . . 9
β’ ((π β§ π¦ β (π΅ β© β+)) β π β
β) |
29 | 28 | fmpttd 7067 |
. . . . . . . 8
β’ (π β (π¦ β (π΅ β© β+) β¦ π):(π΅ β©
β+)βΆβ) |
30 | | frel 6677 |
. . . . . . . 8
β’ ((π¦ β (π΅ β© β+) β¦ π):(π΅ β© β+)βΆβ
β Rel (π¦ β (π΅ β© β+)
β¦ π)) |
31 | 29, 30 | syl 17 |
. . . . . . 7
β’ (π β Rel (π¦ β (π΅ β© β+) β¦ π)) |
32 | | eqid 2733 |
. . . . . . . . 9
β’ (π¦ β (π΅ β© β+) β¦ π) = (π¦ β (π΅ β© β+) β¦ π) |
33 | 32, 28 | dmmptd 6650 |
. . . . . . . 8
β’ (π β dom (π¦ β (π΅ β© β+) β¦ π) = (π΅ β©
β+)) |
34 | | inss1 4192 |
. . . . . . . 8
β’ (π΅ β© β+)
β π΅ |
35 | 33, 34 | eqsstrdi 4002 |
. . . . . . 7
β’ (π β dom (π¦ β (π΅ β© β+) β¦ π) β π΅) |
36 | | relssres 5982 |
. . . . . . 7
β’ ((Rel
(π¦ β (π΅ β© β+)
β¦ π) β§ dom (π¦ β (π΅ β© β+) β¦ π) β π΅) β ((π¦ β (π΅ β© β+) β¦ π) βΎ π΅) = (π¦ β (π΅ β© β+) β¦ π)) |
37 | 31, 35, 36 | syl2anc 585 |
. . . . . 6
β’ (π β ((π¦ β (π΅ β© β+) β¦ π) βΎ π΅) = (π¦ β (π΅ β© β+) β¦ π)) |
38 | 37 | reseq1d 5940 |
. . . . 5
β’ (π β (((π¦ β (π΅ β© β+) β¦ π) βΎ π΅) βΎ (1[,)+β)) = ((π¦ β (π΅ β© β+) β¦ π) βΎ
(1[,)+β))) |
39 | 20, 26, 38 | 3eqtr3d 2781 |
. . . 4
β’ (π β ((π¦ β π΅ β¦ π) βΎ (1[,)+β)) = ((π¦ β (π΅ β© β+) β¦ π) βΎ
(1[,)+β))) |
40 | 39 | breq1d 5119 |
. . 3
β’ (π β (((π¦ β π΅ β¦ π) βΎ (1[,)+β))
βπ πΆ β ((π¦ β (π΅ β© β+) β¦ π) βΎ (1[,)+β))
βπ πΆ)) |
41 | | rlimcnp2.b |
. . . 4
β’ (π β π΅ β β) |
42 | | 1red 11164 |
. . . 4
β’ (π β 1 β
β) |
43 | 22, 41, 42 | rlimresb 15456 |
. . 3
β’ (π β ((π¦ β π΅ β¦ π) βπ πΆ β ((π¦ β π΅ β¦ π) βΎ (1[,)+β))
βπ πΆ)) |
44 | 34, 41 | sstrid 3959 |
. . . 4
β’ (π β (π΅ β© β+) β
β) |
45 | 29, 44, 42 | rlimresb 15456 |
. . 3
β’ (π β ((π¦ β (π΅ β© β+) β¦ π) βπ
πΆ β ((π¦ β (π΅ β© β+) β¦ π) βΎ (1[,)+β))
βπ πΆ)) |
46 | 40, 43, 45 | 3bitr4d 311 |
. 2
β’ (π β ((π¦ β π΅ β¦ π) βπ πΆ β (π¦ β (π΅ β© β+) β¦ π) βπ
πΆ)) |
47 | | inss2 4193 |
. . . . . . . . . . 11
β’ (π΅ β© β+)
β β+ |
48 | 47 | a1i 11 |
. . . . . . . . . 10
β’ (π β (π΅ β© β+) β
β+) |
49 | 48 | sselda 3948 |
. . . . . . . . 9
β’ ((π β§ π¦ β (π΅ β© β+)) β π¦ β
β+) |
50 | 49 | rpreccld 12975 |
. . . . . . . 8
β’ ((π β§ π¦ β (π΅ β© β+)) β (1 /
π¦) β
β+) |
51 | 50 | rpne0d 12970 |
. . . . . . 7
β’ ((π β§ π¦ β (π΅ β© β+)) β (1 /
π¦) β 0) |
52 | 51 | neneqd 2945 |
. . . . . 6
β’ ((π β§ π¦ β (π΅ β© β+)) β Β¬ (1
/ π¦) = 0) |
53 | 52 | iffalsed 4501 |
. . . . 5
β’ ((π β§ π¦ β (π΅ β© β+)) β if((1 /
π¦) = 0, πΆ, β¦(1 / π¦) / π₯β¦π
) = β¦(1 / π¦) / π₯β¦π
) |
54 | | oveq2 7369 |
. . . . . . . . . 10
β’ (π₯ = (1 / π¦) β (1 / π₯) = (1 / (1 / π¦))) |
55 | | rpcnne0 12941 |
. . . . . . . . . . 11
β’ (π¦ β β+
β (π¦ β β
β§ π¦ β
0)) |
56 | | recrec 11860 |
. . . . . . . . . . 11
β’ ((π¦ β β β§ π¦ β 0) β (1 / (1 / π¦)) = π¦) |
57 | 49, 55, 56 | 3syl 18 |
. . . . . . . . . 10
β’ ((π β§ π¦ β (π΅ β© β+)) β (1 / (1
/ π¦)) = π¦) |
58 | 54, 57 | sylan9eqr 2795 |
. . . . . . . . 9
β’ (((π β§ π¦ β (π΅ β© β+)) β§ π₯ = (1 / π¦)) β (1 / π₯) = π¦) |
59 | 58 | eqcomd 2739 |
. . . . . . . 8
β’ (((π β§ π¦ β (π΅ β© β+)) β§ π₯ = (1 / π¦)) β π¦ = (1 / π₯)) |
60 | | rlimcnp2.s |
. . . . . . . 8
β’ (π¦ = (1 / π₯) β π = π
) |
61 | 59, 60 | syl 17 |
. . . . . . 7
β’ (((π β§ π¦ β (π΅ β© β+)) β§ π₯ = (1 / π¦)) β π = π
) |
62 | 61 | eqcomd 2739 |
. . . . . 6
β’ (((π β§ π¦ β (π΅ β© β+)) β§ π₯ = (1 / π¦)) β π
= π) |
63 | 50, 62 | csbied 3897 |
. . . . 5
β’ ((π β§ π¦ β (π΅ β© β+)) β
β¦(1 / π¦) /
π₯β¦π
= π) |
64 | 53, 63 | eqtrd 2773 |
. . . 4
β’ ((π β§ π¦ β (π΅ β© β+)) β if((1 /
π¦) = 0, πΆ, β¦(1 / π¦) / π₯β¦π
) = π) |
65 | 64 | mpteq2dva 5209 |
. . 3
β’ (π β (π¦ β (π΅ β© β+) β¦ if((1 /
π¦) = 0, πΆ, β¦(1 / π¦) / π₯β¦π
)) = (π¦ β (π΅ β© β+) β¦ π)) |
66 | 65 | breq1d 5119 |
. 2
β’ (π β ((π¦ β (π΅ β© β+) β¦ if((1 /
π¦) = 0, πΆ, β¦(1 / π¦) / π₯β¦π
)) βπ πΆ β (π¦ β (π΅ β© β+) β¦ π) βπ
πΆ)) |
67 | | rlimcnp2.a |
. . . 4
β’ (π β π΄ β (0[,)+β)) |
68 | | rlimcnp2.0 |
. . . 4
β’ (π β 0 β π΄) |
69 | | rlimcnp2.c |
. . . . . 6
β’ (π β πΆ β β) |
70 | 69 | ad2antrr 725 |
. . . . 5
β’ (((π β§ π€ β π΄) β§ π€ = 0) β πΆ β β) |
71 | 67 | sselda 3948 |
. . . . . . . . . . . 12
β’ ((π β§ π€ β π΄) β π€ β (0[,)+β)) |
72 | | 0re 11165 |
. . . . . . . . . . . . 13
β’ 0 β
β |
73 | | pnfxr 11217 |
. . . . . . . . . . . . 13
β’ +β
β β* |
74 | | elico2 13337 |
. . . . . . . . . . . . 13
β’ ((0
β β β§ +β β β*) β (π€ β (0[,)+β) β
(π€ β β β§ 0
β€ π€ β§ π€ <
+β))) |
75 | 72, 73, 74 | mp2an 691 |
. . . . . . . . . . . 12
β’ (π€ β (0[,)+β) β
(π€ β β β§ 0
β€ π€ β§ π€ <
+β)) |
76 | 71, 75 | sylib 217 |
. . . . . . . . . . 11
β’ ((π β§ π€ β π΄) β (π€ β β β§ 0 β€ π€ β§ π€ < +β)) |
77 | 76 | simp1d 1143 |
. . . . . . . . . 10
β’ ((π β§ π€ β π΄) β π€ β β) |
78 | 77 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ π€ β π΄) β§ Β¬ π€ = 0) β π€ β β) |
79 | 76 | simp2d 1144 |
. . . . . . . . . . . . . 14
β’ ((π β§ π€ β π΄) β 0 β€ π€) |
80 | | leloe 11249 |
. . . . . . . . . . . . . . 15
β’ ((0
β β β§ π€
β β) β (0 β€ π€ β (0 < π€ β¨ 0 = π€))) |
81 | 72, 77, 80 | sylancr 588 |
. . . . . . . . . . . . . 14
β’ ((π β§ π€ β π΄) β (0 β€ π€ β (0 < π€ β¨ 0 = π€))) |
82 | 79, 81 | mpbid 231 |
. . . . . . . . . . . . 13
β’ ((π β§ π€ β π΄) β (0 < π€ β¨ 0 = π€)) |
83 | 82 | ord 863 |
. . . . . . . . . . . 12
β’ ((π β§ π€ β π΄) β (Β¬ 0 < π€ β 0 = π€)) |
84 | | eqcom 2740 |
. . . . . . . . . . . 12
β’ (0 =
π€ β π€ = 0) |
85 | 83, 84 | syl6ib 251 |
. . . . . . . . . . 11
β’ ((π β§ π€ β π΄) β (Β¬ 0 < π€ β π€ = 0)) |
86 | 85 | con1d 145 |
. . . . . . . . . 10
β’ ((π β§ π€ β π΄) β (Β¬ π€ = 0 β 0 < π€)) |
87 | 86 | imp 408 |
. . . . . . . . 9
β’ (((π β§ π€ β π΄) β§ Β¬ π€ = 0) β 0 < π€) |
88 | 78, 87 | elrpd 12962 |
. . . . . . . 8
β’ (((π β§ π€ β π΄) β§ Β¬ π€ = 0) β π€ β β+) |
89 | | rpcnne0 12941 |
. . . . . . . . 9
β’ (π€ β β+
β (π€ β β
β§ π€ β
0)) |
90 | | recrec 11860 |
. . . . . . . . 9
β’ ((π€ β β β§ π€ β 0) β (1 / (1 / π€)) = π€) |
91 | 89, 90 | syl 17 |
. . . . . . . 8
β’ (π€ β β+
β (1 / (1 / π€)) =
π€) |
92 | 88, 91 | syl 17 |
. . . . . . 7
β’ (((π β§ π€ β π΄) β§ Β¬ π€ = 0) β (1 / (1 / π€)) = π€) |
93 | 92 | csbeq1d 3863 |
. . . . . 6
β’ (((π β§ π€ β π΄) β§ Β¬ π€ = 0) β β¦(1 / (1 / π€)) / π₯β¦π
= β¦π€ / π₯β¦π
) |
94 | | oveq2 7369 |
. . . . . . . . 9
β’ (π¦ = (1 / π€) β (1 / π¦) = (1 / (1 / π€))) |
95 | 94 | csbeq1d 3863 |
. . . . . . . 8
β’ (π¦ = (1 / π€) β β¦(1 / π¦) / π₯β¦π
= β¦(1 / (1 / π€)) / π₯β¦π
) |
96 | 95 | eleq1d 2819 |
. . . . . . 7
β’ (π¦ = (1 / π€) β (β¦(1 / π¦) / π₯β¦π
β β β β¦(1 /
(1 / π€)) / π₯β¦π
β β)) |
97 | 63, 28 | eqeltrd 2834 |
. . . . . . . . 9
β’ ((π β§ π¦ β (π΅ β© β+)) β
β¦(1 / π¦) /
π₯β¦π
β
β) |
98 | 97 | ralrimiva 3140 |
. . . . . . . 8
β’ (π β βπ¦ β (π΅ β© β+)β¦(1
/ π¦) / π₯β¦π
β β) |
99 | 98 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π€ β π΄) β§ Β¬ π€ = 0) β βπ¦ β (π΅ β© β+)β¦(1
/ π¦) / π₯β¦π
β β) |
100 | | simplr 768 |
. . . . . . . . 9
β’ (((π β§ π€ β π΄) β§ Β¬ π€ = 0) β π€ β π΄) |
101 | | simpll 766 |
. . . . . . . . . 10
β’ (((π β§ π€ β π΄) β§ Β¬ π€ = 0) β π) |
102 | | eleq1 2822 |
. . . . . . . . . . . . 13
β’ (π¦ = (1 / π€) β (π¦ β π΅ β (1 / π€) β π΅)) |
103 | 94 | eleq1d 2819 |
. . . . . . . . . . . . 13
β’ (π¦ = (1 / π€) β ((1 / π¦) β π΄ β (1 / (1 / π€)) β π΄)) |
104 | 102, 103 | bibi12d 346 |
. . . . . . . . . . . 12
β’ (π¦ = (1 / π€) β ((π¦ β π΅ β (1 / π¦) β π΄) β ((1 / π€) β π΅ β (1 / (1 / π€)) β π΄))) |
105 | | rlimcnp2.d |
. . . . . . . . . . . . . 14
β’ ((π β§ π¦ β β+) β (π¦ β π΅ β (1 / π¦) β π΄)) |
106 | 105 | ralrimiva 3140 |
. . . . . . . . . . . . 13
β’ (π β βπ¦ β β+ (π¦ β π΅ β (1 / π¦) β π΄)) |
107 | 106 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π€ β β+) β
βπ¦ β
β+ (π¦
β π΅ β (1 / π¦) β π΄)) |
108 | | rpreccl 12949 |
. . . . . . . . . . . . 13
β’ (π€ β β+
β (1 / π€) β
β+) |
109 | 108 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β§ π€ β β+) β (1 /
π€) β
β+) |
110 | 104, 107,
109 | rspcdva 3584 |
. . . . . . . . . . 11
β’ ((π β§ π€ β β+) β ((1 /
π€) β π΅ β (1 / (1 / π€)) β π΄)) |
111 | 91 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β§ π€ β β+) β (1 / (1 /
π€)) = π€) |
112 | 111 | eleq1d 2819 |
. . . . . . . . . . 11
β’ ((π β§ π€ β β+) β ((1 / (1
/ π€)) β π΄ β π€ β π΄)) |
113 | 110, 112 | bitr2d 280 |
. . . . . . . . . 10
β’ ((π β§ π€ β β+) β (π€ β π΄ β (1 / π€) β π΅)) |
114 | 101, 88, 113 | syl2anc 585 |
. . . . . . . . 9
β’ (((π β§ π€ β π΄) β§ Β¬ π€ = 0) β (π€ β π΄ β (1 / π€) β π΅)) |
115 | 100, 114 | mpbid 231 |
. . . . . . . 8
β’ (((π β§ π€ β π΄) β§ Β¬ π€ = 0) β (1 / π€) β π΅) |
116 | 88 | rpreccld 12975 |
. . . . . . . 8
β’ (((π β§ π€ β π΄) β§ Β¬ π€ = 0) β (1 / π€) β
β+) |
117 | 115, 116 | elind 4158 |
. . . . . . 7
β’ (((π β§ π€ β π΄) β§ Β¬ π€ = 0) β (1 / π€) β (π΅ β©
β+)) |
118 | 96, 99, 117 | rspcdva 3584 |
. . . . . 6
β’ (((π β§ π€ β π΄) β§ Β¬ π€ = 0) β β¦(1 / (1 / π€)) / π₯β¦π
β β) |
119 | 93, 118 | eqeltrrd 2835 |
. . . . 5
β’ (((π β§ π€ β π΄) β§ Β¬ π€ = 0) β β¦π€ / π₯β¦π
β β) |
120 | 70, 119 | ifclda 4525 |
. . . 4
β’ ((π β§ π€ β π΄) β if(π€ = 0, πΆ, β¦π€ / π₯β¦π
) β β) |
121 | 109 | biantrud 533 |
. . . . . 6
β’ ((π β§ π€ β β+) β ((1 /
π€) β π΅ β ((1 / π€) β π΅ β§ (1 / π€) β
β+))) |
122 | 113, 121 | bitrd 279 |
. . . . 5
β’ ((π β§ π€ β β+) β (π€ β π΄ β ((1 / π€) β π΅ β§ (1 / π€) β
β+))) |
123 | | elin 3930 |
. . . . 5
β’ ((1 /
π€) β (π΅ β© β+)
β ((1 / π€) β
π΅ β§ (1 / π€) β
β+)) |
124 | 122, 123 | bitr4di 289 |
. . . 4
β’ ((π β§ π€ β β+) β (π€ β π΄ β (1 / π€) β (π΅ β©
β+))) |
125 | | iftrue 4496 |
. . . 4
β’ (π€ = 0 β if(π€ = 0, πΆ, β¦π€ / π₯β¦π
) = πΆ) |
126 | | eqeq1 2737 |
. . . . 5
β’ (π€ = (1 / π¦) β (π€ = 0 β (1 / π¦) = 0)) |
127 | | csbeq1 3862 |
. . . . 5
β’ (π€ = (1 / π¦) β β¦π€ / π₯β¦π
= β¦(1 / π¦) / π₯β¦π
) |
128 | 126, 127 | ifbieq2d 4516 |
. . . 4
β’ (π€ = (1 / π¦) β if(π€ = 0, πΆ, β¦π€ / π₯β¦π
) = if((1 / π¦) = 0, πΆ, β¦(1 / π¦) / π₯β¦π
)) |
129 | | rlimcnp2.j |
. . . 4
β’ π½ =
(TopOpenββfld) |
130 | | rlimcnp2.k |
. . . 4
β’ πΎ = (π½ βΎt π΄) |
131 | 67, 68, 48, 120, 124, 125, 128, 129, 130 | rlimcnp 26338 |
. . 3
β’ (π β ((π¦ β (π΅ β© β+) β¦ if((1 /
π¦) = 0, πΆ, β¦(1 / π¦) / π₯β¦π
)) βπ πΆ β (π€ β π΄ β¦ if(π€ = 0, πΆ, β¦π€ / π₯β¦π
)) β ((πΎ CnP π½)β0))) |
132 | | nfcv 2904 |
. . . . 5
β’
β²π€if(π₯ = 0, πΆ, π
) |
133 | | nfv 1918 |
. . . . . 6
β’
β²π₯ π€ = 0 |
134 | | nfcv 2904 |
. . . . . 6
β’
β²π₯πΆ |
135 | | nfcsb1v 3884 |
. . . . . 6
β’
β²π₯β¦π€ / π₯β¦π
|
136 | 133, 134,
135 | nfif 4520 |
. . . . 5
β’
β²π₯if(π€ = 0, πΆ, β¦π€ / π₯β¦π
) |
137 | | eqeq1 2737 |
. . . . . 6
β’ (π₯ = π€ β (π₯ = 0 β π€ = 0)) |
138 | | csbeq1a 3873 |
. . . . . 6
β’ (π₯ = π€ β π
= β¦π€ / π₯β¦π
) |
139 | 137, 138 | ifbieq2d 4516 |
. . . . 5
β’ (π₯ = π€ β if(π₯ = 0, πΆ, π
) = if(π€ = 0, πΆ, β¦π€ / π₯β¦π
)) |
140 | 132, 136,
139 | cbvmpt 5220 |
. . . 4
β’ (π₯ β π΄ β¦ if(π₯ = 0, πΆ, π
)) = (π€ β π΄ β¦ if(π€ = 0, πΆ, β¦π€ / π₯β¦π
)) |
141 | 140 | eleq1i 2825 |
. . 3
β’ ((π₯ β π΄ β¦ if(π₯ = 0, πΆ, π
)) β ((πΎ CnP π½)β0) β (π€ β π΄ β¦ if(π€ = 0, πΆ, β¦π€ / π₯β¦π
)) β ((πΎ CnP π½)β0)) |
142 | 131, 141 | bitr4di 289 |
. 2
β’ (π β ((π¦ β (π΅ β© β+) β¦ if((1 /
π¦) = 0, πΆ, β¦(1 / π¦) / π₯β¦π
)) βπ πΆ β (π₯ β π΄ β¦ if(π₯ = 0, πΆ, π
)) β ((πΎ CnP π½)β0))) |
143 | 46, 66, 142 | 3bitr2d 307 |
1
β’ (π β ((π¦ β π΅ β¦ π) βπ πΆ β (π₯ β π΄ β¦ if(π₯ = 0, πΆ, π
)) β ((πΎ CnP π½)β0))) |