Step | Hyp | Ref
| Expression |
1 | | xralrple3.a |
. . . . . 6
โข (๐ โ ๐ด โ
โ*) |
2 | 1 | ad2antrr 725 |
. . . . 5
โข (((๐ โง ๐ด โค ๐ต) โง ๐ฅ โ โ+) โ ๐ด โ
โ*) |
3 | | xralrple3.b |
. . . . . . 7
โข (๐ โ ๐ต โ โ) |
4 | 3 | rexrd 11210 |
. . . . . 6
โข (๐ โ ๐ต โ
โ*) |
5 | 4 | ad2antrr 725 |
. . . . 5
โข (((๐ โง ๐ด โค ๐ต) โง ๐ฅ โ โ+) โ ๐ต โ
โ*) |
6 | 3 | ad2antrr 725 |
. . . . . . 7
โข (((๐ โง ๐ด โค ๐ต) โง ๐ฅ โ โ+) โ ๐ต โ
โ) |
7 | | xralrple3.c |
. . . . . . . . 9
โข (๐ โ ๐ถ โ โ) |
8 | 7 | ad2antrr 725 |
. . . . . . . 8
โข (((๐ โง ๐ด โค ๐ต) โง ๐ฅ โ โ+) โ ๐ถ โ
โ) |
9 | | rpre 12928 |
. . . . . . . . 9
โข (๐ฅ โ โ+
โ ๐ฅ โ
โ) |
10 | 9 | adantl 483 |
. . . . . . . 8
โข (((๐ โง ๐ด โค ๐ต) โง ๐ฅ โ โ+) โ ๐ฅ โ
โ) |
11 | 8, 10 | remulcld 11190 |
. . . . . . 7
โข (((๐ โง ๐ด โค ๐ต) โง ๐ฅ โ โ+) โ (๐ถ ยท ๐ฅ) โ โ) |
12 | 6, 11 | readdcld 11189 |
. . . . . 6
โข (((๐ โง ๐ด โค ๐ต) โง ๐ฅ โ โ+) โ (๐ต + (๐ถ ยท ๐ฅ)) โ โ) |
13 | 12 | rexrd 11210 |
. . . . 5
โข (((๐ โง ๐ด โค ๐ต) โง ๐ฅ โ โ+) โ (๐ต + (๐ถ ยท ๐ฅ)) โ
โ*) |
14 | | simplr 768 |
. . . . 5
โข (((๐ โง ๐ด โค ๐ต) โง ๐ฅ โ โ+) โ ๐ด โค ๐ต) |
15 | 7 | adantr 482 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ โ+) โ ๐ถ โ
โ) |
16 | 9 | adantl 483 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ โ+) โ ๐ฅ โ
โ) |
17 | | xralrple3.g |
. . . . . . . . 9
โข (๐ โ 0 โค ๐ถ) |
18 | 17 | adantr 482 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ โ+) โ 0 โค
๐ถ) |
19 | | rpge0 12933 |
. . . . . . . . 9
โข (๐ฅ โ โ+
โ 0 โค ๐ฅ) |
20 | 19 | adantl 483 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ โ+) โ 0 โค
๐ฅ) |
21 | 15, 16, 18, 20 | mulge0d 11737 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ โ+) โ 0 โค
(๐ถ ยท ๐ฅ)) |
22 | 3 | adantr 482 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ โ+) โ ๐ต โ
โ) |
23 | 15, 16 | remulcld 11190 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ โ+) โ (๐ถ ยท ๐ฅ) โ โ) |
24 | 22, 23 | addge01d 11748 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ โ+) โ (0 โค
(๐ถ ยท ๐ฅ) โ ๐ต โค (๐ต + (๐ถ ยท ๐ฅ)))) |
25 | 21, 24 | mpbid 231 |
. . . . . 6
โข ((๐ โง ๐ฅ โ โ+) โ ๐ต โค (๐ต + (๐ถ ยท ๐ฅ))) |
26 | 25 | adantlr 714 |
. . . . 5
โข (((๐ โง ๐ด โค ๐ต) โง ๐ฅ โ โ+) โ ๐ต โค (๐ต + (๐ถ ยท ๐ฅ))) |
27 | 2, 5, 13, 14, 26 | xrletrd 13087 |
. . . 4
โข (((๐ โง ๐ด โค ๐ต) โง ๐ฅ โ โ+) โ ๐ด โค (๐ต + (๐ถ ยท ๐ฅ))) |
28 | 27 | ralrimiva 3140 |
. . 3
โข ((๐ โง ๐ด โค ๐ต) โ โ๐ฅ โ โ+ ๐ด โค (๐ต + (๐ถ ยท ๐ฅ))) |
29 | 28 | ex 414 |
. 2
โข (๐ โ (๐ด โค ๐ต โ โ๐ฅ โ โ+ ๐ด โค (๐ต + (๐ถ ยท ๐ฅ)))) |
30 | | 1rp 12924 |
. . . . . . 7
โข 1 โ
โ+ |
31 | | oveq2 7366 |
. . . . . . . . . 10
โข (๐ฅ = 1 โ (๐ถ ยท ๐ฅ) = (๐ถ ยท 1)) |
32 | 31 | oveq2d 7374 |
. . . . . . . . 9
โข (๐ฅ = 1 โ (๐ต + (๐ถ ยท ๐ฅ)) = (๐ต + (๐ถ ยท 1))) |
33 | 32 | breq2d 5118 |
. . . . . . . 8
โข (๐ฅ = 1 โ (๐ด โค (๐ต + (๐ถ ยท ๐ฅ)) โ ๐ด โค (๐ต + (๐ถ ยท 1)))) |
34 | 33 | rspcva 3578 |
. . . . . . 7
โข ((1
โ โ+ โง โ๐ฅ โ โ+ ๐ด โค (๐ต + (๐ถ ยท ๐ฅ))) โ ๐ด โค (๐ต + (๐ถ ยท 1))) |
35 | 30, 34 | mpan 689 |
. . . . . 6
โข
(โ๐ฅ โ
โ+ ๐ด โค
(๐ต + (๐ถ ยท ๐ฅ)) โ ๐ด โค (๐ต + (๐ถ ยท 1))) |
36 | 35 | ad2antlr 726 |
. . . . 5
โข (((๐ โง โ๐ฅ โ โ+ ๐ด โค (๐ต + (๐ถ ยท ๐ฅ))) โง ๐ถ = 0) โ ๐ด โค (๐ต + (๐ถ ยท 1))) |
37 | | oveq1 7365 |
. . . . . . . . . 10
โข (๐ถ = 0 โ (๐ถ ยท 1) = (0 ยท
1)) |
38 | | 0cn 11152 |
. . . . . . . . . . . 12
โข 0 โ
โ |
39 | 38 | mulid1i 11164 |
. . . . . . . . . . 11
โข (0
ยท 1) = 0 |
40 | 39 | a1i 11 |
. . . . . . . . . 10
โข (๐ถ = 0 โ (0 ยท 1) =
0) |
41 | 37, 40 | eqtrd 2773 |
. . . . . . . . 9
โข (๐ถ = 0 โ (๐ถ ยท 1) = 0) |
42 | 41 | oveq2d 7374 |
. . . . . . . 8
โข (๐ถ = 0 โ (๐ต + (๐ถ ยท 1)) = (๐ต + 0)) |
43 | 42 | adantl 483 |
. . . . . . 7
โข ((๐ โง ๐ถ = 0) โ (๐ต + (๐ถ ยท 1)) = (๐ต + 0)) |
44 | 3 | recnd 11188 |
. . . . . . . . 9
โข (๐ โ ๐ต โ โ) |
45 | 44 | adantr 482 |
. . . . . . . 8
โข ((๐ โง ๐ถ = 0) โ ๐ต โ โ) |
46 | 45 | addid1d 11360 |
. . . . . . 7
โข ((๐ โง ๐ถ = 0) โ (๐ต + 0) = ๐ต) |
47 | 43, 46 | eqtrd 2773 |
. . . . . 6
โข ((๐ โง ๐ถ = 0) โ (๐ต + (๐ถ ยท 1)) = ๐ต) |
48 | 47 | adantlr 714 |
. . . . 5
โข (((๐ โง โ๐ฅ โ โ+ ๐ด โค (๐ต + (๐ถ ยท ๐ฅ))) โง ๐ถ = 0) โ (๐ต + (๐ถ ยท 1)) = ๐ต) |
49 | 36, 48 | breqtrd 5132 |
. . . 4
โข (((๐ โง โ๐ฅ โ โ+ ๐ด โค (๐ต + (๐ถ ยท ๐ฅ))) โง ๐ถ = 0) โ ๐ด โค ๐ต) |
50 | | neqne 2948 |
. . . . . . . 8
โข (ยฌ
๐ถ = 0 โ ๐ถ โ 0) |
51 | 50 | adantl 483 |
. . . . . . 7
โข ((๐ โง ยฌ ๐ถ = 0) โ ๐ถ โ 0) |
52 | 7 | adantr 482 |
. . . . . . . 8
โข ((๐ โง ๐ถ โ 0) โ ๐ถ โ โ) |
53 | | 0red 11163 |
. . . . . . . . 9
โข ((๐ โง ๐ถ โ 0) โ 0 โ
โ) |
54 | 17 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง ๐ถ โ 0) โ 0 โค ๐ถ) |
55 | | simpr 486 |
. . . . . . . . 9
โข ((๐ โง ๐ถ โ 0) โ ๐ถ โ 0) |
56 | 53, 52, 54, 55 | leneltd 11314 |
. . . . . . . 8
โข ((๐ โง ๐ถ โ 0) โ 0 < ๐ถ) |
57 | 52, 56 | elrpd 12959 |
. . . . . . 7
โข ((๐ โง ๐ถ โ 0) โ ๐ถ โ
โ+) |
58 | 51, 57 | syldan 592 |
. . . . . 6
โข ((๐ โง ยฌ ๐ถ = 0) โ ๐ถ โ
โ+) |
59 | 58 | adantlr 714 |
. . . . 5
โข (((๐ โง โ๐ฅ โ โ+ ๐ด โค (๐ต + (๐ถ ยท ๐ฅ))) โง ยฌ ๐ถ = 0) โ ๐ถ โ
โ+) |
60 | | simpr 486 |
. . . . . . . . . . . 12
โข ((๐ถ โ โ+
โง ๐ฆ โ
โ+) โ ๐ฆ โ โ+) |
61 | | simpl 484 |
. . . . . . . . . . . 12
โข ((๐ถ โ โ+
โง ๐ฆ โ
โ+) โ ๐ถ โ
โ+) |
62 | 60, 61 | rpdivcld 12979 |
. . . . . . . . . . 11
โข ((๐ถ โ โ+
โง ๐ฆ โ
โ+) โ (๐ฆ / ๐ถ) โ
โ+) |
63 | 62 | adantll 713 |
. . . . . . . . . 10
โข
(((โ๐ฅ โ
โ+ ๐ด โค
(๐ต + (๐ถ ยท ๐ฅ)) โง ๐ถ โ โ+) โง ๐ฆ โ โ+)
โ (๐ฆ / ๐ถ) โ
โ+) |
64 | | simpll 766 |
. . . . . . . . . 10
โข
(((โ๐ฅ โ
โ+ ๐ด โค
(๐ต + (๐ถ ยท ๐ฅ)) โง ๐ถ โ โ+) โง ๐ฆ โ โ+)
โ โ๐ฅ โ
โ+ ๐ด โค
(๐ต + (๐ถ ยท ๐ฅ))) |
65 | | oveq2 7366 |
. . . . . . . . . . . . 13
โข (๐ฅ = (๐ฆ / ๐ถ) โ (๐ถ ยท ๐ฅ) = (๐ถ ยท (๐ฆ / ๐ถ))) |
66 | 65 | oveq2d 7374 |
. . . . . . . . . . . 12
โข (๐ฅ = (๐ฆ / ๐ถ) โ (๐ต + (๐ถ ยท ๐ฅ)) = (๐ต + (๐ถ ยท (๐ฆ / ๐ถ)))) |
67 | 66 | breq2d 5118 |
. . . . . . . . . . 11
โข (๐ฅ = (๐ฆ / ๐ถ) โ (๐ด โค (๐ต + (๐ถ ยท ๐ฅ)) โ ๐ด โค (๐ต + (๐ถ ยท (๐ฆ / ๐ถ))))) |
68 | 67 | rspcva 3578 |
. . . . . . . . . 10
โข (((๐ฆ / ๐ถ) โ โ+ โง
โ๐ฅ โ
โ+ ๐ด โค
(๐ต + (๐ถ ยท ๐ฅ))) โ ๐ด โค (๐ต + (๐ถ ยท (๐ฆ / ๐ถ)))) |
69 | 63, 64, 68 | syl2anc 585 |
. . . . . . . . 9
โข
(((โ๐ฅ โ
โ+ ๐ด โค
(๐ต + (๐ถ ยท ๐ฅ)) โง ๐ถ โ โ+) โง ๐ฆ โ โ+)
โ ๐ด โค (๐ต + (๐ถ ยท (๐ฆ / ๐ถ)))) |
70 | 69 | adantlll 717 |
. . . . . . . 8
โข ((((๐ โง โ๐ฅ โ โ+ ๐ด โค (๐ต + (๐ถ ยท ๐ฅ))) โง ๐ถ โ โ+) โง ๐ฆ โ โ+)
โ ๐ด โค (๐ต + (๐ถ ยท (๐ฆ / ๐ถ)))) |
71 | 60 | rpcnd 12964 |
. . . . . . . . . . 11
โข ((๐ถ โ โ+
โง ๐ฆ โ
โ+) โ ๐ฆ โ โ) |
72 | 61 | rpcnd 12964 |
. . . . . . . . . . 11
โข ((๐ถ โ โ+
โง ๐ฆ โ
โ+) โ ๐ถ โ โ) |
73 | 61 | rpne0d 12967 |
. . . . . . . . . . 11
โข ((๐ถ โ โ+
โง ๐ฆ โ
โ+) โ ๐ถ โ 0) |
74 | 71, 72, 73 | divcan2d 11938 |
. . . . . . . . . 10
โข ((๐ถ โ โ+
โง ๐ฆ โ
โ+) โ (๐ถ ยท (๐ฆ / ๐ถ)) = ๐ฆ) |
75 | 74 | adantll 713 |
. . . . . . . . 9
โข ((((๐ โง โ๐ฅ โ โ+ ๐ด โค (๐ต + (๐ถ ยท ๐ฅ))) โง ๐ถ โ โ+) โง ๐ฆ โ โ+)
โ (๐ถ ยท (๐ฆ / ๐ถ)) = ๐ฆ) |
76 | 75 | oveq2d 7374 |
. . . . . . . 8
โข ((((๐ โง โ๐ฅ โ โ+ ๐ด โค (๐ต + (๐ถ ยท ๐ฅ))) โง ๐ถ โ โ+) โง ๐ฆ โ โ+)
โ (๐ต + (๐ถ ยท (๐ฆ / ๐ถ))) = (๐ต + ๐ฆ)) |
77 | 70, 76 | breqtrd 5132 |
. . . . . . 7
โข ((((๐ โง โ๐ฅ โ โ+ ๐ด โค (๐ต + (๐ถ ยท ๐ฅ))) โง ๐ถ โ โ+) โง ๐ฆ โ โ+)
โ ๐ด โค (๐ต + ๐ฆ)) |
78 | 77 | ralrimiva 3140 |
. . . . . 6
โข (((๐ โง โ๐ฅ โ โ+ ๐ด โค (๐ต + (๐ถ ยท ๐ฅ))) โง ๐ถ โ โ+) โ
โ๐ฆ โ
โ+ ๐ด โค
(๐ต + ๐ฆ)) |
79 | | xralrple 13130 |
. . . . . . . 8
โข ((๐ด โ โ*
โง ๐ต โ โ)
โ (๐ด โค ๐ต โ โ๐ฆ โ โ+
๐ด โค (๐ต + ๐ฆ))) |
80 | 1, 3, 79 | syl2anc 585 |
. . . . . . 7
โข (๐ โ (๐ด โค ๐ต โ โ๐ฆ โ โ+ ๐ด โค (๐ต + ๐ฆ))) |
81 | 80 | ad2antrr 725 |
. . . . . 6
โข (((๐ โง โ๐ฅ โ โ+ ๐ด โค (๐ต + (๐ถ ยท ๐ฅ))) โง ๐ถ โ โ+) โ (๐ด โค ๐ต โ โ๐ฆ โ โ+ ๐ด โค (๐ต + ๐ฆ))) |
82 | 78, 81 | mpbird 257 |
. . . . 5
โข (((๐ โง โ๐ฅ โ โ+ ๐ด โค (๐ต + (๐ถ ยท ๐ฅ))) โง ๐ถ โ โ+) โ ๐ด โค ๐ต) |
83 | 59, 82 | syldan 592 |
. . . 4
โข (((๐ โง โ๐ฅ โ โ+ ๐ด โค (๐ต + (๐ถ ยท ๐ฅ))) โง ยฌ ๐ถ = 0) โ ๐ด โค ๐ต) |
84 | 49, 83 | pm2.61dan 812 |
. . 3
โข ((๐ โง โ๐ฅ โ โ+ ๐ด โค (๐ต + (๐ถ ยท ๐ฅ))) โ ๐ด โค ๐ต) |
85 | 84 | ex 414 |
. 2
โข (๐ โ (โ๐ฅ โ โ+
๐ด โค (๐ต + (๐ถ ยท ๐ฅ)) โ ๐ด โค ๐ต)) |
86 | 29, 85 | impbid 211 |
1
โข (๐ โ (๐ด โค ๐ต โ โ๐ฅ โ โ+ ๐ด โค (๐ต + (๐ถ ยท ๐ฅ)))) |