Step | Hyp | Ref
| Expression |
1 | | fzfi 13884 |
. . . . . . . 8
β’
(1...((β―βπ΅) β (β―βπ΄))) β Fin |
2 | | ficardom 9904 |
. . . . . . . 8
β’
((1...((β―βπ΅) β (β―βπ΄))) β Fin β
(cardβ(1...((β―βπ΅) β (β―βπ΄)))) β Ο) |
3 | 1, 2 | ax-mp 5 |
. . . . . . 7
β’
(cardβ(1...((β―βπ΅) β (β―βπ΄)))) β Ο |
4 | | eqid 2737 |
. . . . . . . . . . . . . 14
β’
(rec((π₯ β V
β¦ (π₯ + 1)), 0)
βΎ Ο) = (rec((π₯
β V β¦ (π₯ + 1)),
0) βΎ Ο) |
5 | 4 | hashgval 14240 |
. . . . . . . . . . . . 13
β’ (π΄ β Fin β ((rec((π₯ β V β¦ (π₯ + 1)), 0) βΎ
Ο)β(cardβπ΄)) = (β―βπ΄)) |
6 | 5 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π΄ β Fin β§ π΅ β Fin) β§
(β―βπ΄) β€
(β―βπ΅)) β
((rec((π₯ β V β¦
(π₯ + 1)), 0) βΎ
Ο)β(cardβπ΄)) = (β―βπ΄)) |
7 | 4 | hashgval 14240 |
. . . . . . . . . . . . . 14
β’
((1...((β―βπ΅) β (β―βπ΄))) β Fin β ((rec((π₯ β V β¦ (π₯ + 1)), 0) βΎ
Ο)β(cardβ(1...((β―βπ΅) β (β―βπ΄))))) =
(β―β(1...((β―βπ΅) β (β―βπ΄))))) |
8 | 1, 7 | ax-mp 5 |
. . . . . . . . . . . . 13
β’
((rec((π₯ β V
β¦ (π₯ + 1)), 0)
βΎ Ο)β(cardβ(1...((β―βπ΅) β (β―βπ΄))))) =
(β―β(1...((β―βπ΅) β (β―βπ΄)))) |
9 | | hashcl 14263 |
. . . . . . . . . . . . . . . 16
β’ (π΄ β Fin β
(β―βπ΄) β
β0) |
10 | 9 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β Fin β§ π΅ β Fin) β§
(β―βπ΄) β€
(β―βπ΅)) β
(β―βπ΄) β
β0) |
11 | | hashcl 14263 |
. . . . . . . . . . . . . . . 16
β’ (π΅ β Fin β
(β―βπ΅) β
β0) |
12 | 11 | ad2antlr 726 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β Fin β§ π΅ β Fin) β§
(β―βπ΄) β€
(β―βπ΅)) β
(β―βπ΅) β
β0) |
13 | | simpr 486 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β Fin β§ π΅ β Fin) β§
(β―βπ΄) β€
(β―βπ΅)) β
(β―βπ΄) β€
(β―βπ΅)) |
14 | | nn0sub2 12571 |
. . . . . . . . . . . . . . 15
β’
(((β―βπ΄)
β β0 β§ (β―βπ΅) β β0 β§
(β―βπ΄) β€
(β―βπ΅)) β
((β―βπ΅) β
(β―βπ΄)) β
β0) |
15 | 10, 12, 13, 14 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ (((π΄ β Fin β§ π΅ β Fin) β§
(β―βπ΄) β€
(β―βπ΅)) β
((β―βπ΅) β
(β―βπ΄)) β
β0) |
16 | | hashfz1 14253 |
. . . . . . . . . . . . . 14
β’
(((β―βπ΅)
β (β―βπ΄))
β β0 β (β―β(1...((β―βπ΅) β (β―βπ΄)))) = ((β―βπ΅) β (β―βπ΄))) |
17 | 15, 16 | syl 17 |
. . . . . . . . . . . . 13
β’ (((π΄ β Fin β§ π΅ β Fin) β§
(β―βπ΄) β€
(β―βπ΅)) β
(β―β(1...((β―βπ΅) β (β―βπ΄)))) = ((β―βπ΅) β (β―βπ΄))) |
18 | 8, 17 | eqtrid 2789 |
. . . . . . . . . . . 12
β’ (((π΄ β Fin β§ π΅ β Fin) β§
(β―βπ΄) β€
(β―βπ΅)) β
((rec((π₯ β V β¦
(π₯ + 1)), 0) βΎ
Ο)β(cardβ(1...((β―βπ΅) β (β―βπ΄))))) = ((β―βπ΅) β (β―βπ΄))) |
19 | 6, 18 | oveq12d 7380 |
. . . . . . . . . . 11
β’ (((π΄ β Fin β§ π΅ β Fin) β§
(β―βπ΄) β€
(β―βπ΅)) β
(((rec((π₯ β V β¦
(π₯ + 1)), 0) βΎ
Ο)β(cardβπ΄)) + ((rec((π₯ β V β¦ (π₯ + 1)), 0) βΎ
Ο)β(cardβ(1...((β―βπ΅) β (β―βπ΄)))))) = ((β―βπ΄) + ((β―βπ΅) β (β―βπ΄)))) |
20 | 9 | nn0cnd 12482 |
. . . . . . . . . . . . 13
β’ (π΄ β Fin β
(β―βπ΄) β
β) |
21 | 11 | nn0cnd 12482 |
. . . . . . . . . . . . 13
β’ (π΅ β Fin β
(β―βπ΅) β
β) |
22 | | pncan3 11416 |
. . . . . . . . . . . . 13
β’
(((β―βπ΄)
β β β§ (β―βπ΅) β β) β
((β―βπ΄) +
((β―βπ΅) β
(β―βπ΄))) =
(β―βπ΅)) |
23 | 20, 21, 22 | syl2an 597 |
. . . . . . . . . . . 12
β’ ((π΄ β Fin β§ π΅ β Fin) β
((β―βπ΄) +
((β―βπ΅) β
(β―βπ΄))) =
(β―βπ΅)) |
24 | 23 | adantr 482 |
. . . . . . . . . . 11
β’ (((π΄ β Fin β§ π΅ β Fin) β§
(β―βπ΄) β€
(β―βπ΅)) β
((β―βπ΄) +
((β―βπ΅) β
(β―βπ΄))) =
(β―βπ΅)) |
25 | 19, 24 | eqtrd 2777 |
. . . . . . . . . 10
β’ (((π΄ β Fin β§ π΅ β Fin) β§
(β―βπ΄) β€
(β―βπ΅)) β
(((rec((π₯ β V β¦
(π₯ + 1)), 0) βΎ
Ο)β(cardβπ΄)) + ((rec((π₯ β V β¦ (π₯ + 1)), 0) βΎ
Ο)β(cardβ(1...((β―βπ΅) β (β―βπ΄)))))) = (β―βπ΅)) |
26 | | ficardom 9904 |
. . . . . . . . . . . 12
β’ (π΄ β Fin β
(cardβπ΄) β
Ο) |
27 | 26 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π΄ β Fin β§ π΅ β Fin) β§
(β―βπ΄) β€
(β―βπ΅)) β
(cardβπ΄) β
Ο) |
28 | 4 | hashgadd 14284 |
. . . . . . . . . . 11
β’
(((cardβπ΄)
β Ο β§ (cardβ(1...((β―βπ΅) β (β―βπ΄)))) β Ο) β ((rec((π₯ β V β¦ (π₯ + 1)), 0) βΎ
Ο)β((cardβπ΄) +o
(cardβ(1...((β―βπ΅) β (β―βπ΄)))))) = (((rec((π₯ β V β¦ (π₯ + 1)), 0) βΎ
Ο)β(cardβπ΄)) + ((rec((π₯ β V β¦ (π₯ + 1)), 0) βΎ
Ο)β(cardβ(1...((β―βπ΅) β (β―βπ΄))))))) |
29 | 27, 3, 28 | sylancl 587 |
. . . . . . . . . 10
β’ (((π΄ β Fin β§ π΅ β Fin) β§
(β―βπ΄) β€
(β―βπ΅)) β
((rec((π₯ β V β¦
(π₯ + 1)), 0) βΎ
Ο)β((cardβπ΄) +o
(cardβ(1...((β―βπ΅) β (β―βπ΄)))))) = (((rec((π₯ β V β¦ (π₯ + 1)), 0) βΎ
Ο)β(cardβπ΄)) + ((rec((π₯ β V β¦ (π₯ + 1)), 0) βΎ
Ο)β(cardβ(1...((β―βπ΅) β (β―βπ΄))))))) |
30 | 4 | hashgval 14240 |
. . . . . . . . . . 11
β’ (π΅ β Fin β ((rec((π₯ β V β¦ (π₯ + 1)), 0) βΎ
Ο)β(cardβπ΅)) = (β―βπ΅)) |
31 | 30 | ad2antlr 726 |
. . . . . . . . . 10
β’ (((π΄ β Fin β§ π΅ β Fin) β§
(β―βπ΄) β€
(β―βπ΅)) β
((rec((π₯ β V β¦
(π₯ + 1)), 0) βΎ
Ο)β(cardβπ΅)) = (β―βπ΅)) |
32 | 25, 29, 31 | 3eqtr4d 2787 |
. . . . . . . . 9
β’ (((π΄ β Fin β§ π΅ β Fin) β§
(β―βπ΄) β€
(β―βπ΅)) β
((rec((π₯ β V β¦
(π₯ + 1)), 0) βΎ
Ο)β((cardβπ΄) +o
(cardβ(1...((β―βπ΅) β (β―βπ΄)))))) = ((rec((π₯ β V β¦ (π₯ + 1)), 0) βΎ
Ο)β(cardβπ΅))) |
33 | 32 | fveq2d 6851 |
. . . . . . . 8
β’ (((π΄ β Fin β§ π΅ β Fin) β§
(β―βπ΄) β€
(β―βπ΅)) β
(β‘(rec((π₯ β V β¦ (π₯ + 1)), 0) βΎ
Ο)β((rec((π₯
β V β¦ (π₯ + 1)),
0) βΎ Ο)β((cardβπ΄) +o
(cardβ(1...((β―βπ΅) β (β―βπ΄))))))) = (β‘(rec((π₯ β V β¦ (π₯ + 1)), 0) βΎ
Ο)β((rec((π₯
β V β¦ (π₯ + 1)),
0) βΎ Ο)β(cardβπ΅)))) |
34 | 4 | hashgf1o 13883 |
. . . . . . . . 9
β’
(rec((π₯ β V
β¦ (π₯ + 1)), 0)
βΎ Ο):Οβ1-1-ontoββ0 |
35 | | nnacl 8563 |
. . . . . . . . . 10
β’
(((cardβπ΄)
β Ο β§ (cardβ(1...((β―βπ΅) β (β―βπ΄)))) β Ο) β
((cardβπ΄)
+o (cardβ(1...((β―βπ΅) β (β―βπ΄))))) β Ο) |
36 | 27, 3, 35 | sylancl 587 |
. . . . . . . . 9
β’ (((π΄ β Fin β§ π΅ β Fin) β§
(β―βπ΄) β€
(β―βπ΅)) β
((cardβπ΄)
+o (cardβ(1...((β―βπ΅) β (β―βπ΄))))) β Ο) |
37 | | f1ocnvfv1 7227 |
. . . . . . . . 9
β’
(((rec((π₯ β V
β¦ (π₯ + 1)), 0)
βΎ Ο):Οβ1-1-ontoββ0 β§
((cardβπ΄)
+o (cardβ(1...((β―βπ΅) β (β―βπ΄))))) β Ο) β (β‘(rec((π₯ β V β¦ (π₯ + 1)), 0) βΎ
Ο)β((rec((π₯
β V β¦ (π₯ + 1)),
0) βΎ Ο)β((cardβπ΄) +o
(cardβ(1...((β―βπ΅) β (β―βπ΄))))))) = ((cardβπ΄) +o
(cardβ(1...((β―βπ΅) β (β―βπ΄)))))) |
38 | 34, 36, 37 | sylancr 588 |
. . . . . . . 8
β’ (((π΄ β Fin β§ π΅ β Fin) β§
(β―βπ΄) β€
(β―βπ΅)) β
(β‘(rec((π₯ β V β¦ (π₯ + 1)), 0) βΎ
Ο)β((rec((π₯
β V β¦ (π₯ + 1)),
0) βΎ Ο)β((cardβπ΄) +o
(cardβ(1...((β―βπ΅) β (β―βπ΄))))))) = ((cardβπ΄) +o
(cardβ(1...((β―βπ΅) β (β―βπ΄)))))) |
39 | | ficardom 9904 |
. . . . . . . . . 10
β’ (π΅ β Fin β
(cardβπ΅) β
Ο) |
40 | 39 | ad2antlr 726 |
. . . . . . . . 9
β’ (((π΄ β Fin β§ π΅ β Fin) β§
(β―βπ΄) β€
(β―βπ΅)) β
(cardβπ΅) β
Ο) |
41 | | f1ocnvfv1 7227 |
. . . . . . . . 9
β’
(((rec((π₯ β V
β¦ (π₯ + 1)), 0)
βΎ Ο):Οβ1-1-ontoββ0 β§
(cardβπ΅) β
Ο) β (β‘(rec((π₯ β V β¦ (π₯ + 1)), 0) βΎ
Ο)β((rec((π₯
β V β¦ (π₯ + 1)),
0) βΎ Ο)β(cardβπ΅))) = (cardβπ΅)) |
42 | 34, 40, 41 | sylancr 588 |
. . . . . . . 8
β’ (((π΄ β Fin β§ π΅ β Fin) β§
(β―βπ΄) β€
(β―βπ΅)) β
(β‘(rec((π₯ β V β¦ (π₯ + 1)), 0) βΎ
Ο)β((rec((π₯
β V β¦ (π₯ + 1)),
0) βΎ Ο)β(cardβπ΅))) = (cardβπ΅)) |
43 | 33, 38, 42 | 3eqtr3d 2785 |
. . . . . . 7
β’ (((π΄ β Fin β§ π΅ β Fin) β§
(β―βπ΄) β€
(β―βπ΅)) β
((cardβπ΄)
+o (cardβ(1...((β―βπ΅) β (β―βπ΄))))) = (cardβπ΅)) |
44 | | oveq2 7370 |
. . . . . . . . 9
β’ (π¦ =
(cardβ(1...((β―βπ΅) β (β―βπ΄)))) β ((cardβπ΄) +o π¦) = ((cardβπ΄) +o
(cardβ(1...((β―βπ΅) β (β―βπ΄)))))) |
45 | 44 | eqeq1d 2739 |
. . . . . . . 8
β’ (π¦ =
(cardβ(1...((β―βπ΅) β (β―βπ΄)))) β (((cardβπ΄) +o π¦) = (cardβπ΅) β ((cardβπ΄) +o
(cardβ(1...((β―βπ΅) β (β―βπ΄))))) = (cardβπ΅))) |
46 | 45 | rspcev 3584 |
. . . . . . 7
β’
(((cardβ(1...((β―βπ΅) β (β―βπ΄)))) β Ο β§ ((cardβπ΄) +o
(cardβ(1...((β―βπ΅) β (β―βπ΄))))) = (cardβπ΅)) β βπ¦ β Ο ((cardβπ΄) +o π¦) = (cardβπ΅)) |
47 | 3, 43, 46 | sylancr 588 |
. . . . . 6
β’ (((π΄ β Fin β§ π΅ β Fin) β§
(β―βπ΄) β€
(β―βπ΅)) β
βπ¦ β Ο
((cardβπ΄)
+o π¦) =
(cardβπ΅)) |
48 | 47 | ex 414 |
. . . . 5
β’ ((π΄ β Fin β§ π΅ β Fin) β
((β―βπ΄) β€
(β―βπ΅) β
βπ¦ β Ο
((cardβπ΄)
+o π¦) =
(cardβπ΅))) |
49 | | cardnn 9906 |
. . . . . . . . . 10
β’ (π¦ β Ο β
(cardβπ¦) = π¦) |
50 | 49 | adantl 483 |
. . . . . . . . 9
β’ (((π΄ β Fin β§ π΅ β Fin) β§ π¦ β Ο) β
(cardβπ¦) = π¦) |
51 | 50 | oveq2d 7378 |
. . . . . . . 8
β’ (((π΄ β Fin β§ π΅ β Fin) β§ π¦ β Ο) β
((cardβπ΄)
+o (cardβπ¦)) = ((cardβπ΄) +o π¦)) |
52 | 51 | eqeq1d 2739 |
. . . . . . 7
β’ (((π΄ β Fin β§ π΅ β Fin) β§ π¦ β Ο) β
(((cardβπ΄)
+o (cardβπ¦)) = (cardβπ΅) β ((cardβπ΄) +o π¦) = (cardβπ΅))) |
53 | | fveq2 6847 |
. . . . . . . 8
β’
(((cardβπ΄)
+o (cardβπ¦)) = (cardβπ΅) β ((rec((π₯ β V β¦ (π₯ + 1)), 0) βΎ
Ο)β((cardβπ΄) +o (cardβπ¦))) = ((rec((π₯ β V β¦ (π₯ + 1)), 0) βΎ
Ο)β(cardβπ΅))) |
54 | | nnfi 9118 |
. . . . . . . . 9
β’ (π¦ β Ο β π¦ β Fin) |
55 | | ficardom 9904 |
. . . . . . . . . . . . . 14
β’ (π¦ β Fin β
(cardβπ¦) β
Ο) |
56 | 4 | hashgadd 14284 |
. . . . . . . . . . . . . 14
β’
(((cardβπ΄)
β Ο β§ (cardβπ¦) β Ο) β ((rec((π₯ β V β¦ (π₯ + 1)), 0) βΎ
Ο)β((cardβπ΄) +o (cardβπ¦))) = (((rec((π₯ β V β¦ (π₯ + 1)), 0) βΎ
Ο)β(cardβπ΄)) + ((rec((π₯ β V β¦ (π₯ + 1)), 0) βΎ
Ο)β(cardβπ¦)))) |
57 | 26, 55, 56 | syl2an 597 |
. . . . . . . . . . . . 13
β’ ((π΄ β Fin β§ π¦ β Fin) β ((rec((π₯ β V β¦ (π₯ + 1)), 0) βΎ
Ο)β((cardβπ΄) +o (cardβπ¦))) = (((rec((π₯ β V β¦ (π₯ + 1)), 0) βΎ
Ο)β(cardβπ΄)) + ((rec((π₯ β V β¦ (π₯ + 1)), 0) βΎ
Ο)β(cardβπ¦)))) |
58 | 4 | hashgval 14240 |
. . . . . . . . . . . . . 14
β’ (π¦ β Fin β ((rec((π₯ β V β¦ (π₯ + 1)), 0) βΎ
Ο)β(cardβπ¦)) = (β―βπ¦)) |
59 | 5, 58 | oveqan12d 7381 |
. . . . . . . . . . . . 13
β’ ((π΄ β Fin β§ π¦ β Fin) β
(((rec((π₯ β V β¦
(π₯ + 1)), 0) βΎ
Ο)β(cardβπ΄)) + ((rec((π₯ β V β¦ (π₯ + 1)), 0) βΎ
Ο)β(cardβπ¦))) = ((β―βπ΄) + (β―βπ¦))) |
60 | 57, 59 | eqtrd 2777 |
. . . . . . . . . . . 12
β’ ((π΄ β Fin β§ π¦ β Fin) β ((rec((π₯ β V β¦ (π₯ + 1)), 0) βΎ
Ο)β((cardβπ΄) +o (cardβπ¦))) = ((β―βπ΄) + (β―βπ¦))) |
61 | 60 | adantlr 714 |
. . . . . . . . . . 11
β’ (((π΄ β Fin β§ π΅ β Fin) β§ π¦ β Fin) β ((rec((π₯ β V β¦ (π₯ + 1)), 0) βΎ
Ο)β((cardβπ΄) +o (cardβπ¦))) = ((β―βπ΄) + (β―βπ¦))) |
62 | 30 | ad2antlr 726 |
. . . . . . . . . . 11
β’ (((π΄ β Fin β§ π΅ β Fin) β§ π¦ β Fin) β ((rec((π₯ β V β¦ (π₯ + 1)), 0) βΎ
Ο)β(cardβπ΅)) = (β―βπ΅)) |
63 | 61, 62 | eqeq12d 2753 |
. . . . . . . . . 10
β’ (((π΄ β Fin β§ π΅ β Fin) β§ π¦ β Fin) β
(((rec((π₯ β V β¦
(π₯ + 1)), 0) βΎ
Ο)β((cardβπ΄) +o (cardβπ¦))) = ((rec((π₯ β V β¦ (π₯ + 1)), 0) βΎ
Ο)β(cardβπ΅)) β ((β―βπ΄) + (β―βπ¦)) = (β―βπ΅))) |
64 | | hashcl 14263 |
. . . . . . . . . . . . . . 15
β’ (π¦ β Fin β
(β―βπ¦) β
β0) |
65 | 64 | nn0ge0d 12483 |
. . . . . . . . . . . . . 14
β’ (π¦ β Fin β 0 β€
(β―βπ¦)) |
66 | 65 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π΄ β Fin β§ π¦ β Fin) β 0 β€
(β―βπ¦)) |
67 | 9 | nn0red 12481 |
. . . . . . . . . . . . . 14
β’ (π΄ β Fin β
(β―βπ΄) β
β) |
68 | 64 | nn0red 12481 |
. . . . . . . . . . . . . 14
β’ (π¦ β Fin β
(β―βπ¦) β
β) |
69 | | addge01 11672 |
. . . . . . . . . . . . . 14
β’
(((β―βπ΄)
β β β§ (β―βπ¦) β β) β (0 β€
(β―βπ¦) β
(β―βπ΄) β€
((β―βπ΄) +
(β―βπ¦)))) |
70 | 67, 68, 69 | syl2an 597 |
. . . . . . . . . . . . 13
β’ ((π΄ β Fin β§ π¦ β Fin) β (0 β€
(β―βπ¦) β
(β―βπ΄) β€
((β―βπ΄) +
(β―βπ¦)))) |
71 | 66, 70 | mpbid 231 |
. . . . . . . . . . . 12
β’ ((π΄ β Fin β§ π¦ β Fin) β
(β―βπ΄) β€
((β―βπ΄) +
(β―βπ¦))) |
72 | 71 | adantlr 714 |
. . . . . . . . . . 11
β’ (((π΄ β Fin β§ π΅ β Fin) β§ π¦ β Fin) β
(β―βπ΄) β€
((β―βπ΄) +
(β―βπ¦))) |
73 | | breq2 5114 |
. . . . . . . . . . 11
β’
(((β―βπ΄)
+ (β―βπ¦)) =
(β―βπ΅) β
((β―βπ΄) β€
((β―βπ΄) +
(β―βπ¦)) β
(β―βπ΄) β€
(β―βπ΅))) |
74 | 72, 73 | syl5ibcom 244 |
. . . . . . . . . 10
β’ (((π΄ β Fin β§ π΅ β Fin) β§ π¦ β Fin) β
(((β―βπ΄) +
(β―βπ¦)) =
(β―βπ΅) β
(β―βπ΄) β€
(β―βπ΅))) |
75 | 63, 74 | sylbid 239 |
. . . . . . . . 9
β’ (((π΄ β Fin β§ π΅ β Fin) β§ π¦ β Fin) β
(((rec((π₯ β V β¦
(π₯ + 1)), 0) βΎ
Ο)β((cardβπ΄) +o (cardβπ¦))) = ((rec((π₯ β V β¦ (π₯ + 1)), 0) βΎ
Ο)β(cardβπ΅)) β (β―βπ΄) β€ (β―βπ΅))) |
76 | 54, 75 | sylan2 594 |
. . . . . . . 8
β’ (((π΄ β Fin β§ π΅ β Fin) β§ π¦ β Ο) β
(((rec((π₯ β V β¦
(π₯ + 1)), 0) βΎ
Ο)β((cardβπ΄) +o (cardβπ¦))) = ((rec((π₯ β V β¦ (π₯ + 1)), 0) βΎ
Ο)β(cardβπ΅)) β (β―βπ΄) β€ (β―βπ΅))) |
77 | 53, 76 | syl5 34 |
. . . . . . 7
β’ (((π΄ β Fin β§ π΅ β Fin) β§ π¦ β Ο) β
(((cardβπ΄)
+o (cardβπ¦)) = (cardβπ΅) β (β―βπ΄) β€ (β―βπ΅))) |
78 | 52, 77 | sylbird 260 |
. . . . . 6
β’ (((π΄ β Fin β§ π΅ β Fin) β§ π¦ β Ο) β
(((cardβπ΄)
+o π¦) =
(cardβπ΅) β
(β―βπ΄) β€
(β―βπ΅))) |
79 | 78 | rexlimdva 3153 |
. . . . 5
β’ ((π΄ β Fin β§ π΅ β Fin) β
(βπ¦ β Ο
((cardβπ΄)
+o π¦) =
(cardβπ΅) β
(β―βπ΄) β€
(β―βπ΅))) |
80 | 48, 79 | impbid 211 |
. . . 4
β’ ((π΄ β Fin β§ π΅ β Fin) β
((β―βπ΄) β€
(β―βπ΅) β
βπ¦ β Ο
((cardβπ΄)
+o π¦) =
(cardβπ΅))) |
81 | | nnawordex 8589 |
. . . . 5
β’
(((cardβπ΄)
β Ο β§ (cardβπ΅) β Ο) β ((cardβπ΄) β (cardβπ΅) β βπ¦ β Ο
((cardβπ΄)
+o π¦) =
(cardβπ΅))) |
82 | 26, 39, 81 | syl2an 597 |
. . . 4
β’ ((π΄ β Fin β§ π΅ β Fin) β
((cardβπ΄) β
(cardβπ΅) β
βπ¦ β Ο
((cardβπ΄)
+o π¦) =
(cardβπ΅))) |
83 | | finnum 9891 |
. . . . 5
β’ (π΄ β Fin β π΄ β dom
card) |
84 | | finnum 9891 |
. . . . 5
β’ (π΅ β Fin β π΅ β dom
card) |
85 | | carddom2 9920 |
. . . . 5
β’ ((π΄ β dom card β§ π΅ β dom card) β
((cardβπ΄) β
(cardβπ΅) β π΄ βΌ π΅)) |
86 | 83, 84, 85 | syl2an 597 |
. . . 4
β’ ((π΄ β Fin β§ π΅ β Fin) β
((cardβπ΄) β
(cardβπ΅) β π΄ βΌ π΅)) |
87 | 80, 82, 86 | 3bitr2d 307 |
. . 3
β’ ((π΄ β Fin β§ π΅ β Fin) β
((β―βπ΄) β€
(β―βπ΅) β
π΄ βΌ π΅)) |
88 | 87 | adantlr 714 |
. 2
β’ (((π΄ β Fin β§ π΅ β π) β§ π΅ β Fin) β ((β―βπ΄) β€ (β―βπ΅) β π΄ βΌ π΅)) |
89 | | hashxrcl 14264 |
. . . . . 6
β’ (π΄ β Fin β
(β―βπ΄) β
β*) |
90 | 89 | ad2antrr 725 |
. . . . 5
β’ (((π΄ β Fin β§ π΅ β π) β§ Β¬ π΅ β Fin) β (β―βπ΄) β
β*) |
91 | | pnfge 13058 |
. . . . 5
β’
((β―βπ΄)
β β* β (β―βπ΄) β€ +β) |
92 | 90, 91 | syl 17 |
. . . 4
β’ (((π΄ β Fin β§ π΅ β π) β§ Β¬ π΅ β Fin) β (β―βπ΄) β€
+β) |
93 | | hashinf 14242 |
. . . . 5
β’ ((π΅ β π β§ Β¬ π΅ β Fin) β (β―βπ΅) = +β) |
94 | 93 | adantll 713 |
. . . 4
β’ (((π΄ β Fin β§ π΅ β π) β§ Β¬ π΅ β Fin) β (β―βπ΅) = +β) |
95 | 92, 94 | breqtrrd 5138 |
. . 3
β’ (((π΄ β Fin β§ π΅ β π) β§ Β¬ π΅ β Fin) β (β―βπ΄) β€ (β―βπ΅)) |
96 | | isinffi 9935 |
. . . . . 6
β’ ((Β¬
π΅ β Fin β§ π΄ β Fin) β βπ π:π΄β1-1βπ΅) |
97 | 96 | ancoms 460 |
. . . . 5
β’ ((π΄ β Fin β§ Β¬ π΅ β Fin) β βπ π:π΄β1-1βπ΅) |
98 | 97 | adantlr 714 |
. . . 4
β’ (((π΄ β Fin β§ π΅ β π) β§ Β¬ π΅ β Fin) β βπ π:π΄β1-1βπ΅) |
99 | | brdomg 8903 |
. . . . 5
β’ (π΅ β π β (π΄ βΌ π΅ β βπ π:π΄β1-1βπ΅)) |
100 | 99 | ad2antlr 726 |
. . . 4
β’ (((π΄ β Fin β§ π΅ β π) β§ Β¬ π΅ β Fin) β (π΄ βΌ π΅ β βπ π:π΄β1-1βπ΅)) |
101 | 98, 100 | mpbird 257 |
. . 3
β’ (((π΄ β Fin β§ π΅ β π) β§ Β¬ π΅ β Fin) β π΄ βΌ π΅) |
102 | 95, 101 | 2thd 265 |
. 2
β’ (((π΄ β Fin β§ π΅ β π) β§ Β¬ π΅ β Fin) β ((β―βπ΄) β€ (β―βπ΅) β π΄ βΌ π΅)) |
103 | 88, 102 | pm2.61dan 812 |
1
β’ ((π΄ β Fin β§ π΅ β π) β ((β―βπ΄) β€ (β―βπ΅) β π΄ βΌ π΅)) |