# Metamath Proof Explorer

Description: Associativity of extended real addition. The correct condition here is "it is not the case that both +oo and -oo appear as one of A , B , C , i.e. -. { +oo , -oo } C_ { A , B , C } ", but this condition is difficult to work with, so we break the theorem into two parts: this one, where -oo is not present in A , B , C , and xaddass2 , where +oo is not present. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xaddass ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {A}\ne \mathrm{-\infty }\right)\wedge \left({B}\in {ℝ}^{*}\wedge {B}\ne \mathrm{-\infty }\right)\wedge \left({C}\in {ℝ}^{*}\wedge {C}\ne \mathrm{-\infty }\right)\right)\to \left({A}{+}_{𝑒}{B}\right){+}_{𝑒}{C}={A}{+}_{𝑒}\left({B}{+}_{𝑒}{C}\right)$

### Proof

Step Hyp Ref Expression
1 recn ${⊢}{A}\in ℝ\to {A}\in ℂ$
2 recn ${⊢}{B}\in ℝ\to {B}\in ℂ$
3 recn ${⊢}{C}\in ℝ\to {C}\in ℂ$
4 addass ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to {A}+{B}+{C}={A}+{B}+{C}$
5 1 2 3 4 syl3an ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℝ\right)\to {A}+{B}+{C}={A}+{B}+{C}$
6 5 3expa ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {C}\in ℝ\right)\to {A}+{B}+{C}={A}+{B}+{C}$
7 readdcl ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to {A}+{B}\in ℝ$
8 rexadd ${⊢}\left({A}+{B}\in ℝ\wedge {C}\in ℝ\right)\to \left({A}+{B}\right){+}_{𝑒}{C}={A}+{B}+{C}$
9 7 8 sylan ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {C}\in ℝ\right)\to \left({A}+{B}\right){+}_{𝑒}{C}={A}+{B}+{C}$
10 readdcl ${⊢}\left({B}\in ℝ\wedge {C}\in ℝ\right)\to {B}+{C}\in ℝ$
11 rexadd ${⊢}\left({A}\in ℝ\wedge {B}+{C}\in ℝ\right)\to {A}{+}_{𝑒}\left({B}+{C}\right)={A}+{B}+{C}$
12 10 11 sylan2 ${⊢}\left({A}\in ℝ\wedge \left({B}\in ℝ\wedge {C}\in ℝ\right)\right)\to {A}{+}_{𝑒}\left({B}+{C}\right)={A}+{B}+{C}$
13 12 anassrs ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {C}\in ℝ\right)\to {A}{+}_{𝑒}\left({B}+{C}\right)={A}+{B}+{C}$
14 6 9 13 3eqtr4d ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {C}\in ℝ\right)\to \left({A}+{B}\right){+}_{𝑒}{C}={A}{+}_{𝑒}\left({B}+{C}\right)$
15 rexadd ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to {A}{+}_{𝑒}{B}={A}+{B}$
16 15 adantr ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {C}\in ℝ\right)\to {A}{+}_{𝑒}{B}={A}+{B}$
17 16 oveq1d ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {C}\in ℝ\right)\to \left({A}{+}_{𝑒}{B}\right){+}_{𝑒}{C}=\left({A}+{B}\right){+}_{𝑒}{C}$
18 rexadd ${⊢}\left({B}\in ℝ\wedge {C}\in ℝ\right)\to {B}{+}_{𝑒}{C}={B}+{C}$
19 18 adantll ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {C}\in ℝ\right)\to {B}{+}_{𝑒}{C}={B}+{C}$
20 19 oveq2d ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {C}\in ℝ\right)\to {A}{+}_{𝑒}\left({B}{+}_{𝑒}{C}\right)={A}{+}_{𝑒}\left({B}+{C}\right)$
21 14 17 20 3eqtr4d ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {C}\in ℝ\right)\to \left({A}{+}_{𝑒}{B}\right){+}_{𝑒}{C}={A}{+}_{𝑒}\left({B}{+}_{𝑒}{C}\right)$
22 21 adantll ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{*}\wedge {A}\ne \mathrm{-\infty }\right)\wedge \left({B}\in {ℝ}^{*}\wedge {B}\ne \mathrm{-\infty }\right)\wedge \left({C}\in {ℝ}^{*}\wedge {C}\ne \mathrm{-\infty }\right)\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge {C}\in ℝ\right)\to \left({A}{+}_{𝑒}{B}\right){+}_{𝑒}{C}={A}{+}_{𝑒}\left({B}{+}_{𝑒}{C}\right)$
23 oveq2 ${⊢}{C}=\mathrm{+\infty }\to \left({A}{+}_{𝑒}{B}\right){+}_{𝑒}{C}=\left({A}{+}_{𝑒}{B}\right){+}_{𝑒}\mathrm{+\infty }$
24 simp1l ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {A}\ne \mathrm{-\infty }\right)\wedge \left({B}\in {ℝ}^{*}\wedge {B}\ne \mathrm{-\infty }\right)\wedge \left({C}\in {ℝ}^{*}\wedge {C}\ne \mathrm{-\infty }\right)\right)\to {A}\in {ℝ}^{*}$
25 simp2l ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {A}\ne \mathrm{-\infty }\right)\wedge \left({B}\in {ℝ}^{*}\wedge {B}\ne \mathrm{-\infty }\right)\wedge \left({C}\in {ℝ}^{*}\wedge {C}\ne \mathrm{-\infty }\right)\right)\to {B}\in {ℝ}^{*}$
26 xaddcl ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to {A}{+}_{𝑒}{B}\in {ℝ}^{*}$
27 24 25 26 syl2anc ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {A}\ne \mathrm{-\infty }\right)\wedge \left({B}\in {ℝ}^{*}\wedge {B}\ne \mathrm{-\infty }\right)\wedge \left({C}\in {ℝ}^{*}\wedge {C}\ne \mathrm{-\infty }\right)\right)\to {A}{+}_{𝑒}{B}\in {ℝ}^{*}$
28 xaddnemnf ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {A}\ne \mathrm{-\infty }\right)\wedge \left({B}\in {ℝ}^{*}\wedge {B}\ne \mathrm{-\infty }\right)\right)\to {A}{+}_{𝑒}{B}\ne \mathrm{-\infty }$
29 28 3adant3 ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {A}\ne \mathrm{-\infty }\right)\wedge \left({B}\in {ℝ}^{*}\wedge {B}\ne \mathrm{-\infty }\right)\wedge \left({C}\in {ℝ}^{*}\wedge {C}\ne \mathrm{-\infty }\right)\right)\to {A}{+}_{𝑒}{B}\ne \mathrm{-\infty }$
30 xaddpnf1 ${⊢}\left({A}{+}_{𝑒}{B}\in {ℝ}^{*}\wedge {A}{+}_{𝑒}{B}\ne \mathrm{-\infty }\right)\to \left({A}{+}_{𝑒}{B}\right){+}_{𝑒}\mathrm{+\infty }=\mathrm{+\infty }$
31 27 29 30 syl2anc ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {A}\ne \mathrm{-\infty }\right)\wedge \left({B}\in {ℝ}^{*}\wedge {B}\ne \mathrm{-\infty }\right)\wedge \left({C}\in {ℝ}^{*}\wedge {C}\ne \mathrm{-\infty }\right)\right)\to \left({A}{+}_{𝑒}{B}\right){+}_{𝑒}\mathrm{+\infty }=\mathrm{+\infty }$
32 23 31 sylan9eqr ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {A}\ne \mathrm{-\infty }\right)\wedge \left({B}\in {ℝ}^{*}\wedge {B}\ne \mathrm{-\infty }\right)\wedge \left({C}\in {ℝ}^{*}\wedge {C}\ne \mathrm{-\infty }\right)\right)\wedge {C}=\mathrm{+\infty }\right)\to \left({A}{+}_{𝑒}{B}\right){+}_{𝑒}{C}=\mathrm{+\infty }$
33 xaddpnf1 ${⊢}\left({A}\in {ℝ}^{*}\wedge {A}\ne \mathrm{-\infty }\right)\to {A}{+}_{𝑒}\mathrm{+\infty }=\mathrm{+\infty }$
34 33 3ad2ant1 ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {A}\ne \mathrm{-\infty }\right)\wedge \left({B}\in {ℝ}^{*}\wedge {B}\ne \mathrm{-\infty }\right)\wedge \left({C}\in {ℝ}^{*}\wedge {C}\ne \mathrm{-\infty }\right)\right)\to {A}{+}_{𝑒}\mathrm{+\infty }=\mathrm{+\infty }$
35 34 adantr ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {A}\ne \mathrm{-\infty }\right)\wedge \left({B}\in {ℝ}^{*}\wedge {B}\ne \mathrm{-\infty }\right)\wedge \left({C}\in {ℝ}^{*}\wedge {C}\ne \mathrm{-\infty }\right)\right)\wedge {C}=\mathrm{+\infty }\right)\to {A}{+}_{𝑒}\mathrm{+\infty }=\mathrm{+\infty }$
36 32 35 eqtr4d ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {A}\ne \mathrm{-\infty }\right)\wedge \left({B}\in {ℝ}^{*}\wedge {B}\ne \mathrm{-\infty }\right)\wedge \left({C}\in {ℝ}^{*}\wedge {C}\ne \mathrm{-\infty }\right)\right)\wedge {C}=\mathrm{+\infty }\right)\to \left({A}{+}_{𝑒}{B}\right){+}_{𝑒}{C}={A}{+}_{𝑒}\mathrm{+\infty }$
37 oveq2 ${⊢}{C}=\mathrm{+\infty }\to {B}{+}_{𝑒}{C}={B}{+}_{𝑒}\mathrm{+\infty }$
38 xaddpnf1 ${⊢}\left({B}\in {ℝ}^{*}\wedge {B}\ne \mathrm{-\infty }\right)\to {B}{+}_{𝑒}\mathrm{+\infty }=\mathrm{+\infty }$
39 38 3ad2ant2 ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {A}\ne \mathrm{-\infty }\right)\wedge \left({B}\in {ℝ}^{*}\wedge {B}\ne \mathrm{-\infty }\right)\wedge \left({C}\in {ℝ}^{*}\wedge {C}\ne \mathrm{-\infty }\right)\right)\to {B}{+}_{𝑒}\mathrm{+\infty }=\mathrm{+\infty }$
40 37 39 sylan9eqr ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {A}\ne \mathrm{-\infty }\right)\wedge \left({B}\in {ℝ}^{*}\wedge {B}\ne \mathrm{-\infty }\right)\wedge \left({C}\in {ℝ}^{*}\wedge {C}\ne \mathrm{-\infty }\right)\right)\wedge {C}=\mathrm{+\infty }\right)\to {B}{+}_{𝑒}{C}=\mathrm{+\infty }$
41 40 oveq2d ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {A}\ne \mathrm{-\infty }\right)\wedge \left({B}\in {ℝ}^{*}\wedge {B}\ne \mathrm{-\infty }\right)\wedge \left({C}\in {ℝ}^{*}\wedge {C}\ne \mathrm{-\infty }\right)\right)\wedge {C}=\mathrm{+\infty }\right)\to {A}{+}_{𝑒}\left({B}{+}_{𝑒}{C}\right)={A}{+}_{𝑒}\mathrm{+\infty }$
42 36 41 eqtr4d ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {A}\ne \mathrm{-\infty }\right)\wedge \left({B}\in {ℝ}^{*}\wedge {B}\ne \mathrm{-\infty }\right)\wedge \left({C}\in {ℝ}^{*}\wedge {C}\ne \mathrm{-\infty }\right)\right)\wedge {C}=\mathrm{+\infty }\right)\to \left({A}{+}_{𝑒}{B}\right){+}_{𝑒}{C}={A}{+}_{𝑒}\left({B}{+}_{𝑒}{C}\right)$
43 42 adantlr ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{*}\wedge {A}\ne \mathrm{-\infty }\right)\wedge \left({B}\in {ℝ}^{*}\wedge {B}\ne \mathrm{-\infty }\right)\wedge \left({C}\in {ℝ}^{*}\wedge {C}\ne \mathrm{-\infty }\right)\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge {C}=\mathrm{+\infty }\right)\to \left({A}{+}_{𝑒}{B}\right){+}_{𝑒}{C}={A}{+}_{𝑒}\left({B}{+}_{𝑒}{C}\right)$
44 simp3 ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {A}\ne \mathrm{-\infty }\right)\wedge \left({B}\in {ℝ}^{*}\wedge {B}\ne \mathrm{-\infty }\right)\wedge \left({C}\in {ℝ}^{*}\wedge {C}\ne \mathrm{-\infty }\right)\right)\to \left({C}\in {ℝ}^{*}\wedge {C}\ne \mathrm{-\infty }\right)$
45 xrnemnf ${⊢}\left({C}\in {ℝ}^{*}\wedge {C}\ne \mathrm{-\infty }\right)↔\left({C}\in ℝ\vee {C}=\mathrm{+\infty }\right)$
46 44 45 sylib ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {A}\ne \mathrm{-\infty }\right)\wedge \left({B}\in {ℝ}^{*}\wedge {B}\ne \mathrm{-\infty }\right)\wedge \left({C}\in {ℝ}^{*}\wedge {C}\ne \mathrm{-\infty }\right)\right)\to \left({C}\in ℝ\vee {C}=\mathrm{+\infty }\right)$
47 46 adantr ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {A}\ne \mathrm{-\infty }\right)\wedge \left({B}\in {ℝ}^{*}\wedge {B}\ne \mathrm{-\infty }\right)\wedge \left({C}\in {ℝ}^{*}\wedge {C}\ne \mathrm{-\infty }\right)\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\to \left({C}\in ℝ\vee {C}=\mathrm{+\infty }\right)$
48 22 43 47 mpjaodan ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {A}\ne \mathrm{-\infty }\right)\wedge \left({B}\in {ℝ}^{*}\wedge {B}\ne \mathrm{-\infty }\right)\wedge \left({C}\in {ℝ}^{*}\wedge {C}\ne \mathrm{-\infty }\right)\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\to \left({A}{+}_{𝑒}{B}\right){+}_{𝑒}{C}={A}{+}_{𝑒}\left({B}{+}_{𝑒}{C}\right)$
49 48 anassrs ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{*}\wedge {A}\ne \mathrm{-\infty }\right)\wedge \left({B}\in {ℝ}^{*}\wedge {B}\ne \mathrm{-\infty }\right)\wedge \left({C}\in {ℝ}^{*}\wedge {C}\ne \mathrm{-\infty }\right)\right)\wedge {A}\in ℝ\right)\wedge {B}\in ℝ\right)\to \left({A}{+}_{𝑒}{B}\right){+}_{𝑒}{C}={A}{+}_{𝑒}\left({B}{+}_{𝑒}{C}\right)$
50 xaddpnf2 ${⊢}\left({C}\in {ℝ}^{*}\wedge {C}\ne \mathrm{-\infty }\right)\to \mathrm{+\infty }{+}_{𝑒}{C}=\mathrm{+\infty }$
51 50 3ad2ant3 ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {A}\ne \mathrm{-\infty }\right)\wedge \left({B}\in {ℝ}^{*}\wedge {B}\ne \mathrm{-\infty }\right)\wedge \left({C}\in {ℝ}^{*}\wedge {C}\ne \mathrm{-\infty }\right)\right)\to \mathrm{+\infty }{+}_{𝑒}{C}=\mathrm{+\infty }$
52 51 34 eqtr4d ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {A}\ne \mathrm{-\infty }\right)\wedge \left({B}\in {ℝ}^{*}\wedge {B}\ne \mathrm{-\infty }\right)\wedge \left({C}\in {ℝ}^{*}\wedge {C}\ne \mathrm{-\infty }\right)\right)\to \mathrm{+\infty }{+}_{𝑒}{C}={A}{+}_{𝑒}\mathrm{+\infty }$
53 52 adantr ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {A}\ne \mathrm{-\infty }\right)\wedge \left({B}\in {ℝ}^{*}\wedge {B}\ne \mathrm{-\infty }\right)\wedge \left({C}\in {ℝ}^{*}\wedge {C}\ne \mathrm{-\infty }\right)\right)\wedge {B}=\mathrm{+\infty }\right)\to \mathrm{+\infty }{+}_{𝑒}{C}={A}{+}_{𝑒}\mathrm{+\infty }$
54 oveq2 ${⊢}{B}=\mathrm{+\infty }\to {A}{+}_{𝑒}{B}={A}{+}_{𝑒}\mathrm{+\infty }$
55 54 34 sylan9eqr ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {A}\ne \mathrm{-\infty }\right)\wedge \left({B}\in {ℝ}^{*}\wedge {B}\ne \mathrm{-\infty }\right)\wedge \left({C}\in {ℝ}^{*}\wedge {C}\ne \mathrm{-\infty }\right)\right)\wedge {B}=\mathrm{+\infty }\right)\to {A}{+}_{𝑒}{B}=\mathrm{+\infty }$
56 55 oveq1d ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {A}\ne \mathrm{-\infty }\right)\wedge \left({B}\in {ℝ}^{*}\wedge {B}\ne \mathrm{-\infty }\right)\wedge \left({C}\in {ℝ}^{*}\wedge {C}\ne \mathrm{-\infty }\right)\right)\wedge {B}=\mathrm{+\infty }\right)\to \left({A}{+}_{𝑒}{B}\right){+}_{𝑒}{C}=\mathrm{+\infty }{+}_{𝑒}{C}$
57 oveq1 ${⊢}{B}=\mathrm{+\infty }\to {B}{+}_{𝑒}{C}=\mathrm{+\infty }{+}_{𝑒}{C}$
58 57 51 sylan9eqr ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {A}\ne \mathrm{-\infty }\right)\wedge \left({B}\in {ℝ}^{*}\wedge {B}\ne \mathrm{-\infty }\right)\wedge \left({C}\in {ℝ}^{*}\wedge {C}\ne \mathrm{-\infty }\right)\right)\wedge {B}=\mathrm{+\infty }\right)\to {B}{+}_{𝑒}{C}=\mathrm{+\infty }$
59 58 oveq2d ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {A}\ne \mathrm{-\infty }\right)\wedge \left({B}\in {ℝ}^{*}\wedge {B}\ne \mathrm{-\infty }\right)\wedge \left({C}\in {ℝ}^{*}\wedge {C}\ne \mathrm{-\infty }\right)\right)\wedge {B}=\mathrm{+\infty }\right)\to {A}{+}_{𝑒}\left({B}{+}_{𝑒}{C}\right)={A}{+}_{𝑒}\mathrm{+\infty }$
60 53 56 59 3eqtr4d ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {A}\ne \mathrm{-\infty }\right)\wedge \left({B}\in {ℝ}^{*}\wedge {B}\ne \mathrm{-\infty }\right)\wedge \left({C}\in {ℝ}^{*}\wedge {C}\ne \mathrm{-\infty }\right)\right)\wedge {B}=\mathrm{+\infty }\right)\to \left({A}{+}_{𝑒}{B}\right){+}_{𝑒}{C}={A}{+}_{𝑒}\left({B}{+}_{𝑒}{C}\right)$
61 60 adantlr ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{*}\wedge {A}\ne \mathrm{-\infty }\right)\wedge \left({B}\in {ℝ}^{*}\wedge {B}\ne \mathrm{-\infty }\right)\wedge \left({C}\in {ℝ}^{*}\wedge {C}\ne \mathrm{-\infty }\right)\right)\wedge {A}\in ℝ\right)\wedge {B}=\mathrm{+\infty }\right)\to \left({A}{+}_{𝑒}{B}\right){+}_{𝑒}{C}={A}{+}_{𝑒}\left({B}{+}_{𝑒}{C}\right)$
62 simpl2 ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {A}\ne \mathrm{-\infty }\right)\wedge \left({B}\in {ℝ}^{*}\wedge {B}\ne \mathrm{-\infty }\right)\wedge \left({C}\in {ℝ}^{*}\wedge {C}\ne \mathrm{-\infty }\right)\right)\wedge {A}\in ℝ\right)\to \left({B}\in {ℝ}^{*}\wedge {B}\ne \mathrm{-\infty }\right)$
63 xrnemnf ${⊢}\left({B}\in {ℝ}^{*}\wedge {B}\ne \mathrm{-\infty }\right)↔\left({B}\in ℝ\vee {B}=\mathrm{+\infty }\right)$
64 62 63 sylib ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {A}\ne \mathrm{-\infty }\right)\wedge \left({B}\in {ℝ}^{*}\wedge {B}\ne \mathrm{-\infty }\right)\wedge \left({C}\in {ℝ}^{*}\wedge {C}\ne \mathrm{-\infty }\right)\right)\wedge {A}\in ℝ\right)\to \left({B}\in ℝ\vee {B}=\mathrm{+\infty }\right)$
65 49 61 64 mpjaodan ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {A}\ne \mathrm{-\infty }\right)\wedge \left({B}\in {ℝ}^{*}\wedge {B}\ne \mathrm{-\infty }\right)\wedge \left({C}\in {ℝ}^{*}\wedge {C}\ne \mathrm{-\infty }\right)\right)\wedge {A}\in ℝ\right)\to \left({A}{+}_{𝑒}{B}\right){+}_{𝑒}{C}={A}{+}_{𝑒}\left({B}{+}_{𝑒}{C}\right)$
66 simpl3 ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {A}\ne \mathrm{-\infty }\right)\wedge \left({B}\in {ℝ}^{*}\wedge {B}\ne \mathrm{-\infty }\right)\wedge \left({C}\in {ℝ}^{*}\wedge {C}\ne \mathrm{-\infty }\right)\right)\wedge {A}=\mathrm{+\infty }\right)\to \left({C}\in {ℝ}^{*}\wedge {C}\ne \mathrm{-\infty }\right)$
67 66 50 syl ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {A}\ne \mathrm{-\infty }\right)\wedge \left({B}\in {ℝ}^{*}\wedge {B}\ne \mathrm{-\infty }\right)\wedge \left({C}\in {ℝ}^{*}\wedge {C}\ne \mathrm{-\infty }\right)\right)\wedge {A}=\mathrm{+\infty }\right)\to \mathrm{+\infty }{+}_{𝑒}{C}=\mathrm{+\infty }$
68 simpl2l ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {A}\ne \mathrm{-\infty }\right)\wedge \left({B}\in {ℝ}^{*}\wedge {B}\ne \mathrm{-\infty }\right)\wedge \left({C}\in {ℝ}^{*}\wedge {C}\ne \mathrm{-\infty }\right)\right)\wedge {A}=\mathrm{+\infty }\right)\to {B}\in {ℝ}^{*}$
69 simpl3l ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {A}\ne \mathrm{-\infty }\right)\wedge \left({B}\in {ℝ}^{*}\wedge {B}\ne \mathrm{-\infty }\right)\wedge \left({C}\in {ℝ}^{*}\wedge {C}\ne \mathrm{-\infty }\right)\right)\wedge {A}=\mathrm{+\infty }\right)\to {C}\in {ℝ}^{*}$
70 xaddcl ${⊢}\left({B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\to {B}{+}_{𝑒}{C}\in {ℝ}^{*}$
71 68 69 70 syl2anc ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {A}\ne \mathrm{-\infty }\right)\wedge \left({B}\in {ℝ}^{*}\wedge {B}\ne \mathrm{-\infty }\right)\wedge \left({C}\in {ℝ}^{*}\wedge {C}\ne \mathrm{-\infty }\right)\right)\wedge {A}=\mathrm{+\infty }\right)\to {B}{+}_{𝑒}{C}\in {ℝ}^{*}$
72 simpl2 ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {A}\ne \mathrm{-\infty }\right)\wedge \left({B}\in {ℝ}^{*}\wedge {B}\ne \mathrm{-\infty }\right)\wedge \left({C}\in {ℝ}^{*}\wedge {C}\ne \mathrm{-\infty }\right)\right)\wedge {A}=\mathrm{+\infty }\right)\to \left({B}\in {ℝ}^{*}\wedge {B}\ne \mathrm{-\infty }\right)$
73 xaddnemnf ${⊢}\left(\left({B}\in {ℝ}^{*}\wedge {B}\ne \mathrm{-\infty }\right)\wedge \left({C}\in {ℝ}^{*}\wedge {C}\ne \mathrm{-\infty }\right)\right)\to {B}{+}_{𝑒}{C}\ne \mathrm{-\infty }$
74 72 66 73 syl2anc ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {A}\ne \mathrm{-\infty }\right)\wedge \left({B}\in {ℝ}^{*}\wedge {B}\ne \mathrm{-\infty }\right)\wedge \left({C}\in {ℝ}^{*}\wedge {C}\ne \mathrm{-\infty }\right)\right)\wedge {A}=\mathrm{+\infty }\right)\to {B}{+}_{𝑒}{C}\ne \mathrm{-\infty }$
75 xaddpnf2 ${⊢}\left({B}{+}_{𝑒}{C}\in {ℝ}^{*}\wedge {B}{+}_{𝑒}{C}\ne \mathrm{-\infty }\right)\to \mathrm{+\infty }{+}_{𝑒}\left({B}{+}_{𝑒}{C}\right)=\mathrm{+\infty }$
76 71 74 75 syl2anc ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {A}\ne \mathrm{-\infty }\right)\wedge \left({B}\in {ℝ}^{*}\wedge {B}\ne \mathrm{-\infty }\right)\wedge \left({C}\in {ℝ}^{*}\wedge {C}\ne \mathrm{-\infty }\right)\right)\wedge {A}=\mathrm{+\infty }\right)\to \mathrm{+\infty }{+}_{𝑒}\left({B}{+}_{𝑒}{C}\right)=\mathrm{+\infty }$
77 67 76 eqtr4d ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {A}\ne \mathrm{-\infty }\right)\wedge \left({B}\in {ℝ}^{*}\wedge {B}\ne \mathrm{-\infty }\right)\wedge \left({C}\in {ℝ}^{*}\wedge {C}\ne \mathrm{-\infty }\right)\right)\wedge {A}=\mathrm{+\infty }\right)\to \mathrm{+\infty }{+}_{𝑒}{C}=\mathrm{+\infty }{+}_{𝑒}\left({B}{+}_{𝑒}{C}\right)$
78 simpr ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {A}\ne \mathrm{-\infty }\right)\wedge \left({B}\in {ℝ}^{*}\wedge {B}\ne \mathrm{-\infty }\right)\wedge \left({C}\in {ℝ}^{*}\wedge {C}\ne \mathrm{-\infty }\right)\right)\wedge {A}=\mathrm{+\infty }\right)\to {A}=\mathrm{+\infty }$
79 78 oveq1d ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {A}\ne \mathrm{-\infty }\right)\wedge \left({B}\in {ℝ}^{*}\wedge {B}\ne \mathrm{-\infty }\right)\wedge \left({C}\in {ℝ}^{*}\wedge {C}\ne \mathrm{-\infty }\right)\right)\wedge {A}=\mathrm{+\infty }\right)\to {A}{+}_{𝑒}{B}=\mathrm{+\infty }{+}_{𝑒}{B}$
80 xaddpnf2 ${⊢}\left({B}\in {ℝ}^{*}\wedge {B}\ne \mathrm{-\infty }\right)\to \mathrm{+\infty }{+}_{𝑒}{B}=\mathrm{+\infty }$
81 72 80 syl ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {A}\ne \mathrm{-\infty }\right)\wedge \left({B}\in {ℝ}^{*}\wedge {B}\ne \mathrm{-\infty }\right)\wedge \left({C}\in {ℝ}^{*}\wedge {C}\ne \mathrm{-\infty }\right)\right)\wedge {A}=\mathrm{+\infty }\right)\to \mathrm{+\infty }{+}_{𝑒}{B}=\mathrm{+\infty }$
82 79 81 eqtrd ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {A}\ne \mathrm{-\infty }\right)\wedge \left({B}\in {ℝ}^{*}\wedge {B}\ne \mathrm{-\infty }\right)\wedge \left({C}\in {ℝ}^{*}\wedge {C}\ne \mathrm{-\infty }\right)\right)\wedge {A}=\mathrm{+\infty }\right)\to {A}{+}_{𝑒}{B}=\mathrm{+\infty }$
83 82 oveq1d ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {A}\ne \mathrm{-\infty }\right)\wedge \left({B}\in {ℝ}^{*}\wedge {B}\ne \mathrm{-\infty }\right)\wedge \left({C}\in {ℝ}^{*}\wedge {C}\ne \mathrm{-\infty }\right)\right)\wedge {A}=\mathrm{+\infty }\right)\to \left({A}{+}_{𝑒}{B}\right){+}_{𝑒}{C}=\mathrm{+\infty }{+}_{𝑒}{C}$
84 78 oveq1d ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {A}\ne \mathrm{-\infty }\right)\wedge \left({B}\in {ℝ}^{*}\wedge {B}\ne \mathrm{-\infty }\right)\wedge \left({C}\in {ℝ}^{*}\wedge {C}\ne \mathrm{-\infty }\right)\right)\wedge {A}=\mathrm{+\infty }\right)\to {A}{+}_{𝑒}\left({B}{+}_{𝑒}{C}\right)=\mathrm{+\infty }{+}_{𝑒}\left({B}{+}_{𝑒}{C}\right)$
85 77 83 84 3eqtr4d ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {A}\ne \mathrm{-\infty }\right)\wedge \left({B}\in {ℝ}^{*}\wedge {B}\ne \mathrm{-\infty }\right)\wedge \left({C}\in {ℝ}^{*}\wedge {C}\ne \mathrm{-\infty }\right)\right)\wedge {A}=\mathrm{+\infty }\right)\to \left({A}{+}_{𝑒}{B}\right){+}_{𝑒}{C}={A}{+}_{𝑒}\left({B}{+}_{𝑒}{C}\right)$
86 simp1 ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {A}\ne \mathrm{-\infty }\right)\wedge \left({B}\in {ℝ}^{*}\wedge {B}\ne \mathrm{-\infty }\right)\wedge \left({C}\in {ℝ}^{*}\wedge {C}\ne \mathrm{-\infty }\right)\right)\to \left({A}\in {ℝ}^{*}\wedge {A}\ne \mathrm{-\infty }\right)$
87 xrnemnf ${⊢}\left({A}\in {ℝ}^{*}\wedge {A}\ne \mathrm{-\infty }\right)↔\left({A}\in ℝ\vee {A}=\mathrm{+\infty }\right)$
88 86 87 sylib ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {A}\ne \mathrm{-\infty }\right)\wedge \left({B}\in {ℝ}^{*}\wedge {B}\ne \mathrm{-\infty }\right)\wedge \left({C}\in {ℝ}^{*}\wedge {C}\ne \mathrm{-\infty }\right)\right)\to \left({A}\in ℝ\vee {A}=\mathrm{+\infty }\right)$
89 65 85 88 mpjaodan ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {A}\ne \mathrm{-\infty }\right)\wedge \left({B}\in {ℝ}^{*}\wedge {B}\ne \mathrm{-\infty }\right)\wedge \left({C}\in {ℝ}^{*}\wedge {C}\ne \mathrm{-\infty }\right)\right)\to \left({A}{+}_{𝑒}{B}\right){+}_{𝑒}{C}={A}{+}_{𝑒}\left({B}{+}_{𝑒}{C}\right)$