This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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