Theorem 2elfz3nn0

Description: If there are two elements in a finite set of sequential integers starting at 0, these two elements as well as the upper bound are nonnegative integers. (Contributed by Alexander van der Vekens, 7-Apr-2018)

	Ref	Expression
Assertion	2elfz3nn0	⊢ ( ( 𝐴 ∈ ( 0 ... 𝑁 ) ∧ 𝐵 ∈ ( 0 ... 𝑁 ) ) → ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) )

Proof

Step	Hyp	Ref	Expression
1		elfznn0	⊢ ( 𝐴 ∈ ( 0 ... 𝑁 ) → 𝐴 ∈ ℕ0 )
2		elfz2nn0	⊢ ( 𝐵 ∈ ( 0 ... 𝑁 ) ↔ ( 𝐵 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝐵 ≤ 𝑁 ) )
3		3anass	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ↔ ( 𝐴 ∈ ℕ0 ∧ ( 𝐵 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) )
4	3	simplbi2com	⊢ ( ( 𝐵 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ∈ ℕ0 → ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) )
5	4	3adant3	⊢ ( ( 𝐵 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝐵 ≤ 𝑁 ) → ( 𝐴 ∈ ℕ0 → ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) )
6	2 5	sylbi	⊢ ( 𝐵 ∈ ( 0 ... 𝑁 ) → ( 𝐴 ∈ ℕ0 → ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) )
7	1 6	mpan9	⊢ ( ( 𝐴 ∈ ( 0 ... 𝑁 ) ∧ 𝐵 ∈ ( 0 ... 𝑁 ) ) → ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) )