Step | Hyp | Ref
| Expression |
1 | | prodeq1 15857 |
. . . . 5
β’ (π΄ = β
β βπ β π΄ π΅ = βπ β β
π΅) |
2 | | prod0 15891 |
. . . . 5
β’
βπ β
β
π΅ =
1 |
3 | 1, 2 | eqtrdi 2786 |
. . . 4
β’ (π΄ = β
β βπ β π΄ π΅ = 1) |
4 | | ax-1ne0 11181 |
. . . . 5
β’ 1 β
0 |
5 | 4 | a1i 11 |
. . . 4
β’ (π΄ = β
β 1 β
0) |
6 | 3, 5 | eqnetrd 3006 |
. . 3
β’ (π΄ = β
β βπ β π΄ π΅ β 0) |
7 | 6 | a1i 11 |
. 2
β’ (π β (π΄ = β
β βπ β π΄ π΅ β 0)) |
8 | | prodfc 15893 |
. . . . . . 7
β’
βπ β
π΄ ((π β π΄ β¦ π΅)βπ) = βπ β π΄ π΅ |
9 | | fveq2 6890 |
. . . . . . . 8
β’ (π = (πβπ) β ((π β π΄ β¦ π΅)βπ) = ((π β π΄ β¦ π΅)β(πβπ))) |
10 | | simprl 767 |
. . . . . . . 8
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (β―βπ΄) β
β) |
11 | | simprr 769 |
. . . . . . . 8
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β π:(1...(β―βπ΄))β1-1-ontoβπ΄) |
12 | | fprodn0.2 |
. . . . . . . . . . 11
β’ ((π β§ π β π΄) β π΅ β β) |
13 | 12 | fmpttd 7115 |
. . . . . . . . . 10
β’ (π β (π β π΄ β¦ π΅):π΄βΆβ) |
14 | 13 | adantr 479 |
. . . . . . . . 9
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (π β π΄ β¦ π΅):π΄βΆβ) |
15 | 14 | ffvelcdmda 7085 |
. . . . . . . 8
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β π΄) β ((π β π΄ β¦ π΅)βπ) β β) |
16 | | f1of 6832 |
. . . . . . . . . 10
β’ (π:(1...(β―βπ΄))β1-1-ontoβπ΄ β π:(1...(β―βπ΄))βΆπ΄) |
17 | 11, 16 | syl 17 |
. . . . . . . . 9
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β π:(1...(β―βπ΄))βΆπ΄) |
18 | | fvco3 6989 |
. . . . . . . . 9
β’ ((π:(1...(β―βπ΄))βΆπ΄ β§ π β (1...(β―βπ΄))) β (((π β π΄ β¦ π΅) β π)βπ) = ((π β π΄ β¦ π΅)β(πβπ))) |
19 | 17, 18 | sylan 578 |
. . . . . . . 8
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (1...(β―βπ΄))) β (((π β π΄ β¦ π΅) β π)βπ) = ((π β π΄ β¦ π΅)β(πβπ))) |
20 | 9, 10, 11, 15, 19 | fprod 15889 |
. . . . . . 7
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β βπ β π΄ ((π β π΄ β¦ π΅)βπ) = (seq1( Β· , ((π β π΄ β¦ π΅) β π))β(β―βπ΄))) |
21 | 8, 20 | eqtr3id 2784 |
. . . . . 6
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β βπ β π΄ π΅ = (seq1( Β· , ((π β π΄ β¦ π΅) β π))β(β―βπ΄))) |
22 | | nnuz 12869 |
. . . . . . . 8
β’ β =
(β€β₯β1) |
23 | 10, 22 | eleqtrdi 2841 |
. . . . . . 7
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (β―βπ΄) β
(β€β₯β1)) |
24 | | fco 6740 |
. . . . . . . . 9
β’ (((π β π΄ β¦ π΅):π΄βΆβ β§ π:(1...(β―βπ΄))βΆπ΄) β ((π β π΄ β¦ π΅) β π):(1...(β―βπ΄))βΆβ) |
25 | 14, 17, 24 | syl2anc 582 |
. . . . . . . 8
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β ((π β π΄ β¦ π΅) β π):(1...(β―βπ΄))βΆβ) |
26 | 25 | ffvelcdmda 7085 |
. . . . . . 7
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (1...(β―βπ΄))) β (((π β π΄ β¦ π΅) β π)βπ) β β) |
27 | | fvco3 6989 |
. . . . . . . . 9
β’ ((π:(1...(β―βπ΄))βΆπ΄ β§ π β (1...(β―βπ΄))) β (((π β π΄ β¦ π΅) β π)βπ) = ((π β π΄ β¦ π΅)β(πβπ))) |
28 | 17, 27 | sylan 578 |
. . . . . . . 8
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (1...(β―βπ΄))) β (((π β π΄ β¦ π΅) β π)βπ) = ((π β π΄ β¦ π΅)β(πβπ))) |
29 | 16 | ffvelcdmda 7085 |
. . . . . . . . . . 11
β’ ((π:(1...(β―βπ΄))β1-1-ontoβπ΄ β§ π β (1...(β―βπ΄))) β (πβπ) β π΄) |
30 | 29 | adantll 710 |
. . . . . . . . . 10
β’
((((β―βπ΄)
β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄) β§ π β (1...(β―βπ΄))) β (πβπ) β π΄) |
31 | | simpr 483 |
. . . . . . . . . . . 12
β’ ((π β§ (πβπ) β π΄) β (πβπ) β π΄) |
32 | | nfcv 2901 |
. . . . . . . . . . . . . 14
β’
β²π(πβπ) |
33 | | nfv 1915 |
. . . . . . . . . . . . . . 15
β’
β²ππ |
34 | | nfcsb1v 3917 |
. . . . . . . . . . . . . . . 16
β’
β²πβ¦(πβπ) / πβ¦π΅ |
35 | 34 | nfel1 2917 |
. . . . . . . . . . . . . . 15
β’
β²πβ¦(πβπ) / πβ¦π΅ β β |
36 | 33, 35 | nfim 1897 |
. . . . . . . . . . . . . 14
β’
β²π(π β β¦(πβπ) / πβ¦π΅ β β) |
37 | | csbeq1a 3906 |
. . . . . . . . . . . . . . . 16
β’ (π = (πβπ) β π΅ = β¦(πβπ) / πβ¦π΅) |
38 | 37 | eleq1d 2816 |
. . . . . . . . . . . . . . 15
β’ (π = (πβπ) β (π΅ β β β β¦(πβπ) / πβ¦π΅ β β)) |
39 | 38 | imbi2d 339 |
. . . . . . . . . . . . . 14
β’ (π = (πβπ) β ((π β π΅ β β) β (π β β¦(πβπ) / πβ¦π΅ β β))) |
40 | 12 | expcom 412 |
. . . . . . . . . . . . . 14
β’ (π β π΄ β (π β π΅ β β)) |
41 | 32, 36, 39, 40 | vtoclgaf 3564 |
. . . . . . . . . . . . 13
β’ ((πβπ) β π΄ β (π β β¦(πβπ) / πβ¦π΅ β β)) |
42 | 41 | impcom 406 |
. . . . . . . . . . . 12
β’ ((π β§ (πβπ) β π΄) β β¦(πβπ) / πβ¦π΅ β β) |
43 | | eqid 2730 |
. . . . . . . . . . . . 13
β’ (π β π΄ β¦ π΅) = (π β π΄ β¦ π΅) |
44 | 43 | fvmpts 7000 |
. . . . . . . . . . . 12
β’ (((πβπ) β π΄ β§ β¦(πβπ) / πβ¦π΅ β β) β ((π β π΄ β¦ π΅)β(πβπ)) = β¦(πβπ) / πβ¦π΅) |
45 | 31, 42, 44 | syl2anc 582 |
. . . . . . . . . . 11
β’ ((π β§ (πβπ) β π΄) β ((π β π΄ β¦ π΅)β(πβπ)) = β¦(πβπ) / πβ¦π΅) |
46 | | nfcv 2901 |
. . . . . . . . . . . . . . 15
β’
β²π0 |
47 | 34, 46 | nfne 3041 |
. . . . . . . . . . . . . 14
β’
β²πβ¦(πβπ) / πβ¦π΅ β 0 |
48 | 33, 47 | nfim 1897 |
. . . . . . . . . . . . 13
β’
β²π(π β β¦(πβπ) / πβ¦π΅ β 0) |
49 | 37 | neeq1d 2998 |
. . . . . . . . . . . . . 14
β’ (π = (πβπ) β (π΅ β 0 β β¦(πβπ) / πβ¦π΅ β 0)) |
50 | 49 | imbi2d 339 |
. . . . . . . . . . . . 13
β’ (π = (πβπ) β ((π β π΅ β 0) β (π β β¦(πβπ) / πβ¦π΅ β 0))) |
51 | | fprodn0.3 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π΄) β π΅ β 0) |
52 | 51 | expcom 412 |
. . . . . . . . . . . . 13
β’ (π β π΄ β (π β π΅ β 0)) |
53 | 32, 48, 50, 52 | vtoclgaf 3564 |
. . . . . . . . . . . 12
β’ ((πβπ) β π΄ β (π β β¦(πβπ) / πβ¦π΅ β 0)) |
54 | 53 | impcom 406 |
. . . . . . . . . . 11
β’ ((π β§ (πβπ) β π΄) β β¦(πβπ) / πβ¦π΅ β 0) |
55 | 45, 54 | eqnetrd 3006 |
. . . . . . . . . 10
β’ ((π β§ (πβπ) β π΄) β ((π β π΄ β¦ π΅)β(πβπ)) β 0) |
56 | 30, 55 | sylan2 591 |
. . . . . . . . 9
β’ ((π β§ (((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄) β§ π β (1...(β―βπ΄)))) β ((π β π΄ β¦ π΅)β(πβπ)) β 0) |
57 | 56 | anassrs 466 |
. . . . . . . 8
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (1...(β―βπ΄))) β ((π β π΄ β¦ π΅)β(πβπ)) β 0) |
58 | 28, 57 | eqnetrd 3006 |
. . . . . . 7
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (1...(β―βπ΄))) β (((π β π΄ β¦ π΅) β π)βπ) β 0) |
59 | 23, 26, 58 | prodfn0 15844 |
. . . . . 6
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (seq1( Β· ,
((π β π΄ β¦ π΅) β π))β(β―βπ΄)) β 0) |
60 | 21, 59 | eqnetrd 3006 |
. . . . 5
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β βπ β π΄ π΅ β 0) |
61 | 60 | expr 455 |
. . . 4
β’ ((π β§ (β―βπ΄) β β) β (π:(1...(β―βπ΄))β1-1-ontoβπ΄ β βπ β π΄ π΅ β 0)) |
62 | 61 | exlimdv 1934 |
. . 3
β’ ((π β§ (β―βπ΄) β β) β
(βπ π:(1...(β―βπ΄))β1-1-ontoβπ΄ β βπ β π΄ π΅ β 0)) |
63 | 62 | expimpd 452 |
. 2
β’ (π β (((β―βπ΄) β β β§
βπ π:(1...(β―βπ΄))β1-1-ontoβπ΄) β βπ β π΄ π΅ β 0)) |
64 | | fprodn0.1 |
. . 3
β’ (π β π΄ β Fin) |
65 | | fz1f1o 15660 |
. . 3
β’ (π΄ β Fin β (π΄ = β
β¨
((β―βπ΄) β
β β§ βπ
π:(1...(β―βπ΄))β1-1-ontoβπ΄))) |
66 | 64, 65 | syl 17 |
. 2
β’ (π β (π΄ = β
β¨ ((β―βπ΄) β β β§
βπ π:(1...(β―βπ΄))β1-1-ontoβπ΄))) |
67 | 7, 63, 66 | mpjaod 856 |
1
β’ (π β βπ β π΄ π΅ β 0) |