Step | Hyp | Ref
| Expression |
1 | | prodeq1 11563 |
. . 3
โข (๐ค = โ
โ โ๐ โ ๐ค (1 / ๐ต) = โ๐ โ โ
(1 / ๐ต)) |
2 | | prodeq1 11563 |
. . . 4
โข (๐ค = โ
โ โ๐ โ ๐ค ๐ต = โ๐ โ โ
๐ต) |
3 | 2 | oveq2d 5893 |
. . 3
โข (๐ค = โ
โ (1 /
โ๐ โ ๐ค ๐ต) = (1 / โ๐ โ โ
๐ต)) |
4 | 1, 3 | eqeq12d 2192 |
. 2
โข (๐ค = โ
โ (โ๐ โ ๐ค (1 / ๐ต) = (1 / โ๐ โ ๐ค ๐ต) โ โ๐ โ โ
(1 / ๐ต) = (1 / โ๐ โ โ
๐ต))) |
5 | | prodeq1 11563 |
. . 3
โข (๐ค = ๐ฆ โ โ๐ โ ๐ค (1 / ๐ต) = โ๐ โ ๐ฆ (1 / ๐ต)) |
6 | | prodeq1 11563 |
. . . 4
โข (๐ค = ๐ฆ โ โ๐ โ ๐ค ๐ต = โ๐ โ ๐ฆ ๐ต) |
7 | 6 | oveq2d 5893 |
. . 3
โข (๐ค = ๐ฆ โ (1 / โ๐ โ ๐ค ๐ต) = (1 / โ๐ โ ๐ฆ ๐ต)) |
8 | 5, 7 | eqeq12d 2192 |
. 2
โข (๐ค = ๐ฆ โ (โ๐ โ ๐ค (1 / ๐ต) = (1 / โ๐ โ ๐ค ๐ต) โ โ๐ โ ๐ฆ (1 / ๐ต) = (1 / โ๐ โ ๐ฆ ๐ต))) |
9 | | prodeq1 11563 |
. . 3
โข (๐ค = (๐ฆ โช {๐ง}) โ โ๐ โ ๐ค (1 / ๐ต) = โ๐ โ (๐ฆ โช {๐ง})(1 / ๐ต)) |
10 | | prodeq1 11563 |
. . . 4
โข (๐ค = (๐ฆ โช {๐ง}) โ โ๐ โ ๐ค ๐ต = โ๐ โ (๐ฆ โช {๐ง})๐ต) |
11 | 10 | oveq2d 5893 |
. . 3
โข (๐ค = (๐ฆ โช {๐ง}) โ (1 / โ๐ โ ๐ค ๐ต) = (1 / โ๐ โ (๐ฆ โช {๐ง})๐ต)) |
12 | 9, 11 | eqeq12d 2192 |
. 2
โข (๐ค = (๐ฆ โช {๐ง}) โ (โ๐ โ ๐ค (1 / ๐ต) = (1 / โ๐ โ ๐ค ๐ต) โ โ๐ โ (๐ฆ โช {๐ง})(1 / ๐ต) = (1 / โ๐ โ (๐ฆ โช {๐ง})๐ต))) |
13 | | prodeq1 11563 |
. . 3
โข (๐ค = ๐ด โ โ๐ โ ๐ค (1 / ๐ต) = โ๐ โ ๐ด (1 / ๐ต)) |
14 | | prodeq1 11563 |
. . . 4
โข (๐ค = ๐ด โ โ๐ โ ๐ค ๐ต = โ๐ โ ๐ด ๐ต) |
15 | 14 | oveq2d 5893 |
. . 3
โข (๐ค = ๐ด โ (1 / โ๐ โ ๐ค ๐ต) = (1 / โ๐ โ ๐ด ๐ต)) |
16 | 13, 15 | eqeq12d 2192 |
. 2
โข (๐ค = ๐ด โ (โ๐ โ ๐ค (1 / ๐ต) = (1 / โ๐ โ ๐ค ๐ต) โ โ๐ โ ๐ด (1 / ๐ต) = (1 / โ๐ โ ๐ด ๐ต))) |
17 | | 1div1e1 8663 |
. . . 4
โข (1 / 1) =
1 |
18 | | prod0 11595 |
. . . . 5
โข
โ๐ โ
โ
๐ต =
1 |
19 | 18 | oveq2i 5888 |
. . . 4
โข (1 /
โ๐ โ โ
๐ต) = (1 /
1) |
20 | | prod0 11595 |
. . . 4
โข
โ๐ โ
โ
(1 / ๐ต) =
1 |
21 | 17, 19, 20 | 3eqtr4ri 2209 |
. . 3
โข
โ๐ โ
โ
(1 / ๐ต) = (1 /
โ๐ โ โ
๐ต) |
22 | 21 | a1i 9 |
. 2
โข (๐ โ โ๐ โ โ
(1 / ๐ต) = (1 / โ๐ โ โ
๐ต)) |
23 | | simpr 110 |
. . . . . 6
โข ((((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง โ๐ โ ๐ฆ (1 / ๐ต) = (1 / โ๐ โ ๐ฆ ๐ต)) โ โ๐ โ ๐ฆ (1 / ๐ต) = (1 / โ๐ โ ๐ฆ ๐ต)) |
24 | 23 | oveq1d 5892 |
. . . . 5
โข ((((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง โ๐ โ ๐ฆ (1 / ๐ต) = (1 / โ๐ โ ๐ฆ ๐ต)) โ (โ๐ โ ๐ฆ (1 / ๐ต) ยท (1 / โฆ๐ง / ๐โฆ๐ต)) = ((1 / โ๐ โ ๐ฆ ๐ต) ยท (1 / โฆ๐ง / ๐โฆ๐ต))) |
25 | | 1cnd 7975 |
. . . . . . 7
โข ((((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง โ๐ โ ๐ฆ (1 / ๐ต) = (1 / โ๐ โ ๐ฆ ๐ต)) โ 1 โ โ) |
26 | | simplr 528 |
. . . . . . . . 9
โข (((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ ๐ฆ โ Fin) |
27 | | simplll 533 |
. . . . . . . . . 10
โข ((((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง ๐ โ ๐ฆ) โ ๐) |
28 | | simplrl 535 |
. . . . . . . . . . 11
โข ((((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง ๐ โ ๐ฆ) โ ๐ฆ โ ๐ด) |
29 | | simpr 110 |
. . . . . . . . . . 11
โข ((((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง ๐ โ ๐ฆ) โ ๐ โ ๐ฆ) |
30 | 28, 29 | sseldd 3158 |
. . . . . . . . . 10
โข ((((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง ๐ โ ๐ฆ) โ ๐ โ ๐ด) |
31 | | fprodrec.ccl |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) |
32 | 27, 30, 31 | syl2anc 411 |
. . . . . . . . 9
โข ((((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง ๐ โ ๐ฆ) โ ๐ต โ โ) |
33 | 26, 32 | fprodcl 11617 |
. . . . . . . 8
โข (((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ โ๐ โ ๐ฆ ๐ต โ โ) |
34 | 33 | adantr 276 |
. . . . . . 7
โข ((((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง โ๐ โ ๐ฆ (1 / ๐ต) = (1 / โ๐ โ ๐ฆ ๐ต)) โ โ๐ โ ๐ฆ ๐ต โ โ) |
35 | | simprr 531 |
. . . . . . . . . 10
โข (((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ ๐ง โ (๐ด โ ๐ฆ)) |
36 | 35 | eldifad 3142 |
. . . . . . . . 9
โข (((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ ๐ง โ ๐ด) |
37 | 31 | ralrimiva 2550 |
. . . . . . . . . 10
โข (๐ โ โ๐ โ ๐ด ๐ต โ โ) |
38 | 37 | ad2antrr 488 |
. . . . . . . . 9
โข (((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ โ๐ โ ๐ด ๐ต โ โ) |
39 | | nfcsb1v 3092 |
. . . . . . . . . . 11
โข
โฒ๐โฆ๐ง / ๐โฆ๐ต |
40 | 39 | nfel1 2330 |
. . . . . . . . . 10
โข
โฒ๐โฆ๐ง / ๐โฆ๐ต โ โ |
41 | | csbeq1a 3068 |
. . . . . . . . . . 11
โข (๐ = ๐ง โ ๐ต = โฆ๐ง / ๐โฆ๐ต) |
42 | 41 | eleq1d 2246 |
. . . . . . . . . 10
โข (๐ = ๐ง โ (๐ต โ โ โ โฆ๐ง / ๐โฆ๐ต โ โ)) |
43 | 40, 42 | rspc 2837 |
. . . . . . . . 9
โข (๐ง โ ๐ด โ (โ๐ โ ๐ด ๐ต โ โ โ โฆ๐ง / ๐โฆ๐ต โ โ)) |
44 | 36, 38, 43 | sylc 62 |
. . . . . . . 8
โข (((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ โฆ๐ง / ๐โฆ๐ต โ โ) |
45 | 44 | adantr 276 |
. . . . . . 7
โข ((((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง โ๐ โ ๐ฆ (1 / ๐ต) = (1 / โ๐ โ ๐ฆ ๐ต)) โ โฆ๐ง / ๐โฆ๐ต โ โ) |
46 | | fprodrec.cap |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ๐ด) โ ๐ต # 0) |
47 | 27, 30, 46 | syl2anc 411 |
. . . . . . . . 9
โข ((((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง ๐ โ ๐ฆ) โ ๐ต # 0) |
48 | 26, 32, 47 | fprodap0 11631 |
. . . . . . . 8
โข (((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ โ๐ โ ๐ฆ ๐ต # 0) |
49 | 48 | adantr 276 |
. . . . . . 7
โข ((((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง โ๐ โ ๐ฆ (1 / ๐ต) = (1 / โ๐ โ ๐ฆ ๐ต)) โ โ๐ โ ๐ฆ ๐ต # 0) |
50 | 46 | ralrimiva 2550 |
. . . . . . . . . 10
โข (๐ โ โ๐ โ ๐ด ๐ต # 0) |
51 | 50 | ad2antrr 488 |
. . . . . . . . 9
โข (((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ โ๐ โ ๐ด ๐ต # 0) |
52 | | nfcv 2319 |
. . . . . . . . . . 11
โข
โฒ๐
# |
53 | | nfcv 2319 |
. . . . . . . . . . 11
โข
โฒ๐0 |
54 | 39, 52, 53 | nfbr 4051 |
. . . . . . . . . 10
โข
โฒ๐โฆ๐ง / ๐โฆ๐ต # 0 |
55 | 41 | breq1d 4015 |
. . . . . . . . . 10
โข (๐ = ๐ง โ (๐ต # 0 โ โฆ๐ง / ๐โฆ๐ต # 0)) |
56 | 54, 55 | rspc 2837 |
. . . . . . . . 9
โข (๐ง โ ๐ด โ (โ๐ โ ๐ด ๐ต # 0 โ โฆ๐ง / ๐โฆ๐ต # 0)) |
57 | 36, 51, 56 | sylc 62 |
. . . . . . . 8
โข (((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ โฆ๐ง / ๐โฆ๐ต # 0) |
58 | 57 | adantr 276 |
. . . . . . 7
โข ((((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง โ๐ โ ๐ฆ (1 / ๐ต) = (1 / โ๐ โ ๐ฆ ๐ต)) โ โฆ๐ง / ๐โฆ๐ต # 0) |
59 | 25, 34, 25, 45, 49, 58 | divmuldivapd 8791 |
. . . . . 6
โข ((((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง โ๐ โ ๐ฆ (1 / ๐ต) = (1 / โ๐ โ ๐ฆ ๐ต)) โ ((1 / โ๐ โ ๐ฆ ๐ต) ยท (1 / โฆ๐ง / ๐โฆ๐ต)) = ((1 ยท 1) / (โ๐ โ ๐ฆ ๐ต ยท โฆ๐ง / ๐โฆ๐ต))) |
60 | | 1t1e1 9073 |
. . . . . . 7
โข (1
ยท 1) = 1 |
61 | 60 | oveq1i 5887 |
. . . . . 6
โข ((1
ยท 1) / (โ๐
โ ๐ฆ ๐ต ยท โฆ๐ง / ๐โฆ๐ต)) = (1 / (โ๐ โ ๐ฆ ๐ต ยท โฆ๐ง / ๐โฆ๐ต)) |
62 | 59, 61 | eqtrdi 2226 |
. . . . 5
โข ((((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง โ๐ โ ๐ฆ (1 / ๐ต) = (1 / โ๐ โ ๐ฆ ๐ต)) โ ((1 / โ๐ โ ๐ฆ ๐ต) ยท (1 / โฆ๐ง / ๐โฆ๐ต)) = (1 / (โ๐ โ ๐ฆ ๐ต ยท โฆ๐ง / ๐โฆ๐ต))) |
63 | 24, 62 | eqtrd 2210 |
. . . 4
โข ((((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง โ๐ โ ๐ฆ (1 / ๐ต) = (1 / โ๐ โ ๐ฆ ๐ต)) โ (โ๐ โ ๐ฆ (1 / ๐ต) ยท (1 / โฆ๐ง / ๐โฆ๐ต)) = (1 / (โ๐ โ ๐ฆ ๐ต ยท โฆ๐ง / ๐โฆ๐ต))) |
64 | | nfcv 2319 |
. . . . . . 7
โข
โฒ๐1 |
65 | | nfcv 2319 |
. . . . . . 7
โข
โฒ๐
/ |
66 | 64, 65, 39 | nfov 5907 |
. . . . . 6
โข
โฒ๐(1 /
โฆ๐ง / ๐โฆ๐ต) |
67 | 35 | eldifbd 3143 |
. . . . . 6
โข (((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ ยฌ ๐ง โ ๐ฆ) |
68 | 32, 47 | recclapd 8740 |
. . . . . 6
โข ((((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง ๐ โ ๐ฆ) โ (1 / ๐ต) โ โ) |
69 | 44, 57 | recclapd 8740 |
. . . . . 6
โข (((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ (1 / โฆ๐ง / ๐โฆ๐ต) โ โ) |
70 | 41 | oveq2d 5893 |
. . . . . 6
โข (๐ = ๐ง โ (1 / ๐ต) = (1 / โฆ๐ง / ๐โฆ๐ต)) |
71 | 66, 26, 35, 67, 68, 69, 70 | fprodunsn 11614 |
. . . . 5
โข (((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ โ๐ โ (๐ฆ โช {๐ง})(1 / ๐ต) = (โ๐ โ ๐ฆ (1 / ๐ต) ยท (1 / โฆ๐ง / ๐โฆ๐ต))) |
72 | 71 | adantr 276 |
. . . 4
โข ((((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง โ๐ โ ๐ฆ (1 / ๐ต) = (1 / โ๐ โ ๐ฆ ๐ต)) โ โ๐ โ (๐ฆ โช {๐ง})(1 / ๐ต) = (โ๐ โ ๐ฆ (1 / ๐ต) ยท (1 / โฆ๐ง / ๐โฆ๐ต))) |
73 | 39, 26, 35, 67, 32, 44, 41 | fprodunsn 11614 |
. . . . . 6
โข (((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ โ๐ โ (๐ฆ โช {๐ง})๐ต = (โ๐ โ ๐ฆ ๐ต ยท โฆ๐ง / ๐โฆ๐ต)) |
74 | 73 | oveq2d 5893 |
. . . . 5
โข (((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ (1 / โ๐ โ (๐ฆ โช {๐ง})๐ต) = (1 / (โ๐ โ ๐ฆ ๐ต ยท โฆ๐ง / ๐โฆ๐ต))) |
75 | 74 | adantr 276 |
. . . 4
โข ((((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง โ๐ โ ๐ฆ (1 / ๐ต) = (1 / โ๐ โ ๐ฆ ๐ต)) โ (1 / โ๐ โ (๐ฆ โช {๐ง})๐ต) = (1 / (โ๐ โ ๐ฆ ๐ต ยท โฆ๐ง / ๐โฆ๐ต))) |
76 | 63, 72, 75 | 3eqtr4d 2220 |
. . 3
โข ((((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง โ๐ โ ๐ฆ (1 / ๐ต) = (1 / โ๐ โ ๐ฆ ๐ต)) โ โ๐ โ (๐ฆ โช {๐ง})(1 / ๐ต) = (1 / โ๐ โ (๐ฆ โช {๐ง})๐ต)) |
77 | 76 | ex 115 |
. 2
โข (((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ (โ๐ โ ๐ฆ (1 / ๐ต) = (1 / โ๐ โ ๐ฆ ๐ต) โ โ๐ โ (๐ฆ โช {๐ง})(1 / ๐ต) = (1 / โ๐ โ (๐ฆ โช {๐ง})๐ต))) |
78 | | fprodrec.a |
. 2
โข (๐ โ ๐ด โ Fin) |
79 | 4, 8, 12, 16, 22, 77, 78 | findcard2sd 6894 |
1
โข (๐ โ โ๐ โ ๐ด (1 / ๐ต) = (1 / โ๐ โ ๐ด ๐ต)) |