ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  pcfac GIF version

Theorem pcfac 12347
Description: Calculate the prime count of a factorial. (Contributed by Mario Carneiro, 11-Mar-2014.) (Revised by Mario Carneiro, 21-May-2014.)
Assertion
Ref Expression
pcfac ((๐‘ โˆˆ โ„•0 โˆง ๐‘€ โˆˆ (โ„คโ‰ฅโ€˜๐‘) โˆง ๐‘ƒ โˆˆ โ„™) โ†’ (๐‘ƒ pCnt (!โ€˜๐‘)) = ฮฃ๐‘˜ โˆˆ (1...๐‘€)(โŒŠโ€˜(๐‘ / (๐‘ƒโ†‘๐‘˜))))
Distinct variable groups:   ๐‘ƒ,๐‘˜   ๐‘˜,๐‘   ๐‘˜,๐‘€

Proof of Theorem pcfac
Dummy variables ๐‘š ๐‘› ๐‘ฅ ๐‘— are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq2 5515 . . . . . . . 8 (๐‘ฅ = 0 โ†’ (โ„คโ‰ฅโ€˜๐‘ฅ) = (โ„คโ‰ฅโ€˜0))
2 fveq2 5515 . . . . . . . . . 10 (๐‘ฅ = 0 โ†’ (!โ€˜๐‘ฅ) = (!โ€˜0))
32oveq2d 5890 . . . . . . . . 9 (๐‘ฅ = 0 โ†’ (๐‘ƒ pCnt (!โ€˜๐‘ฅ)) = (๐‘ƒ pCnt (!โ€˜0)))
4 fvoveq1 5897 . . . . . . . . . 10 (๐‘ฅ = 0 โ†’ (โŒŠโ€˜(๐‘ฅ / (๐‘ƒโ†‘๐‘˜))) = (โŒŠโ€˜(0 / (๐‘ƒโ†‘๐‘˜))))
54sumeq2sdv 11377 . . . . . . . . 9 (๐‘ฅ = 0 โ†’ ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘ฅ / (๐‘ƒโ†‘๐‘˜))) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(0 / (๐‘ƒโ†‘๐‘˜))))
63, 5eqeq12d 2192 . . . . . . . 8 (๐‘ฅ = 0 โ†’ ((๐‘ƒ pCnt (!โ€˜๐‘ฅ)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘ฅ / (๐‘ƒโ†‘๐‘˜))) โ†” (๐‘ƒ pCnt (!โ€˜0)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(0 / (๐‘ƒโ†‘๐‘˜)))))
71, 6raleqbidv 2684 . . . . . . 7 (๐‘ฅ = 0 โ†’ (โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘ฅ)(๐‘ƒ pCnt (!โ€˜๐‘ฅ)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘ฅ / (๐‘ƒโ†‘๐‘˜))) โ†” โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜0)(๐‘ƒ pCnt (!โ€˜0)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(0 / (๐‘ƒโ†‘๐‘˜)))))
87imbi2d 230 . . . . . 6 (๐‘ฅ = 0 โ†’ ((๐‘ƒ โˆˆ โ„™ โ†’ โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘ฅ)(๐‘ƒ pCnt (!โ€˜๐‘ฅ)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘ฅ / (๐‘ƒโ†‘๐‘˜)))) โ†” (๐‘ƒ โˆˆ โ„™ โ†’ โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜0)(๐‘ƒ pCnt (!โ€˜0)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(0 / (๐‘ƒโ†‘๐‘˜))))))
9 fveq2 5515 . . . . . . . 8 (๐‘ฅ = ๐‘› โ†’ (โ„คโ‰ฅโ€˜๐‘ฅ) = (โ„คโ‰ฅโ€˜๐‘›))
10 fveq2 5515 . . . . . . . . . 10 (๐‘ฅ = ๐‘› โ†’ (!โ€˜๐‘ฅ) = (!โ€˜๐‘›))
1110oveq2d 5890 . . . . . . . . 9 (๐‘ฅ = ๐‘› โ†’ (๐‘ƒ pCnt (!โ€˜๐‘ฅ)) = (๐‘ƒ pCnt (!โ€˜๐‘›)))
12 fvoveq1 5897 . . . . . . . . . 10 (๐‘ฅ = ๐‘› โ†’ (โŒŠโ€˜(๐‘ฅ / (๐‘ƒโ†‘๐‘˜))) = (โŒŠโ€˜(๐‘› / (๐‘ƒโ†‘๐‘˜))))
1312sumeq2sdv 11377 . . . . . . . . 9 (๐‘ฅ = ๐‘› โ†’ ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘ฅ / (๐‘ƒโ†‘๐‘˜))) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘› / (๐‘ƒโ†‘๐‘˜))))
1411, 13eqeq12d 2192 . . . . . . . 8 (๐‘ฅ = ๐‘› โ†’ ((๐‘ƒ pCnt (!โ€˜๐‘ฅ)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘ฅ / (๐‘ƒโ†‘๐‘˜))) โ†” (๐‘ƒ pCnt (!โ€˜๐‘›)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘› / (๐‘ƒโ†‘๐‘˜)))))
159, 14raleqbidv 2684 . . . . . . 7 (๐‘ฅ = ๐‘› โ†’ (โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘ฅ)(๐‘ƒ pCnt (!โ€˜๐‘ฅ)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘ฅ / (๐‘ƒโ†‘๐‘˜))) โ†” โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘ƒ pCnt (!โ€˜๐‘›)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘› / (๐‘ƒโ†‘๐‘˜)))))
1615imbi2d 230 . . . . . 6 (๐‘ฅ = ๐‘› โ†’ ((๐‘ƒ โˆˆ โ„™ โ†’ โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘ฅ)(๐‘ƒ pCnt (!โ€˜๐‘ฅ)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘ฅ / (๐‘ƒโ†‘๐‘˜)))) โ†” (๐‘ƒ โˆˆ โ„™ โ†’ โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘ƒ pCnt (!โ€˜๐‘›)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘› / (๐‘ƒโ†‘๐‘˜))))))
17 fveq2 5515 . . . . . . . 8 (๐‘ฅ = (๐‘› + 1) โ†’ (โ„คโ‰ฅโ€˜๐‘ฅ) = (โ„คโ‰ฅโ€˜(๐‘› + 1)))
18 fveq2 5515 . . . . . . . . . 10 (๐‘ฅ = (๐‘› + 1) โ†’ (!โ€˜๐‘ฅ) = (!โ€˜(๐‘› + 1)))
1918oveq2d 5890 . . . . . . . . 9 (๐‘ฅ = (๐‘› + 1) โ†’ (๐‘ƒ pCnt (!โ€˜๐‘ฅ)) = (๐‘ƒ pCnt (!โ€˜(๐‘› + 1))))
20 fvoveq1 5897 . . . . . . . . . 10 (๐‘ฅ = (๐‘› + 1) โ†’ (โŒŠโ€˜(๐‘ฅ / (๐‘ƒโ†‘๐‘˜))) = (โŒŠโ€˜((๐‘› + 1) / (๐‘ƒโ†‘๐‘˜))))
2120sumeq2sdv 11377 . . . . . . . . 9 (๐‘ฅ = (๐‘› + 1) โ†’ ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘ฅ / (๐‘ƒโ†‘๐‘˜))) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜((๐‘› + 1) / (๐‘ƒโ†‘๐‘˜))))
2219, 21eqeq12d 2192 . . . . . . . 8 (๐‘ฅ = (๐‘› + 1) โ†’ ((๐‘ƒ pCnt (!โ€˜๐‘ฅ)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘ฅ / (๐‘ƒโ†‘๐‘˜))) โ†” (๐‘ƒ pCnt (!โ€˜(๐‘› + 1))) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜((๐‘› + 1) / (๐‘ƒโ†‘๐‘˜)))))
2317, 22raleqbidv 2684 . . . . . . 7 (๐‘ฅ = (๐‘› + 1) โ†’ (โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘ฅ)(๐‘ƒ pCnt (!โ€˜๐‘ฅ)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘ฅ / (๐‘ƒโ†‘๐‘˜))) โ†” โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))(๐‘ƒ pCnt (!โ€˜(๐‘› + 1))) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜((๐‘› + 1) / (๐‘ƒโ†‘๐‘˜)))))
2423imbi2d 230 . . . . . 6 (๐‘ฅ = (๐‘› + 1) โ†’ ((๐‘ƒ โˆˆ โ„™ โ†’ โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘ฅ)(๐‘ƒ pCnt (!โ€˜๐‘ฅ)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘ฅ / (๐‘ƒโ†‘๐‘˜)))) โ†” (๐‘ƒ โˆˆ โ„™ โ†’ โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))(๐‘ƒ pCnt (!โ€˜(๐‘› + 1))) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜((๐‘› + 1) / (๐‘ƒโ†‘๐‘˜))))))
25 fveq2 5515 . . . . . . . 8 (๐‘ฅ = ๐‘ โ†’ (โ„คโ‰ฅโ€˜๐‘ฅ) = (โ„คโ‰ฅโ€˜๐‘))
26 fveq2 5515 . . . . . . . . . 10 (๐‘ฅ = ๐‘ โ†’ (!โ€˜๐‘ฅ) = (!โ€˜๐‘))
2726oveq2d 5890 . . . . . . . . 9 (๐‘ฅ = ๐‘ โ†’ (๐‘ƒ pCnt (!โ€˜๐‘ฅ)) = (๐‘ƒ pCnt (!โ€˜๐‘)))
28 fvoveq1 5897 . . . . . . . . . 10 (๐‘ฅ = ๐‘ โ†’ (โŒŠโ€˜(๐‘ฅ / (๐‘ƒโ†‘๐‘˜))) = (โŒŠโ€˜(๐‘ / (๐‘ƒโ†‘๐‘˜))))
2928sumeq2sdv 11377 . . . . . . . . 9 (๐‘ฅ = ๐‘ โ†’ ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘ฅ / (๐‘ƒโ†‘๐‘˜))) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘ / (๐‘ƒโ†‘๐‘˜))))
3027, 29eqeq12d 2192 . . . . . . . 8 (๐‘ฅ = ๐‘ โ†’ ((๐‘ƒ pCnt (!โ€˜๐‘ฅ)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘ฅ / (๐‘ƒโ†‘๐‘˜))) โ†” (๐‘ƒ pCnt (!โ€˜๐‘)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘ / (๐‘ƒโ†‘๐‘˜)))))
3125, 30raleqbidv 2684 . . . . . . 7 (๐‘ฅ = ๐‘ โ†’ (โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘ฅ)(๐‘ƒ pCnt (!โ€˜๐‘ฅ)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘ฅ / (๐‘ƒโ†‘๐‘˜))) โ†” โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘)(๐‘ƒ pCnt (!โ€˜๐‘)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘ / (๐‘ƒโ†‘๐‘˜)))))
3231imbi2d 230 . . . . . 6 (๐‘ฅ = ๐‘ โ†’ ((๐‘ƒ โˆˆ โ„™ โ†’ โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘ฅ)(๐‘ƒ pCnt (!โ€˜๐‘ฅ)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘ฅ / (๐‘ƒโ†‘๐‘˜)))) โ†” (๐‘ƒ โˆˆ โ„™ โ†’ โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘)(๐‘ƒ pCnt (!โ€˜๐‘)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘ / (๐‘ƒโ†‘๐‘˜))))))
33 1zzd 9279 . . . . . . . . . 10 ((๐‘ƒ โˆˆ โ„™ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜0)) โ†’ 1 โˆˆ โ„ค)
34 eluzelz 9536 . . . . . . . . . . 11 (๐‘š โˆˆ (โ„คโ‰ฅโ€˜0) โ†’ ๐‘š โˆˆ โ„ค)
3534adantl 277 . . . . . . . . . 10 ((๐‘ƒ โˆˆ โ„™ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜0)) โ†’ ๐‘š โˆˆ โ„ค)
3633, 35fzfigd 10430 . . . . . . . . 9 ((๐‘ƒ โˆˆ โ„™ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜0)) โ†’ (1...๐‘š) โˆˆ Fin)
37 isumz 11396 . . . . . . . . . 10 (((1 โˆˆ โ„ค โˆง (1...๐‘š) โŠ† (โ„คโ‰ฅโ€˜1) โˆง โˆ€๐‘— โˆˆ (โ„คโ‰ฅโ€˜1)DECID ๐‘— โˆˆ (1...๐‘š)) โˆจ (1...๐‘š) โˆˆ Fin) โ†’ ฮฃ๐‘˜ โˆˆ (1...๐‘š)0 = 0)
3837olcs 736 . . . . . . . . 9 ((1...๐‘š) โˆˆ Fin โ†’ ฮฃ๐‘˜ โˆˆ (1...๐‘š)0 = 0)
3936, 38syl 14 . . . . . . . 8 ((๐‘ƒ โˆˆ โ„™ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜0)) โ†’ ฮฃ๐‘˜ โˆˆ (1...๐‘š)0 = 0)
40 0nn0 9190 . . . . . . . . . 10 0 โˆˆ โ„•0
41 elfznn 10053 . . . . . . . . . . . . 13 (๐‘˜ โˆˆ (1...๐‘š) โ†’ ๐‘˜ โˆˆ โ„•)
4241nnnn0d 9228 . . . . . . . . . . . 12 (๐‘˜ โˆˆ (1...๐‘š) โ†’ ๐‘˜ โˆˆ โ„•0)
43 nn0uz 9561 . . . . . . . . . . . 12 โ„•0 = (โ„คโ‰ฅโ€˜0)
4442, 43eleqtrdi 2270 . . . . . . . . . . 11 (๐‘˜ โˆˆ (1...๐‘š) โ†’ ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜0))
4544adantl 277 . . . . . . . . . 10 (((๐‘ƒ โˆˆ โ„™ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜0)) โˆง ๐‘˜ โˆˆ (1...๐‘š)) โ†’ ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜0))
46 simpll 527 . . . . . . . . . 10 (((๐‘ƒ โˆˆ โ„™ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜0)) โˆง ๐‘˜ โˆˆ (1...๐‘š)) โ†’ ๐‘ƒ โˆˆ โ„™)
47 pcfaclem 12346 . . . . . . . . . 10 ((0 โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜0) โˆง ๐‘ƒ โˆˆ โ„™) โ†’ (โŒŠโ€˜(0 / (๐‘ƒโ†‘๐‘˜))) = 0)
4840, 45, 46, 47mp3an2i 1342 . . . . . . . . 9 (((๐‘ƒ โˆˆ โ„™ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜0)) โˆง ๐‘˜ โˆˆ (1...๐‘š)) โ†’ (โŒŠโ€˜(0 / (๐‘ƒโ†‘๐‘˜))) = 0)
4948sumeq2dv 11375 . . . . . . . 8 ((๐‘ƒ โˆˆ โ„™ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜0)) โ†’ ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(0 / (๐‘ƒโ†‘๐‘˜))) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)0)
50 fac0 10707 . . . . . . . . . . 11 (!โ€˜0) = 1
5150oveq2i 5885 . . . . . . . . . 10 (๐‘ƒ pCnt (!โ€˜0)) = (๐‘ƒ pCnt 1)
52 pc1 12304 . . . . . . . . . 10 (๐‘ƒ โˆˆ โ„™ โ†’ (๐‘ƒ pCnt 1) = 0)
5351, 52eqtrid 2222 . . . . . . . . 9 (๐‘ƒ โˆˆ โ„™ โ†’ (๐‘ƒ pCnt (!โ€˜0)) = 0)
5453adantr 276 . . . . . . . 8 ((๐‘ƒ โˆˆ โ„™ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜0)) โ†’ (๐‘ƒ pCnt (!โ€˜0)) = 0)
5539, 49, 543eqtr4rd 2221 . . . . . . 7 ((๐‘ƒ โˆˆ โ„™ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜0)) โ†’ (๐‘ƒ pCnt (!โ€˜0)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(0 / (๐‘ƒโ†‘๐‘˜))))
5655ralrimiva 2550 . . . . . 6 (๐‘ƒ โˆˆ โ„™ โ†’ โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜0)(๐‘ƒ pCnt (!โ€˜0)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(0 / (๐‘ƒโ†‘๐‘˜))))
57 nn0z 9272 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„•0 โ†’ ๐‘› โˆˆ โ„ค)
5857adantr 276 . . . . . . . . . . 11 ((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โ†’ ๐‘› โˆˆ โ„ค)
59 uzid 9541 . . . . . . . . . . 11 (๐‘› โˆˆ โ„ค โ†’ ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘›))
60 peano2uz 9582 . . . . . . . . . . 11 (๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘›) โ†’ (๐‘› + 1) โˆˆ (โ„คโ‰ฅโ€˜๐‘›))
6158, 59, 603syl 17 . . . . . . . . . 10 ((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โ†’ (๐‘› + 1) โˆˆ (โ„คโ‰ฅโ€˜๐‘›))
62 uzss 9547 . . . . . . . . . 10 ((๐‘› + 1) โˆˆ (โ„คโ‰ฅโ€˜๐‘›) โ†’ (โ„คโ‰ฅโ€˜(๐‘› + 1)) โŠ† (โ„คโ‰ฅโ€˜๐‘›))
63 ssralv 3219 . . . . . . . . . 10 ((โ„คโ‰ฅโ€˜(๐‘› + 1)) โŠ† (โ„คโ‰ฅโ€˜๐‘›) โ†’ (โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘ƒ pCnt (!โ€˜๐‘›)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘› / (๐‘ƒโ†‘๐‘˜))) โ†’ โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))(๐‘ƒ pCnt (!โ€˜๐‘›)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘› / (๐‘ƒโ†‘๐‘˜)))))
6461, 62, 633syl 17 . . . . . . . . 9 ((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โ†’ (โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘ƒ pCnt (!โ€˜๐‘›)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘› / (๐‘ƒโ†‘๐‘˜))) โ†’ โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))(๐‘ƒ pCnt (!โ€˜๐‘›)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘› / (๐‘ƒโ†‘๐‘˜)))))
65 oveq1 5881 . . . . . . . . . . 11 ((๐‘ƒ pCnt (!โ€˜๐‘›)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘› / (๐‘ƒโ†‘๐‘˜))) โ†’ ((๐‘ƒ pCnt (!โ€˜๐‘›)) + (๐‘ƒ pCnt (๐‘› + 1))) = (ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘› / (๐‘ƒโ†‘๐‘˜))) + (๐‘ƒ pCnt (๐‘› + 1))))
66 simpll 527 . . . . . . . . . . . . . . 15 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ ๐‘› โˆˆ โ„•0)
67 facp1 10709 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„•0 โ†’ (!โ€˜(๐‘› + 1)) = ((!โ€˜๐‘›) ยท (๐‘› + 1)))
6866, 67syl 14 . . . . . . . . . . . . . 14 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ (!โ€˜(๐‘› + 1)) = ((!โ€˜๐‘›) ยท (๐‘› + 1)))
6968oveq2d 5890 . . . . . . . . . . . . 13 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ (๐‘ƒ pCnt (!โ€˜(๐‘› + 1))) = (๐‘ƒ pCnt ((!โ€˜๐‘›) ยท (๐‘› + 1))))
70 simplr 528 . . . . . . . . . . . . . 14 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ ๐‘ƒ โˆˆ โ„™)
71 faccl 10714 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„•0 โ†’ (!โ€˜๐‘›) โˆˆ โ„•)
72 nnz 9271 . . . . . . . . . . . . . . . 16 ((!โ€˜๐‘›) โˆˆ โ„• โ†’ (!โ€˜๐‘›) โˆˆ โ„ค)
73 nnne0 8946 . . . . . . . . . . . . . . . 16 ((!โ€˜๐‘›) โˆˆ โ„• โ†’ (!โ€˜๐‘›) โ‰  0)
7472, 73jca 306 . . . . . . . . . . . . . . 15 ((!โ€˜๐‘›) โˆˆ โ„• โ†’ ((!โ€˜๐‘›) โˆˆ โ„ค โˆง (!โ€˜๐‘›) โ‰  0))
7566, 71, 743syl 17 . . . . . . . . . . . . . 14 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ ((!โ€˜๐‘›) โˆˆ โ„ค โˆง (!โ€˜๐‘›) โ‰  0))
76 nn0p1nn 9214 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„•0 โ†’ (๐‘› + 1) โˆˆ โ„•)
77 nnz 9271 . . . . . . . . . . . . . . . 16 ((๐‘› + 1) โˆˆ โ„• โ†’ (๐‘› + 1) โˆˆ โ„ค)
78 nnne0 8946 . . . . . . . . . . . . . . . 16 ((๐‘› + 1) โˆˆ โ„• โ†’ (๐‘› + 1) โ‰  0)
7977, 78jca 306 . . . . . . . . . . . . . . 15 ((๐‘› + 1) โˆˆ โ„• โ†’ ((๐‘› + 1) โˆˆ โ„ค โˆง (๐‘› + 1) โ‰  0))
8066, 76, 793syl 17 . . . . . . . . . . . . . 14 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ ((๐‘› + 1) โˆˆ โ„ค โˆง (๐‘› + 1) โ‰  0))
81 pcmul 12300 . . . . . . . . . . . . . 14 ((๐‘ƒ โˆˆ โ„™ โˆง ((!โ€˜๐‘›) โˆˆ โ„ค โˆง (!โ€˜๐‘›) โ‰  0) โˆง ((๐‘› + 1) โˆˆ โ„ค โˆง (๐‘› + 1) โ‰  0)) โ†’ (๐‘ƒ pCnt ((!โ€˜๐‘›) ยท (๐‘› + 1))) = ((๐‘ƒ pCnt (!โ€˜๐‘›)) + (๐‘ƒ pCnt (๐‘› + 1))))
8270, 75, 80, 81syl3anc 1238 . . . . . . . . . . . . 13 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ (๐‘ƒ pCnt ((!โ€˜๐‘›) ยท (๐‘› + 1))) = ((๐‘ƒ pCnt (!โ€˜๐‘›)) + (๐‘ƒ pCnt (๐‘› + 1))))
8369, 82eqtr2d 2211 . . . . . . . . . . . 12 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ ((๐‘ƒ pCnt (!โ€˜๐‘›)) + (๐‘ƒ pCnt (๐‘› + 1))) = (๐‘ƒ pCnt (!โ€˜(๐‘› + 1))))
8466adantr 276 . . . . . . . . . . . . . . . . . 18 ((((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โˆง ๐‘˜ โˆˆ (1...๐‘š)) โ†’ ๐‘› โˆˆ โ„•0)
8584nn0zd 9372 . . . . . . . . . . . . . . . . 17 ((((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โˆง ๐‘˜ โˆˆ (1...๐‘š)) โ†’ ๐‘› โˆˆ โ„ค)
86 prmnn 12109 . . . . . . . . . . . . . . . . . . 19 (๐‘ƒ โˆˆ โ„™ โ†’ ๐‘ƒ โˆˆ โ„•)
8786ad2antlr 489 . . . . . . . . . . . . . . . . . 18 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ ๐‘ƒ โˆˆ โ„•)
88 nnexpcl 10532 . . . . . . . . . . . . . . . . . 18 ((๐‘ƒ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0) โ†’ (๐‘ƒโ†‘๐‘˜) โˆˆ โ„•)
8987, 42, 88syl2an 289 . . . . . . . . . . . . . . . . 17 ((((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โˆง ๐‘˜ โˆˆ (1...๐‘š)) โ†’ (๐‘ƒโ†‘๐‘˜) โˆˆ โ„•)
90 fldivp1 12345 . . . . . . . . . . . . . . . . 17 ((๐‘› โˆˆ โ„ค โˆง (๐‘ƒโ†‘๐‘˜) โˆˆ โ„•) โ†’ ((โŒŠโ€˜((๐‘› + 1) / (๐‘ƒโ†‘๐‘˜))) โˆ’ (โŒŠโ€˜(๐‘› / (๐‘ƒโ†‘๐‘˜)))) = if((๐‘ƒโ†‘๐‘˜) โˆฅ (๐‘› + 1), 1, 0))
9185, 89, 90syl2anc 411 . . . . . . . . . . . . . . . 16 ((((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โˆง ๐‘˜ โˆˆ (1...๐‘š)) โ†’ ((โŒŠโ€˜((๐‘› + 1) / (๐‘ƒโ†‘๐‘˜))) โˆ’ (โŒŠโ€˜(๐‘› / (๐‘ƒโ†‘๐‘˜)))) = if((๐‘ƒโ†‘๐‘˜) โˆฅ (๐‘› + 1), 1, 0))
92 elfzuz 10020 . . . . . . . . . . . . . . . . . . 19 (๐‘˜ โˆˆ (1...๐‘š) โ†’ ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜1))
9366, 76syl 14 . . . . . . . . . . . . . . . . . . . . 21 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ (๐‘› + 1) โˆˆ โ„•)
9470, 93pccld 12299 . . . . . . . . . . . . . . . . . . . 20 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ (๐‘ƒ pCnt (๐‘› + 1)) โˆˆ โ„•0)
9594nn0zd 9372 . . . . . . . . . . . . . . . . . . 19 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ (๐‘ƒ pCnt (๐‘› + 1)) โˆˆ โ„ค)
96 elfz5 10016 . . . . . . . . . . . . . . . . . . 19 ((๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜1) โˆง (๐‘ƒ pCnt (๐‘› + 1)) โˆˆ โ„ค) โ†’ (๐‘˜ โˆˆ (1...(๐‘ƒ pCnt (๐‘› + 1))) โ†” ๐‘˜ โ‰ค (๐‘ƒ pCnt (๐‘› + 1))))
9792, 95, 96syl2anr 290 . . . . . . . . . . . . . . . . . 18 ((((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โˆง ๐‘˜ โˆˆ (1...๐‘š)) โ†’ (๐‘˜ โˆˆ (1...(๐‘ƒ pCnt (๐‘› + 1))) โ†” ๐‘˜ โ‰ค (๐‘ƒ pCnt (๐‘› + 1))))
98 simpllr 534 . . . . . . . . . . . . . . . . . . 19 ((((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โˆง ๐‘˜ โˆˆ (1...๐‘š)) โ†’ ๐‘ƒ โˆˆ โ„™)
9984, 76syl 14 . . . . . . . . . . . . . . . . . . . 20 ((((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โˆง ๐‘˜ โˆˆ (1...๐‘š)) โ†’ (๐‘› + 1) โˆˆ โ„•)
10099nnzd 9373 . . . . . . . . . . . . . . . . . . 19 ((((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โˆง ๐‘˜ โˆˆ (1...๐‘š)) โ†’ (๐‘› + 1) โˆˆ โ„ค)
10142adantl 277 . . . . . . . . . . . . . . . . . . 19 ((((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โˆง ๐‘˜ โˆˆ (1...๐‘š)) โ†’ ๐‘˜ โˆˆ โ„•0)
102 pcdvdsb 12318 . . . . . . . . . . . . . . . . . . 19 ((๐‘ƒ โˆˆ โ„™ โˆง (๐‘› + 1) โˆˆ โ„ค โˆง ๐‘˜ โˆˆ โ„•0) โ†’ (๐‘˜ โ‰ค (๐‘ƒ pCnt (๐‘› + 1)) โ†” (๐‘ƒโ†‘๐‘˜) โˆฅ (๐‘› + 1)))
10398, 100, 101, 102syl3anc 1238 . . . . . . . . . . . . . . . . . 18 ((((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โˆง ๐‘˜ โˆˆ (1...๐‘š)) โ†’ (๐‘˜ โ‰ค (๐‘ƒ pCnt (๐‘› + 1)) โ†” (๐‘ƒโ†‘๐‘˜) โˆฅ (๐‘› + 1)))
10497, 103bitr2d 189 . . . . . . . . . . . . . . . . 17 ((((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โˆง ๐‘˜ โˆˆ (1...๐‘š)) โ†’ ((๐‘ƒโ†‘๐‘˜) โˆฅ (๐‘› + 1) โ†” ๐‘˜ โˆˆ (1...(๐‘ƒ pCnt (๐‘› + 1)))))
105104ifbid 3555 . . . . . . . . . . . . . . . 16 ((((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โˆง ๐‘˜ โˆˆ (1...๐‘š)) โ†’ if((๐‘ƒโ†‘๐‘˜) โˆฅ (๐‘› + 1), 1, 0) = if(๐‘˜ โˆˆ (1...(๐‘ƒ pCnt (๐‘› + 1))), 1, 0))
10691, 105eqtrd 2210 . . . . . . . . . . . . . . 15 ((((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โˆง ๐‘˜ โˆˆ (1...๐‘š)) โ†’ ((โŒŠโ€˜((๐‘› + 1) / (๐‘ƒโ†‘๐‘˜))) โˆ’ (โŒŠโ€˜(๐‘› / (๐‘ƒโ†‘๐‘˜)))) = if(๐‘˜ โˆˆ (1...(๐‘ƒ pCnt (๐‘› + 1))), 1, 0))
107106sumeq2dv 11375 . . . . . . . . . . . . . 14 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ ฮฃ๐‘˜ โˆˆ (1...๐‘š)((โŒŠโ€˜((๐‘› + 1) / (๐‘ƒโ†‘๐‘˜))) โˆ’ (โŒŠโ€˜(๐‘› / (๐‘ƒโ†‘๐‘˜)))) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)if(๐‘˜ โˆˆ (1...(๐‘ƒ pCnt (๐‘› + 1))), 1, 0))
108 1zzd 9279 . . . . . . . . . . . . . . . 16 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ 1 โˆˆ โ„ค)
109 eluzelz 9536 . . . . . . . . . . . . . . . . 17 (๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1)) โ†’ ๐‘š โˆˆ โ„ค)
110109adantl 277 . . . . . . . . . . . . . . . 16 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ ๐‘š โˆˆ โ„ค)
111108, 110fzfigd 10430 . . . . . . . . . . . . . . 15 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ (1...๐‘š) โˆˆ Fin)
112 znq 9623 . . . . . . . . . . . . . . . . . 18 (((๐‘› + 1) โˆˆ โ„ค โˆง (๐‘ƒโ†‘๐‘˜) โˆˆ โ„•) โ†’ ((๐‘› + 1) / (๐‘ƒโ†‘๐‘˜)) โˆˆ โ„š)
113100, 89, 112syl2anc 411 . . . . . . . . . . . . . . . . 17 ((((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โˆง ๐‘˜ โˆˆ (1...๐‘š)) โ†’ ((๐‘› + 1) / (๐‘ƒโ†‘๐‘˜)) โˆˆ โ„š)
114113flqcld 10276 . . . . . . . . . . . . . . . 16 ((((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โˆง ๐‘˜ โˆˆ (1...๐‘š)) โ†’ (โŒŠโ€˜((๐‘› + 1) / (๐‘ƒโ†‘๐‘˜))) โˆˆ โ„ค)
115114zcnd 9375 . . . . . . . . . . . . . . 15 ((((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โˆง ๐‘˜ โˆˆ (1...๐‘š)) โ†’ (โŒŠโ€˜((๐‘› + 1) / (๐‘ƒโ†‘๐‘˜))) โˆˆ โ„‚)
116 znq 9623 . . . . . . . . . . . . . . . . . 18 ((๐‘› โˆˆ โ„ค โˆง (๐‘ƒโ†‘๐‘˜) โˆˆ โ„•) โ†’ (๐‘› / (๐‘ƒโ†‘๐‘˜)) โˆˆ โ„š)
11785, 89, 116syl2anc 411 . . . . . . . . . . . . . . . . 17 ((((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โˆง ๐‘˜ โˆˆ (1...๐‘š)) โ†’ (๐‘› / (๐‘ƒโ†‘๐‘˜)) โˆˆ โ„š)
118117flqcld 10276 . . . . . . . . . . . . . . . 16 ((((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โˆง ๐‘˜ โˆˆ (1...๐‘š)) โ†’ (โŒŠโ€˜(๐‘› / (๐‘ƒโ†‘๐‘˜))) โˆˆ โ„ค)
119118zcnd 9375 . . . . . . . . . . . . . . 15 ((((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โˆง ๐‘˜ โˆˆ (1...๐‘š)) โ†’ (โŒŠโ€˜(๐‘› / (๐‘ƒโ†‘๐‘˜))) โˆˆ โ„‚)
120111, 115, 119fsumsub 11459 . . . . . . . . . . . . . 14 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ ฮฃ๐‘˜ โˆˆ (1...๐‘š)((โŒŠโ€˜((๐‘› + 1) / (๐‘ƒโ†‘๐‘˜))) โˆ’ (โŒŠโ€˜(๐‘› / (๐‘ƒโ†‘๐‘˜)))) = (ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜((๐‘› + 1) / (๐‘ƒโ†‘๐‘˜))) โˆ’ ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘› / (๐‘ƒโ†‘๐‘˜)))))
12194nn0red 9229 . . . . . . . . . . . . . . . . . . 19 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ (๐‘ƒ pCnt (๐‘› + 1)) โˆˆ โ„)
12266nn0red 9229 . . . . . . . . . . . . . . . . . . . 20 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ ๐‘› โˆˆ โ„)
123 peano2re 8092 . . . . . . . . . . . . . . . . . . . 20 (๐‘› โˆˆ โ„ โ†’ (๐‘› + 1) โˆˆ โ„)
124122, 123syl 14 . . . . . . . . . . . . . . . . . . 19 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ (๐‘› + 1) โˆˆ โ„)
125110zred 9374 . . . . . . . . . . . . . . . . . . 19 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ ๐‘š โˆˆ โ„)
12693nnzd 9373 . . . . . . . . . . . . . . . . . . . . 21 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ (๐‘› + 1) โˆˆ โ„ค)
127 zdcle 9328 . . . . . . . . . . . . . . . . . . . . 21 (((๐‘ƒ pCnt (๐‘› + 1)) โˆˆ โ„ค โˆง (๐‘› + 1) โˆˆ โ„ค) โ†’ DECID (๐‘ƒ pCnt (๐‘› + 1)) โ‰ค (๐‘› + 1))
12895, 126, 127syl2anc 411 . . . . . . . . . . . . . . . . . . . 20 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ DECID (๐‘ƒ pCnt (๐‘› + 1)) โ‰ค (๐‘› + 1))
129 zletric 9296 . . . . . . . . . . . . . . . . . . . . . . 23 (((๐‘ƒ pCnt (๐‘› + 1)) โˆˆ โ„ค โˆง (๐‘› + 1) โˆˆ โ„ค) โ†’ ((๐‘ƒ pCnt (๐‘› + 1)) โ‰ค (๐‘› + 1) โˆจ (๐‘› + 1) โ‰ค (๐‘ƒ pCnt (๐‘› + 1))))
13095, 126, 129syl2anc 411 . . . . . . . . . . . . . . . . . . . . . 22 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ ((๐‘ƒ pCnt (๐‘› + 1)) โ‰ค (๐‘› + 1) โˆจ (๐‘› + 1) โ‰ค (๐‘ƒ pCnt (๐‘› + 1))))
131130ord 724 . . . . . . . . . . . . . . . . . . . . 21 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ (ยฌ (๐‘ƒ pCnt (๐‘› + 1)) โ‰ค (๐‘› + 1) โ†’ (๐‘› + 1) โ‰ค (๐‘ƒ pCnt (๐‘› + 1))))
13293nnnn0d 9228 . . . . . . . . . . . . . . . . . . . . . . 23 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ (๐‘› + 1) โˆˆ โ„•0)
133 pcdvdsb 12318 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘ƒ โˆˆ โ„™ โˆง (๐‘› + 1) โˆˆ โ„ค โˆง (๐‘› + 1) โˆˆ โ„•0) โ†’ ((๐‘› + 1) โ‰ค (๐‘ƒ pCnt (๐‘› + 1)) โ†” (๐‘ƒโ†‘(๐‘› + 1)) โˆฅ (๐‘› + 1)))
13470, 126, 132, 133syl3anc 1238 . . . . . . . . . . . . . . . . . . . . . 22 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ ((๐‘› + 1) โ‰ค (๐‘ƒ pCnt (๐‘› + 1)) โ†” (๐‘ƒโ†‘(๐‘› + 1)) โˆฅ (๐‘› + 1)))
13587, 132nnexpcld 10675 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ (๐‘ƒโ†‘(๐‘› + 1)) โˆˆ โ„•)
136135nnzd 9373 . . . . . . . . . . . . . . . . . . . . . . . 24 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ (๐‘ƒโ†‘(๐‘› + 1)) โˆˆ โ„ค)
137 dvdsle 11849 . . . . . . . . . . . . . . . . . . . . . . . 24 (((๐‘ƒโ†‘(๐‘› + 1)) โˆˆ โ„ค โˆง (๐‘› + 1) โˆˆ โ„•) โ†’ ((๐‘ƒโ†‘(๐‘› + 1)) โˆฅ (๐‘› + 1) โ†’ (๐‘ƒโ†‘(๐‘› + 1)) โ‰ค (๐‘› + 1)))
138136, 93, 137syl2anc 411 . . . . . . . . . . . . . . . . . . . . . . 23 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ ((๐‘ƒโ†‘(๐‘› + 1)) โˆฅ (๐‘› + 1) โ†’ (๐‘ƒโ†‘(๐‘› + 1)) โ‰ค (๐‘› + 1)))
139135nnred 8931 . . . . . . . . . . . . . . . . . . . . . . . 24 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ (๐‘ƒโ†‘(๐‘› + 1)) โˆˆ โ„)
140139, 124lenltd 8074 . . . . . . . . . . . . . . . . . . . . . . 23 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ ((๐‘ƒโ†‘(๐‘› + 1)) โ‰ค (๐‘› + 1) โ†” ยฌ (๐‘› + 1) < (๐‘ƒโ†‘(๐‘› + 1))))
141138, 140sylibd 149 . . . . . . . . . . . . . . . . . . . . . 22 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ ((๐‘ƒโ†‘(๐‘› + 1)) โˆฅ (๐‘› + 1) โ†’ ยฌ (๐‘› + 1) < (๐‘ƒโ†‘(๐‘› + 1))))
142134, 141sylbid 150 . . . . . . . . . . . . . . . . . . . . 21 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ ((๐‘› + 1) โ‰ค (๐‘ƒ pCnt (๐‘› + 1)) โ†’ ยฌ (๐‘› + 1) < (๐‘ƒโ†‘(๐‘› + 1))))
143131, 142syld 45 . . . . . . . . . . . . . . . . . . . 20 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ (ยฌ (๐‘ƒ pCnt (๐‘› + 1)) โ‰ค (๐‘› + 1) โ†’ ยฌ (๐‘› + 1) < (๐‘ƒโ†‘(๐‘› + 1))))
144 prmuz2 12130 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ƒ โˆˆ โ„™ โ†’ ๐‘ƒ โˆˆ (โ„คโ‰ฅโ€˜2))
145144ad2antlr 489 . . . . . . . . . . . . . . . . . . . . 21 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ ๐‘ƒ โˆˆ (โ„คโ‰ฅโ€˜2))
146 bernneq3 10642 . . . . . . . . . . . . . . . . . . . . 21 ((๐‘ƒ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง (๐‘› + 1) โˆˆ โ„•0) โ†’ (๐‘› + 1) < (๐‘ƒโ†‘(๐‘› + 1)))
147145, 132, 146syl2anc 411 . . . . . . . . . . . . . . . . . . . 20 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ (๐‘› + 1) < (๐‘ƒโ†‘(๐‘› + 1)))
148 condc 853 . . . . . . . . . . . . . . . . . . . 20 (DECID (๐‘ƒ pCnt (๐‘› + 1)) โ‰ค (๐‘› + 1) โ†’ ((ยฌ (๐‘ƒ pCnt (๐‘› + 1)) โ‰ค (๐‘› + 1) โ†’ ยฌ (๐‘› + 1) < (๐‘ƒโ†‘(๐‘› + 1))) โ†’ ((๐‘› + 1) < (๐‘ƒโ†‘(๐‘› + 1)) โ†’ (๐‘ƒ pCnt (๐‘› + 1)) โ‰ค (๐‘› + 1))))
149128, 143, 147, 148syl3c 63 . . . . . . . . . . . . . . . . . . 19 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ (๐‘ƒ pCnt (๐‘› + 1)) โ‰ค (๐‘› + 1))
150 eluzle 9539 . . . . . . . . . . . . . . . . . . . 20 (๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1)) โ†’ (๐‘› + 1) โ‰ค ๐‘š)
151150adantl 277 . . . . . . . . . . . . . . . . . . 19 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ (๐‘› + 1) โ‰ค ๐‘š)
152121, 124, 125, 149, 151letrd 8080 . . . . . . . . . . . . . . . . . 18 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ (๐‘ƒ pCnt (๐‘› + 1)) โ‰ค ๐‘š)
153 eluz 9540 . . . . . . . . . . . . . . . . . . 19 (((๐‘ƒ pCnt (๐‘› + 1)) โˆˆ โ„ค โˆง ๐‘š โˆˆ โ„ค) โ†’ (๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘ƒ pCnt (๐‘› + 1))) โ†” (๐‘ƒ pCnt (๐‘› + 1)) โ‰ค ๐‘š))
15495, 110, 153syl2anc 411 . . . . . . . . . . . . . . . . . 18 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ (๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘ƒ pCnt (๐‘› + 1))) โ†” (๐‘ƒ pCnt (๐‘› + 1)) โ‰ค ๐‘š))
155152, 154mpbird 167 . . . . . . . . . . . . . . . . 17 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘ƒ pCnt (๐‘› + 1))))
156 fzss2 10063 . . . . . . . . . . . . . . . . 17 (๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘ƒ pCnt (๐‘› + 1))) โ†’ (1...(๐‘ƒ pCnt (๐‘› + 1))) โŠ† (1...๐‘š))
157155, 156syl 14 . . . . . . . . . . . . . . . 16 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ (1...(๐‘ƒ pCnt (๐‘› + 1))) โŠ† (1...๐‘š))
158 elfzelz 10024 . . . . . . . . . . . . . . . . . . 19 (๐‘— โˆˆ (1...๐‘š) โ†’ ๐‘— โˆˆ โ„ค)
159158adantl 277 . . . . . . . . . . . . . . . . . 18 ((((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โˆง ๐‘— โˆˆ (1...๐‘š)) โ†’ ๐‘— โˆˆ โ„ค)
160 1zzd 9279 . . . . . . . . . . . . . . . . . 18 ((((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โˆง ๐‘— โˆˆ (1...๐‘š)) โ†’ 1 โˆˆ โ„ค)
16195adantr 276 . . . . . . . . . . . . . . . . . 18 ((((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โˆง ๐‘— โˆˆ (1...๐‘š)) โ†’ (๐‘ƒ pCnt (๐‘› + 1)) โˆˆ โ„ค)
162 fzdcel 10039 . . . . . . . . . . . . . . . . . 18 ((๐‘— โˆˆ โ„ค โˆง 1 โˆˆ โ„ค โˆง (๐‘ƒ pCnt (๐‘› + 1)) โˆˆ โ„ค) โ†’ DECID ๐‘— โˆˆ (1...(๐‘ƒ pCnt (๐‘› + 1))))
163159, 160, 161, 162syl3anc 1238 . . . . . . . . . . . . . . . . 17 ((((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โˆง ๐‘— โˆˆ (1...๐‘š)) โ†’ DECID ๐‘— โˆˆ (1...(๐‘ƒ pCnt (๐‘› + 1))))
164163ralrimiva 2550 . . . . . . . . . . . . . . . 16 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ โˆ€๐‘— โˆˆ (1...๐‘š)DECID ๐‘— โˆˆ (1...(๐‘ƒ pCnt (๐‘› + 1))))
165 sumhashdc 12344 . . . . . . . . . . . . . . . 16 (((1...๐‘š) โˆˆ Fin โˆง (1...(๐‘ƒ pCnt (๐‘› + 1))) โŠ† (1...๐‘š) โˆง โˆ€๐‘— โˆˆ (1...๐‘š)DECID ๐‘— โˆˆ (1...(๐‘ƒ pCnt (๐‘› + 1)))) โ†’ ฮฃ๐‘˜ โˆˆ (1...๐‘š)if(๐‘˜ โˆˆ (1...(๐‘ƒ pCnt (๐‘› + 1))), 1, 0) = (โ™ฏโ€˜(1...(๐‘ƒ pCnt (๐‘› + 1)))))
166111, 157, 164, 165syl3anc 1238 . . . . . . . . . . . . . . 15 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ ฮฃ๐‘˜ โˆˆ (1...๐‘š)if(๐‘˜ โˆˆ (1...(๐‘ƒ pCnt (๐‘› + 1))), 1, 0) = (โ™ฏโ€˜(1...(๐‘ƒ pCnt (๐‘› + 1)))))
167 hashfz1 10762 . . . . . . . . . . . . . . . 16 ((๐‘ƒ pCnt (๐‘› + 1)) โˆˆ โ„•0 โ†’ (โ™ฏโ€˜(1...(๐‘ƒ pCnt (๐‘› + 1)))) = (๐‘ƒ pCnt (๐‘› + 1)))
16894, 167syl 14 . . . . . . . . . . . . . . 15 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ (โ™ฏโ€˜(1...(๐‘ƒ pCnt (๐‘› + 1)))) = (๐‘ƒ pCnt (๐‘› + 1)))
169166, 168eqtrd 2210 . . . . . . . . . . . . . 14 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ ฮฃ๐‘˜ โˆˆ (1...๐‘š)if(๐‘˜ โˆˆ (1...(๐‘ƒ pCnt (๐‘› + 1))), 1, 0) = (๐‘ƒ pCnt (๐‘› + 1)))
170107, 120, 1693eqtr3d 2218 . . . . . . . . . . . . 13 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ (ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜((๐‘› + 1) / (๐‘ƒโ†‘๐‘˜))) โˆ’ ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘› / (๐‘ƒโ†‘๐‘˜)))) = (๐‘ƒ pCnt (๐‘› + 1)))
171111, 115fsumcl 11407 . . . . . . . . . . . . . 14 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜((๐‘› + 1) / (๐‘ƒโ†‘๐‘˜))) โˆˆ โ„‚)
172111, 119fsumcl 11407 . . . . . . . . . . . . . 14 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘› / (๐‘ƒโ†‘๐‘˜))) โˆˆ โ„‚)
17394nn0cnd 9230 . . . . . . . . . . . . . 14 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ (๐‘ƒ pCnt (๐‘› + 1)) โˆˆ โ„‚)
174171, 172, 173subaddd 8285 . . . . . . . . . . . . 13 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ ((ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜((๐‘› + 1) / (๐‘ƒโ†‘๐‘˜))) โˆ’ ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘› / (๐‘ƒโ†‘๐‘˜)))) = (๐‘ƒ pCnt (๐‘› + 1)) โ†” (ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘› / (๐‘ƒโ†‘๐‘˜))) + (๐‘ƒ pCnt (๐‘› + 1))) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜((๐‘› + 1) / (๐‘ƒโ†‘๐‘˜)))))
175170, 174mpbid 147 . . . . . . . . . . . 12 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ (ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘› / (๐‘ƒโ†‘๐‘˜))) + (๐‘ƒ pCnt (๐‘› + 1))) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜((๐‘› + 1) / (๐‘ƒโ†‘๐‘˜))))
17683, 175eqeq12d 2192 . . . . . . . . . . 11 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ (((๐‘ƒ pCnt (!โ€˜๐‘›)) + (๐‘ƒ pCnt (๐‘› + 1))) = (ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘› / (๐‘ƒโ†‘๐‘˜))) + (๐‘ƒ pCnt (๐‘› + 1))) โ†” (๐‘ƒ pCnt (!โ€˜(๐‘› + 1))) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜((๐‘› + 1) / (๐‘ƒโ†‘๐‘˜)))))
17765, 176imbitrid 154 . . . . . . . . . 10 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ ((๐‘ƒ pCnt (!โ€˜๐‘›)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘› / (๐‘ƒโ†‘๐‘˜))) โ†’ (๐‘ƒ pCnt (!โ€˜(๐‘› + 1))) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜((๐‘› + 1) / (๐‘ƒโ†‘๐‘˜)))))
178177ralimdva 2544 . . . . . . . . 9 ((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โ†’ (โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))(๐‘ƒ pCnt (!โ€˜๐‘›)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘› / (๐‘ƒโ†‘๐‘˜))) โ†’ โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))(๐‘ƒ pCnt (!โ€˜(๐‘› + 1))) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜((๐‘› + 1) / (๐‘ƒโ†‘๐‘˜)))))
17964, 178syld 45 . . . . . . . 8 ((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โ†’ (โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘ƒ pCnt (!โ€˜๐‘›)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘› / (๐‘ƒโ†‘๐‘˜))) โ†’ โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))(๐‘ƒ pCnt (!โ€˜(๐‘› + 1))) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜((๐‘› + 1) / (๐‘ƒโ†‘๐‘˜)))))
180179ex 115 . . . . . . 7 (๐‘› โˆˆ โ„•0 โ†’ (๐‘ƒ โˆˆ โ„™ โ†’ (โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘ƒ pCnt (!โ€˜๐‘›)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘› / (๐‘ƒโ†‘๐‘˜))) โ†’ โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))(๐‘ƒ pCnt (!โ€˜(๐‘› + 1))) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜((๐‘› + 1) / (๐‘ƒโ†‘๐‘˜))))))
181180a2d 26 . . . . . 6 (๐‘› โˆˆ โ„•0 โ†’ ((๐‘ƒ โˆˆ โ„™ โ†’ โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘ƒ pCnt (!โ€˜๐‘›)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘› / (๐‘ƒโ†‘๐‘˜)))) โ†’ (๐‘ƒ โˆˆ โ„™ โ†’ โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))(๐‘ƒ pCnt (!โ€˜(๐‘› + 1))) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜((๐‘› + 1) / (๐‘ƒโ†‘๐‘˜))))))
1828, 16, 24, 32, 56, 181nn0ind 9366 . . . . 5 (๐‘ โˆˆ โ„•0 โ†’ (๐‘ƒ โˆˆ โ„™ โ†’ โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘)(๐‘ƒ pCnt (!โ€˜๐‘)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘ / (๐‘ƒโ†‘๐‘˜)))))
183182imp 124 . . . 4 ((๐‘ โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โ†’ โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘)(๐‘ƒ pCnt (!โ€˜๐‘)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘ / (๐‘ƒโ†‘๐‘˜))))
184 oveq2 5882 . . . . . . 7 (๐‘š = ๐‘€ โ†’ (1...๐‘š) = (1...๐‘€))
185184sumeq1d 11373 . . . . . 6 (๐‘š = ๐‘€ โ†’ ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘ / (๐‘ƒโ†‘๐‘˜))) = ฮฃ๐‘˜ โˆˆ (1...๐‘€)(โŒŠโ€˜(๐‘ / (๐‘ƒโ†‘๐‘˜))))
186185eqeq2d 2189 . . . . 5 (๐‘š = ๐‘€ โ†’ ((๐‘ƒ pCnt (!โ€˜๐‘)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘ / (๐‘ƒโ†‘๐‘˜))) โ†” (๐‘ƒ pCnt (!โ€˜๐‘)) = ฮฃ๐‘˜ โˆˆ (1...๐‘€)(โŒŠโ€˜(๐‘ / (๐‘ƒโ†‘๐‘˜)))))
187186rspcv 2837 . . . 4 (๐‘€ โˆˆ (โ„คโ‰ฅโ€˜๐‘) โ†’ (โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘)(๐‘ƒ pCnt (!โ€˜๐‘)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘ / (๐‘ƒโ†‘๐‘˜))) โ†’ (๐‘ƒ pCnt (!โ€˜๐‘)) = ฮฃ๐‘˜ โˆˆ (1...๐‘€)(โŒŠโ€˜(๐‘ / (๐‘ƒโ†‘๐‘˜)))))
188183, 187syl5 32 . . 3 (๐‘€ โˆˆ (โ„คโ‰ฅโ€˜๐‘) โ†’ ((๐‘ โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โ†’ (๐‘ƒ pCnt (!โ€˜๐‘)) = ฮฃ๐‘˜ โˆˆ (1...๐‘€)(โŒŠโ€˜(๐‘ / (๐‘ƒโ†‘๐‘˜)))))
1891883impib 1201 . 2 ((๐‘€ โˆˆ (โ„คโ‰ฅโ€˜๐‘) โˆง ๐‘ โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โ†’ (๐‘ƒ pCnt (!โ€˜๐‘)) = ฮฃ๐‘˜ โˆˆ (1...๐‘€)(โŒŠโ€˜(๐‘ / (๐‘ƒโ†‘๐‘˜))))
1901893com12 1207 1 ((๐‘ โˆˆ โ„•0 โˆง ๐‘€ โˆˆ (โ„คโ‰ฅโ€˜๐‘) โˆง ๐‘ƒ โˆˆ โ„™) โ†’ (๐‘ƒ pCnt (!โ€˜๐‘)) = ฮฃ๐‘˜ โˆˆ (1...๐‘€)(โŒŠโ€˜(๐‘ / (๐‘ƒโ†‘๐‘˜))))
Colors of variables: wff set class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โˆง wa 104   โ†” wb 105   โˆจ wo 708  DECID wdc 834   โˆง w3a 978   = wceq 1353   โˆˆ wcel 2148   โ‰  wne 2347  โˆ€wral 2455   โŠ† wss 3129  ifcif 3534   class class class wbr 4003  โ€˜cfv 5216  (class class class)co 5874  Fincfn 6739  โ„cr 7809  0cc0 7810  1c1 7811   + caddc 7813   ยท cmul 7815   < clt 7991   โ‰ค cle 7992   โˆ’ cmin 8127   / cdiv 8628  โ„•cn 8918  2c2 8969  โ„•0cn0 9175  โ„คcz 9252  โ„คโ‰ฅcuz 9527  โ„šcq 9618  ...cfz 10007  โŒŠcfl 10267  โ†‘cexp 10518  !cfa 10704  โ™ฏchash 10754  ฮฃcsu 11360   โˆฅ cdvds 11793  โ„™cprime 12106   pCnt cpc 12283
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4118  ax-sep 4121  ax-nul 4129  ax-pow 4174  ax-pr 4209  ax-un 4433  ax-setind 4536  ax-iinf 4587  ax-cnex 7901  ax-resscn 7902  ax-1cn 7903  ax-1re 7904  ax-icn 7905  ax-addcl 7906  ax-addrcl 7907  ax-mulcl 7908  ax-mulrcl 7909  ax-addcom 7910  ax-mulcom 7911  ax-addass 7912  ax-mulass 7913  ax-distr 7914  ax-i2m1 7915  ax-0lt1 7916  ax-1rid 7917  ax-0id 7918  ax-rnegex 7919  ax-precex 7920  ax-cnre 7921  ax-pre-ltirr 7922  ax-pre-ltwlin 7923  ax-pre-lttrn 7924  ax-pre-apti 7925  ax-pre-ltadd 7926  ax-pre-mulgt0 7927  ax-pre-mulext 7928  ax-arch 7929  ax-caucvg 7930
This theorem depends on definitions:  df-bi 117  df-stab 831  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-reu 2462  df-rmo 2463  df-rab 2464  df-v 2739  df-sbc 2963  df-csb 3058  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-nul 3423  df-if 3535  df-pw 3577  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-int 3845  df-iun 3888  df-br 4004  df-opab 4065  df-mpt 4066  df-tr 4102  df-id 4293  df-po 4296  df-iso 4297  df-iord 4366  df-on 4368  df-ilim 4369  df-suc 4371  df-iom 4590  df-xp 4632  df-rel 4633  df-cnv 4634  df-co 4635  df-dm 4636  df-rn 4637  df-res 4638  df-ima 4639  df-iota 5178  df-fun 5218  df-fn 5219  df-f 5220  df-f1 5221  df-fo 5222  df-f1o 5223  df-fv 5224  df-isom 5225  df-riota 5830  df-ov 5877  df-oprab 5878  df-mpo 5879  df-1st 6140  df-2nd 6141  df-recs 6305  df-irdg 6370  df-frec 6391  df-1o 6416  df-2o 6417  df-oadd 6420  df-er 6534  df-en 6740  df-dom 6741  df-fin 6742  df-sup 6982  df-inf 6983  df-pnf 7993  df-mnf 7994  df-xr 7995  df-ltxr 7996  df-le 7997  df-sub 8129  df-neg 8130  df-reap 8531  df-ap 8538  df-div 8629  df-inn 8919  df-2 8977  df-3 8978  df-4 8979  df-n0 9176  df-z 9253  df-uz 9528  df-q 9619  df-rp 9653  df-fz 10008  df-fzo 10142  df-fl 10269  df-mod 10322  df-seqfrec 10445  df-exp 10519  df-fac 10705  df-ihash 10755  df-cj 10850  df-re 10851  df-im 10852  df-rsqrt 11006  df-abs 11007  df-clim 11286  df-sumdc 11361  df-dvds 11794  df-gcd 11943  df-prm 12107  df-pc 12284
This theorem is referenced by:  pcbc  12348
  Copyright terms: Public domain W3C validator