Step | Hyp | Ref
| Expression |
1 | | prodeq1 11561 |
. . 3
โข (๐ค = โ
โ โ๐ โ ๐ค ๐ต = โ๐ โ โ
๐ต) |
2 | | prodeq1 11561 |
. . 3
โข (๐ค = โ
โ โ๐ โ ๐ค ๐ถ = โ๐ โ โ
๐ถ) |
3 | 1, 2 | breq12d 4017 |
. 2
โข (๐ค = โ
โ (โ๐ โ ๐ค ๐ต โค โ๐ โ ๐ค ๐ถ โ โ๐ โ โ
๐ต โค โ๐ โ โ
๐ถ)) |
4 | | prodeq1 11561 |
. . 3
โข (๐ค = ๐ฆ โ โ๐ โ ๐ค ๐ต = โ๐ โ ๐ฆ ๐ต) |
5 | | prodeq1 11561 |
. . 3
โข (๐ค = ๐ฆ โ โ๐ โ ๐ค ๐ถ = โ๐ โ ๐ฆ ๐ถ) |
6 | 4, 5 | breq12d 4017 |
. 2
โข (๐ค = ๐ฆ โ (โ๐ โ ๐ค ๐ต โค โ๐ โ ๐ค ๐ถ โ โ๐ โ ๐ฆ ๐ต โค โ๐ โ ๐ฆ ๐ถ)) |
7 | | prodeq1 11561 |
. . 3
โข (๐ค = (๐ฆ โช {๐ง}) โ โ๐ โ ๐ค ๐ต = โ๐ โ (๐ฆ โช {๐ง})๐ต) |
8 | | prodeq1 11561 |
. . 3
โข (๐ค = (๐ฆ โช {๐ง}) โ โ๐ โ ๐ค ๐ถ = โ๐ โ (๐ฆ โช {๐ง})๐ถ) |
9 | 7, 8 | breq12d 4017 |
. 2
โข (๐ค = (๐ฆ โช {๐ง}) โ (โ๐ โ ๐ค ๐ต โค โ๐ โ ๐ค ๐ถ โ โ๐ โ (๐ฆ โช {๐ง})๐ต โค โ๐ โ (๐ฆ โช {๐ง})๐ถ)) |
10 | | prodeq1 11561 |
. . 3
โข (๐ค = ๐ด โ โ๐ โ ๐ค ๐ต = โ๐ โ ๐ด ๐ต) |
11 | | prodeq1 11561 |
. . 3
โข (๐ค = ๐ด โ โ๐ โ ๐ค ๐ถ = โ๐ โ ๐ด ๐ถ) |
12 | 10, 11 | breq12d 4017 |
. 2
โข (๐ค = ๐ด โ (โ๐ โ ๐ค ๐ต โค โ๐ โ ๐ค ๐ถ โ โ๐ โ ๐ด ๐ต โค โ๐ โ ๐ด ๐ถ)) |
13 | | prod0 11593 |
. . . 4
โข
โ๐ โ
โ
๐ต =
1 |
14 | | prod0 11593 |
. . . 4
โข
โ๐ โ
โ
๐ถ =
1 |
15 | 13, 14 | eqtr4i 2201 |
. . 3
โข
โ๐ โ
โ
๐ต = โ๐ โ โ
๐ถ |
16 | | 1re 7956 |
. . . . 5
โข 1 โ
โ |
17 | 13, 16 | eqeltri 2250 |
. . . 4
โข
โ๐ โ
โ
๐ต โ
โ |
18 | 17 | eqlei 8051 |
. . 3
โข
(โ๐ โ
โ
๐ต = โ๐ โ โ
๐ถ โ โ๐ โ โ
๐ต โค โ๐ โ โ
๐ถ) |
19 | 15, 18 | mp1i 10 |
. 2
โข (๐ โ โ๐ โ โ
๐ต โค โ๐ โ โ
๐ถ) |
20 | | fprodle.kph |
. . . . . . . . 9
โข
โฒ๐๐ |
21 | | nfv 1528 |
. . . . . . . . 9
โข
โฒ๐ ๐ฆ โ Fin |
22 | 20, 21 | nfan 1565 |
. . . . . . . 8
โข
โฒ๐(๐ โง ๐ฆ โ Fin) |
23 | | nfv 1528 |
. . . . . . . 8
โข
โฒ๐(๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ)) |
24 | 22, 23 | nfan 1565 |
. . . . . . 7
โข
โฒ๐((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) |
25 | | simplr 528 |
. . . . . . 7
โข (((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ ๐ฆ โ Fin) |
26 | | simplll 533 |
. . . . . . . 8
โข ((((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง ๐ โ ๐ฆ) โ ๐) |
27 | | simplrl 535 |
. . . . . . . . 9
โข ((((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง ๐ โ ๐ฆ) โ ๐ฆ โ ๐ด) |
28 | | simpr 110 |
. . . . . . . . 9
โข ((((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง ๐ โ ๐ฆ) โ ๐ โ ๐ฆ) |
29 | 27, 28 | sseldd 3157 |
. . . . . . . 8
โข ((((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง ๐ โ ๐ฆ) โ ๐ โ ๐ด) |
30 | | fprodle.b |
. . . . . . . 8
โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) |
31 | 26, 29, 30 | syl2anc 411 |
. . . . . . 7
โข ((((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง ๐ โ ๐ฆ) โ ๐ต โ โ) |
32 | 24, 25, 31 | fprodreclf 11622 |
. . . . . 6
โข (((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ โ๐ โ ๐ฆ ๐ต โ โ) |
33 | 32 | adantr 276 |
. . . . 5
โข ((((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง โ๐ โ ๐ฆ ๐ต โค โ๐ โ ๐ฆ ๐ถ) โ โ๐ โ ๐ฆ ๐ต โ โ) |
34 | | fprodle.c |
. . . . . . . 8
โข ((๐ โง ๐ โ ๐ด) โ ๐ถ โ โ) |
35 | 26, 29, 34 | syl2anc 411 |
. . . . . . 7
โข ((((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง ๐ โ ๐ฆ) โ ๐ถ โ โ) |
36 | 24, 25, 35 | fprodreclf 11622 |
. . . . . 6
โข (((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ โ๐ โ ๐ฆ ๐ถ โ โ) |
37 | 36 | adantr 276 |
. . . . 5
โข ((((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง โ๐ โ ๐ฆ ๐ต โค โ๐ โ ๐ฆ ๐ถ) โ โ๐ โ ๐ฆ ๐ถ โ โ) |
38 | | simpll 527 |
. . . . . . 7
โข (((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ ๐) |
39 | | simprr 531 |
. . . . . . . 8
โข (((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ ๐ง โ (๐ด โ ๐ฆ)) |
40 | 39 | eldifad 3141 |
. . . . . . 7
โข (((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ ๐ง โ ๐ด) |
41 | 30 | ex 115 |
. . . . . . . . . 10
โข (๐ โ (๐ โ ๐ด โ ๐ต โ โ)) |
42 | 20, 41 | ralrimi 2548 |
. . . . . . . . 9
โข (๐ โ โ๐ โ ๐ด ๐ต โ โ) |
43 | | nfv 1528 |
. . . . . . . . . 10
โข
โฒ๐ง ๐ต โ โ |
44 | | nfcsb1v 3091 |
. . . . . . . . . . 11
โข
โฒ๐โฆ๐ง / ๐โฆ๐ต |
45 | 44 | nfel1 2330 |
. . . . . . . . . 10
โข
โฒ๐โฆ๐ง / ๐โฆ๐ต โ โ |
46 | | csbeq1a 3067 |
. . . . . . . . . . 11
โข (๐ = ๐ง โ ๐ต = โฆ๐ง / ๐โฆ๐ต) |
47 | 46 | eleq1d 2246 |
. . . . . . . . . 10
โข (๐ = ๐ง โ (๐ต โ โ โ โฆ๐ง / ๐โฆ๐ต โ โ)) |
48 | 43, 45, 47 | cbvral 2700 |
. . . . . . . . 9
โข
(โ๐ โ
๐ด ๐ต โ โ โ โ๐ง โ ๐ด โฆ๐ง / ๐โฆ๐ต โ โ) |
49 | 42, 48 | sylib 122 |
. . . . . . . 8
โข (๐ โ โ๐ง โ ๐ด โฆ๐ง / ๐โฆ๐ต โ โ) |
50 | | rsp 2524 |
. . . . . . . 8
โข
(โ๐ง โ
๐ด โฆ๐ง / ๐โฆ๐ต โ โ โ (๐ง โ ๐ด โ โฆ๐ง / ๐โฆ๐ต โ โ)) |
51 | 49, 50 | syl 14 |
. . . . . . 7
โข (๐ โ (๐ง โ ๐ด โ โฆ๐ง / ๐โฆ๐ต โ โ)) |
52 | 38, 40, 51 | sylc 62 |
. . . . . 6
โข (((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ โฆ๐ง / ๐โฆ๐ต โ โ) |
53 | 52 | adantr 276 |
. . . . 5
โข ((((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง โ๐ โ ๐ฆ ๐ต โค โ๐ โ ๐ฆ ๐ถ) โ โฆ๐ง / ๐โฆ๐ต โ โ) |
54 | 34 | ex 115 |
. . . . . . . . . 10
โข (๐ โ (๐ โ ๐ด โ ๐ถ โ โ)) |
55 | 20, 54 | ralrimi 2548 |
. . . . . . . . 9
โข (๐ โ โ๐ โ ๐ด ๐ถ โ โ) |
56 | | nfv 1528 |
. . . . . . . . . 10
โข
โฒ๐ง ๐ถ โ โ |
57 | | nfcsb1v 3091 |
. . . . . . . . . . 11
โข
โฒ๐โฆ๐ง / ๐โฆ๐ถ |
58 | 57 | nfel1 2330 |
. . . . . . . . . 10
โข
โฒ๐โฆ๐ง / ๐โฆ๐ถ โ โ |
59 | | csbeq1a 3067 |
. . . . . . . . . . 11
โข (๐ = ๐ง โ ๐ถ = โฆ๐ง / ๐โฆ๐ถ) |
60 | 59 | eleq1d 2246 |
. . . . . . . . . 10
โข (๐ = ๐ง โ (๐ถ โ โ โ โฆ๐ง / ๐โฆ๐ถ โ โ)) |
61 | 56, 58, 60 | cbvral 2700 |
. . . . . . . . 9
โข
(โ๐ โ
๐ด ๐ถ โ โ โ โ๐ง โ ๐ด โฆ๐ง / ๐โฆ๐ถ โ โ) |
62 | 55, 61 | sylib 122 |
. . . . . . . 8
โข (๐ โ โ๐ง โ ๐ด โฆ๐ง / ๐โฆ๐ถ โ โ) |
63 | | rsp 2524 |
. . . . . . . 8
โข
(โ๐ง โ
๐ด โฆ๐ง / ๐โฆ๐ถ โ โ โ (๐ง โ ๐ด โ โฆ๐ง / ๐โฆ๐ถ โ โ)) |
64 | 62, 63 | syl 14 |
. . . . . . 7
โข (๐ โ (๐ง โ ๐ด โ โฆ๐ง / ๐โฆ๐ถ โ โ)) |
65 | 38, 40, 64 | sylc 62 |
. . . . . 6
โข (((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ โฆ๐ง / ๐โฆ๐ถ โ โ) |
66 | 65 | adantr 276 |
. . . . 5
โข ((((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง โ๐ โ ๐ฆ ๐ต โค โ๐ โ ๐ฆ ๐ถ) โ โฆ๐ง / ๐โฆ๐ถ โ โ) |
67 | | fprodle.0l3b |
. . . . . . . 8
โข ((๐ โง ๐ โ ๐ด) โ 0 โค ๐ต) |
68 | 26, 29, 67 | syl2anc 411 |
. . . . . . 7
โข ((((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง ๐ โ ๐ฆ) โ 0 โค ๐ต) |
69 | 24, 25, 31, 68 | fprodge0 11645 |
. . . . . 6
โข (((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ 0 โค โ๐ โ ๐ฆ ๐ต) |
70 | 69 | adantr 276 |
. . . . 5
โข ((((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง โ๐ โ ๐ฆ ๐ต โค โ๐ โ ๐ฆ ๐ถ) โ 0 โค โ๐ โ ๐ฆ ๐ต) |
71 | 67 | ex 115 |
. . . . . . . . 9
โข (๐ โ (๐ โ ๐ด โ 0 โค ๐ต)) |
72 | 20, 71 | ralrimi 2548 |
. . . . . . . 8
โข (๐ โ โ๐ โ ๐ด 0 โค ๐ต) |
73 | 38, 72 | syl 14 |
. . . . . . 7
โข (((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ โ๐ โ ๐ด 0 โค ๐ต) |
74 | | nfcv 2319 |
. . . . . . . . 9
โข
โฒ๐0 |
75 | | nfcv 2319 |
. . . . . . . . 9
โข
โฒ๐
โค |
76 | 74, 75, 44 | nfbr 4050 |
. . . . . . . 8
โข
โฒ๐0 โค
โฆ๐ง / ๐โฆ๐ต |
77 | 46 | breq2d 4016 |
. . . . . . . 8
โข (๐ = ๐ง โ (0 โค ๐ต โ 0 โค โฆ๐ง / ๐โฆ๐ต)) |
78 | 76, 77 | rspc 2836 |
. . . . . . 7
โข (๐ง โ ๐ด โ (โ๐ โ ๐ด 0 โค ๐ต โ 0 โค โฆ๐ง / ๐โฆ๐ต)) |
79 | 40, 73, 78 | sylc 62 |
. . . . . 6
โข (((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ 0 โค โฆ๐ง / ๐โฆ๐ต) |
80 | 79 | adantr 276 |
. . . . 5
โข ((((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง โ๐ โ ๐ฆ ๐ต โค โ๐ โ ๐ฆ ๐ถ) โ 0 โค โฆ๐ง / ๐โฆ๐ต) |
81 | | simpr 110 |
. . . . 5
โข ((((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง โ๐ โ ๐ฆ ๐ต โค โ๐ โ ๐ฆ ๐ถ) โ โ๐ โ ๐ฆ ๐ต โค โ๐ โ ๐ฆ ๐ถ) |
82 | 40 | adantr 276 |
. . . . . 6
โข ((((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง โ๐ โ ๐ฆ ๐ต โค โ๐ โ ๐ฆ ๐ถ) โ ๐ง โ ๐ด) |
83 | | fprodle.blec |
. . . . . . . . 9
โข ((๐ โง ๐ โ ๐ด) โ ๐ต โค ๐ถ) |
84 | 83 | ex 115 |
. . . . . . . 8
โข (๐ โ (๐ โ ๐ด โ ๐ต โค ๐ถ)) |
85 | 20, 84 | ralrimi 2548 |
. . . . . . 7
โข (๐ โ โ๐ โ ๐ด ๐ต โค ๐ถ) |
86 | 85 | ad3antrrr 492 |
. . . . . 6
โข ((((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง โ๐ โ ๐ฆ ๐ต โค โ๐ โ ๐ฆ ๐ถ) โ โ๐ โ ๐ด ๐ต โค ๐ถ) |
87 | 44, 75, 57 | nfbr 4050 |
. . . . . . 7
โข
โฒ๐โฆ๐ง / ๐โฆ๐ต โค โฆ๐ง / ๐โฆ๐ถ |
88 | 46, 59 | breq12d 4017 |
. . . . . . 7
โข (๐ = ๐ง โ (๐ต โค ๐ถ โ โฆ๐ง / ๐โฆ๐ต โค โฆ๐ง / ๐โฆ๐ถ)) |
89 | 87, 88 | rspc 2836 |
. . . . . 6
โข (๐ง โ ๐ด โ (โ๐ โ ๐ด ๐ต โค ๐ถ โ โฆ๐ง / ๐โฆ๐ต โค โฆ๐ง / ๐โฆ๐ถ)) |
90 | 82, 86, 89 | sylc 62 |
. . . . 5
โข ((((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง โ๐ โ ๐ฆ ๐ต โค โ๐ โ ๐ฆ ๐ถ) โ โฆ๐ง / ๐โฆ๐ต โค โฆ๐ง / ๐โฆ๐ถ) |
91 | 33, 37, 53, 66, 70, 80, 81, 90 | lemul12ad 8899 |
. . . 4
โข ((((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง โ๐ โ ๐ฆ ๐ต โค โ๐ โ ๐ฆ ๐ถ) โ (โ๐ โ ๐ฆ ๐ต ยท โฆ๐ง / ๐โฆ๐ต) โค (โ๐ โ ๐ฆ ๐ถ ยท โฆ๐ง / ๐โฆ๐ถ)) |
92 | 39 | eldifbd 3142 |
. . . . . . 7
โข (((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ ยฌ ๐ง โ ๐ฆ) |
93 | 30 | recnd 7986 |
. . . . . . . 8
โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) |
94 | 26, 29, 93 | syl2anc 411 |
. . . . . . 7
โข ((((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง ๐ โ ๐ฆ) โ ๐ต โ โ) |
95 | 52 | recnd 7986 |
. . . . . . 7
โข (((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ โฆ๐ง / ๐โฆ๐ต โ โ) |
96 | 24, 44, 25, 39, 92, 94, 46, 95 | fprodsplitsn 11641 |
. . . . . 6
โข (((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ โ๐ โ (๐ฆ โช {๐ง})๐ต = (โ๐ โ ๐ฆ ๐ต ยท โฆ๐ง / ๐โฆ๐ต)) |
97 | 35 | recnd 7986 |
. . . . . . 7
โข ((((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง ๐ โ ๐ฆ) โ ๐ถ โ โ) |
98 | 65 | recnd 7986 |
. . . . . . 7
โข (((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ โฆ๐ง / ๐โฆ๐ถ โ โ) |
99 | 24, 57, 25, 39, 92, 97, 59, 98 | fprodsplitsn 11641 |
. . . . . 6
โข (((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ โ๐ โ (๐ฆ โช {๐ง})๐ถ = (โ๐ โ ๐ฆ ๐ถ ยท โฆ๐ง / ๐โฆ๐ถ)) |
100 | 96, 99 | breq12d 4017 |
. . . . 5
โข (((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ (โ๐ โ (๐ฆ โช {๐ง})๐ต โค โ๐ โ (๐ฆ โช {๐ง})๐ถ โ (โ๐ โ ๐ฆ ๐ต ยท โฆ๐ง / ๐โฆ๐ต) โค (โ๐ โ ๐ฆ ๐ถ ยท โฆ๐ง / ๐โฆ๐ถ))) |
101 | 100 | adantr 276 |
. . . 4
โข ((((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง โ๐ โ ๐ฆ ๐ต โค โ๐ โ ๐ฆ ๐ถ) โ (โ๐ โ (๐ฆ โช {๐ง})๐ต โค โ๐ โ (๐ฆ โช {๐ง})๐ถ โ (โ๐ โ ๐ฆ ๐ต ยท โฆ๐ง / ๐โฆ๐ต) โค (โ๐ โ ๐ฆ ๐ถ ยท โฆ๐ง / ๐โฆ๐ถ))) |
102 | 91, 101 | mpbird 167 |
. . 3
โข ((((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง โ๐ โ ๐ฆ ๐ต โค โ๐ โ ๐ฆ ๐ถ) โ โ๐ โ (๐ฆ โช {๐ง})๐ต โค โ๐ โ (๐ฆ โช {๐ง})๐ถ) |
103 | 102 | ex 115 |
. 2
โข (((๐ โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ (โ๐ โ ๐ฆ ๐ต โค โ๐ โ ๐ฆ ๐ถ โ โ๐ โ (๐ฆ โช {๐ง})๐ต โค โ๐ โ (๐ฆ โช {๐ง})๐ถ)) |
104 | | fprodle.a |
. 2
โข (๐ โ ๐ด โ Fin) |
105 | 3, 6, 9, 12, 19, 103, 104 | findcard2sd 6892 |
1
โข (๐ โ โ๐ โ ๐ด ๐ต โค โ๐ โ ๐ด ๐ถ) |