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

Theorem sylow1lem1 19381
Description: Lemma for sylow1 19386. The p-adic valuation of the size of ๐‘† is equal to the number of excess powers of ๐‘ƒ in (โ™ฏโ€˜๐‘‹) / (๐‘ƒโ†‘๐‘). (Contributed by Mario Carneiro, 15-Jan-2015.)
Hypotheses
Ref Expression
sylow1.x ๐‘‹ = (Baseโ€˜๐บ)
sylow1.g (๐œ‘ โ†’ ๐บ โˆˆ Grp)
sylow1.f (๐œ‘ โ†’ ๐‘‹ โˆˆ Fin)
sylow1.p (๐œ‘ โ†’ ๐‘ƒ โˆˆ โ„™)
sylow1.n (๐œ‘ โ†’ ๐‘ โˆˆ โ„•0)
sylow1.d (๐œ‘ โ†’ (๐‘ƒโ†‘๐‘) โˆฅ (โ™ฏโ€˜๐‘‹))
sylow1lem.a + = (+gโ€˜๐บ)
sylow1lem.s ๐‘† = {๐‘  โˆˆ ๐’ซ ๐‘‹ โˆฃ (โ™ฏโ€˜๐‘ ) = (๐‘ƒโ†‘๐‘)}
Assertion
Ref Expression
sylow1lem1 (๐œ‘ โ†’ ((โ™ฏโ€˜๐‘†) โˆˆ โ„• โˆง (๐‘ƒ pCnt (โ™ฏโ€˜๐‘†)) = ((๐‘ƒ pCnt (โ™ฏโ€˜๐‘‹)) โˆ’ ๐‘)))
Distinct variable groups:   ๐‘,๐‘    ๐‘‹,๐‘    + ,๐‘    ๐บ,๐‘    ๐‘ƒ,๐‘ 
Allowed substitution hints:   ๐œ‘(๐‘ )   ๐‘†(๐‘ )

