Step | Hyp | Ref
| Expression |
1 | | iscau3.3 |
. . 3
β’ (π β π· β (βMetβπ)) |
2 | | iscau2 24664 |
. . 3
β’ (π· β (βMetβπ) β (πΉ β (Cauβπ·) β (πΉ β (π βpm β) β§
βπ₯ β
β+ βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯)))) |
3 | 1, 2 | syl 17 |
. 2
β’ (π β (πΉ β (Cauβπ·) β (πΉ β (π βpm β) β§
βπ₯ β
β+ βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯)))) |
4 | 1 | adantr 482 |
. . . . . 6
β’ ((π β§ πΉ β (π βpm β)) β π· β (βMetβπ)) |
5 | | ssid 3970 |
. . . . . . 7
β’ β€
β β€ |
6 | | simpr 486 |
. . . . . . 7
β’ ((π β dom πΉ β§ (πΉβπ) β π) β (πΉβπ) β π) |
7 | | eleq1 2822 |
. . . . . . 7
β’ ((πΉβπ) = (πΉβπ) β ((πΉβπ) β π β (πΉβπ) β π)) |
8 | | eleq1 2822 |
. . . . . . 7
β’ ((πΉβπ) = (πΉβπ) β ((πΉβπ) β π β (πΉβπ) β π)) |
9 | | xmetsym 23723 |
. . . . . . . 8
β’ ((π· β (βMetβπ) β§ (πΉβπ) β π β§ (πΉβπ) β π) β ((πΉβπ)π·(πΉβπ)) = ((πΉβπ)π·(πΉβπ))) |
10 | 9 | fveq2d 6850 |
. . . . . . 7
β’ ((π· β (βMetβπ) β§ (πΉβπ) β π β§ (πΉβπ) β π) β ( I β((πΉβπ)π·(πΉβπ))) = ( I β((πΉβπ)π·(πΉβπ)))) |
11 | | xmetsym 23723 |
. . . . . . . 8
β’ ((π· β (βMetβπ) β§ (πΉβπ) β π β§ (πΉβπ) β π) β ((πΉβπ)π·(πΉβπ)) = ((πΉβπ)π·(πΉβπ))) |
12 | 11 | fveq2d 6850 |
. . . . . . 7
β’ ((π· β (βMetβπ) β§ (πΉβπ) β π β§ (πΉβπ) β π) β ( I β((πΉβπ)π·(πΉβπ))) = ( I β((πΉβπ)π·(πΉβπ)))) |
13 | | simp1 1137 |
. . . . . . . . . . 11
β’ ((π· β (βMetβπ) β§ ((πΉβπ) β π β§ (πΉβπ) β π) β§ ((πΉβπ) β π β§ π₯ β β)) β π· β (βMetβπ)) |
14 | | simp2l 1200 |
. . . . . . . . . . 11
β’ ((π· β (βMetβπ) β§ ((πΉβπ) β π β§ (πΉβπ) β π) β§ ((πΉβπ) β π β§ π₯ β β)) β (πΉβπ) β π) |
15 | | simp3l 1202 |
. . . . . . . . . . 11
β’ ((π· β (βMetβπ) β§ ((πΉβπ) β π β§ (πΉβπ) β π) β§ ((πΉβπ) β π β§ π₯ β β)) β (πΉβπ) β π) |
16 | | xmetcl 23707 |
. . . . . . . . . . 11
β’ ((π· β (βMetβπ) β§ (πΉβπ) β π β§ (πΉβπ) β π) β ((πΉβπ)π·(πΉβπ)) β
β*) |
17 | 13, 14, 15, 16 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((π· β (βMetβπ) β§ ((πΉβπ) β π β§ (πΉβπ) β π) β§ ((πΉβπ) β π β§ π₯ β β)) β ((πΉβπ)π·(πΉβπ)) β
β*) |
18 | | simp2r 1201 |
. . . . . . . . . . 11
β’ ((π· β (βMetβπ) β§ ((πΉβπ) β π β§ (πΉβπ) β π) β§ ((πΉβπ) β π β§ π₯ β β)) β (πΉβπ) β π) |
19 | | xmetcl 23707 |
. . . . . . . . . . 11
β’ ((π· β (βMetβπ) β§ (πΉβπ) β π β§ (πΉβπ) β π) β ((πΉβπ)π·(πΉβπ)) β
β*) |
20 | 13, 15, 18, 19 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((π· β (βMetβπ) β§ ((πΉβπ) β π β§ (πΉβπ) β π) β§ ((πΉβπ) β π β§ π₯ β β)) β ((πΉβπ)π·(πΉβπ)) β
β*) |
21 | | simp3r 1203 |
. . . . . . . . . . . 12
β’ ((π· β (βMetβπ) β§ ((πΉβπ) β π β§ (πΉβπ) β π) β§ ((πΉβπ) β π β§ π₯ β β)) β π₯ β β) |
22 | 21 | rehalfcld 12408 |
. . . . . . . . . . 11
β’ ((π· β (βMetβπ) β§ ((πΉβπ) β π β§ (πΉβπ) β π) β§ ((πΉβπ) β π β§ π₯ β β)) β (π₯ / 2) β β) |
23 | 22 | rexrd 11213 |
. . . . . . . . . 10
β’ ((π· β (βMetβπ) β§ ((πΉβπ) β π β§ (πΉβπ) β π) β§ ((πΉβπ) β π β§ π₯ β β)) β (π₯ / 2) β
β*) |
24 | | xlt2add 13188 |
. . . . . . . . . 10
β’
(((((πΉβπ)π·(πΉβπ)) β β* β§ ((πΉβπ)π·(πΉβπ)) β β*) β§ ((π₯ / 2) β β*
β§ (π₯ / 2) β
β*)) β ((((πΉβπ)π·(πΉβπ)) < (π₯ / 2) β§ ((πΉβπ)π·(πΉβπ)) < (π₯ / 2)) β (((πΉβπ)π·(πΉβπ)) +π ((πΉβπ)π·(πΉβπ))) < ((π₯ / 2) +π (π₯ / 2)))) |
25 | 17, 20, 23, 23, 24 | syl22anc 838 |
. . . . . . . . 9
β’ ((π· β (βMetβπ) β§ ((πΉβπ) β π β§ (πΉβπ) β π) β§ ((πΉβπ) β π β§ π₯ β β)) β ((((πΉβπ)π·(πΉβπ)) < (π₯ / 2) β§ ((πΉβπ)π·(πΉβπ)) < (π₯ / 2)) β (((πΉβπ)π·(πΉβπ)) +π ((πΉβπ)π·(πΉβπ))) < ((π₯ / 2) +π (π₯ / 2)))) |
26 | 22, 22 | rexaddd 13162 |
. . . . . . . . . . . 12
β’ ((π· β (βMetβπ) β§ ((πΉβπ) β π β§ (πΉβπ) β π) β§ ((πΉβπ) β π β§ π₯ β β)) β ((π₯ / 2) +π (π₯ / 2)) = ((π₯ / 2) + (π₯ / 2))) |
27 | 21 | recnd 11191 |
. . . . . . . . . . . . 13
β’ ((π· β (βMetβπ) β§ ((πΉβπ) β π β§ (πΉβπ) β π) β§ ((πΉβπ) β π β§ π₯ β β)) β π₯ β β) |
28 | 27 | 2halvesd 12407 |
. . . . . . . . . . . 12
β’ ((π· β (βMetβπ) β§ ((πΉβπ) β π β§ (πΉβπ) β π) β§ ((πΉβπ) β π β§ π₯ β β)) β ((π₯ / 2) + (π₯ / 2)) = π₯) |
29 | 26, 28 | eqtrd 2773 |
. . . . . . . . . . 11
β’ ((π· β (βMetβπ) β§ ((πΉβπ) β π β§ (πΉβπ) β π) β§ ((πΉβπ) β π β§ π₯ β β)) β ((π₯ / 2) +π (π₯ / 2)) = π₯) |
30 | 29 | breq2d 5121 |
. . . . . . . . . 10
β’ ((π· β (βMetβπ) β§ ((πΉβπ) β π β§ (πΉβπ) β π) β§ ((πΉβπ) β π β§ π₯ β β)) β ((((πΉβπ)π·(πΉβπ)) +π ((πΉβπ)π·(πΉβπ))) < ((π₯ / 2) +π (π₯ / 2)) β (((πΉβπ)π·(πΉβπ)) +π ((πΉβπ)π·(πΉβπ))) < π₯)) |
31 | | xmettri 23727 |
. . . . . . . . . . . 12
β’ ((π· β (βMetβπ) β§ ((πΉβπ) β π β§ (πΉβπ) β π β§ (πΉβπ) β π)) β ((πΉβπ)π·(πΉβπ)) β€ (((πΉβπ)π·(πΉβπ)) +π ((πΉβπ)π·(πΉβπ)))) |
32 | 13, 14, 18, 15, 31 | syl13anc 1373 |
. . . . . . . . . . 11
β’ ((π· β (βMetβπ) β§ ((πΉβπ) β π β§ (πΉβπ) β π) β§ ((πΉβπ) β π β§ π₯ β β)) β ((πΉβπ)π·(πΉβπ)) β€ (((πΉβπ)π·(πΉβπ)) +π ((πΉβπ)π·(πΉβπ)))) |
33 | | xmetcl 23707 |
. . . . . . . . . . . . 13
β’ ((π· β (βMetβπ) β§ (πΉβπ) β π β§ (πΉβπ) β π) β ((πΉβπ)π·(πΉβπ)) β
β*) |
34 | 13, 14, 18, 33 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((π· β (βMetβπ) β§ ((πΉβπ) β π β§ (πΉβπ) β π) β§ ((πΉβπ) β π β§ π₯ β β)) β ((πΉβπ)π·(πΉβπ)) β
β*) |
35 | 17, 20 | xaddcld 13229 |
. . . . . . . . . . . 12
β’ ((π· β (βMetβπ) β§ ((πΉβπ) β π β§ (πΉβπ) β π) β§ ((πΉβπ) β π β§ π₯ β β)) β (((πΉβπ)π·(πΉβπ)) +π ((πΉβπ)π·(πΉβπ))) β
β*) |
36 | 21 | rexrd 11213 |
. . . . . . . . . . . 12
β’ ((π· β (βMetβπ) β§ ((πΉβπ) β π β§ (πΉβπ) β π) β§ ((πΉβπ) β π β§ π₯ β β)) β π₯ β β*) |
37 | | xrlelttr 13084 |
. . . . . . . . . . . 12
β’ ((((πΉβπ)π·(πΉβπ)) β β* β§ (((πΉβπ)π·(πΉβπ)) +π ((πΉβπ)π·(πΉβπ))) β β* β§ π₯ β β*)
β ((((πΉβπ)π·(πΉβπ)) β€ (((πΉβπ)π·(πΉβπ)) +π ((πΉβπ)π·(πΉβπ))) β§ (((πΉβπ)π·(πΉβπ)) +π ((πΉβπ)π·(πΉβπ))) < π₯) β ((πΉβπ)π·(πΉβπ)) < π₯)) |
38 | 34, 35, 36, 37 | syl3anc 1372 |
. . . . . . . . . . 11
β’ ((π· β (βMetβπ) β§ ((πΉβπ) β π β§ (πΉβπ) β π) β§ ((πΉβπ) β π β§ π₯ β β)) β ((((πΉβπ)π·(πΉβπ)) β€ (((πΉβπ)π·(πΉβπ)) +π ((πΉβπ)π·(πΉβπ))) β§ (((πΉβπ)π·(πΉβπ)) +π ((πΉβπ)π·(πΉβπ))) < π₯) β ((πΉβπ)π·(πΉβπ)) < π₯)) |
39 | 32, 38 | mpand 694 |
. . . . . . . . . 10
β’ ((π· β (βMetβπ) β§ ((πΉβπ) β π β§ (πΉβπ) β π) β§ ((πΉβπ) β π β§ π₯ β β)) β ((((πΉβπ)π·(πΉβπ)) +π ((πΉβπ)π·(πΉβπ))) < π₯ β ((πΉβπ)π·(πΉβπ)) < π₯)) |
40 | 30, 39 | sylbid 239 |
. . . . . . . . 9
β’ ((π· β (βMetβπ) β§ ((πΉβπ) β π β§ (πΉβπ) β π) β§ ((πΉβπ) β π β§ π₯ β β)) β ((((πΉβπ)π·(πΉβπ)) +π ((πΉβπ)π·(πΉβπ))) < ((π₯ / 2) +π (π₯ / 2)) β ((πΉβπ)π·(πΉβπ)) < π₯)) |
41 | 25, 40 | syld 47 |
. . . . . . . 8
β’ ((π· β (βMetβπ) β§ ((πΉβπ) β π β§ (πΉβπ) β π) β§ ((πΉβπ) β π β§ π₯ β β)) β ((((πΉβπ)π·(πΉβπ)) < (π₯ / 2) β§ ((πΉβπ)π·(πΉβπ)) < (π₯ / 2)) β ((πΉβπ)π·(πΉβπ)) < π₯)) |
42 | | ovex 7394 |
. . . . . . . . . . 11
β’ ((πΉβπ)π·(πΉβπ)) β V |
43 | | fvi 6921 |
. . . . . . . . . . 11
β’ (((πΉβπ)π·(πΉβπ)) β V β ( I β((πΉβπ)π·(πΉβπ))) = ((πΉβπ)π·(πΉβπ))) |
44 | 42, 43 | ax-mp 5 |
. . . . . . . . . 10
β’ ( I
β((πΉβπ)π·(πΉβπ))) = ((πΉβπ)π·(πΉβπ)) |
45 | 44 | breq1i 5116 |
. . . . . . . . 9
β’ (( I
β((πΉβπ)π·(πΉβπ))) < (π₯ / 2) β ((πΉβπ)π·(πΉβπ)) < (π₯ / 2)) |
46 | | ovex 7394 |
. . . . . . . . . . 11
β’ ((πΉβπ)π·(πΉβπ)) β V |
47 | | fvi 6921 |
. . . . . . . . . . 11
β’ (((πΉβπ)π·(πΉβπ)) β V β ( I β((πΉβπ)π·(πΉβπ))) = ((πΉβπ)π·(πΉβπ))) |
48 | 46, 47 | ax-mp 5 |
. . . . . . . . . 10
β’ ( I
β((πΉβπ)π·(πΉβπ))) = ((πΉβπ)π·(πΉβπ)) |
49 | 48 | breq1i 5116 |
. . . . . . . . 9
β’ (( I
β((πΉβπ)π·(πΉβπ))) < (π₯ / 2) β ((πΉβπ)π·(πΉβπ)) < (π₯ / 2)) |
50 | 45, 49 | anbi12i 628 |
. . . . . . . 8
β’ ((( I
β((πΉβπ)π·(πΉβπ))) < (π₯ / 2) β§ ( I β((πΉβπ)π·(πΉβπ))) < (π₯ / 2)) β (((πΉβπ)π·(πΉβπ)) < (π₯ / 2) β§ ((πΉβπ)π·(πΉβπ)) < (π₯ / 2))) |
51 | | ovex 7394 |
. . . . . . . . . 10
β’ ((πΉβπ)π·(πΉβπ)) β V |
52 | | fvi 6921 |
. . . . . . . . . 10
β’ (((πΉβπ)π·(πΉβπ)) β V β ( I β((πΉβπ)π·(πΉβπ))) = ((πΉβπ)π·(πΉβπ))) |
53 | 51, 52 | ax-mp 5 |
. . . . . . . . 9
β’ ( I
β((πΉβπ)π·(πΉβπ))) = ((πΉβπ)π·(πΉβπ)) |
54 | 53 | breq1i 5116 |
. . . . . . . 8
β’ (( I
β((πΉβπ)π·(πΉβπ))) < π₯ β ((πΉβπ)π·(πΉβπ)) < π₯) |
55 | 41, 50, 54 | 3imtr4g 296 |
. . . . . . 7
β’ ((π· β (βMetβπ) β§ ((πΉβπ) β π β§ (πΉβπ) β π) β§ ((πΉβπ) β π β§ π₯ β β)) β ((( I β((πΉβπ)π·(πΉβπ))) < (π₯ / 2) β§ ( I β((πΉβπ)π·(πΉβπ))) < (π₯ / 2)) β ( I β((πΉβπ)π·(πΉβπ))) < π₯)) |
56 | 5, 6, 7, 8, 10, 12, 55 | cau3lem 15248 |
. . . . . 6
β’ (π· β (βMetβπ) β (βπ₯ β β+
βπ β β€
βπ β
(β€β₯βπ)((π β dom πΉ β§ (πΉβπ) β π) β§ ( I β((πΉβπ)π·(πΉβπ))) < π₯) β βπ₯ β β+ βπ β β€ βπ β
(β€β₯βπ)((π β dom πΉ β§ (πΉβπ) β π) β§ βπ β (β€β₯βπ)( I β((πΉβπ)π·(πΉβπ))) < π₯))) |
57 | 4, 56 | syl 17 |
. . . . 5
β’ ((π β§ πΉ β (π βpm β)) β
(βπ₯ β
β+ βπ β β€ βπ β (β€β₯βπ)((π β dom πΉ β§ (πΉβπ) β π) β§ ( I β((πΉβπ)π·(πΉβπ))) < π₯) β βπ₯ β β+ βπ β β€ βπ β
(β€β₯βπ)((π β dom πΉ β§ (πΉβπ) β π) β§ βπ β (β€β₯βπ)( I β((πΉβπ)π·(πΉβπ))) < π₯))) |
58 | 44 | breq1i 5116 |
. . . . . . . . . 10
β’ (( I
β((πΉβπ)π·(πΉβπ))) < π₯ β ((πΉβπ)π·(πΉβπ)) < π₯) |
59 | 58 | anbi2i 624 |
. . . . . . . . 9
β’ (((π β dom πΉ β§ (πΉβπ) β π) β§ ( I β((πΉβπ)π·(πΉβπ))) < π₯) β ((π β dom πΉ β§ (πΉβπ) β π) β§ ((πΉβπ)π·(πΉβπ)) < π₯)) |
60 | | df-3an 1090 |
. . . . . . . . 9
β’ ((π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯) β ((π β dom πΉ β§ (πΉβπ) β π) β§ ((πΉβπ)π·(πΉβπ)) < π₯)) |
61 | 59, 60 | bitr4i 278 |
. . . . . . . 8
β’ (((π β dom πΉ β§ (πΉβπ) β π) β§ ( I β((πΉβπ)π·(πΉβπ))) < π₯) β (π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯)) |
62 | 61 | ralbii 3093 |
. . . . . . 7
β’
(βπ β
(β€β₯βπ)((π β dom πΉ β§ (πΉβπ) β π) β§ ( I β((πΉβπ)π·(πΉβπ))) < π₯) β βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯)) |
63 | 62 | rexbii 3094 |
. . . . . 6
β’
(βπ β
β€ βπ β
(β€β₯βπ)((π β dom πΉ β§ (πΉβπ) β π) β§ ( I β((πΉβπ)π·(πΉβπ))) < π₯) β βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯)) |
64 | 63 | ralbii 3093 |
. . . . 5
β’
(βπ₯ β
β+ βπ β β€ βπ β (β€β₯βπ)((π β dom πΉ β§ (πΉβπ) β π) β§ ( I β((πΉβπ)π·(πΉβπ))) < π₯) β βπ₯ β β+ βπ β β€ βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯)) |
65 | 54 | ralbii 3093 |
. . . . . . . . . 10
β’
(βπ β
(β€β₯βπ)( I β((πΉβπ)π·(πΉβπ))) < π₯ β βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯) |
66 | 65 | anbi2i 624 |
. . . . . . . . 9
β’ (((π β dom πΉ β§ (πΉβπ) β π) β§ βπ β (β€β₯βπ)( I β((πΉβπ)π·(πΉβπ))) < π₯) β ((π β dom πΉ β§ (πΉβπ) β π) β§ βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯)) |
67 | | df-3an 1090 |
. . . . . . . . 9
β’ ((π β dom πΉ β§ (πΉβπ) β π β§ βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯) β ((π β dom πΉ β§ (πΉβπ) β π) β§ βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯)) |
68 | 66, 67 | bitr4i 278 |
. . . . . . . 8
β’ (((π β dom πΉ β§ (πΉβπ) β π) β§ βπ β (β€β₯βπ)( I β((πΉβπ)π·(πΉβπ))) < π₯) β (π β dom πΉ β§ (πΉβπ) β π β§ βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯)) |
69 | 68 | ralbii 3093 |
. . . . . . 7
β’
(βπ β
(β€β₯βπ)((π β dom πΉ β§ (πΉβπ) β π) β§ βπ β (β€β₯βπ)( I β((πΉβπ)π·(πΉβπ))) < π₯) β βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯)) |
70 | 69 | rexbii 3094 |
. . . . . 6
β’
(βπ β
β€ βπ β
(β€β₯βπ)((π β dom πΉ β§ (πΉβπ) β π) β§ βπ β (β€β₯βπ)( I β((πΉβπ)π·(πΉβπ))) < π₯) β βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯)) |
71 | 70 | ralbii 3093 |
. . . . 5
β’
(βπ₯ β
β+ βπ β β€ βπ β (β€β₯βπ)((π β dom πΉ β§ (πΉβπ) β π) β§ βπ β (β€β₯βπ)( I β((πΉβπ)π·(πΉβπ))) < π₯) β βπ₯ β β+ βπ β β€ βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯)) |
72 | 57, 64, 71 | 3bitr3g 313 |
. . . 4
β’ ((π β§ πΉ β (π βpm β)) β
(βπ₯ β
β+ βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯) β βπ₯ β β+ βπ β β€ βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯))) |
73 | | iscau3.4 |
. . . . . . 7
β’ (π β π β β€) |
74 | 73 | adantr 482 |
. . . . . 6
β’ ((π β§ πΉ β (π βpm β)) β π β
β€) |
75 | | iscau3.2 |
. . . . . . 7
β’ π =
(β€β₯βπ) |
76 | 75 | rexuz3 15242 |
. . . . . 6
β’ (π β β€ β
(βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯) β βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯))) |
77 | 74, 76 | syl 17 |
. . . . 5
β’ ((π β§ πΉ β (π βpm β)) β
(βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯) β βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯))) |
78 | 77 | ralbidv 3171 |
. . . 4
β’ ((π β§ πΉ β (π βpm β)) β
(βπ₯ β
β+ βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯) β βπ₯ β β+ βπ β β€ βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯))) |
79 | 72, 78 | bitr4d 282 |
. . 3
β’ ((π β§ πΉ β (π βpm β)) β
(βπ₯ β
β+ βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯) β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯))) |
80 | 79 | pm5.32da 580 |
. 2
β’ (π β ((πΉ β (π βpm β) β§
βπ₯ β
β+ βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯)) β (πΉ β (π βpm β) β§
βπ₯ β
β+ βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯)))) |
81 | 3, 80 | bitrd 279 |
1
β’ (π β (πΉ β (Cauβπ·) β (πΉ β (π βpm β) β§
βπ₯ β
β+ βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯)))) |