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