Step | Hyp | Ref
| Expression |
1 | | rpxr 12932 |
. . . 4
โข (๐ถ โ โ+
โ ๐ถ โ
โ*) |
2 | | rpge0 12936 |
. . . 4
โข (๐ถ โ โ+
โ 0 โค ๐ถ) |
3 | 1, 2 | jca 513 |
. . 3
โข (๐ถ โ โ+
โ (๐ถ โ
โ* โง 0 โค ๐ถ)) |
4 | | xlemul1a 13216 |
. . . 4
โข (((๐ด โ โ*
โง ๐ต โ
โ* โง (๐ถ โ โ* โง 0 โค
๐ถ)) โง ๐ด โค ๐ต) โ (๐ด ยทe ๐ถ) โค (๐ต ยทe ๐ถ)) |
5 | 4 | ex 414 |
. . 3
โข ((๐ด โ โ*
โง ๐ต โ
โ* โง (๐ถ โ โ* โง 0 โค
๐ถ)) โ (๐ด โค ๐ต โ (๐ด ยทe ๐ถ) โค (๐ต ยทe ๐ถ))) |
6 | 3, 5 | syl3an3 1166 |
. 2
โข ((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ+) โ (๐ด โค ๐ต โ (๐ด ยทe ๐ถ) โค (๐ต ยทe ๐ถ))) |
7 | | simp1 1137 |
. . . . 5
โข ((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ+) โ ๐ด โ
โ*) |
8 | 1 | 3ad2ant3 1136 |
. . . . 5
โข ((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ+) โ ๐ถ โ
โ*) |
9 | | xmulcl 13201 |
. . . . 5
โข ((๐ด โ โ*
โง ๐ถ โ
โ*) โ (๐ด ยทe ๐ถ) โ
โ*) |
10 | 7, 8, 9 | syl2anc 585 |
. . . 4
โข ((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ+) โ (๐ด ยทe ๐ถ) โ
โ*) |
11 | | simp2 1138 |
. . . . 5
โข ((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ+) โ ๐ต โ
โ*) |
12 | | xmulcl 13201 |
. . . . 5
โข ((๐ต โ โ*
โง ๐ถ โ
โ*) โ (๐ต ยทe ๐ถ) โ
โ*) |
13 | 11, 8, 12 | syl2anc 585 |
. . . 4
โข ((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ+) โ (๐ต ยทe ๐ถ) โ
โ*) |
14 | | rpreccl 12949 |
. . . . . 6
โข (๐ถ โ โ+
โ (1 / ๐ถ) โ
โ+) |
15 | 14 | 3ad2ant3 1136 |
. . . . 5
โข ((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ+) โ (1 / ๐ถ) โ
โ+) |
16 | | rpxr 12932 |
. . . . 5
โข ((1 /
๐ถ) โ
โ+ โ (1 / ๐ถ) โ
โ*) |
17 | 15, 16 | syl 17 |
. . . 4
โข ((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ+) โ (1 / ๐ถ) โ
โ*) |
18 | | rpge0 12936 |
. . . . 5
โข ((1 /
๐ถ) โ
โ+ โ 0 โค (1 / ๐ถ)) |
19 | 15, 18 | syl 17 |
. . . 4
โข ((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ+) โ 0 โค (1 / ๐ถ)) |
20 | | xlemul1a 13216 |
. . . . 5
โข ((((๐ด ยทe ๐ถ) โ โ*
โง (๐ต
ยทe ๐ถ)
โ โ* โง ((1 / ๐ถ) โ โ* โง 0 โค (1
/ ๐ถ))) โง (๐ด ยทe ๐ถ) โค (๐ต ยทe ๐ถ)) โ ((๐ด ยทe ๐ถ) ยทe (1 / ๐ถ)) โค ((๐ต ยทe ๐ถ) ยทe (1 / ๐ถ))) |
21 | 20 | ex 414 |
. . . 4
โข (((๐ด ยทe ๐ถ) โ โ*
โง (๐ต
ยทe ๐ถ)
โ โ* โง ((1 / ๐ถ) โ โ* โง 0 โค (1
/ ๐ถ))) โ ((๐ด ยทe ๐ถ) โค (๐ต ยทe ๐ถ) โ ((๐ด ยทe ๐ถ) ยทe (1 / ๐ถ)) โค ((๐ต ยทe ๐ถ) ยทe (1 / ๐ถ)))) |
22 | 10, 13, 17, 19, 21 | syl112anc 1375 |
. . 3
โข ((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ+) โ ((๐ด ยทe ๐ถ) โค (๐ต ยทe ๐ถ) โ ((๐ด ยทe ๐ถ) ยทe (1 / ๐ถ)) โค ((๐ต ยทe ๐ถ) ยทe (1 / ๐ถ)))) |
23 | | xmulass 13215 |
. . . . . 6
โข ((๐ด โ โ*
โง ๐ถ โ
โ* โง (1 / ๐ถ) โ โ*) โ ((๐ด ยทe ๐ถ) ยทe (1 /
๐ถ)) = (๐ด ยทe (๐ถ ยทe (1 / ๐ถ)))) |
24 | 7, 8, 17, 23 | syl3anc 1372 |
. . . . 5
โข ((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ+) โ ((๐ด ยทe ๐ถ) ยทe (1 / ๐ถ)) = (๐ด ยทe (๐ถ ยทe (1 / ๐ถ)))) |
25 | | rpre 12931 |
. . . . . . . . 9
โข (๐ถ โ โ+
โ ๐ถ โ
โ) |
26 | 25 | 3ad2ant3 1136 |
. . . . . . . 8
โข ((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ+) โ ๐ถ โ โ) |
27 | 15 | rpred 12965 |
. . . . . . . 8
โข ((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ+) โ (1 / ๐ถ) โ โ) |
28 | | rexmul 13199 |
. . . . . . . 8
โข ((๐ถ โ โ โง (1 / ๐ถ) โ โ) โ (๐ถ ยทe (1 / ๐ถ)) = (๐ถ ยท (1 / ๐ถ))) |
29 | 26, 27, 28 | syl2anc 585 |
. . . . . . 7
โข ((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ+) โ (๐ถ ยทe (1 / ๐ถ)) = (๐ถ ยท (1 / ๐ถ))) |
30 | 26 | recnd 11191 |
. . . . . . . 8
โข ((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ+) โ ๐ถ โ โ) |
31 | | rpne0 12939 |
. . . . . . . . 9
โข (๐ถ โ โ+
โ ๐ถ โ
0) |
32 | 31 | 3ad2ant3 1136 |
. . . . . . . 8
โข ((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ+) โ ๐ถ โ 0) |
33 | 30, 32 | recidd 11934 |
. . . . . . 7
โข ((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ+) โ (๐ถ ยท (1 / ๐ถ)) = 1) |
34 | 29, 33 | eqtrd 2773 |
. . . . . 6
โข ((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ+) โ (๐ถ ยทe (1 / ๐ถ)) = 1) |
35 | 34 | oveq2d 7377 |
. . . . 5
โข ((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ+) โ (๐ด ยทe (๐ถ ยทe (1 / ๐ถ))) = (๐ด ยทe 1)) |
36 | | xmulid1 13207 |
. . . . . 6
โข (๐ด โ โ*
โ (๐ด
ยทe 1) = ๐ด) |
37 | 7, 36 | syl 17 |
. . . . 5
โข ((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ+) โ (๐ด ยทe 1) = ๐ด) |
38 | 24, 35, 37 | 3eqtrd 2777 |
. . . 4
โข ((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ+) โ ((๐ด ยทe ๐ถ) ยทe (1 / ๐ถ)) = ๐ด) |
39 | | xmulass 13215 |
. . . . . 6
โข ((๐ต โ โ*
โง ๐ถ โ
โ* โง (1 / ๐ถ) โ โ*) โ ((๐ต ยทe ๐ถ) ยทe (1 /
๐ถ)) = (๐ต ยทe (๐ถ ยทe (1 / ๐ถ)))) |
40 | 11, 8, 17, 39 | syl3anc 1372 |
. . . . 5
โข ((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ+) โ ((๐ต ยทe ๐ถ) ยทe (1 / ๐ถ)) = (๐ต ยทe (๐ถ ยทe (1 / ๐ถ)))) |
41 | 34 | oveq2d 7377 |
. . . . 5
โข ((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ+) โ (๐ต ยทe (๐ถ ยทe (1 / ๐ถ))) = (๐ต ยทe 1)) |
42 | | xmulid1 13207 |
. . . . . 6
โข (๐ต โ โ*
โ (๐ต
ยทe 1) = ๐ต) |
43 | 11, 42 | syl 17 |
. . . . 5
โข ((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ+) โ (๐ต ยทe 1) = ๐ต) |
44 | 40, 41, 43 | 3eqtrd 2777 |
. . . 4
โข ((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ+) โ ((๐ต ยทe ๐ถ) ยทe (1 / ๐ถ)) = ๐ต) |
45 | 38, 44 | breq12d 5122 |
. . 3
โข ((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ+) โ (((๐ด ยทe ๐ถ) ยทe (1 / ๐ถ)) โค ((๐ต ยทe ๐ถ) ยทe (1 / ๐ถ)) โ ๐ด โค ๐ต)) |
46 | 22, 45 | sylibd 238 |
. 2
โข ((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ+) โ ((๐ด ยทe ๐ถ) โค (๐ต ยทe ๐ถ) โ ๐ด โค ๐ต)) |
47 | 6, 46 | impbid 211 |
1
โข ((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ถ
โ โ+) โ (๐ด โค ๐ต โ (๐ด ยทe ๐ถ) โค (๐ต ยทe ๐ถ))) |