Metamath Proof Explorer


Theorem lediv23

Description: Swap denominator with other side of 'less than or equal to'. (Contributed by NM, 30-May-2005)

Ref Expression
Assertion lediv23 A B 0 < B C 0 < C A B C A C B

Proof

Step Hyp Ref Expression
1 simpl B 0 < B B
2 gt0ne0 B 0 < B B 0
3 1 2 jca B 0 < B B B 0
4 redivcl A B B 0 A B
5 4 3expb A B B 0 A B
6 3 5 sylan2 A B 0 < B A B
7 6 3adant3 A B 0 < B C A B
8 simp3 A B 0 < B C C
9 simp2 A B 0 < B C B 0 < B
10 lemul1 A B C B 0 < B A B C A B B C B
11 7 8 9 10 syl3anc A B 0 < B C A B C A B B C B
12 11 3adant3r A B 0 < B C 0 < C A B C A B B C B
13 recn A A
14 13 adantr A B 0 < B A
15 recn B B
16 15 ad2antrl A B 0 < B B
17 2 adantl A B 0 < B B 0
18 14 16 17 divcan1d A B 0 < B A B B = A
19 18 3adant3 A B 0 < B C 0 < C A B B = A
20 19 breq1d A B 0 < B C 0 < C A B B C B A C B
21 remulcl C B C B
22 21 ancoms B C C B
23 22 adantrr B C 0 < C C B
24 23 3adant1 A B C 0 < C C B
25 lediv1 A C B C 0 < C A C B A C C B C
26 24 25 syld3an2 A B C 0 < C A C B A C C B C
27 recn C C
28 27 adantr C 0 < C C
29 gt0ne0 C 0 < C C 0
30 28 29 jca C 0 < C C C 0
31 divcan3 B C C 0 C B C = B
32 31 3expb B C C 0 C B C = B
33 15 30 32 syl2an B C 0 < C C B C = B
34 33 3adant1 A B C 0 < C C B C = B
35 34 breq2d A B C 0 < C A C C B C A C B
36 26 35 bitrd A B C 0 < C A C B A C B
37 36 3adant2r A B 0 < B C 0 < C A C B A C B
38 12 20 37 3bitrd A B 0 < B C 0 < C A B C A C B