Step | Hyp | Ref
| Expression |
1 | | wrdfin 13323 |
. . 3
Word
|
2 | | wrdf 13310 |
. . 3
Word
..^
|
3 | | simpr 477 |
. . . . . . . . 9
..^
..^ |
4 | 3 | adantr 481 |
. . . . . . . 8
..^
..^ ..^
|
5 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
|
6 | 5 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
|
7 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
|
8 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . 19
|
9 | 8 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . 18
|
10 | 7, 9 | preq12d 4276 |
. . . . . . . . . . . . . . . . 17
|
11 | 6, 10 | eqeq12d 2637 |
. . . . . . . . . . . . . . . 16
|
12 | 11 | rspcv 3305 |
. . . . . . . . . . . . . . 15
..^
..^
|
13 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
|
14 | 13 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
|
15 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
|
16 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . 19
|
17 | 16 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . 18
|
18 | 15, 17 | preq12d 4276 |
. . . . . . . . . . . . . . . . 17
|
19 | 14, 18 | eqeq12d 2637 |
. . . . . . . . . . . . . . . 16
|
20 | 19 | rspcv 3305 |
. . . . . . . . . . . . . . 15
..^
..^
|
21 | 12, 20 | anim12ii 594 |
. . . . . . . . . . . . . 14
..^ ..^ ..^
|
22 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
|
23 | | simpl 473 |
. . . . . . . . . . . . . . . . . . . . 21
|
24 | 23 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . 20
|
25 | 24 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
|
26 | | simpl 473 |
. . . . . . . . . . . . . . . . . . 19
|
27 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . 20
|
28 | 27 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
|
29 | 25, 26, 28 | 3eqtrd 2660 |
. . . . . . . . . . . . . . . . . 18
|
30 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . 20
|
31 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . 20
|
32 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . 20
|
33 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . 20
|
34 | 30, 31, 32, 33 | preq12b 4382 |
. . . . . . . . . . . . . . . . . . 19
|
35 | | dff13 6512 |
. . . . . . . . . . . . . . . . . . . . 21
|
36 | | elfzofz 12485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
..^
|
37 | | elfzofz 12485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
..^
|
38 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
39 | 38 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
40 | | eqeq1 2626 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
41 | 39, 40 | imbi12d 334 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
42 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
43 | 42 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
44 | | eqeq2 2633 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
45 | 43, 44 | imbi12d 334 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
46 | 41, 45 | rspc2v 3322 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
47 | 36, 37, 46 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
..^ ..^
|
48 | 47 | a1dd 50 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
..^ ..^
|
49 | 48 | com14 96 |
. . . . . . . . . . . . . . . . . . . . . . . 24
..^ ..^ |
50 | 49 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
..^
..^
|
51 | | hashcl 13147 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
52 | 36 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
..^
|
53 | | fzofzp1 12565 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
..^
|
54 | 52, 53 | anim12d1 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
..^ ..^ |
55 | 54 | imp 445 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
..^ ..^
|
56 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
57 | 56 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
58 | | eqeq2 2633 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
59 | 57, 58 | imbi12d 334 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
60 | 41, 59 | rspc2v 3322 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
61 | 55, 60 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
..^ ..^
|
62 | 61 | imp 445 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
..^ ..^
|
63 | | fzofzp1 12565 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
..^
|
64 | 63 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
..^ |
65 | 64, 37 | anim12d1 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
..^ ..^ |
66 | 65 | imp 445 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
..^ ..^
|
67 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
68 | 67 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
69 | | eqeq1 2626 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
70 | 68, 69 | imbi12d 334 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
71 | 42 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
72 | | eqeq2 2633 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
73 | 71, 72 | imbi12d 334 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
74 | 70, 73 | rspc2v 3322 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
75 | 66, 74 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
..^ ..^
|
76 | 75 | imp 445 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
..^ ..^
|
77 | 62, 76 | anim12d 586 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
..^ ..^
|
78 | 77 | expimpd 629 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
..^ ..^
|
79 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
80 | 79 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
81 | 80 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
..^ ..^
|
82 | | elfzonn0 12512 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
..^
|
83 | | nn0cn 11302 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
|
84 | | add1p1 11283 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
|
85 | 83, 84 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
|
86 | 85 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
87 | | 2cnd 11093 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
|
88 | | 2ne0 11113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
|
89 | 88 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
|
90 | | addn0nid 10451 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
|
91 | 83, 87, 89, 90 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
|
92 | | eqneqall 2805 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
|
93 | 91, 92 | syl5com 31 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
94 | 86, 93 | sylbid 230 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
95 | 82, 94 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
..^
|
96 | 95 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
..^ ..^
|
97 | 96 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
..^ ..^
|
98 | 81, 97 | sylbid 230 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
..^ ..^
|
99 | 98 | expimpd 629 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
..^ ..^
|
100 | 99 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
..^ ..^
|
101 | 78, 100 | syld 47 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
..^ ..^
|
102 | 101 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
..^ ..^
|
103 | 51, 102 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
..^ ..^
|
104 | 103 | com3l 89 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
..^ ..^
|
105 | 104 | expd 452 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
..^ ..^ |
106 | 105 | com34 91 |
. . . . . . . . . . . . . . . . . . . . . . . 24
..^ ..^
|
107 | 106 | com14 96 |
. . . . . . . . . . . . . . . . . . . . . . 23
..^
..^
|
108 | 50, 107 | jaoi 394 |
. . . . . . . . . . . . . . . . . . . . . 22
..^
..^
|
109 | 108 | adantld 483 |
. . . . . . . . . . . . . . . . . . . . 21
..^ ..^ |
110 | 35, 109 | syl5bi 232 |
. . . . . . . . . . . . . . . . . . . 20
..^ ..^ |
111 | 110 | com23 86 |
. . . . . . . . . . . . . . . . . . 19
..^ ..^ |
112 | 34, 111 | sylbi 207 |
. . . . . . . . . . . . . . . . . 18
..^
..^
|
113 | 29, 112 | syl 17 |
. . . . . . . . . . . . . . . . 17
..^
..^
|
114 | 113 | ex 450 |
. . . . . . . . . . . . . . . 16
..^ ..^ |
115 | 22, 114 | syl 17 |
. . . . . . . . . . . . . . 15
..^ ..^ |
116 | 115 | com15 101 |
. . . . . . . . . . . . . 14
..^ ..^
|
117 | 21, 116 | syld 47 |
. . . . . . . . . . . . 13
..^ ..^ ..^
|
118 | 117 | com14 96 |
. . . . . . . . . . . 12
..^
..^ ..^
|
119 | 118 | imp 445 |
. . . . . . . . . . 11
..^
..^ ..^
|
120 | 119 | impcom 446 |
. . . . . . . . . 10
..^ ..^
..^ |
121 | 120 | ralrimivv 2970 |
. . . . . . . . 9
..^
..^ ..^
|
122 | 121 | adantlr 751 |
. . . . . . . 8
..^
..^
..^ ..^
|
123 | | dff13 6512 |
. . . . . . . 8
..^
..^
..^ ..^
|
124 | 4, 122, 123 | sylanbrc 698 |
. . . . . . 7
..^
..^ ..^ |
125 | | df-f1 5893 |
. . . . . . 7
..^
..^
|
126 | 124, 125 | sylib 208 |
. . . . . 6
..^
..^ ..^ |
127 | | simpr 477 |
. . . . . 6
..^
|
128 | 126, 127 | syl 17 |
. . . . 5
..^
..^ |
129 | 128 | ex 450 |
. . . 4
..^
..^ |
130 | 129 | expd 452 |
. . 3
..^
..^ |
131 | 1, 2, 130 | syl2anc 693 |
. 2
Word
..^ |
132 | 131 | impcom 446 |
1
Word ..^ |