Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bcprod Structured version   Visualization version   GIF version

Theorem bcprod 35337
Description: A product identity for binomial coefficents. (Contributed by Scott Fenton, 23-Jun-2020.)
Assertion
Ref Expression
bcprod (๐‘ โˆˆ โ„• โ†’ โˆ๐‘˜ โˆˆ (1...(๐‘ โˆ’ 1))((๐‘ โˆ’ 1)C๐‘˜) = โˆ๐‘˜ โˆˆ (1...(๐‘ โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘)))
Distinct variable group:   ๐‘˜,๐‘

Proof of Theorem bcprod
Dummy variables ๐‘› ๐‘š ๐‘— are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq1 7431 . . . . . . 7 (๐‘š = 1 โ†’ (๐‘š โˆ’ 1) = (1 โˆ’ 1))
2 1m1e0 12320 . . . . . . 7 (1 โˆ’ 1) = 0
31, 2eqtrdi 2783 . . . . . 6 (๐‘š = 1 โ†’ (๐‘š โˆ’ 1) = 0)
43oveq2d 7440 . . . . 5 (๐‘š = 1 โ†’ (1...(๐‘š โˆ’ 1)) = (1...0))
5 fz10 13560 . . . . 5 (1...0) = โˆ…
64, 5eqtrdi 2783 . . . 4 (๐‘š = 1 โ†’ (1...(๐‘š โˆ’ 1)) = โˆ…)
73oveq1d 7439 . . . . 5 (๐‘š = 1 โ†’ ((๐‘š โˆ’ 1)C๐‘˜) = (0C๐‘˜))
87adantr 479 . . . 4 ((๐‘š = 1 โˆง ๐‘˜ โˆˆ (1...(๐‘š โˆ’ 1))) โ†’ ((๐‘š โˆ’ 1)C๐‘˜) = (0C๐‘˜))
96, 8prodeq12dv 15908 . . 3 (๐‘š = 1 โ†’ โˆ๐‘˜ โˆˆ (1...(๐‘š โˆ’ 1))((๐‘š โˆ’ 1)C๐‘˜) = โˆ๐‘˜ โˆˆ โˆ… (0C๐‘˜))
10 oveq2 7432 . . . . . 6 (๐‘š = 1 โ†’ ((2 ยท ๐‘˜) โˆ’ ๐‘š) = ((2 ยท ๐‘˜) โˆ’ 1))
1110oveq2d 7440 . . . . 5 (๐‘š = 1 โ†’ (๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘š)) = (๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ 1)))
1211adantr 479 . . . 4 ((๐‘š = 1 โˆง ๐‘˜ โˆˆ (1...(๐‘š โˆ’ 1))) โ†’ (๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘š)) = (๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ 1)))
136, 12prodeq12dv 15908 . . 3 (๐‘š = 1 โ†’ โˆ๐‘˜ โˆˆ (1...(๐‘š โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘š)) = โˆ๐‘˜ โˆˆ โˆ… (๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ 1)))
149, 13eqeq12d 2743 . 2 (๐‘š = 1 โ†’ (โˆ๐‘˜ โˆˆ (1...(๐‘š โˆ’ 1))((๐‘š โˆ’ 1)C๐‘˜) = โˆ๐‘˜ โˆˆ (1...(๐‘š โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘š)) โ†” โˆ๐‘˜ โˆˆ โˆ… (0C๐‘˜) = โˆ๐‘˜ โˆˆ โˆ… (๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ 1))))
15 oveq1 7431 . . . . 5 (๐‘š = ๐‘› โ†’ (๐‘š โˆ’ 1) = (๐‘› โˆ’ 1))
1615oveq2d 7440 . . . 4 (๐‘š = ๐‘› โ†’ (1...(๐‘š โˆ’ 1)) = (1...(๐‘› โˆ’ 1)))
1715oveq1d 7439 . . . . 5 (๐‘š = ๐‘› โ†’ ((๐‘š โˆ’ 1)C๐‘˜) = ((๐‘› โˆ’ 1)C๐‘˜))
1817adantr 479 . . . 4 ((๐‘š = ๐‘› โˆง ๐‘˜ โˆˆ (1...(๐‘š โˆ’ 1))) โ†’ ((๐‘š โˆ’ 1)C๐‘˜) = ((๐‘› โˆ’ 1)C๐‘˜))
1916, 18prodeq12dv 15908 . . 3 (๐‘š = ๐‘› โ†’ โˆ๐‘˜ โˆˆ (1...(๐‘š โˆ’ 1))((๐‘š โˆ’ 1)C๐‘˜) = โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))((๐‘› โˆ’ 1)C๐‘˜))
20 oveq2 7432 . . . . . 6 (๐‘š = ๐‘› โ†’ ((2 ยท ๐‘˜) โˆ’ ๐‘š) = ((2 ยท ๐‘˜) โˆ’ ๐‘›))
2120oveq2d 7440 . . . . 5 (๐‘š = ๐‘› โ†’ (๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘š)) = (๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘›)))
2221adantr 479 . . . 4 ((๐‘š = ๐‘› โˆง ๐‘˜ โˆˆ (1...(๐‘š โˆ’ 1))) โ†’ (๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘š)) = (๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘›)))
2316, 22prodeq12dv 15908 . . 3 (๐‘š = ๐‘› โ†’ โˆ๐‘˜ โˆˆ (1...(๐‘š โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘š)) = โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘›)))
2419, 23eqeq12d 2743 . 2 (๐‘š = ๐‘› โ†’ (โˆ๐‘˜ โˆˆ (1...(๐‘š โˆ’ 1))((๐‘š โˆ’ 1)C๐‘˜) = โˆ๐‘˜ โˆˆ (1...(๐‘š โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘š)) โ†” โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))((๐‘› โˆ’ 1)C๐‘˜) = โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘›))))
25 oveq1 7431 . . . . 5 (๐‘š = (๐‘› + 1) โ†’ (๐‘š โˆ’ 1) = ((๐‘› + 1) โˆ’ 1))
2625oveq2d 7440 . . . 4 (๐‘š = (๐‘› + 1) โ†’ (1...(๐‘š โˆ’ 1)) = (1...((๐‘› + 1) โˆ’ 1)))
2725oveq1d 7439 . . . . 5 (๐‘š = (๐‘› + 1) โ†’ ((๐‘š โˆ’ 1)C๐‘˜) = (((๐‘› + 1) โˆ’ 1)C๐‘˜))
2827adantr 479 . . . 4 ((๐‘š = (๐‘› + 1) โˆง ๐‘˜ โˆˆ (1...(๐‘š โˆ’ 1))) โ†’ ((๐‘š โˆ’ 1)C๐‘˜) = (((๐‘› + 1) โˆ’ 1)C๐‘˜))
2926, 28prodeq12dv 15908 . . 3 (๐‘š = (๐‘› + 1) โ†’ โˆ๐‘˜ โˆˆ (1...(๐‘š โˆ’ 1))((๐‘š โˆ’ 1)C๐‘˜) = โˆ๐‘˜ โˆˆ (1...((๐‘› + 1) โˆ’ 1))(((๐‘› + 1) โˆ’ 1)C๐‘˜))
30 oveq2 7432 . . . . . 6 (๐‘š = (๐‘› + 1) โ†’ ((2 ยท ๐‘˜) โˆ’ ๐‘š) = ((2 ยท ๐‘˜) โˆ’ (๐‘› + 1)))
3130oveq2d 7440 . . . . 5 (๐‘š = (๐‘› + 1) โ†’ (๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘š)) = (๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ (๐‘› + 1))))
3231adantr 479 . . . 4 ((๐‘š = (๐‘› + 1) โˆง ๐‘˜ โˆˆ (1...(๐‘š โˆ’ 1))) โ†’ (๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘š)) = (๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ (๐‘› + 1))))
3326, 32prodeq12dv 15908 . . 3 (๐‘š = (๐‘› + 1) โ†’ โˆ๐‘˜ โˆˆ (1...(๐‘š โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘š)) = โˆ๐‘˜ โˆˆ (1...((๐‘› + 1) โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ (๐‘› + 1))))
3429, 33eqeq12d 2743 . 2 (๐‘š = (๐‘› + 1) โ†’ (โˆ๐‘˜ โˆˆ (1...(๐‘š โˆ’ 1))((๐‘š โˆ’ 1)C๐‘˜) = โˆ๐‘˜ โˆˆ (1...(๐‘š โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘š)) โ†” โˆ๐‘˜ โˆˆ (1...((๐‘› + 1) โˆ’ 1))(((๐‘› + 1) โˆ’ 1)C๐‘˜) = โˆ๐‘˜ โˆˆ (1...((๐‘› + 1) โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ (๐‘› + 1)))))
35 oveq1 7431 . . . . 5 (๐‘š = ๐‘ โ†’ (๐‘š โˆ’ 1) = (๐‘ โˆ’ 1))
3635oveq2d 7440 . . . 4 (๐‘š = ๐‘ โ†’ (1...(๐‘š โˆ’ 1)) = (1...(๐‘ โˆ’ 1)))
3735oveq1d 7439 . . . . 5 (๐‘š = ๐‘ โ†’ ((๐‘š โˆ’ 1)C๐‘˜) = ((๐‘ โˆ’ 1)C๐‘˜))
3837adantr 479 . . . 4 ((๐‘š = ๐‘ โˆง ๐‘˜ โˆˆ (1...(๐‘š โˆ’ 1))) โ†’ ((๐‘š โˆ’ 1)C๐‘˜) = ((๐‘ โˆ’ 1)C๐‘˜))
3936, 38prodeq12dv 15908 . . 3 (๐‘š = ๐‘ โ†’ โˆ๐‘˜ โˆˆ (1...(๐‘š โˆ’ 1))((๐‘š โˆ’ 1)C๐‘˜) = โˆ๐‘˜ โˆˆ (1...(๐‘ โˆ’ 1))((๐‘ โˆ’ 1)C๐‘˜))
40 oveq2 7432 . . . . . 6 (๐‘š = ๐‘ โ†’ ((2 ยท ๐‘˜) โˆ’ ๐‘š) = ((2 ยท ๐‘˜) โˆ’ ๐‘))
4140oveq2d 7440 . . . . 5 (๐‘š = ๐‘ โ†’ (๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘š)) = (๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘)))
4241adantr 479 . . . 4 ((๐‘š = ๐‘ โˆง ๐‘˜ โˆˆ (1...(๐‘š โˆ’ 1))) โ†’ (๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘š)) = (๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘)))
4336, 42prodeq12dv 15908 . . 3 (๐‘š = ๐‘ โ†’ โˆ๐‘˜ โˆˆ (1...(๐‘š โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘š)) = โˆ๐‘˜ โˆˆ (1...(๐‘ โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘)))
4439, 43eqeq12d 2743 . 2 (๐‘š = ๐‘ โ†’ (โˆ๐‘˜ โˆˆ (1...(๐‘š โˆ’ 1))((๐‘š โˆ’ 1)C๐‘˜) = โˆ๐‘˜ โˆˆ (1...(๐‘š โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘š)) โ†” โˆ๐‘˜ โˆˆ (1...(๐‘ โˆ’ 1))((๐‘ โˆ’ 1)C๐‘˜) = โˆ๐‘˜ โˆˆ (1...(๐‘ โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘))))
45 prod0 15925 . . 3 โˆ๐‘˜ โˆˆ โˆ… (0C๐‘˜) = 1
46 prod0 15925 . . 3 โˆ๐‘˜ โˆˆ โˆ… (๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ 1)) = 1
4745, 46eqtr4i 2758 . 2 โˆ๐‘˜ โˆˆ โˆ… (0C๐‘˜) = โˆ๐‘˜ โˆˆ โˆ… (๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ 1))
48 simpr 483 . . . . 5 ((๐‘› โˆˆ โ„• โˆง โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))((๐‘› โˆ’ 1)C๐‘˜) = โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘›))) โ†’ โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))((๐‘› โˆ’ 1)C๐‘˜) = โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘›)))
4948oveq1d 7439 . . . 4 ((๐‘› โˆˆ โ„• โˆง โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))((๐‘› โˆ’ 1)C๐‘˜) = โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘›))) โ†’ (โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))((๐‘› โˆ’ 1)C๐‘˜) ยท ((๐‘›โ†‘(๐‘› โˆ’ 1)) / (!โ€˜(๐‘› โˆ’ 1)))) = (โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘›)) ยท ((๐‘›โ†‘(๐‘› โˆ’ 1)) / (!โ€˜(๐‘› โˆ’ 1)))))
50 nncn 12256 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ ๐‘› โˆˆ โ„‚)
51 1cnd 11245 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ 1 โˆˆ โ„‚)
5250, 51pncand 11608 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ ((๐‘› + 1) โˆ’ 1) = ๐‘›)
5352oveq2d 7440 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ (1...((๐‘› + 1) โˆ’ 1)) = (1...๐‘›))
5452oveq1d 7439 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ (((๐‘› + 1) โˆ’ 1)C๐‘˜) = (๐‘›C๐‘˜))
5554adantr 479 . . . . . . 7 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...((๐‘› + 1) โˆ’ 1))) โ†’ (((๐‘› + 1) โˆ’ 1)C๐‘˜) = (๐‘›C๐‘˜))
5653, 55prodeq12dv 15908 . . . . . 6 (๐‘› โˆˆ โ„• โ†’ โˆ๐‘˜ โˆˆ (1...((๐‘› + 1) โˆ’ 1))(((๐‘› + 1) โˆ’ 1)C๐‘˜) = โˆ๐‘˜ โˆˆ (1...๐‘›)(๐‘›C๐‘˜))
57 elnnuz 12902 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†” ๐‘› โˆˆ (โ„คโ‰ฅโ€˜1))
5857biimpi 215 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ ๐‘› โˆˆ (โ„คโ‰ฅโ€˜1))
59 nnnn0 12515 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ ๐‘› โˆˆ โ„•0)
60 elfzelz 13539 . . . . . . . . 9 (๐‘˜ โˆˆ (1...๐‘›) โ†’ ๐‘˜ โˆˆ โ„ค)
61 bccl 14319 . . . . . . . . 9 ((๐‘› โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ โ„ค) โ†’ (๐‘›C๐‘˜) โˆˆ โ„•0)
6259, 60, 61syl2an 594 . . . . . . . 8 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...๐‘›)) โ†’ (๐‘›C๐‘˜) โˆˆ โ„•0)
6362nn0cnd 12570 . . . . . . 7 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...๐‘›)) โ†’ (๐‘›C๐‘˜) โˆˆ โ„‚)
64 oveq2 7432 . . . . . . 7 (๐‘˜ = ๐‘› โ†’ (๐‘›C๐‘˜) = (๐‘›C๐‘›))
6558, 63, 64fprodm1 15949 . . . . . 6 (๐‘› โˆˆ โ„• โ†’ โˆ๐‘˜ โˆˆ (1...๐‘›)(๐‘›C๐‘˜) = (โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘›C๐‘˜) ยท (๐‘›C๐‘›)))
66 bcnn 14309 . . . . . . . . 9 (๐‘› โˆˆ โ„•0 โ†’ (๐‘›C๐‘›) = 1)
6759, 66syl 17 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ (๐‘›C๐‘›) = 1)
6867oveq2d 7440 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ (โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘›C๐‘˜) ยท (๐‘›C๐‘›)) = (โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘›C๐‘˜) ยท 1))
69 fzfid 13976 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ (1...(๐‘› โˆ’ 1)) โˆˆ Fin)
70 elfzelz 13539 . . . . . . . . . . 11 (๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1)) โ†’ ๐‘˜ โˆˆ โ„ค)
7159, 70, 61syl2an 594 . . . . . . . . . 10 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ (๐‘›C๐‘˜) โˆˆ โ„•0)
7271nn0cnd 12570 . . . . . . . . 9 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ (๐‘›C๐‘˜) โˆˆ โ„‚)
7369, 72fprodcl 15934 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘›C๐‘˜) โˆˆ โ„‚)
7473mulridd 11267 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ (โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘›C๐‘˜) ยท 1) = โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘›C๐‘˜))
75 fz1ssfz0 13635 . . . . . . . . . . 11 (1...(๐‘› โˆ’ 1)) โІ (0...(๐‘› โˆ’ 1))
7675sseli 3976 . . . . . . . . . 10 (๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1)) โ†’ ๐‘˜ โˆˆ (0...(๐‘› โˆ’ 1)))
77 bcm1nt 35336 . . . . . . . . . 10 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (0...(๐‘› โˆ’ 1))) โ†’ (๐‘›C๐‘˜) = (((๐‘› โˆ’ 1)C๐‘˜) ยท (๐‘› / (๐‘› โˆ’ ๐‘˜))))
7876, 77sylan2 591 . . . . . . . . 9 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ (๐‘›C๐‘˜) = (((๐‘› โˆ’ 1)C๐‘˜) ยท (๐‘› / (๐‘› โˆ’ ๐‘˜))))
7978prodeq2dv 15905 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘›C๐‘˜) = โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(((๐‘› โˆ’ 1)C๐‘˜) ยท (๐‘› / (๐‘› โˆ’ ๐‘˜))))
80 nnm1nn0 12549 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ (๐‘› โˆ’ 1) โˆˆ โ„•0)
81 bccl 14319 . . . . . . . . . . 11 (((๐‘› โˆ’ 1) โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ โ„ค) โ†’ ((๐‘› โˆ’ 1)C๐‘˜) โˆˆ โ„•0)
8280, 70, 81syl2an 594 . . . . . . . . . 10 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ ((๐‘› โˆ’ 1)C๐‘˜) โˆˆ โ„•0)
8382nn0cnd 12570 . . . . . . . . 9 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ ((๐‘› โˆ’ 1)C๐‘˜) โˆˆ โ„‚)
8450adantr 479 . . . . . . . . . 10 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ ๐‘› โˆˆ โ„‚)
85 elfznn 13568 . . . . . . . . . . . . . . 15 (๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1)) โ†’ ๐‘˜ โˆˆ โ„•)
8685adantl 480 . . . . . . . . . . . . . 14 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ ๐‘˜ โˆˆ โ„•)
8786nnred 12263 . . . . . . . . . . . . 13 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ ๐‘˜ โˆˆ โ„)
8880adantr 479 . . . . . . . . . . . . . 14 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ (๐‘› โˆ’ 1) โˆˆ โ„•0)
8988nn0red 12569 . . . . . . . . . . . . 13 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ (๐‘› โˆ’ 1) โˆˆ โ„)
90 nnre 12255 . . . . . . . . . . . . . 14 (๐‘› โˆˆ โ„• โ†’ ๐‘› โˆˆ โ„)
9190adantr 479 . . . . . . . . . . . . 13 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ ๐‘› โˆˆ โ„)
92 elfzle2 13543 . . . . . . . . . . . . . 14 (๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1)) โ†’ ๐‘˜ โ‰ค (๐‘› โˆ’ 1))
9392adantl 480 . . . . . . . . . . . . 13 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ ๐‘˜ โ‰ค (๐‘› โˆ’ 1))
9491ltm1d 12182 . . . . . . . . . . . . 13 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ (๐‘› โˆ’ 1) < ๐‘›)
9587, 89, 91, 93, 94lelttrd 11408 . . . . . . . . . . . 12 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ ๐‘˜ < ๐‘›)
96 simpl 481 . . . . . . . . . . . . 13 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ ๐‘› โˆˆ โ„•)
97 nnsub 12292 . . . . . . . . . . . . 13 ((๐‘˜ โˆˆ โ„• โˆง ๐‘› โˆˆ โ„•) โ†’ (๐‘˜ < ๐‘› โ†” (๐‘› โˆ’ ๐‘˜) โˆˆ โ„•))
9886, 96, 97syl2anc 582 . . . . . . . . . . . 12 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ (๐‘˜ < ๐‘› โ†” (๐‘› โˆ’ ๐‘˜) โˆˆ โ„•))
9995, 98mpbid 231 . . . . . . . . . . 11 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ (๐‘› โˆ’ ๐‘˜) โˆˆ โ„•)
10099nncnd 12264 . . . . . . . . . 10 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ (๐‘› โˆ’ ๐‘˜) โˆˆ โ„‚)
10199nnne0d 12298 . . . . . . . . . 10 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ (๐‘› โˆ’ ๐‘˜) โ‰  0)
10284, 100, 101divcld 12026 . . . . . . . . 9 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ (๐‘› / (๐‘› โˆ’ ๐‘˜)) โˆˆ โ„‚)
10369, 83, 102fprodmul 15942 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(((๐‘› โˆ’ 1)C๐‘˜) ยท (๐‘› / (๐‘› โˆ’ ๐‘˜))) = (โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))((๐‘› โˆ’ 1)C๐‘˜) ยท โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘› / (๐‘› โˆ’ ๐‘˜))))
10469, 84, 100, 101fproddiv 15943 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘› / (๐‘› โˆ’ ๐‘˜)) = (โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))๐‘› / โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘› โˆ’ ๐‘˜)))
105 fzfi 13975 . . . . . . . . . . . . 13 (1...(๐‘› โˆ’ 1)) โˆˆ Fin
106 fprodconst 15960 . . . . . . . . . . . . 13 (((1...(๐‘› โˆ’ 1)) โˆˆ Fin โˆง ๐‘› โˆˆ โ„‚) โ†’ โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))๐‘› = (๐‘›โ†‘(โ™ฏโ€˜(1...(๐‘› โˆ’ 1)))))
107105, 50, 106sylancr 585 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))๐‘› = (๐‘›โ†‘(โ™ฏโ€˜(1...(๐‘› โˆ’ 1)))))
108 hashfz1 14343 . . . . . . . . . . . . . 14 ((๐‘› โˆ’ 1) โˆˆ โ„•0 โ†’ (โ™ฏโ€˜(1...(๐‘› โˆ’ 1))) = (๐‘› โˆ’ 1))
10980, 108syl 17 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ (โ™ฏโ€˜(1...(๐‘› โˆ’ 1))) = (๐‘› โˆ’ 1))
110109oveq2d 7440 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ (๐‘›โ†‘(โ™ฏโ€˜(1...(๐‘› โˆ’ 1)))) = (๐‘›โ†‘(๐‘› โˆ’ 1)))
111107, 110eqtr2d 2768 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ (๐‘›โ†‘(๐‘› โˆ’ 1)) = โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))๐‘›)
112 fprodfac 15955 . . . . . . . . . . . . 13 ((๐‘› โˆ’ 1) โˆˆ โ„•0 โ†’ (!โ€˜(๐‘› โˆ’ 1)) = โˆ๐‘— โˆˆ (1...(๐‘› โˆ’ 1))๐‘—)
11380, 112syl 17 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ (!โ€˜(๐‘› โˆ’ 1)) = โˆ๐‘— โˆˆ (1...(๐‘› โˆ’ 1))๐‘—)
114 nnz 12615 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ ๐‘› โˆˆ โ„ค)
115 1zzd 12629 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ 1 โˆˆ โ„ค)
11680nn0zd 12620 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ (๐‘› โˆ’ 1) โˆˆ โ„ค)
117 elfznn 13568 . . . . . . . . . . . . . . 15 (๐‘— โˆˆ (1...(๐‘› โˆ’ 1)) โ†’ ๐‘— โˆˆ โ„•)
118117adantl 480 . . . . . . . . . . . . . 14 ((๐‘› โˆˆ โ„• โˆง ๐‘— โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ ๐‘— โˆˆ โ„•)
119118nncnd 12264 . . . . . . . . . . . . 13 ((๐‘› โˆˆ โ„• โˆง ๐‘— โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ ๐‘— โˆˆ โ„‚)
120 id 22 . . . . . . . . . . . . 13 (๐‘— = (๐‘› โˆ’ ๐‘˜) โ†’ ๐‘— = (๐‘› โˆ’ ๐‘˜))
121114, 115, 116, 119, 120fprodrev 15959 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ โˆ๐‘— โˆˆ (1...(๐‘› โˆ’ 1))๐‘— = โˆ๐‘˜ โˆˆ ((๐‘› โˆ’ (๐‘› โˆ’ 1))...(๐‘› โˆ’ 1))(๐‘› โˆ’ ๐‘˜))
12250, 51nncand 11612 . . . . . . . . . . . . . 14 (๐‘› โˆˆ โ„• โ†’ (๐‘› โˆ’ (๐‘› โˆ’ 1)) = 1)
123122oveq1d 7439 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ ((๐‘› โˆ’ (๐‘› โˆ’ 1))...(๐‘› โˆ’ 1)) = (1...(๐‘› โˆ’ 1)))
124123prodeq1d 15903 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ โˆ๐‘˜ โˆˆ ((๐‘› โˆ’ (๐‘› โˆ’ 1))...(๐‘› โˆ’ 1))(๐‘› โˆ’ ๐‘˜) = โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘› โˆ’ ๐‘˜))
125113, 121, 1243eqtrd 2771 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ (!โ€˜(๐‘› โˆ’ 1)) = โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘› โˆ’ ๐‘˜))
126111, 125oveq12d 7442 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ ((๐‘›โ†‘(๐‘› โˆ’ 1)) / (!โ€˜(๐‘› โˆ’ 1))) = (โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))๐‘› / โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘› โˆ’ ๐‘˜)))
127104, 126eqtr4d 2770 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘› / (๐‘› โˆ’ ๐‘˜)) = ((๐‘›โ†‘(๐‘› โˆ’ 1)) / (!โ€˜(๐‘› โˆ’ 1))))
128127oveq2d 7440 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ (โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))((๐‘› โˆ’ 1)C๐‘˜) ยท โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘› / (๐‘› โˆ’ ๐‘˜))) = (โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))((๐‘› โˆ’ 1)C๐‘˜) ยท ((๐‘›โ†‘(๐‘› โˆ’ 1)) / (!โ€˜(๐‘› โˆ’ 1)))))
12979, 103, 1283eqtrd 2771 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘›C๐‘˜) = (โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))((๐‘› โˆ’ 1)C๐‘˜) ยท ((๐‘›โ†‘(๐‘› โˆ’ 1)) / (!โ€˜(๐‘› โˆ’ 1)))))
13068, 74, 1293eqtrd 2771 . . . . . 6 (๐‘› โˆˆ โ„• โ†’ (โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘›C๐‘˜) ยท (๐‘›C๐‘›)) = (โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))((๐‘› โˆ’ 1)C๐‘˜) ยท ((๐‘›โ†‘(๐‘› โˆ’ 1)) / (!โ€˜(๐‘› โˆ’ 1)))))
13156, 65, 1303eqtrd 2771 . . . . 5 (๐‘› โˆˆ โ„• โ†’ โˆ๐‘˜ โˆˆ (1...((๐‘› + 1) โˆ’ 1))(((๐‘› + 1) โˆ’ 1)C๐‘˜) = (โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))((๐‘› โˆ’ 1)C๐‘˜) ยท ((๐‘›โ†‘(๐‘› โˆ’ 1)) / (!โ€˜(๐‘› โˆ’ 1)))))
132131adantr 479 . . . 4 ((๐‘› โˆˆ โ„• โˆง โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))((๐‘› โˆ’ 1)C๐‘˜) = โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘›))) โ†’ โˆ๐‘˜ โˆˆ (1...((๐‘› + 1) โˆ’ 1))(((๐‘› + 1) โˆ’ 1)C๐‘˜) = (โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))((๐‘› โˆ’ 1)C๐‘˜) ยท ((๐‘›โ†‘(๐‘› โˆ’ 1)) / (!โ€˜(๐‘› โˆ’ 1)))))
13353prodeq1d 15903 . . . . . 6 (๐‘› โˆˆ โ„• โ†’ โˆ๐‘˜ โˆˆ (1...((๐‘› + 1) โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ (๐‘› + 1))) = โˆ๐‘˜ โˆˆ (1...๐‘›)(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ (๐‘› + 1))))
134 elfznn 13568 . . . . . . . . . 10 (๐‘˜ โˆˆ (1...๐‘›) โ†’ ๐‘˜ โˆˆ โ„•)
135134adantl 480 . . . . . . . . 9 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...๐‘›)) โ†’ ๐‘˜ โˆˆ โ„•)
136135nncnd 12264 . . . . . . . 8 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...๐‘›)) โ†’ ๐‘˜ โˆˆ โ„‚)
137135nnne0d 12298 . . . . . . . 8 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...๐‘›)) โ†’ ๐‘˜ โ‰  0)
138 2nn 12321 . . . . . . . . . . . 12 2 โˆˆ โ„•
139138a1i 11 . . . . . . . . . . 11 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...๐‘›)) โ†’ 2 โˆˆ โ„•)
140139, 135nnmulcld 12301 . . . . . . . . . 10 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...๐‘›)) โ†’ (2 ยท ๐‘˜) โˆˆ โ„•)
141140nnzd 12621 . . . . . . . . 9 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...๐‘›)) โ†’ (2 ยท ๐‘˜) โˆˆ โ„ค)
142 peano2nn 12260 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ (๐‘› + 1) โˆˆ โ„•)
143142adantr 479 . . . . . . . . . 10 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...๐‘›)) โ†’ (๐‘› + 1) โˆˆ โ„•)
144143nnzd 12621 . . . . . . . . 9 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...๐‘›)) โ†’ (๐‘› + 1) โˆˆ โ„ค)
145141, 144zsubcld 12707 . . . . . . . 8 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...๐‘›)) โ†’ ((2 ยท ๐‘˜) โˆ’ (๐‘› + 1)) โˆˆ โ„ค)
146136, 137, 145expclzd 14153 . . . . . . 7 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...๐‘›)) โ†’ (๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ (๐‘› + 1))) โˆˆ โ„‚)
147 id 22 . . . . . . . 8 (๐‘˜ = ๐‘› โ†’ ๐‘˜ = ๐‘›)
148 oveq2 7432 . . . . . . . . 9 (๐‘˜ = ๐‘› โ†’ (2 ยท ๐‘˜) = (2 ยท ๐‘›))
149148oveq1d 7439 . . . . . . . 8 (๐‘˜ = ๐‘› โ†’ ((2 ยท ๐‘˜) โˆ’ (๐‘› + 1)) = ((2 ยท ๐‘›) โˆ’ (๐‘› + 1)))
150147, 149oveq12d 7442 . . . . . . 7 (๐‘˜ = ๐‘› โ†’ (๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ (๐‘› + 1))) = (๐‘›โ†‘((2 ยท ๐‘›) โˆ’ (๐‘› + 1))))
15158, 146, 150fprodm1 15949 . . . . . 6 (๐‘› โˆˆ โ„• โ†’ โˆ๐‘˜ โˆˆ (1...๐‘›)(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ (๐‘› + 1))) = (โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ (๐‘› + 1))) ยท (๐‘›โ†‘((2 ยท ๐‘›) โˆ’ (๐‘› + 1)))))
15286nncnd 12264 . . . . . . . . . . 11 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ ๐‘˜ โˆˆ โ„‚)
15386nnne0d 12298 . . . . . . . . . . 11 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ ๐‘˜ โ‰  0)
154138a1i 11 . . . . . . . . . . . . . 14 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ 2 โˆˆ โ„•)
155154, 86nnmulcld 12301 . . . . . . . . . . . . 13 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ (2 ยท ๐‘˜) โˆˆ โ„•)
156155nnzd 12621 . . . . . . . . . . . 12 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ (2 ยท ๐‘˜) โˆˆ โ„ค)
157114adantr 479 . . . . . . . . . . . 12 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ ๐‘› โˆˆ โ„ค)
158156, 157zsubcld 12707 . . . . . . . . . . 11 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ ((2 ยท ๐‘˜) โˆ’ ๐‘›) โˆˆ โ„ค)
159152, 153, 158expclzd 14153 . . . . . . . . . 10 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ (๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘›)) โˆˆ โ„‚)
16069, 159, 152, 153fproddiv 15943 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))((๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘›)) / ๐‘˜) = (โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘›)) / โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))๐‘˜))
161155nncnd 12264 . . . . . . . . . . . . 13 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ (2 ยท ๐‘˜) โˆˆ โ„‚)
162 1cnd 11245 . . . . . . . . . . . . 13 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ 1 โˆˆ โ„‚)
163161, 84, 162subsub4d 11638 . . . . . . . . . . . 12 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ (((2 ยท ๐‘˜) โˆ’ ๐‘›) โˆ’ 1) = ((2 ยท ๐‘˜) โˆ’ (๐‘› + 1)))
164163oveq2d 7440 . . . . . . . . . . 11 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ (๐‘˜โ†‘(((2 ยท ๐‘˜) โˆ’ ๐‘›) โˆ’ 1)) = (๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ (๐‘› + 1))))
165152, 153, 158expm1d 14158 . . . . . . . . . . 11 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ (๐‘˜โ†‘(((2 ยท ๐‘˜) โˆ’ ๐‘›) โˆ’ 1)) = ((๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘›)) / ๐‘˜))
166164, 165eqtr3d 2769 . . . . . . . . . 10 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ (๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ (๐‘› + 1))) = ((๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘›)) / ๐‘˜))
167166prodeq2dv 15905 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ (๐‘› + 1))) = โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))((๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘›)) / ๐‘˜))
168 fprodfac 15955 . . . . . . . . . . 11 ((๐‘› โˆ’ 1) โˆˆ โ„•0 โ†’ (!โ€˜(๐‘› โˆ’ 1)) = โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))๐‘˜)
16980, 168syl 17 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ (!โ€˜(๐‘› โˆ’ 1)) = โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))๐‘˜)
170169oveq2d 7440 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ (โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘›)) / (!โ€˜(๐‘› โˆ’ 1))) = (โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘›)) / โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))๐‘˜))
171160, 167, 1703eqtr4d 2777 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ (๐‘› + 1))) = (โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘›)) / (!โ€˜(๐‘› โˆ’ 1))))
172138a1i 11 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ 2 โˆˆ โ„•)
173 id 22 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ ๐‘› โˆˆ โ„•)
174172, 173nnmulcld 12301 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ (2 ยท ๐‘›) โˆˆ โ„•)
175174nncnd 12264 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ (2 ยท ๐‘›) โˆˆ โ„‚)
176175, 50, 51subsub4d 11638 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ (((2 ยท ๐‘›) โˆ’ ๐‘›) โˆ’ 1) = ((2 ยท ๐‘›) โˆ’ (๐‘› + 1)))
177502timesd 12491 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ (2 ยท ๐‘›) = (๐‘› + ๐‘›))
17850, 50, 177mvrladdd 11663 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ ((2 ยท ๐‘›) โˆ’ ๐‘›) = ๐‘›)
179178oveq1d 7439 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ (((2 ยท ๐‘›) โˆ’ ๐‘›) โˆ’ 1) = (๐‘› โˆ’ 1))
180176, 179eqtr3d 2769 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ ((2 ยท ๐‘›) โˆ’ (๐‘› + 1)) = (๐‘› โˆ’ 1))
181180oveq2d 7440 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ (๐‘›โ†‘((2 ยท ๐‘›) โˆ’ (๐‘› + 1))) = (๐‘›โ†‘(๐‘› โˆ’ 1)))
182171, 181oveq12d 7442 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ (โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ (๐‘› + 1))) ยท (๐‘›โ†‘((2 ยท ๐‘›) โˆ’ (๐‘› + 1)))) = ((โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘›)) / (!โ€˜(๐‘› โˆ’ 1))) ยท (๐‘›โ†‘(๐‘› โˆ’ 1))))
18369, 159fprodcl 15934 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘›)) โˆˆ โ„‚)
184 faccl 14280 . . . . . . . . . 10 ((๐‘› โˆ’ 1) โˆˆ โ„•0 โ†’ (!โ€˜(๐‘› โˆ’ 1)) โˆˆ โ„•)
18580, 184syl 17 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ (!โ€˜(๐‘› โˆ’ 1)) โˆˆ โ„•)
186185nncnd 12264 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ (!โ€˜(๐‘› โˆ’ 1)) โˆˆ โ„‚)
18750, 80expcld 14148 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ (๐‘›โ†‘(๐‘› โˆ’ 1)) โˆˆ โ„‚)
188185nnne0d 12298 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ (!โ€˜(๐‘› โˆ’ 1)) โ‰  0)
189183, 186, 187, 188div32d 12049 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ ((โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘›)) / (!โ€˜(๐‘› โˆ’ 1))) ยท (๐‘›โ†‘(๐‘› โˆ’ 1))) = (โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘›)) ยท ((๐‘›โ†‘(๐‘› โˆ’ 1)) / (!โ€˜(๐‘› โˆ’ 1)))))
190182, 189eqtrd 2767 . . . . . 6 (๐‘› โˆˆ โ„• โ†’ (โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ (๐‘› + 1))) ยท (๐‘›โ†‘((2 ยท ๐‘›) โˆ’ (๐‘› + 1)))) = (โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘›)) ยท ((๐‘›โ†‘(๐‘› โˆ’ 1)) / (!โ€˜(๐‘› โˆ’ 1)))))
191133, 151, 1903eqtrd 2771 . . . . 5 (๐‘› โˆˆ โ„• โ†’ โˆ๐‘˜ โˆˆ (1...((๐‘› + 1) โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ (๐‘› + 1))) = (โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘›)) ยท ((๐‘›โ†‘(๐‘› โˆ’ 1)) / (!โ€˜(๐‘› โˆ’ 1)))))
192191adantr 479 . . . 4 ((๐‘› โˆˆ โ„• โˆง โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))((๐‘› โˆ’ 1)C๐‘˜) = โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘›))) โ†’ โˆ๐‘˜ โˆˆ (1...((๐‘› + 1) โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ (๐‘› + 1))) = (โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘›)) ยท ((๐‘›โ†‘(๐‘› โˆ’ 1)) / (!โ€˜(๐‘› โˆ’ 1)))))
19349, 132, 1923eqtr4d 2777 . . 3 ((๐‘› โˆˆ โ„• โˆง โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))((๐‘› โˆ’ 1)C๐‘˜) = โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘›))) โ†’ โˆ๐‘˜ โˆˆ (1...((๐‘› + 1) โˆ’ 1))(((๐‘› + 1) โˆ’ 1)C๐‘˜) = โˆ๐‘˜ โˆˆ (1...((๐‘› + 1) โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ (๐‘› + 1))))
194193ex 411 . 2 (๐‘› โˆˆ โ„• โ†’ (โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))((๐‘› โˆ’ 1)C๐‘˜) = โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘›)) โ†’ โˆ๐‘˜ โˆˆ (1...((๐‘› + 1) โˆ’ 1))(((๐‘› + 1) โˆ’ 1)C๐‘˜) = โˆ๐‘˜ โˆˆ (1...((๐‘› + 1) โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ (๐‘› + 1)))))
19514, 24, 34, 44, 47, 194nnind 12266 1 (๐‘ โˆˆ โ„• โ†’ โˆ๐‘˜ โˆˆ (1...(๐‘ โˆ’ 1))((๐‘ โˆ’ 1)C๐‘˜) = โˆ๐‘˜ โˆˆ (1...(๐‘ โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘)))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 394   = wceq 1533   โˆˆ wcel 2098  โˆ…c0 4324   class class class wbr 5150  โ€˜cfv 6551  (class class class)co 7424  Fincfn 8968  โ„‚cc 11142  โ„cr 11143  0cc0 11144  1c1 11145   + caddc 11147   ยท cmul 11149   < clt 11284   โ‰ค cle 11285   โˆ’ cmin 11480   / cdiv 11907  โ„•cn 12248  2c2 12303  โ„•0cn0 12508  โ„คcz 12594  โ„คโ‰ฅcuz 12858  ...cfz 13522  โ†‘cexp 14064  !cfa 14270  Ccbc 14299  โ™ฏchash 14327  โˆcprod 15887
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 2166  ax-ext 2698  ax-rep 5287  ax-sep 5301  ax-nul 5308  ax-pow 5367  ax-pr 5431  ax-un 7744  ax-inf2 9670  ax-cnex 11200  ax-resscn 11201  ax-1cn 11202  ax-icn 11203  ax-addcl 11204  ax-addrcl 11205  ax-mulcl 11206  ax-mulrcl 11207  ax-mulcom 11208  ax-addass 11209  ax-mulass 11210  ax-distr 11211  ax-i2m1 11212  ax-1ne0 11213  ax-1rid 11214  ax-rnegex 11215  ax-rrecex 11216  ax-cnre 11217  ax-pre-lttri 11218  ax-pre-lttrn 11219  ax-pre-ltadd 11220  ax-pre-mulgt0 11221  ax-pre-sup 11222
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2937  df-nel 3043  df-ral 3058  df-rex 3067  df-rmo 3372  df-reu 3373  df-rab 3429  df-v 3473  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4325  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4911  df-int 4952  df-iun 5000  df-br 5151  df-opab 5213  df-mpt 5234  df-tr 5268  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5635  df-se 5636  df-we 5637  df-xp 5686  df-rel 5687  df-cnv 5688  df-co 5689  df-dm 5690  df-rn 5691  df-res 5692  df-ima 5693  df-pred 6308  df-ord 6375  df-on 6376  df-lim 6377  df-suc 6378  df-iota 6503  df-fun 6553  df-fn 6554  df-f 6555  df-f1 6556  df-fo 6557  df-f1o 6558  df-fv 6559  df-isom 6560  df-riota 7380  df-ov 7427  df-oprab 7428  df-mpo 7429  df-om 7875  df-1st 7997  df-2nd 7998  df-frecs 8291  df-wrecs 8322  df-recs 8396  df-rdg 8435  df-1o 8491  df-er 8729  df-en 8969  df-dom 8970  df-sdom 8971  df-fin 8972  df-sup 9471  df-oi 9539  df-card 9968  df-pnf 11286  df-mnf 11287  df-xr 11288  df-ltxr 11289  df-le 11290  df-sub 11482  df-neg 11483  df-div 11908  df-nn 12249  df-2 12311  df-3 12312  df-n0 12509  df-z 12595  df-uz 12859  df-rp 13013  df-fz 13523  df-fzo 13666  df-seq 14005  df-exp 14065  df-fac 14271  df-bc 14300  df-hash 14328  df-cj 15084  df-re 15085  df-im 15086  df-sqrt 15220  df-abs 15221  df-clim 15470  df-prod 15888
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator