This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ ℕ0* ∧ 𝐵 ∈ ℕ0* ) → ( ( 𝐴 +𝑒 𝐵 ) = 0 ↔ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) )

Proof

Step Hyp Ref Expression
1 elxnn0 ⊢ ( 𝐴 ∈ ℕ0* ↔ ( 𝐴 ∈ ℕ0 ∨ 𝐴 = +∞ ) )
2 elxnn0 ⊢ ( 𝐵 ∈ ℕ0* ↔ ( 𝐵 ∈ ℕ0 ∨ 𝐵 = +∞ ) )
3 nn0re ⊢ ( 𝐴 ∈ ℕ0 → 𝐴 ∈ ℝ )
4 nn0re ⊢ ( 𝐵 ∈ ℕ0 → 𝐵 ∈ ℝ )
5 rexadd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 +𝑒 𝐵 ) = ( 𝐴 + 𝐵 ) )
6 3 4 5 syl2an ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( 𝐴 +𝑒 𝐵 ) = ( 𝐴 + 𝐵 ) )
7 6 eqeq1d ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( ( 𝐴 +𝑒 𝐵 ) = 0 ↔ ( 𝐴 + 𝐵 ) = 0 ) )
8 nn0ge0 ⊢ ( 𝐴 ∈ ℕ0 → 0 ≤ 𝐴 )
9 3 8 jca ⊢ ( 𝐴 ∈ ℕ0 → ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) )
10 nn0ge0 ⊢ ( 𝐵 ∈ ℕ0 → 0 ≤ 𝐵 )
11 4 10 jca ⊢ ( 𝐵 ∈ ℕ0 → ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) )
12 add20 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( ( 𝐴 + 𝐵 ) = 0 ↔ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) )
13 9 11 12 syl2an ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( ( 𝐴 + 𝐵 ) = 0 ↔ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) )
14 7 13 bitrd ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( ( 𝐴 +𝑒 𝐵 ) = 0 ↔ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) )
15 14 biimpd ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( ( 𝐴 +𝑒 𝐵 ) = 0 → ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) )
16 15 expcom ⊢ ( 𝐵 ∈ ℕ0 → ( 𝐴 ∈ ℕ0 → ( ( 𝐴 +𝑒 𝐵 ) = 0 → ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) ) )
17 oveq2 ⊢ ( 𝐵 = +∞ → ( 𝐴 +𝑒 𝐵 ) = ( 𝐴 +𝑒 +∞ ) )
18 17 eqeq1d ⊢ ( 𝐵 = +∞ → ( ( 𝐴 +𝑒 𝐵 ) = 0 ↔ ( 𝐴 +𝑒 +∞ ) = 0 ) )
19 18 adantr ⊢ ( ( 𝐵 = +∞ ∧ 𝐴 ∈ ℕ0 ) → ( ( 𝐴 +𝑒 𝐵 ) = 0 ↔ ( 𝐴 +𝑒 +∞ ) = 0 ) )
20 nn0xnn0 ⊢ ( 𝐴 ∈ ℕ0 → 𝐴 ∈ ℕ0* )
21 xnn0xrnemnf ⊢ ( 𝐴 ∈ ℕ0* → ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞ ) )
22 xaddpnf1 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞ ) → ( 𝐴 +𝑒 +∞ ) = +∞ )
23 20 21 22 3syl ⊢ ( 𝐴 ∈ ℕ0 → ( 𝐴 +𝑒 +∞ ) = +∞ )
24 23 adantl ⊢ ( ( 𝐵 = +∞ ∧ 𝐴 ∈ ℕ0 ) → ( 𝐴 +𝑒 +∞ ) = +∞ )
25 24 eqeq1d ⊢ ( ( 𝐵 = +∞ ∧ 𝐴 ∈ ℕ0 ) → ( ( 𝐴 +𝑒 +∞ ) = 0 ↔ +∞ = 0 ) )
26 19 25 bitrd ⊢ ( ( 𝐵 = +∞ ∧ 𝐴 ∈ ℕ0 ) → ( ( 𝐴 +𝑒 𝐵 ) = 0 ↔ +∞ = 0 ) )
27 0re ⊢ 0 ∈ ℝ
28 renepnf ⊢ ( 0 ∈ ℝ → 0 ≠ +∞ )
29 27 28 ax-mp ⊢ 0 ≠ +∞
30 29 nesymi ⊢ ¬ +∞ = 0
31 30 pm2.21i ⊢ ( +∞ = 0 → ( 𝐴 = 0 ∧ 𝐵 = 0 ) )
32 26 31 biimtrdi ⊢ ( ( 𝐵 = +∞ ∧ 𝐴 ∈ ℕ0 ) → ( ( 𝐴 +𝑒 𝐵 ) = 0 → ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) )
33 32 ex ⊢ ( 𝐵 = +∞ → ( 𝐴 ∈ ℕ0 → ( ( 𝐴 +𝑒 𝐵 ) = 0 → ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) ) )
34 16 33 jaoi ⊢ ( ( 𝐵 ∈ ℕ0 ∨ 𝐵 = +∞ ) → ( 𝐴 ∈ ℕ0 → ( ( 𝐴 +𝑒 𝐵 ) = 0 → ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) ) )
35 2 34 sylbi ⊢ ( 𝐵 ∈ ℕ0* → ( 𝐴 ∈ ℕ0 → ( ( 𝐴 +𝑒 𝐵 ) = 0 → ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) ) )
36 35 com12 ⊢ ( 𝐴 ∈ ℕ0 → ( 𝐵 ∈ ℕ0* → ( ( 𝐴 +𝑒 𝐵 ) = 0 → ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) ) )
37 oveq1 ⊢ ( 𝐴 = +∞ → ( 𝐴 +𝑒 𝐵 ) = ( +∞ +𝑒 𝐵 ) )
38 37 eqeq1d ⊢ ( 𝐴 = +∞ → ( ( 𝐴 +𝑒 𝐵 ) = 0 ↔ ( +∞ +𝑒 𝐵 ) = 0 ) )
39 xnn0xrnemnf ⊢ ( 𝐵 ∈ ℕ0* → ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞ ) )
40 xaddpnf2 ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞ ) → ( +∞ +𝑒 𝐵 ) = +∞ )
41 39 40 syl ⊢ ( 𝐵 ∈ ℕ0* → ( +∞ +𝑒 𝐵 ) = +∞ )
42 41 eqeq1d ⊢ ( 𝐵 ∈ ℕ0* → ( ( +∞ +𝑒 𝐵 ) = 0 ↔ +∞ = 0 ) )
43 38 42 sylan9bb ⊢ ( ( 𝐴 = +∞ ∧ 𝐵 ∈ ℕ0* ) → ( ( 𝐴 +𝑒 𝐵 ) = 0 ↔ +∞ = 0 ) )
44 43 31 biimtrdi ⊢ ( ( 𝐴 = +∞ ∧ 𝐵 ∈ ℕ0* ) → ( ( 𝐴 +𝑒 𝐵 ) = 0 → ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) )
45 44 ex ⊢ ( 𝐴 = +∞ → ( 𝐵 ∈ ℕ0* → ( ( 𝐴 +𝑒 𝐵 ) = 0 → ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) ) )
46 36 45 jaoi ⊢ ( ( 𝐴 ∈ ℕ0 ∨ 𝐴 = +∞ ) → ( 𝐵 ∈ ℕ0* → ( ( 𝐴 +𝑒 𝐵 ) = 0 → ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) ) )
47 1 46 sylbi ⊢ ( 𝐴 ∈ ℕ0* → ( 𝐵 ∈ ℕ0* → ( ( 𝐴 +𝑒 𝐵 ) = 0 → ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) ) )
48 47 imp ⊢ ( ( 𝐴 ∈ ℕ0* ∧ 𝐵 ∈ ℕ0* ) → ( ( 𝐴 +𝑒 𝐵 ) = 0 → ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) )
49 oveq12 ⊢ ( ( 𝐴 = 0 ∧ 𝐵 = 0 ) → ( 𝐴 +𝑒 𝐵 ) = ( 0 +𝑒 0 ) )
50 0xr ⊢ 0 ∈ ℝ*
51 xaddrid ⊢ ( 0 ∈ ℝ* → ( 0 +𝑒 0 ) = 0 )
52 50 51 ax-mp ⊢ ( 0 +𝑒 0 ) = 0
53 49 52 eqtrdi ⊢ ( ( 𝐴 = 0 ∧ 𝐵 = 0 ) → ( 𝐴 +𝑒 𝐵 ) = 0 )
54 48 53 impbid1 ⊢ ( ( 𝐴 ∈ ℕ0* ∧ 𝐵 ∈ ℕ0* ) → ( ( 𝐴 +𝑒 𝐵 ) = 0 ↔ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) )