Step Hyp Ref
Expression 1 fveq2 5871 . . . . . 6
2 1 oveq1d 6311 . . . . 5
3 pweq 4015 . . . . . . 7
4 rabeq 3103 . . . . . . 7
5 3 , 4 syl 16 . . . . . 6
6 5 fveq2d 5875 . . . . 5
7 2 , 6 eqeq12d 2479 . . . 4
8 7 ralbidv 2896 . . 3
9 fveq2 5871 . . . . . 6
10 9 oveq1d 6311 . . . . 5
11 pweq 4015 . . . . . . 7
12 rabeq 3103 . . . . . . 7
13 11 , 12 syl 16 . . . . . 6
14 13 fveq2d 5875 . . . . 5
15 10 , 14 eqeq12d 2479 . . . 4
16 15 ralbidv 2896 . . 3
17 fveq2 5871 . . . . . 6
18 17 oveq1d 6311 . . . . 5
19 pweq 4015 . . . . . . 7
20 rabeq 3103 . . . . . . 7
21 19 , 20 syl 16 . . . . . 6
22 21 fveq2d 5875 . . . . 5
23 18 , 22 eqeq12d 2479 . . . 4
24 23 ralbidv 2896 . . 3
25 fveq2 5871 . . . . . 6
26 25 oveq1d 6311 . . . . 5
27 pweq 4015 . . . . . . 7
28 rabeq 3103 . . . . . . 7
29 27 , 28 syl 16 . . . . . 6
30 29 fveq2d 5875 . . . . 5
31 26 , 30 eqeq12d 2479 . . . 4
32 31 ralbidv 2896 . . 3
33 hash0 12437 . . . . . . . . . 10
34 33 a1i 11 . . . . . . . . 9
35 elfz1eq 11726 . . . . . . . . 9
36 34 , 35 oveq12d 6314 . . . . . . . 8
37 0nn0 10835 . . . . . . . . 9
38 bcn0 12388 . . . . . . . . 9
39 37 , 38 ax-mp 5 . . . . . . . 8
40 36 , 39 syl6eq 2514 . . . . . . 7
41 pw0 4177 . . . . . . . . . 10
42 35 eqcomd 2465 . . . . . . . . . . . 12
43 41 raleqi 3058 . . . . . . . . . . . . 13
44 0ex 4582 . . . . . . . . . . . . . 14
45 fveq2 5871 . . . . . . . . . . . . . . . 16
46 45 , 33 syl6eq 2514 . . . . . . . . . . . . . . 15
47 46 eqeq1d 2459 . . . . . . . . . . . . . 14
48 44 , 47 ralsn 4068 . . . . . . . . . . . . 13
49 43 , 48 bitri 249 . . . . . . . . . . . 12
50 42 , 49 sylibr 212 . . . . . . . . . . 11
51 rabid2 3035 . . . . . . . . . . 11
52 50 , 51 sylibr 212 . . . . . . . . . 10
53 41 , 52 syl5reqr 2513 . . . . . . . . 9
54 53 fveq2d 5875 . . . . . . . 8
55 hashsng 12438 . . . . . . . . 9
56 44 , 55 ax-mp 5 . . . . . . . 8
57 54 , 56 syl6eq 2514 . . . . . . 7
58 40 , 57 eqtr4d 2501 . . . . . 6
59 58 adantl 466 . . . . 5
60 33 oveq1i 6306 . . . . . 6
61 bcval3 12384 . . . . . . . 8
62 37 , 61 mp3an1 1311 . . . . . . 7
63 id 22 . . . . . . . . . . . . . 14
64 0z 10900 . . . . . . . . . . . . . . 15
65 elfz3 11725 . . . . . . . . . . . . . . 15
66 64 , 65 ax-mp 5 . . . . . . . . . . . . . 14
67 63 , 66 syl6eqelr 2554 . . . . . . . . . . . . 13
68 67 con3i 135 . . . . . . . . . . . 12
69 68 adantl 466 . . . . . . . . . . 11
70 41 raleqi 3058 . . . . . . . . . . . 12
71 47 notbid 294 . . . . . . . . . . . . 13
72 44 , 71 ralsn 4068 . . . . . . . . . . . 12
73 70 , 72 bitri 249 . . . . . . . . . . 11
74 69 , 73 sylibr 212 . . . . . . . . . 10
75 rabeq0 3807 . . . . . . . . . 10
76 74 , 75 sylibr 212 . . . . . . . . 9
77 76 fveq2d 5875 . . . . . . . 8
78 77 , 33 syl6eq 2514 . . . . . . 7
79 62 , 78 eqtr4d 2501 . . . . . 6
80 60 , 79 syl5eq 2510 . . . . 5
81 59 , 80 pm2.61dan 791 . . . 4
82 81 rgen 2817 . . 3
83 oveq2 6304 . . . . . 6
84 eqeq2 2472 . . . . . . . . 9
85 84 rabbidv 3101 . . . . . . . 8
86 fveq2 5871 . . . . . . . . . 10
87 86 eqeq1d 2459 . . . . . . . . 9
88 87 cbvrabv 3108 . . . . . . . 8
89 85 , 88 syl6eq 2514 . . . . . . 7
90 89 fveq2d 5875 . . . . . 6
91 83 , 90 eqeq12d 2479 . . . . 5
92 91 cbvralv 3084 . . . 4
93 simpll 753 . . . . . . 7
94 simplr 755 . . . . . . 7
95 simprr 757 . . . . . . . 8
96 88 fveq2i 5874 . . . . . . . . . 10
97 96 eqeq2i 2475 . . . . . . . . 9
98 97 ralbii 2888 . . . . . . . 8
99 95 , 98 sylibr 212 . . . . . . 7
100 simprl 756 . . . . . . 7
101 93 , 94 , 99 , 100 hashbclem 12501 . . . . . 6
102 101 expr 615 . . . . 5
103 102 ralrimdva 2875 . . . 4
104 92 , 103 syl5bi 217 . . 3
105 8 , 16 , 24 , 32 , 82 , 104 findcard2s 7781 . 2
106 oveq2 6304 . . . 4
107 eqeq2 2472 . . . . . 6
108 107 rabbidv 3101 . . . . 5
109 108 fveq2d 5875 . . . 4
110 106 , 109 eqeq12d 2479 . . 3
111 110 rspccva 3209 . 2
112 105 , 111 sylan 471 1
