Step Hyp Ref
Expression 1 elfz2nn0 11798 . . 3
2 elfz2nn0 11798 . . . . 5
3 elfzo0 11863 . . . . . . . 8
4 nn0z 10912 . . . . . . . . . . . . 13
5 nn0z 10912 . . . . . . . . . . . . 13
6 znnsub 10935 . . . . . . . . . . . . 13
7 4 , 5 , 6 syl2an 477 . . . . . . . . . . . 12
8 simpr 461 . . . . . . . . . . . . . . . 16
9 simpll 753 . . . . . . . . . . . . . . . 16
10 nn0addcl 10856 . . . . . . . . . . . . . . . 16
11 8 , 9 , 10 syl2anr 478 . . . . . . . . . . . . . . 15
12 11 adantr 465 . . . . . . . . . . . . . 14
13 0red 9618 . . . . . . . . . . . . . . . . . . . . . 22
14 nn0re 10829 . . . . . . . . . . . . . . . . . . . . . . 23
15 14 adantr 465 . . . . . . . . . . . . . . . . . . . . . 22
16 nn0re 10829 . . . . . . . . . . . . . . . . . . . . . . 23
17 16 adantl 466 . . . . . . . . . . . . . . . . . . . . . 22
18 13 , 15 , 17 3jca 1176 . . . . . . . . . . . . . . . . . . . . 21
19 18 adantr 465 . . . . . . . . . . . . . . . . . . . 20
20 nn0ge0 10846 . . . . . . . . . . . . . . . . . . . . . 22
21 20 adantr 465 . . . . . . . . . . . . . . . . . . . . 21
22 21 anim1i 568 . . . . . . . . . . . . . . . . . . . 20
23 lelttr 9696 . . . . . . . . . . . . . . . . . . . 20
24 19 , 22 , 23 sylc 60 . . . . . . . . . . . . . . . . . . 19
25 24 ex 434 . . . . . . . . . . . . . . . . . 18
26 0red 9618 . . . . . . . . . . . . . . . . . . . . . . . . 25
27 16 adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . 25
28 nn0re 10829 . . . . . . . . . . . . . . . . . . . . . . . . . 26
29 28 adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25
30 ltletr 9697 . . . . . . . . . . . . . . . . . . . . . . . . 25
31 26 , 27 , 29 , 30 syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . . 24
32 nn0z 10912 . . . . . . . . . . . . . . . . . . . . . . . . . 26
33 elnnz 10899 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
34 33 simplbi2 625 . . . . . . . . . . . . . . . . . . . . . . . . . 26
35 32 , 34 syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25
36 35 adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24
37 31 , 36 syld 44 . . . . . . . . . . . . . . . . . . . . . . 23
38 37 exp4b 607 . . . . . . . . . . . . . . . . . . . . . 22
39 38 com24 87 . . . . . . . . . . . . . . . . . . . . 21
40 39 imp 429 . . . . . . . . . . . . . . . . . . . 20
41 40 com13 80 . . . . . . . . . . . . . . . . . . 19
42 41 adantl 466 . . . . . . . . . . . . . . . . . 18
43 25 , 42 syld 44 . . . . . . . . . . . . . . . . 17
44 43 imp 429 . . . . . . . . . . . . . . . 16
45 44 adantr 465 . . . . . . . . . . . . . . 15
46 45 imp 429 . . . . . . . . . . . . . 14
47 nn0re 10829 . . . . . . . . . . . . . . . . . . . . 21
48 47 adantl 466 . . . . . . . . . . . . . . . . . . . 20
49 15 adantr 465 . . . . . . . . . . . . . . . . . . . 20
50 readdcl 9596 . . . . . . . . . . . . . . . . . . . 20
51 48 , 49 , 50 syl2anr 478 . . . . . . . . . . . . . . . . . . 19
52 51 adantr 465 . . . . . . . . . . . . . . . . . 18
53 17 adantr 465 . . . . . . . . . . . . . . . . . . . 20
54 53 adantr 465 . . . . . . . . . . . . . . . . . . 19
55 54 adantr 465 . . . . . . . . . . . . . . . . . 18
56 28 adantl 466 . . . . . . . . . . . . . . . . . 18
57 52 , 55 , 56 3jca 1176 . . . . . . . . . . . . . . . . 17
58 57 adantr 465 . . . . . . . . . . . . . . . 16
59 47 adantl 466 . . . . . . . . . . . . . . . . . . . . . . . 24
60 15 adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24
61 17 adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24
62 59 , 60 , 61 ltaddsubd 10177 . . . . . . . . . . . . . . . . . . . . . . 23
63 62 exbiri 622 . . . . . . . . . . . . . . . . . . . . . 22
64 63 com23 78 . . . . . . . . . . . . . . . . . . . . 21
65 64 impd 431 . . . . . . . . . . . . . . . . . . . 20
66 65 adantr 465 . . . . . . . . . . . . . . . . . . 19
67 66 imp 429 . . . . . . . . . . . . . . . . . 18
68 67 adantr 465 . . . . . . . . . . . . . . . . 17
69 68 anim1i 568 . . . . . . . . . . . . . . . 16
70 ltletr 9697 . . . . . . . . . . . . . . . 16
71 58 , 69 , 70 sylc 60 . . . . . . . . . . . . . . 15
72 71 anasss 647 . . . . . . . . . . . . . 14
73 elfzo0 11863 . . . . . . . . . . . . . 14
74 12 , 46 , 72 , 73 syl3anbrc 1180 . . . . . . . . . . . . 13
75 74 exp53 617 . . . . . . . . . . . 12
76 7 , 75 sylbird 235 . . . . . . . . . . 11
77 76 3adant3 1016 . . . . . . . . . 10
78 77 com14 88 . . . . . . . . 9
79 78 3imp 1190 . . . . . . . 8
80 3 , 79 sylbi 195 . . . . . . 7
81 80 com13 80 . . . . . 6
82 81 3adant1 1014 . . . . 5
83 2 , 82 sylbi 195 . . . 4
84 83 com12 31 . . 3
85 1 , 84 sylbi 195 . 2
86 85 imp 429 1
