Step | Hyp | Ref
| Expression |
1 | | 3simpb 1150 |
. . . . . . 7
โข ((๐ด โ
(โคโฅโ๐) โง โ๐ โ (โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , ๐น) โ ๐ฆ) โง seq๐( ยท , ๐น) โ ๐ฅ) โ (๐ด โ (โคโฅโ๐) โง seq๐( ยท , ๐น) โ ๐ฅ)) |
2 | 1 | reximi 3084 |
. . . . . 6
โข
(โ๐ โ
โค (๐ด โ
(โคโฅโ๐) โง โ๐ โ (โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , ๐น) โ ๐ฆ) โง seq๐( ยท , ๐น) โ ๐ฅ) โ โ๐ โ โค (๐ด โ (โคโฅโ๐) โง seq๐( ยท , ๐น) โ ๐ฅ)) |
3 | | 3simpb 1150 |
. . . . . . 7
โข ((๐ด โ
(โคโฅโ๐) โง โ๐ โ (โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , ๐น) โ ๐ฆ) โง seq๐( ยท , ๐น) โ ๐ง) โ (๐ด โ (โคโฅโ๐) โง seq๐( ยท , ๐น) โ ๐ง)) |
4 | 3 | reximi 3084 |
. . . . . 6
โข
(โ๐ โ
โค (๐ด โ
(โคโฅโ๐) โง โ๐ โ (โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , ๐น) โ ๐ฆ) โง seq๐( ยท , ๐น) โ ๐ง) โ โ๐ โ โค (๐ด โ (โคโฅโ๐) โง seq๐( ยท , ๐น) โ ๐ง)) |
5 | | fveq2 6843 |
. . . . . . . . . . . 12
โข (๐ = ๐ค โ (โคโฅโ๐) =
(โคโฅโ๐ค)) |
6 | 5 | sseq2d 3977 |
. . . . . . . . . . 11
โข (๐ = ๐ค โ (๐ด โ (โคโฅโ๐) โ ๐ด โ (โคโฅโ๐ค))) |
7 | | seqeq1 13915 |
. . . . . . . . . . . 12
โข (๐ = ๐ค โ seq๐( ยท , ๐น) = seq๐ค( ยท , ๐น)) |
8 | 7 | breq1d 5116 |
. . . . . . . . . . 11
โข (๐ = ๐ค โ (seq๐( ยท , ๐น) โ ๐ง โ seq๐ค( ยท , ๐น) โ ๐ง)) |
9 | 6, 8 | anbi12d 632 |
. . . . . . . . . 10
โข (๐ = ๐ค โ ((๐ด โ (โคโฅโ๐) โง seq๐( ยท , ๐น) โ ๐ง) โ (๐ด โ (โคโฅโ๐ค) โง seq๐ค( ยท , ๐น) โ ๐ง))) |
10 | 9 | cbvrexvw 3225 |
. . . . . . . . 9
โข
(โ๐ โ
โค (๐ด โ
(โคโฅโ๐) โง seq๐( ยท , ๐น) โ ๐ง) โ โ๐ค โ โค (๐ด โ (โคโฅโ๐ค) โง seq๐ค( ยท , ๐น) โ ๐ง)) |
11 | 10 | anbi2i 624 |
. . . . . . . 8
โข
((โ๐ โ
โค (๐ด โ
(โคโฅโ๐) โง seq๐( ยท , ๐น) โ ๐ฅ) โง โ๐ โ โค (๐ด โ (โคโฅโ๐) โง seq๐( ยท , ๐น) โ ๐ง)) โ (โ๐ โ โค (๐ด โ (โคโฅโ๐) โง seq๐( ยท , ๐น) โ ๐ฅ) โง โ๐ค โ โค (๐ด โ (โคโฅโ๐ค) โง seq๐ค( ยท , ๐น) โ ๐ง))) |
12 | | reeanv 3216 |
. . . . . . . 8
โข
(โ๐ โ
โค โ๐ค โ
โค ((๐ด โ
(โคโฅโ๐) โง seq๐( ยท , ๐น) โ ๐ฅ) โง (๐ด โ (โคโฅโ๐ค) โง seq๐ค( ยท , ๐น) โ ๐ง)) โ (โ๐ โ โค (๐ด โ (โคโฅโ๐) โง seq๐( ยท , ๐น) โ ๐ฅ) โง โ๐ค โ โค (๐ด โ (โคโฅโ๐ค) โง seq๐ค( ยท , ๐น) โ ๐ง))) |
13 | 11, 12 | bitr4i 278 |
. . . . . . 7
โข
((โ๐ โ
โค (๐ด โ
(โคโฅโ๐) โง seq๐( ยท , ๐น) โ ๐ฅ) โง โ๐ โ โค (๐ด โ (โคโฅโ๐) โง seq๐( ยท , ๐น) โ ๐ง)) โ โ๐ โ โค โ๐ค โ โค ((๐ด โ (โคโฅโ๐) โง seq๐( ยท , ๐น) โ ๐ฅ) โง (๐ด โ (โคโฅโ๐ค) โง seq๐ค( ยท , ๐น) โ ๐ง))) |
14 | | simprlr 779 |
. . . . . . . . . . . . 13
โข (((๐ โ โค โง ๐ค โ โค) โง ((๐ด โ
(โคโฅโ๐) โง seq๐( ยท , ๐น) โ ๐ฅ) โง (๐ด โ (โคโฅโ๐ค) โง seq๐ค( ยท , ๐น) โ ๐ง))) โ seq๐( ยท , ๐น) โ ๐ฅ) |
15 | 14 | adantl 483 |
. . . . . . . . . . . 12
โข ((๐ โง ((๐ โ โค โง ๐ค โ โค) โง ((๐ด โ (โคโฅโ๐) โง seq๐( ยท , ๐น) โ ๐ฅ) โง (๐ด โ (โคโฅโ๐ค) โง seq๐ค( ยท , ๐น) โ ๐ง)))) โ seq๐( ยท , ๐น) โ ๐ฅ) |
16 | | prodmo.1 |
. . . . . . . . . . . . 13
โข ๐น = (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1)) |
17 | | prodmo.2 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) |
18 | 17 | adantlr 714 |
. . . . . . . . . . . . 13
โข (((๐ โง ((๐ โ โค โง ๐ค โ โค) โง ((๐ด โ (โคโฅโ๐) โง seq๐( ยท , ๐น) โ ๐ฅ) โง (๐ด โ (โคโฅโ๐ค) โง seq๐ค( ยท , ๐น) โ ๐ง)))) โง ๐ โ ๐ด) โ ๐ต โ โ) |
19 | | simprll 778 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ โ โค โง ๐ค โ โค) โง ((๐ด โ (โคโฅโ๐) โง seq๐( ยท , ๐น) โ ๐ฅ) โง (๐ด โ (โคโฅโ๐ค) โง seq๐ค( ยท , ๐น) โ ๐ง)))) โ ๐ โ โค) |
20 | | simprlr 779 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ โ โค โง ๐ค โ โค) โง ((๐ด โ (โคโฅโ๐) โง seq๐( ยท , ๐น) โ ๐ฅ) โง (๐ด โ (โคโฅโ๐ค) โง seq๐ค( ยท , ๐น) โ ๐ง)))) โ ๐ค โ โค) |
21 | | simprll 778 |
. . . . . . . . . . . . . 14
โข (((๐ โ โค โง ๐ค โ โค) โง ((๐ด โ
(โคโฅโ๐) โง seq๐( ยท , ๐น) โ ๐ฅ) โง (๐ด โ (โคโฅโ๐ค) โง seq๐ค( ยท , ๐น) โ ๐ง))) โ ๐ด โ (โคโฅโ๐)) |
22 | 21 | adantl 483 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ โ โค โง ๐ค โ โค) โง ((๐ด โ (โคโฅโ๐) โง seq๐( ยท , ๐น) โ ๐ฅ) โง (๐ด โ (โคโฅโ๐ค) โง seq๐ค( ยท , ๐น) โ ๐ง)))) โ ๐ด โ (โคโฅโ๐)) |
23 | | simprrl 780 |
. . . . . . . . . . . . . 14
โข (((๐ โ โค โง ๐ค โ โค) โง ((๐ด โ
(โคโฅโ๐) โง seq๐( ยท , ๐น) โ ๐ฅ) โง (๐ด โ (โคโฅโ๐ค) โง seq๐ค( ยท , ๐น) โ ๐ง))) โ ๐ด โ (โคโฅโ๐ค)) |
24 | 23 | adantl 483 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ โ โค โง ๐ค โ โค) โง ((๐ด โ (โคโฅโ๐) โง seq๐( ยท , ๐น) โ ๐ฅ) โง (๐ด โ (โคโฅโ๐ค) โง seq๐ค( ยท , ๐น) โ ๐ง)))) โ ๐ด โ (โคโฅโ๐ค)) |
25 | 16, 18, 19, 20, 22, 24 | prodrb 15820 |
. . . . . . . . . . . 12
โข ((๐ โง ((๐ โ โค โง ๐ค โ โค) โง ((๐ด โ (โคโฅโ๐) โง seq๐( ยท , ๐น) โ ๐ฅ) โง (๐ด โ (โคโฅโ๐ค) โง seq๐ค( ยท , ๐น) โ ๐ง)))) โ (seq๐( ยท , ๐น) โ ๐ฅ โ seq๐ค( ยท , ๐น) โ ๐ฅ)) |
26 | 15, 25 | mpbid 231 |
. . . . . . . . . . 11
โข ((๐ โง ((๐ โ โค โง ๐ค โ โค) โง ((๐ด โ (โคโฅโ๐) โง seq๐( ยท , ๐น) โ ๐ฅ) โง (๐ด โ (โคโฅโ๐ค) โง seq๐ค( ยท , ๐น) โ ๐ง)))) โ seq๐ค( ยท , ๐น) โ ๐ฅ) |
27 | | simprrr 781 |
. . . . . . . . . . . 12
โข (((๐ โ โค โง ๐ค โ โค) โง ((๐ด โ
(โคโฅโ๐) โง seq๐( ยท , ๐น) โ ๐ฅ) โง (๐ด โ (โคโฅโ๐ค) โง seq๐ค( ยท , ๐น) โ ๐ง))) โ seq๐ค( ยท , ๐น) โ ๐ง) |
28 | 27 | adantl 483 |
. . . . . . . . . . 11
โข ((๐ โง ((๐ โ โค โง ๐ค โ โค) โง ((๐ด โ (โคโฅโ๐) โง seq๐( ยท , ๐น) โ ๐ฅ) โง (๐ด โ (โคโฅโ๐ค) โง seq๐ค( ยท , ๐น) โ ๐ง)))) โ seq๐ค( ยท , ๐น) โ ๐ง) |
29 | | climuni 15440 |
. . . . . . . . . . 11
โข
((seq๐ค( ยท ,
๐น) โ ๐ฅ โง seq๐ค( ยท , ๐น) โ ๐ง) โ ๐ฅ = ๐ง) |
30 | 26, 28, 29 | syl2anc 585 |
. . . . . . . . . 10
โข ((๐ โง ((๐ โ โค โง ๐ค โ โค) โง ((๐ด โ (โคโฅโ๐) โง seq๐( ยท , ๐น) โ ๐ฅ) โง (๐ด โ (โคโฅโ๐ค) โง seq๐ค( ยท , ๐น) โ ๐ง)))) โ ๐ฅ = ๐ง) |
31 | 30 | expcom 415 |
. . . . . . . . 9
โข (((๐ โ โค โง ๐ค โ โค) โง ((๐ด โ
(โคโฅโ๐) โง seq๐( ยท , ๐น) โ ๐ฅ) โง (๐ด โ (โคโฅโ๐ค) โง seq๐ค( ยท , ๐น) โ ๐ง))) โ (๐ โ ๐ฅ = ๐ง)) |
32 | 31 | ex 414 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ค โ โค) โ (((๐ด โ
(โคโฅโ๐) โง seq๐( ยท , ๐น) โ ๐ฅ) โง (๐ด โ (โคโฅโ๐ค) โง seq๐ค( ยท , ๐น) โ ๐ง)) โ (๐ โ ๐ฅ = ๐ง))) |
33 | 32 | rexlimivv 3193 |
. . . . . . 7
โข
(โ๐ โ
โค โ๐ค โ
โค ((๐ด โ
(โคโฅโ๐) โง seq๐( ยท , ๐น) โ ๐ฅ) โง (๐ด โ (โคโฅโ๐ค) โง seq๐ค( ยท , ๐น) โ ๐ง)) โ (๐ โ ๐ฅ = ๐ง)) |
34 | 13, 33 | sylbi 216 |
. . . . . 6
โข
((โ๐ โ
โค (๐ด โ
(โคโฅโ๐) โง seq๐( ยท , ๐น) โ ๐ฅ) โง โ๐ โ โค (๐ด โ (โคโฅโ๐) โง seq๐( ยท , ๐น) โ ๐ง)) โ (๐ โ ๐ฅ = ๐ง)) |
35 | 2, 4, 34 | syl2an 597 |
. . . . 5
โข
((โ๐ โ
โค (๐ด โ
(โคโฅโ๐) โง โ๐ โ (โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , ๐น) โ ๐ฆ) โง seq๐( ยท , ๐น) โ ๐ฅ) โง โ๐ โ โค (๐ด โ (โคโฅโ๐) โง โ๐ โ
(โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , ๐น) โ ๐ฆ) โง seq๐( ยท , ๐น) โ ๐ง)) โ (๐ โ ๐ฅ = ๐ง)) |
36 | | prodmo.3 |
. . . . . . . . . 10
โข ๐บ = (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต) |
37 | 16, 17, 36 | prodmolem2 15823 |
. . . . . . . . 9
โข ((๐ โง โ๐ โ โค (๐ด โ (โคโฅโ๐) โง โ๐ โ
(โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , ๐น) โ ๐ฆ) โง seq๐( ยท , ๐น) โ ๐ง)) โ (โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , ๐บ)โ๐)) โ ๐ง = ๐ฅ)) |
38 | | equcomi 2021 |
. . . . . . . . 9
โข (๐ง = ๐ฅ โ ๐ฅ = ๐ง) |
39 | 37, 38 | syl6 35 |
. . . . . . . 8
โข ((๐ โง โ๐ โ โค (๐ด โ (โคโฅโ๐) โง โ๐ โ
(โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , ๐น) โ ๐ฆ) โง seq๐( ยท , ๐น) โ ๐ง)) โ (โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , ๐บ)โ๐)) โ ๐ฅ = ๐ง)) |
40 | 39 | expimpd 455 |
. . . . . . 7
โข (๐ โ ((โ๐ โ โค (๐ด โ
(โคโฅโ๐) โง โ๐ โ (โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , ๐น) โ ๐ฆ) โง seq๐( ยท , ๐น) โ ๐ง) โง โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , ๐บ)โ๐))) โ ๐ฅ = ๐ง)) |
41 | 40 | com12 32 |
. . . . . 6
โข
((โ๐ โ
โค (๐ด โ
(โคโฅโ๐) โง โ๐ โ (โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , ๐น) โ ๐ฆ) โง seq๐( ยท , ๐น) โ ๐ง) โง โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , ๐บ)โ๐))) โ (๐ โ ๐ฅ = ๐ง)) |
42 | 41 | ancoms 460 |
. . . . 5
โข
((โ๐ โ
โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , ๐บ)โ๐)) โง โ๐ โ โค (๐ด โ (โคโฅโ๐) โง โ๐ โ
(โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , ๐น) โ ๐ฆ) โง seq๐( ยท , ๐น) โ ๐ง)) โ (๐ โ ๐ฅ = ๐ง)) |
43 | 16, 17, 36 | prodmolem2 15823 |
. . . . . . 7
โข ((๐ โง โ๐ โ โค (๐ด โ (โคโฅโ๐) โง โ๐ โ
(โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , ๐น) โ ๐ฆ) โง seq๐( ยท , ๐น) โ ๐ฅ)) โ (โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ง = (seq1( ยท , ๐บ)โ๐)) โ ๐ฅ = ๐ง)) |
44 | 43 | expimpd 455 |
. . . . . 6
โข (๐ โ ((โ๐ โ โค (๐ด โ
(โคโฅโ๐) โง โ๐ โ (โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , ๐น) โ ๐ฆ) โง seq๐( ยท , ๐น) โ ๐ฅ) โง โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ง = (seq1( ยท , ๐บ)โ๐))) โ ๐ฅ = ๐ง)) |
45 | 44 | com12 32 |
. . . . 5
โข
((โ๐ โ
โค (๐ด โ
(โคโฅโ๐) โง โ๐ โ (โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , ๐น) โ ๐ฆ) โง seq๐( ยท , ๐น) โ ๐ฅ) โง โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ง = (seq1( ยท , ๐บ)โ๐))) โ (๐ โ ๐ฅ = ๐ง)) |
46 | | reeanv 3216 |
. . . . . . . 8
โข
(โ๐ โ
โ โ๐ค โ
โ (โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , ๐บ)โ๐)) โง โ๐(๐:(1...๐ค)โ1-1-ontoโ๐ด โง ๐ง = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐ค))) โ (โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , ๐บ)โ๐)) โง โ๐ค โ โ โ๐(๐:(1...๐ค)โ1-1-ontoโ๐ด โง ๐ง = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐ค)))) |
47 | | exdistrv 1960 |
. . . . . . . . 9
โข
(โ๐โ๐((๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , ๐บ)โ๐)) โง (๐:(1...๐ค)โ1-1-ontoโ๐ด โง ๐ง = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐ค))) โ (โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , ๐บ)โ๐)) โง โ๐(๐:(1...๐ค)โ1-1-ontoโ๐ด โง ๐ง = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐ค)))) |
48 | 47 | 2rexbii 3125 |
. . . . . . . 8
โข
(โ๐ โ
โ โ๐ค โ
โ โ๐โ๐((๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , ๐บ)โ๐)) โง (๐:(1...๐ค)โ1-1-ontoโ๐ด โง ๐ง = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐ค))) โ โ๐ โ โ โ๐ค โ โ (โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , ๐บ)โ๐)) โง โ๐(๐:(1...๐ค)โ1-1-ontoโ๐ด โง ๐ง = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐ค)))) |
49 | | oveq2 7366 |
. . . . . . . . . . . . . 14
โข (๐ = ๐ค โ (1...๐) = (1...๐ค)) |
50 | 49 | f1oeq2d 6781 |
. . . . . . . . . . . . 13
โข (๐ = ๐ค โ (๐:(1...๐)โ1-1-ontoโ๐ด โ ๐:(1...๐ค)โ1-1-ontoโ๐ด)) |
51 | | fveq2 6843 |
. . . . . . . . . . . . . 14
โข (๐ = ๐ค โ (seq1( ยท , ๐บ)โ๐) = (seq1( ยท , ๐บ)โ๐ค)) |
52 | 51 | eqeq2d 2744 |
. . . . . . . . . . . . 13
โข (๐ = ๐ค โ (๐ง = (seq1( ยท , ๐บ)โ๐) โ ๐ง = (seq1( ยท , ๐บ)โ๐ค))) |
53 | 50, 52 | anbi12d 632 |
. . . . . . . . . . . 12
โข (๐ = ๐ค โ ((๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ง = (seq1( ยท , ๐บ)โ๐)) โ (๐:(1...๐ค)โ1-1-ontoโ๐ด โง ๐ง = (seq1( ยท , ๐บ)โ๐ค)))) |
54 | 53 | exbidv 1925 |
. . . . . . . . . . 11
โข (๐ = ๐ค โ (โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ง = (seq1( ยท , ๐บ)โ๐)) โ โ๐(๐:(1...๐ค)โ1-1-ontoโ๐ด โง ๐ง = (seq1( ยท , ๐บ)โ๐ค)))) |
55 | | f1oeq1 6773 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ (๐:(1...๐ค)โ1-1-ontoโ๐ด โ ๐:(1...๐ค)โ1-1-ontoโ๐ด)) |
56 | | fveq1 6842 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ = ๐ โ (๐โ๐) = (๐โ๐)) |
57 | 56 | csbeq1d 3860 |
. . . . . . . . . . . . . . . . . 18
โข (๐ = ๐ โ โฆ(๐โ๐) / ๐โฆ๐ต = โฆ(๐โ๐) / ๐โฆ๐ต) |
58 | 57 | mpteq2dv 5208 |
. . . . . . . . . . . . . . . . 17
โข (๐ = ๐ โ (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต) = (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต)) |
59 | 36, 58 | eqtrid 2785 |
. . . . . . . . . . . . . . . 16
โข (๐ = ๐ โ ๐บ = (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต)) |
60 | 59 | seqeq3d 13920 |
. . . . . . . . . . . . . . 15
โข (๐ = ๐ โ seq1( ยท , ๐บ) = seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))) |
61 | 60 | fveq1d 6845 |
. . . . . . . . . . . . . 14
โข (๐ = ๐ โ (seq1( ยท , ๐บ)โ๐ค) = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐ค)) |
62 | 61 | eqeq2d 2744 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ (๐ง = (seq1( ยท , ๐บ)โ๐ค) โ ๐ง = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐ค))) |
63 | 55, 62 | anbi12d 632 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ ((๐:(1...๐ค)โ1-1-ontoโ๐ด โง ๐ง = (seq1( ยท , ๐บ)โ๐ค)) โ (๐:(1...๐ค)โ1-1-ontoโ๐ด โง ๐ง = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐ค)))) |
64 | 63 | cbvexvw 2041 |
. . . . . . . . . . 11
โข
(โ๐(๐:(1...๐ค)โ1-1-ontoโ๐ด โง ๐ง = (seq1( ยท , ๐บ)โ๐ค)) โ โ๐(๐:(1...๐ค)โ1-1-ontoโ๐ด โง ๐ง = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐ค))) |
65 | 54, 64 | bitrdi 287 |
. . . . . . . . . 10
โข (๐ = ๐ค โ (โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ง = (seq1( ยท , ๐บ)โ๐)) โ โ๐(๐:(1...๐ค)โ1-1-ontoโ๐ด โง ๐ง = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐ค)))) |
66 | 65 | cbvrexvw 3225 |
. . . . . . . . 9
โข
(โ๐ โ
โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ง = (seq1( ยท , ๐บ)โ๐)) โ โ๐ค โ โ โ๐(๐:(1...๐ค)โ1-1-ontoโ๐ด โง ๐ง = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐ค))) |
67 | 66 | anbi2i 624 |
. . . . . . . 8
โข
((โ๐ โ
โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , ๐บ)โ๐)) โง โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ง = (seq1( ยท , ๐บ)โ๐))) โ (โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , ๐บ)โ๐)) โง โ๐ค โ โ โ๐(๐:(1...๐ค)โ1-1-ontoโ๐ด โง ๐ง = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐ค)))) |
68 | 46, 48, 67 | 3bitr4i 303 |
. . . . . . 7
โข
(โ๐ โ
โ โ๐ค โ
โ โ๐โ๐((๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , ๐บ)โ๐)) โง (๐:(1...๐ค)โ1-1-ontoโ๐ด โง ๐ง = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐ค))) โ (โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , ๐บ)โ๐)) โง โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ง = (seq1( ยท , ๐บ)โ๐)))) |
69 | | an4 655 |
. . . . . . . . . 10
โข (((๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , ๐บ)โ๐)) โง (๐:(1...๐ค)โ1-1-ontoโ๐ด โง ๐ง = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐ค))) โ ((๐:(1...๐)โ1-1-ontoโ๐ด โง ๐:(1...๐ค)โ1-1-ontoโ๐ด) โง (๐ฅ = (seq1( ยท , ๐บ)โ๐) โง ๐ง = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐ค)))) |
70 | 17 | ad4ant14 751 |
. . . . . . . . . . . . 13
โข ((((๐ โง (๐ โ โ โง ๐ค โ โ)) โง (๐:(1...๐)โ1-1-ontoโ๐ด โง ๐:(1...๐ค)โ1-1-ontoโ๐ด)) โง ๐ โ ๐ด) โ ๐ต โ โ) |
71 | | fveq2 6843 |
. . . . . . . . . . . . . . . 16
โข (๐ = ๐ โ (๐โ๐) = (๐โ๐)) |
72 | 71 | csbeq1d 3860 |
. . . . . . . . . . . . . . 15
โข (๐ = ๐ โ โฆ(๐โ๐) / ๐โฆ๐ต = โฆ(๐โ๐) / ๐โฆ๐ต) |
73 | 72 | cbvmptv 5219 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โฆ
โฆ(๐โ๐) / ๐โฆ๐ต) = (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต) |
74 | 36, 73 | eqtri 2761 |
. . . . . . . . . . . . 13
โข ๐บ = (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต) |
75 | | fveq2 6843 |
. . . . . . . . . . . . . . 15
โข (๐ = ๐ โ (๐โ๐) = (๐โ๐)) |
76 | 75 | csbeq1d 3860 |
. . . . . . . . . . . . . 14
โข (๐ = ๐ โ โฆ(๐โ๐) / ๐โฆ๐ต = โฆ(๐โ๐) / ๐โฆ๐ต) |
77 | 76 | cbvmptv 5219 |
. . . . . . . . . . . . 13
โข (๐ โ โ โฆ
โฆ(๐โ๐) / ๐โฆ๐ต) = (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต) |
78 | | simplr 768 |
. . . . . . . . . . . . 13
โข (((๐ โง (๐ โ โ โง ๐ค โ โ)) โง (๐:(1...๐)โ1-1-ontoโ๐ด โง ๐:(1...๐ค)โ1-1-ontoโ๐ด)) โ (๐ โ โ โง ๐ค โ โ)) |
79 | | simprl 770 |
. . . . . . . . . . . . 13
โข (((๐ โง (๐ โ โ โง ๐ค โ โ)) โง (๐:(1...๐)โ1-1-ontoโ๐ด โง ๐:(1...๐ค)โ1-1-ontoโ๐ด)) โ ๐:(1...๐)โ1-1-ontoโ๐ด) |
80 | | simprr 772 |
. . . . . . . . . . . . 13
โข (((๐ โง (๐ โ โ โง ๐ค โ โ)) โง (๐:(1...๐)โ1-1-ontoโ๐ด โง ๐:(1...๐ค)โ1-1-ontoโ๐ด)) โ ๐:(1...๐ค)โ1-1-ontoโ๐ด) |
81 | 16, 70, 74, 77, 78, 79, 80 | prodmolem3 15821 |
. . . . . . . . . . . 12
โข (((๐ โง (๐ โ โ โง ๐ค โ โ)) โง (๐:(1...๐)โ1-1-ontoโ๐ด โง ๐:(1...๐ค)โ1-1-ontoโ๐ด)) โ (seq1( ยท ,
๐บ)โ๐) = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐ค)) |
82 | | eqeq12 2750 |
. . . . . . . . . . . 12
โข ((๐ฅ = (seq1( ยท , ๐บ)โ๐) โง ๐ง = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐ค)) โ (๐ฅ = ๐ง โ (seq1( ยท , ๐บ)โ๐) = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐ค))) |
83 | 81, 82 | syl5ibrcom 247 |
. . . . . . . . . . 11
โข (((๐ โง (๐ โ โ โง ๐ค โ โ)) โง (๐:(1...๐)โ1-1-ontoโ๐ด โง ๐:(1...๐ค)โ1-1-ontoโ๐ด)) โ ((๐ฅ = (seq1( ยท , ๐บ)โ๐) โง ๐ง = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐ค)) โ ๐ฅ = ๐ง)) |
84 | 83 | expimpd 455 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ โ โง ๐ค โ โ)) โ (((๐:(1...๐)โ1-1-ontoโ๐ด โง ๐:(1...๐ค)โ1-1-ontoโ๐ด) โง (๐ฅ = (seq1( ยท , ๐บ)โ๐) โง ๐ง = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐ค))) โ ๐ฅ = ๐ง)) |
85 | 69, 84 | biimtrid 241 |
. . . . . . . . 9
โข ((๐ โง (๐ โ โ โง ๐ค โ โ)) โ (((๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , ๐บ)โ๐)) โง (๐:(1...๐ค)โ1-1-ontoโ๐ด โง ๐ง = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐ค))) โ ๐ฅ = ๐ง)) |
86 | 85 | exlimdvv 1938 |
. . . . . . . 8
โข ((๐ โง (๐ โ โ โง ๐ค โ โ)) โ (โ๐โ๐((๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , ๐บ)โ๐)) โง (๐:(1...๐ค)โ1-1-ontoโ๐ด โง ๐ง = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐ค))) โ ๐ฅ = ๐ง)) |
87 | 86 | rexlimdvva 3202 |
. . . . . . 7
โข (๐ โ (โ๐ โ โ โ๐ค โ โ โ๐โ๐((๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , ๐บ)โ๐)) โง (๐:(1...๐ค)โ1-1-ontoโ๐ด โง ๐ง = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐ค))) โ ๐ฅ = ๐ง)) |
88 | 68, 87 | biimtrrid 242 |
. . . . . 6
โข (๐ โ ((โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , ๐บ)โ๐)) โง โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ง = (seq1( ยท , ๐บ)โ๐))) โ ๐ฅ = ๐ง)) |
89 | 88 | com12 32 |
. . . . 5
โข
((โ๐ โ
โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , ๐บ)โ๐)) โง โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ง = (seq1( ยท , ๐บ)โ๐))) โ (๐ โ ๐ฅ = ๐ง)) |
90 | 35, 42, 45, 89 | ccase 1037 |
. . . 4
โข
(((โ๐ โ
โค (๐ด โ
(โคโฅโ๐) โง โ๐ โ (โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , ๐น) โ ๐ฆ) โง seq๐( ยท , ๐น) โ ๐ฅ) โจ โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , ๐บ)โ๐))) โง (โ๐ โ โค (๐ด โ (โคโฅโ๐) โง โ๐ โ
(โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , ๐น) โ ๐ฆ) โง seq๐( ยท , ๐น) โ ๐ง) โจ โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ง = (seq1( ยท , ๐บ)โ๐)))) โ (๐ โ ๐ฅ = ๐ง)) |
91 | 90 | com12 32 |
. . 3
โข (๐ โ (((โ๐ โ โค (๐ด โ
(โคโฅโ๐) โง โ๐ โ (โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , ๐น) โ ๐ฆ) โง seq๐( ยท , ๐น) โ ๐ฅ) โจ โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , ๐บ)โ๐))) โง (โ๐ โ โค (๐ด โ (โคโฅโ๐) โง โ๐ โ
(โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , ๐น) โ ๐ฆ) โง seq๐( ยท , ๐น) โ ๐ง) โจ โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ง = (seq1( ยท , ๐บ)โ๐)))) โ ๐ฅ = ๐ง)) |
92 | 91 | alrimivv 1932 |
. 2
โข (๐ โ โ๐ฅโ๐ง(((โ๐ โ โค (๐ด โ (โคโฅโ๐) โง โ๐ โ
(โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , ๐น) โ ๐ฆ) โง seq๐( ยท , ๐น) โ ๐ฅ) โจ โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , ๐บ)โ๐))) โง (โ๐ โ โค (๐ด โ (โคโฅโ๐) โง โ๐ โ
(โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , ๐น) โ ๐ฆ) โง seq๐( ยท , ๐น) โ ๐ง) โจ โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ง = (seq1( ยท , ๐บ)โ๐)))) โ ๐ฅ = ๐ง)) |
93 | | breq2 5110 |
. . . . . 6
โข (๐ฅ = ๐ง โ (seq๐( ยท , ๐น) โ ๐ฅ โ seq๐( ยท , ๐น) โ ๐ง)) |
94 | 93 | 3anbi3d 1443 |
. . . . 5
โข (๐ฅ = ๐ง โ ((๐ด โ (โคโฅโ๐) โง โ๐ โ
(โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , ๐น) โ ๐ฆ) โง seq๐( ยท , ๐น) โ ๐ฅ) โ (๐ด โ (โคโฅโ๐) โง โ๐ โ
(โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , ๐น) โ ๐ฆ) โง seq๐( ยท , ๐น) โ ๐ง))) |
95 | 94 | rexbidv 3172 |
. . . 4
โข (๐ฅ = ๐ง โ (โ๐ โ โค (๐ด โ (โคโฅโ๐) โง โ๐ โ
(โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , ๐น) โ ๐ฆ) โง seq๐( ยท , ๐น) โ ๐ฅ) โ โ๐ โ โค (๐ด โ (โคโฅโ๐) โง โ๐ โ
(โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , ๐น) โ ๐ฆ) โง seq๐( ยท , ๐น) โ ๐ง))) |
96 | | eqeq1 2737 |
. . . . . . 7
โข (๐ฅ = ๐ง โ (๐ฅ = (seq1( ยท , ๐บ)โ๐) โ ๐ง = (seq1( ยท , ๐บ)โ๐))) |
97 | 96 | anbi2d 630 |
. . . . . 6
โข (๐ฅ = ๐ง โ ((๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , ๐บ)โ๐)) โ (๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ง = (seq1( ยท , ๐บ)โ๐)))) |
98 | 97 | exbidv 1925 |
. . . . 5
โข (๐ฅ = ๐ง โ (โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , ๐บ)โ๐)) โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ง = (seq1( ยท , ๐บ)โ๐)))) |
99 | 98 | rexbidv 3172 |
. . . 4
โข (๐ฅ = ๐ง โ (โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , ๐บ)โ๐)) โ โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ง = (seq1( ยท , ๐บ)โ๐)))) |
100 | 95, 99 | orbi12d 918 |
. . 3
โข (๐ฅ = ๐ง โ ((โ๐ โ โค (๐ด โ (โคโฅโ๐) โง โ๐ โ
(โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , ๐น) โ ๐ฆ) โง seq๐( ยท , ๐น) โ ๐ฅ) โจ โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , ๐บ)โ๐))) โ (โ๐ โ โค (๐ด โ (โคโฅโ๐) โง โ๐ โ
(โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , ๐น) โ ๐ฆ) โง seq๐( ยท , ๐น) โ ๐ง) โจ โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ง = (seq1( ยท , ๐บ)โ๐))))) |
101 | 100 | mo4 2561 |
. 2
โข
(โ*๐ฅ(โ๐ โ โค (๐ด โ (โคโฅโ๐) โง โ๐ โ
(โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , ๐น) โ ๐ฆ) โง seq๐( ยท , ๐น) โ ๐ฅ) โจ โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , ๐บ)โ๐))) โ โ๐ฅโ๐ง(((โ๐ โ โค (๐ด โ (โคโฅโ๐) โง โ๐ โ
(โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , ๐น) โ ๐ฆ) โง seq๐( ยท , ๐น) โ ๐ฅ) โจ โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , ๐บ)โ๐))) โง (โ๐ โ โค (๐ด โ (โคโฅโ๐) โง โ๐ โ
(โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , ๐น) โ ๐ฆ) โง seq๐( ยท , ๐น) โ ๐ง) โจ โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ง = (seq1( ยท , ๐บ)โ๐)))) โ ๐ฅ = ๐ง)) |
102 | 92, 101 | sylibr 233 |
1
โข (๐ โ โ*๐ฅ(โ๐ โ โค (๐ด โ (โคโฅโ๐) โง โ๐ โ
(โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , ๐น) โ ๐ฆ) โง seq๐( ยท , ๐น) โ ๐ฅ) โจ โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , ๐บ)โ๐)))) |