Metamath Proof Explorer

Theorem dnibndlem3

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

Ref Expression
Hypotheses dnibndlem3.1 ⊢ T = x ∈ ℝ ⟼ x + 1 2 − x
dnibndlem3.2 ⊢ φ → A ∈ ℝ
dnibndlem3.3 ⊢ φ → B ∈ ℝ
dnibndlem3.4 ⊢ φ → B + 1 2 = A + 1 2 + 1
Assertion dnibndlem3 ⊢ φ → B − A = B − B + 1 2 − 1 2 + A + 1 2 + 1 2 - A

Proof

Step Hyp Ref Expression
1 dnibndlem3.1 ⊢ T = x ∈ ℝ ⟼ x + 1 2 − x
2 dnibndlem3.2 ⊢ φ → A ∈ ℝ
3 dnibndlem3.3 ⊢ φ → B ∈ ℝ
4 dnibndlem3.4 ⊢ φ → B + 1 2 = A + 1 2 + 1
5 3 recnd ⊢ φ → B ∈ ℂ
6 halfre ⊢ 1 2 ∈ ℝ
7 6 a1i ⊢ φ → 1 2 ∈ ℝ
8 3 7 jca ⊢ φ → B ∈ ℝ ∧ 1 2 ∈ ℝ
9 readdcl ⊢ B ∈ ℝ ∧ 1 2 ∈ ℝ → B + 1 2 ∈ ℝ
10 8 9 syl ⊢ φ → B + 1 2 ∈ ℝ
11 reflcl ⊢ B + 1 2 ∈ ℝ → B + 1 2 ∈ ℝ
12 10 11 syl ⊢ φ → B + 1 2 ∈ ℝ
13 12 recnd ⊢ φ → B + 1 2 ∈ ℂ
14 halfcn ⊢ 1 2 ∈ ℂ
15 14 a1i ⊢ φ → 1 2 ∈ ℂ
16 13 15 subcld ⊢ φ → B + 1 2 − 1 2 ∈ ℂ
17 2 recnd ⊢ φ → A ∈ ℂ
18 5 16 17 3jca ⊢ φ → B ∈ ℂ ∧ B + 1 2 − 1 2 ∈ ℂ ∧ A ∈ ℂ
19 npncan ⊢ B ∈ ℂ ∧ B + 1 2 − 1 2 ∈ ℂ ∧ A ∈ ℂ → B − B + 1 2 − 1 2 + B + 1 2 − 1 2 - A = B − A
20 18 19 syl ⊢ φ → B − B + 1 2 − 1 2 + B + 1 2 − 1 2 - A = B − A
21 20 eqcomd ⊢ φ → B − A = B − B + 1 2 − 1 2 + B + 1 2 − 1 2 - A
22 4 oveq1d ⊢ φ → B + 1 2 − 1 2 = A + 1 2 + 1 - 1 2
23 2 7 jca ⊢ φ → A ∈ ℝ ∧ 1 2 ∈ ℝ
24 readdcl ⊢ A ∈ ℝ ∧ 1 2 ∈ ℝ → A + 1 2 ∈ ℝ
25 23 24 syl ⊢ φ → A + 1 2 ∈ ℝ
26 reflcl ⊢ A + 1 2 ∈ ℝ → A + 1 2 ∈ ℝ
27 25 26 syl ⊢ φ → A + 1 2 ∈ ℝ
28 27 recnd ⊢ φ → A + 1 2 ∈ ℂ
29 1cnd ⊢ φ → 1 ∈ ℂ
30 28 29 15 3jca ⊢ φ → A + 1 2 ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 2 ∈ ℂ
31 addsubass ⊢ A + 1 2 ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 2 ∈ ℂ → A + 1 2 + 1 - 1 2 = A + 1 2 + 1 - 1 2
32 30 31 syl ⊢ φ → A + 1 2 + 1 - 1 2 = A + 1 2 + 1 - 1 2
33 1mhlfehlf ⊢ 1 − 1 2 = 1 2
34 33 a1i ⊢ φ → 1 − 1 2 = 1 2
35 34 oveq2d ⊢ φ → A + 1 2 + 1 - 1 2 = A + 1 2 + 1 2
36 22 32 35 3eqtrd ⊢ φ → B + 1 2 − 1 2 = A + 1 2 + 1 2
37 36 oveq1d ⊢ φ → B + 1 2 - 1 2 - A = A + 1 2 + 1 2 - A
38 37 oveq2d ⊢ φ → B − B + 1 2 − 1 2 + B + 1 2 − 1 2 - A = B − B + 1 2 − 1 2 + A + 1 2 + 1 2 - A
39 21 38 eqtrd ⊢ φ → B − A = B − B + 1 2 − 1 2 + A + 1 2 + 1 2 - A
40 39 fveq2d ⊢ φ → B − A = B − B + 1 2 − 1 2 + A + 1 2 + 1 2 - A