Step |
Hyp |
Ref |
Expression |
1 |
|
nn0re |
|
2 |
1
|
3ad2ant1 |
|
3 |
2
|
recnd |
|
4 |
|
ax-1cn |
|
5 |
|
addcom |
|
6 |
3 4 5
|
sylancl |
|
7 |
|
diffi |
|
8 |
7
|
3ad2ant2 |
|
9 |
|
fzfid |
|
10 |
|
incom |
|
11 |
|
disjdif |
|
12 |
10 11
|
eqtri |
|
13 |
12
|
a1i |
|
14 |
|
hashun |
|
15 |
8 9 13 14
|
syl3anc |
|
16 |
|
uncom |
|
17 |
|
simp3 |
|
18 |
|
undif |
|
19 |
17 18
|
sylib |
|
20 |
16 19
|
syl5eq |
|
21 |
20
|
fveq2d |
|
22 |
|
hashfz1 |
|
23 |
22
|
3ad2ant1 |
|
24 |
23
|
oveq2d |
|
25 |
15 21 24
|
3eqtr3d |
|
26 |
6 25
|
oveq12d |
|
27 |
26
|
fveq2d |
|
28 |
|
1zzd |
|
29 |
|
hashcl |
|
30 |
8 29
|
syl |
|
31 |
30
|
nn0zd |
|
32 |
|
nn0z |
|
33 |
32
|
3ad2ant1 |
|
34 |
|
fzen |
|
35 |
28 31 33 34
|
syl3anc |
|
36 |
35
|
ensymd |
|
37 |
|
fzfi |
|
38 |
|
fzfi |
|
39 |
|
hashen |
|
40 |
37 38 39
|
mp2an |
|
41 |
36 40
|
sylibr |
|
42 |
|
hashfz1 |
|
43 |
30 42
|
syl |
|
44 |
27 41 43
|
3eqtrd |
|
45 |
|
fzfi |
|
46 |
|
hashen |
|
47 |
45 8 46
|
sylancr |
|
48 |
44 47
|
mpbid |
|
49 |
|
bren |
|
50 |
48 49
|
sylib |
|
51 |
|
simpl1 |
|
52 |
51
|
nn0zd |
|
53 |
|
simpl2 |
|
54 |
|
hashcl |
|
55 |
53 54
|
syl |
|
56 |
55
|
nn0zd |
|
57 |
|
nn0addge2 |
|
58 |
2 30 57
|
syl2anc |
|
59 |
58 25
|
breqtrrd |
|
60 |
59
|
adantr |
|
61 |
|
eluz2 |
|
62 |
52 56 60 61
|
syl3anbrc |
|
63 |
|
vex |
|
64 |
|
ovex |
|
65 |
|
resiexg |
|
66 |
64 65
|
ax-mp |
|
67 |
63 66
|
unex |
|
68 |
67
|
a1i |
|
69 |
|
simpr |
|
70 |
|
f1oi |
|
71 |
70
|
a1i |
|
72 |
|
incom |
|
73 |
51
|
nn0red |
|
74 |
73
|
ltp1d |
|
75 |
|
fzdisj |
|
76 |
74 75
|
syl |
|
77 |
72 76
|
syl5eq |
|
78 |
12
|
a1i |
|
79 |
|
f1oun |
|
80 |
69 71 77 78 79
|
syl22anc |
|
81 |
|
uncom |
|
82 |
|
fzsplit1nn0 |
|
83 |
51 55 60 82
|
syl3anc |
|
84 |
81 83
|
eqtr4id |
|
85 |
|
simpl3 |
|
86 |
85 18
|
sylib |
|
87 |
16 86
|
syl5eq |
|
88 |
|
f1oeq23 |
|
89 |
84 87 88
|
syl2anc |
|
90 |
80 89
|
mpbid |
|
91 |
|
resundir |
|
92 |
|
dmres |
|
93 |
|
f1odm |
|
94 |
93
|
adantl |
|
95 |
94
|
ineq2d |
|
96 |
95 76
|
eqtrd |
|
97 |
92 96
|
syl5eq |
|
98 |
|
relres |
|
99 |
|
reldm0 |
|
100 |
98 99
|
ax-mp |
|
101 |
97 100
|
sylibr |
|
102 |
|
residm |
|
103 |
102
|
a1i |
|
104 |
101 103
|
uneq12d |
|
105 |
|
uncom |
|
106 |
|
un0 |
|
107 |
105 106
|
eqtri |
|
108 |
104 107
|
eqtrdi |
|
109 |
91 108
|
syl5eq |
|
110 |
|
oveq2 |
|
111 |
110
|
f1oeq2d |
|
112 |
111
|
anbi1d |
|
113 |
|
f1oeq1 |
|
114 |
|
reseq1 |
|
115 |
114
|
eqeq1d |
|
116 |
113 115
|
anbi12d |
|
117 |
112 116
|
rspc2ev |
|
118 |
62 68 90 109 117
|
syl112anc |
|
119 |
50 118
|
exlimddv |
|