Step | Hyp | Ref
| Expression |
1 | | eqid 2177 |
. . . 4
β’
(β€β₯βπ) = (β€β₯βπ) |
2 | | prodssdc.m |
. . . 4
β’ (π β π β β€) |
3 | | prodssdc.3 |
. . . 4
β’ (π β βπ β (β€β₯βπ)βπ¦(π¦ # 0 β§ seqπ( Β· , (π β (β€β₯βπ) β¦ if(π β π΅, πΆ, 1))) β π¦)) |
4 | | prodss.1 |
. . . . 5
β’ (π β π΄ β π΅) |
5 | | prodss.5 |
. . . . 5
β’ (π β π΅ β (β€β₯βπ)) |
6 | 4, 5 | sstrd 3165 |
. . . 4
β’ (π β π΄ β (β€β₯βπ)) |
7 | | prodssdc.a |
. . . 4
β’ (π β βπ β (β€β₯βπ)DECID π β π΄) |
8 | | simpr 110 |
. . . . . 6
β’ ((π β§ π β (β€β₯βπ)) β π β (β€β₯βπ)) |
9 | | eleq1w 2238 |
. . . . . . . . . 10
β’ (π = π β (π β π΅ β π β π΅)) |
10 | 9 | dcbid 838 |
. . . . . . . . 9
β’ (π = π β (DECID π β π΅ β DECID π β π΅)) |
11 | | prodssdc.b |
. . . . . . . . . 10
β’ (π β βπ β (β€β₯βπ)DECID π β π΅) |
12 | 11 | adantr 276 |
. . . . . . . . 9
β’ ((π β§ π β (β€β₯βπ)) β βπ β
(β€β₯βπ)DECID π β π΅) |
13 | 10, 12, 8 | rspcdva 2846 |
. . . . . . . 8
β’ ((π β§ π β (β€β₯βπ)) β DECID
π β π΅) |
14 | | exmiddc 836 |
. . . . . . . 8
β’
(DECID π β π΅ β (π β π΅ β¨ Β¬ π β π΅)) |
15 | 13, 14 | syl 14 |
. . . . . . 7
β’ ((π β§ π β (β€β₯βπ)) β (π β π΅ β¨ Β¬ π β π΅)) |
16 | | iftrue 3539 |
. . . . . . . . . . . 12
β’ (π β π΅ β if(π β π΅, β¦π / πβ¦πΆ, 1) = β¦π / πβ¦πΆ) |
17 | 16 | adantl 277 |
. . . . . . . . . . 11
β’ ((π β§ π β π΅) β if(π β π΅, β¦π / πβ¦πΆ, 1) = β¦π / πβ¦πΆ) |
18 | | prodss.2 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β π΄) β πΆ β β) |
19 | 18 | ex 115 |
. . . . . . . . . . . . . . 15
β’ (π β (π β π΄ β πΆ β β)) |
20 | 19 | adantr 276 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π΅) β (π β π΄ β πΆ β β)) |
21 | | eldif 3138 |
. . . . . . . . . . . . . . . 16
β’ (π β (π΅ β π΄) β (π β π΅ β§ Β¬ π β π΄)) |
22 | | prodss.4 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (π΅ β π΄)) β πΆ = 1) |
23 | | ax-1cn 7903 |
. . . . . . . . . . . . . . . . 17
β’ 1 β
β |
24 | 22, 23 | eqeltrdi 2268 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (π΅ β π΄)) β πΆ β β) |
25 | 21, 24 | sylan2br 288 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β π΅ β§ Β¬ π β π΄)) β πΆ β β) |
26 | 25 | expr 375 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π΅) β (Β¬ π β π΄ β πΆ β β)) |
27 | | eleq1w 2238 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (π β π΄ β π β π΄)) |
28 | 27 | dcbid 838 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (DECID π β π΄ β DECID π β π΄)) |
29 | 7 | adantr 276 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β π΅) β βπ β (β€β₯βπ)DECID π β π΄) |
30 | 5 | sselda 3155 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β π΅) β π β (β€β₯βπ)) |
31 | 28, 29, 30 | rspcdva 2846 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π΅) β DECID π β π΄) |
32 | | exmiddc 836 |
. . . . . . . . . . . . . . 15
β’
(DECID π β π΄ β (π β π΄ β¨ Β¬ π β π΄)) |
33 | 31, 32 | syl 14 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π΅) β (π β π΄ β¨ Β¬ π β π΄)) |
34 | 20, 26, 33 | mpjaod 718 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π΅) β πΆ β β) |
35 | 34 | ralrimiva 2550 |
. . . . . . . . . . . 12
β’ (π β βπ β π΅ πΆ β β) |
36 | | nfcsb1v 3090 |
. . . . . . . . . . . . . 14
β’
β²πβ¦π / πβ¦πΆ |
37 | 36 | nfel1 2330 |
. . . . . . . . . . . . 13
β’
β²πβ¦π / πβ¦πΆ β β |
38 | | csbeq1a 3066 |
. . . . . . . . . . . . . 14
β’ (π = π β πΆ = β¦π / πβ¦πΆ) |
39 | 38 | eleq1d 2246 |
. . . . . . . . . . . . 13
β’ (π = π β (πΆ β β β β¦π / πβ¦πΆ β β)) |
40 | 37, 39 | rspc 2835 |
. . . . . . . . . . . 12
β’ (π β π΅ β (βπ β π΅ πΆ β β β β¦π / πβ¦πΆ β β)) |
41 | 35, 40 | mpan9 281 |
. . . . . . . . . . 11
β’ ((π β§ π β π΅) β β¦π / πβ¦πΆ β β) |
42 | 17, 41 | eqeltrd 2254 |
. . . . . . . . . 10
β’ ((π β§ π β π΅) β if(π β π΅, β¦π / πβ¦πΆ, 1) β β) |
43 | 42 | ex 115 |
. . . . . . . . 9
β’ (π β (π β π΅ β if(π β π΅, β¦π / πβ¦πΆ, 1) β β)) |
44 | | iffalse 3542 |
. . . . . . . . . . 11
β’ (Β¬
π β π΅ β if(π β π΅, β¦π / πβ¦πΆ, 1) = 1) |
45 | 44, 23 | eqeltrdi 2268 |
. . . . . . . . . 10
β’ (Β¬
π β π΅ β if(π β π΅, β¦π / πβ¦πΆ, 1) β β) |
46 | 45 | a1i 9 |
. . . . . . . . 9
β’ (π β (Β¬ π β π΅ β if(π β π΅, β¦π / πβ¦πΆ, 1) β β)) |
47 | 43, 46 | jaod 717 |
. . . . . . . 8
β’ (π β ((π β π΅ β¨ Β¬ π β π΅) β if(π β π΅, β¦π / πβ¦πΆ, 1) β β)) |
48 | 47 | adantr 276 |
. . . . . . 7
β’ ((π β§ π β (β€β₯βπ)) β ((π β π΅ β¨ Β¬ π β π΅) β if(π β π΅, β¦π / πβ¦πΆ, 1) β β)) |
49 | 15, 48 | mpd 13 |
. . . . . 6
β’ ((π β§ π β (β€β₯βπ)) β if(π β π΅, β¦π / πβ¦πΆ, 1) β β) |
50 | | nfcv 2319 |
. . . . . . 7
β’
β²ππ |
51 | | nfv 1528 |
. . . . . . . 8
β’
β²π π β π΅ |
52 | | nfcv 2319 |
. . . . . . . 8
β’
β²π1 |
53 | 51, 36, 52 | nfif 3562 |
. . . . . . 7
β’
β²πif(π β π΅, β¦π / πβ¦πΆ, 1) |
54 | | eleq1w 2238 |
. . . . . . . 8
β’ (π = π β (π β π΅ β π β π΅)) |
55 | 54, 38 | ifbieq1d 3556 |
. . . . . . 7
β’ (π = π β if(π β π΅, πΆ, 1) = if(π β π΅, β¦π / πβ¦πΆ, 1)) |
56 | | eqid 2177 |
. . . . . . 7
β’ (π β
(β€β₯βπ) β¦ if(π β π΅, πΆ, 1)) = (π β (β€β₯βπ) β¦ if(π β π΅, πΆ, 1)) |
57 | 50, 53, 55, 56 | fvmptf 5608 |
. . . . . 6
β’ ((π β
(β€β₯βπ) β§ if(π β π΅, β¦π / πβ¦πΆ, 1) β β) β ((π β
(β€β₯βπ) β¦ if(π β π΅, πΆ, 1))βπ) = if(π β π΅, β¦π / πβ¦πΆ, 1)) |
58 | 8, 49, 57 | syl2anc 411 |
. . . . 5
β’ ((π β§ π β (β€β₯βπ)) β ((π β (β€β₯βπ) β¦ if(π β π΅, πΆ, 1))βπ) = if(π β π΅, β¦π / πβ¦πΆ, 1)) |
59 | | iftrue 3539 |
. . . . . . . . . . . . . . 15
β’ (π β π΄ β if(π β π΄, ((π β π΄ β¦ πΆ)βπ), 1) = ((π β π΄ β¦ πΆ)βπ)) |
60 | 59 | adantl 277 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π΄) β if(π β π΄, ((π β π΄ β¦ πΆ)βπ), 1) = ((π β π΄ β¦ πΆ)βπ)) |
61 | | simpr 110 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π΄) β π β π΄) |
62 | 4 | sselda 3155 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β π΄) β π β π΅) |
63 | 62, 41 | syldan 282 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π΄) β β¦π / πβ¦πΆ β β) |
64 | | eqid 2177 |
. . . . . . . . . . . . . . . 16
β’ (π β π΄ β¦ πΆ) = (π β π΄ β¦ πΆ) |
65 | 64 | fvmpts 5594 |
. . . . . . . . . . . . . . 15
β’ ((π β π΄ β§ β¦π / πβ¦πΆ β β) β ((π β π΄ β¦ πΆ)βπ) = β¦π / πβ¦πΆ) |
66 | 61, 63, 65 | syl2anc 411 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π΄) β ((π β π΄ β¦ πΆ)βπ) = β¦π / πβ¦πΆ) |
67 | 60, 66 | eqtrd 2210 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π΄) β if(π β π΄, ((π β π΄ β¦ πΆ)βπ), 1) = β¦π / πβ¦πΆ) |
68 | 67 | ex 115 |
. . . . . . . . . . . 12
β’ (π β (π β π΄ β if(π β π΄, ((π β π΄ β¦ πΆ)βπ), 1) = β¦π / πβ¦πΆ)) |
69 | 68 | adantr 276 |
. . . . . . . . . . 11
β’ ((π β§ π β π΅) β (π β π΄ β if(π β π΄, ((π β π΄ β¦ πΆ)βπ), 1) = β¦π / πβ¦πΆ)) |
70 | | iffalse 3542 |
. . . . . . . . . . . . . . 15
β’ (Β¬
π β π΄ β if(π β π΄, ((π β π΄ β¦ πΆ)βπ), 1) = 1) |
71 | 70 | adantl 277 |
. . . . . . . . . . . . . 14
β’ ((π β π΅ β§ Β¬ π β π΄) β if(π β π΄, ((π β π΄ β¦ πΆ)βπ), 1) = 1) |
72 | 71 | adantl 277 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β π΅ β§ Β¬ π β π΄)) β if(π β π΄, ((π β π΄ β¦ πΆ)βπ), 1) = 1) |
73 | | eldif 3138 |
. . . . . . . . . . . . . 14
β’ (π β (π΅ β π΄) β (π β π΅ β§ Β¬ π β π΄)) |
74 | 22 | ralrimiva 2550 |
. . . . . . . . . . . . . . 15
β’ (π β βπ β (π΅ β π΄)πΆ = 1) |
75 | 36 | nfeq1 2329 |
. . . . . . . . . . . . . . . 16
β’
β²πβ¦π / πβ¦πΆ = 1 |
76 | 38 | eqeq1d 2186 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (πΆ = 1 β β¦π / πβ¦πΆ = 1)) |
77 | 75, 76 | rspc 2835 |
. . . . . . . . . . . . . . 15
β’ (π β (π΅ β π΄) β (βπ β (π΅ β π΄)πΆ = 1 β β¦π / πβ¦πΆ = 1)) |
78 | 74, 77 | mpan9 281 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (π΅ β π΄)) β β¦π / πβ¦πΆ = 1) |
79 | 73, 78 | sylan2br 288 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β π΅ β§ Β¬ π β π΄)) β β¦π / πβ¦πΆ = 1) |
80 | 72, 79 | eqtr4d 2213 |
. . . . . . . . . . . 12
β’ ((π β§ (π β π΅ β§ Β¬ π β π΄)) β if(π β π΄, ((π β π΄ β¦ πΆ)βπ), 1) = β¦π / πβ¦πΆ) |
81 | 80 | expr 375 |
. . . . . . . . . . 11
β’ ((π β§ π β π΅) β (Β¬ π β π΄ β if(π β π΄, ((π β π΄ β¦ πΆ)βπ), 1) = β¦π / πβ¦πΆ)) |
82 | | eleq1w 2238 |
. . . . . . . . . . . . . 14
β’ (π = π β (π β π΄ β π β π΄)) |
83 | 82 | dcbid 838 |
. . . . . . . . . . . . 13
β’ (π = π β (DECID π β π΄ β DECID π β π΄)) |
84 | 7 | adantr 276 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π΅) β βπ β (β€β₯βπ)DECID π β π΄) |
85 | 5 | sselda 3155 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π΅) β π β (β€β₯βπ)) |
86 | 83, 84, 85 | rspcdva 2846 |
. . . . . . . . . . . 12
β’ ((π β§ π β π΅) β DECID π β π΄) |
87 | | exmiddc 836 |
. . . . . . . . . . . 12
β’
(DECID π β π΄ β (π β π΄ β¨ Β¬ π β π΄)) |
88 | 86, 87 | syl 14 |
. . . . . . . . . . 11
β’ ((π β§ π β π΅) β (π β π΄ β¨ Β¬ π β π΄)) |
89 | 69, 81, 88 | mpjaod 718 |
. . . . . . . . . 10
β’ ((π β§ π β π΅) β if(π β π΄, ((π β π΄ β¦ πΆ)βπ), 1) = β¦π / πβ¦πΆ) |
90 | 89, 17 | eqtr4d 2213 |
. . . . . . . . 9
β’ ((π β§ π β π΅) β if(π β π΄, ((π β π΄ β¦ πΆ)βπ), 1) = if(π β π΅, β¦π / πβ¦πΆ, 1)) |
91 | 90 | ex 115 |
. . . . . . . 8
β’ (π β (π β π΅ β if(π β π΄, ((π β π΄ β¦ πΆ)βπ), 1) = if(π β π΅, β¦π / πβ¦πΆ, 1))) |
92 | 4 | ssneld 3157 |
. . . . . . . . . . . 12
β’ (π β (Β¬ π β π΅ β Β¬ π β π΄)) |
93 | 92 | imp 124 |
. . . . . . . . . . 11
β’ ((π β§ Β¬ π β π΅) β Β¬ π β π΄) |
94 | 93, 70 | syl 14 |
. . . . . . . . . 10
β’ ((π β§ Β¬ π β π΅) β if(π β π΄, ((π β π΄ β¦ πΆ)βπ), 1) = 1) |
95 | 44 | adantl 277 |
. . . . . . . . . 10
β’ ((π β§ Β¬ π β π΅) β if(π β π΅, β¦π / πβ¦πΆ, 1) = 1) |
96 | 94, 95 | eqtr4d 2213 |
. . . . . . . . 9
β’ ((π β§ Β¬ π β π΅) β if(π β π΄, ((π β π΄ β¦ πΆ)βπ), 1) = if(π β π΅, β¦π / πβ¦πΆ, 1)) |
97 | 96 | ex 115 |
. . . . . . . 8
β’ (π β (Β¬ π β π΅ β if(π β π΄, ((π β π΄ β¦ πΆ)βπ), 1) = if(π β π΅, β¦π / πβ¦πΆ, 1))) |
98 | 91, 97 | jaod 717 |
. . . . . . 7
β’ (π β ((π β π΅ β¨ Β¬ π β π΅) β if(π β π΄, ((π β π΄ β¦ πΆ)βπ), 1) = if(π β π΅, β¦π / πβ¦πΆ, 1))) |
99 | 98 | adantr 276 |
. . . . . 6
β’ ((π β§ π β (β€β₯βπ)) β ((π β π΅ β¨ Β¬ π β π΅) β if(π β π΄, ((π β π΄ β¦ πΆ)βπ), 1) = if(π β π΅, β¦π / πβ¦πΆ, 1))) |
100 | 15, 99 | mpd 13 |
. . . . 5
β’ ((π β§ π β (β€β₯βπ)) β if(π β π΄, ((π β π΄ β¦ πΆ)βπ), 1) = if(π β π΅, β¦π / πβ¦πΆ, 1)) |
101 | 58, 100 | eqtr4d 2213 |
. . . 4
β’ ((π β§ π β (β€β₯βπ)) β ((π β (β€β₯βπ) β¦ if(π β π΅, πΆ, 1))βπ) = if(π β π΄, ((π β π΄ β¦ πΆ)βπ), 1)) |
102 | 18 | fmpttd 5671 |
. . . . 5
β’ (π β (π β π΄ β¦ πΆ):π΄βΆβ) |
103 | 102 | ffvelcdmda 5651 |
. . . 4
β’ ((π β§ π β π΄) β ((π β π΄ β¦ πΆ)βπ) β β) |
104 | 1, 2, 3, 6, 7, 101, 103 | zproddc 11586 |
. . 3
β’ (π β βπ β π΄ ((π β π΄ β¦ πΆ)βπ) = ( β βseqπ( Β· , (π β (β€β₯βπ) β¦ if(π β π΅, πΆ, 1))))) |
105 | | simpr 110 |
. . . . . . . . . . 11
β’ ((π β§ π β π΅) β π β π΅) |
106 | | eqid 2177 |
. . . . . . . . . . . 12
β’ (π β π΅ β¦ πΆ) = (π β π΅ β¦ πΆ) |
107 | 106 | fvmpts 5594 |
. . . . . . . . . . 11
β’ ((π β π΅ β§ β¦π / πβ¦πΆ β β) β ((π β π΅ β¦ πΆ)βπ) = β¦π / πβ¦πΆ) |
108 | 105, 41, 107 | syl2anc 411 |
. . . . . . . . . 10
β’ ((π β§ π β π΅) β ((π β π΅ β¦ πΆ)βπ) = β¦π / πβ¦πΆ) |
109 | 108 | ifeq1d 3551 |
. . . . . . . . 9
β’ ((π β§ π β π΅) β if(π β π΅, ((π β π΅ β¦ πΆ)βπ), 1) = if(π β π΅, β¦π / πβ¦πΆ, 1)) |
110 | 109 | ex 115 |
. . . . . . . 8
β’ (π β (π β π΅ β if(π β π΅, ((π β π΅ β¦ πΆ)βπ), 1) = if(π β π΅, β¦π / πβ¦πΆ, 1))) |
111 | | iffalse 3542 |
. . . . . . . . . 10
β’ (Β¬
π β π΅ β if(π β π΅, ((π β π΅ β¦ πΆ)βπ), 1) = 1) |
112 | 111, 44 | eqtr4d 2213 |
. . . . . . . . 9
β’ (Β¬
π β π΅ β if(π β π΅, ((π β π΅ β¦ πΆ)βπ), 1) = if(π β π΅, β¦π / πβ¦πΆ, 1)) |
113 | 112 | a1i 9 |
. . . . . . . 8
β’ (π β (Β¬ π β π΅ β if(π β π΅, ((π β π΅ β¦ πΆ)βπ), 1) = if(π β π΅, β¦π / πβ¦πΆ, 1))) |
114 | 110, 113 | jaod 717 |
. . . . . . 7
β’ (π β ((π β π΅ β¨ Β¬ π β π΅) β if(π β π΅, ((π β π΅ β¦ πΆ)βπ), 1) = if(π β π΅, β¦π / πβ¦πΆ, 1))) |
115 | 114 | adantr 276 |
. . . . . 6
β’ ((π β§ π β (β€β₯βπ)) β ((π β π΅ β¨ Β¬ π β π΅) β if(π β π΅, ((π β π΅ β¦ πΆ)βπ), 1) = if(π β π΅, β¦π / πβ¦πΆ, 1))) |
116 | 15, 115 | mpd 13 |
. . . . 5
β’ ((π β§ π β (β€β₯βπ)) β if(π β π΅, ((π β π΅ β¦ πΆ)βπ), 1) = if(π β π΅, β¦π / πβ¦πΆ, 1)) |
117 | 58, 116 | eqtr4d 2213 |
. . . 4
β’ ((π β§ π β (β€β₯βπ)) β ((π β (β€β₯βπ) β¦ if(π β π΅, πΆ, 1))βπ) = if(π β π΅, ((π β π΅ β¦ πΆ)βπ), 1)) |
118 | 34 | fmpttd 5671 |
. . . . 5
β’ (π β (π β π΅ β¦ πΆ):π΅βΆβ) |
119 | 118 | ffvelcdmda 5651 |
. . . 4
β’ ((π β§ π β π΅) β ((π β π΅ β¦ πΆ)βπ) β β) |
120 | 1, 2, 3, 5, 11, 117, 119 | zproddc 11586 |
. . 3
β’ (π β βπ β π΅ ((π β π΅ β¦ πΆ)βπ) = ( β βseqπ( Β· , (π β (β€β₯βπ) β¦ if(π β π΅, πΆ, 1))))) |
121 | 104, 120 | eqtr4d 2213 |
. 2
β’ (π β βπ β π΄ ((π β π΄ β¦ πΆ)βπ) = βπ β π΅ ((π β π΅ β¦ πΆ)βπ)) |
122 | 18 | ralrimiva 2550 |
. . 3
β’ (π β βπ β π΄ πΆ β β) |
123 | | prodfct 11594 |
. . 3
β’
(βπ β
π΄ πΆ β β β βπ β π΄ ((π β π΄ β¦ πΆ)βπ) = βπ β π΄ πΆ) |
124 | 122, 123 | syl 14 |
. 2
β’ (π β βπ β π΄ ((π β π΄ β¦ πΆ)βπ) = βπ β π΄ πΆ) |
125 | | prodfct 11594 |
. . 3
β’
(βπ β
π΅ πΆ β β β βπ β π΅ ((π β π΅ β¦ πΆ)βπ) = βπ β π΅ πΆ) |
126 | 35, 125 | syl 14 |
. 2
β’ (π β βπ β π΅ ((π β π΅ β¦ πΆ)βπ) = βπ β π΅ πΆ) |
127 | 121, 124,
126 | 3eqtr3d 2218 |
1
β’ (π β βπ β π΄ πΆ = βπ β π΅ πΆ) |