Step | Hyp | Ref
| Expression |
1 | | 1div1e1 11850 |
. . . . 5
β’ (1 / 1) =
1 |
2 | 1 | eqcomi 2742 |
. . . 4
β’ 1 = (1 /
1) |
3 | | prodeq1 15797 |
. . . . 5
β’ (π΄ = β
β βπ β π΄ (π΅ / πΆ) = βπ β β
(π΅ / πΆ)) |
4 | | prod0 15831 |
. . . . 5
β’
βπ β
β
(π΅ / πΆ) = 1 |
5 | 3, 4 | eqtrdi 2789 |
. . . 4
β’ (π΄ = β
β βπ β π΄ (π΅ / πΆ) = 1) |
6 | | prodeq1 15797 |
. . . . . 6
β’ (π΄ = β
β βπ β π΄ π΅ = βπ β β
π΅) |
7 | | prod0 15831 |
. . . . . 6
β’
βπ β
β
π΅ =
1 |
8 | 6, 7 | eqtrdi 2789 |
. . . . 5
β’ (π΄ = β
β βπ β π΄ π΅ = 1) |
9 | | prodeq1 15797 |
. . . . . 6
β’ (π΄ = β
β βπ β π΄ πΆ = βπ β β
πΆ) |
10 | | prod0 15831 |
. . . . . 6
β’
βπ β
β
πΆ =
1 |
11 | 9, 10 | eqtrdi 2789 |
. . . . 5
β’ (π΄ = β
β βπ β π΄ πΆ = 1) |
12 | 8, 11 | oveq12d 7376 |
. . . 4
β’ (π΄ = β
β (βπ β π΄ π΅ / βπ β π΄ πΆ) = (1 / 1)) |
13 | 2, 5, 12 | 3eqtr4a 2799 |
. . 3
β’ (π΄ = β
β βπ β π΄ (π΅ / πΆ) = (βπ β π΄ π΅ / βπ β π΄ πΆ)) |
14 | 13 | a1i 11 |
. 2
β’ (π β (π΄ = β
β βπ β π΄ (π΅ / πΆ) = (βπ β π΄ π΅ / βπ β π΄ πΆ))) |
15 | | simprl 770 |
. . . . . . . . 9
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (β―βπ΄) β
β) |
16 | | nnuz 12811 |
. . . . . . . . 9
β’ β =
(β€β₯β1) |
17 | 15, 16 | eleqtrdi 2844 |
. . . . . . . 8
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (β―βπ΄) β
(β€β₯β1)) |
18 | | fprodmul.2 |
. . . . . . . . . . 11
β’ ((π β§ π β π΄) β π΅ β β) |
19 | 18 | fmpttd 7064 |
. . . . . . . . . 10
β’ (π β (π β π΄ β¦ π΅):π΄βΆβ) |
20 | | f1of 6785 |
. . . . . . . . . . 11
β’ (π:(1...(β―βπ΄))β1-1-ontoβπ΄ β π:(1...(β―βπ΄))βΆπ΄) |
21 | 20 | adantl 483 |
. . . . . . . . . 10
β’
(((β―βπ΄)
β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄) β π:(1...(β―βπ΄))βΆπ΄) |
22 | | fco 6693 |
. . . . . . . . . 10
β’ (((π β π΄ β¦ π΅):π΄βΆβ β§ π:(1...(β―βπ΄))βΆπ΄) β ((π β π΄ β¦ π΅) β π):(1...(β―βπ΄))βΆβ) |
23 | 19, 21, 22 | syl2an 597 |
. . . . . . . . 9
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β ((π β π΄ β¦ π΅) β π):(1...(β―βπ΄))βΆβ) |
24 | 23 | ffvelcdmda 7036 |
. . . . . . . 8
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (1...(β―βπ΄))) β (((π β π΄ β¦ π΅) β π)βπ) β β) |
25 | | fprodmul.3 |
. . . . . . . . . . 11
β’ ((π β§ π β π΄) β πΆ β β) |
26 | 25 | fmpttd 7064 |
. . . . . . . . . 10
β’ (π β (π β π΄ β¦ πΆ):π΄βΆβ) |
27 | | fco 6693 |
. . . . . . . . . 10
β’ (((π β π΄ β¦ πΆ):π΄βΆβ β§ π:(1...(β―βπ΄))βΆπ΄) β ((π β π΄ β¦ πΆ) β π):(1...(β―βπ΄))βΆβ) |
28 | 26, 21, 27 | syl2an 597 |
. . . . . . . . 9
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β ((π β π΄ β¦ πΆ) β π):(1...(β―βπ΄))βΆβ) |
29 | 28 | ffvelcdmda 7036 |
. . . . . . . 8
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (1...(β―βπ΄))) β (((π β π΄ β¦ πΆ) β π)βπ) β β) |
30 | | simprr 772 |
. . . . . . . . . . 11
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β π:(1...(β―βπ΄))β1-1-ontoβπ΄) |
31 | 30, 20 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β π:(1...(β―βπ΄))βΆπ΄) |
32 | | fvco3 6941 |
. . . . . . . . . 10
β’ ((π:(1...(β―βπ΄))βΆπ΄ β§ π β (1...(β―βπ΄))) β (((π β π΄ β¦ πΆ) β π)βπ) = ((π β π΄ β¦ πΆ)β(πβπ))) |
33 | 31, 32 | sylan 581 |
. . . . . . . . 9
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (1...(β―βπ΄))) β (((π β π΄ β¦ πΆ) β π)βπ) = ((π β π΄ β¦ πΆ)β(πβπ))) |
34 | 31 | ffvelcdmda 7036 |
. . . . . . . . . 10
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (1...(β―βπ΄))) β (πβπ) β π΄) |
35 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π΄) β π β π΄) |
36 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’ (π β π΄ β¦ πΆ) = (π β π΄ β¦ πΆ) |
37 | 36 | fvmpt2 6960 |
. . . . . . . . . . . . . 14
β’ ((π β π΄ β§ πΆ β β) β ((π β π΄ β¦ πΆ)βπ) = πΆ) |
38 | 35, 25, 37 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π΄) β ((π β π΄ β¦ πΆ)βπ) = πΆ) |
39 | | fproddiv.4 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π΄) β πΆ β 0) |
40 | 38, 39 | eqnetrd 3008 |
. . . . . . . . . . . 12
β’ ((π β§ π β π΄) β ((π β π΄ β¦ πΆ)βπ) β 0) |
41 | 40 | ralrimiva 3140 |
. . . . . . . . . . 11
β’ (π β βπ β π΄ ((π β π΄ β¦ πΆ)βπ) β 0) |
42 | 41 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (1...(β―βπ΄))) β βπ β π΄ ((π β π΄ β¦ πΆ)βπ) β 0) |
43 | | nffvmpt1 6854 |
. . . . . . . . . . . 12
β’
β²π((π β π΄ β¦ πΆ)β(πβπ)) |
44 | | nfcv 2904 |
. . . . . . . . . . . 12
β’
β²π0 |
45 | 43, 44 | nfne 3042 |
. . . . . . . . . . 11
β’
β²π((π β π΄ β¦ πΆ)β(πβπ)) β 0 |
46 | | fveq2 6843 |
. . . . . . . . . . . 12
β’ (π = (πβπ) β ((π β π΄ β¦ πΆ)βπ) = ((π β π΄ β¦ πΆ)β(πβπ))) |
47 | 46 | neeq1d 3000 |
. . . . . . . . . . 11
β’ (π = (πβπ) β (((π β π΄ β¦ πΆ)βπ) β 0 β ((π β π΄ β¦ πΆ)β(πβπ)) β 0)) |
48 | 45, 47 | rspc 3568 |
. . . . . . . . . 10
β’ ((πβπ) β π΄ β (βπ β π΄ ((π β π΄ β¦ πΆ)βπ) β 0 β ((π β π΄ β¦ πΆ)β(πβπ)) β 0)) |
49 | 34, 42, 48 | sylc 65 |
. . . . . . . . 9
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (1...(β―βπ΄))) β ((π β π΄ β¦ πΆ)β(πβπ)) β 0) |
50 | 33, 49 | eqnetrd 3008 |
. . . . . . . 8
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (1...(β―βπ΄))) β (((π β π΄ β¦ πΆ) β π)βπ) β 0) |
51 | 18, 25, 39 | divcld 11936 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π΄) β (π΅ / πΆ) β β) |
52 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’ (π β π΄ β¦ (π΅ / πΆ)) = (π β π΄ β¦ (π΅ / πΆ)) |
53 | 52 | fvmpt2 6960 |
. . . . . . . . . . . . . 14
β’ ((π β π΄ β§ (π΅ / πΆ) β β) β ((π β π΄ β¦ (π΅ / πΆ))βπ) = (π΅ / πΆ)) |
54 | 35, 51, 53 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π΄) β ((π β π΄ β¦ (π΅ / πΆ))βπ) = (π΅ / πΆ)) |
55 | | eqid 2733 |
. . . . . . . . . . . . . . . 16
β’ (π β π΄ β¦ π΅) = (π β π΄ β¦ π΅) |
56 | 55 | fvmpt2 6960 |
. . . . . . . . . . . . . . 15
β’ ((π β π΄ β§ π΅ β β) β ((π β π΄ β¦ π΅)βπ) = π΅) |
57 | 35, 18, 56 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π΄) β ((π β π΄ β¦ π΅)βπ) = π΅) |
58 | 57, 38 | oveq12d 7376 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π΄) β (((π β π΄ β¦ π΅)βπ) / ((π β π΄ β¦ πΆ)βπ)) = (π΅ / πΆ)) |
59 | 54, 58 | eqtr4d 2776 |
. . . . . . . . . . . 12
β’ ((π β§ π β π΄) β ((π β π΄ β¦ (π΅ / πΆ))βπ) = (((π β π΄ β¦ π΅)βπ) / ((π β π΄ β¦ πΆ)βπ))) |
60 | 59 | ralrimiva 3140 |
. . . . . . . . . . 11
β’ (π β βπ β π΄ ((π β π΄ β¦ (π΅ / πΆ))βπ) = (((π β π΄ β¦ π΅)βπ) / ((π β π΄ β¦ πΆ)βπ))) |
61 | 60 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (1...(β―βπ΄))) β βπ β π΄ ((π β π΄ β¦ (π΅ / πΆ))βπ) = (((π β π΄ β¦ π΅)βπ) / ((π β π΄ β¦ πΆ)βπ))) |
62 | | nffvmpt1 6854 |
. . . . . . . . . . . 12
β’
β²π((π β π΄ β¦ (π΅ / πΆ))β(πβπ)) |
63 | | nffvmpt1 6854 |
. . . . . . . . . . . . 13
β’
β²π((π β π΄ β¦ π΅)β(πβπ)) |
64 | | nfcv 2904 |
. . . . . . . . . . . . 13
β’
β²π
/ |
65 | 63, 64, 43 | nfov 7388 |
. . . . . . . . . . . 12
β’
β²π(((π β π΄ β¦ π΅)β(πβπ)) / ((π β π΄ β¦ πΆ)β(πβπ))) |
66 | 62, 65 | nfeq 2917 |
. . . . . . . . . . 11
β’
β²π((π β π΄ β¦ (π΅ / πΆ))β(πβπ)) = (((π β π΄ β¦ π΅)β(πβπ)) / ((π β π΄ β¦ πΆ)β(πβπ))) |
67 | | fveq2 6843 |
. . . . . . . . . . . 12
β’ (π = (πβπ) β ((π β π΄ β¦ (π΅ / πΆ))βπ) = ((π β π΄ β¦ (π΅ / πΆ))β(πβπ))) |
68 | | fveq2 6843 |
. . . . . . . . . . . . 13
β’ (π = (πβπ) β ((π β π΄ β¦ π΅)βπ) = ((π β π΄ β¦ π΅)β(πβπ))) |
69 | 68, 46 | oveq12d 7376 |
. . . . . . . . . . . 12
β’ (π = (πβπ) β (((π β π΄ β¦ π΅)βπ) / ((π β π΄ β¦ πΆ)βπ)) = (((π β π΄ β¦ π΅)β(πβπ)) / ((π β π΄ β¦ πΆ)β(πβπ)))) |
70 | 67, 69 | eqeq12d 2749 |
. . . . . . . . . . 11
β’ (π = (πβπ) β (((π β π΄ β¦ (π΅ / πΆ))βπ) = (((π β π΄ β¦ π΅)βπ) / ((π β π΄ β¦ πΆ)βπ)) β ((π β π΄ β¦ (π΅ / πΆ))β(πβπ)) = (((π β π΄ β¦ π΅)β(πβπ)) / ((π β π΄ β¦ πΆ)β(πβπ))))) |
71 | 66, 70 | rspc 3568 |
. . . . . . . . . 10
β’ ((πβπ) β π΄ β (βπ β π΄ ((π β π΄ β¦ (π΅ / πΆ))βπ) = (((π β π΄ β¦ π΅)βπ) / ((π β π΄ β¦ πΆ)βπ)) β ((π β π΄ β¦ (π΅ / πΆ))β(πβπ)) = (((π β π΄ β¦ π΅)β(πβπ)) / ((π β π΄ β¦ πΆ)β(πβπ))))) |
72 | 34, 61, 71 | sylc 65 |
. . . . . . . . 9
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (1...(β―βπ΄))) β ((π β π΄ β¦ (π΅ / πΆ))β(πβπ)) = (((π β π΄ β¦ π΅)β(πβπ)) / ((π β π΄ β¦ πΆ)β(πβπ)))) |
73 | | fvco3 6941 |
. . . . . . . . . 10
β’ ((π:(1...(β―βπ΄))βΆπ΄ β§ π β (1...(β―βπ΄))) β (((π β π΄ β¦ (π΅ / πΆ)) β π)βπ) = ((π β π΄ β¦ (π΅ / πΆ))β(πβπ))) |
74 | 31, 73 | sylan 581 |
. . . . . . . . 9
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (1...(β―βπ΄))) β (((π β π΄ β¦ (π΅ / πΆ)) β π)βπ) = ((π β π΄ β¦ (π΅ / πΆ))β(πβπ))) |
75 | | fvco3 6941 |
. . . . . . . . . . 11
β’ ((π:(1...(β―βπ΄))βΆπ΄ β§ π β (1...(β―βπ΄))) β (((π β π΄ β¦ π΅) β π)βπ) = ((π β π΄ β¦ π΅)β(πβπ))) |
76 | 31, 75 | sylan 581 |
. . . . . . . . . 10
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (1...(β―βπ΄))) β (((π β π΄ β¦ π΅) β π)βπ) = ((π β π΄ β¦ π΅)β(πβπ))) |
77 | 76, 33 | oveq12d 7376 |
. . . . . . . . 9
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (1...(β―βπ΄))) β ((((π β π΄ β¦ π΅) β π)βπ) / (((π β π΄ β¦ πΆ) β π)βπ)) = (((π β π΄ β¦ π΅)β(πβπ)) / ((π β π΄ β¦ πΆ)β(πβπ)))) |
78 | 72, 74, 77 | 3eqtr4d 2783 |
. . . . . . . 8
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (1...(β―βπ΄))) β (((π β π΄ β¦ (π΅ / πΆ)) β π)βπ) = ((((π β π΄ β¦ π΅) β π)βπ) / (((π β π΄ β¦ πΆ) β π)βπ))) |
79 | 17, 24, 29, 50, 78 | prodfdiv 15786 |
. . . . . . 7
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (seq1( Β· ,
((π β π΄ β¦ (π΅ / πΆ)) β π))β(β―βπ΄)) = ((seq1( Β· , ((π β π΄ β¦ π΅) β π))β(β―βπ΄)) / (seq1( Β· , ((π β π΄ β¦ πΆ) β π))β(β―βπ΄)))) |
80 | | fveq2 6843 |
. . . . . . . 8
β’ (π = (πβπ) β ((π β π΄ β¦ (π΅ / πΆ))βπ) = ((π β π΄ β¦ (π΅ / πΆ))β(πβπ))) |
81 | 51 | fmpttd 7064 |
. . . . . . . . . 10
β’ (π β (π β π΄ β¦ (π΅ / πΆ)):π΄βΆβ) |
82 | 81 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (π β π΄ β¦ (π΅ / πΆ)):π΄βΆβ) |
83 | 82 | ffvelcdmda 7036 |
. . . . . . . 8
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β π΄) β ((π β π΄ β¦ (π΅ / πΆ))βπ) β β) |
84 | 80, 15, 30, 83, 74 | fprod 15829 |
. . . . . . 7
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β βπ β π΄ ((π β π΄ β¦ (π΅ / πΆ))βπ) = (seq1( Β· , ((π β π΄ β¦ (π΅ / πΆ)) β π))β(β―βπ΄))) |
85 | | fveq2 6843 |
. . . . . . . . 9
β’ (π = (πβπ) β ((π β π΄ β¦ π΅)βπ) = ((π β π΄ β¦ π΅)β(πβπ))) |
86 | 19 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (π β π΄ β¦ π΅):π΄βΆβ) |
87 | 86 | ffvelcdmda 7036 |
. . . . . . . . 9
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β π΄) β ((π β π΄ β¦ π΅)βπ) β β) |
88 | 85, 15, 30, 87, 76 | fprod 15829 |
. . . . . . . 8
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β βπ β π΄ ((π β π΄ β¦ π΅)βπ) = (seq1( Β· , ((π β π΄ β¦ π΅) β π))β(β―βπ΄))) |
89 | | fveq2 6843 |
. . . . . . . . 9
β’ (π = (πβπ) β ((π β π΄ β¦ πΆ)βπ) = ((π β π΄ β¦ πΆ)β(πβπ))) |
90 | 26 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (π β π΄ β¦ πΆ):π΄βΆβ) |
91 | 90 | ffvelcdmda 7036 |
. . . . . . . . 9
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β π΄) β ((π β π΄ β¦ πΆ)βπ) β β) |
92 | 89, 15, 30, 91, 33 | fprod 15829 |
. . . . . . . 8
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β βπ β π΄ ((π β π΄ β¦ πΆ)βπ) = (seq1( Β· , ((π β π΄ β¦ πΆ) β π))β(β―βπ΄))) |
93 | 88, 92 | oveq12d 7376 |
. . . . . . 7
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (βπ β π΄ ((π β π΄ β¦ π΅)βπ) / βπ β π΄ ((π β π΄ β¦ πΆ)βπ)) = ((seq1( Β· , ((π β π΄ β¦ π΅) β π))β(β―βπ΄)) / (seq1( Β· , ((π β π΄ β¦ πΆ) β π))β(β―βπ΄)))) |
94 | 79, 84, 93 | 3eqtr4d 2783 |
. . . . . 6
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β βπ β π΄ ((π β π΄ β¦ (π΅ / πΆ))βπ) = (βπ β π΄ ((π β π΄ β¦ π΅)βπ) / βπ β π΄ ((π β π΄ β¦ πΆ)βπ))) |
95 | | prodfc 15833 |
. . . . . 6
β’
βπ β
π΄ ((π β π΄ β¦ (π΅ / πΆ))βπ) = βπ β π΄ (π΅ / πΆ) |
96 | | prodfc 15833 |
. . . . . . 7
β’
βπ β
π΄ ((π β π΄ β¦ π΅)βπ) = βπ β π΄ π΅ |
97 | | prodfc 15833 |
. . . . . . 7
β’
βπ β
π΄ ((π β π΄ β¦ πΆ)βπ) = βπ β π΄ πΆ |
98 | 96, 97 | oveq12i 7370 |
. . . . . 6
β’
(βπ β
π΄ ((π β π΄ β¦ π΅)βπ) / βπ β π΄ ((π β π΄ β¦ πΆ)βπ)) = (βπ β π΄ π΅ / βπ β π΄ πΆ) |
99 | 94, 95, 98 | 3eqtr3g 2796 |
. . . . 5
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β βπ β π΄ (π΅ / πΆ) = (βπ β π΄ π΅ / βπ β π΄ πΆ)) |
100 | 99 | expr 458 |
. . . 4
β’ ((π β§ (β―βπ΄) β β) β (π:(1...(β―βπ΄))β1-1-ontoβπ΄ β βπ β π΄ (π΅ / πΆ) = (βπ β π΄ π΅ / βπ β π΄ πΆ))) |
101 | 100 | exlimdv 1937 |
. . 3
β’ ((π β§ (β―βπ΄) β β) β
(βπ π:(1...(β―βπ΄))β1-1-ontoβπ΄ β βπ β π΄ (π΅ / πΆ) = (βπ β π΄ π΅ / βπ β π΄ πΆ))) |
102 | 101 | expimpd 455 |
. 2
β’ (π β (((β―βπ΄) β β β§
βπ π:(1...(β―βπ΄))β1-1-ontoβπ΄) β βπ β π΄ (π΅ / πΆ) = (βπ β π΄ π΅ / βπ β π΄ πΆ))) |
103 | | fprodmul.1 |
. . 3
β’ (π β π΄ β Fin) |
104 | | fz1f1o 15600 |
. . 3
β’ (π΄ β Fin β (π΄ = β
β¨
((β―βπ΄) β
β β§ βπ
π:(1...(β―βπ΄))β1-1-ontoβπ΄))) |
105 | 103, 104 | syl 17 |
. 2
β’ (π β (π΄ = β
β¨ ((β―βπ΄) β β β§
βπ π:(1...(β―βπ΄))β1-1-ontoβπ΄))) |
106 | 14, 102, 105 | mpjaod 859 |
1
β’ (π β βπ β π΄ (π΅ / πΆ) = (βπ β π΄ π΅ / βπ β π΄ πΆ)) |