Step | Hyp | Ref
| Expression |
1 | | itgsubst.x |
. . 3
โข (๐ โ ๐ โ โ) |
2 | | itgsubst.y |
. . 3
โข (๐ โ ๐ โ โ) |
3 | | itgsubst.le |
. . 3
โข (๐ โ ๐ โค ๐) |
4 | | ioossre 13331 |
. . . . 5
โข (๐(,)๐) โ โ |
5 | | ax-resscn 11113 |
. . . . 5
โข โ
โ โ |
6 | | cncfss 24278 |
. . . . 5
โข (((๐(,)๐) โ โ โง โ โ
โ) โ ((๐[,]๐)โcnโ(๐(,)๐)) โ ((๐[,]๐)โcnโโ)) |
7 | 4, 5, 6 | mp2an 691 |
. . . 4
โข ((๐[,]๐)โcnโ(๐(,)๐)) โ ((๐[,]๐)โcnโโ) |
8 | | itgsubst.a |
. . . 4
โข (๐ โ (๐ฅ โ (๐[,]๐) โฆ ๐ด) โ ((๐[,]๐)โcnโ(๐(,)๐))) |
9 | 7, 8 | sselid 3943 |
. . 3
โข (๐ โ (๐ฅ โ (๐[,]๐) โฆ ๐ด) โ ((๐[,]๐)โcnโโ)) |
10 | 1, 2, 3, 9 | evthicc 24839 |
. 2
โข (๐ โ (โ๐ฆ โ (๐[,]๐)โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) โง โ๐ฆ โ (๐[,]๐)โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง))) |
11 | | ressxr 11204 |
. . . . . . . 8
โข โ
โ โ* |
12 | 4, 11 | sstri 3954 |
. . . . . . 7
โข (๐(,)๐) โ
โ* |
13 | | cncff 24272 |
. . . . . . . . . 10
โข ((๐ฅ โ (๐[,]๐) โฆ ๐ด) โ ((๐[,]๐)โcnโ(๐(,)๐)) โ (๐ฅ โ (๐[,]๐) โฆ ๐ด):(๐[,]๐)โถ(๐(,)๐)) |
14 | 8, 13 | syl 17 |
. . . . . . . . 9
โข (๐ โ (๐ฅ โ (๐[,]๐) โฆ ๐ด):(๐[,]๐)โถ(๐(,)๐)) |
15 | 14 | adantr 482 |
. . . . . . . 8
โข ((๐ โง (๐ฆ โ (๐[,]๐) โง โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ))) โ (๐ฅ โ (๐[,]๐) โฆ ๐ด):(๐[,]๐)โถ(๐(,)๐)) |
16 | | simprl 770 |
. . . . . . . 8
โข ((๐ โง (๐ฆ โ (๐[,]๐) โง โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ))) โ ๐ฆ โ (๐[,]๐)) |
17 | 15, 16 | ffvelcdmd 7037 |
. . . . . . 7
โข ((๐ โง (๐ฆ โ (๐[,]๐) โง โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ))) โ ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) โ (๐(,)๐)) |
18 | 12, 17 | sselid 3943 |
. . . . . 6
โข ((๐ โง (๐ฆ โ (๐[,]๐) โง โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ))) โ ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) โ
โ*) |
19 | | itgsubst.w |
. . . . . . 7
โข (๐ โ ๐ โ
โ*) |
20 | 19 | adantr 482 |
. . . . . 6
โข ((๐ โง (๐ฆ โ (๐[,]๐) โง โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ))) โ ๐ โ
โ*) |
21 | | eliooord 13329 |
. . . . . . . 8
โข (((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) โ (๐(,)๐) โ (๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) โง ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) < ๐)) |
22 | 17, 21 | syl 17 |
. . . . . . 7
โข ((๐ โง (๐ฆ โ (๐[,]๐) โง โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ))) โ (๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) โง ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) < ๐)) |
23 | 22 | simprd 497 |
. . . . . 6
โข ((๐ โง (๐ฆ โ (๐[,]๐) โง โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ))) โ ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) < ๐) |
24 | | qbtwnxr 13125 |
. . . . . 6
โข ((((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) โ โ* โง ๐ โ โ*
โง ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) < ๐) โ โ๐ โ โ (((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) < ๐ โง ๐ < ๐)) |
25 | 18, 20, 23, 24 | syl3anc 1372 |
. . . . 5
โข ((๐ โง (๐ฆ โ (๐[,]๐) โง โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ))) โ โ๐ โ โ (((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) < ๐ โง ๐ < ๐)) |
26 | | qre 12883 |
. . . . . . 7
โข (๐ โ โ โ ๐ โ
โ) |
27 | 26 | ad2antrl 727 |
. . . . . 6
โข (((๐ โง (๐ฆ โ (๐[,]๐) โง โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ))) โง (๐ โ โ โง (((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) < ๐ โง ๐ < ๐))) โ ๐ โ โ) |
28 | | itgsubst.z |
. . . . . . . 8
โข (๐ โ ๐ โ
โ*) |
29 | 28 | ad2antrr 725 |
. . . . . . 7
โข (((๐ โง (๐ฆ โ (๐[,]๐) โง โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ))) โง (๐ โ โ โง (((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) < ๐ โง ๐ < ๐))) โ ๐ โ
โ*) |
30 | 18 | adantr 482 |
. . . . . . 7
โข (((๐ โง (๐ฆ โ (๐[,]๐) โง โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ))) โง (๐ โ โ โง (((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) < ๐ โง ๐ < ๐))) โ ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) โ
โ*) |
31 | 27 | rexrd 11210 |
. . . . . . 7
โข (((๐ โง (๐ฆ โ (๐[,]๐) โง โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ))) โง (๐ โ โ โง (((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) < ๐ โง ๐ < ๐))) โ ๐ โ โ*) |
32 | 22 | simpld 496 |
. . . . . . . 8
โข ((๐ โง (๐ฆ โ (๐[,]๐) โง โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ))) โ ๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ)) |
33 | 32 | adantr 482 |
. . . . . . 7
โข (((๐ โง (๐ฆ โ (๐[,]๐) โง โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ))) โง (๐ โ โ โง (((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) < ๐ โง ๐ < ๐))) โ ๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ)) |
34 | | simprrl 780 |
. . . . . . 7
โข (((๐ โง (๐ฆ โ (๐[,]๐) โง โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ))) โง (๐ โ โ โง (((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) < ๐ โง ๐ < ๐))) โ ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) < ๐) |
35 | 29, 30, 31, 33, 34 | xrlttrd 13084 |
. . . . . 6
โข (((๐ โง (๐ฆ โ (๐[,]๐) โง โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ))) โง (๐ โ โ โง (((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) < ๐ โง ๐ < ๐))) โ ๐ < ๐) |
36 | | simprrr 781 |
. . . . . 6
โข (((๐ โง (๐ฆ โ (๐[,]๐) โง โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ))) โง (๐ โ โ โง (((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) < ๐ โง ๐ < ๐))) โ ๐ < ๐) |
37 | 19 | ad2antrr 725 |
. . . . . . 7
โข (((๐ โง (๐ฆ โ (๐[,]๐) โง โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ))) โง (๐ โ โ โง (((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) < ๐ โง ๐ < ๐))) โ ๐ โ
โ*) |
38 | | elioo2 13311 |
. . . . . . 7
โข ((๐ โ โ*
โง ๐ โ
โ*) โ (๐ โ (๐(,)๐) โ (๐ โ โ โง ๐ < ๐ โง ๐ < ๐))) |
39 | 29, 37, 38 | syl2anc 585 |
. . . . . 6
โข (((๐ โง (๐ฆ โ (๐[,]๐) โง โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ))) โง (๐ โ โ โง (((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) < ๐ โง ๐ < ๐))) โ (๐ โ (๐(,)๐) โ (๐ โ โ โง ๐ < ๐ โง ๐ < ๐))) |
40 | 27, 35, 36, 39 | mpbir3and 1343 |
. . . . 5
โข (((๐ โง (๐ฆ โ (๐[,]๐) โง โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ))) โง (๐ โ โ โง (((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) < ๐ โง ๐ < ๐))) โ ๐ โ (๐(,)๐)) |
41 | | anass 470 |
. . . . . 6
โข (((๐ โง ๐ฆ โ (๐[,]๐)) โง โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ)) โ (๐ โง (๐ฆ โ (๐[,]๐) โง โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ)))) |
42 | | simprrl 780 |
. . . . . . . . . . 11
โข (((๐ โง ๐ฆ โ (๐[,]๐)) โง (๐ โ โ โง (((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) < ๐ โง ๐ < ๐))) โ ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) < ๐) |
43 | 42 | adantr 482 |
. . . . . . . . . 10
โข ((((๐ โง ๐ฆ โ (๐[,]๐)) โง (๐ โ โ โง (((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) < ๐ โง ๐ < ๐))) โง ๐ง โ (๐[,]๐)) โ ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) < ๐) |
44 | 14 | ad2antrr 725 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ฆ โ (๐[,]๐)) โง (๐ โ โ โง (((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) < ๐ โง ๐ < ๐))) โ (๐ฅ โ (๐[,]๐) โฆ ๐ด):(๐[,]๐)โถ(๐(,)๐)) |
45 | 44 | ffvelcdmda 7036 |
. . . . . . . . . . . 12
โข ((((๐ โง ๐ฆ โ (๐[,]๐)) โง (๐ โ โ โง (((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) < ๐ โง ๐ < ๐))) โง ๐ง โ (๐[,]๐)) โ ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โ (๐(,)๐)) |
46 | 12, 45 | sselid 3943 |
. . . . . . . . . . 11
โข ((((๐ โง ๐ฆ โ (๐[,]๐)) โง (๐ โ โ โง (((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) < ๐ โง ๐ < ๐))) โง ๐ง โ (๐[,]๐)) โ ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โ
โ*) |
47 | | simplr 768 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ฆ โ (๐[,]๐)) โง (๐ โ โ โง (((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) < ๐ โง ๐ < ๐))) โ ๐ฆ โ (๐[,]๐)) |
48 | 44, 47 | ffvelcdmd 7037 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ฆ โ (๐[,]๐)) โง (๐ โ โ โง (((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) < ๐ โง ๐ < ๐))) โ ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) โ (๐(,)๐)) |
49 | 12, 48 | sselid 3943 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ฆ โ (๐[,]๐)) โง (๐ โ โ โง (((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) < ๐ โง ๐ < ๐))) โ ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) โ
โ*) |
50 | 49 | adantr 482 |
. . . . . . . . . . 11
โข ((((๐ โง ๐ฆ โ (๐[,]๐)) โง (๐ โ โ โง (((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) < ๐ โง ๐ < ๐))) โง ๐ง โ (๐[,]๐)) โ ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) โ
โ*) |
51 | 26 | ad2antrl 727 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ฆ โ (๐[,]๐)) โง (๐ โ โ โง (((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) < ๐ โง ๐ < ๐))) โ ๐ โ โ) |
52 | 51 | adantr 482 |
. . . . . . . . . . . 12
โข ((((๐ โง ๐ฆ โ (๐[,]๐)) โง (๐ โ โ โง (((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) < ๐ โง ๐ < ๐))) โง ๐ง โ (๐[,]๐)) โ ๐ โ โ) |
53 | 52 | rexrd 11210 |
. . . . . . . . . . 11
โข ((((๐ โง ๐ฆ โ (๐[,]๐)) โง (๐ โ โ โง (((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) < ๐ โง ๐ < ๐))) โง ๐ง โ (๐[,]๐)) โ ๐ โ โ*) |
54 | | xrlelttr 13081 |
. . . . . . . . . . 11
โข ((((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โ โ* โง ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) โ โ* โง ๐ โ โ*)
โ ((((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) โง ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) < ๐) โ ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) < ๐)) |
55 | 46, 50, 53, 54 | syl3anc 1372 |
. . . . . . . . . 10
โข ((((๐ โง ๐ฆ โ (๐[,]๐)) โง (๐ โ โ โง (((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) < ๐ โง ๐ < ๐))) โง ๐ง โ (๐[,]๐)) โ ((((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) โง ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) < ๐) โ ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) < ๐)) |
56 | 43, 55 | mpan2d 693 |
. . . . . . . . 9
โข ((((๐ โง ๐ฆ โ (๐[,]๐)) โง (๐ โ โ โง (((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) < ๐ โง ๐ < ๐))) โง ๐ง โ (๐[,]๐)) โ (((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) โ ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) < ๐)) |
57 | 56 | ralimdva 3161 |
. . . . . . . 8
โข (((๐ โง ๐ฆ โ (๐[,]๐)) โง (๐ โ โ โง (((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) < ๐ โง ๐ < ๐))) โ (โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) โ โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) < ๐)) |
58 | 57 | imp 408 |
. . . . . . 7
โข ((((๐ โง ๐ฆ โ (๐[,]๐)) โง (๐ โ โ โง (((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) < ๐ โง ๐ < ๐))) โง โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ)) โ โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) < ๐) |
59 | 58 | an32s 651 |
. . . . . 6
โข ((((๐ โง ๐ฆ โ (๐[,]๐)) โง โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ)) โง (๐ โ โ โง (((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) < ๐ โง ๐ < ๐))) โ โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) < ๐) |
60 | 41, 59 | sylanbr 583 |
. . . . 5
โข (((๐ โง (๐ฆ โ (๐[,]๐) โง โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ))) โง (๐ โ โ โง (((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) < ๐ โง ๐ < ๐))) โ โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) < ๐) |
61 | 25, 40, 60 | reximssdv 3166 |
. . . 4
โข ((๐ โง (๐ฆ โ (๐[,]๐) โง โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ))) โ โ๐ โ (๐(,)๐)โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) < ๐) |
62 | 61 | rexlimdvaa 3150 |
. . 3
โข (๐ โ (โ๐ฆ โ (๐[,]๐)โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) โ โ๐ โ (๐(,)๐)โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) < ๐)) |
63 | 28 | adantr 482 |
. . . . . 6
โข ((๐ โง (๐ฆ โ (๐[,]๐) โง โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง))) โ ๐ โ
โ*) |
64 | 14 | adantr 482 |
. . . . . . . 8
โข ((๐ โง (๐ฆ โ (๐[,]๐) โง โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง))) โ (๐ฅ โ (๐[,]๐) โฆ ๐ด):(๐[,]๐)โถ(๐(,)๐)) |
65 | | simprl 770 |
. . . . . . . 8
โข ((๐ โง (๐ฆ โ (๐[,]๐) โง โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง))) โ ๐ฆ โ (๐[,]๐)) |
66 | 64, 65 | ffvelcdmd 7037 |
. . . . . . 7
โข ((๐ โง (๐ฆ โ (๐[,]๐) โง โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง))) โ ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) โ (๐(,)๐)) |
67 | 12, 66 | sselid 3943 |
. . . . . 6
โข ((๐ โง (๐ฆ โ (๐[,]๐) โง โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง))) โ ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) โ
โ*) |
68 | 66, 21 | syl 17 |
. . . . . . 7
โข ((๐ โง (๐ฆ โ (๐[,]๐) โง โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง))) โ (๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) โง ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) < ๐)) |
69 | 68 | simpld 496 |
. . . . . 6
โข ((๐ โง (๐ฆ โ (๐[,]๐) โง โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง))) โ ๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ)) |
70 | | qbtwnxr 13125 |
. . . . . 6
โข ((๐ โ โ*
โง ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) โ โ* โง ๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ)) โ โ๐ โ โ (๐ < ๐ โง ๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ))) |
71 | 63, 67, 69, 70 | syl3anc 1372 |
. . . . 5
โข ((๐ โง (๐ฆ โ (๐[,]๐) โง โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง))) โ โ๐ โ โ (๐ < ๐ โง ๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ))) |
72 | | qre 12883 |
. . . . . . 7
โข (๐ โ โ โ ๐ โ
โ) |
73 | 72 | ad2antrl 727 |
. . . . . 6
โข (((๐ โง (๐ฆ โ (๐[,]๐) โง โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง))) โง (๐ โ โ โง (๐ < ๐ โง ๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ)))) โ ๐ โ โ) |
74 | | simprrl 780 |
. . . . . 6
โข (((๐ โง (๐ฆ โ (๐[,]๐) โง โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง))) โง (๐ โ โ โง (๐ < ๐ โง ๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ)))) โ ๐ < ๐) |
75 | 73 | rexrd 11210 |
. . . . . . 7
โข (((๐ โง (๐ฆ โ (๐[,]๐) โง โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง))) โง (๐ โ โ โง (๐ < ๐ โง ๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ)))) โ ๐ โ โ*) |
76 | 67 | adantr 482 |
. . . . . . 7
โข (((๐ โง (๐ฆ โ (๐[,]๐) โง โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง))) โง (๐ โ โ โง (๐ < ๐ โง ๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ)))) โ ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) โ
โ*) |
77 | 19 | ad2antrr 725 |
. . . . . . 7
โข (((๐ โง (๐ฆ โ (๐[,]๐) โง โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง))) โง (๐ โ โ โง (๐ < ๐ โง ๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ)))) โ ๐ โ
โ*) |
78 | | simprrr 781 |
. . . . . . 7
โข (((๐ โง (๐ฆ โ (๐[,]๐) โง โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง))) โง (๐ โ โ โง (๐ < ๐ โง ๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ)))) โ ๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ)) |
79 | 68 | simprd 497 |
. . . . . . . 8
โข ((๐ โง (๐ฆ โ (๐[,]๐) โง โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง))) โ ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) < ๐) |
80 | 79 | adantr 482 |
. . . . . . 7
โข (((๐ โง (๐ฆ โ (๐[,]๐) โง โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง))) โง (๐ โ โ โง (๐ < ๐ โง ๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ)))) โ ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) < ๐) |
81 | 75, 76, 77, 78, 80 | xrlttrd 13084 |
. . . . . 6
โข (((๐ โง (๐ฆ โ (๐[,]๐) โง โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง))) โง (๐ โ โ โง (๐ < ๐ โง ๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ)))) โ ๐ < ๐) |
82 | 28 | ad2antrr 725 |
. . . . . . 7
โข (((๐ โง (๐ฆ โ (๐[,]๐) โง โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง))) โง (๐ โ โ โง (๐ < ๐ โง ๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ)))) โ ๐ โ
โ*) |
83 | | elioo2 13311 |
. . . . . . 7
โข ((๐ โ โ*
โง ๐ โ
โ*) โ (๐ โ (๐(,)๐) โ (๐ โ โ โง ๐ < ๐ โง ๐ < ๐))) |
84 | 82, 77, 83 | syl2anc 585 |
. . . . . 6
โข (((๐ โง (๐ฆ โ (๐[,]๐) โง โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง))) โง (๐ โ โ โง (๐ < ๐ โง ๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ)))) โ (๐ โ (๐(,)๐) โ (๐ โ โ โง ๐ < ๐ โง ๐ < ๐))) |
85 | 73, 74, 81, 84 | mpbir3and 1343 |
. . . . 5
โข (((๐ โง (๐ฆ โ (๐[,]๐) โง โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง))) โง (๐ โ โ โง (๐ < ๐ โง ๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ)))) โ ๐ โ (๐(,)๐)) |
86 | | anass 470 |
. . . . . 6
โข (((๐ โง ๐ฆ โ (๐[,]๐)) โง โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง)) โ (๐ โง (๐ฆ โ (๐[,]๐) โง โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง)))) |
87 | | simprrr 781 |
. . . . . . . . . . 11
โข (((๐ โง ๐ฆ โ (๐[,]๐)) โง (๐ โ โ โง (๐ < ๐ โง ๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ)))) โ ๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ)) |
88 | 87 | adantr 482 |
. . . . . . . . . 10
โข ((((๐ โง ๐ฆ โ (๐[,]๐)) โง (๐ โ โ โง (๐ < ๐ โง ๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ)))) โง ๐ง โ (๐[,]๐)) โ ๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ)) |
89 | 72 | ad2antrl 727 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ฆ โ (๐[,]๐)) โง (๐ โ โ โง (๐ < ๐ โง ๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ)))) โ ๐ โ โ) |
90 | 89 | adantr 482 |
. . . . . . . . . . . 12
โข ((((๐ โง ๐ฆ โ (๐[,]๐)) โง (๐ โ โ โง (๐ < ๐ โง ๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ)))) โง ๐ง โ (๐[,]๐)) โ ๐ โ โ) |
91 | 90 | rexrd 11210 |
. . . . . . . . . . 11
โข ((((๐ โง ๐ฆ โ (๐[,]๐)) โง (๐ โ โ โง (๐ < ๐ โง ๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ)))) โง ๐ง โ (๐[,]๐)) โ ๐ โ โ*) |
92 | 14 | ad2antrr 725 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ฆ โ (๐[,]๐)) โง (๐ โ โ โง (๐ < ๐ โง ๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ)))) โ (๐ฅ โ (๐[,]๐) โฆ ๐ด):(๐[,]๐)โถ(๐(,)๐)) |
93 | | simplr 768 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ฆ โ (๐[,]๐)) โง (๐ โ โ โง (๐ < ๐ โง ๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ)))) โ ๐ฆ โ (๐[,]๐)) |
94 | 92, 93 | ffvelcdmd 7037 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ฆ โ (๐[,]๐)) โง (๐ โ โ โง (๐ < ๐ โง ๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ)))) โ ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) โ (๐(,)๐)) |
95 | 12, 94 | sselid 3943 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ฆ โ (๐[,]๐)) โง (๐ โ โ โง (๐ < ๐ โง ๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ)))) โ ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) โ
โ*) |
96 | 95 | adantr 482 |
. . . . . . . . . . 11
โข ((((๐ โง ๐ฆ โ (๐[,]๐)) โง (๐ โ โ โง (๐ < ๐ โง ๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ)))) โง ๐ง โ (๐[,]๐)) โ ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) โ
โ*) |
97 | 92 | ffvelcdmda 7036 |
. . . . . . . . . . . 12
โข ((((๐ โง ๐ฆ โ (๐[,]๐)) โง (๐ โ โ โง (๐ < ๐ โง ๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ)))) โง ๐ง โ (๐[,]๐)) โ ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โ (๐(,)๐)) |
98 | 12, 97 | sselid 3943 |
. . . . . . . . . . 11
โข ((((๐ โง ๐ฆ โ (๐[,]๐)) โง (๐ โ โ โง (๐ < ๐ โง ๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ)))) โง ๐ง โ (๐[,]๐)) โ ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โ
โ*) |
99 | | xrltletr 13082 |
. . . . . . . . . . 11
โข ((๐ โ โ*
โง ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) โ โ* โง ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โ โ*) โ ((๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) โง ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง)) โ ๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง))) |
100 | 91, 96, 98, 99 | syl3anc 1372 |
. . . . . . . . . 10
โข ((((๐ โง ๐ฆ โ (๐[,]๐)) โง (๐ โ โ โง (๐ < ๐ โง ๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ)))) โง ๐ง โ (๐[,]๐)) โ ((๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) โง ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง)) โ ๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง))) |
101 | 88, 100 | mpand 694 |
. . . . . . . . 9
โข ((((๐ โง ๐ฆ โ (๐[,]๐)) โง (๐ โ โ โง (๐ < ๐ โง ๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ)))) โง ๐ง โ (๐[,]๐)) โ (((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โ ๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง))) |
102 | 101 | ralimdva 3161 |
. . . . . . . 8
โข (((๐ โง ๐ฆ โ (๐[,]๐)) โง (๐ โ โ โง (๐ < ๐ โง ๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ)))) โ (โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โ โ๐ง โ (๐[,]๐)๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง))) |
103 | 102 | imp 408 |
. . . . . . 7
โข ((((๐ โง ๐ฆ โ (๐[,]๐)) โง (๐ โ โ โง (๐ < ๐ โง ๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ)))) โง โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง)) โ โ๐ง โ (๐[,]๐)๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง)) |
104 | 103 | an32s 651 |
. . . . . 6
โข ((((๐ โง ๐ฆ โ (๐[,]๐)) โง โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง)) โง (๐ โ โ โง (๐ < ๐ โง ๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ)))) โ โ๐ง โ (๐[,]๐)๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง)) |
105 | 86, 104 | sylanbr 583 |
. . . . 5
โข (((๐ โง (๐ฆ โ (๐[,]๐) โง โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง))) โง (๐ โ โ โง (๐ < ๐ โง ๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ)))) โ โ๐ง โ (๐[,]๐)๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง)) |
106 | 71, 85, 105 | reximssdv 3166 |
. . . 4
โข ((๐ โง (๐ฆ โ (๐[,]๐) โง โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง))) โ โ๐ โ (๐(,)๐)โ๐ง โ (๐[,]๐)๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง)) |
107 | 106 | rexlimdvaa 3150 |
. . 3
โข (๐ โ (โ๐ฆ โ (๐[,]๐)โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โ โ๐ โ (๐(,)๐)โ๐ง โ (๐[,]๐)๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง))) |
108 | | ancom 462 |
. . . . 5
โข
((โ๐ โ
(๐(,)๐)โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) < ๐ โง โ๐ โ (๐(,)๐)โ๐ง โ (๐[,]๐)๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง)) โ (โ๐ โ (๐(,)๐)โ๐ง โ (๐[,]๐)๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โง โ๐ โ (๐(,)๐)โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) < ๐)) |
109 | | reeanv 3216 |
. . . . 5
โข
(โ๐ โ
(๐(,)๐)โ๐ โ (๐(,)๐)(โ๐ง โ (๐[,]๐)๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โง โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) < ๐) โ (โ๐ โ (๐(,)๐)โ๐ง โ (๐[,]๐)๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โง โ๐ โ (๐(,)๐)โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) < ๐)) |
110 | 108, 109 | bitr4i 278 |
. . . 4
โข
((โ๐ โ
(๐(,)๐)โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) < ๐ โง โ๐ โ (๐(,)๐)โ๐ง โ (๐[,]๐)๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง)) โ โ๐ โ (๐(,)๐)โ๐ โ (๐(,)๐)(โ๐ง โ (๐[,]๐)๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โง โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) < ๐)) |
111 | | r19.26 3111 |
. . . . . 6
โข
(โ๐ง โ
(๐[,]๐)(๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โง ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) < ๐) โ (โ๐ง โ (๐[,]๐)๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โง โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) < ๐)) |
112 | 14 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ (๐(,)๐) โง ๐ โ (๐(,)๐))) โ (๐ฅ โ (๐[,]๐) โฆ ๐ด):(๐[,]๐)โถ(๐(,)๐)) |
113 | 112 | ffvelcdmda 7036 |
. . . . . . . . . . 11
โข (((๐ โง (๐ โ (๐(,)๐) โง ๐ โ (๐(,)๐))) โง ๐ง โ (๐[,]๐)) โ ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โ (๐(,)๐)) |
114 | 4, 113 | sselid 3943 |
. . . . . . . . . 10
โข (((๐ โง (๐ โ (๐(,)๐) โง ๐ โ (๐(,)๐))) โง ๐ง โ (๐[,]๐)) โ ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โ โ) |
115 | 114 | 3biant1d 1479 |
. . . . . . . . 9
โข (((๐ โง (๐ โ (๐(,)๐) โง ๐ โ (๐(,)๐))) โง ๐ง โ (๐[,]๐)) โ ((๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โง ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) < ๐) โ (((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โ โ โง ๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โง ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) < ๐))) |
116 | | simplrl 776 |
. . . . . . . . . . 11
โข (((๐ โง (๐ โ (๐(,)๐) โง ๐ โ (๐(,)๐))) โง ๐ง โ (๐[,]๐)) โ ๐ โ (๐(,)๐)) |
117 | 12, 116 | sselid 3943 |
. . . . . . . . . 10
โข (((๐ โง (๐ โ (๐(,)๐) โง ๐ โ (๐(,)๐))) โง ๐ง โ (๐[,]๐)) โ ๐ โ โ*) |
118 | | simplrr 777 |
. . . . . . . . . . 11
โข (((๐ โง (๐ โ (๐(,)๐) โง ๐ โ (๐(,)๐))) โง ๐ง โ (๐[,]๐)) โ ๐ โ (๐(,)๐)) |
119 | 12, 118 | sselid 3943 |
. . . . . . . . . 10
โข (((๐ โง (๐ โ (๐(,)๐) โง ๐ โ (๐(,)๐))) โง ๐ง โ (๐[,]๐)) โ ๐ โ โ*) |
120 | | elioo2 13311 |
. . . . . . . . . 10
โข ((๐ โ โ*
โง ๐ โ
โ*) โ (((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โ (๐(,)๐) โ (((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โ โ โง ๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โง ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) < ๐))) |
121 | 117, 119,
120 | syl2anc 585 |
. . . . . . . . 9
โข (((๐ โง (๐ โ (๐(,)๐) โง ๐ โ (๐(,)๐))) โง ๐ง โ (๐[,]๐)) โ (((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โ (๐(,)๐) โ (((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โ โ โง ๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โง ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) < ๐))) |
122 | 115, 121 | bitr4d 282 |
. . . . . . . 8
โข (((๐ โง (๐ โ (๐(,)๐) โง ๐ โ (๐(,)๐))) โง ๐ง โ (๐[,]๐)) โ ((๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โง ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) < ๐) โ ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โ (๐(,)๐))) |
123 | 122 | ralbidva 3169 |
. . . . . . 7
โข ((๐ โง (๐ โ (๐(,)๐) โง ๐ โ (๐(,)๐))) โ (โ๐ง โ (๐[,]๐)(๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โง ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) < ๐) โ โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โ (๐(,)๐))) |
124 | | nffvmpt1 6854 |
. . . . . . . . . . . 12
โข
โฒ๐ฅ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) |
125 | 124 | nfel1 2920 |
. . . . . . . . . . 11
โข
โฒ๐ฅ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โ (๐(,)๐) |
126 | | nfv 1918 |
. . . . . . . . . . 11
โข
โฒ๐ง((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฅ) โ (๐(,)๐) |
127 | | fveq2 6843 |
. . . . . . . . . . . 12
โข (๐ง = ๐ฅ โ ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) = ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฅ)) |
128 | 127 | eleq1d 2819 |
. . . . . . . . . . 11
โข (๐ง = ๐ฅ โ (((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โ (๐(,)๐) โ ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฅ) โ (๐(,)๐))) |
129 | 125, 126,
128 | cbvralw 3288 |
. . . . . . . . . 10
โข
(โ๐ง โ
(๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โ (๐(,)๐) โ โ๐ฅ โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฅ) โ (๐(,)๐)) |
130 | | simpr 486 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ฅ โ (๐[,]๐)) โ ๐ฅ โ (๐[,]๐)) |
131 | 14 | fvmptelcdm 7062 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ฅ โ (๐[,]๐)) โ ๐ด โ (๐(,)๐)) |
132 | | eqid 2733 |
. . . . . . . . . . . . . 14
โข (๐ฅ โ (๐[,]๐) โฆ ๐ด) = (๐ฅ โ (๐[,]๐) โฆ ๐ด) |
133 | 132 | fvmpt2 6960 |
. . . . . . . . . . . . 13
โข ((๐ฅ โ (๐[,]๐) โง ๐ด โ (๐(,)๐)) โ ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฅ) = ๐ด) |
134 | 130, 131,
133 | syl2anc 585 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฅ โ (๐[,]๐)) โ ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฅ) = ๐ด) |
135 | 134 | eleq1d 2819 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ (๐[,]๐)) โ (((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฅ) โ (๐(,)๐) โ ๐ด โ (๐(,)๐))) |
136 | 135 | ralbidva 3169 |
. . . . . . . . . 10
โข (๐ โ (โ๐ฅ โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฅ) โ (๐(,)๐) โ โ๐ฅ โ (๐[,]๐)๐ด โ (๐(,)๐))) |
137 | 129, 136 | bitrid 283 |
. . . . . . . . 9
โข (๐ โ (โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โ (๐(,)๐) โ โ๐ฅ โ (๐[,]๐)๐ด โ (๐(,)๐))) |
138 | 137 | adantr 482 |
. . . . . . . 8
โข ((๐ โง (๐ โ (๐(,)๐) โง ๐ โ (๐(,)๐))) โ (โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โ (๐(,)๐) โ โ๐ฅ โ (๐[,]๐)๐ด โ (๐(,)๐))) |
139 | 1 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง ((๐ โ (๐(,)๐) โง ๐ โ (๐(,)๐)) โง โ๐ฅ โ (๐[,]๐)๐ด โ (๐(,)๐))) โ ๐ โ โ) |
140 | 2 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง ((๐ โ (๐(,)๐) โง ๐ โ (๐(,)๐)) โง โ๐ฅ โ (๐[,]๐)๐ด โ (๐(,)๐))) โ ๐ โ โ) |
141 | 3 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง ((๐ โ (๐(,)๐) โง ๐ โ (๐(,)๐)) โง โ๐ฅ โ (๐[,]๐)๐ด โ (๐(,)๐))) โ ๐ โค ๐) |
142 | 28 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง ((๐ โ (๐(,)๐) โง ๐ โ (๐(,)๐)) โง โ๐ฅ โ (๐[,]๐)๐ด โ (๐(,)๐))) โ ๐ โ
โ*) |
143 | 19 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง ((๐ โ (๐(,)๐) โง ๐ โ (๐(,)๐)) โง โ๐ฅ โ (๐[,]๐)๐ด โ (๐(,)๐))) โ ๐ โ
โ*) |
144 | | nfcv 2904 |
. . . . . . . . . . . . . 14
โข
โฒ๐ฆ๐ด |
145 | | nfcsb1v 3881 |
. . . . . . . . . . . . . 14
โข
โฒ๐ฅโฆ๐ฆ / ๐ฅโฆ๐ด |
146 | | csbeq1a 3870 |
. . . . . . . . . . . . . 14
โข (๐ฅ = ๐ฆ โ ๐ด = โฆ๐ฆ / ๐ฅโฆ๐ด) |
147 | 144, 145,
146 | cbvmpt 5217 |
. . . . . . . . . . . . 13
โข (๐ฅ โ (๐[,]๐) โฆ ๐ด) = (๐ฆ โ (๐[,]๐) โฆ โฆ๐ฆ / ๐ฅโฆ๐ด) |
148 | 147, 8 | eqeltrrid 2839 |
. . . . . . . . . . . 12
โข (๐ โ (๐ฆ โ (๐[,]๐) โฆ โฆ๐ฆ / ๐ฅโฆ๐ด) โ ((๐[,]๐)โcnโ(๐(,)๐))) |
149 | 148 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง ((๐ โ (๐(,)๐) โง ๐ โ (๐(,)๐)) โง โ๐ฅ โ (๐[,]๐)๐ด โ (๐(,)๐))) โ (๐ฆ โ (๐[,]๐) โฆ โฆ๐ฆ / ๐ฅโฆ๐ด) โ ((๐[,]๐)โcnโ(๐(,)๐))) |
150 | | nfcv 2904 |
. . . . . . . . . . . . . 14
โข
โฒ๐ฆ๐ต |
151 | | nfcsb1v 3881 |
. . . . . . . . . . . . . 14
โข
โฒ๐ฅโฆ๐ฆ / ๐ฅโฆ๐ต |
152 | | csbeq1a 3870 |
. . . . . . . . . . . . . 14
โข (๐ฅ = ๐ฆ โ ๐ต = โฆ๐ฆ / ๐ฅโฆ๐ต) |
153 | 150, 151,
152 | cbvmpt 5217 |
. . . . . . . . . . . . 13
โข (๐ฅ โ (๐(,)๐) โฆ ๐ต) = (๐ฆ โ (๐(,)๐) โฆ โฆ๐ฆ / ๐ฅโฆ๐ต) |
154 | | itgsubst.b |
. . . . . . . . . . . . 13
โข (๐ โ (๐ฅ โ (๐(,)๐) โฆ ๐ต) โ (((๐(,)๐)โcnโโ) โฉ
๐ฟ1)) |
155 | 153, 154 | eqeltrrid 2839 |
. . . . . . . . . . . 12
โข (๐ โ (๐ฆ โ (๐(,)๐) โฆ โฆ๐ฆ / ๐ฅโฆ๐ต) โ (((๐(,)๐)โcnโโ) โฉ
๐ฟ1)) |
156 | 155 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง ((๐ โ (๐(,)๐) โง ๐ โ (๐(,)๐)) โง โ๐ฅ โ (๐[,]๐)๐ด โ (๐(,)๐))) โ (๐ฆ โ (๐(,)๐) โฆ โฆ๐ฆ / ๐ฅโฆ๐ต) โ (((๐(,)๐)โcnโโ) โฉ
๐ฟ1)) |
157 | | nfcv 2904 |
. . . . . . . . . . . . . 14
โข
โฒ๐ฃ๐ถ |
158 | | nfcsb1v 3881 |
. . . . . . . . . . . . . 14
โข
โฒ๐ขโฆ๐ฃ / ๐ขโฆ๐ถ |
159 | | csbeq1a 3870 |
. . . . . . . . . . . . . 14
โข (๐ข = ๐ฃ โ ๐ถ = โฆ๐ฃ / ๐ขโฆ๐ถ) |
160 | 157, 158,
159 | cbvmpt 5217 |
. . . . . . . . . . . . 13
โข (๐ข โ (๐(,)๐) โฆ ๐ถ) = (๐ฃ โ (๐(,)๐) โฆ โฆ๐ฃ / ๐ขโฆ๐ถ) |
161 | | itgsubst.c |
. . . . . . . . . . . . 13
โข (๐ โ (๐ข โ (๐(,)๐) โฆ ๐ถ) โ ((๐(,)๐)โcnโโ)) |
162 | 160, 161 | eqeltrrid 2839 |
. . . . . . . . . . . 12
โข (๐ โ (๐ฃ โ (๐(,)๐) โฆ โฆ๐ฃ / ๐ขโฆ๐ถ) โ ((๐(,)๐)โcnโโ)) |
163 | 162 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง ((๐ โ (๐(,)๐) โง ๐ โ (๐(,)๐)) โง โ๐ฅ โ (๐[,]๐)๐ด โ (๐(,)๐))) โ (๐ฃ โ (๐(,)๐) โฆ โฆ๐ฃ / ๐ขโฆ๐ถ) โ ((๐(,)๐)โcnโโ)) |
164 | | itgsubst.da |
. . . . . . . . . . . . 13
โข (๐ โ (โ D (๐ฅ โ (๐[,]๐) โฆ ๐ด)) = (๐ฅ โ (๐(,)๐) โฆ ๐ต)) |
165 | 147 | oveq2i 7369 |
. . . . . . . . . . . . 13
โข (โ
D (๐ฅ โ (๐[,]๐) โฆ ๐ด)) = (โ D (๐ฆ โ (๐[,]๐) โฆ โฆ๐ฆ / ๐ฅโฆ๐ด)) |
166 | 164, 165,
153 | 3eqtr3g 2796 |
. . . . . . . . . . . 12
โข (๐ โ (โ D (๐ฆ โ (๐[,]๐) โฆ โฆ๐ฆ / ๐ฅโฆ๐ด)) = (๐ฆ โ (๐(,)๐) โฆ โฆ๐ฆ / ๐ฅโฆ๐ต)) |
167 | 166 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง ((๐ โ (๐(,)๐) โง ๐ โ (๐(,)๐)) โง โ๐ฅ โ (๐[,]๐)๐ด โ (๐(,)๐))) โ (โ D (๐ฆ โ (๐[,]๐) โฆ โฆ๐ฆ / ๐ฅโฆ๐ด)) = (๐ฆ โ (๐(,)๐) โฆ โฆ๐ฆ / ๐ฅโฆ๐ต)) |
168 | | csbeq1 3859 |
. . . . . . . . . . 11
โข (๐ฃ = โฆ๐ฆ / ๐ฅโฆ๐ด โ โฆ๐ฃ / ๐ขโฆ๐ถ = โฆโฆ๐ฆ / ๐ฅโฆ๐ด / ๐ขโฆ๐ถ) |
169 | | csbeq1 3859 |
. . . . . . . . . . 11
โข (๐ฆ = ๐ โ โฆ๐ฆ / ๐ฅโฆ๐ด = โฆ๐ / ๐ฅโฆ๐ด) |
170 | | csbeq1 3859 |
. . . . . . . . . . 11
โข (๐ฆ = ๐ โ โฆ๐ฆ / ๐ฅโฆ๐ด = โฆ๐ / ๐ฅโฆ๐ด) |
171 | | simprll 778 |
. . . . . . . . . . 11
โข ((๐ โง ((๐ โ (๐(,)๐) โง ๐ โ (๐(,)๐)) โง โ๐ฅ โ (๐[,]๐)๐ด โ (๐(,)๐))) โ ๐ โ (๐(,)๐)) |
172 | | simprlr 779 |
. . . . . . . . . . 11
โข ((๐ โง ((๐ โ (๐(,)๐) โง ๐ โ (๐(,)๐)) โง โ๐ฅ โ (๐[,]๐)๐ด โ (๐(,)๐))) โ ๐ โ (๐(,)๐)) |
173 | | simprr 772 |
. . . . . . . . . . . 12
โข ((๐ โง ((๐ โ (๐(,)๐) โง ๐ โ (๐(,)๐)) โง โ๐ฅ โ (๐[,]๐)๐ด โ (๐(,)๐))) โ โ๐ฅ โ (๐[,]๐)๐ด โ (๐(,)๐)) |
174 | 145 | nfel1 2920 |
. . . . . . . . . . . . 13
โข
โฒ๐ฅโฆ๐ฆ / ๐ฅโฆ๐ด โ (๐(,)๐) |
175 | 146 | eleq1d 2819 |
. . . . . . . . . . . . 13
โข (๐ฅ = ๐ฆ โ (๐ด โ (๐(,)๐) โ โฆ๐ฆ / ๐ฅโฆ๐ด โ (๐(,)๐))) |
176 | 174, 175 | rspc 3568 |
. . . . . . . . . . . 12
โข (๐ฆ โ (๐[,]๐) โ (โ๐ฅ โ (๐[,]๐)๐ด โ (๐(,)๐) โ โฆ๐ฆ / ๐ฅโฆ๐ด โ (๐(,)๐))) |
177 | 173, 176 | mpan9 508 |
. . . . . . . . . . 11
โข (((๐ โง ((๐ โ (๐(,)๐) โง ๐ โ (๐(,)๐)) โง โ๐ฅ โ (๐[,]๐)๐ด โ (๐(,)๐))) โง ๐ฆ โ (๐[,]๐)) โ โฆ๐ฆ / ๐ฅโฆ๐ด โ (๐(,)๐)) |
178 | 139, 140,
141, 142, 143, 149, 156, 163, 167, 168, 169, 170, 171, 172, 177 | itgsubstlem 25428 |
. . . . . . . . . 10
โข ((๐ โง ((๐ โ (๐(,)๐) โง ๐ โ (๐(,)๐)) โง โ๐ฅ โ (๐[,]๐)๐ด โ (๐(,)๐))) โ โจ[โฆ๐ / ๐ฅโฆ๐ด โ โฆ๐ / ๐ฅโฆ๐ด]โฆ๐ฃ / ๐ขโฆ๐ถ d๐ฃ = โจ[๐ โ ๐](โฆโฆ๐ฆ / ๐ฅโฆ๐ด / ๐ขโฆ๐ถ ยท โฆ๐ฆ / ๐ฅโฆ๐ต) d๐ฆ) |
179 | 159, 157,
158 | cbvditg 25234 |
. . . . . . . . . . . 12
โข
โจ[โฆ๐ / ๐ฅโฆ๐ด โ โฆ๐ / ๐ฅโฆ๐ด]๐ถ d๐ข = โจ[โฆ๐ / ๐ฅโฆ๐ด โ โฆ๐ / ๐ฅโฆ๐ด]โฆ๐ฃ / ๐ขโฆ๐ถ d๐ฃ |
180 | | nfcvd 2905 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ
โฒ๐ฅ๐พ) |
181 | | itgsubst.k |
. . . . . . . . . . . . . . 15
โข (๐ฅ = ๐ โ ๐ด = ๐พ) |
182 | 180, 181 | csbiegf 3890 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ
โฆ๐ / ๐ฅโฆ๐ด = ๐พ) |
183 | | ditgeq1 25228 |
. . . . . . . . . . . . . 14
โข
(โฆ๐ /
๐ฅโฆ๐ด = ๐พ โ โจ[โฆ๐ / ๐ฅโฆ๐ด โ โฆ๐ / ๐ฅโฆ๐ด]๐ถ d๐ข = โจ[๐พ โ โฆ๐ / ๐ฅโฆ๐ด]๐ถ d๐ข) |
184 | 1, 182, 183 | 3syl 18 |
. . . . . . . . . . . . 13
โข (๐ โ
โจ[โฆ๐ /
๐ฅโฆ๐ด โ โฆ๐ / ๐ฅโฆ๐ด]๐ถ d๐ข = โจ[๐พ โ โฆ๐ / ๐ฅโฆ๐ด]๐ถ d๐ข) |
185 | | nfcvd 2905 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ
โฒ๐ฅ๐ฟ) |
186 | | itgsubst.l |
. . . . . . . . . . . . . . 15
โข (๐ฅ = ๐ โ ๐ด = ๐ฟ) |
187 | 185, 186 | csbiegf 3890 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ
โฆ๐ / ๐ฅโฆ๐ด = ๐ฟ) |
188 | | ditgeq2 25229 |
. . . . . . . . . . . . . 14
โข
(โฆ๐ /
๐ฅโฆ๐ด = ๐ฟ โ โจ[๐พ โ โฆ๐ / ๐ฅโฆ๐ด]๐ถ d๐ข = โจ[๐พ โ ๐ฟ]๐ถ d๐ข) |
189 | 2, 187, 188 | 3syl 18 |
. . . . . . . . . . . . 13
โข (๐ โ โจ[๐พ โ โฆ๐ / ๐ฅโฆ๐ด]๐ถ d๐ข = โจ[๐พ โ ๐ฟ]๐ถ d๐ข) |
190 | 184, 189 | eqtrd 2773 |
. . . . . . . . . . . 12
โข (๐ โ
โจ[โฆ๐ /
๐ฅโฆ๐ด โ โฆ๐ / ๐ฅโฆ๐ด]๐ถ d๐ข = โจ[๐พ โ ๐ฟ]๐ถ d๐ข) |
191 | 179, 190 | eqtr3id 2787 |
. . . . . . . . . . 11
โข (๐ โ
โจ[โฆ๐ /
๐ฅโฆ๐ด โ โฆ๐ / ๐ฅโฆ๐ด]โฆ๐ฃ / ๐ขโฆ๐ถ d๐ฃ = โจ[๐พ โ ๐ฟ]๐ถ d๐ข) |
192 | 191 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง ((๐ โ (๐(,)๐) โง ๐ โ (๐(,)๐)) โง โ๐ฅ โ (๐[,]๐)๐ด โ (๐(,)๐))) โ โจ[โฆ๐ / ๐ฅโฆ๐ด โ โฆ๐ / ๐ฅโฆ๐ด]โฆ๐ฃ / ๐ขโฆ๐ถ d๐ฃ = โจ[๐พ โ ๐ฟ]๐ถ d๐ข) |
193 | 146 | csbeq1d 3860 |
. . . . . . . . . . . . . 14
โข (๐ฅ = ๐ฆ โ โฆ๐ด / ๐ขโฆ๐ถ = โฆโฆ๐ฆ / ๐ฅโฆ๐ด / ๐ขโฆ๐ถ) |
194 | 193, 152 | oveq12d 7376 |
. . . . . . . . . . . . 13
โข (๐ฅ = ๐ฆ โ (โฆ๐ด / ๐ขโฆ๐ถ ยท ๐ต) = (โฆโฆ๐ฆ / ๐ฅโฆ๐ด / ๐ขโฆ๐ถ ยท โฆ๐ฆ / ๐ฅโฆ๐ต)) |
195 | | nfcv 2904 |
. . . . . . . . . . . . 13
โข
โฒ๐ฆ(โฆ๐ด / ๐ขโฆ๐ถ ยท ๐ต) |
196 | | nfcv 2904 |
. . . . . . . . . . . . . . 15
โข
โฒ๐ฅ๐ถ |
197 | 145, 196 | nfcsbw 3883 |
. . . . . . . . . . . . . 14
โข
โฒ๐ฅโฆโฆ๐ฆ / ๐ฅโฆ๐ด / ๐ขโฆ๐ถ |
198 | | nfcv 2904 |
. . . . . . . . . . . . . 14
โข
โฒ๐ฅ
ยท |
199 | 197, 198,
151 | nfov 7388 |
. . . . . . . . . . . . 13
โข
โฒ๐ฅ(โฆโฆ๐ฆ / ๐ฅโฆ๐ด / ๐ขโฆ๐ถ ยท โฆ๐ฆ / ๐ฅโฆ๐ต) |
200 | 194, 195,
199 | cbvditg 25234 |
. . . . . . . . . . . 12
โข
โจ[๐ โ
๐](โฆ๐ด / ๐ขโฆ๐ถ ยท ๐ต) d๐ฅ = โจ[๐ โ ๐](โฆโฆ๐ฆ / ๐ฅโฆ๐ด / ๐ขโฆ๐ถ ยท โฆ๐ฆ / ๐ฅโฆ๐ต) d๐ฆ |
201 | | ioossicc 13356 |
. . . . . . . . . . . . . . . . . 18
โข (๐(,)๐) โ (๐[,]๐) |
202 | 201 | sseli 3941 |
. . . . . . . . . . . . . . . . 17
โข (๐ฅ โ (๐(,)๐) โ ๐ฅ โ (๐[,]๐)) |
203 | 202, 131 | sylan2 594 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ฅ โ (๐(,)๐)) โ ๐ด โ (๐(,)๐)) |
204 | | nfcvd 2905 |
. . . . . . . . . . . . . . . . 17
โข (๐ด โ (๐(,)๐) โ โฒ๐ข๐ธ) |
205 | | itgsubst.e |
. . . . . . . . . . . . . . . . 17
โข (๐ข = ๐ด โ ๐ถ = ๐ธ) |
206 | 204, 205 | csbiegf 3890 |
. . . . . . . . . . . . . . . 16
โข (๐ด โ (๐(,)๐) โ โฆ๐ด / ๐ขโฆ๐ถ = ๐ธ) |
207 | 203, 206 | syl 17 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ฅ โ (๐(,)๐)) โ โฆ๐ด / ๐ขโฆ๐ถ = ๐ธ) |
208 | 207 | oveq1d 7373 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ฅ โ (๐(,)๐)) โ (โฆ๐ด / ๐ขโฆ๐ถ ยท ๐ต) = (๐ธ ยท ๐ต)) |
209 | 208 | itgeq2dv 25162 |
. . . . . . . . . . . . 13
โข (๐ โ โซ(๐(,)๐)(โฆ๐ด / ๐ขโฆ๐ถ ยท ๐ต) d๐ฅ = โซ(๐(,)๐)(๐ธ ยท ๐ต) d๐ฅ) |
210 | 3 | ditgpos 25236 |
. . . . . . . . . . . . 13
โข (๐ โ โจ[๐ โ ๐](โฆ๐ด / ๐ขโฆ๐ถ ยท ๐ต) d๐ฅ = โซ(๐(,)๐)(โฆ๐ด / ๐ขโฆ๐ถ ยท ๐ต) d๐ฅ) |
211 | 3 | ditgpos 25236 |
. . . . . . . . . . . . 13
โข (๐ โ โจ[๐ โ ๐](๐ธ ยท ๐ต) d๐ฅ = โซ(๐(,)๐)(๐ธ ยท ๐ต) d๐ฅ) |
212 | 209, 210,
211 | 3eqtr4d 2783 |
. . . . . . . . . . . 12
โข (๐ โ โจ[๐ โ ๐](โฆ๐ด / ๐ขโฆ๐ถ ยท ๐ต) d๐ฅ = โจ[๐ โ ๐](๐ธ ยท ๐ต) d๐ฅ) |
213 | 200, 212 | eqtr3id 2787 |
. . . . . . . . . . 11
โข (๐ โ โจ[๐ โ ๐](โฆโฆ๐ฆ / ๐ฅโฆ๐ด / ๐ขโฆ๐ถ ยท โฆ๐ฆ / ๐ฅโฆ๐ต) d๐ฆ = โจ[๐ โ ๐](๐ธ ยท ๐ต) d๐ฅ) |
214 | 213 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง ((๐ โ (๐(,)๐) โง ๐ โ (๐(,)๐)) โง โ๐ฅ โ (๐[,]๐)๐ด โ (๐(,)๐))) โ โจ[๐ โ ๐](โฆโฆ๐ฆ / ๐ฅโฆ๐ด / ๐ขโฆ๐ถ ยท โฆ๐ฆ / ๐ฅโฆ๐ต) d๐ฆ = โจ[๐ โ ๐](๐ธ ยท ๐ต) d๐ฅ) |
215 | 178, 192,
214 | 3eqtr3d 2781 |
. . . . . . . . 9
โข ((๐ โง ((๐ โ (๐(,)๐) โง ๐ โ (๐(,)๐)) โง โ๐ฅ โ (๐[,]๐)๐ด โ (๐(,)๐))) โ โจ[๐พ โ ๐ฟ]๐ถ d๐ข = โจ[๐ โ ๐](๐ธ ยท ๐ต) d๐ฅ) |
216 | 215 | expr 458 |
. . . . . . . 8
โข ((๐ โง (๐ โ (๐(,)๐) โง ๐ โ (๐(,)๐))) โ (โ๐ฅ โ (๐[,]๐)๐ด โ (๐(,)๐) โ โจ[๐พ โ ๐ฟ]๐ถ d๐ข = โจ[๐ โ ๐](๐ธ ยท ๐ต) d๐ฅ)) |
217 | 138, 216 | sylbid 239 |
. . . . . . 7
โข ((๐ โง (๐ โ (๐(,)๐) โง ๐ โ (๐(,)๐))) โ (โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โ (๐(,)๐) โ โจ[๐พ โ ๐ฟ]๐ถ d๐ข = โจ[๐ โ ๐](๐ธ ยท ๐ต) d๐ฅ)) |
218 | 123, 217 | sylbid 239 |
. . . . . 6
โข ((๐ โง (๐ โ (๐(,)๐) โง ๐ โ (๐(,)๐))) โ (โ๐ง โ (๐[,]๐)(๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โง ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) < ๐) โ โจ[๐พ โ ๐ฟ]๐ถ d๐ข = โจ[๐ โ ๐](๐ธ ยท ๐ต) d๐ฅ)) |
219 | 111, 218 | biimtrrid 242 |
. . . . 5
โข ((๐ โง (๐ โ (๐(,)๐) โง ๐ โ (๐(,)๐))) โ ((โ๐ง โ (๐[,]๐)๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โง โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) < ๐) โ โจ[๐พ โ ๐ฟ]๐ถ d๐ข = โจ[๐ โ ๐](๐ธ ยท ๐ต) d๐ฅ)) |
220 | 219 | rexlimdvva 3202 |
. . . 4
โข (๐ โ (โ๐ โ (๐(,)๐)โ๐ โ (๐(,)๐)(โ๐ง โ (๐[,]๐)๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โง โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) < ๐) โ โจ[๐พ โ ๐ฟ]๐ถ d๐ข = โจ[๐ โ ๐](๐ธ ยท ๐ต) d๐ฅ)) |
221 | 110, 220 | biimtrid 241 |
. . 3
โข (๐ โ ((โ๐ โ (๐(,)๐)โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) < ๐ โง โ๐ โ (๐(,)๐)โ๐ง โ (๐[,]๐)๐ < ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง)) โ โจ[๐พ โ ๐ฟ]๐ถ d๐ข = โจ[๐ โ ๐](๐ธ ยท ๐ต) d๐ฅ)) |
222 | 62, 107, 221 | syl2and 609 |
. 2
โข (๐ โ ((โ๐ฆ โ (๐[,]๐)โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) โง โ๐ฆ โ (๐[,]๐)โ๐ง โ (๐[,]๐)((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ฆ) โค ((๐ฅ โ (๐[,]๐) โฆ ๐ด)โ๐ง)) โ โจ[๐พ โ ๐ฟ]๐ถ d๐ข = โจ[๐ โ ๐](๐ธ ยท ๐ต) d๐ฅ)) |
223 | 10, 222 | mpd 15 |
1
โข (๐ โ โจ[๐พ โ ๐ฟ]๐ถ d๐ข = โจ[๐ โ ๐](๐ธ ยท ๐ต) d๐ฅ) |