Proof of Theorem sylow1lem1
Dummy variables ๐‘ฅ ๐‘› are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sylow1.f . . . . 5 (๐œ‘ โ†’ ๐‘‹ โˆˆ Fin)
2 sylow1.p . . . . . . . 8 (๐œ‘ โ†’ ๐‘ƒ โˆˆ โ„™)
3 prmnn 16551 . . . . . . . 8 (๐‘ƒ โˆˆ โ„™ โ†’ ๐‘ƒ โˆˆ โ„•)
42, 3syl 17 . . . . . . 7 (๐œ‘ โ†’ ๐‘ƒ โˆˆ โ„•)
5 sylow1.n . . . . . . 7 (๐œ‘ โ†’ ๐‘ โˆˆ โ„•0)
64, 5nnexpcld 14149 . . . . . 6 (๐œ‘ โ†’ (๐‘ƒโ†‘๐‘) โˆˆ โ„•)
76nnzd 12527 . . . . 5 (๐œ‘ โ†’ (๐‘ƒโ†‘๐‘) โˆˆ โ„ค)
8 hashbc 14351 . . . . 5 ((๐‘‹ โˆˆ Fin โˆง (๐‘ƒโ†‘๐‘) โˆˆ โ„ค) โ†’ ((โ™ฏโ€˜๐‘‹)C(๐‘ƒโ†‘๐‘)) = (โ™ฏโ€˜{๐‘  โˆˆ ๐’ซ ๐‘‹ โˆฃ (โ™ฏโ€˜๐‘ ) = (๐‘ƒโ†‘๐‘)}))
91, 7, 8syl2anc 585 . . . 4 (๐œ‘ โ†’ ((โ™ฏโ€˜๐‘‹)C(๐‘ƒโ†‘๐‘)) = (โ™ฏโ€˜{๐‘  โˆˆ ๐’ซ ๐‘‹ โˆฃ (โ™ฏโ€˜๐‘ ) = (๐‘ƒโ†‘๐‘)}))
10 sylow1lem.s . . . . 5 ๐‘† = {๐‘  โˆˆ ๐’ซ ๐‘‹ โˆฃ (โ™ฏโ€˜๐‘ ) = (๐‘ƒโ†‘๐‘)}
1110fveq2i 6846 . . . 4 (โ™ฏโ€˜๐‘†) = (โ™ฏโ€˜{๐‘  โˆˆ ๐’ซ ๐‘‹ โˆฃ (โ™ฏโ€˜๐‘ ) = (๐‘ƒโ†‘๐‘)})
129, 11eqtr4di 2795 . . 3 (๐œ‘ โ†’ ((โ™ฏโ€˜๐‘‹)C(๐‘ƒโ†‘๐‘)) = (โ™ฏโ€˜๐‘†))
13 sylow1.d . . . . . 6 (๐œ‘ โ†’ (๐‘ƒโ†‘๐‘) โˆฅ (โ™ฏโ€˜๐‘‹))
14 sylow1.g . . . . . . . . . 10 (๐œ‘ โ†’ ๐บ โˆˆ Grp)
15 sylow1.x . . . . . . . . . . 11 ๐‘‹ = (Baseโ€˜๐บ)
1615grpbn0 18780 . . . . . . . . . 10 (๐บ โˆˆ Grp โ†’ ๐‘‹ โ‰  โˆ…)
1714, 16syl 17 . . . . . . . . 9 (๐œ‘ โ†’ ๐‘‹ โ‰  โˆ…)
18 hasheq0 14264 . . . . . . . . . . 11 (๐‘‹ โˆˆ Fin โ†’ ((โ™ฏโ€˜๐‘‹) = 0 โ†” ๐‘‹ = โˆ…))
191, 18syl 17 . . . . . . . . . 10 (๐œ‘ โ†’ ((โ™ฏโ€˜๐‘‹) = 0 โ†” ๐‘‹ = โˆ…))
2019necon3bbid 2982 . . . . . . . . 9 (๐œ‘ โ†’ (ยฌ (โ™ฏโ€˜๐‘‹) = 0 โ†” ๐‘‹ โ‰  โˆ…))
2117, 20mpbird 257 . . . . . . . 8 (๐œ‘ โ†’ ยฌ (โ™ฏโ€˜๐‘‹) = 0)
22 hashcl 14257 . . . . . . . . . . 11 (๐‘‹ โˆˆ Fin โ†’ (โ™ฏโ€˜๐‘‹) โˆˆ โ„•0)
231, 22syl 17 . . . . . . . . . 10 (๐œ‘ โ†’ (โ™ฏโ€˜๐‘‹) โˆˆ โ„•0)
24 elnn0 12416 . . . . . . . . . 10 ((โ™ฏโ€˜๐‘‹) โˆˆ โ„•0 โ†” ((โ™ฏโ€˜๐‘‹) โˆˆ โ„• โˆจ (โ™ฏโ€˜๐‘‹) = 0))
2523, 24sylib 217 . . . . . . . . 9 (๐œ‘ โ†’ ((โ™ฏโ€˜๐‘‹) โˆˆ โ„• โˆจ (โ™ฏโ€˜๐‘‹) = 0))
2625ord 863 . . . . . . . 8 (๐œ‘ โ†’ (ยฌ (โ™ฏโ€˜๐‘‹) โˆˆ โ„• โ†’ (โ™ฏโ€˜๐‘‹) = 0))
2721, 26mt3d 148 . . . . . . 7 (๐œ‘ โ†’ (โ™ฏโ€˜๐‘‹) โˆˆ โ„•)
28 dvdsle 16193 . . . . . . 7 (((๐‘ƒโ†‘๐‘) โˆˆ โ„ค โˆง (โ™ฏโ€˜๐‘‹) โˆˆ โ„•) โ†’ ((๐‘ƒโ†‘๐‘) โˆฅ (โ™ฏโ€˜๐‘‹) โ†’ (๐‘ƒโ†‘๐‘) โ‰ค (โ™ฏโ€˜๐‘‹)))
297, 27, 28syl2anc 585 . . . . . 6 (๐œ‘ โ†’ ((๐‘ƒโ†‘๐‘) โˆฅ (โ™ฏโ€˜๐‘‹) โ†’ (๐‘ƒโ†‘๐‘) โ‰ค (โ™ฏโ€˜๐‘‹)))
3013, 29mpd 15 . . . . 5 (๐œ‘ โ†’ (๐‘ƒโ†‘๐‘) โ‰ค (โ™ฏโ€˜๐‘‹))
316nnnn0d 12474 . . . . . . 7 (๐œ‘ โ†’ (๐‘ƒโ†‘๐‘) โˆˆ โ„•0)
32 nn0uz 12806 . . . . . . 7 โ„•0 = (โ„คโ‰ฅโ€˜0)
3331, 32eleqtrdi 2848 . . . . . 6 (๐œ‘ โ†’ (๐‘ƒโ†‘๐‘) โˆˆ (โ„คโ‰ฅโ€˜0))
3423nn0zd 12526 . . . . . 6 (๐œ‘ โ†’ (โ™ฏโ€˜๐‘‹) โˆˆ โ„ค)
35 elfz5 13434 . . . . . 6 (((๐‘ƒโ†‘๐‘) โˆˆ (โ„คโ‰ฅโ€˜0) โˆง (โ™ฏโ€˜๐‘‹) โˆˆ โ„ค) โ†’ ((๐‘ƒโ†‘๐‘) โˆˆ (0...(โ™ฏโ€˜๐‘‹)) โ†” (๐‘ƒโ†‘๐‘) โ‰ค (โ™ฏโ€˜๐‘‹)))
3633, 34, 35syl2anc 585 . . . . 5 (๐œ‘ โ†’ ((๐‘ƒโ†‘๐‘) โˆˆ (0...(โ™ฏโ€˜๐‘‹)) โ†” (๐‘ƒโ†‘๐‘) โ‰ค (โ™ฏโ€˜๐‘‹)))
3730, 36mpbird 257 . . . 4 (๐œ‘ โ†’ (๐‘ƒโ†‘๐‘) โˆˆ (0...(โ™ฏโ€˜๐‘‹)))
38 bccl2 14224 . . . 4 ((๐‘ƒโ†‘๐‘) โˆˆ (0...(โ™ฏโ€˜๐‘‹)) โ†’ ((โ™ฏโ€˜๐‘‹)C(๐‘ƒโ†‘๐‘)) โˆˆ โ„•)
3937, 38syl 17 . . 3 (๐œ‘ โ†’ ((โ™ฏโ€˜๐‘‹)C(๐‘ƒโ†‘๐‘)) โˆˆ โ„•)
4012, 39eqeltrrd 2839 . 2 (๐œ‘ โ†’ (โ™ฏโ€˜๐‘†) โˆˆ โ„•)
41 nnuz 12807 . . . . . . . . . . 11 โ„• = (โ„คโ‰ฅโ€˜1)
426, 41eleqtrdi 2848 . . . . . . . . . 10 (๐œ‘ โ†’ (๐‘ƒโ†‘๐‘) โˆˆ (โ„คโ‰ฅโ€˜1))
43 elfz5 13434 . . . . . . . . . 10 (((๐‘ƒโ†‘๐‘) โˆˆ (โ„คโ‰ฅโ€˜1) โˆง (โ™ฏโ€˜๐‘‹) โˆˆ โ„ค) โ†’ ((๐‘ƒโ†‘๐‘) โˆˆ (1...(โ™ฏโ€˜๐‘‹)) โ†” (๐‘ƒโ†‘๐‘) โ‰ค (โ™ฏโ€˜๐‘‹)))
4442, 34, 43syl2anc 585 . . . . . . . . 9 (๐œ‘ โ†’ ((๐‘ƒโ†‘๐‘) โˆˆ (1...(โ™ฏโ€˜๐‘‹)) โ†” (๐‘ƒโ†‘๐‘) โ‰ค (โ™ฏโ€˜๐‘‹)))
4530, 44mpbird 257 . . . . . . . 8 (๐œ‘ โ†’ (๐‘ƒโ†‘๐‘) โˆˆ (1...(โ™ฏโ€˜๐‘‹)))
46 1zzd 12535 . . . . . . . . 9 (๐œ‘ โ†’ 1 โˆˆ โ„ค)
47 fzsubel 13478 . . . . . . . . 9 (((1 โˆˆ โ„ค โˆง (โ™ฏโ€˜๐‘‹) โˆˆ โ„ค) โˆง ((๐‘ƒโ†‘๐‘) โˆˆ โ„ค โˆง 1 โˆˆ โ„ค)) โ†’ ((๐‘ƒโ†‘๐‘) โˆˆ (1...(โ™ฏโ€˜๐‘‹)) โ†” ((๐‘ƒโ†‘๐‘) โˆ’ 1) โˆˆ ((1 โˆ’ 1)...((โ™ฏโ€˜๐‘‹) โˆ’ 1))))
4846, 34, 7, 46, 47syl22anc 838 . . . . . . . 8 (๐œ‘ โ†’ ((๐‘ƒโ†‘๐‘) โˆˆ (1...(โ™ฏโ€˜๐‘‹)) โ†” ((๐‘ƒโ†‘๐‘) โˆ’ 1) โˆˆ ((1 โˆ’ 1)...((โ™ฏโ€˜๐‘‹) โˆ’ 1))))
4945, 48mpbid 231 . . . . . . 7 (๐œ‘ โ†’ ((๐‘ƒโ†‘๐‘) โˆ’ 1) โˆˆ ((1 โˆ’ 1)...((โ™ฏโ€˜๐‘‹) โˆ’ 1)))
50 1m1e0 12226 . . . . . . . 8 (1 โˆ’ 1) = 0
5150oveq1i 7368 . . . . . . 7 ((1 โˆ’ 1)...((โ™ฏโ€˜๐‘‹) โˆ’ 1)) = (0...((โ™ฏโ€˜๐‘‹) โˆ’ 1))
5249, 51eleqtrdi 2848 . . . . . 6 (๐œ‘ โ†’ ((๐‘ƒโ†‘๐‘) โˆ’ 1) โˆˆ (0...((โ™ฏโ€˜๐‘‹) โˆ’ 1)))
53 bcp1nk 14218 . . . . . 6 (((๐‘ƒโ†‘๐‘) โˆ’ 1) โˆˆ (0...((โ™ฏโ€˜๐‘‹) โˆ’ 1)) โ†’ ((((โ™ฏโ€˜๐‘‹) โˆ’ 1) + 1)C(((๐‘ƒโ†‘๐‘) โˆ’ 1) + 1)) = ((((โ™ฏโ€˜๐‘‹) โˆ’ 1)C((๐‘ƒโ†‘๐‘) โˆ’ 1)) ยท ((((โ™ฏโ€˜๐‘‹) โˆ’ 1) + 1) / (((๐‘ƒโ†‘๐‘) โˆ’ 1) + 1))))
5452, 53syl 17 . . . . 5 (๐œ‘ โ†’ ((((โ™ฏโ€˜๐‘‹) โˆ’ 1) + 1)C(((๐‘ƒโ†‘๐‘) โˆ’ 1) + 1)) = ((((โ™ฏโ€˜๐‘‹) โˆ’ 1)C((๐‘ƒโ†‘๐‘) โˆ’ 1)) ยท ((((โ™ฏโ€˜๐‘‹) โˆ’ 1) + 1) / (((๐‘ƒโ†‘๐‘) โˆ’ 1) + 1))))
5523nn0cnd 12476 . . . . . . 7 (๐œ‘ โ†’ (โ™ฏโ€˜๐‘‹) โˆˆ โ„‚)
56 ax-1cn 11110 . . . . . . 7 1 โˆˆ โ„‚
57 npcan 11411 . . . . . . 7 (((โ™ฏโ€˜๐‘‹) โˆˆ โ„‚ โˆง 1 โˆˆ โ„‚) โ†’ (((โ™ฏโ€˜๐‘‹) โˆ’ 1) + 1) = (โ™ฏโ€˜๐‘‹))
5855, 56, 57sylancl 587 . . . . . 6 (๐œ‘ โ†’ (((โ™ฏโ€˜๐‘‹) โˆ’ 1) + 1) = (โ™ฏโ€˜๐‘‹))
596nncnd 12170 . . . . . . 7 (๐œ‘ โ†’ (๐‘ƒโ†‘๐‘) โˆˆ โ„‚)
60 npcan 11411 . . . . . . 7 (((๐‘ƒโ†‘๐‘) โˆˆ โ„‚ โˆง 1 โˆˆ โ„‚) โ†’ (((๐‘ƒโ†‘๐‘) โˆ’ 1) + 1) = (๐‘ƒโ†‘๐‘))
6159, 56, 60sylancl 587 . . . . . 6 (๐œ‘ โ†’ (((๐‘ƒโ†‘๐‘) โˆ’ 1) + 1) = (๐‘ƒโ†‘๐‘))
6258, 61oveq12d 7376 . . . . 5 (๐œ‘ โ†’ ((((โ™ฏโ€˜๐‘‹) โˆ’ 1) + 1)C(((๐‘ƒโ†‘๐‘) โˆ’ 1) + 1)) = ((โ™ฏโ€˜๐‘‹)C(๐‘ƒโ†‘๐‘)))
6358, 61oveq12d 7376 . . . . . 6 (๐œ‘ โ†’ ((((โ™ฏโ€˜๐‘‹) โˆ’ 1) + 1) / (((๐‘ƒโ†‘๐‘) โˆ’ 1) + 1)) = ((โ™ฏโ€˜๐‘‹) / (๐‘ƒโ†‘๐‘)))
6463oveq2d 7374 . . . . 5 (๐œ‘ โ†’ ((((โ™ฏโ€˜๐‘‹) โˆ’ 1)C((๐‘ƒโ†‘๐‘) โˆ’ 1)) ยท ((((โ™ฏโ€˜๐‘‹) โˆ’ 1) + 1) / (((๐‘ƒโ†‘๐‘) โˆ’ 1) + 1))) = ((((โ™ฏโ€˜๐‘‹) โˆ’ 1)C((๐‘ƒโ†‘๐‘) โˆ’ 1)) ยท ((โ™ฏโ€˜๐‘‹) / (๐‘ƒโ†‘๐‘))))
6554, 62, 643eqtr3d 2785 . . . 4 (๐œ‘ โ†’ ((โ™ฏโ€˜๐‘‹)C(๐‘ƒโ†‘๐‘)) = ((((โ™ฏโ€˜๐‘‹) โˆ’ 1)C((๐‘ƒโ†‘๐‘) โˆ’ 1)) ยท ((โ™ฏโ€˜๐‘‹) / (๐‘ƒโ†‘๐‘))))
6665oveq2d 7374 . . 3 (๐œ‘ โ†’ (๐‘ƒ pCnt ((โ™ฏโ€˜๐‘‹)C(๐‘ƒโ†‘๐‘))) = (๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ 1)C((๐‘ƒโ†‘๐‘) โˆ’ 1)) ยท ((โ™ฏโ€˜๐‘‹) / (๐‘ƒโ†‘๐‘)))))
6712oveq2d 7374 . . 3 (๐œ‘ โ†’ (๐‘ƒ pCnt ((โ™ฏโ€˜๐‘‹)C(๐‘ƒโ†‘๐‘))) = (๐‘ƒ pCnt (โ™ฏโ€˜๐‘†)))
68 bccl2 14224 . . . . . . 7 (((๐‘ƒโ†‘๐‘) โˆ’ 1) โˆˆ (0...((โ™ฏโ€˜๐‘‹) โˆ’ 1)) โ†’ (((โ™ฏโ€˜๐‘‹) โˆ’ 1)C((๐‘ƒโ†‘๐‘) โˆ’ 1)) โˆˆ โ„•)
6952, 68syl 17 . . . . . 6 (๐œ‘ โ†’ (((โ™ฏโ€˜๐‘‹) โˆ’ 1)C((๐‘ƒโ†‘๐‘) โˆ’ 1)) โˆˆ โ„•)
7069nnzd 12527 . . . . 5 (๐œ‘ โ†’ (((โ™ฏโ€˜๐‘‹) โˆ’ 1)C((๐‘ƒโ†‘๐‘) โˆ’ 1)) โˆˆ โ„ค)
7169nnne0d 12204 . . . . 5 (๐œ‘ โ†’ (((โ™ฏโ€˜๐‘‹) โˆ’ 1)C((๐‘ƒโ†‘๐‘) โˆ’ 1)) โ‰  0)
726nnne0d 12204 . . . . . . 7 (๐œ‘ โ†’ (๐‘ƒโ†‘๐‘) โ‰  0)
73 dvdsval2 16140 . . . . . . 7 (((๐‘ƒโ†‘๐‘) โˆˆ โ„ค โˆง (๐‘ƒโ†‘๐‘) โ‰  0 โˆง (โ™ฏโ€˜๐‘‹) โˆˆ โ„ค) โ†’ ((๐‘ƒโ†‘๐‘) โˆฅ (โ™ฏโ€˜๐‘‹) โ†” ((โ™ฏโ€˜๐‘‹) / (๐‘ƒโ†‘๐‘)) โˆˆ โ„ค))
747, 72, 34, 73syl3anc 1372 . . . . . 6 (๐œ‘ โ†’ ((๐‘ƒโ†‘๐‘) โˆฅ (โ™ฏโ€˜๐‘‹) โ†” ((โ™ฏโ€˜๐‘‹) / (๐‘ƒโ†‘๐‘)) โˆˆ โ„ค))
7513, 74mpbid 231 . . . . 5 (๐œ‘ โ†’ ((โ™ฏโ€˜๐‘‹) / (๐‘ƒโ†‘๐‘)) โˆˆ โ„ค)
7627nnne0d 12204 . . . . . 6 (๐œ‘ โ†’ (โ™ฏโ€˜๐‘‹) โ‰  0)
7755, 59, 76, 72divne0d 11948 . . . . 5 (๐œ‘ โ†’ ((โ™ฏโ€˜๐‘‹) / (๐‘ƒโ†‘๐‘)) โ‰  0)
78 pcmul 16724 . . . . 5 ((๐‘ƒ โˆˆ โ„™ โˆง ((((โ™ฏโ€˜๐‘‹) โˆ’ 1)C((๐‘ƒโ†‘๐‘) โˆ’ 1)) โˆˆ โ„ค โˆง (((โ™ฏโ€˜๐‘‹) โˆ’ 1)C((๐‘ƒโ†‘๐‘) โˆ’ 1)) โ‰  0) โˆง (((โ™ฏโ€˜๐‘‹) / (๐‘ƒโ†‘๐‘)) โˆˆ โ„ค โˆง ((โ™ฏโ€˜๐‘‹) / (๐‘ƒโ†‘๐‘)) โ‰  0)) โ†’ (๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ 1)C((๐‘ƒโ†‘๐‘) โˆ’ 1)) ยท ((โ™ฏโ€˜๐‘‹) / (๐‘ƒโ†‘๐‘)))) = ((๐‘ƒ pCnt (((โ™ฏโ€˜๐‘‹) โˆ’ 1)C((๐‘ƒโ†‘๐‘) โˆ’ 1))) + (๐‘ƒ pCnt ((โ™ฏโ€˜๐‘‹) / (๐‘ƒโ†‘๐‘)))))
792, 70, 71, 75, 77, 78syl122anc 1380 . . . 4 (๐œ‘ โ†’ (๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ 1)C((๐‘ƒโ†‘๐‘) โˆ’ 1)) ยท ((โ™ฏโ€˜๐‘‹) / (๐‘ƒโ†‘๐‘)))) = ((๐‘ƒ pCnt (((โ™ฏโ€˜๐‘‹) โˆ’ 1)C((๐‘ƒโ†‘๐‘) โˆ’ 1))) + (๐‘ƒ pCnt ((โ™ฏโ€˜๐‘‹) / (๐‘ƒโ†‘๐‘)))))
80 1cnd 11151 . . . . . . . . 9 (๐œ‘ โ†’ 1 โˆˆ โ„‚)
8155, 59, 80npncand 11537 . . . . . . . 8 (๐œ‘ โ†’ (((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ((๐‘ƒโ†‘๐‘) โˆ’ 1)) = ((โ™ฏโ€˜๐‘‹) โˆ’ 1))
8281oveq1d 7373 . . . . . . 7 (๐œ‘ โ†’ ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ((๐‘ƒโ†‘๐‘) โˆ’ 1))C((๐‘ƒโ†‘๐‘) โˆ’ 1)) = (((โ™ฏโ€˜๐‘‹) โˆ’ 1)C((๐‘ƒโ†‘๐‘) โˆ’ 1)))
8382oveq2d 7374 . . . . . 6 (๐œ‘ โ†’ (๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ((๐‘ƒโ†‘๐‘) โˆ’ 1))C((๐‘ƒโ†‘๐‘) โˆ’ 1))) = (๐‘ƒ pCnt (((โ™ฏโ€˜๐‘‹) โˆ’ 1)C((๐‘ƒโ†‘๐‘) โˆ’ 1))))
846nnred 12169 . . . . . . . 8 (๐œ‘ โ†’ (๐‘ƒโ†‘๐‘) โˆˆ โ„)
8584ltm1d 12088 . . . . . . 7 (๐œ‘ โ†’ ((๐‘ƒโ†‘๐‘) โˆ’ 1) < (๐‘ƒโ†‘๐‘))
86 nnm1nn0 12455 . . . . . . . . 9 ((๐‘ƒโ†‘๐‘) โˆˆ โ„• โ†’ ((๐‘ƒโ†‘๐‘) โˆ’ 1) โˆˆ โ„•0)
876, 86syl 17 . . . . . . . 8 (๐œ‘ โ†’ ((๐‘ƒโ†‘๐‘) โˆ’ 1) โˆˆ โ„•0)
88 breq1 5109 . . . . . . . . . . 11 (๐‘ฅ = 0 โ†’ (๐‘ฅ < (๐‘ƒโ†‘๐‘) โ†” 0 < (๐‘ƒโ†‘๐‘)))
89 bcxmaslem1 15720 . . . . . . . . . . . . 13 (๐‘ฅ = 0 โ†’ ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘ฅ)C๐‘ฅ) = ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + 0)C0))
9089oveq2d 7374 . . . . . . . . . . . 12 (๐‘ฅ = 0 โ†’ (๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘ฅ)C๐‘ฅ)) = (๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + 0)C0)))
9190eqeq1d 2739 . . . . . . . . . . 11 (๐‘ฅ = 0 โ†’ ((๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘ฅ)C๐‘ฅ)) = 0 โ†” (๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + 0)C0)) = 0))
9288, 91imbi12d 345 . . . . . . . . . 10 (๐‘ฅ = 0 โ†’ ((๐‘ฅ < (๐‘ƒโ†‘๐‘) โ†’ (๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘ฅ)C๐‘ฅ)) = 0) โ†” (0 < (๐‘ƒโ†‘๐‘) โ†’ (๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + 0)C0)) = 0)))
9392imbi2d 341 . . . . . . . . 9 (๐‘ฅ = 0 โ†’ ((๐œ‘ โ†’ (๐‘ฅ < (๐‘ƒโ†‘๐‘) โ†’ (๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘ฅ)C๐‘ฅ)) = 0)) โ†” (๐œ‘ โ†’ (0 < (๐‘ƒโ†‘๐‘) โ†’ (๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + 0)C0)) = 0))))
94 breq1 5109 . . . . . . . . . . 11 (๐‘ฅ = ๐‘› โ†’ (๐‘ฅ < (๐‘ƒโ†‘๐‘) โ†” ๐‘› < (๐‘ƒโ†‘๐‘)))
95 bcxmaslem1 15720 . . . . . . . . . . . . 13 (๐‘ฅ = ๐‘› โ†’ ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘ฅ)C๐‘ฅ) = ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›)C๐‘›))
9695oveq2d 7374 . . . . . . . . . . . 12 (๐‘ฅ = ๐‘› โ†’ (๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘ฅ)C๐‘ฅ)) = (๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›)C๐‘›)))
9796eqeq1d 2739 . . . . . . . . . . 11 (๐‘ฅ = ๐‘› โ†’ ((๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘ฅ)C๐‘ฅ)) = 0 โ†” (๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›)C๐‘›)) = 0))
9894, 97imbi12d 345 . . . . . . . . . 10 (๐‘ฅ = ๐‘› โ†’ ((๐‘ฅ < (๐‘ƒโ†‘๐‘) โ†’ (๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘ฅ)C๐‘ฅ)) = 0) โ†” (๐‘› < (๐‘ƒโ†‘๐‘) โ†’ (๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›)C๐‘›)) = 0)))
9998imbi2d 341 . . . . . . . . 9 (๐‘ฅ = ๐‘› โ†’ ((๐œ‘ โ†’ (๐‘ฅ < (๐‘ƒโ†‘๐‘) โ†’ (๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘ฅ)C๐‘ฅ)) = 0)) โ†” (๐œ‘ โ†’ (๐‘› < (๐‘ƒโ†‘๐‘) โ†’ (๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›)C๐‘›)) = 0))))
100 breq1 5109 . . . . . . . . . . 11 (๐‘ฅ = (๐‘› + 1) โ†’ (๐‘ฅ < (๐‘ƒโ†‘๐‘) โ†” (๐‘› + 1) < (๐‘ƒโ†‘๐‘)))
101 bcxmaslem1 15720 . . . . . . . . . . . . 13 (๐‘ฅ = (๐‘› + 1) โ†’ ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘ฅ)C๐‘ฅ) = ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + (๐‘› + 1))C(๐‘› + 1)))
102101oveq2d 7374 . . . . . . . . . . . 12 (๐‘ฅ = (๐‘› + 1) โ†’ (๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘ฅ)C๐‘ฅ)) = (๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + (๐‘› + 1))C(๐‘› + 1))))
103102eqeq1d 2739 . . . . . . . . . . 11 (๐‘ฅ = (๐‘› + 1) โ†’ ((๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘ฅ)C๐‘ฅ)) = 0 โ†” (๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + (๐‘› + 1))C(๐‘› + 1))) = 0))
104100, 103imbi12d 345 . . . . . . . . . 10 (๐‘ฅ = (๐‘› + 1) โ†’ ((๐‘ฅ < (๐‘ƒโ†‘๐‘) โ†’ (๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘ฅ)C๐‘ฅ)) = 0) โ†” ((๐‘› + 1) < (๐‘ƒโ†‘๐‘) โ†’ (๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + (๐‘› + 1))C(๐‘› + 1))) = 0)))
105104imbi2d 341 . . . . . . . . 9 (๐‘ฅ = (๐‘› + 1) โ†’ ((๐œ‘ โ†’ (๐‘ฅ < (๐‘ƒโ†‘๐‘) โ†’ (๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘ฅ)C๐‘ฅ)) = 0)) โ†” (๐œ‘ โ†’ ((๐‘› + 1) < (๐‘ƒโ†‘๐‘) โ†’ (๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + (๐‘› + 1))C(๐‘› + 1))) = 0))))
106 breq1 5109 . . . . . . . . . . 11 (๐‘ฅ = ((๐‘ƒโ†‘๐‘) โˆ’ 1) โ†’ (๐‘ฅ < (๐‘ƒโ†‘๐‘) โ†” ((๐‘ƒโ†‘๐‘) โˆ’ 1) < (๐‘ƒโ†‘๐‘)))
107 bcxmaslem1 15720 . . . . . . . . . . . . 13 (๐‘ฅ = ((๐‘ƒโ†‘๐‘) โˆ’ 1) โ†’ ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘ฅ)C๐‘ฅ) = ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ((๐‘ƒโ†‘๐‘) โˆ’ 1))C((๐‘ƒโ†‘๐‘) โˆ’ 1)))
108107oveq2d 7374 . . . . . . . . . . . 12 (๐‘ฅ = ((๐‘ƒโ†‘๐‘) โˆ’ 1) โ†’ (๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘ฅ)C๐‘ฅ)) = (๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ((๐‘ƒโ†‘๐‘) โˆ’ 1))C((๐‘ƒโ†‘๐‘) โˆ’ 1))))
109108eqeq1d 2739 . . . . . . . . . . 11 (๐‘ฅ = ((๐‘ƒโ†‘๐‘) โˆ’ 1) โ†’ ((๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘ฅ)C๐‘ฅ)) = 0 โ†” (๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ((๐‘ƒโ†‘๐‘) โˆ’ 1))C((๐‘ƒโ†‘๐‘) โˆ’ 1))) = 0))
110106, 109imbi12d 345 . . . . . . . . . 10 (๐‘ฅ = ((๐‘ƒโ†‘๐‘) โˆ’ 1) โ†’ ((๐‘ฅ < (๐‘ƒโ†‘๐‘) โ†’ (๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘ฅ)C๐‘ฅ)) = 0) โ†” (((๐‘ƒโ†‘๐‘) โˆ’ 1) < (๐‘ƒโ†‘๐‘) โ†’ (๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ((๐‘ƒโ†‘๐‘) โˆ’ 1))C((๐‘ƒโ†‘๐‘) โˆ’ 1))) = 0)))
111110imbi2d 341 . . . . . . . . 9 (๐‘ฅ = ((๐‘ƒโ†‘๐‘) โˆ’ 1) โ†’ ((๐œ‘ โ†’ (๐‘ฅ < (๐‘ƒโ†‘๐‘) โ†’ (๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘ฅ)C๐‘ฅ)) = 0)) โ†” (๐œ‘ โ†’ (((๐‘ƒโ†‘๐‘) โˆ’ 1) < (๐‘ƒโ†‘๐‘) โ†’ (๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ((๐‘ƒโ†‘๐‘) โˆ’ 1))C((๐‘ƒโ†‘๐‘) โˆ’ 1))) = 0))))
112 znn0sub 12551 . . . . . . . . . . . . . . . 16 (((๐‘ƒโ†‘๐‘) โˆˆ โ„ค โˆง (โ™ฏโ€˜๐‘‹) โˆˆ โ„ค) โ†’ ((๐‘ƒโ†‘๐‘) โ‰ค (โ™ฏโ€˜๐‘‹) โ†” ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) โˆˆ โ„•0))
1137, 34, 112syl2anc 585 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((๐‘ƒโ†‘๐‘) โ‰ค (โ™ฏโ€˜๐‘‹) โ†” ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) โˆˆ โ„•0))
11430, 113mpbid 231 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) โˆˆ โ„•0)
115 0nn0 12429 . . . . . . . . . . . . . 14 0 โˆˆ โ„•0
116 nn0addcl 12449 . . . . . . . . . . . . . 14 ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) โˆˆ โ„•0 โˆง 0 โˆˆ โ„•0) โ†’ (((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + 0) โˆˆ โ„•0)
117114, 115, 116sylancl 587 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + 0) โˆˆ โ„•0)
118 bcn0 14211 . . . . . . . . . . . . 13 ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + 0) โˆˆ โ„•0 โ†’ ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + 0)C0) = 1)
119117, 118syl 17 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + 0)C0) = 1)
120119oveq2d 7374 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + 0)C0)) = (๐‘ƒ pCnt 1))
121 pc1 16728 . . . . . . . . . . . 12 (๐‘ƒ โˆˆ โ„™ โ†’ (๐‘ƒ pCnt 1) = 0)
1222, 121syl 17 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘ƒ pCnt 1) = 0)
123120, 122eqtrd 2777 . . . . . . . . . 10 (๐œ‘ โ†’ (๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + 0)C0)) = 0)
124123a1d 25 . . . . . . . . 9 (๐œ‘ โ†’ (0 < (๐‘ƒโ†‘๐‘) โ†’ (๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + 0)C0)) = 0))
125 nn0re 12423 . . . . . . . . . . . . . 14 (๐‘› โˆˆ โ„•0 โ†’ ๐‘› โˆˆ โ„)
126125ad2antrl 727 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ ๐‘› โˆˆ โ„)
127 nn0p1nn 12453 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„•0 โ†’ (๐‘› + 1) โˆˆ โ„•)
128127ad2antrl 727 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ (๐‘› + 1) โˆˆ โ„•)
129128nnred 12169 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ (๐‘› + 1) โˆˆ โ„)
1306adantr 482 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ (๐‘ƒโ†‘๐‘) โˆˆ โ„•)
131130nnred 12169 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ (๐‘ƒโ†‘๐‘) โˆˆ โ„)
132126ltp1d 12086 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ ๐‘› < (๐‘› + 1))
133 simprr 772 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ (๐‘› + 1) < (๐‘ƒโ†‘๐‘))
134126, 129, 131, 132, 133lttrd 11317 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ ๐‘› < (๐‘ƒโ†‘๐‘))
135134expr 458 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ โ„•0) โ†’ ((๐‘› + 1) < (๐‘ƒโ†‘๐‘) โ†’ ๐‘› < (๐‘ƒโ†‘๐‘)))
136135imim1d 82 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘› โˆˆ โ„•0) โ†’ ((๐‘› < (๐‘ƒโ†‘๐‘) โ†’ (๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›)C๐‘›)) = 0) โ†’ ((๐‘› + 1) < (๐‘ƒโ†‘๐‘) โ†’ (๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›)C๐‘›)) = 0)))
137 oveq1 7365 . . . . . . . . . . 11 ((๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›)C๐‘›)) = 0 โ†’ ((๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›)C๐‘›)) + (๐‘ƒ pCnt (((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›) + 1) / (๐‘› + 1)))) = (0 + (๐‘ƒ pCnt (((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›) + 1) / (๐‘› + 1)))))
138114adantr 482 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) โˆˆ โ„•0)
139138nn0cnd 12476 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) โˆˆ โ„‚)
140 nn0cn 12424 . . . . . . . . . . . . . . . . . 18 (๐‘› โˆˆ โ„•0 โ†’ ๐‘› โˆˆ โ„‚)
141140ad2antrl 727 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ ๐‘› โˆˆ โ„‚)
142 1cnd 11151 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ 1 โˆˆ โ„‚)
143139, 141, 142addassd 11178 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›) + 1) = (((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + (๐‘› + 1)))
144143oveq1d 7373 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ (((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›) + 1)C(๐‘› + 1)) = ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + (๐‘› + 1))C(๐‘› + 1)))
145 nn0addge2 12461 . . . . . . . . . . . . . . . . . 18 ((๐‘› โˆˆ โ„ โˆง ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) โˆˆ โ„•0) โ†’ ๐‘› โ‰ค (((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›))
146126, 138, 145syl2anc 585 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ ๐‘› โ‰ค (((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›))
147 simprl 770 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ ๐‘› โˆˆ โ„•0)
148147, 32eleqtrdi 2848 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ ๐‘› โˆˆ (โ„คโ‰ฅโ€˜0))
149138, 147nn0addcld 12478 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ (((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›) โˆˆ โ„•0)
150149nn0zd 12526 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ (((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›) โˆˆ โ„ค)
151 elfz5 13434 . . . . . . . . . . . . . . . . . 18 ((๐‘› โˆˆ (โ„คโ‰ฅโ€˜0) โˆง (((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›) โˆˆ โ„ค) โ†’ (๐‘› โˆˆ (0...(((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›)) โ†” ๐‘› โ‰ค (((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›)))
152148, 150, 151syl2anc 585 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ (๐‘› โˆˆ (0...(((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›)) โ†” ๐‘› โ‰ค (((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›)))
153146, 152mpbird 257 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ ๐‘› โˆˆ (0...(((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›)))
154 bcp1nk 14218 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ (0...(((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›)) โ†’ (((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›) + 1)C(๐‘› + 1)) = (((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›)C๐‘›) ยท (((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›) + 1) / (๐‘› + 1))))
155153, 154syl 17 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ (((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›) + 1)C(๐‘› + 1)) = (((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›)C๐‘›) ยท (((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›) + 1) / (๐‘› + 1))))
156144, 155eqtr3d 2779 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + (๐‘› + 1))C(๐‘› + 1)) = (((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›)C๐‘›) ยท (((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›) + 1) / (๐‘› + 1))))
157156oveq2d 7374 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ (๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + (๐‘› + 1))C(๐‘› + 1))) = (๐‘ƒ pCnt (((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›)C๐‘›) ยท (((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›) + 1) / (๐‘› + 1)))))
1582adantr 482 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ ๐‘ƒ โˆˆ โ„™)
159 bccl2 14224 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ (0...(((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›)) โ†’ ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›)C๐‘›) โˆˆ โ„•)
160153, 159syl 17 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›)C๐‘›) โˆˆ โ„•)
161 nnq 12888 . . . . . . . . . . . . . . 15 (((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›)C๐‘›) โˆˆ โ„• โ†’ ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›)C๐‘›) โˆˆ โ„š)
162160, 161syl 17 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›)C๐‘›) โˆˆ โ„š)
163160nnne0d 12204 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›)C๐‘›) โ‰  0)
164150peano2zd 12611 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›) + 1) โˆˆ โ„ค)
165 znq 12878 . . . . . . . . . . . . . . 15 ((((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›) + 1) โˆˆ โ„ค โˆง (๐‘› + 1) โˆˆ โ„•) โ†’ (((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›) + 1) / (๐‘› + 1)) โˆˆ โ„š)
166164, 128, 165syl2anc 585 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ (((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›) + 1) / (๐‘› + 1)) โˆˆ โ„š)
167 nn0p1nn 12453 . . . . . . . . . . . . . . . . 17 ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›) โˆˆ โ„•0 โ†’ ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›) + 1) โˆˆ โ„•)
168149, 167syl 17 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›) + 1) โˆˆ โ„•)
169 nnrp 12927 . . . . . . . . . . . . . . . . 17 (((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›) + 1) โˆˆ โ„• โ†’ ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›) + 1) โˆˆ โ„+)
170 nnrp 12927 . . . . . . . . . . . . . . . . 17 ((๐‘› + 1) โˆˆ โ„• โ†’ (๐‘› + 1) โˆˆ โ„+)
171 rpdivcl 12941 . . . . . . . . . . . . . . . . 17 ((((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›) + 1) โˆˆ โ„+ โˆง (๐‘› + 1) โˆˆ โ„+) โ†’ (((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›) + 1) / (๐‘› + 1)) โˆˆ โ„+)
172169, 170, 171syl2an 597 . . . . . . . . . . . . . . . 16 ((((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›) + 1) โˆˆ โ„• โˆง (๐‘› + 1) โˆˆ โ„•) โ†’ (((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›) + 1) / (๐‘› + 1)) โˆˆ โ„+)
173168, 128, 172syl2anc 585 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ (((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›) + 1) / (๐‘› + 1)) โˆˆ โ„+)
174173rpne0d 12963 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ (((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›) + 1) / (๐‘› + 1)) โ‰  0)
175 pcqmul 16726 . . . . . . . . . . . . . 14 ((๐‘ƒ โˆˆ โ„™ โˆง (((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›)C๐‘›) โˆˆ โ„š โˆง ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›)C๐‘›) โ‰  0) โˆง ((((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›) + 1) / (๐‘› + 1)) โˆˆ โ„š โˆง (((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›) + 1) / (๐‘› + 1)) โ‰  0)) โ†’ (๐‘ƒ pCnt (((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›)C๐‘›) ยท (((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›) + 1) / (๐‘› + 1)))) = ((๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›)C๐‘›)) + (๐‘ƒ pCnt (((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›) + 1) / (๐‘› + 1)))))
176158, 162, 163, 166, 174, 175syl122anc 1380 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ (๐‘ƒ pCnt (((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›)C๐‘›) ยท (((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›) + 1) / (๐‘› + 1)))) = ((๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›)C๐‘›)) + (๐‘ƒ pCnt (((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›) + 1) / (๐‘› + 1)))))
177157, 176eqtrd 2777 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ (๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + (๐‘› + 1))C(๐‘› + 1))) = ((๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›)C๐‘›)) + (๐‘ƒ pCnt (((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›) + 1) / (๐‘› + 1)))))
178168nnne0d 12204 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›) + 1) โ‰  0)
179 pcdiv 16725 . . . . . . . . . . . . . . . 16 ((๐‘ƒ โˆˆ โ„™ โˆง (((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›) + 1) โˆˆ โ„ค โˆง ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›) + 1) โ‰  0) โˆง (๐‘› + 1) โˆˆ โ„•) โ†’ (๐‘ƒ pCnt (((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›) + 1) / (๐‘› + 1))) = ((๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›) + 1)) โˆ’ (๐‘ƒ pCnt (๐‘› + 1))))
180158, 164, 178, 128, 179syl121anc 1376 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ (๐‘ƒ pCnt (((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›) + 1) / (๐‘› + 1))) = ((๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›) + 1)) โˆ’ (๐‘ƒ pCnt (๐‘› + 1))))
181128nncnd 12170 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ (๐‘› + 1) โˆˆ โ„‚)
182139, 181, 143comraddd 11370 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›) + 1) = ((๐‘› + 1) + ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘))))
183182oveq2d 7374 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ (๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›) + 1)) = (๐‘ƒ pCnt ((๐‘› + 1) + ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)))))
184 simpr 486 . . . . . . . . . . . . . . . . . . . . . 22 (((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โˆง ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) = 0) โ†’ ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) = 0)
185184oveq2d 7374 . . . . . . . . . . . . . . . . . . . . 21 (((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โˆง ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) = 0) โ†’ ((๐‘› + 1) + ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘))) = ((๐‘› + 1) + 0))
186181addid1d 11356 . . . . . . . . . . . . . . . . . . . . . 22 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ ((๐‘› + 1) + 0) = (๐‘› + 1))
187186adantr 482 . . . . . . . . . . . . . . . . . . . . 21 (((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โˆง ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) = 0) โ†’ ((๐‘› + 1) + 0) = (๐‘› + 1))
188185, 187eqtr2d 2778 . . . . . . . . . . . . . . . . . . . 20 (((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โˆง ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) = 0) โ†’ (๐‘› + 1) = ((๐‘› + 1) + ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘))))
189188oveq2d 7374 . . . . . . . . . . . . . . . . . . 19 (((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โˆง ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) = 0) โ†’ (๐‘ƒ pCnt (๐‘› + 1)) = (๐‘ƒ pCnt ((๐‘› + 1) + ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)))))
1902ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20 (((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โˆง ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) โ‰  0) โ†’ ๐‘ƒ โˆˆ โ„™)
191 nnq 12888 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘› + 1) โˆˆ โ„• โ†’ (๐‘› + 1) โˆˆ โ„š)
192128, 191syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ (๐‘› + 1) โˆˆ โ„š)
193192adantr 482 . . . . . . . . . . . . . . . . . . . 20 (((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โˆง ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) โ‰  0) โ†’ (๐‘› + 1) โˆˆ โ„š)
194138nn0zd 12526 . . . . . . . . . . . . . . . . . . . . . 22 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) โˆˆ โ„ค)
195 zq 12880 . . . . . . . . . . . . . . . . . . . . . 22 (((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) โˆˆ โ„ค โ†’ ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) โˆˆ โ„š)
196194, 195syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) โˆˆ โ„š)
197196adantr 482 . . . . . . . . . . . . . . . . . . . 20 (((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โˆง ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) โ‰  0) โ†’ ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) โˆˆ โ„š)
198158, 128pccld 16723 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ (๐‘ƒ pCnt (๐‘› + 1)) โˆˆ โ„•0)
199198nn0red 12475 . . . . . . . . . . . . . . . . . . . . . 22 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ (๐‘ƒ pCnt (๐‘› + 1)) โˆˆ โ„)
200199adantr 482 . . . . . . . . . . . . . . . . . . . . 21 (((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โˆง ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) โ‰  0) โ†’ (๐‘ƒ pCnt (๐‘› + 1)) โˆˆ โ„)
2015adantr 482 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ ๐‘ โˆˆ โ„•0)
202201nn0red 12475 . . . . . . . . . . . . . . . . . . . . . 22 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ ๐‘ โˆˆ โ„)
203202adantr 482 . . . . . . . . . . . . . . . . . . . . 21 (((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โˆง ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) โ‰  0) โ†’ ๐‘ โˆˆ โ„)
204 simpr 486 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โˆง ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) โ‰  0) โ†’ ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) โ‰  0)
205204neneqd 2949 . . . . . . . . . . . . . . . . . . . . . . . 24 (((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โˆง ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) โ‰  0) โ†’ ยฌ ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) = 0)
206114ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โˆง ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) โ‰  0) โ†’ ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) โˆˆ โ„•0)
207 elnn0 12416 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) โˆˆ โ„•0 โ†” (((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) โˆˆ โ„• โˆจ ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) = 0))
208206, 207sylib 217 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โˆง ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) โ‰  0) โ†’ (((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) โˆˆ โ„• โˆจ ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) = 0))
209208ord 863 . . . . . . . . . . . . . . . . . . . . . . . 24 (((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โˆง ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) โ‰  0) โ†’ (ยฌ ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) โˆˆ โ„• โ†’ ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) = 0))
210205, 209mt3d 148 . . . . . . . . . . . . . . . . . . . . . . 23 (((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โˆง ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) โ‰  0) โ†’ ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) โˆˆ โ„•)
211190, 210pccld 16723 . . . . . . . . . . . . . . . . . . . . . 22 (((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โˆง ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) โ‰  0) โ†’ (๐‘ƒ pCnt ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘))) โˆˆ โ„•0)
212211nn0red 12475 . . . . . . . . . . . . . . . . . . . . 21 (((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โˆง ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) โ‰  0) โ†’ (๐‘ƒ pCnt ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘))) โˆˆ โ„)
213128nnzd 12527 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ (๐‘› + 1) โˆˆ โ„ค)
214 pcdvdsb 16742 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((๐‘ƒ โˆˆ โ„™ โˆง (๐‘› + 1) โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„•0) โ†’ (๐‘ โ‰ค (๐‘ƒ pCnt (๐‘› + 1)) โ†” (๐‘ƒโ†‘๐‘) โˆฅ (๐‘› + 1)))
215158, 213, 201, 214syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ (๐‘ โ‰ค (๐‘ƒ pCnt (๐‘› + 1)) โ†” (๐‘ƒโ†‘๐‘) โˆฅ (๐‘› + 1)))
2167adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ (๐‘ƒโ†‘๐‘) โˆˆ โ„ค)
217 dvdsle 16193 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((๐‘ƒโ†‘๐‘) โˆˆ โ„ค โˆง (๐‘› + 1) โˆˆ โ„•) โ†’ ((๐‘ƒโ†‘๐‘) โˆฅ (๐‘› + 1) โ†’ (๐‘ƒโ†‘๐‘) โ‰ค (๐‘› + 1)))
218216, 128, 217syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ ((๐‘ƒโ†‘๐‘) โˆฅ (๐‘› + 1) โ†’ (๐‘ƒโ†‘๐‘) โ‰ค (๐‘› + 1)))
219215, 218sylbid 239 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ (๐‘ โ‰ค (๐‘ƒ pCnt (๐‘› + 1)) โ†’ (๐‘ƒโ†‘๐‘) โ‰ค (๐‘› + 1)))
220202, 199lenltd 11302 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ (๐‘ โ‰ค (๐‘ƒ pCnt (๐‘› + 1)) โ†” ยฌ (๐‘ƒ pCnt (๐‘› + 1)) < ๐‘))
221131, 129lenltd 11302 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ ((๐‘ƒโ†‘๐‘) โ‰ค (๐‘› + 1) โ†” ยฌ (๐‘› + 1) < (๐‘ƒโ†‘๐‘)))
222219, 220, 2213imtr3d 293 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ (ยฌ (๐‘ƒ pCnt (๐‘› + 1)) < ๐‘ โ†’ ยฌ (๐‘› + 1) < (๐‘ƒโ†‘๐‘)))
223133, 222mt4d 117 . . . . . . . . . . . . . . . . . . . . . 22 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ (๐‘ƒ pCnt (๐‘› + 1)) < ๐‘)
224223adantr 482 . . . . . . . . . . . . . . . . . . . . 21 (((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โˆง ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) โ‰  0) โ†’ (๐‘ƒ pCnt (๐‘› + 1)) < ๐‘)
225 dvdssubr 16188 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((๐‘ƒโ†‘๐‘) โˆˆ โ„ค โˆง (โ™ฏโ€˜๐‘‹) โˆˆ โ„ค) โ†’ ((๐‘ƒโ†‘๐‘) โˆฅ (โ™ฏโ€˜๐‘‹) โ†” (๐‘ƒโ†‘๐‘) โˆฅ ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘))))
2267, 34, 225syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐œ‘ โ†’ ((๐‘ƒโ†‘๐‘) โˆฅ (โ™ฏโ€˜๐‘‹) โ†” (๐‘ƒโ†‘๐‘) โˆฅ ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘))))
22713, 226mpbid 231 . . . . . . . . . . . . . . . . . . . . . . 23 (๐œ‘ โ†’ (๐‘ƒโ†‘๐‘) โˆฅ ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)))
228227ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . 22 (((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โˆง ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) โ‰  0) โ†’ (๐‘ƒโ†‘๐‘) โˆฅ ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)))
229206nn0zd 12526 . . . . . . . . . . . . . . . . . . . . . . 23 (((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โˆง ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) โ‰  0) โ†’ ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) โˆˆ โ„ค)
2305ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23 (((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โˆง ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) โ‰  0) โ†’ ๐‘ โˆˆ โ„•0)
231 pcdvdsb 16742 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘ƒ โˆˆ โ„™ โˆง ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„•0) โ†’ (๐‘ โ‰ค (๐‘ƒ pCnt ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘))) โ†” (๐‘ƒโ†‘๐‘) โˆฅ ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘))))
232190, 229, 230, 231syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . 22 (((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โˆง ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) โ‰  0) โ†’ (๐‘ โ‰ค (๐‘ƒ pCnt ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘))) โ†” (๐‘ƒโ†‘๐‘) โˆฅ ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘))))
233228, 232mpbird 257 . . . . . . . . . . . . . . . . . . . . 21 (((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โˆง ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) โ‰  0) โ†’ ๐‘ โ‰ค (๐‘ƒ pCnt ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘))))
234200, 203, 212, 224, 233ltletrd 11316 . . . . . . . . . . . . . . . . . . . 20 (((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โˆง ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) โ‰  0) โ†’ (๐‘ƒ pCnt (๐‘› + 1)) < (๐‘ƒ pCnt ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘))))
235190, 193, 197, 234pcadd2 16763 . . . . . . . . . . . . . . . . . . 19 (((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โˆง ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) โ‰  0) โ†’ (๐‘ƒ pCnt (๐‘› + 1)) = (๐‘ƒ pCnt ((๐‘› + 1) + ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)))))
236189, 235pm2.61dane 3033 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ (๐‘ƒ pCnt (๐‘› + 1)) = (๐‘ƒ pCnt ((๐‘› + 1) + ((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)))))
237183, 236eqtr4d 2780 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ (๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›) + 1)) = (๐‘ƒ pCnt (๐‘› + 1)))
238198nn0cnd 12476 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ (๐‘ƒ pCnt (๐‘› + 1)) โˆˆ โ„‚)
239237, 238eqeltrd 2838 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ (๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›) + 1)) โˆˆ โ„‚)
240239, 237subeq0bd 11582 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ ((๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›) + 1)) โˆ’ (๐‘ƒ pCnt (๐‘› + 1))) = 0)
241180, 240eqtrd 2777 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ (๐‘ƒ pCnt (((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›) + 1) / (๐‘› + 1))) = 0)
242241oveq2d 7374 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ (0 + (๐‘ƒ pCnt (((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›) + 1) / (๐‘› + 1)))) = (0 + 0))
243 00id 11331 . . . . . . . . . . . . 13 (0 + 0) = 0
244242, 243eqtr2di 2794 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ 0 = (0 + (๐‘ƒ pCnt (((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›) + 1) / (๐‘› + 1)))))
245177, 244eqeq12d 2753 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ ((๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + (๐‘› + 1))C(๐‘› + 1))) = 0 โ†” ((๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›)C๐‘›)) + (๐‘ƒ pCnt (((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›) + 1) / (๐‘› + 1)))) = (0 + (๐‘ƒ pCnt (((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›) + 1) / (๐‘› + 1))))))
246137, 245syl5ibr 246 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘› โˆˆ โ„•0 โˆง (๐‘› + 1) < (๐‘ƒโ†‘๐‘))) โ†’ ((๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›)C๐‘›)) = 0 โ†’ (๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + (๐‘› + 1))C(๐‘› + 1))) = 0))
247136, 246animpimp2impd 845 . . . . . . . . 9 (๐‘› โˆˆ โ„•0 โ†’ ((๐œ‘ โ†’ (๐‘› < (๐‘ƒโ†‘๐‘) โ†’ (๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ๐‘›)C๐‘›)) = 0)) โ†’ (๐œ‘ โ†’ ((๐‘› + 1) < (๐‘ƒโ†‘๐‘) โ†’ (๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + (๐‘› + 1))C(๐‘› + 1))) = 0))))
24893, 99, 105, 111, 124, 247nn0ind 12599 . . . . . . . 8 (((๐‘ƒโ†‘๐‘) โˆ’ 1) โˆˆ โ„•0 โ†’ (๐œ‘ โ†’ (((๐‘ƒโ†‘๐‘) โˆ’ 1) < (๐‘ƒโ†‘๐‘) โ†’ (๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ((๐‘ƒโ†‘๐‘) โˆ’ 1))C((๐‘ƒโ†‘๐‘) โˆ’ 1))) = 0)))
24987, 248mpcom 38 . . . . . . 7 (๐œ‘ โ†’ (((๐‘ƒโ†‘๐‘) โˆ’ 1) < (๐‘ƒโ†‘๐‘) โ†’ (๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ((๐‘ƒโ†‘๐‘) โˆ’ 1))C((๐‘ƒโ†‘๐‘) โˆ’ 1))) = 0))
25085, 249mpd 15 . . . . . 6 (๐œ‘ โ†’ (๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ (๐‘ƒโ†‘๐‘)) + ((๐‘ƒโ†‘๐‘) โˆ’ 1))C((๐‘ƒโ†‘๐‘) โˆ’ 1))) = 0)
25183, 250eqtr3d 2779 . . . . 5 (๐œ‘ โ†’ (๐‘ƒ pCnt (((โ™ฏโ€˜๐‘‹) โˆ’ 1)C((๐‘ƒโ†‘๐‘) โˆ’ 1))) = 0)
252 pcdiv 16725 . . . . . . 7 ((๐‘ƒ โˆˆ โ„™ โˆง ((โ™ฏโ€˜๐‘‹) โˆˆ โ„ค โˆง (โ™ฏโ€˜๐‘‹) โ‰  0) โˆง (๐‘ƒโ†‘๐‘) โˆˆ โ„•) โ†’ (๐‘ƒ pCnt ((โ™ฏโ€˜๐‘‹) / (๐‘ƒโ†‘๐‘))) = ((๐‘ƒ pCnt (โ™ฏโ€˜๐‘‹)) โˆ’ (๐‘ƒ pCnt (๐‘ƒโ†‘๐‘))))
2532, 34, 76, 6, 252syl121anc 1376 . . . . . 6 (๐œ‘ โ†’ (๐‘ƒ pCnt ((โ™ฏโ€˜๐‘‹) / (๐‘ƒโ†‘๐‘))) = ((๐‘ƒ pCnt (โ™ฏโ€˜๐‘‹)) โˆ’ (๐‘ƒ pCnt (๐‘ƒโ†‘๐‘))))
2545nn0zd 12526 . . . . . . . 8 (๐œ‘ โ†’ ๐‘ โˆˆ โ„ค)
255 pcid 16746 . . . . . . . 8 ((๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ โ„ค) โ†’ (๐‘ƒ pCnt (๐‘ƒโ†‘๐‘)) = ๐‘)
2562, 254, 255syl2anc 585 . . . . . . 7 (๐œ‘ โ†’ (๐‘ƒ pCnt (๐‘ƒโ†‘๐‘)) = ๐‘)
257256oveq2d 7374 . . . . . 6 (๐œ‘ โ†’ ((๐‘ƒ pCnt (โ™ฏโ€˜๐‘‹)) โˆ’ (๐‘ƒ pCnt (๐‘ƒโ†‘๐‘))) = ((๐‘ƒ pCnt (โ™ฏโ€˜๐‘‹)) โˆ’ ๐‘))
258253, 257eqtrd 2777 . . . . 5 (๐œ‘ โ†’ (๐‘ƒ pCnt ((โ™ฏโ€˜๐‘‹) / (๐‘ƒโ†‘๐‘))) = ((๐‘ƒ pCnt (โ™ฏโ€˜๐‘‹)) โˆ’ ๐‘))
259251, 258oveq12d 7376 . . . 4 (๐œ‘ โ†’ ((๐‘ƒ pCnt (((โ™ฏโ€˜๐‘‹) โˆ’ 1)C((๐‘ƒโ†‘๐‘) โˆ’ 1))) + (๐‘ƒ pCnt ((โ™ฏโ€˜๐‘‹) / (๐‘ƒโ†‘๐‘)))) = (0 + ((๐‘ƒ pCnt (โ™ฏโ€˜๐‘‹)) โˆ’ ๐‘)))
2602, 27pccld 16723 . . . . . . . 8 (๐œ‘ โ†’ (๐‘ƒ pCnt (โ™ฏโ€˜๐‘‹)) โˆˆ โ„•0)
261260nn0zd 12526 . . . . . . 7 (๐œ‘ โ†’ (๐‘ƒ pCnt (โ™ฏโ€˜๐‘‹)) โˆˆ โ„ค)
262261, 254zsubcld 12613 . . . . . 6 (๐œ‘ โ†’ ((๐‘ƒ pCnt (โ™ฏโ€˜๐‘‹)) โˆ’ ๐‘) โˆˆ โ„ค)
263262zcnd 12609 . . . . 5 (๐œ‘ โ†’ ((๐‘ƒ pCnt (โ™ฏโ€˜๐‘‹)) โˆ’ ๐‘) โˆˆ โ„‚)
264263addid2d 11357 . . . 4 (๐œ‘ โ†’ (0 + ((๐‘ƒ pCnt (โ™ฏโ€˜๐‘‹)) โˆ’ ๐‘)) = ((๐‘ƒ pCnt (โ™ฏโ€˜๐‘‹)) โˆ’ ๐‘))
26579, 259, 2643eqtrd 2781 . . 3 (๐œ‘ โ†’ (๐‘ƒ pCnt ((((โ™ฏโ€˜๐‘‹) โˆ’ 1)C((๐‘ƒโ†‘๐‘) โˆ’ 1)) ยท ((โ™ฏโ€˜๐‘‹) / (๐‘ƒโ†‘๐‘)))) = ((๐‘ƒ pCnt (โ™ฏโ€˜๐‘‹)) โˆ’ ๐‘))
26666, 67, 2653eqtr3d 2785 . 2 (๐œ‘ โ†’ (๐‘ƒ pCnt (โ™ฏโ€˜๐‘†)) = ((๐‘ƒ pCnt (โ™ฏโ€˜๐‘‹)) โˆ’ ๐‘))
26740, 266jca 513 1 (๐œ‘ โ†’ ((โ™ฏโ€˜๐‘†) โˆˆ โ„• โˆง (๐‘ƒ pCnt (โ™ฏโ€˜๐‘†)) = ((๐‘ƒ pCnt (โ™ฏโ€˜๐‘‹)) โˆ’ ๐‘)))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 397   โˆจ wo 846   = wceq 1542   โˆˆ wcel 2107   โ‰  wne 2944  {crab 3408  โˆ…c0 4283  ๐’ซ cpw 4561   class class class wbr 5106  โ€˜cfv 6497  (class class class)co 7358  Fincfn 8884  โ„‚cc 11050  โ„cr 11051  0cc0 11052  1c1 11053   + caddc 11055   ยท cmul 11057   < clt 11190   โ‰ค cle 11191   โˆ’ cmin 11386   / cdiv 11813  โ„•cn 12154  โ„•0cn0 12414  โ„คcz 12500  โ„คโ‰ฅcuz 12764  โ„šcq 12874  โ„+crp 12916  ...cfz 13425  โ†‘cexp 13968  Ccbc 14203  โ™ฏchash 14231   โˆฅ cdvds 16137  โ„™cprime 16548   pCnt cpc 16709  Basecbs 17084  +gcplusg 17134  Grpcgrp 18749
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673  ax-cnex 11108  ax-resscn 11109  ax-1cn 11110  ax-icn 11111  ax-addcl 11112  ax-addrcl 11113  ax-mulcl 11114  ax-mulrcl 11115  ax-mulcom 11116  ax-addass 11117  ax-mulass 11118  ax-distr 11119  ax-i2m1 11120  ax-1ne0 11121  ax-1rid 11122  ax-rnegex 11123  ax-rrecex 11124  ax-cnre 11125  ax-pre-lttri 11126  ax-pre-lttrn 11127  ax-pre-ltadd 11128  ax-pre-mulgt0 11129  ax-pre-sup 11130
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rmo 3354  df-reu 3355  df-rab 3409  df-v 3448  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3930  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-int 4909  df-iun 4957  df-br 5107  df-opab 5169  df-mpt 5190  df-tr 5224  df-id 5532  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5589  df-we 5591  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6254  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-riota 7314  df-ov 7361  df-oprab 7362  df-mpo 7363  df-om 7804  df-1st 7922  df-2nd 7923  df-frecs 8213  df-wrecs 8244  df-recs 8318  df-rdg 8357  df-1o 8413  df-2o 8414  df-oadd 8417  df-er 8649  df-en 8885  df-dom 8886  df-sdom 8887  df-fin 8888  df-sup 9379  df-inf 9380  df-dju 9838  df-card 9876  df-pnf 11192  df-mnf 11193  df-xr 11194  df-ltxr 11195  df-le 11196  df-sub 11388  df-neg 11389  df-div 11814  df-nn 12155  df-2 12217  df-3 12218  df-n0 12415  df-z 12501  df-uz 12765  df-q 12875  df-rp 12917  df-fz 13426  df-fl 13698  df-mod 13776  df-seq 13908  df-exp 13969  df-fac 14175  df-bc 14204  df-hash 14232  df-cj 14985  df-re 14986  df-im 14987  df-sqrt 15121  df-abs 15122  df-dvds 16138  df-gcd 16376  df-prm 16549  df-pc 16710  df-0g 17324  df-mgm 18498  df-sgrp 18547  df-mnd 18558  df-grp 18752
This theorem is referenced by:  sylow1lem3  19383
  Copyright terms: Public domain W3C validator