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

Theorem hashf1 14363
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 6739 . . . . . . . . 9 (๐‘ฅ = โˆ… โ†’ (๐‘“:๐‘ฅโ€“1-1โ†’๐ต โ†” ๐‘“:โˆ…โ€“1-1โ†’๐ต))
2 f1fn 6744 . . . . . . . . . . . 12 (๐‘“:โˆ…โ€“1-1โ†’๐ต โ†’ ๐‘“ Fn โˆ…)
3 fn0 6637 . . . . . . . . . . . 12 (๐‘“ Fn โˆ… โ†” ๐‘“ = โˆ…)
42, 3sylib 217 . . . . . . . . . . 11 (๐‘“:โˆ…โ€“1-1โ†’๐ต โ†’ ๐‘“ = โˆ…)
5 f10 6822 . . . . . . . . . . . 12 โˆ…:โˆ…โ€“1-1โ†’๐ต
6 f1eq1 6738 . . . . . . . . . . . 12 (๐‘“ = โˆ… โ†’ (๐‘“:โˆ…โ€“1-1โ†’๐ต โ†” โˆ…:โˆ…โ€“1-1โ†’๐ต))
75, 6mpbiri 258 . . . . . . . . . . 11 (๐‘“ = โˆ… โ†’ ๐‘“:โˆ…โ€“1-1โ†’๐ต)
84, 7impbii 208 . . . . . . . . . 10 (๐‘“:โˆ…โ€“1-1โ†’๐ต โ†” ๐‘“ = โˆ…)
9 velsn 4607 . . . . . . . . . 10 (๐‘“ โˆˆ {โˆ…} โ†” ๐‘“ = โˆ…)
108, 9bitr4i 278 . . . . . . . . 9 (๐‘“:โˆ…โ€“1-1โ†’๐ต โ†” ๐‘“ โˆˆ {โˆ…})
111, 10bitrdi 287 . . . . . . . 8 (๐‘ฅ = โˆ… โ†’ (๐‘“:๐‘ฅโ€“1-1โ†’๐ต โ†” ๐‘“ โˆˆ {โˆ…}))
1211abbi1dv 2873 . . . . . . 7 (๐‘ฅ = โˆ… โ†’ {๐‘“ โˆฃ ๐‘“:๐‘ฅโ€“1-1โ†’๐ต} = {โˆ…})
1312fveq2d 6851 . . . . . 6 (๐‘ฅ = โˆ… โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฅโ€“1-1โ†’๐ต}) = (โ™ฏโ€˜{โˆ…}))
14 0ex 5269 . . . . . . 7 โˆ… โˆˆ V
15 hashsng 14276 . . . . . . 7 (โˆ… โˆˆ V โ†’ (โ™ฏโ€˜{โˆ…}) = 1)
1614, 15ax-mp 5 . . . . . 6 (โ™ฏโ€˜{โˆ…}) = 1
1713, 16eqtrdi 2793 . . . . 5 (๐‘ฅ = โˆ… โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฅโ€“1-1โ†’๐ต}) = 1)
18 fveq2 6847 . . . . . . . . 9 (๐‘ฅ = โˆ… โ†’ (โ™ฏโ€˜๐‘ฅ) = (โ™ฏโ€˜โˆ…))
19 hash0 14274 . . . . . . . . 9 (โ™ฏโ€˜โˆ…) = 0
2018, 19eqtrdi 2793 . . . . . . . 8 (๐‘ฅ = โˆ… โ†’ (โ™ฏโ€˜๐‘ฅ) = 0)
2120fveq2d 6851 . . . . . . 7 (๐‘ฅ = โˆ… โ†’ (!โ€˜(โ™ฏโ€˜๐‘ฅ)) = (!โ€˜0))
22 fac0 14183 . . . . . . 7 (!โ€˜0) = 1
2321, 22eqtrdi 2793 . . . . . 6 (๐‘ฅ = โˆ… โ†’ (!โ€˜(โ™ฏโ€˜๐‘ฅ)) = 1)
2420oveq2d 7378 . . . . . 6 (๐‘ฅ = โˆ… โ†’ ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฅ)) = ((โ™ฏโ€˜๐ต)C0))
2523, 24oveq12d 7380 . . . . 5 (๐‘ฅ = โˆ… โ†’ ((!โ€˜(โ™ฏโ€˜๐‘ฅ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฅ))) = (1 ยท ((โ™ฏโ€˜๐ต)C0)))
2617, 25eqeq12d 2753 . . . 4 (๐‘ฅ = โˆ… โ†’ ((โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฅโ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜๐‘ฅ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฅ))) โ†” 1 = (1 ยท ((โ™ฏโ€˜๐ต)C0))))
2726imbi2d 341 . . 3 (๐‘ฅ = โˆ… โ†’ ((๐ต โˆˆ Fin โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฅโ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜๐‘ฅ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฅ)))) โ†” (๐ต โˆˆ Fin โ†’ 1 = (1 ยท ((โ™ฏโ€˜๐ต)C0)))))
28 f1eq2 6739 . . . . . . 7 (๐‘ฅ = ๐‘ฆ โ†’ (๐‘“:๐‘ฅโ€“1-1โ†’๐ต โ†” ๐‘“:๐‘ฆโ€“1-1โ†’๐ต))
2928abbidv 2806 . . . . . 6 (๐‘ฅ = ๐‘ฆ โ†’ {๐‘“ โˆฃ ๐‘“:๐‘ฅโ€“1-1โ†’๐ต} = {๐‘“ โˆฃ ๐‘“:๐‘ฆโ€“1-1โ†’๐ต})
3029fveq2d 6851 . . . . 5 (๐‘ฅ = ๐‘ฆ โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฅโ€“1-1โ†’๐ต}) = (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฆโ€“1-1โ†’๐ต}))
31 2fveq3 6852 . . . . . 6 (๐‘ฅ = ๐‘ฆ โ†’ (!โ€˜(โ™ฏโ€˜๐‘ฅ)) = (!โ€˜(โ™ฏโ€˜๐‘ฆ)))
32 fveq2 6847 . . . . . . 7 (๐‘ฅ = ๐‘ฆ โ†’ (โ™ฏโ€˜๐‘ฅ) = (โ™ฏโ€˜๐‘ฆ))
3332oveq2d 7378 . . . . . 6 (๐‘ฅ = ๐‘ฆ โ†’ ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฅ)) = ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฆ)))
3431, 33oveq12d 7380 . . . . 5 (๐‘ฅ = ๐‘ฆ โ†’ ((!โ€˜(โ™ฏโ€˜๐‘ฅ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฅ))) = ((!โ€˜(โ™ฏโ€˜๐‘ฆ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฆ))))
3530, 34eqeq12d 2753 . . . 4 (๐‘ฅ = ๐‘ฆ โ†’ ((โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฅโ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜๐‘ฅ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฅ))) โ†” (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฆโ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜๐‘ฆ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฆ)))))
3635imbi2d 341 . . 3 (๐‘ฅ = ๐‘ฆ โ†’ ((๐ต โˆˆ Fin โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฅโ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜๐‘ฅ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฅ)))) โ†” (๐ต โˆˆ Fin โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฆโ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜๐‘ฆ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฆ))))))
37 f1eq2 6739 . . . . . . 7 (๐‘ฅ = (๐‘ฆ โˆช {๐‘ง}) โ†’ (๐‘“:๐‘ฅโ€“1-1โ†’๐ต โ†” ๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต))
3837abbidv 2806 . . . . . 6 (๐‘ฅ = (๐‘ฆ โˆช {๐‘ง}) โ†’ {๐‘“ โˆฃ ๐‘“:๐‘ฅโ€“1-1โ†’๐ต} = {๐‘“ โˆฃ ๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต})
3938fveq2d 6851 . . . . 5 (๐‘ฅ = (๐‘ฆ โˆช {๐‘ง}) โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฅโ€“1-1โ†’๐ต}) = (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต}))
40 2fveq3 6852 . . . . . 6 (๐‘ฅ = (๐‘ฆ โˆช {๐‘ง}) โ†’ (!โ€˜(โ™ฏโ€˜๐‘ฅ)) = (!โ€˜(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))))
41 fveq2 6847 . . . . . . 7 (๐‘ฅ = (๐‘ฆ โˆช {๐‘ง}) โ†’ (โ™ฏโ€˜๐‘ฅ) = (โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง})))
4241oveq2d 7378 . . . . . 6 (๐‘ฅ = (๐‘ฆ โˆช {๐‘ง}) โ†’ ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฅ)) = ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))))
4340, 42oveq12d 7380 . . . . 5 (๐‘ฅ = (๐‘ฆ โˆช {๐‘ง}) โ†’ ((!โ€˜(โ™ฏโ€˜๐‘ฅ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฅ))) = ((!โ€˜(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง})))))
4439, 43eqeq12d 2753 . . . 4 (๐‘ฅ = (๐‘ฆ โˆช {๐‘ง}) โ†’ ((โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฅโ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜๐‘ฅ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฅ))) โ†” (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))))))
4544imbi2d 341 . . 3 (๐‘ฅ = (๐‘ฆ โˆช {๐‘ง}) โ†’ ((๐ต โˆˆ Fin โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฅโ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜๐‘ฅ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฅ)))) โ†” (๐ต โˆˆ Fin โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง})))))))
46 f1eq2 6739 . . . . . . 7 (๐‘ฅ = ๐ด โ†’ (๐‘“:๐‘ฅโ€“1-1โ†’๐ต โ†” ๐‘“:๐ดโ€“1-1โ†’๐ต))
4746abbidv 2806 . . . . . 6 (๐‘ฅ = ๐ด โ†’ {๐‘“ โˆฃ ๐‘“:๐‘ฅโ€“1-1โ†’๐ต} = {๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต})
4847fveq2d 6851 . . . . 5 (๐‘ฅ = ๐ด โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฅโ€“1-1โ†’๐ต}) = (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต}))
49 2fveq3 6852 . . . . . 6 (๐‘ฅ = ๐ด โ†’ (!โ€˜(โ™ฏโ€˜๐‘ฅ)) = (!โ€˜(โ™ฏโ€˜๐ด)))
50 fveq2 6847 . . . . . . 7 (๐‘ฅ = ๐ด โ†’ (โ™ฏโ€˜๐‘ฅ) = (โ™ฏโ€˜๐ด))
5150oveq2d 7378 . . . . . 6 (๐‘ฅ = ๐ด โ†’ ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฅ)) = ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐ด)))
5249, 51oveq12d 7380 . . . . 5 (๐‘ฅ = ๐ด โ†’ ((!โ€˜(โ™ฏโ€˜๐‘ฅ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฅ))) = ((!โ€˜(โ™ฏโ€˜๐ด)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐ด))))
5348, 52eqeq12d 2753 . . . 4 (๐‘ฅ = ๐ด โ†’ ((โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฅโ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜๐‘ฅ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฅ))) โ†” (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜๐ด)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐ด)))))
5453imbi2d 341 . . 3 (๐‘ฅ = ๐ด โ†’ ((๐ต โˆˆ Fin โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฅโ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜๐‘ฅ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฅ)))) โ†” (๐ต โˆˆ Fin โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜๐ด)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐ด))))))
55 hashcl 14263 . . . . . 6 (๐ต โˆˆ Fin โ†’ (โ™ฏโ€˜๐ต) โˆˆ โ„•0)
56 bcn0 14217 . . . . . 6 ((โ™ฏโ€˜๐ต) โˆˆ โ„•0 โ†’ ((โ™ฏโ€˜๐ต)C0) = 1)
5755, 56syl 17 . . . . 5 (๐ต โˆˆ Fin โ†’ ((โ™ฏโ€˜๐ต)C0) = 1)
5857oveq2d 7378 . . . 4 (๐ต โˆˆ Fin โ†’ (1 ยท ((โ™ฏโ€˜๐ต)C0)) = (1 ยท 1))
59 1t1e1 12322 . . . 4 (1 ยท 1) = 1
6058, 59eqtr2di 2794 . . 3 (๐ต โˆˆ Fin โ†’ 1 = (1 ยท ((โ™ฏโ€˜๐ต)C0)))
61 abn0 4345 . . . . . . . . . . . . 13 ({๐‘“ โˆฃ ๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต} โ‰  โˆ… โ†” โˆƒ๐‘“ ๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต)
62 f1domg 8919 . . . . . . . . . . . . . . . 16 (๐ต โˆˆ Fin โ†’ (๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต โ†’ (๐‘ฆ โˆช {๐‘ง}) โ‰ผ ๐ต))
6362adantr 482 . . . . . . . . . . . . . . 15 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ (๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต โ†’ (๐‘ฆ โˆช {๐‘ง}) โ‰ผ ๐ต))
64 hashunsng 14299 . . . . . . . . . . . . . . . . . . 19 (๐‘ง โˆˆ V โ†’ ((๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ) โ†’ (โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง})) = ((โ™ฏโ€˜๐‘ฆ) + 1)))
6564elv 3454 . . . . . . . . . . . . . . . . . 18 ((๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ) โ†’ (โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง})) = ((โ™ฏโ€˜๐‘ฆ) + 1))
6665adantl 483 . . . . . . . . . . . . . . . . 17 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ (โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง})) = ((โ™ฏโ€˜๐‘ฆ) + 1))
6766breq1d 5120 . . . . . . . . . . . . . . . 16 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ ((โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง})) โ‰ค (โ™ฏโ€˜๐ต) โ†” ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)))
68 simprl 770 . . . . . . . . . . . . . . . . . 18 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ ๐‘ฆ โˆˆ Fin)
69 snfi 8995 . . . . . . . . . . . . . . . . . 18 {๐‘ง} โˆˆ Fin
70 unfi 9123 . . . . . . . . . . . . . . . . . 18 ((๐‘ฆ โˆˆ Fin โˆง {๐‘ง} โˆˆ Fin) โ†’ (๐‘ฆ โˆช {๐‘ง}) โˆˆ Fin)
7168, 69, 70sylancl 587 . . . . . . . . . . . . . . . . 17 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ (๐‘ฆ โˆช {๐‘ง}) โˆˆ Fin)
72 simpl 484 . . . . . . . . . . . . . . . . 17 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ ๐ต โˆˆ Fin)
73 hashdom 14286 . . . . . . . . . . . . . . . . 17 (((๐‘ฆ โˆช {๐‘ง}) โˆˆ Fin โˆง ๐ต โˆˆ Fin) โ†’ ((โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง})) โ‰ค (โ™ฏโ€˜๐ต) โ†” (๐‘ฆ โˆช {๐‘ง}) โ‰ผ ๐ต))
7471, 72, 73syl2anc 585 . . . . . . . . . . . . . . . 16 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ ((โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง})) โ‰ค (โ™ฏโ€˜๐ต) โ†” (๐‘ฆ โˆช {๐‘ง}) โ‰ผ ๐ต))
75 hashcl 14263 . . . . . . . . . . . . . . . . . . . 20 (๐‘ฆ โˆˆ Fin โ†’ (โ™ฏโ€˜๐‘ฆ) โˆˆ โ„•0)
7675ad2antrl 727 . . . . . . . . . . . . . . . . . . 19 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ (โ™ฏโ€˜๐‘ฆ) โˆˆ โ„•0)
77 nn0p1nn 12459 . . . . . . . . . . . . . . . . . . 19 ((โ™ฏโ€˜๐‘ฆ) โˆˆ โ„•0 โ†’ ((โ™ฏโ€˜๐‘ฆ) + 1) โˆˆ โ„•)
7876, 77syl 17 . . . . . . . . . . . . . . . . . 18 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ ((โ™ฏโ€˜๐‘ฆ) + 1) โˆˆ โ„•)
7978nnred 12175 . . . . . . . . . . . . . . . . 17 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ ((โ™ฏโ€˜๐‘ฆ) + 1) โˆˆ โ„)
8055adantr 482 . . . . . . . . . . . . . . . . . 18 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ (โ™ฏโ€˜๐ต) โˆˆ โ„•0)
8180nn0red 12481 . . . . . . . . . . . . . . . . 17 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ (โ™ฏโ€˜๐ต) โˆˆ โ„)
8279, 81lenltd 11308 . . . . . . . . . . . . . . . 16 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ (((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต) โ†” ยฌ (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)))
8367, 74, 823bitr3d 309 . . . . . . . . . . . . . . 15 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ ((๐‘ฆ โˆช {๐‘ง}) โ‰ผ ๐ต โ†” ยฌ (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)))
8463, 83sylibd 238 . . . . . . . . . . . . . 14 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ (๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต โ†’ ยฌ (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)))
8584exlimdv 1937 . . . . . . . . . . . . 13 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ (โˆƒ๐‘“ ๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต โ†’ ยฌ (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)))
8661, 85biimtrid 241 . . . . . . . . . . . 12 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ ({๐‘“ โˆฃ ๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต} โ‰  โˆ… โ†’ ยฌ (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)))
8786necon4ad 2963 . . . . . . . . . . 11 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ ((โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1) โ†’ {๐‘“ โˆฃ ๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต} = โˆ…))
8887imp 408 . . . . . . . . . 10 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)) โ†’ {๐‘“ โˆฃ ๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต} = โˆ…)
8988fveq2d 6851 . . . . . . . . 9 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)) โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต}) = (โ™ฏโ€˜โˆ…))
90 hashcl 14263 . . . . . . . . . . . . . 14 ((๐‘ฆ โˆช {๐‘ง}) โˆˆ Fin โ†’ (โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง})) โˆˆ โ„•0)
9171, 90syl 17 . . . . . . . . . . . . 13 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ (โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง})) โˆˆ โ„•0)
9291faccld 14191 . . . . . . . . . . . 12 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ (!โ€˜(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) โˆˆ โ„•)
9392nncnd 12176 . . . . . . . . . . 11 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ (!โ€˜(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) โˆˆ โ„‚)
9493adantr 482 . . . . . . . . . 10 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)) โ†’ (!โ€˜(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) โˆˆ โ„‚)
9594mul01d 11361 . . . . . . . . 9 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)) โ†’ ((!โ€˜(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) ยท 0) = 0)
9619, 89, 953eqtr4a 2803 . . . . . . . 8 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)) โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) ยท 0))
9766adantr 482 . . . . . . . . . . 11 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)) โ†’ (โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง})) = ((โ™ฏโ€˜๐‘ฆ) + 1))
9897oveq2d 7378 . . . . . . . . . 10 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)) โ†’ ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) = ((โ™ฏโ€˜๐ต)C((โ™ฏโ€˜๐‘ฆ) + 1)))
9980adantr 482 . . . . . . . . . . 11 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)) โ†’ (โ™ฏโ€˜๐ต) โˆˆ โ„•0)
10078adantr 482 . . . . . . . . . . . 12 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)) โ†’ ((โ™ฏโ€˜๐‘ฆ) + 1) โˆˆ โ„•)
101100nnzd 12533 . . . . . . . . . . 11 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)) โ†’ ((โ™ฏโ€˜๐‘ฆ) + 1) โˆˆ โ„ค)
102 animorr 978 . . . . . . . . . . 11 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)) โ†’ (((โ™ฏโ€˜๐‘ฆ) + 1) < 0 โˆจ (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)))
103 bcval4 14214 . . . . . . . . . . 11 (((โ™ฏโ€˜๐ต) โˆˆ โ„•0 โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โˆˆ โ„ค โˆง (((โ™ฏโ€˜๐‘ฆ) + 1) < 0 โˆจ (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1))) โ†’ ((โ™ฏโ€˜๐ต)C((โ™ฏโ€˜๐‘ฆ) + 1)) = 0)
10499, 101, 102, 103syl3anc 1372 . . . . . . . . . 10 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)) โ†’ ((โ™ฏโ€˜๐ต)C((โ™ฏโ€˜๐‘ฆ) + 1)) = 0)
10598, 104eqtrd 2777 . . . . . . . . 9 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)) โ†’ ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) = 0)
106105oveq2d 7378 . . . . . . . 8 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)) โ†’ ((!โ€˜(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง})))) = ((!โ€˜(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) ยท 0))
10796, 106eqtr4d 2780 . . . . . . 7 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)) โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง})))))
108107a1d 25 . . . . . 6 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)) โ†’ ((โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฆโ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜๐‘ฆ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฆ))) โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))))))
109 oveq2 7370 . . . . . . 7 ((โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฆโ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜๐‘ฆ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฆ))) โ†’ (((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) ยท (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฆโ€“1-1โ†’๐ต})) = (((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) ยท ((!โ€˜(โ™ฏโ€˜๐‘ฆ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฆ)))))
11068adantr 482 . . . . . . . . 9 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ๐‘ฆ โˆˆ Fin)
11172adantr 482 . . . . . . . . 9 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ๐ต โˆˆ Fin)
112 simplrr 777 . . . . . . . . 9 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ยฌ ๐‘ง โˆˆ ๐‘ฆ)
113 simpr 486 . . . . . . . . 9 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต))
114110, 111, 112, 113hashf1lem2 14362 . . . . . . . 8 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต}) = (((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) ยท (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฆโ€“1-1โ†’๐ต})))
11580adantr 482 . . . . . . . . . . . . . 14 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (โ™ฏโ€˜๐ต) โˆˆ โ„•0)
116115faccld 14191 . . . . . . . . . . . . 13 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (!โ€˜(โ™ฏโ€˜๐ต)) โˆˆ โ„•)
117116nncnd 12176 . . . . . . . . . . . 12 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (!โ€˜(โ™ฏโ€˜๐ต)) โˆˆ โ„‚)
11876adantr 482 . . . . . . . . . . . . . . . 16 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (โ™ฏโ€˜๐‘ฆ) โˆˆ โ„•0)
119 peano2nn0 12460 . . . . . . . . . . . . . . . 16 ((โ™ฏโ€˜๐‘ฆ) โˆˆ โ„•0 โ†’ ((โ™ฏโ€˜๐‘ฆ) + 1) โˆˆ โ„•0)
120118, 119syl 17 . . . . . . . . . . . . . . 15 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((โ™ฏโ€˜๐‘ฆ) + 1) โˆˆ โ„•0)
121 nn0sub2 12571 . . . . . . . . . . . . . . 15 ((((โ™ฏโ€˜๐‘ฆ) + 1) โˆˆ โ„•0 โˆง (โ™ฏโ€˜๐ต) โˆˆ โ„•0 โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1)) โˆˆ โ„•0)
122120, 115, 113, 121syl3anc 1372 . . . . . . . . . . . . . 14 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1)) โˆˆ โ„•0)
123122faccld 14191 . . . . . . . . . . . . 13 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1))) โˆˆ โ„•)
124123nncnd 12176 . . . . . . . . . . . 12 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1))) โˆˆ โ„‚)
125123nnne0d 12210 . . . . . . . . . . . 12 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1))) โ‰  0)
126117, 124, 125divcld 11938 . . . . . . . . . . 11 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1)))) โˆˆ โ„‚)
127120faccld 14191 . . . . . . . . . . . 12 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (!โ€˜((โ™ฏโ€˜๐‘ฆ) + 1)) โˆˆ โ„•)
128127nncnd 12176 . . . . . . . . . . 11 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (!โ€˜((โ™ฏโ€˜๐‘ฆ) + 1)) โˆˆ โ„‚)
129127nnne0d 12210 . . . . . . . . . . 11 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (!โ€˜((โ™ฏโ€˜๐‘ฆ) + 1)) โ‰  0)
130126, 128, 129divcan2d 11940 . . . . . . . . . 10 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((!โ€˜((โ™ฏโ€˜๐‘ฆ) + 1)) ยท (((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1)))) / (!โ€˜((โ™ฏโ€˜๐‘ฆ) + 1)))) = ((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1)))))
131115nn0cnd 12482 . . . . . . . . . . . 12 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (โ™ฏโ€˜๐ต) โˆˆ โ„‚)
132118nn0cnd 12482 . . . . . . . . . . . 12 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (โ™ฏโ€˜๐‘ฆ) โˆˆ โ„‚)
133131, 132subcld 11519 . . . . . . . . . . 11 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) โˆˆ โ„‚)
134 ax-1cn 11116 . . . . . . . . . . . . . 14 1 โˆˆ โ„‚
135 npcan 11417 . . . . . . . . . . . . . 14 ((((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) โˆˆ โ„‚ โˆง 1 โˆˆ โ„‚) โ†’ ((((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) โˆ’ 1) + 1) = ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)))
136133, 134, 135sylancl 587 . . . . . . . . . . . . 13 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) โˆ’ 1) + 1) = ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)))
137 1cnd 11157 . . . . . . . . . . . . . . . 16 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ 1 โˆˆ โ„‚)
138131, 132, 137subsub4d 11550 . . . . . . . . . . . . . . 15 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) โˆ’ 1) = ((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1)))
139138, 122eqeltrd 2838 . . . . . . . . . . . . . 14 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) โˆ’ 1) โˆˆ โ„•0)
140 nn0p1nn 12459 . . . . . . . . . . . . . 14 ((((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) โˆ’ 1) โˆˆ โ„•0 โ†’ ((((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) โˆ’ 1) + 1) โˆˆ โ„•)
141139, 140syl 17 . . . . . . . . . . . . 13 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) โˆ’ 1) + 1) โˆˆ โ„•)
142136, 141eqeltrrd 2839 . . . . . . . . . . . 12 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) โˆˆ โ„•)
143142nnne0d 12210 . . . . . . . . . . 11 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) โ‰  0)
144126, 133, 143divcan2d 11940 . . . . . . . . . 10 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) ยท (((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1)))) / ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)))) = ((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1)))))
145130, 144eqtr4d 2780 . . . . . . . . 9 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((!โ€˜((โ™ฏโ€˜๐‘ฆ) + 1)) ยท (((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1)))) / (!โ€˜((โ™ฏโ€˜๐‘ฆ) + 1)))) = (((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) ยท (((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1)))) / ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)))))
14666adantr 482 . . . . . . . . . . 11 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง})) = ((โ™ฏโ€˜๐‘ฆ) + 1))
147146fveq2d 6851 . . . . . . . . . 10 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (!โ€˜(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) = (!โ€˜((โ™ฏโ€˜๐‘ฆ) + 1)))
148 nn0uz 12812 . . . . . . . . . . . . . . 15 โ„•0 = (โ„คโ‰ฅโ€˜0)
149120, 148eleqtrdi 2848 . . . . . . . . . . . . . 14 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((โ™ฏโ€˜๐‘ฆ) + 1) โˆˆ (โ„คโ‰ฅโ€˜0))
150115nn0zd 12532 . . . . . . . . . . . . . 14 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (โ™ฏโ€˜๐ต) โˆˆ โ„ค)
151 elfz5 13440 . . . . . . . . . . . . . 14 ((((โ™ฏโ€˜๐‘ฆ) + 1) โˆˆ (โ„คโ‰ฅโ€˜0) โˆง (โ™ฏโ€˜๐ต) โˆˆ โ„ค) โ†’ (((โ™ฏโ€˜๐‘ฆ) + 1) โˆˆ (0...(โ™ฏโ€˜๐ต)) โ†” ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)))
152149, 150, 151syl2anc 585 . . . . . . . . . . . . 13 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (((โ™ฏโ€˜๐‘ฆ) + 1) โˆˆ (0...(โ™ฏโ€˜๐ต)) โ†” ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)))
153113, 152mpbird 257 . . . . . . . . . . . 12 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((โ™ฏโ€˜๐‘ฆ) + 1) โˆˆ (0...(โ™ฏโ€˜๐ต)))
154 bcval2 14212 . . . . . . . . . . . 12 (((โ™ฏโ€˜๐‘ฆ) + 1) โˆˆ (0...(โ™ฏโ€˜๐ต)) โ†’ ((โ™ฏโ€˜๐ต)C((โ™ฏโ€˜๐‘ฆ) + 1)) = ((!โ€˜(โ™ฏโ€˜๐ต)) / ((!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1))) ยท (!โ€˜((โ™ฏโ€˜๐‘ฆ) + 1)))))
155153, 154syl 17 . . . . . . . . . . 11 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((โ™ฏโ€˜๐ต)C((โ™ฏโ€˜๐‘ฆ) + 1)) = ((!โ€˜(โ™ฏโ€˜๐ต)) / ((!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1))) ยท (!โ€˜((โ™ฏโ€˜๐‘ฆ) + 1)))))
156146oveq2d 7378 . . . . . . . . . . 11 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) = ((โ™ฏโ€˜๐ต)C((โ™ฏโ€˜๐‘ฆ) + 1)))
157117, 124, 128, 125, 129divdiv1d 11969 . . . . . . . . . . 11 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1)))) / (!โ€˜((โ™ฏโ€˜๐‘ฆ) + 1))) = ((!โ€˜(โ™ฏโ€˜๐ต)) / ((!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1))) ยท (!โ€˜((โ™ฏโ€˜๐‘ฆ) + 1)))))
158155, 156, 1573eqtr4d 2787 . . . . . . . . . 10 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) = (((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1)))) / (!โ€˜((โ™ฏโ€˜๐‘ฆ) + 1))))
159147, 158oveq12d 7380 . . . . . . . . 9 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((!โ€˜(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง})))) = ((!โ€˜((โ™ฏโ€˜๐‘ฆ) + 1)) ยท (((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1)))) / (!โ€˜((โ™ฏโ€˜๐‘ฆ) + 1)))))
160118, 148eleqtrdi 2848 . . . . . . . . . . . . . . 15 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (โ™ฏโ€˜๐‘ฆ) โˆˆ (โ„คโ‰ฅโ€˜0))
161 peano2fzr 13461 . . . . . . . . . . . . . . 15 (((โ™ฏโ€˜๐‘ฆ) โˆˆ (โ„คโ‰ฅโ€˜0) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โˆˆ (0...(โ™ฏโ€˜๐ต))) โ†’ (โ™ฏโ€˜๐‘ฆ) โˆˆ (0...(โ™ฏโ€˜๐ต)))
162160, 153, 161syl2anc 585 . . . . . . . . . . . . . 14 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (โ™ฏโ€˜๐‘ฆ) โˆˆ (0...(โ™ฏโ€˜๐ต)))
163 bcval2 14212 . . . . . . . . . . . . . 14 ((โ™ฏโ€˜๐‘ฆ) โˆˆ (0...(โ™ฏโ€˜๐ต)) โ†’ ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฆ)) = ((!โ€˜(โ™ฏโ€˜๐ต)) / ((!โ€˜((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ))) ยท (!โ€˜(โ™ฏโ€˜๐‘ฆ)))))
164162, 163syl 17 . . . . . . . . . . . . 13 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฆ)) = ((!โ€˜(โ™ฏโ€˜๐ต)) / ((!โ€˜((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ))) ยท (!โ€˜(โ™ฏโ€˜๐‘ฆ)))))
165 elfzle2 13452 . . . . . . . . . . . . . . . . . 18 ((โ™ฏโ€˜๐‘ฆ) โˆˆ (0...(โ™ฏโ€˜๐ต)) โ†’ (โ™ฏโ€˜๐‘ฆ) โ‰ค (โ™ฏโ€˜๐ต))
166162, 165syl 17 . . . . . . . . . . . . . . . . 17 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (โ™ฏโ€˜๐‘ฆ) โ‰ค (โ™ฏโ€˜๐ต))
167 nn0sub2 12571 . . . . . . . . . . . . . . . . 17 (((โ™ฏโ€˜๐‘ฆ) โˆˆ โ„•0 โˆง (โ™ฏโ€˜๐ต) โˆˆ โ„•0 โˆง (โ™ฏโ€˜๐‘ฆ) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) โˆˆ โ„•0)
168118, 115, 166, 167syl3anc 1372 . . . . . . . . . . . . . . . 16 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) โˆˆ โ„•0)
169168faccld 14191 . . . . . . . . . . . . . . 15 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ))) โˆˆ โ„•)
170169nncnd 12176 . . . . . . . . . . . . . 14 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ))) โˆˆ โ„‚)
171118faccld 14191 . . . . . . . . . . . . . . 15 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (!โ€˜(โ™ฏโ€˜๐‘ฆ)) โˆˆ โ„•)
172171nncnd 12176 . . . . . . . . . . . . . 14 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (!โ€˜(โ™ฏโ€˜๐‘ฆ)) โˆˆ โ„‚)
173169nnne0d 12210 . . . . . . . . . . . . . 14 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ))) โ‰  0)
174171nnne0d 12210 . . . . . . . . . . . . . 14 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (!โ€˜(โ™ฏโ€˜๐‘ฆ)) โ‰  0)
175117, 170, 172, 173, 174divdiv1d 11969 . . . . . . . . . . . . 13 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)))) / (!โ€˜(โ™ฏโ€˜๐‘ฆ))) = ((!โ€˜(โ™ฏโ€˜๐ต)) / ((!โ€˜((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ))) ยท (!โ€˜(โ™ฏโ€˜๐‘ฆ)))))
176164, 175eqtr4d 2780 . . . . . . . . . . . 12 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฆ)) = (((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)))) / (!โ€˜(โ™ฏโ€˜๐‘ฆ))))
177176oveq2d 7378 . . . . . . . . . . 11 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((!โ€˜(โ™ฏโ€˜๐‘ฆ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฆ))) = ((!โ€˜(โ™ฏโ€˜๐‘ฆ)) ยท (((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)))) / (!โ€˜(โ™ฏโ€˜๐‘ฆ)))))
178 facnn2 14189 . . . . . . . . . . . . . . 15 (((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) โˆˆ โ„• โ†’ (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ))) = ((!โ€˜(((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) โˆ’ 1)) ยท ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ))))
179142, 178syl 17 . . . . . . . . . . . . . 14 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ))) = ((!โ€˜(((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) โˆ’ 1)) ยท ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ))))
180138fveq2d 6851 . . . . . . . . . . . . . . 15 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (!โ€˜(((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) โˆ’ 1)) = (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1))))
181180oveq1d 7377 . . . . . . . . . . . . . 14 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((!โ€˜(((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) โˆ’ 1)) ยท ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ))) = ((!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1))) ยท ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ))))
182179, 181eqtrd 2777 . . . . . . . . . . . . 13 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ))) = ((!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1))) ยท ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ))))
183182oveq2d 7378 . . . . . . . . . . . 12 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)))) = ((!โ€˜(โ™ฏโ€˜๐ต)) / ((!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1))) ยท ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)))))
184117, 170, 173divcld 11938 . . . . . . . . . . . . 13 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)))) โˆˆ โ„‚)
185184, 172, 174divcan2d 11940 . . . . . . . . . . . 12 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((!โ€˜(โ™ฏโ€˜๐‘ฆ)) ยท (((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)))) / (!โ€˜(โ™ฏโ€˜๐‘ฆ)))) = ((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)))))
186117, 124, 133, 125, 143divdiv1d 11969 . . . . . . . . . . . 12 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1)))) / ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ))) = ((!โ€˜(โ™ฏโ€˜๐ต)) / ((!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1))) ยท ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)))))
187183, 185, 1863eqtr4d 2787 . . . . . . . . . . 11 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((!โ€˜(โ™ฏโ€˜๐‘ฆ)) ยท (((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)))) / (!โ€˜(โ™ฏโ€˜๐‘ฆ)))) = (((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1)))) / ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ))))
188177, 187eqtrd 2777 . . . . . . . . . 10 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((!โ€˜(โ™ฏโ€˜๐‘ฆ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฆ))) = (((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1)))) / ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ))))
189188oveq2d 7378 . . . . . . . . 9 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) ยท ((!โ€˜(โ™ฏโ€˜๐‘ฆ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฆ)))) = (((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) ยท (((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1)))) / ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)))))
190145, 159, 1893eqtr4d 2787 . . . . . . . 8 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((!โ€˜(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง})))) = (((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) ยท ((!โ€˜(โ™ฏโ€˜๐‘ฆ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฆ)))))
191114, 190eqeq12d 2753 . . . . . . 7 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง})))) โ†” (((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) ยท (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฆโ€“1-1โ†’๐ต})) = (((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) ยท ((!โ€˜(โ™ฏโ€˜๐‘ฆ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฆ))))))
192109, 191syl5ibr 246 . . . . . 6 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฆโ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜๐‘ฆ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฆ))) โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))))))
193108, 192, 81, 79ltlecasei 11270 . . . . 5 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ ((โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฆโ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜๐‘ฆ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฆ))) โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))))))
194193expcom 415 . . . 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 9116 . 2 (๐ด โˆˆ Fin โ†’ (๐ต โˆˆ Fin โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜๐ด)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐ด)))))
197196imp 408 1 ((๐ด โˆˆ Fin โˆง ๐ต โˆˆ Fin) โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜๐ด)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐ด))))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 397   โˆจ wo 846   = wceq 1542  โˆƒwex 1782   โˆˆ wcel 2107  {cab 2714   โ‰  wne 2944  Vcvv 3448   โˆช cun 3913  โˆ…c0 4287  {csn 4591   class class class wbr 5110   Fn wfn 6496  โ€“1-1โ†’wf1 6498  โ€˜cfv 6501  (class class class)co 7362   โ‰ผ cdom 8888  Fincfn 8890  โ„‚cc 11056  0cc0 11058  1c1 11059   + caddc 11061   ยท cmul 11063   < clt 11196   โ‰ค cle 11197   โˆ’ cmin 11392   / cdiv 11819  โ„•cn 12160  โ„•0cn0 12420  โ„คcz 12506  โ„คโ‰ฅcuz 12770  ...cfz 13431  !cfa 14180  Ccbc 14209  โ™ฏchash 14237
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-cnex 11114  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-mulcom 11122  ax-addass 11123  ax-mulass 11124  ax-distr 11125  ax-i2m1 11126  ax-1ne0 11127  ax-1rid 11128  ax-rnegex 11129  ax-rrecex 11130  ax-cnre 11131  ax-pre-lttri 11132  ax-pre-lttrn 11133  ax-pre-ltadd 11134  ax-pre-mulgt0 11135
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rmo 3356  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-om 7808  df-1st 7926  df-2nd 7927  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-oadd 8421  df-er 8655  df-map 8774  df-pm 8775  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-dju 9844  df-card 9882  df-pnf 11198  df-mnf 11199  df-xr 11200  df-ltxr 11201  df-le 11202  df-sub 11394  df-neg 11395  df-div 11820  df-nn 12161  df-n0 12421  df-xnn0 12493  df-z 12507  df-uz 12771  df-fz 13432  df-seq 13914  df-fac 14181  df-bc 14210  df-hash 14238
This theorem is referenced by:  hashfac  14364  birthdaylem2  26318
  Copyright terms: Public domain W3C validator