Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > xaddpnf2 | Structured version Visualization version GIF version |
Description: Addition of positive infinity on the left. (Contributed by Mario Carneiro, 20-Aug-2015.) |
Ref | Expression |
---|---|
xaddpnf2 | ⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞) → (+∞ +𝑒 𝐴) = +∞) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pnfxr 11075 | . . 3 ⊢ +∞ ∈ ℝ* | |
2 | xaddval 13003 | . . 3 ⊢ ((+∞ ∈ ℝ* ∧ 𝐴 ∈ ℝ*) → (+∞ +𝑒 𝐴) = if(+∞ = +∞, if(𝐴 = -∞, 0, +∞), if(+∞ = -∞, if(𝐴 = +∞, 0, -∞), if(𝐴 = +∞, +∞, if(𝐴 = -∞, -∞, (+∞ + 𝐴)))))) | |
3 | 1, 2 | mpan 688 | . 2 ⊢ (𝐴 ∈ ℝ* → (+∞ +𝑒 𝐴) = if(+∞ = +∞, if(𝐴 = -∞, 0, +∞), if(+∞ = -∞, if(𝐴 = +∞, 0, -∞), if(𝐴 = +∞, +∞, if(𝐴 = -∞, -∞, (+∞ + 𝐴)))))) |
4 | eqid 2736 | . . . 4 ⊢ +∞ = +∞ | |
5 | 4 | iftruei 4472 | . . 3 ⊢ if(+∞ = +∞, if(𝐴 = -∞, 0, +∞), if(+∞ = -∞, if(𝐴 = +∞, 0, -∞), if(𝐴 = +∞, +∞, if(𝐴 = -∞, -∞, (+∞ + 𝐴))))) = if(𝐴 = -∞, 0, +∞) |
6 | ifnefalse 4477 | . . 3 ⊢ (𝐴 ≠ -∞ → if(𝐴 = -∞, 0, +∞) = +∞) | |
7 | 5, 6 | eqtrid 2788 | . 2 ⊢ (𝐴 ≠ -∞ → if(+∞ = +∞, if(𝐴 = -∞, 0, +∞), if(+∞ = -∞, if(𝐴 = +∞, 0, -∞), if(𝐴 = +∞, +∞, if(𝐴 = -∞, -∞, (+∞ + 𝐴))))) = +∞) |
8 | 3, 7 | sylan9eq 2796 | 1 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞) → (+∞ +𝑒 𝐴) = +∞) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 = wceq 1539 ∈ wcel 2104 ≠ wne 2941 ifcif 4465 (class class class)co 7307 0cc0 10917 + caddc 10920 +∞cpnf 11052 -∞cmnf 11053 ℝ*cxr 11054 +𝑒 cxad 12892 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2707 ax-sep 5232 ax-nul 5239 ax-pow 5297 ax-pr 5361 ax-un 7620 ax-cnex 10973 ax-1cn 10975 ax-icn 10976 ax-addcl 10977 ax-mulcl 10979 ax-i2m1 10985 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 846 df-3an 1089 df-tru 1542 df-fal 1552 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2887 df-ne 2942 df-ral 3063 df-rex 3072 df-rab 3287 df-v 3439 df-sbc 3722 df-dif 3895 df-un 3897 df-in 3899 df-ss 3909 df-nul 4263 df-if 4466 df-pw 4541 df-sn 4566 df-pr 4568 df-op 4572 df-uni 4845 df-br 5082 df-opab 5144 df-id 5500 df-xp 5606 df-rel 5607 df-cnv 5608 df-co 5609 df-dm 5610 df-iota 6410 df-fun 6460 df-fv 6466 df-ov 7310 df-oprab 7311 df-mpo 7312 df-pnf 11057 df-mnf 11058 df-xr 11059 df-xadd 12895 |
This theorem is referenced by: xnn0xaddcl 13015 xaddnemnf 13016 xaddcom 13020 xaddid1 13021 xnn0xadd0 13027 xnegdi 13028 xaddass 13029 xleadd1a 13033 xadddilem 13074 xadddi2 13077 hashinfxadd 14145 xrsdsreclblem 20689 isxmet2d 23525 xaddeq0 31121 xrge0adddir 31346 xrge0iifhom 31932 infrpge 42938 infleinflem1 42957 ovolsplit 43578 sge0pr 43982 sge0split 43997 sge0xaddlem1 44021 sge0xadd 44023 |
Copyright terms: Public domain | W3C validator |