Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . . . 5
β’
(β€β₯βπ) = (β€β₯βπ) |
2 | | simpr 486 |
. . . . 5
β’ ((π β§ π β β€) β π β β€) |
3 | | prodss.3 |
. . . . . 6
β’ (π β βπ β (β€β₯βπ)βπ¦(π¦ β 0 β§ seqπ( Β· , (π β (β€β₯βπ) β¦ if(π β π΅, πΆ, 1))) β π¦)) |
4 | 3 | adantr 482 |
. . . . 5
β’ ((π β§ π β β€) β βπ β
(β€β₯βπ)βπ¦(π¦ β 0 β§ seqπ( Β· , (π β (β€β₯βπ) β¦ if(π β π΅, πΆ, 1))) β π¦)) |
5 | | prodss.1 |
. . . . . . 7
β’ (π β π΄ β π΅) |
6 | | prodss.5 |
. . . . . . 7
β’ (π β π΅ β (β€β₯βπ)) |
7 | 5, 6 | sstrd 3959 |
. . . . . 6
β’ (π β π΄ β (β€β₯βπ)) |
8 | 7 | adantr 482 |
. . . . 5
β’ ((π β§ π β β€) β π΄ β (β€β₯βπ)) |
9 | | simpr 486 |
. . . . . . 7
β’ (((π β§ π β β€) β§ π β (β€β₯βπ)) β π β (β€β₯βπ)) |
10 | | iftrue 4497 |
. . . . . . . . . . . 12
β’ (π β π΅ β if(π β π΅, β¦π / πβ¦πΆ, 1) = β¦π / πβ¦πΆ) |
11 | 10 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β§ π β π΅) β if(π β π΅, β¦π / πβ¦πΆ, 1) = β¦π / πβ¦πΆ) |
12 | | prodss.2 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β π΄) β πΆ β β) |
13 | 12 | ex 414 |
. . . . . . . . . . . . . . 15
β’ (π β (π β π΄ β πΆ β β)) |
14 | 13 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π΅) β (π β π΄ β πΆ β β)) |
15 | | eldif 3925 |
. . . . . . . . . . . . . . . 16
β’ (π β (π΅ β π΄) β (π β π΅ β§ Β¬ π β π΄)) |
16 | | prodss.4 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (π΅ β π΄)) β πΆ = 1) |
17 | | ax-1cn 11116 |
. . . . . . . . . . . . . . . . 17
β’ 1 β
β |
18 | 16, 17 | eqeltrdi 2846 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (π΅ β π΄)) β πΆ β β) |
19 | 15, 18 | sylan2br 596 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β π΅ β§ Β¬ π β π΄)) β πΆ β β) |
20 | 19 | expr 458 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π΅) β (Β¬ π β π΄ β πΆ β β)) |
21 | 14, 20 | pm2.61d 179 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π΅) β πΆ β β) |
22 | 21 | ralrimiva 3144 |
. . . . . . . . . . . 12
β’ (π β βπ β π΅ πΆ β β) |
23 | | nfcsb1v 3885 |
. . . . . . . . . . . . . 14
β’
β²πβ¦π / πβ¦πΆ |
24 | 23 | nfel1 2924 |
. . . . . . . . . . . . 13
β’
β²πβ¦π / πβ¦πΆ β β |
25 | | csbeq1a 3874 |
. . . . . . . . . . . . . 14
β’ (π = π β πΆ = β¦π / πβ¦πΆ) |
26 | 25 | eleq1d 2823 |
. . . . . . . . . . . . 13
β’ (π = π β (πΆ β β β β¦π / πβ¦πΆ β β)) |
27 | 24, 26 | rspc 3572 |
. . . . . . . . . . . 12
β’ (π β π΅ β (βπ β π΅ πΆ β β β β¦π / πβ¦πΆ β β)) |
28 | 22, 27 | mpan9 508 |
. . . . . . . . . . 11
β’ ((π β§ π β π΅) β β¦π / πβ¦πΆ β β) |
29 | 11, 28 | eqeltrd 2838 |
. . . . . . . . . 10
β’ ((π β§ π β π΅) β if(π β π΅, β¦π / πβ¦πΆ, 1) β β) |
30 | | iffalse 4500 |
. . . . . . . . . . . 12
β’ (Β¬
π β π΅ β if(π β π΅, β¦π / πβ¦πΆ, 1) = 1) |
31 | 30, 17 | eqeltrdi 2846 |
. . . . . . . . . . 11
β’ (Β¬
π β π΅ β if(π β π΅, β¦π / πβ¦πΆ, 1) β β) |
32 | 31 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ Β¬ π β π΅) β if(π β π΅, β¦π / πβ¦πΆ, 1) β β) |
33 | 29, 32 | pm2.61dan 812 |
. . . . . . . . 9
β’ (π β if(π β π΅, β¦π / πβ¦πΆ, 1) β β) |
34 | 33 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β β€) β if(π β π΅, β¦π / πβ¦πΆ, 1) β β) |
35 | 34 | adantr 482 |
. . . . . . 7
β’ (((π β§ π β β€) β§ π β (β€β₯βπ)) β if(π β π΅, β¦π / πβ¦πΆ, 1) β β) |
36 | | nfcv 2908 |
. . . . . . . 8
β’
β²ππ |
37 | | nfv 1918 |
. . . . . . . . 9
β’
β²π π β π΅ |
38 | | nfcv 2908 |
. . . . . . . . 9
β’
β²π1 |
39 | 37, 23, 38 | nfif 4521 |
. . . . . . . 8
β’
β²πif(π β π΅, β¦π / πβ¦πΆ, 1) |
40 | | eleq1w 2821 |
. . . . . . . . 9
β’ (π = π β (π β π΅ β π β π΅)) |
41 | 40, 25 | ifbieq1d 4515 |
. . . . . . . 8
β’ (π = π β if(π β π΅, πΆ, 1) = if(π β π΅, β¦π / πβ¦πΆ, 1)) |
42 | | eqid 2737 |
. . . . . . . 8
β’ (π β
(β€β₯βπ) β¦ if(π β π΅, πΆ, 1)) = (π β (β€β₯βπ) β¦ if(π β π΅, πΆ, 1)) |
43 | 36, 39, 41, 42 | fvmptf 6974 |
. . . . . . 7
β’ ((π β
(β€β₯βπ) β§ if(π β π΅, β¦π / πβ¦πΆ, 1) β β) β ((π β
(β€β₯βπ) β¦ if(π β π΅, πΆ, 1))βπ) = if(π β π΅, β¦π / πβ¦πΆ, 1)) |
44 | 9, 35, 43 | syl2anc 585 |
. . . . . 6
β’ (((π β§ π β β€) β§ π β (β€β₯βπ)) β ((π β (β€β₯βπ) β¦ if(π β π΅, πΆ, 1))βπ) = if(π β π΅, β¦π / πβ¦πΆ, 1)) |
45 | | iftrue 4497 |
. . . . . . . . . . . . . 14
β’ (π β π΄ β if(π β π΄, ((π β π΄ β¦ πΆ)βπ), 1) = ((π β π΄ β¦ πΆ)βπ)) |
46 | 45 | adantl 483 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β€) β§ π β π΄) β if(π β π΄, ((π β π΄ β¦ πΆ)βπ), 1) = ((π β π΄ β¦ πΆ)βπ)) |
47 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β€) β§ π β π΄) β π β π΄) |
48 | 5 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β€) β π΄ β π΅) |
49 | 48 | sselda 3949 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β€) β§ π β π΄) β π β π΅) |
50 | 28 | adantlr 714 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β€) β§ π β π΅) β β¦π / πβ¦πΆ β β) |
51 | 49, 50 | syldan 592 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β€) β§ π β π΄) β β¦π / πβ¦πΆ β β) |
52 | | eqid 2737 |
. . . . . . . . . . . . . . 15
β’ (π β π΄ β¦ πΆ) = (π β π΄ β¦ πΆ) |
53 | 52 | fvmpts 6956 |
. . . . . . . . . . . . . 14
β’ ((π β π΄ β§ β¦π / πβ¦πΆ β β) β ((π β π΄ β¦ πΆ)βπ) = β¦π / πβ¦πΆ) |
54 | 47, 51, 53 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β€) β§ π β π΄) β ((π β π΄ β¦ πΆ)βπ) = β¦π / πβ¦πΆ) |
55 | 46, 54 | eqtrd 2777 |
. . . . . . . . . . . 12
β’ (((π β§ π β β€) β§ π β π΄) β if(π β π΄, ((π β π΄ β¦ πΆ)βπ), 1) = β¦π / πβ¦πΆ) |
56 | 55 | ex 414 |
. . . . . . . . . . 11
β’ ((π β§ π β β€) β (π β π΄ β if(π β π΄, ((π β π΄ β¦ πΆ)βπ), 1) = β¦π / πβ¦πΆ)) |
57 | 56 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ π β β€) β§ π β π΅) β (π β π΄ β if(π β π΄, ((π β π΄ β¦ πΆ)βπ), 1) = β¦π / πβ¦πΆ)) |
58 | | iffalse 4500 |
. . . . . . . . . . . . . 14
β’ (Β¬
π β π΄ β if(π β π΄, ((π β π΄ β¦ πΆ)βπ), 1) = 1) |
59 | 58 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π β π΅ β§ Β¬ π β π΄) β if(π β π΄, ((π β π΄ β¦ πΆ)βπ), 1) = 1) |
60 | 59 | adantl 483 |
. . . . . . . . . . . 12
β’ (((π β§ π β β€) β§ (π β π΅ β§ Β¬ π β π΄)) β if(π β π΄, ((π β π΄ β¦ πΆ)βπ), 1) = 1) |
61 | | eldif 3925 |
. . . . . . . . . . . . 13
β’ (π β (π΅ β π΄) β (π β π΅ β§ Β¬ π β π΄)) |
62 | 16 | ralrimiva 3144 |
. . . . . . . . . . . . . . 15
β’ (π β βπ β (π΅ β π΄)πΆ = 1) |
63 | 62 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β€) β βπ β (π΅ β π΄)πΆ = 1) |
64 | 23 | nfeq1 2923 |
. . . . . . . . . . . . . . 15
β’
β²πβ¦π / πβ¦πΆ = 1 |
65 | 25 | eqeq1d 2739 |
. . . . . . . . . . . . . . 15
β’ (π = π β (πΆ = 1 β β¦π / πβ¦πΆ = 1)) |
66 | 64, 65 | rspc 3572 |
. . . . . . . . . . . . . 14
β’ (π β (π΅ β π΄) β (βπ β (π΅ β π΄)πΆ = 1 β β¦π / πβ¦πΆ = 1)) |
67 | 63, 66 | mpan9 508 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β€) β§ π β (π΅ β π΄)) β β¦π / πβ¦πΆ = 1) |
68 | 61, 67 | sylan2br 596 |
. . . . . . . . . . . 12
β’ (((π β§ π β β€) β§ (π β π΅ β§ Β¬ π β π΄)) β β¦π / πβ¦πΆ = 1) |
69 | 60, 68 | eqtr4d 2780 |
. . . . . . . . . . 11
β’ (((π β§ π β β€) β§ (π β π΅ β§ Β¬ π β π΄)) β if(π β π΄, ((π β π΄ β¦ πΆ)βπ), 1) = β¦π / πβ¦πΆ) |
70 | 69 | expr 458 |
. . . . . . . . . 10
β’ (((π β§ π β β€) β§ π β π΅) β (Β¬ π β π΄ β if(π β π΄, ((π β π΄ β¦ πΆ)βπ), 1) = β¦π / πβ¦πΆ)) |
71 | 57, 70 | pm2.61d 179 |
. . . . . . . . 9
β’ (((π β§ π β β€) β§ π β π΅) β if(π β π΄, ((π β π΄ β¦ πΆ)βπ), 1) = β¦π / πβ¦πΆ) |
72 | 10 | adantl 483 |
. . . . . . . . 9
β’ (((π β§ π β β€) β§ π β π΅) β if(π β π΅, β¦π / πβ¦πΆ, 1) = β¦π / πβ¦πΆ) |
73 | 71, 72 | eqtr4d 2780 |
. . . . . . . 8
β’ (((π β§ π β β€) β§ π β π΅) β if(π β π΄, ((π β π΄ β¦ πΆ)βπ), 1) = if(π β π΅, β¦π / πβ¦πΆ, 1)) |
74 | 48 | ssneld 3951 |
. . . . . . . . . . 11
β’ ((π β§ π β β€) β (Β¬ π β π΅ β Β¬ π β π΄)) |
75 | 74 | imp 408 |
. . . . . . . . . 10
β’ (((π β§ π β β€) β§ Β¬ π β π΅) β Β¬ π β π΄) |
76 | 75, 58 | syl 17 |
. . . . . . . . 9
β’ (((π β§ π β β€) β§ Β¬ π β π΅) β if(π β π΄, ((π β π΄ β¦ πΆ)βπ), 1) = 1) |
77 | 30 | adantl 483 |
. . . . . . . . 9
β’ (((π β§ π β β€) β§ Β¬ π β π΅) β if(π β π΅, β¦π / πβ¦πΆ, 1) = 1) |
78 | 76, 77 | eqtr4d 2780 |
. . . . . . . 8
β’ (((π β§ π β β€) β§ Β¬ π β π΅) β if(π β π΄, ((π β π΄ β¦ πΆ)βπ), 1) = if(π β π΅, β¦π / πβ¦πΆ, 1)) |
79 | 73, 78 | pm2.61dan 812 |
. . . . . . 7
β’ ((π β§ π β β€) β if(π β π΄, ((π β π΄ β¦ πΆ)βπ), 1) = if(π β π΅, β¦π / πβ¦πΆ, 1)) |
80 | 79 | adantr 482 |
. . . . . 6
β’ (((π β§ π β β€) β§ π β (β€β₯βπ)) β if(π β π΄, ((π β π΄ β¦ πΆ)βπ), 1) = if(π β π΅, β¦π / πβ¦πΆ, 1)) |
81 | 44, 80 | eqtr4d 2780 |
. . . . 5
β’ (((π β§ π β β€) β§ π β (β€β₯βπ)) β ((π β (β€β₯βπ) β¦ if(π β π΅, πΆ, 1))βπ) = if(π β π΄, ((π β π΄ β¦ πΆ)βπ), 1)) |
82 | 12 | fmpttd 7068 |
. . . . . . 7
β’ (π β (π β π΄ β¦ πΆ):π΄βΆβ) |
83 | 82 | adantr 482 |
. . . . . 6
β’ ((π β§ π β β€) β (π β π΄ β¦ πΆ):π΄βΆβ) |
84 | 83 | ffvelcdmda 7040 |
. . . . 5
β’ (((π β§ π β β€) β§ π β π΄) β ((π β π΄ β¦ πΆ)βπ) β β) |
85 | 1, 2, 4, 8, 81, 84 | zprod 15827 |
. . . 4
β’ ((π β§ π β β€) β βπ β π΄ ((π β π΄ β¦ πΆ)βπ) = ( β βseqπ( Β· , (π β (β€β₯βπ) β¦ if(π β π΅, πΆ, 1))))) |
86 | 6 | adantr 482 |
. . . . 5
β’ ((π β§ π β β€) β π΅ β (β€β₯βπ)) |
87 | 43 | ancoms 460 |
. . . . . . 7
β’
((if(π β π΅, β¦π / πβ¦πΆ, 1) β β β§ π β (β€β₯βπ)) β ((π β (β€β₯βπ) β¦ if(π β π΅, πΆ, 1))βπ) = if(π β π΅, β¦π / πβ¦πΆ, 1)) |
88 | 34, 87 | sylan 581 |
. . . . . 6
β’ (((π β§ π β β€) β§ π β (β€β₯βπ)) β ((π β (β€β₯βπ) β¦ if(π β π΅, πΆ, 1))βπ) = if(π β π΅, β¦π / πβ¦πΆ, 1)) |
89 | | simpr 486 |
. . . . . . . . . 10
β’ (((π β§ π β β€) β§ π β π΅) β π β π΅) |
90 | | eqid 2737 |
. . . . . . . . . . 11
β’ (π β π΅ β¦ πΆ) = (π β π΅ β¦ πΆ) |
91 | 90 | fvmpts 6956 |
. . . . . . . . . 10
β’ ((π β π΅ β§ β¦π / πβ¦πΆ β β) β ((π β π΅ β¦ πΆ)βπ) = β¦π / πβ¦πΆ) |
92 | 89, 50, 91 | syl2anc 585 |
. . . . . . . . 9
β’ (((π β§ π β β€) β§ π β π΅) β ((π β π΅ β¦ πΆ)βπ) = β¦π / πβ¦πΆ) |
93 | 92 | ifeq1d 4510 |
. . . . . . . 8
β’ (((π β§ π β β€) β§ π β π΅) β if(π β π΅, ((π β π΅ β¦ πΆ)βπ), 1) = if(π β π΅, β¦π / πβ¦πΆ, 1)) |
94 | 93 | adantlr 714 |
. . . . . . 7
β’ ((((π β§ π β β€) β§ π β (β€β₯βπ)) β§ π β π΅) β if(π β π΅, ((π β π΅ β¦ πΆ)βπ), 1) = if(π β π΅, β¦π / πβ¦πΆ, 1)) |
95 | | iffalse 4500 |
. . . . . . . . 9
β’ (Β¬
π β π΅ β if(π β π΅, ((π β π΅ β¦ πΆ)βπ), 1) = 1) |
96 | 95, 30 | eqtr4d 2780 |
. . . . . . . 8
β’ (Β¬
π β π΅ β if(π β π΅, ((π β π΅ β¦ πΆ)βπ), 1) = if(π β π΅, β¦π / πβ¦πΆ, 1)) |
97 | 96 | adantl 483 |
. . . . . . 7
β’ ((((π β§ π β β€) β§ π β (β€β₯βπ)) β§ Β¬ π β π΅) β if(π β π΅, ((π β π΅ β¦ πΆ)βπ), 1) = if(π β π΅, β¦π / πβ¦πΆ, 1)) |
98 | 94, 97 | pm2.61dan 812 |
. . . . . 6
β’ (((π β§ π β β€) β§ π β (β€β₯βπ)) β if(π β π΅, ((π β π΅ β¦ πΆ)βπ), 1) = if(π β π΅, β¦π / πβ¦πΆ, 1)) |
99 | 88, 98 | eqtr4d 2780 |
. . . . 5
β’ (((π β§ π β β€) β§ π β (β€β₯βπ)) β ((π β (β€β₯βπ) β¦ if(π β π΅, πΆ, 1))βπ) = if(π β π΅, ((π β π΅ β¦ πΆ)βπ), 1)) |
100 | 21 | fmpttd 7068 |
. . . . . . 7
β’ (π β (π β π΅ β¦ πΆ):π΅βΆβ) |
101 | 100 | adantr 482 |
. . . . . 6
β’ ((π β§ π β β€) β (π β π΅ β¦ πΆ):π΅βΆβ) |
102 | 101 | ffvelcdmda 7040 |
. . . . 5
β’ (((π β§ π β β€) β§ π β π΅) β ((π β π΅ β¦ πΆ)βπ) β β) |
103 | 1, 2, 4, 86, 99, 102 | zprod 15827 |
. . . 4
β’ ((π β§ π β β€) β βπ β π΅ ((π β π΅ β¦ πΆ)βπ) = ( β βseqπ( Β· , (π β (β€β₯βπ) β¦ if(π β π΅, πΆ, 1))))) |
104 | 85, 103 | eqtr4d 2780 |
. . 3
β’ ((π β§ π β β€) β βπ β π΄ ((π β π΄ β¦ πΆ)βπ) = βπ β π΅ ((π β π΅ β¦ πΆ)βπ)) |
105 | | prodfc 15835 |
. . 3
β’
βπ β
π΄ ((π β π΄ β¦ πΆ)βπ) = βπ β π΄ πΆ |
106 | | prodfc 15835 |
. . 3
β’
βπ β
π΅ ((π β π΅ β¦ πΆ)βπ) = βπ β π΅ πΆ |
107 | 104, 105,
106 | 3eqtr3g 2800 |
. 2
β’ ((π β§ π β β€) β βπ β π΄ πΆ = βπ β π΅ πΆ) |
108 | 5 | adantr 482 |
. . . . . 6
β’ ((π β§ Β¬ π β β€) β π΄ β π΅) |
109 | 6 | adantr 482 |
. . . . . . 7
β’ ((π β§ Β¬ π β β€) β π΅ β (β€β₯βπ)) |
110 | | uzf 12773 |
. . . . . . . . . . 11
β’
β€β₯:β€βΆπ« β€ |
111 | 110 | fdmi 6685 |
. . . . . . . . . 10
β’ dom
β€β₯ = β€ |
112 | 111 | eleq2i 2830 |
. . . . . . . . 9
β’ (π β dom
β€β₯ β π β β€) |
113 | | ndmfv 6882 |
. . . . . . . . 9
β’ (Β¬
π β dom
β€β₯ β (β€β₯βπ) = β
) |
114 | 112, 113 | sylnbir 331 |
. . . . . . . 8
β’ (Β¬
π β β€ β
(β€β₯βπ) = β
) |
115 | 114 | adantl 483 |
. . . . . . 7
β’ ((π β§ Β¬ π β β€) β
(β€β₯βπ) = β
) |
116 | 109, 115 | sseqtrd 3989 |
. . . . . 6
β’ ((π β§ Β¬ π β β€) β π΅ β β
) |
117 | 108, 116 | sstrd 3959 |
. . . . 5
β’ ((π β§ Β¬ π β β€) β π΄ β β
) |
118 | | ss0 4363 |
. . . . 5
β’ (π΄ β β
β π΄ = β
) |
119 | 117, 118 | syl 17 |
. . . 4
β’ ((π β§ Β¬ π β β€) β π΄ = β
) |
120 | | ss0 4363 |
. . . . 5
β’ (π΅ β β
β π΅ = β
) |
121 | 116, 120 | syl 17 |
. . . 4
β’ ((π β§ Β¬ π β β€) β π΅ = β
) |
122 | 119, 121 | eqtr4d 2780 |
. . 3
β’ ((π β§ Β¬ π β β€) β π΄ = π΅) |
123 | 122 | prodeq1d 15811 |
. 2
β’ ((π β§ Β¬ π β β€) β βπ β π΄ πΆ = βπ β π΅ πΆ) |
124 | 107, 123 | pm2.61dan 812 |
1
β’ (π β βπ β π΄ πΆ = βπ β π΅ πΆ) |