Step Hyp Ref
Expression 1 oveq1 6303 . . . . . . . . 9
2 1 eqeq2d 2471 . . . . . . . 8
3 2 anbi2d 703 . . . . . . 7
4 3 adantr 465 . . . . . 6
5 elfznn0 11800 . . . . . . . . . . . . . . . . 17
6 elfznn0 11800 . . . . . . . . . . . . . . . . 17
7 nn0addcl 10856 . . . . . . . . . . . . . . . . 17
8 5 , 6 , 7 syl2anr 478 . . . . . . . . . . . . . . . 16
9 8 adantr 465 . . . . . . . . . . . . . . 15
10 elfz3nn0 11801 . . . . . . . . . . . . . . . 16
11 10 ad2antlr 726 . . . . . . . . . . . . . . 15
12 simprl 756 . . . . . . . . . . . . . . 15
13 elfz2nn0 11798 . . . . . . . . . . . . . . 15
14 9 , 11 , 12 , 13 syl3anbrc 1180 . . . . . . . . . . . . . 14
15 14 adantr 465 . . . . . . . . . . . . 13
16 cshwcsh2id.1 . . . . . . . . . . . . . . . . . 18
17 16 adantl 466 . . . . . . . . . . . . . . . . 17
18 17 adantl 466 . . . . . . . . . . . . . . . 16
19 elfzelz 11717 . . . . . . . . . . . . . . . . 17
20 19 ad2antlr 726 . . . . . . . . . . . . . . . 16
21 elfzelz 11717 . . . . . . . . . . . . . . . . . 18
22 21 adantr 465 . . . . . . . . . . . . . . . . 17
23 22 adantr 465 . . . . . . . . . . . . . . . 16
24 2cshw 12781 . . . . . . . . . . . . . . . 16
25 18 , 20 , 23 , 24 syl3anc 1228 . . . . . . . . . . . . . . 15
26 25 eqeq2d 2471 . . . . . . . . . . . . . 14
27 26 biimpa 484 . . . . . . . . . . . . 13
28 15 , 27 jca 532 . . . . . . . . . . . 12
29 28 exp41 610 . . . . . . . . . . 11
30 29 com23 78 . . . . . . . . . 10
31 30 com24 87 . . . . . . . . 9
32 31 imp 429 . . . . . . . 8
33 32 com12 31 . . . . . . 7
34 33 adantl 466 . . . . . 6
35 4 , 34 sylbid 215 . . . . 5
36 35 ancoms 453 . . . 4
37 36 impcom 430 . . 3
38 oveq2 6304 . . . . 5
39 38 eqeq2d 2471 . . . 4
40 39 rspcev 3210 . . 3
41 37 , 40 syl6com 35 . 2
42 elfz2 11708 . . . . . . . . . . . . . . . . . . 19
43 nn0z 10912 . . . . . . . . . . . . . . . . . . . . . . 23
44 zaddcl 10929 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
45 44 ex 434 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
46 45 adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . 26
47 46 impcom 430 . . . . . . . . . . . . . . . . . . . . . . . . 25
48 simprl 756 . . . . . . . . . . . . . . . . . . . . . . . . 25
49 47 , 48 zsubcld 10999 . . . . . . . . . . . . . . . . . . . . . . . 24
50 49 ex 434 . . . . . . . . . . . . . . . . . . . . . . 23
51 43 , 50 syl 16 . . . . . . . . . . . . . . . . . . . . . 22
52 51 com12 31 . . . . . . . . . . . . . . . . . . . . 21
53 52 3adant1 1014 . . . . . . . . . . . . . . . . . . . 20
54 53 adantr 465 . . . . . . . . . . . . . . . . . . 19
55 42 , 54 sylbi 195 . . . . . . . . . . . . . . . . . 18
56 6 , 55 mpan9 469 . . . . . . . . . . . . . . . . 17
57 56 adantr 465 . . . . . . . . . . . . . . . 16
58 elfz2nn0 11798 . . . . . . . . . . . . . . . . . . . . 21
59 nn0re 10829 . . . . . . . . . . . . . . . . . . . . . . . . . 26
60 nn0re 10829 . . . . . . . . . . . . . . . . . . . . . . . . . 26
61 59 , 60 anim12i 566 . . . . . . . . . . . . . . . . . . . . . . . . 25
62 nn0re 10829 . . . . . . . . . . . . . . . . . . . . . . . . 25
63 61 , 62 anim12i 566 . . . . . . . . . . . . . . . . . . . . . . . 24
64 simplr 755 . . . . . . . . . . . . . . . . . . . . . . . . . 26
65 readdcl 9596 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
66 65 adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . 26
67 64 , 66 ltnled 9753 . . . . . . . . . . . . . . . . . . . . . . . . 25
68 64 , 66 posdifd 10164 . . . . . . . . . . . . . . . . . . . . . . . . . 26
69 68 biimpd 207 . . . . . . . . . . . . . . . . . . . . . . . . 25
70 67 , 69 sylbird 235 . . . . . . . . . . . . . . . . . . . . . . . 24
71 63 , 70 syl 16 . . . . . . . . . . . . . . . . . . . . . . 23
72 71 ex 434 . . . . . . . . . . . . . . . . . . . . . 22
73 72 3adant3 1016 . . . . . . . . . . . . . . . . . . . . 21
74 58 , 73 sylbi 195 . . . . . . . . . . . . . . . . . . . 20
75 6 , 74 mpan9 469 . . . . . . . . . . . . . . . . . . 19
76 75 com12 31 . . . . . . . . . . . . . . . . . 18
77 76 adantr 465 . . . . . . . . . . . . . . . . 17
78 77 impcom 430 . . . . . . . . . . . . . . . 16
79 elnnz 10899 . . . . . . . . . . . . . . . 16
80 57 , 78 , 79 sylanbrc 664 . . . . . . . . . . . . . . 15
81 80 nnnn0d 10877 . . . . . . . . . . . . . 14
82 10 ad2antlr 726 . . . . . . . . . . . . . 14
83 cshwcsh2id.2 . . . . . . . . . . . . . . . . 17
84 oveq2 6304 . . . . . . . . . . . . . . . . . . . . 21
85 84 eleq2d 2527 . . . . . . . . . . . . . . . . . . . 20
86 85 anbi1d 704 . . . . . . . . . . . . . . . . . . 19
87 elfz2nn0 11798 . . . . . . . . . . . . . . . . . . . . 21
88 59 adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
89 88 , 62 anim12i 566 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
90 60 , 60 jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
91 90 ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
92 le2add 10059 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
93 89 , 91 , 92 syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
94 nn0readdcl 10883 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
95 94 adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
96 60 ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
97 95 , 96 , 96 lesubadd2d 10176 . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
98 93 , 97 sylibrd 234 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
99 98 expcomd 438 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
100 99 ex 434 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
101 100 com24 87 . . . . . . . . . . . . . . . . . . . . . . . . . 26
102 101 3impia 1193 . . . . . . . . . . . . . . . . . . . . . . . . 25
103 102 com13 80 . . . . . . . . . . . . . . . . . . . . . . . 24
104 103 imp 429 . . . . . . . . . . . . . . . . . . . . . . 23
105 58 , 104 syl5bi 217 . . . . . . . . . . . . . . . . . . . . . 22
106 105 3adant2 1015 . . . . . . . . . . . . . . . . . . . . 21
107 87 , 106 sylbi 195 . . . . . . . . . . . . . . . . . . . 20
108 107 imp 429 . . . . . . . . . . . . . . . . . . 19
109 86 , 108 syl6bi 228 . . . . . . . . . . . . . . . . . 18
110 109 adantr 465 . . . . . . . . . . . . . . . . 17
111 83 , 110 syl 16 . . . . . . . . . . . . . . . 16
112 111 adantl 466 . . . . . . . . . . . . . . 15
113 112 impcom 430 . . . . . . . . . . . . . 14
114 elfz2nn0 11798 . . . . . . . . . . . . . 14
115 81 , 82 , 113 , 114 syl3anbrc 1180 . . . . . . . . . . . . 13
116 115 adantr 465 . . . . . . . . . . . 12
117 16 adantl 466 . . . . . . . . . . . . . . . . 17
118 117 adantl 466 . . . . . . . . . . . . . . . 16
119 19 ad2antlr 726 . . . . . . . . . . . . . . . 16
120 22 adantr 465 . . . . . . . . . . . . . . . 16
121 118 , 119 ,
120 , 24 syl3anc 1228 . . . . . . . . . . . . . . 15
122 19 , 21 , 44 syl2anr 478 . . . . . . . . . . . . . . . 16
123 cshwsublen 12767 . . . . . . . . . . . . . . . 16
124 117 , 122 ,
123 syl2anr 478 . . . . . . . . . . . . . . 15
125 121 , 124 eqtrd 2498 . . . . . . . . . . . . . 14
126 125 eqeq2d 2471 . . . . . . . . . . . . 13
127 126 biimpa 484 . . . . . . . . . . . 12
128 116 , 127 jca 532 . . . . . . . . . . 11
129 128 exp41 610 . . . . . . . . . 10
130 129 com23 78 . . . . . . . . 9
131 130 com24 87 . . . . . . . 8
132 131 imp 429 . . . . . . 7
133 3 , 132 syl6bi 228 . . . . . 6
134 133 com23 78 . . . . 5
135 134 impcom 430 . . . 4
136 135 impcom 430 . . 3
137 oveq2 6304 . . . . 5
138 137 eqeq2d 2471 . . . 4
139 138 rspcev 3210 . . 3
140 136 , 139 syl6com 35 . 2
141 41 , 140 pm2.61ian 790 1
