Description: A variation on prmind assuming complete induction for primes. (Contributed by Mario Carneiro, 20-Jun-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | prmind.1 | |
|
prmind.2 | |
||
prmind.3 | |
||
prmind.4 | |
||
prmind.5 | |
||
prmind.6 | |
||
prmind2.7 | |
||
prmind2.8 | |
||
Assertion | prmind2 | |