Step | Hyp | Ref
| Expression |
1 | | xralrple2.x |
. . . . 5
โข
โฒ๐ฅ๐ |
2 | | nfv 1918 |
. . . . 5
โข
โฒ๐ฅ ๐ด โค ๐ต |
3 | 1, 2 | nfan 1903 |
. . . 4
โข
โฒ๐ฅ(๐ โง ๐ด โค ๐ต) |
4 | | xralrple2.a |
. . . . . . 7
โข (๐ โ ๐ด โ
โ*) |
5 | 4 | ad2antrr 725 |
. . . . . 6
โข (((๐ โง ๐ด โค ๐ต) โง ๐ฅ โ โ+) โ ๐ด โ
โ*) |
6 | | icossxr 13356 |
. . . . . . 7
โข
(0[,)+โ) โ โ* |
7 | | xralrple2.b |
. . . . . . . 8
โข (๐ โ ๐ต โ (0[,)+โ)) |
8 | 7 | ad2antrr 725 |
. . . . . . 7
โข (((๐ โง ๐ด โค ๐ต) โง ๐ฅ โ โ+) โ ๐ต โ
(0[,)+โ)) |
9 | 6, 8 | sselid 3947 |
. . . . . 6
โข (((๐ โง ๐ด โค ๐ต) โง ๐ฅ โ โ+) โ ๐ต โ
โ*) |
10 | | 1red 11163 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ โ+) โ 1 โ
โ) |
11 | | rpre 12930 |
. . . . . . . . . . 11
โข (๐ฅ โ โ+
โ ๐ฅ โ
โ) |
12 | 11 | adantl 483 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ โ+) โ ๐ฅ โ
โ) |
13 | 10, 12 | readdcld 11191 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ โ+) โ (1 +
๐ฅ) โ
โ) |
14 | | rge0ssre 13380 |
. . . . . . . . . . 11
โข
(0[,)+โ) โ โ |
15 | 14, 7 | sselid 3947 |
. . . . . . . . . 10
โข (๐ โ ๐ต โ โ) |
16 | 15 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ โ+) โ ๐ต โ
โ) |
17 | 13, 16 | remulcld 11192 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ โ+) โ ((1 +
๐ฅ) ยท ๐ต) โ
โ) |
18 | 17 | rexrd 11212 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ โ+) โ ((1 +
๐ฅ) ยท ๐ต) โ
โ*) |
19 | 18 | adantlr 714 |
. . . . . 6
โข (((๐ โง ๐ด โค ๐ต) โง ๐ฅ โ โ+) โ ((1 +
๐ฅ) ยท ๐ต) โ
โ*) |
20 | | simplr 768 |
. . . . . 6
โข (((๐ โง ๐ด โค ๐ต) โง ๐ฅ โ โ+) โ ๐ด โค ๐ต) |
21 | 15 | ad2antrr 725 |
. . . . . . 7
โข (((๐ โง ๐ด โค ๐ต) โง ๐ฅ โ โ+) โ ๐ต โ
โ) |
22 | | 1red 11163 |
. . . . . . . . 9
โข (๐ฅ โ โ+
โ 1 โ โ) |
23 | 22, 11 | readdcld 11191 |
. . . . . . . 8
โข (๐ฅ โ โ+
โ (1 + ๐ฅ) โ
โ) |
24 | 23 | adantl 483 |
. . . . . . 7
โข (((๐ โง ๐ด โค ๐ต) โง ๐ฅ โ โ+) โ (1 +
๐ฅ) โ
โ) |
25 | | 0xr 11209 |
. . . . . . . . . . 11
โข 0 โ
โ* |
26 | 25 | a1i 11 |
. . . . . . . . . 10
โข (๐ต โ (0[,)+โ) โ 0
โ โ*) |
27 | | pnfxr 11216 |
. . . . . . . . . . 11
โข +โ
โ โ* |
28 | 27 | a1i 11 |
. . . . . . . . . 10
โข (๐ต โ (0[,)+โ) โ
+โ โ โ*) |
29 | | id 22 |
. . . . . . . . . 10
โข (๐ต โ (0[,)+โ) โ
๐ต โ
(0[,)+โ)) |
30 | | icogelb 13322 |
. . . . . . . . . 10
โข ((0
โ โ* โง +โ โ โ* โง
๐ต โ (0[,)+โ))
โ 0 โค ๐ต) |
31 | 26, 28, 29, 30 | syl3anc 1372 |
. . . . . . . . 9
โข (๐ต โ (0[,)+โ) โ 0
โค ๐ต) |
32 | 7, 31 | syl 17 |
. . . . . . . 8
โข (๐ โ 0 โค ๐ต) |
33 | 32 | ad2antrr 725 |
. . . . . . 7
โข (((๐ โง ๐ด โค ๐ต) โง ๐ฅ โ โ+) โ 0 โค
๐ต) |
34 | | id 22 |
. . . . . . . . . 10
โข (๐ฅ โ โ+
โ ๐ฅ โ
โ+) |
35 | 22, 34 | ltaddrpd 12997 |
. . . . . . . . 9
โข (๐ฅ โ โ+
โ 1 < (1 + ๐ฅ)) |
36 | 22, 23, 35 | ltled 11310 |
. . . . . . . 8
โข (๐ฅ โ โ+
โ 1 โค (1 + ๐ฅ)) |
37 | 36 | adantl 483 |
. . . . . . 7
โข (((๐ โง ๐ด โค ๐ต) โง ๐ฅ โ โ+) โ 1 โค (1
+ ๐ฅ)) |
38 | 21, 24, 33, 37 | lemulge12d 12100 |
. . . . . 6
โข (((๐ โง ๐ด โค ๐ต) โง ๐ฅ โ โ+) โ ๐ต โค ((1 + ๐ฅ) ยท ๐ต)) |
39 | 5, 9, 19, 20, 38 | xrletrd 13088 |
. . . . 5
โข (((๐ โง ๐ด โค ๐ต) โง ๐ฅ โ โ+) โ ๐ด โค ((1 + ๐ฅ) ยท ๐ต)) |
40 | 39 | ex 414 |
. . . 4
โข ((๐ โง ๐ด โค ๐ต) โ (๐ฅ โ โ+ โ ๐ด โค ((1 + ๐ฅ) ยท ๐ต))) |
41 | 3, 40 | ralrimi 3243 |
. . 3
โข ((๐ โง ๐ด โค ๐ต) โ โ๐ฅ โ โ+ ๐ด โค ((1 + ๐ฅ) ยท ๐ต)) |
42 | 41 | ex 414 |
. 2
โข (๐ โ (๐ด โค ๐ต โ โ๐ฅ โ โ+ ๐ด โค ((1 + ๐ฅ) ยท ๐ต))) |
43 | 4 | ad3antrrr 729 |
. . . . . . 7
โข ((((๐ โง โ๐ฅ โ โ+ ๐ด โค ((1 + ๐ฅ) ยท ๐ต)) โง ๐ฆ โ โ+) โง ๐ต = 0) โ ๐ด โ
โ*) |
44 | | id 22 |
. . . . . . . . . . . 12
โข (๐ต = 0 โ ๐ต = 0) |
45 | | 0red 11165 |
. . . . . . . . . . . 12
โข (๐ต = 0 โ 0 โ
โ) |
46 | 44, 45 | eqeltrd 2838 |
. . . . . . . . . . 11
โข (๐ต = 0 โ ๐ต โ โ) |
47 | 46 | adantl 483 |
. . . . . . . . . 10
โข ((๐ฆ โ โ+
โง ๐ต = 0) โ ๐ต โ
โ) |
48 | | rpre 12930 |
. . . . . . . . . . 11
โข (๐ฆ โ โ+
โ ๐ฆ โ
โ) |
49 | 48 | adantr 482 |
. . . . . . . . . 10
โข ((๐ฆ โ โ+
โง ๐ต = 0) โ ๐ฆ โ
โ) |
50 | 47, 49 | readdcld 11191 |
. . . . . . . . 9
โข ((๐ฆ โ โ+
โง ๐ต = 0) โ (๐ต + ๐ฆ) โ โ) |
51 | 50 | rexrd 11212 |
. . . . . . . 8
โข ((๐ฆ โ โ+
โง ๐ต = 0) โ (๐ต + ๐ฆ) โ
โ*) |
52 | 51 | adantll 713 |
. . . . . . 7
โข ((((๐ โง โ๐ฅ โ โ+ ๐ด โค ((1 + ๐ฅ) ยท ๐ต)) โง ๐ฆ โ โ+) โง ๐ต = 0) โ (๐ต + ๐ฆ) โ
โ*) |
53 | 25 | a1i 11 |
. . . . . . . 8
โข ((((๐ โง โ๐ฅ โ โ+ ๐ด โค ((1 + ๐ฅ) ยท ๐ต)) โง ๐ฆ โ โ+) โง ๐ต = 0) โ 0 โ
โ*) |
54 | | 1rp 12926 |
. . . . . . . . . . . . . 14
โข 1 โ
โ+ |
55 | 54 | a1i 11 |
. . . . . . . . . . . . 13
โข
(โ๐ฅ โ
โ+ ๐ด โค
((1 + ๐ฅ) ยท ๐ต) โ 1 โ
โ+) |
56 | | id 22 |
. . . . . . . . . . . . 13
โข
(โ๐ฅ โ
โ+ ๐ด โค
((1 + ๐ฅ) ยท ๐ต) โ โ๐ฅ โ โ+
๐ด โค ((1 + ๐ฅ) ยท ๐ต)) |
57 | | oveq2 7370 |
. . . . . . . . . . . . . . . 16
โข (๐ฅ = 1 โ (1 + ๐ฅ) = (1 + 1)) |
58 | 57 | oveq1d 7377 |
. . . . . . . . . . . . . . 15
โข (๐ฅ = 1 โ ((1 + ๐ฅ) ยท ๐ต) = ((1 + 1) ยท ๐ต)) |
59 | 58 | breq2d 5122 |
. . . . . . . . . . . . . 14
โข (๐ฅ = 1 โ (๐ด โค ((1 + ๐ฅ) ยท ๐ต) โ ๐ด โค ((1 + 1) ยท ๐ต))) |
60 | 59 | rspcva 3582 |
. . . . . . . . . . . . 13
โข ((1
โ โ+ โง โ๐ฅ โ โ+ ๐ด โค ((1 + ๐ฅ) ยท ๐ต)) โ ๐ด โค ((1 + 1) ยท ๐ต)) |
61 | 55, 56, 60 | syl2anc 585 |
. . . . . . . . . . . 12
โข
(โ๐ฅ โ
โ+ ๐ด โค
((1 + ๐ฅ) ยท ๐ต) โ ๐ด โค ((1 + 1) ยท ๐ต)) |
62 | | 1p1e2 12285 |
. . . . . . . . . . . . . 14
โข (1 + 1) =
2 |
63 | 62 | a1i 11 |
. . . . . . . . . . . . 13
โข
(โ๐ฅ โ
โ+ ๐ด โค
((1 + ๐ฅ) ยท ๐ต) โ (1 + 1) =
2) |
64 | 63 | oveq1d 7377 |
. . . . . . . . . . . 12
โข
(โ๐ฅ โ
โ+ ๐ด โค
((1 + ๐ฅ) ยท ๐ต) โ ((1 + 1) ยท ๐ต) = (2 ยท ๐ต)) |
65 | 61, 64 | breqtrd 5136 |
. . . . . . . . . . 11
โข
(โ๐ฅ โ
โ+ ๐ด โค
((1 + ๐ฅ) ยท ๐ต) โ ๐ด โค (2 ยท ๐ต)) |
66 | 65 | adantr 482 |
. . . . . . . . . 10
โข
((โ๐ฅ โ
โ+ ๐ด โค
((1 + ๐ฅ) ยท ๐ต) โง ๐ต = 0) โ ๐ด โค (2 ยท ๐ต)) |
67 | | simpr 486 |
. . . . . . . . . 10
โข
((โ๐ฅ โ
โ+ ๐ด โค
((1 + ๐ฅ) ยท ๐ต) โง ๐ต = 0) โ ๐ต = 0) |
68 | | simpl 484 |
. . . . . . . . . . 11
โข ((๐ด โค (2 ยท ๐ต) โง ๐ต = 0) โ ๐ด โค (2 ยท ๐ต)) |
69 | | oveq2 7370 |
. . . . . . . . . . . . 13
โข (๐ต = 0 โ (2 ยท ๐ต) = (2 ยท
0)) |
70 | | 2cnd 12238 |
. . . . . . . . . . . . . 14
โข (๐ต = 0 โ 2 โ
โ) |
71 | 70 | mul01d 11361 |
. . . . . . . . . . . . 13
โข (๐ต = 0 โ (2 ยท 0) =
0) |
72 | 69, 71 | eqtrd 2777 |
. . . . . . . . . . . 12
โข (๐ต = 0 โ (2 ยท ๐ต) = 0) |
73 | 72 | adantl 483 |
. . . . . . . . . . 11
โข ((๐ด โค (2 ยท ๐ต) โง ๐ต = 0) โ (2 ยท ๐ต) = 0) |
74 | 68, 73 | breqtrd 5136 |
. . . . . . . . . 10
โข ((๐ด โค (2 ยท ๐ต) โง ๐ต = 0) โ ๐ด โค 0) |
75 | 66, 67, 74 | syl2anc 585 |
. . . . . . . . 9
โข
((โ๐ฅ โ
โ+ ๐ด โค
((1 + ๐ฅ) ยท ๐ต) โง ๐ต = 0) โ ๐ด โค 0) |
76 | 75 | ad4ant24 753 |
. . . . . . . 8
โข ((((๐ โง โ๐ฅ โ โ+ ๐ด โค ((1 + ๐ฅ) ยท ๐ต)) โง ๐ฆ โ โ+) โง ๐ต = 0) โ ๐ด โค 0) |
77 | | rpgt0 12934 |
. . . . . . . . . . 11
โข (๐ฆ โ โ+
โ 0 < ๐ฆ) |
78 | 77 | adantr 482 |
. . . . . . . . . 10
โข ((๐ฆ โ โ+
โง ๐ต = 0) โ 0 <
๐ฆ) |
79 | | oveq1 7369 |
. . . . . . . . . . . 12
โข (๐ต = 0 โ (๐ต + ๐ฆ) = (0 + ๐ฆ)) |
80 | 79 | adantl 483 |
. . . . . . . . . . 11
โข ((๐ฆ โ โ+
โง ๐ต = 0) โ (๐ต + ๐ฆ) = (0 + ๐ฆ)) |
81 | 48 | recnd 11190 |
. . . . . . . . . . . . 13
โข (๐ฆ โ โ+
โ ๐ฆ โ
โ) |
82 | 81 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ฆ โ โ+
โง ๐ต = 0) โ ๐ฆ โ
โ) |
83 | 82 | addid2d 11363 |
. . . . . . . . . . 11
โข ((๐ฆ โ โ+
โง ๐ต = 0) โ (0 +
๐ฆ) = ๐ฆ) |
84 | 80, 83 | eqtr2d 2778 |
. . . . . . . . . 10
โข ((๐ฆ โ โ+
โง ๐ต = 0) โ ๐ฆ = (๐ต + ๐ฆ)) |
85 | 78, 84 | breqtrd 5136 |
. . . . . . . . 9
โข ((๐ฆ โ โ+
โง ๐ต = 0) โ 0 <
(๐ต + ๐ฆ)) |
86 | 85 | adantll 713 |
. . . . . . . 8
โข ((((๐ โง โ๐ฅ โ โ+ ๐ด โค ((1 + ๐ฅ) ยท ๐ต)) โง ๐ฆ โ โ+) โง ๐ต = 0) โ 0 < (๐ต + ๐ฆ)) |
87 | 43, 53, 52, 76, 86 | xrlelttrd 13086 |
. . . . . . 7
โข ((((๐ โง โ๐ฅ โ โ+ ๐ด โค ((1 + ๐ฅ) ยท ๐ต)) โง ๐ฆ โ โ+) โง ๐ต = 0) โ ๐ด < (๐ต + ๐ฆ)) |
88 | 43, 52, 87 | xrltled 13076 |
. . . . . 6
โข ((((๐ โง โ๐ฅ โ โ+ ๐ด โค ((1 + ๐ฅ) ยท ๐ต)) โง ๐ฆ โ โ+) โง ๐ต = 0) โ ๐ด โค (๐ต + ๐ฆ)) |
89 | | simpl 484 |
. . . . . . 7
โข ((((๐ โง โ๐ฅ โ โ+ ๐ด โค ((1 + ๐ฅ) ยท ๐ต)) โง ๐ฆ โ โ+) โง ยฌ
๐ต = 0) โ ((๐ โง โ๐ฅ โ โ+ ๐ด โค ((1 + ๐ฅ) ยท ๐ต)) โง ๐ฆ โ
โ+)) |
90 | 15 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง ยฌ ๐ต = 0) โ ๐ต โ โ) |
91 | | 0red 11165 |
. . . . . . . . . 10
โข ((๐ โง ยฌ ๐ต = 0) โ 0 โ
โ) |
92 | 32 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง ยฌ ๐ต = 0) โ 0 โค ๐ต) |
93 | 44 | necon3bi 2971 |
. . . . . . . . . . 11
โข (ยฌ
๐ต = 0 โ ๐ต โ 0) |
94 | 93 | adantl 483 |
. . . . . . . . . 10
โข ((๐ โง ยฌ ๐ต = 0) โ ๐ต โ 0) |
95 | 91, 90, 92, 94 | leneltd 11316 |
. . . . . . . . 9
โข ((๐ โง ยฌ ๐ต = 0) โ 0 < ๐ต) |
96 | 90, 95 | elrpd 12961 |
. . . . . . . 8
โข ((๐ โง ยฌ ๐ต = 0) โ ๐ต โ
โ+) |
97 | 96 | ad4ant14 751 |
. . . . . . 7
โข ((((๐ โง โ๐ฅ โ โ+ ๐ด โค ((1 + ๐ฅ) ยท ๐ต)) โง ๐ฆ โ โ+) โง ยฌ
๐ต = 0) โ ๐ต โ
โ+) |
98 | | simplr 768 |
. . . . . . . . . . 11
โข
(((โ๐ฅ โ
โ+ ๐ด โค
((1 + ๐ฅ) ยท ๐ต) โง ๐ฆ โ โ+) โง ๐ต โ โ+)
โ ๐ฆ โ
โ+) |
99 | | simpr 486 |
. . . . . . . . . . 11
โข
(((โ๐ฅ โ
โ+ ๐ด โค
((1 + ๐ฅ) ยท ๐ต) โง ๐ฆ โ โ+) โง ๐ต โ โ+)
โ ๐ต โ
โ+) |
100 | 98, 99 | rpdivcld 12981 |
. . . . . . . . . 10
โข
(((โ๐ฅ โ
โ+ ๐ด โค
((1 + ๐ฅ) ยท ๐ต) โง ๐ฆ โ โ+) โง ๐ต โ โ+)
โ (๐ฆ / ๐ต) โ
โ+) |
101 | | simpll 766 |
. . . . . . . . . 10
โข
(((โ๐ฅ โ
โ+ ๐ด โค
((1 + ๐ฅ) ยท ๐ต) โง ๐ฆ โ โ+) โง ๐ต โ โ+)
โ โ๐ฅ โ
โ+ ๐ด โค
((1 + ๐ฅ) ยท ๐ต)) |
102 | | oveq2 7370 |
. . . . . . . . . . . . 13
โข (๐ฅ = (๐ฆ / ๐ต) โ (1 + ๐ฅ) = (1 + (๐ฆ / ๐ต))) |
103 | 102 | oveq1d 7377 |
. . . . . . . . . . . 12
โข (๐ฅ = (๐ฆ / ๐ต) โ ((1 + ๐ฅ) ยท ๐ต) = ((1 + (๐ฆ / ๐ต)) ยท ๐ต)) |
104 | 103 | breq2d 5122 |
. . . . . . . . . . 11
โข (๐ฅ = (๐ฆ / ๐ต) โ (๐ด โค ((1 + ๐ฅ) ยท ๐ต) โ ๐ด โค ((1 + (๐ฆ / ๐ต)) ยท ๐ต))) |
105 | 104 | rspcva 3582 |
. . . . . . . . . 10
โข (((๐ฆ / ๐ต) โ โ+ โง
โ๐ฅ โ
โ+ ๐ด โค
((1 + ๐ฅ) ยท ๐ต)) โ ๐ด โค ((1 + (๐ฆ / ๐ต)) ยท ๐ต)) |
106 | 100, 101,
105 | syl2anc 585 |
. . . . . . . . 9
โข
(((โ๐ฅ โ
โ+ ๐ด โค
((1 + ๐ฅ) ยท ๐ต) โง ๐ฆ โ โ+) โง ๐ต โ โ+)
โ ๐ด โค ((1 + (๐ฆ / ๐ต)) ยท ๐ต)) |
107 | 106 | adantlll 717 |
. . . . . . . 8
โข ((((๐ โง โ๐ฅ โ โ+ ๐ด โค ((1 + ๐ฅ) ยท ๐ต)) โง ๐ฆ โ โ+) โง ๐ต โ โ+)
โ ๐ด โค ((1 + (๐ฆ / ๐ต)) ยท ๐ต)) |
108 | | 1cnd 11157 |
. . . . . . . . . . 11
โข ((๐ฆ โ โ+
โง ๐ต โ
โ+) โ 1 โ โ) |
109 | 81 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ฆ โ โ+
โง ๐ต โ
โ+) โ ๐ฆ โ โ) |
110 | | rpcn 12932 |
. . . . . . . . . . . . 13
โข (๐ต โ โ+
โ ๐ต โ
โ) |
111 | 110 | adantl 483 |
. . . . . . . . . . . 12
โข ((๐ฆ โ โ+
โง ๐ต โ
โ+) โ ๐ต โ โ) |
112 | | rpne0 12938 |
. . . . . . . . . . . . 13
โข (๐ต โ โ+
โ ๐ต โ
0) |
113 | 112 | adantl 483 |
. . . . . . . . . . . 12
โข ((๐ฆ โ โ+
โง ๐ต โ
โ+) โ ๐ต โ 0) |
114 | 109, 111,
113 | divcld 11938 |
. . . . . . . . . . 11
โข ((๐ฆ โ โ+
โง ๐ต โ
โ+) โ (๐ฆ / ๐ต) โ โ) |
115 | 108, 114,
111 | adddird 11187 |
. . . . . . . . . 10
โข ((๐ฆ โ โ+
โง ๐ต โ
โ+) โ ((1 + (๐ฆ / ๐ต)) ยท ๐ต) = ((1 ยท ๐ต) + ((๐ฆ / ๐ต) ยท ๐ต))) |
116 | 111 | mulid2d 11180 |
. . . . . . . . . . 11
โข ((๐ฆ โ โ+
โง ๐ต โ
โ+) โ (1 ยท ๐ต) = ๐ต) |
117 | 109, 111,
113 | divcan1d 11939 |
. . . . . . . . . . 11
โข ((๐ฆ โ โ+
โง ๐ต โ
โ+) โ ((๐ฆ / ๐ต) ยท ๐ต) = ๐ฆ) |
118 | 116, 117 | oveq12d 7380 |
. . . . . . . . . 10
โข ((๐ฆ โ โ+
โง ๐ต โ
โ+) โ ((1 ยท ๐ต) + ((๐ฆ / ๐ต) ยท ๐ต)) = (๐ต + ๐ฆ)) |
119 | | eqidd 2738 |
. . . . . . . . . 10
โข ((๐ฆ โ โ+
โง ๐ต โ
โ+) โ (๐ต + ๐ฆ) = (๐ต + ๐ฆ)) |
120 | 115, 118,
119 | 3eqtrd 2781 |
. . . . . . . . 9
โข ((๐ฆ โ โ+
โง ๐ต โ
โ+) โ ((1 + (๐ฆ / ๐ต)) ยท ๐ต) = (๐ต + ๐ฆ)) |
121 | 120 | adantll 713 |
. . . . . . . 8
โข ((((๐ โง โ๐ฅ โ โ+ ๐ด โค ((1 + ๐ฅ) ยท ๐ต)) โง ๐ฆ โ โ+) โง ๐ต โ โ+)
โ ((1 + (๐ฆ / ๐ต)) ยท ๐ต) = (๐ต + ๐ฆ)) |
122 | 107, 121 | breqtrd 5136 |
. . . . . . 7
โข ((((๐ โง โ๐ฅ โ โ+ ๐ด โค ((1 + ๐ฅ) ยท ๐ต)) โง ๐ฆ โ โ+) โง ๐ต โ โ+)
โ ๐ด โค (๐ต + ๐ฆ)) |
123 | 89, 97, 122 | syl2anc 585 |
. . . . . 6
โข ((((๐ โง โ๐ฅ โ โ+ ๐ด โค ((1 + ๐ฅ) ยท ๐ต)) โง ๐ฆ โ โ+) โง ยฌ
๐ต = 0) โ ๐ด โค (๐ต + ๐ฆ)) |
124 | 88, 123 | pm2.61dan 812 |
. . . . 5
โข (((๐ โง โ๐ฅ โ โ+ ๐ด โค ((1 + ๐ฅ) ยท ๐ต)) โง ๐ฆ โ โ+) โ ๐ด โค (๐ต + ๐ฆ)) |
125 | 124 | ralrimiva 3144 |
. . . 4
โข ((๐ โง โ๐ฅ โ โ+ ๐ด โค ((1 + ๐ฅ) ยท ๐ต)) โ โ๐ฆ โ โ+ ๐ด โค (๐ต + ๐ฆ)) |
126 | | xralrple 13131 |
. . . . . 6
โข ((๐ด โ โ*
โง ๐ต โ โ)
โ (๐ด โค ๐ต โ โ๐ฆ โ โ+
๐ด โค (๐ต + ๐ฆ))) |
127 | 4, 15, 126 | syl2anc 585 |
. . . . 5
โข (๐ โ (๐ด โค ๐ต โ โ๐ฆ โ โ+ ๐ด โค (๐ต + ๐ฆ))) |
128 | 127 | adantr 482 |
. . . 4
โข ((๐ โง โ๐ฅ โ โ+ ๐ด โค ((1 + ๐ฅ) ยท ๐ต)) โ (๐ด โค ๐ต โ โ๐ฆ โ โ+ ๐ด โค (๐ต + ๐ฆ))) |
129 | 125, 128 | mpbird 257 |
. . 3
โข ((๐ โง โ๐ฅ โ โ+ ๐ด โค ((1 + ๐ฅ) ยท ๐ต)) โ ๐ด โค ๐ต) |
130 | 129 | ex 414 |
. 2
โข (๐ โ (โ๐ฅ โ โ+
๐ด โค ((1 + ๐ฅ) ยท ๐ต) โ ๐ด โค ๐ต)) |
131 | 42, 130 | impbid 211 |
1
โข (๐ โ (๐ด โค ๐ต โ โ๐ฅ โ โ+ ๐ด โค ((1 + ๐ฅ) ยท ๐ต))) |