Theorem le9lt10

Description: A "decimal digit" (i.e. a nonnegative integer less than or equal to 9) is less than 10. (Contributed by AV, 8-Sep-2021)

	Ref	Expression
Hypotheses	le9lt10.c	⊢ 𝐴 ∈ ℕ0
	le9lt10.e	⊢ 𝐴 ≤ 9
Assertion	le9lt10	⊢ 𝐴 < ; 1 0

Proof

Step	Hyp	Ref	Expression
1		le9lt10.c	⊢ 𝐴 ∈ ℕ0
2		le9lt10.e	⊢ 𝐴 ≤ 9
3	1	nn0zi	⊢ 𝐴 ∈ ℤ
4		9nn0	⊢ 9 ∈ ℕ0
5	4	nn0zi	⊢ 9 ∈ ℤ
6		zleltp1	⊢ ( ( 𝐴 ∈ ℤ ∧ 9 ∈ ℤ ) → ( 𝐴 ≤ 9 ↔ 𝐴 < ( 9 + 1 ) ) )
7	3 5 6	mp2an	⊢ ( 𝐴 ≤ 9 ↔ 𝐴 < ( 9 + 1 ) )
8	2 7	mpbi	⊢ 𝐴 < ( 9 + 1 )
9		9p1e10	⊢ ( 9 + 1 ) = ; 1 0
10	8 9	breqtri	⊢ 𝐴 < ; 1 0