Description: Addition is an operation on the complex numbers. This theorem can be used as an alternate axiom for complex numbers in place of the less specific axaddcl . This construction-dependent theorem should not be referenced directly; instead, use ax-addf . (Contributed by NM, 8-Feb-2005) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | axaddf | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | moeq | |
|
2 | 1 | mosubop | |
3 | 2 | mosubop | |
4 | anass | |
|
5 | 4 | 2exbii | |
6 | 19.42vv | |
|
7 | 5 6 | bitri | |
8 | 7 | 2exbii | |
9 | 8 | mobii | |
10 | 3 9 | mpbir | |
11 | 10 | moani | |
12 | 11 | funoprab | |
13 | df-add | |
|
14 | 13 | funeqi | |
15 | 12 14 | mpbir | |
16 | 13 | dmeqi | |
17 | dmoprabss | |
|
18 | 16 17 | eqsstri | |
19 | 0ncn | |
|
20 | df-c | |
|
21 | oveq1 | |
|
22 | 21 | eleq1d | |
23 | oveq2 | |
|
24 | 23 | eleq1d | |
25 | addcnsr | |
|
26 | addclsr | |
|
27 | addclsr | |
|
28 | 26 27 | anim12i | |
29 | 28 | an4s | |
30 | opelxpi | |
|
31 | 29 30 | syl | |
32 | 25 31 | eqeltrd | |
33 | 20 22 24 32 | 2optocl | |
34 | 33 20 | eleqtrrdi | |
35 | 19 34 | oprssdm | |
36 | 18 35 | eqssi | |
37 | df-fn | |
|
38 | 15 36 37 | mpbir2an | |
39 | 34 | rgen2 | |
40 | ffnov | |
|
41 | 38 39 40 | mpbir2an | |