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 -> ( ph <-> ps ) )
	prmind.2	|- ( x = y -> ( ph <-> ch ) )
	prmind.3	|- ( x = z -> ( ph <-> th ) )
	prmind.4	|- ( x = ( y x. z ) -> ( ph <-> ta ) )
	prmind.5	|- ( x = A -> ( ph <-> et ) )
	prmind.6	|- ps
	prmind.7	|- ( x e. Prime -> ph )
	prmind.8	|- ( ( y e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) -> ( ( ch /\ th ) -> ta ) )
Assertion	prmind	|- ( A e. NN -> et )

Proof

Step	Hyp	Ref	Expression
1		prmind.1	|- ( x = 1 -> ( ph <-> ps ) )
2		prmind.2	|- ( x = y -> ( ph <-> ch ) )
3		prmind.3	|- ( x = z -> ( ph <-> th ) )
4		prmind.4	|- ( x = ( y x. z ) -> ( ph <-> ta ) )
5		prmind.5	|- ( x = A -> ( ph <-> et ) )
6		prmind.6	|- ps
7		prmind.7	|- ( x e. Prime -> ph )
8		prmind.8	|- ( ( y e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) -> ( ( ch /\ th ) -> ta ) )
9	7	adantr	|- ( ( x e. Prime /\ A. y e. ( 1 ... ( x - 1 ) ) ch ) -> ph )
10	1 2 3 4 5 6 9 8	prmind2	|- ( A e. NN -> et )