This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝐴 ∈ ℕ → 𝜂 )