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

Metamath Proof Explorer

Theorem dp2lt10

Description: Decimal fraction builds real numbers less than 10. (Contributed by Thierry Arnoux, 16-Dec-2021)

Ref Expression
Hypotheses dp2lt10.a ⊢ 𝐴 ∈ ℕ0
dp2lt10.b ⊢ 𝐵 ∈ ℝ+
dp2lt10.1 ⊢ 𝐴 < 1 0
dp2lt10.2 ⊢ 𝐵 < 1 0
Assertion dp2lt10 𝐴 𝐵 < 1 0

Proof

Step Hyp Ref Expression
1 dp2lt10.a ⊢ 𝐴 ∈ ℕ0
2 dp2lt10.b ⊢ 𝐵 ∈ ℝ+
3 dp2lt10.1 ⊢ 𝐴 < 1 0
4 dp2lt10.2 ⊢ 𝐵 < 1 0
5 df-dp2 ⊢ 𝐴 𝐵 = ( 𝐴 + ( 𝐵 / 1 0 ) )
6 9p1e10 ⊢ ( 9 + 1 ) = 1 0
7 3 6 breqtrri ⊢ 𝐴 < ( 9 + 1 )
8 1 nn0zi ⊢ 𝐴 ∈ ℤ
9 9nn0 ⊢ 9 ∈ ℕ0
10 9 nn0zi ⊢ 9 ∈ ℤ
11 zleltp1 ⊢ ( ( 𝐴 ∈ ℤ ∧ 9 ∈ ℤ ) → ( 𝐴 ≤ 9 ↔ 𝐴 < ( 9 + 1 ) ) )
12 8 10 11 mp2an ⊢ ( 𝐴 ≤ 9 ↔ 𝐴 < ( 9 + 1 ) )
13 7 12 mpbir ⊢ 𝐴 ≤ 9
14 rpssre ⊢ ℝ+ ⊆ ℝ
15 14 2 sselii ⊢ 𝐵 ∈ ℝ
16 10re ⊢ 1 0 ∈ ℝ
17 10pos ⊢ 0 < 1 0
18 16 17 elrpii ⊢ 1 0 ∈ ℝ+
19 divlt1lt ⊢ ( ( 𝐵 ∈ ℝ ∧ 1 0 ∈ ℝ+ ) → ( ( 𝐵 / 1 0 ) < 1 ↔ 𝐵 < 1 0 ) )
20 15 18 19 mp2an ⊢ ( ( 𝐵 / 1 0 ) < 1 ↔ 𝐵 < 1 0 )
21 4 20 mpbir ⊢ ( 𝐵 / 1 0 ) < 1
22 1 nn0rei ⊢ 𝐴 ∈ ℝ
23 0re ⊢ 0 ∈ ℝ
24 23 17 gtneii ⊢ 1 0 ≠ 0
25 15 16 24 redivcli ⊢ ( 𝐵 / 1 0 ) ∈ ℝ
26 22 25 pm3.2i ⊢ ( 𝐴 ∈ ℝ ∧ ( 𝐵 / 1 0 ) ∈ ℝ )
27 9re ⊢ 9 ∈ ℝ
28 1re ⊢ 1 ∈ ℝ
29 27 28 pm3.2i ⊢ ( 9 ∈ ℝ ∧ 1 ∈ ℝ )
30 leltadd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 / 1 0 ) ∈ ℝ ) ∧ ( 9 ∈ ℝ ∧ 1 ∈ ℝ ) ) → ( ( 𝐴 ≤ 9 ∧ ( 𝐵 / 1 0 ) < 1 ) → ( 𝐴 + ( 𝐵 / 1 0 ) ) < ( 9 + 1 ) ) )
31 26 29 30 mp2an ⊢ ( ( 𝐴 ≤ 9 ∧ ( 𝐵 / 1 0 ) < 1 ) → ( 𝐴 + ( 𝐵 / 1 0 ) ) < ( 9 + 1 ) )
32 13 21 31 mp2an ⊢ ( 𝐴 + ( 𝐵 / 1 0 ) ) < ( 9 + 1 )
33 32 6 breqtri ⊢ ( 𝐴 + ( 𝐵 / 1 0 ) ) < 1 0
34 5 33 eqbrtri ⊢ 𝐴 𝐵 < 1 0