Step | Hyp | Ref | Expression |
1 |
|
anl |
_z1 = _z2 /\ _K1 == _K2 -> _z1 = _z2 |
2 |
1 |
anwl |
_z1 = _z2 /\ _K1 == _K2 /\ _F1 == _F2 -> _z1 = _z2 |
3 |
2 |
anwl |
_z1 = _z2 /\ _K1 == _K2 /\ _F1 == _F2 /\ _x1 = _x2 -> _z1 = _z2 |
4 |
3 |
anwl |
_z1 = _z2 /\ _K1 == _K2 /\ _F1 == _F2 /\ _x1 = _x2 /\ _n1 = _n2 -> _z1 = _z2 |
5 |
4 |
anwl |
_z1 = _z2 /\ _K1 == _K2 /\ _F1 == _F2 /\ _x1 = _x2 /\ _n1 = _n2 /\ _k1 = _k2 -> _z1 = _z2 |
6 |
|
anr |
_z1 = _z2 /\ _K1 == _K2 -> _K1 == _K2 |
7 |
6 |
anwl |
_z1 = _z2 /\ _K1 == _K2 /\ _F1 == _F2 -> _K1 == _K2 |
8 |
7 |
anwl |
_z1 = _z2 /\ _K1 == _K2 /\ _F1 == _F2 /\ _x1 = _x2 -> _K1 == _K2 |
9 |
8 |
anwl |
_z1 = _z2 /\ _K1 == _K2 /\ _F1 == _F2 /\ _x1 = _x2 /\ _n1 = _n2 -> _K1 == _K2 |
10 |
9 |
anwl |
_z1 = _z2 /\ _K1 == _K2 /\ _F1 == _F2 /\ _x1 = _x2 /\ _n1 = _n2 /\ _k1 = _k2 -> _K1 == _K2 |
11 |
|
anr |
_z1 = _z2 /\ _K1 == _K2 /\ _F1 == _F2 -> _F1 == _F2 |
12 |
11 |
anwl |
_z1 = _z2 /\ _K1 == _K2 /\ _F1 == _F2 /\ _x1 = _x2 -> _F1 == _F2 |
13 |
12 |
anwl |
_z1 = _z2 /\ _K1 == _K2 /\ _F1 == _F2 /\ _x1 = _x2 /\ _n1 = _n2 -> _F1 == _F2 |
14 |
13 |
anwl |
_z1 = _z2 /\ _K1 == _K2 /\ _F1 == _F2 /\ _x1 = _x2 /\ _n1 = _n2 /\ _k1 = _k2 -> _F1 == _F2 |
15 |
|
anr |
_z1 = _z2 /\ _K1 == _K2 /\ _F1 == _F2 /\ _x1 = _x2 -> _x1 = _x2 |
16 |
15 |
anwl |
_z1 = _z2 /\ _K1 == _K2 /\ _F1 == _F2 /\ _x1 = _x2 /\ _n1 = _n2 -> _x1 = _x2 |
17 |
16 |
anwl |
_z1 = _z2 /\ _K1 == _K2 /\ _F1 == _F2 /\ _x1 = _x2 /\ _n1 = _n2 /\ _k1 = _k2 -> _x1 = _x2 |
18 |
|
anr |
_z1 = _z2 /\ _K1 == _K2 /\ _F1 == _F2 /\ _x1 = _x2 /\ _n1 = _n2 -> _n1 = _n2 |
19 |
18 |
anwl |
_z1 = _z2 /\ _K1 == _K2 /\ _F1 == _F2 /\ _x1 = _x2 /\ _n1 = _n2 /\ _k1 = _k2 -> _n1 = _n2 |
20 |
|
anr |
_z1 = _z2 /\ _K1 == _K2 /\ _F1 == _F2 /\ _x1 = _x2 /\ _n1 = _n2 /\ _k1 = _k2 -> _k1 = _k2 |
21 |
5, 10, 14, 17, 19, 20 |
grecaux2eqd |
_z1 = _z2 /\ _K1 == _K2 /\ _F1 == _F2 /\ _x1 = _x2 /\ _n1 = _n2 /\ _k1 = _k2 -> grecaux2 _z1 _K1 _F1 _x1 _n1 _k1 = grecaux2 _z2 _K2 _F2 _x2 _n2 _k2 |
22 |
21 |
exp |
_z1 = _z2 /\ _K1 == _K2 /\ _F1 == _F2 /\ _x1 = _x2 /\ _n1 = _n2 -> _k1 = _k2 -> grecaux2 _z1 _K1 _F1 _x1 _n1 _k1 = grecaux2 _z2 _K2 _F2 _x2 _n2 _k2 |
23 |
22 |
exp |
_z1 = _z2 /\ _K1 == _K2 /\ _F1 == _F2 /\ _x1 = _x2 -> _n1 = _n2 -> _k1 = _k2 -> grecaux2 _z1 _K1 _F1 _x1 _n1 _k1 = grecaux2 _z2 _K2 _F2 _x2 _n2 _k2 |
24 |
23 |
exp |
_z1 = _z2 /\ _K1 == _K2 /\ _F1 == _F2 -> _x1 = _x2 -> _n1 = _n2 -> _k1 = _k2 -> grecaux2 _z1 _K1 _F1 _x1 _n1 _k1 = grecaux2 _z2 _K2 _F2 _x2 _n2 _k2 |
25 |
24 |
exp |
_z1 = _z2 /\ _K1 == _K2 -> _F1 == _F2 -> _x1 = _x2 -> _n1 = _n2 -> _k1 = _k2 -> grecaux2 _z1 _K1 _F1 _x1 _n1 _k1 = grecaux2 _z2 _K2 _F2 _x2 _n2 _k2 |
26 |
25 |
exp |
_z1 = _z2 -> _K1 == _K2 -> _F1 == _F2 -> _x1 = _x2 -> _n1 = _n2 -> _k1 = _k2 -> grecaux2 _z1 _K1 _F1 _x1 _n1 _k1 = grecaux2 _z2 _K2 _F2 _x2 _n2 _k2 |