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

Theorem bcmono 27228
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 12863 . . . . . 6 (๐ต โˆˆ (โ„คโ‰ฅโ€˜๐ด) โ†’ ๐ด โˆˆ โ„ค)
433ad2ant2 1131 . . . . 5 ((๐‘ โˆˆ โ„•0 โˆง ๐ต โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐ต โ‰ค (๐‘ / 2)) โ†’ ๐ด โˆˆ โ„ค)
54anim1i 613 . . . 4 (((๐‘ โˆˆ โ„•0 โˆง ๐ต โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐ต โ‰ค (๐‘ / 2)) โˆง 0 โ‰ค ๐ด) โ†’ (๐ด โˆˆ โ„ค โˆง 0 โ‰ค ๐ด))
6 elnn0z 12607 . . . 4 (๐ด โˆˆ โ„•0 โ†” (๐ด โˆˆ โ„ค โˆง 0 โ‰ค ๐ด))
75, 6sylibr 233 . . 3 (((๐‘ โˆˆ โ„•0 โˆง ๐ต โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐ต โ‰ค (๐‘ / 2)) โˆง 0 โ‰ค ๐ด) โ†’ ๐ด โˆˆ โ„•0)
8 simpl3 1190 . . 3 (((๐‘ โˆˆ โ„•0 โˆง ๐ต โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐ต โ‰ค (๐‘ / 2)) โˆง 0 โ‰ค ๐ด) โ†’ ๐ต โ‰ค (๐‘ / 2))
9 breq1 5153 . . . . . . 7 (๐‘ฅ = ๐ด โ†’ (๐‘ฅ โ‰ค (๐‘ / 2) โ†” ๐ด โ‰ค (๐‘ / 2)))
10 oveq2 7432 . . . . . . . 8 (๐‘ฅ = ๐ด โ†’ (๐‘C๐‘ฅ) = (๐‘C๐ด))
1110breq2d 5162 . . . . . . 7 (๐‘ฅ = ๐ด โ†’ ((๐‘C๐ด) โ‰ค (๐‘C๐‘ฅ) โ†” (๐‘C๐ด) โ‰ค (๐‘C๐ด)))
129, 11imbi12d 343 . . . . . 6 (๐‘ฅ = ๐ด โ†’ ((๐‘ฅ โ‰ค (๐‘ / 2) โ†’ (๐‘C๐ด) โ‰ค (๐‘C๐‘ฅ)) โ†” (๐ด โ‰ค (๐‘ / 2) โ†’ (๐‘C๐ด) โ‰ค (๐‘C๐ด))))
1312imbi2d 339 . . . . 5 (๐‘ฅ = ๐ด โ†’ (((๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โ†’ (๐‘ฅ โ‰ค (๐‘ / 2) โ†’ (๐‘C๐ด) โ‰ค (๐‘C๐‘ฅ))) โ†” ((๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โ†’ (๐ด โ‰ค (๐‘ / 2) โ†’ (๐‘C๐ด) โ‰ค (๐‘C๐ด)))))
14 breq1 5153 . . . . . . 7 (๐‘ฅ = ๐‘˜ โ†’ (๐‘ฅ โ‰ค (๐‘ / 2) โ†” ๐‘˜ โ‰ค (๐‘ / 2)))
15 oveq2 7432 . . . . . . . 8 (๐‘ฅ = ๐‘˜ โ†’ (๐‘C๐‘ฅ) = (๐‘C๐‘˜))
1615breq2d 5162 . . . . . . 7 (๐‘ฅ = ๐‘˜ โ†’ ((๐‘C๐ด) โ‰ค (๐‘C๐‘ฅ) โ†” (๐‘C๐ด) โ‰ค (๐‘C๐‘˜)))
1714, 16imbi12d 343 . . . . . 6 (๐‘ฅ = ๐‘˜ โ†’ ((๐‘ฅ โ‰ค (๐‘ / 2) โ†’ (๐‘C๐ด) โ‰ค (๐‘C๐‘ฅ)) โ†” (๐‘˜ โ‰ค (๐‘ / 2) โ†’ (๐‘C๐ด) โ‰ค (๐‘C๐‘˜))))
1817imbi2d 339 . . . . 5 (๐‘ฅ = ๐‘˜ โ†’ (((๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โ†’ (๐‘ฅ โ‰ค (๐‘ / 2) โ†’ (๐‘C๐ด) โ‰ค (๐‘C๐‘ฅ))) โ†” ((๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โ†’ (๐‘˜ โ‰ค (๐‘ / 2) โ†’ (๐‘C๐ด) โ‰ค (๐‘C๐‘˜)))))
19 breq1 5153 . . . . . . 7 (๐‘ฅ = (๐‘˜ + 1) โ†’ (๐‘ฅ โ‰ค (๐‘ / 2) โ†” (๐‘˜ + 1) โ‰ค (๐‘ / 2)))
20 oveq2 7432 . . . . . . . 8 (๐‘ฅ = (๐‘˜ + 1) โ†’ (๐‘C๐‘ฅ) = (๐‘C(๐‘˜ + 1)))
2120breq2d 5162 . . . . . . 7 (๐‘ฅ = (๐‘˜ + 1) โ†’ ((๐‘C๐ด) โ‰ค (๐‘C๐‘ฅ) โ†” (๐‘C๐ด) โ‰ค (๐‘C(๐‘˜ + 1))))
2219, 21imbi12d 343 . . . . . 6 (๐‘ฅ = (๐‘˜ + 1) โ†’ ((๐‘ฅ โ‰ค (๐‘ / 2) โ†’ (๐‘C๐ด) โ‰ค (๐‘C๐‘ฅ)) โ†” ((๐‘˜ + 1) โ‰ค (๐‘ / 2) โ†’ (๐‘C๐ด) โ‰ค (๐‘C(๐‘˜ + 1)))))
2322imbi2d 339 . . . . 5 (๐‘ฅ = (๐‘˜ + 1) โ†’ (((๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โ†’ (๐‘ฅ โ‰ค (๐‘ / 2) โ†’ (๐‘C๐ด) โ‰ค (๐‘C๐‘ฅ))) โ†” ((๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โ†’ ((๐‘˜ + 1) โ‰ค (๐‘ / 2) โ†’ (๐‘C๐ด) โ‰ค (๐‘C(๐‘˜ + 1))))))
24 breq1 5153 . . . . . . 7 (๐‘ฅ = ๐ต โ†’ (๐‘ฅ โ‰ค (๐‘ / 2) โ†” ๐ต โ‰ค (๐‘ / 2)))
25 oveq2 7432 . . . . . . . 8 (๐‘ฅ = ๐ต โ†’ (๐‘C๐‘ฅ) = (๐‘C๐ต))
2625breq2d 5162 . . . . . . 7 (๐‘ฅ = ๐ต โ†’ ((๐‘C๐ด) โ‰ค (๐‘C๐‘ฅ) โ†” (๐‘C๐ด) โ‰ค (๐‘C๐ต)))
2724, 26imbi12d 343 . . . . . 6 (๐‘ฅ = ๐ต โ†’ ((๐‘ฅ โ‰ค (๐‘ / 2) โ†’ (๐‘C๐ด) โ‰ค (๐‘C๐‘ฅ)) โ†” (๐ต โ‰ค (๐‘ / 2) โ†’ (๐‘C๐ด) โ‰ค (๐‘C๐ต))))
2827imbi2d 339 . . . . 5 (๐‘ฅ = ๐ต โ†’ (((๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โ†’ (๐‘ฅ โ‰ค (๐‘ / 2) โ†’ (๐‘C๐ด) โ‰ค (๐‘C๐‘ฅ))) โ†” ((๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โ†’ (๐ต โ‰ค (๐‘ / 2) โ†’ (๐‘C๐ด) โ‰ค (๐‘C๐ต)))))
29 bccl 14319 . . . . . . . . . 10 ((๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„ค) โ†’ (๐‘C๐ด) โˆˆ โ„•0)
3029nn0red 12569 . . . . . . . . 9 ((๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„ค) โ†’ (๐‘C๐ด) โˆˆ โ„)
3130leidd 11816 . . . . . . . 8 ((๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„ค) โ†’ (๐‘C๐ด) โ‰ค (๐‘C๐ด))
3231a1d 25 . . . . . . 7 ((๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„ค) โ†’ (๐ด โ‰ค (๐‘ / 2) โ†’ (๐‘C๐ด) โ‰ค (๐‘C๐ด)))
3332expcom 412 . . . . . 6 (๐ด โˆˆ โ„ค โ†’ (๐‘ โˆˆ โ„•0 โ†’ (๐ด โ‰ค (๐‘ / 2) โ†’ (๐‘C๐ด) โ‰ค (๐‘C๐ด))))
3433adantrd 490 . . . . 5 (๐ด โˆˆ โ„ค โ†’ ((๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โ†’ (๐ด โ‰ค (๐‘ / 2) โ†’ (๐‘C๐ด) โ‰ค (๐‘C๐ด))))
35 eluzelz 12868 . . . . . . . . . . . . 13 (๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐ด) โ†’ ๐‘˜ โˆˆ โ„ค)
36353ad2ant1 1130 . . . . . . . . . . . 12 ((๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โ†’ ๐‘˜ โˆˆ โ„ค)
3736zred 12702 . . . . . . . . . . 11 ((๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โ†’ ๐‘˜ โˆˆ โ„)
3837lep1d 12181 . . . . . . . . . 10 ((๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โ†’ ๐‘˜ โ‰ค (๐‘˜ + 1))
39 peano2re 11423 . . . . . . . . . . . 12 (๐‘˜ โˆˆ โ„ โ†’ (๐‘˜ + 1) โˆˆ โ„)
4037, 39syl 17 . . . . . . . . . . 11 ((๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โ†’ (๐‘˜ + 1) โˆˆ โ„)
41 nn0re 12517 . . . . . . . . . . . . 13 (๐‘ โˆˆ โ„•0 โ†’ ๐‘ โˆˆ โ„)
42413ad2ant2 1131 . . . . . . . . . . . 12 ((๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โ†’ ๐‘ โˆˆ โ„)
4342rehalfcld 12495 . . . . . . . . . . 11 ((๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โ†’ (๐‘ / 2) โˆˆ โ„)
44 letr 11344 . . . . . . . . . . 11 ((๐‘˜ โˆˆ โ„ โˆง (๐‘˜ + 1) โˆˆ โ„ โˆง (๐‘ / 2) โˆˆ โ„) โ†’ ((๐‘˜ โ‰ค (๐‘˜ + 1) โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ ๐‘˜ โ‰ค (๐‘ / 2)))
4537, 40, 43, 44syl3anc 1368 . . . . . . . . . 10 ((๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โ†’ ((๐‘˜ โ‰ค (๐‘˜ + 1) โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ ๐‘˜ โ‰ค (๐‘ / 2)))
4638, 45mpand 693 . . . . . . . . 9 ((๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โ†’ ((๐‘˜ + 1) โ‰ค (๐‘ / 2) โ†’ ๐‘˜ โ‰ค (๐‘ / 2)))
4746imim1d 82 . . . . . . . 8 ((๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โ†’ ((๐‘˜ โ‰ค (๐‘ / 2) โ†’ (๐‘C๐ด) โ‰ค (๐‘C๐‘˜)) โ†’ ((๐‘˜ + 1) โ‰ค (๐‘ / 2) โ†’ (๐‘C๐ด) โ‰ค (๐‘C๐‘˜))))
48 eluznn0 12937 . . . . . . . . . . . . 13 ((๐ด โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐ด)) โ†’ ๐‘˜ โˆˆ โ„•0)
49413ad2ant2 1131 . . . . . . . . . . . . . . . . 17 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ ๐‘ โˆˆ โ„)
50 nn0re 12517 . . . . . . . . . . . . . . . . . 18 (๐‘˜ โˆˆ โ„•0 โ†’ ๐‘˜ โˆˆ โ„)
51503ad2ant1 1130 . . . . . . . . . . . . . . . . 17 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ ๐‘˜ โˆˆ โ„)
52 nn0p1nn 12547 . . . . . . . . . . . . . . . . . . . 20 (๐‘˜ โˆˆ โ„•0 โ†’ (๐‘˜ + 1) โˆˆ โ„•)
53523ad2ant1 1130 . . . . . . . . . . . . . . . . . . 19 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (๐‘˜ + 1) โˆˆ โ„•)
5453nnnn0d 12568 . . . . . . . . . . . . . . . . . 18 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (๐‘˜ + 1) โˆˆ โ„•0)
5554nn0red 12569 . . . . . . . . . . . . . . . . 17 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (๐‘˜ + 1) โˆˆ โ„)
5653nncnd 12264 . . . . . . . . . . . . . . . . . . 19 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (๐‘˜ + 1) โˆˆ โ„‚)
57562timesd 12491 . . . . . . . . . . . . . . . . . 18 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (2 ยท (๐‘˜ + 1)) = ((๐‘˜ + 1) + (๐‘˜ + 1)))
58 simp3 1135 . . . . . . . . . . . . . . . . . . 19 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (๐‘˜ + 1) โ‰ค (๐‘ / 2))
59 2re 12322 . . . . . . . . . . . . . . . . . . . . . 22 2 โˆˆ โ„
60 2pos 12351 . . . . . . . . . . . . . . . . . . . . . 22 0 < 2
6159, 60pm3.2i 469 . . . . . . . . . . . . . . . . . . . . 21 (2 โˆˆ โ„ โˆง 0 < 2)
6261a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (2 โˆˆ โ„ โˆง 0 < 2))
63 lemuldiv2 12131 . . . . . . . . . . . . . . . . . . . 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 256 . . . . . . . . . . . . . . . . . 18 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (2 ยท (๐‘˜ + 1)) โ‰ค ๐‘)
6657, 65eqbrtrrd 5174 . . . . . . . . . . . . . . . . 17 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ ((๐‘˜ + 1) + (๐‘˜ + 1)) โ‰ค ๐‘)
6751lep1d 12181 . . . . . . . . . . . . . . . . 17 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ ๐‘˜ โ‰ค (๐‘˜ + 1))
6849, 51, 55, 55, 66, 67lesub3d 11868 . . . . . . . . . . . . . . . 16 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (๐‘˜ + 1) โ‰ค (๐‘ โˆ’ ๐‘˜))
69 nnre 12255 . . . . . . . . . . . . . . . . . . 19 ((๐‘˜ + 1) โˆˆ โ„• โ†’ (๐‘˜ + 1) โˆˆ โ„)
70 nngt0 12279 . . . . . . . . . . . . . . . . . . 19 ((๐‘˜ + 1) โˆˆ โ„• โ†’ 0 < (๐‘˜ + 1))
7169, 70jca 510 . . . . . . . . . . . . . . . . . 18 ((๐‘˜ + 1) โˆˆ โ„• โ†’ ((๐‘˜ + 1) โˆˆ โ„ โˆง 0 < (๐‘˜ + 1)))
7253, 71syl 17 . . . . . . . . . . . . . . . . 17 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ ((๐‘˜ + 1) โˆˆ โ„ โˆง 0 < (๐‘˜ + 1)))
73 nn0z 12619 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ โˆˆ โ„•0 โ†’ ๐‘ โˆˆ โ„ค)
74733ad2ant2 1131 . . . . . . . . . . . . . . . . . . . 20 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ ๐‘ โˆˆ โ„ค)
75 nn0z 12619 . . . . . . . . . . . . . . . . . . . . 21 (๐‘˜ โˆˆ โ„•0 โ†’ ๐‘˜ โˆˆ โ„ค)
76753ad2ant1 1130 . . . . . . . . . . . . . . . . . . . 20 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ ๐‘˜ โˆˆ โ„ค)
7774, 76zsubcld 12707 . . . . . . . . . . . . . . . . . . 19 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (๐‘ โˆ’ ๐‘˜) โˆˆ โ„ค)
7849rehalfcld 12495 . . . . . . . . . . . . . . . . . . . . 21 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (๐‘ / 2) โˆˆ โ„)
7949, 59jctir 519 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (๐‘ โˆˆ โ„ โˆง 2 โˆˆ โ„))
80 nn0ge0 12533 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐‘ โˆˆ โ„•0 โ†’ 0 โ‰ค ๐‘)
81803ad2ant2 1131 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ 0 โ‰ค ๐‘)
82 1le2 12457 . . . . . . . . . . . . . . . . . . . . . . . 24 1 โ‰ค 2
8381, 82jctir 519 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (0 โ‰ค ๐‘ โˆง 1 โ‰ค 2))
84 lemulge12 12113 . . . . . . . . . . . . . . . . . . . . . . 23 (((๐‘ โˆˆ โ„ โˆง 2 โˆˆ โ„) โˆง (0 โ‰ค ๐‘ โˆง 1 โ‰ค 2)) โ†’ ๐‘ โ‰ค (2 ยท ๐‘))
8579, 83, 84syl2anc 582 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ ๐‘ โ‰ค (2 ยท ๐‘))
86 ledivmul 12126 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘ โˆˆ โ„ โˆง ๐‘ โˆˆ โ„ โˆง (2 โˆˆ โ„ โˆง 0 < 2)) โ†’ ((๐‘ / 2) โ‰ค ๐‘ โ†” ๐‘ โ‰ค (2 ยท ๐‘)))
8749, 49, 62, 86syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ ((๐‘ / 2) โ‰ค ๐‘ โ†” ๐‘ โ‰ค (2 ยท ๐‘)))
8885, 87mpbird 256 . . . . . . . . . . . . . . . . . . . . 21 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (๐‘ / 2) โ‰ค ๐‘)
8955, 78, 49, 58, 88letrd 11407 . . . . . . . . . . . . . . . . . . . 20 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (๐‘˜ + 1) โ‰ค ๐‘)
90 1red 11251 . . . . . . . . . . . . . . . . . . . . 21 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ 1 โˆˆ โ„)
9151, 90, 49leaddsub2d 11852 . . . . . . . . . . . . . . . . . . . 20 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ ((๐‘˜ + 1) โ‰ค ๐‘ โ†” 1 โ‰ค (๐‘ โˆ’ ๐‘˜)))
9289, 91mpbid 231 . . . . . . . . . . . . . . . . . . 19 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ 1 โ‰ค (๐‘ โˆ’ ๐‘˜))
93 elnnz1 12624 . . . . . . . . . . . . . . . . . . 19 ((๐‘ โˆ’ ๐‘˜) โˆˆ โ„• โ†” ((๐‘ โˆ’ ๐‘˜) โˆˆ โ„ค โˆง 1 โ‰ค (๐‘ โˆ’ ๐‘˜)))
9477, 92, 93sylanbrc 581 . . . . . . . . . . . . . . . . . 18 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (๐‘ โˆ’ ๐‘˜) โˆˆ โ„•)
95 nnre 12255 . . . . . . . . . . . . . . . . . . 19 ((๐‘ โˆ’ ๐‘˜) โˆˆ โ„• โ†’ (๐‘ โˆ’ ๐‘˜) โˆˆ โ„)
96 nngt0 12279 . . . . . . . . . . . . . . . . . . 19 ((๐‘ โˆ’ ๐‘˜) โˆˆ โ„• โ†’ 0 < (๐‘ โˆ’ ๐‘˜))
9795, 96jca 510 . . . . . . . . . . . . . . . . . 18 ((๐‘ โˆ’ ๐‘˜) โˆˆ โ„• โ†’ ((๐‘ โˆ’ ๐‘˜) โˆˆ โ„ โˆง 0 < (๐‘ โˆ’ ๐‘˜)))
9894, 97syl 17 . . . . . . . . . . . . . . . . 17 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ ((๐‘ โˆ’ ๐‘˜) โˆˆ โ„ โˆง 0 < (๐‘ โˆ’ ๐‘˜)))
99 faccl 14280 . . . . . . . . . . . . . . . . . . . 20 (๐‘ โˆˆ โ„•0 โ†’ (!โ€˜๐‘) โˆˆ โ„•)
100993ad2ant2 1131 . . . . . . . . . . . . . . . . . . 19 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (!โ€˜๐‘) โˆˆ โ„•)
101 nnm1nn0 12549 . . . . . . . . . . . . . . . . . . . . 21 ((๐‘ โˆ’ ๐‘˜) โˆˆ โ„• โ†’ ((๐‘ โˆ’ ๐‘˜) โˆ’ 1) โˆˆ โ„•0)
102 faccl 14280 . . . . . . . . . . . . . . . . . . . . 21 (((๐‘ โˆ’ ๐‘˜) โˆ’ 1) โˆˆ โ„•0 โ†’ (!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) โˆˆ โ„•)
10394, 101, 1023syl 18 . . . . . . . . . . . . . . . . . . . 20 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) โˆˆ โ„•)
104 faccl 14280 . . . . . . . . . . . . . . . . . . . . 21 (๐‘˜ โˆˆ โ„•0 โ†’ (!โ€˜๐‘˜) โˆˆ โ„•)
1051043ad2ant1 1130 . . . . . . . . . . . . . . . . . . . 20 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (!โ€˜๐‘˜) โˆˆ โ„•)
106103, 105nnmulcld 12301 . . . . . . . . . . . . . . . . . . 19 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ ((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (!โ€˜๐‘˜)) โˆˆ โ„•)
107 nnrp 13023 . . . . . . . . . . . . . . . . . . . 20 ((!โ€˜๐‘) โˆˆ โ„• โ†’ (!โ€˜๐‘) โˆˆ โ„+)
108 nnrp 13023 . . . . . . . . . . . . . . . . . . . 20 (((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (!โ€˜๐‘˜)) โˆˆ โ„• โ†’ ((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (!โ€˜๐‘˜)) โˆˆ โ„+)
109 rpdivcl 13037 . . . . . . . . . . . . . . . . . . . 20 (((!โ€˜๐‘) โˆˆ โ„+ โˆง ((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (!โ€˜๐‘˜)) โˆˆ โ„+) โ†’ ((!โ€˜๐‘) / ((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (!โ€˜๐‘˜))) โˆˆ โ„+)
110107, 108, 109syl2an 594 . . . . . . . . . . . . . . . . . . 19 (((!โ€˜๐‘) โˆˆ โ„• โˆง ((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (!โ€˜๐‘˜)) โˆˆ โ„•) โ†’ ((!โ€˜๐‘) / ((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (!โ€˜๐‘˜))) โˆˆ โ„+)
111100, 106, 110syl2anc 582 . . . . . . . . . . . . . . . . . 18 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ ((!โ€˜๐‘) / ((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (!โ€˜๐‘˜))) โˆˆ โ„+)
112111rpregt0d 13060 . . . . . . . . . . . . . . . . 17 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (((!โ€˜๐‘) / ((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (!โ€˜๐‘˜))) โˆˆ โ„ โˆง 0 < ((!โ€˜๐‘) / ((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (!โ€˜๐‘˜)))))
113 lediv2 12140 . . . . . . . . . . . . . . . . 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 14279 . . . . . . . . . . . . . . . . . . . 20 ((๐‘ โˆ’ ๐‘˜) โˆˆ โ„• โ†’ (!โ€˜(๐‘ โˆ’ ๐‘˜)) = ((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (๐‘ โˆ’ ๐‘˜)))
11794, 116syl 17 . . . . . . . . . . . . . . . . . . 19 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (!โ€˜(๐‘ โˆ’ ๐‘˜)) = ((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (๐‘ โˆ’ ๐‘˜)))
118117oveq1d 7439 . . . . . . . . . . . . . . . . . 18 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ ((!โ€˜(๐‘ โˆ’ ๐‘˜)) ยท (!โ€˜๐‘˜)) = (((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (๐‘ โˆ’ ๐‘˜)) ยท (!โ€˜๐‘˜)))
119103nncnd 12264 . . . . . . . . . . . . . . . . . . 19 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) โˆˆ โ„‚)
120105nncnd 12264 . . . . . . . . . . . . . . . . . . 19 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (!โ€˜๐‘˜) โˆˆ โ„‚)
12177zcnd 12703 . . . . . . . . . . . . . . . . . . 19 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (๐‘ โˆ’ ๐‘˜) โˆˆ โ„‚)
122119, 120, 121mul32d 11460 . . . . . . . . . . . . . . . . . 18 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (!โ€˜๐‘˜)) ยท (๐‘ โˆ’ ๐‘˜)) = (((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (๐‘ โˆ’ ๐‘˜)) ยท (!โ€˜๐‘˜)))
123118, 122eqtr4d 2770 . . . . . . . . . . . . . . . . 17 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ ((!โ€˜(๐‘ โˆ’ ๐‘˜)) ยท (!โ€˜๐‘˜)) = (((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (!โ€˜๐‘˜)) ยท (๐‘ โˆ’ ๐‘˜)))
124123oveq2d 7440 . . . . . . . . . . . . . . . 16 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ ((!โ€˜๐‘) / ((!โ€˜(๐‘ โˆ’ ๐‘˜)) ยท (!โ€˜๐‘˜))) = ((!โ€˜๐‘) / (((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (!โ€˜๐‘˜)) ยท (๐‘ โˆ’ ๐‘˜))))
125 0zd 12606 . . . . . . . . . . . . . . . . . 18 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ 0 โˆˆ โ„ค)
126 nn0ge0 12533 . . . . . . . . . . . . . . . . . . 19 (๐‘˜ โˆˆ โ„•0 โ†’ 0 โ‰ค ๐‘˜)
1271263ad2ant1 1130 . . . . . . . . . . . . . . . . . 18 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ 0 โ‰ค ๐‘˜)
12851, 55, 49, 67, 89letrd 11407 . . . . . . . . . . . . . . . . . 18 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ ๐‘˜ โ‰ค ๐‘)
129125, 74, 76, 127, 128elfzd 13530 . . . . . . . . . . . . . . . . 17 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ ๐‘˜ โˆˆ (0...๐‘))
130 bcval2 14302 . . . . . . . . . . . . . . . . 17 (๐‘˜ โˆˆ (0...๐‘) โ†’ (๐‘C๐‘˜) = ((!โ€˜๐‘) / ((!โ€˜(๐‘ โˆ’ ๐‘˜)) ยท (!โ€˜๐‘˜))))
131129, 130syl 17 . . . . . . . . . . . . . . . 16 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (๐‘C๐‘˜) = ((!โ€˜๐‘) / ((!โ€˜(๐‘ โˆ’ ๐‘˜)) ยท (!โ€˜๐‘˜))))
132100nncnd 12264 . . . . . . . . . . . . . . . . 17 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (!โ€˜๐‘) โˆˆ โ„‚)
133106nncnd 12264 . . . . . . . . . . . . . . . . 17 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ ((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (!โ€˜๐‘˜)) โˆˆ โ„‚)
134106nnne0d 12298 . . . . . . . . . . . . . . . . 17 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ ((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (!โ€˜๐‘˜)) โ‰  0)
13594nnne0d 12298 . . . . . . . . . . . . . . . . 17 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (๐‘ โˆ’ ๐‘˜) โ‰  0)
136132, 133, 121, 134, 135divdiv1d 12057 . . . . . . . . . . . . . . . 16 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (((!โ€˜๐‘) / ((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (!โ€˜๐‘˜))) / (๐‘ โˆ’ ๐‘˜)) = ((!โ€˜๐‘) / (((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (!โ€˜๐‘˜)) ยท (๐‘ โˆ’ ๐‘˜))))
137124, 131, 1363eqtr4d 2777 . . . . . . . . . . . . . . 15 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (๐‘C๐‘˜) = (((!โ€˜๐‘) / ((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (!โ€˜๐‘˜))) / (๐‘ โˆ’ ๐‘˜)))
138 nn0cn 12518 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ โˆˆ โ„•0 โ†’ ๐‘ โˆˆ โ„‚)
1391383ad2ant2 1131 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ ๐‘ โˆˆ โ„‚)
140 nn0cn 12518 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘˜ โˆˆ โ„•0 โ†’ ๐‘˜ โˆˆ โ„‚)
1411403ad2ant1 1130 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ ๐‘˜ โˆˆ โ„‚)
142 1cnd 11245 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ 1 โˆˆ โ„‚)
143139, 141, 142subsub4d 11638 . . . . . . . . . . . . . . . . . . . . 21 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ ((๐‘ โˆ’ ๐‘˜) โˆ’ 1) = (๐‘ โˆ’ (๐‘˜ + 1)))
144143eqcomd 2733 . . . . . . . . . . . . . . . . . . . 20 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (๐‘ โˆ’ (๐‘˜ + 1)) = ((๐‘ โˆ’ ๐‘˜) โˆ’ 1))
145144fveq2d 6904 . . . . . . . . . . . . . . . . . . 19 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (!โ€˜(๐‘ โˆ’ (๐‘˜ + 1))) = (!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)))
146 facp1 14275 . . . . . . . . . . . . . . . . . . . 20 (๐‘˜ โˆˆ โ„•0 โ†’ (!โ€˜(๐‘˜ + 1)) = ((!โ€˜๐‘˜) ยท (๐‘˜ + 1)))
1471463ad2ant1 1130 . . . . . . . . . . . . . . . . . . 19 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (!โ€˜(๐‘˜ + 1)) = ((!โ€˜๐‘˜) ยท (๐‘˜ + 1)))
148145, 147oveq12d 7442 . . . . . . . . . . . . . . . . . 18 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ ((!โ€˜(๐‘ โˆ’ (๐‘˜ + 1))) ยท (!โ€˜(๐‘˜ + 1))) = ((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท ((!โ€˜๐‘˜) ยท (๐‘˜ + 1))))
149119, 120, 56mulassd 11273 . . . . . . . . . . . . . . . . . 18 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (!โ€˜๐‘˜)) ยท (๐‘˜ + 1)) = ((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท ((!โ€˜๐‘˜) ยท (๐‘˜ + 1))))
150148, 149eqtr4d 2770 . . . . . . . . . . . . . . . . 17 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ ((!โ€˜(๐‘ โˆ’ (๐‘˜ + 1))) ยท (!โ€˜(๐‘˜ + 1))) = (((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (!โ€˜๐‘˜)) ยท (๐‘˜ + 1)))
151150oveq2d 7440 . . . . . . . . . . . . . . . 16 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ ((!โ€˜๐‘) / ((!โ€˜(๐‘ โˆ’ (๐‘˜ + 1))) ยท (!โ€˜(๐‘˜ + 1)))) = ((!โ€˜๐‘) / (((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (!โ€˜๐‘˜)) ยท (๐‘˜ + 1))))
15253nnzd 12621 . . . . . . . . . . . . . . . . . 18 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (๐‘˜ + 1) โˆˆ โ„ค)
15354nn0ge0d 12571 . . . . . . . . . . . . . . . . . 18 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ 0 โ‰ค (๐‘˜ + 1))
154125, 74, 152, 153, 89elfzd 13530 . . . . . . . . . . . . . . . . 17 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (๐‘˜ + 1) โˆˆ (0...๐‘))
155 bcval2 14302 . . . . . . . . . . . . . . . . 17 ((๐‘˜ + 1) โˆˆ (0...๐‘) โ†’ (๐‘C(๐‘˜ + 1)) = ((!โ€˜๐‘) / ((!โ€˜(๐‘ โˆ’ (๐‘˜ + 1))) ยท (!โ€˜(๐‘˜ + 1)))))
156154, 155syl 17 . . . . . . . . . . . . . . . 16 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (๐‘C(๐‘˜ + 1)) = ((!โ€˜๐‘) / ((!โ€˜(๐‘ โˆ’ (๐‘˜ + 1))) ยท (!โ€˜(๐‘˜ + 1)))))
15753nnne0d 12298 . . . . . . . . . . . . . . . . 17 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (๐‘˜ + 1) โ‰  0)
158132, 133, 56, 134, 157divdiv1d 12057 . . . . . . . . . . . . . . . 16 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (((!โ€˜๐‘) / ((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (!โ€˜๐‘˜))) / (๐‘˜ + 1)) = ((!โ€˜๐‘) / (((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (!โ€˜๐‘˜)) ยท (๐‘˜ + 1))))
159151, 156, 1583eqtr4d 2777 . . . . . . . . . . . . . . 15 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โ‰ค (๐‘ / 2)) โ†’ (๐‘C(๐‘˜ + 1)) = (((!โ€˜๐‘) / ((!โ€˜((๐‘ โˆ’ ๐‘˜) โˆ’ 1)) ยท (!โ€˜๐‘˜))) / (๐‘˜ + 1)))
160115, 137, 1593brtr4d 5182 . . . . . . . . . . . . . 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 12619 . . . . . . . . . . . . . . 15 (๐ด โˆˆ โ„•0 โ†’ ๐ด โˆˆ โ„ค)
1671663ad2ant3 1132 . . . . . . . . . . . . . 14 ((๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โ†’ ๐ด โˆˆ โ„ค)
168165, 167, 29syl2anc 582 . . . . . . . . . . . . 13 ((๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โ†’ (๐‘C๐ด) โˆˆ โ„•0)
169168nn0red 12569 . . . . . . . . . . . 12 ((๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โ†’ (๐‘C๐ด) โˆˆ โ„)
170 bccl 14319 . . . . . . . . . . . . . 14 ((๐‘ โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ โ„ค) โ†’ (๐‘C๐‘˜) โˆˆ โ„•0)
171165, 36, 170syl2anc 582 . . . . . . . . . . . . 13 ((๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โ†’ (๐‘C๐‘˜) โˆˆ โ„•0)
172171nn0red 12569 . . . . . . . . . . . 12 ((๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โ†’ (๐‘C๐‘˜) โˆˆ โ„)
17336peano2zd 12705 . . . . . . . . . . . . . 14 ((๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โ†’ (๐‘˜ + 1) โˆˆ โ„ค)
174 bccl 14319 . . . . . . . . . . . . . 14 ((๐‘ โˆˆ โ„•0 โˆง (๐‘˜ + 1) โˆˆ โ„ค) โ†’ (๐‘C(๐‘˜ + 1)) โˆˆ โ„•0)
175165, 173, 174syl2anc 582 . . . . . . . . . . . . 13 ((๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โ†’ (๐‘C(๐‘˜ + 1)) โˆˆ โ„•0)
176175nn0red 12569 . . . . . . . . . . . 12 ((๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐‘ โˆˆ โ„•0 โˆง ๐ด โˆˆ โ„•0) โ†’ (๐‘C(๐‘˜ + 1)) โˆˆ โ„)
177 letr 11344 . . . . . . . . . . . 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 415 . . . . . . . . . 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 12926 . . . 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 479 . . . 4 (((๐‘ โˆˆ โ„•0 โˆง ๐ต โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐ต โ‰ค (๐‘ / 2)) โˆง ๐ด < 0) โ†’ ๐ด โˆˆ โ„ค)
190 animorrl 978 . . . 4 (((๐‘ โˆˆ โ„•0 โˆง ๐ต โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐ต โ‰ค (๐‘ / 2)) โˆง ๐ด < 0) โ†’ (๐ด < 0 โˆจ ๐‘ < ๐ด))
191 bcval4 14304 . . . 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 12868 . . . . . 6 (๐ต โˆˆ (โ„คโ‰ฅโ€˜๐ด) โ†’ ๐ต โˆˆ โ„ค)
195193, 194syl 17 . . . . 5 (((๐‘ โˆˆ โ„•0 โˆง ๐ต โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐ต โ‰ค (๐‘ / 2)) โˆง ๐ด < 0) โ†’ ๐ต โˆˆ โ„ค)
196 bccl 14319 . . . . 5 ((๐‘ โˆˆ โ„•0 โˆง ๐ต โˆˆ โ„ค) โ†’ (๐‘C๐ต) โˆˆ โ„•0)
197188, 195, 196syl2anc 582 . . . 4 (((๐‘ โˆˆ โ„•0 โˆง ๐ต โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐ต โ‰ค (๐‘ / 2)) โˆง ๐ด < 0) โ†’ (๐‘C๐ต) โˆˆ โ„•0)
198197nn0ge0d 12571 . . 3 (((๐‘ โˆˆ โ„•0 โˆง ๐ต โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐ต โ‰ค (๐‘ / 2)) โˆง ๐ด < 0) โ†’ 0 โ‰ค (๐‘C๐ต))
199192, 198eqbrtrd 5172 . 2 (((๐‘ โˆˆ โ„•0 โˆง ๐ต โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐ต โ‰ค (๐‘ / 2)) โˆง ๐ด < 0) โ†’ (๐‘C๐ด) โ‰ค (๐‘C๐ต))
200 0re 11252 . . 3 0 โˆˆ โ„
2014zred 12702 . . 3 ((๐‘ โˆˆ โ„•0 โˆง ๐ต โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐ต โ‰ค (๐‘ / 2)) โ†’ ๐ด โˆˆ โ„)
202 lelttric 11357 . . 3 ((0 โˆˆ โ„ โˆง ๐ด โˆˆ โ„) โ†’ (0 โ‰ค ๐ด โˆจ ๐ด < 0))
203200, 201, 202sylancr 585 . 2 ((๐‘ โˆˆ โ„•0 โˆง ๐ต โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐ต โ‰ค (๐‘ / 2)) โ†’ (0 โ‰ค ๐ด โˆจ ๐ด < 0))
204187, 199, 203mpjaodan 956 1 ((๐‘ โˆˆ โ„•0 โˆง ๐ต โˆˆ (โ„คโ‰ฅโ€˜๐ด) โˆง ๐ต โ‰ค (๐‘ / 2)) โ†’ (๐‘C๐ด) โ‰ค (๐‘C๐ต))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 394   โˆจ wo 845   โˆง w3a 1084   = wceq 1533   โˆˆ wcel 2098   class class class wbr 5150  โ€˜cfv 6551  (class class class)co 7424  โ„‚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  โ„+crp 13012  ...cfz 13522  !cfa 14270  Ccbc 14299
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-sep 5301  ax-nul 5308  ax-pow 5367  ax-pr 5431  ax-un 7744  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
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-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-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-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-er 8729  df-en 8969  df-dom 8970  df-sdom 8971  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-n0 12509  df-z 12595  df-uz 12859  df-rp 13013  df-fz 13523  df-seq 14005  df-fac 14271  df-bc 14300
This theorem is referenced by:  bcmax  27229
  Copyright terms: Public domain W3C validator