Step | Hyp | Ref
| Expression |
1 | | nfra1 2495 |
. . . . . . . . . . . . . . . 16
|
2 | | nfv 1515 |
. . . . . . . . . . . . . . . 16
|
3 | 1, 2 | nfan 1552 |
. . . . . . . . . . . . . . 15
|
4 | | nfv 1515 |
. . . . . . . . . . . . . . 15
DECID |
5 | 3, 4 | nfan 1552 |
. . . . . . . . . . . . . 14
DECID |
6 | | nfv 1515 |
. . . . . . . . . . . . . 14
|
7 | 5, 6 | nfan 1552 |
. . . . . . . . . . . . 13
DECID
|
8 | | simp-4l 531 |
. . . . . . . . . . . . . . . 16
DECID
|
9 | | simpr 109 |
. . . . . . . . . . . . . . . 16
DECID
|
10 | | rsp 2511 |
. . . . . . . . . . . . . . . 16
|
11 | 8, 9, 10 | sylc 62 |
. . . . . . . . . . . . . . 15
DECID
|
12 | 11 | adantllr 473 |
. . . . . . . . . . . . . 14
DECID
|
13 | | simpllr 524 |
. . . . . . . . . . . . . . . 16
DECID
|
14 | | simplrl 525 |
. . . . . . . . . . . . . . . 16
DECID
|
15 | | simplrr 526 |
. . . . . . . . . . . . . . . 16
DECID
DECID |
16 | | simpr 109 |
. . . . . . . . . . . . . . . 16
DECID
|
17 | 13, 14, 15, 16 | sumdc 11289 |
. . . . . . . . . . . . . . 15
DECID
DECID |
18 | 17 | adantlr 469 |
. . . . . . . . . . . . . 14
DECID
DECID |
19 | 12, 18 | ifeq1dadc 3546 |
. . . . . . . . . . . . 13
DECID
|
20 | 7, 19 | mpteq2da 4066 |
. . . . . . . . . . . 12
DECID
|
21 | 20 | seqeq3d 10379 |
. . . . . . . . . . 11
DECID
|
22 | 21 | breq1d 3987 |
. . . . . . . . . 10
DECID
|
23 | 22 | anbi2d 460 |
. . . . . . . . 9
DECID
#
# |
24 | 23 | exbidv 1812 |
. . . . . . . 8
DECID
# #
|
25 | 24 | rexbidva 2461 |
. . . . . . 7
DECID #
#
|
26 | 11, 17 | ifeq1dadc 3546 |
. . . . . . . . . 10
DECID
|
27 | 5, 26 | mpteq2da 4066 |
. . . . . . . . 9
DECID
|
28 | 27 | seqeq3d 10379 |
. . . . . . . 8
DECID |
29 | 28 | breq1d 3987 |
. . . . . . 7
DECID
|
30 | 25, 29 | anbi12d 465 |
. . . . . 6
DECID #
#
|
31 | 30 | pm5.32da 448 |
. . . . 5
DECID
#
DECID
#
|
32 | 31 | rexbidva 2461 |
. . . 4
DECID #
DECID
#
|
33 | | f1of 5427 |
. . . . . . . . . . . . . . 15
|
34 | 33 | ad3antlr 485 |
. . . . . . . . . . . . . 14
|
35 | | simplr 520 |
. . . . . . . . . . . . . . 15
|
36 | | simpr 109 |
. . . . . . . . . . . . . . 15
|
37 | | simp-4r 532 |
. . . . . . . . . . . . . . . . 17
|
38 | 37 | nnzd 9304 |
. . . . . . . . . . . . . . . 16
|
39 | | fznn 10015 |
. . . . . . . . . . . . . . . 16
|
40 | 38, 39 | syl 14 |
. . . . . . . . . . . . . . 15
|
41 | 35, 36, 40 | mpbir2and 933 |
. . . . . . . . . . . . . 14
|
42 | 34, 41 | ffvelrnd 5616 |
. . . . . . . . . . . . 13
|
43 | | simp-4l 531 |
. . . . . . . . . . . . 13
|
44 | | nfcsb1v 3074 |
. . . . . . . . . . . . . . 15
|
45 | | nfcsb1v 3074 |
. . . . . . . . . . . . . . 15
|
46 | 44, 45 | nfeq 2314 |
. . . . . . . . . . . . . 14
|
47 | | csbeq1a 3050 |
. . . . . . . . . . . . . . 15
|
48 | | csbeq1a 3050 |
. . . . . . . . . . . . . . 15
|
49 | 47, 48 | eqeq12d 2179 |
. . . . . . . . . . . . . 14
|
50 | 46, 49 | rspc 2820 |
. . . . . . . . . . . . 13
|
51 | 42, 43, 50 | sylc 62 |
. . . . . . . . . . . 12
|
52 | | simpr 109 |
. . . . . . . . . . . . . 14
|
53 | 52 | nnzd 9304 |
. . . . . . . . . . . . 13
|
54 | | simpllr 524 |
. . . . . . . . . . . . . 14
|
55 | 54 | nnzd 9304 |
. . . . . . . . . . . . 13
|
56 | | zdcle 9259 |
. . . . . . . . . . . . 13
DECID |
57 | 53, 55, 56 | syl2anc 409 |
. . . . . . . . . . . 12
DECID
|
58 | 51, 57 | ifeq1dadc 3546 |
. . . . . . . . . . 11
|
59 | 58 | mpteq2dva 4067 |
. . . . . . . . . 10
|
60 | 59 | seqeq3d 10379 |
. . . . . . . . 9
|
61 | 60 | fveq1d 5483 |
. . . . . . . 8
|
62 | 61 | eqeq2d 2176 |
. . . . . . 7
|
63 | 62 | pm5.32da 448 |
. . . . . 6
|
64 | 63 | exbidv 1812 |
. . . . 5
|
65 | 64 | rexbidva 2461 |
. . . 4
|
66 | 32, 65 | orbi12d 783 |
. . 3
DECID
#
DECID #
|
67 | 66 | iotabidv 5169 |
. 2
DECID
#
DECID
#
|
68 | | df-proddc 11482 |
. 2
DECID #
|
69 | | df-proddc 11482 |
. 2
DECID #
|
70 | 67, 68, 69 | 3eqtr4g 2222 |
1
|