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	⊢ ( 𝑥 = 1 → ( 𝜑 ↔ 𝜓 ) )
	prmind.2	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜒 ) )
	prmind.3	⊢ ( 𝑥 = 𝑧 → ( 𝜑 ↔ 𝜃 ) )
	prmind.4	⊢ ( 𝑥 = ( 𝑦 · 𝑧 ) → ( 𝜑 ↔ 𝜏 ) )
	prmind.5	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜂 ) )
	prmind.6	⊢ 𝜓
	prmind.7	⊢ ( 𝑥 ∈ ℙ → 𝜑 )
	prmind.8	⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝜒 ∧ 𝜃 ) → 𝜏 ) )
Assertion	prmind	⊢ ( 𝐴 ∈ ℕ → 𝜂 )

Proof

Step	Hyp	Ref	Expression
1		prmind.1	⊢ ( 𝑥 = 1 → ( 𝜑 ↔ 𝜓 ) )
2		prmind.2	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜒 ) )
3		prmind.3	⊢ ( 𝑥 = 𝑧 → ( 𝜑 ↔ 𝜃 ) )
4		prmind.4	⊢ ( 𝑥 = ( 𝑦 · 𝑧 ) → ( 𝜑 ↔ 𝜏 ) )
5		prmind.5	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜂 ) )
6		prmind.6	⊢ 𝜓
7		prmind.7	⊢ ( 𝑥 ∈ ℙ → 𝜑 )
8		prmind.8	⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝜒 ∧ 𝜃 ) → 𝜏 ) )
9	7	adantr	⊢ ( ( 𝑥 ∈ ℙ ∧ ∀ 𝑦 ∈ ( 1 ... ( 𝑥 − 1 ) ) 𝜒 ) → 𝜑 )
10	1 2 3 4 5 6 9 8	prmind2	⊢ ( 𝐴 ∈ ℕ → 𝜂 )