Description: Poset extensionality for division. (Contributed by Stefan O'Rear, 6-Sep-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | dvdsext | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | breq1 | |
|
2 | 1 | ralrimivw | |
3 | simpll | |
|
4 | simplr | |
|
5 | nn0z | |
|
6 | iddvds | |
|
7 | 5 6 | syl | |
8 | 7 | ad2antlr | |
9 | breq2 | |
|
10 | breq2 | |
|
11 | 9 10 | bibi12d | |
12 | 11 | rspcva | |
13 | 12 | adantll | |
14 | 8 13 | mpbird | |
15 | nn0z | |
|
16 | iddvds | |
|
17 | 15 16 | syl | |
18 | 17 | ad2antrr | |
19 | breq2 | |
|
20 | breq2 | |
|
21 | 19 20 | bibi12d | |
22 | 21 | rspcva | |
23 | 22 | adantlr | |
24 | 18 23 | mpbid | |
25 | dvdseq | |
|
26 | 3 4 14 24 25 | syl22anc | |
27 | 26 | ex | |
28 | 2 27 | impbid2 | |