Step | Hyp | Ref
| Expression |
1 | | lmxrge0.j |
. . . . . . 7
β’ π½ =
(TopOpenβ(β*π βΎs
(0[,]+β))) |
2 | | eqid 2732 |
. . . . . . . 8
β’
(β*π βΎs
(0[,]+β)) = (β*π βΎs
(0[,]+β)) |
3 | | xrstopn 22597 |
. . . . . . . 8
β’
(ordTopβ β€ ) =
(TopOpenββ*π ) |
4 | 2, 3 | resstopn 22575 |
. . . . . . 7
β’
((ordTopβ β€ ) βΎt (0[,]+β)) =
(TopOpenβ(β*π βΎs
(0[,]+β))) |
5 | 1, 4 | eqtr4i 2763 |
. . . . . 6
β’ π½ = ((ordTopβ β€ )
βΎt (0[,]+β)) |
6 | | letopon 22594 |
. . . . . . 7
β’
(ordTopβ β€ ) β
(TopOnββ*) |
7 | | iccssxr 13358 |
. . . . . . 7
β’
(0[,]+β) β β* |
8 | | resttopon 22550 |
. . . . . . 7
β’
(((ordTopβ β€ ) β (TopOnββ*) β§
(0[,]+β) β β*) β ((ordTopβ β€ )
βΎt (0[,]+β)) β
(TopOnβ(0[,]+β))) |
9 | 6, 7, 8 | mp2an 691 |
. . . . . 6
β’
((ordTopβ β€ ) βΎt (0[,]+β)) β
(TopOnβ(0[,]+β)) |
10 | 5, 9 | eqeltri 2829 |
. . . . 5
β’ π½ β
(TopOnβ(0[,]+β)) |
11 | 10 | a1i 11 |
. . . 4
β’ (π β π½ β
(TopOnβ(0[,]+β))) |
12 | | nnuz 12816 |
. . . 4
β’ β =
(β€β₯β1) |
13 | | 1zzd 12544 |
. . . 4
β’ (π β 1 β
β€) |
14 | | lmxrge0.6 |
. . . 4
β’ (π β πΉ:ββΆ(0[,]+β)) |
15 | | lmxrge0.7 |
. . . 4
β’ ((π β§ π β β) β (πΉβπ) = π΄) |
16 | 11, 12, 13, 14, 15 | lmbrf 22649 |
. . 3
β’ (π β (πΉ(βπ‘βπ½)+β β (+β
β (0[,]+β) β§ βπ β π½ (+β β π β βπ β β βπ β (β€β₯βπ)π΄ β π)))) |
17 | | 0xr 11212 |
. . . . 5
β’ 0 β
β* |
18 | | pnfxr 11219 |
. . . . 5
β’ +β
β β* |
19 | | 0lepnf 13063 |
. . . . 5
β’ 0 β€
+β |
20 | | ubicc2 13393 |
. . . . 5
β’ ((0
β β* β§ +β β β* β§ 0
β€ +β) β +β β (0[,]+β)) |
21 | 17, 18, 19, 20 | mp3an 1462 |
. . . 4
β’ +β
β (0[,]+β) |
22 | 21 | biantrur 532 |
. . 3
β’
(βπ β
π½ (+β β π β βπ β β βπ β
(β€β₯βπ)π΄ β π) β (+β β (0[,]+β)
β§ βπ β
π½ (+β β π β βπ β β βπ β
(β€β₯βπ)π΄ β π))) |
23 | 16, 22 | bitr4di 289 |
. 2
β’ (π β (πΉ(βπ‘βπ½)+β β βπ β π½ (+β β π β βπ β β βπ β (β€β₯βπ)π΄ β π))) |
24 | | rexr 11211 |
. . . . . . . . . 10
β’ (π₯ β β β π₯ β
β*) |
25 | 18 | a1i 11 |
. . . . . . . . . 10
β’ (π₯ β β β +β
β β*) |
26 | | ltpnf 13051 |
. . . . . . . . . 10
β’ (π₯ β β β π₯ < +β) |
27 | | ubioc1 13328 |
. . . . . . . . . 10
β’ ((π₯ β β*
β§ +β β β* β§ π₯ < +β) β +β β (π₯(,]+β)) |
28 | 24, 25, 26, 27 | syl3anc 1372 |
. . . . . . . . 9
β’ (π₯ β β β +β
β (π₯(,]+β)) |
29 | | 0ltpnf 13053 |
. . . . . . . . . 10
β’ 0 <
+β |
30 | | ubioc1 13328 |
. . . . . . . . . 10
β’ ((0
β β* β§ +β β β* β§ 0
< +β) β +β β (0(,]+β)) |
31 | 17, 18, 29, 30 | mp3an 1462 |
. . . . . . . . 9
β’ +β
β (0(,]+β) |
32 | 28, 31 | jctir 522 |
. . . . . . . 8
β’ (π₯ β β β (+β
β (π₯(,]+β) β§
+β β (0(,]+β))) |
33 | | elin 3930 |
. . . . . . . 8
β’ (+β
β ((π₯(,]+β)
β© (0(,]+β)) β (+β β (π₯(,]+β) β§ +β β
(0(,]+β))) |
34 | 32, 33 | sylibr 233 |
. . . . . . 7
β’ (π₯ β β β +β
β ((π₯(,]+β)
β© (0(,]+β))) |
35 | 34 | ad2antlr 726 |
. . . . . 6
β’ (((π β§ π₯ β β) β§ βπ β π½ (+β β π β βπ β β βπ β (β€β₯βπ)π΄ β π)) β +β β ((π₯(,]+β) β©
(0(,]+β))) |
36 | | letop 22595 |
. . . . . . . . . . 11
β’
(ordTopβ β€ ) β Top |
37 | | ovex 7396 |
. . . . . . . . . . 11
β’
(0[,]+β) β V |
38 | | iocpnfordt 22604 |
. . . . . . . . . . . 12
β’ (π₯(,]+β) β
(ordTopβ β€ ) |
39 | | iocpnfordt 22604 |
. . . . . . . . . . . 12
β’
(0(,]+β) β (ordTopβ β€ ) |
40 | | inopn 22286 |
. . . . . . . . . . . 12
β’
(((ordTopβ β€ ) β Top β§ (π₯(,]+β) β (ordTopβ β€ )
β§ (0(,]+β) β (ordTopβ β€ )) β ((π₯(,]+β) β© (0(,]+β)) β
(ordTopβ β€ )) |
41 | 36, 38, 39, 40 | mp3an 1462 |
. . . . . . . . . . 11
β’ ((π₯(,]+β) β©
(0(,]+β)) β (ordTopβ β€ ) |
42 | | elrestr 17325 |
. . . . . . . . . . 11
β’
(((ordTopβ β€ ) β Top β§ (0[,]+β) β V β§
((π₯(,]+β) β©
(0(,]+β)) β (ordTopβ β€ )) β (((π₯(,]+β) β© (0(,]+β)) β©
(0[,]+β)) β ((ordTopβ β€ ) βΎt
(0[,]+β))) |
43 | 36, 37, 41, 42 | mp3an 1462 |
. . . . . . . . . 10
β’ (((π₯(,]+β) β©
(0(,]+β)) β© (0[,]+β)) β ((ordTopβ β€ )
βΎt (0[,]+β)) |
44 | | inss2 4195 |
. . . . . . . . . . . . 13
β’ ((π₯(,]+β) β©
(0(,]+β)) β (0(,]+β) |
45 | | iocssicc 13365 |
. . . . . . . . . . . . 13
β’
(0(,]+β) β (0[,]+β) |
46 | 44, 45 | sstri 3957 |
. . . . . . . . . . . 12
β’ ((π₯(,]+β) β©
(0(,]+β)) β (0[,]+β) |
47 | | sseqin2 4181 |
. . . . . . . . . . . 12
β’ (((π₯(,]+β) β©
(0(,]+β)) β (0[,]+β) β ((0[,]+β) β© ((π₯(,]+β) β©
(0(,]+β))) = ((π₯(,]+β) β©
(0(,]+β))) |
48 | 46, 47 | mpbi 229 |
. . . . . . . . . . 11
β’
((0[,]+β) β© ((π₯(,]+β) β© (0(,]+β))) = ((π₯(,]+β) β©
(0(,]+β)) |
49 | | incom 4167 |
. . . . . . . . . . 11
β’
((0[,]+β) β© ((π₯(,]+β) β© (0(,]+β))) =
(((π₯(,]+β) β©
(0(,]+β)) β© (0[,]+β)) |
50 | 48, 49 | eqtr3i 2762 |
. . . . . . . . . 10
β’ ((π₯(,]+β) β©
(0(,]+β)) = (((π₯(,]+β) β© (0(,]+β)) β©
(0[,]+β)) |
51 | 43, 50, 5 | 3eltr4i 2846 |
. . . . . . . . 9
β’ ((π₯(,]+β) β©
(0(,]+β)) β π½ |
52 | 51 | a1i 11 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β ((π₯(,]+β) β© (0(,]+β)) β
π½) |
53 | | eleq2 2822 |
. . . . . . . . . . 11
β’ (π = ((π₯(,]+β) β© (0(,]+β)) β
(+β β π β
+β β ((π₯(,]+β) β©
(0(,]+β)))) |
54 | 53 | adantl 483 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β) β§ π = ((π₯(,]+β) β© (0(,]+β))) β
(+β β π β
+β β ((π₯(,]+β) β©
(0(,]+β)))) |
55 | 54 | biimprd 248 |
. . . . . . . . 9
β’ (((π β§ π₯ β β) β§ π = ((π₯(,]+β) β© (0(,]+β))) β
(+β β ((π₯(,]+β) β© (0(,]+β)) β
+β β π)) |
56 | | simp-5r 785 |
. . . . . . . . . . . . . . 15
β’
((((((π β§ π₯ β β) β§ π = ((π₯(,]+β) β© (0(,]+β))) β§
π β β) β§
π β
(β€β₯βπ)) β§ π΄ β π) β π₯ β β) |
57 | 56 | rexrd 11215 |
. . . . . . . . . . . . . 14
β’
((((((π β§ π₯ β β) β§ π = ((π₯(,]+β) β© (0(,]+β))) β§
π β β) β§
π β
(β€β₯βπ)) β§ π΄ β π) β π₯ β β*) |
58 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’
((((((π β§ π₯ β β) β§ π = ((π₯(,]+β) β© (0(,]+β))) β§
π β β) β§
π β
(β€β₯βπ)) β§ π΄ β π) β π΄ β π) |
59 | | simp-4r 783 |
. . . . . . . . . . . . . . . 16
β’
((((((π β§ π₯ β β) β§ π = ((π₯(,]+β) β© (0(,]+β))) β§
π β β) β§
π β
(β€β₯βπ)) β§ π΄ β π) β π = ((π₯(,]+β) β©
(0(,]+β))) |
60 | 58, 59 | eleqtrd 2835 |
. . . . . . . . . . . . . . 15
β’
((((((π β§ π₯ β β) β§ π = ((π₯(,]+β) β© (0(,]+β))) β§
π β β) β§
π β
(β€β₯βπ)) β§ π΄ β π) β π΄ β ((π₯(,]+β) β©
(0(,]+β))) |
61 | | elin 3930 |
. . . . . . . . . . . . . . . 16
β’ (π΄ β ((π₯(,]+β) β© (0(,]+β)) β
(π΄ β (π₯(,]+β) β§ π΄ β
(0(,]+β))) |
62 | 61 | simplbi 499 |
. . . . . . . . . . . . . . 15
β’ (π΄ β ((π₯(,]+β) β© (0(,]+β)) β
π΄ β (π₯(,]+β)) |
63 | 60, 62 | syl 17 |
. . . . . . . . . . . . . 14
β’
((((((π β§ π₯ β β) β§ π = ((π₯(,]+β) β© (0(,]+β))) β§
π β β) β§
π β
(β€β₯βπ)) β§ π΄ β π) β π΄ β (π₯(,]+β)) |
64 | | elioc1 13317 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ β β*
β§ +β β β*) β (π΄ β (π₯(,]+β) β (π΄ β β* β§ π₯ < π΄ β§ π΄ β€ +β))) |
65 | 18, 64 | mpan2 690 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β β*
β (π΄ β (π₯(,]+β) β (π΄ β β*
β§ π₯ < π΄ β§ π΄ β€ +β))) |
66 | 65 | biimpa 478 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β β*
β§ π΄ β (π₯(,]+β)) β (π΄ β β*
β§ π₯ < π΄ β§ π΄ β€ +β)) |
67 | 66 | simp2d 1144 |
. . . . . . . . . . . . . 14
β’ ((π₯ β β*
β§ π΄ β (π₯(,]+β)) β π₯ < π΄) |
68 | 57, 63, 67 | syl2anc 585 |
. . . . . . . . . . . . 13
β’
((((((π β§ π₯ β β) β§ π = ((π₯(,]+β) β© (0(,]+β))) β§
π β β) β§
π β
(β€β₯βπ)) β§ π΄ β π) β π₯ < π΄) |
69 | 68 | ex 414 |
. . . . . . . . . . . 12
β’
(((((π β§ π₯ β β) β§ π = ((π₯(,]+β) β© (0(,]+β))) β§
π β β) β§
π β
(β€β₯βπ)) β (π΄ β π β π₯ < π΄)) |
70 | 69 | ralimdva 3161 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β β) β§ π = ((π₯(,]+β) β© (0(,]+β))) β§
π β β) β
(βπ β
(β€β₯βπ)π΄ β π β βπ β (β€β₯βπ)π₯ < π΄)) |
71 | 70 | reximdva 3162 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β) β§ π = ((π₯(,]+β) β© (0(,]+β))) β
(βπ β β
βπ β
(β€β₯βπ)π΄ β π β βπ β β βπ β (β€β₯βπ)π₯ < π΄)) |
72 | | fveq2 6848 |
. . . . . . . . . . . 12
β’ (π = π β (β€β₯βπ) =
(β€β₯βπ)) |
73 | 72 | raleqdv 3312 |
. . . . . . . . . . 11
β’ (π = π β (βπ β (β€β₯βπ)π₯ < π΄ β βπ β (β€β₯βπ)π₯ < π΄)) |
74 | 73 | cbvrexvw 3225 |
. . . . . . . . . 10
β’
(βπ β
β βπ β
(β€β₯βπ)π₯ < π΄ β βπ β β βπ β (β€β₯βπ)π₯ < π΄) |
75 | 71, 74 | syl6ibr 252 |
. . . . . . . . 9
β’ (((π β§ π₯ β β) β§ π = ((π₯(,]+β) β© (0(,]+β))) β
(βπ β β
βπ β
(β€β₯βπ)π΄ β π β βπ β β βπ β (β€β₯βπ)π₯ < π΄)) |
76 | 55, 75 | imim12d 81 |
. . . . . . . 8
β’ (((π β§ π₯ β β) β§ π = ((π₯(,]+β) β© (0(,]+β))) β
((+β β π β
βπ β β
βπ β
(β€β₯βπ)π΄ β π) β (+β β ((π₯(,]+β) β©
(0(,]+β)) β βπ β β βπ β (β€β₯βπ)π₯ < π΄))) |
77 | 52, 76 | rspcimdv 3573 |
. . . . . . 7
β’ ((π β§ π₯ β β) β (βπ β π½ (+β β π β βπ β β βπ β (β€β₯βπ)π΄ β π) β (+β β ((π₯(,]+β) β©
(0(,]+β)) β βπ β β βπ β (β€β₯βπ)π₯ < π΄))) |
78 | 77 | imp 408 |
. . . . . 6
β’ (((π β§ π₯ β β) β§ βπ β π½ (+β β π β βπ β β βπ β (β€β₯βπ)π΄ β π)) β (+β β ((π₯(,]+β) β©
(0(,]+β)) β βπ β β βπ β (β€β₯βπ)π₯ < π΄)) |
79 | 35, 78 | mpd 15 |
. . . . 5
β’ (((π β§ π₯ β β) β§ βπ β π½ (+β β π β βπ β β βπ β (β€β₯βπ)π΄ β π)) β βπ β β βπ β (β€β₯βπ)π₯ < π΄) |
80 | 79 | ex 414 |
. . . 4
β’ ((π β§ π₯ β β) β (βπ β π½ (+β β π β βπ β β βπ β (β€β₯βπ)π΄ β π) β βπ β β βπ β (β€β₯βπ)π₯ < π΄)) |
81 | 80 | ralrimdva 3148 |
. . 3
β’ (π β (βπ β π½ (+β β π β βπ β β βπ β (β€β₯βπ)π΄ β π) β βπ₯ β β βπ β β βπ β (β€β₯βπ)π₯ < π΄)) |
82 | | simplll 774 |
. . . . . 6
β’ ((((π β§ π β π½) β§ βπ₯ β β βπ β β βπ β (β€β₯βπ)π₯ < π΄) β§ +β β π) β π) |
83 | | simpllr 775 |
. . . . . . 7
β’ ((((π β§ π β π½) β§ βπ₯ β β βπ β β βπ β (β€β₯βπ)π₯ < π΄) β§ +β β π) β π β π½) |
84 | | simpr 486 |
. . . . . . 7
β’ ((((π β§ π β π½) β§ βπ₯ β β βπ β β βπ β (β€β₯βπ)π₯ < π΄) β§ +β β π) β +β β π) |
85 | 1 | pnfneige0 32622 |
. . . . . . 7
β’ ((π β π½ β§ +β β π) β βπ₯ β β (π₯(,]+β) β π) |
86 | 83, 84, 85 | syl2anc 585 |
. . . . . 6
β’ ((((π β§ π β π½) β§ βπ₯ β β βπ β β βπ β (β€β₯βπ)π₯ < π΄) β§ +β β π) β βπ₯ β β (π₯(,]+β) β π) |
87 | | simplr 768 |
. . . . . 6
β’ ((((π β§ π β π½) β§ βπ₯ β β βπ β β βπ β (β€β₯βπ)π₯ < π΄) β§ +β β π) β βπ₯ β β βπ β β βπ β (β€β₯βπ)π₯ < π΄) |
88 | | r19.29r 3116 |
. . . . . . . 8
β’
((βπ₯ β
β (π₯(,]+β)
β π β§
βπ₯ β β
βπ β β
βπ β
(β€β₯βπ)π₯ < π΄) β βπ₯ β β ((π₯(,]+β) β π β§ βπ β β βπ β (β€β₯βπ)π₯ < π΄)) |
89 | | simp-4l 782 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π₯ β β) β§ (π₯(,]+β) β π) β§ π β β) β§ π β (β€β₯βπ)) β π) |
90 | | uznnssnn 12830 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β
(β€β₯βπ) β β) |
91 | 90 | ad2antlr 726 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π₯ β β) β§ (π₯(,]+β) β π) β§ π β β) β§ π β (β€β₯βπ)) β
(β€β₯βπ) β β) |
92 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π₯ β β) β§ (π₯(,]+β) β π) β§ π β β) β§ π β (β€β₯βπ)) β π β (β€β₯βπ)) |
93 | 91, 92 | sseldd 3949 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π₯ β β) β§ (π₯(,]+β) β π) β§ π β β) β§ π β (β€β₯βπ)) β π β β) |
94 | 89, 93 | jca 513 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π₯ β β) β§ (π₯(,]+β) β π) β§ π β β) β§ π β (β€β₯βπ)) β (π β§ π β β)) |
95 | | simp-4r 783 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π₯ β β) β§ (π₯(,]+β) β π) β§ π β β) β§ π β (β€β₯βπ)) β π₯ β β) |
96 | | simpllr 775 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π₯ β β) β§ (π₯(,]+β) β π) β§ π β β) β§ π β (β€β₯βπ)) β (π₯(,]+β) β π) |
97 | | simplr 768 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π β β) β§ π₯ β β) β§ (π₯(,]+β) β π) β§ π₯ < π΄) β (π₯(,]+β) β π) |
98 | | simplr 768 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π β β) β§ π₯ β β) β§ π₯ < π΄) β π₯ β β) |
99 | 98 | rexrd 11215 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β β) β§ π₯ β β) β§ π₯ < π΄) β π₯ β β*) |
100 | 14 | ffvelcdmda 7041 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β β) β (πΉβπ) β (0[,]+β)) |
101 | 15, 100 | eqeltrrd 2834 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β β) β π΄ β (0[,]+β)) |
102 | 7, 101 | sselid 3946 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β β) β π΄ β
β*) |
103 | 102 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β β) β§ π₯ β β) β§ π₯ < π΄) β π΄ β
β*) |
104 | | simpr 486 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β β) β§ π₯ β β) β§ π₯ < π΄) β π₯ < π΄) |
105 | | pnfge 13061 |
. . . . . . . . . . . . . . . . . . 19
β’ (π΄ β β*
β π΄ β€
+β) |
106 | 103, 105 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β β) β§ π₯ β β) β§ π₯ < π΄) β π΄ β€ +β) |
107 | 65 | biimpar 479 |
. . . . . . . . . . . . . . . . . 18
β’ ((π₯ β β*
β§ (π΄ β
β* β§ π₯
< π΄ β§ π΄ β€ +β)) β π΄ β (π₯(,]+β)) |
108 | 99, 103, 104, 106, 107 | syl13anc 1373 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β β) β§ π₯ β β) β§ π₯ < π΄) β π΄ β (π₯(,]+β)) |
109 | 108 | adantlr 714 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π β β) β§ π₯ β β) β§ (π₯(,]+β) β π) β§ π₯ < π΄) β π΄ β (π₯(,]+β)) |
110 | 97, 109 | sseldd 3949 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π β β) β§ π₯ β β) β§ (π₯(,]+β) β π) β§ π₯ < π΄) β π΄ β π) |
111 | 110 | ex 414 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β β) β§ π₯ β β) β§ (π₯(,]+β) β π) β (π₯ < π΄ β π΄ β π)) |
112 | 94, 95, 96, 111 | syl21anc 837 |
. . . . . . . . . . . . 13
β’
(((((π β§ π₯ β β) β§ (π₯(,]+β) β π) β§ π β β) β§ π β (β€β₯βπ)) β (π₯ < π΄ β π΄ β π)) |
113 | 112 | ralimdva 3161 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β β) β§ (π₯(,]+β) β π) β§ π β β) β (βπ β
(β€β₯βπ)π₯ < π΄ β βπ β (β€β₯βπ)π΄ β π)) |
114 | 113 | reximdva 3162 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β) β§ (π₯(,]+β) β π) β (βπ β β βπ β (β€β₯βπ)π₯ < π΄ β βπ β β βπ β (β€β₯βπ)π΄ β π)) |
115 | 74, 114 | biimtrid 241 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β) β§ (π₯(,]+β) β π) β (βπ β β βπ β (β€β₯βπ)π₯ < π΄ β βπ β β βπ β (β€β₯βπ)π΄ β π)) |
116 | 115 | expimpd 455 |
. . . . . . . . 9
β’ ((π β§ π₯ β β) β (((π₯(,]+β) β π β§ βπ β β βπ β (β€β₯βπ)π₯ < π΄) β βπ β β βπ β (β€β₯βπ)π΄ β π)) |
117 | 116 | rexlimdva 3149 |
. . . . . . . 8
β’ (π β (βπ₯ β β ((π₯(,]+β) β π β§ βπ β β βπ β (β€β₯βπ)π₯ < π΄) β βπ β β βπ β (β€β₯βπ)π΄ β π)) |
118 | 88, 117 | syl5 34 |
. . . . . . 7
β’ (π β ((βπ₯ β β (π₯(,]+β) β π β§ βπ₯ β β βπ β β βπ β
(β€β₯βπ)π₯ < π΄) β βπ β β βπ β (β€β₯βπ)π΄ β π)) |
119 | 118 | imp 408 |
. . . . . 6
β’ ((π β§ (βπ₯ β β (π₯(,]+β) β π β§ βπ₯ β β βπ β β βπ β (β€β₯βπ)π₯ < π΄)) β βπ β β βπ β (β€β₯βπ)π΄ β π) |
120 | 82, 86, 87, 119 | syl12anc 836 |
. . . . 5
β’ ((((π β§ π β π½) β§ βπ₯ β β βπ β β βπ β (β€β₯βπ)π₯ < π΄) β§ +β β π) β βπ β β βπ β (β€β₯βπ)π΄ β π) |
121 | 120 | exp31 421 |
. . . 4
β’ ((π β§ π β π½) β (βπ₯ β β βπ β β βπ β (β€β₯βπ)π₯ < π΄ β (+β β π β βπ β β βπ β (β€β₯βπ)π΄ β π))) |
122 | 121 | ralrimdva 3148 |
. . 3
β’ (π β (βπ₯ β β βπ β β βπ β
(β€β₯βπ)π₯ < π΄ β βπ β π½ (+β β π β βπ β β βπ β (β€β₯βπ)π΄ β π))) |
123 | 81, 122 | impbid 211 |
. 2
β’ (π β (βπ β π½ (+β β π β βπ β β βπ β (β€β₯βπ)π΄ β π) β βπ₯ β β βπ β β βπ β (β€β₯βπ)π₯ < π΄)) |
124 | 23, 123 | bitrd 279 |
1
β’ (π β (πΉ(βπ‘βπ½)+β β βπ₯ β β βπ β β βπ β
(β€β₯βπ)π₯ < π΄)) |