Theorem xaddass

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	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞ ) ∧ ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞ ) ∧ ( 𝐶 ∈ ℝ* ∧ 𝐶 ≠ -∞ ) ) → ( ( 𝐴 +𝑒 𝐵 ) +𝑒 𝐶 ) = ( 𝐴 +𝑒 ( 𝐵 +𝑒 𝐶 ) ) )

Proof

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