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+12−x
dnibndlem3.2 ⊢φ→A∈ℝ
dnibndlem3.3 ⊢φ→B∈ℝ
dnibndlem3.4 ⊢φ→B+12=A+12+1
Assertion dnibndlem3 ⊢φ→B−A=B−B+12−12+A+12+12-A

Proof

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