Step | Hyp | Ref
| Expression |
1 | | prodeq1 15793 |
. . 3
โข (๐ฅ = โ
โ โ๐ โ ๐ฅ (๐ตโ๐) = โ๐ โ โ
(๐ตโ๐)) |
2 | | prodeq1 15793 |
. . . 4
โข (๐ฅ = โ
โ โ๐ โ ๐ฅ ๐ต = โ๐ โ โ
๐ต) |
3 | 2 | oveq1d 7373 |
. . 3
โข (๐ฅ = โ
โ (โ๐ โ ๐ฅ ๐ตโ๐) = (โ๐ โ โ
๐ตโ๐)) |
4 | 1, 3 | eqeq12d 2753 |
. 2
โข (๐ฅ = โ
โ (โ๐ โ ๐ฅ (๐ตโ๐) = (โ๐ โ ๐ฅ ๐ตโ๐) โ โ๐ โ โ
(๐ตโ๐) = (โ๐ โ โ
๐ตโ๐))) |
5 | | prodeq1 15793 |
. . 3
โข (๐ฅ = ๐ฆ โ โ๐ โ ๐ฅ (๐ตโ๐) = โ๐ โ ๐ฆ (๐ตโ๐)) |
6 | | prodeq1 15793 |
. . . 4
โข (๐ฅ = ๐ฆ โ โ๐ โ ๐ฅ ๐ต = โ๐ โ ๐ฆ ๐ต) |
7 | 6 | oveq1d 7373 |
. . 3
โข (๐ฅ = ๐ฆ โ (โ๐ โ ๐ฅ ๐ตโ๐) = (โ๐ โ ๐ฆ ๐ตโ๐)) |
8 | 5, 7 | eqeq12d 2753 |
. 2
โข (๐ฅ = ๐ฆ โ (โ๐ โ ๐ฅ (๐ตโ๐) = (โ๐ โ ๐ฅ ๐ตโ๐) โ โ๐ โ ๐ฆ (๐ตโ๐) = (โ๐ โ ๐ฆ ๐ตโ๐))) |
9 | | prodeq1 15793 |
. . 3
โข (๐ฅ = (๐ฆ โช {๐ง}) โ โ๐ โ ๐ฅ (๐ตโ๐) = โ๐ โ (๐ฆ โช {๐ง})(๐ตโ๐)) |
10 | | prodeq1 15793 |
. . . 4
โข (๐ฅ = (๐ฆ โช {๐ง}) โ โ๐ โ ๐ฅ ๐ต = โ๐ โ (๐ฆ โช {๐ง})๐ต) |
11 | 10 | oveq1d 7373 |
. . 3
โข (๐ฅ = (๐ฆ โช {๐ง}) โ (โ๐ โ ๐ฅ ๐ตโ๐) = (โ๐ โ (๐ฆ โช {๐ง})๐ตโ๐)) |
12 | 9, 11 | eqeq12d 2753 |
. 2
โข (๐ฅ = (๐ฆ โช {๐ง}) โ (โ๐ โ ๐ฅ (๐ตโ๐) = (โ๐ โ ๐ฅ ๐ตโ๐) โ โ๐ โ (๐ฆ โช {๐ง})(๐ตโ๐) = (โ๐ โ (๐ฆ โช {๐ง})๐ตโ๐))) |
13 | | prodeq1 15793 |
. . 3
โข (๐ฅ = ๐ด โ โ๐ โ ๐ฅ (๐ตโ๐) = โ๐ โ ๐ด (๐ตโ๐)) |
14 | | prodeq1 15793 |
. . . 4
โข (๐ฅ = ๐ด โ โ๐ โ ๐ฅ ๐ต = โ๐ โ ๐ด ๐ต) |
15 | 14 | oveq1d 7373 |
. . 3
โข (๐ฅ = ๐ด โ (โ๐ โ ๐ฅ ๐ตโ๐) = (โ๐ โ ๐ด ๐ตโ๐)) |
16 | 13, 15 | eqeq12d 2753 |
. 2
โข (๐ฅ = ๐ด โ (โ๐ โ ๐ฅ (๐ตโ๐) = (โ๐ โ ๐ฅ ๐ตโ๐) โ โ๐ โ ๐ด (๐ตโ๐) = (โ๐ โ ๐ด ๐ตโ๐))) |
17 | | fprodexp.n |
. . . . . 6
โข (๐ โ ๐ โ
โ0) |
18 | 17 | nn0zd 12526 |
. . . . 5
โข (๐ โ ๐ โ โค) |
19 | | 1exp 13998 |
. . . . 5
โข (๐ โ โค โ
(1โ๐) =
1) |
20 | 18, 19 | syl 17 |
. . . 4
โข (๐ โ (1โ๐) = 1) |
21 | 20 | eqcomd 2743 |
. . 3
โข (๐ โ 1 = (1โ๐)) |
22 | | prod0 15827 |
. . . 4
โข
โ๐ โ
โ
(๐ตโ๐) = 1 |
23 | 22 | a1i 11 |
. . 3
โข (๐ โ โ๐ โ โ
(๐ตโ๐) = 1) |
24 | | prod0 15827 |
. . . . 5
โข
โ๐ โ
โ
๐ต =
1 |
25 | 24 | oveq1i 7368 |
. . . 4
โข
(โ๐ โ
โ
๐ตโ๐) = (1โ๐) |
26 | 25 | a1i 11 |
. . 3
โข (๐ โ (โ๐ โ โ
๐ตโ๐) = (1โ๐)) |
27 | 21, 23, 26 | 3eqtr4d 2787 |
. 2
โข (๐ โ โ๐ โ โ
(๐ตโ๐) = (โ๐ โ โ
๐ตโ๐)) |
28 | | fprodexp.kph |
. . . . . . . . 9
โข
โฒ๐๐ |
29 | | nfv 1918 |
. . . . . . . . 9
โข
โฒ๐(๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ)) |
30 | 28, 29 | nfan 1903 |
. . . . . . . 8
โข
โฒ๐(๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) |
31 | | fprodexp.a |
. . . . . . . . . . 11
โข (๐ โ ๐ด โ Fin) |
32 | 31 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง ๐ฆ โ ๐ด) โ ๐ด โ Fin) |
33 | | simpr 486 |
. . . . . . . . . 10
โข ((๐ โง ๐ฆ โ ๐ด) โ ๐ฆ โ ๐ด) |
34 | | ssfi 9118 |
. . . . . . . . . 10
โข ((๐ด โ Fin โง ๐ฆ โ ๐ด) โ ๐ฆ โ Fin) |
35 | 32, 33, 34 | syl2anc 585 |
. . . . . . . . 9
โข ((๐ โง ๐ฆ โ ๐ด) โ ๐ฆ โ Fin) |
36 | 35 | adantrr 716 |
. . . . . . . 8
โข ((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ ๐ฆ โ Fin) |
37 | | simpll 766 |
. . . . . . . . . 10
โข (((๐ โง ๐ฆ โ ๐ด) โง ๐ โ ๐ฆ) โ ๐) |
38 | 33 | sselda 3945 |
. . . . . . . . . 10
โข (((๐ โง ๐ฆ โ ๐ด) โง ๐ โ ๐ฆ) โ ๐ โ ๐ด) |
39 | | fprodexp.b |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) |
40 | 37, 38, 39 | syl2anc 585 |
. . . . . . . . 9
โข (((๐ โง ๐ฆ โ ๐ด) โง ๐ โ ๐ฆ) โ ๐ต โ โ) |
41 | 40 | adantlrr 720 |
. . . . . . . 8
โข (((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง ๐ โ ๐ฆ) โ ๐ต โ โ) |
42 | 30, 36, 41 | fprodclf 15876 |
. . . . . . 7
โข ((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ โ๐ โ ๐ฆ ๐ต โ โ) |
43 | | simpl 484 |
. . . . . . . 8
โข ((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ ๐) |
44 | | simprr 772 |
. . . . . . . . 9
โข ((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ ๐ง โ (๐ด โ ๐ฆ)) |
45 | 44 | eldifad 3923 |
. . . . . . . 8
โข ((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ ๐ง โ ๐ด) |
46 | | nfv 1918 |
. . . . . . . . . . 11
โข
โฒ๐ ๐ง โ ๐ด |
47 | 28, 46 | nfan 1903 |
. . . . . . . . . 10
โข
โฒ๐(๐ โง ๐ง โ ๐ด) |
48 | | nfcsb1v 3881 |
. . . . . . . . . . 11
โข
โฒ๐โฆ๐ง / ๐โฆ๐ต |
49 | 48 | nfel1 2924 |
. . . . . . . . . 10
โข
โฒ๐โฆ๐ง / ๐โฆ๐ต โ โ |
50 | 47, 49 | nfim 1900 |
. . . . . . . . 9
โข
โฒ๐((๐ โง ๐ง โ ๐ด) โ โฆ๐ง / ๐โฆ๐ต โ โ) |
51 | | eleq1w 2821 |
. . . . . . . . . . 11
โข (๐ = ๐ง โ (๐ โ ๐ด โ ๐ง โ ๐ด)) |
52 | 51 | anbi2d 630 |
. . . . . . . . . 10
โข (๐ = ๐ง โ ((๐ โง ๐ โ ๐ด) โ (๐ โง ๐ง โ ๐ด))) |
53 | | csbeq1a 3870 |
. . . . . . . . . . 11
โข (๐ = ๐ง โ ๐ต = โฆ๐ง / ๐โฆ๐ต) |
54 | 53 | eleq1d 2823 |
. . . . . . . . . 10
โข (๐ = ๐ง โ (๐ต โ โ โ โฆ๐ง / ๐โฆ๐ต โ โ)) |
55 | 52, 54 | imbi12d 345 |
. . . . . . . . 9
โข (๐ = ๐ง โ (((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) โ ((๐ โง ๐ง โ ๐ด) โ โฆ๐ง / ๐โฆ๐ต โ โ))) |
56 | 50, 55, 39 | chvarfv 2234 |
. . . . . . . 8
โข ((๐ โง ๐ง โ ๐ด) โ โฆ๐ง / ๐โฆ๐ต โ โ) |
57 | 43, 45, 56 | syl2anc 585 |
. . . . . . 7
โข ((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ โฆ๐ง / ๐โฆ๐ต โ โ) |
58 | 17 | adantr 482 |
. . . . . . 7
โข ((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ ๐ โ
โ0) |
59 | | mulexp 14008 |
. . . . . . 7
โข
((โ๐ โ
๐ฆ ๐ต โ โ โง โฆ๐ง / ๐โฆ๐ต โ โ โง ๐ โ โ0) โ
((โ๐ โ ๐ฆ ๐ต ยท โฆ๐ง / ๐โฆ๐ต)โ๐) = ((โ๐ โ ๐ฆ ๐ตโ๐) ยท (โฆ๐ง / ๐โฆ๐ตโ๐))) |
60 | 42, 57, 58, 59 | syl3anc 1372 |
. . . . . 6
โข ((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ ((โ๐ โ ๐ฆ ๐ต ยท โฆ๐ง / ๐โฆ๐ต)โ๐) = ((โ๐ โ ๐ฆ ๐ตโ๐) ยท (โฆ๐ง / ๐โฆ๐ตโ๐))) |
61 | 60 | eqcomd 2743 |
. . . . 5
โข ((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ ((โ๐ โ ๐ฆ ๐ตโ๐) ยท (โฆ๐ง / ๐โฆ๐ตโ๐)) = ((โ๐ โ ๐ฆ ๐ต ยท โฆ๐ง / ๐โฆ๐ต)โ๐)) |
62 | 61 | adantr 482 |
. . . 4
โข (((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง โ๐ โ ๐ฆ (๐ตโ๐) = (โ๐ โ ๐ฆ ๐ตโ๐)) โ ((โ๐ โ ๐ฆ ๐ตโ๐) ยท (โฆ๐ง / ๐โฆ๐ตโ๐)) = ((โ๐ โ ๐ฆ ๐ต ยท โฆ๐ง / ๐โฆ๐ต)โ๐)) |
63 | | nfcv 2908 |
. . . . . . . 8
โข
โฒ๐โ |
64 | | nfcv 2908 |
. . . . . . . 8
โข
โฒ๐๐ |
65 | 48, 63, 64 | nfov 7388 |
. . . . . . 7
โข
โฒ๐(โฆ๐ง / ๐โฆ๐ตโ๐) |
66 | 44 | eldifbd 3924 |
. . . . . . 7
โข ((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ ยฌ ๐ง โ ๐ฆ) |
67 | 17 | ad2antrr 725 |
. . . . . . . . 9
โข (((๐ โง ๐ฆ โ ๐ด) โง ๐ โ ๐ฆ) โ ๐ โ
โ0) |
68 | 40, 67 | expcld 14052 |
. . . . . . . 8
โข (((๐ โง ๐ฆ โ ๐ด) โง ๐ โ ๐ฆ) โ (๐ตโ๐) โ โ) |
69 | 68 | adantlrr 720 |
. . . . . . 7
โข (((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง ๐ โ ๐ฆ) โ (๐ตโ๐) โ โ) |
70 | 53 | oveq1d 7373 |
. . . . . . 7
โข (๐ = ๐ง โ (๐ตโ๐) = (โฆ๐ง / ๐โฆ๐ตโ๐)) |
71 | 57, 58 | expcld 14052 |
. . . . . . 7
โข ((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ (โฆ๐ง / ๐โฆ๐ตโ๐) โ โ) |
72 | 30, 65, 36, 44, 66, 69, 70, 71 | fprodsplitsn 15873 |
. . . . . 6
โข ((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ โ๐ โ (๐ฆ โช {๐ง})(๐ตโ๐) = (โ๐ โ ๐ฆ (๐ตโ๐) ยท (โฆ๐ง / ๐โฆ๐ตโ๐))) |
73 | 72 | adantr 482 |
. . . . 5
โข (((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง โ๐ โ ๐ฆ (๐ตโ๐) = (โ๐ โ ๐ฆ ๐ตโ๐)) โ โ๐ โ (๐ฆ โช {๐ง})(๐ตโ๐) = (โ๐ โ ๐ฆ (๐ตโ๐) ยท (โฆ๐ง / ๐โฆ๐ตโ๐))) |
74 | | oveq1 7365 |
. . . . . 6
โข
(โ๐ โ
๐ฆ (๐ตโ๐) = (โ๐ โ ๐ฆ ๐ตโ๐) โ (โ๐ โ ๐ฆ (๐ตโ๐) ยท (โฆ๐ง / ๐โฆ๐ตโ๐)) = ((โ๐ โ ๐ฆ ๐ตโ๐) ยท (โฆ๐ง / ๐โฆ๐ตโ๐))) |
75 | 74 | adantl 483 |
. . . . 5
โข (((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง โ๐ โ ๐ฆ (๐ตโ๐) = (โ๐ โ ๐ฆ ๐ตโ๐)) โ (โ๐ โ ๐ฆ (๐ตโ๐) ยท (โฆ๐ง / ๐โฆ๐ตโ๐)) = ((โ๐ โ ๐ฆ ๐ตโ๐) ยท (โฆ๐ง / ๐โฆ๐ตโ๐))) |
76 | 73, 75 | eqtrd 2777 |
. . . 4
โข (((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง โ๐ โ ๐ฆ (๐ตโ๐) = (โ๐ โ ๐ฆ ๐ตโ๐)) โ โ๐ โ (๐ฆ โช {๐ง})(๐ตโ๐) = ((โ๐ โ ๐ฆ ๐ตโ๐) ยท (โฆ๐ง / ๐โฆ๐ตโ๐))) |
77 | 30, 48, 36, 44, 66, 41, 53, 57 | fprodsplitsn 15873 |
. . . . . 6
โข ((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ โ๐ โ (๐ฆ โช {๐ง})๐ต = (โ๐ โ ๐ฆ ๐ต ยท โฆ๐ง / ๐โฆ๐ต)) |
78 | 77 | adantr 482 |
. . . . 5
โข (((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง โ๐ โ ๐ฆ (๐ตโ๐) = (โ๐ โ ๐ฆ ๐ตโ๐)) โ โ๐ โ (๐ฆ โช {๐ง})๐ต = (โ๐ โ ๐ฆ ๐ต ยท โฆ๐ง / ๐โฆ๐ต)) |
79 | 78 | oveq1d 7373 |
. . . 4
โข (((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง โ๐ โ ๐ฆ (๐ตโ๐) = (โ๐ โ ๐ฆ ๐ตโ๐)) โ (โ๐ โ (๐ฆ โช {๐ง})๐ตโ๐) = ((โ๐ โ ๐ฆ ๐ต ยท โฆ๐ง / ๐โฆ๐ต)โ๐)) |
80 | 62, 76, 79 | 3eqtr4d 2787 |
. . 3
โข (((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง โ๐ โ ๐ฆ (๐ตโ๐) = (โ๐ โ ๐ฆ ๐ตโ๐)) โ โ๐ โ (๐ฆ โช {๐ง})(๐ตโ๐) = (โ๐ โ (๐ฆ โช {๐ง})๐ตโ๐)) |
81 | 80 | ex 414 |
. 2
โข ((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ (โ๐ โ ๐ฆ (๐ตโ๐) = (โ๐ โ ๐ฆ ๐ตโ๐) โ โ๐ โ (๐ฆ โช {๐ง})(๐ตโ๐) = (โ๐ โ (๐ฆ โช {๐ง})๐ตโ๐))) |
82 | 4, 8, 12, 16, 27, 81, 31 | findcard2d 9111 |
1
โข (๐ โ โ๐ โ ๐ด (๐ตโ๐) = (โ๐ โ ๐ด ๐ตโ๐)) |