Step | Hyp | Ref
| Expression |
1 | | lo1add.3 |
. 2
โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ต) โ โค๐(1)) |
2 | | lo1add.4 |
. 2
โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ถ) โ โค๐(1)) |
3 | | reeanv 3216 |
. . . 4
โข
(โ๐ โ
โ โ๐ โ
โ (โ๐ โ
โ โ๐ฅ โ
๐ด (๐ โค ๐ฅ โ ๐ต โค ๐) โง โ๐ โ โ โ๐ฅ โ ๐ด (๐ โค ๐ฅ โ ๐ถ โค ๐)) โ (โ๐ โ โ โ๐ โ โ โ๐ฅ โ ๐ด (๐ โค ๐ฅ โ ๐ต โค ๐) โง โ๐ โ โ โ๐ โ โ โ๐ฅ โ ๐ด (๐ โค ๐ฅ โ ๐ถ โค ๐))) |
4 | | o1add2.1 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ ๐) |
5 | 4 | ralrimiva 3140 |
. . . . . . . . . 10
โข (๐ โ โ๐ฅ โ ๐ด ๐ต โ ๐) |
6 | | dmmptg 6195 |
. . . . . . . . . 10
โข
(โ๐ฅ โ
๐ด ๐ต โ ๐ โ dom (๐ฅ โ ๐ด โฆ ๐ต) = ๐ด) |
7 | 5, 6 | syl 17 |
. . . . . . . . 9
โข (๐ โ dom (๐ฅ โ ๐ด โฆ ๐ต) = ๐ด) |
8 | | lo1dm 15407 |
. . . . . . . . . 10
โข ((๐ฅ โ ๐ด โฆ ๐ต) โ โค๐(1) โ dom (๐ฅ โ ๐ด โฆ ๐ต) โ โ) |
9 | 1, 8 | syl 17 |
. . . . . . . . 9
โข (๐ โ dom (๐ฅ โ ๐ด โฆ ๐ต) โ โ) |
10 | 7, 9 | eqsstrrd 3984 |
. . . . . . . 8
โข (๐ โ ๐ด โ โ) |
11 | 10 | adantr 482 |
. . . . . . 7
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ ๐ด โ โ) |
12 | | rexanre 15237 |
. . . . . . 7
โข (๐ด โ โ โ
(โ๐ โ โ
โ๐ฅ โ ๐ด (๐ โค ๐ฅ โ (๐ต โค ๐ โง ๐ถ โค ๐)) โ (โ๐ โ โ โ๐ฅ โ ๐ด (๐ โค ๐ฅ โ ๐ต โค ๐) โง โ๐ โ โ โ๐ฅ โ ๐ด (๐ โค ๐ฅ โ ๐ถ โค ๐)))) |
13 | 11, 12 | syl 17 |
. . . . . 6
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ (โ๐ โ โ โ๐ฅ โ ๐ด (๐ โค ๐ฅ โ (๐ต โค ๐ โง ๐ถ โค ๐)) โ (โ๐ โ โ โ๐ฅ โ ๐ด (๐ โค ๐ฅ โ ๐ต โค ๐) โง โ๐ โ โ โ๐ฅ โ ๐ด (๐ โค ๐ฅ โ ๐ถ โค ๐)))) |
14 | | simprl 770 |
. . . . . . . . 9
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ ๐ โ โ) |
15 | | simprr 772 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ ๐ โ โ) |
16 | | 0re 11162 |
. . . . . . . . . 10
โข 0 โ
โ |
17 | | ifcl 4532 |
. . . . . . . . . 10
โข ((๐ โ โ โง 0 โ
โ) โ if(0 โค ๐, ๐, 0) โ โ) |
18 | 15, 16, 17 | sylancl 587 |
. . . . . . . . 9
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ if(0 โค ๐, ๐, 0) โ โ) |
19 | 14, 18 | remulcld 11190 |
. . . . . . . 8
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ (๐ ยท if(0 โค ๐, ๐, 0)) โ โ) |
20 | | simplrr 777 |
. . . . . . . . . . . . 13
โข (((๐ โง (๐ โ โ โง ๐ โ โ)) โง ๐ฅ โ ๐ด) โ ๐ โ โ) |
21 | | max2 13112 |
. . . . . . . . . . . . 13
โข ((0
โ โ โง ๐
โ โ) โ ๐
โค if(0 โค ๐, ๐, 0)) |
22 | 16, 20, 21 | sylancr 588 |
. . . . . . . . . . . 12
โข (((๐ โง (๐ โ โ โง ๐ โ โ)) โง ๐ฅ โ ๐ด) โ ๐ โค if(0 โค ๐, ๐, 0)) |
23 | | o1add2.2 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ถ โ ๐) |
24 | 23, 2 | lo1mptrcl 15510 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ถ โ โ) |
25 | 24 | adantlr 714 |
. . . . . . . . . . . . 13
โข (((๐ โง (๐ โ โ โง ๐ โ โ)) โง ๐ฅ โ ๐ด) โ ๐ถ โ โ) |
26 | 20, 16, 17 | sylancl 587 |
. . . . . . . . . . . . 13
โข (((๐ โง (๐ โ โ โง ๐ โ โ)) โง ๐ฅ โ ๐ด) โ if(0 โค ๐, ๐, 0) โ โ) |
27 | | letr 11254 |
. . . . . . . . . . . . 13
โข ((๐ถ โ โ โง ๐ โ โ โง if(0 โค
๐, ๐, 0) โ โ) โ ((๐ถ โค ๐ โง ๐ โค if(0 โค ๐, ๐, 0)) โ ๐ถ โค if(0 โค ๐, ๐, 0))) |
28 | 25, 20, 26, 27 | syl3anc 1372 |
. . . . . . . . . . . 12
โข (((๐ โง (๐ โ โ โง ๐ โ โ)) โง ๐ฅ โ ๐ด) โ ((๐ถ โค ๐ โง ๐ โค if(0 โค ๐, ๐, 0)) โ ๐ถ โค if(0 โค ๐, ๐, 0))) |
29 | 22, 28 | mpan2d 693 |
. . . . . . . . . . 11
โข (((๐ โง (๐ โ โ โง ๐ โ โ)) โง ๐ฅ โ ๐ด) โ (๐ถ โค ๐ โ ๐ถ โค if(0 โค ๐, ๐, 0))) |
30 | 4, 1 | lo1mptrcl 15510 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ โ) |
31 | 30 | adantlr 714 |
. . . . . . . . . . . . 13
โข (((๐ โง (๐ โ โ โง ๐ โ โ)) โง ๐ฅ โ ๐ด) โ ๐ต โ โ) |
32 | | lo1mul.5 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ฅ โ ๐ด) โ 0 โค ๐ต) |
33 | 32 | adantlr 714 |
. . . . . . . . . . . . 13
โข (((๐ โง (๐ โ โ โง ๐ โ โ)) โง ๐ฅ โ ๐ด) โ 0 โค ๐ต) |
34 | 31, 33 | jca 513 |
. . . . . . . . . . . 12
โข (((๐ โง (๐ โ โ โง ๐ โ โ)) โง ๐ฅ โ ๐ด) โ (๐ต โ โ โง 0 โค ๐ต)) |
35 | | simplrl 776 |
. . . . . . . . . . . 12
โข (((๐ โง (๐ โ โ โง ๐ โ โ)) โง ๐ฅ โ ๐ด) โ ๐ โ โ) |
36 | | max1 13110 |
. . . . . . . . . . . . . 14
โข ((0
โ โ โง ๐
โ โ) โ 0 โค if(0 โค ๐, ๐, 0)) |
37 | 16, 20, 36 | sylancr 588 |
. . . . . . . . . . . . 13
โข (((๐ โง (๐ โ โ โง ๐ โ โ)) โง ๐ฅ โ ๐ด) โ 0 โค if(0 โค ๐, ๐, 0)) |
38 | 26, 37 | jca 513 |
. . . . . . . . . . . 12
โข (((๐ โง (๐ โ โ โง ๐ โ โ)) โง ๐ฅ โ ๐ด) โ (if(0 โค ๐, ๐, 0) โ โ โง 0 โค if(0 โค
๐, ๐, 0))) |
39 | | lemul12b 12017 |
. . . . . . . . . . . 12
โข ((((๐ต โ โ โง 0 โค
๐ต) โง ๐ โ โ) โง (๐ถ โ โ โง (if(0 โค ๐, ๐, 0) โ โ โง 0 โค if(0 โค
๐, ๐, 0)))) โ ((๐ต โค ๐ โง ๐ถ โค if(0 โค ๐, ๐, 0)) โ (๐ต ยท ๐ถ) โค (๐ ยท if(0 โค ๐, ๐, 0)))) |
40 | 34, 35, 25, 38, 39 | syl22anc 838 |
. . . . . . . . . . 11
โข (((๐ โง (๐ โ โ โง ๐ โ โ)) โง ๐ฅ โ ๐ด) โ ((๐ต โค ๐ โง ๐ถ โค if(0 โค ๐, ๐, 0)) โ (๐ต ยท ๐ถ) โค (๐ ยท if(0 โค ๐, ๐, 0)))) |
41 | 29, 40 | sylan2d 606 |
. . . . . . . . . 10
โข (((๐ โง (๐ โ โ โง ๐ โ โ)) โง ๐ฅ โ ๐ด) โ ((๐ต โค ๐ โง ๐ถ โค ๐) โ (๐ต ยท ๐ถ) โค (๐ ยท if(0 โค ๐, ๐, 0)))) |
42 | 41 | imim2d 57 |
. . . . . . . . 9
โข (((๐ โง (๐ โ โ โง ๐ โ โ)) โง ๐ฅ โ ๐ด) โ ((๐ โค ๐ฅ โ (๐ต โค ๐ โง ๐ถ โค ๐)) โ (๐ โค ๐ฅ โ (๐ต ยท ๐ถ) โค (๐ ยท if(0 โค ๐, ๐, 0))))) |
43 | 42 | ralimdva 3161 |
. . . . . . . 8
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ (โ๐ฅ โ ๐ด (๐ โค ๐ฅ โ (๐ต โค ๐ โง ๐ถ โค ๐)) โ โ๐ฅ โ ๐ด (๐ โค ๐ฅ โ (๐ต ยท ๐ถ) โค (๐ ยท if(0 โค ๐, ๐, 0))))) |
44 | | breq2 5110 |
. . . . . . . . . . 11
โข (๐ = (๐ ยท if(0 โค ๐, ๐, 0)) โ ((๐ต ยท ๐ถ) โค ๐ โ (๐ต ยท ๐ถ) โค (๐ ยท if(0 โค ๐, ๐, 0)))) |
45 | 44 | imbi2d 341 |
. . . . . . . . . 10
โข (๐ = (๐ ยท if(0 โค ๐, ๐, 0)) โ ((๐ โค ๐ฅ โ (๐ต ยท ๐ถ) โค ๐) โ (๐ โค ๐ฅ โ (๐ต ยท ๐ถ) โค (๐ ยท if(0 โค ๐, ๐, 0))))) |
46 | 45 | ralbidv 3171 |
. . . . . . . . 9
โข (๐ = (๐ ยท if(0 โค ๐, ๐, 0)) โ (โ๐ฅ โ ๐ด (๐ โค ๐ฅ โ (๐ต ยท ๐ถ) โค ๐) โ โ๐ฅ โ ๐ด (๐ โค ๐ฅ โ (๐ต ยท ๐ถ) โค (๐ ยท if(0 โค ๐, ๐, 0))))) |
47 | 46 | rspcev 3580 |
. . . . . . . 8
โข (((๐ ยท if(0 โค ๐, ๐, 0)) โ โ โง โ๐ฅ โ ๐ด (๐ โค ๐ฅ โ (๐ต ยท ๐ถ) โค (๐ ยท if(0 โค ๐, ๐, 0)))) โ โ๐ โ โ โ๐ฅ โ ๐ด (๐ โค ๐ฅ โ (๐ต ยท ๐ถ) โค ๐)) |
48 | 19, 43, 47 | syl6an 683 |
. . . . . . 7
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ (โ๐ฅ โ ๐ด (๐ โค ๐ฅ โ (๐ต โค ๐ โง ๐ถ โค ๐)) โ โ๐ โ โ โ๐ฅ โ ๐ด (๐ โค ๐ฅ โ (๐ต ยท ๐ถ) โค ๐))) |
49 | 48 | reximdv 3164 |
. . . . . 6
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ (โ๐ โ โ โ๐ฅ โ ๐ด (๐ โค ๐ฅ โ (๐ต โค ๐ โง ๐ถ โค ๐)) โ โ๐ โ โ โ๐ โ โ โ๐ฅ โ ๐ด (๐ โค ๐ฅ โ (๐ต ยท ๐ถ) โค ๐))) |
50 | 13, 49 | sylbird 260 |
. . . . 5
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ ((โ๐ โ โ โ๐ฅ โ ๐ด (๐ โค ๐ฅ โ ๐ต โค ๐) โง โ๐ โ โ โ๐ฅ โ ๐ด (๐ โค ๐ฅ โ ๐ถ โค ๐)) โ โ๐ โ โ โ๐ โ โ โ๐ฅ โ ๐ด (๐ โค ๐ฅ โ (๐ต ยท ๐ถ) โค ๐))) |
51 | 50 | rexlimdvva 3202 |
. . . 4
โข (๐ โ (โ๐ โ โ โ๐ โ โ (โ๐ โ โ โ๐ฅ โ ๐ด (๐ โค ๐ฅ โ ๐ต โค ๐) โง โ๐ โ โ โ๐ฅ โ ๐ด (๐ โค ๐ฅ โ ๐ถ โค ๐)) โ โ๐ โ โ โ๐ โ โ โ๐ฅ โ ๐ด (๐ โค ๐ฅ โ (๐ต ยท ๐ถ) โค ๐))) |
52 | 3, 51 | biimtrrid 242 |
. . 3
โข (๐ โ ((โ๐ โ โ โ๐ โ โ โ๐ฅ โ ๐ด (๐ โค ๐ฅ โ ๐ต โค ๐) โง โ๐ โ โ โ๐ โ โ โ๐ฅ โ ๐ด (๐ โค ๐ฅ โ ๐ถ โค ๐)) โ โ๐ โ โ โ๐ โ โ โ๐ฅ โ ๐ด (๐ โค ๐ฅ โ (๐ต ยท ๐ถ) โค ๐))) |
53 | 10, 30 | ello1mpt 15409 |
. . . . 5
โข (๐ โ ((๐ฅ โ ๐ด โฆ ๐ต) โ โค๐(1) โ
โ๐ โ โ
โ๐ โ โ
โ๐ฅ โ ๐ด (๐ โค ๐ฅ โ ๐ต โค ๐))) |
54 | | rexcom 3272 |
. . . . 5
โข
(โ๐ โ
โ โ๐ โ
โ โ๐ฅ โ
๐ด (๐ โค ๐ฅ โ ๐ต โค ๐) โ โ๐ โ โ โ๐ โ โ โ๐ฅ โ ๐ด (๐ โค ๐ฅ โ ๐ต โค ๐)) |
55 | 53, 54 | bitrdi 287 |
. . . 4
โข (๐ โ ((๐ฅ โ ๐ด โฆ ๐ต) โ โค๐(1) โ
โ๐ โ โ
โ๐ โ โ
โ๐ฅ โ ๐ด (๐ โค ๐ฅ โ ๐ต โค ๐))) |
56 | 10, 24 | ello1mpt 15409 |
. . . . 5
โข (๐ โ ((๐ฅ โ ๐ด โฆ ๐ถ) โ โค๐(1) โ
โ๐ โ โ
โ๐ โ โ
โ๐ฅ โ ๐ด (๐ โค ๐ฅ โ ๐ถ โค ๐))) |
57 | | rexcom 3272 |
. . . . 5
โข
(โ๐ โ
โ โ๐ โ
โ โ๐ฅ โ
๐ด (๐ โค ๐ฅ โ ๐ถ โค ๐) โ โ๐ โ โ โ๐ โ โ โ๐ฅ โ ๐ด (๐ โค ๐ฅ โ ๐ถ โค ๐)) |
58 | 56, 57 | bitrdi 287 |
. . . 4
โข (๐ โ ((๐ฅ โ ๐ด โฆ ๐ถ) โ โค๐(1) โ
โ๐ โ โ
โ๐ โ โ
โ๐ฅ โ ๐ด (๐ โค ๐ฅ โ ๐ถ โค ๐))) |
59 | 55, 58 | anbi12d 632 |
. . 3
โข (๐ โ (((๐ฅ โ ๐ด โฆ ๐ต) โ โค๐(1) โง (๐ฅ โ ๐ด โฆ ๐ถ) โ โค๐(1)) โ
(โ๐ โ โ
โ๐ โ โ
โ๐ฅ โ ๐ด (๐ โค ๐ฅ โ ๐ต โค ๐) โง โ๐ โ โ โ๐ โ โ โ๐ฅ โ ๐ด (๐ โค ๐ฅ โ ๐ถ โค ๐)))) |
60 | 30, 24 | remulcld 11190 |
. . . 4
โข ((๐ โง ๐ฅ โ ๐ด) โ (๐ต ยท ๐ถ) โ โ) |
61 | 10, 60 | ello1mpt 15409 |
. . 3
โข (๐ โ ((๐ฅ โ ๐ด โฆ (๐ต ยท ๐ถ)) โ โค๐(1) โ
โ๐ โ โ
โ๐ โ โ
โ๐ฅ โ ๐ด (๐ โค ๐ฅ โ (๐ต ยท ๐ถ) โค ๐))) |
62 | 52, 59, 61 | 3imtr4d 294 |
. 2
โข (๐ โ (((๐ฅ โ ๐ด โฆ ๐ต) โ โค๐(1) โง (๐ฅ โ ๐ด โฆ ๐ถ) โ โค๐(1)) โ (๐ฅ โ ๐ด โฆ (๐ต ยท ๐ถ)) โ
โค๐(1))) |
63 | 1, 2, 62 | mp2and 698 |
1
โข (๐ โ (๐ฅ โ ๐ด โฆ (๐ต ยท ๐ถ)) โ โค๐(1)) |