Metamath Proof Explorer


Theorem dnibndlem13

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

Ref Expression
Hypotheses dnibndlem13.1 T=xx+12x
dnibndlem13.2 φA
dnibndlem13.3 φB
dnibndlem13.4 φA+12B+12
Assertion dnibndlem13 φTBTABA

Proof

Step Hyp Ref Expression
1 dnibndlem13.1 T=xx+12x
2 dnibndlem13.2 φA
3 dnibndlem13.3 φB
4 dnibndlem13.4 φA+12B+12
5 2 ad2antrr φA+12<B+12A+12+2B+12A
6 3 ad2antrr φA+12<B+12A+12+2B+12B
7 simpr φA+12<B+12A+12+2B+12A+12+2B+12
8 1 5 6 7 dnibndlem12 φA+12<B+12A+12+2B+12TBTABA
9 2 ad2antrr φA+12<B+12A+12+1=B+12A
10 3 ad2antrr φA+12<B+12A+12+1=B+12B
11 simpr φA+12<B+12A+12+1=B+12A+12+1=B+12
12 11 eqcomd φA+12<B+12A+12+1=B+12B+12=A+12+1
13 1 9 10 12 dnibndlem9 φA+12<B+12A+12+1=B+12TBTABA
14 simpr φA+12<B+12A+12<B+12
15 halfre 12
16 15 a1i φ12
17 2 16 readdcld φA+12
18 17 flcld φA+12
19 3 16 readdcld φB+12
20 19 flcld φB+12
21 18 20 jca φA+12B+12
22 21 adantr φA+12<B+12A+12B+12
23 zltp1le A+12B+12A+12<B+12A+12+1B+12
24 22 23 syl φA+12<B+12A+12<B+12A+12+1B+12
25 14 24 mpbid φA+12<B+12A+12+1B+12
26 reflcl A+12A+12
27 17 26 syl φA+12
28 peano2re A+12A+12+1
29 27 28 syl φA+12+1
30 29 adantr φA+12<B+12A+12+1
31 20 zred φB+12
32 31 adantr φA+12<B+12B+12
33 30 32 leloed φA+12<B+12A+12+1B+12A+12+1<B+12A+12+1=B+12
34 25 33 mpbid φA+12<B+12A+12+1<B+12A+12+1=B+12
35 18 peano2zd φA+12+1
36 35 20 jca φA+12+1B+12
37 zltp1le A+12+1B+12A+12+1<B+12A+12+1+1B+12
38 36 37 syl φA+12+1<B+12A+12+1+1B+12
39 27 recnd φA+12
40 1cnd φ1
41 39 40 40 addassd φA+12+1+1=A+12+1+1
42 1p1e2 1+1=2
43 42 a1i φ1+1=2
44 43 oveq2d φA+12+1+1=A+12+2
45 41 44 eqtrd φA+12+1+1=A+12+2
46 45 breq1d φA+12+1+1B+12A+12+2B+12
47 38 46 bitrd φA+12+1<B+12A+12+2B+12
48 47 biimpd φA+12+1<B+12A+12+2B+12
49 48 adantr φA+12<B+12A+12+1<B+12A+12+2B+12
50 49 orim1d φA+12<B+12A+12+1<B+12A+12+1=B+12A+12+2B+12A+12+1=B+12
51 34 50 mpd φA+12<B+12A+12+2B+12A+12+1=B+12
52 8 13 51 mpjaodan φA+12<B+12TBTABA
53 2 adantr φA+12=B+12A
54 3 adantr φA+12=B+12B
55 simpr φA+12=B+12A+12=B+12
56 55 eqcomd φA+12=B+12B+12=A+12
57 1 53 54 56 dnibndlem2 φA+12=B+12TBTABA
58 27 31 leloed φA+12B+12A+12<B+12A+12=B+12
59 4 58 mpbid φA+12<B+12A+12=B+12
60 52 57 59 mpjaodan φTBTABA