Theorem prmind

Description: Perform induction over the multiplicative structure of NN . If a property ph ( x ) holds for the primes and 1 and is preserved under multiplication, then it holds for every positive integer. (Contributed by Mario Carneiro, 20-Jun-2015)

	Ref	Expression
Hypotheses	prmind.1	$$⊢x=1\to \left(\phi \leftrightarrow \psi \right)$$
	prmind.2	$$⊢x=y\to \left(\phi \leftrightarrow \chi \right)$$
	prmind.3	$$⊢x=z\to \left(\phi \leftrightarrow \theta \right)$$
	prmind.4	$$⊢x=yz\to \left(\phi \leftrightarrow \tau \right)$$
	prmind.5	$$⊢x=A\to \left(\phi \leftrightarrow \eta \right)$$
	prmind.6	$$⊢\psi$$
	prmind.7	$$⊢x\in \mathbb{P}\to \phi$$
	prmind.8	$$⊢\left(y\in {\mathbb{Z}}_{\ge 2}\wedge z\in {\mathbb{Z}}_{\ge 2}\right)\to \left(\left(\chi \wedge \theta \right)\to \tau \right)$$
Assertion	prmind	$$⊢A\in \mathbb{N}\to \eta$$

Proof

Step	Hyp	Ref	Expression
1		prmind.1	$$⊢x=1\to \left(\phi \leftrightarrow \psi \right)$$
2		prmind.2	$$⊢x=y\to \left(\phi \leftrightarrow \chi \right)$$
3		prmind.3	$$⊢x=z\to \left(\phi \leftrightarrow \theta \right)$$
4		prmind.4	$$⊢x=yz\to \left(\phi \leftrightarrow \tau \right)$$
5		prmind.5	$$⊢x=A\to \left(\phi \leftrightarrow \eta \right)$$
6		prmind.6	$$⊢\psi$$
7		prmind.7	$$⊢x\in \mathbb{P}\to \phi$$
8		prmind.8	$$⊢\left(y\in {\mathbb{Z}}_{\ge 2}\wedge z\in {\mathbb{Z}}_{\ge 2}\right)\to \left(\left(\chi \wedge \theta \right)\to \tau \right)$$
9	7	adantr	$$⊢\left(x\in \mathbb{P}\wedge \forall y\in \left(1\dots x-1\right)\chi \right)\to \phi$$
10	1 2 3 4 5 6 9 8	prmind2	$$⊢A\in \mathbb{N}\to \eta$$