Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  xaddpnf1 GIF version

 Description: Addition of positive infinity on the right. (Contributed by Mario Carneiro, 20-Aug-2015.)
Assertion
Ref Expression
xaddpnf1 ((𝐴 ∈ ℝ*𝐴 ≠ -∞) → (𝐴 +𝑒 +∞) = +∞)

StepHypRef Expression
1 pnfxr 7909 . . . 4 +∞ ∈ ℝ*
2 xaddval 9727 . . . 4 ((𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 +𝑒 +∞) = if(𝐴 = +∞, if(+∞ = -∞, 0, +∞), if(𝐴 = -∞, if(+∞ = +∞, 0, -∞), if(+∞ = +∞, +∞, if(+∞ = -∞, -∞, (𝐴 + +∞))))))
31, 2mpan2 422 . . 3 (𝐴 ∈ ℝ* → (𝐴 +𝑒 +∞) = if(𝐴 = +∞, if(+∞ = -∞, 0, +∞), if(𝐴 = -∞, if(+∞ = +∞, 0, -∞), if(+∞ = +∞, +∞, if(+∞ = -∞, -∞, (𝐴 + +∞))))))
43adantr 274 . 2 ((𝐴 ∈ ℝ*𝐴 ≠ -∞) → (𝐴 +𝑒 +∞) = if(𝐴 = +∞, if(+∞ = -∞, 0, +∞), if(𝐴 = -∞, if(+∞ = +∞, 0, -∞), if(+∞ = +∞, +∞, if(+∞ = -∞, -∞, (𝐴 + +∞))))))
5 pnfnemnf 7911 . . . . 5 +∞ ≠ -∞
6 ifnefalse 3512 . . . . 5 (+∞ ≠ -∞ → if(+∞ = -∞, 0, +∞) = +∞)
75, 6mp1i 10 . . . 4 (𝐴 ≠ -∞ → if(+∞ = -∞, 0, +∞) = +∞)
8 ifnefalse 3512 . . . . 5 (𝐴 ≠ -∞ → if(𝐴 = -∞, if(+∞ = +∞, 0, -∞), if(+∞ = +∞, +∞, if(+∞ = -∞, -∞, (𝐴 + +∞)))) = if(+∞ = +∞, +∞, if(+∞ = -∞, -∞, (𝐴 + +∞))))
9 eqid 2154 . . . . . 6 +∞ = +∞
109iftruei 3507 . . . . 5 if(+∞ = +∞, +∞, if(+∞ = -∞, -∞, (𝐴 + +∞))) = +∞
118, 10eqtrdi 2203 . . . 4 (𝐴 ≠ -∞ → if(𝐴 = -∞, if(+∞ = +∞, 0, -∞), if(+∞ = +∞, +∞, if(+∞ = -∞, -∞, (𝐴 + +∞)))) = +∞)
127, 11ifeq12d 3520 . . 3 (𝐴 ≠ -∞ → if(𝐴 = +∞, if(+∞ = -∞, 0, +∞), if(𝐴 = -∞, if(+∞ = +∞, 0, -∞), if(+∞ = +∞, +∞, if(+∞ = -∞, -∞, (𝐴 + +∞))))) = if(𝐴 = +∞, +∞, +∞))
13 xrpnfdc 9724 . . . 4 (𝐴 ∈ ℝ*DECID 𝐴 = +∞)
14 ifiddc 3534 . . . 4 (DECID 𝐴 = +∞ → if(𝐴 = +∞, +∞, +∞) = +∞)
1513, 14syl 14 . . 3 (𝐴 ∈ ℝ* → if(𝐴 = +∞, +∞, +∞) = +∞)
1612, 15sylan9eqr 2209 . 2 ((𝐴 ∈ ℝ*𝐴 ≠ -∞) → if(𝐴 = +∞, if(+∞ = -∞, 0, +∞), if(𝐴 = -∞, if(+∞ = +∞, 0, -∞), if(+∞ = +∞, +∞, if(+∞ = -∞, -∞, (𝐴 + +∞))))) = +∞)
174, 16eqtrd 2187 1 ((𝐴 ∈ ℝ*𝐴 ≠ -∞) → (𝐴 +𝑒 +∞) = +∞)