Step Hyp Ref
Expression 1 fzo0ss1 11855 . . . . . . . . 9
2 fzossfz 11846 . . . . . . . . 9
3 1 , 2 sstri 3512 . . . . . . . 8
4 fssres 5756 . . . . . . . 8
5 3 , 4 mpan2 671 . . . . . . 7
6 5 biantrud 507 . . . . . 6
7 ancom 450 . . . . . . 7
8 df-f1 5598 . . . . . . 7
9 7 , 8 bitr4i 252 . . . . . 6
10 6 , 9 syl6bb 261 . . . . 5
11 simp-4r 768 . . . . . . . . 9
12 dff13 6166 . . . . . . . . . . . . . . 15
13 fveq2 5871 . . . . . . . . . . . . . . . . . . . . . . . . . 26
14 13 eqeq1d 2459 . . . . . . . . . . . . . . . . . . . . . . . . 25
15 equequ1 1798 . . . . . . . . . . . . . . . . . . . . . . . . 25
16 14 , 15 imbi12d 320 . . . . . . . . . . . . . . . . . . . . . . . 24
17 fveq2 5871 . . . . . . . . . . . . . . . . . . . . . . . . . 26
18 17 eqeq2d 2471 . . . . . . . . . . . . . . . . . . . . . . . . 25
19 equequ2 1799 . . . . . . . . . . . . . . . . . . . . . . . . 25
20 18 , 19 imbi12d 320 . . . . . . . . . . . . . . . . . . . . . . . 24
21 16 , 20 rspc2va 3220 . . . . . . . . . . . . . . . . . . . . . . 23
22 fvres 5885 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
23 22 eqcomd 2465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
24 fvres 5885 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
25 24 eqcomd 2465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
26 23 , 25 eqeqan12d 2480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
27 26 biimpd 207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
28 27 imim1d 75 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
29 28 imp 429 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
30 29 a1d 25 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
31 30 a1d 25 . . . . . . . . . . . . . . . . . . . . . . . . . 26
32 31 a1d 25 . . . . . . . . . . . . . . . . . . . . . . . . 25
33 32 a1d 25 . . . . . . . . . . . . . . . . . . . . . . . 24
34 33 expcom 435 . . . . . . . . . . . . . . . . . . . . . . 23
35 21 , 34 syl 16 . . . . . . . . . . . . . . . . . . . . . 22
36 35 ex 434 . . . . . . . . . . . . . . . . . . . . 21
37 36 pm2.43a 49 . . . . . . . . . . . . . . . . . . . 20
38 ianor 488 . . . . . . . . . . . . . . . . . . . . 21
39 eqcom 2466 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
40 injresinjlem 11925 . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
41 40 imp 429 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
42 41 imp41 593 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
43 eqcom 2466 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
44 42 , 43 syl6ib 226 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
45 39 , 44 syl5bi 217 . . . . . . . . . . . . . . . . . . . . . . . . . 26
46 45 ex 434 . . . . . . . . . . . . . . . . . . . . . . . . 25
47 46 ancomsd 454 . . . . . . . . . . . . . . . . . . . . . . . 24
48 47 exp41 610 . . . . . . . . . . . . . . . . . . . . . . 23
49 injresinjlem 11925 . . . . . . . . . . . . . . . . . . . . . . 23
50 48 , 49 jaoi 379 . . . . . . . . . . . . . . . . . . . . . 22
51 50 a1d 25 . . . . . . . . . . . . . . . . . . . . 21
52 38 , 51 sylbi 195 . . . . . . . . . . . . . . . . . . . 20
53 37 , 52 pm2.61i 164 . . . . . . . . . . . . . . . . . . 19
54 53 imp41 593 . . . . . . . . . . . . . . . . . 18
55 54 ralrimivv 2877 . . . . . . . . . . . . . . . . 17
56 55 exp41 610 . . . . . . . . . . . . . . . 16
57 56 adantl 466 . . . . . . . . . . . . . . 15
58 12 , 57 sylbi 195 . . . . . . . . . . . . . 14
59 58 com13 80 . . . . . . . . . . . . 13
60 59 ex 434 . . . . . . . . . . . 12
61 60 com24 87 . . . . . . . . . . 11
62 61 impcom 430 . . . . . . . . . 10
63 62 imp41 593 . . . . . . . . 9
64 dff13 6166 . . . . . . . . 9
65 11 , 63 , 64 sylanbrc 664 . . . . . . . 8
66 11 biantrurd 508 . . . . . . . . 9
67 df-f1 5598 . . . . . . . . 9
68 66 , 67 syl6bbr 263 . . . . . . . 8
69 65 , 68 mpbird 232 . . . . . . 7
70 69 ex 434 . . . . . 6
71 70 exp41 610 . . . . 5
72 10 , 71 syl6bi 228 . . . 4
73 72 pm2.43a 49 . . 3
74 73 3imp 1190 . 2
75 74 com12 31 1
