Step Hyp Ref
Expression 1 oveq2 6304 . . . . . . 7
2 1 eleq2d 2527 . . . . . 6
3 elfz1eq 11726 . . . . . . 7
4 elfz1eq 11726 . . . . . . . . 9
5 swrd00 12645 . . . . . . . . . . 11
6 swrd00 12645 . . . . . . . . . . 11
7 5 , 6 eqtr4i 2489 . . . . . . . . . 10
8 opeq1 4217 . . . . . . . . . . 11
9 8 oveq2d 6312 . . . . . . . . . 10
10 8 oveq2d 6312 . . . . . . . . . 10
11 7 , 9 , 10 3eqtr4a 2524 . . . . . . . . 9
12 4 , 11 syl 16 . . . . . . . 8
13 oveq2 6304 . . . . . . . . . 10
14 13 eleq2d 2527 . . . . . . . . 9
15 opeq2 4218 . . . . . . . . . . 11
16 15 oveq2d 6312 . . . . . . . . . 10
17 15 oveq2d 6312 . . . . . . . . . 10
18 16 , 17 eqeq12d 2479 . . . . . . . . 9
19 14 , 18 imbi12d 320 . . . . . . . 8
20 12 , 19 mpbiri 233 . . . . . . 7
21 3 , 20 syl 16 . . . . . 6
22 2 , 21 syl6bi 228 . . . . 5
23 22 com23 78 . . . 4
24 23 impd 431 . . 3
25 24 a1d 25 . 2
26 ccatcl 12593 . . . . . . . 8
27 26 adantl 466 . . . . . . 7
28 27 adantr 465 . . . . . 6
29 simprl 756 . . . . . 6
30 elfzelfzccat 12598 . . . . . . . . . 10
31 30 adantl 466 . . . . . . . . 9
32 31 com12 31 . . . . . . . 8
33 32 adantl 466 . . . . . . 7
34 33 impcom 430 . . . . . 6
35 swrdvalfn 12663 . . . . . 6
36 28 , 29 , 34 , 35 syl3anc 1228 . . . . 5
37 3anass 977 . . . . . . . . 9
38 37 simplbi2 625 . . . . . . . 8
39 38 ad2antrl 727 . . . . . . 7
40 39 imp 429 . . . . . 6
41 swrdvalfn 12663 . . . . . 6
42 40 , 41 syl 16 . . . . 5
43 simprl 756 . . . . . . . 8
44 43 ad2antrr 725 . . . . . . 7
45 simprr 757 . . . . . . . 8
46 45 ad2antrr 725 . . . . . . 7
47 elfzo0 11863 . . . . . . . . . 10
48 elfz2nn0 11798 . . . . . . . . . . . . . 14
49 nn0addcl 10856 . . . . . . . . . . . . . . . 16
50 49 expcom 435 . . . . . . . . . . . . . . 15
51 50 3ad2ant1 1017 . . . . . . . . . . . . . 14
52 48 , 51 sylbi 195 . . . . . . . . . . . . 13
53 52 ad2antrl 727 . . . . . . . . . . . 12
54 53 com12 31 . . . . . . . . . . 11
55 54 3ad2ant1 1017 . . . . . . . . . 10
56 47 , 55 sylbi 195 . . . . . . . . 9
57 56 impcom 430 . . . . . . . 8
58 lencl 12562 . . . . . . . . . . . 12
59 df-ne 2654 . . . . . . . . . . . . 13
60 elnnne0 10834 . . . . . . . . . . . . . 14
61 60 simplbi2 625 . . . . . . . . . . . . 13
62 59 , 61 syl5bir 218 . . . . . . . . . . . 12
63 58 , 62 syl 16 . . . . . . . . . . 11
64 63 adantr 465 . . . . . . . . . 10
65 64 impcom 430 . . . . . . . . 9
66 65 ad2antrr 725 . . . . . . . 8
67 elfz2nn0 11798 . . . . . . . . . . . . . . . 16
68 nn0re 10829 . . . . . . . . . . . . . . . . . . . . . . . . . 26
69 68 ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . 25
70 nn0re 10829 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
71 70 adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . 26
72 71 adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . 25
73 nn0re 10829 . . . . . . . . . . . . . . . . . . . . . . . . . 26
74 73 ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . 25
75 69 , 72 , 74 ltaddsubd 10177 . . . . . . . . . . . . . . . . . . . . . . . 24
76 nn0re 10829 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
77 49 , 76 syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
78 77 adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . 26
79 nn0re 10829 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
80 79 adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
81 80 adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . 26
82 ltletr 9697 . . . . . . . . . . . . . . . . . . . . . . . . . 26
83 78 , 74 , 81 , 82 syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . . . 25
84 83 expd 436 . . . . . . . . . . . . . . . . . . . . . . . 24
85 75 , 84 sylbird 235 . . . . . . . . . . . . . . . . . . . . . . 23
86 85 ex 434 . . . . . . . . . . . . . . . . . . . . . 22
87 86 com24 87 . . . . . . . . . . . . . . . . . . . . 21
88 87 3impia 1193 . . . . . . . . . . . . . . . . . . . 20
89 88 com13 80 . . . . . . . . . . . . . . . . . . 19
90 89 impancom 440 . . . . . . . . . . . . . . . . . 18
91 90 3adant2 1015 . . . . . . . . . . . . . . . . 17
92 91 com13 80 . . . . . . . . . . . . . . . 16
93 67 , 92 sylbi 195 . . . . . . . . . . . . . . 15
94 93 com12 31 . . . . . . . . . . . . . 14
95 94 3ad2ant1 1017 . . . . . . . . . . . . 13
96 48 , 95 sylbi 195 . . . . . . . . . . . 12
97 96 a1i 11 . . . . . . . . . . 11
98 97 imp32 433 . . . . . . . . . 10
99 47 , 98 syl5bi 217 . . . . . . . . 9
100 99 imp 429 . . . . . . . 8
101 elfzo0 11863 . . . . . . . 8
102 57 , 66 , 100 , 101 syl3anbrc 1180 . . . . . . 7
103 ccatval1 12595 . . . . . . 7
104 44 , 46 , 102 , 103 syl3anc 1228 . . . . . 6
105 27 ad2antrr 725 . . . . . . . 8
106 29 adantr 465 . . . . . . . 8
107 34 adantr 465 . . . . . . . 8
108 105 , 106 ,
107 3jca 1176 . . . . . . 7
109 swrdfv 12651 . . . . . . 7
110 108 , 109 sylancom 667 . . . . . 6
111 swrdfv 12651 . . . . . . 7
112 40 , 111 sylan 471 . . . . . 6
113 104 , 110 ,
112 3eqtr4d 2508 . . . . 5
114 36 , 42 , 113 eqfnfvd 5984 . . . 4
115 114 ex 434 . . 3
116 115 ex 434 . 2
117 25 , 116 pm2.61i 164 1
