Step Hyp Ref
Expression 1 posdif 10070 . . . 4
2 resubcl 9906 . . . . . . 7
3 nnrecl 10818 . . . . . . 7
4 2 , 3 sylan 471 . . . . . 6
5 4 ex 434 . . . . 5
6 5 ancoms 453 . . . 4
7 1 , 6 sylbid 215 . . 3
8 nnre 10568 . . . . . . . . 9
9 8 adantl 466 . . . . . . . 8
10 simplr 755 . . . . . . . 8
11 9 , 10 remulcld 9645 . . . . . . 7
12 peano2rem 9909 . . . . . . 7
13 11 , 12 syl 16 . . . . . 6
14 zbtwnre 11209 . . . . . 6
15 reurex 3074 . . . . . 6
16 13 , 14 , 15 3syl 20 . . . . 5
17 znq 11215 . . . . . . . . . . 11
18 17 ancoms 453 . . . . . . . . . 10
19 18 adantl 466 . . . . . . . . 9
20 an32 798 . . . . . . . . . 10
21 8 ad2antrl 727 . . . . . . . . . . . . . 14
22 simpll 753 . . . . . . . . . . . . . 14
23 21 , 22 remulcld 9645 . . . . . . . . . . . . 13
24 13 adantrr 716 . . . . . . . . . . . . 13
25 zre 10893 . . . . . . . . . . . . . 14
26 25 ad2antll 728 . . . . . . . . . . . . 13
27 ltletr 9697 . . . . . . . . . . . . 13
28 23 , 24 , 26 , 27 syl3anc 1228 . . . . . . . . . . . 12
29 21 recnd 9643 . . . . . . . . . . . . . . . . 17
30 simplr 755 . . . . . . . . . . . . . . . . . 18
31 30 recnd 9643 . . . . . . . . . . . . . . . . 17
32 22 recnd 9643 . . . . . . . . . . . . . . . . 17
33 29 , 31 , 32 subdid 10037 . . . . . . . . . . . . . . . 16
34 33 breq2d 4464 . . . . . . . . . . . . . . 15
35 1red 9632 . . . . . . . . . . . . . . . 16
36 30 , 22 resubcld 10012 . . . . . . . . . . . . . . . 16
37 nngt0 10590 . . . . . . . . . . . . . . . . 17
38 37 ad2antrl 727 . . . . . . . . . . . . . . . 16
39 ltdivmul 10442 . . . . . . . . . . . . . . . 16
40 35 , 36 , 21 , 38 , 39 syl112anc 1232 . . . . . . . . . . . . . . 15
41 11 adantrr 716 . . . . . . . . . . . . . . . 16
42 ltsub13 10058 . . . . . . . . . . . . . . . 16
43 23 , 41 , 35 , 42 syl3anc 1228 . . . . . . . . . . . . . . 15
44 34 , 40 , 43 3bitr4rd 286 . . . . . . . . . . . . . 14
45 44 anbi1d 704 . . . . . . . . . . . . 13
46 ancom 450 . . . . . . . . . . . . 13
47 45 , 46 syl6bb 261 . . . . . . . . . . . 12
48 ltmuldiv2 10441 . . . . . . . . . . . . 13
49 22 , 26 , 21 , 38 , 48 syl112anc 1232 . . . . . . . . . . . 12
50 28 , 47 , 49 3imtr3d 267 . . . . . . . . . . 11
51 41 recnd 9643 . . . . . . . . . . . . . . 15
52 ax-1cn 9571 . . . . . . . . . . . . . . 15
53 npcan 9852 . . . . . . . . . . . . . . 15
54 51 , 52 , 53 sylancl 662 . . . . . . . . . . . . . 14
55 54 breq2d 4464 . . . . . . . . . . . . 13
56 ltdivmul 10442 . . . . . . . . . . . . . 14
57 26 , 30 , 21 , 38 , 56 syl112anc 1232 . . . . . . . . . . . . 13
58 55 , 57 bitr4d 256 . . . . . . . . . . . 12
59 58 biimpd 207 . . . . . . . . . . 11
60 50 , 59 anim12d 563 . . . . . . . . . 10
61 20 , 60 syl5bi 217 . . . . . . . . 9
62 breq2 4456 . . . . . . . . . . 11
63 breq1 4455 . . . . . . . . . . 11
64 62 , 63 anbi12d 710 . . . . . . . . . 10
65 64 rspcev 3210 . . . . . . . . 9
66 19 , 61 , 65 syl6an 545 . . . . . . . 8
67 66 expd 436 . . . . . . 7
68 67 expr 615 . . . . . 6
69 68 rexlimdv 2947 . . . . 5
70 16 , 69 mpd 15 . . . 4
71 70 rexlimdva 2949 . . 3
72 7 , 71 syld 44 . 2
73 72 3impia 1193 1
