Step | Hyp | Ref
| Expression |
1 | | uzrdg.b |
. 2
|
2 | | fveq2 5178 |
. . . . 5
|
3 | | fveq2 5178 |
. . . . . 6
|
4 | 2 | fveq2d 5182 |
. . . . . 6
|
5 | 3, 4 | opeq12d 3557 |
. . . . 5
|
6 | 2, 5 | eqeq12d 2054 |
. . . 4
|
7 | 6 | imbi2d 219 |
. . 3
|
8 | | fveq2 5178 |
. . . . 5
|
9 | | fveq2 5178 |
. . . . . 6
|
10 | 8 | fveq2d 5182 |
. . . . . 6
|
11 | 9, 10 | opeq12d 3557 |
. . . . 5
|
12 | 8, 11 | eqeq12d 2054 |
. . . 4
|
13 | | fveq2 5178 |
. . . . 5
|
14 | | fveq2 5178 |
. . . . . 6
|
15 | 13 | fveq2d 5182 |
. . . . . 6
|
16 | 14, 15 | opeq12d 3557 |
. . . . 5
|
17 | 13, 16 | eqeq12d 2054 |
. . . 4
|
18 | | fveq2 5178 |
. . . . 5
|
19 | | fveq2 5178 |
. . . . . 6
|
20 | 18 | fveq2d 5182 |
. . . . . 6
|
21 | 19, 20 | opeq12d 3557 |
. . . . 5
|
22 | 18, 21 | eqeq12d 2054 |
. . . 4
|
23 | | uzrdg.2 |
. . . . . . 7
frec
|
24 | 23 | fveq1i 5179 |
. . . . . 6
frec
|
25 | | frec2uz.1 |
. . . . . . . 8
|
26 | | uzrdg.a |
. . . . . . . 8
|
27 | | opexg 3964 |
. . . . . . . 8
|
28 | 25, 26, 27 | syl2anc 391 |
. . . . . . 7
|
29 | | frec0g 5983 |
. . . . . . 7
frec |
30 | 28, 29 | syl 14 |
. . . . . 6
frec |
31 | 24, 30 | syl5eq 2084 |
. . . . 5
|
32 | | frec2uz.2 |
. . . . . . 7
frec |
33 | 25, 32 | frec2uz0d 9185 |
. . . . . 6
|
34 | 31 | fveq2d 5182 |
. . . . . . 7
|
35 | | uzid 8487 |
. . . . . . . . 9
|
36 | 25, 35 | syl 14 |
. . . . . . . 8
|
37 | | op2ndg 5778 |
. . . . . . . 8
|
38 | 36, 26, 37 | syl2anc 391 |
. . . . . . 7
|
39 | 34, 38 | eqtrd 2072 |
. . . . . 6
|
40 | 33, 39 | opeq12d 3557 |
. . . . 5
|
41 | 31, 40 | eqtr4d 2075 |
. . . 4
|
42 | | zex 8254 |
. . . . . . . . . . . . . . . 16
|
43 | | uzssz 8492 |
. . . . . . . . . . . . . . . 16
|
44 | 42, 43 | ssexi 3895 |
. . . . . . . . . . . . . . 15
|
45 | 44 | a1i 9 |
. . . . . . . . . . . . . 14
|
46 | | uzrdg.s |
. . . . . . . . . . . . . . 15
|
47 | 46 | adantr 261 |
. . . . . . . . . . . . . 14
|
48 | | mpt2exga 5835 |
. . . . . . . . . . . . . 14
|
49 | 45, 47, 48 | syl2anc 391 |
. . . . . . . . . . . . 13
|
50 | | vex 2560 |
. . . . . . . . . . . . . 14
|
51 | 50 | a1i 9 |
. . . . . . . . . . . . 13
|
52 | | fvexg 5194 |
. . . . . . . . . . . . 13
|
53 | 49, 51, 52 | syl2anc 391 |
. . . . . . . . . . . 12
|
54 | 53 | alrimiv 1754 |
. . . . . . . . . . 11
|
55 | 28 | adantr 261 |
. . . . . . . . . . 11
|
56 | | simpr 103 |
. . . . . . . . . . 11
|
57 | | frecsuc 5991 |
. . . . . . . . . . 11
frec frec |
58 | 54, 55, 56, 57 | syl3anc 1135 |
. . . . . . . . . 10
frec frec |
59 | 23 | fveq1i 5179 |
. . . . . . . . . 10
frec |
60 | 23 | fveq1i 5179 |
. . . . . . . . . . 11
frec |
61 | 60 | fveq2i 5181 |
. . . . . . . . . 10
frec |
62 | 58, 59, 61 | 3eqtr4g 2097 |
. . . . . . . . 9
|
63 | 62 | adantr 261 |
. . . . . . . 8
|
64 | | fveq2 5178 |
. . . . . . . . 9
|
65 | | df-ov 5515 |
. . . . . . . . . 10
|
66 | 25 | adantr 261 |
. . . . . . . . . . . 12
|
67 | 66, 32, 56 | frec2uzuzd 9188 |
. . . . . . . . . . 11
|
68 | | uzrdg.f |
. . . . . . . . . . . . 13
|
69 | 25, 32, 46, 26, 68, 23 | frecuzrdgrrn 9194 |
. . . . . . . . . . . 12
|
70 | | xp2nd 5793 |
. . . . . . . . . . . 12
|
71 | 69, 70 | syl 14 |
. . . . . . . . . . 11
|
72 | | peano2uz 8526 |
. . . . . . . . . . . . 13
|
73 | 67, 72 | syl 14 |
. . . . . . . . . . . 12
|
74 | 68 | caovclg 5653 |
. . . . . . . . . . . . . 14
|
75 | 74 | adantlr 446 |
. . . . . . . . . . . . 13
|
76 | 75, 67, 71 | caovcld 5654 |
. . . . . . . . . . . 12
|
77 | | opelxp 4374 |
. . . . . . . . . . . 12
|
78 | 73, 76, 77 | sylanbrc 394 |
. . . . . . . . . . 11
|
79 | | oveq1 5519 |
. . . . . . . . . . . . 13
|
80 | | oveq1 5519 |
. . . . . . . . . . . . 13
|
81 | 79, 80 | opeq12d 3557 |
. . . . . . . . . . . 12
|
82 | | oveq2 5520 |
. . . . . . . . . . . . 13
|
83 | 82 | opeq2d 3556 |
. . . . . . . . . . . 12
|
84 | | oveq1 5519 |
. . . . . . . . . . . . . 14
|
85 | | oveq1 5519 |
. . . . . . . . . . . . . 14
|
86 | 84, 85 | opeq12d 3557 |
. . . . . . . . . . . . 13
|
87 | | oveq2 5520 |
. . . . . . . . . . . . . 14
|
88 | 87 | opeq2d 3556 |
. . . . . . . . . . . . 13
|
89 | 86, 88 | cbvmpt2v 5584 |
. . . . . . . . . . . 12
|
90 | 81, 83, 89 | ovmpt2g 5635 |
. . . . . . . . . . 11
|
91 | 67, 71, 78, 90 | syl3anc 1135 |
. . . . . . . . . 10
|
92 | 65, 91 | syl5eqr 2086 |
. . . . . . . . 9
|
93 | 64, 92 | sylan9eqr 2094 |
. . . . . . . 8
|
94 | 63, 93 | eqtrd 2072 |
. . . . . . 7
|
95 | 66, 32, 56 | frec2uzsucd 9187 |
. . . . . . . . 9
|
96 | 95 | adantr 261 |
. . . . . . . 8
|
97 | 94 | fveq2d 5182 |
. . . . . . . . 9
|
98 | 66, 32, 56 | frec2uzzd 9186 |
. . . . . . . . . . . 12
|
99 | 98 | peano2zd 8363 |
. . . . . . . . . . 11
|
100 | 99 | adantr 261 |
. . . . . . . . . 10
|
101 | 76 | adantr 261 |
. . . . . . . . . 10
|
102 | | op2ndg 5778 |
. . . . . . . . . 10
|
103 | 100, 101,
102 | syl2anc 391 |
. . . . . . . . 9
|
104 | 97, 103 | eqtrd 2072 |
. . . . . . . 8
|
105 | 96, 104 | opeq12d 3557 |
. . . . . . 7
|
106 | 94, 105 | eqtr4d 2075 |
. . . . . 6
|
107 | 106 | ex 108 |
. . . . 5
|
108 | 107 | expcom 109 |
. . . 4
|
109 | 12, 17, 22, 41, 108 | finds2 4324 |
. . 3
|
110 | 7, 109 | vtoclga 2619 |
. 2
|
111 | 1, 110 | mpcom 32 |
1
|