RSPrimeLower

Statistics

Metric	Count
Definitions	0
Theorems `count_prime_le_imp_le_nth`, `nth_prime_gt_bound`, `p_n_lower_large`, `p_n_lower_small`, `pi_nth_prime'`	5
Total	5

Name	Kind	Assumes	Proves	Validates	Depends On
`count_prime_le_imp_le_nth` 📖	—	—	—	—	—
`nth_prime_gt_bound` 📖	mathematical	—	`nth_prime'`	—	`count_prime_le_imp_le_nth`
`p_n_lower_large` 📖	mathematical	—	`nth_prime'`	—	`Dusart.corollary_5_3_b` `LogTables.exp_1_112_lt` `pi_nth_prime'` `LogTables.log_32_gt` `LogTables.log_2_353_gt` `LogTables.log_3_2_gt`
`p_n_lower_small` 📖	mathematical	—	`nth_prime'`	—	`nth_prime_gt_bound` `count_prime_127_le_30` `count_prime_113_le_29` `count_prime_109_le_28` `count_prime_107_le_27` `count_prime_103_le_26` `count_prime_101_le_25` `count_prime_97_le_24` `count_prime_89_le_23` `count_prime_83_le_22` `count_prime_79_le_21` `count_prime_73_le_20` `count_prime_71_le_19` `count_prime_67_le_18` `count_prime_61_le_17` `count_prime_59_le_16` `count_prime_53_le_15` `count_prime_47_le_14` `count_prime_43_le_13` `count_prime_41_le_12` `count_prime_37_le_11` `count_prime_31_le_10` `count_prime_29_le_9` `count_prime_23_le_8` `count_prime_19_le_7` `count_prime_17_le_6` `count_prime_13_le_5` `count_prime_11_le_4` `count_prime_7_le_3` `count_prime_5_le_2` `count_prime_3_le_1`
`pi_nth_prime'` 📖	mathematical	—	`pi` `nth_prime'`	—	—

---