Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > addclnq | Unicode version |
Description: Closure of addition on positive fractions. (Contributed by NM, 29-Aug-1995.) |
Ref | Expression |
---|---|
addclnq |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-nqqs 7297 | . . 3 | |
2 | oveq1 5857 | . . . 4 | |
3 | 2 | eleq1d 2239 | . . 3 |
4 | oveq2 5858 | . . . 4 | |
5 | 4 | eleq1d 2239 | . . 3 |
6 | addpipqqs 7319 | . . . 4 | |
7 | mulclpi 7277 | . . . . . . . 8 | |
8 | mulclpi 7277 | . . . . . . . 8 | |
9 | addclpi 7276 | . . . . . . . 8 | |
10 | 7, 8, 9 | syl2an 287 | . . . . . . 7 |
11 | 10 | an42s 584 | . . . . . 6 |
12 | mulclpi 7277 | . . . . . . 7 | |
13 | 12 | ad2ant2l 505 | . . . . . 6 |
14 | 11, 13 | jca 304 | . . . . 5 |
15 | opelxpi 4641 | . . . . 5 | |
16 | enqex 7309 | . . . . . 6 | |
17 | 16 | ecelqsi 6563 | . . . . 5 |
18 | 14, 15, 17 | 3syl 17 | . . . 4 |
19 | 6, 18 | eqeltrd 2247 | . . 3 |
20 | 1, 3, 5, 19 | 2ecoptocl 6597 | . 2 |
21 | 20, 1 | eleqtrrdi 2264 | 1 |
Copyright terms: Public domain | W3C validator |