# Metamath Proof Explorer

Description: The extended real addition of the size of an infinite set with the size of an arbitrary set yields plus infinity. (Contributed by Alexander van der Vekens, 20-Dec-2017)

Ref Expression
Assertion hashinfxadd $⊢ A ∈ V ∧ B ∈ W ∧ A ∉ ℕ 0 → A + 𝑒 B = +∞$

### Proof

Step Hyp Ref Expression
1 hashnn0pnf $⊢ A ∈ V → A ∈ ℕ 0 ∨ A = +∞$
2 df-nel $⊢ A ∉ ℕ 0 ↔ ¬ A ∈ ℕ 0$
3 2 anbi2i $⊢ A = +∞ ∨ A ∈ ℕ 0 ∧ A ∉ ℕ 0 ↔ A = +∞ ∨ A ∈ ℕ 0 ∧ ¬ A ∈ ℕ 0$
4 pm5.61 $⊢ A = +∞ ∨ A ∈ ℕ 0 ∧ ¬ A ∈ ℕ 0 ↔ A = +∞ ∧ ¬ A ∈ ℕ 0$
5 3 4 sylbb $⊢ A = +∞ ∨ A ∈ ℕ 0 ∧ A ∉ ℕ 0 → A = +∞ ∧ ¬ A ∈ ℕ 0$
6 5 ex $⊢ A = +∞ ∨ A ∈ ℕ 0 → A ∉ ℕ 0 → A = +∞ ∧ ¬ A ∈ ℕ 0$
7 6 orcoms $⊢ A ∈ ℕ 0 ∨ A = +∞ → A ∉ ℕ 0 → A = +∞ ∧ ¬ A ∈ ℕ 0$
8 1 7 syl $⊢ A ∈ V → A ∉ ℕ 0 → A = +∞ ∧ ¬ A ∈ ℕ 0$
9 8 imp $⊢ A ∈ V ∧ A ∉ ℕ 0 → A = +∞ ∧ ¬ A ∈ ℕ 0$
10 9 3adant2 $⊢ A ∈ V ∧ B ∈ W ∧ A ∉ ℕ 0 → A = +∞ ∧ ¬ A ∈ ℕ 0$
11 oveq1 $⊢ A = +∞ → A + 𝑒 B = +∞ + 𝑒 B$
12 hashxrcl $⊢ B ∈ W → B ∈ ℝ *$
13 hashnemnf $⊢ B ∈ W → B ≠ −∞$
14 12 13 jca $⊢ B ∈ W → B ∈ ℝ * ∧ B ≠ −∞$
15 14 3ad2ant2 $⊢ A ∈ V ∧ B ∈ W ∧ A ∉ ℕ 0 → B ∈ ℝ * ∧ B ≠ −∞$
16 xaddpnf2 $⊢ B ∈ ℝ * ∧ B ≠ −∞ → +∞ + 𝑒 B = +∞$
17 15 16 syl $⊢ A ∈ V ∧ B ∈ W ∧ A ∉ ℕ 0 → +∞ + 𝑒 B = +∞$
18 11 17 sylan9eqr $⊢ A ∈ V ∧ B ∈ W ∧ A ∉ ℕ 0 ∧ A = +∞ → A + 𝑒 B = +∞$
19 18 expcom $⊢ A = +∞ → A ∈ V ∧ B ∈ W ∧ A ∉ ℕ 0 → A + 𝑒 B = +∞$
20 19 adantr $⊢ A = +∞ ∧ ¬ A ∈ ℕ 0 → A ∈ V ∧ B ∈ W ∧ A ∉ ℕ 0 → A + 𝑒 B = +∞$
21 10 20 mpcom $⊢ A ∈ V ∧ B ∈ W ∧ A ∉ ℕ 0 → A + 𝑒 B = +∞$