Step Hyp Ref
Expression 1 ral0 3934 . . . 4
2 oveq2 6304 . . . . . 6
3 fzo0 11849 . . . . . 6
4 2 , 3 syl6eq 2514 . . . . 5
5 4 raleqdv 3060 . . . 4
6 1 , 5 mpbiri 233 . . 3
7 6 a1d 25 . 2
8 simprl 756 . . . . . . . 8
9 lencl 12562 . . . . . . . . . . 11
10 1nn0 10836 . . . . . . . . . . . . . 14
11 10 a1i 11 . . . . . . . . . . . . 13
12 df-ne 2654 . . . . . . . . . . . . . . . 16
13 elnnne0 10834 . . . . . . . . . . . . . . . . 17
14 13 simplbi2com 627 . . . . . . . . . . . . . . . 16
15 12 , 14 sylbir 213 . . . . . . . . . . . . . . 15
16 15 adantr 465 . . . . . . . . . . . . . 14
17 16 impcom 430 . . . . . . . . . . . . 13
18 df-ne 2654 . . . . . . . . . . . . . . . 16
19 18 biimpri 206 . . . . . . . . . . . . . . 15
20 19 ad2antll 728 . . . . . . . . . . . . . 14
21 nngt1ne1 10588 . . . . . . . . . . . . . . 15
22 17 , 21 syl 16 . . . . . . . . . . . . . 14
23 20 , 22 mpbird 232 . . . . . . . . . . . . 13
24 elfzo0 11863 . . . . . . . . . . . . 13
25 11 , 17 , 23 , 24 syl3anbrc 1180 . . . . . . . . . . . 12
26 25 ex 434 . . . . . . . . . . 11
27 9 , 26 syl 16 . . . . . . . . . 10
28 27 adantr 465 . . . . . . . . 9
29 28 impcom 430 . . . . . . . 8
30 simprr 757 . . . . . . . 8
31 lbfzo0 11862 . . . . . . . . . . . . . . . . 17
32 31 biimpri 206 . . . . . . . . . . . . . . . 16
33 13 , 32 sylbir 213 . . . . . . . . . . . . . . 15
34 33 ex 434 . . . . . . . . . . . . . 14
35 12 , 34 syl5bir 218 . . . . . . . . . . . . 13
36 9 , 35 syl 16 . . . . . . . . . . . 12
37 36 adantr 465 . . . . . . . . . . 11
38 37 com12 31 . . . . . . . . . 10
39 38 adantr 465 . . . . . . . . 9
40 39 imp 429 . . . . . . . 8
41 elfzoelz 11829 . . . . . . . . . 10
42 cshweqrep 12789 . . . . . . . . . 10
43 41 , 42 sylan2 474 . . . . . . . . 9
44 43 imp 429 . . . . . . . 8
45 8 , 29 , 30 , 40 , 44 syl22anc 1229 . . . . . . 7
46 0nn0 10835 . . . . . . . . 9
47 fzossnn0 11856 . . . . . . . . 9
48 ssralv 3563 . . . . . . . . 9
49 46 , 47 , 48 mp2b 10 . . . . . . . 8
50 eqcom 2466 . . . . . . . . . 10
51 elfzoelz 11829 . . . . . . . . . . . . . . . 16
52 zre 10893 . . . . . . . . . . . . . . . . . . 19
53 ax-1rid 9583 . . . . . . . . . . . . . . . . . . 19
54 52 , 53 syl 16 . . . . . . . . . . . . . . . . . 18
55 54 oveq2d 6312 . . . . . . . . . . . . . . . . 17
56 zcn 10894 . . . . . . . . . . . . . . . . . 18
57 56 addid2d 9802 . . . . . . . . . . . . . . . . 17
58 55 , 57 eqtrd 2498 . . . . . . . . . . . . . . . 16
59 51 , 58 syl 16 . . . . . . . . . . . . . . 15
60 59 oveq1d 6311 . . . . . . . . . . . . . 14
61 zmodidfzoimp 12026 . . . . . . . . . . . . . 14
62 60 , 61 eqtrd 2498 . . . . . . . . . . . . 13
63 62 fveq2d 5875 . . . . . . . . . . . 12
64 63 eqeq1d 2459 . . . . . . . . . . 11
65 64 biimpd 207 . . . . . . . . . 10
66 50 , 65 syl5bi 217 . . . . . . . . 9
67 66 ralimia 2848 . . . . . . . 8
68 49 , 67 syl 16 . . . . . . 7
69 45 , 68 syl 16 . . . . . 6
70 69 ex 434 . . . . 5
71 70 impancom 440 . . . 4
72 eqid 2457 . . . . . 6
73 c0ex 9611 . . . . . . 7
74 fveq2 5871 . . . . . . . 8
75 74 eqeq1d 2459 . . . . . . 7
76 73 , 75 ralsn 4068 . . . . . 6
77 72 , 76 mpbir 209 . . . . 5
78 oveq2 6304 . . . . . . 7
79 fzo01 11897 . . . . . . 7
80 78 , 79 syl6eq 2514 . . . . . 6
81 80 raleqdv 3060 . . . . 5
82 77 , 81 mpbiri 233 . . . 4
83 71 , 82 pm2.61d2 160 . . 3
84 83 ex 434 . 2
85 7 , 84 pm2.61i 164 1
