Step | Hyp | Ref
| Expression |
1 | | fiunelros.2 |
. 2
|
2 | | simpr 477 |
. . . . 5
|
3 | 2 | nnred 11035 |
. . . 4
|
4 | 3 | leidd 10594 |
. . 3
|
5 | | breq1 4656 |
. . . . 5
|
6 | | oveq2 6658 |
. . . . . . 7
..^ ..^ |
7 | 6 | iuneq1d 4545 |
. . . . . 6
..^ ..^ |
8 | 7 | eleq1d 2686 |
. . . . 5
..^
..^ |
9 | 5, 8 | imbi12d 334 |
. . . 4
..^
..^ |
10 | | breq1 4656 |
. . . . 5
|
11 | | oveq2 6658 |
. . . . . . 7
..^ ..^ |
12 | 11 | iuneq1d 4545 |
. . . . . 6
..^ ..^ |
13 | 12 | eleq1d 2686 |
. . . . 5
..^
..^ |
14 | 10, 13 | imbi12d 334 |
. . . 4
..^
..^ |
15 | | breq1 4656 |
. . . . 5
|
16 | | oveq2 6658 |
. . . . . . 7
..^ ..^ |
17 | 16 | iuneq1d 4545 |
. . . . . 6
..^ ..^ |
18 | 17 | eleq1d 2686 |
. . . . 5
..^
..^ |
19 | 15, 18 | imbi12d 334 |
. . . 4
..^
..^ |
20 | | breq1 4656 |
. . . . 5
|
21 | | oveq2 6658 |
. . . . . . 7
..^ ..^ |
22 | 21 | iuneq1d 4545 |
. . . . . 6
..^ ..^ |
23 | 22 | eleq1d 2686 |
. . . . 5
..^
..^ |
24 | 20, 23 | imbi12d 334 |
. . . 4
..^
..^ |
25 | | fzo0 12492 |
. . . . . . . 8
..^ |
26 | | iuneq1 4534 |
. . . . . . . 8
..^ ..^ |
27 | 25, 26 | ax-mp 5 |
. . . . . . 7
..^ |
28 | | 0iun 4577 |
. . . . . . 7
|
29 | 27, 28 | eqtri 2644 |
. . . . . 6
..^ |
30 | | fiunelros.1 |
. . . . . . 7
|
31 | | isros.1 |
. . . . . . . 8
|
32 | 31 | 0elros 30233 |
. . . . . . 7
|
33 | 30, 32 | syl 17 |
. . . . . 6
|
34 | 29, 33 | syl5eqel 2705 |
. . . . 5
..^ |
35 | 34 | a1d 25 |
. . . 4
..^ |
36 | | simpllr 799 |
. . . . . . . 8
..^
|
37 | | fzosplitsn 12576 |
. . . . . . . . . 10
..^ ..^ |
38 | | nnuz 11723 |
. . . . . . . . . 10
|
39 | 37, 38 | eleq2s 2719 |
. . . . . . . . 9
..^ ..^ |
40 | 39 | iuneq1d 4545 |
. . . . . . . 8
..^ ..^ |
41 | 36, 40 | syl 17 |
. . . . . . 7
..^
..^ ..^ |
42 | | iunxun 4605 |
. . . . . . 7
..^ ..^ |
43 | 41, 42 | syl6eq 2672 |
. . . . . 6
..^
..^
..^ |
44 | 30 | ad3antrrr 766 |
. . . . . . 7
..^
|
45 | 36 | nnred 11035 |
. . . . . . . . 9
..^
|
46 | 1 | ad3antrrr 766 |
. . . . . . . . . 10
..^
|
47 | 46 | nnred 11035 |
. . . . . . . . 9
..^
|
48 | | simpr 477 |
. . . . . . . . . 10
..^
|
49 | | nnltp1le 11433 |
. . . . . . . . . . 11
|
50 | 36, 46, 49 | syl2anc 693 |
. . . . . . . . . 10
..^
|
51 | 48, 50 | mpbird 247 |
. . . . . . . . 9
..^
|
52 | 45, 47, 51 | ltled 10185 |
. . . . . . . 8
..^
|
53 | | simplr 792 |
. . . . . . . 8
..^
..^ |
54 | 52, 53 | mpd 15 |
. . . . . . 7
..^
..^ |
55 | | nfcsb1v 3549 |
. . . . . . . . . 10
|
56 | | csbeq1a 3542 |
. . . . . . . . . 10
|
57 | 55, 56 | iunxsngf 29375 |
. . . . . . . . 9
|
58 | 36, 57 | syl 17 |
. . . . . . . 8
..^
|
59 | | simplll 798 |
. . . . . . . . 9
..^
|
60 | | elfzo1 12517 |
. . . . . . . . . 10
..^ |
61 | 36, 46, 51, 60 | syl3anbrc 1246 |
. . . . . . . . 9
..^
..^ |
62 | | nfv 1843 |
. . . . . . . . . . 11
..^ |
63 | | nfcv 2764 |
. . . . . . . . . . . 12
|
64 | 55, 63 | nfel 2777 |
. . . . . . . . . . 11
|
65 | 62, 64 | nfim 1825 |
. . . . . . . . . 10
..^
|
66 | | eleq1 2689 |
. . . . . . . . . . . 12
..^
..^ |
67 | 66 | anbi2d 740 |
. . . . . . . . . . 11
..^
..^ |
68 | 56 | eleq1d 2686 |
. . . . . . . . . . 11
|
69 | 67, 68 | imbi12d 334 |
. . . . . . . . . 10
..^
..^
|
70 | | fiunelros.3 |
. . . . . . . . . 10
..^ |
71 | 65, 69, 70 | chvar 2262 |
. . . . . . . . 9
..^
|
72 | 59, 61, 71 | syl2anc 693 |
. . . . . . . 8
..^
|
73 | 58, 72 | eqeltrd 2701 |
. . . . . . 7
..^
|
74 | 31 | unelros 30234 |
. . . . . . 7
..^
..^ |
75 | 44, 54, 73, 74 | syl3anc 1326 |
. . . . . 6
..^
..^ |
76 | 43, 75 | eqeltrd 2701 |
. . . . 5
..^
..^ |
77 | 76 | ex 450 |
. . . 4
..^ ..^ |
78 | 9, 14, 19, 24, 35, 77 | nnindd 29566 |
. . 3
..^ |
79 | 4, 78 | mpd 15 |
. 2
..^ |
80 | 1, 79 | mpdan 702 |
1
..^ |