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

Theorem bcmono 27161
Description: The binomial coefficient is monotone in its second argument, up to the midway point. (Contributed by Mario Carneiro, 5-Mar-2014.)
Assertion
Ref Expression
bcmono ((๐‘ โˆˆ โ„•0 โˆง ๐ต โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐ต โ‰ค (๐‘ / 2)) โ†’ (๐‘C๐ด) โ‰ค (๐‘C๐ต))

Proof of Theorem bcmono
Dummy variables ๐‘ฅ ๐‘˜ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpl2 1189 . . 3 (((๐‘ โˆˆ โ„•0 โˆง ๐ต โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐ต โ‰ค (๐‘ / 2)) โˆง 0 โ‰ค ๐ด) โ†’ ๐ต โˆˆ (โ„คโ‰ฅโ€˜๐ด))
2 simpl1 1188 . . 3 (((๐‘ โˆˆ โ„•0 โˆง ๐ต โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐ต โ‰ค (๐‘ / 2)) โˆง 0 โ‰ค ๐ด) โ†’ ๐‘ โˆˆ โ„•0)
3 eluzel2 12828 . . . . . 6 (๐ต โˆˆ (โ„คโ‰ฅโ€˜๐ด) โ†’ ๐ด โˆˆ โ„ค)
433ad2ant2 1131 . . . . 5 ((๐‘ โˆˆ โ„•0 โˆง ๐ต โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐ต โ‰ค (๐‘ / 2)) โ†’ ๐ด โˆˆ โ„ค)
54anim1i 614 . . . 4 (((๐‘ โˆˆ โ„•0 โˆง ๐ต โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐ต โ‰ค (๐‘ / 2)) โˆง 0 โ‰ค ๐ด) โ†’ (๐ด โˆˆ โ„ค โˆง 0 โ‰ค ๐ด))
6 elnn0z 12572 . . . 4 (๐ด โˆˆ โ„•0 โ†” (๐ด โˆˆ โ„ค โˆง 0 โ‰ค ๐ด))
75, 6sylibr 233 . . 3 (((๐‘ โˆˆ โ„•0 โˆง ๐ต โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐ต โ‰ค (๐‘ / 2)) โˆง 0 โ‰ค ๐ด) โ†’ ๐ด โˆˆ โ„•0)
8 simpl3 1190 . . 3 (((๐‘ โˆˆ โ„•0 โˆง ๐ต โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐ต โ‰ค (๐‘ / 2)) โˆง 0 โ‰ค ๐ด) โ†’ ๐ต โ‰ค (๐‘ / 2))
9 breq1 5144 . . . . . . 7 (๐‘ฅ = ๐ด โ†’ (๐‘ฅ โ‰ค (๐‘ / 2) โ†” ๐ด โ‰ค (๐‘ / 2)))
10 oveq2 7412 . . . . . . . 8 (๐‘ฅ = ๐ด โ†’ (๐‘C๐‘ฅ) = (๐‘C๐ด))
1110breq2d 5153 . . . . . . 7 (๐‘ฅ = ๐ด โ†’ ((๐‘C๐ด) โ‰ค (๐‘C๐‘ฅ) โ†” (๐‘C๐ด) โ‰ค (๐‘C๐ด)))
129, 11imbi12d 344 . . . . . 6 (๐‘ฅ = ๐ด โ†’ ((๐‘ฅ โ‰ค (๐‘ / 2) โ†’ (๐‘C๐ด) โ‰ค (๐‘C๐‘ฅ)) โ†” (๐ด โ‰ค (๐‘ / 2) โ†’ (๐‘C๐ด) โ‰ค (๐‘C๐ด))))
1312imbi2d 340 . . . . 5 (๐‘ฅ = ๐ด โ†’ (((๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โ†’ (๐‘ฅ โ‰ค (๐‘ / 2) โ†’ (๐‘C๐ด) โ‰ค (๐‘C๐‘ฅ))) โ†” ((๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โ†’ (๐ด โ‰ค (๐‘ / 2) โ†’ (๐‘C๐ด) โ‰ค (๐‘C๐ด)))))
14 breq1 5144 . . . . . . 7 (๐‘ฅ = ๐‘˜ โ†’ (๐‘ฅ โ‰ค (๐‘ / 2) โ†” ๐‘˜ โ‰ค (๐‘ / 2)))
15 oveq2 7412 . . . . . . . 8 (๐‘ฅ = ๐‘˜ โ†’ (๐‘C๐‘ฅ) = (๐‘C๐‘˜))
1615breq2d 5153 . . . . . . 7 (๐‘ฅ = ๐‘˜ โ†’ ((๐‘C๐ด) โ‰ค (๐‘C๐‘ฅ) โ†” (๐‘C๐ด) โ‰ค (๐‘C๐‘˜)))
1714, 16imbi12d 344 . . . . . 6 (๐‘ฅ = ๐‘˜ โ†’ ((๐‘ฅ โ‰ค (๐‘ / 2) โ†’ (๐‘C๐ด) โ‰ค (๐‘C๐‘ฅ)) โ†” (๐‘˜ โ‰ค (๐‘ / 2) โ†’ (๐‘C๐ด) โ‰ค (๐‘C๐‘˜))))
1817imbi2d 340 . . . . 5 (๐‘ฅ = ๐‘˜ โ†’ (((๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โ†’ (๐‘ฅ โ‰ค (๐‘ / 2) โ†’ (๐‘C๐ด) โ‰ค (๐‘C๐‘ฅ))) โ†” ((๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โ†’ (๐‘˜ โ‰ค (๐‘ / 2) โ†’ (๐‘C๐ด) โ‰ค (๐‘C๐‘˜)))))
19 breq1 5144 . . . . . . 7 (๐‘ฅ = (๐‘˜ + 1) โ†’ (๐‘ฅ โ‰ค (๐‘ / 2) โ†” (๐‘˜ + 1) โ‰ค (๐‘ / 2)))
20 oveq2 7412 . . . . . . . 8 (๐‘ฅ = (๐‘˜ + 1) โ†’ (๐‘C๐‘ฅ) = (๐‘C(๐‘˜ + 1)))
2120breq2d 5153 . . . . . . 7 (๐‘ฅ = (๐‘˜ + 1) โ†’ ((๐‘C๐ด) โ‰ค (๐‘C๐‘ฅ) โ†” (๐‘C๐ด) โ‰ค (๐‘C(๐‘˜ + 1))))
2219, 21imbi12d 344 . . . . . 6 (๐‘ฅ = (๐‘˜ + 1) โ†’ ((๐‘ฅ โ‰ค (๐‘ / 2) โ†’ (๐‘C๐ด) โ‰ค (๐‘C๐‘ฅ)) โ†” ((๐‘˜ + 1) โ‰ค (๐‘ / 2) โ†’ (๐‘C๐ด) โ‰ค (๐‘C(๐‘˜ + 1)))))
2322imbi2d 340 . . . . 5 (๐‘ฅ = (๐‘˜ + 1) โ†’ (((๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โ†’ (๐‘ฅ โ‰ค (๐‘ / 2) โ†’ (๐‘C๐ด) โ‰ค (๐‘C๐‘ฅ))) โ†” ((๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โ†’ ((๐‘˜ + 1) โ‰ค (๐‘ / 2) โ†’ (๐‘C๐ด) โ‰ค (๐‘C(๐‘˜ + 1))))))
24 breq1 5144 . . . . . . 7 (๐‘ฅ = ๐ต โ†’ (๐‘ฅ โ‰ค (๐‘ / 2) โ†” ๐ต โ‰ค (๐‘ / 2)))
25 oveq2 7412 . . . . . . . 8 (๐‘ฅ = ๐ต โ†’ (๐‘C๐‘ฅ) = (๐‘C๐ต))
2625breq2d 5153 . . . . . . 7 (๐‘ฅ = ๐ต โ†’ ((๐‘C๐ด) โ‰ค (๐‘C๐‘ฅ) โ†” (๐‘C๐ด) โ‰ค (๐‘C๐ต)))
2724, 26imbi12d 344 . . . . . 6 (๐‘ฅ = ๐ต โ†’ ((๐‘ฅ โ‰ค (๐‘ / 2) โ†’ (๐‘C๐ด) โ‰ค (๐‘C๐‘ฅ)) โ†” (๐ต โ‰ค (๐‘ / 2) โ†’ (๐‘C๐ด) โ‰ค (๐‘C๐ต))))
2827imbi2d 340 . . . . 5 (๐‘ฅ = ๐ต โ†’ (((๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โ†’ (๐‘ฅ โ‰ค (๐‘ / 2) โ†’ (๐‘C๐ด) โ‰ค (๐‘C๐‘ฅ))) โ†” ((๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โ†’ (๐ต โ‰ค (๐‘ / 2) โ†’ (๐‘C๐ด) โ‰ค (๐‘C๐ต)))))
29 bccl 14285 . . . . . . . . . 10 ((๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„ค) โ†’ (๐‘C๐ด) โˆˆ โ„•0)
3029nn0red 12534 . . . . . . . . 9 ((๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„ค) โ†’ (๐‘C๐ด) โˆˆ โ„)
3130leidd 11781 . . . . . . . 8 ((๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„ค) โ†’ (๐‘C๐ด) โ‰ค (๐‘C๐ด))
3231a1d 25 . . . . . . 7 ((๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„ค) โ†’ (๐ด โ‰ค (๐‘ / 2) โ†’ (๐‘C๐ด) โ‰ค (๐‘C๐ด)))
3332expcom 413 . . . . . 6 (๐ด โˆˆ โ„ค โ†’ (๐‘ โˆˆ โ„•0 โ†’ (๐ด โ‰ค (๐‘ / 2) โ†’ (๐‘C๐ด) โ‰ค (๐‘C๐ด))))
3433adantrd 491 . . . . 5 (๐ด โˆˆ โ„ค โ†’ ((๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โ†’ (๐ด โ‰ค (๐‘ / 2) โ†’ (๐‘C๐ด) โ‰ค (๐‘C๐ด))))
35 eluzelz 12833 . . . . . . . . . . . . 13 (๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐ด) โ†’ ๐‘˜ โˆˆ โ„ค)
36353ad2ant1 1130 . . . . . . . . . . . 12 ((๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โ†’ ๐‘˜ โˆˆ โ„ค)
3736zred 12667 . . . . . . . . . . 11 ((๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โ†’ ๐‘˜ โˆˆ โ„)
3837lep1d 12146 . . . . . . . . . 10 ((๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โ†’ ๐‘˜ โ‰ค (๐‘˜ + 1))
39 peano2re 11388 . . . . . . . . . . . 12 (๐‘˜ โˆˆ โ„ โ†’ (๐‘˜ + 1) โˆˆ โ„)
4037, 39syl 17 . . . . . . . . . . 11 ((๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โ†’ (๐‘˜ + 1) โˆˆ โ„)
41 nn0re 12482 . . . . . . . . . . . . 13 (๐‘ โˆˆ โ„•0 โ†’ ๐‘ โˆˆ โ„)
42413ad2ant2 1131 . . . . . . . . . . . 12 ((๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โ†’ ๐‘ โˆˆ โ„)
4342rehalfcld 12460 . . . . . . . . . . 11 ((๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โ†’ (๐‘ / 2) โˆˆ โ„)
44 letr 11309 . . . . . . . . . . 11 ((๐‘˜ โˆˆ โ„ โˆง (๐‘˜ + 1) โˆˆ โ„ โˆง (๐‘ / 2) โˆˆ โ„) โ†’ ((๐‘˜ โ‰ค (๐‘˜ + 1) โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ ๐‘˜ โ‰ค (๐‘ / 2)))
4537, 40, 43, 44syl3anc 1368 . . . . . . . . . 10 ((๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โ†’ ((๐‘˜ โ‰ค (๐‘˜ + 1) โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ ๐‘˜ โ‰ค (๐‘ / 2)))
4638, 45mpand 692 . . . . . . . . 9 ((๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โ†’ ((๐‘˜ + 1) โ‰ค (๐‘ / 2) โ†’ ๐‘˜ โ‰ค (๐‘ / 2)))
4746imim1d 82 . . . . . . . 8 ((๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โ†’ ((๐‘˜ โ‰ค (๐‘ / 2) โ†’ (๐‘C๐ด) โ‰ค (๐‘C๐‘˜)) โ†’ ((๐‘˜ + 1) โ‰ค (๐‘ / 2) โ†’ (๐‘C๐ด) โ‰ค (๐‘C๐‘˜))))
48 eluznn0 12902 . . . . . . . . . . . . 13 ((๐ด โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐ด)) โ†’ ๐‘˜ โˆˆ โ„•0)
49413ad2ant2 1131 . . . . . . . . . . . . . . . . 17 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ ๐‘ โˆˆ โ„)
50 nn0re 12482 . . . . . . . . . . . . . . . . . 18 (๐‘˜ โˆˆ โ„•0 โ†’ ๐‘˜ โˆˆ โ„)
51503ad2ant1 1130 . . . . . . . . . . . . . . . . 17 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ ๐‘˜ โˆˆ โ„)
52 nn0p1nn 12512 . . . . . . . . . . . . . . . . . . . 20 (๐‘˜ โˆˆ โ„•0 โ†’ (๐‘˜ + 1) โˆˆ โ„•)
53523ad2ant1 1130 . . . . . . . . . . . . . . . . . . 19 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (๐‘˜ + 1) โˆˆ โ„•)
5453nnnn0d 12533 . . . . . . . . . . . . . . . . . 18 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (๐‘˜ + 1) โˆˆ โ„•0)
5554nn0red 12534 . . . . . . . . . . . . . . . . 17 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (๐‘˜ + 1) โˆˆ โ„)
5653nncnd 12229 . . . . . . . . . . . . . . . . . . 19 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (๐‘˜ + 1) โˆˆ โ„‚)
57562timesd 12456 . . . . . . . . . . . . . . . . . 18 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (2 ยท (๐‘˜ + 1)) = ((๐‘˜ + 1) + (๐‘˜ + 1)))
58 simp3 1135 . . . . . . . . . . . . . . . . . . 19 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (๐‘˜ + 1) โ‰ค (๐‘ / 2))
59 2re 12287 . . . . . . . . . . . . . . . . . . . . . 22 2 โˆˆ โ„
60 2pos 12316 . . . . . . . . . . . . . . . . . . . . . 22 0 < 2
6159, 60pm3.2i 470 . . . . . . . . . . . . . . . . . . . . 21 (2 โˆˆ โ„ โˆง 0 < 2)
6261a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (2 โˆˆ โ„ โˆง 0 < 2))
63 lemuldiv2 12096 . . . . . . . . . . . . . . . . . . . 20 (((๐‘˜ + 1) โˆˆ โ„ โˆง ๐‘ โˆˆ โ„ โˆง (2 โˆˆ โ„ โˆง 0 < 2)) โ†’ ((2 ยท (๐‘˜ + 1)) โ‰ค ๐‘ โ†” (๐‘˜ + 1) โ‰ค (๐‘ / 2)))
6455, 49, 62, 63syl3anc 1368 . . . . . . . . . . . . . . . . . . 19 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ ((2 ยท (๐‘˜ + 1)) โ‰ค ๐‘ โ†” (๐‘˜ + 1) โ‰ค (๐‘ / 2)))
6558, 64mpbird 257 . . . . . . . . . . . . . . . . . 18 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (2 ยท (๐‘˜ + 1)) โ‰ค ๐‘)
6657, 65eqbrtrrd 5165 . . . . . . . . . . . . . . . . 17 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ ((๐‘˜ + 1) + (๐‘˜ + 1)) โ‰ค ๐‘)
6751lep1d 12146 . . . . . . . . . . . . . . . . 17 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ ๐‘˜ โ‰ค (๐‘˜ + 1))
6849, 51, 55, 55, 66, 67lesub3d 11833 . . . . . . . . . . . . . . . 16 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (๐‘˜ + 1) โ‰ค (๐‘ โˆ’ ๐‘˜))
69 nnre 12220 . . . . . . . . . . . . . . . . . . 19 ((๐‘˜ + 1) โˆˆ โ„• โ†’ (๐‘˜ + 1) โˆˆ โ„)
70 nngt0 12244 . . . . . . . . . . . . . . . . . . 19 ((๐‘˜ + 1) โˆˆ โ„• โ†’ 0 < (๐‘˜ + 1))
7169, 70jca 511 . . . . . . . . . . . . . . . . . 18 ((๐‘˜ + 1) โˆˆ โ„• โ†’ ((๐‘˜ + 1) โˆˆ โ„ โˆง 0 < (๐‘˜ + 1)))
7253, 71syl 17 . . . . . . . . . . . . . . . . 17 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ ((๐‘˜ + 1) โˆˆ โ„ โˆง 0 < (๐‘˜ + 1)))
73 nn0z 12584 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ โˆˆ โ„•0 โ†’ ๐‘ โˆˆ โ„ค)
74733ad2ant2 1131 . . . . . . . . . . . . . . . . . . . 20 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ ๐‘ โˆˆ โ„ค)
75 nn0z 12584 . . . . . . . . . . . . . . . . . . . . 21 (๐‘˜ โˆˆ โ„•0 โ†’ ๐‘˜ โˆˆ โ„ค)
76753ad2ant1 1130 . . . . . . . . . . . . . . . . . . . 20 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ ๐‘˜ โˆˆ โ„ค)
7774, 76zsubcld 12672 . . . . . . . . . . . . . . . . . . 19 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (๐‘ โˆ’ ๐‘˜) โˆˆ โ„ค)
7849rehalfcld 12460 . . . . . . . . . . . . . . . . . . . . 21 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (๐‘ / 2) โˆˆ โ„)
7949, 59jctir 520 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (๐‘ โˆˆ โ„ โˆง 2 โˆˆ โ„))
80 nn0ge0 12498 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐‘ โˆˆ โ„•0 โ†’ 0 โ‰ค ๐‘)
81803ad2ant2 1131 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ 0 โ‰ค ๐‘)
82 1le2 12422 . . . . . . . . . . . . . . . . . . . . . . . 24 1 โ‰ค 2
8381, 82jctir 520 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (0 โ‰ค ๐‘ โˆง 1 โ‰ค 2))
84 lemulge12 12078 . . . . . . . . . . . . . . . . . . . . . . 23 (((๐‘ โˆˆ โ„ โˆง 2 โˆˆ โ„) โˆง (0 โ‰ค ๐‘ โˆง 1 โ‰ค 2)) โ†’ ๐‘ โ‰ค (2 ยท ๐‘))
8579, 83, 84syl2anc 583 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ ๐‘ โ‰ค (2 ยท ๐‘))
86 ledivmul 12091 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘ โˆˆ โ„ โˆง ๐‘ โˆˆ โ„ โˆง (2 โˆˆ โ„ โˆง 0 < 2)) โ†’ ((๐‘ / 2) โ‰ค ๐‘ โ†” ๐‘ โ‰ค (2 ยท ๐‘)))
8749, 49, 62, 86syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ ((๐‘ / 2) โ‰ค ๐‘ โ†” ๐‘ โ‰ค (2 ยท ๐‘)))
8885, 87mpbird 257 . . . . . . . . . . . . . . . . . . . . 21 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (๐‘ / 2) โ‰ค ๐‘)
8955, 78, 49, 58, 88letrd 11372 . . . . . . . . . . . . . . . . . . . 20 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (๐‘˜ + 1) โ‰ค ๐‘)
90 1red 11216 . . . . . . . . . . . . . . . . . . . . 21 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ 1 โˆˆ โ„)
9151, 90, 49leaddsub2d 11817 . . . . . . . . . . . . . . . . . . . 20 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ ((๐‘˜ + 1) โ‰ค ๐‘ โ†” 1 โ‰ค (๐‘ โˆ’ ๐‘˜)))
9289, 91mpbid 231 . . . . . . . . . . . . . . . . . . 19 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ 1 โ‰ค (๐‘ โˆ’ ๐‘˜))
93 elnnz1 12589 . . . . . . . . . . . . . . . . . . 19 ((๐‘ โˆ’ ๐‘˜) โˆˆ โ„• โ†” ((๐‘ โˆ’ ๐‘˜) โˆˆ โ„ค โˆง 1 โ‰ค (๐‘ โˆ’ ๐‘˜)))
9477, 92, 93sylanbrc 582 . . . . . . . . . . . . . . . . . 18 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (๐‘ โˆ’ ๐‘˜) โˆˆ โ„•)
95 nnre 12220 . . . . . . . . . . . . . . . . . . 19 ((๐‘ โˆ’ ๐‘˜) โˆˆ โ„• โ†’ (๐‘ โˆ’ ๐‘˜) โˆˆ โ„)
96 nngt0 12244 . . . . . . . . . . . . . . . . . . 19 ((๐‘ โˆ’ ๐‘˜) โˆˆ โ„• โ†’ 0 < (๐‘ โˆ’ ๐‘˜))
9795, 96jca 511 . . . . . . . . . . . . . . . . . 18 ((๐‘ โˆ’ ๐‘˜) โˆˆ โ„• โ†’ ((๐‘ โˆ’ ๐‘˜) โˆˆ โ„ โˆง 0 < (๐‘ โˆ’ ๐‘˜)))
9894, 97syl 17 . . . . . . . . . . . . . . . . 17 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ ((๐‘ โˆ’ ๐‘˜) โˆˆ โ„ โˆง 0 < (๐‘ โˆ’ ๐‘˜)))
99 faccl 14246 . . . . . . . . . . . . . . . . . . . 20 (๐‘ โˆˆ โ„•0 โ†’ (!โ€˜๐‘) โˆˆ โ„•)
100993ad2ant2 1131 . . . . . . . . . . . . . . . . . . 19 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (!โ€˜๐‘) โˆˆ โ„•)
101 nnm1nn0 12514 . . . . . . . . . . . . . . . . . . . . 21 ((๐‘ โˆ’ ๐‘˜) โˆˆ โ„• โ†’ ((๐‘ โˆ’ ๐‘˜) โˆ’ 1) โˆˆ โ„•0)
102 faccl 14246 . . . . . . . . . . . . . . . . . . . . 21 (((๐‘ โˆ’ ๐‘˜) โˆ’ 1) โˆˆ โ„•0 โ†’ (!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) โˆˆ โ„•)
10394, 101, 1023syl 18 . . . . . . . . . . . . . . . . . . . 20 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) โˆˆ โ„•)
104 faccl 14246 . . . . . . . . . . . . . . . . . . . . 21 (๐‘˜ โˆˆ โ„•0 โ†’ (!โ€˜๐‘˜) โˆˆ โ„•)
1051043ad2ant1 1130 . . . . . . . . . . . . . . . . . . . 20 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (!โ€˜๐‘˜) โˆˆ โ„•)
106103, 105nnmulcld 12266 . . . . . . . . . . . . . . . . . . 19 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ ((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (!โ€˜๐‘˜)) โˆˆ โ„•)
107 nnrp 12988 . . . . . . . . . . . . . . . . . . . 20 ((!โ€˜๐‘) โˆˆ โ„• โ†’ (!โ€˜๐‘) โˆˆ โ„+)
108 nnrp 12988 . . . . . . . . . . . . . . . . . . . 20 (((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (!โ€˜๐‘˜)) โˆˆ โ„• โ†’ ((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (!โ€˜๐‘˜)) โˆˆ โ„+)
109 rpdivcl 13002 . . . . . . . . . . . . . . . . . . . 20 (((!โ€˜๐‘) โˆˆ โ„+ โˆง ((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (!โ€˜๐‘˜)) โˆˆ โ„+) โ†’ ((!โ€˜๐‘) / ((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (!โ€˜๐‘˜))) โˆˆ โ„+)
110107, 108, 109syl2an 595 . . . . . . . . . . . . . . . . . . 19 (((!โ€˜๐‘) โˆˆ โ„• โˆง ((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (!โ€˜๐‘˜)) โˆˆ โ„•) โ†’ ((!โ€˜๐‘) / ((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (!โ€˜๐‘˜))) โˆˆ โ„+)
111100, 106, 110syl2anc 583 . . . . . . . . . . . . . . . . . 18 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ ((!โ€˜๐‘) / ((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (!โ€˜๐‘˜))) โˆˆ โ„+)
112111rpregt0d 13025 . . . . . . . . . . . . . . . . 17 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (((!โ€˜๐‘) / ((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (!โ€˜๐‘˜))) โˆˆ โ„ โˆง 0 < ((!โ€˜๐‘) / ((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (!โ€˜๐‘˜)))))
113 lediv2 12105 . . . . . . . . . . . . . . . . 17 ((((๐‘˜ + 1) โˆˆ โ„ โˆง 0 < (๐‘˜ + 1)) โˆง ((๐‘ โˆ’ ๐‘˜) โˆˆ โ„ โˆง 0 < (๐‘ โˆ’ ๐‘˜)) โˆง (((!โ€˜๐‘) / ((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (!โ€˜๐‘˜))) โˆˆ โ„ โˆง 0 < ((!โ€˜๐‘) / ((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (!โ€˜๐‘˜))))) โ†’ ((๐‘˜ + 1) โ‰ค (๐‘ โˆ’ ๐‘˜) โ†” (((!โ€˜๐‘) / ((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (!โ€˜๐‘˜))) / (๐‘ โˆ’ ๐‘˜)) โ‰ค (((!โ€˜๐‘) / ((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (!โ€˜๐‘˜))) / (๐‘˜ + 1))))
11472, 98, 112, 113syl3anc 1368 . . . . . . . . . . . . . . . 16 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ ((๐‘˜ + 1) โ‰ค (๐‘ โˆ’ ๐‘˜) โ†” (((!โ€˜๐‘) / ((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (!โ€˜๐‘˜))) / (๐‘ โˆ’ ๐‘˜)) โ‰ค (((!โ€˜๐‘) / ((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (!โ€˜๐‘˜))) / (๐‘˜ + 1))))
11568, 114mpbid 231 . . . . . . . . . . . . . . 15 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (((!โ€˜๐‘) / ((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (!โ€˜๐‘˜))) / (๐‘ โˆ’ ๐‘˜)) โ‰ค (((!โ€˜๐‘) / ((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (!โ€˜๐‘˜))) / (๐‘˜ + 1)))
116 facnn2 14245 . . . . . . . . . . . . . . . . . . . 20 ((๐‘ โˆ’ ๐‘˜) โˆˆ โ„• โ†’ (!โ€˜(๐‘ โˆ’ ๐‘˜)) = ((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (๐‘ โˆ’ ๐‘˜)))
11794, 116syl 17 . . . . . . . . . . . . . . . . . . 19 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (!โ€˜(๐‘ โˆ’ ๐‘˜)) = ((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (๐‘ โˆ’ ๐‘˜)))
118117oveq1d 7419 . . . . . . . . . . . . . . . . . 18 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ ((!โ€˜(๐‘ โˆ’ ๐‘˜)) ยท (!โ€˜๐‘˜)) = (((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (๐‘ โˆ’ ๐‘˜)) ยท (!โ€˜๐‘˜)))
119103nncnd 12229 . . . . . . . . . . . . . . . . . . 19 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) โˆˆ โ„‚)
120105nncnd 12229 . . . . . . . . . . . . . . . . . . 19 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (!โ€˜๐‘˜) โˆˆ โ„‚)
12177zcnd 12668 . . . . . . . . . . . . . . . . . . 19 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (๐‘ โˆ’ ๐‘˜) โˆˆ โ„‚)
122119, 120, 121mul32d 11425 . . . . . . . . . . . . . . . . . 18 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (!โ€˜๐‘˜)) ยท (๐‘ โˆ’ ๐‘˜)) = (((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (๐‘ โˆ’ ๐‘˜)) ยท (!โ€˜๐‘˜)))
123118, 122eqtr4d 2769 . . . . . . . . . . . . . . . . 17 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ ((!โ€˜(๐‘ โˆ’ ๐‘˜)) ยท (!โ€˜๐‘˜)) = (((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (!โ€˜๐‘˜)) ยท (๐‘ โˆ’ ๐‘˜)))
124123oveq2d 7420 . . . . . . . . . . . . . . . 16 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ ((!โ€˜๐‘) / ((!โ€˜(๐‘ โˆ’ ๐‘˜)) ยท (!โ€˜๐‘˜))) = ((!โ€˜๐‘) / (((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (!โ€˜๐‘˜)) ยท (๐‘ โˆ’ ๐‘˜))))
125 0zd 12571 . . . . . . . . . . . . . . . . . 18 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ 0 โˆˆ โ„ค)
126 nn0ge0 12498 . . . . . . . . . . . . . . . . . . 19 (๐‘˜ โˆˆ โ„•0 โ†’ 0 โ‰ค ๐‘˜)
1271263ad2ant1 1130 . . . . . . . . . . . . . . . . . 18 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ 0 โ‰ค ๐‘˜)
12851, 55, 49, 67, 89letrd 11372 . . . . . . . . . . . . . . . . . 18 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ ๐‘˜ โ‰ค ๐‘)
129125, 74, 76, 127, 128elfzd 13495 . . . . . . . . . . . . . . . . 17 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ ๐‘˜ โˆˆ (0...๐‘))
130 bcval2 14268 . . . . . . . . . . . . . . . . 17 (๐‘˜ โˆˆ (0...๐‘) โ†’ (๐‘C๐‘˜) = ((!โ€˜๐‘) / ((!โ€˜(๐‘ โˆ’ ๐‘˜)) ยท (!โ€˜๐‘˜))))
131129, 130syl 17 . . . . . . . . . . . . . . . 16 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (๐‘C๐‘˜) = ((!โ€˜๐‘) / ((!โ€˜(๐‘ โˆ’ ๐‘˜)) ยท (!โ€˜๐‘˜))))
132100nncnd 12229 . . . . . . . . . . . . . . . . 17 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (!โ€˜๐‘) โˆˆ โ„‚)
133106nncnd 12229 . . . . . . . . . . . . . . . . 17 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ ((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (!โ€˜๐‘˜)) โˆˆ โ„‚)
134106nnne0d 12263 . . . . . . . . . . . . . . . . 17 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ ((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (!โ€˜๐‘˜)) โ‰  0)
13594nnne0d 12263 . . . . . . . . . . . . . . . . 17 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (๐‘ โˆ’ ๐‘˜) โ‰  0)
136132, 133, 121, 134, 135divdiv1d 12022 . . . . . . . . . . . . . . . 16 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (((!โ€˜๐‘) / ((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (!โ€˜๐‘˜))) / (๐‘ โˆ’ ๐‘˜)) = ((!โ€˜๐‘) / (((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (!โ€˜๐‘˜)) ยท (๐‘ โˆ’ ๐‘˜))))
137124, 131, 1363eqtr4d 2776 . . . . . . . . . . . . . . 15 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (๐‘C๐‘˜) = (((!โ€˜๐‘) / ((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (!โ€˜๐‘˜))) / (๐‘ โˆ’ ๐‘˜)))
138 nn0cn 12483 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ โˆˆ โ„•0 โ†’ ๐‘ โˆˆ โ„‚)
1391383ad2ant2 1131 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ ๐‘ โˆˆ โ„‚)
140 nn0cn 12483 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘˜ โˆˆ โ„•0 โ†’ ๐‘˜ โˆˆ โ„‚)
1411403ad2ant1 1130 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ ๐‘˜ โˆˆ โ„‚)
142 1cnd 11210 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ 1 โˆˆ โ„‚)
143139, 141, 142subsub4d 11603 . . . . . . . . . . . . . . . . . . . . 21 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ ((๐‘ โˆ’ ๐‘˜) โˆ’ 1) = (๐‘ โˆ’ (๐‘˜ + 1)))
144143eqcomd 2732 . . . . . . . . . . . . . . . . . . . 20 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (๐‘ โˆ’ (๐‘˜ + 1)) = ((๐‘ โˆ’ ๐‘˜) โˆ’ 1))
145144fveq2d 6888 . . . . . . . . . . . . . . . . . . 19 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (!โ€˜(๐‘ โˆ’ (๐‘˜ + 1))) = (!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)))
146 facp1 14241 . . . . . . . . . . . . . . . . . . . 20 (๐‘˜ โˆˆ โ„•0 โ†’ (!โ€˜(๐‘˜ + 1)) = ((!โ€˜๐‘˜) ยท (๐‘˜ + 1)))
1471463ad2ant1 1130 . . . . . . . . . . . . . . . . . . 19 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (!โ€˜(๐‘˜ + 1)) = ((!โ€˜๐‘˜) ยท (๐‘˜ + 1)))
148145, 147oveq12d 7422 . . . . . . . . . . . . . . . . . 18 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ ((!โ€˜(๐‘ โˆ’ (๐‘˜ + 1))) ยท (!โ€˜(๐‘˜ + 1))) = ((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท ((!โ€˜๐‘˜) ยท (๐‘˜ + 1))))
149119, 120, 56mulassd 11238 . . . . . . . . . . . . . . . . . 18 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (!โ€˜๐‘˜)) ยท (๐‘˜ + 1)) = ((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท ((!โ€˜๐‘˜) ยท (๐‘˜ + 1))))
150148, 149eqtr4d 2769 . . . . . . . . . . . . . . . . 17 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ ((!โ€˜(๐‘ โˆ’ (๐‘˜ + 1))) ยท (!โ€˜(๐‘˜ + 1))) = (((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (!โ€˜๐‘˜)) ยท (๐‘˜ + 1)))
151150oveq2d 7420 . . . . . . . . . . . . . . . 16 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ ((!โ€˜๐‘) / ((!โ€˜(๐‘ โˆ’ (๐‘˜ + 1))) ยท (!โ€˜(๐‘˜ + 1)))) = ((!โ€˜๐‘) / (((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (!โ€˜๐‘˜)) ยท (๐‘˜ + 1))))
15253nnzd 12586 . . . . . . . . . . . . . . . . . 18 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (๐‘˜ + 1) โˆˆ โ„ค)
15354nn0ge0d 12536 . . . . . . . . . . . . . . . . . 18 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ 0 โ‰ค (๐‘˜ + 1))
154125, 74, 152, 153, 89elfzd 13495 . . . . . . . . . . . . . . . . 17 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (๐‘˜ + 1) โˆˆ (0...๐‘))
155 bcval2 14268 . . . . . . . . . . . . . . . . 17 ((๐‘˜ + 1) โˆˆ (0...๐‘) โ†’ (๐‘C(๐‘˜ + 1)) = ((!โ€˜๐‘) / ((!โ€˜(๐‘ โˆ’ (๐‘˜ + 1))) ยท (!โ€˜(๐‘˜ + 1)))))
156154, 155syl 17 . . . . . . . . . . . . . . . 16 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (๐‘C(๐‘˜ + 1)) = ((!โ€˜๐‘) / ((!โ€˜(๐‘ โˆ’ (๐‘˜ + 1))) ยท (!โ€˜(๐‘˜ + 1)))))
15753nnne0d 12263 . . . . . . . . . . . . . . . . 17 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (๐‘˜ + 1) โ‰  0)
158132, 133, 56, 134, 157divdiv1d 12022 . . . . . . . . . . . . . . . 16 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (((!โ€˜๐‘) / ((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (!โ€˜๐‘˜))) / (๐‘˜ + 1)) = ((!โ€˜๐‘) / (((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (!โ€˜๐‘˜)) ยท (๐‘˜ + 1))))
159151, 156, 1583eqtr4d 2776 . . . . . . . . . . . . . . 15 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (๐‘C(๐‘˜ + 1)) = (((!โ€˜๐‘) / ((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (!โ€˜๐‘˜))) / (๐‘˜ + 1)))
160115, 137, 1593brtr4d 5173 . . . . . . . . . . . . . 14 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (๐‘C๐‘˜) โ‰ค (๐‘C(๐‘˜ + 1)))
1611603exp 1116 . . . . . . . . . . . . 13 (๐‘˜ โˆˆ โ„•0 โ†’ (๐‘ โˆˆ โ„•0 โ†’ ((๐‘˜ + 1) โ‰ค (๐‘ / 2) โ†’ (๐‘C๐‘˜) โ‰ค (๐‘C(๐‘˜ + 1)))))
16248, 161syl 17 . . . . . . . . . . . 12 ((๐ด โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐ด)) โ†’ (๐‘ โˆˆ โ„•0 โ†’ ((๐‘˜ + 1) โ‰ค (๐‘ / 2) โ†’ (๐‘C๐‘˜) โ‰ค (๐‘C(๐‘˜ + 1)))))
1631623impia 1114 . . . . . . . . . . 11 ((๐ด โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐‘ โˆˆ โ„•0) โ†’ ((๐‘˜ + 1) โ‰ค (๐‘ / 2) โ†’ (๐‘C๐‘˜) โ‰ค (๐‘C(๐‘˜ + 1))))
1641633coml 1124 . . . . . . . . . 10 ((๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โ†’ ((๐‘˜ + 1) โ‰ค (๐‘ / 2) โ†’ (๐‘C๐‘˜) โ‰ค (๐‘C(๐‘˜ + 1))))
165 simp2 1134 . . . . . . . . . . . . . 14 ((๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โ†’ ๐‘ โˆˆ โ„•0)
166 nn0z 12584 . . . . . . . . . . . . . . 15 (๐ด โˆˆ โ„•0 โ†’ ๐ด โˆˆ โ„ค)
1671663ad2ant3 1132 . . . . . . . . . . . . . 14 ((๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โ†’ ๐ด โˆˆ โ„ค)
168165, 167, 29syl2anc 583 . . . . . . . . . . . . 13 ((๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โ†’ (๐‘C๐ด) โˆˆ โ„•0)
169168nn0red 12534 . . . . . . . . . . . 12 ((๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โ†’ (๐‘C๐ด) โˆˆ โ„)
170 bccl 14285 . . . . . . . . . . . . . 14 ((๐‘ โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ โ„ค) โ†’ (๐‘C๐‘˜) โˆˆ โ„•0)
171165, 36, 170syl2anc 583 . . . . . . . . . . . . 13 ((๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โ†’ (๐‘C๐‘˜) โˆˆ โ„•0)
172171nn0red 12534 . . . . . . . . . . . 12 ((๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โ†’ (๐‘C๐‘˜) โˆˆ โ„)
17336peano2zd 12670 . . . . . . . . . . . . . 14 ((๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โ†’ (๐‘˜ + 1) โˆˆ โ„ค)
174 bccl 14285 . . . . . . . . . . . . . 14 ((๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โˆˆ โ„ค) โ†’ (๐‘C(๐‘˜ + 1)) โˆˆ โ„•0)
175165, 173, 174syl2anc 583 . . . . . . . . . . . . 13 ((๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โ†’ (๐‘C(๐‘˜ + 1)) โˆˆ โ„•0)
176175nn0red 12534 . . . . . . . . . . . 12 ((๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โ†’ (๐‘C(๐‘˜ + 1)) โˆˆ โ„)
177 letr 11309 . . . . . . . . . . . 12 (((๐‘C๐ด) โˆˆ โ„ โˆง (๐‘C๐‘˜) โˆˆ โ„ โˆง (๐‘C(๐‘˜ + 1)) โˆˆ โ„) โ†’ (((๐‘C๐ด) โ‰ค (๐‘C๐‘˜) โˆง (๐‘C๐‘˜) โ‰ค (๐‘C(๐‘˜ + 1))) โ†’ (๐‘C๐ด) โ‰ค (๐‘C(๐‘˜ + 1))))
178169, 172, 176, 177syl3anc 1368 . . . . . . . . . . 11 ((๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โ†’ (((๐‘C๐ด) โ‰ค (๐‘C๐‘˜) โˆง (๐‘C๐‘˜) โ‰ค (๐‘C(๐‘˜ + 1))) โ†’ (๐‘C๐ด) โ‰ค (๐‘C(๐‘˜ + 1))))
179178expcomd 416 . . . . . . . . . 10 ((๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โ†’ ((๐‘C๐‘˜) โ‰ค (๐‘C(๐‘˜ + 1)) โ†’ ((๐‘C๐ด) โ‰ค (๐‘C๐‘˜) โ†’ (๐‘C๐ด) โ‰ค (๐‘C(๐‘˜ + 1)))))
180164, 179syld 47 . . . . . . . . 9 ((๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โ†’ ((๐‘˜ + 1) โ‰ค (๐‘ / 2) โ†’ ((๐‘C๐ด) โ‰ค (๐‘C๐‘˜) โ†’ (๐‘C๐ด) โ‰ค (๐‘C(๐‘˜ + 1)))))
181180a2d 29 . . . . . . . 8 ((๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โ†’ (((๐‘˜ + 1) โ‰ค (๐‘ / 2) โ†’ (๐‘C๐ด) โ‰ค (๐‘C๐‘˜)) โ†’ ((๐‘˜ + 1) โ‰ค (๐‘ / 2) โ†’ (๐‘C๐ด) โ‰ค (๐‘C(๐‘˜ + 1)))))
18247, 181syld 47 . . . . . . 7 ((๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โ†’ ((๐‘˜ โ‰ค (๐‘ / 2) โ†’ (๐‘C๐ด) โ‰ค (๐‘C๐‘˜)) โ†’ ((๐‘˜ + 1) โ‰ค (๐‘ / 2) โ†’ (๐‘C๐ด) โ‰ค (๐‘C(๐‘˜ + 1)))))
1831823expib 1119 . . . . . 6 (๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐ด) โ†’ ((๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โ†’ ((๐‘˜ โ‰ค (๐‘ / 2) โ†’ (๐‘C๐ด) โ‰ค (๐‘C๐‘˜)) โ†’ ((๐‘˜ + 1) โ‰ค (๐‘ / 2) โ†’ (๐‘C๐ด) โ‰ค (๐‘C(๐‘˜ + 1))))))
184183a2d 29 . . . . 5 (๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐ด) โ†’ (((๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โ†’ (๐‘˜ โ‰ค (๐‘ / 2) โ†’ (๐‘C๐ด) โ‰ค (๐‘C๐‘˜))) โ†’ ((๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โ†’ ((๐‘˜ + 1) โ‰ค (๐‘ / 2) โ†’ (๐‘C๐ด) โ‰ค (๐‘C(๐‘˜ + 1))))))
18513, 18, 23, 28, 34, 184uzind4 12891 . . . 4 (๐ต โˆˆ (โ„คโ‰ฅโ€˜๐ด) โ†’ ((๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โ†’ (๐ต โ‰ค (๐‘ / 2) โ†’ (๐‘C๐ด) โ‰ค (๐‘C๐ต))))
1861853imp 1108 . . 3 ((๐ต โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง (๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โˆง ๐ต โ‰ค (๐‘ / 2)) โ†’ (๐‘C๐ด) โ‰ค (๐‘C๐ต))
1871, 2, 7, 8, 186syl121anc 1372 . 2 (((๐‘ โˆˆ โ„•0 โˆง ๐ต โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐ต โ‰ค (๐‘ / 2)) โˆง 0 โ‰ค ๐ด) โ†’ (๐‘C๐ด) โ‰ค (๐‘C๐ต))
188 simpl1 1188 . . . 4 (((๐‘ โˆˆ โ„•0 โˆง ๐ต โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐ต โ‰ค (๐‘ / 2)) โˆง ๐ด < 0) โ†’ ๐‘ โˆˆ โ„•0)
1894adantr 480 . . . 4 (((๐‘ โˆˆ โ„•0 โˆง ๐ต โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐ต โ‰ค (๐‘ / 2)) โˆง ๐ด < 0) โ†’ ๐ด โˆˆ โ„ค)
190 animorrl 977 . . . 4 (((๐‘ โˆˆ โ„•0 โˆง ๐ต โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐ต โ‰ค (๐‘ / 2)) โˆง ๐ด < 0) โ†’ (๐ด < 0 โˆจ ๐‘ < ๐ด))
191 bcval4 14270 . . . 4 ((๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„ค โˆง (๐ด < 0 โˆจ ๐‘ < ๐ด)) โ†’ (๐‘C๐ด) = 0)
192188, 189, 190, 191syl3anc 1368 . . 3 (((๐‘ โˆˆ โ„•0 โˆง ๐ต โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐ต โ‰ค (๐‘ / 2)) โˆง ๐ด < 0) โ†’ (๐‘C๐ด) = 0)
193 simpl2 1189 . . . . . 6 (((๐‘ โˆˆ โ„•0 โˆง ๐ต โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐ต โ‰ค (๐‘ / 2)) โˆง ๐ด < 0) โ†’ ๐ต โˆˆ (โ„คโ‰ฅโ€˜๐ด))
194 eluzelz 12833 . . . . . 6 (๐ต โˆˆ (โ„คโ‰ฅโ€˜๐ด) โ†’ ๐ต โˆˆ โ„ค)
195193, 194syl 17 . . . . 5 (((๐‘ โˆˆ โ„•0 โˆง ๐ต โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐ต โ‰ค (๐‘ / 2)) โˆง ๐ด < 0) โ†’ ๐ต โˆˆ โ„ค)
196 bccl 14285 . . . . 5 ((๐‘ โˆˆ โ„•0 โˆง ๐ต โˆˆ โ„ค) โ†’ (๐‘C๐ต) โˆˆ โ„•0)
197188, 195, 196syl2anc 583 . . . 4 (((๐‘ โˆˆ โ„•0 โˆง ๐ต โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐ต โ‰ค (๐‘ / 2)) โˆง ๐ด < 0) โ†’ (๐‘C๐ต) โˆˆ โ„•0)
198197nn0ge0d 12536 . . 3 (((๐‘ โˆˆ โ„•0 โˆง ๐ต โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐ต โ‰ค (๐‘ / 2)) โˆง ๐ด < 0) โ†’ 0 โ‰ค (๐‘C๐ต))
199192, 198eqbrtrd 5163 . 2 (((๐‘ โˆˆ โ„•0 โˆง ๐ต โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐ต โ‰ค (๐‘ / 2)) โˆง ๐ด < 0) โ†’ (๐‘C๐ด) โ‰ค (๐‘C๐ต))
200 0re 11217 . . 3 0 โˆˆ โ„
2014zred 12667 . . 3 ((๐‘ โˆˆ โ„•0 โˆง ๐ต โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐ต โ‰ค (๐‘ / 2)) โ†’ ๐ด โˆˆ โ„)
202 lelttric 11322 . . 3 ((0 โˆˆ โ„ โˆง ๐ด โˆˆ โ„) โ†’ (0 โ‰ค ๐ด โˆจ ๐ด < 0))
203200, 201, 202sylancr 586 . 2 ((๐‘ โˆˆ โ„•0 โˆง ๐ต โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐ต โ‰ค (๐‘ / 2)) โ†’ (0 โ‰ค ๐ด โˆจ ๐ด < 0))
204187, 199, 203mpjaodan 955 1 ((๐‘ โˆˆ โ„•0 โˆง ๐ต โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐ต โ‰ค (๐‘ / 2)) โ†’ (๐‘C๐ด) โ‰ค (๐‘C๐ต))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 395   โˆจ wo 844   โˆง w3a 1084   = wceq 1533   โˆˆ wcel 2098   class class class wbr 5141  โ€˜cfv 6536  (class class class)co 7404  โ„‚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  โ„+crp 12977  ...cfz 13487  !cfa 14236  Ccbc 14265
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-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7721  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
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-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-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-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-er 8702  df-en 8939  df-dom 8940  df-sdom 8941  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-n0 12474  df-z 12560  df-uz 12824  df-rp 12978  df-fz 13488  df-seq 13970  df-fac 14237  df-bc 14266
This theorem is referenced by:  bcmax  27162
  Copyright terms: Public domain W3C validator