Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  chtwordi Structured version   Unicode version

Theorem chtwordi 23296
 Description: The Chebyshev function is weakly increasing. (Contributed by Mario Carneiro, 22-Sep-2014.)
Assertion
Ref Expression
chtwordi

Proof of Theorem chtwordi
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 simp2 997 . . . 4
2 ppifi 23245 . . . 4
31, 2syl 16 . . 3
4 inss2 3724 . . . . . . . . . 10
5 simpr 461 . . . . . . . . . 10
64, 5sseldi 3507 . . . . . . . . 9
7 prmuz2 14111 . . . . . . . . 9
86, 7syl 16 . . . . . . . 8
9 eluz2b2 11166 . . . . . . . 8
108, 9sylib 196 . . . . . . 7
1110simpld 459 . . . . . 6
1211nnred 10563 . . . . 5
1310simprd 463 . . . . 5
1412, 13rplogcld 22880 . . . 4
1514rpred 11268 . . 3
1614rpge0d 11272 . . 3
17 0red 9609 . . . . 5
18 0le0 10637 . . . . . 6
1918a1i 11 . . . . 5
20 simp3 998 . . . . 5
21 iccss 11604 . . . . 5
2217, 1, 19, 20, 21syl22anc 1229 . . . 4
23 ssrin 3728 . . . 4
2422, 23syl 16 . . 3
253, 15, 16, 24fsumless 13590 . 2
26 chtval 23250 . . 3