Step | Hyp | Ref
| Expression |
1 | | eqid 2736 |
. . . 4
β’
(β€β₯βπ) = (β€β₯βπ) |
2 | | simpr 485 |
. . . 4
β’ ((π΄ β
(β€β₯βπ) β§ π β β€) β π β β€) |
3 | | ax-1ne0 11116 |
. . . . 5
β’ 1 β
0 |
4 | 3 | a1i 11 |
. . . 4
β’ ((π΄ β
(β€β₯βπ) β§ π β β€) β 1 β
0) |
5 | 1 | prodfclim1 15770 |
. . . . 5
β’ (π β β€ β seqπ( Β· ,
((β€β₯βπ) Γ {1})) β 1) |
6 | 5 | adantl 482 |
. . . 4
β’ ((π΄ β
(β€β₯βπ) β§ π β β€) β seqπ( Β· ,
((β€β₯βπ) Γ {1})) β 1) |
7 | | simpl 483 |
. . . 4
β’ ((π΄ β
(β€β₯βπ) β§ π β β€) β π΄ β (β€β₯βπ)) |
8 | | 1ex 11147 |
. . . . . . 7
β’ 1 β
V |
9 | 8 | fvconst2 7149 |
. . . . . 6
β’ (π β
(β€β₯βπ) β
(((β€β₯βπ) Γ {1})βπ) = 1) |
10 | | ifid 4524 |
. . . . . 6
β’ if(π β π΄, 1, 1) = 1 |
11 | 9, 10 | eqtr4di 2794 |
. . . . 5
β’ (π β
(β€β₯βπ) β
(((β€β₯βπ) Γ {1})βπ) = if(π β π΄, 1, 1)) |
12 | 11 | adantl 482 |
. . . 4
β’ (((π΄ β
(β€β₯βπ) β§ π β β€) β§ π β (β€β₯βπ)) β
(((β€β₯βπ) Γ {1})βπ) = if(π β π΄, 1, 1)) |
13 | | 1cnd 11146 |
. . . 4
β’ (((π΄ β
(β€β₯βπ) β§ π β β€) β§ π β π΄) β 1 β β) |
14 | 1, 2, 4, 6, 7, 12,
13 | zprodn0 15814 |
. . 3
β’ ((π΄ β
(β€β₯βπ) β§ π β β€) β βπ β π΄ 1 = 1) |
15 | | uzf 12762 |
. . . . . . . . 9
β’
β€β₯:β€βΆπ« β€ |
16 | 15 | fdmi 6677 |
. . . . . . . 8
β’ dom
β€β₯ = β€ |
17 | 16 | eleq2i 2829 |
. . . . . . 7
β’ (π β dom
β€β₯ β π β β€) |
18 | | ndmfv 6874 |
. . . . . . 7
β’ (Β¬
π β dom
β€β₯ β (β€β₯βπ) = β
) |
19 | 17, 18 | sylnbir 330 |
. . . . . 6
β’ (Β¬
π β β€ β
(β€β₯βπ) = β
) |
20 | 19 | sseq2d 3974 |
. . . . 5
β’ (Β¬
π β β€ β
(π΄ β
(β€β₯βπ) β π΄ β β
)) |
21 | 20 | biimpac 479 |
. . . 4
β’ ((π΄ β
(β€β₯βπ) β§ Β¬ π β β€) β π΄ β β
) |
22 | | ss0 4356 |
. . . 4
β’ (π΄ β β
β π΄ = β
) |
23 | | prodeq1 15784 |
. . . . 5
β’ (π΄ = β
β βπ β π΄ 1 = βπ β β
1) |
24 | | prod0 15818 |
. . . . 5
β’
βπ β
β
1 = 1 |
25 | 23, 24 | eqtrdi 2792 |
. . . 4
β’ (π΄ = β
β βπ β π΄ 1 = 1) |
26 | 21, 22, 25 | 3syl 18 |
. . 3
β’ ((π΄ β
(β€β₯βπ) β§ Β¬ π β β€) β βπ β π΄ 1 = 1) |
27 | 14, 26 | pm2.61dan 811 |
. 2
β’ (π΄ β
(β€β₯βπ) β βπ β π΄ 1 = 1) |
28 | | fz1f1o 15587 |
. . 3
β’ (π΄ β Fin β (π΄ = β
β¨
((β―βπ΄) β
β β§ βπ
π:(1...(β―βπ΄))β1-1-ontoβπ΄))) |
29 | | eqidd 2737 |
. . . . . . . . 9
β’ (π = (πβπ) β 1 = 1) |
30 | | simpl 483 |
. . . . . . . . 9
β’
(((β―βπ΄)
β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄) β (β―βπ΄) β
β) |
31 | | simpr 485 |
. . . . . . . . 9
β’
(((β―βπ΄)
β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄) β π:(1...(β―βπ΄))β1-1-ontoβπ΄) |
32 | | 1cnd 11146 |
. . . . . . . . 9
β’
((((β―βπ΄)
β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄) β§ π β π΄) β 1 β β) |
33 | | elfznn 13462 |
. . . . . . . . . . 11
β’ (π β
(1...(β―βπ΄))
β π β
β) |
34 | 8 | fvconst2 7149 |
. . . . . . . . . . 11
β’ (π β β β ((β
Γ {1})βπ) =
1) |
35 | 33, 34 | syl 17 |
. . . . . . . . . 10
β’ (π β
(1...(β―βπ΄))
β ((β Γ {1})βπ) = 1) |
36 | 35 | adantl 482 |
. . . . . . . . 9
β’
((((β―βπ΄)
β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄) β§ π β (1...(β―βπ΄))) β ((β Γ
{1})βπ) =
1) |
37 | 29, 30, 31, 32, 36 | fprod 15816 |
. . . . . . . 8
β’
(((β―βπ΄)
β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄) β βπ β π΄ 1 = (seq1( Β· , (β Γ
{1}))β(β―βπ΄))) |
38 | | nnuz 12798 |
. . . . . . . . . 10
β’ β =
(β€β₯β1) |
39 | 38 | prodf1 15768 |
. . . . . . . . 9
β’
((β―βπ΄)
β β β (seq1( Β· , (β Γ
{1}))β(β―βπ΄)) = 1) |
40 | 39 | adantr 481 |
. . . . . . . 8
β’
(((β―βπ΄)
β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄) β (seq1( Β· ,
(β Γ {1}))β(β―βπ΄)) = 1) |
41 | 37, 40 | eqtrd 2776 |
. . . . . . 7
β’
(((β―βπ΄)
β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄) β βπ β π΄ 1 = 1) |
42 | 41 | ex 413 |
. . . . . 6
β’
((β―βπ΄)
β β β (π:(1...(β―βπ΄))β1-1-ontoβπ΄ β βπ β π΄ 1 = 1)) |
43 | 42 | exlimdv 1936 |
. . . . 5
β’
((β―βπ΄)
β β β (βπ π:(1...(β―βπ΄))β1-1-ontoβπ΄ β βπ β π΄ 1 = 1)) |
44 | 43 | imp 407 |
. . . 4
β’
(((β―βπ΄)
β β β§ βπ π:(1...(β―βπ΄))β1-1-ontoβπ΄) β βπ β π΄ 1 = 1) |
45 | 25, 44 | jaoi 855 |
. . 3
β’ ((π΄ = β
β¨
((β―βπ΄) β
β β§ βπ
π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β βπ β π΄ 1 = 1) |
46 | 28, 45 | syl 17 |
. 2
β’ (π΄ β Fin β βπ β π΄ 1 = 1) |
47 | 27, 46 | jaoi 855 |
1
β’ ((π΄ β
(β€β₯βπ) β¨ π΄ β Fin) β βπ β π΄ 1 = 1) |