Step Hyp Ref
Expression 1 difelfznle 11818 . . . . . . . . . . . . . . . . . . 19
2 1 3exp 1195 . . . . . . . . . . . . . . . . . 18
3 2 ad2antrr 725 . . . . . . . . . . . . . . . . 17
4 3 imp 429 . . . . . . . . . . . . . . . 16
5 4 adantr 465 . . . . . . . . . . . . . . 15
6 5 com12 31 . . . . . . . . . . . . . 14
7 6 adantl 466 . . . . . . . . . . . . 13
8 7 imp 429 . . . . . . . . . . . 12
9 simprl 756 . . . . . . . . . . . . . . . . . . . . . . . . 25
10 9 ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . 24
11 elfzelz 11717 . . . . . . . . . . . . . . . . . . . . . . . . . 26
12 11 adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25
13 12 ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . 24
14 elfz2 11708 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
15 elfzelz 11717 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
16 zaddcl 10929 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
17 16 adantrr 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
18 simprr 757 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
19 17 , 18 zsubcld 10999 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
20 19 ex 434 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
21 15 , 20 syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
22 21 com12 31 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
23 22 3adant1 1014 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
24 23 adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
25 14 , 24 sylbi 195 . . . . . . . . . . . . . . . . . . . . . . . . . 26
26 25 ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . 25
27 26 imp 429 . . . . . . . . . . . . . . . . . . . . . . . 24
28 2cshw 12781 . . . . . . . . . . . . . . . . . . . . . . . 24
29 10 , 13 , 27 , 28 syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . 23
30 18 , 19 zaddcld 10998 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
31 30 ex 434 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
32 15 , 31 syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
33 32 com12 31 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
34 33 3adant1 1014 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
35 34 adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
36 14 , 35 sylbi 195 . . . . . . . . . . . . . . . . . . . . . . . . . 26
37 36 ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . 25
38 37 imp 429 . . . . . . . . . . . . . . . . . . . . . . . 24
39 cshwsublen 12767 . . . . . . . . . . . . . . . . . . . . . . . 24
40 10 , 38 , 39 syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . 23
41 29 , 40 eqtrd 2498 . . . . . . . . . . . . . . . . . . . . . 22
42 elfz2nn0 11798 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
43 elfznn0 11800 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
44 nn0cn 10830 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
45 nn0cn 10830 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
46 nn0cn 10830 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
47 45 , 46 anim12i 566 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
48 simprl 756 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
49 addcl 9595 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
50 49 adantrl 715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
51 48 , 50 pncan3d 9957 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
52 51 oveq1d 6311 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
53 pncan 9849 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
54 53 adantrl 715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
55 52 , 54 eqtrd 2498 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
56 44 , 47 , 55 syl2an 477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
57 56 ex 434 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
58 43 , 57 syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
59 58 com12 31 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
60 59 3adant3 1016 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
61 42 , 60 sylbi 195 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
62 61 adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . 26
63 oveq2 6304 . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
64 63 eqeq1d 2459 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
65 64 imbi2d 316 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
66 65 adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
67 66 adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . 26
68 62 , 67 mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . . 25
69 68 adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24
70 69 imp 429 . . . . . . . . . . . . . . . . . . . . . . 23
71 70 oveq2d 6312 . . . . . . . . . . . . . . . . . . . . . 22
72 41 , 71 eqtr2d 2499 . . . . . . . . . . . . . . . . . . . . 21
73 72 adantr 465 . . . . . . . . . . . . . . . . . . . 20
74 oveq1 6303 . . . . . . . . . . . . . . . . . . . . 21
75 74 adantl 466 . . . . . . . . . . . . . . . . . . . 20
76 73 , 75 eqtr4d 2501 . . . . . . . . . . . . . . . . . . 19
77 76 exp41 610 . . . . . . . . . . . . . . . . . 18
78 77 com24 87 . . . . . . . . . . . . . . . . 17
79 78 imp41 593 . . . . . . . . . . . . . . . 16
80 79 eqeq2d 2471 . . . . . . . . . . . . . . 15
81 80 biimpd 207 . . . . . . . . . . . . . 14
82 81 impancom 440 . . . . . . . . . . . . 13
83 82 impcom 430 . . . . . . . . . . . 12
84 oveq2 6304 . . . . . . . . . . . . . 14
85 84 eqeq2d 2471 . . . . . . . . . . . . 13
86 85 rspcev 3210 . . . . . . . . . . . 12
87 8 , 83 , 86 syl2anc 661 . . . . . . . . . . 11
88 87 exp31 604 . . . . . . . . . 10
89 oveq2 6304 . . . . . . . . . . . . . . . 16
90 89 eqeq2d 2471 . . . . . . . . . . . . . . 15
91 cshw0 12765 . . . . . . . . . . . . . . . . . . . . . 22
92 91 adantr 465 . . . . . . . . . . . . . . . . . . . . 21
93 92 eqeq2d 2471 . . . . . . . . . . . . . . . . . . . 20
94 fznn0sub2 11810 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
95 94 adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
96 oveq1 6303 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
97 96 eleq1d 2526 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
98 97 ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
99 95 , 98 mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . . . 26
100 99 adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25
101 oveq1 6303 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
102 simpl 457 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
103 2cshwid 12782 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
104 102 , 11 , 103 syl2an 477 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
105 101 , 104 sylan9eqr 2520 . . . . . . . . . . . . . . . . . . . . . . . . . 26
106 105 eqcomd 2465 . . . . . . . . . . . . . . . . . . . . . . . . 25
107 oveq2 6304 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
108 107 eqeq2d 2471 . . . . . . . . . . . . . . . . . . . . . . . . . 26
109 108 rspcev 3210 . . . . . . . . . . . . . . . . . . . . . . . . 25
110 100 , 106 ,
109 syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . 24
111 110 adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23
112 eqeq1 2461 . . . . . . . . . . . . . . . . . . . . . . . . 25
113 112 rexbidv 2968 . . . . . . . . . . . . . . . . . . . . . . . 24
114 113 adantl 466 . . . . . . . . . . . . . . . . . . . . . . 23
115 111 , 114 mpbird 232 . . . . . . . . . . . . . . . . . . . . . 22
116 115 exp41 610 . . . . . . . . . . . . . . . . . . . . 21
117 116 com24 87 . . . . . . . . . . . . . . . . . . . 20
118 93 , 117 sylbid 215 . . . . . . . . . . . . . . . . . . 19
119 118 com24 87 . . . . . . . . . . . . . . . . . 18
120 119 impcom 430 . . . . . . . . . . . . . . . . 17
121 120 com13 80 . . . . . . . . . . . . . . . 16
122 121 a1d 25 . . . . . . . . . . . . . . 15
123 90 , 122 syl6bi 228 . . . . . . . . . . . . . 14
124 123 com24 87 . . . . . . . . . . . . 13
125 124 com15 93 . . . . . . . . . . . 12
126 125 imp41 593 . . . . . . . . . . 11
127 126 com12 31 . . . . . . . . . 10
128 difelfzle 11817 . . . . . . . . . . . . . . . . 17
129 128 3exp 1195 . . . . . . . . . . . . . . . 16
130 129 ad2antrr 725 . . . . . . . . . . . . . . 15
131 130 imp 429 . . . . . . . . . . . . . 14
132 131 adantr 465 . . . . . . . . . . . . 13
133 132 impcom 430 . . . . . . . . . . . 12
134 9 ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . 24
135 12 ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . 24
136 zsubcl 10931 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
137 136 ex 434 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
138 15 , 137 syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
139 11 , 138 syl5com 30 . . . . . . . . . . . . . . . . . . . . . . . . . 26
140 139 ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . 25
141 140 imp 429 . . . . . . . . . . . . . . . . . . . . . . . 24
142 2cshw 12781 . . . . . . . . . . . . . . . . . . . . . . . 24
143 134 , 135 ,
141 , 142 syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . 23
144 zcn 10894 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
145 15 zcnd 10995 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
146 pncan3 9851 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
147 144 , 145 ,
146 syl2anr 478 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
