Step | Hyp | Ref
| Expression |
1 | | ovolicc.2 |
. . . . . 6
β’ (π β π΅ β β) |
2 | 1 | adantr 482 |
. . . . 5
β’ ((π β§ π β β) β π΅ β β) |
3 | | ovolicc2.5 |
. . . . . . . . 9
β’ (π β πΉ:ββΆ( β€ β© (β
Γ β))) |
4 | | inss2 4193 |
. . . . . . . . 9
β’ ( β€
β© (β Γ β)) β (β Γ
β) |
5 | | fss 6689 |
. . . . . . . . 9
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ ( β€ β© (β Γ β))
β (β Γ β)) β πΉ:ββΆ(β Γ
β)) |
6 | 3, 4, 5 | sylancl 587 |
. . . . . . . 8
β’ (π β πΉ:ββΆ(β Γ
β)) |
7 | 6 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β β) β πΉ:ββΆ(β Γ
β)) |
8 | | ovolicc2.8 |
. . . . . . . . 9
β’ (π β πΊ:πβΆβ) |
9 | 8 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β β) β πΊ:πβΆβ) |
10 | | nnuz 12814 |
. . . . . . . . . . . 12
β’ β =
(β€β₯β1) |
11 | | ovolicc2.15 |
. . . . . . . . . . . 12
β’ πΎ = seq1((π» β 1st ), (β Γ
{πΆ})) |
12 | | 1zzd 12542 |
. . . . . . . . . . . 12
β’ (π β 1 β
β€) |
13 | | ovolicc2.14 |
. . . . . . . . . . . 12
β’ (π β πΆ β π) |
14 | | ovolicc2.11 |
. . . . . . . . . . . 12
β’ (π β π»:πβΆπ) |
15 | 10, 11, 12, 13, 14 | algrf 16457 |
. . . . . . . . . . 11
β’ (π β πΎ:ββΆπ) |
16 | 15 | ffvelcdmda 7039 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (πΎβπ) β π) |
17 | | ineq1 4169 |
. . . . . . . . . . . 12
β’ (π’ = (πΎβπ) β (π’ β© (π΄[,]π΅)) = ((πΎβπ) β© (π΄[,]π΅))) |
18 | 17 | neeq1d 3000 |
. . . . . . . . . . 11
β’ (π’ = (πΎβπ) β ((π’ β© (π΄[,]π΅)) β β
β ((πΎβπ) β© (π΄[,]π΅)) β β
)) |
19 | | ovolicc2.10 |
. . . . . . . . . . 11
β’ π = {π’ β π β£ (π’ β© (π΄[,]π΅)) β β
} |
20 | 18, 19 | elrab2 3652 |
. . . . . . . . . 10
β’ ((πΎβπ) β π β ((πΎβπ) β π β§ ((πΎβπ) β© (π΄[,]π΅)) β β
)) |
21 | 16, 20 | sylib 217 |
. . . . . . . . 9
β’ ((π β§ π β β) β ((πΎβπ) β π β§ ((πΎβπ) β© (π΄[,]π΅)) β β
)) |
22 | 21 | simpld 496 |
. . . . . . . 8
β’ ((π β§ π β β) β (πΎβπ) β π) |
23 | 9, 22 | ffvelcdmd 7040 |
. . . . . . 7
β’ ((π β§ π β β) β (πΊβ(πΎβπ)) β β) |
24 | 7, 23 | ffvelcdmd 7040 |
. . . . . 6
β’ ((π β§ π β β) β (πΉβ(πΊβ(πΎβπ))) β (β Γ
β)) |
25 | | xp2nd 7958 |
. . . . . 6
β’ ((πΉβ(πΊβ(πΎβπ))) β (β Γ β) β
(2nd β(πΉβ(πΊβ(πΎβπ)))) β β) |
26 | 24, 25 | syl 17 |
. . . . 5
β’ ((π β§ π β β) β (2nd
β(πΉβ(πΊβ(πΎβπ)))) β β) |
27 | 2, 26 | ltnled 11310 |
. . . 4
β’ ((π β§ π β β) β (π΅ < (2nd β(πΉβ(πΊβ(πΎβπ)))) β Β¬ (2nd
β(πΉβ(πΊβ(πΎβπ)))) β€ π΅)) |
28 | | simprl 770 |
. . . . . 6
β’ ((π β§ (π β β β§ π΅ < (2nd β(πΉβ(πΊβ(πΎβπ)))))) β π β β) |
29 | 1 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π β β β§ π΅ < (2nd β(πΉβ(πΊβ(πΎβπ)))))) β π΅ β β) |
30 | 21 | adantrr 716 |
. . . . . . . . . 10
β’ ((π β§ (π β β β§ π΅ < (2nd β(πΉβ(πΊβ(πΎβπ)))))) β ((πΎβπ) β π β§ ((πΎβπ) β© (π΄[,]π΅)) β β
)) |
31 | 30 | simprd 497 |
. . . . . . . . 9
β’ ((π β§ (π β β β§ π΅ < (2nd β(πΉβ(πΊβ(πΎβπ)))))) β ((πΎβπ) β© (π΄[,]π΅)) β β
) |
32 | | n0 4310 |
. . . . . . . . 9
β’ (((πΎβπ) β© (π΄[,]π΅)) β β
β βπ₯ π₯ β ((πΎβπ) β© (π΄[,]π΅))) |
33 | 31, 32 | sylib 217 |
. . . . . . . 8
β’ ((π β§ (π β β β§ π΅ < (2nd β(πΉβ(πΊβ(πΎβπ)))))) β βπ₯ π₯ β ((πΎβπ) β© (π΄[,]π΅))) |
34 | | xp1st 7957 |
. . . . . . . . . . . 12
β’ ((πΉβ(πΊβ(πΎβπ))) β (β Γ β) β
(1st β(πΉβ(πΊβ(πΎβπ)))) β β) |
35 | 24, 34 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (1st
β(πΉβ(πΊβ(πΎβπ)))) β β) |
36 | 35 | adantrr 716 |
. . . . . . . . . 10
β’ ((π β§ (π β β β§ π΅ < (2nd β(πΉβ(πΊβ(πΎβπ)))))) β (1st β(πΉβ(πΊβ(πΎβπ)))) β β) |
37 | 36 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ (π β β β§ π΅ < (2nd β(πΉβ(πΊβ(πΎβπ)))))) β§ π₯ β ((πΎβπ) β© (π΄[,]π΅))) β (1st β(πΉβ(πΊβ(πΎβπ)))) β β) |
38 | | simpr 486 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β β β§ π΅ < (2nd β(πΉβ(πΊβ(πΎβπ)))))) β§ π₯ β ((πΎβπ) β© (π΄[,]π΅))) β π₯ β ((πΎβπ) β© (π΄[,]π΅))) |
39 | | elin 3930 |
. . . . . . . . . . . . 13
β’ (π₯ β ((πΎβπ) β© (π΄[,]π΅)) β (π₯ β (πΎβπ) β§ π₯ β (π΄[,]π΅))) |
40 | 38, 39 | sylib 217 |
. . . . . . . . . . . 12
β’ (((π β§ (π β β β§ π΅ < (2nd β(πΉβ(πΊβ(πΎβπ)))))) β§ π₯ β ((πΎβπ) β© (π΄[,]π΅))) β (π₯ β (πΎβπ) β§ π₯ β (π΄[,]π΅))) |
41 | 40 | simprd 497 |
. . . . . . . . . . 11
β’ (((π β§ (π β β β§ π΅ < (2nd β(πΉβ(πΊβ(πΎβπ)))))) β§ π₯ β ((πΎβπ) β© (π΄[,]π΅))) β π₯ β (π΄[,]π΅)) |
42 | | ovolicc.1 |
. . . . . . . . . . . . 13
β’ (π β π΄ β β) |
43 | | elicc2 13338 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§ π΅ β β) β (π₯ β (π΄[,]π΅) β (π₯ β β β§ π΄ β€ π₯ β§ π₯ β€ π΅))) |
44 | 42, 1, 43 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (π β (π₯ β (π΄[,]π΅) β (π₯ β β β§ π΄ β€ π₯ β§ π₯ β€ π΅))) |
45 | 44 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ (π β β β§ π΅ < (2nd β(πΉβ(πΊβ(πΎβπ)))))) β§ π₯ β ((πΎβπ) β© (π΄[,]π΅))) β (π₯ β (π΄[,]π΅) β (π₯ β β β§ π΄ β€ π₯ β§ π₯ β€ π΅))) |
46 | 41, 45 | mpbid 231 |
. . . . . . . . . 10
β’ (((π β§ (π β β β§ π΅ < (2nd β(πΉβ(πΊβ(πΎβπ)))))) β§ π₯ β ((πΎβπ) β© (π΄[,]π΅))) β (π₯ β β β§ π΄ β€ π₯ β§ π₯ β€ π΅)) |
47 | 46 | simp1d 1143 |
. . . . . . . . 9
β’ (((π β§ (π β β β§ π΅ < (2nd β(πΉβ(πΊβ(πΎβπ)))))) β§ π₯ β ((πΎβπ) β© (π΄[,]π΅))) β π₯ β β) |
48 | 1 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ (π β β β§ π΅ < (2nd β(πΉβ(πΊβ(πΎβπ)))))) β§ π₯ β ((πΎβπ) β© (π΄[,]π΅))) β π΅ β β) |
49 | 40 | simpld 496 |
. . . . . . . . . . 11
β’ (((π β§ (π β β β§ π΅ < (2nd β(πΉβ(πΊβ(πΎβπ)))))) β§ π₯ β ((πΎβπ) β© (π΄[,]π΅))) β π₯ β (πΎβπ)) |
50 | 30 | simpld 496 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β β β§ π΅ < (2nd β(πΉβ(πΊβ(πΎβπ)))))) β (πΎβπ) β π) |
51 | | ovolicc.3 |
. . . . . . . . . . . . . 14
β’ (π β π΄ β€ π΅) |
52 | | ovolicc2.4 |
. . . . . . . . . . . . . 14
β’ π = seq1( + , ((abs β
β ) β πΉ)) |
53 | | ovolicc2.6 |
. . . . . . . . . . . . . 14
β’ (π β π β (π« ran ((,) β πΉ) β© Fin)) |
54 | | ovolicc2.7 |
. . . . . . . . . . . . . 14
β’ (π β (π΄[,]π΅) β βͺ π) |
55 | | ovolicc2.9 |
. . . . . . . . . . . . . 14
β’ ((π β§ π‘ β π) β (((,) β πΉ)β(πΊβπ‘)) = π‘) |
56 | 42, 1, 51, 52, 3, 53, 54, 8, 55 | ovolicc2lem1 24904 |
. . . . . . . . . . . . 13
β’ ((π β§ (πΎβπ) β π) β (π₯ β (πΎβπ) β (π₯ β β β§ (1st
β(πΉβ(πΊβ(πΎβπ)))) < π₯ β§ π₯ < (2nd β(πΉβ(πΊβ(πΎβπ))))))) |
57 | 50, 56 | syldan 592 |
. . . . . . . . . . . 12
β’ ((π β§ (π β β β§ π΅ < (2nd β(πΉβ(πΊβ(πΎβπ)))))) β (π₯ β (πΎβπ) β (π₯ β β β§ (1st
β(πΉβ(πΊβ(πΎβπ)))) < π₯ β§ π₯ < (2nd β(πΉβ(πΊβ(πΎβπ))))))) |
58 | 57 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ (π β β β§ π΅ < (2nd β(πΉβ(πΊβ(πΎβπ)))))) β§ π₯ β ((πΎβπ) β© (π΄[,]π΅))) β (π₯ β (πΎβπ) β (π₯ β β β§ (1st
β(πΉβ(πΊβ(πΎβπ)))) < π₯ β§ π₯ < (2nd β(πΉβ(πΊβ(πΎβπ))))))) |
59 | 49, 58 | mpbid 231 |
. . . . . . . . . 10
β’ (((π β§ (π β β β§ π΅ < (2nd β(πΉβ(πΊβ(πΎβπ)))))) β§ π₯ β ((πΎβπ) β© (π΄[,]π΅))) β (π₯ β β β§ (1st
β(πΉβ(πΊβ(πΎβπ)))) < π₯ β§ π₯ < (2nd β(πΉβ(πΊβ(πΎβπ)))))) |
60 | 59 | simp2d 1144 |
. . . . . . . . 9
β’ (((π β§ (π β β β§ π΅ < (2nd β(πΉβ(πΊβ(πΎβπ)))))) β§ π₯ β ((πΎβπ) β© (π΄[,]π΅))) β (1st β(πΉβ(πΊβ(πΎβπ)))) < π₯) |
61 | 46 | simp3d 1145 |
. . . . . . . . 9
β’ (((π β§ (π β β β§ π΅ < (2nd β(πΉβ(πΊβ(πΎβπ)))))) β§ π₯ β ((πΎβπ) β© (π΄[,]π΅))) β π₯ β€ π΅) |
62 | 37, 47, 48, 60, 61 | ltletrd 11323 |
. . . . . . . 8
β’ (((π β§ (π β β β§ π΅ < (2nd β(πΉβ(πΊβ(πΎβπ)))))) β§ π₯ β ((πΎβπ) β© (π΄[,]π΅))) β (1st β(πΉβ(πΊβ(πΎβπ)))) < π΅) |
63 | 33, 62 | exlimddv 1939 |
. . . . . . 7
β’ ((π β§ (π β β β§ π΅ < (2nd β(πΉβ(πΊβ(πΎβπ)))))) β (1st β(πΉβ(πΊβ(πΎβπ)))) < π΅) |
64 | | simprr 772 |
. . . . . . 7
β’ ((π β§ (π β β β§ π΅ < (2nd β(πΉβ(πΊβ(πΎβπ)))))) β π΅ < (2nd β(πΉβ(πΊβ(πΎβπ))))) |
65 | 42, 1, 51, 52, 3, 53, 54, 8, 55 | ovolicc2lem1 24904 |
. . . . . . . 8
β’ ((π β§ (πΎβπ) β π) β (π΅ β (πΎβπ) β (π΅ β β β§ (1st
β(πΉβ(πΊβ(πΎβπ)))) < π΅ β§ π΅ < (2nd β(πΉβ(πΊβ(πΎβπ))))))) |
66 | 50, 65 | syldan 592 |
. . . . . . 7
β’ ((π β§ (π β β β§ π΅ < (2nd β(πΉβ(πΊβ(πΎβπ)))))) β (π΅ β (πΎβπ) β (π΅ β β β§ (1st
β(πΉβ(πΊβ(πΎβπ)))) < π΅ β§ π΅ < (2nd β(πΉβ(πΊβ(πΎβπ))))))) |
67 | 29, 63, 64, 66 | mpbir3and 1343 |
. . . . . 6
β’ ((π β§ (π β β β§ π΅ < (2nd β(πΉβ(πΊβ(πΎβπ)))))) β π΅ β (πΎβπ)) |
68 | | fveq2 6846 |
. . . . . . . 8
β’ (π = π β (πΎβπ) = (πΎβπ)) |
69 | 68 | eleq2d 2820 |
. . . . . . 7
β’ (π = π β (π΅ β (πΎβπ) β π΅ β (πΎβπ))) |
70 | | ovolicc2.16 |
. . . . . . 7
β’ π = {π β β β£ π΅ β (πΎβπ)} |
71 | 69, 70 | elrab2 3652 |
. . . . . 6
β’ (π β π β (π β β β§ π΅ β (πΎβπ))) |
72 | 28, 67, 71 | sylanbrc 584 |
. . . . 5
β’ ((π β§ (π β β β§ π΅ < (2nd β(πΉβ(πΊβ(πΎβπ)))))) β π β π) |
73 | 72 | expr 458 |
. . . 4
β’ ((π β§ π β β) β (π΅ < (2nd β(πΉβ(πΊβ(πΎβπ)))) β π β π)) |
74 | 27, 73 | sylbird 260 |
. . 3
β’ ((π β§ π β β) β (Β¬
(2nd β(πΉβ(πΊβ(πΎβπ)))) β€ π΅ β π β π)) |
75 | 74 | con1d 145 |
. 2
β’ ((π β§ π β β) β (Β¬ π β π β (2nd β(πΉβ(πΊβ(πΎβπ)))) β€ π΅)) |
76 | 75 | impr 456 |
1
β’ ((π β§ (π β β β§ Β¬ π β π)) β (2nd β(πΉβ(πΊβ(πΎβπ)))) β€ π΅) |