Step | Hyp | Ref
| Expression |
1 | | relowlpssretop.1 |
. . 3
β’ πΌ = ([,) β (β Γ
β)) |
2 | 1 | relowlssretop 35880 |
. 2
β’
(topGenβran (,)) β (topGenβπΌ) |
3 | | 2re 12232 |
. . . . 5
β’ 2 β
β |
4 | | 1lt2 12329 |
. . . . 5
β’ 1 <
2 |
5 | | ovex 7391 |
. . . . . . . . . . . 12
β’
(1[,)π) β
V |
6 | | sbcan 3792 |
. . . . . . . . . . . . . . 15
β’
([1 / π₯](π β β β§ π₯ < π) β ([1 / π₯]π β β β§ [1 / π₯]π₯ < π)) |
7 | | 1re 11160 |
. . . . . . . . . . . . . . . . 17
β’ 1 β
β |
8 | | sbcg 3819 |
. . . . . . . . . . . . . . . . 17
β’ (1 β
β β ([1 / π₯]π β β β π β β)) |
9 | 7, 8 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
β’
([1 / π₯]π β β β π β β) |
10 | | sbcbr123 5160 |
. . . . . . . . . . . . . . . . 17
β’
([1 / π₯]π₯ < π β β¦1 / π₯β¦π₯β¦1 / π₯β¦ < β¦1 / π₯β¦π) |
11 | | csbvarg 4392 |
. . . . . . . . . . . . . . . . . . 19
β’ (1 β
β β β¦1 / π₯β¦π₯ = 1) |
12 | 7, 11 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
β’
β¦1 / π₯β¦π₯ = 1 |
13 | | csbconstg 3875 |
. . . . . . . . . . . . . . . . . . 19
β’ (1 β
β β β¦1 / π₯β¦π = π) |
14 | 7, 13 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
β’
β¦1 / π₯β¦π = π |
15 | 12, 14 | breq12i 5115 |
. . . . . . . . . . . . . . . . 17
β’
(β¦1 / π₯β¦π₯β¦1 / π₯β¦ < β¦1 / π₯β¦π β 1β¦1 /
π₯β¦ < π) |
16 | | csbconstg 3875 |
. . . . . . . . . . . . . . . . . . 19
β’ (1 β
β β β¦1 / π₯β¦ < = <
) |
17 | 7, 16 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
β’
β¦1 / π₯β¦ < = < |
18 | 17 | breqi 5112 |
. . . . . . . . . . . . . . . . 17
β’
(1β¦1 / π₯β¦ < π β 1 < π) |
19 | 10, 15, 18 | 3bitri 297 |
. . . . . . . . . . . . . . . 16
β’
([1 / π₯]π₯ < π β 1 < π) |
20 | 9, 19 | anbi12i 628 |
. . . . . . . . . . . . . . 15
β’
(([1 / π₯]π β β β§ [1 / π₯]π₯ < π) β (π β β β§ 1 < π)) |
21 | 6, 20 | bitri 275 |
. . . . . . . . . . . . . 14
β’
([1 / π₯](π β β β§ π₯ < π) β (π β β β§ 1 < π)) |
22 | | sbceqg 4370 |
. . . . . . . . . . . . . . . 16
β’ (1 β
β β ([1 / π₯]π = (π₯[,)π) β β¦1 / π₯β¦π = β¦1 / π₯β¦(π₯[,)π))) |
23 | 7, 22 | ax-mp 5 |
. . . . . . . . . . . . . . 15
β’
([1 / π₯]π = (π₯[,)π) β β¦1 / π₯β¦π = β¦1 / π₯β¦(π₯[,)π)) |
24 | | csbconstg 3875 |
. . . . . . . . . . . . . . . . 17
β’ (1 β
β β β¦1 / π₯β¦π = π) |
25 | 7, 24 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
β’
β¦1 / π₯β¦π = π |
26 | | csbov123 7400 |
. . . . . . . . . . . . . . . . 17
β’
β¦1 / π₯β¦(π₯[,)π) = (β¦1 / π₯β¦π₯β¦1 / π₯β¦[,)β¦1 / π₯β¦π) |
27 | | csbconstg 3875 |
. . . . . . . . . . . . . . . . . . 19
β’ (1 β
β β β¦1 / π₯β¦[,) = [,)) |
28 | 7, 27 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
β’
β¦1 / π₯β¦[,) = [,) |
29 | 12, 14, 28 | oveq123i 7372 |
. . . . . . . . . . . . . . . . 17
β’
(β¦1 / π₯β¦π₯β¦1 / π₯β¦[,)β¦1 / π₯β¦π) = (1[,)π) |
30 | 26, 29 | eqtri 2761 |
. . . . . . . . . . . . . . . 16
β’
β¦1 / π₯β¦(π₯[,)π) = (1[,)π) |
31 | 25, 30 | eqeq12i 2751 |
. . . . . . . . . . . . . . 15
β’
(β¦1 / π₯β¦π = β¦1 / π₯β¦(π₯[,)π) β π = (1[,)π)) |
32 | 23, 31 | bitri 275 |
. . . . . . . . . . . . . 14
β’
([1 / π₯]π = (π₯[,)π) β π = (1[,)π)) |
33 | | sbcan 3792 |
. . . . . . . . . . . . . . 15
β’
([1 / π₯]((π β β β§ π₯ < π) β§ π = (π₯[,)π)) β ([1 / π₯](π β β β§ π₯ < π) β§ [1 / π₯]π = (π₯[,)π))) |
34 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β β β§ π₯ < π) β§ π = (π₯[,)π)) β§ π₯ β β) β π₯ β β) |
35 | | simpl 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((π₯ β β β§ π β β) β π₯ β
β) |
36 | | leid 11256 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π₯ β β β π₯ β€ π₯) |
37 | 35, 36 | jccir 523 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((π₯ β β β§ π β β) β (π₯ β β β§ π₯ β€ π₯)) |
38 | | rexr 11206 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (π β β β π β
β*) |
39 | | elico2 13334 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ ((π₯ β β β§ π β β*)
β (π₯ β (π₯[,)π) β (π₯ β β β§ π₯ β€ π₯ β§ π₯ < π))) |
40 | 38, 39 | sylan2 594 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ ((π₯ β β β§ π β β) β (π₯ β (π₯[,)π) β (π₯ β β β§ π₯ β€ π₯ β§ π₯ < π))) |
41 | | df-3an 1090 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ ((π₯ β β β§ π₯ β€ π₯ β§ π₯ < π) β ((π₯ β β β§ π₯ β€ π₯) β§ π₯ < π)) |
42 | 40, 41 | bitrdi 287 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((π₯ β β β§ π β β) β (π₯ β (π₯[,)π) β ((π₯ β β β§ π₯ β€ π₯) β§ π₯ < π))) |
43 | 42 | baibd 541 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (((π₯ β β β§ π β β) β§ (π₯ β β β§ π₯ β€ π₯)) β (π₯ β (π₯[,)π) β π₯ < π)) |
44 | 37, 43 | mpdan 686 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π₯ β β β§ π β β) β (π₯ β (π₯[,)π) β π₯ < π)) |
45 | 44 | biimpar 479 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (((π₯ β β β§ π β β) β§ π₯ < π) β π₯ β (π₯[,)π)) |
46 | 45 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((((π₯ β β β§ π β β) β§ π₯ < π) β§ π = (π₯[,)π)) β π₯ β (π₯[,)π)) |
47 | | eleq2 2823 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π = (π₯[,)π) β (π₯ β π β π₯ β (π₯[,)π))) |
48 | 47 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((((π₯ β β β§ π β β) β§ π₯ < π) β§ π = (π₯[,)π)) β (π₯ β π β π₯ β (π₯[,)π))) |
49 | 46, 48 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π₯ β β β§ π β β) β§ π₯ < π) β§ π = (π₯[,)π)) β π₯ β π) |
50 | | rexpssxrxp 11205 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (β
Γ β) β (β* Γ
β*) |
51 | | opelxpi 5671 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ ((π₯ β β β§ π β β) β
β¨π₯, πβ© β (β Γ
β)) |
52 | 50, 51 | sselid 3943 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ ((π₯ β β β§ π β β) β
β¨π₯, πβ© β (β* Γ
β*)) |
53 | | df-ico 13276 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ [,) =
(π₯ β
β*, π
β β* β¦ {π§ β β* β£ (π₯ β€ π§ β§ π§ < π)}) |
54 | 53 | ixxf 13280 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’
[,):(β* Γ β*)βΆπ«
β* |
55 | 54 | fdmi 6681 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ dom [,) =
(β* Γ β*) |
56 | 55 | eleq2i 2826 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’
(β¨π₯, πβ© β dom [,) β
β¨π₯, πβ© β (β* Γ
β*)) |
57 | 53 | mpofun 7481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ Fun
[,) |
58 | | funfvima 7181 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ ((Fun [,)
β§ β¨π₯, πβ© β dom [,)) β
(β¨π₯, πβ© β (β Γ
β) β ([,)ββ¨π₯, πβ©) β ([,) β (β Γ
β)))) |
59 | 57, 58 | mpan 689 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’
(β¨π₯, πβ© β dom [,) β
(β¨π₯, πβ© β (β Γ
β) β ([,)ββ¨π₯, πβ©) β ([,) β (β Γ
β)))) |
60 | 56, 59 | sylbir 234 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’
(β¨π₯, πβ© β
(β* Γ β*) β (β¨π₯, πβ© β (β Γ β)
β ([,)ββ¨π₯,
πβ©) β ([,)
β (β Γ β)))) |
61 | 52, 51, 60 | sylc 65 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((π₯ β β β§ π β β) β
([,)ββ¨π₯, πβ©) β ([,) β
(β Γ β))) |
62 | | df-ov 7361 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π₯[,)π) = ([,)ββ¨π₯, πβ©) |
63 | 61, 62, 1 | 3eltr4g 2851 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((π₯ β β β§ π β β) β (π₯[,)π) β πΌ) |
64 | | eleq1 2822 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π = (π₯[,)π) β (π β πΌ β (π₯[,)π) β πΌ)) |
65 | 63, 64 | syl5ibrcom 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π₯ β β β§ π β β) β (π = (π₯[,)π) β π β πΌ)) |
66 | 65 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (((π₯ β β β§ π β β) β§ π = (π₯[,)π)) β π β πΌ) |
67 | | ioof 13370 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’
(,):(β* Γ β*)βΆπ«
β |
68 | | ffn 6669 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’
((,):(β* Γ β*)βΆπ«
β β (,) Fn (β* Γ
β*)) |
69 | 67, 68 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (,) Fn
(β* Γ β*) |
70 | | ovelrn 7531 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ ((,) Fn
(β* Γ β*) β (π β ran (,) β βπ β β*
βπ β
β* π =
(π(,)π))) |
71 | 69, 70 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (π β ran (,) β
βπ β
β* βπ β β* π = (π(,)π)) |
72 | | iooelexlt 35879 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
β’ (π₯ β (π(,)π) β βπ¦ β (π(,)π)π¦ < π₯) |
73 | | df-rex 3071 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
β’
(βπ¦ β
(π(,)π)π¦ < π₯ β βπ¦(π¦ β (π(,)π) β§ π¦ < π₯)) |
74 | 72, 73 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
β’ (π₯ β (π(,)π) β βπ¦(π¦ β (π(,)π) β§ π¦ < π₯)) |
75 | | simpl 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
β’ ((π¦ β (π(,)π) β§ π¦ < π₯) β π¦ β (π(,)π)) |
76 | 75 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
β’ (π₯ β (π(,)π) β ((π¦ β (π(,)π) β§ π¦ < π₯) β π¦ β (π(,)π))) |
77 | 53 | elmpocl2 7598 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . 53
β’ (π¦ β (π₯[,)π) β π β β*) |
78 | | elioore 13300 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . 57
β’ (π₯ β (π(,)π) β π₯ β β) |
79 | | elico2 13334 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . 57
β’ ((π₯ β β β§ π β β*)
β (π¦ β (π₯[,)π) β (π¦ β β β§ π₯ β€ π¦ β§ π¦ < π))) |
80 | 78, 79 | sylan 581 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . 56
β’ ((π₯ β (π(,)π) β§ π β β*) β (π¦ β (π₯[,)π) β (π¦ β β β§ π₯ β€ π¦ β§ π¦ < π))) |
81 | | simp2 1138 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . 56
β’ ((π¦ β β β§ π₯ β€ π¦ β§ π¦ < π) β π₯ β€ π¦) |
82 | 80, 81 | syl6bi 253 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . 55
β’ ((π₯ β (π(,)π) β§ π β β*) β (π¦ β (π₯[,)π) β π₯ β€ π¦)) |
83 | 82 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . 54
β’ (π₯ β (π(,)π) β (π β β* β (π¦ β (π₯[,)π) β π₯ β€ π¦))) |
84 | 83 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . 53
β’ (π₯ β (π(,)π) β (π¦ β (π₯[,)π) β (π β β* β π₯ β€ π¦))) |
85 | 77, 84 | mpdi 45 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . 52
β’ (π₯ β (π(,)π) β (π¦ β (π₯[,)π) β π₯ β€ π¦)) |
86 | 85 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . 51
β’ ((π₯ β (π(,)π) β§ π¦ β (π₯[,)π)) β π₯ β€ π¦) |
87 | 78 | rexrd 11210 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . 53
β’ (π₯ β (π(,)π) β π₯ β β*) |
88 | 87 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . 52
β’ ((π₯ β (π(,)π) β§ π¦ β (π₯[,)π)) β π₯ β β*) |
89 | | elicore 13322 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . 54
β’ ((π₯ β β β§ π¦ β (π₯[,)π)) β π¦ β β) |
90 | 78, 89 | sylan 581 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . 53
β’ ((π₯ β (π(,)π) β§ π¦ β (π₯[,)π)) β π¦ β β) |
91 | 90 | rexrd 11210 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . 52
β’ ((π₯ β (π(,)π) β§ π¦ β (π₯[,)π)) β π¦ β β*) |
92 | | xrlenlt 11225 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . 54
β’ ((π₯ β β*
β§ π¦ β
β*) β (π₯ β€ π¦ β Β¬ π¦ < π₯)) |
93 | 92 | biimpd 228 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . 53
β’ ((π₯ β β*
β§ π¦ β
β*) β (π₯ β€ π¦ β Β¬ π¦ < π₯)) |
94 | 93 | con2d 134 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . 52
β’ ((π₯ β β*
β§ π¦ β
β*) β (π¦ < π₯ β Β¬ π₯ β€ π¦)) |
95 | 88, 91, 94 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . 51
β’ ((π₯ β (π(,)π) β§ π¦ β (π₯[,)π)) β (π¦ < π₯ β Β¬ π₯ β€ π¦)) |
96 | 86, 95 | mt2d 136 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
β’ ((π₯ β (π(,)π) β§ π¦ β (π₯[,)π)) β Β¬ π¦ < π₯) |
97 | 96 | intnand 490 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
β’ ((π₯ β (π(,)π) β§ π¦ β (π₯[,)π)) β Β¬ (π¦ β (π(,)π) β§ π¦ < π₯)) |
98 | 97 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
β’ (π₯ β (π(,)π) β (π¦ β (π₯[,)π) β Β¬ (π¦ β (π(,)π) β§ π¦ < π₯))) |
99 | 98 | con2d 134 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
β’ (π₯ β (π(,)π) β ((π¦ β (π(,)π) β§ π¦ < π₯) β Β¬ π¦ β (π₯[,)π))) |
100 | 76, 99 | jcad 514 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
β’ (π₯ β (π(,)π) β ((π¦ β (π(,)π) β§ π¦ < π₯) β (π¦ β (π(,)π) β§ Β¬ π¦ β (π₯[,)π)))) |
101 | | annim 405 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
β’ ((π¦ β (π(,)π) β§ Β¬ π¦ β (π₯[,)π)) β Β¬ (π¦ β (π(,)π) β π¦ β (π₯[,)π))) |
102 | 100, 101 | syl6ib 251 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
β’ (π₯ β (π(,)π) β ((π¦ β (π(,)π) β§ π¦ < π₯) β Β¬ (π¦ β (π(,)π) β π¦ β (π₯[,)π)))) |
103 | 102 | eximdv 1921 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
β’ (π₯ β (π(,)π) β (βπ¦(π¦ β (π(,)π) β§ π¦ < π₯) β βπ¦ Β¬ (π¦ β (π(,)π) β π¦ β (π₯[,)π)))) |
104 | 74, 103 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
β’ (π₯ β (π(,)π) β βπ¦ Β¬ (π¦ β (π(,)π) β π¦ β (π₯[,)π))) |
105 | | exnal 1830 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
β’
(βπ¦ Β¬
(π¦ β (π(,)π) β π¦ β (π₯[,)π)) β Β¬ βπ¦(π¦ β (π(,)π) β π¦ β (π₯[,)π))) |
106 | 104, 105 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’ (π₯ β (π(,)π) β Β¬ βπ¦(π¦ β (π(,)π) β π¦ β (π₯[,)π))) |
107 | | dfss2 3931 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’ ((π(,)π) β (π₯[,)π) β βπ¦(π¦ β (π(,)π) β π¦ β (π₯[,)π))) |
108 | 106, 107 | sylnibr 329 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’ (π₯ β (π(,)π) β Β¬ (π(,)π) β (π₯[,)π)) |
109 | | imnan 401 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’ ((π₯ β (π(,)π) β Β¬ (π(,)π) β (π₯[,)π)) β Β¬ (π₯ β (π(,)π) β§ (π(,)π) β (π₯[,)π))) |
110 | 108, 109 | mpbi 229 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ Β¬
(π₯ β (π(,)π) β§ (π(,)π) β (π₯[,)π)) |
111 | | eleq2 2823 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’ (π = (π(,)π) β (π₯ β π β π₯ β (π(,)π))) |
112 | | sseq1 3970 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’ (π = (π(,)π) β (π β (π₯[,)π) β (π(,)π) β (π₯[,)π))) |
113 | 111, 112 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ (π = (π(,)π) β ((π₯ β π β§ π β (π₯[,)π)) β (π₯ β (π(,)π) β§ (π(,)π) β (π₯[,)π)))) |
114 | 110, 113 | mtbiri 327 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ (π = (π(,)π) β Β¬ (π₯ β π β§ π β (π₯[,)π))) |
115 | | sseq2 3971 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’ (π = (π₯[,)π) β (π β π β π β (π₯[,)π))) |
116 | 115 | anbi2d 630 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ (π = (π₯[,)π) β ((π₯ β π β§ π β π) β (π₯ β π β§ π β (π₯[,)π)))) |
117 | 116 | notbid 318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ (π = (π₯[,)π) β (Β¬ (π₯ β π β§ π β π) β Β¬ (π₯ β π β§ π β (π₯[,)π)))) |
118 | 114, 117 | syl5ibrcom 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ (π = (π(,)π) β (π = (π₯[,)π) β Β¬ (π₯ β π β§ π β π))) |
119 | 118 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ ((π β β*
β§ π β
β*) β (π = (π(,)π) β (π = (π₯[,)π) β Β¬ (π₯ β π β§ π β π)))) |
120 | 119 | rexlimivv 3193 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’
(βπ β
β* βπ β β* π = (π(,)π) β (π = (π₯[,)π) β Β¬ (π₯ β π β§ π β π))) |
121 | 71, 120 | sylbi 216 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π β ran (,) β (π = (π₯[,)π) β Β¬ (π₯ β π β§ π β π))) |
122 | 121 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π = (π₯[,)π) β (π β ran (,) β Β¬ (π₯ β π β§ π β π))) |
123 | 122 | ralrimiv 3139 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π = (π₯[,)π) β βπ β ran (,) Β¬ (π₯ β π β§ π β π)) |
124 | | ralnex 3072 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’
(βπ β
ran (,) Β¬ (π₯ β
π β§ π β π) β Β¬ βπ β ran (,)(π₯ β π β§ π β π)) |
125 | 123, 124 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π = (π₯[,)π) β Β¬ βπ β ran (,)(π₯ β π β§ π β π)) |
126 | 125 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (((π₯ β β β§ π β β) β§ π = (π₯[,)π)) β Β¬ βπ β ran (,)(π₯ β π β§ π β π)) |
127 | 66, 126 | jca 513 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((π₯ β β β§ π β β) β§ π = (π₯[,)π)) β (π β πΌ β§ Β¬ βπ β ran (,)(π₯ β π β§ π β π))) |
128 | 127 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π₯ β β β§ π β β) β§ π₯ < π) β§ π = (π₯[,)π)) β (π β πΌ β§ Β¬ βπ β ran (,)(π₯ β π β§ π β π))) |
129 | 49, 128 | jca 513 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π₯ β β β§ π β β) β§ π₯ < π) β§ π = (π₯[,)π)) β (π₯ β π β§ (π β πΌ β§ Β¬ βπ β ran (,)(π₯ β π β§ π β π)))) |
130 | | an12 644 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π₯ β π β§ (π β πΌ β§ Β¬ βπ β ran (,)(π₯ β π β§ π β π))) β (π β πΌ β§ (π₯ β π β§ Β¬ βπ β ran (,)(π₯ β π β§ π β π)))) |
131 | | annim 405 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π₯ β π β§ Β¬ βπ β ran (,)(π₯ β π β§ π β π)) β Β¬ (π₯ β π β βπ β ran (,)(π₯ β π β§ π β π))) |
132 | 131 | anbi2i 624 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β πΌ β§ (π₯ β π β§ Β¬ βπ β ran (,)(π₯ β π β§ π β π))) β (π β πΌ β§ Β¬ (π₯ β π β βπ β ran (,)(π₯ β π β§ π β π)))) |
133 | 130, 132 | bitri 275 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π₯ β π β§ (π β πΌ β§ Β¬ βπ β ran (,)(π₯ β π β§ π β π))) β (π β πΌ β§ Β¬ (π₯ β π β βπ β ran (,)(π₯ β π β§ π β π)))) |
134 | 129, 133 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π₯ β β β§ π β β) β§ π₯ < π) β§ π = (π₯[,)π)) β (π β πΌ β§ Β¬ (π₯ β π β βπ β ran (,)(π₯ β π β§ π β π)))) |
135 | | rspe 3231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β πΌ β§ Β¬ (π₯ β π β βπ β ran (,)(π₯ β π β§ π β π))) β βπ β πΌ Β¬ (π₯ β π β βπ β ran (,)(π₯ β π β§ π β π))) |
136 | 134, 135 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π₯ β β β§ π β β) β§ π₯ < π) β§ π = (π₯[,)π)) β βπ β πΌ Β¬ (π₯ β π β βπ β ran (,)(π₯ β π β§ π β π))) |
137 | | rexnal 3100 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(βπ β
πΌ Β¬ (π₯ β π β βπ β ran (,)(π₯ β π β§ π β π)) β Β¬ βπ β πΌ (π₯ β π β βπ β ran (,)(π₯ β π β§ π β π))) |
138 | 136, 137 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π₯ β β β§ π β β) β§ π₯ < π) β§ π = (π₯[,)π)) β Β¬ βπ β πΌ (π₯ β π β βπ β ran (,)(π₯ β π β§ π β π))) |
139 | 138 | exp41 436 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π₯ β β β (π β β β (π₯ < π β (π = (π₯[,)π) β Β¬ βπ β πΌ (π₯ β π β βπ β ran (,)(π₯ β π β§ π β π)))))) |
140 | 139 | com4l 92 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β β β (π₯ < π β (π = (π₯[,)π) β (π₯ β β β Β¬ βπ β πΌ (π₯ β π β βπ β ran (,)(π₯ β π β§ π β π)))))) |
141 | 140 | imp41 427 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β β β§ π₯ < π) β§ π = (π₯[,)π)) β§ π₯ β β) β Β¬ βπ β πΌ (π₯ β π β βπ β ran (,)(π₯ β π β§ π β π))) |
142 | | rspe 3231 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π₯ β β β§ Β¬
βπ β πΌ (π₯ β π β βπ β ran (,)(π₯ β π β§ π β π))) β βπ₯ β β Β¬ βπ β πΌ (π₯ β π β βπ β ran (,)(π₯ β π β§ π β π))) |
143 | 34, 141, 142 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β β β§ π₯ < π) β§ π = (π₯[,)π)) β§ π₯ β β) β βπ₯ β β Β¬
βπ β πΌ (π₯ β π β βπ β ran (,)(π₯ β π β§ π β π))) |
144 | | rexnal 3100 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(βπ₯ β
β Β¬ βπ
β πΌ (π₯ β π β βπ β ran (,)(π₯ β π β§ π β π)) β Β¬ βπ₯ β β βπ β πΌ (π₯ β π β βπ β ran (,)(π₯ β π β§ π β π))) |
145 | 143, 144 | sylib 217 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β β β§ π₯ < π) β§ π = (π₯[,)π)) β§ π₯ β β) β Β¬ βπ₯ β β βπ β πΌ (π₯ β π β βπ β ran (,)(π₯ β π β§ π β π))) |
146 | | df-ico 13276 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ [,) =
(π β
β*, π
β β* β¦ {π§ β β* β£ (π β€ π§ β§ π§ < π)}) |
147 | 146 | ixxex 13281 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ [,)
β V |
148 | | imaexg 7853 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ([,)
β V β ([,) β (β Γ β)) β
V) |
149 | 147, 148 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ([,)
β (β Γ β)) β V |
150 | 1, 149 | eqeltri 2830 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ πΌ β V |
151 | 1 | icoreunrn 35876 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ β =
βͺ πΌ |
152 | | unirnioo 13372 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ β =
βͺ ran (,) |
153 | 151, 152 | eqtr3i 2763 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ βͺ πΌ =
βͺ ran (,) |
154 | | tgss2 22353 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((πΌ β V β§ βͺ πΌ =
βͺ ran (,)) β ((topGenβπΌ) β (topGenβran (,)) β
βπ₯ β βͺ πΌβπ β πΌ (π₯ β π β βπ β ran (,)(π₯ β π β§ π β π)))) |
155 | 150, 153,
154 | mp2an 691 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((topGenβπΌ)
β (topGenβran (,)) β βπ₯ β βͺ πΌβπ β πΌ (π₯ β π β βπ β ran (,)(π₯ β π β§ π β π))) |
156 | 151 | raleqi 3310 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(βπ₯ β
β βπ β
πΌ (π₯ β π β βπ β ran (,)(π₯ β π β§ π β π)) β βπ₯ β βͺ πΌβπ β πΌ (π₯ β π β βπ β ran (,)(π₯ β π β§ π β π))) |
157 | 155, 156 | bitr4i 278 |
. . . . . . . . . . . . . . . . . . . 20
β’
((topGenβπΌ)
β (topGenβran (,)) β βπ₯ β β βπ β πΌ (π₯ β π β βπ β ran (,)(π₯ β π β§ π β π))) |
158 | 145, 157 | sylnibr 329 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β β β§ π₯ < π) β§ π = (π₯[,)π)) β§ π₯ β β) β Β¬
(topGenβπΌ) β
(topGenβran (,))) |
159 | 158 | sbcth 3755 |
. . . . . . . . . . . . . . . . . 18
β’ (1 β
β β [1 / π₯]((((π β β β§ π₯ < π) β§ π = (π₯[,)π)) β§ π₯ β β) β Β¬
(topGenβπΌ) β
(topGenβran (,)))) |
160 | 7, 159 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
β’ [1
/ π₯]((((π β β β§ π₯ < π) β§ π = (π₯[,)π)) β§ π₯ β β) β Β¬
(topGenβπΌ) β
(topGenβran (,))) |
161 | | sbcimg 3791 |
. . . . . . . . . . . . . . . . . 18
β’ (1 β
β β ([1 / π₯]((((π β β β§ π₯ < π) β§ π = (π₯[,)π)) β§ π₯ β β) β Β¬
(topGenβπΌ) β
(topGenβran (,))) β ([1 / π₯](((π β β β§ π₯ < π) β§ π = (π₯[,)π)) β§ π₯ β β) β [1 / π₯] Β¬
(topGenβπΌ) β
(topGenβran (,))))) |
162 | 7, 161 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
β’
([1 / π₯]((((π β β β§ π₯ < π) β§ π = (π₯[,)π)) β§ π₯ β β) β Β¬
(topGenβπΌ) β
(topGenβran (,))) β ([1 / π₯](((π β β β§ π₯ < π) β§ π = (π₯[,)π)) β§ π₯ β β) β [1 / π₯] Β¬
(topGenβπΌ) β
(topGenβran (,)))) |
163 | 160, 162 | mpbi 229 |
. . . . . . . . . . . . . . . 16
β’
([1 / π₯](((π β β β§ π₯ < π) β§ π = (π₯[,)π)) β§ π₯ β β) β [1 / π₯] Β¬
(topGenβπΌ) β
(topGenβran (,))) |
164 | | sbcel1v 3811 |
. . . . . . . . . . . . . . . . . 18
β’
([1 / π₯]π₯ β β β 1 β
β) |
165 | 7, 164 | mpbir 230 |
. . . . . . . . . . . . . . . . 17
β’ [1
/ π₯]π₯ β β |
166 | | sbcan 3792 |
. . . . . . . . . . . . . . . . 17
β’
([1 / π₯](((π β β β§ π₯ < π) β§ π = (π₯[,)π)) β§ π₯ β β) β ([1 / π₯]((π β β β§ π₯ < π) β§ π = (π₯[,)π)) β§ [1 / π₯]π₯ β β)) |
167 | 165, 166 | mpbiran2 709 |
. . . . . . . . . . . . . . . 16
β’
([1 / π₯](((π β β β§ π₯ < π) β§ π = (π₯[,)π)) β§ π₯ β β) β [1 / π₯]((π β β β§ π₯ < π) β§ π = (π₯[,)π))) |
168 | | sbcg 3819 |
. . . . . . . . . . . . . . . . 17
β’ (1 β
β β ([1 / π₯] Β¬ (topGenβπΌ) β (topGenβran (,))
β Β¬ (topGenβπΌ) β (topGenβran
(,)))) |
169 | 7, 168 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
β’
([1 / π₯] Β¬ (topGenβπΌ) β (topGenβran (,))
β Β¬ (topGenβπΌ) β (topGenβran
(,))) |
170 | 163, 167,
169 | 3imtr3i 291 |
. . . . . . . . . . . . . . 15
β’
([1 / π₯]((π β β β§ π₯ < π) β§ π = (π₯[,)π)) β Β¬ (topGenβπΌ) β (topGenβran
(,))) |
171 | 33, 170 | sylbir 234 |
. . . . . . . . . . . . . 14
β’
(([1 / π₯](π β β β§ π₯ < π) β§ [1 / π₯]π = (π₯[,)π)) β Β¬ (topGenβπΌ) β (topGenβran
(,))) |
172 | 21, 32, 171 | syl2anbr 600 |
. . . . . . . . . . . . 13
β’ (((π β β β§ 1 <
π) β§ π = (1[,)π)) β Β¬ (topGenβπΌ) β (topGenβran
(,))) |
173 | 172 | sbcth 3755 |
. . . . . . . . . . . 12
β’
((1[,)π) β V
β [(1[,)π) /
π](((π β β β§ 1 <
π) β§ π = (1[,)π)) β Β¬ (topGenβπΌ) β (topGenβran
(,)))) |
174 | 5, 173 | ax-mp 5 |
. . . . . . . . . . 11
β’
[(1[,)π) /
π](((π β β β§ 1 <
π) β§ π = (1[,)π)) β Β¬ (topGenβπΌ) β (topGenβran
(,))) |
175 | | sbcimg 3791 |
. . . . . . . . . . . 12
β’
((1[,)π) β V
β ([(1[,)π) /
π](((π β β β§ 1 <
π) β§ π = (1[,)π)) β Β¬ (topGenβπΌ) β (topGenβran
(,))) β ([(1[,)π) / π]((π β β β§ 1 < π) β§ π = (1[,)π)) β [(1[,)π) / π] Β¬ (topGenβπΌ) β (topGenβran
(,))))) |
176 | 5, 175 | ax-mp 5 |
. . . . . . . . . . 11
β’
([(1[,)π) /
π](((π β β β§ 1 <
π) β§ π = (1[,)π)) β Β¬ (topGenβπΌ) β (topGenβran
(,))) β ([(1[,)π) / π]((π β β β§ 1 < π) β§ π = (1[,)π)) β [(1[,)π) / π] Β¬ (topGenβπΌ) β (topGenβran
(,)))) |
177 | 174, 176 | mpbi 229 |
. . . . . . . . . 10
β’
([(1[,)π) /
π]((π β β β§ 1 <
π) β§ π = (1[,)π)) β [(1[,)π) / π] Β¬ (topGenβπΌ) β (topGenβran
(,))) |
178 | | sbcan 3792 |
. . . . . . . . . . 11
β’
([(1[,)π) /
π]((π β β β§ 1 <
π) β§ π = (1[,)π)) β ([(1[,)π) / π](π β β β§ 1 < π) β§ [(1[,)π) / π]π = (1[,)π))) |
179 | | eqid 2733 |
. . . . . . . . . . . . 13
β’
(1[,)π) = (1[,)π) |
180 | | eqsbc1 3789 |
. . . . . . . . . . . . . 14
β’
((1[,)π) β V
β ([(1[,)π) /
π]π = (1[,)π) β (1[,)π) = (1[,)π))) |
181 | 5, 180 | ax-mp 5 |
. . . . . . . . . . . . 13
β’
([(1[,)π) /
π]π = (1[,)π) β (1[,)π) = (1[,)π)) |
182 | 179, 181 | mpbir 230 |
. . . . . . . . . . . 12
β’
[(1[,)π) /
π]π = (1[,)π) |
183 | | sbcg 3819 |
. . . . . . . . . . . . . 14
β’
((1[,)π) β V
β ([(1[,)π) /
π](π β β β§ 1 <
π) β (π β β β§ 1 <
π))) |
184 | 5, 183 | ax-mp 5 |
. . . . . . . . . . . . 13
β’
([(1[,)π) /
π](π β β β§ 1 <
π) β (π β β β§ 1 <
π)) |
185 | 184 | anbi1i 625 |
. . . . . . . . . . . 12
β’
(([(1[,)π) /
π](π β β β§ 1 <
π) β§ [(1[,)π) / π]π = (1[,)π)) β ((π β β β§ 1 < π) β§ [(1[,)π) / π]π = (1[,)π))) |
186 | 182, 185 | mpbiran2 709 |
. . . . . . . . . . 11
β’
(([(1[,)π) /
π](π β β β§ 1 <
π) β§ [(1[,)π) / π]π = (1[,)π)) β (π β β β§ 1 < π)) |
187 | 178, 186 | bitri 275 |
. . . . . . . . . 10
β’
([(1[,)π) /
π]((π β β β§ 1 <
π) β§ π = (1[,)π)) β (π β β β§ 1 < π)) |
188 | | sbcg 3819 |
. . . . . . . . . . 11
β’
((1[,)π) β V
β ([(1[,)π) /
π] Β¬
(topGenβπΌ) β
(topGenβran (,)) β Β¬ (topGenβπΌ) β (topGenβran
(,)))) |
189 | 5, 188 | ax-mp 5 |
. . . . . . . . . 10
β’
([(1[,)π) /
π] Β¬
(topGenβπΌ) β
(topGenβran (,)) β Β¬ (topGenβπΌ) β (topGenβran
(,))) |
190 | 177, 187,
189 | 3imtr3i 291 |
. . . . . . . . 9
β’ ((π β β β§ 1 <
π) β Β¬
(topGenβπΌ) β
(topGenβran (,))) |
191 | 190 | sbcth 3755 |
. . . . . . . 8
β’ (2 β
β β [2 / π]((π β β β§ 1 < π) β Β¬
(topGenβπΌ) β
(topGenβran (,)))) |
192 | 3, 191 | ax-mp 5 |
. . . . . . 7
β’ [2
/ π]((π β β β§ 1 <
π) β Β¬
(topGenβπΌ) β
(topGenβran (,))) |
193 | | sbcimg 3791 |
. . . . . . . 8
β’ (2 β
β β ([2 / π]((π β β β§ 1 < π) β Β¬
(topGenβπΌ) β
(topGenβran (,))) β ([2 / π](π β β β§ 1 < π) β [2 / π] Β¬
(topGenβπΌ) β
(topGenβran (,))))) |
194 | 3, 193 | ax-mp 5 |
. . . . . . 7
β’
([2 / π]((π β β β§ 1 < π) β Β¬
(topGenβπΌ) β
(topGenβran (,))) β ([2 / π](π β β β§ 1 < π) β [2 / π] Β¬
(topGenβπΌ) β
(topGenβran (,)))) |
195 | 192, 194 | mpbi 229 |
. . . . . 6
β’
([2 / π](π β β β§ 1 < π) β [2 / π] Β¬
(topGenβπΌ) β
(topGenβran (,))) |
196 | | sbcan 3792 |
. . . . . . 7
β’
([2 / π](π β β β§ 1 < π) β ([2 / π]π β β β§ [2 / π]1 < π)) |
197 | | sbcel1v 3811 |
. . . . . . . 8
β’
([2 / π]π β β β 2 β
β) |
198 | | sbcbr123 5160 |
. . . . . . . . 9
β’
([2 / π]1 < π β β¦2 / πβ¦1β¦2 / πβ¦ <
β¦2 / πβ¦π) |
199 | | csbconstg 3875 |
. . . . . . . . . . 11
β’ (2 β
β β β¦2 / πβ¦1 = 1) |
200 | 3, 199 | ax-mp 5 |
. . . . . . . . . 10
β’
β¦2 / πβ¦1 = 1 |
201 | | csbvarg 4392 |
. . . . . . . . . . 11
β’ (2 β
β β β¦2 / πβ¦π = 2) |
202 | 3, 201 | ax-mp 5 |
. . . . . . . . . 10
β’
β¦2 / πβ¦π = 2 |
203 | 200, 202 | breq12i 5115 |
. . . . . . . . 9
β’
(β¦2 / πβ¦1β¦2 / πβ¦ <
β¦2 / πβ¦π β 1β¦2 / πβ¦ <
2) |
204 | | csbconstg 3875 |
. . . . . . . . . . 11
β’ (2 β
β β β¦2 / πβ¦ < = <
) |
205 | 3, 204 | ax-mp 5 |
. . . . . . . . . 10
β’
β¦2 / πβ¦ < = < |
206 | 205 | breqi 5112 |
. . . . . . . . 9
β’
(1β¦2 / πβ¦ < 2 β 1 <
2) |
207 | 198, 203,
206 | 3bitri 297 |
. . . . . . . 8
β’
([2 / π]1 < π β 1 < 2) |
208 | 197, 207 | anbi12i 628 |
. . . . . . 7
β’
(([2 / π]π β β β§ [2 / π]1 < π) β (2 β β β§
1 < 2)) |
209 | 196, 208 | bitri 275 |
. . . . . 6
β’
([2 / π](π β β β§ 1 < π) β (2 β β β§
1 < 2)) |
210 | | sbcg 3819 |
. . . . . . 7
β’ (2 β
β β ([2 / π] Β¬ (topGenβπΌ) β (topGenβran (,))
β Β¬ (topGenβπΌ) β (topGenβran
(,)))) |
211 | 3, 210 | ax-mp 5 |
. . . . . 6
β’
([2 / π] Β¬ (topGenβπΌ) β (topGenβran (,))
β Β¬ (topGenβπΌ) β (topGenβran
(,))) |
212 | 195, 209,
211 | 3imtr3i 291 |
. . . . 5
β’ ((2
β β β§ 1 < 2) β Β¬ (topGenβπΌ) β (topGenβran
(,))) |
213 | 3, 4, 212 | mp2an 691 |
. . . 4
β’ Β¬
(topGenβπΌ) β
(topGenβran (,)) |
214 | | eqimss 4001 |
. . . 4
β’
((topGenβπΌ) =
(topGenβran (,)) β (topGenβπΌ) β (topGenβran
(,))) |
215 | 213, 214 | mto 196 |
. . 3
β’ Β¬
(topGenβπΌ) =
(topGenβran (,)) |
216 | 215 | nesymir 2999 |
. 2
β’
(topGenβran (,)) β (topGenβπΌ) |
217 | | df-pss 3930 |
. 2
β’
((topGenβran (,)) β (topGenβπΌ) β ((topGenβran (,)) β
(topGenβπΌ) β§
(topGenβran (,)) β (topGenβπΌ))) |
218 | 2, 216, 217 | mpbir2an 710 |
1
β’
(topGenβran (,)) β (topGenβπΌ) |