Step | Hyp | Ref
| Expression |
1 | | cxpaddle.1 |
. . . . . . . 8
โข (๐ โ ๐ด โ โ) |
2 | | cxpaddle.3 |
. . . . . . . 8
โข (๐ โ ๐ต โ โ) |
3 | 1, 2 | readdcld 11243 |
. . . . . . 7
โข (๐ โ (๐ด + ๐ต) โ โ) |
4 | | cxpaddle.2 |
. . . . . . . 8
โข (๐ โ 0 โค ๐ด) |
5 | | cxpaddle.4 |
. . . . . . . 8
โข (๐ โ 0 โค ๐ต) |
6 | 1, 2, 4, 5 | addge0d 11790 |
. . . . . . 7
โข (๐ โ 0 โค (๐ด + ๐ต)) |
7 | | cxpaddle.5 |
. . . . . . . 8
โข (๐ โ ๐ถ โ
โ+) |
8 | 7 | rpred 13016 |
. . . . . . 7
โข (๐ โ ๐ถ โ โ) |
9 | 3, 6, 8 | recxpcld 26231 |
. . . . . 6
โข (๐ โ ((๐ด + ๐ต)โ๐๐ถ) โ โ) |
10 | 9 | adantr 482 |
. . . . 5
โข ((๐ โง 0 < (๐ด + ๐ต)) โ ((๐ด + ๐ต)โ๐๐ถ) โ โ) |
11 | 10 | recnd 11242 |
. . . 4
โข ((๐ โง 0 < (๐ด + ๐ต)) โ ((๐ด + ๐ต)โ๐๐ถ) โ โ) |
12 | 11 | mullidd 11232 |
. . 3
โข ((๐ โง 0 < (๐ด + ๐ต)) โ (1 ยท ((๐ด + ๐ต)โ๐๐ถ)) = ((๐ด + ๐ต)โ๐๐ถ)) |
13 | 1 | adantr 482 |
. . . . . . 7
โข ((๐ โง 0 < (๐ด + ๐ต)) โ ๐ด โ โ) |
14 | 3 | anim1i 616 |
. . . . . . . 8
โข ((๐ โง 0 < (๐ด + ๐ต)) โ ((๐ด + ๐ต) โ โ โง 0 < (๐ด + ๐ต))) |
15 | | elrp 12976 |
. . . . . . . 8
โข ((๐ด + ๐ต) โ โ+ โ ((๐ด + ๐ต) โ โ โง 0 < (๐ด + ๐ต))) |
16 | 14, 15 | sylibr 233 |
. . . . . . 7
โข ((๐ โง 0 < (๐ด + ๐ต)) โ (๐ด + ๐ต) โ
โ+) |
17 | 13, 16 | rerpdivcld 13047 |
. . . . . 6
โข ((๐ โง 0 < (๐ด + ๐ต)) โ (๐ด / (๐ด + ๐ต)) โ โ) |
18 | 2 | adantr 482 |
. . . . . . 7
โข ((๐ โง 0 < (๐ด + ๐ต)) โ ๐ต โ โ) |
19 | 18, 16 | rerpdivcld 13047 |
. . . . . 6
โข ((๐ โง 0 < (๐ด + ๐ต)) โ (๐ต / (๐ด + ๐ต)) โ โ) |
20 | 4 | adantr 482 |
. . . . . . . 8
โข ((๐ โง 0 < (๐ด + ๐ต)) โ 0 โค ๐ด) |
21 | 3 | adantr 482 |
. . . . . . . 8
โข ((๐ โง 0 < (๐ด + ๐ต)) โ (๐ด + ๐ต) โ โ) |
22 | | simpr 486 |
. . . . . . . 8
โข ((๐ โง 0 < (๐ด + ๐ต)) โ 0 < (๐ด + ๐ต)) |
23 | | divge0 12083 |
. . . . . . . 8
โข (((๐ด โ โ โง 0 โค
๐ด) โง ((๐ด + ๐ต) โ โ โง 0 < (๐ด + ๐ต))) โ 0 โค (๐ด / (๐ด + ๐ต))) |
24 | 13, 20, 21, 22, 23 | syl22anc 838 |
. . . . . . 7
โข ((๐ โง 0 < (๐ด + ๐ต)) โ 0 โค (๐ด / (๐ด + ๐ต))) |
25 | 8 | adantr 482 |
. . . . . . 7
โข ((๐ โง 0 < (๐ด + ๐ต)) โ ๐ถ โ โ) |
26 | 17, 24, 25 | recxpcld 26231 |
. . . . . 6
โข ((๐ โง 0 < (๐ด + ๐ต)) โ ((๐ด / (๐ด + ๐ต))โ๐๐ถ) โ
โ) |
27 | 5 | adantr 482 |
. . . . . . . 8
โข ((๐ โง 0 < (๐ด + ๐ต)) โ 0 โค ๐ต) |
28 | | divge0 12083 |
. . . . . . . 8
โข (((๐ต โ โ โง 0 โค
๐ต) โง ((๐ด + ๐ต) โ โ โง 0 < (๐ด + ๐ต))) โ 0 โค (๐ต / (๐ด + ๐ต))) |
29 | 18, 27, 21, 22, 28 | syl22anc 838 |
. . . . . . 7
โข ((๐ โง 0 < (๐ด + ๐ต)) โ 0 โค (๐ต / (๐ด + ๐ต))) |
30 | 19, 29, 25 | recxpcld 26231 |
. . . . . 6
โข ((๐ โง 0 < (๐ด + ๐ต)) โ ((๐ต / (๐ด + ๐ต))โ๐๐ถ) โ
โ) |
31 | 1, 2 | addge01d 11802 |
. . . . . . . . . . 11
โข (๐ โ (0 โค ๐ต โ ๐ด โค (๐ด + ๐ต))) |
32 | 5, 31 | mpbid 231 |
. . . . . . . . . 10
โข (๐ โ ๐ด โค (๐ด + ๐ต)) |
33 | 32 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง 0 < (๐ด + ๐ต)) โ ๐ด โค (๐ด + ๐ต)) |
34 | 21 | recnd 11242 |
. . . . . . . . . 10
โข ((๐ โง 0 < (๐ด + ๐ต)) โ (๐ด + ๐ต) โ โ) |
35 | 34 | mulridd 11231 |
. . . . . . . . 9
โข ((๐ โง 0 < (๐ด + ๐ต)) โ ((๐ด + ๐ต) ยท 1) = (๐ด + ๐ต)) |
36 | 33, 35 | breqtrrd 5177 |
. . . . . . . 8
โข ((๐ โง 0 < (๐ด + ๐ต)) โ ๐ด โค ((๐ด + ๐ต) ยท 1)) |
37 | | 1red 11215 |
. . . . . . . . 9
โข ((๐ โง 0 < (๐ด + ๐ต)) โ 1 โ โ) |
38 | | ledivmul 12090 |
. . . . . . . . 9
โข ((๐ด โ โ โง 1 โ
โ โง ((๐ด + ๐ต) โ โ โง 0 <
(๐ด + ๐ต))) โ ((๐ด / (๐ด + ๐ต)) โค 1 โ ๐ด โค ((๐ด + ๐ต) ยท 1))) |
39 | 13, 37, 21, 22, 38 | syl112anc 1375 |
. . . . . . . 8
โข ((๐ โง 0 < (๐ด + ๐ต)) โ ((๐ด / (๐ด + ๐ต)) โค 1 โ ๐ด โค ((๐ด + ๐ต) ยท 1))) |
40 | 36, 39 | mpbird 257 |
. . . . . . 7
โข ((๐ โง 0 < (๐ด + ๐ต)) โ (๐ด / (๐ด + ๐ต)) โค 1) |
41 | 7 | adantr 482 |
. . . . . . 7
โข ((๐ โง 0 < (๐ด + ๐ต)) โ ๐ถ โ
โ+) |
42 | | cxpaddle.6 |
. . . . . . . 8
โข (๐ โ ๐ถ โค 1) |
43 | 42 | adantr 482 |
. . . . . . 7
โข ((๐ โง 0 < (๐ด + ๐ต)) โ ๐ถ โค 1) |
44 | 17, 24, 40, 41, 43 | cxpaddlelem 26259 |
. . . . . 6
โข ((๐ โง 0 < (๐ด + ๐ต)) โ (๐ด / (๐ด + ๐ต)) โค ((๐ด / (๐ด + ๐ต))โ๐๐ถ)) |
45 | 2, 1 | addge02d 11803 |
. . . . . . . . . . 11
โข (๐ โ (0 โค ๐ด โ ๐ต โค (๐ด + ๐ต))) |
46 | 4, 45 | mpbid 231 |
. . . . . . . . . 10
โข (๐ โ ๐ต โค (๐ด + ๐ต)) |
47 | 46 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง 0 < (๐ด + ๐ต)) โ ๐ต โค (๐ด + ๐ต)) |
48 | 47, 35 | breqtrrd 5177 |
. . . . . . . 8
โข ((๐ โง 0 < (๐ด + ๐ต)) โ ๐ต โค ((๐ด + ๐ต) ยท 1)) |
49 | | ledivmul 12090 |
. . . . . . . . 9
โข ((๐ต โ โ โง 1 โ
โ โง ((๐ด + ๐ต) โ โ โง 0 <
(๐ด + ๐ต))) โ ((๐ต / (๐ด + ๐ต)) โค 1 โ ๐ต โค ((๐ด + ๐ต) ยท 1))) |
50 | 18, 37, 21, 22, 49 | syl112anc 1375 |
. . . . . . . 8
โข ((๐ โง 0 < (๐ด + ๐ต)) โ ((๐ต / (๐ด + ๐ต)) โค 1 โ ๐ต โค ((๐ด + ๐ต) ยท 1))) |
51 | 48, 50 | mpbird 257 |
. . . . . . 7
โข ((๐ โง 0 < (๐ด + ๐ต)) โ (๐ต / (๐ด + ๐ต)) โค 1) |
52 | 19, 29, 51, 41, 43 | cxpaddlelem 26259 |
. . . . . 6
โข ((๐ โง 0 < (๐ด + ๐ต)) โ (๐ต / (๐ด + ๐ต)) โค ((๐ต / (๐ด + ๐ต))โ๐๐ถ)) |
53 | 17, 19, 26, 30, 44, 52 | le2addd 11833 |
. . . . 5
โข ((๐ โง 0 < (๐ด + ๐ต)) โ ((๐ด / (๐ด + ๐ต)) + (๐ต / (๐ด + ๐ต))) โค (((๐ด / (๐ด + ๐ต))โ๐๐ถ) + ((๐ต / (๐ด + ๐ต))โ๐๐ถ))) |
54 | 13 | recnd 11242 |
. . . . . . 7
โข ((๐ โง 0 < (๐ด + ๐ต)) โ ๐ด โ โ) |
55 | 18 | recnd 11242 |
. . . . . . 7
โข ((๐ โง 0 < (๐ด + ๐ต)) โ ๐ต โ โ) |
56 | 16 | rpne0d 13021 |
. . . . . . 7
โข ((๐ โง 0 < (๐ด + ๐ต)) โ (๐ด + ๐ต) โ 0) |
57 | 54, 55, 34, 56 | divdird 12028 |
. . . . . 6
โข ((๐ โง 0 < (๐ด + ๐ต)) โ ((๐ด + ๐ต) / (๐ด + ๐ต)) = ((๐ด / (๐ด + ๐ต)) + (๐ต / (๐ด + ๐ต)))) |
58 | 34, 56 | dividd 11988 |
. . . . . 6
โข ((๐ โง 0 < (๐ด + ๐ต)) โ ((๐ด + ๐ต) / (๐ด + ๐ต)) = 1) |
59 | 57, 58 | eqtr3d 2775 |
. . . . 5
โข ((๐ โง 0 < (๐ด + ๐ต)) โ ((๐ด / (๐ด + ๐ต)) + (๐ต / (๐ด + ๐ต))) = 1) |
60 | 8 | recnd 11242 |
. . . . . . . . 9
โข (๐ โ ๐ถ โ โ) |
61 | 60 | adantr 482 |
. . . . . . . 8
โข ((๐ โง 0 < (๐ด + ๐ต)) โ ๐ถ โ โ) |
62 | 13, 20, 16, 61 | divcxpd 26230 |
. . . . . . 7
โข ((๐ โง 0 < (๐ด + ๐ต)) โ ((๐ด / (๐ด + ๐ต))โ๐๐ถ) = ((๐ดโ๐๐ถ) / ((๐ด + ๐ต)โ๐๐ถ))) |
63 | 18, 27, 16, 61 | divcxpd 26230 |
. . . . . . 7
โข ((๐ โง 0 < (๐ด + ๐ต)) โ ((๐ต / (๐ด + ๐ต))โ๐๐ถ) = ((๐ตโ๐๐ถ) / ((๐ด + ๐ต)โ๐๐ถ))) |
64 | 62, 63 | oveq12d 7427 |
. . . . . 6
โข ((๐ โง 0 < (๐ด + ๐ต)) โ (((๐ด / (๐ด + ๐ต))โ๐๐ถ) + ((๐ต / (๐ด + ๐ต))โ๐๐ถ)) = (((๐ดโ๐๐ถ) / ((๐ด + ๐ต)โ๐๐ถ)) + ((๐ตโ๐๐ถ) / ((๐ด + ๐ต)โ๐๐ถ)))) |
65 | 1, 4, 8 | recxpcld 26231 |
. . . . . . . . 9
โข (๐ โ (๐ดโ๐๐ถ) โ โ) |
66 | 65 | recnd 11242 |
. . . . . . . 8
โข (๐ โ (๐ดโ๐๐ถ) โ โ) |
67 | 66 | adantr 482 |
. . . . . . 7
โข ((๐ โง 0 < (๐ด + ๐ต)) โ (๐ดโ๐๐ถ) โ โ) |
68 | 2, 5, 8 | recxpcld 26231 |
. . . . . . . . 9
โข (๐ โ (๐ตโ๐๐ถ) โ โ) |
69 | 68 | recnd 11242 |
. . . . . . . 8
โข (๐ โ (๐ตโ๐๐ถ) โ โ) |
70 | 69 | adantr 482 |
. . . . . . 7
โข ((๐ โง 0 < (๐ด + ๐ต)) โ (๐ตโ๐๐ถ) โ โ) |
71 | 16, 25 | rpcxpcld 26241 |
. . . . . . . 8
โข ((๐ โง 0 < (๐ด + ๐ต)) โ ((๐ด + ๐ต)โ๐๐ถ) โ
โ+) |
72 | 71 | rpne0d 13021 |
. . . . . . 7
โข ((๐ โง 0 < (๐ด + ๐ต)) โ ((๐ด + ๐ต)โ๐๐ถ) โ 0) |
73 | 67, 70, 11, 72 | divdird 12028 |
. . . . . 6
โข ((๐ โง 0 < (๐ด + ๐ต)) โ (((๐ดโ๐๐ถ) + (๐ตโ๐๐ถ)) / ((๐ด + ๐ต)โ๐๐ถ)) = (((๐ดโ๐๐ถ) / ((๐ด + ๐ต)โ๐๐ถ)) + ((๐ตโ๐๐ถ) / ((๐ด + ๐ต)โ๐๐ถ)))) |
74 | 64, 73 | eqtr4d 2776 |
. . . . 5
โข ((๐ โง 0 < (๐ด + ๐ต)) โ (((๐ด / (๐ด + ๐ต))โ๐๐ถ) + ((๐ต / (๐ด + ๐ต))โ๐๐ถ)) = (((๐ดโ๐๐ถ) + (๐ตโ๐๐ถ)) / ((๐ด + ๐ต)โ๐๐ถ))) |
75 | 53, 59, 74 | 3brtr3d 5180 |
. . . 4
โข ((๐ โง 0 < (๐ด + ๐ต)) โ 1 โค (((๐ดโ๐๐ถ) + (๐ตโ๐๐ถ)) / ((๐ด + ๐ต)โ๐๐ถ))) |
76 | 65, 68 | readdcld 11243 |
. . . . . 6
โข (๐ โ ((๐ดโ๐๐ถ) + (๐ตโ๐๐ถ)) โ โ) |
77 | 76 | adantr 482 |
. . . . 5
โข ((๐ โง 0 < (๐ด + ๐ต)) โ ((๐ดโ๐๐ถ) + (๐ตโ๐๐ถ)) โ โ) |
78 | 37, 77, 71 | lemuldivd 13065 |
. . . 4
โข ((๐ โง 0 < (๐ด + ๐ต)) โ ((1 ยท ((๐ด + ๐ต)โ๐๐ถ)) โค ((๐ดโ๐๐ถ) + (๐ตโ๐๐ถ)) โ 1 โค (((๐ดโ๐๐ถ) + (๐ตโ๐๐ถ)) / ((๐ด + ๐ต)โ๐๐ถ)))) |
79 | 75, 78 | mpbird 257 |
. . 3
โข ((๐ โง 0 < (๐ด + ๐ต)) โ (1 ยท ((๐ด + ๐ต)โ๐๐ถ)) โค ((๐ดโ๐๐ถ) + (๐ตโ๐๐ถ))) |
80 | 12, 79 | eqbrtrrd 5173 |
. 2
โข ((๐ โง 0 < (๐ด + ๐ต)) โ ((๐ด + ๐ต)โ๐๐ถ) โค ((๐ดโ๐๐ถ) + (๐ตโ๐๐ถ))) |
81 | 7 | rpne0d 13021 |
. . . . . 6
โข (๐ โ ๐ถ โ 0) |
82 | 60, 81 | 0cxpd 26218 |
. . . . 5
โข (๐ โ
(0โ๐๐ถ) = 0) |
83 | 1, 4, 8 | cxpge0d 26232 |
. . . . . 6
โข (๐ โ 0 โค (๐ดโ๐๐ถ)) |
84 | 2, 5, 8 | cxpge0d 26232 |
. . . . . 6
โข (๐ โ 0 โค (๐ตโ๐๐ถ)) |
85 | 65, 68, 83, 84 | addge0d 11790 |
. . . . 5
โข (๐ โ 0 โค ((๐ดโ๐๐ถ) + (๐ตโ๐๐ถ))) |
86 | 82, 85 | eqbrtrd 5171 |
. . . 4
โข (๐ โ
(0โ๐๐ถ) โค ((๐ดโ๐๐ถ) + (๐ตโ๐๐ถ))) |
87 | | oveq1 7416 |
. . . . 5
โข (0 =
(๐ด + ๐ต) โ (0โ๐๐ถ) = ((๐ด + ๐ต)โ๐๐ถ)) |
88 | 87 | breq1d 5159 |
. . . 4
โข (0 =
(๐ด + ๐ต) โ ((0โ๐๐ถ) โค ((๐ดโ๐๐ถ) + (๐ตโ๐๐ถ)) โ ((๐ด + ๐ต)โ๐๐ถ) โค ((๐ดโ๐๐ถ) + (๐ตโ๐๐ถ)))) |
89 | 86, 88 | syl5ibcom 244 |
. . 3
โข (๐ โ (0 = (๐ด + ๐ต) โ ((๐ด + ๐ต)โ๐๐ถ) โค ((๐ดโ๐๐ถ) + (๐ตโ๐๐ถ)))) |
90 | 89 | imp 408 |
. 2
โข ((๐ โง 0 = (๐ด + ๐ต)) โ ((๐ด + ๐ต)โ๐๐ถ) โค ((๐ดโ๐๐ถ) + (๐ตโ๐๐ถ))) |
91 | | 0re 11216 |
. . . 4
โข 0 โ
โ |
92 | | leloe 11300 |
. . . 4
โข ((0
โ โ โง (๐ด +
๐ต) โ โ) โ
(0 โค (๐ด + ๐ต) โ (0 < (๐ด + ๐ต) โจ 0 = (๐ด + ๐ต)))) |
93 | 91, 3, 92 | sylancr 588 |
. . 3
โข (๐ โ (0 โค (๐ด + ๐ต) โ (0 < (๐ด + ๐ต) โจ 0 = (๐ด + ๐ต)))) |
94 | 6, 93 | mpbid 231 |
. 2
โข (๐ โ (0 < (๐ด + ๐ต) โจ 0 = (๐ด + ๐ต))) |
95 | 80, 90, 94 | mpjaodan 958 |
1
โข (๐ โ ((๐ด + ๐ต)โ๐๐ถ) โค ((๐ดโ๐๐ถ) + (๐ตโ๐๐ถ))) |