Step Hyp Ref
Expression 1 df-3an 975 . . . . 5
2 1 biimpri 206 . . . 4
3 2 3adant2 1015 . . 3
4 ssfzo12 11905 . . 3
5 3 , 4 syl 16 . 2
6 elfzo2 11832 . . . . . 6
7 eluz2 11116 . . . . . . . . 9
8 simprrl 765 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
9 8 adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . 26
10 simpll 753 . . . . . . . . . . . . . . . . . . . . . . . . . 26
11 zre 10893 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
12 11 adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
13 12 adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
14 13 adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
15 zre 10893 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
16 15 adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
17 16 adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
18 17 adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
19 zre 10893 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
20 19 adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
21 letr 9699 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
22 14 , 18 , 20 , 21 syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
23 22 imp 429 . . . . . . . . . . . . . . . . . . . . . . . . . 26
24 9 , 10 , 23 3jca 1176 . . . . . . . . . . . . . . . . . . . . . . . . 25
25 24 exp31 604 . . . . . . . . . . . . . . . . . . . . . . . 24
26 25 com23 78 . . . . . . . . . . . . . . . . . . . . . . 23
27 26 expdimp 437 . . . . . . . . . . . . . . . . . . . . . 22
28 27 impancom 440 . . . . . . . . . . . . . . . . . . . . 21
29 28 com13 80 . . . . . . . . . . . . . . . . . . . 20
30 29 3adant3 1016 . . . . . . . . . . . . . . . . . . 19
31 30 com12 31 . . . . . . . . . . . . . . . . . 18
32 31 adantr 465 . . . . . . . . . . . . . . . . 17
33 32 impcom 430 . . . . . . . . . . . . . . . 16
34 33 com12 31 . . . . . . . . . . . . . . 15
35 34 adantr 465 . . . . . . . . . . . . . 14
36 35 imp 429 . . . . . . . . . . . . 13
37 eluz2 11116 . . . . . . . . . . . . 13
38 36 , 37 sylibr 212 . . . . . . . . . . . 12
39 simpl2r 1050 . . . . . . . . . . . . 13
40 39 adantl 466 . . . . . . . . . . . 12
41 19 adantl 466 . . . . . . . . . . . . . . . . . . . . . . 23
42 zre 10893 . . . . . . . . . . . . . . . . . . . . . . . 24
43 42 ad3antlr 730 . . . . . . . . . . . . . . . . . . . . . . 23
44 zre 10893 . . . . . . . . . . . . . . . . . . . . . . . . . 26
45 44 adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . 25
46 45 adantl 466 . . . . . . . . . . . . . . . . . . . . . . . 24
47 46 adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23
48 ltletr 9697 . . . . . . . . . . . . . . . . . . . . . . 23
49 41 , 43 , 47 , 48 syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . 22
50 49 ex 434 . . . . . . . . . . . . . . . . . . . . 21
51 50 com23 78 . . . . . . . . . . . . . . . . . . . 20
52 51 3adant3 1016 . . . . . . . . . . . . . . . . . . 19
53 52 expcomd 438 . . . . . . . . . . . . . . . . . 18
54 53 adantld 467 . . . . . . . . . . . . . . . . 17
55 54 imp 429 . . . . . . . . . . . . . . . 16
56 55 com13 80 . . . . . . . . . . . . . . 15
57 56 adantr 465 . . . . . . . . . . . . . 14
58 57 imp 429 . . . . . . . . . . . . 13
59 58 imp 429 . . . . . . . . . . . 12
60 elfzo2 11832 . . . . . . . . . . . 12
61 38 , 40 , 59 , 60 syl3anbrc 1180 . . . . . . . . . . 11
62 61 exp31 604 . . . . . . . . . 10
63 62 3adant1 1014 . . . . . . . . 9
64 7 , 63 sylbi 195 . . . . . . . 8
65 64 imp 429 . . . . . . 7
66 65 3adant2 1015 . . . . . 6
67 6 , 66 sylbi 195 . . . . 5
68 67 com12 31 . . . 4
69 68 ssrdv 3509 . . 3
70 69 ex 434 . 2
71 5 , 70 impbid 191 1
