Description: Convert a theorem for real/complex numbers into one for positive integers. (Contributed by Jeff Hoffman, 17-Jun-2008)
Ref | Expression | ||
---|---|---|---|
Hypotheses | nnssi2.1 | ⊢ ℕ ⊆ 𝐷 | |
nnssi2.2 | ⊢ ( 𝐵 ∈ ℕ → 𝜑 ) | ||
nnssi2.3 | ⊢ ( ( 𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝜑 ) → 𝜓 ) | ||
Assertion | nnssi2 | ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → 𝜓 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nnssi2.1 | ⊢ ℕ ⊆ 𝐷 | |
2 | nnssi2.2 | ⊢ ( 𝐵 ∈ ℕ → 𝜑 ) | |
3 | nnssi2.3 | ⊢ ( ( 𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝜑 ) → 𝜓 ) | |
4 | 1 | sseli | ⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ 𝐷 ) |
5 | 1 | sseli | ⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ 𝐷 ) |
6 | 4 5 2 | 3anim123i | ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝜑 ) ) |
7 | 6 | 3anidm23 | ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝜑 ) ) |
8 | 7 3 | syl | ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → 𝜓 ) |