Step | Hyp | Ref
| Expression |
1 | | simpr 484 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง ๐ โ (0[,]1)) โ ๐ โ (0[,]1)) |
2 | | 0red 11233 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง ๐ โ (0[,]1)) โ 0 โ
โ) |
3 | | 1red 11231 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง ๐ โ (0[,]1)) โ 1 โ
โ) |
4 | | elicc01 13461 |
. . . . . . . 8
โข (๐ โ (0[,]1) โ (๐ โ โ โง 0 โค
๐ โง ๐ โค 1)) |
5 | 4 | simp1bi 1143 |
. . . . . . 7
โข (๐ โ (0[,]1) โ ๐ โ
โ) |
6 | 5 | adantl 481 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง ๐ โ (0[,]1)) โ ๐ โ โ) |
7 | | difrp 13030 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด < ๐ต โ (๐ต โ ๐ด) โ
โ+)) |
8 | 7 | biimp3a 1466 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โ (๐ต โ ๐ด) โ
โ+) |
9 | 8 | adantr 480 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง ๐ โ (0[,]1)) โ (๐ต โ ๐ด) โ
โ+) |
10 | | eqid 2727 |
. . . . . . 7
โข (0
ยท (๐ต โ ๐ด)) = (0 ยท (๐ต โ ๐ด)) |
11 | | eqid 2727 |
. . . . . . 7
โข (1
ยท (๐ต โ ๐ด)) = (1 ยท (๐ต โ ๐ด)) |
12 | 10, 11 | iccdil 13485 |
. . . . . 6
โข (((0
โ โ โง 1 โ โ) โง (๐ โ โ โง (๐ต โ ๐ด) โ โ+)) โ (๐ โ (0[,]1) โ (๐ ยท (๐ต โ ๐ด)) โ ((0 ยท (๐ต โ ๐ด))[,](1 ยท (๐ต โ ๐ด))))) |
13 | 2, 3, 6, 9, 12 | syl22anc 838 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง ๐ โ (0[,]1)) โ (๐ โ (0[,]1) โ (๐ ยท (๐ต โ ๐ด)) โ ((0 ยท (๐ต โ ๐ด))[,](1 ยท (๐ต โ ๐ด))))) |
14 | 1, 13 | mpbid 231 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง ๐ โ (0[,]1)) โ (๐ ยท (๐ต โ ๐ด)) โ ((0 ยท (๐ต โ ๐ด))[,](1 ยท (๐ต โ ๐ด)))) |
15 | | simpl2 1190 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง ๐ โ (0[,]1)) โ ๐ต โ โ) |
16 | | simpl1 1189 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง ๐ โ (0[,]1)) โ ๐ด โ โ) |
17 | 15, 16 | resubcld 11658 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง ๐ โ (0[,]1)) โ (๐ต โ ๐ด) โ โ) |
18 | 17 | recnd 11258 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง ๐ โ (0[,]1)) โ (๐ต โ ๐ด) โ โ) |
19 | 18 | mul02d 11428 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง ๐ โ (0[,]1)) โ (0 ยท (๐ต โ ๐ด)) = 0) |
20 | 18 | mullidd 11248 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง ๐ โ (0[,]1)) โ (1 ยท (๐ต โ ๐ด)) = (๐ต โ ๐ด)) |
21 | 19, 20 | oveq12d 7432 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง ๐ โ (0[,]1)) โ ((0 ยท (๐ต โ ๐ด))[,](1 ยท (๐ต โ ๐ด))) = (0[,](๐ต โ ๐ด))) |
22 | 14, 21 | eleqtrd 2830 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง ๐ โ (0[,]1)) โ (๐ ยท (๐ต โ ๐ด)) โ (0[,](๐ต โ ๐ด))) |
23 | 6, 17 | remulcld 11260 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง ๐ โ (0[,]1)) โ (๐ ยท (๐ต โ ๐ด)) โ โ) |
24 | | eqid 2727 |
. . . . 5
โข (0 +
๐ด) = (0 + ๐ด) |
25 | | eqid 2727 |
. . . . 5
โข ((๐ต โ ๐ด) + ๐ด) = ((๐ต โ ๐ด) + ๐ด) |
26 | 24, 25 | iccshftr 13481 |
. . . 4
โข (((0
โ โ โง (๐ต
โ ๐ด) โ โ)
โง ((๐ ยท (๐ต โ ๐ด)) โ โ โง ๐ด โ โ)) โ ((๐ ยท (๐ต โ ๐ด)) โ (0[,](๐ต โ ๐ด)) โ ((๐ ยท (๐ต โ ๐ด)) + ๐ด) โ ((0 + ๐ด)[,]((๐ต โ ๐ด) + ๐ด)))) |
27 | 2, 17, 23, 16, 26 | syl22anc 838 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง ๐ โ (0[,]1)) โ ((๐ ยท (๐ต โ ๐ด)) โ (0[,](๐ต โ ๐ด)) โ ((๐ ยท (๐ต โ ๐ด)) + ๐ด) โ ((0 + ๐ด)[,]((๐ต โ ๐ด) + ๐ด)))) |
28 | 22, 27 | mpbid 231 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง ๐ โ (0[,]1)) โ ((๐ ยท (๐ต โ ๐ด)) + ๐ด) โ ((0 + ๐ด)[,]((๐ต โ ๐ด) + ๐ด))) |
29 | 6 | recnd 11258 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง ๐ โ (0[,]1)) โ ๐ โ โ) |
30 | 15 | recnd 11258 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง ๐ โ (0[,]1)) โ ๐ต โ โ) |
31 | 29, 30 | mulcld 11250 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง ๐ โ (0[,]1)) โ (๐ ยท ๐ต) โ โ) |
32 | 16 | recnd 11258 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง ๐ โ (0[,]1)) โ ๐ด โ โ) |
33 | 29, 32 | mulcld 11250 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง ๐ โ (0[,]1)) โ (๐ ยท ๐ด) โ โ) |
34 | 31, 33, 32 | subadd23d 11609 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง ๐ โ (0[,]1)) โ (((๐ ยท ๐ต) โ (๐ ยท ๐ด)) + ๐ด) = ((๐ ยท ๐ต) + (๐ด โ (๐ ยท ๐ด)))) |
35 | 29, 30, 32 | subdid 11686 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง ๐ โ (0[,]1)) โ (๐ ยท (๐ต โ ๐ด)) = ((๐ ยท ๐ต) โ (๐ ยท ๐ด))) |
36 | 35 | oveq1d 7429 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง ๐ โ (0[,]1)) โ ((๐ ยท (๐ต โ ๐ด)) + ๐ด) = (((๐ ยท ๐ต) โ (๐ ยท ๐ด)) + ๐ด)) |
37 | | 1re 11230 |
. . . . . . . 8
โข 1 โ
โ |
38 | | resubcl 11540 |
. . . . . . . 8
โข ((1
โ โ โง ๐
โ โ) โ (1 โ ๐) โ โ) |
39 | 37, 6, 38 | sylancr 586 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง ๐ โ (0[,]1)) โ (1 โ ๐) โ
โ) |
40 | 39, 16 | remulcld 11260 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง ๐ โ (0[,]1)) โ ((1 โ ๐) ยท ๐ด) โ โ) |
41 | 40 | recnd 11258 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง ๐ โ (0[,]1)) โ ((1 โ ๐) ยท ๐ด) โ โ) |
42 | 41, 31 | addcomd 11432 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง ๐ โ (0[,]1)) โ (((1 โ ๐) ยท ๐ด) + (๐ ยท ๐ต)) = ((๐ ยท ๐ต) + ((1 โ ๐) ยท ๐ด))) |
43 | | 1cnd 11225 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง ๐ โ (0[,]1)) โ 1 โ
โ) |
44 | 43, 29, 32 | subdird 11687 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง ๐ โ (0[,]1)) โ ((1 โ ๐) ยท ๐ด) = ((1 ยท ๐ด) โ (๐ ยท ๐ด))) |
45 | 32 | mullidd 11248 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง ๐ โ (0[,]1)) โ (1 ยท ๐ด) = ๐ด) |
46 | 45 | oveq1d 7429 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง ๐ โ (0[,]1)) โ ((1 ยท ๐ด) โ (๐ ยท ๐ด)) = (๐ด โ (๐ ยท ๐ด))) |
47 | 44, 46 | eqtrd 2767 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง ๐ โ (0[,]1)) โ ((1 โ ๐) ยท ๐ด) = (๐ด โ (๐ ยท ๐ด))) |
48 | 47 | oveq2d 7430 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง ๐ โ (0[,]1)) โ ((๐ ยท ๐ต) + ((1 โ ๐) ยท ๐ด)) = ((๐ ยท ๐ต) + (๐ด โ (๐ ยท ๐ด)))) |
49 | 42, 48 | eqtrd 2767 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง ๐ โ (0[,]1)) โ (((1 โ ๐) ยท ๐ด) + (๐ ยท ๐ต)) = ((๐ ยท ๐ต) + (๐ด โ (๐ ยท ๐ด)))) |
50 | 34, 36, 49 | 3eqtr4d 2777 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง ๐ โ (0[,]1)) โ ((๐ ยท (๐ต โ ๐ด)) + ๐ด) = (((1 โ ๐) ยท ๐ด) + (๐ ยท ๐ต))) |
51 | 32 | addlidd 11431 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง ๐ โ (0[,]1)) โ (0 + ๐ด) = ๐ด) |
52 | 30, 32 | npcand 11591 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง ๐ โ (0[,]1)) โ ((๐ต โ ๐ด) + ๐ด) = ๐ต) |
53 | 51, 52 | oveq12d 7432 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง ๐ โ (0[,]1)) โ ((0 + ๐ด)[,]((๐ต โ ๐ด) + ๐ด)) = (๐ด[,]๐ต)) |
54 | 28, 50, 53 | 3eltr3d 2842 |
1
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง ๐ โ (0[,]1)) โ (((1 โ ๐) ยท ๐ด) + (๐ ยท ๐ต)) โ (๐ด[,]๐ต)) |