Step | Hyp | Ref
| Expression |
1 | | ssrab2 4072 |
. . . . . . 7
β’ {π β (1..^π) β£ π₯ β π΄} β (1..^π) |
2 | | fzossnn 13687 |
. . . . . . . . . 10
β’
(1..^π) β
β |
3 | | nnuz 12869 |
. . . . . . . . . 10
β’ β =
(β€β₯β1) |
4 | 2, 3 | sseqtri 4013 |
. . . . . . . . 9
β’
(1..^π) β
(β€β₯β1) |
5 | 1, 4 | sstri 3986 |
. . . . . . . 8
β’ {π β (1..^π) β£ π₯ β π΄} β
(β€β₯β1) |
6 | | rabn0 4380 |
. . . . . . . . 9
β’ ({π β (1..^π) β£ π₯ β π΄} β β
β βπ β (1..^π)π₯ β π΄) |
7 | 6 | biimpri 227 |
. . . . . . . 8
β’
(βπ β
(1..^π)π₯ β π΄ β {π β (1..^π) β£ π₯ β π΄} β β
) |
8 | | infssuzcl 12920 |
. . . . . . . 8
β’ (({π β (1..^π) β£ π₯ β π΄} β (β€β₯β1)
β§ {π β (1..^π) β£ π₯ β π΄} β β
) β inf({π β (1..^π) β£ π₯ β π΄}, β, < ) β {π β (1..^π) β£ π₯ β π΄}) |
9 | 5, 7, 8 | sylancr 586 |
. . . . . . 7
β’
(βπ β
(1..^π)π₯ β π΄ β inf({π β (1..^π) β£ π₯ β π΄}, β, < ) β {π β (1..^π) β£ π₯ β π΄}) |
10 | 1, 9 | sselid 3975 |
. . . . . 6
β’
(βπ β
(1..^π)π₯ β π΄ β inf({π β (1..^π) β£ π₯ β π΄}, β, < ) β (1..^π)) |
11 | | nfrab1 3445 |
. . . . . . . . . . 11
β’
β²π{π β (1..^π) β£ π₯ β π΄} |
12 | | nfcv 2897 |
. . . . . . . . . . 11
β’
β²πβ |
13 | | nfcv 2897 |
. . . . . . . . . . 11
β’
β²π
< |
14 | 11, 12, 13 | nfinf 9479 |
. . . . . . . . . 10
β’
β²πinf({π β (1..^π) β£ π₯ β π΄}, β, < ) |
15 | | nfcv 2897 |
. . . . . . . . . 10
β’
β²π(1..^π) |
16 | 14 | nfcsb1 3912 |
. . . . . . . . . . 11
β’
β²πβ¦inf({π β (1..^π) β£ π₯ β π΄}, β, < ) / πβ¦π΄ |
17 | 16 | nfcri 2884 |
. . . . . . . . . 10
β’
β²π π₯ β
β¦inf({π
β (1..^π) β£
π₯ β π΄}, β, < ) / πβ¦π΄ |
18 | | csbeq1a 3902 |
. . . . . . . . . . 11
β’ (π = inf({π β (1..^π) β£ π₯ β π΄}, β, < ) β π΄ = β¦inf({π β (1..^π) β£ π₯ β π΄}, β, < ) / πβ¦π΄) |
19 | 18 | eleq2d 2813 |
. . . . . . . . . 10
β’ (π = inf({π β (1..^π) β£ π₯ β π΄}, β, < ) β (π₯ β π΄ β π₯ β β¦inf({π β (1..^π) β£ π₯ β π΄}, β, < ) / πβ¦π΄)) |
20 | 14, 15, 17, 19 | elrabf 3674 |
. . . . . . . . 9
β’
(inf({π β
(1..^π) β£ π₯ β π΄}, β, < ) β {π β (1..^π) β£ π₯ β π΄} β (inf({π β (1..^π) β£ π₯ β π΄}, β, < ) β (1..^π) β§ π₯ β β¦inf({π β (1..^π) β£ π₯ β π΄}, β, < ) / πβ¦π΄)) |
21 | 9, 20 | sylib 217 |
. . . . . . . 8
β’
(βπ β
(1..^π)π₯ β π΄ β (inf({π β (1..^π) β£ π₯ β π΄}, β, < ) β (1..^π) β§ π₯ β β¦inf({π β (1..^π) β£ π₯ β π΄}, β, < ) / πβ¦π΄)) |
22 | 21 | simprd 495 |
. . . . . . 7
β’
(βπ β
(1..^π)π₯ β π΄ β π₯ β β¦inf({π β (1..^π) β£ π₯ β π΄}, β, < ) / πβ¦π΄) |
23 | 1, 2 | sstri 3986 |
. . . . . . . . . . 11
β’ {π β (1..^π) β£ π₯ β π΄} β β |
24 | | nnssre 12220 |
. . . . . . . . . . 11
β’ β
β β |
25 | 23, 24 | sstri 3986 |
. . . . . . . . . 10
β’ {π β (1..^π) β£ π₯ β π΄} β β |
26 | 25, 9 | sselid 3975 |
. . . . . . . . 9
β’
(βπ β
(1..^π)π₯ β π΄ β inf({π β (1..^π) β£ π₯ β π΄}, β, < ) β
β) |
27 | 26 | ltnrd 11352 |
. . . . . . . 8
β’
(βπ β
(1..^π)π₯ β π΄ β Β¬ inf({π β (1..^π) β£ π₯ β π΄}, β, < ) < inf({π β (1..^π) β£ π₯ β π΄}, β, < )) |
28 | | eliun 4994 |
. . . . . . . . 9
β’ (π₯ β βͺ π β (1..^inf({π β (1..^π) β£ π₯ β π΄}, β, < ))π΅ β βπ β (1..^inf({π β (1..^π) β£ π₯ β π΄}, β, < ))π₯ β π΅) |
29 | 26 | ad2antrr 723 |
. . . . . . . . . . 11
β’
(((βπ β
(1..^π)π₯ β π΄ β§ π β (1..^inf({π β (1..^π) β£ π₯ β π΄}, β, < ))) β§ π₯ β π΅) β inf({π β (1..^π) β£ π₯ β π΄}, β, < ) β
β) |
30 | | elfzouz2 13653 |
. . . . . . . . . . . . . . . 16
β’
(inf({π β
(1..^π) β£ π₯ β π΄}, β, < ) β (1..^π) β π β
(β€β₯βinf({π β (1..^π) β£ π₯ β π΄}, β, < ))) |
31 | | fzoss2 13666 |
. . . . . . . . . . . . . . . 16
β’ (π β
(β€β₯βinf({π β (1..^π) β£ π₯ β π΄}, β, < )) β (1..^inf({π β (1..^π) β£ π₯ β π΄}, β, < )) β (1..^π)) |
32 | 10, 30, 31 | 3syl 18 |
. . . . . . . . . . . . . . 15
β’
(βπ β
(1..^π)π₯ β π΄ β (1..^inf({π β (1..^π) β£ π₯ β π΄}, β, < )) β (1..^π)) |
33 | 32 | sselda 3977 |
. . . . . . . . . . . . . 14
β’
((βπ β
(1..^π)π₯ β π΄ β§ π β (1..^inf({π β (1..^π) β£ π₯ β π΄}, β, < ))) β π β (1..^π)) |
34 | 33 | adantr 480 |
. . . . . . . . . . . . 13
β’
(((βπ β
(1..^π)π₯ β π΄ β§ π β (1..^inf({π β (1..^π) β£ π₯ β π΄}, β, < ))) β§ π₯ β π΅) β π β (1..^π)) |
35 | 2, 34 | sselid 3975 |
. . . . . . . . . . . 12
β’
(((βπ β
(1..^π)π₯ β π΄ β§ π β (1..^inf({π β (1..^π) β£ π₯ β π΄}, β, < ))) β§ π₯ β π΅) β π β β) |
36 | 35 | nnred 12231 |
. . . . . . . . . . 11
β’
(((βπ β
(1..^π)π₯ β π΄ β§ π β (1..^inf({π β (1..^π) β£ π₯ β π΄}, β, < ))) β§ π₯ β π΅) β π β β) |
37 | | simpr 484 |
. . . . . . . . . . . . 13
β’
(((βπ β
(1..^π)π₯ β π΄ β§ π β (1..^inf({π β (1..^π) β£ π₯ β π΄}, β, < ))) β§ π₯ β π΅) β π₯ β π΅) |
38 | | nfcv 2897 |
. . . . . . . . . . . . . 14
β’
β²ππ |
39 | | iundisj3.0 |
. . . . . . . . . . . . . . 15
β’
β²ππ΅ |
40 | 39 | nfcri 2884 |
. . . . . . . . . . . . . 14
β’
β²π π₯ β π΅ |
41 | | iundisj3.1 |
. . . . . . . . . . . . . . 15
β’ (π = π β π΄ = π΅) |
42 | 41 | eleq2d 2813 |
. . . . . . . . . . . . . 14
β’ (π = π β (π₯ β π΄ β π₯ β π΅)) |
43 | 38, 15, 40, 42 | elrabf 3674 |
. . . . . . . . . . . . 13
β’ (π β {π β (1..^π) β£ π₯ β π΄} β (π β (1..^π) β§ π₯ β π΅)) |
44 | 34, 37, 43 | sylanbrc 582 |
. . . . . . . . . . . 12
β’
(((βπ β
(1..^π)π₯ β π΄ β§ π β (1..^inf({π β (1..^π) β£ π₯ β π΄}, β, < ))) β§ π₯ β π΅) β π β {π β (1..^π) β£ π₯ β π΄}) |
45 | | infssuzle 12919 |
. . . . . . . . . . . 12
β’ (({π β (1..^π) β£ π₯ β π΄} β (β€β₯β1)
β§ π β {π β (1..^π) β£ π₯ β π΄}) β inf({π β (1..^π) β£ π₯ β π΄}, β, < ) β€ π) |
46 | 5, 44, 45 | sylancr 586 |
. . . . . . . . . . 11
β’
(((βπ β
(1..^π)π₯ β π΄ β§ π β (1..^inf({π β (1..^π) β£ π₯ β π΄}, β, < ))) β§ π₯ β π΅) β inf({π β (1..^π) β£ π₯ β π΄}, β, < ) β€ π) |
47 | | elfzolt2 13647 |
. . . . . . . . . . . 12
β’ (π β (1..^inf({π β (1..^π) β£ π₯ β π΄}, β, < )) β π < inf({π β (1..^π) β£ π₯ β π΄}, β, < )) |
48 | 47 | ad2antlr 724 |
. . . . . . . . . . 11
β’
(((βπ β
(1..^π)π₯ β π΄ β§ π β (1..^inf({π β (1..^π) β£ π₯ β π΄}, β, < ))) β§ π₯ β π΅) β π < inf({π β (1..^π) β£ π₯ β π΄}, β, < )) |
49 | 29, 36, 29, 46, 48 | lelttrd 11376 |
. . . . . . . . . 10
β’
(((βπ β
(1..^π)π₯ β π΄ β§ π β (1..^inf({π β (1..^π) β£ π₯ β π΄}, β, < ))) β§ π₯ β π΅) β inf({π β (1..^π) β£ π₯ β π΄}, β, < ) < inf({π β (1..^π) β£ π₯ β π΄}, β, < )) |
50 | 49 | rexlimdva2 3151 |
. . . . . . . . 9
β’
(βπ β
(1..^π)π₯ β π΄ β (βπ β (1..^inf({π β (1..^π) β£ π₯ β π΄}, β, < ))π₯ β π΅ β inf({π β (1..^π) β£ π₯ β π΄}, β, < ) < inf({π β (1..^π) β£ π₯ β π΄}, β, < ))) |
51 | 28, 50 | biimtrid 241 |
. . . . . . . 8
β’
(βπ β
(1..^π)π₯ β π΄ β (π₯ β βͺ
π β (1..^inf({π β (1..^π) β£ π₯ β π΄}, β, < ))π΅ β inf({π β (1..^π) β£ π₯ β π΄}, β, < ) < inf({π β (1..^π) β£ π₯ β π΄}, β, < ))) |
52 | 27, 51 | mtod 197 |
. . . . . . 7
β’
(βπ β
(1..^π)π₯ β π΄ β Β¬ π₯ β βͺ
π β (1..^inf({π β (1..^π) β£ π₯ β π΄}, β, < ))π΅) |
53 | 22, 52 | eldifd 3954 |
. . . . . 6
β’
(βπ β
(1..^π)π₯ β π΄ β π₯ β (β¦inf({π β (1..^π) β£ π₯ β π΄}, β, < ) / πβ¦π΄ β βͺ
π β (1..^inf({π β (1..^π) β£ π₯ β π΄}, β, < ))π΅)) |
54 | | csbeq1 3891 |
. . . . . . . . 9
β’ (π = inf({π β (1..^π) β£ π₯ β π΄}, β, < ) β
β¦π / πβ¦π΄ = β¦inf({π β (1..^π) β£ π₯ β π΄}, β, < ) / πβ¦π΄) |
55 | | oveq2 7413 |
. . . . . . . . . 10
β’ (π = inf({π β (1..^π) β£ π₯ β π΄}, β, < ) β (1..^π) = (1..^inf({π β (1..^π) β£ π₯ β π΄}, β, < ))) |
56 | 55 | iuneq1d 5017 |
. . . . . . . . 9
β’ (π = inf({π β (1..^π) β£ π₯ β π΄}, β, < ) β βͺ π β (1..^π)π΅ = βͺ π β (1..^inf({π β (1..^π) β£ π₯ β π΄}, β, < ))π΅) |
57 | 54, 56 | difeq12d 4118 |
. . . . . . . 8
β’ (π = inf({π β (1..^π) β£ π₯ β π΄}, β, < ) β
(β¦π / πβ¦π΄ β βͺ
π β (1..^π)π΅) = (β¦inf({π β (1..^π) β£ π₯ β π΄}, β, < ) / πβ¦π΄ β βͺ
π β (1..^inf({π β (1..^π) β£ π₯ β π΄}, β, < ))π΅)) |
58 | 57 | eleq2d 2813 |
. . . . . . 7
β’ (π = inf({π β (1..^π) β£ π₯ β π΄}, β, < ) β (π₯ β (β¦π / πβ¦π΄ β βͺ
π β (1..^π)π΅) β π₯ β (β¦inf({π β (1..^π) β£ π₯ β π΄}, β, < ) / πβ¦π΄ β βͺ
π β (1..^inf({π β (1..^π) β£ π₯ β π΄}, β, < ))π΅))) |
59 | 58 | rspcev 3606 |
. . . . . 6
β’
((inf({π β
(1..^π) β£ π₯ β π΄}, β, < ) β (1..^π) β§ π₯ β (β¦inf({π β (1..^π) β£ π₯ β π΄}, β, < ) / πβ¦π΄ β βͺ
π β (1..^inf({π β (1..^π) β£ π₯ β π΄}, β, < ))π΅)) β βπ β (1..^π)π₯ β (β¦π / πβ¦π΄ β βͺ
π β (1..^π)π΅)) |
60 | 10, 53, 59 | syl2anc 583 |
. . . . 5
β’
(βπ β
(1..^π)π₯ β π΄ β βπ β (1..^π)π₯ β (β¦π / πβ¦π΄ β βͺ
π β (1..^π)π΅)) |
61 | | nfv 1909 |
. . . . . 6
β’
β²π π₯ β (π΄ β βͺ
π β (1..^π)π΅) |
62 | | nfcsb1v 3913 |
. . . . . . . 8
β’
β²πβ¦π / πβ¦π΄ |
63 | | nfcv 2897 |
. . . . . . . . 9
β’
β²π(1..^π) |
64 | 63, 39 | nfiun 5020 |
. . . . . . . 8
β’
β²πβͺ π β (1..^π)π΅ |
65 | 62, 64 | nfdif 4120 |
. . . . . . 7
β’
β²π(β¦π / πβ¦π΄ β βͺ
π β (1..^π)π΅) |
66 | 65 | nfcri 2884 |
. . . . . 6
β’
β²π π₯ β (β¦π / πβ¦π΄ β βͺ
π β (1..^π)π΅) |
67 | | csbeq1a 3902 |
. . . . . . . 8
β’ (π = π β π΄ = β¦π / πβ¦π΄) |
68 | | oveq2 7413 |
. . . . . . . . 9
β’ (π = π β (1..^π) = (1..^π)) |
69 | 68 | iuneq1d 5017 |
. . . . . . . 8
β’ (π = π β βͺ
π β (1..^π)π΅ = βͺ π β (1..^π)π΅) |
70 | 67, 69 | difeq12d 4118 |
. . . . . . 7
β’ (π = π β (π΄ β βͺ
π β (1..^π)π΅) = (β¦π / πβ¦π΄ β βͺ
π β (1..^π)π΅)) |
71 | 70 | eleq2d 2813 |
. . . . . 6
β’ (π = π β (π₯ β (π΄ β βͺ
π β (1..^π)π΅) β π₯ β (β¦π / πβ¦π΄ β βͺ
π β (1..^π)π΅))) |
72 | 61, 66, 71 | cbvrexw 3298 |
. . . . 5
β’
(βπ β
(1..^π)π₯ β (π΄ β βͺ
π β (1..^π)π΅) β βπ β (1..^π)π₯ β (β¦π / πβ¦π΄ β βͺ
π β (1..^π)π΅)) |
73 | 60, 72 | sylibr 233 |
. . . 4
β’
(βπ β
(1..^π)π₯ β π΄ β βπ β (1..^π)π₯ β (π΄ β βͺ
π β (1..^π)π΅)) |
74 | | eldifi 4121 |
. . . . 5
β’ (π₯ β (π΄ β βͺ
π β (1..^π)π΅) β π₯ β π΄) |
75 | 74 | reximi 3078 |
. . . 4
β’
(βπ β
(1..^π)π₯ β (π΄ β βͺ
π β (1..^π)π΅) β βπ β (1..^π)π₯ β π΄) |
76 | 73, 75 | impbii 208 |
. . 3
β’
(βπ β
(1..^π)π₯ β π΄ β βπ β (1..^π)π₯ β (π΄ β βͺ
π β (1..^π)π΅)) |
77 | | eliun 4994 |
. . 3
β’ (π₯ β βͺ π β (1..^π)π΄ β βπ β (1..^π)π₯ β π΄) |
78 | | eliun 4994 |
. . 3
β’ (π₯ β βͺ π β (1..^π)(π΄ β βͺ
π β (1..^π)π΅) β βπ β (1..^π)π₯ β (π΄ β βͺ
π β (1..^π)π΅)) |
79 | 76, 77, 78 | 3bitr4i 303 |
. 2
β’ (π₯ β βͺ π β (1..^π)π΄ β π₯ β βͺ
π β (1..^π)(π΄ β βͺ
π β (1..^π)π΅)) |
80 | 79 | eqriv 2723 |
1
β’ βͺ π β (1..^π)π΄ = βͺ π β (1..^π)(π΄ β βͺ
π β (1..^π)π΅) |