xnn0xaddcl

Description: The extended nonnegative integers are closed under extended addition. (Contributed by AV, 10-Dec-2020)

		Ref	Expression
	Assertion	xnn0xaddcl	⊢ ( ( 𝐴 ∈ ℕ₀^* ∧ 𝐵 ∈ ℕ₀^* ) → ( 𝐴 +_𝑒 𝐵 ) ∈ ℕ₀^* )

Proof

Step	Hyp	Ref	Expression
1		nn0addcl	⊢ ( ( 𝐴 ∈ ℕ₀ ∧ 𝐵 ∈ ℕ₀ ) → ( 𝐴 + 𝐵 ) ∈ ℕ₀ )
2	1	nn0xnn0d	⊢ ( ( 𝐴 ∈ ℕ₀ ∧ 𝐵 ∈ ℕ₀ ) → ( 𝐴 + 𝐵 ) ∈ ℕ₀^* )
3		nn0re	⊢ ( 𝐴 ∈ ℕ₀ → 𝐴 ∈ ℝ )
4		nn0re	⊢ ( 𝐵 ∈ ℕ₀ → 𝐵 ∈ ℝ )
5		rexadd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 +_𝑒 𝐵 ) = ( 𝐴 + 𝐵 ) )
6	5	eleq1d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 +_𝑒 𝐵 ) ∈ ℕ₀^* ↔ ( 𝐴 + 𝐵 ) ∈ ℕ₀^* ) )
7	3 4 6	syl2an	⊢ ( ( 𝐴 ∈ ℕ₀ ∧ 𝐵 ∈ ℕ₀ ) → ( ( 𝐴 +_𝑒 𝐵 ) ∈ ℕ₀^* ↔ ( 𝐴 + 𝐵 ) ∈ ℕ₀^* ) )
8	2 7	mpbird	⊢ ( ( 𝐴 ∈ ℕ₀ ∧ 𝐵 ∈ ℕ₀ ) → ( 𝐴 +_𝑒 𝐵 ) ∈ ℕ₀^* )
9	8	a1d	⊢ ( ( 𝐴 ∈ ℕ₀ ∧ 𝐵 ∈ ℕ₀ ) → ( ( 𝐴 ∈ ℕ₀^* ∧ 𝐵 ∈ ℕ₀^* ) → ( 𝐴 +_𝑒 𝐵 ) ∈ ℕ₀^* ) )
10		ianor	⊢ ( ¬ ( 𝐴 ∈ ℕ₀ ∧ 𝐵 ∈ ℕ₀ ) ↔ ( ¬ 𝐴 ∈ ℕ₀ ∨ ¬ 𝐵 ∈ ℕ₀ ) )
11		xnn0nnn0pnf	⊢ ( ( 𝐴 ∈ ℕ₀^* ∧ ¬ 𝐴 ∈ ℕ₀ ) → 𝐴 = +∞ )
12		oveq1	⊢ ( 𝐴 = +∞ → ( 𝐴 +_𝑒 𝐵 ) = ( +∞ +_𝑒 𝐵 ) )
13		xnn0xrnemnf	⊢ ( 𝐵 ∈ ℕ₀^* → ( 𝐵 ∈ ℝ^* ∧ 𝐵 ≠ -∞ ) )
14		xaddpnf2	⊢ ( ( 𝐵 ∈ ℝ^* ∧ 𝐵 ≠ -∞ ) → ( +∞ +_𝑒 𝐵 ) = +∞ )
15	13 14	syl	⊢ ( 𝐵 ∈ ℕ₀^* → ( +∞ +_𝑒 𝐵 ) = +∞ )
16	12 15	sylan9eq	⊢ ( ( 𝐴 = +∞ ∧ 𝐵 ∈ ℕ₀^* ) → ( 𝐴 +_𝑒 𝐵 ) = +∞ )
17	16	ex	⊢ ( 𝐴 = +∞ → ( 𝐵 ∈ ℕ₀^* → ( 𝐴 +_𝑒 𝐵 ) = +∞ ) )
18	11 17	syl	⊢ ( ( 𝐴 ∈ ℕ₀^* ∧ ¬ 𝐴 ∈ ℕ₀ ) → ( 𝐵 ∈ ℕ₀^* → ( 𝐴 +_𝑒 𝐵 ) = +∞ ) )
19	18	expcom	⊢ ( ¬ 𝐴 ∈ ℕ₀ → ( 𝐴 ∈ ℕ₀^* → ( 𝐵 ∈ ℕ₀^* → ( 𝐴 +_𝑒 𝐵 ) = +∞ ) ) )
20	19	impd	⊢ ( ¬ 𝐴 ∈ ℕ₀ → ( ( 𝐴 ∈ ℕ₀^* ∧ 𝐵 ∈ ℕ₀^* ) → ( 𝐴 +_𝑒 𝐵 ) = +∞ ) )
21		xnn0nnn0pnf	⊢ ( ( 𝐵 ∈ ℕ₀^* ∧ ¬ 𝐵 ∈ ℕ₀ ) → 𝐵 = +∞ )
22		oveq2	⊢ ( 𝐵 = +∞ → ( 𝐴 +_𝑒 𝐵 ) = ( 𝐴 +_𝑒 +∞ ) )
23		xnn0xrnemnf	⊢ ( 𝐴 ∈ ℕ₀^* → ( 𝐴 ∈ ℝ^* ∧ 𝐴 ≠ -∞ ) )
24		xaddpnf1	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐴 ≠ -∞ ) → ( 𝐴 +_𝑒 +∞ ) = +∞ )
25	23 24	syl	⊢ ( 𝐴 ∈ ℕ₀^* → ( 𝐴 +_𝑒 +∞ ) = +∞ )
26	22 25	sylan9eq	⊢ ( ( 𝐵 = +∞ ∧ 𝐴 ∈ ℕ₀^* ) → ( 𝐴 +_𝑒 𝐵 ) = +∞ )
27	26	ex	⊢ ( 𝐵 = +∞ → ( 𝐴 ∈ ℕ₀^* → ( 𝐴 +_𝑒 𝐵 ) = +∞ ) )
28	21 27	syl	⊢ ( ( 𝐵 ∈ ℕ₀^* ∧ ¬ 𝐵 ∈ ℕ₀ ) → ( 𝐴 ∈ ℕ₀^* → ( 𝐴 +_𝑒 𝐵 ) = +∞ ) )
29	28	expcom	⊢ ( ¬ 𝐵 ∈ ℕ₀ → ( 𝐵 ∈ ℕ₀^* → ( 𝐴 ∈ ℕ₀^* → ( 𝐴 +_𝑒 𝐵 ) = +∞ ) ) )
30	29	impcomd	⊢ ( ¬ 𝐵 ∈ ℕ₀ → ( ( 𝐴 ∈ ℕ₀^* ∧ 𝐵 ∈ ℕ₀^* ) → ( 𝐴 +_𝑒 𝐵 ) = +∞ ) )
31	20 30	jaoi	⊢ ( ( ¬ 𝐴 ∈ ℕ₀ ∨ ¬ 𝐵 ∈ ℕ₀ ) → ( ( 𝐴 ∈ ℕ₀^* ∧ 𝐵 ∈ ℕ₀^* ) → ( 𝐴 +_𝑒 𝐵 ) = +∞ ) )
32	31	imp	⊢ ( ( ( ¬ 𝐴 ∈ ℕ₀ ∨ ¬ 𝐵 ∈ ℕ₀ ) ∧ ( 𝐴 ∈ ℕ₀^* ∧ 𝐵 ∈ ℕ₀^* ) ) → ( 𝐴 +_𝑒 𝐵 ) = +∞ )
33		pnf0xnn0	⊢ +∞ ∈ ℕ₀^*
34	32 33	eqeltrdi	⊢ ( ( ( ¬ 𝐴 ∈ ℕ₀ ∨ ¬ 𝐵 ∈ ℕ₀ ) ∧ ( 𝐴 ∈ ℕ₀^* ∧ 𝐵 ∈ ℕ₀^* ) ) → ( 𝐴 +_𝑒 𝐵 ) ∈ ℕ₀^* )
35	34	ex	⊢ ( ( ¬ 𝐴 ∈ ℕ₀ ∨ ¬ 𝐵 ∈ ℕ₀ ) → ( ( 𝐴 ∈ ℕ₀^* ∧ 𝐵 ∈ ℕ₀^* ) → ( 𝐴 +_𝑒 𝐵 ) ∈ ℕ₀^* ) )
36	10 35	sylbi	⊢ ( ¬ ( 𝐴 ∈ ℕ₀ ∧ 𝐵 ∈ ℕ₀ ) → ( ( 𝐴 ∈ ℕ₀^* ∧ 𝐵 ∈ ℕ₀^* ) → ( 𝐴 +_𝑒 𝐵 ) ∈ ℕ₀^* ) )
37	9 36	pm2.61i	⊢ ( ( 𝐴 ∈ ℕ₀^* ∧ 𝐵 ∈ ℕ₀^* ) → ( 𝐴 +_𝑒 𝐵 ) ∈ ℕ₀^* )

Metamath Proof Explorer

Theorem xnn0xaddcl

Proof