Step | Hyp | Ref
| Expression |
1 | | cxpaddlelem.1 |
. . . . . 6
โข (๐ โ ๐ด โ โ) |
2 | | cxpaddlelem.2 |
. . . . . 6
โข (๐ โ 0 โค ๐ด) |
3 | | 1re 11219 |
. . . . . . 7
โข 1 โ
โ |
4 | | cxpaddlelem.4 |
. . . . . . . 8
โข (๐ โ ๐ต โ
โ+) |
5 | 4 | rpred 13021 |
. . . . . . 7
โข (๐ โ ๐ต โ โ) |
6 | | resubcl 11529 |
. . . . . . 7
โข ((1
โ โ โง ๐ต
โ โ) โ (1 โ ๐ต) โ โ) |
7 | 3, 5, 6 | sylancr 586 |
. . . . . 6
โข (๐ โ (1 โ ๐ต) โ
โ) |
8 | 1, 2, 7 | recxpcld 26468 |
. . . . 5
โข (๐ โ (๐ดโ๐(1 โ ๐ต)) โ
โ) |
9 | 8 | adantr 480 |
. . . 4
โข ((๐ โง 0 < ๐ด) โ (๐ดโ๐(1 โ ๐ต)) โ
โ) |
10 | | 1red 11220 |
. . . 4
โข ((๐ โง 0 < ๐ด) โ 1 โ โ) |
11 | | recxpcl 26420 |
. . . . . . 7
โข ((๐ด โ โ โง 0 โค
๐ด โง ๐ต โ โ) โ (๐ดโ๐๐ต) โ โ) |
12 | | cxpge0 26428 |
. . . . . . 7
โข ((๐ด โ โ โง 0 โค
๐ด โง ๐ต โ โ) โ 0 โค (๐ดโ๐๐ต)) |
13 | 11, 12 | jca 511 |
. . . . . 6
โข ((๐ด โ โ โง 0 โค
๐ด โง ๐ต โ โ) โ ((๐ดโ๐๐ต) โ โ โง 0 โค (๐ดโ๐๐ต))) |
14 | 1, 2, 5, 13 | syl3anc 1370 |
. . . . 5
โข (๐ โ ((๐ดโ๐๐ต) โ โ โง 0 โค (๐ดโ๐๐ต))) |
15 | 14 | adantr 480 |
. . . 4
โข ((๐ โง 0 < ๐ด) โ ((๐ดโ๐๐ต) โ โ โง 0 โค (๐ดโ๐๐ต))) |
16 | | cxpaddlelem.3 |
. . . . . . . 8
โข (๐ โ ๐ด โค 1) |
17 | 16 | ad2antrr 723 |
. . . . . . 7
โข (((๐ โง 0 < ๐ด) โง ๐ต < 1) โ ๐ด โค 1) |
18 | 1 | ad2antrr 723 |
. . . . . . . 8
โข (((๐ โง 0 < ๐ด) โง ๐ต < 1) โ ๐ด โ โ) |
19 | 2 | ad2antrr 723 |
. . . . . . . 8
โข (((๐ โง 0 < ๐ด) โง ๐ต < 1) โ 0 โค ๐ด) |
20 | | 1red 11220 |
. . . . . . . 8
โข (((๐ โง 0 < ๐ด) โง ๐ต < 1) โ 1 โ
โ) |
21 | | 0le1 11742 |
. . . . . . . . 9
โข 0 โค
1 |
22 | 21 | a1i 11 |
. . . . . . . 8
โข (((๐ โง 0 < ๐ด) โง ๐ต < 1) โ 0 โค 1) |
23 | | difrp 13017 |
. . . . . . . . . . 11
โข ((๐ต โ โ โง 1 โ
โ) โ (๐ต < 1
โ (1 โ ๐ต) โ
โ+)) |
24 | 5, 3, 23 | sylancl 585 |
. . . . . . . . . 10
โข (๐ โ (๐ต < 1 โ (1 โ ๐ต) โ
โ+)) |
25 | 24 | adantr 480 |
. . . . . . . . 9
โข ((๐ โง 0 < ๐ด) โ (๐ต < 1 โ (1 โ ๐ต) โ
โ+)) |
26 | 25 | biimpa 476 |
. . . . . . . 8
โข (((๐ โง 0 < ๐ด) โง ๐ต < 1) โ (1 โ ๐ต) โ
โ+) |
27 | 18, 19, 20, 22, 26 | cxple2d 26472 |
. . . . . . 7
โข (((๐ โง 0 < ๐ด) โง ๐ต < 1) โ (๐ด โค 1 โ (๐ดโ๐(1 โ ๐ต)) โค
(1โ๐(1 โ ๐ต)))) |
28 | 17, 27 | mpbid 231 |
. . . . . 6
โข (((๐ โง 0 < ๐ด) โง ๐ต < 1) โ (๐ดโ๐(1 โ ๐ต)) โค
(1โ๐(1 โ ๐ต))) |
29 | 7 | recnd 11247 |
. . . . . . . 8
โข (๐ โ (1 โ ๐ต) โ
โ) |
30 | 29 | 1cxpd 26452 |
. . . . . . 7
โข (๐ โ
(1โ๐(1 โ ๐ต)) = 1) |
31 | 30 | ad2antrr 723 |
. . . . . 6
โข (((๐ โง 0 < ๐ด) โง ๐ต < 1) โ
(1โ๐(1 โ ๐ต)) = 1) |
32 | 28, 31 | breqtrd 5174 |
. . . . 5
โข (((๐ โง 0 < ๐ด) โง ๐ต < 1) โ (๐ดโ๐(1 โ ๐ต)) โค 1) |
33 | | simpr 484 |
. . . . . . . . . 10
โข (((๐ โง 0 < ๐ด) โง ๐ต = 1) โ ๐ต = 1) |
34 | 33 | oveq2d 7428 |
. . . . . . . . 9
โข (((๐ โง 0 < ๐ด) โง ๐ต = 1) โ (1 โ ๐ต) = (1 โ 1)) |
35 | | 1m1e0 12289 |
. . . . . . . . 9
โข (1
โ 1) = 0 |
36 | 34, 35 | eqtrdi 2787 |
. . . . . . . 8
โข (((๐ โง 0 < ๐ด) โง ๐ต = 1) โ (1 โ ๐ต) = 0) |
37 | 36 | oveq2d 7428 |
. . . . . . 7
โข (((๐ โง 0 < ๐ด) โง ๐ต = 1) โ (๐ดโ๐(1 โ ๐ต)) = (๐ดโ๐0)) |
38 | 1 | recnd 11247 |
. . . . . . . . 9
โข (๐ โ ๐ด โ โ) |
39 | 38 | ad2antrr 723 |
. . . . . . . 8
โข (((๐ โง 0 < ๐ด) โง ๐ต = 1) โ ๐ด โ โ) |
40 | 39 | cxp0d 26450 |
. . . . . . 7
โข (((๐ โง 0 < ๐ด) โง ๐ต = 1) โ (๐ดโ๐0) =
1) |
41 | 37, 40 | eqtrd 2771 |
. . . . . 6
โข (((๐ โง 0 < ๐ด) โง ๐ต = 1) โ (๐ดโ๐(1 โ ๐ต)) = 1) |
42 | | 1le1 11847 |
. . . . . 6
โข 1 โค
1 |
43 | 41, 42 | eqbrtrdi 5187 |
. . . . 5
โข (((๐ โง 0 < ๐ด) โง ๐ต = 1) โ (๐ดโ๐(1 โ ๐ต)) โค 1) |
44 | | cxpaddlelem.5 |
. . . . . . 7
โข (๐ โ ๐ต โค 1) |
45 | | leloe 11305 |
. . . . . . . 8
โข ((๐ต โ โ โง 1 โ
โ) โ (๐ต โค 1
โ (๐ต < 1 โจ ๐ต = 1))) |
46 | 5, 3, 45 | sylancl 585 |
. . . . . . 7
โข (๐ โ (๐ต โค 1 โ (๐ต < 1 โจ ๐ต = 1))) |
47 | 44, 46 | mpbid 231 |
. . . . . 6
โข (๐ โ (๐ต < 1 โจ ๐ต = 1)) |
48 | 47 | adantr 480 |
. . . . 5
โข ((๐ โง 0 < ๐ด) โ (๐ต < 1 โจ ๐ต = 1)) |
49 | 32, 43, 48 | mpjaodan 956 |
. . . 4
โข ((๐ โง 0 < ๐ด) โ (๐ดโ๐(1 โ ๐ต)) โค 1) |
50 | | lemul1a 12073 |
. . . 4
โข ((((๐ดโ๐(1
โ ๐ต)) โ โ
โง 1 โ โ โง ((๐ดโ๐๐ต) โ โ โง 0 โค (๐ดโ๐๐ต))) โง (๐ดโ๐(1 โ ๐ต)) โค 1) โ ((๐ดโ๐(1
โ ๐ต)) ยท (๐ดโ๐๐ต)) โค (1 ยท (๐ดโ๐๐ต))) |
51 | 9, 10, 15, 49, 50 | syl31anc 1372 |
. . 3
โข ((๐ โง 0 < ๐ด) โ ((๐ดโ๐(1 โ ๐ต)) ยท (๐ดโ๐๐ต)) โค (1 ยท (๐ดโ๐๐ต))) |
52 | | ax-1cn 11172 |
. . . . . . 7
โข 1 โ
โ |
53 | 5 | recnd 11247 |
. . . . . . 7
โข (๐ โ ๐ต โ โ) |
54 | | npcan 11474 |
. . . . . . 7
โข ((1
โ โ โง ๐ต
โ โ) โ ((1 โ ๐ต) + ๐ต) = 1) |
55 | 52, 53, 54 | sylancr 586 |
. . . . . 6
โข (๐ โ ((1 โ ๐ต) + ๐ต) = 1) |
56 | 55 | adantr 480 |
. . . . 5
โข ((๐ โง 0 < ๐ด) โ ((1 โ ๐ต) + ๐ต) = 1) |
57 | 56 | oveq2d 7428 |
. . . 4
โข ((๐ โง 0 < ๐ด) โ (๐ดโ๐((1 โ ๐ต) + ๐ต)) = (๐ดโ๐1)) |
58 | 38 | adantr 480 |
. . . . 5
โข ((๐ โง 0 < ๐ด) โ ๐ด โ โ) |
59 | 1 | anim1i 614 |
. . . . . . 7
โข ((๐ โง 0 < ๐ด) โ (๐ด โ โ โง 0 < ๐ด)) |
60 | | elrp 12981 |
. . . . . . 7
โข (๐ด โ โ+
โ (๐ด โ โ
โง 0 < ๐ด)) |
61 | 59, 60 | sylibr 233 |
. . . . . 6
โข ((๐ โง 0 < ๐ด) โ ๐ด โ
โ+) |
62 | 61 | rpne0d 13026 |
. . . . 5
โข ((๐ โง 0 < ๐ด) โ ๐ด โ 0) |
63 | 29 | adantr 480 |
. . . . 5
โข ((๐ โง 0 < ๐ด) โ (1 โ ๐ต) โ โ) |
64 | 53 | adantr 480 |
. . . . 5
โข ((๐ โง 0 < ๐ด) โ ๐ต โ โ) |
65 | 58, 62, 63, 64 | cxpaddd 26462 |
. . . 4
โข ((๐ โง 0 < ๐ด) โ (๐ดโ๐((1 โ ๐ต) + ๐ต)) = ((๐ดโ๐(1 โ ๐ต)) ยท (๐ดโ๐๐ต))) |
66 | 38 | cxp1d 26451 |
. . . . 5
โข (๐ โ (๐ดโ๐1) = ๐ด) |
67 | 66 | adantr 480 |
. . . 4
โข ((๐ โง 0 < ๐ด) โ (๐ดโ๐1) = ๐ด) |
68 | 57, 65, 67 | 3eqtr3d 2779 |
. . 3
โข ((๐ โง 0 < ๐ด) โ ((๐ดโ๐(1 โ ๐ต)) ยท (๐ดโ๐๐ต)) = ๐ด) |
69 | 38, 53 | cxpcld 26453 |
. . . . 5
โข (๐ โ (๐ดโ๐๐ต) โ โ) |
70 | 69 | mullidd 11237 |
. . . 4
โข (๐ โ (1 ยท (๐ดโ๐๐ต)) = (๐ดโ๐๐ต)) |
71 | 70 | adantr 480 |
. . 3
โข ((๐ โง 0 < ๐ด) โ (1 ยท (๐ดโ๐๐ต)) = (๐ดโ๐๐ต)) |
72 | 51, 68, 71 | 3brtr3d 5179 |
. 2
โข ((๐ โง 0 < ๐ด) โ ๐ด โค (๐ดโ๐๐ต)) |
73 | 1, 2, 5 | cxpge0d 26469 |
. . . 4
โข (๐ โ 0 โค (๐ดโ๐๐ต)) |
74 | | breq1 5151 |
. . . 4
โข (0 =
๐ด โ (0 โค (๐ดโ๐๐ต) โ ๐ด โค (๐ดโ๐๐ต))) |
75 | 73, 74 | syl5ibcom 244 |
. . 3
โข (๐ โ (0 = ๐ด โ ๐ด โค (๐ดโ๐๐ต))) |
76 | 75 | imp 406 |
. 2
โข ((๐ โง 0 = ๐ด) โ ๐ด โค (๐ดโ๐๐ต)) |
77 | | 0re 11221 |
. . . 4
โข 0 โ
โ |
78 | | leloe 11305 |
. . . 4
โข ((0
โ โ โง ๐ด
โ โ) โ (0 โค ๐ด โ (0 < ๐ด โจ 0 = ๐ด))) |
79 | 77, 1, 78 | sylancr 586 |
. . 3
โข (๐ โ (0 โค ๐ด โ (0 < ๐ด โจ 0 = ๐ด))) |
80 | 2, 79 | mpbid 231 |
. 2
โข (๐ โ (0 < ๐ด โจ 0 = ๐ด)) |
81 | 72, 76, 80 | mpjaodan 956 |
1
โข (๐ โ ๐ด โค (๐ดโ๐๐ต)) |