MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  hashf1 Structured version   Visualization version   GIF version

Theorem hashf1 14422
Description: The permutation number โˆฃ ๐ด โˆฃ ! ยท ( โˆฃ ๐ต โˆฃ C โˆฃ ๐ด โˆฃ ) = โˆฃ ๐ต โˆฃ ! / ( โˆฃ ๐ต โˆฃ โˆ’ โˆฃ ๐ด โˆฃ )! counts the number of injections from ๐ด to ๐ต. (Contributed by Mario Carneiro, 21-Jan-2015.)
Assertion
Ref Expression
hashf1 ((๐ด โˆˆ Fin โˆง ๐ต โˆˆ Fin) โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜๐ด)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐ด))))
Distinct variable groups:   ๐ด,๐‘“   ๐ต,๐‘“

Proof of Theorem hashf1
Dummy variables ๐‘ฅ ๐‘ฆ ๐‘ง are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 f1eq2 6776 . . . . . . . . 9 (๐‘ฅ = โˆ… โ†’ (๐‘“:๐‘ฅโ€“1-1โ†’๐ต โ†” ๐‘“:โˆ…โ€“1-1โ†’๐ต))
2 f1fn 6781 . . . . . . . . . . . 12 (๐‘“:โˆ…โ€“1-1โ†’๐ต โ†’ ๐‘“ Fn โˆ…)
3 fn0 6674 . . . . . . . . . . . 12 (๐‘“ Fn โˆ… โ†” ๐‘“ = โˆ…)
42, 3sylib 217 . . . . . . . . . . 11 (๐‘“:โˆ…โ€“1-1โ†’๐ต โ†’ ๐‘“ = โˆ…)
5 f10 6859 . . . . . . . . . . . 12 โˆ…:โˆ…โ€“1-1โ†’๐ต
6 f1eq1 6775 . . . . . . . . . . . 12 (๐‘“ = โˆ… โ†’ (๐‘“:โˆ…โ€“1-1โ†’๐ต โ†” โˆ…:โˆ…โ€“1-1โ†’๐ต))
75, 6mpbiri 258 . . . . . . . . . . 11 (๐‘“ = โˆ… โ†’ ๐‘“:โˆ…โ€“1-1โ†’๐ต)
84, 7impbii 208 . . . . . . . . . 10 (๐‘“:โˆ…โ€“1-1โ†’๐ต โ†” ๐‘“ = โˆ…)
9 velsn 4639 . . . . . . . . . 10 (๐‘“ โˆˆ {โˆ…} โ†” ๐‘“ = โˆ…)
108, 9bitr4i 278 . . . . . . . . 9 (๐‘“:โˆ…โ€“1-1โ†’๐ต โ†” ๐‘“ โˆˆ {โˆ…})
111, 10bitrdi 287 . . . . . . . 8 (๐‘ฅ = โˆ… โ†’ (๐‘“:๐‘ฅโ€“1-1โ†’๐ต โ†” ๐‘“ โˆˆ {โˆ…}))
1211eqabcdv 2862 . . . . . . 7 (๐‘ฅ = โˆ… โ†’ {๐‘“ โˆฃ ๐‘“:๐‘ฅโ€“1-1โ†’๐ต} = {โˆ…})
1312fveq2d 6888 . . . . . 6 (๐‘ฅ = โˆ… โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฅโ€“1-1โ†’๐ต}) = (โ™ฏโ€˜{โˆ…}))
14 0ex 5300 . . . . . . 7 โˆ… โˆˆ V
15 hashsng 14332 . . . . . . 7 (โˆ… โˆˆ V โ†’ (โ™ฏโ€˜{โˆ…}) = 1)
1614, 15ax-mp 5 . . . . . 6 (โ™ฏโ€˜{โˆ…}) = 1
1713, 16eqtrdi 2782 . . . . 5 (๐‘ฅ = โˆ… โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฅโ€“1-1โ†’๐ต}) = 1)
18 fveq2 6884 . . . . . . . . 9 (๐‘ฅ = โˆ… โ†’ (โ™ฏโ€˜๐‘ฅ) = (โ™ฏโ€˜โˆ…))
19 hash0 14330 . . . . . . . . 9 (โ™ฏโ€˜โˆ…) = 0
2018, 19eqtrdi 2782 . . . . . . . 8 (๐‘ฅ = โˆ… โ†’ (โ™ฏโ€˜๐‘ฅ) = 0)
2120fveq2d 6888 . . . . . . 7 (๐‘ฅ = โˆ… โ†’ (!โ€˜(โ™ฏโ€˜๐‘ฅ)) = (!โ€˜0))
22 fac0 14239 . . . . . . 7 (!โ€˜0) = 1
2321, 22eqtrdi 2782 . . . . . 6 (๐‘ฅ = โˆ… โ†’ (!โ€˜(โ™ฏโ€˜๐‘ฅ)) = 1)
2420oveq2d 7420 . . . . . 6 (๐‘ฅ = โˆ… โ†’ ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฅ)) = ((โ™ฏโ€˜๐ต)C0))
2523, 24oveq12d 7422 . . . . 5 (๐‘ฅ = โˆ… โ†’ ((!โ€˜(โ™ฏโ€˜๐‘ฅ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฅ))) = (1 ยท ((โ™ฏโ€˜๐ต)C0)))
2617, 25eqeq12d 2742 . . . 4 (๐‘ฅ = โˆ… โ†’ ((โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฅโ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜๐‘ฅ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฅ))) โ†” 1 = (1 ยท ((โ™ฏโ€˜๐ต)C0))))
2726imbi2d 340 . . 3 (๐‘ฅ = โˆ… โ†’ ((๐ต โˆˆ Fin โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฅโ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜๐‘ฅ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฅ)))) โ†” (๐ต โˆˆ Fin โ†’ 1 = (1 ยท ((โ™ฏโ€˜๐ต)C0)))))
28 f1eq2 6776 . . . . . . 7 (๐‘ฅ = ๐‘ฆ โ†’ (๐‘“:๐‘ฅโ€“1-1โ†’๐ต โ†” ๐‘“:๐‘ฆโ€“1-1โ†’๐ต))
2928abbidv 2795 . . . . . 6 (๐‘ฅ = ๐‘ฆ โ†’ {๐‘“ โˆฃ ๐‘“:๐‘ฅโ€“1-1โ†’๐ต} = {๐‘“ โˆฃ ๐‘“:๐‘ฆโ€“1-1โ†’๐ต})
3029fveq2d 6888 . . . . 5 (๐‘ฅ = ๐‘ฆ โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฅโ€“1-1โ†’๐ต}) = (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฆโ€“1-1โ†’๐ต}))
31 2fveq3 6889 . . . . . 6 (๐‘ฅ = ๐‘ฆ โ†’ (!โ€˜(โ™ฏโ€˜๐‘ฅ)) = (!โ€˜(โ™ฏโ€˜๐‘ฆ)))
32 fveq2 6884 . . . . . . 7 (๐‘ฅ = ๐‘ฆ โ†’ (โ™ฏโ€˜๐‘ฅ) = (โ™ฏโ€˜๐‘ฆ))
3332oveq2d 7420 . . . . . 6 (๐‘ฅ = ๐‘ฆ โ†’ ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฅ)) = ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฆ)))
3431, 33oveq12d 7422 . . . . 5 (๐‘ฅ = ๐‘ฆ โ†’ ((!โ€˜(โ™ฏโ€˜๐‘ฅ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฅ))) = ((!โ€˜(โ™ฏโ€˜๐‘ฆ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฆ))))
3530, 34eqeq12d 2742 . . . 4 (๐‘ฅ = ๐‘ฆ โ†’ ((โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฅโ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜๐‘ฅ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฅ))) โ†” (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฆโ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜๐‘ฆ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฆ)))))
3635imbi2d 340 . . 3 (๐‘ฅ = ๐‘ฆ โ†’ ((๐ต โˆˆ Fin โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฅโ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜๐‘ฅ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฅ)))) โ†” (๐ต โˆˆ Fin โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฆโ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜๐‘ฆ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฆ))))))
37 f1eq2 6776 . . . . . . 7 (๐‘ฅ = (๐‘ฆ โˆช {๐‘ง}) โ†’ (๐‘“:๐‘ฅโ€“1-1โ†’๐ต โ†” ๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต))
3837abbidv 2795 . . . . . 6 (๐‘ฅ = (๐‘ฆ โˆช {๐‘ง}) โ†’ {๐‘“ โˆฃ ๐‘“:๐‘ฅโ€“1-1โ†’๐ต} = {๐‘“ โˆฃ ๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต})
3938fveq2d 6888 . . . . 5 (๐‘ฅ = (๐‘ฆ โˆช {๐‘ง}) โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฅโ€“1-1โ†’๐ต}) = (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต}))
40 2fveq3 6889 . . . . . 6 (๐‘ฅ = (๐‘ฆ โˆช {๐‘ง}) โ†’ (!โ€˜(โ™ฏโ€˜๐‘ฅ)) = (!โ€˜(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))))
41 fveq2 6884 . . . . . . 7 (๐‘ฅ = (๐‘ฆ โˆช {๐‘ง}) โ†’ (โ™ฏโ€˜๐‘ฅ) = (โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง})))
4241oveq2d 7420 . . . . . 6 (๐‘ฅ = (๐‘ฆ โˆช {๐‘ง}) โ†’ ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฅ)) = ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))))
4340, 42oveq12d 7422 . . . . 5 (๐‘ฅ = (๐‘ฆ โˆช {๐‘ง}) โ†’ ((!โ€˜(โ™ฏโ€˜๐‘ฅ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฅ))) = ((!โ€˜(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง})))))
4439, 43eqeq12d 2742 . . . 4 (๐‘ฅ = (๐‘ฆ โˆช {๐‘ง}) โ†’ ((โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฅโ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜๐‘ฅ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฅ))) โ†” (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))))))
4544imbi2d 340 . . 3 (๐‘ฅ = (๐‘ฆ โˆช {๐‘ง}) โ†’ ((๐ต โˆˆ Fin โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฅโ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜๐‘ฅ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฅ)))) โ†” (๐ต โˆˆ Fin โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง})))))))
46 f1eq2 6776 . . . . . . 7 (๐‘ฅ = ๐ด โ†’ (๐‘“:๐‘ฅโ€“1-1โ†’๐ต โ†” ๐‘“:๐ดโ€“1-1โ†’๐ต))
4746abbidv 2795 . . . . . 6 (๐‘ฅ = ๐ด โ†’ {๐‘“ โˆฃ ๐‘“:๐‘ฅโ€“1-1โ†’๐ต} = {๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต})
4847fveq2d 6888 . . . . 5 (๐‘ฅ = ๐ด โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฅโ€“1-1โ†’๐ต}) = (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต}))
49 2fveq3 6889 . . . . . 6 (๐‘ฅ = ๐ด โ†’ (!โ€˜(โ™ฏโ€˜๐‘ฅ)) = (!โ€˜(โ™ฏโ€˜๐ด)))
50 fveq2 6884 . . . . . . 7 (๐‘ฅ = ๐ด โ†’ (โ™ฏโ€˜๐‘ฅ) = (โ™ฏโ€˜๐ด))
5150oveq2d 7420 . . . . . 6 (๐‘ฅ = ๐ด โ†’ ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฅ)) = ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐ด)))
5249, 51oveq12d 7422 . . . . 5 (๐‘ฅ = ๐ด โ†’ ((!โ€˜(โ™ฏโ€˜๐‘ฅ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฅ))) = ((!โ€˜(โ™ฏโ€˜๐ด)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐ด))))
5348, 52eqeq12d 2742 . . . 4 (๐‘ฅ = ๐ด โ†’ ((โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฅโ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜๐‘ฅ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฅ))) โ†” (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜๐ด)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐ด)))))
5453imbi2d 340 . . 3 (๐‘ฅ = ๐ด โ†’ ((๐ต โˆˆ Fin โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฅโ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜๐‘ฅ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฅ)))) โ†” (๐ต โˆˆ Fin โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜๐ด)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐ด))))))
55 hashcl 14319 . . . . . 6 (๐ต โˆˆ Fin โ†’ (โ™ฏโ€˜๐ต) โˆˆ โ„•0)
56 bcn0 14273 . . . . . 6 ((โ™ฏโ€˜๐ต) โˆˆ โ„•0 โ†’ ((โ™ฏโ€˜๐ต)C0) = 1)
5755, 56syl 17 . . . . 5 (๐ต โˆˆ Fin โ†’ ((โ™ฏโ€˜๐ต)C0) = 1)
5857oveq2d 7420 . . . 4 (๐ต โˆˆ Fin โ†’ (1 ยท ((โ™ฏโ€˜๐ต)C0)) = (1 ยท 1))
59 1t1e1 12375 . . . 4 (1 ยท 1) = 1
6058, 59eqtr2di 2783 . . 3 (๐ต โˆˆ Fin โ†’ 1 = (1 ยท ((โ™ฏโ€˜๐ต)C0)))
61 abn0 4375 . . . . . . . . . . . . 13 ({๐‘“ โˆฃ ๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต} โ‰  โˆ… โ†” โˆƒ๐‘“ ๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต)
62 f1domg 8967 . . . . . . . . . . . . . . . 16 (๐ต โˆˆ Fin โ†’ (๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต โ†’ (๐‘ฆ โˆช {๐‘ง}) โ‰ผ ๐ต))
6362adantr 480 . . . . . . . . . . . . . . 15 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ (๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต โ†’ (๐‘ฆ โˆช {๐‘ง}) โ‰ผ ๐ต))
64 hashunsng 14355 . . . . . . . . . . . . . . . . . . 19 (๐‘ง โˆˆ V โ†’ ((๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ) โ†’ (โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง})) = ((โ™ฏโ€˜๐‘ฆ) + 1)))
6564elv 3474 . . . . . . . . . . . . . . . . . 18 ((๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ) โ†’ (โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง})) = ((โ™ฏโ€˜๐‘ฆ) + 1))
6665adantl 481 . . . . . . . . . . . . . . . . 17 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ (โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง})) = ((โ™ฏโ€˜๐‘ฆ) + 1))
6766breq1d 5151 . . . . . . . . . . . . . . . 16 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ ((โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง})) โ‰ค (โ™ฏโ€˜๐ต) โ†” ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)))
68 simprl 768 . . . . . . . . . . . . . . . . . 18 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ ๐‘ฆ โˆˆ Fin)
69 snfi 9043 . . . . . . . . . . . . . . . . . 18 {๐‘ง} โˆˆ Fin
70 unfi 9171 . . . . . . . . . . . . . . . . . 18 ((๐‘ฆ โˆˆ Fin โˆง {๐‘ง} โˆˆ Fin) โ†’ (๐‘ฆ โˆช {๐‘ง}) โˆˆ Fin)
7168, 69, 70sylancl 585 . . . . . . . . . . . . . . . . 17 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ (๐‘ฆ โˆช {๐‘ง}) โˆˆ Fin)
72 simpl 482 . . . . . . . . . . . . . . . . 17 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ ๐ต โˆˆ Fin)
73 hashdom 14342 . . . . . . . . . . . . . . . . 17 (((๐‘ฆ โˆช {๐‘ง}) โˆˆ Fin โˆง ๐ต โˆˆ Fin) โ†’ ((โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง})) โ‰ค (โ™ฏโ€˜๐ต) โ†” (๐‘ฆ โˆช {๐‘ง}) โ‰ผ ๐ต))
7471, 72, 73syl2anc 583 . . . . . . . . . . . . . . . 16 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ ((โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง})) โ‰ค (โ™ฏโ€˜๐ต) โ†” (๐‘ฆ โˆช {๐‘ง}) โ‰ผ ๐ต))
75 hashcl 14319 . . . . . . . . . . . . . . . . . . . 20 (๐‘ฆ โˆˆ Fin โ†’ (โ™ฏโ€˜๐‘ฆ) โˆˆ โ„•0)
7675ad2antrl 725 . . . . . . . . . . . . . . . . . . 19 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ (โ™ฏโ€˜๐‘ฆ) โˆˆ โ„•0)
77 nn0p1nn 12512 . . . . . . . . . . . . . . . . . . 19 ((โ™ฏโ€˜๐‘ฆ) โˆˆ โ„•0 โ†’ ((โ™ฏโ€˜๐‘ฆ) + 1) โˆˆ โ„•)
7876, 77syl 17 . . . . . . . . . . . . . . . . . 18 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ ((โ™ฏโ€˜๐‘ฆ) + 1) โˆˆ โ„•)
7978nnred 12228 . . . . . . . . . . . . . . . . 17 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ ((โ™ฏโ€˜๐‘ฆ) + 1) โˆˆ โ„)
8055adantr 480 . . . . . . . . . . . . . . . . . 18 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ (โ™ฏโ€˜๐ต) โˆˆ โ„•0)
8180nn0red 12534 . . . . . . . . . . . . . . . . 17 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ (โ™ฏโ€˜๐ต) โˆˆ โ„)
8279, 81lenltd 11361 . . . . . . . . . . . . . . . 16 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ (((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต) โ†” ยฌ (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)))
8367, 74, 823bitr3d 309 . . . . . . . . . . . . . . 15 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ ((๐‘ฆ โˆช {๐‘ง}) โ‰ผ ๐ต โ†” ยฌ (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)))
8463, 83sylibd 238 . . . . . . . . . . . . . 14 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ (๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต โ†’ ยฌ (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)))
8584exlimdv 1928 . . . . . . . . . . . . 13 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ (โˆƒ๐‘“ ๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต โ†’ ยฌ (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)))
8661, 85biimtrid 241 . . . . . . . . . . . 12 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ ({๐‘“ โˆฃ ๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต} โ‰  โˆ… โ†’ ยฌ (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)))
8786necon4ad 2953 . . . . . . . . . . 11 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ ((โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1) โ†’ {๐‘“ โˆฃ ๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต} = โˆ…))
8887imp 406 . . . . . . . . . 10 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)) โ†’ {๐‘“ โˆฃ ๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต} = โˆ…)
8988fveq2d 6888 . . . . . . . . 9 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)) โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต}) = (โ™ฏโ€˜โˆ…))
90 hashcl 14319 . . . . . . . . . . . . . 14 ((๐‘ฆ โˆช {๐‘ง}) โˆˆ Fin โ†’ (โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง})) โˆˆ โ„•0)
9171, 90syl 17 . . . . . . . . . . . . 13 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ (โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง})) โˆˆ โ„•0)
9291faccld 14247 . . . . . . . . . . . 12 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ (!โ€˜(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) โˆˆ โ„•)
9392nncnd 12229 . . . . . . . . . . 11 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ (!โ€˜(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) โˆˆ โ„‚)
9493adantr 480 . . . . . . . . . 10 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)) โ†’ (!โ€˜(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) โˆˆ โ„‚)
9594mul01d 11414 . . . . . . . . 9 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)) โ†’ ((!โ€˜(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) ยท 0) = 0)
9619, 89, 953eqtr4a 2792 . . . . . . . 8 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)) โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) ยท 0))
9766adantr 480 . . . . . . . . . . 11 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)) โ†’ (โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง})) = ((โ™ฏโ€˜๐‘ฆ) + 1))
9897oveq2d 7420 . . . . . . . . . 10 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)) โ†’ ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) = ((โ™ฏโ€˜๐ต)C((โ™ฏโ€˜๐‘ฆ) + 1)))
9980adantr 480 . . . . . . . . . . 11 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)) โ†’ (โ™ฏโ€˜๐ต) โˆˆ โ„•0)
10078adantr 480 . . . . . . . . . . . 12 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)) โ†’ ((โ™ฏโ€˜๐‘ฆ) + 1) โˆˆ โ„•)
101100nnzd 12586 . . . . . . . . . . 11 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)) โ†’ ((โ™ฏโ€˜๐‘ฆ) + 1) โˆˆ โ„ค)
102 animorr 975 . . . . . . . . . . 11 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)) โ†’ (((โ™ฏโ€˜๐‘ฆ) + 1) < 0 โˆจ (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)))
103 bcval4 14270 . . . . . . . . . . 11 (((โ™ฏโ€˜๐ต) โˆˆ โ„•0 โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โˆˆ โ„ค โˆง (((โ™ฏโ€˜๐‘ฆ) + 1) < 0 โˆจ (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1))) โ†’ ((โ™ฏโ€˜๐ต)C((โ™ฏโ€˜๐‘ฆ) + 1)) = 0)
10499, 101, 102, 103syl3anc 1368 . . . . . . . . . 10 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)) โ†’ ((โ™ฏโ€˜๐ต)C((โ™ฏโ€˜๐‘ฆ) + 1)) = 0)
10598, 104eqtrd 2766 . . . . . . . . 9 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)) โ†’ ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) = 0)
106105oveq2d 7420 . . . . . . . 8 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)) โ†’ ((!โ€˜(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง})))) = ((!โ€˜(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) ยท 0))
10796, 106eqtr4d 2769 . . . . . . 7 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)) โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง})))))
108107a1d 25 . . . . . 6 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)) โ†’ ((โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฆโ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜๐‘ฆ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฆ))) โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))))))
109 oveq2 7412 . . . . . . 7 ((โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฆโ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜๐‘ฆ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฆ))) โ†’ (((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) ยท (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฆโ€“1-1โ†’๐ต})) = (((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) ยท ((!โ€˜(โ™ฏโ€˜๐‘ฆ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฆ)))))
11068adantr 480 . . . . . . . . 9 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ๐‘ฆ โˆˆ Fin)
11172adantr 480 . . . . . . . . 9 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ๐ต โˆˆ Fin)
112 simplrr 775 . . . . . . . . 9 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ยฌ ๐‘ง โˆˆ ๐‘ฆ)
113 simpr 484 . . . . . . . . 9 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต))
114110, 111, 112, 113hashf1lem2 14421 . . . . . . . 8 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต}) = (((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) ยท (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฆโ€“1-1โ†’๐ต})))
11580adantr 480 . . . . . . . . . . . . . 14 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (โ™ฏโ€˜๐ต) โˆˆ โ„•0)
116115faccld 14247 . . . . . . . . . . . . 13 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (!โ€˜(โ™ฏโ€˜๐ต)) โˆˆ โ„•)
117116nncnd 12229 . . . . . . . . . . . 12 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (!โ€˜(โ™ฏโ€˜๐ต)) โˆˆ โ„‚)
11876adantr 480 . . . . . . . . . . . . . . . 16 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (โ™ฏโ€˜๐‘ฆ) โˆˆ โ„•0)
119 peano2nn0 12513 . . . . . . . . . . . . . . . 16 ((โ™ฏโ€˜๐‘ฆ) โˆˆ โ„•0 โ†’ ((โ™ฏโ€˜๐‘ฆ) + 1) โˆˆ โ„•0)
120118, 119syl 17 . . . . . . . . . . . . . . 15 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((โ™ฏโ€˜๐‘ฆ) + 1) โˆˆ โ„•0)
121 nn0sub2 12624 . . . . . . . . . . . . . . 15 ((((โ™ฏโ€˜๐‘ฆ) + 1) โˆˆ โ„•0 โˆง (โ™ฏโ€˜๐ต) โˆˆ โ„•0 โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1)) โˆˆ โ„•0)
122120, 115, 113, 121syl3anc 1368 . . . . . . . . . . . . . 14 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1)) โˆˆ โ„•0)
123122faccld 14247 . . . . . . . . . . . . 13 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1))) โˆˆ โ„•)
124123nncnd 12229 . . . . . . . . . . . 12 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1))) โˆˆ โ„‚)
125123nnne0d 12263 . . . . . . . . . . . 12 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1))) โ‰  0)
126117, 124, 125divcld 11991 . . . . . . . . . . 11 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1)))) โˆˆ โ„‚)
127120faccld 14247 . . . . . . . . . . . 12 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (!โ€˜((โ™ฏโ€˜๐‘ฆ) + 1)) โˆˆ โ„•)
128127nncnd 12229 . . . . . . . . . . 11 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (!โ€˜((โ™ฏโ€˜๐‘ฆ) + 1)) โˆˆ โ„‚)
129127nnne0d 12263 . . . . . . . . . . 11 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (!โ€˜((โ™ฏโ€˜๐‘ฆ) + 1)) โ‰  0)
130126, 128, 129divcan2d 11993 . . . . . . . . . 10 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((!โ€˜((โ™ฏโ€˜๐‘ฆ) + 1)) ยท (((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1)))) / (!โ€˜((โ™ฏโ€˜๐‘ฆ) + 1)))) = ((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1)))))
131115nn0cnd 12535 . . . . . . . . . . . 12 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (โ™ฏโ€˜๐ต) โˆˆ โ„‚)
132118nn0cnd 12535 . . . . . . . . . . . 12 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (โ™ฏโ€˜๐‘ฆ) โˆˆ โ„‚)
133131, 132subcld 11572 . . . . . . . . . . 11 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) โˆˆ โ„‚)
134 ax-1cn 11167 . . . . . . . . . . . . . 14 1 โˆˆ โ„‚
135 npcan 11470 . . . . . . . . . . . . . 14 ((((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) โˆˆ โ„‚ โˆง 1 โˆˆ โ„‚) โ†’ ((((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) โˆ’ 1) + 1) = ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)))
136133, 134, 135sylancl 585 . . . . . . . . . . . . 13 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) โˆ’ 1) + 1) = ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)))
137 1cnd 11210 . . . . . . . . . . . . . . . 16 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ 1 โˆˆ โ„‚)
138131, 132, 137subsub4d 11603 . . . . . . . . . . . . . . 15 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) โˆ’ 1) = ((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1)))
139138, 122eqeltrd 2827 . . . . . . . . . . . . . 14 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) โˆ’ 1) โˆˆ โ„•0)
140 nn0p1nn 12512 . . . . . . . . . . . . . 14 ((((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) โˆ’ 1) โˆˆ โ„•0 โ†’ ((((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) โˆ’ 1) + 1) โˆˆ โ„•)
141139, 140syl 17 . . . . . . . . . . . . 13 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) โˆ’ 1) + 1) โˆˆ โ„•)
142136, 141eqeltrrd 2828 . . . . . . . . . . . 12 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) โˆˆ โ„•)
143142nnne0d 12263 . . . . . . . . . . 11 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) โ‰  0)
144126, 133, 143divcan2d 11993 . . . . . . . . . 10 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) ยท (((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1)))) / ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)))) = ((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1)))))
145130, 144eqtr4d 2769 . . . . . . . . 9 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((!โ€˜((โ™ฏโ€˜๐‘ฆ) + 1)) ยท (((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1)))) / (!โ€˜((โ™ฏโ€˜๐‘ฆ) + 1)))) = (((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) ยท (((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1)))) / ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)))))
14666adantr 480 . . . . . . . . . . 11 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง})) = ((โ™ฏโ€˜๐‘ฆ) + 1))
147146fveq2d 6888 . . . . . . . . . 10 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (!โ€˜(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) = (!โ€˜((โ™ฏโ€˜๐‘ฆ) + 1)))
148 nn0uz 12865 . . . . . . . . . . . . . . 15 โ„•0 = (โ„คโ‰ฅโ€˜0)
149120, 148eleqtrdi 2837 . . . . . . . . . . . . . 14 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((โ™ฏโ€˜๐‘ฆ) + 1) โˆˆ (โ„คโ‰ฅโ€˜0))
150115nn0zd 12585 . . . . . . . . . . . . . 14 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (โ™ฏโ€˜๐ต) โˆˆ โ„ค)
151 elfz5 13496 . . . . . . . . . . . . . 14 ((((โ™ฏโ€˜๐‘ฆ) + 1) โˆˆ (โ„คโ‰ฅโ€˜0) โˆง (โ™ฏโ€˜๐ต) โˆˆ โ„ค) โ†’ (((โ™ฏโ€˜๐‘ฆ) + 1) โˆˆ (0...(โ™ฏโ€˜๐ต)) โ†” ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)))
152149, 150, 151syl2anc 583 . . . . . . . . . . . . 13 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (((โ™ฏโ€˜๐‘ฆ) + 1) โˆˆ (0...(โ™ฏโ€˜๐ต)) โ†” ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)))
153113, 152mpbird 257 . . . . . . . . . . . 12 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((โ™ฏโ€˜๐‘ฆ) + 1) โˆˆ (0...(โ™ฏโ€˜๐ต)))
154 bcval2 14268 . . . . . . . . . . . 12 (((โ™ฏโ€˜๐‘ฆ) + 1) โˆˆ (0...(โ™ฏโ€˜๐ต)) โ†’ ((โ™ฏโ€˜๐ต)C((โ™ฏโ€˜๐‘ฆ) + 1)) = ((!โ€˜(โ™ฏโ€˜๐ต)) / ((!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1))) ยท (!โ€˜((โ™ฏโ€˜๐‘ฆ) + 1)))))
155153, 154syl 17 . . . . . . . . . . 11 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((โ™ฏโ€˜๐ต)C((โ™ฏโ€˜๐‘ฆ) + 1)) = ((!โ€˜(โ™ฏโ€˜๐ต)) / ((!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1))) ยท (!โ€˜((โ™ฏโ€˜๐‘ฆ) + 1)))))
156146oveq2d 7420 . . . . . . . . . . 11 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) = ((โ™ฏโ€˜๐ต)C((โ™ฏโ€˜๐‘ฆ) + 1)))
157117, 124, 128, 125, 129divdiv1d 12022 . . . . . . . . . . 11 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1)))) / (!โ€˜((โ™ฏโ€˜๐‘ฆ) + 1))) = ((!โ€˜(โ™ฏโ€˜๐ต)) / ((!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1))) ยท (!โ€˜((โ™ฏโ€˜๐‘ฆ) + 1)))))
158155, 156, 1573eqtr4d 2776 . . . . . . . . . 10 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) = (((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1)))) / (!โ€˜((โ™ฏโ€˜๐‘ฆ) + 1))))
159147, 158oveq12d 7422 . . . . . . . . 9 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((!โ€˜(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง})))) = ((!โ€˜((โ™ฏโ€˜๐‘ฆ) + 1)) ยท (((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1)))) / (!โ€˜((โ™ฏโ€˜๐‘ฆ) + 1)))))
160118, 148eleqtrdi 2837 . . . . . . . . . . . . . . 15 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (โ™ฏโ€˜๐‘ฆ) โˆˆ (โ„คโ‰ฅโ€˜0))
161 peano2fzr 13517 . . . . . . . . . . . . . . 15 (((โ™ฏโ€˜๐‘ฆ) โˆˆ (โ„คโ‰ฅโ€˜0) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โˆˆ (0...(โ™ฏโ€˜๐ต))) โ†’ (โ™ฏโ€˜๐‘ฆ) โˆˆ (0...(โ™ฏโ€˜๐ต)))
162160, 153, 161syl2anc 583 . . . . . . . . . . . . . 14 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (โ™ฏโ€˜๐‘ฆ) โˆˆ (0...(โ™ฏโ€˜๐ต)))
163 bcval2 14268 . . . . . . . . . . . . . 14 ((โ™ฏโ€˜๐‘ฆ) โˆˆ (0...(โ™ฏโ€˜๐ต)) โ†’ ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฆ)) = ((!โ€˜(โ™ฏโ€˜๐ต)) / ((!โ€˜((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ))) ยท (!โ€˜(โ™ฏโ€˜๐‘ฆ)))))
164162, 163syl 17 . . . . . . . . . . . . 13 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฆ)) = ((!โ€˜(โ™ฏโ€˜๐ต)) / ((!โ€˜((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ))) ยท (!โ€˜(โ™ฏโ€˜๐‘ฆ)))))
165 elfzle2 13508 . . . . . . . . . . . . . . . . . 18 ((โ™ฏโ€˜๐‘ฆ) โˆˆ (0...(โ™ฏโ€˜๐ต)) โ†’ (โ™ฏโ€˜๐‘ฆ) โ‰ค (โ™ฏโ€˜๐ต))
166162, 165syl 17 . . . . . . . . . . . . . . . . 17 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (โ™ฏโ€˜๐‘ฆ) โ‰ค (โ™ฏโ€˜๐ต))
167 nn0sub2 12624 . . . . . . . . . . . . . . . . 17 (((โ™ฏโ€˜๐‘ฆ) โˆˆ โ„•0 โˆง (โ™ฏโ€˜๐ต) โˆˆ โ„•0 โˆง (โ™ฏโ€˜๐‘ฆ) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) โˆˆ โ„•0)
168118, 115, 166, 167syl3anc 1368 . . . . . . . . . . . . . . . 16 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) โˆˆ โ„•0)
169168faccld 14247 . . . . . . . . . . . . . . 15 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ))) โˆˆ โ„•)
170169nncnd 12229 . . . . . . . . . . . . . 14 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ))) โˆˆ โ„‚)
171118faccld 14247 . . . . . . . . . . . . . . 15 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (!โ€˜(โ™ฏโ€˜๐‘ฆ)) โˆˆ โ„•)
172171nncnd 12229 . . . . . . . . . . . . . 14 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (!โ€˜(โ™ฏโ€˜๐‘ฆ)) โˆˆ โ„‚)
173169nnne0d 12263 . . . . . . . . . . . . . 14 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ))) โ‰  0)
174171nnne0d 12263 . . . . . . . . . . . . . 14 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (!โ€˜(โ™ฏโ€˜๐‘ฆ)) โ‰  0)
175117, 170, 172, 173, 174divdiv1d 12022 . . . . . . . . . . . . 13 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)))) / (!โ€˜(โ™ฏโ€˜๐‘ฆ))) = ((!โ€˜(โ™ฏโ€˜๐ต)) / ((!โ€˜((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ))) ยท (!โ€˜(โ™ฏโ€˜๐‘ฆ)))))
176164, 175eqtr4d 2769 . . . . . . . . . . . 12 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฆ)) = (((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)))) / (!โ€˜(โ™ฏโ€˜๐‘ฆ))))
177176oveq2d 7420 . . . . . . . . . . 11 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((!โ€˜(โ™ฏโ€˜๐‘ฆ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฆ))) = ((!โ€˜(โ™ฏโ€˜๐‘ฆ)) ยท (((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)))) / (!โ€˜(โ™ฏโ€˜๐‘ฆ)))))
178 facnn2 14245 . . . . . . . . . . . . . . 15 (((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) โˆˆ โ„• โ†’ (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ))) = ((!โ€˜(((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) โˆ’ 1)) ยท ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ))))
179142, 178syl 17 . . . . . . . . . . . . . 14 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ))) = ((!โ€˜(((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) โˆ’ 1)) ยท ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ))))
180138fveq2d 6888 . . . . . . . . . . . . . . 15 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (!โ€˜(((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) โˆ’ 1)) = (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1))))
181180oveq1d 7419 . . . . . . . . . . . . . 14 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((!โ€˜(((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) โˆ’ 1)) ยท ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ))) = ((!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1))) ยท ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ))))
182179, 181eqtrd 2766 . . . . . . . . . . . . 13 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ))) = ((!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1))) ยท ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ))))
183182oveq2d 7420 . . . . . . . . . . . 12 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)))) = ((!โ€˜(โ™ฏโ€˜๐ต)) / ((!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1))) ยท ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)))))
184117, 170, 173divcld 11991 . . . . . . . . . . . . 13 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)))) โˆˆ โ„‚)
185184, 172, 174divcan2d 11993 . . . . . . . . . . . 12 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((!โ€˜(โ™ฏโ€˜๐‘ฆ)) ยท (((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)))) / (!โ€˜(โ™ฏโ€˜๐‘ฆ)))) = ((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)))))
186117, 124, 133, 125, 143divdiv1d 12022 . . . . . . . . . . . 12 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1)))) / ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ))) = ((!โ€˜(โ™ฏโ€˜๐ต)) / ((!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1))) ยท ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)))))
187183, 185, 1863eqtr4d 2776 . . . . . . . . . . 11 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((!โ€˜(โ™ฏโ€˜๐‘ฆ)) ยท (((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)))) / (!โ€˜(โ™ฏโ€˜๐‘ฆ)))) = (((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1)))) / ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ))))
188177, 187eqtrd 2766 . . . . . . . . . 10 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((!โ€˜(โ™ฏโ€˜๐‘ฆ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฆ))) = (((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1)))) / ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ))))
189188oveq2d 7420 . . . . . . . . 9 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) ยท ((!โ€˜(โ™ฏโ€˜๐‘ฆ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฆ)))) = (((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) ยท (((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1)))) / ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)))))
190145, 159, 1893eqtr4d 2776 . . . . . . . 8 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((!โ€˜(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง})))) = (((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) ยท ((!โ€˜(โ™ฏโ€˜๐‘ฆ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฆ)))))
191114, 190eqeq12d 2742 . . . . . . 7 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง})))) โ†” (((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) ยท (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฆโ€“1-1โ†’๐ต})) = (((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) ยท ((!โ€˜(โ™ฏโ€˜๐‘ฆ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฆ))))))
192109, 191imbitrrid 245 . . . . . 6 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฆโ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜๐‘ฆ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฆ))) โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))))))
193108, 192, 81, 79ltlecasei 11323 . . . . 5 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ ((โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฆโ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜๐‘ฆ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฆ))) โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))))))
194193expcom 413 . . . 4 ((๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ) โ†’ (๐ต โˆˆ Fin โ†’ ((โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฆโ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜๐‘ฆ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฆ))) โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง})))))))
195194a2d 29 . . 3 ((๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ) โ†’ ((๐ต โˆˆ Fin โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฆโ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜๐‘ฆ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฆ)))) โ†’ (๐ต โˆˆ Fin โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง})))))))
19627, 36, 45, 54, 60, 195findcard2s 9164 . 2 (๐ด โˆˆ Fin โ†’ (๐ต โˆˆ Fin โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜๐ด)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐ด)))))
197196imp 406 1 ((๐ด โˆˆ Fin โˆง ๐ต โˆˆ Fin) โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜๐ด)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐ด))))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 395   โˆจ wo 844   = wceq 1533  โˆƒwex 1773   โˆˆ wcel 2098  {cab 2703   โ‰  wne 2934  Vcvv 3468   โˆช cun 3941  โˆ…c0 4317  {csn 4623   class class class wbr 5141   Fn wfn 6531  โ€“1-1โ†’wf1 6533  โ€˜cfv 6536  (class class class)co 7404   โ‰ผ cdom 8936  Fincfn 8938  โ„‚cc 11107  0cc0 11109  1c1 11110   + caddc 11112   ยท cmul 11114   < clt 11249   โ‰ค cle 11250   โˆ’ cmin 11445   / cdiv 11872  โ„•cn 12213  โ„•0cn0 12473  โ„คcz 12559  โ„คโ‰ฅcuz 12823  ...cfz 13487  !cfa 14236  Ccbc 14265  โ™ฏchash 14293
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2697  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7721  ax-cnex 11165  ax-resscn 11166  ax-1cn 11167  ax-icn 11168  ax-addcl 11169  ax-addrcl 11170  ax-mulcl 11171  ax-mulrcl 11172  ax-mulcom 11173  ax-addass 11174  ax-mulass 11175  ax-distr 11176  ax-i2m1 11177  ax-1ne0 11178  ax-1rid 11179  ax-rnegex 11180  ax-rrecex 11181  ax-cnre 11182  ax-pre-lttri 11183  ax-pre-lttrn 11184  ax-pre-ltadd 11185  ax-pre-mulgt0 11186
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-nel 3041  df-ral 3056  df-rex 3065  df-rmo 3370  df-reu 3371  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-pss 3962  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-int 4944  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6293  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6488  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7360  df-ov 7407  df-oprab 7408  df-mpo 7409  df-om 7852  df-1st 7971  df-2nd 7972  df-frecs 8264  df-wrecs 8295  df-recs 8369  df-rdg 8408  df-1o 8464  df-oadd 8468  df-er 8702  df-map 8821  df-pm 8822  df-en 8939  df-dom 8940  df-sdom 8941  df-fin 8942  df-dju 9895  df-card 9933  df-pnf 11251  df-mnf 11252  df-xr 11253  df-ltxr 11254  df-le 11255  df-sub 11447  df-neg 11448  df-div 11873  df-nn 12214  df-n0 12474  df-xnn0 12546  df-z 12560  df-uz 12824  df-fz 13488  df-seq 13970  df-fac 14237  df-bc 14266  df-hash 14294
This theorem is referenced by:  hashfac  14423  birthdaylem2  26835
  Copyright terms: Public domain W3C validator