Description: The sum of two extended nonnegative integers is 0 iff each of the two extended nonnegative integers is 0 . (Contributed by AV, 14-Dec-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | xnn0xadd0 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elxnn0 | |
|
2 | elxnn0 | |
|
3 | nn0re | |
|
4 | nn0re | |
|
5 | rexadd | |
|
6 | 3 4 5 | syl2an | |
7 | 6 | eqeq1d | |
8 | nn0ge0 | |
|
9 | 3 8 | jca | |
10 | nn0ge0 | |
|
11 | 4 10 | jca | |
12 | add20 | |
|
13 | 9 11 12 | syl2an | |
14 | 7 13 | bitrd | |
15 | 14 | biimpd | |
16 | 15 | expcom | |
17 | oveq2 | |
|
18 | 17 | eqeq1d | |
19 | 18 | adantr | |
20 | nn0xnn0 | |
|
21 | xnn0xrnemnf | |
|
22 | xaddpnf1 | |
|
23 | 20 21 22 | 3syl | |
24 | 23 | adantl | |
25 | 24 | eqeq1d | |
26 | 19 25 | bitrd | |
27 | 0re | |
|
28 | renepnf | |
|
29 | 27 28 | ax-mp | |
30 | 29 | nesymi | |
31 | 30 | pm2.21i | |
32 | 26 31 | syl6bi | |
33 | 32 | ex | |
34 | 16 33 | jaoi | |
35 | 2 34 | sylbi | |
36 | 35 | com12 | |
37 | oveq1 | |
|
38 | 37 | eqeq1d | |
39 | xnn0xrnemnf | |
|
40 | xaddpnf2 | |
|
41 | 39 40 | syl | |
42 | 41 | eqeq1d | |
43 | 38 42 | sylan9bb | |
44 | 43 31 | syl6bi | |
45 | 44 | ex | |
46 | 36 45 | jaoi | |
47 | 1 46 | sylbi | |
48 | 47 | imp | |
49 | oveq12 | |
|
50 | 0xr | |
|
51 | xaddid1 | |
|
52 | 50 51 | ax-mp | |
53 | 49 52 | eqtrdi | |
54 | 48 53 | impbid1 | |