Description: X is a subset of CC . This statement is very often used when computing derivatives. (Contributed by Glauco Siliprandi, 5-Apr-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | dvdmsscn.s | ||
dvdmsscn.x | |||
Assertion | dvdmsscn |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dvdmsscn.s | ||
2 | dvdmsscn.x | ||
3 | restsspw | ||
4 | 3 2 | sseldi | |
5 | elpwi | ||
6 | 4 5 | syl | |
7 | recnprss | ||
8 | 1 7 | syl | |
9 | 6 8 | sstrd |