Step | Hyp | Ref
| Expression |
1 | | bcp1n 14277 |
. . . . . . 7
โข (๐พ โ (0...(๐ โ 1)) โ (((๐ โ 1) + 1)C๐พ) = (((๐ โ 1)C๐พ) ยท (((๐ โ 1) + 1) / (((๐ โ 1) + 1) โ ๐พ)))) |
2 | | nnz 12578 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ๐ โ
โค) |
3 | 2 | zcnd 12666 |
. . . . . . . . . . 11
โข (๐ โ โ โ ๐ โ
โ) |
4 | 3 | adantl 481 |
. . . . . . . . . 10
โข ((๐พ โ (0...(๐ โ 1)) โง ๐ โ โ) โ ๐ โ โ) |
5 | | 1cnd 11208 |
. . . . . . . . . 10
โข ((๐พ โ (0...(๐ โ 1)) โง ๐ โ โ) โ 1 โ
โ) |
6 | 4, 5 | npcand 11574 |
. . . . . . . . 9
โข ((๐พ โ (0...(๐ โ 1)) โง ๐ โ โ) โ ((๐ โ 1) + 1) = ๐) |
7 | 6 | oveq1d 7417 |
. . . . . . . 8
โข ((๐พ โ (0...(๐ โ 1)) โง ๐ โ โ) โ (((๐ โ 1) + 1)C๐พ) = (๐C๐พ)) |
8 | 6 | oveq1d 7417 |
. . . . . . . . . 10
โข ((๐พ โ (0...(๐ โ 1)) โง ๐ โ โ) โ (((๐ โ 1) + 1) โ ๐พ) = (๐ โ ๐พ)) |
9 | 6, 8 | oveq12d 7420 |
. . . . . . . . 9
โข ((๐พ โ (0...(๐ โ 1)) โง ๐ โ โ) โ (((๐ โ 1) + 1) / (((๐ โ 1) + 1) โ ๐พ)) = (๐ / (๐ โ ๐พ))) |
10 | 9 | oveq2d 7418 |
. . . . . . . 8
โข ((๐พ โ (0...(๐ โ 1)) โง ๐ โ โ) โ (((๐ โ 1)C๐พ) ยท (((๐ โ 1) + 1) / (((๐ โ 1) + 1) โ ๐พ))) = (((๐ โ 1)C๐พ) ยท (๐ / (๐ โ ๐พ)))) |
11 | 7, 10 | eqeq12d 2740 |
. . . . . . 7
โข ((๐พ โ (0...(๐ โ 1)) โง ๐ โ โ) โ ((((๐ โ 1) + 1)C๐พ) = (((๐ โ 1)C๐พ) ยท (((๐ โ 1) + 1) / (((๐ โ 1) + 1) โ ๐พ))) โ (๐C๐พ) = (((๐ โ 1)C๐พ) ยท (๐ / (๐ โ ๐พ))))) |
12 | 1, 11 | imbitrid 243 |
. . . . . 6
โข ((๐พ โ (0...(๐ โ 1)) โง ๐ โ โ) โ (๐พ โ (0...(๐ โ 1)) โ (๐C๐พ) = (((๐ โ 1)C๐พ) ยท (๐ / (๐ โ ๐พ))))) |
13 | 12 | 3impia 1114 |
. . . . 5
โข ((๐พ โ (0...(๐ โ 1)) โง ๐ โ โ โง ๐พ โ (0...(๐ โ 1))) โ (๐C๐พ) = (((๐ โ 1)C๐พ) ยท (๐ / (๐ โ ๐พ)))) |
14 | 13 | 3anidm13 1417 |
. . . 4
โข ((๐พ โ (0...(๐ โ 1)) โง ๐ โ โ) โ (๐C๐พ) = (((๐ โ 1)C๐พ) ยท (๐ / (๐ โ ๐พ)))) |
15 | | elfznn0 13595 |
. . . . . . . . 9
โข (๐พ โ (0...(๐ โ 1)) โ ๐พ โ
โ0) |
16 | 15 | adantr 480 |
. . . . . . . 8
โข ((๐พ โ (0...(๐ โ 1)) โง ๐ โ โ) โ ๐พ โ
โ0) |
17 | | simpr 484 |
. . . . . . . . 9
โข ((๐พ โ (0...(๐ โ 1)) โง ๐ โ โ) โ ๐ โ โ) |
18 | 17 | nnnn0d 12531 |
. . . . . . . 8
โข ((๐พ โ (0...(๐ โ 1)) โง ๐ โ โ) โ ๐ โ
โ0) |
19 | | elfzelz 13502 |
. . . . . . . . . . 11
โข (๐พ โ (0...(๐ โ 1)) โ ๐พ โ โค) |
20 | 19 | adantr 480 |
. . . . . . . . . 10
โข ((๐พ โ (0...(๐ โ 1)) โง ๐ โ โ) โ ๐พ โ โค) |
21 | 20 | zred 12665 |
. . . . . . . . 9
โข ((๐พ โ (0...(๐ โ 1)) โง ๐ โ โ) โ ๐พ โ โ) |
22 | 2 | adantl 481 |
. . . . . . . . . 10
โข ((๐พ โ (0...(๐ โ 1)) โง ๐ โ โ) โ ๐ โ โค) |
23 | 22 | zred 12665 |
. . . . . . . . 9
โข ((๐พ โ (0...(๐ โ 1)) โง ๐ โ โ) โ ๐ โ โ) |
24 | | elfzle2 13506 |
. . . . . . . . . . 11
โข (๐พ โ (0...(๐ โ 1)) โ ๐พ โค (๐ โ 1)) |
25 | 24 | adantr 480 |
. . . . . . . . . 10
โข ((๐พ โ (0...(๐ โ 1)) โง ๐ โ โ) โ ๐พ โค (๐ โ 1)) |
26 | | zltlem1 12614 |
. . . . . . . . . . 11
โข ((๐พ โ โค โง ๐ โ โค) โ (๐พ < ๐ โ ๐พ โค (๐ โ 1))) |
27 | 19, 2, 26 | syl2an 595 |
. . . . . . . . . 10
โข ((๐พ โ (0...(๐ โ 1)) โง ๐ โ โ) โ (๐พ < ๐ โ ๐พ โค (๐ โ 1))) |
28 | 25, 27 | mpbird 257 |
. . . . . . . . 9
โข ((๐พ โ (0...(๐ โ 1)) โง ๐ โ โ) โ ๐พ < ๐) |
29 | 21, 23, 28 | ltled 11361 |
. . . . . . . 8
โข ((๐พ โ (0...(๐ โ 1)) โง ๐ โ โ) โ ๐พ โค ๐) |
30 | | elfz2nn0 13593 |
. . . . . . . 8
โข (๐พ โ (0...๐) โ (๐พ โ โ0 โง ๐ โ โ0
โง ๐พ โค ๐)) |
31 | 16, 18, 29, 30 | syl3anbrc 1340 |
. . . . . . 7
โข ((๐พ โ (0...(๐ โ 1)) โง ๐ โ โ) โ ๐พ โ (0...๐)) |
32 | | bcrpcl 14269 |
. . . . . . 7
โข (๐พ โ (0...๐) โ (๐C๐พ) โ
โ+) |
33 | 31, 32 | syl 17 |
. . . . . 6
โข ((๐พ โ (0...(๐ โ 1)) โง ๐ โ โ) โ (๐C๐พ) โ
โ+) |
34 | 33 | rpcnd 13019 |
. . . . 5
โข ((๐พ โ (0...(๐ โ 1)) โง ๐ โ โ) โ (๐C๐พ) โ โ) |
35 | 19 | zcnd 12666 |
. . . . . . . 8
โข (๐พ โ (0...(๐ โ 1)) โ ๐พ โ โ) |
36 | 35 | adantr 480 |
. . . . . . 7
โข ((๐พ โ (0...(๐ โ 1)) โง ๐ โ โ) โ ๐พ โ โ) |
37 | 4, 36 | subcld 11570 |
. . . . . 6
โข ((๐พ โ (0...(๐ โ 1)) โง ๐ โ โ) โ (๐ โ ๐พ) โ โ) |
38 | 36, 4 | negsubdi2d 11586 |
. . . . . . 7
โข ((๐พ โ (0...(๐ โ 1)) โง ๐ โ โ) โ -(๐พ โ ๐) = (๐ โ ๐พ)) |
39 | 21, 23 | resubcld 11641 |
. . . . . . . . 9
โข ((๐พ โ (0...(๐ โ 1)) โง ๐ โ โ) โ (๐พ โ ๐) โ โ) |
40 | 39 | recnd 11241 |
. . . . . . . 8
โข ((๐พ โ (0...(๐ โ 1)) โง ๐ โ โ) โ (๐พ โ ๐) โ โ) |
41 | 4 | addlidd 11414 |
. . . . . . . . . . 11
โข ((๐พ โ (0...(๐ โ 1)) โง ๐ โ โ) โ (0 + ๐) = ๐) |
42 | 28, 41 | breqtrrd 5167 |
. . . . . . . . . 10
โข ((๐พ โ (0...(๐ โ 1)) โง ๐ โ โ) โ ๐พ < (0 + ๐)) |
43 | | 0red 11216 |
. . . . . . . . . . 11
โข ((๐พ โ (0...(๐ โ 1)) โง ๐ โ โ) โ 0 โ
โ) |
44 | 21, 23, 43 | ltsubaddd 11809 |
. . . . . . . . . 10
โข ((๐พ โ (0...(๐ โ 1)) โง ๐ โ โ) โ ((๐พ โ ๐) < 0 โ ๐พ < (0 + ๐))) |
45 | 42, 44 | mpbird 257 |
. . . . . . . . 9
โข ((๐พ โ (0...(๐ โ 1)) โง ๐ โ โ) โ (๐พ โ ๐) < 0) |
46 | 45 | lt0ne0d 11778 |
. . . . . . . 8
โข ((๐พ โ (0...(๐ โ 1)) โง ๐ โ โ) โ (๐พ โ ๐) โ 0) |
47 | 40, 46 | negne0d 11568 |
. . . . . . 7
โข ((๐พ โ (0...(๐ โ 1)) โง ๐ โ โ) โ -(๐พ โ ๐) โ 0) |
48 | 38, 47 | eqnetrrd 3001 |
. . . . . 6
โข ((๐พ โ (0...(๐ โ 1)) โง ๐ โ โ) โ (๐ โ ๐พ) โ 0) |
49 | 4, 37, 48 | divcld 11989 |
. . . . 5
โข ((๐พ โ (0...(๐ โ 1)) โง ๐ โ โ) โ (๐ / (๐ โ ๐พ)) โ โ) |
50 | | bcrpcl 14269 |
. . . . . . 7
โข (๐พ โ (0...(๐ โ 1)) โ ((๐ โ 1)C๐พ) โ
โ+) |
51 | 50 | adantr 480 |
. . . . . 6
โข ((๐พ โ (0...(๐ โ 1)) โง ๐ โ โ) โ ((๐ โ 1)C๐พ) โ
โ+) |
52 | 51 | rpcnne0d 13026 |
. . . . 5
โข ((๐พ โ (0...(๐ โ 1)) โง ๐ โ โ) โ (((๐ โ 1)C๐พ) โ โ โง ((๐ โ 1)C๐พ) โ 0)) |
53 | | divmul2 11875 |
. . . . 5
โข (((๐C๐พ) โ โ โง (๐ / (๐ โ ๐พ)) โ โ โง (((๐ โ 1)C๐พ) โ โ โง ((๐ โ 1)C๐พ) โ 0)) โ (((๐C๐พ) / ((๐ โ 1)C๐พ)) = (๐ / (๐ โ ๐พ)) โ (๐C๐พ) = (((๐ โ 1)C๐พ) ยท (๐ / (๐ โ ๐พ))))) |
54 | 34, 49, 52, 53 | syl3anc 1368 |
. . . 4
โข ((๐พ โ (0...(๐ โ 1)) โง ๐ โ โ) โ (((๐C๐พ) / ((๐ โ 1)C๐พ)) = (๐ / (๐ โ ๐พ)) โ (๐C๐พ) = (((๐ โ 1)C๐พ) ยท (๐ / (๐ โ ๐พ))))) |
55 | 14, 54 | mpbird 257 |
. . 3
โข ((๐พ โ (0...(๐ โ 1)) โง ๐ โ โ) โ ((๐C๐พ) / ((๐ โ 1)C๐พ)) = (๐ / (๐ โ ๐พ))) |
56 | 55 | oveq2d 7418 |
. 2
โข ((๐พ โ (0...(๐ โ 1)) โง ๐ โ โ) โ (1 / ((๐C๐พ) / ((๐ โ 1)C๐พ))) = (1 / (๐ / (๐ โ ๐พ)))) |
57 | 51 | rpcnd 13019 |
. . 3
โข ((๐พ โ (0...(๐ โ 1)) โง ๐ โ โ) โ ((๐ โ 1)C๐พ) โ โ) |
58 | | bccl2 14284 |
. . . . 5
โข (๐พ โ (0...๐) โ (๐C๐พ) โ โ) |
59 | 31, 58 | syl 17 |
. . . 4
โข ((๐พ โ (0...(๐ โ 1)) โง ๐ โ โ) โ (๐C๐พ) โ โ) |
60 | 59 | nnne0d 12261 |
. . 3
โข ((๐พ โ (0...(๐ โ 1)) โง ๐ โ โ) โ (๐C๐พ) โ 0) |
61 | | bccl2 14284 |
. . . . 5
โข (๐พ โ (0...(๐ โ 1)) โ ((๐ โ 1)C๐พ) โ โ) |
62 | 61 | nnne0d 12261 |
. . . 4
โข (๐พ โ (0...(๐ โ 1)) โ ((๐ โ 1)C๐พ) โ 0) |
63 | 62 | adantr 480 |
. . 3
โข ((๐พ โ (0...(๐ โ 1)) โง ๐ โ โ) โ ((๐ โ 1)C๐พ) โ 0) |
64 | 34, 57, 60, 63 | recdivd 12006 |
. 2
โข ((๐พ โ (0...(๐ โ 1)) โง ๐ โ โ) โ (1 / ((๐C๐พ) / ((๐ โ 1)C๐พ))) = (((๐ โ 1)C๐พ) / (๐C๐พ))) |
65 | 17 | nnne0d 12261 |
. . 3
โข ((๐พ โ (0...(๐ โ 1)) โง ๐ โ โ) โ ๐ โ 0) |
66 | 4, 37, 65, 48 | recdivd 12006 |
. 2
โข ((๐พ โ (0...(๐ โ 1)) โง ๐ โ โ) โ (1 / (๐ / (๐ โ ๐พ))) = ((๐ โ ๐พ) / ๐)) |
67 | 56, 64, 66 | 3eqtr3d 2772 |
1
โข ((๐พ โ (0...(๐ โ 1)) โง ๐ โ โ) โ (((๐ โ 1)C๐พ) / (๐C๐พ)) = ((๐ โ ๐พ) / ๐)) |