Metamath Proof Explorer

Theorem dnibndlem5

Description: Lemma for dnibnd . (Contributed by Asger C. Ipsen, 4-Apr-2021)

Ref Expression
Assertion dnibndlem5 ⊢ A ∈ ℝ → 0 < A + 1 2 + 1 2 - A

Proof

Step Hyp Ref Expression
1 id ⊢ A ∈ ℝ → A ∈ ℝ
2 halfre ⊢ 1 2 ∈ ℝ
3 2 a1i ⊢ A ∈ ℝ → 1 2 ∈ ℝ
4 readdcl ⊢ A ∈ ℝ ∧ 1 2 ∈ ℝ → A + 1 2 ∈ ℝ
5 1 3 4 syl2anc2 ⊢ A ∈ ℝ → A + 1 2 ∈ ℝ
6 flltp1 ⊢ A + 1 2 ∈ ℝ → A + 1 2 < A + 1 2 + 1
7 5 6 syl ⊢ A ∈ ℝ → A + 1 2 < A + 1 2 + 1
8 ax-1cn ⊢ 1 ∈ ℂ
9 2halves ⊢ 1 ∈ ℂ → 1 2 + 1 2 = 1
10 8 9 ax-mp ⊢ 1 2 + 1 2 = 1
11 10 eqcomi ⊢ 1 = 1 2 + 1 2
12 11 a1i ⊢ A ∈ ℝ → 1 = 1 2 + 1 2
13 12 oveq2d ⊢ A ∈ ℝ → A + 1 2 + 1 = A + 1 2 + 1 2 + 1 2
14 reflcl ⊢ A + 1 2 ∈ ℝ → A + 1 2 ∈ ℝ
15 5 14 syl ⊢ A ∈ ℝ → A + 1 2 ∈ ℝ
16 15 recnd ⊢ A ∈ ℝ → A + 1 2 ∈ ℂ
17 3 recnd ⊢ A ∈ ℝ → 1 2 ∈ ℂ
18 16 17 17 3jca ⊢ A ∈ ℝ → A + 1 2 ∈ ℂ ∧ 1 2 ∈ ℂ ∧ 1 2 ∈ ℂ
19 addass ⊢ A + 1 2 ∈ ℂ ∧ 1 2 ∈ ℂ ∧ 1 2 ∈ ℂ → A + 1 2 + 1 2 + 1 2 = A + 1 2 + 1 2 + 1 2
20 18 19 syl ⊢ A ∈ ℝ → A + 1 2 + 1 2 + 1 2 = A + 1 2 + 1 2 + 1 2
21 20 eqcomd ⊢ A ∈ ℝ → A + 1 2 + 1 2 + 1 2 = A + 1 2 + 1 2 + 1 2
22 13 21 eqtrd ⊢ A ∈ ℝ → A + 1 2 + 1 = A + 1 2 + 1 2 + 1 2
23 7 22 breqtrd ⊢ A ∈ ℝ → A + 1 2 < A + 1 2 + 1 2 + 1 2
24 15 3 jca ⊢ A ∈ ℝ → A + 1 2 ∈ ℝ ∧ 1 2 ∈ ℝ
25 readdcl ⊢ A + 1 2 ∈ ℝ ∧ 1 2 ∈ ℝ → A + 1 2 + 1 2 ∈ ℝ
26 24 25 syl ⊢ A ∈ ℝ → A + 1 2 + 1 2 ∈ ℝ
27 1 26 3 ltadd1d ⊢ A ∈ ℝ → A < A + 1 2 + 1 2 ↔ A + 1 2 < A + 1 2 + 1 2 + 1 2
28 23 27 mpbird ⊢ A ∈ ℝ → A < A + 1 2 + 1 2
29 1 26 posdifd ⊢ A ∈ ℝ → A < A + 1 2 + 1 2 ↔ 0 < A + 1 2 + 1 2 - A
30 28 29 mpbid ⊢ A ∈ ℝ → 0 < A + 1 2 + 1 2 - A