Step | Hyp | Ref
| Expression |
1 | | inss1 4229 |
. . 3
β’ (π· β© πΌ) β π· |
2 | 1 | a1i 11 |
. 2
β’ (π β (π· β© πΌ) β π·) |
3 | 2 | sselda 3983 |
. . . . . . 7
β’ ((π β§ π₯ β (π· β© πΌ)) β π₯ β π·) |
4 | | smflimlem4.6 |
. . . . . . . . . 10
β’ πΊ = (π₯ β π· β¦ ( β β(π β π β¦ ((πΉβπ)βπ₯)))) |
5 | 4 | a1i 11 |
. . . . . . . . 9
β’ (π β πΊ = (π₯ β π· β¦ ( β β(π β π β¦ ((πΉβπ)βπ₯))))) |
6 | | nfv 1918 |
. . . . . . . . . . 11
β’
β²π(π β§ π₯ β π·) |
7 | | nfcv 2904 |
. . . . . . . . . . 11
β’
β²ππΉ |
8 | | nfcv 2904 |
. . . . . . . . . . 11
β’
β²π§πΉ |
9 | | smflimlem4.2 |
. . . . . . . . . . 11
β’ π =
(β€β₯βπ) |
10 | | smflimlem4.3 |
. . . . . . . . . . . . . 14
β’ (π β π β SAlg) |
11 | 10 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π) β π β SAlg) |
12 | | smflimlem4.4 |
. . . . . . . . . . . . . 14
β’ (π β πΉ:πβΆ(SMblFnβπ)) |
13 | 12 | ffvelcdmda 7087 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π) β (πΉβπ) β (SMblFnβπ)) |
14 | | eqid 2733 |
. . . . . . . . . . . . 13
β’ dom
(πΉβπ) = dom (πΉβπ) |
15 | 11, 13, 14 | smff 45448 |
. . . . . . . . . . . 12
β’ ((π β§ π β π) β (πΉβπ):dom (πΉβπ)βΆβ) |
16 | 15 | adantlr 714 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β π·) β§ π β π) β (πΉβπ):dom (πΉβπ)βΆβ) |
17 | | smflimlem4.5 |
. . . . . . . . . . . 12
β’ π· = {π₯ β βͺ
π β π β© π β
(β€β₯βπ)dom (πΉβπ) β£ (π β π β¦ ((πΉβπ)βπ₯)) β dom β } |
18 | | fveq2 6892 |
. . . . . . . . . . . . . . 15
β’ (π₯ = π§ β ((πΉβπ)βπ₯) = ((πΉβπ)βπ§)) |
19 | 18 | mpteq2dv 5251 |
. . . . . . . . . . . . . 14
β’ (π₯ = π§ β (π β π β¦ ((πΉβπ)βπ₯)) = (π β π β¦ ((πΉβπ)βπ§))) |
20 | 19 | eleq1d 2819 |
. . . . . . . . . . . . 13
β’ (π₯ = π§ β ((π β π β¦ ((πΉβπ)βπ₯)) β dom β β (π β π β¦ ((πΉβπ)βπ§)) β dom β )) |
21 | 20 | cbvrabv 3443 |
. . . . . . . . . . . 12
β’ {π₯ β βͺ π β π β© π β
(β€β₯βπ)dom (πΉβπ) β£ (π β π β¦ ((πΉβπ)βπ₯)) β dom β } = {π§ β βͺ
π β π β© π β
(β€β₯βπ)dom (πΉβπ) β£ (π β π β¦ ((πΉβπ)βπ§)) β dom β } |
22 | 17, 21 | eqtri 2761 |
. . . . . . . . . . 11
β’ π· = {π§ β βͺ
π β π β© π β
(β€β₯βπ)dom (πΉβπ) β£ (π β π β¦ ((πΉβπ)βπ§)) β dom β } |
23 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π·) β π₯ β π·) |
24 | 6, 7, 8, 9, 16, 22, 23 | fnlimfvre 44390 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π·) β ( β β(π β π β¦ ((πΉβπ)βπ₯))) β β) |
25 | 24 | elexd 3495 |
. . . . . . . . 9
β’ ((π β§ π₯ β π·) β ( β β(π β π β¦ ((πΉβπ)βπ₯))) β V) |
26 | 5, 25 | fvmpt2d 7012 |
. . . . . . . 8
β’ ((π β§ π₯ β π·) β (πΊβπ₯) = ( β β(π β π β¦ ((πΉβπ)βπ₯)))) |
27 | 26, 24 | eqeltrd 2834 |
. . . . . . 7
β’ ((π β§ π₯ β π·) β (πΊβπ₯) β β) |
28 | 3, 27 | syldan 592 |
. . . . . 6
β’ ((π β§ π₯ β (π· β© πΌ)) β (πΊβπ₯) β β) |
29 | 28 | adantr 482 |
. . . . 5
β’ (((π β§ π₯ β (π· β© πΌ)) β§ π¦ β β+) β (πΊβπ₯) β β) |
30 | | smflimlem4.7 |
. . . . . . . 8
β’ (π β π΄ β β) |
31 | 30 | adantr 482 |
. . . . . . 7
β’ ((π β§ π¦ β β+) β π΄ β
β) |
32 | | rpre 12982 |
. . . . . . . 8
β’ (π¦ β β+
β π¦ β
β) |
33 | 32 | adantl 483 |
. . . . . . 7
β’ ((π β§ π¦ β β+) β π¦ β
β) |
34 | 31, 33 | readdcld 11243 |
. . . . . 6
β’ ((π β§ π¦ β β+) β (π΄ + π¦) β β) |
35 | 34 | adantlr 714 |
. . . . 5
β’ (((π β§ π₯ β (π· β© πΌ)) β§ π¦ β β+) β (π΄ + π¦) β β) |
36 | | nfv 1918 |
. . . . . . . 8
β’
β²π((π β§ π₯ β (π· β© πΌ)) β§ π¦ β β+) |
37 | | rphalfcl 13001 |
. . . . . . . . . . 11
β’ (π¦ β β+
β (π¦ / 2) β
β+) |
38 | | rpgtrecnn 44090 |
. . . . . . . . . . 11
β’ ((π¦ / 2) β β+
β βπ β
β (1 / π) < (π¦ / 2)) |
39 | 37, 38 | syl 17 |
. . . . . . . . . 10
β’ (π¦ β β+
β βπ β
β (1 / π) < (π¦ / 2)) |
40 | 39 | adantl 483 |
. . . . . . . . 9
β’ (((π β§ π₯ β (π· β© πΌ)) β§ π¦ β β+) β
βπ β β (1
/ π) < (π¦ / 2)) |
41 | 10 | ad4antr 731 |
. . . . . . . . . . 11
β’
(((((π β§ π₯ β (π· β© πΌ)) β§ π¦ β β+) β§ π β β) β§ (1 /
π) < (π¦ / 2)) β π β SAlg) |
42 | 13 | adantlr 714 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β (π· β© πΌ)) β§ π β π) β (πΉβπ) β (SMblFnβπ)) |
43 | 42 | ad5ant15 758 |
. . . . . . . . . . 11
β’
((((((π β§ π₯ β (π· β© πΌ)) β§ π¦ β β+) β§ π β β) β§ (1 /
π) < (π¦ / 2)) β§ π β π) β (πΉβπ) β (SMblFnβπ)) |
44 | 30 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (π· β© πΌ)) β π΄ β β) |
45 | 44 | ad3antrrr 729 |
. . . . . . . . . . 11
β’
(((((π β§ π₯ β (π· β© πΌ)) β§ π¦ β β+) β§ π β β) β§ (1 /
π) < (π¦ / 2)) β π΄ β β) |
46 | | smflimlem4.8 |
. . . . . . . . . . . 12
β’ π = (π β π, π β β β¦ {π β π β£ {π₯ β dom (πΉβπ) β£ ((πΉβπ)βπ₯) < (π΄ + (1 / π))} = (π β© dom (πΉβπ))}) |
47 | | nfcv 2904 |
. . . . . . . . . . . . 13
β’
β²ππ |
48 | | nfcv 2904 |
. . . . . . . . . . . . 13
β’
β²ππ |
49 | | nfcv 2904 |
. . . . . . . . . . . . 13
β’
β²π{π β π β£ {π₯ β dom (πΉβπ) β£ ((πΉβπ)βπ₯) < (π΄ + (1 / π))} = (π β© dom (πΉβπ))} |
50 | | nfcv 2904 |
. . . . . . . . . . . . 13
β’
β²π{π β π β£ {π§ β dom (πΉβπ) β£ ((πΉβπ)βπ§) < (π΄ + (1 / π))} = (π β© dom (πΉβπ))} |
51 | 18 | breq1d 5159 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = π§ β (((πΉβπ)βπ₯) < (π΄ + (1 / π)) β ((πΉβπ)βπ§) < (π΄ + (1 / π)))) |
52 | 51 | cbvrabv 3443 |
. . . . . . . . . . . . . . . . 17
β’ {π₯ β dom (πΉβπ) β£ ((πΉβπ)βπ₯) < (π΄ + (1 / π))} = {π§ β dom (πΉβπ) β£ ((πΉβπ)βπ§) < (π΄ + (1 / π))} |
53 | 52 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (π = π β {π₯ β dom (πΉβπ) β£ ((πΉβπ)βπ₯) < (π΄ + (1 / π))} = {π§ β dom (πΉβπ) β£ ((πΉβπ)βπ§) < (π΄ + (1 / π))}) |
54 | | oveq2 7417 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β (1 / π) = (1 / π)) |
55 | 54 | oveq2d 7425 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β (π΄ + (1 / π)) = (π΄ + (1 / π))) |
56 | 55 | breq2d 5161 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (((πΉβπ)βπ§) < (π΄ + (1 / π)) β ((πΉβπ)βπ§) < (π΄ + (1 / π)))) |
57 | 56 | rabbidv 3441 |
. . . . . . . . . . . . . . . 16
β’ (π = π β {π§ β dom (πΉβπ) β£ ((πΉβπ)βπ§) < (π΄ + (1 / π))} = {π§ β dom (πΉβπ) β£ ((πΉβπ)βπ§) < (π΄ + (1 / π))}) |
58 | 53, 57 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
β’ (π = π β {π₯ β dom (πΉβπ) β£ ((πΉβπ)βπ₯) < (π΄ + (1 / π))} = {π§ β dom (πΉβπ) β£ ((πΉβπ)βπ§) < (π΄ + (1 / π))}) |
59 | 58 | eqeq1d 2735 |
. . . . . . . . . . . . . 14
β’ (π = π β ({π₯ β dom (πΉβπ) β£ ((πΉβπ)βπ₯) < (π΄ + (1 / π))} = (π β© dom (πΉβπ)) β {π§ β dom (πΉβπ) β£ ((πΉβπ)βπ§) < (π΄ + (1 / π))} = (π β© dom (πΉβπ)))) |
60 | 59 | rabbidv 3441 |
. . . . . . . . . . . . 13
β’ (π = π β {π β π β£ {π₯ β dom (πΉβπ) β£ ((πΉβπ)βπ₯) < (π΄ + (1 / π))} = (π β© dom (πΉβπ))} = {π β π β£ {π§ β dom (πΉβπ) β£ ((πΉβπ)βπ§) < (π΄ + (1 / π))} = (π β© dom (πΉβπ))}) |
61 | 47, 48, 49, 50, 60 | cbvmpo2 43786 |
. . . . . . . . . . . 12
β’ (π β π, π β β β¦ {π β π β£ {π₯ β dom (πΉβπ) β£ ((πΉβπ)βπ₯) < (π΄ + (1 / π))} = (π β© dom (πΉβπ))}) = (π β π, π β β β¦ {π β π β£ {π§ β dom (πΉβπ) β£ ((πΉβπ)βπ§) < (π΄ + (1 / π))} = (π β© dom (πΉβπ))}) |
62 | 46, 61 | eqtri 2761 |
. . . . . . . . . . 11
β’ π = (π β π, π β β β¦ {π β π β£ {π§ β dom (πΉβπ) β£ ((πΉβπ)βπ§) < (π΄ + (1 / π))} = (π β© dom (πΉβπ))}) |
63 | | smflimlem4.9 |
. . . . . . . . . . . 12
β’ π» = (π β π, π β β β¦ (πΆβ(πππ))) |
64 | | nfcv 2904 |
. . . . . . . . . . . . 13
β’
β²π(πΆβ(πππ)) |
65 | | nfcv 2904 |
. . . . . . . . . . . . 13
β’
β²π(πΆβ(πππ)) |
66 | | oveq2 7417 |
. . . . . . . . . . . . . 14
β’ (π = π β (πππ) = (πππ)) |
67 | 66 | fveq2d 6896 |
. . . . . . . . . . . . 13
β’ (π = π β (πΆβ(πππ)) = (πΆβ(πππ))) |
68 | 47, 48, 64, 65, 67 | cbvmpo2 43786 |
. . . . . . . . . . . 12
β’ (π β π, π β β β¦ (πΆβ(πππ))) = (π β π, π β β β¦ (πΆβ(πππ))) |
69 | 63, 68 | eqtri 2761 |
. . . . . . . . . . 11
β’ π» = (π β π, π β β β¦ (πΆβ(πππ))) |
70 | | smflimlem4.10 |
. . . . . . . . . . . 12
β’ πΌ = β© π β β βͺ π β π β© π β
(β€β₯βπ)(ππ»π) |
71 | | simpll 766 |
. . . . . . . . . . . . . . . 16
β’ (((π = π β§ π β π) β§ π β (β€β₯βπ)) β π = π) |
72 | 71 | oveq2d 7425 |
. . . . . . . . . . . . . . 15
β’ (((π = π β§ π β π) β§ π β (β€β₯βπ)) β (ππ»π) = (ππ»π)) |
73 | 72 | iineq2dv 5023 |
. . . . . . . . . . . . . 14
β’ ((π = π β§ π β π) β β©
π β
(β€β₯βπ)(ππ»π) = β© π β
(β€β₯βπ)(ππ»π)) |
74 | 73 | iuneq2dv 5022 |
. . . . . . . . . . . . 13
β’ (π = π β βͺ
π β π β© π β
(β€β₯βπ)(ππ»π) = βͺ π β π β© π β
(β€β₯βπ)(ππ»π)) |
75 | 74 | cbviinv 5045 |
. . . . . . . . . . . 12
β’ β© π β β βͺ π β π β© π β
(β€β₯βπ)(ππ»π) = β© π β β βͺ π β π β© π β
(β€β₯βπ)(ππ»π) |
76 | 70, 75 | eqtri 2761 |
. . . . . . . . . . 11
β’ πΌ = β© π β β βͺ π β π β© π β
(β€β₯βπ)(ππ»π) |
77 | | smflimlem4.11 |
. . . . . . . . . . . . 13
β’ ((π β§ π β ran π) β (πΆβπ) β π) |
78 | 77 | adantlr 714 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β (π· β© πΌ)) β§ π β ran π) β (πΆβπ) β π) |
79 | 78 | ad5ant15 758 |
. . . . . . . . . . 11
β’
((((((π β§ π₯ β (π· β© πΌ)) β§ π¦ β β+) β§ π β β) β§ (1 /
π) < (π¦ / 2)) β§ π β ran π) β (πΆβπ) β π) |
80 | | simp-4r 783 |
. . . . . . . . . . 11
β’
(((((π β§ π₯ β (π· β© πΌ)) β§ π¦ β β+) β§ π β β) β§ (1 /
π) < (π¦ / 2)) β π₯ β (π· β© πΌ)) |
81 | | simplr 768 |
. . . . . . . . . . 11
β’
(((((π β§ π₯ β (π· β© πΌ)) β§ π¦ β β+) β§ π β β) β§ (1 /
π) < (π¦ / 2)) β π β β) |
82 | 37 | ad3antlr 730 |
. . . . . . . . . . 11
β’
(((((π β§ π₯ β (π· β© πΌ)) β§ π¦ β β+) β§ π β β) β§ (1 /
π) < (π¦ / 2)) β (π¦ / 2) β
β+) |
83 | | simpr 486 |
. . . . . . . . . . 11
β’
(((((π β§ π₯ β (π· β© πΌ)) β§ π¦ β β+) β§ π β β) β§ (1 /
π) < (π¦ / 2)) β (1 / π) < (π¦ / 2)) |
84 | 9, 41, 43, 22, 45, 62, 69, 76, 79, 80, 81, 82, 83 | smflimlem3 45489 |
. . . . . . . . . 10
β’
(((((π β§ π₯ β (π· β© πΌ)) β§ π¦ β β+) β§ π β β) β§ (1 /
π) < (π¦ / 2)) β βπ β π βπ β (β€β₯βπ)(π₯ β dom (πΉβπ) β§ ((πΉβπ)βπ₯) < (π΄ + (π¦ / 2)))) |
85 | 84 | rexlimdva2 3158 |
. . . . . . . . 9
β’ (((π β§ π₯ β (π· β© πΌ)) β§ π¦ β β+) β
(βπ β β (1
/ π) < (π¦ / 2) β βπ β π βπ β (β€β₯βπ)(π₯ β dom (πΉβπ) β§ ((πΉβπ)βπ₯) < (π΄ + (π¦ / 2))))) |
86 | 40, 85 | mpd 15 |
. . . . . . . 8
β’ (((π β§ π₯ β (π· β© πΌ)) β§ π¦ β β+) β
βπ β π βπ β (β€β₯βπ)(π₯ β dom (πΉβπ) β§ ((πΉβπ)βπ₯) < (π΄ + (π¦ / 2)))) |
87 | | nfv 1918 |
. . . . . . . . . 10
β’
β²π((π β§ π₯ β (π· β© πΌ)) β§ π¦ β β+) |
88 | | nfcv 2904 |
. . . . . . . . . 10
β’
β²ππΉ |
89 | | nfcv 2904 |
. . . . . . . . . 10
β’
β²π₯πΉ |
90 | | smflimlem4.1 |
. . . . . . . . . . 11
β’ (π β π β β€) |
91 | 90 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π₯ β (π· β© πΌ)) β§ π¦ β β+) β π β
β€) |
92 | | eleq1w 2817 |
. . . . . . . . . . . . . 14
β’ (π = π β (π β π β π β π)) |
93 | 92 | anbi2d 630 |
. . . . . . . . . . . . 13
β’ (π = π β ((π β§ π β π) β (π β§ π β π))) |
94 | | fveq2 6892 |
. . . . . . . . . . . . . 14
β’ (π = π β (πΉβπ) = (πΉβπ)) |
95 | 94 | dmeqd 5906 |
. . . . . . . . . . . . . 14
β’ (π = π β dom (πΉβπ) = dom (πΉβπ)) |
96 | 94, 95 | feq12d 6706 |
. . . . . . . . . . . . 13
β’ (π = π β ((πΉβπ):dom (πΉβπ)βΆβ β (πΉβπ):dom (πΉβπ)βΆβ)) |
97 | 93, 96 | imbi12d 345 |
. . . . . . . . . . . 12
β’ (π = π β (((π β§ π β π) β (πΉβπ):dom (πΉβπ)βΆβ) β ((π β§ π β π) β (πΉβπ):dom (πΉβπ)βΆβ))) |
98 | 97, 15 | chvarvv 2003 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β (πΉβπ):dom (πΉβπ)βΆβ) |
99 | 98 | ad4ant14 751 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β (π· β© πΌ)) β§ π¦ β β+) β§ π β π) β (πΉβπ):dom (πΉβπ)βΆβ) |
100 | | fveq2 6892 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (πΉβπ) = (πΉβπ)) |
101 | 100 | dmeqd 5906 |
. . . . . . . . . . . . . . . 16
β’ (π = π β dom (πΉβπ) = dom (πΉβπ)) |
102 | 101 | cbviinv 5045 |
. . . . . . . . . . . . . . 15
β’ β© π β (β€β₯βπ)dom (πΉβπ) = β© π β
(β€β₯βπ)dom (πΉβπ) |
103 | 102 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β π β β©
π β
(β€β₯βπ)dom (πΉβπ) = β© π β
(β€β₯βπ)dom (πΉβπ)) |
104 | 103 | iuneq2i 5019 |
. . . . . . . . . . . . 13
β’ βͺ π β π β© π β
(β€β₯βπ)dom (πΉβπ) = βͺ π β π β© π β
(β€β₯βπ)dom (πΉβπ) |
105 | | fveq2 6892 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (β€β₯βπ) =
(β€β₯βπ)) |
106 | 105 | iineq1d 43779 |
. . . . . . . . . . . . . . 15
β’ (π = π β β©
π β
(β€β₯βπ)dom (πΉβπ) = β© π β
(β€β₯βπ)dom (πΉβπ)) |
107 | | fveq2 6892 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β (πΉβπ) = (πΉβπ)) |
108 | 107 | dmeqd 5906 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β dom (πΉβπ) = dom (πΉβπ)) |
109 | 108 | cbviinv 5045 |
. . . . . . . . . . . . . . . 16
β’ β© π β (β€β₯βπ)dom (πΉβπ) = β© π β
(β€β₯βπ)dom (πΉβπ) |
110 | 109 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (π = π β β©
π β
(β€β₯βπ)dom (πΉβπ) = β© π β
(β€β₯βπ)dom (πΉβπ)) |
111 | 106, 110 | eqtrd 2773 |
. . . . . . . . . . . . . 14
β’ (π = π β β©
π β
(β€β₯βπ)dom (πΉβπ) = β© π β
(β€β₯βπ)dom (πΉβπ)) |
112 | 111 | cbviunv 5044 |
. . . . . . . . . . . . 13
β’ βͺ π β π β© π β
(β€β₯βπ)dom (πΉβπ) = βͺ π β π β© π β
(β€β₯βπ)dom (πΉβπ) |
113 | 104, 112 | eqtri 2761 |
. . . . . . . . . . . 12
β’ βͺ π β π β© π β
(β€β₯βπ)dom (πΉβπ) = βͺ π β π β© π β
(β€β₯βπ)dom (πΉβπ) |
114 | 113 | rabeqi 3446 |
. . . . . . . . . . 11
β’ {π₯ β βͺ π β π β© π β
(β€β₯βπ)dom (πΉβπ) β£ (π β π β¦ ((πΉβπ)βπ₯)) β dom β } = {π₯ β βͺ
π β π β© π β
(β€β₯βπ)dom (πΉβπ) β£ (π β π β¦ ((πΉβπ)βπ₯)) β dom β } |
115 | | fveq2 6892 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (πΉβπ) = (πΉβπ)) |
116 | 115 | fveq1d 6894 |
. . . . . . . . . . . . . . 15
β’ (π = π β ((πΉβπ)βπ₯) = ((πΉβπ)βπ₯)) |
117 | 116 | cbvmptv 5262 |
. . . . . . . . . . . . . 14
β’ (π β π β¦ ((πΉβπ)βπ₯)) = (π β π β¦ ((πΉβπ)βπ₯)) |
118 | 117 | eqcomi 2742 |
. . . . . . . . . . . . 13
β’ (π β π β¦ ((πΉβπ)βπ₯)) = (π β π β¦ ((πΉβπ)βπ₯)) |
119 | 118 | eleq1i 2825 |
. . . . . . . . . . . 12
β’ ((π β π β¦ ((πΉβπ)βπ₯)) β dom β β (π β π β¦ ((πΉβπ)βπ₯)) β dom β ) |
120 | 119 | rabbii 3439 |
. . . . . . . . . . 11
β’ {π₯ β βͺ π β π β© π β
(β€β₯βπ)dom (πΉβπ) β£ (π β π β¦ ((πΉβπ)βπ₯)) β dom β } = {π₯ β βͺ
π β π β© π β
(β€β₯βπ)dom (πΉβπ) β£ (π β π β¦ ((πΉβπ)βπ₯)) β dom β } |
121 | 17, 114, 120 | 3eqtri 2765 |
. . . . . . . . . 10
β’ π· = {π₯ β βͺ
π β π β© π β
(β€β₯βπ)dom (πΉβπ) β£ (π β π β¦ ((πΉβπ)βπ₯)) β dom β } |
122 | 118 | fveq2i 6895 |
. . . . . . . . . . . 12
β’ ( β
β(π β π β¦ ((πΉβπ)βπ₯))) = ( β β(π β π β¦ ((πΉβπ)βπ₯))) |
123 | 122 | mpteq2i 5254 |
. . . . . . . . . . 11
β’ (π₯ β π· β¦ ( β β(π β π β¦ ((πΉβπ)βπ₯)))) = (π₯ β π· β¦ ( β β(π β π β¦ ((πΉβπ)βπ₯)))) |
124 | 4, 123 | eqtri 2761 |
. . . . . . . . . 10
β’ πΊ = (π₯ β π· β¦ ( β β(π β π β¦ ((πΉβπ)βπ₯)))) |
125 | 3 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ π₯ β (π· β© πΌ)) β§ π¦ β β+) β π₯ β π·) |
126 | 37 | adantl 483 |
. . . . . . . . . 10
β’ (((π β§ π₯ β (π· β© πΌ)) β§ π¦ β β+) β (π¦ / 2) β
β+) |
127 | 87, 88, 89, 91, 9, 99, 121, 124, 125, 126 | fnlimabslt 44395 |
. . . . . . . . 9
β’ (((π β§ π₯ β (π· β© πΌ)) β§ π¦ β β+) β
βπ β π βπ β (β€β₯βπ)(((πΉβπ)βπ₯) β β β§ (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < (π¦ / 2))) |
128 | 29 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π₯ β (π· β© πΌ)) β§ π¦ β β+) β§ ((πΉβπ)βπ₯) β β) β (πΊβπ₯) β β) |
129 | | simpr 486 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π₯ β (π· β© πΌ)) β§ π¦ β β+) β§ ((πΉβπ)βπ₯) β β) β ((πΉβπ)βπ₯) β β) |
130 | 128, 129 | resubcld 11642 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π₯ β (π· β© πΌ)) β§ π¦ β β+) β§ ((πΉβπ)βπ₯) β β) β ((πΊβπ₯) β ((πΉβπ)βπ₯)) β β) |
131 | 130 | adantrr 716 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π₯ β (π· β© πΌ)) β§ π¦ β β+) β§ (((πΉβπ)βπ₯) β β β§ (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < (π¦ / 2))) β ((πΊβπ₯) β ((πΉβπ)βπ₯)) β β) |
132 | 130 | recnd 11242 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π₯ β (π· β© πΌ)) β§ π¦ β β+) β§ ((πΉβπ)βπ₯) β β) β ((πΊβπ₯) β ((πΉβπ)βπ₯)) β β) |
133 | 132 | abscld 15383 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π₯ β (π· β© πΌ)) β§ π¦ β β+) β§ ((πΉβπ)βπ₯) β β) β (absβ((πΊβπ₯) β ((πΉβπ)βπ₯))) β β) |
134 | 133 | adantrr 716 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π₯ β (π· β© πΌ)) β§ π¦ β β+) β§ (((πΉβπ)βπ₯) β β β§ (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < (π¦ / 2))) β (absβ((πΊβπ₯) β ((πΉβπ)βπ₯))) β β) |
135 | 32 | rehalfcld 12459 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ β β+
β (π¦ / 2) β
β) |
136 | 135 | ad2antlr 726 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π₯ β (π· β© πΌ)) β§ π¦ β β+) β§ (((πΉβπ)βπ₯) β β β§ (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < (π¦ / 2))) β (π¦ / 2) β β) |
137 | 131 | leabsd 15361 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π₯ β (π· β© πΌ)) β§ π¦ β β+) β§ (((πΉβπ)βπ₯) β β β§ (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < (π¦ / 2))) β ((πΊβπ₯) β ((πΉβπ)βπ₯)) β€ (absβ((πΊβπ₯) β ((πΉβπ)βπ₯)))) |
138 | 28 | recnd 11242 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π₯ β (π· β© πΌ)) β (πΊβπ₯) β β) |
139 | 138 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π₯ β (π· β© πΌ)) β§ ((πΉβπ)βπ₯) β β) β (πΊβπ₯) β β) |
140 | | recn 11200 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((πΉβπ)βπ₯) β β β ((πΉβπ)βπ₯) β β) |
141 | 140 | adantl 483 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π₯ β (π· β© πΌ)) β§ ((πΉβπ)βπ₯) β β) β ((πΉβπ)βπ₯) β β) |
142 | 139, 141 | abssubd 15400 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π₯ β (π· β© πΌ)) β§ ((πΉβπ)βπ₯) β β) β (absβ((πΊβπ₯) β ((πΉβπ)βπ₯))) = (absβ(((πΉβπ)βπ₯) β (πΊβπ₯)))) |
143 | 142 | adantrr 716 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π₯ β (π· β© πΌ)) β§ (((πΉβπ)βπ₯) β β β§ (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < (π¦ / 2))) β (absβ((πΊβπ₯) β ((πΉβπ)βπ₯))) = (absβ(((πΉβπ)βπ₯) β (πΊβπ₯)))) |
144 | | simprr 772 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π₯ β (π· β© πΌ)) β§ (((πΉβπ)βπ₯) β β β§ (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < (π¦ / 2))) β (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < (π¦ / 2)) |
145 | 143, 144 | eqbrtrd 5171 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π₯ β (π· β© πΌ)) β§ (((πΉβπ)βπ₯) β β β§ (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < (π¦ / 2))) β (absβ((πΊβπ₯) β ((πΉβπ)βπ₯))) < (π¦ / 2)) |
146 | 145 | adantlr 714 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π₯ β (π· β© πΌ)) β§ π¦ β β+) β§ (((πΉβπ)βπ₯) β β β§ (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < (π¦ / 2))) β (absβ((πΊβπ₯) β ((πΉβπ)βπ₯))) < (π¦ / 2)) |
147 | 131, 134,
136, 137, 146 | lelttrd 11372 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π₯ β (π· β© πΌ)) β§ π¦ β β+) β§ (((πΉβπ)βπ₯) β β β§ (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < (π¦ / 2))) β ((πΊβπ₯) β ((πΉβπ)βπ₯)) < (π¦ / 2)) |
148 | 29 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π₯ β (π· β© πΌ)) β§ π¦ β β+) β§ (((πΉβπ)βπ₯) β β β§ (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < (π¦ / 2))) β (πΊβπ₯) β β) |
149 | | simprl 770 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π₯ β (π· β© πΌ)) β§ π¦ β β+) β§ (((πΉβπ)βπ₯) β β β§ (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < (π¦ / 2))) β ((πΉβπ)βπ₯) β β) |
150 | 148, 149,
136 | ltsubadd2d 11812 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π₯ β (π· β© πΌ)) β§ π¦ β β+) β§ (((πΉβπ)βπ₯) β β β§ (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < (π¦ / 2))) β (((πΊβπ₯) β ((πΉβπ)βπ₯)) < (π¦ / 2) β (πΊβπ₯) < (((πΉβπ)βπ₯) + (π¦ / 2)))) |
151 | 147, 150 | mpbid 231 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π₯ β (π· β© πΌ)) β§ π¦ β β+) β§ (((πΉβπ)βπ₯) β β β§ (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < (π¦ / 2))) β (πΊβπ₯) < (((πΉβπ)βπ₯) + (π¦ / 2))) |
152 | 151 | ex 414 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β (π· β© πΌ)) β§ π¦ β β+) β ((((πΉβπ)βπ₯) β β β§ (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < (π¦ / 2)) β (πΊβπ₯) < (((πΉβπ)βπ₯) + (π¦ / 2)))) |
153 | 152 | ad2antrr 725 |
. . . . . . . . . . . 12
β’
(((((π β§ π₯ β (π· β© πΌ)) β§ π¦ β β+) β§ π β π) β§ π β (β€β₯βπ)) β ((((πΉβπ)βπ₯) β β β§ (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < (π¦ / 2)) β (πΊβπ₯) < (((πΉβπ)βπ₯) + (π¦ / 2)))) |
154 | 153 | ralimdva 3168 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β (π· β© πΌ)) β§ π¦ β β+) β§ π β π) β (βπ β (β€β₯βπ)(((πΉβπ)βπ₯) β β β§ (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < (π¦ / 2)) β βπ β (β€β₯βπ)(πΊβπ₯) < (((πΉβπ)βπ₯) + (π¦ / 2)))) |
155 | 154 | ex 414 |
. . . . . . . . . 10
β’ (((π β§ π₯ β (π· β© πΌ)) β§ π¦ β β+) β (π β π β (βπ β (β€β₯βπ)(((πΉβπ)βπ₯) β β β§ (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < (π¦ / 2)) β βπ β (β€β₯βπ)(πΊβπ₯) < (((πΉβπ)βπ₯) + (π¦ / 2))))) |
156 | 36, 155 | reximdai 3259 |
. . . . . . . . 9
β’ (((π β§ π₯ β (π· β© πΌ)) β§ π¦ β β+) β
(βπ β π βπ β (β€β₯βπ)(((πΉβπ)βπ₯) β β β§ (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < (π¦ / 2)) β βπ β π βπ β (β€β₯βπ)(πΊβπ₯) < (((πΉβπ)βπ₯) + (π¦ / 2)))) |
157 | 127, 156 | mpd 15 |
. . . . . . . 8
β’ (((π β§ π₯ β (π· β© πΌ)) β§ π¦ β β+) β
βπ β π βπ β (β€β₯βπ)(πΊβπ₯) < (((πΉβπ)βπ₯) + (π¦ / 2))) |
158 | 115 | dmeqd 5906 |
. . . . . . . . . 10
β’ (π = π β dom (πΉβπ) = dom (πΉβπ)) |
159 | 158 | eleq2d 2820 |
. . . . . . . . 9
β’ (π = π β (π₯ β dom (πΉβπ) β π₯ β dom (πΉβπ))) |
160 | 116 | breq1d 5159 |
. . . . . . . . 9
β’ (π = π β (((πΉβπ)βπ₯) < (π΄ + (π¦ / 2)) β ((πΉβπ)βπ₯) < (π΄ + (π¦ / 2)))) |
161 | 159, 160 | anbi12d 632 |
. . . . . . . 8
β’ (π = π β ((π₯ β dom (πΉβπ) β§ ((πΉβπ)βπ₯) < (π΄ + (π¦ / 2))) β (π₯ β dom (πΉβπ) β§ ((πΉβπ)βπ₯) < (π΄ + (π¦ / 2))))) |
162 | 116 | oveq1d 7424 |
. . . . . . . . 9
β’ (π = π β (((πΉβπ)βπ₯) + (π¦ / 2)) = (((πΉβπ)βπ₯) + (π¦ / 2))) |
163 | 162 | breq2d 5161 |
. . . . . . . 8
β’ (π = π β ((πΊβπ₯) < (((πΉβπ)βπ₯) + (π¦ / 2)) β (πΊβπ₯) < (((πΉβπ)βπ₯) + (π¦ / 2)))) |
164 | 36, 9, 86, 157, 161, 163 | rexanuz3 43785 |
. . . . . . 7
β’ (((π β§ π₯ β (π· β© πΌ)) β§ π¦ β β+) β
βπ β π ((π₯ β dom (πΉβπ) β§ ((πΉβπ)βπ₯) < (π΄ + (π¦ / 2))) β§ (πΊβπ₯) < (((πΉβπ)βπ₯) + (π¦ / 2)))) |
165 | | df-3an 1090 |
. . . . . . . . 9
β’ ((π₯ β dom (πΉβπ) β§ ((πΉβπ)βπ₯) < (π΄ + (π¦ / 2)) β§ (πΊβπ₯) < (((πΉβπ)βπ₯) + (π¦ / 2))) β ((π₯ β dom (πΉβπ) β§ ((πΉβπ)βπ₯) < (π΄ + (π¦ / 2))) β§ (πΊβπ₯) < (((πΉβπ)βπ₯) + (π¦ / 2)))) |
166 | | 3ancomb 1100 |
. . . . . . . . 9
β’ ((π₯ β dom (πΉβπ) β§ ((πΉβπ)βπ₯) < (π΄ + (π¦ / 2)) β§ (πΊβπ₯) < (((πΉβπ)βπ₯) + (π¦ / 2))) β (π₯ β dom (πΉβπ) β§ (πΊβπ₯) < (((πΉβπ)βπ₯) + (π¦ / 2)) β§ ((πΉβπ)βπ₯) < (π΄ + (π¦ / 2)))) |
167 | 165, 166 | bitr3i 277 |
. . . . . . . 8
β’ (((π₯ β dom (πΉβπ) β§ ((πΉβπ)βπ₯) < (π΄ + (π¦ / 2))) β§ (πΊβπ₯) < (((πΉβπ)βπ₯) + (π¦ / 2))) β (π₯ β dom (πΉβπ) β§ (πΊβπ₯) < (((πΉβπ)βπ₯) + (π¦ / 2)) β§ ((πΉβπ)βπ₯) < (π΄ + (π¦ / 2)))) |
168 | 167 | rexbii 3095 |
. . . . . . 7
β’
(βπ β
π ((π₯ β dom (πΉβπ) β§ ((πΉβπ)βπ₯) < (π΄ + (π¦ / 2))) β§ (πΊβπ₯) < (((πΉβπ)βπ₯) + (π¦ / 2))) β βπ β π (π₯ β dom (πΉβπ) β§ (πΊβπ₯) < (((πΉβπ)βπ₯) + (π¦ / 2)) β§ ((πΉβπ)βπ₯) < (π΄ + (π¦ / 2)))) |
169 | 164, 168 | sylib 217 |
. . . . . 6
β’ (((π β§ π₯ β (π· β© πΌ)) β§ π¦ β β+) β
βπ β π (π₯ β dom (πΉβπ) β§ (πΊβπ₯) < (((πΉβπ)βπ₯) + (π¦ / 2)) β§ ((πΉβπ)βπ₯) < (π΄ + (π¦ / 2)))) |
170 | 29 | ad2antrr 725 |
. . . . . . . . 9
β’
(((((π β§ π₯ β (π· β© πΌ)) β§ π¦ β β+) β§ π β π) β§ (π₯ β dom (πΉβπ) β§ (πΊβπ₯) < (((πΉβπ)βπ₯) + (π¦ / 2)) β§ ((πΉβπ)βπ₯) < (π΄ + (π¦ / 2)))) β (πΊβπ₯) β β) |
171 | 15 | 3adant3 1133 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π β§ π₯ β dom (πΉβπ)) β (πΉβπ):dom (πΉβπ)βΆβ) |
172 | | simp3 1139 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π β§ π₯ β dom (πΉβπ)) β π₯ β dom (πΉβπ)) |
173 | 171, 172 | ffvelcdmd 7088 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π β§ π₯ β dom (πΉβπ)) β ((πΉβπ)βπ₯) β β) |
174 | 173 | ad4ant134 1175 |
. . . . . . . . . . . 12
β’ ((((π β§ π¦ β β+) β§ π β π) β§ π₯ β dom (πΉβπ)) β ((πΉβπ)βπ₯) β β) |
175 | | simpllr 775 |
. . . . . . . . . . . . 13
β’ ((((π β§ π¦ β β+) β§ π β π) β§ π₯ β dom (πΉβπ)) β π¦ β β+) |
176 | 175, 135 | syl 17 |
. . . . . . . . . . . 12
β’ ((((π β§ π¦ β β+) β§ π β π) β§ π₯ β dom (πΉβπ)) β (π¦ / 2) β β) |
177 | 174, 176 | readdcld 11243 |
. . . . . . . . . . 11
β’ ((((π β§ π¦ β β+) β§ π β π) β§ π₯ β dom (πΉβπ)) β (((πΉβπ)βπ₯) + (π¦ / 2)) β β) |
178 | 177 | adantl3r 749 |
. . . . . . . . . 10
β’
(((((π β§ π₯ β (π· β© πΌ)) β§ π¦ β β+) β§ π β π) β§ π₯ β dom (πΉβπ)) β (((πΉβπ)βπ₯) + (π¦ / 2)) β β) |
179 | 178 | 3ad2antr1 1189 |
. . . . . . . . 9
β’
(((((π β§ π₯ β (π· β© πΌ)) β§ π¦ β β+) β§ π β π) β§ (π₯ β dom (πΉβπ) β§ (πΊβπ₯) < (((πΉβπ)βπ₯) + (π¦ / 2)) β§ ((πΉβπ)βπ₯) < (π΄ + (π¦ / 2)))) β (((πΉβπ)βπ₯) + (π¦ / 2)) β β) |
180 | | rehalfcl 12438 |
. . . . . . . . . . . . . 14
β’ (π¦ β β β (π¦ / 2) β
β) |
181 | 33, 180 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β§ π¦ β β+) β (π¦ / 2) β
β) |
182 | 31, 181 | jca 513 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β β+) β (π΄ β β β§ (π¦ / 2) β
β)) |
183 | | readdcl 11193 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ (π¦ / 2) β β) β
(π΄ + (π¦ / 2)) β β) |
184 | 182, 183 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β β+) β (π΄ + (π¦ / 2)) β β) |
185 | 184, 181 | readdcld 11243 |
. . . . . . . . . 10
β’ ((π β§ π¦ β β+) β ((π΄ + (π¦ / 2)) + (π¦ / 2)) β β) |
186 | 185 | ad5ant13 756 |
. . . . . . . . 9
β’
(((((π β§ π₯ β (π· β© πΌ)) β§ π¦ β β+) β§ π β π) β§ (π₯ β dom (πΉβπ) β§ (πΊβπ₯) < (((πΉβπ)βπ₯) + (π¦ / 2)) β§ ((πΉβπ)βπ₯) < (π΄ + (π¦ / 2)))) β ((π΄ + (π¦ / 2)) + (π¦ / 2)) β β) |
187 | | simpr2 1196 |
. . . . . . . . 9
β’
(((((π β§ π₯ β (π· β© πΌ)) β§ π¦ β β+) β§ π β π) β§ (π₯ β dom (πΉβπ) β§ (πΊβπ₯) < (((πΉβπ)βπ₯) + (π¦ / 2)) β§ ((πΉβπ)βπ₯) < (π΄ + (π¦ / 2)))) β (πΊβπ₯) < (((πΉβπ)βπ₯) + (π¦ / 2))) |
188 | 174 | adantrr 716 |
. . . . . . . . . . . 12
β’ ((((π β§ π¦ β β+) β§ π β π) β§ (π₯ β dom (πΉβπ) β§ ((πΉβπ)βπ₯) < (π΄ + (π¦ / 2)))) β ((πΉβπ)βπ₯) β β) |
189 | 184 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ ((((π β§ π¦ β β+) β§ π β π) β§ (π₯ β dom (πΉβπ) β§ ((πΉβπ)βπ₯) < (π΄ + (π¦ / 2)))) β (π΄ + (π¦ / 2)) β β) |
190 | 176 | adantrr 716 |
. . . . . . . . . . . 12
β’ ((((π β§ π¦ β β+) β§ π β π) β§ (π₯ β dom (πΉβπ) β§ ((πΉβπ)βπ₯) < (π΄ + (π¦ / 2)))) β (π¦ / 2) β β) |
191 | | simprr 772 |
. . . . . . . . . . . 12
β’ ((((π β§ π¦ β β+) β§ π β π) β§ (π₯ β dom (πΉβπ) β§ ((πΉβπ)βπ₯) < (π΄ + (π¦ / 2)))) β ((πΉβπ)βπ₯) < (π΄ + (π¦ / 2))) |
192 | 188, 189,
190, 191 | ltadd1dd 11825 |
. . . . . . . . . . 11
β’ ((((π β§ π¦ β β+) β§ π β π) β§ (π₯ β dom (πΉβπ) β§ ((πΉβπ)βπ₯) < (π΄ + (π¦ / 2)))) β (((πΉβπ)βπ₯) + (π¦ / 2)) < ((π΄ + (π¦ / 2)) + (π¦ / 2))) |
193 | 192 | adantl3r 749 |
. . . . . . . . . 10
β’
(((((π β§ π₯ β (π· β© πΌ)) β§ π¦ β β+) β§ π β π) β§ (π₯ β dom (πΉβπ) β§ ((πΉβπ)βπ₯) < (π΄ + (π¦ / 2)))) β (((πΉβπ)βπ₯) + (π¦ / 2)) < ((π΄ + (π¦ / 2)) + (π¦ / 2))) |
194 | 193 | 3adantr2 1171 |
. . . . . . . . 9
β’
(((((π β§ π₯ β (π· β© πΌ)) β§ π¦ β β+) β§ π β π) β§ (π₯ β dom (πΉβπ) β§ (πΊβπ₯) < (((πΉβπ)βπ₯) + (π¦ / 2)) β§ ((πΉβπ)βπ₯) < (π΄ + (π¦ / 2)))) β (((πΉβπ)βπ₯) + (π¦ / 2)) < ((π΄ + (π¦ / 2)) + (π¦ / 2))) |
195 | 170, 179,
186, 187, 194 | lttrd 11375 |
. . . . . . . 8
β’
(((((π β§ π₯ β (π· β© πΌ)) β§ π¦ β β+) β§ π β π) β§ (π₯ β dom (πΉβπ) β§ (πΊβπ₯) < (((πΉβπ)βπ₯) + (π¦ / 2)) β§ ((πΉβπ)βπ₯) < (π΄ + (π¦ / 2)))) β (πΊβπ₯) < ((π΄ + (π¦ / 2)) + (π¦ / 2))) |
196 | 31 | recnd 11242 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β β+) β π΄ β
β) |
197 | 181 | recnd 11242 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β β+) β (π¦ / 2) β
β) |
198 | 196, 197,
197 | addassd 11236 |
. . . . . . . . . 10
β’ ((π β§ π¦ β β+) β ((π΄ + (π¦ / 2)) + (π¦ / 2)) = (π΄ + ((π¦ / 2) + (π¦ / 2)))) |
199 | 32 | recnd 11242 |
. . . . . . . . . . . . 13
β’ (π¦ β β+
β π¦ β
β) |
200 | | 2halves 12440 |
. . . . . . . . . . . . 13
β’ (π¦ β β β ((π¦ / 2) + (π¦ / 2)) = π¦) |
201 | 199, 200 | syl 17 |
. . . . . . . . . . . 12
β’ (π¦ β β+
β ((π¦ / 2) + (π¦ / 2)) = π¦) |
202 | 201 | oveq2d 7425 |
. . . . . . . . . . 11
β’ (π¦ β β+
β (π΄ + ((π¦ / 2) + (π¦ / 2))) = (π΄ + π¦)) |
203 | 202 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π¦ β β+) β (π΄ + ((π¦ / 2) + (π¦ / 2))) = (π΄ + π¦)) |
204 | 198, 203 | eqtrd 2773 |
. . . . . . . . 9
β’ ((π β§ π¦ β β+) β ((π΄ + (π¦ / 2)) + (π¦ / 2)) = (π΄ + π¦)) |
205 | 204 | ad5ant13 756 |
. . . . . . . 8
β’
(((((π β§ π₯ β (π· β© πΌ)) β§ π¦ β β+) β§ π β π) β§ (π₯ β dom (πΉβπ) β§ (πΊβπ₯) < (((πΉβπ)βπ₯) + (π¦ / 2)) β§ ((πΉβπ)βπ₯) < (π΄ + (π¦ / 2)))) β ((π΄ + (π¦ / 2)) + (π¦ / 2)) = (π΄ + π¦)) |
206 | 195, 205 | breqtrd 5175 |
. . . . . . 7
β’
(((((π β§ π₯ β (π· β© πΌ)) β§ π¦ β β+) β§ π β π) β§ (π₯ β dom (πΉβπ) β§ (πΊβπ₯) < (((πΉβπ)βπ₯) + (π¦ / 2)) β§ ((πΉβπ)βπ₯) < (π΄ + (π¦ / 2)))) β (πΊβπ₯) < (π΄ + π¦)) |
207 | 206 | rexlimdva2 3158 |
. . . . . 6
β’ (((π β§ π₯ β (π· β© πΌ)) β§ π¦ β β+) β
(βπ β π (π₯ β dom (πΉβπ) β§ (πΊβπ₯) < (((πΉβπ)βπ₯) + (π¦ / 2)) β§ ((πΉβπ)βπ₯) < (π΄ + (π¦ / 2))) β (πΊβπ₯) < (π΄ + π¦))) |
208 | 169, 207 | mpd 15 |
. . . . 5
β’ (((π β§ π₯ β (π· β© πΌ)) β§ π¦ β β+) β (πΊβπ₯) < (π΄ + π¦)) |
209 | 29, 35, 208 | ltled 11362 |
. . . 4
β’ (((π β§ π₯ β (π· β© πΌ)) β§ π¦ β β+) β (πΊβπ₯) β€ (π΄ + π¦)) |
210 | 209 | ralrimiva 3147 |
. . 3
β’ ((π β§ π₯ β (π· β© πΌ)) β βπ¦ β β+ (πΊβπ₯) β€ (π΄ + π¦)) |
211 | | alrple 13185 |
. . . 4
β’ (((πΊβπ₯) β β β§ π΄ β β) β ((πΊβπ₯) β€ π΄ β βπ¦ β β+ (πΊβπ₯) β€ (π΄ + π¦))) |
212 | 28, 44, 211 | syl2anc 585 |
. . 3
β’ ((π β§ π₯ β (π· β© πΌ)) β ((πΊβπ₯) β€ π΄ β βπ¦ β β+ (πΊβπ₯) β€ (π΄ + π¦))) |
213 | 210, 212 | mpbird 257 |
. 2
β’ ((π β§ π₯ β (π· β© πΌ)) β (πΊβπ₯) β€ π΄) |
214 | 2, 213 | ssrabdv 4072 |
1
β’ (π β (π· β© πΌ) β {π₯ β π· β£ (πΊβπ₯) β€ π΄}) |