Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  efltlemlt Unicode version

Theorem efltlemlt 12878
 Description: Lemma for eflt 12879. The converse of efltim 11416 plus the epsilon-delta setup. (Contributed by Jim Kingdon, 22-May-2024.)
Hypotheses
Ref Expression
efltlemlt.a
efltlemlt.b
efltlemlt.lt
efltlemlt.d
efltlemlt.ed
Assertion
Ref Expression
efltlemlt

Proof of Theorem efltlemlt
StepHypRef Expression
1 efltlemlt.lt . . . . 5
21ad2antrr 479 . . . 4
3 efltlemlt.b . . . . . . 7
43ad2antrr 479 . . . . . 6
54reefcld 11387 . . . . 5
6 efltlemlt.a . . . . . . 7
76ad2antrr 479 . . . . . 6
87reefcld 11387 . . . . 5
96adantr 274 . . . . . . 7
10 efltim 11416 . . . . . . 7
113, 9, 10syl2an2r 584 . . . . . 6
1211imp 123 . . . . 5
135, 8, 12ltnsymd 7894 . . . 4
142, 13pm2.21dd 609 . . 3
156reefcld 11387 . . . . . . 7
163reefcld 11387 . . . . . . 7
1715, 16, 1ltled 7893 . . . . . . 7
1815, 16, 17abssuble0d 10961 . . . . . 6
1918ad2antrr 479 . . . . 5
20 efltlemlt.d . . . . . . . . . 10
2120rpred 9495 . . . . . . . . 9
226, 3, 21absdifltd 10962 . . . . . . . 8
2322biimprd 157 . . . . . . 7
2423impl 377 . . . . . 6
25 efltlemlt.ed . . . . . . 7
2625ad2antrr 479 . . . . . 6
2724, 26mpd 13 . . . . 5
2819, 27eqbrtrrd 3952 . . . 4
2916, 15resubcld 8155 . . . . . 6
3029ad2antrr 479 . . . . 5
3130ltnrd 7887 . . . 4
3228, 31pm2.21dd 609 . . 3
333, 20ltaddrpd 9529 . . . . 5
343, 21readdcld 7807 . . . . . 6
35 axltwlin 7844 . . . . . 6
363, 34, 6, 35syl3anc 1216 . . . . 5
3733, 36mpd 13 . . . 4