Step | Hyp | Ref
| Expression |
1 | | psgnunilem3.l |
. . . 4
|
2 | | psgnunilem3.w2 |
. . . 4
|
3 | 1, 2 | eqeltrrd 2702 |
. . 3
|
4 | 3 | nnnn0d 11351 |
. 2
|
5 | | psgnunilem3.w1 |
. . . . . . 7
Word |
6 | | wrdf 13310 |
. . . . . . 7
Word ..^ |
7 | 5, 6 | syl 17 |
. . . . . 6
..^ |
8 | | 0nn0 11307 |
. . . . . . . . 9
|
9 | 8 | a1i 11 |
. . . . . . . 8
|
10 | 3 | nngt0d 11064 |
. . . . . . . 8
|
11 | | elfzo0 12508 |
. . . . . . . 8
..^
|
12 | 9, 3, 10, 11 | syl3anbrc 1246 |
. . . . . . 7
..^ |
13 | 1 | oveq2d 6666 |
. . . . . . 7
..^ ..^ |
14 | 12, 13 | eleqtrrd 2704 |
. . . . . 6
..^ |
15 | 7, 14 | ffvelrnd 6360 |
. . . . 5
|
16 | | eqid 2622 |
. . . . . 6
pmTrsp pmTrsp |
17 | | psgnunilem3.t |
. . . . . 6
pmTrsp |
18 | 16, 17 | pmtrfmvdn0 17882 |
. . . . 5
|
19 | 15, 18 | syl 17 |
. . . 4
|
20 | | n0 3931 |
. . . 4
|
21 | 19, 20 | sylib 208 |
. . 3
|
22 | | fzonel 12483 |
. . . . . . . 8
..^ |
23 | | simpr1 1067 |
. . . . . . . 8
g ..^ ..^
..^ |
24 | 22, 23 | mto 188 |
. . . . . . 7
g ..^ ..^ |
25 | 24 | a1i 11 |
. . . . . 6
Word g
..^ ..^ |
26 | 25 | nrex 3000 |
. . . . 5
Word g ..^ ..^ |
27 | | eleq1 2689 |
. . . . . . . . . 10
..^
..^ |
28 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
29 | 28 | difeq1d 3727 |
. . . . . . . . . . . 12
|
30 | 29 | dmeqd 5326 |
. . . . . . . . . . 11
|
31 | 30 | eleq2d 2687 |
. . . . . . . . . 10
|
32 | | oveq2 6658 |
. . . . . . . . . . 11
..^ ..^ |
33 | 32 | raleqdv 3144 |
. . . . . . . . . 10
..^
..^ |
34 | 27, 31, 33 | 3anbi123d 1399 |
. . . . . . . . 9
..^
..^
..^
..^ |
35 | 34 | anbi2d 740 |
. . . . . . . 8
g
..^ ..^
g
..^ ..^ |
36 | 35 | rexbidv 3052 |
. . . . . . 7
Word g ..^ ..^
Word g
..^ ..^ |
37 | 36 | imbi2d 330 |
. . . . . 6
Word g
..^ ..^
Word g
..^ ..^ |
38 | | eleq1 2689 |
. . . . . . . . . . 11
..^
..^ |
39 | | fveq2 6191 |
. . . . . . . . . . . . . 14
|
40 | 39 | difeq1d 3727 |
. . . . . . . . . . . . 13
|
41 | 40 | dmeqd 5326 |
. . . . . . . . . . . 12
|
42 | 41 | eleq2d 2687 |
. . . . . . . . . . 11
|
43 | | oveq2 6658 |
. . . . . . . . . . . 12
..^ ..^ |
44 | 43 | raleqdv 3144 |
. . . . . . . . . . 11
..^
..^ |
45 | 38, 42, 44 | 3anbi123d 1399 |
. . . . . . . . . 10
..^
..^
..^ ..^ |
46 | 45 | anbi2d 740 |
. . . . . . . . 9
g
..^ ..^
g
..^ ..^ |
47 | 46 | rexbidv 3052 |
. . . . . . . 8
Word g ..^ ..^
Word g
..^ ..^ |
48 | | oveq2 6658 |
. . . . . . . . . . . 12
g g |
49 | 48 | eqeq1d 2624 |
. . . . . . . . . . 11
g
g
|
50 | | fveq2 6191 |
. . . . . . . . . . . 12
|
51 | 50 | eqeq1d 2624 |
. . . . . . . . . . 11
|
52 | 49, 51 | anbi12d 747 |
. . . . . . . . . 10
g g |
53 | | fveq1 6190 |
. . . . . . . . . . . . . 14
|
54 | 53 | difeq1d 3727 |
. . . . . . . . . . . . 13
|
55 | 54 | dmeqd 5326 |
. . . . . . . . . . . 12
|
56 | 55 | eleq2d 2687 |
. . . . . . . . . . 11
|
57 | | fveq1 6190 |
. . . . . . . . . . . . . . . . 17
|
58 | 57 | difeq1d 3727 |
. . . . . . . . . . . . . . . 16
|
59 | 58 | dmeqd 5326 |
. . . . . . . . . . . . . . 15
|
60 | 59 | eleq2d 2687 |
. . . . . . . . . . . . . 14
|
61 | 60 | notbid 308 |
. . . . . . . . . . . . 13
|
62 | 61 | ralbidv 2986 |
. . . . . . . . . . . 12
..^
..^ |
63 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
|
64 | 63 | difeq1d 3727 |
. . . . . . . . . . . . . . . 16
|
65 | 64 | dmeqd 5326 |
. . . . . . . . . . . . . . 15
|
66 | 65 | eleq2d 2687 |
. . . . . . . . . . . . . 14
|
67 | 66 | notbid 308 |
. . . . . . . . . . . . 13
|
68 | 67 | cbvralv 3171 |
. . . . . . . . . . . 12
..^
..^
|
69 | 62, 68 | syl6bb 276 |
. . . . . . . . . . 11
..^
..^ |
70 | 56, 69 | 3anbi23d 1402 |
. . . . . . . . . 10
..^
..^
..^ ..^ |
71 | 52, 70 | anbi12d 747 |
. . . . . . . . 9
g
..^ ..^
g
..^ ..^ |
72 | 71 | cbvrexv 3172 |
. . . . . . . 8
Word g ..^ ..^
Word g
..^ ..^ |
73 | 47, 72 | syl6bb 276 |
. . . . . . 7
Word g ..^ ..^
Word g
..^ ..^ |
74 | 73 | imbi2d 330 |
. . . . . 6
Word g
..^ ..^
Word g
..^ ..^ |
75 | | eleq1 2689 |
. . . . . . . . . 10
..^
..^ |
76 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
77 | 76 | difeq1d 3727 |
. . . . . . . . . . . 12
|
78 | 77 | dmeqd 5326 |
. . . . . . . . . . 11
|
79 | 78 | eleq2d 2687 |
. . . . . . . . . 10
|
80 | | oveq2 6658 |
. . . . . . . . . . 11
..^ ..^ |
81 | 80 | raleqdv 3144 |
. . . . . . . . . 10
..^
..^ |
82 | 75, 79, 81 | 3anbi123d 1399 |
. . . . . . . . 9
..^
..^
..^
..^ |
83 | 82 | anbi2d 740 |
. . . . . . . 8
g
..^ ..^
g
..^ ..^ |
84 | 83 | rexbidv 3052 |
. . . . . . 7
Word g ..^ ..^
Word g
..^ ..^ |
85 | 84 | imbi2d 330 |
. . . . . 6
Word g
..^ ..^
Word g
..^ ..^ |
86 | | eleq1 2689 |
. . . . . . . . . 10
..^
..^ |
87 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
88 | 87 | difeq1d 3727 |
. . . . . . . . . . . 12
|
89 | 88 | dmeqd 5326 |
. . . . . . . . . . 11
|
90 | 89 | eleq2d 2687 |
. . . . . . . . . 10
|
91 | | oveq2 6658 |
. . . . . . . . . . 11
..^ ..^ |
92 | 91 | raleqdv 3144 |
. . . . . . . . . 10
..^
..^ |
93 | 86, 90, 92 | 3anbi123d 1399 |
. . . . . . . . 9
..^
..^
..^ ..^ |
94 | 93 | anbi2d 740 |
. . . . . . . 8
g
..^ ..^
g
..^ ..^ |
95 | 94 | rexbidv 3052 |
. . . . . . 7
Word g ..^ ..^
Word g
..^ ..^ |
96 | 95 | imbi2d 330 |
. . . . . 6
Word g
..^ ..^
Word g
..^ ..^ |
97 | 5 | adantr 481 |
. . . . . . 7
Word |
98 | | psgnunilem3.w3 |
. . . . . . . . 9
g
|
99 | 98, 1 | jca 554 |
. . . . . . . 8
g |
100 | 99 | adantr 481 |
. . . . . . 7
g
|
101 | 12 | adantr 481 |
. . . . . . . 8
..^ |
102 | | simpr 477 |
. . . . . . . 8
|
103 | | ral0 4076 |
. . . . . . . . . 10
|
104 | | fzo0 12492 |
. . . . . . . . . . 11
..^ |
105 | 104 | raleqi 3142 |
. . . . . . . . . 10
..^
|
106 | 103, 105 | mpbir 221 |
. . . . . . . . 9
..^ |
107 | 106 | a1i 11 |
. . . . . . . 8
..^ |
108 | 101, 102,
107 | 3jca 1242 |
. . . . . . 7
..^
..^ |
109 | | oveq2 6658 |
. . . . . . . . . . 11
g g |
110 | 109 | eqeq1d 2624 |
. . . . . . . . . 10
g
g
|
111 | | fveq2 6191 |
. . . . . . . . . . 11
|
112 | 111 | eqeq1d 2624 |
. . . . . . . . . 10
|
113 | 110, 112 | anbi12d 747 |
. . . . . . . . 9
g g |
114 | | fveq1 6190 |
. . . . . . . . . . . . 13
|
115 | 114 | difeq1d 3727 |
. . . . . . . . . . . 12
|
116 | 115 | dmeqd 5326 |
. . . . . . . . . . 11
|
117 | 116 | eleq2d 2687 |
. . . . . . . . . 10
|
118 | | fveq1 6190 |
. . . . . . . . . . . . . . 15
|
119 | 118 | difeq1d 3727 |
. . . . . . . . . . . . . 14
|
120 | 119 | dmeqd 5326 |
. . . . . . . . . . . . 13
|
121 | 120 | eleq2d 2687 |
. . . . . . . . . . . 12
|
122 | 121 | notbid 308 |
. . . . . . . . . . 11
|
123 | 122 | ralbidv 2986 |
. . . . . . . . . 10
..^
..^ |
124 | 117, 123 | 3anbi23d 1402 |
. . . . . . . . 9
..^
..^
..^
..^ |
125 | 113, 124 | anbi12d 747 |
. . . . . . . 8
g
..^ ..^
g
..^ ..^ |
126 | 125 | rspcev 3309 |
. . . . . . 7
Word g
..^ ..^ Word g
..^ ..^ |
127 | 97, 100, 108, 126 | syl12anc 1324 |
. . . . . 6
Word g
..^ ..^ |
128 | | psgnunilem3.g |
. . . . . . . . . 10
|
129 | | psgnunilem3.d |
. . . . . . . . . . 11
|
130 | 129 | ad2antrr 762 |
. . . . . . . . . 10
Word
g
..^ ..^
|
131 | | simprl 794 |
. . . . . . . . . 10
Word
g
..^ ..^
Word |
132 | | simpll 790 |
. . . . . . . . . . 11
g ..^ ..^ g
|
133 | 132 | ad2antll 765 |
. . . . . . . . . 10
Word
g
..^ ..^
g |
134 | | simplr 792 |
. . . . . . . . . . 11
g ..^ ..^ |
135 | 134 | ad2antll 765 |
. . . . . . . . . 10
Word
g
..^ ..^
|
136 | | simpr1 1067 |
. . . . . . . . . . 11
g ..^ ..^ ..^ |
137 | 136 | ad2antll 765 |
. . . . . . . . . 10
Word
g
..^ ..^
..^ |
138 | | simpr2 1068 |
. . . . . . . . . . 11
g ..^ ..^
|
139 | 138 | ad2antll 765 |
. . . . . . . . . 10
Word
g
..^ ..^
|
140 | | simpr3 1069 |
. . . . . . . . . . 11
g ..^ ..^
..^
|
141 | 140 | ad2antll 765 |
. . . . . . . . . 10
Word
g
..^ ..^
..^ |
142 | | psgnunilem3.in |
. . . . . . . . . . . 12
Word g |
143 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
|
144 | 143 | eqeq1d 2624 |
. . . . . . . . . . . . . 14
|
145 | | oveq2 6658 |
. . . . . . . . . . . . . . 15
g g |
146 | 145 | eqeq1d 2624 |
. . . . . . . . . . . . . 14
g
g
|
147 | 144, 146 | anbi12d 747 |
. . . . . . . . . . . . 13
g
g |
148 | 147 | cbvrexv 3172 |
. . . . . . . . . . . 12
Word
g
Word
g
|
149 | 142, 148 | sylnib 318 |
. . . . . . . . . . 11
Word g |
150 | 149 | ad2antrr 762 |
. . . . . . . . . 10
Word
g
..^ ..^
Word g |
151 | 128, 17, 130, 131, 133, 135, 137, 139, 141, 150 | psgnunilem2 17915 |
. . . . . . . . 9
Word
g
..^ ..^
Word g
..^ ..^ |
152 | 151 | rexlimdvaa 3032 |
. . . . . . . 8
Word g ..^ ..^
Word g ..^ ..^ |
153 | 152 | a2i 14 |
. . . . . . 7
Word g
..^ ..^
Word g
..^ ..^ |
154 | 153 | a1i 11 |
. . . . . 6
Word g
..^ ..^
Word g
..^ ..^ |
155 | 37, 74, 85, 96, 127, 154 | nn0ind 11472 |
. . . . 5
Word g
..^ ..^ |
156 | 26, 155 | mtoi 190 |
. . . 4
|
157 | 156 | con2i 134 |
. . 3
|
158 | 21, 157 | exlimddv 1863 |
. 2
|
159 | 4, 158 | pm2.65i 185 |
1
|