Metamath Proof Explorer

Theorem xrge0adddir

Description: Right-distributivity of extended nonnegative real multiplication over addition. (Contributed by Thierry Arnoux, 30-Jun-2017)

Ref Expression
Assertion xrge0adddir ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ → A + 𝑒 B ⋅ 𝑒 C = A ⋅ 𝑒 C + 𝑒 B ⋅ 𝑒 C

Proof

Step Hyp Ref Expression
1 iccssxr ⊢ 0 +∞ ⊆ ℝ *
2 simpl1 ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ ∧ C ∈ 0 +∞ → A ∈ 0 +∞
3 1 2 sselid ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ ∧ C ∈ 0 +∞ → A ∈ ℝ *
4 simpl2 ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ ∧ C ∈ 0 +∞ → B ∈ 0 +∞
5 1 4 sselid ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ ∧ C ∈ 0 +∞ → B ∈ ℝ *
6 rge0ssre ⊢ 0 +∞ ⊆ ℝ
7 simpr ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ ∧ C ∈ 0 +∞ → C ∈ 0 +∞
8 6 7 sselid ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ ∧ C ∈ 0 +∞ → C ∈ ℝ
9 xadddir ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ → A + 𝑒 B ⋅ 𝑒 C = A ⋅ 𝑒 C + 𝑒 B ⋅ 𝑒 C
10 3 5 8 9 syl3anc ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ ∧ C ∈ 0 +∞ → A + 𝑒 B ⋅ 𝑒 C = A ⋅ 𝑒 C + 𝑒 B ⋅ 𝑒 C
11 simpll1 ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ ∧ C = +∞ ∧ 0 < A → A ∈ 0 +∞
12 1 11 sselid ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ ∧ C = +∞ ∧ 0 < A → A ∈ ℝ *
13 simpll2 ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ ∧ C = +∞ ∧ 0 < A → B ∈ 0 +∞
14 1 13 sselid ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ ∧ C = +∞ ∧ 0 < A → B ∈ ℝ *
15 12 14 xaddcld ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ ∧ C = +∞ ∧ 0 < A → A + 𝑒 B ∈ ℝ *
16 simpr ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ ∧ C = +∞ ∧ 0 < A → 0 < A
17 xrge0addgt0 ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ 0 < A → 0 < A + 𝑒 B
18 11 13 16 17 syl21anc ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ ∧ C = +∞ ∧ 0 < A → 0 < A + 𝑒 B
19 xmulpnf1 ⊢ A + 𝑒 B ∈ ℝ * ∧ 0 < A + 𝑒 B → A + 𝑒 B ⋅ 𝑒 +∞ = +∞
20 15 18 19 syl2anc ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ ∧ C = +∞ ∧ 0 < A → A + 𝑒 B ⋅ 𝑒 +∞ = +∞
21 oveq2 ⊢ C = +∞ → A + 𝑒 B ⋅ 𝑒 C = A + 𝑒 B ⋅ 𝑒 +∞
22 21 ad2antlr ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ ∧ C = +∞ ∧ 0 < A → A + 𝑒 B ⋅ 𝑒 C = A + 𝑒 B ⋅ 𝑒 +∞
23 simpll3 ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ ∧ C = +∞ ∧ 0 < A → C ∈ 0 +∞
24 ge0xmulcl ⊢ B ∈ 0 +∞ ∧ C ∈ 0 +∞ → B ⋅ 𝑒 C ∈ 0 +∞
25 13 23 24 syl2anc ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ ∧ C = +∞ ∧ 0 < A → B ⋅ 𝑒 C ∈ 0 +∞
26 1 25 sselid ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ ∧ C = +∞ ∧ 0 < A → B ⋅ 𝑒 C ∈ ℝ *
27 xrge0neqmnf ⊢ B ⋅ 𝑒 C ∈ 0 +∞ → B ⋅ 𝑒 C ≠ −∞
28 25 27 syl ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ ∧ C = +∞ ∧ 0 < A → B ⋅ 𝑒 C ≠ −∞
29 xaddpnf2 ⊢ B ⋅ 𝑒 C ∈ ℝ * ∧ B ⋅ 𝑒 C ≠ −∞ → +∞ + 𝑒 B ⋅ 𝑒 C = +∞
30 26 28 29 syl2anc ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ ∧ C = +∞ ∧ 0 < A → +∞ + 𝑒 B ⋅ 𝑒 C = +∞
31 20 22 30 3eqtr4d ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ ∧ C = +∞ ∧ 0 < A → A + 𝑒 B ⋅ 𝑒 C = +∞ + 𝑒 B ⋅ 𝑒 C
32 oveq2 ⊢ C = +∞ → A ⋅ 𝑒 C = A ⋅ 𝑒 +∞
33 32 ad2antlr ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ ∧ C = +∞ ∧ 0 < A → A ⋅ 𝑒 C = A ⋅ 𝑒 +∞
34 xmulpnf1 ⊢ A ∈ ℝ * ∧ 0 < A → A ⋅ 𝑒 +∞ = +∞
35 12 16 34 syl2anc ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ ∧ C = +∞ ∧ 0 < A → A ⋅ 𝑒 +∞ = +∞
36 33 35 eqtrd ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ ∧ C = +∞ ∧ 0 < A → A ⋅ 𝑒 C = +∞
37 36 oveq1d ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ ∧ C = +∞ ∧ 0 < A → A ⋅ 𝑒 C + 𝑒 B ⋅ 𝑒 C = +∞ + 𝑒 B ⋅ 𝑒 C
38 31 37 eqtr4d ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ ∧ C = +∞ ∧ 0 < A → A + 𝑒 B ⋅ 𝑒 C = A ⋅ 𝑒 C + 𝑒 B ⋅ 𝑒 C
39 simpll3 ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ ∧ C = +∞ ∧ 0 = A → C ∈ 0 +∞
40 1 39 sselid ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ ∧ C = +∞ ∧ 0 = A → C ∈ ℝ *
41 xmul02 ⊢ C ∈ ℝ * → 0 ⋅ 𝑒 C = 0
42 40 41 syl ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ ∧ C = +∞ ∧ 0 = A → 0 ⋅ 𝑒 C = 0
43 42 oveq1d ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ ∧ C = +∞ ∧ 0 = A → 0 ⋅ 𝑒 C + 𝑒 B ⋅ 𝑒 C = 0 + 𝑒 B ⋅ 𝑒 C
44 oveq1 ⊢ 0 = A → 0 ⋅ 𝑒 C = A ⋅ 𝑒 C
45 44 adantl ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ ∧ C = +∞ ∧ 0 = A → 0 ⋅ 𝑒 C = A ⋅ 𝑒 C
46 45 oveq1d ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ ∧ C = +∞ ∧ 0 = A → 0 ⋅ 𝑒 C + 𝑒 B ⋅ 𝑒 C = A ⋅ 𝑒 C + 𝑒 B ⋅ 𝑒 C
47 simpll2 ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ ∧ C = +∞ ∧ 0 = A → B ∈ 0 +∞
48 1 47 sselid ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ ∧ C = +∞ ∧ 0 = A → B ∈ ℝ *
49 48 40 xmulcld ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ ∧ C = +∞ ∧ 0 = A → B ⋅ 𝑒 C ∈ ℝ *
50 xaddlid ⊢ B ⋅ 𝑒 C ∈ ℝ * → 0 + 𝑒 B ⋅ 𝑒 C = B ⋅ 𝑒 C
51 49 50 syl ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ ∧ C = +∞ ∧ 0 = A → 0 + 𝑒 B ⋅ 𝑒 C = B ⋅ 𝑒 C
52 43 46 51 3eqtr3d ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ ∧ C = +∞ ∧ 0 = A → A ⋅ 𝑒 C + 𝑒 B ⋅ 𝑒 C = B ⋅ 𝑒 C
53 xaddlid ⊢ B ∈ ℝ * → 0 + 𝑒 B = B
54 48 53 syl ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ ∧ C = +∞ ∧ 0 = A → 0 + 𝑒 B = B
55 54 oveq1d ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ ∧ C = +∞ ∧ 0 = A → 0 + 𝑒 B ⋅ 𝑒 C = B ⋅ 𝑒 C
56 oveq1 ⊢ 0 = A → 0 + 𝑒 B = A + 𝑒 B
57 56 oveq1d ⊢ 0 = A → 0 + 𝑒 B ⋅ 𝑒 C = A + 𝑒 B ⋅ 𝑒 C
58 57 adantl ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ ∧ C = +∞ ∧ 0 = A → 0 + 𝑒 B ⋅ 𝑒 C = A + 𝑒 B ⋅ 𝑒 C
59 52 55 58 3eqtr2rd ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ ∧ C = +∞ ∧ 0 = A → A + 𝑒 B ⋅ 𝑒 C = A ⋅ 𝑒 C + 𝑒 B ⋅ 𝑒 C
60 0xr ⊢ 0 ∈ ℝ *
61 60 a1i ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ ∧ C = +∞ → 0 ∈ ℝ *
62 simpl1 ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ ∧ C = +∞ → A ∈ 0 +∞
63 1 62 sselid ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ ∧ C = +∞ → A ∈ ℝ *
64 pnfxr ⊢ +∞ ∈ ℝ *
65 64 a1i ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ ∧ C = +∞ → +∞ ∈ ℝ *
66 iccgelb ⊢ 0 ∈ ℝ * ∧ +∞ ∈ ℝ * ∧ A ∈ 0 +∞ → 0 ≤ A
67 61 65 62 66 syl3anc ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ ∧ C = +∞ → 0 ≤ A
68 xrleloe ⊢ 0 ∈ ℝ * ∧ A ∈ ℝ * → 0 ≤ A ↔ 0 < A ∨ 0 = A
69 68 biimpa ⊢ 0 ∈ ℝ * ∧ A ∈ ℝ * ∧ 0 ≤ A → 0 < A ∨ 0 = A
70 61 63 67 69 syl21anc ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ ∧ C = +∞ → 0 < A ∨ 0 = A
71 38 59 70 mpjaodan ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ ∧ C = +∞ → A + 𝑒 B ⋅ 𝑒 C = A ⋅ 𝑒 C + 𝑒 B ⋅ 𝑒 C
72 0lepnf ⊢ 0 ≤ +∞
73 eliccelico ⊢ 0 ∈ ℝ * ∧ +∞ ∈ ℝ * ∧ 0 ≤ +∞ → C ∈ 0 +∞ ↔ C ∈ 0 +∞ ∨ C = +∞
74 60 64 72 73 mp3an ⊢ C ∈ 0 +∞ ↔ C ∈ 0 +∞ ∨ C = +∞
75 74 3anbi3i ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ ↔ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ ∨ C = +∞
76 75 simp3bi ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ → C ∈ 0 +∞ ∨ C = +∞
77 10 71 76 mpjaodan ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ → A + 𝑒 B ⋅ 𝑒 C = A ⋅ 𝑒 C + 𝑒 B ⋅ 𝑒 C