Step | Hyp | Ref
| Expression |
1 | | itg2addnc.f2 |
. . . . . . . . . . 11
β’ (π β πΉ:ββΆ(0[,)+β)) |
2 | | rge0ssre 13380 |
. . . . . . . . . . 11
β’
(0[,)+β) β β |
3 | | fss 6690 |
. . . . . . . . . . 11
β’ ((πΉ:ββΆ(0[,)+β)
β§ (0[,)+β) β β) β πΉ:ββΆβ) |
4 | 1, 2, 3 | sylancl 587 |
. . . . . . . . . 10
β’ (π β πΉ:ββΆβ) |
5 | 4 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ β β dom β«1) β§ π£ β β+)
β πΉ:ββΆβ) |
6 | 5 | ffvelcdmda 7040 |
. . . . . . . 8
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π₯ β β)
β (πΉβπ₯) β
β) |
7 | | rpre 12930 |
. . . . . . . . . 10
β’ (π£ β β+
β π£ β
β) |
8 | | 3re 12240 |
. . . . . . . . . . 11
β’ 3 β
β |
9 | | 3ne0 12266 |
. . . . . . . . . . 11
β’ 3 β
0 |
10 | 8, 9 | pm3.2i 472 |
. . . . . . . . . 10
β’ (3 β
β β§ 3 β 0) |
11 | | redivcl 11881 |
. . . . . . . . . . 11
β’ ((π£ β β β§ 3 β
β β§ 3 β 0) β (π£ / 3) β β) |
12 | 11 | 3expb 1121 |
. . . . . . . . . 10
β’ ((π£ β β β§ (3 β
β β§ 3 β 0)) β (π£ / 3) β β) |
13 | 7, 10, 12 | sylancl 587 |
. . . . . . . . 9
β’ (π£ β β+
β (π£ / 3) β
β) |
14 | 13 | ad2antlr 726 |
. . . . . . . 8
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π₯ β β)
β (π£ / 3) β
β) |
15 | | rpcnne0 12940 |
. . . . . . . . . 10
β’ (π£ β β+
β (π£ β β
β§ π£ β
0)) |
16 | | 3cn 12241 |
. . . . . . . . . . 11
β’ 3 β
β |
17 | 16, 9 | pm3.2i 472 |
. . . . . . . . . 10
β’ (3 β
β β§ 3 β 0) |
18 | | divne0 11832 |
. . . . . . . . . 10
β’ (((π£ β β β§ π£ β 0) β§ (3 β β
β§ 3 β 0)) β (π£
/ 3) β 0) |
19 | 15, 17, 18 | sylancl 587 |
. . . . . . . . 9
β’ (π£ β β+
β (π£ / 3) β
0) |
20 | 19 | ad2antlr 726 |
. . . . . . . 8
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π₯ β β)
β (π£ / 3) β
0) |
21 | 6, 14, 20 | redivcld 11990 |
. . . . . . 7
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π₯ β β)
β ((πΉβπ₯) / (π£ / 3)) β β) |
22 | | reflcl 13708 |
. . . . . . 7
β’ (((πΉβπ₯) / (π£ / 3)) β β β
(ββ((πΉβπ₯) / (π£ / 3))) β β) |
23 | 21, 22 | syl 17 |
. . . . . 6
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π₯ β β)
β (ββ((πΉβπ₯) / (π£ / 3))) β β) |
24 | | peano2rem 11475 |
. . . . . 6
β’
((ββ((πΉβπ₯) / (π£ / 3))) β β β
((ββ((πΉβπ₯) / (π£ / 3))) β 1) β
β) |
25 | 23, 24 | syl 17 |
. . . . 5
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π₯ β β)
β ((ββ((πΉβπ₯) / (π£ / 3))) β 1) β
β) |
26 | 25, 14 | remulcld 11192 |
. . . 4
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π₯ β β)
β (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β
β) |
27 | | i1ff 25056 |
. . . . . 6
β’ (β β dom β«1
β β:ββΆβ) |
28 | 27 | ad2antlr 726 |
. . . . 5
β’ (((π β§ β β dom β«1) β§ π£ β β+)
β β:ββΆβ) |
29 | 28 | ffvelcdmda 7040 |
. . . 4
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π₯ β β)
β (ββπ₯) β
β) |
30 | 26, 29 | ifcld 4537 |
. . 3
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π₯ β β)
β if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯)) β β) |
31 | 30 | fmpttd 7068 |
. 2
β’ (((π β§ β β dom β«1) β§ π£ β β+)
β (π₯ β β
β¦ if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯))):ββΆβ) |
32 | | fzfi 13884 |
. . . . 5
β’
(0...-(ββ-((sup(ran β, β, < ) / (π£ / 3)) + 1))) β Fin |
33 | | ovex 7395 |
. . . . . . 7
β’ ((π‘ β 1) Β· (π£ / 3)) β V |
34 | | eqid 2737 |
. . . . . . 7
β’ (π‘ β
(0...-(ββ-((sup(ran β, β, < ) / (π£ / 3)) + 1))) β¦ ((π‘ β 1) Β· (π£ / 3))) = (π‘ β (0...-(ββ-((sup(ran β, β, < ) / (π£ / 3)) + 1))) β¦ ((π‘ β 1) Β· (π£ / 3))) |
35 | 33, 34 | fnmpti 6649 |
. . . . . 6
β’ (π‘ β
(0...-(ββ-((sup(ran β, β, < ) / (π£ / 3)) + 1))) β¦ ((π‘ β 1) Β· (π£ / 3))) Fn (0...-(ββ-((sup(ran
β, β, < ) / (π£ / 3)) + 1))) |
36 | | dffn4 6767 |
. . . . . 6
β’ ((π‘ β
(0...-(ββ-((sup(ran β, β, < ) / (π£ / 3)) + 1))) β¦ ((π‘ β 1) Β· (π£ / 3))) Fn (0...-(ββ-((sup(ran
β, β, < ) / (π£ / 3)) + 1))) β (π‘ β
(0...-(ββ-((sup(ran β, β, < ) / (π£ / 3)) + 1))) β¦ ((π‘ β 1) Β· (π£ / 3))):(0...-(ββ-((sup(ran β, β, < ) / (π£ / 3)) + 1)))βontoβran (π‘ β (0...-(ββ-((sup(ran β, β, < ) / (π£ / 3)) + 1))) β¦ ((π‘ β 1) Β· (π£ / 3)))) |
37 | 35, 36 | mpbi 229 |
. . . . 5
β’ (π‘ β
(0...-(ββ-((sup(ran β, β, < ) / (π£ / 3)) + 1))) β¦ ((π‘ β 1) Β· (π£ / 3))):(0...-(ββ-((sup(ran β, β, < ) / (π£ / 3)) + 1)))βontoβran (π‘ β (0...-(ββ-((sup(ran β, β, < ) / (π£ / 3)) + 1))) β¦ ((π‘ β 1) Β· (π£ / 3))) |
38 | | fofi 9289 |
. . . . 5
β’
(((0...-(ββ-((sup(ran β, β, < ) / (π£ / 3)) + 1))) β Fin β§ (π‘ β
(0...-(ββ-((sup(ran β, β, < ) / (π£ / 3)) + 1))) β¦ ((π‘ β 1) Β· (π£ / 3))):(0...-(ββ-((sup(ran β, β, < ) / (π£ / 3)) + 1)))βontoβran (π‘ β (0...-(ββ-((sup(ran β, β, < ) / (π£ / 3)) + 1))) β¦ ((π‘ β 1) Β· (π£ / 3)))) β ran (π‘ β
(0...-(ββ-((sup(ran β, β, < ) / (π£ / 3)) + 1))) β¦ ((π‘ β 1) Β· (π£ / 3))) β Fin) |
39 | 32, 37, 38 | mp2an 691 |
. . . 4
β’ ran
(π‘ β
(0...-(ββ-((sup(ran β, β, < ) / (π£ / 3)) + 1))) β¦ ((π‘ β 1) Β· (π£ / 3))) β Fin |
40 | | i1frn 25057 |
. . . . 5
β’ (β β dom β«1
β ran β β
Fin) |
41 | 40 | ad2antlr 726 |
. . . 4
β’ (((π β§ β β dom β«1) β§ π£ β β+)
β ran β β
Fin) |
42 | | unfi 9123 |
. . . 4
β’ ((ran
(π‘ β
(0...-(ββ-((sup(ran β, β, < ) / (π£ / 3)) + 1))) β¦ ((π‘ β 1) Β· (π£ / 3))) β Fin β§ ran β β Fin) β (ran (π‘ β
(0...-(ββ-((sup(ran β, β, < ) / (π£ / 3)) + 1))) β¦ ((π‘ β 1) Β· (π£ / 3))) βͺ ran β) β Fin) |
43 | 39, 41, 42 | sylancr 588 |
. . 3
β’ (((π β§ β β dom β«1) β§ π£ β β+)
β (ran (π‘ β
(0...-(ββ-((sup(ran β, β, < ) / (π£ / 3)) + 1))) β¦ ((π‘ β 1) Β· (π£ / 3))) βͺ ran β) β Fin) |
44 | | 0zd 12518 |
. . . . . . . . . 10
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π₯ β β) β§
((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0)) β 0 β
β€) |
45 | 27 | frnd 6681 |
. . . . . . . . . . . . . . . 16
β’ (β β dom β«1
β ran β β
β) |
46 | | i1f0rn 25062 |
. . . . . . . . . . . . . . . . . 18
β’ (β β dom β«1
β 0 β ran β) |
47 | | elex2 2817 |
. . . . . . . . . . . . . . . . . 18
β’ (0 β
ran β β βπ₯ π₯ β ran β) |
48 | 46, 47 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (β β dom β«1
β βπ₯ π₯ β ran β) |
49 | | n0 4311 |
. . . . . . . . . . . . . . . . 17
β’ (ran
β β β
β
βπ₯ π₯ β ran β) |
50 | 48, 49 | sylibr 233 |
. . . . . . . . . . . . . . . 16
β’ (β β dom β«1
β ran β β
β
) |
51 | | fimaxre2 12107 |
. . . . . . . . . . . . . . . . 17
β’ ((ran
β β β β§ ran
β β Fin) β
βπ₯ β β
βπ¦ β ran β π¦ β€ π₯) |
52 | 45, 40, 51 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ (β β dom β«1
β βπ₯ β
β βπ¦ β
ran β π¦ β€ π₯) |
53 | | suprcl 12122 |
. . . . . . . . . . . . . . . 16
β’ ((ran
β β β β§ ran
β β β
β§
βπ₯ β β
βπ¦ β ran β π¦ β€ π₯) β sup(ran β, β, < ) β
β) |
54 | 45, 50, 52, 53 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ (β β dom β«1
β sup(ran β, β,
< ) β β) |
55 | 54 | ad3antlr 730 |
. . . . . . . . . . . . . 14
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π₯ β β)
β sup(ran β, β,
< ) β β) |
56 | 55, 14, 20 | redivcld 11990 |
. . . . . . . . . . . . 13
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π₯ β β)
β (sup(ran β, β,
< ) / (π£ / 3)) β
β) |
57 | | peano2re 11335 |
. . . . . . . . . . . . 13
β’ ((sup(ran
β, β, < ) / (π£ / 3)) β β β
((sup(ran β, β, < )
/ (π£ / 3)) + 1) β
β) |
58 | 56, 57 | syl 17 |
. . . . . . . . . . . 12
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π₯ β β)
β ((sup(ran β, β,
< ) / (π£ / 3)) + 1)
β β) |
59 | | ceicl 13753 |
. . . . . . . . . . . 12
β’
(((sup(ran β,
β, < ) / (π£ / 3))
+ 1) β β β -(ββ-((sup(ran β, β, < ) / (π£ / 3)) + 1)) β β€) |
60 | 58, 59 | syl 17 |
. . . . . . . . . . 11
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π₯ β β)
β -(ββ-((sup(ran β, β, < ) / (π£ / 3)) + 1)) β β€) |
61 | 60 | adantr 482 |
. . . . . . . . . 10
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π₯ β β) β§
((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0)) β -(ββ-((sup(ran
β, β, < ) / (π£ / 3)) + 1)) β
β€) |
62 | 21 | flcld 13710 |
. . . . . . . . . . 11
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π₯ β β)
β (ββ((πΉβπ₯) / (π£ / 3))) β β€) |
63 | 62 | adantr 482 |
. . . . . . . . . 10
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π₯ β β) β§
((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0)) β (ββ((πΉβπ₯) / (π£ / 3))) β β€) |
64 | | 3nn 12239 |
. . . . . . . . . . . . . . . . 17
β’ 3 β
β |
65 | | nnrp 12933 |
. . . . . . . . . . . . . . . . 17
β’ (3 β
β β 3 β β+) |
66 | 64, 65 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
β’ 3 β
β+ |
67 | | rpdivcl 12947 |
. . . . . . . . . . . . . . . 16
β’ ((π£ β β+
β§ 3 β β+) β (π£ / 3) β
β+) |
68 | 66, 67 | mpan2 690 |
. . . . . . . . . . . . . . 15
β’ (π£ β β+
β (π£ / 3) β
β+) |
69 | 68 | ad2antlr 726 |
. . . . . . . . . . . . . 14
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π₯ β β)
β (π£ / 3) β
β+) |
70 | 1 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ β β dom β«1) β§ π£ β β+)
β πΉ:ββΆ(0[,)+β)) |
71 | 70 | ffvelcdmda 7040 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π₯ β β)
β (πΉβπ₯) β
(0[,)+β)) |
72 | | elrege0 13378 |
. . . . . . . . . . . . . . . 16
β’ ((πΉβπ₯) β (0[,)+β) β ((πΉβπ₯) β β β§ 0 β€ (πΉβπ₯))) |
73 | 71, 72 | sylib 217 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π₯ β β)
β ((πΉβπ₯) β β β§ 0 β€
(πΉβπ₯))) |
74 | 73 | simprd 497 |
. . . . . . . . . . . . . 14
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π₯ β β)
β 0 β€ (πΉβπ₯)) |
75 | 6, 69, 74 | divge0d 13004 |
. . . . . . . . . . . . 13
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π₯ β β)
β 0 β€ ((πΉβπ₯) / (π£ / 3))) |
76 | | flge0nn0 13732 |
. . . . . . . . . . . . 13
β’ ((((πΉβπ₯) / (π£ / 3)) β β β§ 0 β€ ((πΉβπ₯) / (π£ / 3))) β (ββ((πΉβπ₯) / (π£ / 3))) β
β0) |
77 | 21, 75, 76 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π₯ β β)
β (ββ((πΉβπ₯) / (π£ / 3))) β
β0) |
78 | 77 | nn0ge0d 12483 |
. . . . . . . . . . 11
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π₯ β β)
β 0 β€ (ββ((πΉβπ₯) / (π£ / 3)))) |
79 | 78 | adantr 482 |
. . . . . . . . . 10
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π₯ β β) β§
((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0)) β 0 β€
(ββ((πΉβπ₯) / (π£ / 3)))) |
80 | 45, 50, 52 | 3jca 1129 |
. . . . . . . . . . . . . . 15
β’ (β β dom β«1
β (ran β β
β β§ ran β β
β
β§ βπ₯
β β βπ¦
β ran β π¦ β€ π₯)) |
81 | 80 | ad3antlr 730 |
. . . . . . . . . . . . . 14
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π₯ β β)
β (ran β β
β β§ ran β β
β
β§ βπ₯
β β βπ¦
β ran β π¦ β€ π₯)) |
82 | | ffn 6673 |
. . . . . . . . . . . . . . . . . 18
β’ (β:ββΆβ β
β Fn
β) |
83 | 27, 82 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (β β dom β«1
β β Fn
β) |
84 | | dffn3 6686 |
. . . . . . . . . . . . . . . . 17
β’ (β Fn β β β:ββΆran β) |
85 | 83, 84 | sylib 217 |
. . . . . . . . . . . . . . . 16
β’ (β β dom β«1
β β:ββΆran
β) |
86 | 85 | ad2antlr 726 |
. . . . . . . . . . . . . . 15
β’ (((π β§ β β dom β«1) β§ π£ β β+)
β β:ββΆran
β) |
87 | 86 | ffvelcdmda 7040 |
. . . . . . . . . . . . . 14
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π₯ β β)
β (ββπ₯) β ran β) |
88 | | suprub 12123 |
. . . . . . . . . . . . . 14
β’ (((ran
β β β β§ ran
β β β
β§
βπ₯ β β
βπ¦ β ran β π¦ β€ π₯) β§ (ββπ₯) β ran β) β (ββπ₯) β€ sup(ran β, β, < )) |
89 | 81, 87, 88 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π₯ β β)
β (ββπ₯) β€ sup(ran β, β, <
)) |
90 | | letr 11256 |
. . . . . . . . . . . . . . 15
β’
(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β β β§
(ββπ₯) β β β§ sup(ran β, β, < ) β β)
β (((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β€ sup(ran β, β, < )) β
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ sup(ran β, β, <
))) |
91 | 26, 29, 55, 90 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π₯ β β)
β (((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β€ sup(ran β, β, < )) β
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ sup(ran β, β, <
))) |
92 | 25, 55, 69 | lemuldivd 13013 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π₯ β β)
β ((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ sup(ran β, β, < ) β
((ββ((πΉβπ₯) / (π£ / 3))) β 1) β€ (sup(ran β, β, < ) / (π£ / 3)))) |
93 | | 1red 11163 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π₯ β β)
β 1 β β) |
94 | 23, 93, 56 | lesubaddd 11759 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π₯ β β)
β (((ββ((πΉβπ₯) / (π£ / 3))) β 1) β€ (sup(ran β, β, < ) / (π£ / 3)) β
(ββ((πΉβπ₯) / (π£ / 3))) β€ ((sup(ran β, β, < ) / (π£ / 3)) + 1))) |
95 | 92, 94 | bitrd 279 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π₯ β β)
β ((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ sup(ran β, β, < ) β
(ββ((πΉβπ₯) / (π£ / 3))) β€ ((sup(ran β, β, < ) / (π£ / 3)) + 1))) |
96 | | ceige 13756 |
. . . . . . . . . . . . . . . . 17
β’
(((sup(ran β,
β, < ) / (π£ / 3))
+ 1) β β β ((sup(ran β, β, < ) / (π£ / 3)) + 1) β€ -(ββ-((sup(ran
β, β, < ) / (π£ / 3)) + 1))) |
97 | 58, 96 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π₯ β β)
β ((sup(ran β, β,
< ) / (π£ / 3)) + 1) β€
-(ββ-((sup(ran β, β, < ) / (π£ / 3)) + 1))) |
98 | 60 | zred 12614 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π₯ β β)
β -(ββ-((sup(ran β, β, < ) / (π£ / 3)) + 1)) β β) |
99 | | letr 11256 |
. . . . . . . . . . . . . . . . 17
β’
(((ββ((πΉβπ₯) / (π£ / 3))) β β β§ ((sup(ran β, β, < ) / (π£ / 3)) + 1) β β β§
-(ββ-((sup(ran β, β, < ) / (π£ / 3)) + 1)) β β) β
(((ββ((πΉβπ₯) / (π£ / 3))) β€ ((sup(ran β, β, < ) / (π£ / 3)) + 1) β§ ((sup(ran β, β, < ) / (π£ / 3)) + 1) β€
-(ββ-((sup(ran β, β, < ) / (π£ / 3)) + 1))) β (ββ((πΉβπ₯) / (π£ / 3))) β€ -(ββ-((sup(ran β, β, < ) / (π£ / 3)) + 1)))) |
100 | 23, 58, 98, 99 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π₯ β β)
β (((ββ((πΉβπ₯) / (π£ / 3))) β€ ((sup(ran β, β, < ) / (π£ / 3)) + 1) β§ ((sup(ran β, β, < ) / (π£ / 3)) + 1) β€
-(ββ-((sup(ran β, β, < ) / (π£ / 3)) + 1))) β (ββ((πΉβπ₯) / (π£ / 3))) β€ -(ββ-((sup(ran β, β, < ) / (π£ / 3)) + 1)))) |
101 | 97, 100 | mpan2d 693 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π₯ β β)
β ((ββ((πΉβπ₯) / (π£ / 3))) β€ ((sup(ran β, β, < ) / (π£ / 3)) + 1) β (ββ((πΉβπ₯) / (π£ / 3))) β€ -(ββ-((sup(ran β, β, < ) / (π£ / 3)) + 1)))) |
102 | 95, 101 | sylbid 239 |
. . . . . . . . . . . . . 14
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π₯ β β)
β ((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ sup(ran β, β, < ) β
(ββ((πΉβπ₯) / (π£ / 3))) β€ -(ββ-((sup(ran β, β, < ) / (π£ / 3)) + 1)))) |
103 | 91, 102 | syld 47 |
. . . . . . . . . . . . 13
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π₯ β β)
β (((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β€ sup(ran β, β, < )) β
(ββ((πΉβπ₯) / (π£ / 3))) β€ -(ββ-((sup(ran β, β, < ) / (π£ / 3)) + 1)))) |
104 | 89, 103 | mpan2d 693 |
. . . . . . . . . . . 12
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π₯ β β)
β ((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β (ββ((πΉβπ₯) / (π£ / 3))) β€ -(ββ-((sup(ran β, β, < ) / (π£ / 3)) + 1)))) |
105 | 104 | adantrd 493 |
. . . . . . . . . . 11
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π₯ β β)
β (((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0) β (ββ((πΉβπ₯) / (π£ / 3))) β€ -(ββ-((sup(ran β, β, < ) / (π£ / 3)) + 1)))) |
106 | 105 | imp 408 |
. . . . . . . . . 10
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π₯ β β) β§
((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0)) β (ββ((πΉβπ₯) / (π£ / 3))) β€ -(ββ-((sup(ran β, β, < ) / (π£ / 3)) + 1))) |
107 | 44, 61, 63, 79, 106 | elfzd 13439 |
. . . . . . . . 9
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π₯ β β) β§
((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0)) β (ββ((πΉβπ₯) / (π£ / 3))) β
(0...-(ββ-((sup(ran β, β, < ) / (π£ / 3)) + 1)))) |
108 | | eqid 2737 |
. . . . . . . . 9
β’
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) =
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) |
109 | | oveq1 7369 |
. . . . . . . . . . 11
β’ (π‘ = (ββ((πΉβπ₯) / (π£ / 3))) β (π‘ β 1) = ((ββ((πΉβπ₯) / (π£ / 3))) β 1)) |
110 | 109 | oveq1d 7377 |
. . . . . . . . . 10
β’ (π‘ = (ββ((πΉβπ₯) / (π£ / 3))) β ((π‘ β 1) Β· (π£ / 3)) = (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3))) |
111 | 110 | rspceeqv 3600 |
. . . . . . . . 9
β’
(((ββ((πΉβπ₯) / (π£ / 3))) β
(0...-(ββ-((sup(ran β, β, < ) / (π£ / 3)) + 1))) β§ (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) =
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3))) β βπ‘ β
(0...-(ββ-((sup(ran β, β, < ) / (π£ / 3)) + 1)))(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) = ((π‘ β 1) Β· (π£ / 3))) |
112 | 107, 108,
111 | sylancl 587 |
. . . . . . . 8
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π₯ β β) β§
((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0)) β βπ‘ β (0...-(ββ-((sup(ran β, β, < ) / (π£ / 3)) +
1)))(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) = ((π‘ β 1) Β· (π£ / 3))) |
113 | | ovex 7395 |
. . . . . . . . 9
β’
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β V |
114 | 34 | elrnmpt 5916 |
. . . . . . . . 9
β’
((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β V β
((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β ran (π‘ β
(0...-(ββ-((sup(ran β, β, < ) / (π£ / 3)) + 1))) β¦ ((π‘ β 1) Β· (π£ / 3))) β βπ‘ β (0...-(ββ-((sup(ran β, β, < ) / (π£ / 3)) +
1)))(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) = ((π‘ β 1) Β· (π£ / 3)))) |
115 | 113, 114 | ax-mp 5 |
. . . . . . . 8
β’
((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β ran (π‘ β
(0...-(ββ-((sup(ran β, β, < ) / (π£ / 3)) + 1))) β¦ ((π‘ β 1) Β· (π£ / 3))) β βπ‘ β (0...-(ββ-((sup(ran β, β, < ) / (π£ / 3)) +
1)))(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) = ((π‘ β 1) Β· (π£ / 3))) |
116 | 112, 115 | sylibr 233 |
. . . . . . 7
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π₯ β β) β§
((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0)) β (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β ran (π‘ β
(0...-(ββ-((sup(ran β, β, < ) / (π£ / 3)) + 1))) β¦ ((π‘ β 1) Β· (π£ / 3)))) |
117 | | elun1 4141 |
. . . . . . 7
β’
((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β ran (π‘ β
(0...-(ββ-((sup(ran β, β, < ) / (π£ / 3)) + 1))) β¦ ((π‘ β 1) Β· (π£ / 3))) β (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β (ran (π‘ β
(0...-(ββ-((sup(ran β, β, < ) / (π£ / 3)) + 1))) β¦ ((π‘ β 1) Β· (π£ / 3))) βͺ ran β)) |
118 | 116, 117 | syl 17 |
. . . . . 6
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π₯ β β) β§
((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0)) β (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β (ran (π‘ β
(0...-(ββ-((sup(ran β, β, < ) / (π£ / 3)) + 1))) β¦ ((π‘ β 1) Β· (π£ / 3))) βͺ ran β)) |
119 | | elun2 4142 |
. . . . . . . 8
β’ ((ββπ₯) β ran β β (ββπ₯) β (ran (π‘ β (0...-(ββ-((sup(ran β, β, < ) / (π£ / 3)) + 1))) β¦ ((π‘ β 1) Β· (π£ / 3))) βͺ ran β)) |
120 | 87, 119 | syl 17 |
. . . . . . 7
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π₯ β β)
β (ββπ₯) β (ran (π‘ β
(0...-(ββ-((sup(ran β, β, < ) / (π£ / 3)) + 1))) β¦ ((π‘ β 1) Β· (π£ / 3))) βͺ ran β)) |
121 | 120 | adantr 482 |
. . . . . 6
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π₯ β β) β§ Β¬
((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0)) β (ββπ₯) β (ran (π‘ β (0...-(ββ-((sup(ran β, β, < ) / (π£ / 3)) + 1))) β¦ ((π‘ β 1) Β· (π£ / 3))) βͺ ran β)) |
122 | 118, 121 | ifclda 4526 |
. . . . 5
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π₯ β β)
β if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯)) β (ran (π‘ β (0...-(ββ-((sup(ran β, β, < ) / (π£ / 3)) + 1))) β¦ ((π‘ β 1) Β· (π£ / 3))) βͺ ran β)) |
123 | 122 | fmpttd 7068 |
. . . 4
β’ (((π β§ β β dom β«1) β§ π£ β β+)
β (π₯ β β
β¦ if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯))):ββΆ(ran (π‘ β (0...-(ββ-((sup(ran β, β, < ) / (π£ / 3)) + 1))) β¦ ((π‘ β 1) Β· (π£ / 3))) βͺ ran β)) |
124 | 123 | frnd 6681 |
. . 3
β’ (((π β§ β β dom β«1) β§ π£ β β+)
β ran (π₯ β
β β¦ if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯))) β (ran (π‘ β (0...-(ββ-((sup(ran β, β, < ) / (π£ / 3)) + 1))) β¦ ((π‘ β 1) Β· (π£ / 3))) βͺ ran β)) |
125 | | ssfi 9124 |
. . 3
β’ (((ran
(π‘ β
(0...-(ββ-((sup(ran β, β, < ) / (π£ / 3)) + 1))) β¦ ((π‘ β 1) Β· (π£ / 3))) βͺ ran β) β Fin β§ ran (π₯ β β β¦
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯))) β (ran (π‘ β (0...-(ββ-((sup(ran β, β, < ) / (π£ / 3)) + 1))) β¦ ((π‘ β 1) Β· (π£ / 3))) βͺ ran β)) β ran (π₯ β β β¦
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯))) β Fin) |
126 | 43, 124, 125 | syl2anc 585 |
. 2
β’ (((π β§ β β dom β«1) β§ π£ β β+)
β ran (π₯ β
β β¦ if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯))) β Fin) |
127 | | eqid 2737 |
. . . . 5
β’ (π₯ β β β¦
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯))) = (π₯ β β β¦
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯))) |
128 | 127 | mptpreima 6195 |
. . . 4
β’ (β‘(π₯ β β β¦
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯))) β {π‘}) = {π₯ β β β£
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯)) β {π‘}} |
129 | | unrab 4270 |
. . . . 5
β’ ({π₯ β β β£
(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0) β§ π‘ = (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)))} βͺ {π₯ β β β£ ((Β¬
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β¨ (ββπ₯) = 0) β§ π‘ = (ββπ₯))}) = {π₯ β β β£
((((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0) β§ π‘ = (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3))) β¨ ((Β¬
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β¨ (ββπ₯) = 0) β§ π‘ = (ββπ₯)))} |
130 | | inrab 4271 |
. . . . . . . 8
β’ ({π₯ β β β£
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)} β© {π₯ β β β£ (ββπ₯) β 0}) = {π₯ β β β£
((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0)} |
131 | 130 | ineq1i 4173 |
. . . . . . 7
β’ (({π₯ β β β£
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)} β© {π₯ β β β£ (ββπ₯) β 0}) β© {π₯ β β β£ π‘ = (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3))}) = ({π₯ β β β£
((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0)} β© {π₯ β β β£ π‘ = (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3))}) |
132 | | inrab 4271 |
. . . . . . 7
β’ ({π₯ β β β£
((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0)} β© {π₯ β β β£ π‘ = (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3))}) = {π₯ β β β£
(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0) β§ π‘ = (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)))} |
133 | 131, 132 | eqtri 2765 |
. . . . . 6
β’ (({π₯ β β β£
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)} β© {π₯ β β β£ (ββπ₯) β 0}) β© {π₯ β β β£ π‘ = (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3))}) = {π₯ β β β£
(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0) β§ π‘ = (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)))} |
134 | | unrab 4270 |
. . . . . . . 8
β’ ({π₯ β β β£ Β¬
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)} βͺ {π₯ β β β£ (ββπ₯) = 0}) = {π₯ β β β£ (Β¬
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β¨ (ββπ₯) = 0)} |
135 | 134 | ineq1i 4173 |
. . . . . . 7
β’ (({π₯ β β β£ Β¬
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)} βͺ {π₯ β β β£ (ββπ₯) = 0}) β© {π₯ β β β£ π‘ = (ββπ₯)}) = ({π₯ β β β£ (Β¬
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β¨ (ββπ₯) = 0)} β© {π₯ β β β£ π‘ = (ββπ₯)}) |
136 | | inrab 4271 |
. . . . . . 7
β’ ({π₯ β β β£ (Β¬
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β¨ (ββπ₯) = 0)} β© {π₯ β β β£ π‘ = (ββπ₯)}) = {π₯ β β β£ ((Β¬
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β¨ (ββπ₯) = 0) β§ π‘ = (ββπ₯))} |
137 | 135, 136 | eqtri 2765 |
. . . . . 6
β’ (({π₯ β β β£ Β¬
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)} βͺ {π₯ β β β£ (ββπ₯) = 0}) β© {π₯ β β β£ π‘ = (ββπ₯)}) = {π₯ β β β£ ((Β¬
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β¨ (ββπ₯) = 0) β§ π‘ = (ββπ₯))} |
138 | 133, 137 | uneq12i 4126 |
. . . . 5
β’ ((({π₯ β β β£
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)} β© {π₯ β β β£ (ββπ₯) β 0}) β© {π₯ β β β£ π‘ = (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3))}) βͺ (({π₯ β β β£ Β¬
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)} βͺ {π₯ β β β£ (ββπ₯) = 0}) β© {π₯ β β β£ π‘ = (ββπ₯)})) = ({π₯ β β β£
(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0) β§ π‘ = (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)))} βͺ {π₯ β β β£ ((Β¬
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β¨ (ββπ₯) = 0) β§ π‘ = (ββπ₯))}) |
139 | | eqcom 2744 |
. . . . . . 7
β’
(if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯)) = π‘ β π‘ = if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯))) |
140 | | fvex 6860 |
. . . . . . . . 9
β’ (ββπ₯) β V |
141 | 113, 140 | ifex 4541 |
. . . . . . . 8
β’
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯)) β V |
142 | 141 | elsn 4606 |
. . . . . . 7
β’
(if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯)) β {π‘} β if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯)) = π‘) |
143 | | ianor 981 |
. . . . . . . . . . 11
β’ (Β¬
((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0) β (Β¬
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β¨ Β¬ (ββπ₯) β 0)) |
144 | | nne 2948 |
. . . . . . . . . . . 12
β’ (Β¬
(ββπ₯) β 0 β (ββπ₯) = 0) |
145 | 144 | orbi2i 912 |
. . . . . . . . . . 11
β’ ((Β¬
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β¨ Β¬ (ββπ₯) β 0) β (Β¬
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β¨ (ββπ₯) = 0)) |
146 | 143, 145 | bitr2i 276 |
. . . . . . . . . 10
β’ ((Β¬
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β¨ (ββπ₯) = 0) β Β¬ ((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0)) |
147 | 146 | anbi1i 625 |
. . . . . . . . 9
β’ (((Β¬
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β¨ (ββπ₯) = 0) β§ π‘ = (ββπ₯)) β (Β¬ ((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0) β§ π‘ = (ββπ₯))) |
148 | 147 | orbi2i 912 |
. . . . . . . 8
β’
(((((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0) β§ π‘ = (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3))) β¨ ((Β¬
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β¨ (ββπ₯) = 0) β§ π‘ = (ββπ₯))) β ((((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0) β§ π‘ = (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3))) β¨ (Β¬
((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0) β§ π‘ = (ββπ₯)))) |
149 | | eqif 4532 |
. . . . . . . 8
β’ (π‘ = if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯)) β ((((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0) β§ π‘ = (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3))) β¨ (Β¬
((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0) β§ π‘ = (ββπ₯)))) |
150 | 148, 149 | bitr4i 278 |
. . . . . . 7
β’
(((((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0) β§ π‘ = (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3))) β¨ ((Β¬
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β¨ (ββπ₯) = 0) β§ π‘ = (ββπ₯))) β π‘ = if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯))) |
151 | 139, 142,
150 | 3bitr4i 303 |
. . . . . 6
β’
(if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯)) β {π‘} β ((((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0) β§ π‘ = (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3))) β¨ ((Β¬
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β¨ (ββπ₯) = 0) β§ π‘ = (ββπ₯)))) |
152 | 151 | rabbii 3416 |
. . . . 5
β’ {π₯ β β β£
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯)) β {π‘}} = {π₯ β β β£
((((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0) β§ π‘ = (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3))) β¨ ((Β¬
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β¨ (ββπ₯) = 0) β§ π‘ = (ββπ₯)))} |
153 | 129, 138,
152 | 3eqtr4ri 2776 |
. . . 4
β’ {π₯ β β β£
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯)) β {π‘}} = ((({π₯ β β β£
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)} β© {π₯ β β β£ (ββπ₯) β 0}) β© {π₯ β β β£ π‘ = (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3))}) βͺ (({π₯ β β β£ Β¬
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)} βͺ {π₯ β β β£ (ββπ₯) = 0}) β© {π₯ β β β£ π‘ = (ββπ₯)})) |
154 | 128, 153 | eqtri 2765 |
. . 3
β’ (β‘(π₯ β β β¦
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯))) β {π‘}) = ((({π₯ β β β£
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)} β© {π₯ β β β£ (ββπ₯) β 0}) β© {π₯ β β β£ π‘ = (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3))}) βͺ (({π₯ β β β£ Β¬
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)} βͺ {π₯ β β β£ (ββπ₯) = 0}) β© {π₯ β β β£ π‘ = (ββπ₯)})) |
155 | | eldifi 4091 |
. . . . . 6
β’ (π‘ β (ran (π₯ β β β¦
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯))) β {0}) β π‘ β ran (π₯ β β β¦
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯)))) |
156 | 31 | frnd 6681 |
. . . . . . 7
β’ (((π β§ β β dom β«1) β§ π£ β β+)
β ran (π₯ β
β β¦ if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯))) β β) |
157 | 156 | sseld 3948 |
. . . . . 6
β’ (((π β§ β β dom β«1) β§ π£ β β+)
β (π‘ β ran (π₯ β β β¦
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯))) β π‘ β β)) |
158 | 155, 157 | syl5 34 |
. . . . 5
β’ (((π β§ β β dom β«1) β§ π£ β β+)
β (π‘ β (ran
(π₯ β β β¦
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯))) β {0}) β π‘ β β)) |
159 | 158 | imdistani 570 |
. . . 4
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π‘ β (ran (π₯ β β β¦
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯))) β {0})) β (((π β§ β β dom β«1) β§ π£ β β+)
β§ π‘ β
β)) |
160 | | rabiun 36080 |
. . . . . . . . . 10
β’ {π₯ β βͺ π‘ β ran β(β‘β β {π‘}) β£ (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)} = βͺ
π‘ β ran β{π₯ β (β‘β β {π‘}) β£ (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)} |
161 | | cnvimarndm 6039 |
. . . . . . . . . . . . . 14
β’ (β‘β β ran β) = dom β |
162 | | iunid 5025 |
. . . . . . . . . . . . . . . 16
β’ βͺ π‘ β ran β{π‘} = ran β |
163 | 162 | imaeq2i 6016 |
. . . . . . . . . . . . . . 15
β’ (β‘β β βͺ
π‘ β ran β{π‘}) = (β‘β β ran β) |
164 | | imaiun 7197 |
. . . . . . . . . . . . . . 15
β’ (β‘β β βͺ
π‘ β ran β{π‘}) = βͺ
π‘ β ran β(β‘β β {π‘}) |
165 | 163, 164 | eqtr3i 2767 |
. . . . . . . . . . . . . 14
β’ (β‘β β ran β) = βͺ π‘ β ran β(β‘β β {π‘}) |
166 | 161, 165 | eqtr3i 2767 |
. . . . . . . . . . . . 13
β’ dom β = βͺ π‘ β ran β(β‘β β {π‘}) |
167 | 27 | fdmd 6684 |
. . . . . . . . . . . . 13
β’ (β β dom β«1
β dom β =
β) |
168 | 166, 167 | eqtr3id 2791 |
. . . . . . . . . . . 12
β’ (β β dom β«1
β βͺ π‘ β ran β(β‘β β {π‘}) = β) |
169 | 168 | ad2antlr 726 |
. . . . . . . . . . 11
β’ (((π β§ β β dom β«1) β§ π£ β β+)
β βͺ π‘ β ran β(β‘β β {π‘}) = β) |
170 | | rabeq 3424 |
. . . . . . . . . . 11
β’ (βͺ π‘ β ran β(β‘β β {π‘}) = β β {π₯ β βͺ
π‘ β ran β(β‘β β {π‘}) β£ (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)} = {π₯ β β β£
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)}) |
171 | 169, 170 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ β β dom β«1) β§ π£ β β+)
β {π₯ β βͺ π‘ β ran β(β‘β β {π‘}) β£ (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)} = {π₯ β β β£
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)}) |
172 | 160, 171 | eqtr3id 2791 |
. . . . . . . . 9
β’ (((π β§ β β dom β«1) β§ π£ β β+)
β βͺ π‘ β ran β{π₯ β (β‘β β {π‘}) β£ (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)} = {π₯ β β β£
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)}) |
173 | | fniniseg 7015 |
. . . . . . . . . . . . . . . . . 18
β’ (β Fn β β (π₯ β (β‘β β {π‘}) β (π₯ β β β§ (ββπ₯) = π‘))) |
174 | 27, 82, 173 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
β’ (β β dom β«1
β (π₯ β (β‘β β {π‘}) β (π₯ β β β§ (ββπ₯) = π‘))) |
175 | 174 | simplbda 501 |
. . . . . . . . . . . . . . . 16
β’ ((β β dom β«1
β§ π₯ β (β‘β β {π‘})) β (ββπ₯) = π‘) |
176 | 175 | breq2d 5122 |
. . . . . . . . . . . . . . 15
β’ ((β β dom β«1
β§ π₯ β (β‘β β {π‘})) β ((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ π‘)) |
177 | 176 | rabbidva 3417 |
. . . . . . . . . . . . . 14
β’ (β β dom β«1
β {π₯ β (β‘β β {π‘}) β£ (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)} = {π₯ β (β‘β β {π‘}) β£ (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ π‘}) |
178 | | inrab2 4272 |
. . . . . . . . . . . . . . 15
β’ ({π₯ β β β£
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ π‘} β© (β‘β β {π‘})) = {π₯ β (β β© (β‘β β {π‘})) β£ (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ π‘} |
179 | | imassrn 6029 |
. . . . . . . . . . . . . . . . . 18
β’ (β‘β β {π‘}) β ran β‘β |
180 | | dfdm4 5856 |
. . . . . . . . . . . . . . . . . . 19
β’ dom β = ran β‘β |
181 | 180, 167 | eqtr3id 2791 |
. . . . . . . . . . . . . . . . . 18
β’ (β β dom β«1
β ran β‘β = β) |
182 | 179, 181 | sseqtrid 4001 |
. . . . . . . . . . . . . . . . 17
β’ (β β dom β«1
β (β‘β β {π‘}) β β) |
183 | | sseqin2 4180 |
. . . . . . . . . . . . . . . . 17
β’ ((β‘β β {π‘}) β β β (β β©
(β‘β β {π‘})) = (β‘β β {π‘})) |
184 | 182, 183 | sylib 217 |
. . . . . . . . . . . . . . . 16
β’ (β β dom β«1
β (β β© (β‘β β {π‘})) = (β‘β β {π‘})) |
185 | | rabeq 3424 |
. . . . . . . . . . . . . . . 16
β’ ((β
β© (β‘β β {π‘})) = (β‘β β {π‘}) β {π₯ β (β β© (β‘β β {π‘})) β£ (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ π‘} = {π₯ β (β‘β β {π‘}) β£ (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ π‘}) |
186 | 184, 185 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (β β dom β«1
β {π₯ β (β
β© (β‘β β {π‘})) β£ (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ π‘} = {π₯ β (β‘β β {π‘}) β£ (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ π‘}) |
187 | 178, 186 | eqtrid 2789 |
. . . . . . . . . . . . . 14
β’ (β β dom β«1
β ({π₯ β β
β£ (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ π‘} β© (β‘β β {π‘})) = {π₯ β (β‘β β {π‘}) β£ (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ π‘}) |
188 | 177, 187 | eqtr4d 2780 |
. . . . . . . . . . . . 13
β’ (β β dom β«1
β {π₯ β (β‘β β {π‘}) β£ (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)} = ({π₯ β β β£
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ π‘} β© (β‘β β {π‘}))) |
189 | 188 | ad3antlr 730 |
. . . . . . . . . . . 12
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π‘ β ran β) β {π₯ β (β‘β β {π‘}) β£ (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)} = ({π₯ β β β£
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ π‘} β© (β‘β β {π‘}))) |
190 | 25 | adantlr 714 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β ran β) β§ π₯ β β) β
((ββ((πΉβπ₯) / (π£ / 3))) β 1) β
β) |
191 | 45 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ β β dom β«1) β§ π£ β β+)
β ran β β
β) |
192 | 191 | sselda 3949 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π‘ β ran β) β π‘ β β) |
193 | 192 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β ran β) β§ π₯ β β) β π‘ β β) |
194 | 68 | ad3antlr 730 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β ran β) β§ π₯ β β) β (π£ / 3) β
β+) |
195 | 190, 193,
194 | lemuldivd 13013 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β ran β) β§ π₯ β β) β
((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ π‘ β ((ββ((πΉβπ₯) / (π£ / 3))) β 1) β€ (π‘ / (π£ / 3)))) |
196 | 23 | adantlr 714 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β ran β) β§ π₯ β β) β
(ββ((πΉβπ₯) / (π£ / 3))) β β) |
197 | | 1red 11163 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β ran β) β§ π₯ β β) β 1 β
β) |
198 | 13 | ad3antlr 730 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β ran β) β§ π₯ β β) β (π£ / 3) β β) |
199 | 19 | ad3antlr 730 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β ran β) β§ π₯ β β) β (π£ / 3) β 0) |
200 | 193, 198,
199 | redivcld 11990 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β ran β) β§ π₯ β β) β (π‘ / (π£ / 3)) β β) |
201 | 196, 197,
200 | lesubaddd 11759 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β ran β) β§ π₯ β β) β
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) β€ (π‘ / (π£ / 3)) β (ββ((πΉβπ₯) / (π£ / 3))) β€ ((π‘ / (π£ / 3)) + 1))) |
202 | 6 | adantlr 714 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β ran β) β§ π₯ β β) β (πΉβπ₯) β β) |
203 | | peano2re 11335 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π‘ / (π£ / 3)) β β β ((π‘ / (π£ / 3)) + 1) β β) |
204 | 200, 203 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β ran β) β§ π₯ β β) β ((π‘ / (π£ / 3)) + 1) β β) |
205 | | reflcl 13708 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π‘ / (π£ / 3)) + 1) β β β
(ββ((π‘ / (π£ / 3)) + 1)) β
β) |
206 | 204, 205 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β ran β) β§ π₯ β β) β
(ββ((π‘ / (π£ / 3)) + 1)) β
β) |
207 | | peano2re 11335 |
. . . . . . . . . . . . . . . . . . . 20
β’
((ββ((π‘
/ (π£ / 3)) + 1)) β
β β ((ββ((π‘ / (π£ / 3)) + 1)) + 1) β
β) |
208 | 206, 207 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β ran β) β§ π₯ β β) β
((ββ((π‘ /
(π£ / 3)) + 1)) + 1) β
β) |
209 | 202, 208,
194 | ltdivmuld 13015 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β ran β) β§ π₯ β β) β (((πΉβπ₯) / (π£ / 3)) < ((ββ((π‘ / (π£ / 3)) + 1)) + 1) β (πΉβπ₯) < ((π£ / 3) Β· ((ββ((π‘ / (π£ / 3)) + 1)) + 1)))) |
210 | 21 | adantlr 714 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β ran β) β§ π₯ β β) β ((πΉβπ₯) / (π£ / 3)) β β) |
211 | | flflp1 13719 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((πΉβπ₯) / (π£ / 3)) β β β§ ((π‘ / (π£ / 3)) + 1) β β) β
((ββ((πΉβπ₯) / (π£ / 3))) β€ ((π‘ / (π£ / 3)) + 1) β ((πΉβπ₯) / (π£ / 3)) < ((ββ((π‘ / (π£ / 3)) + 1)) + 1))) |
212 | 210, 204,
211 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β ran β) β§ π₯ β β) β
((ββ((πΉβπ₯) / (π£ / 3))) β€ ((π‘ / (π£ / 3)) + 1) β ((πΉβπ₯) / (π£ / 3)) < ((ββ((π‘ / (π£ / 3)) + 1)) + 1))) |
213 | 198, 208 | remulcld 11192 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β ran β) β§ π₯ β β) β ((π£ / 3) Β· ((ββ((π‘ / (π£ / 3)) + 1)) + 1)) β
β) |
214 | 213 | rexrd 11212 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β ran β) β§ π₯ β β) β ((π£ / 3) Β· ((ββ((π‘ / (π£ / 3)) + 1)) + 1)) β
β*) |
215 | | elioomnf 13368 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π£ / 3) Β·
((ββ((π‘ /
(π£ / 3)) + 1)) + 1)) β
β* β ((πΉβπ₯) β (-β(,)((π£ / 3) Β· ((ββ((π‘ / (π£ / 3)) + 1)) + 1))) β ((πΉβπ₯) β β β§ (πΉβπ₯) < ((π£ / 3) Β· ((ββ((π‘ / (π£ / 3)) + 1)) + 1))))) |
216 | 214, 215 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β ran β) β§ π₯ β β) β ((πΉβπ₯) β (-β(,)((π£ / 3) Β· ((ββ((π‘ / (π£ / 3)) + 1)) + 1))) β ((πΉβπ₯) β β β§ (πΉβπ₯) < ((π£ / 3) Β· ((ββ((π‘ / (π£ / 3)) + 1)) + 1))))) |
217 | 202 | biantrurd 534 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β ran β) β§ π₯ β β) β ((πΉβπ₯) < ((π£ / 3) Β· ((ββ((π‘ / (π£ / 3)) + 1)) + 1)) β ((πΉβπ₯) β β β§ (πΉβπ₯) < ((π£ / 3) Β· ((ββ((π‘ / (π£ / 3)) + 1)) + 1))))) |
218 | 216, 217 | bitr4d 282 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β ran β) β§ π₯ β β) β ((πΉβπ₯) β (-β(,)((π£ / 3) Β· ((ββ((π‘ / (π£ / 3)) + 1)) + 1))) β (πΉβπ₯) < ((π£ / 3) Β· ((ββ((π‘ / (π£ / 3)) + 1)) + 1)))) |
219 | 209, 212,
218 | 3bitr4d 311 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β ran β) β§ π₯ β β) β
((ββ((πΉβπ₯) / (π£ / 3))) β€ ((π‘ / (π£ / 3)) + 1) β (πΉβπ₯) β (-β(,)((π£ / 3) Β· ((ββ((π‘ / (π£ / 3)) + 1)) + 1))))) |
220 | 195, 201,
219 | 3bitrd 305 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β ran β) β§ π₯ β β) β
((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ π‘ β (πΉβπ₯) β (-β(,)((π£ / 3) Β· ((ββ((π‘ / (π£ / 3)) + 1)) + 1))))) |
221 | 220 | rabbidva 3417 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π‘ β ran β) β {π₯ β β β£
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ π‘} = {π₯ β β β£ (πΉβπ₯) β (-β(,)((π£ / 3) Β· ((ββ((π‘ / (π£ / 3)) + 1)) + 1)))}) |
222 | 1 | feqmptd 6915 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β πΉ = (π₯ β β β¦ (πΉβπ₯))) |
223 | 222 | cnveqd 5836 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β‘πΉ = β‘(π₯ β β β¦ (πΉβπ₯))) |
224 | 223 | imaeq1d 6017 |
. . . . . . . . . . . . . . . . 17
β’ (π β (β‘πΉ β (-β(,)((π£ / 3) Β· ((ββ((π‘ / (π£ / 3)) + 1)) + 1)))) = (β‘(π₯ β β β¦ (πΉβπ₯)) β (-β(,)((π£ / 3) Β· ((ββ((π‘ / (π£ / 3)) + 1)) + 1))))) |
225 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β β β¦ (πΉβπ₯)) = (π₯ β β β¦ (πΉβπ₯)) |
226 | 225 | mptpreima 6195 |
. . . . . . . . . . . . . . . . 17
β’ (β‘(π₯ β β β¦ (πΉβπ₯)) β (-β(,)((π£ / 3) Β· ((ββ((π‘ / (π£ / 3)) + 1)) + 1)))) = {π₯ β β β£ (πΉβπ₯) β (-β(,)((π£ / 3) Β· ((ββ((π‘ / (π£ / 3)) + 1)) + 1)))} |
227 | 224, 226 | eqtrdi 2793 |
. . . . . . . . . . . . . . . 16
β’ (π β (β‘πΉ β (-β(,)((π£ / 3) Β· ((ββ((π‘ / (π£ / 3)) + 1)) + 1)))) = {π₯ β β β£ (πΉβπ₯) β (-β(,)((π£ / 3) Β· ((ββ((π‘ / (π£ / 3)) + 1)) + 1)))}) |
228 | 227 | ad3antrrr 729 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π‘ β ran β) β (β‘πΉ β (-β(,)((π£ / 3) Β· ((ββ((π‘ / (π£ / 3)) + 1)) + 1)))) = {π₯ β β β£ (πΉβπ₯) β (-β(,)((π£ / 3) Β· ((ββ((π‘ / (π£ / 3)) + 1)) + 1)))}) |
229 | 221, 228 | eqtr4d 2780 |
. . . . . . . . . . . . . 14
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π‘ β ran β) β {π₯ β β β£
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ π‘} = (β‘πΉ β (-β(,)((π£ / 3) Β· ((ββ((π‘ / (π£ / 3)) + 1)) + 1))))) |
230 | | itg2addnc.f1 |
. . . . . . . . . . . . . . . 16
β’ (π β πΉ β MblFn) |
231 | | mbfima 25010 |
. . . . . . . . . . . . . . . 16
β’ ((πΉ β MblFn β§ πΉ:ββΆβ) β
(β‘πΉ β (-β(,)((π£ / 3) Β· ((ββ((π‘ / (π£ / 3)) + 1)) + 1)))) β dom
vol) |
232 | 230, 4, 231 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (π β (β‘πΉ β (-β(,)((π£ / 3) Β· ((ββ((π‘ / (π£ / 3)) + 1)) + 1)))) β dom
vol) |
233 | 232 | ad3antrrr 729 |
. . . . . . . . . . . . . 14
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π‘ β ran β) β (β‘πΉ β (-β(,)((π£ / 3) Β· ((ββ((π‘ / (π£ / 3)) + 1)) + 1)))) β dom
vol) |
234 | 229, 233 | eqeltrd 2838 |
. . . . . . . . . . . . 13
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π‘ β ran β) β {π₯ β β β£
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ π‘} β dom vol) |
235 | 45 | sseld 3948 |
. . . . . . . . . . . . . . . 16
β’ (β β dom β«1
β (π‘ β ran β β π‘ β β)) |
236 | 235 | ad2antlr 726 |
. . . . . . . . . . . . . . 15
β’ (((π β§ β β dom β«1) β§ π£ β β+)
β (π‘ β ran β β π‘ β β)) |
237 | 236 | imdistani 570 |
. . . . . . . . . . . . . 14
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π‘ β ran β) β (((π β§ β β dom β«1) β§ π£ β β+)
β§ π‘ β
β)) |
238 | | i1fmbf 25055 |
. . . . . . . . . . . . . . . . 17
β’ (β β dom β«1
β β β
MblFn) |
239 | 238, 27 | jca 513 |
. . . . . . . . . . . . . . . 16
β’ (β β dom β«1
β (β β MblFn β§
β:ββΆβ)) |
240 | 239 | ad2antlr 726 |
. . . . . . . . . . . . . . 15
β’ (((π β§ β β dom β«1) β§ π£ β β+)
β (β β MblFn β§
β:ββΆβ)) |
241 | | mbfimasn 25012 |
. . . . . . . . . . . . . . . 16
β’ ((β β MblFn β§ β:ββΆβ β§
π‘ β β) β
(β‘β β {π‘}) β dom vol) |
242 | 241 | 3expa 1119 |
. . . . . . . . . . . . . . 15
β’ (((β β MblFn β§ β:ββΆβ) β§
π‘ β β) β
(β‘β β {π‘}) β dom vol) |
243 | 240, 242 | sylan 581 |
. . . . . . . . . . . . . 14
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π‘ β β)
β (β‘β β {π‘}) β dom vol) |
244 | 237, 243 | syl 17 |
. . . . . . . . . . . . 13
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π‘ β ran β) β (β‘β β {π‘}) β dom vol) |
245 | | inmbl 24922 |
. . . . . . . . . . . . 13
β’ (({π₯ β β β£
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ π‘} β dom vol β§ (β‘β β {π‘}) β dom vol) β ({π₯ β β β£
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ π‘} β© (β‘β β {π‘})) β dom vol) |
246 | 234, 244,
245 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π‘ β ran β) β ({π₯ β β β£
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ π‘} β© (β‘β β {π‘})) β dom vol) |
247 | 189, 246 | eqeltrd 2838 |
. . . . . . . . . . 11
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π‘ β ran β) β {π₯ β (β‘β β {π‘}) β£ (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)} β dom vol) |
248 | 247 | ralrimiva 3144 |
. . . . . . . . . 10
β’ (((π β§ β β dom β«1) β§ π£ β β+)
β βπ‘ β ran
β{π₯ β (β‘β β {π‘}) β£ (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)} β dom vol) |
249 | | finiunmbl 24924 |
. . . . . . . . . 10
β’ ((ran
β β Fin β§
βπ‘ β ran β{π₯ β (β‘β β {π‘}) β£ (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)} β dom vol) β βͺ π‘ β ran β{π₯ β (β‘β β {π‘}) β£ (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)} β dom vol) |
250 | 41, 248, 249 | syl2anc 585 |
. . . . . . . . 9
β’ (((π β§ β β dom β«1) β§ π£ β β+)
β βͺ π‘ β ran β{π₯ β (β‘β β {π‘}) β£ (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)} β dom vol) |
251 | 172, 250 | eqeltrrd 2839 |
. . . . . . . 8
β’ (((π β§ β β dom β«1) β§ π£ β β+)
β {π₯ β β
β£ (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)} β dom vol) |
252 | | unrab 4270 |
. . . . . . . . . . 11
β’ ({π₯ β β β£ (ββπ₯) β (-β(,)0)} βͺ {π₯ β β β£ (ββπ₯) β (0(,)+β)}) = {π₯ β β β£ ((ββπ₯) β (-β(,)0) β¨ (ββπ₯) β (0(,)+β))} |
253 | 27 | feqmptd 6915 |
. . . . . . . . . . . . . . 15
β’ (β β dom β«1
β β = (π₯ β β β¦ (ββπ₯))) |
254 | 253 | cnveqd 5836 |
. . . . . . . . . . . . . 14
β’ (β β dom β«1
β β‘β = β‘(π₯ β β β¦ (ββπ₯))) |
255 | 254 | imaeq1d 6017 |
. . . . . . . . . . . . 13
β’ (β β dom β«1
β (β‘β β (-β(,)0)) = (β‘(π₯ β β β¦ (ββπ₯)) β (-β(,)0))) |
256 | | eqid 2737 |
. . . . . . . . . . . . . 14
β’ (π₯ β β β¦ (ββπ₯)) = (π₯ β β β¦ (ββπ₯)) |
257 | 256 | mptpreima 6195 |
. . . . . . . . . . . . 13
β’ (β‘(π₯ β β β¦ (ββπ₯)) β (-β(,)0)) = {π₯ β β β£ (ββπ₯) β (-β(,)0)} |
258 | 255, 257 | eqtrdi 2793 |
. . . . . . . . . . . 12
β’ (β β dom β«1
β (β‘β β (-β(,)0)) = {π₯ β β β£ (ββπ₯) β (-β(,)0)}) |
259 | 254 | imaeq1d 6017 |
. . . . . . . . . . . . 13
β’ (β β dom β«1
β (β‘β β (0(,)+β)) = (β‘(π₯ β β β¦ (ββπ₯)) β (0(,)+β))) |
260 | 256 | mptpreima 6195 |
. . . . . . . . . . . . 13
β’ (β‘(π₯ β β β¦ (ββπ₯)) β (0(,)+β)) = {π₯ β β β£ (ββπ₯) β (0(,)+β)} |
261 | 259, 260 | eqtrdi 2793 |
. . . . . . . . . . . 12
β’ (β β dom β«1
β (β‘β β (0(,)+β)) = {π₯ β β β£ (ββπ₯) β (0(,)+β)}) |
262 | 258, 261 | uneq12d 4129 |
. . . . . . . . . . 11
β’ (β β dom β«1
β ((β‘β β (-β(,)0)) βͺ (β‘β β (0(,)+β))) = ({π₯ β β β£ (ββπ₯) β (-β(,)0)} βͺ {π₯ β β β£ (ββπ₯) β (0(,)+β)})) |
263 | 27 | ffvelcdmda 7040 |
. . . . . . . . . . . . 13
β’ ((β β dom β«1
β§ π₯ β β)
β (ββπ₯) β
β) |
264 | | 0re 11164 |
. . . . . . . . . . . . . . 15
β’ 0 β
β |
265 | | lttri2 11244 |
. . . . . . . . . . . . . . 15
β’ (((ββπ₯) β β β§ 0 β β)
β ((ββπ₯) β 0 β ((ββπ₯) < 0 β¨ 0 < (ββπ₯)))) |
266 | 264, 265 | mpan2 690 |
. . . . . . . . . . . . . 14
β’ ((ββπ₯) β β β ((ββπ₯) β 0 β ((ββπ₯) < 0 β¨ 0 < (ββπ₯)))) |
267 | | ibar 530 |
. . . . . . . . . . . . . . 15
β’ ((ββπ₯) β β β (((ββπ₯) < 0 β¨ 0 < (ββπ₯)) β ((ββπ₯) β β β§ ((ββπ₯) < 0 β¨ 0 < (ββπ₯))))) |
268 | | andi 1007 |
. . . . . . . . . . . . . . . 16
β’ (((ββπ₯) β β β§ ((ββπ₯) < 0 β¨ 0 < (ββπ₯))) β (((ββπ₯) β β β§ (ββπ₯) < 0) β¨ ((ββπ₯) β β β§ 0 < (ββπ₯)))) |
269 | | 0xr 11209 |
. . . . . . . . . . . . . . . . 17
β’ 0 β
β* |
270 | | elioomnf 13368 |
. . . . . . . . . . . . . . . . . 18
β’ (0 β
β* β ((ββπ₯) β (-β(,)0) β ((ββπ₯) β β β§ (ββπ₯) < 0))) |
271 | | elioopnf 13367 |
. . . . . . . . . . . . . . . . . 18
β’ (0 β
β* β ((ββπ₯) β (0(,)+β) β ((ββπ₯) β β β§ 0 < (ββπ₯)))) |
272 | 270, 271 | orbi12d 918 |
. . . . . . . . . . . . . . . . 17
β’ (0 β
β* β (((ββπ₯) β (-β(,)0) β¨ (ββπ₯) β (0(,)+β)) β (((ββπ₯) β β β§ (ββπ₯) < 0) β¨ ((ββπ₯) β β β§ 0 < (ββπ₯))))) |
273 | 269, 272 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
β’ (((ββπ₯) β (-β(,)0) β¨ (ββπ₯) β (0(,)+β)) β (((ββπ₯) β β β§ (ββπ₯) < 0) β¨ ((ββπ₯) β β β§ 0 < (ββπ₯)))) |
274 | 268, 273 | bitr4i 278 |
. . . . . . . . . . . . . . 15
β’ (((ββπ₯) β β β§ ((ββπ₯) < 0 β¨ 0 < (ββπ₯))) β ((ββπ₯) β (-β(,)0) β¨ (ββπ₯) β (0(,)+β))) |
275 | 267, 274 | bitrdi 287 |
. . . . . . . . . . . . . 14
β’ ((ββπ₯) β β β (((ββπ₯) < 0 β¨ 0 < (ββπ₯)) β ((ββπ₯) β (-β(,)0) β¨ (ββπ₯) β (0(,)+β)))) |
276 | 266, 275 | bitrd 279 |
. . . . . . . . . . . . 13
β’ ((ββπ₯) β β β ((ββπ₯) β 0 β ((ββπ₯) β (-β(,)0) β¨ (ββπ₯) β (0(,)+β)))) |
277 | 263, 276 | syl 17 |
. . . . . . . . . . . 12
β’ ((β β dom β«1
β§ π₯ β β)
β ((ββπ₯) β 0 β ((ββπ₯) β (-β(,)0) β¨ (ββπ₯) β (0(,)+β)))) |
278 | 277 | rabbidva 3417 |
. . . . . . . . . . 11
β’ (β β dom β«1
β {π₯ β β
β£ (ββπ₯) β 0} = {π₯ β β β£ ((ββπ₯) β (-β(,)0) β¨ (ββπ₯) β (0(,)+β))}) |
279 | 252, 262,
278 | 3eqtr4a 2803 |
. . . . . . . . . 10
β’ (β β dom β«1
β ((β‘β β (-β(,)0)) βͺ (β‘β β (0(,)+β))) = {π₯ β β β£ (ββπ₯) β 0}) |
280 | | i1fima 25058 |
. . . . . . . . . . 11
β’ (β β dom β«1
β (β‘β β (-β(,)0)) β dom
vol) |
281 | | i1fima 25058 |
. . . . . . . . . . 11
β’ (β β dom β«1
β (β‘β β (0(,)+β)) β dom
vol) |
282 | | unmbl 24917 |
. . . . . . . . . . 11
β’ (((β‘β β (-β(,)0)) β dom vol β§
(β‘β β (0(,)+β)) β dom vol)
β ((β‘β β (-β(,)0)) βͺ (β‘β β (0(,)+β))) β dom
vol) |
283 | 280, 281,
282 | syl2anc 585 |
. . . . . . . . . 10
β’ (β β dom β«1
β ((β‘β β (-β(,)0)) βͺ (β‘β β (0(,)+β))) β dom
vol) |
284 | 279, 283 | eqeltrrd 2839 |
. . . . . . . . 9
β’ (β β dom β«1
β {π₯ β β
β£ (ββπ₯) β 0} β dom
vol) |
285 | 284 | ad2antlr 726 |
. . . . . . . 8
β’ (((π β§ β β dom β«1) β§ π£ β β+)
β {π₯ β β
β£ (ββπ₯) β 0} β dom
vol) |
286 | | inmbl 24922 |
. . . . . . . 8
β’ (({π₯ β β β£
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)} β dom vol β§ {π₯ β β β£ (ββπ₯) β 0} β dom vol) β ({π₯ β β β£
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)} β© {π₯ β β β£ (ββπ₯) β 0}) β dom vol) |
287 | 251, 285,
286 | syl2anc 585 |
. . . . . . 7
β’ (((π β§ β β dom β«1) β§ π£ β β+)
β ({π₯ β β
β£ (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)} β© {π₯ β β β£ (ββπ₯) β 0}) β dom vol) |
288 | 287 | adantr 482 |
. . . . . 6
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π‘ β β)
β ({π₯ β β
β£ (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)} β© {π₯ β β β£ (ββπ₯) β 0}) β dom vol) |
289 | 23 | recnd 11190 |
. . . . . . . . . . 11
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π₯ β β)
β (ββ((πΉβπ₯) / (π£ / 3))) β β) |
290 | 289 | adantlr 714 |
. . . . . . . . . 10
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ π₯ β β) β
(ββ((πΉβπ₯) / (π£ / 3))) β β) |
291 | | 1cnd 11157 |
. . . . . . . . . 10
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ π₯ β β) β 1 β
β) |
292 | | simplr 768 |
. . . . . . . . . . . 12
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ π₯ β β) β π‘ β β) |
293 | 13 | ad3antlr 730 |
. . . . . . . . . . . 12
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ π₯ β β) β (π£ / 3) β β) |
294 | 19 | ad3antlr 730 |
. . . . . . . . . . . 12
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ π₯ β β) β (π£ / 3) β 0) |
295 | 292, 293,
294 | redivcld 11990 |
. . . . . . . . . . 11
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ π₯ β β) β (π‘ / (π£ / 3)) β β) |
296 | 295 | recnd 11190 |
. . . . . . . . . 10
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ π₯ β β) β (π‘ / (π£ / 3)) β β) |
297 | 290, 291,
296 | subadd2d 11538 |
. . . . . . . . 9
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ π₯ β β) β
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) = (π‘ / (π£ / 3)) β ((π‘ / (π£ / 3)) + 1) = (ββ((πΉβπ₯) / (π£ / 3))))) |
298 | | eqcom 2744 |
. . . . . . . . . 10
β’
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) = (π‘ / (π£ / 3)) β (π‘ / (π£ / 3)) = ((ββ((πΉβπ₯) / (π£ / 3))) β 1)) |
299 | | recn 11148 |
. . . . . . . . . . . 12
β’ (π‘ β β β π‘ β
β) |
300 | 299 | ad2antlr 726 |
. . . . . . . . . . 11
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ π₯ β β) β π‘ β β) |
301 | 25 | recnd 11190 |
. . . . . . . . . . . 12
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π₯ β β)
β ((ββ((πΉβπ₯) / (π£ / 3))) β 1) β
β) |
302 | 301 | adantlr 714 |
. . . . . . . . . . 11
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ π₯ β β) β
((ββ((πΉβπ₯) / (π£ / 3))) β 1) β
β) |
303 | 13 | recnd 11190 |
. . . . . . . . . . . 12
β’ (π£ β β+
β (π£ / 3) β
β) |
304 | 303 | ad3antlr 730 |
. . . . . . . . . . 11
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ π₯ β β) β (π£ / 3) β β) |
305 | 300, 302,
304, 294 | divmul3d 11972 |
. . . . . . . . . 10
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ π₯ β β) β ((π‘ / (π£ / 3)) = ((ββ((πΉβπ₯) / (π£ / 3))) β 1) β π‘ = (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)))) |
306 | 298, 305 | bitrid 283 |
. . . . . . . . 9
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ π₯ β β) β
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) = (π‘ / (π£ / 3)) β π‘ = (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)))) |
307 | 297, 306 | bitr3d 281 |
. . . . . . . 8
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ π₯ β β) β (((π‘ / (π£ / 3)) + 1) = (ββ((πΉβπ₯) / (π£ / 3))) β π‘ = (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)))) |
308 | 307 | rabbidva 3417 |
. . . . . . 7
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π‘ β β)
β {π₯ β β
β£ ((π‘ / (π£ / 3)) + 1) =
(ββ((πΉβπ₯) / (π£ / 3)))} = {π₯ β β β£ π‘ = (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3))}) |
309 | | imaundi 6107 |
. . . . . . . . . . 11
β’ (β‘πΉ β ({(((π‘ / (π£ / 3)) + 1) Β· (π£ / 3))} βͺ ((((π‘ / (π£ / 3)) + 1) Β· (π£ / 3))(,)((π£ / 3) Β· (((π‘ / (π£ / 3)) + 1) + 1))))) = ((β‘πΉ β {(((π‘ / (π£ / 3)) + 1) Β· (π£ / 3))}) βͺ (β‘πΉ β ((((π‘ / (π£ / 3)) + 1) Β· (π£ / 3))(,)((π£ / 3) Β· (((π‘ / (π£ / 3)) + 1) + 1))))) |
310 | 223 | ad4antr 731 |
. . . . . . . . . . . 12
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ ((π‘ / (π£ / 3)) + 1) β β€) β β‘πΉ = β‘(π₯ β β β¦ (πΉβπ₯))) |
311 | | zre 12510 |
. . . . . . . . . . . . . . . 16
β’ (((π‘ / (π£ / 3)) + 1) β β€ β ((π‘ / (π£ / 3)) + 1) β β) |
312 | 311 | adantl 483 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ ((π‘ / (π£ / 3)) + 1) β β€) β ((π‘ / (π£ / 3)) + 1) β β) |
313 | 13 | ad3antlr 730 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ ((π‘ / (π£ / 3)) + 1) β β€) β (π£ / 3) β
β) |
314 | 312, 313 | remulcld 11192 |
. . . . . . . . . . . . . 14
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ ((π‘ / (π£ / 3)) + 1) β β€) β (((π‘ / (π£ / 3)) + 1) Β· (π£ / 3)) β β) |
315 | 314 | rexrd 11212 |
. . . . . . . . . . . . 13
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ ((π‘ / (π£ / 3)) + 1) β β€) β (((π‘ / (π£ / 3)) + 1) Β· (π£ / 3)) β
β*) |
316 | | peano2z 12551 |
. . . . . . . . . . . . . . . . 17
β’ (((π‘ / (π£ / 3)) + 1) β β€ β (((π‘ / (π£ / 3)) + 1) + 1) β
β€) |
317 | 316 | zred 12614 |
. . . . . . . . . . . . . . . 16
β’ (((π‘ / (π£ / 3)) + 1) β β€ β (((π‘ / (π£ / 3)) + 1) + 1) β
β) |
318 | 317 | adantl 483 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ ((π‘ / (π£ / 3)) + 1) β β€) β (((π‘ / (π£ / 3)) + 1) + 1) β
β) |
319 | 313, 318 | remulcld 11192 |
. . . . . . . . . . . . . 14
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ ((π‘ / (π£ / 3)) + 1) β β€) β ((π£ / 3) Β· (((π‘ / (π£ / 3)) + 1) + 1)) β
β) |
320 | 319 | rexrd 11212 |
. . . . . . . . . . . . 13
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ ((π‘ / (π£ / 3)) + 1) β β€) β ((π£ / 3) Β· (((π‘ / (π£ / 3)) + 1) + 1)) β
β*) |
321 | | zcn 12511 |
. . . . . . . . . . . . . . . 16
β’ (((π‘ / (π£ / 3)) + 1) β β€ β ((π‘ / (π£ / 3)) + 1) β β) |
322 | 321 | adantl 483 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ ((π‘ / (π£ / 3)) + 1) β β€) β ((π‘ / (π£ / 3)) + 1) β β) |
323 | 303 | ad3antlr 730 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ ((π‘ / (π£ / 3)) + 1) β β€) β (π£ / 3) β
β) |
324 | 322, 323 | mulcomd 11183 |
. . . . . . . . . . . . . 14
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ ((π‘ / (π£ / 3)) + 1) β β€) β (((π‘ / (π£ / 3)) + 1) Β· (π£ / 3)) = ((π£ / 3) Β· ((π‘ / (π£ / 3)) + 1))) |
325 | 68 | ad3antlr 730 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ ((π‘ / (π£ / 3)) + 1) β β€) β (π£ / 3) β
β+) |
326 | 311 | ltp1d 12092 |
. . . . . . . . . . . . . . . 16
β’ (((π‘ / (π£ / 3)) + 1) β β€ β ((π‘ / (π£ / 3)) + 1) < (((π‘ / (π£ / 3)) + 1) + 1)) |
327 | 326 | adantl 483 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ ((π‘ / (π£ / 3)) + 1) β β€) β ((π‘ / (π£ / 3)) + 1) < (((π‘ / (π£ / 3)) + 1) + 1)) |
328 | 312, 318,
325, 327 | ltmul2dd 13020 |
. . . . . . . . . . . . . 14
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ ((π‘ / (π£ / 3)) + 1) β β€) β ((π£ / 3) Β· ((π‘ / (π£ / 3)) + 1)) < ((π£ / 3) Β· (((π‘ / (π£ / 3)) + 1) + 1))) |
329 | 324, 328 | eqbrtrd 5132 |
. . . . . . . . . . . . 13
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ ((π‘ / (π£ / 3)) + 1) β β€) β (((π‘ / (π£ / 3)) + 1) Β· (π£ / 3)) < ((π£ / 3) Β· (((π‘ / (π£ / 3)) + 1) + 1))) |
330 | | snunioo 13402 |
. . . . . . . . . . . . 13
β’
(((((π‘ / (π£ / 3)) + 1) Β· (π£ / 3)) β
β* β§ ((π£ / 3) Β· (((π‘ / (π£ / 3)) + 1) + 1)) β β*
β§ (((π‘ / (π£ / 3)) + 1) Β· (π£ / 3)) < ((π£ / 3) Β· (((π‘ / (π£ / 3)) + 1) + 1))) β ({(((π‘ / (π£ / 3)) + 1) Β· (π£ / 3))} βͺ ((((π‘ / (π£ / 3)) + 1) Β· (π£ / 3))(,)((π£ / 3) Β· (((π‘ / (π£ / 3)) + 1) + 1)))) = ((((π‘ / (π£ / 3)) + 1) Β· (π£ / 3))[,)((π£ / 3) Β· (((π‘ / (π£ / 3)) + 1) + 1)))) |
331 | 315, 320,
329, 330 | syl3anc 1372 |
. . . . . . . . . . . 12
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ ((π‘ / (π£ / 3)) + 1) β β€) β ({(((π‘ / (π£ / 3)) + 1) Β· (π£ / 3))} βͺ ((((π‘ / (π£ / 3)) + 1) Β· (π£ / 3))(,)((π£ / 3) Β· (((π‘ / (π£ / 3)) + 1) + 1)))) = ((((π‘ / (π£ / 3)) + 1) Β· (π£ / 3))[,)((π£ / 3) Β· (((π‘ / (π£ / 3)) + 1) + 1)))) |
332 | 310, 331 | imaeq12d 6019 |
. . . . . . . . . . 11
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ ((π‘ / (π£ / 3)) + 1) β β€) β (β‘πΉ β ({(((π‘ / (π£ / 3)) + 1) Β· (π£ / 3))} βͺ ((((π‘ / (π£ / 3)) + 1) Β· (π£ / 3))(,)((π£ / 3) Β· (((π‘ / (π£ / 3)) + 1) + 1))))) = (β‘(π₯ β β β¦ (πΉβπ₯)) β ((((π‘ / (π£ / 3)) + 1) Β· (π£ / 3))[,)((π£ / 3) Β· (((π‘ / (π£ / 3)) + 1) + 1))))) |
333 | 309, 332 | eqtr3id 2791 |
. . . . . . . . . 10
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ ((π‘ / (π£ / 3)) + 1) β β€) β ((β‘πΉ β {(((π‘ / (π£ / 3)) + 1) Β· (π£ / 3))}) βͺ (β‘πΉ β ((((π‘ / (π£ / 3)) + 1) Β· (π£ / 3))(,)((π£ / 3) Β· (((π‘ / (π£ / 3)) + 1) + 1))))) = (β‘(π₯ β β β¦ (πΉβπ₯)) β ((((π‘ / (π£ / 3)) + 1) Β· (π£ / 3))[,)((π£ / 3) Β· (((π‘ / (π£ / 3)) + 1) + 1))))) |
334 | 225 | mptpreima 6195 |
. . . . . . . . . . 11
β’ (β‘(π₯ β β β¦ (πΉβπ₯)) β ((((π‘ / (π£ / 3)) + 1) Β· (π£ / 3))[,)((π£ / 3) Β· (((π‘ / (π£ / 3)) + 1) + 1)))) = {π₯ β β β£ (πΉβπ₯) β ((((π‘ / (π£ / 3)) + 1) Β· (π£ / 3))[,)((π£ / 3) Β· (((π‘ / (π£ / 3)) + 1) + 1)))} |
335 | 4 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π‘ β β)
β πΉ:ββΆβ) |
336 | 335 | ffvelcdmda 7040 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ π₯ β β) β (πΉβπ₯) β β) |
337 | 336 | 3biant1d 1479 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ π₯ β β) β (((((π‘ / (π£ / 3)) + 1) Β· (π£ / 3)) β€ (πΉβπ₯) β§ (πΉβπ₯) < ((π£ / 3) Β· (((π‘ / (π£ / 3)) + 1) + 1))) β ((πΉβπ₯) β β β§ (((π‘ / (π£ / 3)) + 1) Β· (π£ / 3)) β€ (πΉβπ₯) β§ (πΉβπ₯) < ((π£ / 3) Β· (((π‘ / (π£ / 3)) + 1) + 1))))) |
338 | 337 | adantr 482 |
. . . . . . . . . . . . . . 15
β’
((((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ π₯ β β) β§ ((π‘ / (π£ / 3)) + 1) β β€) β (((((π‘ / (π£ / 3)) + 1) Β· (π£ / 3)) β€ (πΉβπ₯) β§ (πΉβπ₯) < ((π£ / 3) Β· (((π‘ / (π£ / 3)) + 1) + 1))) β ((πΉβπ₯) β β β§ (((π‘ / (π£ / 3)) + 1) Β· (π£ / 3)) β€ (πΉβπ₯) β§ (πΉβπ₯) < ((π£ / 3) Β· (((π‘ / (π£ / 3)) + 1) + 1))))) |
339 | 311 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’
((((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ π₯ β β) β§ ((π‘ / (π£ / 3)) + 1) β β€) β ((π‘ / (π£ / 3)) + 1) β β) |
340 | 336 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’
((((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ π₯ β β) β§ ((π‘ / (π£ / 3)) + 1) β β€) β (πΉβπ₯) β β) |
341 | 68 | ad4antlr 732 |
. . . . . . . . . . . . . . . . 17
β’
((((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ π₯ β β) β§ ((π‘ / (π£ / 3)) + 1) β β€) β (π£ / 3) β
β+) |
342 | 339, 340,
341 | lemuldivd 13013 |
. . . . . . . . . . . . . . . 16
β’
((((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ π₯ β β) β§ ((π‘ / (π£ / 3)) + 1) β β€) β ((((π‘ / (π£ / 3)) + 1) Β· (π£ / 3)) β€ (πΉβπ₯) β ((π‘ / (π£ / 3)) + 1) β€ ((πΉβπ₯) / (π£ / 3)))) |
343 | 317 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’
((((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ π₯ β β) β§ ((π‘ / (π£ / 3)) + 1) β β€) β (((π‘ / (π£ / 3)) + 1) + 1) β
β) |
344 | 340, 343,
341 | ltdivmuld 13015 |
. . . . . . . . . . . . . . . . 17
β’
((((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ π₯ β β) β§ ((π‘ / (π£ / 3)) + 1) β β€) β (((πΉβπ₯) / (π£ / 3)) < (((π‘ / (π£ / 3)) + 1) + 1) β (πΉβπ₯) < ((π£ / 3) Β· (((π‘ / (π£ / 3)) + 1) + 1)))) |
345 | 344 | bicomd 222 |
. . . . . . . . . . . . . . . 16
β’
((((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ π₯ β β) β§ ((π‘ / (π£ / 3)) + 1) β β€) β ((πΉβπ₯) < ((π£ / 3) Β· (((π‘ / (π£ / 3)) + 1) + 1)) β ((πΉβπ₯) / (π£ / 3)) < (((π‘ / (π£ / 3)) + 1) + 1))) |
346 | 342, 345 | anbi12d 632 |
. . . . . . . . . . . . . . 15
β’
((((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ π₯ β β) β§ ((π‘ / (π£ / 3)) + 1) β β€) β (((((π‘ / (π£ / 3)) + 1) Β· (π£ / 3)) β€ (πΉβπ₯) β§ (πΉβπ₯) < ((π£ / 3) Β· (((π‘ / (π£ / 3)) + 1) + 1))) β (((π‘ / (π£ / 3)) + 1) β€ ((πΉβπ₯) / (π£ / 3)) β§ ((πΉβπ₯) / (π£ / 3)) < (((π‘ / (π£ / 3)) + 1) + 1)))) |
347 | 338, 346 | bitr3d 281 |
. . . . . . . . . . . . . 14
β’
((((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ π₯ β β) β§ ((π‘ / (π£ / 3)) + 1) β β€) β (((πΉβπ₯) β β β§ (((π‘ / (π£ / 3)) + 1) Β· (π£ / 3)) β€ (πΉβπ₯) β§ (πΉβπ₯) < ((π£ / 3) Β· (((π‘ / (π£ / 3)) + 1) + 1))) β (((π‘ / (π£ / 3)) + 1) β€ ((πΉβπ₯) / (π£ / 3)) β§ ((πΉβπ₯) / (π£ / 3)) < (((π‘ / (π£ / 3)) + 1) + 1)))) |
348 | | elico2 13335 |
. . . . . . . . . . . . . . . 16
β’
(((((π‘ / (π£ / 3)) + 1) Β· (π£ / 3)) β β β§
((π£ / 3) Β· (((π‘ / (π£ / 3)) + 1) + 1)) β β*)
β ((πΉβπ₯) β ((((π‘ / (π£ / 3)) + 1) Β· (π£ / 3))[,)((π£ / 3) Β· (((π‘ / (π£ / 3)) + 1) + 1))) β ((πΉβπ₯) β β β§ (((π‘ / (π£ / 3)) + 1) Β· (π£ / 3)) β€ (πΉβπ₯) β§ (πΉβπ₯) < ((π£ / 3) Β· (((π‘ / (π£ / 3)) + 1) + 1))))) |
349 | 314, 320,
348 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ ((π‘ / (π£ / 3)) + 1) β β€) β ((πΉβπ₯) β ((((π‘ / (π£ / 3)) + 1) Β· (π£ / 3))[,)((π£ / 3) Β· (((π‘ / (π£ / 3)) + 1) + 1))) β ((πΉβπ₯) β β β§ (((π‘ / (π£ / 3)) + 1) Β· (π£ / 3)) β€ (πΉβπ₯) β§ (πΉβπ₯) < ((π£ / 3) Β· (((π‘ / (π£ / 3)) + 1) + 1))))) |
350 | 349 | adantlr 714 |
. . . . . . . . . . . . . 14
β’
((((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ π₯ β β) β§ ((π‘ / (π£ / 3)) + 1) β β€) β ((πΉβπ₯) β ((((π‘ / (π£ / 3)) + 1) Β· (π£ / 3))[,)((π£ / 3) Β· (((π‘ / (π£ / 3)) + 1) + 1))) β ((πΉβπ₯) β β β§ (((π‘ / (π£ / 3)) + 1) Β· (π£ / 3)) β€ (πΉβπ₯) β§ (πΉβπ₯) < ((π£ / 3) Β· (((π‘ / (π£ / 3)) + 1) + 1))))) |
351 | | eqcom 2744 |
. . . . . . . . . . . . . . 15
β’ (((π‘ / (π£ / 3)) + 1) = (ββ((πΉβπ₯) / (π£ / 3))) β (ββ((πΉβπ₯) / (π£ / 3))) = ((π‘ / (π£ / 3)) + 1)) |
352 | 21 | adantlr 714 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ π₯ β β) β ((πΉβπ₯) / (π£ / 3)) β β) |
353 | | flbi 13728 |
. . . . . . . . . . . . . . . 16
β’ ((((πΉβπ₯) / (π£ / 3)) β β β§ ((π‘ / (π£ / 3)) + 1) β β€) β
((ββ((πΉβπ₯) / (π£ / 3))) = ((π‘ / (π£ / 3)) + 1) β (((π‘ / (π£ / 3)) + 1) β€ ((πΉβπ₯) / (π£ / 3)) β§ ((πΉβπ₯) / (π£ / 3)) < (((π‘ / (π£ / 3)) + 1) + 1)))) |
354 | 352, 353 | sylan 581 |
. . . . . . . . . . . . . . 15
β’
((((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ π₯ β β) β§ ((π‘ / (π£ / 3)) + 1) β β€) β
((ββ((πΉβπ₯) / (π£ / 3))) = ((π‘ / (π£ / 3)) + 1) β (((π‘ / (π£ / 3)) + 1) β€ ((πΉβπ₯) / (π£ / 3)) β§ ((πΉβπ₯) / (π£ / 3)) < (((π‘ / (π£ / 3)) + 1) + 1)))) |
355 | 351, 354 | bitrid 283 |
. . . . . . . . . . . . . 14
β’
((((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ π₯ β β) β§ ((π‘ / (π£ / 3)) + 1) β β€) β (((π‘ / (π£ / 3)) + 1) = (ββ((πΉβπ₯) / (π£ / 3))) β (((π‘ / (π£ / 3)) + 1) β€ ((πΉβπ₯) / (π£ / 3)) β§ ((πΉβπ₯) / (π£ / 3)) < (((π‘ / (π£ / 3)) + 1) + 1)))) |
356 | 347, 350,
355 | 3bitr4d 311 |
. . . . . . . . . . . . 13
β’
((((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ π₯ β β) β§ ((π‘ / (π£ / 3)) + 1) β β€) β ((πΉβπ₯) β ((((π‘ / (π£ / 3)) + 1) Β· (π£ / 3))[,)((π£ / 3) Β· (((π‘ / (π£ / 3)) + 1) + 1))) β ((π‘ / (π£ / 3)) + 1) = (ββ((πΉβπ₯) / (π£ / 3))))) |
357 | 356 | an32s 651 |
. . . . . . . . . . . 12
β’
((((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ ((π‘ / (π£ / 3)) + 1) β β€) β§ π₯ β β) β ((πΉβπ₯) β ((((π‘ / (π£ / 3)) + 1) Β· (π£ / 3))[,)((π£ / 3) Β· (((π‘ / (π£ / 3)) + 1) + 1))) β ((π‘ / (π£ / 3)) + 1) = (ββ((πΉβπ₯) / (π£ / 3))))) |
358 | 357 | rabbidva 3417 |
. . . . . . . . . . 11
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ ((π‘ / (π£ / 3)) + 1) β β€) β {π₯ β β β£ (πΉβπ₯) β ((((π‘ / (π£ / 3)) + 1) Β· (π£ / 3))[,)((π£ / 3) Β· (((π‘ / (π£ / 3)) + 1) + 1)))} = {π₯ β β β£ ((π‘ / (π£ / 3)) + 1) = (ββ((πΉβπ₯) / (π£ / 3)))}) |
359 | 334, 358 | eqtrid 2789 |
. . . . . . . . . 10
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ ((π‘ / (π£ / 3)) + 1) β β€) β (β‘(π₯ β β β¦ (πΉβπ₯)) β ((((π‘ / (π£ / 3)) + 1) Β· (π£ / 3))[,)((π£ / 3) Β· (((π‘ / (π£ / 3)) + 1) + 1)))) = {π₯ β β β£ ((π‘ / (π£ / 3)) + 1) = (ββ((πΉβπ₯) / (π£ / 3)))}) |
360 | 333, 359 | eqtrd 2777 |
. . . . . . . . 9
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ ((π‘ / (π£ / 3)) + 1) β β€) β ((β‘πΉ β {(((π‘ / (π£ / 3)) + 1) Β· (π£ / 3))}) βͺ (β‘πΉ β ((((π‘ / (π£ / 3)) + 1) Β· (π£ / 3))(,)((π£ / 3) Β· (((π‘ / (π£ / 3)) + 1) + 1))))) = {π₯ β β β£ ((π‘ / (π£ / 3)) + 1) = (ββ((πΉβπ₯) / (π£ / 3)))}) |
361 | 230 | ad4antr 731 |
. . . . . . . . . . 11
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ ((π‘ / (π£ / 3)) + 1) β β€) β πΉ β MblFn) |
362 | 4 | ad4antr 731 |
. . . . . . . . . . 11
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ ((π‘ / (π£ / 3)) + 1) β β€) β πΉ:ββΆβ) |
363 | | mbfimasn 25012 |
. . . . . . . . . . 11
β’ ((πΉ β MblFn β§ πΉ:ββΆβ β§
(((π‘ / (π£ / 3)) + 1) Β· (π£ / 3)) β β) β (β‘πΉ β {(((π‘ / (π£ / 3)) + 1) Β· (π£ / 3))}) β dom vol) |
364 | 361, 362,
314, 363 | syl3anc 1372 |
. . . . . . . . . 10
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ ((π‘ / (π£ / 3)) + 1) β β€) β (β‘πΉ β {(((π‘ / (π£ / 3)) + 1) Β· (π£ / 3))}) β dom vol) |
365 | | mbfima 25010 |
. . . . . . . . . . . 12
β’ ((πΉ β MblFn β§ πΉ:ββΆβ) β
(β‘πΉ β ((((π‘ / (π£ / 3)) + 1) Β· (π£ / 3))(,)((π£ / 3) Β· (((π‘ / (π£ / 3)) + 1) + 1)))) β dom
vol) |
366 | 230, 4, 365 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β (β‘πΉ β ((((π‘ / (π£ / 3)) + 1) Β· (π£ / 3))(,)((π£ / 3) Β· (((π‘ / (π£ / 3)) + 1) + 1)))) β dom
vol) |
367 | 366 | ad4antr 731 |
. . . . . . . . . 10
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ ((π‘ / (π£ / 3)) + 1) β β€) β (β‘πΉ β ((((π‘ / (π£ / 3)) + 1) Β· (π£ / 3))(,)((π£ / 3) Β· (((π‘ / (π£ / 3)) + 1) + 1)))) β dom
vol) |
368 | | unmbl 24917 |
. . . . . . . . . 10
β’ (((β‘πΉ β {(((π‘ / (π£ / 3)) + 1) Β· (π£ / 3))}) β dom vol β§ (β‘πΉ β ((((π‘ / (π£ / 3)) + 1) Β· (π£ / 3))(,)((π£ / 3) Β· (((π‘ / (π£ / 3)) + 1) + 1)))) β dom vol) β
((β‘πΉ β {(((π‘ / (π£ / 3)) + 1) Β· (π£ / 3))}) βͺ (β‘πΉ β ((((π‘ / (π£ / 3)) + 1) Β· (π£ / 3))(,)((π£ / 3) Β· (((π‘ / (π£ / 3)) + 1) + 1))))) β dom
vol) |
369 | 364, 367,
368 | syl2anc 585 |
. . . . . . . . 9
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ ((π‘ / (π£ / 3)) + 1) β β€) β ((β‘πΉ β {(((π‘ / (π£ / 3)) + 1) Β· (π£ / 3))}) βͺ (β‘πΉ β ((((π‘ / (π£ / 3)) + 1) Β· (π£ / 3))(,)((π£ / 3) Β· (((π‘ / (π£ / 3)) + 1) + 1))))) β dom
vol) |
370 | 360, 369 | eqeltrrd 2839 |
. . . . . . . 8
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ ((π‘ / (π£ / 3)) + 1) β β€) β {π₯ β β β£ ((π‘ / (π£ / 3)) + 1) = (ββ((πΉβπ₯) / (π£ / 3)))} β dom vol) |
371 | | simpr 486 |
. . . . . . . . . . . . . 14
β’
((((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ π₯ β β) β§ ((π‘ / (π£ / 3)) + 1) = (ββ((πΉβπ₯) / (π£ / 3)))) β ((π‘ / (π£ / 3)) + 1) = (ββ((πΉβπ₯) / (π£ / 3)))) |
372 | 352 | flcld 13710 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ π₯ β β) β
(ββ((πΉβπ₯) / (π£ / 3))) β β€) |
373 | 372 | adantr 482 |
. . . . . . . . . . . . . 14
β’
((((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ π₯ β β) β§ ((π‘ / (π£ / 3)) + 1) = (ββ((πΉβπ₯) / (π£ / 3)))) β (ββ((πΉβπ₯) / (π£ / 3))) β β€) |
374 | 371, 373 | eqeltrd 2838 |
. . . . . . . . . . . . 13
β’
((((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ π₯ β β) β§ ((π‘ / (π£ / 3)) + 1) = (ββ((πΉβπ₯) / (π£ / 3)))) β ((π‘ / (π£ / 3)) + 1) β β€) |
375 | 374 | stoic1a 1775 |
. . . . . . . . . . . 12
β’
((((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ π₯ β β) β§ Β¬ ((π‘ / (π£ / 3)) + 1) β β€) β Β¬
((π‘ / (π£ / 3)) + 1) = (ββ((πΉβπ₯) / (π£ / 3)))) |
376 | 375 | an32s 651 |
. . . . . . . . . . 11
β’
((((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ Β¬ ((π‘ / (π£ / 3)) + 1) β β€) β§ π₯ β β) β Β¬
((π‘ / (π£ / 3)) + 1) = (ββ((πΉβπ₯) / (π£ / 3)))) |
377 | 376 | ralrimiva 3144 |
. . . . . . . . . 10
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ Β¬ ((π‘ / (π£ / 3)) + 1) β β€) β
βπ₯ β β
Β¬ ((π‘ / (π£ / 3)) + 1) =
(ββ((πΉβπ₯) / (π£ / 3)))) |
378 | | rabeq0 4349 |
. . . . . . . . . 10
β’ ({π₯ β β β£ ((π‘ / (π£ / 3)) + 1) = (ββ((πΉβπ₯) / (π£ / 3)))} = β
β βπ₯ β β Β¬ ((π‘ / (π£ / 3)) + 1) = (ββ((πΉβπ₯) / (π£ / 3)))) |
379 | 377, 378 | sylibr 233 |
. . . . . . . . 9
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ Β¬ ((π‘ / (π£ / 3)) + 1) β β€) β {π₯ β β β£ ((π‘ / (π£ / 3)) + 1) = (ββ((πΉβπ₯) / (π£ / 3)))} = β
) |
380 | | 0mbl 24919 |
. . . . . . . . 9
β’ β
β dom vol |
381 | 379, 380 | eqeltrdi 2846 |
. . . . . . . 8
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ Β¬ ((π‘ / (π£ / 3)) + 1) β β€) β {π₯ β β β£ ((π‘ / (π£ / 3)) + 1) = (ββ((πΉβπ₯) / (π£ / 3)))} β dom vol) |
382 | 370, 381 | pm2.61dan 812 |
. . . . . . 7
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π‘ β β)
β {π₯ β β
β£ ((π‘ / (π£ / 3)) + 1) =
(ββ((πΉβπ₯) / (π£ / 3)))} β dom vol) |
383 | 308, 382 | eqeltrrd 2839 |
. . . . . 6
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π‘ β β)
β {π₯ β β
β£ π‘ =
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3))} β dom
vol) |
384 | | inmbl 24922 |
. . . . . 6
β’ ((({π₯ β β β£
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)} β© {π₯ β β β£ (ββπ₯) β 0}) β dom vol β§ {π₯ β β β£ π‘ = (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3))} β dom vol) β
(({π₯ β β β£
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)} β© {π₯ β β β£ (ββπ₯) β 0}) β© {π₯ β β β£ π‘ = (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3))}) β dom
vol) |
385 | 288, 383,
384 | syl2anc 585 |
. . . . 5
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π‘ β β)
β (({π₯ β β
β£ (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)} β© {π₯ β β β£ (ββπ₯) β 0}) β© {π₯ β β β£ π‘ = (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3))}) β dom
vol) |
386 | | rabiun 36080 |
. . . . . . . . . . 11
β’ {π₯ β βͺ π‘ β ran β(β‘β β {π‘}) β£ Β¬ (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)} = βͺ
π‘ β ran β{π₯ β (β‘β β {π‘}) β£ Β¬ (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)} |
387 | | rabeq 3424 |
. . . . . . . . . . . 12
β’ (βͺ π‘ β ran β(β‘β β {π‘}) = β β {π₯ β βͺ
π‘ β ran β(β‘β β {π‘}) β£ Β¬ (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)} = {π₯ β β β£ Β¬
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)}) |
388 | 168, 387 | syl 17 |
. . . . . . . . . . 11
β’ (β β dom β«1
β {π₯ β βͺ π‘ β ran β(β‘β β {π‘}) β£ Β¬ (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)} = {π₯ β β β£ Β¬
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)}) |
389 | 386, 388 | eqtr3id 2791 |
. . . . . . . . . 10
β’ (β β dom β«1
β βͺ π‘ β ran β{π₯ β (β‘β β {π‘}) β£ Β¬ (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)} = {π₯ β β β£ Β¬
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)}) |
390 | 389 | ad2antlr 726 |
. . . . . . . . 9
β’ (((π β§ β β dom β«1) β§ π£ β β+)
β βͺ π‘ β ran β{π₯ β (β‘β β {π‘}) β£ Β¬ (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)} = {π₯ β β β£ Β¬
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)}) |
391 | 176 | notbid 318 |
. . . . . . . . . . . . . . 15
β’ ((β β dom β«1
β§ π₯ β (β‘β β {π‘})) β (Β¬ (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β Β¬ (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ π‘)) |
392 | 391 | rabbidva 3417 |
. . . . . . . . . . . . . 14
β’ (β β dom β«1
β {π₯ β (β‘β β {π‘}) β£ Β¬ (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)} = {π₯ β (β‘β β {π‘}) β£ Β¬ (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ π‘}) |
393 | | inrab2 4272 |
. . . . . . . . . . . . . . 15
β’ ({π₯ β β β£ Β¬
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ π‘} β© (β‘β β {π‘})) = {π₯ β (β β© (β‘β β {π‘})) β£ Β¬ (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ π‘} |
394 | | rabeq 3424 |
. . . . . . . . . . . . . . . 16
β’ ((β
β© (β‘β β {π‘})) = (β‘β β {π‘}) β {π₯ β (β β© (β‘β β {π‘})) β£ Β¬ (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ π‘} = {π₯ β (β‘β β {π‘}) β£ Β¬ (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ π‘}) |
395 | 184, 394 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (β β dom β«1
β {π₯ β (β
β© (β‘β β {π‘})) β£ Β¬ (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ π‘} = {π₯ β (β‘β β {π‘}) β£ Β¬ (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ π‘}) |
396 | 393, 395 | eqtrid 2789 |
. . . . . . . . . . . . . 14
β’ (β β dom β«1
β ({π₯ β β
β£ Β¬ (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ π‘} β© (β‘β β {π‘})) = {π₯ β (β‘β β {π‘}) β£ Β¬ (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ π‘}) |
397 | 392, 396 | eqtr4d 2780 |
. . . . . . . . . . . . 13
β’ (β β dom β«1
β {π₯ β (β‘β β {π‘}) β£ Β¬ (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)} = ({π₯ β β β£ Β¬
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ π‘} β© (β‘β β {π‘}))) |
398 | 397 | ad3antlr 730 |
. . . . . . . . . . . 12
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π‘ β ran β) β {π₯ β (β‘β β {π‘}) β£ Β¬ (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)} = ({π₯ β β β£ Β¬
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ π‘} β© (β‘β β {π‘}))) |
399 | | imaundi 6107 |
. . . . . . . . . . . . . . . . 17
β’ (β‘πΉ β ({((ββ(((π‘ / (π£ / 3)) + 1) + 1)) Β· (π£ / 3))} βͺ
(((ββ(((π‘ /
(π£ / 3)) + 1) + 1))
Β· (π£ /
3))(,)+β))) = ((β‘πΉ β
{((ββ(((π‘ /
(π£ / 3)) + 1) + 1))
Β· (π£ / 3))}) βͺ
(β‘πΉ β (((ββ(((π‘ / (π£ / 3)) + 1) + 1)) Β· (π£ /
3))(,)+β))) |
400 | 13, 19 | jca 513 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π£ β β+
β ((π£ / 3) β
β β§ (π£ / 3) β
0)) |
401 | | redivcl 11881 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π‘ β β β§ (π£ / 3) β β β§
(π£ / 3) β 0) β
(π‘ / (π£ / 3)) β β) |
402 | 401 | 3expb 1121 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π‘ β β β§ ((π£ / 3) β β β§
(π£ / 3) β 0)) β
(π‘ / (π£ / 3)) β β) |
403 | 400, 402 | sylan2 594 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π‘ β β β§ π£ β β+)
β (π‘ / (π£ / 3)) β
β) |
404 | 403 | ancoms 460 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π£ β β+
β§ π‘ β β)
β (π‘ / (π£ / 3)) β
β) |
405 | 404 | adantll 713 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π‘ β β)
β (π‘ / (π£ / 3)) β
β) |
406 | 405, 203 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π‘ β β)
β ((π‘ / (π£ / 3)) + 1) β
β) |
407 | | peano2re 11335 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π‘ / (π£ / 3)) + 1) β β β (((π‘ / (π£ / 3)) + 1) + 1) β
β) |
408 | | reflcl 13708 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π‘ / (π£ / 3)) + 1) + 1) β β β
(ββ(((π‘ /
(π£ / 3)) + 1) + 1)) β
β) |
409 | 406, 407,
408 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π‘ β β)
β (ββ(((π‘
/ (π£ / 3)) + 1) + 1))
β β) |
410 | 13 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π‘ β β)
β (π£ / 3) β
β) |
411 | 409, 410 | remulcld 11192 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π‘ β β)
β ((ββ(((π‘
/ (π£ / 3)) + 1) + 1))
Β· (π£ / 3)) β
β) |
412 | 411 | rexrd 11212 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π‘ β β)
β ((ββ(((π‘
/ (π£ / 3)) + 1) + 1))
Β· (π£ / 3)) β
β*) |
413 | | pnfxr 11216 |
. . . . . . . . . . . . . . . . . . . 20
β’ +β
β β* |
414 | 413 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π‘ β β)
β +β β β*) |
415 | | ltpnf 13048 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((ββ(((π‘ / (π£ / 3)) + 1) + 1)) Β· (π£ / 3)) β β β
((ββ(((π‘ /
(π£ / 3)) + 1) + 1))
Β· (π£ / 3)) <
+β) |
416 | 411, 415 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π‘ β β)
β ((ββ(((π‘
/ (π£ / 3)) + 1) + 1))
Β· (π£ / 3)) <
+β) |
417 | | snunioo 13402 |
. . . . . . . . . . . . . . . . . . 19
β’
((((ββ(((π‘ / (π£ / 3)) + 1) + 1)) Β· (π£ / 3)) β
β* β§ +β β β* β§
((ββ(((π‘ /
(π£ / 3)) + 1) + 1))
Β· (π£ / 3)) <
+β) β ({((ββ(((π‘ / (π£ / 3)) + 1) + 1)) Β· (π£ / 3))} βͺ
(((ββ(((π‘ /
(π£ / 3)) + 1) + 1))
Β· (π£ /
3))(,)+β)) = (((ββ(((π‘ / (π£ / 3)) + 1) + 1)) Β· (π£ /
3))[,)+β)) |
418 | 412, 414,
416, 417 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π‘ β β)
β ({((ββ(((π‘ / (π£ / 3)) + 1) + 1)) Β· (π£ / 3))} βͺ
(((ββ(((π‘ /
(π£ / 3)) + 1) + 1))
Β· (π£ /
3))(,)+β)) = (((ββ(((π‘ / (π£ / 3)) + 1) + 1)) Β· (π£ /
3))[,)+β)) |
419 | 418 | imaeq2d 6018 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π‘ β β)
β (β‘πΉ β ({((ββ(((π‘ / (π£ / 3)) + 1) + 1)) Β· (π£ / 3))} βͺ
(((ββ(((π‘ /
(π£ / 3)) + 1) + 1))
Β· (π£ /
3))(,)+β))) = (β‘πΉ β (((ββ(((π‘ / (π£ / 3)) + 1) + 1)) Β· (π£ /
3))[,)+β))) |
420 | 399, 419 | eqtr3id 2791 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π‘ β β)
β ((β‘πΉ β {((ββ(((π‘ / (π£ / 3)) + 1) + 1)) Β· (π£ / 3))}) βͺ (β‘πΉ β (((ββ(((π‘ / (π£ / 3)) + 1) + 1)) Β· (π£ / 3))(,)+β))) = (β‘πΉ β (((ββ(((π‘ / (π£ / 3)) + 1) + 1)) Β· (π£ /
3))[,)+β))) |
421 | 223 | imaeq1d 6017 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (β‘πΉ β (((ββ(((π‘ / (π£ / 3)) + 1) + 1)) Β· (π£ / 3))[,)+β)) = (β‘(π₯ β β β¦ (πΉβπ₯)) β (((ββ(((π‘ / (π£ / 3)) + 1) + 1)) Β· (π£ /
3))[,)+β))) |
422 | 225 | mptpreima 6195 |
. . . . . . . . . . . . . . . . . 18
β’ (β‘(π₯ β β β¦ (πΉβπ₯)) β (((ββ(((π‘ / (π£ / 3)) + 1) + 1)) Β· (π£ / 3))[,)+β)) = {π₯ β β β£ (πΉβπ₯) β (((ββ(((π‘ / (π£ / 3)) + 1) + 1)) Β· (π£ /
3))[,)+β)} |
423 | 421, 422 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . 17
β’ (π β (β‘πΉ β (((ββ(((π‘ / (π£ / 3)) + 1) + 1)) Β· (π£ / 3))[,)+β)) = {π₯ β β β£ (πΉβπ₯) β (((ββ(((π‘ / (π£ / 3)) + 1) + 1)) Β· (π£ /
3))[,)+β)}) |
424 | 423 | ad3antrrr 729 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π‘ β β)
β (β‘πΉ β (((ββ(((π‘ / (π£ / 3)) + 1) + 1)) Β· (π£ / 3))[,)+β)) = {π₯ β β β£ (πΉβπ₯) β (((ββ(((π‘ / (π£ / 3)) + 1) + 1)) Β· (π£ /
3))[,)+β)}) |
425 | 406, 407 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π‘ β β)
β (((π‘ / (π£ / 3)) + 1) + 1) β
β) |
426 | 425 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ π₯ β β) β (((π‘ / (π£ / 3)) + 1) + 1) β
β) |
427 | | flflp1 13719 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π‘ / (π£ / 3)) + 1) + 1) β β
β§ ((πΉβπ₯) / (π£ / 3)) β β) β
((ββ(((π‘ /
(π£ / 3)) + 1) + 1)) β€
((πΉβπ₯) / (π£ / 3)) β (((π‘ / (π£ / 3)) + 1) + 1) < ((ββ((πΉβπ₯) / (π£ / 3))) + 1))) |
428 | 426, 352,
427 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ π₯ β β) β
((ββ(((π‘ /
(π£ / 3)) + 1) + 1)) β€
((πΉβπ₯) / (π£ / 3)) β (((π‘ / (π£ / 3)) + 1) + 1) < ((ββ((πΉβπ₯) / (π£ / 3))) + 1))) |
429 | 411 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ π₯ β β) β
((ββ(((π‘ /
(π£ / 3)) + 1) + 1))
Β· (π£ / 3)) β
β) |
430 | | elicopnf 13369 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((ββ(((π‘ / (π£ / 3)) + 1) + 1)) Β· (π£ / 3)) β β β
((πΉβπ₯) β
(((ββ(((π‘ /
(π£ / 3)) + 1) + 1))
Β· (π£ /
3))[,)+β) β ((πΉβπ₯) β β β§
((ββ(((π‘ /
(π£ / 3)) + 1) + 1))
Β· (π£ / 3)) β€
(πΉβπ₯)))) |
431 | 429, 430 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ π₯ β β) β ((πΉβπ₯) β (((ββ(((π‘ / (π£ / 3)) + 1) + 1)) Β· (π£ / 3))[,)+β) β
((πΉβπ₯) β β β§
((ββ(((π‘ /
(π£ / 3)) + 1) + 1))
Β· (π£ / 3)) β€
(πΉβπ₯)))) |
432 | 336 | biantrurd 534 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ π₯ β β) β
(((ββ(((π‘ /
(π£ / 3)) + 1) + 1))
Β· (π£ / 3)) β€
(πΉβπ₯) β ((πΉβπ₯) β β β§
((ββ(((π‘ /
(π£ / 3)) + 1) + 1))
Β· (π£ / 3)) β€
(πΉβπ₯)))) |
433 | 409 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ π₯ β β) β
(ββ(((π‘ /
(π£ / 3)) + 1) + 1)) β
β) |
434 | 68 | ad3antlr 730 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ π₯ β β) β (π£ / 3) β
β+) |
435 | 433, 336,
434 | lemuldivd 13013 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ π₯ β β) β
(((ββ(((π‘ /
(π£ / 3)) + 1) + 1))
Β· (π£ / 3)) β€
(πΉβπ₯) β (ββ(((π‘ / (π£ / 3)) + 1) + 1)) β€ ((πΉβπ₯) / (π£ / 3)))) |
436 | 431, 432,
435 | 3bitr2d 307 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ π₯ β β) β ((πΉβπ₯) β (((ββ(((π‘ / (π£ / 3)) + 1) + 1)) Β· (π£ / 3))[,)+β) β
(ββ(((π‘ /
(π£ / 3)) + 1) + 1)) β€
((πΉβπ₯) / (π£ / 3)))) |
437 | 406 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ π₯ β β) β ((π‘ / (π£ / 3)) + 1) β β) |
438 | 352, 22 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ π₯ β β) β
(ββ((πΉβπ₯) / (π£ / 3))) β β) |
439 | | 1red 11163 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ π₯ β β) β 1 β
β) |
440 | 437, 438,
439 | ltadd1d 11755 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ π₯ β β) β (((π‘ / (π£ / 3)) + 1) < (ββ((πΉβπ₯) / (π£ / 3))) β (((π‘ / (π£ / 3)) + 1) + 1) < ((ββ((πΉβπ₯) / (π£ / 3))) + 1))) |
441 | 428, 436,
440 | 3bitr4d 311 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ π₯ β β) β ((πΉβπ₯) β (((ββ(((π‘ / (π£ / 3)) + 1) + 1)) Β· (π£ / 3))[,)+β) β
((π‘ / (π£ / 3)) + 1) < (ββ((πΉβπ₯) / (π£ / 3))))) |
442 | 295, 439,
438 | ltaddsubd 11762 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ π₯ β β) β (((π‘ / (π£ / 3)) + 1) < (ββ((πΉβπ₯) / (π£ / 3))) β (π‘ / (π£ / 3)) < ((ββ((πΉβπ₯) / (π£ / 3))) β 1))) |
443 | 441, 442 | bitrd 279 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ π₯ β β) β ((πΉβπ₯) β (((ββ(((π‘ / (π£ / 3)) + 1) + 1)) Β· (π£ / 3))[,)+β) β (π‘ / (π£ / 3)) < ((ββ((πΉβπ₯) / (π£ / 3))) β 1))) |
444 | 438, 24 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ π₯ β β) β
((ββ((πΉβπ₯) / (π£ / 3))) β 1) β
β) |
445 | 292, 444,
434 | ltdivmul2d 13016 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ π₯ β β) β ((π‘ / (π£ / 3)) < ((ββ((πΉβπ₯) / (π£ / 3))) β 1) β π‘ < (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)))) |
446 | 444, 293 | remulcld 11192 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ π₯ β β) β
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β
β) |
447 | 292, 446 | ltnled 11309 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ π₯ β β) β (π‘ < (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β Β¬
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ π‘)) |
448 | 443, 445,
447 | 3bitrd 305 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ β β dom β«1)
β§ π£ β
β+) β§ π‘ β β) β§ π₯ β β) β ((πΉβπ₯) β (((ββ(((π‘ / (π£ / 3)) + 1) + 1)) Β· (π£ / 3))[,)+β) β Β¬
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ π‘)) |
449 | 448 | rabbidva 3417 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π‘ β β)
β {π₯ β β
β£ (πΉβπ₯) β
(((ββ(((π‘ /
(π£ / 3)) + 1) + 1))
Β· (π£ /
3))[,)+β)} = {π₯
β β β£ Β¬ (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ π‘}) |
450 | 420, 424,
449 | 3eqtrd 2781 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π‘ β β)
β ((β‘πΉ β {((ββ(((π‘ / (π£ / 3)) + 1) + 1)) Β· (π£ / 3))}) βͺ (β‘πΉ β (((ββ(((π‘ / (π£ / 3)) + 1) + 1)) Β· (π£ / 3))(,)+β))) = {π₯ β β β£ Β¬
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ π‘}) |
451 | 230 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π‘ β β)
β πΉ β
MblFn) |
452 | | mbfimasn 25012 |
. . . . . . . . . . . . . . . . 17
β’ ((πΉ β MblFn β§ πΉ:ββΆβ β§
((ββ(((π‘ /
(π£ / 3)) + 1) + 1))
Β· (π£ / 3)) β
β) β (β‘πΉ β {((ββ(((π‘ / (π£ / 3)) + 1) + 1)) Β· (π£ / 3))}) β dom
vol) |
453 | 451, 335,
411, 452 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π‘ β β)
β (β‘πΉ β {((ββ(((π‘ / (π£ / 3)) + 1) + 1)) Β· (π£ / 3))}) β dom
vol) |
454 | | mbfima 25010 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΉ β MblFn β§ πΉ:ββΆβ) β
(β‘πΉ β (((ββ(((π‘ / (π£ / 3)) + 1) + 1)) Β· (π£ / 3))(,)+β)) β dom
vol) |
455 | 230, 4, 454 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’ (π β (β‘πΉ β (((ββ(((π‘ / (π£ / 3)) + 1) + 1)) Β· (π£ / 3))(,)+β)) β dom
vol) |
456 | 455 | ad3antrrr 729 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π‘ β β)
β (β‘πΉ β (((ββ(((π‘ / (π£ / 3)) + 1) + 1)) Β· (π£ / 3))(,)+β)) β dom
vol) |
457 | | unmbl 24917 |
. . . . . . . . . . . . . . . 16
β’ (((β‘πΉ β {((ββ(((π‘ / (π£ / 3)) + 1) + 1)) Β· (π£ / 3))}) β dom vol β§
(β‘πΉ β (((ββ(((π‘ / (π£ / 3)) + 1) + 1)) Β· (π£ / 3))(,)+β)) β dom
vol) β ((β‘πΉ β {((ββ(((π‘ / (π£ / 3)) + 1) + 1)) Β· (π£ / 3))}) βͺ (β‘πΉ β (((ββ(((π‘ / (π£ / 3)) + 1) + 1)) Β· (π£ / 3))(,)+β))) β dom
vol) |
458 | 453, 456,
457 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π‘ β β)
β ((β‘πΉ β {((ββ(((π‘ / (π£ / 3)) + 1) + 1)) Β· (π£ / 3))}) βͺ (β‘πΉ β (((ββ(((π‘ / (π£ / 3)) + 1) + 1)) Β· (π£ / 3))(,)+β))) β dom
vol) |
459 | 450, 458 | eqeltrrd 2839 |
. . . . . . . . . . . . . 14
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π‘ β β)
β {π₯ β β
β£ Β¬ (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ π‘} β dom vol) |
460 | 237, 459 | syl 17 |
. . . . . . . . . . . . 13
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π‘ β ran β) β {π₯ β β β£ Β¬
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ π‘} β dom vol) |
461 | | inmbl 24922 |
. . . . . . . . . . . . 13
β’ (({π₯ β β β£ Β¬
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ π‘} β dom vol β§ (β‘β β {π‘}) β dom vol) β ({π₯ β β β£ Β¬
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ π‘} β© (β‘β β {π‘})) β dom vol) |
462 | 460, 244,
461 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π‘ β ran β) β ({π₯ β β β£ Β¬
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ π‘} β© (β‘β β {π‘})) β dom vol) |
463 | 398, 462 | eqeltrd 2838 |
. . . . . . . . . . 11
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π‘ β ran β) β {π₯ β (β‘β β {π‘}) β£ Β¬ (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)} β dom vol) |
464 | 463 | ralrimiva 3144 |
. . . . . . . . . 10
β’ (((π β§ β β dom β«1) β§ π£ β β+)
β βπ‘ β ran
β{π₯ β (β‘β β {π‘}) β£ Β¬ (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)} β dom vol) |
465 | | finiunmbl 24924 |
. . . . . . . . . 10
β’ ((ran
β β Fin β§
βπ‘ β ran β{π₯ β (β‘β β {π‘}) β£ Β¬ (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)} β dom vol) β βͺ π‘ β ran β{π₯ β (β‘β β {π‘}) β£ Β¬ (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)} β dom vol) |
466 | 41, 464, 465 | syl2anc 585 |
. . . . . . . . 9
β’ (((π β§ β β dom β«1) β§ π£ β β+)
β βͺ π‘ β ran β{π₯ β (β‘β β {π‘}) β£ Β¬ (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)} β dom vol) |
467 | 390, 466 | eqeltrrd 2839 |
. . . . . . . 8
β’ (((π β§ β β dom β«1) β§ π£ β β+)
β {π₯ β β
β£ Β¬ (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)} β dom vol) |
468 | 254 | imaeq1d 6017 |
. . . . . . . . . . 11
β’ (β β dom β«1
β (β‘β β {0}) = (β‘(π₯ β β β¦ (ββπ₯)) β {0})) |
469 | 256 | mptpreima 6195 |
. . . . . . . . . . . 12
β’ (β‘(π₯ β β β¦ (ββπ₯)) β {0}) = {π₯ β β β£ (ββπ₯) β {0}} |
470 | 140 | elsn 4606 |
. . . . . . . . . . . . 13
β’ ((ββπ₯) β {0} β (ββπ₯) = 0) |
471 | 470 | rabbii 3416 |
. . . . . . . . . . . 12
β’ {π₯ β β β£ (ββπ₯) β {0}} = {π₯ β β β£ (ββπ₯) = 0} |
472 | 469, 471 | eqtri 2765 |
. . . . . . . . . . 11
β’ (β‘(π₯ β β β¦ (ββπ₯)) β {0}) = {π₯ β β β£ (ββπ₯) = 0} |
473 | 468, 472 | eqtrdi 2793 |
. . . . . . . . . 10
β’ (β β dom β«1
β (β‘β β {0}) = {π₯ β β β£ (ββπ₯) = 0}) |
474 | | i1fima 25058 |
. . . . . . . . . 10
β’ (β β dom β«1
β (β‘β β {0}) β dom vol) |
475 | 473, 474 | eqeltrrd 2839 |
. . . . . . . . 9
β’ (β β dom β«1
β {π₯ β β
β£ (ββπ₯) = 0} β dom
vol) |
476 | 475 | ad2antlr 726 |
. . . . . . . 8
β’ (((π β§ β β dom β«1) β§ π£ β β+)
β {π₯ β β
β£ (ββπ₯) = 0} β dom
vol) |
477 | | unmbl 24917 |
. . . . . . . 8
β’ (({π₯ β β β£ Β¬
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)} β dom vol β§ {π₯ β β β£ (ββπ₯) = 0} β dom vol) β ({π₯ β β β£ Β¬
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)} βͺ {π₯ β β β£ (ββπ₯) = 0}) β dom vol) |
478 | 467, 476,
477 | syl2anc 585 |
. . . . . . 7
β’ (((π β§ β β dom β«1) β§ π£ β β+)
β ({π₯ β β
β£ Β¬ (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)} βͺ {π₯ β β β£ (ββπ₯) = 0}) β dom vol) |
479 | 478 | adantr 482 |
. . . . . 6
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π‘ β β)
β ({π₯ β β
β£ Β¬ (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)} βͺ {π₯ β β β£ (ββπ₯) = 0}) β dom vol) |
480 | 254 | imaeq1d 6017 |
. . . . . . . . 9
β’ (β β dom β«1
β (β‘β β {π‘}) = (β‘(π₯ β β β¦ (ββπ₯)) β {π‘})) |
481 | 256 | mptpreima 6195 |
. . . . . . . . . 10
β’ (β‘(π₯ β β β¦ (ββπ₯)) β {π‘}) = {π₯ β β β£ (ββπ₯) β {π‘}} |
482 | 140 | elsn 4606 |
. . . . . . . . . . . 12
β’ ((ββπ₯) β {π‘} β (ββπ₯) = π‘) |
483 | | eqcom 2744 |
. . . . . . . . . . . 12
β’ ((ββπ₯) = π‘ β π‘ = (ββπ₯)) |
484 | 482, 483 | bitri 275 |
. . . . . . . . . . 11
β’ ((ββπ₯) β {π‘} β π‘ = (ββπ₯)) |
485 | 484 | rabbii 3416 |
. . . . . . . . . 10
β’ {π₯ β β β£ (ββπ₯) β {π‘}} = {π₯ β β β£ π‘ = (ββπ₯)} |
486 | 481, 485 | eqtri 2765 |
. . . . . . . . 9
β’ (β‘(π₯ β β β¦ (ββπ₯)) β {π‘}) = {π₯ β β β£ π‘ = (ββπ₯)} |
487 | 480, 486 | eqtrdi 2793 |
. . . . . . . 8
β’ (β β dom β«1
β (β‘β β {π‘}) = {π₯ β β β£ π‘ = (ββπ₯)}) |
488 | 487 | ad3antlr 730 |
. . . . . . 7
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π‘ β β)
β (β‘β β {π‘}) = {π₯ β β β£ π‘ = (ββπ₯)}) |
489 | 488, 243 | eqeltrrd 2839 |
. . . . . 6
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π‘ β β)
β {π₯ β β
β£ π‘ = (ββπ₯)} β dom vol) |
490 | | inmbl 24922 |
. . . . . 6
β’ ((({π₯ β β β£ Β¬
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)} βͺ {π₯ β β β£ (ββπ₯) = 0}) β dom vol β§ {π₯ β β β£ π‘ = (ββπ₯)} β dom vol) β (({π₯ β β β£ Β¬
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)} βͺ {π₯ β β β£ (ββπ₯) = 0}) β© {π₯ β β β£ π‘ = (ββπ₯)}) β dom vol) |
491 | 479, 489,
490 | syl2anc 585 |
. . . . 5
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π‘ β β)
β (({π₯ β β
β£ Β¬ (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)} βͺ {π₯ β β β£ (ββπ₯) = 0}) β© {π₯ β β β£ π‘ = (ββπ₯)}) β dom vol) |
492 | | unmbl 24917 |
. . . . 5
β’
(((({π₯ β
β β£ (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)} β© {π₯ β β β£ (ββπ₯) β 0}) β© {π₯ β β β£ π‘ = (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3))}) β dom vol β§
(({π₯ β β β£
Β¬ (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)} βͺ {π₯ β β β£ (ββπ₯) = 0}) β© {π₯ β β β£ π‘ = (ββπ₯)}) β dom vol) β ((({π₯ β β β£
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)} β© {π₯ β β β£ (ββπ₯) β 0}) β© {π₯ β β β£ π‘ = (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3))}) βͺ (({π₯ β β β£ Β¬
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)} βͺ {π₯ β β β£ (ββπ₯) = 0}) β© {π₯ β β β£ π‘ = (ββπ₯)})) β dom vol) |
493 | 385, 491,
492 | syl2anc 585 |
. . . 4
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π‘ β β)
β ((({π₯ β β
β£ (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)} β© {π₯ β β β£ (ββπ₯) β 0}) β© {π₯ β β β£ π‘ = (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3))}) βͺ (({π₯ β β β£ Β¬
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)} βͺ {π₯ β β β£ (ββπ₯) = 0}) β© {π₯ β β β£ π‘ = (ββπ₯)})) β dom vol) |
494 | 159, 493 | syl 17 |
. . 3
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π‘ β (ran (π₯ β β β¦
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯))) β {0})) β ((({π₯ β β β£
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)} β© {π₯ β β β£ (ββπ₯) β 0}) β© {π₯ β β β£ π‘ = (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3))}) βͺ (({π₯ β β β£ Β¬
(((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯)} βͺ {π₯ β β β£ (ββπ₯) = 0}) β© {π₯ β β β£ π‘ = (ββπ₯)})) β dom vol) |
495 | 154, 494 | eqeltrid 2842 |
. 2
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π‘ β (ran (π₯ β β β¦
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯))) β {0})) β (β‘(π₯ β β β¦
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯))) β {π‘}) β dom vol) |
496 | | mblvol 24910 |
. . . 4
β’ ((β‘(π₯ β β β¦
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯))) β {π‘}) β dom vol β (volβ(β‘(π₯ β β β¦
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯))) β {π‘})) = (vol*β(β‘(π₯ β β β¦
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯))) β {π‘}))) |
497 | 495, 496 | syl 17 |
. . 3
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π‘ β (ran (π₯ β β β¦
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯))) β {0})) β (volβ(β‘(π₯ β β β¦
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯))) β {π‘})) = (vol*β(β‘(π₯ β β β¦
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯))) β {π‘}))) |
498 | | eldifsn 4752 |
. . . . . 6
β’ (π‘ β (ran (π₯ β β β¦
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯))) β {0}) β (π‘ β ran (π₯ β β β¦
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯))) β§ π‘ β 0)) |
499 | 157 | anim1d 612 |
. . . . . 6
β’ (((π β§ β β dom β«1) β§ π£ β β+)
β ((π‘ β ran
(π₯ β β β¦
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯))) β§ π‘ β 0) β (π‘ β β β§ π‘ β 0))) |
500 | 498, 499 | biimtrid 241 |
. . . . 5
β’ (((π β§ β β dom β«1) β§ π£ β β+)
β (π‘ β (ran
(π₯ β β β¦
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯))) β {0}) β (π‘ β β β§ π‘ β 0))) |
501 | 500 | imdistani 570 |
. . . 4
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π‘ β (ran (π₯ β β β¦
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯))) β {0})) β (((π β§ β β dom β«1) β§ π£ β β+)
β§ (π‘ β β
β§ π‘ β
0))) |
502 | 128 | a1i 11 |
. . . . . . . . . . 11
β’ (β β dom β«1
β (β‘(π₯ β β β¦
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯))) β {π‘}) = {π₯ β β β£
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯)) β {π‘}}) |
503 | 468, 469 | eqtrdi 2793 |
. . . . . . . . . . 11
β’ (β β dom β«1
β (β‘β β {0}) = {π₯ β β β£ (ββπ₯) β {0}}) |
504 | 502, 503 | ineq12d 4178 |
. . . . . . . . . 10
β’ (β β dom β«1
β ((β‘(π₯ β β β¦
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯))) β {π‘}) β© (β‘β β {0})) = ({π₯ β β β£
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯)) β {π‘}} β© {π₯ β β β£ (ββπ₯) β {0}})) |
505 | | inrab 4271 |
. . . . . . . . . 10
β’ ({π₯ β β β£
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯)) β {π‘}} β© {π₯ β β β£ (ββπ₯) β {0}}) = {π₯ β β β£
(if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯)) β {π‘} β§ (ββπ₯) β {0})} |
506 | 504, 505 | eqtrdi 2793 |
. . . . . . . . 9
β’ (β β dom β«1
β ((β‘(π₯ β β β¦
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯))) β {π‘}) β© (β‘β β {0})) = {π₯ β β β£
(if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯)) β {π‘} β§ (ββπ₯) β {0})}) |
507 | 506 | ad3antlr 730 |
. . . . . . . 8
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ (π‘ β β
β§ π‘ β 0)) β
((β‘(π₯ β β β¦
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯))) β {π‘}) β© (β‘β β {0})) = {π₯ β β β£
(if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯)) β {π‘} β§ (ββπ₯) β {0})}) |
508 | 144 | biimpri 227 |
. . . . . . . . . . . . . . . . . 18
β’ ((ββπ₯) = 0 β Β¬ (ββπ₯) β 0) |
509 | 508 | intnand 490 |
. . . . . . . . . . . . . . . . 17
β’ ((ββπ₯) = 0 β Β¬ ((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0)) |
510 | 509 | iffalsed 4502 |
. . . . . . . . . . . . . . . 16
β’ ((ββπ₯) = 0 β if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯)) = (ββπ₯)) |
511 | | eqtr 2760 |
. . . . . . . . . . . . . . . 16
β’
((if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯)) = (ββπ₯) β§ (ββπ₯) = 0) β if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯)) = 0) |
512 | 510, 511 | mpancom 687 |
. . . . . . . . . . . . . . 15
β’ ((ββπ₯) = 0 β if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯)) = 0) |
513 | 512 | adantl 483 |
. . . . . . . . . . . . . 14
β’ (((π‘ β 0 β§ π₯ β β) β§ (ββπ₯) = 0) β if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯)) = 0) |
514 | | simpll 766 |
. . . . . . . . . . . . . . 15
β’ (((π‘ β 0 β§ π₯ β β) β§ (ββπ₯) = 0) β π‘ β 0) |
515 | 514 | necomd 3000 |
. . . . . . . . . . . . . 14
β’ (((π‘ β 0 β§ π₯ β β) β§ (ββπ₯) = 0) β 0 β π‘) |
516 | 513, 515 | eqnetrd 3012 |
. . . . . . . . . . . . 13
β’ (((π‘ β 0 β§ π₯ β β) β§ (ββπ₯) = 0) β if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯)) β π‘) |
517 | 516 | ex 414 |
. . . . . . . . . . . 12
β’ ((π‘ β 0 β§ π₯ β β) β ((ββπ₯) = 0 β if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯)) β π‘)) |
518 | | orcom 869 |
. . . . . . . . . . . . . 14
β’ ((Β¬
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯)) β {π‘} β¨ Β¬ (ββπ₯) β {0}) β (Β¬ (ββπ₯) β {0} β¨ Β¬
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯)) β {π‘})) |
519 | | ianor 981 |
. . . . . . . . . . . . . 14
β’ (Β¬
(if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯)) β {π‘} β§ (ββπ₯) β {0}) β (Β¬
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯)) β {π‘} β¨ Β¬ (ββπ₯) β {0})) |
520 | | imor 852 |
. . . . . . . . . . . . . 14
β’ (((ββπ₯) β {0} β Β¬
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯)) β {π‘}) β (Β¬ (ββπ₯) β {0} β¨ Β¬
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯)) β {π‘})) |
521 | 518, 519,
520 | 3bitr4i 303 |
. . . . . . . . . . . . 13
β’ (Β¬
(if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯)) β {π‘} β§ (ββπ₯) β {0}) β ((ββπ₯) β {0} β Β¬
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯)) β {π‘})) |
522 | 142 | necon3bbii 2992 |
. . . . . . . . . . . . . 14
β’ (Β¬
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯)) β {π‘} β if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯)) β π‘) |
523 | 470, 522 | imbi12i 351 |
. . . . . . . . . . . . 13
β’ (((ββπ₯) β {0} β Β¬
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯)) β {π‘}) β ((ββπ₯) = 0 β if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯)) β π‘)) |
524 | 521, 523 | bitri 275 |
. . . . . . . . . . . 12
β’ (Β¬
(if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯)) β {π‘} β§ (ββπ₯) β {0}) β ((ββπ₯) = 0 β if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯)) β π‘)) |
525 | 517, 524 | sylibr 233 |
. . . . . . . . . . 11
β’ ((π‘ β 0 β§ π₯ β β) β Β¬
(if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯)) β {π‘} β§ (ββπ₯) β {0})) |
526 | 525 | ralrimiva 3144 |
. . . . . . . . . 10
β’ (π‘ β 0 β βπ₯ β β Β¬
(if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯)) β {π‘} β§ (ββπ₯) β {0})) |
527 | | rabeq0 4349 |
. . . . . . . . . 10
β’ ({π₯ β β β£
(if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯)) β {π‘} β§ (ββπ₯) β {0})} = β
β βπ₯ β β Β¬
(if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯)) β {π‘} β§ (ββπ₯) β {0})) |
528 | 526, 527 | sylibr 233 |
. . . . . . . . 9
β’ (π‘ β 0 β {π₯ β β β£
(if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯)) β {π‘} β§ (ββπ₯) β {0})} = β
) |
529 | 528 | ad2antll 728 |
. . . . . . . 8
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ (π‘ β β
β§ π‘ β 0)) β
{π₯ β β β£
(if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯)) β {π‘} β§ (ββπ₯) β {0})} = β
) |
530 | 507, 529 | eqtrd 2777 |
. . . . . . 7
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ (π‘ β β
β§ π‘ β 0)) β
((β‘(π₯ β β β¦
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯))) β {π‘}) β© (β‘β β {0})) = β
) |
531 | | imassrn 6029 |
. . . . . . . . 9
β’ (β‘(π₯ β β β¦
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯))) β {π‘}) β ran β‘(π₯ β β β¦
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯))) |
532 | | dfdm4 5856 |
. . . . . . . . . 10
β’ dom
(π₯ β β β¦
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯))) = ran β‘(π₯ β β β¦
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯))) |
533 | 141, 127 | dmmpti 6650 |
. . . . . . . . . 10
β’ dom
(π₯ β β β¦
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯))) = β |
534 | 532, 533 | eqtr3i 2767 |
. . . . . . . . 9
β’ ran β‘(π₯ β β β¦
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯))) = β |
535 | 531, 534 | sseqtri 3985 |
. . . . . . . 8
β’ (β‘(π₯ β β β¦
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯))) β {π‘}) β β |
536 | | reldisj 4416 |
. . . . . . . 8
β’ ((β‘(π₯ β β β¦
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯))) β {π‘}) β β β (((β‘(π₯ β β β¦
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯))) β {π‘}) β© (β‘β β {0})) = β
β (β‘(π₯ β β β¦
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯))) β {π‘}) β (β β (β‘β β {0})))) |
537 | 535, 536 | ax-mp 5 |
. . . . . . 7
β’ (((β‘(π₯ β β β¦
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯))) β {π‘}) β© (β‘β β {0})) = β
β (β‘(π₯ β β β¦
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯))) β {π‘}) β (β β (β‘β β {0}))) |
538 | 530, 537 | sylib 217 |
. . . . . 6
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ (π‘ β β
β§ π‘ β 0)) β
(β‘(π₯ β β β¦
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯))) β {π‘}) β (β β (β‘β β {0}))) |
539 | | ffun 6676 |
. . . . . . . . . 10
β’ (β:ββΆβ β
Fun β) |
540 | | difpreima 7020 |
. . . . . . . . . 10
β’ (Fun
β β (β‘β β (ran β β {0})) = ((β‘β β ran β) β (β‘β β {0}))) |
541 | 539, 540 | syl 17 |
. . . . . . . . 9
β’ (β:ββΆβ β
(β‘β β (ran β β {0})) = ((β‘β β ran β) β (β‘β β {0}))) |
542 | | fdm 6682 |
. . . . . . . . . . 11
β’ (β:ββΆβ β
dom β =
β) |
543 | 161, 542 | eqtrid 2789 |
. . . . . . . . . 10
β’ (β:ββΆβ β
(β‘β β ran β) = β) |
544 | 543 | difeq1d 4086 |
. . . . . . . . 9
β’ (β:ββΆβ β
((β‘β β ran β) β (β‘β β {0})) = (β β (β‘β β {0}))) |
545 | 541, 544 | eqtrd 2777 |
. . . . . . . 8
β’ (β:ββΆβ β
(β‘β β (ran β β {0})) = (β β (β‘β β {0}))) |
546 | 27, 545 | syl 17 |
. . . . . . 7
β’ (β β dom β«1
β (β‘β β (ran β β {0})) = (β β (β‘β β {0}))) |
547 | 546 | ad3antlr 730 |
. . . . . 6
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ (π‘ β β
β§ π‘ β 0)) β
(β‘β β (ran β β {0})) = (β β (β‘β β {0}))) |
548 | 538, 547 | sseqtrrd 3990 |
. . . . 5
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ (π‘ β β
β§ π‘ β 0)) β
(β‘(π₯ β β β¦
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯))) β {π‘}) β (β‘β β (ran β β {0}))) |
549 | | imassrn 6029 |
. . . . . . 7
β’ (β‘β β (ran β β {0})) β ran β‘β |
550 | 549, 181 | sseqtrid 4001 |
. . . . . 6
β’ (β β dom β«1
β (β‘β β (ran β β {0})) β
β) |
551 | 550 | ad3antlr 730 |
. . . . 5
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ (π‘ β β
β§ π‘ β 0)) β
(β‘β β (ran β β {0})) β
β) |
552 | | i1fima 25058 |
. . . . . . . 8
β’ (β β dom β«1
β (β‘β β (ran β β {0})) β dom
vol) |
553 | | mblvol 24910 |
. . . . . . . 8
β’ ((β‘β β (ran β β {0})) β dom vol β
(volβ(β‘β β (ran β β {0}))) = (vol*β(β‘β β (ran β β {0})))) |
554 | 552, 553 | syl 17 |
. . . . . . 7
β’ (β β dom β«1
β (volβ(β‘β β (ran β β {0}))) = (vol*β(β‘β β (ran β β {0})))) |
555 | | neldifsn 4757 |
. . . . . . . 8
β’ Β¬ 0
β (ran β β
{0}) |
556 | | i1fima2 25059 |
. . . . . . . 8
β’ ((β β dom β«1
β§ Β¬ 0 β (ran β
β {0})) β (volβ(β‘β β (ran β β {0}))) β
β) |
557 | 555, 556 | mpan2 690 |
. . . . . . 7
β’ (β β dom β«1
β (volβ(β‘β β (ran β β {0}))) β
β) |
558 | 554, 557 | eqeltrrd 2839 |
. . . . . 6
β’ (β β dom β«1
β (vol*β(β‘β β (ran β β {0}))) β
β) |
559 | 558 | ad3antlr 730 |
. . . . 5
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ (π‘ β β
β§ π‘ β 0)) β
(vol*β(β‘β β (ran β β {0}))) β
β) |
560 | | ovolsscl 24866 |
. . . . 5
β’ (((β‘(π₯ β β β¦
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯))) β {π‘}) β (β‘β β (ran β β {0})) β§ (β‘β β (ran β β {0})) β β β§
(vol*β(β‘β β (ran β β {0}))) β β) β
(vol*β(β‘(π₯ β β β¦
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯))) β {π‘})) β β) |
561 | 548, 551,
559, 560 | syl3anc 1372 |
. . . 4
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ (π‘ β β
β§ π‘ β 0)) β
(vol*β(β‘(π₯ β β β¦
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯))) β {π‘})) β β) |
562 | 501, 561 | syl 17 |
. . 3
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π‘ β (ran (π₯ β β β¦
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯))) β {0})) β (vol*β(β‘(π₯ β β β¦
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯))) β {π‘})) β β) |
563 | 497, 562 | eqeltrd 2838 |
. 2
β’ ((((π β§ β β dom β«1) β§ π£ β β+)
β§ π‘ β (ran (π₯ β β β¦
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯))) β {0})) β (volβ(β‘(π₯ β β β¦
if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯))) β {π‘})) β β) |
564 | 31, 126, 495, 563 | i1fd 25061 |
1
β’ (((π β§ β β dom β«1) β§ π£ β β+)
β (π₯ β β
β¦ if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯))) β dom
β«1) |