Step | Hyp | Ref
| Expression |
1 | | iccssxr 13407 |
. . . 4
โข
(0[,]+โ) โ โ* |
2 | | simpl1 1192 |
. . . 4
โข (((๐ด โ (0[,]+โ) โง
๐ต โ (0[,]+โ)
โง ๐ถ โ
(0[,]+โ)) โง ๐ถ
โ (0[,)+โ)) โ ๐ด โ (0[,]+โ)) |
3 | 1, 2 | sselid 3981 |
. . 3
โข (((๐ด โ (0[,]+โ) โง
๐ต โ (0[,]+โ)
โง ๐ถ โ
(0[,]+โ)) โง ๐ถ
โ (0[,)+โ)) โ ๐ด โ
โ*) |
4 | | simpl2 1193 |
. . . 4
โข (((๐ด โ (0[,]+โ) โง
๐ต โ (0[,]+โ)
โง ๐ถ โ
(0[,]+โ)) โง ๐ถ
โ (0[,)+โ)) โ ๐ต โ (0[,]+โ)) |
5 | 1, 4 | sselid 3981 |
. . 3
โข (((๐ด โ (0[,]+โ) โง
๐ต โ (0[,]+โ)
โง ๐ถ โ
(0[,]+โ)) โง ๐ถ
โ (0[,)+โ)) โ ๐ต โ
โ*) |
6 | | rge0ssre 13433 |
. . . 4
โข
(0[,)+โ) โ โ |
7 | | simpr 486 |
. . . 4
โข (((๐ด โ (0[,]+โ) โง
๐ต โ (0[,]+โ)
โง ๐ถ โ
(0[,]+โ)) โง ๐ถ
โ (0[,)+โ)) โ ๐ถ โ (0[,)+โ)) |
8 | 6, 7 | sselid 3981 |
. . 3
โข (((๐ด โ (0[,]+โ) โง
๐ต โ (0[,]+โ)
โง ๐ถ โ
(0[,]+โ)) โง ๐ถ
โ (0[,)+โ)) โ ๐ถ โ โ) |
9 | | xadddir 13275 |
. . 3
โข ((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ) โ ((๐ด
+๐ ๐ต)
ยทe ๐ถ) =
((๐ด ยทe
๐ถ) +๐
(๐ต ยทe
๐ถ))) |
10 | 3, 5, 8, 9 | syl3anc 1372 |
. 2
โข (((๐ด โ (0[,]+โ) โง
๐ต โ (0[,]+โ)
โง ๐ถ โ
(0[,]+โ)) โง ๐ถ
โ (0[,)+โ)) โ ((๐ด +๐ ๐ต) ยทe ๐ถ) = ((๐ด ยทe ๐ถ) +๐ (๐ต ยทe ๐ถ))) |
11 | | simpll1 1213 |
. . . . . . . 8
โข ((((๐ด โ (0[,]+โ) โง
๐ต โ (0[,]+โ)
โง ๐ถ โ
(0[,]+โ)) โง ๐ถ =
+โ) โง 0 < ๐ด)
โ ๐ด โ
(0[,]+โ)) |
12 | 1, 11 | sselid 3981 |
. . . . . . 7
โข ((((๐ด โ (0[,]+โ) โง
๐ต โ (0[,]+โ)
โง ๐ถ โ
(0[,]+โ)) โง ๐ถ =
+โ) โง 0 < ๐ด)
โ ๐ด โ
โ*) |
13 | | simpll2 1214 |
. . . . . . . 8
โข ((((๐ด โ (0[,]+โ) โง
๐ต โ (0[,]+โ)
โง ๐ถ โ
(0[,]+โ)) โง ๐ถ =
+โ) โง 0 < ๐ด)
โ ๐ต โ
(0[,]+โ)) |
14 | 1, 13 | sselid 3981 |
. . . . . . 7
โข ((((๐ด โ (0[,]+โ) โง
๐ต โ (0[,]+โ)
โง ๐ถ โ
(0[,]+โ)) โง ๐ถ =
+โ) โง 0 < ๐ด)
โ ๐ต โ
โ*) |
15 | 12, 14 | xaddcld 13280 |
. . . . . 6
โข ((((๐ด โ (0[,]+โ) โง
๐ต โ (0[,]+โ)
โง ๐ถ โ
(0[,]+โ)) โง ๐ถ =
+โ) โง 0 < ๐ด)
โ (๐ด
+๐ ๐ต)
โ โ*) |
16 | | simpr 486 |
. . . . . . 7
โข ((((๐ด โ (0[,]+โ) โง
๐ต โ (0[,]+โ)
โง ๐ถ โ
(0[,]+โ)) โง ๐ถ =
+โ) โง 0 < ๐ด)
โ 0 < ๐ด) |
17 | | xrge0addgt0 32192 |
. . . . . . 7
โข (((๐ด โ (0[,]+โ) โง
๐ต โ (0[,]+โ))
โง 0 < ๐ด) โ 0
< (๐ด
+๐ ๐ต)) |
18 | 11, 13, 16, 17 | syl21anc 837 |
. . . . . 6
โข ((((๐ด โ (0[,]+โ) โง
๐ต โ (0[,]+โ)
โง ๐ถ โ
(0[,]+โ)) โง ๐ถ =
+โ) โง 0 < ๐ด)
โ 0 < (๐ด
+๐ ๐ต)) |
19 | | xmulpnf1 13253 |
. . . . . 6
โข (((๐ด +๐ ๐ต) โ โ*
โง 0 < (๐ด
+๐ ๐ต))
โ ((๐ด
+๐ ๐ต)
ยทe +โ) = +โ) |
20 | 15, 18, 19 | syl2anc 585 |
. . . . 5
โข ((((๐ด โ (0[,]+โ) โง
๐ต โ (0[,]+โ)
โง ๐ถ โ
(0[,]+โ)) โง ๐ถ =
+โ) โง 0 < ๐ด)
โ ((๐ด
+๐ ๐ต)
ยทe +โ) = +โ) |
21 | | oveq2 7417 |
. . . . . 6
โข (๐ถ = +โ โ ((๐ด +๐ ๐ต) ยทe ๐ถ) = ((๐ด +๐ ๐ต) ยทe
+โ)) |
22 | 21 | ad2antlr 726 |
. . . . 5
โข ((((๐ด โ (0[,]+โ) โง
๐ต โ (0[,]+โ)
โง ๐ถ โ
(0[,]+โ)) โง ๐ถ =
+โ) โง 0 < ๐ด)
โ ((๐ด
+๐ ๐ต)
ยทe ๐ถ) =
((๐ด +๐
๐ต) ยทe
+โ)) |
23 | | simpll3 1215 |
. . . . . . . 8
โข ((((๐ด โ (0[,]+โ) โง
๐ต โ (0[,]+โ)
โง ๐ถ โ
(0[,]+โ)) โง ๐ถ =
+โ) โง 0 < ๐ด)
โ ๐ถ โ
(0[,]+โ)) |
24 | | ge0xmulcl 13440 |
. . . . . . . 8
โข ((๐ต โ (0[,]+โ) โง
๐ถ โ (0[,]+โ))
โ (๐ต
ยทe ๐ถ)
โ (0[,]+โ)) |
25 | 13, 23, 24 | syl2anc 585 |
. . . . . . 7
โข ((((๐ด โ (0[,]+โ) โง
๐ต โ (0[,]+โ)
โง ๐ถ โ
(0[,]+โ)) โง ๐ถ =
+โ) โง 0 < ๐ด)
โ (๐ต
ยทe ๐ถ)
โ (0[,]+โ)) |
26 | 1, 25 | sselid 3981 |
. . . . . 6
โข ((((๐ด โ (0[,]+โ) โง
๐ต โ (0[,]+โ)
โง ๐ถ โ
(0[,]+โ)) โง ๐ถ =
+โ) โง 0 < ๐ด)
โ (๐ต
ยทe ๐ถ)
โ โ*) |
27 | | xrge0neqmnf 13429 |
. . . . . . 7
โข ((๐ต ยทe ๐ถ) โ (0[,]+โ) โ
(๐ต ยทe
๐ถ) โ
-โ) |
28 | 25, 27 | syl 17 |
. . . . . 6
โข ((((๐ด โ (0[,]+โ) โง
๐ต โ (0[,]+โ)
โง ๐ถ โ
(0[,]+โ)) โง ๐ถ =
+โ) โง 0 < ๐ด)
โ (๐ต
ยทe ๐ถ)
โ -โ) |
29 | | xaddpnf2 13206 |
. . . . . 6
โข (((๐ต ยทe ๐ถ) โ โ*
โง (๐ต
ยทe ๐ถ)
โ -โ) โ (+โ +๐ (๐ต ยทe ๐ถ)) = +โ) |
30 | 26, 28, 29 | syl2anc 585 |
. . . . 5
โข ((((๐ด โ (0[,]+โ) โง
๐ต โ (0[,]+โ)
โง ๐ถ โ
(0[,]+โ)) โง ๐ถ =
+โ) โง 0 < ๐ด)
โ (+โ +๐ (๐ต ยทe ๐ถ)) = +โ) |
31 | 20, 22, 30 | 3eqtr4d 2783 |
. . . 4
โข ((((๐ด โ (0[,]+โ) โง
๐ต โ (0[,]+โ)
โง ๐ถ โ
(0[,]+โ)) โง ๐ถ =
+โ) โง 0 < ๐ด)
โ ((๐ด
+๐ ๐ต)
ยทe ๐ถ) =
(+โ +๐ (๐ต ยทe ๐ถ))) |
32 | | oveq2 7417 |
. . . . . . 7
โข (๐ถ = +โ โ (๐ด ยทe ๐ถ) = (๐ด ยทe
+โ)) |
33 | 32 | ad2antlr 726 |
. . . . . 6
โข ((((๐ด โ (0[,]+โ) โง
๐ต โ (0[,]+โ)
โง ๐ถ โ
(0[,]+โ)) โง ๐ถ =
+โ) โง 0 < ๐ด)
โ (๐ด
ยทe ๐ถ) =
(๐ด ยทe
+โ)) |
34 | | xmulpnf1 13253 |
. . . . . . 7
โข ((๐ด โ โ*
โง 0 < ๐ด) โ
(๐ด ยทe
+โ) = +โ) |
35 | 12, 16, 34 | syl2anc 585 |
. . . . . 6
โข ((((๐ด โ (0[,]+โ) โง
๐ต โ (0[,]+โ)
โง ๐ถ โ
(0[,]+โ)) โง ๐ถ =
+โ) โง 0 < ๐ด)
โ (๐ด
ยทe +โ) = +โ) |
36 | 33, 35 | eqtrd 2773 |
. . . . 5
โข ((((๐ด โ (0[,]+โ) โง
๐ต โ (0[,]+โ)
โง ๐ถ โ
(0[,]+โ)) โง ๐ถ =
+โ) โง 0 < ๐ด)
โ (๐ด
ยทe ๐ถ) =
+โ) |
37 | 36 | oveq1d 7424 |
. . . 4
โข ((((๐ด โ (0[,]+โ) โง
๐ต โ (0[,]+โ)
โง ๐ถ โ
(0[,]+โ)) โง ๐ถ =
+โ) โง 0 < ๐ด)
โ ((๐ด
ยทe ๐ถ)
+๐ (๐ต
ยทe ๐ถ)) =
(+โ +๐ (๐ต ยทe ๐ถ))) |
38 | 31, 37 | eqtr4d 2776 |
. . 3
โข ((((๐ด โ (0[,]+โ) โง
๐ต โ (0[,]+โ)
โง ๐ถ โ
(0[,]+โ)) โง ๐ถ =
+โ) โง 0 < ๐ด)
โ ((๐ด
+๐ ๐ต)
ยทe ๐ถ) =
((๐ด ยทe
๐ถ) +๐
(๐ต ยทe
๐ถ))) |
39 | | simpll3 1215 |
. . . . . . . 8
โข ((((๐ด โ (0[,]+โ) โง
๐ต โ (0[,]+โ)
โง ๐ถ โ
(0[,]+โ)) โง ๐ถ =
+โ) โง 0 = ๐ด)
โ ๐ถ โ
(0[,]+โ)) |
40 | 1, 39 | sselid 3981 |
. . . . . . 7
โข ((((๐ด โ (0[,]+โ) โง
๐ต โ (0[,]+โ)
โง ๐ถ โ
(0[,]+โ)) โง ๐ถ =
+โ) โง 0 = ๐ด)
โ ๐ถ โ
โ*) |
41 | | xmul02 13247 |
. . . . . . 7
โข (๐ถ โ โ*
โ (0 ยทe ๐ถ) = 0) |
42 | 40, 41 | syl 17 |
. . . . . 6
โข ((((๐ด โ (0[,]+โ) โง
๐ต โ (0[,]+โ)
โง ๐ถ โ
(0[,]+โ)) โง ๐ถ =
+โ) โง 0 = ๐ด)
โ (0 ยทe ๐ถ) = 0) |
43 | 42 | oveq1d 7424 |
. . . . 5
โข ((((๐ด โ (0[,]+โ) โง
๐ต โ (0[,]+โ)
โง ๐ถ โ
(0[,]+โ)) โง ๐ถ =
+โ) โง 0 = ๐ด)
โ ((0 ยทe ๐ถ) +๐ (๐ต ยทe ๐ถ)) = (0 +๐ (๐ต ยทe ๐ถ))) |
44 | | oveq1 7416 |
. . . . . . 7
โข (0 =
๐ด โ (0
ยทe ๐ถ) =
(๐ด ยทe
๐ถ)) |
45 | 44 | adantl 483 |
. . . . . 6
โข ((((๐ด โ (0[,]+โ) โง
๐ต โ (0[,]+โ)
โง ๐ถ โ
(0[,]+โ)) โง ๐ถ =
+โ) โง 0 = ๐ด)
โ (0 ยทe ๐ถ) = (๐ด ยทe ๐ถ)) |
46 | 45 | oveq1d 7424 |
. . . . 5
โข ((((๐ด โ (0[,]+โ) โง
๐ต โ (0[,]+โ)
โง ๐ถ โ
(0[,]+โ)) โง ๐ถ =
+โ) โง 0 = ๐ด)
โ ((0 ยทe ๐ถ) +๐ (๐ต ยทe ๐ถ)) = ((๐ด ยทe ๐ถ) +๐ (๐ต ยทe ๐ถ))) |
47 | | simpll2 1214 |
. . . . . . . 8
โข ((((๐ด โ (0[,]+โ) โง
๐ต โ (0[,]+โ)
โง ๐ถ โ
(0[,]+โ)) โง ๐ถ =
+โ) โง 0 = ๐ด)
โ ๐ต โ
(0[,]+โ)) |
48 | 1, 47 | sselid 3981 |
. . . . . . 7
โข ((((๐ด โ (0[,]+โ) โง
๐ต โ (0[,]+โ)
โง ๐ถ โ
(0[,]+โ)) โง ๐ถ =
+โ) โง 0 = ๐ด)
โ ๐ต โ
โ*) |
49 | 48, 40 | xmulcld 13281 |
. . . . . 6
โข ((((๐ด โ (0[,]+โ) โง
๐ต โ (0[,]+โ)
โง ๐ถ โ
(0[,]+โ)) โง ๐ถ =
+โ) โง 0 = ๐ด)
โ (๐ต
ยทe ๐ถ)
โ โ*) |
50 | | xaddlid 13221 |
. . . . . 6
โข ((๐ต ยทe ๐ถ) โ โ*
โ (0 +๐ (๐ต ยทe ๐ถ)) = (๐ต ยทe ๐ถ)) |
51 | 49, 50 | syl 17 |
. . . . 5
โข ((((๐ด โ (0[,]+โ) โง
๐ต โ (0[,]+โ)
โง ๐ถ โ
(0[,]+โ)) โง ๐ถ =
+โ) โง 0 = ๐ด)
โ (0 +๐ (๐ต ยทe ๐ถ)) = (๐ต ยทe ๐ถ)) |
52 | 43, 46, 51 | 3eqtr3d 2781 |
. . . 4
โข ((((๐ด โ (0[,]+โ) โง
๐ต โ (0[,]+โ)
โง ๐ถ โ
(0[,]+โ)) โง ๐ถ =
+โ) โง 0 = ๐ด)
โ ((๐ด
ยทe ๐ถ)
+๐ (๐ต
ยทe ๐ถ)) =
(๐ต ยทe
๐ถ)) |
53 | | xaddlid 13221 |
. . . . . 6
โข (๐ต โ โ*
โ (0 +๐ ๐ต) = ๐ต) |
54 | 48, 53 | syl 17 |
. . . . 5
โข ((((๐ด โ (0[,]+โ) โง
๐ต โ (0[,]+โ)
โง ๐ถ โ
(0[,]+โ)) โง ๐ถ =
+โ) โง 0 = ๐ด)
โ (0 +๐ ๐ต) = ๐ต) |
55 | 54 | oveq1d 7424 |
. . . 4
โข ((((๐ด โ (0[,]+โ) โง
๐ต โ (0[,]+โ)
โง ๐ถ โ
(0[,]+โ)) โง ๐ถ =
+โ) โง 0 = ๐ด)
โ ((0 +๐ ๐ต) ยทe ๐ถ) = (๐ต ยทe ๐ถ)) |
56 | | oveq1 7416 |
. . . . . 6
โข (0 =
๐ด โ (0
+๐ ๐ต) =
(๐ด +๐
๐ต)) |
57 | 56 | oveq1d 7424 |
. . . . 5
โข (0 =
๐ด โ ((0
+๐ ๐ต)
ยทe ๐ถ) =
((๐ด +๐
๐ต) ยทe
๐ถ)) |
58 | 57 | adantl 483 |
. . . 4
โข ((((๐ด โ (0[,]+โ) โง
๐ต โ (0[,]+โ)
โง ๐ถ โ
(0[,]+โ)) โง ๐ถ =
+โ) โง 0 = ๐ด)
โ ((0 +๐ ๐ต) ยทe ๐ถ) = ((๐ด +๐ ๐ต) ยทe ๐ถ)) |
59 | 52, 55, 58 | 3eqtr2rd 2780 |
. . 3
โข ((((๐ด โ (0[,]+โ) โง
๐ต โ (0[,]+โ)
โง ๐ถ โ
(0[,]+โ)) โง ๐ถ =
+โ) โง 0 = ๐ด)
โ ((๐ด
+๐ ๐ต)
ยทe ๐ถ) =
((๐ด ยทe
๐ถ) +๐
(๐ต ยทe
๐ถ))) |
60 | | 0xr 11261 |
. . . . 5
โข 0 โ
โ* |
61 | 60 | a1i 11 |
. . . 4
โข (((๐ด โ (0[,]+โ) โง
๐ต โ (0[,]+โ)
โง ๐ถ โ
(0[,]+โ)) โง ๐ถ =
+โ) โ 0 โ โ*) |
62 | | simpl1 1192 |
. . . . 5
โข (((๐ด โ (0[,]+โ) โง
๐ต โ (0[,]+โ)
โง ๐ถ โ
(0[,]+โ)) โง ๐ถ =
+โ) โ ๐ด โ
(0[,]+โ)) |
63 | 1, 62 | sselid 3981 |
. . . 4
โข (((๐ด โ (0[,]+โ) โง
๐ต โ (0[,]+โ)
โง ๐ถ โ
(0[,]+โ)) โง ๐ถ =
+โ) โ ๐ด โ
โ*) |
64 | | pnfxr 11268 |
. . . . . 6
โข +โ
โ โ* |
65 | 64 | a1i 11 |
. . . . 5
โข (((๐ด โ (0[,]+โ) โง
๐ต โ (0[,]+โ)
โง ๐ถ โ
(0[,]+โ)) โง ๐ถ =
+โ) โ +โ โ โ*) |
66 | | iccgelb 13380 |
. . . . 5
โข ((0
โ โ* โง +โ โ โ* โง
๐ด โ (0[,]+โ))
โ 0 โค ๐ด) |
67 | 61, 65, 62, 66 | syl3anc 1372 |
. . . 4
โข (((๐ด โ (0[,]+โ) โง
๐ต โ (0[,]+โ)
โง ๐ถ โ
(0[,]+โ)) โง ๐ถ =
+โ) โ 0 โค ๐ด) |
68 | | xrleloe 13123 |
. . . . 5
โข ((0
โ โ* โง ๐ด โ โ*) โ (0 โค
๐ด โ (0 < ๐ด โจ 0 = ๐ด))) |
69 | 68 | biimpa 478 |
. . . 4
โข (((0
โ โ* โง ๐ด โ โ*) โง 0 โค
๐ด) โ (0 < ๐ด โจ 0 = ๐ด)) |
70 | 61, 63, 67, 69 | syl21anc 837 |
. . 3
โข (((๐ด โ (0[,]+โ) โง
๐ต โ (0[,]+โ)
โง ๐ถ โ
(0[,]+โ)) โง ๐ถ =
+โ) โ (0 < ๐ด
โจ 0 = ๐ด)) |
71 | 38, 59, 70 | mpjaodan 958 |
. 2
โข (((๐ด โ (0[,]+โ) โง
๐ต โ (0[,]+โ)
โง ๐ถ โ
(0[,]+โ)) โง ๐ถ =
+โ) โ ((๐ด
+๐ ๐ต)
ยทe ๐ถ) =
((๐ด ยทe
๐ถ) +๐
(๐ต ยทe
๐ถ))) |
72 | | 0lepnf 13112 |
. . . . 5
โข 0 โค
+โ |
73 | | eliccelico 31988 |
. . . . 5
โข ((0
โ โ* โง +โ โ โ* โง 0
โค +โ) โ (๐ถ
โ (0[,]+โ) โ (๐ถ โ (0[,)+โ) โจ ๐ถ = +โ))) |
74 | 60, 64, 72, 73 | mp3an 1462 |
. . . 4
โข (๐ถ โ (0[,]+โ) โ
(๐ถ โ (0[,)+โ)
โจ ๐ถ =
+โ)) |
75 | 74 | 3anbi3i 1160 |
. . 3
โข ((๐ด โ (0[,]+โ) โง
๐ต โ (0[,]+โ)
โง ๐ถ โ
(0[,]+โ)) โ (๐ด
โ (0[,]+โ) โง ๐ต โ (0[,]+โ) โง (๐ถ โ (0[,)+โ) โจ
๐ถ =
+โ))) |
76 | 75 | simp3bi 1148 |
. 2
โข ((๐ด โ (0[,]+โ) โง
๐ต โ (0[,]+โ)
โง ๐ถ โ
(0[,]+โ)) โ (๐ถ
โ (0[,)+โ) โจ ๐ถ = +โ)) |
77 | 10, 71, 76 | mpjaodan 958 |
1
โข ((๐ด โ (0[,]+โ) โง
๐ต โ (0[,]+โ)
โง ๐ถ โ
(0[,]+โ)) โ ((๐ด
+๐ ๐ต)
ยทe ๐ถ) =
((๐ด ยทe
๐ถ) +๐
(๐ต ยทe
๐ถ))) |