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 35241
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 7411 . . . . . . 7 (๐‘š = 1 โ†’ (๐‘š โˆ’ 1) = (1 โˆ’ 1))
2 1m1e0 12285 . . . . . . 7 (1 โˆ’ 1) = 0
31, 2eqtrdi 2782 . . . . . 6 (๐‘š = 1 โ†’ (๐‘š โˆ’ 1) = 0)
43oveq2d 7420 . . . . 5 (๐‘š = 1 โ†’ (1...(๐‘š โˆ’ 1)) = (1...0))
5 fz10 13525 . . . . 5 (1...0) = โˆ…
64, 5eqtrdi 2782 . . . 4 (๐‘š = 1 โ†’ (1...(๐‘š โˆ’ 1)) = โˆ…)
73oveq1d 7419 . . . . 5 (๐‘š = 1 โ†’ ((๐‘š โˆ’ 1)C๐‘˜) = (0C๐‘˜))
87adantr 480 . . . 4 ((๐‘š = 1 โˆง ๐‘˜ โˆˆ (1...(๐‘š โˆ’ 1))) โ†’ ((๐‘š โˆ’ 1)C๐‘˜) = (0C๐‘˜))
96, 8prodeq12dv 15874 . . 3 (๐‘š = 1 โ†’ โˆ๐‘˜ โˆˆ (1...(๐‘š โˆ’ 1))((๐‘š โˆ’ 1)C๐‘˜) = โˆ๐‘˜ โˆˆ โˆ… (0C๐‘˜))
10 oveq2 7412 . . . . . 6 (๐‘š = 1 โ†’ ((2 ยท ๐‘˜) โˆ’ ๐‘š) = ((2 ยท ๐‘˜) โˆ’ 1))
1110oveq2d 7420 . . . . 5 (๐‘š = 1 โ†’ (๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘š)) = (๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ 1)))
1211adantr 480 . . . 4 ((๐‘š = 1 โˆง ๐‘˜ โˆˆ (1...(๐‘š โˆ’ 1))) โ†’ (๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘š)) = (๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ 1)))
136, 12prodeq12dv 15874 . . 3 (๐‘š = 1 โ†’ โˆ๐‘˜ โˆˆ (1...(๐‘š โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘š)) = โˆ๐‘˜ โˆˆ โˆ… (๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ 1)))
149, 13eqeq12d 2742 . 2 (๐‘š = 1 โ†’ (โˆ๐‘˜ โˆˆ (1...(๐‘š โˆ’ 1))((๐‘š โˆ’ 1)C๐‘˜) = โˆ๐‘˜ โˆˆ (1...(๐‘š โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘š)) โ†” โˆ๐‘˜ โˆˆ โˆ… (0C๐‘˜) = โˆ๐‘˜ โˆˆ โˆ… (๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ 1))))
15 oveq1 7411 . . . . 5 (๐‘š = ๐‘› โ†’ (๐‘š โˆ’ 1) = (๐‘› โˆ’ 1))
1615oveq2d 7420 . . . 4 (๐‘š = ๐‘› โ†’ (1...(๐‘š โˆ’ 1)) = (1...(๐‘› โˆ’ 1)))
1715oveq1d 7419 . . . . 5 (๐‘š = ๐‘› โ†’ ((๐‘š โˆ’ 1)C๐‘˜) = ((๐‘› โˆ’ 1)C๐‘˜))
1817adantr 480 . . . 4 ((๐‘š = ๐‘› โˆง ๐‘˜ โˆˆ (1...(๐‘š โˆ’ 1))) โ†’ ((๐‘š โˆ’ 1)C๐‘˜) = ((๐‘› โˆ’ 1)C๐‘˜))
1916, 18prodeq12dv 15874 . . 3 (๐‘š = ๐‘› โ†’ โˆ๐‘˜ โˆˆ (1...(๐‘š โˆ’ 1))((๐‘š โˆ’ 1)C๐‘˜) = โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))((๐‘› โˆ’ 1)C๐‘˜))
20 oveq2 7412 . . . . . 6 (๐‘š = ๐‘› โ†’ ((2 ยท ๐‘˜) โˆ’ ๐‘š) = ((2 ยท ๐‘˜) โˆ’ ๐‘›))
2120oveq2d 7420 . . . . 5 (๐‘š = ๐‘› โ†’ (๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘š)) = (๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘›)))
2221adantr 480 . . . 4 ((๐‘š = ๐‘› โˆง ๐‘˜ โˆˆ (1...(๐‘š โˆ’ 1))) โ†’ (๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘š)) = (๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘›)))
2316, 22prodeq12dv 15874 . . 3 (๐‘š = ๐‘› โ†’ โˆ๐‘˜ โˆˆ (1...(๐‘š โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘š)) = โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘›)))
2419, 23eqeq12d 2742 . 2 (๐‘š = ๐‘› โ†’ (โˆ๐‘˜ โˆˆ (1...(๐‘š โˆ’ 1))((๐‘š โˆ’ 1)C๐‘˜) = โˆ๐‘˜ โˆˆ (1...(๐‘š โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘š)) โ†” โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))((๐‘› โˆ’ 1)C๐‘˜) = โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘›))))
25 oveq1 7411 . . . . 5 (๐‘š = (๐‘› + 1) โ†’ (๐‘š โˆ’ 1) = ((๐‘› + 1) โˆ’ 1))
2625oveq2d 7420 . . . 4 (๐‘š = (๐‘› + 1) โ†’ (1...(๐‘š โˆ’ 1)) = (1...((๐‘› + 1) โˆ’ 1)))
2725oveq1d 7419 . . . . 5 (๐‘š = (๐‘› + 1) โ†’ ((๐‘š โˆ’ 1)C๐‘˜) = (((๐‘› + 1) โˆ’ 1)C๐‘˜))
2827adantr 480 . . . 4 ((๐‘š = (๐‘› + 1) โˆง ๐‘˜ โˆˆ (1...(๐‘š โˆ’ 1))) โ†’ ((๐‘š โˆ’ 1)C๐‘˜) = (((๐‘› + 1) โˆ’ 1)C๐‘˜))
2926, 28prodeq12dv 15874 . . 3 (๐‘š = (๐‘› + 1) โ†’ โˆ๐‘˜ โˆˆ (1...(๐‘š โˆ’ 1))((๐‘š โˆ’ 1)C๐‘˜) = โˆ๐‘˜ โˆˆ (1...((๐‘› + 1) โˆ’ 1))(((๐‘› + 1) โˆ’ 1)C๐‘˜))
30 oveq2 7412 . . . . . 6 (๐‘š = (๐‘› + 1) โ†’ ((2 ยท ๐‘˜) โˆ’ ๐‘š) = ((2 ยท ๐‘˜) โˆ’ (๐‘› + 1)))
3130oveq2d 7420 . . . . 5 (๐‘š = (๐‘› + 1) โ†’ (๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘š)) = (๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ (๐‘› + 1))))
3231adantr 480 . . . 4 ((๐‘š = (๐‘› + 1) โˆง ๐‘˜ โˆˆ (1...(๐‘š โˆ’ 1))) โ†’ (๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘š)) = (๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ (๐‘› + 1))))
3326, 32prodeq12dv 15874 . . 3 (๐‘š = (๐‘› + 1) โ†’ โˆ๐‘˜ โˆˆ (1...(๐‘š โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘š)) = โˆ๐‘˜ โˆˆ (1...((๐‘› + 1) โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ (๐‘› + 1))))
3429, 33eqeq12d 2742 . 2 (๐‘š = (๐‘› + 1) โ†’ (โˆ๐‘˜ โˆˆ (1...(๐‘š โˆ’ 1))((๐‘š โˆ’ 1)C๐‘˜) = โˆ๐‘˜ โˆˆ (1...(๐‘š โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘š)) โ†” โˆ๐‘˜ โˆˆ (1...((๐‘› + 1) โˆ’ 1))(((๐‘› + 1) โˆ’ 1)C๐‘˜) = โˆ๐‘˜ โˆˆ (1...((๐‘› + 1) โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ (๐‘› + 1)))))
35 oveq1 7411 . . . . 5 (๐‘š = ๐‘ โ†’ (๐‘š โˆ’ 1) = (๐‘ โˆ’ 1))
3635oveq2d 7420 . . . 4 (๐‘š = ๐‘ โ†’ (1...(๐‘š โˆ’ 1)) = (1...(๐‘ โˆ’ 1)))
3735oveq1d 7419 . . . . 5 (๐‘š = ๐‘ โ†’ ((๐‘š โˆ’ 1)C๐‘˜) = ((๐‘ โˆ’ 1)C๐‘˜))
3837adantr 480 . . . 4 ((๐‘š = ๐‘ โˆง ๐‘˜ โˆˆ (1...(๐‘š โˆ’ 1))) โ†’ ((๐‘š โˆ’ 1)C๐‘˜) = ((๐‘ โˆ’ 1)C๐‘˜))
3936, 38prodeq12dv 15874 . . 3 (๐‘š = ๐‘ โ†’ โˆ๐‘˜ โˆˆ (1...(๐‘š โˆ’ 1))((๐‘š โˆ’ 1)C๐‘˜) = โˆ๐‘˜ โˆˆ (1...(๐‘ โˆ’ 1))((๐‘ โˆ’ 1)C๐‘˜))
40 oveq2 7412 . . . . . 6 (๐‘š = ๐‘ โ†’ ((2 ยท ๐‘˜) โˆ’ ๐‘š) = ((2 ยท ๐‘˜) โˆ’ ๐‘))
4140oveq2d 7420 . . . . 5 (๐‘š = ๐‘ โ†’ (๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘š)) = (๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘)))
4241adantr 480 . . . 4 ((๐‘š = ๐‘ โˆง ๐‘˜ โˆˆ (1...(๐‘š โˆ’ 1))) โ†’ (๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘š)) = (๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘)))
4336, 42prodeq12dv 15874 . . 3 (๐‘š = ๐‘ โ†’ โˆ๐‘˜ โˆˆ (1...(๐‘š โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘š)) = โˆ๐‘˜ โˆˆ (1...(๐‘ โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘)))
4439, 43eqeq12d 2742 . 2 (๐‘š = ๐‘ โ†’ (โˆ๐‘˜ โˆˆ (1...(๐‘š โˆ’ 1))((๐‘š โˆ’ 1)C๐‘˜) = โˆ๐‘˜ โˆˆ (1...(๐‘š โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘š)) โ†” โˆ๐‘˜ โˆˆ (1...(๐‘ โˆ’ 1))((๐‘ โˆ’ 1)C๐‘˜) = โˆ๐‘˜ โˆˆ (1...(๐‘ โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘))))
45 prod0 15891 . . 3 โˆ๐‘˜ โˆˆ โˆ… (0C๐‘˜) = 1
46 prod0 15891 . . 3 โˆ๐‘˜ โˆˆ โˆ… (๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ 1)) = 1
4745, 46eqtr4i 2757 . 2 โˆ๐‘˜ โˆˆ โˆ… (0C๐‘˜) = โˆ๐‘˜ โˆˆ โˆ… (๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ 1))
48 simpr 484 . . . . 5 ((๐‘› โˆˆ โ„• โˆง โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))((๐‘› โˆ’ 1)C๐‘˜) = โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘›))) โ†’ โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))((๐‘› โˆ’ 1)C๐‘˜) = โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘›)))
4948oveq1d 7419 . . . 4 ((๐‘› โˆˆ โ„• โˆง โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))((๐‘› โˆ’ 1)C๐‘˜) = โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘›))) โ†’ (โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))((๐‘› โˆ’ 1)C๐‘˜) ยท ((๐‘›โ†‘(๐‘› โˆ’ 1)) / (!โ€˜(๐‘› โˆ’ 1)))) = (โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘›)) ยท ((๐‘›โ†‘(๐‘› โˆ’ 1)) / (!โ€˜(๐‘› โˆ’ 1)))))
50 nncn 12221 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ ๐‘› โˆˆ โ„‚)
51 1cnd 11210 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ 1 โˆˆ โ„‚)
5250, 51pncand 11573 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ ((๐‘› + 1) โˆ’ 1) = ๐‘›)
5352oveq2d 7420 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ (1...((๐‘› + 1) โˆ’ 1)) = (1...๐‘›))
5452oveq1d 7419 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ (((๐‘› + 1) โˆ’ 1)C๐‘˜) = (๐‘›C๐‘˜))
5554adantr 480 . . . . . . 7 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...((๐‘› + 1) โˆ’ 1))) โ†’ (((๐‘› + 1) โˆ’ 1)C๐‘˜) = (๐‘›C๐‘˜))
5653, 55prodeq12dv 15874 . . . . . 6 (๐‘› โˆˆ โ„• โ†’ โˆ๐‘˜ โˆˆ (1...((๐‘› + 1) โˆ’ 1))(((๐‘› + 1) โˆ’ 1)C๐‘˜) = โˆ๐‘˜ โˆˆ (1...๐‘›)(๐‘›C๐‘˜))
57 elnnuz 12867 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†” ๐‘› โˆˆ (โ„คโ‰ฅโ€˜1))
5857biimpi 215 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ ๐‘› โˆˆ (โ„คโ‰ฅโ€˜1))
59 nnnn0 12480 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ ๐‘› โˆˆ โ„•0)
60 elfzelz 13504 . . . . . . . . 9 (๐‘˜ โˆˆ (1...๐‘›) โ†’ ๐‘˜ โˆˆ โ„ค)
61 bccl 14285 . . . . . . . . 9 ((๐‘› โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ โ„ค) โ†’ (๐‘›C๐‘˜) โˆˆ โ„•0)
6259, 60, 61syl2an 595 . . . . . . . 8 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...๐‘›)) โ†’ (๐‘›C๐‘˜) โˆˆ โ„•0)
6362nn0cnd 12535 . . . . . . 7 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...๐‘›)) โ†’ (๐‘›C๐‘˜) โˆˆ โ„‚)
64 oveq2 7412 . . . . . . 7 (๐‘˜ = ๐‘› โ†’ (๐‘›C๐‘˜) = (๐‘›C๐‘›))
6558, 63, 64fprodm1 15915 . . . . . 6 (๐‘› โˆˆ โ„• โ†’ โˆ๐‘˜ โˆˆ (1...๐‘›)(๐‘›C๐‘˜) = (โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘›C๐‘˜) ยท (๐‘›C๐‘›)))
66 bcnn 14275 . . . . . . . . 9 (๐‘› โˆˆ โ„•0 โ†’ (๐‘›C๐‘›) = 1)
6759, 66syl 17 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ (๐‘›C๐‘›) = 1)
6867oveq2d 7420 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ (โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘›C๐‘˜) ยท (๐‘›C๐‘›)) = (โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘›C๐‘˜) ยท 1))
69 fzfid 13941 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ (1...(๐‘› โˆ’ 1)) โˆˆ Fin)
70 elfzelz 13504 . . . . . . . . . . 11 (๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1)) โ†’ ๐‘˜ โˆˆ โ„ค)
7159, 70, 61syl2an 595 . . . . . . . . . 10 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ (๐‘›C๐‘˜) โˆˆ โ„•0)
7271nn0cnd 12535 . . . . . . . . 9 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ (๐‘›C๐‘˜) โˆˆ โ„‚)
7369, 72fprodcl 15900 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘›C๐‘˜) โˆˆ โ„‚)
7473mulridd 11232 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ (โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘›C๐‘˜) ยท 1) = โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘›C๐‘˜))
75 fz1ssfz0 13600 . . . . . . . . . . 11 (1...(๐‘› โˆ’ 1)) โІ (0...(๐‘› โˆ’ 1))
7675sseli 3973 . . . . . . . . . 10 (๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1)) โ†’ ๐‘˜ โˆˆ (0...(๐‘› โˆ’ 1)))
77 bcm1nt 35240 . . . . . . . . . 10 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (0...(๐‘› โˆ’ 1))) โ†’ (๐‘›C๐‘˜) = (((๐‘› โˆ’ 1)C๐‘˜) ยท (๐‘› / (๐‘› โˆ’ ๐‘˜))))
7876, 77sylan2 592 . . . . . . . . 9 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ (๐‘›C๐‘˜) = (((๐‘› โˆ’ 1)C๐‘˜) ยท (๐‘› / (๐‘› โˆ’ ๐‘˜))))
7978prodeq2dv 15871 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘›C๐‘˜) = โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(((๐‘› โˆ’ 1)C๐‘˜) ยท (๐‘› / (๐‘› โˆ’ ๐‘˜))))
80 nnm1nn0 12514 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ (๐‘› โˆ’ 1) โˆˆ โ„•0)
81 bccl 14285 . . . . . . . . . . 11 (((๐‘› โˆ’ 1) โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ โ„ค) โ†’ ((๐‘› โˆ’ 1)C๐‘˜) โˆˆ โ„•0)
8280, 70, 81syl2an 595 . . . . . . . . . 10 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ ((๐‘› โˆ’ 1)C๐‘˜) โˆˆ โ„•0)
8382nn0cnd 12535 . . . . . . . . 9 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ ((๐‘› โˆ’ 1)C๐‘˜) โˆˆ โ„‚)
8450adantr 480 . . . . . . . . . 10 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ ๐‘› โˆˆ โ„‚)
85 elfznn 13533 . . . . . . . . . . . . . . 15 (๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1)) โ†’ ๐‘˜ โˆˆ โ„•)
8685adantl 481 . . . . . . . . . . . . . 14 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ ๐‘˜ โˆˆ โ„•)
8786nnred 12228 . . . . . . . . . . . . 13 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ ๐‘˜ โˆˆ โ„)
8880adantr 480 . . . . . . . . . . . . . 14 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ (๐‘› โˆ’ 1) โˆˆ โ„•0)
8988nn0red 12534 . . . . . . . . . . . . 13 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ (๐‘› โˆ’ 1) โˆˆ โ„)
90 nnre 12220 . . . . . . . . . . . . . 14 (๐‘› โˆˆ โ„• โ†’ ๐‘› โˆˆ โ„)
9190adantr 480 . . . . . . . . . . . . 13 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ ๐‘› โˆˆ โ„)
92 elfzle2 13508 . . . . . . . . . . . . . 14 (๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1)) โ†’ ๐‘˜ โ‰ค (๐‘› โˆ’ 1))
9392adantl 481 . . . . . . . . . . . . 13 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ ๐‘˜ โ‰ค (๐‘› โˆ’ 1))
9491ltm1d 12147 . . . . . . . . . . . . 13 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ (๐‘› โˆ’ 1) < ๐‘›)
9587, 89, 91, 93, 94lelttrd 11373 . . . . . . . . . . . 12 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ ๐‘˜ < ๐‘›)
96 simpl 482 . . . . . . . . . . . . 13 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ ๐‘› โˆˆ โ„•)
97 nnsub 12257 . . . . . . . . . . . . 13 ((๐‘˜ โˆˆ โ„• โˆง ๐‘› โˆˆ โ„•) โ†’ (๐‘˜ < ๐‘› โ†” (๐‘› โˆ’ ๐‘˜) โˆˆ โ„•))
9886, 96, 97syl2anc 583 . . . . . . . . . . . 12 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ (๐‘˜ < ๐‘› โ†” (๐‘› โˆ’ ๐‘˜) โˆˆ โ„•))
9995, 98mpbid 231 . . . . . . . . . . 11 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ (๐‘› โˆ’ ๐‘˜) โˆˆ โ„•)
10099nncnd 12229 . . . . . . . . . 10 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ (๐‘› โˆ’ ๐‘˜) โˆˆ โ„‚)
10199nnne0d 12263 . . . . . . . . . 10 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ (๐‘› โˆ’ ๐‘˜) โ‰  0)
10284, 100, 101divcld 11991 . . . . . . . . 9 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ (๐‘› / (๐‘› โˆ’ ๐‘˜)) โˆˆ โ„‚)
10369, 83, 102fprodmul 15908 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(((๐‘› โˆ’ 1)C๐‘˜) ยท (๐‘› / (๐‘› โˆ’ ๐‘˜))) = (โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))((๐‘› โˆ’ 1)C๐‘˜) ยท โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘› / (๐‘› โˆ’ ๐‘˜))))
10469, 84, 100, 101fproddiv 15909 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘› / (๐‘› โˆ’ ๐‘˜)) = (โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))๐‘› / โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘› โˆ’ ๐‘˜)))
105 fzfi 13940 . . . . . . . . . . . . 13 (1...(๐‘› โˆ’ 1)) โˆˆ Fin
106 fprodconst 15926 . . . . . . . . . . . . 13 (((1...(๐‘› โˆ’ 1)) โˆˆ Fin โˆง ๐‘› โˆˆ โ„‚) โ†’ โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))๐‘› = (๐‘›โ†‘(โ™ฏโ€˜(1...(๐‘› โˆ’ 1)))))
107105, 50, 106sylancr 586 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))๐‘› = (๐‘›โ†‘(โ™ฏโ€˜(1...(๐‘› โˆ’ 1)))))
108 hashfz1 14309 . . . . . . . . . . . . . 14 ((๐‘› โˆ’ 1) โˆˆ โ„•0 โ†’ (โ™ฏโ€˜(1...(๐‘› โˆ’ 1))) = (๐‘› โˆ’ 1))
10980, 108syl 17 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ (โ™ฏโ€˜(1...(๐‘› โˆ’ 1))) = (๐‘› โˆ’ 1))
110109oveq2d 7420 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ (๐‘›โ†‘(โ™ฏโ€˜(1...(๐‘› โˆ’ 1)))) = (๐‘›โ†‘(๐‘› โˆ’ 1)))
111107, 110eqtr2d 2767 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ (๐‘›โ†‘(๐‘› โˆ’ 1)) = โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))๐‘›)
112 fprodfac 15921 . . . . . . . . . . . . 13 ((๐‘› โˆ’ 1) โˆˆ โ„•0 โ†’ (!โ€˜(๐‘› โˆ’ 1)) = โˆ๐‘— โˆˆ (1...(๐‘› โˆ’ 1))๐‘—)
11380, 112syl 17 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ (!โ€˜(๐‘› โˆ’ 1)) = โˆ๐‘— โˆˆ (1...(๐‘› โˆ’ 1))๐‘—)
114 nnz 12580 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ ๐‘› โˆˆ โ„ค)
115 1zzd 12594 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ 1 โˆˆ โ„ค)
11680nn0zd 12585 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ (๐‘› โˆ’ 1) โˆˆ โ„ค)
117 elfznn 13533 . . . . . . . . . . . . . . 15 (๐‘— โˆˆ (1...(๐‘› โˆ’ 1)) โ†’ ๐‘— โˆˆ โ„•)
118117adantl 481 . . . . . . . . . . . . . 14 ((๐‘› โˆˆ โ„• โˆง ๐‘— โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ ๐‘— โˆˆ โ„•)
119118nncnd 12229 . . . . . . . . . . . . 13 ((๐‘› โˆˆ โ„• โˆง ๐‘— โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ ๐‘— โˆˆ โ„‚)
120 id 22 . . . . . . . . . . . . 13 (๐‘— = (๐‘› โˆ’ ๐‘˜) โ†’ ๐‘— = (๐‘› โˆ’ ๐‘˜))
121114, 115, 116, 119, 120fprodrev 15925 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ โˆ๐‘— โˆˆ (1...(๐‘› โˆ’ 1))๐‘— = โˆ๐‘˜ โˆˆ ((๐‘› โˆ’ (๐‘› โˆ’ 1))...(๐‘› โˆ’ 1))(๐‘› โˆ’ ๐‘˜))
12250, 51nncand 11577 . . . . . . . . . . . . . 14 (๐‘› โˆˆ โ„• โ†’ (๐‘› โˆ’ (๐‘› โˆ’ 1)) = 1)
123122oveq1d 7419 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ ((๐‘› โˆ’ (๐‘› โˆ’ 1))...(๐‘› โˆ’ 1)) = (1...(๐‘› โˆ’ 1)))
124123prodeq1d 15869 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ โˆ๐‘˜ โˆˆ ((๐‘› โˆ’ (๐‘› โˆ’ 1))...(๐‘› โˆ’ 1))(๐‘› โˆ’ ๐‘˜) = โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘› โˆ’ ๐‘˜))
125113, 121, 1243eqtrd 2770 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ (!โ€˜(๐‘› โˆ’ 1)) = โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘› โˆ’ ๐‘˜))
126111, 125oveq12d 7422 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ ((๐‘›โ†‘(๐‘› โˆ’ 1)) / (!โ€˜(๐‘› โˆ’ 1))) = (โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))๐‘› / โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘› โˆ’ ๐‘˜)))
127104, 126eqtr4d 2769 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘› / (๐‘› โˆ’ ๐‘˜)) = ((๐‘›โ†‘(๐‘› โˆ’ 1)) / (!โ€˜(๐‘› โˆ’ 1))))
128127oveq2d 7420 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ (โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))((๐‘› โˆ’ 1)C๐‘˜) ยท โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘› / (๐‘› โˆ’ ๐‘˜))) = (โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))((๐‘› โˆ’ 1)C๐‘˜) ยท ((๐‘›โ†‘(๐‘› โˆ’ 1)) / (!โ€˜(๐‘› โˆ’ 1)))))
12979, 103, 1283eqtrd 2770 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘›C๐‘˜) = (โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))((๐‘› โˆ’ 1)C๐‘˜) ยท ((๐‘›โ†‘(๐‘› โˆ’ 1)) / (!โ€˜(๐‘› โˆ’ 1)))))
13068, 74, 1293eqtrd 2770 . . . . . 6 (๐‘› โˆˆ โ„• โ†’ (โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘›C๐‘˜) ยท (๐‘›C๐‘›)) = (โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))((๐‘› โˆ’ 1)C๐‘˜) ยท ((๐‘›โ†‘(๐‘› โˆ’ 1)) / (!โ€˜(๐‘› โˆ’ 1)))))
13156, 65, 1303eqtrd 2770 . . . . 5 (๐‘› โˆˆ โ„• โ†’ โˆ๐‘˜ โˆˆ (1...((๐‘› + 1) โˆ’ 1))(((๐‘› + 1) โˆ’ 1)C๐‘˜) = (โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))((๐‘› โˆ’ 1)C๐‘˜) ยท ((๐‘›โ†‘(๐‘› โˆ’ 1)) / (!โ€˜(๐‘› โˆ’ 1)))))
132131adantr 480 . . . 4 ((๐‘› โˆˆ โ„• โˆง โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))((๐‘› โˆ’ 1)C๐‘˜) = โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘›))) โ†’ โˆ๐‘˜ โˆˆ (1...((๐‘› + 1) โˆ’ 1))(((๐‘› + 1) โˆ’ 1)C๐‘˜) = (โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))((๐‘› โˆ’ 1)C๐‘˜) ยท ((๐‘›โ†‘(๐‘› โˆ’ 1)) / (!โ€˜(๐‘› โˆ’ 1)))))
13353prodeq1d 15869 . . . . . 6 (๐‘› โˆˆ โ„• โ†’ โˆ๐‘˜ โˆˆ (1...((๐‘› + 1) โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ (๐‘› + 1))) = โˆ๐‘˜ โˆˆ (1...๐‘›)(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ (๐‘› + 1))))
134 elfznn 13533 . . . . . . . . . 10 (๐‘˜ โˆˆ (1...๐‘›) โ†’ ๐‘˜ โˆˆ โ„•)
135134adantl 481 . . . . . . . . 9 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...๐‘›)) โ†’ ๐‘˜ โˆˆ โ„•)
136135nncnd 12229 . . . . . . . 8 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...๐‘›)) โ†’ ๐‘˜ โˆˆ โ„‚)
137135nnne0d 12263 . . . . . . . 8 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...๐‘›)) โ†’ ๐‘˜ โ‰  0)
138 2nn 12286 . . . . . . . . . . . 12 2 โˆˆ โ„•
139138a1i 11 . . . . . . . . . . 11 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...๐‘›)) โ†’ 2 โˆˆ โ„•)
140139, 135nnmulcld 12266 . . . . . . . . . 10 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...๐‘›)) โ†’ (2 ยท ๐‘˜) โˆˆ โ„•)
141140nnzd 12586 . . . . . . . . 9 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...๐‘›)) โ†’ (2 ยท ๐‘˜) โˆˆ โ„ค)
142 peano2nn 12225 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ (๐‘› + 1) โˆˆ โ„•)
143142adantr 480 . . . . . . . . . 10 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...๐‘›)) โ†’ (๐‘› + 1) โˆˆ โ„•)
144143nnzd 12586 . . . . . . . . 9 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...๐‘›)) โ†’ (๐‘› + 1) โˆˆ โ„ค)
145141, 144zsubcld 12672 . . . . . . . 8 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...๐‘›)) โ†’ ((2 ยท ๐‘˜) โˆ’ (๐‘› + 1)) โˆˆ โ„ค)
146136, 137, 145expclzd 14119 . . . . . . 7 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...๐‘›)) โ†’ (๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ (๐‘› + 1))) โˆˆ โ„‚)
147 id 22 . . . . . . . 8 (๐‘˜ = ๐‘› โ†’ ๐‘˜ = ๐‘›)
148 oveq2 7412 . . . . . . . . 9 (๐‘˜ = ๐‘› โ†’ (2 ยท ๐‘˜) = (2 ยท ๐‘›))
149148oveq1d 7419 . . . . . . . 8 (๐‘˜ = ๐‘› โ†’ ((2 ยท ๐‘˜) โˆ’ (๐‘› + 1)) = ((2 ยท ๐‘›) โˆ’ (๐‘› + 1)))
150147, 149oveq12d 7422 . . . . . . 7 (๐‘˜ = ๐‘› โ†’ (๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ (๐‘› + 1))) = (๐‘›โ†‘((2 ยท ๐‘›) โˆ’ (๐‘› + 1))))
15158, 146, 150fprodm1 15915 . . . . . 6 (๐‘› โˆˆ โ„• โ†’ โˆ๐‘˜ โˆˆ (1...๐‘›)(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ (๐‘› + 1))) = (โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ (๐‘› + 1))) ยท (๐‘›โ†‘((2 ยท ๐‘›) โˆ’ (๐‘› + 1)))))
15286nncnd 12229 . . . . . . . . . . 11 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ ๐‘˜ โˆˆ โ„‚)
15386nnne0d 12263 . . . . . . . . . . 11 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ ๐‘˜ โ‰  0)
154138a1i 11 . . . . . . . . . . . . . 14 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ 2 โˆˆ โ„•)
155154, 86nnmulcld 12266 . . . . . . . . . . . . 13 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ (2 ยท ๐‘˜) โˆˆ โ„•)
156155nnzd 12586 . . . . . . . . . . . 12 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ (2 ยท ๐‘˜) โˆˆ โ„ค)
157114adantr 480 . . . . . . . . . . . 12 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ ๐‘› โˆˆ โ„ค)
158156, 157zsubcld 12672 . . . . . . . . . . 11 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ ((2 ยท ๐‘˜) โˆ’ ๐‘›) โˆˆ โ„ค)
159152, 153, 158expclzd 14119 . . . . . . . . . 10 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ (๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘›)) โˆˆ โ„‚)
16069, 159, 152, 153fproddiv 15909 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))((๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘›)) / ๐‘˜) = (โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘›)) / โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))๐‘˜))
161155nncnd 12229 . . . . . . . . . . . . 13 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ (2 ยท ๐‘˜) โˆˆ โ„‚)
162 1cnd 11210 . . . . . . . . . . . . 13 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ 1 โˆˆ โ„‚)
163161, 84, 162subsub4d 11603 . . . . . . . . . . . 12 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ (((2 ยท ๐‘˜) โˆ’ ๐‘›) โˆ’ 1) = ((2 ยท ๐‘˜) โˆ’ (๐‘› + 1)))
164163oveq2d 7420 . . . . . . . . . . 11 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ (๐‘˜โ†‘(((2 ยท ๐‘˜) โˆ’ ๐‘›) โˆ’ 1)) = (๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ (๐‘› + 1))))
165152, 153, 158expm1d 14124 . . . . . . . . . . 11 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ (๐‘˜โ†‘(((2 ยท ๐‘˜) โˆ’ ๐‘›) โˆ’ 1)) = ((๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘›)) / ๐‘˜))
166164, 165eqtr3d 2768 . . . . . . . . . 10 ((๐‘› โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))) โ†’ (๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ (๐‘› + 1))) = ((๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘›)) / ๐‘˜))
167166prodeq2dv 15871 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ (๐‘› + 1))) = โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))((๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘›)) / ๐‘˜))
168 fprodfac 15921 . . . . . . . . . . 11 ((๐‘› โˆ’ 1) โˆˆ โ„•0 โ†’ (!โ€˜(๐‘› โˆ’ 1)) = โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))๐‘˜)
16980, 168syl 17 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ (!โ€˜(๐‘› โˆ’ 1)) = โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))๐‘˜)
170169oveq2d 7420 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ (โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘›)) / (!โ€˜(๐‘› โˆ’ 1))) = (โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘›)) / โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))๐‘˜))
171160, 167, 1703eqtr4d 2776 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ (๐‘› + 1))) = (โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘›)) / (!โ€˜(๐‘› โˆ’ 1))))
172138a1i 11 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ 2 โˆˆ โ„•)
173 id 22 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ ๐‘› โˆˆ โ„•)
174172, 173nnmulcld 12266 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ (2 ยท ๐‘›) โˆˆ โ„•)
175174nncnd 12229 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ (2 ยท ๐‘›) โˆˆ โ„‚)
176175, 50, 51subsub4d 11603 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ (((2 ยท ๐‘›) โˆ’ ๐‘›) โˆ’ 1) = ((2 ยท ๐‘›) โˆ’ (๐‘› + 1)))
177502timesd 12456 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ (2 ยท ๐‘›) = (๐‘› + ๐‘›))
17850, 50, 177mvrladdd 11628 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ ((2 ยท ๐‘›) โˆ’ ๐‘›) = ๐‘›)
179178oveq1d 7419 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ (((2 ยท ๐‘›) โˆ’ ๐‘›) โˆ’ 1) = (๐‘› โˆ’ 1))
180176, 179eqtr3d 2768 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ ((2 ยท ๐‘›) โˆ’ (๐‘› + 1)) = (๐‘› โˆ’ 1))
181180oveq2d 7420 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ (๐‘›โ†‘((2 ยท ๐‘›) โˆ’ (๐‘› + 1))) = (๐‘›โ†‘(๐‘› โˆ’ 1)))
182171, 181oveq12d 7422 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ (โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ (๐‘› + 1))) ยท (๐‘›โ†‘((2 ยท ๐‘›) โˆ’ (๐‘› + 1)))) = ((โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘›)) / (!โ€˜(๐‘› โˆ’ 1))) ยท (๐‘›โ†‘(๐‘› โˆ’ 1))))
18369, 159fprodcl 15900 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘›)) โˆˆ โ„‚)
184 faccl 14246 . . . . . . . . . 10 ((๐‘› โˆ’ 1) โˆˆ โ„•0 โ†’ (!โ€˜(๐‘› โˆ’ 1)) โˆˆ โ„•)
18580, 184syl 17 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ (!โ€˜(๐‘› โˆ’ 1)) โˆˆ โ„•)
186185nncnd 12229 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ (!โ€˜(๐‘› โˆ’ 1)) โˆˆ โ„‚)
18750, 80expcld 14114 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ (๐‘›โ†‘(๐‘› โˆ’ 1)) โˆˆ โ„‚)
188185nnne0d 12263 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ (!โ€˜(๐‘› โˆ’ 1)) โ‰  0)
189183, 186, 187, 188div32d 12014 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ ((โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘›)) / (!โ€˜(๐‘› โˆ’ 1))) ยท (๐‘›โ†‘(๐‘› โˆ’ 1))) = (โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘›)) ยท ((๐‘›โ†‘(๐‘› โˆ’ 1)) / (!โ€˜(๐‘› โˆ’ 1)))))
190182, 189eqtrd 2766 . . . . . 6 (๐‘› โˆˆ โ„• โ†’ (โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ (๐‘› + 1))) ยท (๐‘›โ†‘((2 ยท ๐‘›) โˆ’ (๐‘› + 1)))) = (โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘›)) ยท ((๐‘›โ†‘(๐‘› โˆ’ 1)) / (!โ€˜(๐‘› โˆ’ 1)))))
191133, 151, 1903eqtrd 2770 . . . . 5 (๐‘› โˆˆ โ„• โ†’ โˆ๐‘˜ โˆˆ (1...((๐‘› + 1) โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ (๐‘› + 1))) = (โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘›)) ยท ((๐‘›โ†‘(๐‘› โˆ’ 1)) / (!โ€˜(๐‘› โˆ’ 1)))))
192191adantr 480 . . . 4 ((๐‘› โˆˆ โ„• โˆง โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))((๐‘› โˆ’ 1)C๐‘˜) = โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘›))) โ†’ โˆ๐‘˜ โˆˆ (1...((๐‘› + 1) โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ (๐‘› + 1))) = (โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘›)) ยท ((๐‘›โ†‘(๐‘› โˆ’ 1)) / (!โ€˜(๐‘› โˆ’ 1)))))
19349, 132, 1923eqtr4d 2776 . . 3 ((๐‘› โˆˆ โ„• โˆง โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))((๐‘› โˆ’ 1)C๐‘˜) = โˆ๐‘˜ โˆˆ (1...(๐‘› โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘›))) โ†’ โˆ๐‘˜ โˆˆ (1...((๐‘› + 1) โˆ’ 1))(((๐‘› + 1) โˆ’ 1)C๐‘˜) = โˆ๐‘˜ โˆˆ (1...((๐‘› + 1) โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ (๐‘› + 1))))
194193ex 412 . 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 12231 1 (๐‘ โˆˆ โ„• โ†’ โˆ๐‘˜ โˆˆ (1...(๐‘ โˆ’ 1))((๐‘ โˆ’ 1)C๐‘˜) = โˆ๐‘˜ โˆˆ (1...(๐‘ โˆ’ 1))(๐‘˜โ†‘((2 ยท ๐‘˜) โˆ’ ๐‘)))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 395   = wceq 1533   โˆˆ wcel 2098  โˆ…c0 4317   class class class wbr 5141  โ€˜cfv 6536  (class class class)co 7404  Fincfn 8938  โ„‚cc 11107  โ„cr 11108  0cc0 11109  1c1 11110   + caddc 11112   ยท cmul 11114   < clt 11249   โ‰ค cle 11250   โˆ’ cmin 11445   / cdiv 11872  โ„•cn 12213  2c2 12268  โ„•0cn0 12473  โ„คcz 12559  โ„คโ‰ฅcuz 12823  ...cfz 13487  โ†‘cexp 14030  !cfa 14236  Ccbc 14265  โ™ฏchash 14293  โˆcprod 15853
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-inf2 9635  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  ax-pre-sup 11187
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-se 5625  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-isom 6545  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-er 8702  df-en 8939  df-dom 8940  df-sdom 8941  df-fin 8942  df-sup 9436  df-oi 9504  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-2 12276  df-3 12277  df-n0 12474  df-z 12560  df-uz 12824  df-rp 12978  df-fz 13488  df-fzo 13631  df-seq 13970  df-exp 14031  df-fac 14237  df-bc 14266  df-hash 14294  df-cj 15050  df-re 15051  df-im 15052  df-sqrt 15186  df-abs 15187  df-clim 15436  df-prod 15854
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator