MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xaddass Structured version   Visualization version   GIF version

Theorem xaddass 13234
Description: Associativity of extended real addition. The correct condition here is "it is not the case that both +∞ and -∞ appear as one of 𝐴, 𝐵, 𝐶, i.e. ¬ {+∞, -∞} ⊆ {𝐴, 𝐵, 𝐶}", but this condition is difficult to work with, so we break the theorem into two parts: this one, where -∞ is not present in 𝐴, 𝐵, 𝐶, and xaddass2 13235, where +∞ is not present. (Contributed by Mario Carneiro, 20-Aug-2015.)
Assertion
Ref Expression
xaddass (((𝐴 ∈ ℝ*𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ*𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ*𝐶 ≠ -∞)) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 +𝑒 𝐶)))

Proof of Theorem xaddass
StepHypRef Expression
1 recn 11202 . . . . . . . . . 10 (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
2 recn 11202 . . . . . . . . . 10 (𝐵 ∈ ℝ → 𝐵 ∈ ℂ)
3 recn 11202 . . . . . . . . . 10 (𝐶 ∈ ℝ → 𝐶 ∈ ℂ)
4 addass 11199 . . . . . . . . . 10 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
51, 2, 3, 4syl3an 1157 . . . . . . . . 9 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
653expa 1115 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
7 readdcl 11195 . . . . . . . . 9 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
8 rexadd 13217 . . . . . . . . 9 (((𝐴 + 𝐵) ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) +𝑒 𝐶) = ((𝐴 + 𝐵) + 𝐶))
97, 8sylan 579 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) +𝑒 𝐶) = ((𝐴 + 𝐵) + 𝐶))
10 readdcl 11195 . . . . . . . . . 10 ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 + 𝐶) ∈ ℝ)
11 rexadd 13217 . . . . . . . . . 10 ((𝐴 ∈ ℝ ∧ (𝐵 + 𝐶) ∈ ℝ) → (𝐴 +𝑒 (𝐵 + 𝐶)) = (𝐴 + (𝐵 + 𝐶)))
1210, 11sylan2 592 . . . . . . . . 9 ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ)) → (𝐴 +𝑒 (𝐵 + 𝐶)) = (𝐴 + (𝐵 + 𝐶)))
1312anassrs 467 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ) → (𝐴 +𝑒 (𝐵 + 𝐶)) = (𝐴 + (𝐵 + 𝐶)))
146, 9, 133eqtr4d 2776 . . . . . . 7 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 + 𝐶)))
15 rexadd 13217 . . . . . . . . 9 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 +𝑒 𝐵) = (𝐴 + 𝐵))
1615adantr 480 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ) → (𝐴 +𝑒 𝐵) = (𝐴 + 𝐵))
1716oveq1d 7420 . . . . . . 7 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = ((𝐴 + 𝐵) +𝑒 𝐶))
18 rexadd 13217 . . . . . . . . 9 ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 +𝑒 𝐶) = (𝐵 + 𝐶))
1918adantll 711 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ) → (𝐵 +𝑒 𝐶) = (𝐵 + 𝐶))
2019oveq2d 7421 . . . . . . 7 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ) → (𝐴 +𝑒 (𝐵 +𝑒 𝐶)) = (𝐴 +𝑒 (𝐵 + 𝐶)))
2114, 17, 203eqtr4d 2776 . . . . . 6 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 +𝑒 𝐶)))
2221adantll 711 . . . . 5 (((((𝐴 ∈ ℝ*𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ*𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ*𝐶 ≠ -∞)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ 𝐶 ∈ ℝ) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 +𝑒 𝐶)))
23 oveq2 7413 . . . . . . . . 9 (𝐶 = +∞ → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = ((𝐴 +𝑒 𝐵) +𝑒 +∞))
24 simp1l 1194 . . . . . . . . . . 11 (((𝐴 ∈ ℝ*𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ*𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ*𝐶 ≠ -∞)) → 𝐴 ∈ ℝ*)
25 simp2l 1196 . . . . . . . . . . 11 (((𝐴 ∈ ℝ*𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ*𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ*𝐶 ≠ -∞)) → 𝐵 ∈ ℝ*)
26 xaddcl 13224 . . . . . . . . . . 11 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴 +𝑒 𝐵) ∈ ℝ*)
2724, 25, 26syl2anc 583 . . . . . . . . . 10 (((𝐴 ∈ ℝ*𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ*𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ*𝐶 ≠ -∞)) → (𝐴 +𝑒 𝐵) ∈ ℝ*)
28 xaddnemnf 13221 . . . . . . . . . . 11 (((𝐴 ∈ ℝ*𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ*𝐵 ≠ -∞)) → (𝐴 +𝑒 𝐵) ≠ -∞)
29283adant3 1129 . . . . . . . . . 10 (((𝐴 ∈ ℝ*𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ*𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ*𝐶 ≠ -∞)) → (𝐴 +𝑒 𝐵) ≠ -∞)
30 xaddpnf1 13211 . . . . . . . . . 10 (((𝐴 +𝑒 𝐵) ∈ ℝ* ∧ (𝐴 +𝑒 𝐵) ≠ -∞) → ((𝐴 +𝑒 𝐵) +𝑒 +∞) = +∞)
3127, 29, 30syl2anc 583 . . . . . . . . 9 (((𝐴 ∈ ℝ*𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ*𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ*𝐶 ≠ -∞)) → ((𝐴 +𝑒 𝐵) +𝑒 +∞) = +∞)
3223, 31sylan9eqr 2788 . . . . . . . 8 ((((𝐴 ∈ ℝ*𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ*𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ*𝐶 ≠ -∞)) ∧ 𝐶 = +∞) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = +∞)
33 xaddpnf1 13211 . . . . . . . . . 10 ((𝐴 ∈ ℝ*𝐴 ≠ -∞) → (𝐴 +𝑒 +∞) = +∞)
34333ad2ant1 1130 . . . . . . . . 9 (((𝐴 ∈ ℝ*𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ*𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ*𝐶 ≠ -∞)) → (𝐴 +𝑒 +∞) = +∞)
3534adantr 480 . . . . . . . 8 ((((𝐴 ∈ ℝ*𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ*𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ*𝐶 ≠ -∞)) ∧ 𝐶 = +∞) → (𝐴 +𝑒 +∞) = +∞)
3632, 35eqtr4d 2769 . . . . . . 7 ((((𝐴 ∈ ℝ*𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ*𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ*𝐶 ≠ -∞)) ∧ 𝐶 = +∞) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 +∞))
37 oveq2 7413 . . . . . . . . 9 (𝐶 = +∞ → (𝐵 +𝑒 𝐶) = (𝐵 +𝑒 +∞))
38 xaddpnf1 13211 . . . . . . . . . 10 ((𝐵 ∈ ℝ*𝐵 ≠ -∞) → (𝐵 +𝑒 +∞) = +∞)
39383ad2ant2 1131 . . . . . . . . 9 (((𝐴 ∈ ℝ*𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ*𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ*𝐶 ≠ -∞)) → (𝐵 +𝑒 +∞) = +∞)
4037, 39sylan9eqr 2788 . . . . . . . 8 ((((𝐴 ∈ ℝ*𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ*𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ*𝐶 ≠ -∞)) ∧ 𝐶 = +∞) → (𝐵 +𝑒 𝐶) = +∞)
4140oveq2d 7421 . . . . . . 7 ((((𝐴 ∈ ℝ*𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ*𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ*𝐶 ≠ -∞)) ∧ 𝐶 = +∞) → (𝐴 +𝑒 (𝐵 +𝑒 𝐶)) = (𝐴 +𝑒 +∞))
4236, 41eqtr4d 2769 . . . . . 6 ((((𝐴 ∈ ℝ*𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ*𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ*𝐶 ≠ -∞)) ∧ 𝐶 = +∞) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 +𝑒 𝐶)))
4342adantlr 712 . . . . 5 (((((𝐴 ∈ ℝ*𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ*𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ*𝐶 ≠ -∞)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ 𝐶 = +∞) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 +𝑒 𝐶)))
44 simp3 1135 . . . . . . 7 (((𝐴 ∈ ℝ*𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ*𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ*𝐶 ≠ -∞)) → (𝐶 ∈ ℝ*𝐶 ≠ -∞))
45 xrnemnf 13103 . . . . . . 7 ((𝐶 ∈ ℝ*𝐶 ≠ -∞) ↔ (𝐶 ∈ ℝ ∨ 𝐶 = +∞))
4644, 45sylib 217 . . . . . 6 (((𝐴 ∈ ℝ*𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ*𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ*𝐶 ≠ -∞)) → (𝐶 ∈ ℝ ∨ 𝐶 = +∞))
4746adantr 480 . . . . 5 ((((𝐴 ∈ ℝ*𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ*𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ*𝐶 ≠ -∞)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) → (𝐶 ∈ ℝ ∨ 𝐶 = +∞))
4822, 43, 47mpjaodan 955 . . . 4 ((((𝐴 ∈ ℝ*𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ*𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ*𝐶 ≠ -∞)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 +𝑒 𝐶)))
4948anassrs 467 . . 3 (((((𝐴 ∈ ℝ*𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ*𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ*𝐶 ≠ -∞)) ∧ 𝐴 ∈ ℝ) ∧ 𝐵 ∈ ℝ) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 +𝑒 𝐶)))
50 xaddpnf2 13212 . . . . . . . 8 ((𝐶 ∈ ℝ*𝐶 ≠ -∞) → (+∞ +𝑒 𝐶) = +∞)
51503ad2ant3 1132 . . . . . . 7 (((𝐴 ∈ ℝ*𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ*𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ*𝐶 ≠ -∞)) → (+∞ +𝑒 𝐶) = +∞)
5251, 34eqtr4d 2769 . . . . . 6 (((𝐴 ∈ ℝ*𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ*𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ*𝐶 ≠ -∞)) → (+∞ +𝑒 𝐶) = (𝐴 +𝑒 +∞))
5352adantr 480 . . . . 5 ((((𝐴 ∈ ℝ*𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ*𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ*𝐶 ≠ -∞)) ∧ 𝐵 = +∞) → (+∞ +𝑒 𝐶) = (𝐴 +𝑒 +∞))
54 oveq2 7413 . . . . . . 7 (𝐵 = +∞ → (𝐴 +𝑒 𝐵) = (𝐴 +𝑒 +∞))
5554, 34sylan9eqr 2788 . . . . . 6 ((((𝐴 ∈ ℝ*𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ*𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ*𝐶 ≠ -∞)) ∧ 𝐵 = +∞) → (𝐴 +𝑒 𝐵) = +∞)
5655oveq1d 7420 . . . . 5 ((((𝐴 ∈ ℝ*𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ*𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ*𝐶 ≠ -∞)) ∧ 𝐵 = +∞) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (+∞ +𝑒 𝐶))
57 oveq1 7412 . . . . . . 7 (𝐵 = +∞ → (𝐵 +𝑒 𝐶) = (+∞ +𝑒 𝐶))
5857, 51sylan9eqr 2788 . . . . . 6 ((((𝐴 ∈ ℝ*𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ*𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ*𝐶 ≠ -∞)) ∧ 𝐵 = +∞) → (𝐵 +𝑒 𝐶) = +∞)
5958oveq2d 7421 . . . . 5 ((((𝐴 ∈ ℝ*𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ*𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ*𝐶 ≠ -∞)) ∧ 𝐵 = +∞) → (𝐴 +𝑒 (𝐵 +𝑒 𝐶)) = (𝐴 +𝑒 +∞))
6053, 56, 593eqtr4d 2776 . . . 4 ((((𝐴 ∈ ℝ*𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ*𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ*𝐶 ≠ -∞)) ∧ 𝐵 = +∞) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 +𝑒 𝐶)))
6160adantlr 712 . . 3 (((((𝐴 ∈ ℝ*𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ*𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ*𝐶 ≠ -∞)) ∧ 𝐴 ∈ ℝ) ∧ 𝐵 = +∞) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 +𝑒 𝐶)))
62 simpl2 1189 . . . 4 ((((𝐴 ∈ ℝ*𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ*𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ*𝐶 ≠ -∞)) ∧ 𝐴 ∈ ℝ) → (𝐵 ∈ ℝ*𝐵 ≠ -∞))
63 xrnemnf 13103 . . . 4 ((𝐵 ∈ ℝ*𝐵 ≠ -∞) ↔ (𝐵 ∈ ℝ ∨ 𝐵 = +∞))
6462, 63sylib 217 . . 3 ((((𝐴 ∈ ℝ*𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ*𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ*𝐶 ≠ -∞)) ∧ 𝐴 ∈ ℝ) → (𝐵 ∈ ℝ ∨ 𝐵 = +∞))
6549, 61, 64mpjaodan 955 . 2 ((((𝐴 ∈ ℝ*𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ*𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ*𝐶 ≠ -∞)) ∧ 𝐴 ∈ ℝ) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 +𝑒 𝐶)))
66 simpl3 1190 . . . . 5 ((((𝐴 ∈ ℝ*𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ*𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ*𝐶 ≠ -∞)) ∧ 𝐴 = +∞) → (𝐶 ∈ ℝ*𝐶 ≠ -∞))
6766, 50syl 17 . . . 4 ((((𝐴 ∈ ℝ*𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ*𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ*𝐶 ≠ -∞)) ∧ 𝐴 = +∞) → (+∞ +𝑒 𝐶) = +∞)
68 simpl2l 1223 . . . . . 6 ((((𝐴 ∈ ℝ*𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ*𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ*𝐶 ≠ -∞)) ∧ 𝐴 = +∞) → 𝐵 ∈ ℝ*)
69 simpl3l 1225 . . . . . 6 ((((𝐴 ∈ ℝ*𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ*𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ*𝐶 ≠ -∞)) ∧ 𝐴 = +∞) → 𝐶 ∈ ℝ*)
70 xaddcl 13224 . . . . . 6 ((𝐵 ∈ ℝ*𝐶 ∈ ℝ*) → (𝐵 +𝑒 𝐶) ∈ ℝ*)
7168, 69, 70syl2anc 583 . . . . 5 ((((𝐴 ∈ ℝ*𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ*𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ*𝐶 ≠ -∞)) ∧ 𝐴 = +∞) → (𝐵 +𝑒 𝐶) ∈ ℝ*)
72 simpl2 1189 . . . . . 6 ((((𝐴 ∈ ℝ*𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ*𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ*𝐶 ≠ -∞)) ∧ 𝐴 = +∞) → (𝐵 ∈ ℝ*𝐵 ≠ -∞))
73 xaddnemnf 13221 . . . . . 6 (((𝐵 ∈ ℝ*𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ*𝐶 ≠ -∞)) → (𝐵 +𝑒 𝐶) ≠ -∞)
7472, 66, 73syl2anc 583 . . . . 5 ((((𝐴 ∈ ℝ*𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ*𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ*𝐶 ≠ -∞)) ∧ 𝐴 = +∞) → (𝐵 +𝑒 𝐶) ≠ -∞)
75 xaddpnf2 13212 . . . . 5 (((𝐵 +𝑒 𝐶) ∈ ℝ* ∧ (𝐵 +𝑒 𝐶) ≠ -∞) → (+∞ +𝑒 (𝐵 +𝑒 𝐶)) = +∞)
7671, 74, 75syl2anc 583 . . . 4 ((((𝐴 ∈ ℝ*𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ*𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ*𝐶 ≠ -∞)) ∧ 𝐴 = +∞) → (+∞ +𝑒 (𝐵 +𝑒 𝐶)) = +∞)
7767, 76eqtr4d 2769 . . 3 ((((𝐴 ∈ ℝ*𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ*𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ*𝐶 ≠ -∞)) ∧ 𝐴 = +∞) → (+∞ +𝑒 𝐶) = (+∞ +𝑒 (𝐵 +𝑒 𝐶)))
78 simpr 484 . . . . . 6 ((((𝐴 ∈ ℝ*𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ*𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ*𝐶 ≠ -∞)) ∧ 𝐴 = +∞) → 𝐴 = +∞)
7978oveq1d 7420 . . . . 5 ((((𝐴 ∈ ℝ*𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ*𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ*𝐶 ≠ -∞)) ∧ 𝐴 = +∞) → (𝐴 +𝑒 𝐵) = (+∞ +𝑒 𝐵))
80 xaddpnf2 13212 . . . . . 6 ((𝐵 ∈ ℝ*𝐵 ≠ -∞) → (+∞ +𝑒 𝐵) = +∞)
8172, 80syl 17 . . . . 5 ((((𝐴 ∈ ℝ*𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ*𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ*𝐶 ≠ -∞)) ∧ 𝐴 = +∞) → (+∞ +𝑒 𝐵) = +∞)
8279, 81eqtrd 2766 . . . 4 ((((𝐴 ∈ ℝ*𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ*𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ*𝐶 ≠ -∞)) ∧ 𝐴 = +∞) → (𝐴 +𝑒 𝐵) = +∞)
8382oveq1d 7420 . . 3 ((((𝐴 ∈ ℝ*𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ*𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ*𝐶 ≠ -∞)) ∧ 𝐴 = +∞) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (+∞ +𝑒 𝐶))
8478oveq1d 7420 . . 3 ((((𝐴 ∈ ℝ*𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ*𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ*𝐶 ≠ -∞)) ∧ 𝐴 = +∞) → (𝐴 +𝑒 (𝐵 +𝑒 𝐶)) = (+∞ +𝑒 (𝐵 +𝑒 𝐶)))
8577, 83, 843eqtr4d 2776 . 2 ((((𝐴 ∈ ℝ*𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ*𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ*𝐶 ≠ -∞)) ∧ 𝐴 = +∞) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 +𝑒 𝐶)))
86 simp1 1133 . . 3 (((𝐴 ∈ ℝ*𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ*𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ*𝐶 ≠ -∞)) → (𝐴 ∈ ℝ*𝐴 ≠ -∞))
87 xrnemnf 13103 . . 3 ((𝐴 ∈ ℝ*𝐴 ≠ -∞) ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞))
8886, 87sylib 217 . 2 (((𝐴 ∈ ℝ*𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ*𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ*𝐶 ≠ -∞)) → (𝐴 ∈ ℝ ∨ 𝐴 = +∞))
8965, 85, 88mpjaodan 955 1 (((𝐴 ∈ ℝ*𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ*𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ*𝐶 ≠ -∞)) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 +𝑒 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wo 844  w3a 1084   = wceq 1533  wcel 2098  wne 2934  (class class class)co 7405  cc 11110  cr 11111   + caddc 11115  +∞cpnf 11249  -∞cmnf 11250  *cxr 11251   +𝑒 cxad 13096
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2697  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7722  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-addass 11177  ax-i2m1 11180  ax-rnegex 11183  ax-cnre 11185
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-nel 3041  df-ral 3056  df-rex 3065  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-id 5567  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-iota 6489  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7408  df-oprab 7409  df-mpo 7410  df-1st 7974  df-2nd 7975  df-er 8705  df-en 8942  df-dom 8943  df-sdom 8944  df-pnf 11254  df-mnf 11255  df-xr 11256  df-xadd 13099
This theorem is referenced by:  xaddass2  13235  xpncan  13236  xadd4d  13288  xrs1mnd  21298  xlt2addrd  32478  xrge0addass  32694  xrge0npcan  32698  carsgclctunlem2  33848  caragenuncllem  45797
  Copyright terms: Public domain W3C validator