Step | Hyp | Ref
| Expression |
1 | | oveq2 7366 |
. . . . . 6
โข (๐ = 0 โ ((๐ด + ๐ต) FallFac ๐) = ((๐ด + ๐ต) FallFac 0)) |
2 | | oveq2 7366 |
. . . . . . . 8
โข (๐ = 0 โ (0...๐) = (0...0)) |
3 | | fz0sn 13547 |
. . . . . . . 8
โข (0...0) =
{0} |
4 | 2, 3 | eqtrdi 2789 |
. . . . . . 7
โข (๐ = 0 โ (0...๐) = {0}) |
5 | | oveq1 7365 |
. . . . . . . . 9
โข (๐ = 0 โ (๐C๐) = (0C๐)) |
6 | | oveq1 7365 |
. . . . . . . . . . 11
โข (๐ = 0 โ (๐ โ ๐) = (0 โ ๐)) |
7 | 6 | oveq2d 7374 |
. . . . . . . . . 10
โข (๐ = 0 โ (๐ด FallFac (๐ โ ๐)) = (๐ด FallFac (0 โ ๐))) |
8 | 7 | oveq1d 7373 |
. . . . . . . . 9
โข (๐ = 0 โ ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐)) = ((๐ด FallFac (0 โ ๐)) ยท (๐ต FallFac ๐))) |
9 | 5, 8 | oveq12d 7376 |
. . . . . . . 8
โข (๐ = 0 โ ((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐))) = ((0C๐) ยท ((๐ด FallFac (0 โ ๐)) ยท (๐ต FallFac ๐)))) |
10 | 9 | adantr 482 |
. . . . . . 7
โข ((๐ = 0 โง ๐ โ (0...๐)) โ ((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐))) = ((0C๐) ยท ((๐ด FallFac (0 โ ๐)) ยท (๐ต FallFac ๐)))) |
11 | 4, 10 | sumeq12dv 15596 |
. . . . . 6
โข (๐ = 0 โ ฮฃ๐ โ (0...๐)((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐))) = ฮฃ๐ โ {0} ((0C๐) ยท ((๐ด FallFac (0 โ ๐)) ยท (๐ต FallFac ๐)))) |
12 | 1, 11 | eqeq12d 2749 |
. . . . 5
โข (๐ = 0 โ (((๐ด + ๐ต) FallFac ๐) = ฮฃ๐ โ (0...๐)((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐))) โ ((๐ด + ๐ต) FallFac 0) = ฮฃ๐ โ {0} ((0C๐) ยท ((๐ด FallFac (0 โ ๐)) ยท (๐ต FallFac ๐))))) |
13 | 12 | imbi2d 341 |
. . . 4
โข (๐ = 0 โ (((๐ด โ โ โง ๐ต โ โ) โ ((๐ด + ๐ต) FallFac ๐) = ฮฃ๐ โ (0...๐)((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐)))) โ ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด + ๐ต) FallFac 0) = ฮฃ๐ โ {0} ((0C๐) ยท ((๐ด FallFac (0 โ ๐)) ยท (๐ต FallFac ๐)))))) |
14 | | oveq2 7366 |
. . . . . 6
โข (๐ = ๐ โ ((๐ด + ๐ต) FallFac ๐) = ((๐ด + ๐ต) FallFac ๐)) |
15 | | oveq2 7366 |
. . . . . . 7
โข (๐ = ๐ โ (0...๐) = (0...๐)) |
16 | | oveq1 7365 |
. . . . . . . . 9
โข (๐ = ๐ โ (๐C๐) = (๐C๐)) |
17 | | oveq1 7365 |
. . . . . . . . . . 11
โข (๐ = ๐ โ (๐ โ ๐) = (๐ โ ๐)) |
18 | 17 | oveq2d 7374 |
. . . . . . . . . 10
โข (๐ = ๐ โ (๐ด FallFac (๐ โ ๐)) = (๐ด FallFac (๐ โ ๐))) |
19 | 18 | oveq1d 7373 |
. . . . . . . . 9
โข (๐ = ๐ โ ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐)) = ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐))) |
20 | 16, 19 | oveq12d 7376 |
. . . . . . . 8
โข (๐ = ๐ โ ((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐))) = ((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐)))) |
21 | 20 | adantr 482 |
. . . . . . 7
โข ((๐ = ๐ โง ๐ โ (0...๐)) โ ((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐))) = ((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐)))) |
22 | 15, 21 | sumeq12dv 15596 |
. . . . . 6
โข (๐ = ๐ โ ฮฃ๐ โ (0...๐)((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐))) = ฮฃ๐ โ (0...๐)((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐)))) |
23 | 14, 22 | eqeq12d 2749 |
. . . . 5
โข (๐ = ๐ โ (((๐ด + ๐ต) FallFac ๐) = ฮฃ๐ โ (0...๐)((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐))) โ ((๐ด + ๐ต) FallFac ๐) = ฮฃ๐ โ (0...๐)((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐))))) |
24 | 23 | imbi2d 341 |
. . . 4
โข (๐ = ๐ โ (((๐ด โ โ โง ๐ต โ โ) โ ((๐ด + ๐ต) FallFac ๐) = ฮฃ๐ โ (0...๐)((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐)))) โ ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด + ๐ต) FallFac ๐) = ฮฃ๐ โ (0...๐)((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐)))))) |
25 | | oveq2 7366 |
. . . . . 6
โข (๐ = (๐ + 1) โ ((๐ด + ๐ต) FallFac ๐) = ((๐ด + ๐ต) FallFac (๐ + 1))) |
26 | | oveq2 7366 |
. . . . . . 7
โข (๐ = (๐ + 1) โ (0...๐) = (0...(๐ + 1))) |
27 | | oveq1 7365 |
. . . . . . . . 9
โข (๐ = (๐ + 1) โ (๐C๐) = ((๐ + 1)C๐)) |
28 | | oveq1 7365 |
. . . . . . . . . . 11
โข (๐ = (๐ + 1) โ (๐ โ ๐) = ((๐ + 1) โ ๐)) |
29 | 28 | oveq2d 7374 |
. . . . . . . . . 10
โข (๐ = (๐ + 1) โ (๐ด FallFac (๐ โ ๐)) = (๐ด FallFac ((๐ + 1) โ ๐))) |
30 | 29 | oveq1d 7373 |
. . . . . . . . 9
โข (๐ = (๐ + 1) โ ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐)) = ((๐ด FallFac ((๐ + 1) โ ๐)) ยท (๐ต FallFac ๐))) |
31 | 27, 30 | oveq12d 7376 |
. . . . . . . 8
โข (๐ = (๐ + 1) โ ((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐))) = (((๐ + 1)C๐) ยท ((๐ด FallFac ((๐ + 1) โ ๐)) ยท (๐ต FallFac ๐)))) |
32 | 31 | adantr 482 |
. . . . . . 7
โข ((๐ = (๐ + 1) โง ๐ โ (0...๐)) โ ((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐))) = (((๐ + 1)C๐) ยท ((๐ด FallFac ((๐ + 1) โ ๐)) ยท (๐ต FallFac ๐)))) |
33 | 26, 32 | sumeq12dv 15596 |
. . . . . 6
โข (๐ = (๐ + 1) โ ฮฃ๐ โ (0...๐)((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐))) = ฮฃ๐ โ (0...(๐ + 1))(((๐ + 1)C๐) ยท ((๐ด FallFac ((๐ + 1) โ ๐)) ยท (๐ต FallFac ๐)))) |
34 | 25, 33 | eqeq12d 2749 |
. . . . 5
โข (๐ = (๐ + 1) โ (((๐ด + ๐ต) FallFac ๐) = ฮฃ๐ โ (0...๐)((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐))) โ ((๐ด + ๐ต) FallFac (๐ + 1)) = ฮฃ๐ โ (0...(๐ + 1))(((๐ + 1)C๐) ยท ((๐ด FallFac ((๐ + 1) โ ๐)) ยท (๐ต FallFac ๐))))) |
35 | 34 | imbi2d 341 |
. . . 4
โข (๐ = (๐ + 1) โ (((๐ด โ โ โง ๐ต โ โ) โ ((๐ด + ๐ต) FallFac ๐) = ฮฃ๐ โ (0...๐)((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐)))) โ ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด + ๐ต) FallFac (๐ + 1)) = ฮฃ๐ โ (0...(๐ + 1))(((๐ + 1)C๐) ยท ((๐ด FallFac ((๐ + 1) โ ๐)) ยท (๐ต FallFac ๐)))))) |
36 | | oveq2 7366 |
. . . . . 6
โข (๐ = ๐ โ ((๐ด + ๐ต) FallFac ๐) = ((๐ด + ๐ต) FallFac ๐)) |
37 | | oveq2 7366 |
. . . . . . 7
โข (๐ = ๐ โ (0...๐) = (0...๐)) |
38 | | oveq1 7365 |
. . . . . . . . 9
โข (๐ = ๐ โ (๐C๐) = (๐C๐)) |
39 | | oveq1 7365 |
. . . . . . . . . . 11
โข (๐ = ๐ โ (๐ โ ๐) = (๐ โ ๐)) |
40 | 39 | oveq2d 7374 |
. . . . . . . . . 10
โข (๐ = ๐ โ (๐ด FallFac (๐ โ ๐)) = (๐ด FallFac (๐ โ ๐))) |
41 | 40 | oveq1d 7373 |
. . . . . . . . 9
โข (๐ = ๐ โ ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐)) = ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐))) |
42 | 38, 41 | oveq12d 7376 |
. . . . . . . 8
โข (๐ = ๐ โ ((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐))) = ((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐)))) |
43 | 42 | adantr 482 |
. . . . . . 7
โข ((๐ = ๐ โง ๐ โ (0...๐)) โ ((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐))) = ((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐)))) |
44 | 37, 43 | sumeq12dv 15596 |
. . . . . 6
โข (๐ = ๐ โ ฮฃ๐ โ (0...๐)((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐))) = ฮฃ๐ โ (0...๐)((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐)))) |
45 | 36, 44 | eqeq12d 2749 |
. . . . 5
โข (๐ = ๐ โ (((๐ด + ๐ต) FallFac ๐) = ฮฃ๐ โ (0...๐)((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐))) โ ((๐ด + ๐ต) FallFac ๐) = ฮฃ๐ โ (0...๐)((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐))))) |
46 | 45 | imbi2d 341 |
. . . 4
โข (๐ = ๐ โ (((๐ด โ โ โง ๐ต โ โ) โ ((๐ด + ๐ต) FallFac ๐) = ฮฃ๐ โ (0...๐)((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐)))) โ ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด + ๐ต) FallFac ๐) = ฮฃ๐ โ (0...๐)((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐)))))) |
47 | | fallfac0 15916 |
. . . . . . . . 9
โข (๐ด โ โ โ (๐ด FallFac 0) =
1) |
48 | | fallfac0 15916 |
. . . . . . . . 9
โข (๐ต โ โ โ (๐ต FallFac 0) =
1) |
49 | 47, 48 | oveqan12d 7377 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด FallFac 0) ยท (๐ต FallFac 0)) = (1 ยท
1)) |
50 | | 1t1e1 12320 |
. . . . . . . 8
โข (1
ยท 1) = 1 |
51 | 49, 50 | eqtrdi 2789 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด FallFac 0) ยท (๐ต FallFac 0)) =
1) |
52 | 51 | oveq2d 7374 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ (1
ยท ((๐ด FallFac 0)
ยท (๐ต FallFac 0))) =
(1 ยท 1)) |
53 | 52, 50 | eqtrdi 2789 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ (1
ยท ((๐ด FallFac 0)
ยท (๐ต FallFac 0))) =
1) |
54 | | 0cn 11152 |
. . . . . 6
โข 0 โ
โ |
55 | | ax-1cn 11114 |
. . . . . . 7
โข 1 โ
โ |
56 | 53, 55 | eqeltrdi 2842 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ (1
ยท ((๐ด FallFac 0)
ยท (๐ต FallFac 0)))
โ โ) |
57 | | oveq2 7366 |
. . . . . . . . 9
โข (๐ = 0 โ (0C๐) = (0C0)) |
58 | | 0nn0 12433 |
. . . . . . . . . 10
โข 0 โ
โ0 |
59 | | bcnn 14218 |
. . . . . . . . . 10
โข (0 โ
โ0 โ (0C0) = 1) |
60 | 58, 59 | ax-mp 5 |
. . . . . . . . 9
โข (0C0) =
1 |
61 | 57, 60 | eqtrdi 2789 |
. . . . . . . 8
โข (๐ = 0 โ (0C๐) = 1) |
62 | | oveq2 7366 |
. . . . . . . . . . 11
โข (๐ = 0 โ (0 โ ๐) = (0 โ
0)) |
63 | | 0m0e0 12278 |
. . . . . . . . . . 11
โข (0
โ 0) = 0 |
64 | 62, 63 | eqtrdi 2789 |
. . . . . . . . . 10
โข (๐ = 0 โ (0 โ ๐) = 0) |
65 | 64 | oveq2d 7374 |
. . . . . . . . 9
โข (๐ = 0 โ (๐ด FallFac (0 โ ๐)) = (๐ด FallFac 0)) |
66 | | oveq2 7366 |
. . . . . . . . 9
โข (๐ = 0 โ (๐ต FallFac ๐) = (๐ต FallFac 0)) |
67 | 65, 66 | oveq12d 7376 |
. . . . . . . 8
โข (๐ = 0 โ ((๐ด FallFac (0 โ ๐)) ยท (๐ต FallFac ๐)) = ((๐ด FallFac 0) ยท (๐ต FallFac 0))) |
68 | 61, 67 | oveq12d 7376 |
. . . . . . 7
โข (๐ = 0 โ ((0C๐) ยท ((๐ด FallFac (0 โ ๐)) ยท (๐ต FallFac ๐))) = (1 ยท ((๐ด FallFac 0) ยท (๐ต FallFac 0)))) |
69 | 68 | sumsn 15636 |
. . . . . 6
โข ((0
โ โ โง (1 ยท ((๐ด FallFac 0) ยท (๐ต FallFac 0))) โ โ) โ
ฮฃ๐ โ {0}
((0C๐) ยท ((๐ด FallFac (0 โ ๐)) ยท (๐ต FallFac ๐))) = (1 ยท ((๐ด FallFac 0) ยท (๐ต FallFac 0)))) |
70 | 54, 56, 69 | sylancr 588 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ
ฮฃ๐ โ {0}
((0C๐) ยท ((๐ด FallFac (0 โ ๐)) ยท (๐ต FallFac ๐))) = (1 ยท ((๐ด FallFac 0) ยท (๐ต FallFac 0)))) |
71 | | addcl 11138 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด + ๐ต) โ โ) |
72 | | fallfac0 15916 |
. . . . . 6
โข ((๐ด + ๐ต) โ โ โ ((๐ด + ๐ต) FallFac 0) = 1) |
73 | 71, 72 | syl 17 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด + ๐ต) FallFac 0) = 1) |
74 | 53, 70, 73 | 3eqtr4rd 2784 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด + ๐ต) FallFac 0) = ฮฃ๐ โ {0} ((0C๐) ยท ((๐ด FallFac (0 โ ๐)) ยท (๐ต FallFac ๐)))) |
75 | | simprl 770 |
. . . . . . 7
โข ((๐ โ โ0
โง (๐ด โ โ
โง ๐ต โ โ))
โ ๐ด โ
โ) |
76 | | simprr 772 |
. . . . . . 7
โข ((๐ โ โ0
โง (๐ด โ โ
โง ๐ต โ โ))
โ ๐ต โ
โ) |
77 | | simpl 484 |
. . . . . . 7
โข ((๐ โ โ0
โง (๐ด โ โ
โง ๐ต โ โ))
โ ๐ โ
โ0) |
78 | | id 22 |
. . . . . . 7
โข (((๐ด + ๐ต) FallFac ๐) = ฮฃ๐ โ (0...๐)((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐))) โ ((๐ด + ๐ต) FallFac ๐) = ฮฃ๐ โ (0...๐)((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐)))) |
79 | 75, 76, 77, 78 | binomfallfaclem2 15928 |
. . . . . 6
โข (((๐ โ โ0
โง (๐ด โ โ
โง ๐ต โ โ))
โง ((๐ด + ๐ต) FallFac ๐) = ฮฃ๐ โ (0...๐)((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐)))) โ ((๐ด + ๐ต) FallFac (๐ + 1)) = ฮฃ๐ โ (0...(๐ + 1))(((๐ + 1)C๐) ยท ((๐ด FallFac ((๐ + 1) โ ๐)) ยท (๐ต FallFac ๐)))) |
80 | 79 | exp31 421 |
. . . . 5
โข (๐ โ โ0
โ ((๐ด โ โ
โง ๐ต โ โ)
โ (((๐ด + ๐ต) FallFac ๐) = ฮฃ๐ โ (0...๐)((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐))) โ ((๐ด + ๐ต) FallFac (๐ + 1)) = ฮฃ๐ โ (0...(๐ + 1))(((๐ + 1)C๐) ยท ((๐ด FallFac ((๐ + 1) โ ๐)) ยท (๐ต FallFac ๐)))))) |
81 | 80 | a2d 29 |
. . . 4
โข (๐ โ โ0
โ (((๐ด โ โ
โง ๐ต โ โ)
โ ((๐ด + ๐ต) FallFac ๐) = ฮฃ๐ โ (0...๐)((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐)))) โ ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด + ๐ต) FallFac (๐ + 1)) = ฮฃ๐ โ (0...(๐ + 1))(((๐ + 1)C๐) ยท ((๐ด FallFac ((๐ + 1) โ ๐)) ยท (๐ต FallFac ๐)))))) |
82 | 13, 24, 35, 46, 74, 81 | nn0ind 12603 |
. . 3
โข (๐ โ โ0
โ ((๐ด โ โ
โง ๐ต โ โ)
โ ((๐ด + ๐ต) FallFac ๐) = ฮฃ๐ โ (0...๐)((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐))))) |
83 | 82 | com12 32 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ โ โ0
โ ((๐ด + ๐ต) FallFac ๐) = ฮฃ๐ โ (0...๐)((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐))))) |
84 | 83 | 3impia 1118 |
1
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ0)
โ ((๐ด + ๐ต) FallFac ๐) = ฮฃ๐ โ (0...๐)((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐)))) |