Step | Hyp | Ref
| Expression |
1 | | prodeq1 15797 |
. . . . 5
β’ (π΄ = β
β βπ β π΄ π΅ = βπ β β
π΅) |
2 | | prod0 15831 |
. . . . 5
β’
βπ β
β
π΅ =
1 |
3 | 1, 2 | eqtrdi 2789 |
. . . 4
β’ (π΄ = β
β βπ β π΄ π΅ = 1) |
4 | | ax-1ne0 11125 |
. . . . 5
β’ 1 β
0 |
5 | 4 | a1i 11 |
. . . 4
β’ (π΄ = β
β 1 β
0) |
6 | 3, 5 | eqnetrd 3008 |
. . 3
β’ (π΄ = β
β βπ β π΄ π΅ β 0) |
7 | 6 | a1i 11 |
. 2
β’ (π β (π΄ = β
β βπ β π΄ π΅ β 0)) |
8 | | prodfc 15833 |
. . . . . . 7
β’
βπ β
π΄ ((π β π΄ β¦ π΅)βπ) = βπ β π΄ π΅ |
9 | | fveq2 6843 |
. . . . . . . 8
β’ (π = (πβπ) β ((π β π΄ β¦ π΅)βπ) = ((π β π΄ β¦ π΅)β(πβπ))) |
10 | | simprl 770 |
. . . . . . . 8
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (β―βπ΄) β
β) |
11 | | simprr 772 |
. . . . . . . 8
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β π:(1...(β―βπ΄))β1-1-ontoβπ΄) |
12 | | fprodn0.2 |
. . . . . . . . . . 11
β’ ((π β§ π β π΄) β π΅ β β) |
13 | 12 | fmpttd 7064 |
. . . . . . . . . 10
β’ (π β (π β π΄ β¦ π΅):π΄βΆβ) |
14 | 13 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (π β π΄ β¦ π΅):π΄βΆβ) |
15 | 14 | ffvelcdmda 7036 |
. . . . . . . 8
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β π΄) β ((π β π΄ β¦ π΅)βπ) β β) |
16 | | f1of 6785 |
. . . . . . . . . 10
β’ (π:(1...(β―βπ΄))β1-1-ontoβπ΄ β π:(1...(β―βπ΄))βΆπ΄) |
17 | 11, 16 | syl 17 |
. . . . . . . . 9
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β π:(1...(β―βπ΄))βΆπ΄) |
18 | | fvco3 6941 |
. . . . . . . . 9
β’ ((π:(1...(β―βπ΄))βΆπ΄ β§ π β (1...(β―βπ΄))) β (((π β π΄ β¦ π΅) β π)βπ) = ((π β π΄ β¦ π΅)β(πβπ))) |
19 | 17, 18 | sylan 581 |
. . . . . . . 8
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (1...(β―βπ΄))) β (((π β π΄ β¦ π΅) β π)βπ) = ((π β π΄ β¦ π΅)β(πβπ))) |
20 | 9, 10, 11, 15, 19 | fprod 15829 |
. . . . . . 7
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β βπ β π΄ ((π β π΄ β¦ π΅)βπ) = (seq1( Β· , ((π β π΄ β¦ π΅) β π))β(β―βπ΄))) |
21 | 8, 20 | eqtr3id 2787 |
. . . . . 6
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β βπ β π΄ π΅ = (seq1( Β· , ((π β π΄ β¦ π΅) β π))β(β―βπ΄))) |
22 | | nnuz 12811 |
. . . . . . . 8
β’ β =
(β€β₯β1) |
23 | 10, 22 | eleqtrdi 2844 |
. . . . . . 7
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (β―βπ΄) β
(β€β₯β1)) |
24 | | fco 6693 |
. . . . . . . . 9
β’ (((π β π΄ β¦ π΅):π΄βΆβ β§ π:(1...(β―βπ΄))βΆπ΄) β ((π β π΄ β¦ π΅) β π):(1...(β―βπ΄))βΆβ) |
25 | 14, 17, 24 | syl2anc 585 |
. . . . . . . 8
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β ((π β π΄ β¦ π΅) β π):(1...(β―βπ΄))βΆβ) |
26 | 25 | ffvelcdmda 7036 |
. . . . . . 7
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (1...(β―βπ΄))) β (((π β π΄ β¦ π΅) β π)βπ) β β) |
27 | | fvco3 6941 |
. . . . . . . . 9
β’ ((π:(1...(β―βπ΄))βΆπ΄ β§ π β (1...(β―βπ΄))) β (((π β π΄ β¦ π΅) β π)βπ) = ((π β π΄ β¦ π΅)β(πβπ))) |
28 | 17, 27 | sylan 581 |
. . . . . . . 8
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (1...(β―βπ΄))) β (((π β π΄ β¦ π΅) β π)βπ) = ((π β π΄ β¦ π΅)β(πβπ))) |
29 | 16 | ffvelcdmda 7036 |
. . . . . . . . . . 11
β’ ((π:(1...(β―βπ΄))β1-1-ontoβπ΄ β§ π β (1...(β―βπ΄))) β (πβπ) β π΄) |
30 | 29 | adantll 713 |
. . . . . . . . . 10
β’
((((β―βπ΄)
β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄) β§ π β (1...(β―βπ΄))) β (πβπ) β π΄) |
31 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((π β§ (πβπ) β π΄) β (πβπ) β π΄) |
32 | | nfcv 2904 |
. . . . . . . . . . . . . 14
β’
β²π(πβπ) |
33 | | nfv 1918 |
. . . . . . . . . . . . . . 15
β’
β²ππ |
34 | | nfcsb1v 3881 |
. . . . . . . . . . . . . . . 16
β’
β²πβ¦(πβπ) / πβ¦π΅ |
35 | 34 | nfel1 2920 |
. . . . . . . . . . . . . . 15
β’
β²πβ¦(πβπ) / πβ¦π΅ β β |
36 | 33, 35 | nfim 1900 |
. . . . . . . . . . . . . 14
β’
β²π(π β β¦(πβπ) / πβ¦π΅ β β) |
37 | | csbeq1a 3870 |
. . . . . . . . . . . . . . . 16
β’ (π = (πβπ) β π΅ = β¦(πβπ) / πβ¦π΅) |
38 | 37 | eleq1d 2819 |
. . . . . . . . . . . . . . 15
β’ (π = (πβπ) β (π΅ β β β β¦(πβπ) / πβ¦π΅ β β)) |
39 | 38 | imbi2d 341 |
. . . . . . . . . . . . . 14
β’ (π = (πβπ) β ((π β π΅ β β) β (π β β¦(πβπ) / πβ¦π΅ β β))) |
40 | 12 | expcom 415 |
. . . . . . . . . . . . . 14
β’ (π β π΄ β (π β π΅ β β)) |
41 | 32, 36, 39, 40 | vtoclgaf 3532 |
. . . . . . . . . . . . 13
β’ ((πβπ) β π΄ β (π β β¦(πβπ) / πβ¦π΅ β β)) |
42 | 41 | impcom 409 |
. . . . . . . . . . . 12
β’ ((π β§ (πβπ) β π΄) β β¦(πβπ) / πβ¦π΅ β β) |
43 | | eqid 2733 |
. . . . . . . . . . . . 13
β’ (π β π΄ β¦ π΅) = (π β π΄ β¦ π΅) |
44 | 43 | fvmpts 6952 |
. . . . . . . . . . . 12
β’ (((πβπ) β π΄ β§ β¦(πβπ) / πβ¦π΅ β β) β ((π β π΄ β¦ π΅)β(πβπ)) = β¦(πβπ) / πβ¦π΅) |
45 | 31, 42, 44 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((π β§ (πβπ) β π΄) β ((π β π΄ β¦ π΅)β(πβπ)) = β¦(πβπ) / πβ¦π΅) |
46 | | nfcv 2904 |
. . . . . . . . . . . . . . 15
β’
β²π0 |
47 | 34, 46 | nfne 3042 |
. . . . . . . . . . . . . 14
β’
β²πβ¦(πβπ) / πβ¦π΅ β 0 |
48 | 33, 47 | nfim 1900 |
. . . . . . . . . . . . 13
β’
β²π(π β β¦(πβπ) / πβ¦π΅ β 0) |
49 | 37 | neeq1d 3000 |
. . . . . . . . . . . . . 14
β’ (π = (πβπ) β (π΅ β 0 β β¦(πβπ) / πβ¦π΅ β 0)) |
50 | 49 | imbi2d 341 |
. . . . . . . . . . . . 13
β’ (π = (πβπ) β ((π β π΅ β 0) β (π β β¦(πβπ) / πβ¦π΅ β 0))) |
51 | | fprodn0.3 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π΄) β π΅ β 0) |
52 | 51 | expcom 415 |
. . . . . . . . . . . . 13
β’ (π β π΄ β (π β π΅ β 0)) |
53 | 32, 48, 50, 52 | vtoclgaf 3532 |
. . . . . . . . . . . 12
β’ ((πβπ) β π΄ β (π β β¦(πβπ) / πβ¦π΅ β 0)) |
54 | 53 | impcom 409 |
. . . . . . . . . . 11
β’ ((π β§ (πβπ) β π΄) β β¦(πβπ) / πβ¦π΅ β 0) |
55 | 45, 54 | eqnetrd 3008 |
. . . . . . . . . 10
β’ ((π β§ (πβπ) β π΄) β ((π β π΄ β¦ π΅)β(πβπ)) β 0) |
56 | 30, 55 | sylan2 594 |
. . . . . . . . 9
β’ ((π β§ (((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄) β§ π β (1...(β―βπ΄)))) β ((π β π΄ β¦ π΅)β(πβπ)) β 0) |
57 | 56 | anassrs 469 |
. . . . . . . 8
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (1...(β―βπ΄))) β ((π β π΄ β¦ π΅)β(πβπ)) β 0) |
58 | 28, 57 | eqnetrd 3008 |
. . . . . . 7
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (1...(β―βπ΄))) β (((π β π΄ β¦ π΅) β π)βπ) β 0) |
59 | 23, 26, 58 | prodfn0 15784 |
. . . . . 6
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (seq1( Β· ,
((π β π΄ β¦ π΅) β π))β(β―βπ΄)) β 0) |
60 | 21, 59 | eqnetrd 3008 |
. . . . 5
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β βπ β π΄ π΅ β 0) |
61 | 60 | expr 458 |
. . . 4
β’ ((π β§ (β―βπ΄) β β) β (π:(1...(β―βπ΄))β1-1-ontoβπ΄ β βπ β π΄ π΅ β 0)) |
62 | 61 | exlimdv 1937 |
. . 3
β’ ((π β§ (β―βπ΄) β β) β
(βπ π:(1...(β―βπ΄))β1-1-ontoβπ΄ β βπ β π΄ π΅ β 0)) |
63 | 62 | expimpd 455 |
. 2
β’ (π β (((β―βπ΄) β β β§
βπ π:(1...(β―βπ΄))β1-1-ontoβπ΄) β βπ β π΄ π΅ β 0)) |
64 | | fprodn0.1 |
. . 3
β’ (π β π΄ β Fin) |
65 | | fz1f1o 15600 |
. . 3
β’ (π΄ β Fin β (π΄ = β
β¨
((β―βπ΄) β
β β§ βπ
π:(1...(β―βπ΄))β1-1-ontoβπ΄))) |
66 | 64, 65 | syl 17 |
. 2
β’ (π β (π΄ = β
β¨ ((β―βπ΄) β β β§
βπ π:(1...(β―βπ΄))β1-1-ontoβπ΄))) |
67 | 7, 63, 66 | mpjaod 859 |
1
β’ (π β βπ β π΄ π΅ β 0) |