Metamath Proof Explorer


Theorem xnn0xadd0

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 A0*B0*A+𝑒B=0A=0B=0

Proof

Step Hyp Ref Expression
1 elxnn0 A0*A0A=+∞
2 elxnn0 B0*B0B=+∞
3 nn0re A0A
4 nn0re B0B
5 rexadd ABA+𝑒B=A+B
6 3 4 5 syl2an A0B0A+𝑒B=A+B
7 6 eqeq1d A0B0A+𝑒B=0A+B=0
8 nn0ge0 A00A
9 3 8 jca A0A0A
10 nn0ge0 B00B
11 4 10 jca B0B0B
12 add20 A0AB0BA+B=0A=0B=0
13 9 11 12 syl2an A0B0A+B=0A=0B=0
14 7 13 bitrd A0B0A+𝑒B=0A=0B=0
15 14 biimpd A0B0A+𝑒B=0A=0B=0
16 15 expcom B0A0A+𝑒B=0A=0B=0
17 oveq2 B=+∞A+𝑒B=A+𝑒+∞
18 17 eqeq1d B=+∞A+𝑒B=0A+𝑒+∞=0
19 18 adantr B=+∞A0A+𝑒B=0A+𝑒+∞=0
20 nn0xnn0 A0A0*
21 xnn0xrnemnf A0*A*A−∞
22 xaddpnf1 A*A−∞A+𝑒+∞=+∞
23 20 21 22 3syl A0A+𝑒+∞=+∞
24 23 adantl B=+∞A0A+𝑒+∞=+∞
25 24 eqeq1d B=+∞A0A+𝑒+∞=0+∞=0
26 19 25 bitrd B=+∞A0A+𝑒B=0+∞=0
27 0re 0
28 renepnf 00+∞
29 27 28 ax-mp 0+∞
30 29 nesymi ¬+∞=0
31 30 pm2.21i +∞=0A=0B=0
32 26 31 syl6bi B=+∞A0A+𝑒B=0A=0B=0
33 32 ex B=+∞A0A+𝑒B=0A=0B=0
34 16 33 jaoi B0B=+∞A0A+𝑒B=0A=0B=0
35 2 34 sylbi B0*A0A+𝑒B=0A=0B=0
36 35 com12 A0B0*A+𝑒B=0A=0B=0
37 oveq1 A=+∞A+𝑒B=+∞+𝑒B
38 37 eqeq1d A=+∞A+𝑒B=0+∞+𝑒B=0
39 xnn0xrnemnf B0*B*B−∞
40 xaddpnf2 B*B−∞+∞+𝑒B=+∞
41 39 40 syl B0*+∞+𝑒B=+∞
42 41 eqeq1d B0*+∞+𝑒B=0+∞=0
43 38 42 sylan9bb A=+∞B0*A+𝑒B=0+∞=0
44 43 31 syl6bi A=+∞B0*A+𝑒B=0A=0B=0
45 44 ex A=+∞B0*A+𝑒B=0A=0B=0
46 36 45 jaoi A0A=+∞B0*A+𝑒B=0A=0B=0
47 1 46 sylbi A0*B0*A+𝑒B=0A=0B=0
48 47 imp A0*B0*A+𝑒B=0A=0B=0
49 oveq12 A=0B=0A+𝑒B=0+𝑒0
50 0xr 0*
51 xaddid1 0*0+𝑒0=0
52 50 51 ax-mp 0+𝑒0=0
53 49 52 eqtrdi A=0B=0A+𝑒B=0
54 48 53 impbid1 A0*B0*A+𝑒B=0A=0B=0