Step | Hyp | Ref
| Expression |
1 | | psgnunilem4.w1 |
. 2
Word |
2 | | psgnunilem4.w2 |
. 2
g
|
3 | | wrdfin 13323 |
. . . . 5
Word |
4 | | hashcl 13147 |
. . . . 5
|
5 | 1, 3, 4 | 3syl 18 |
. . . 4
|
6 | | nn0uz 11722 |
. . . 4
|
7 | 5, 6 | syl6eleq 2711 |
. . 3
|
8 | | fveq2 6191 |
. . . . . . . . 9
|
9 | | hash0 13158 |
. . . . . . . . 9
|
10 | 8, 9 | syl6eq 2672 |
. . . . . . . 8
|
11 | 10 | oveq2d 6666 |
. . . . . . 7
|
12 | | neg1cn 11124 |
. . . . . . . 8
|
13 | | exp0 12864 |
. . . . . . . 8
|
14 | 12, 13 | ax-mp 5 |
. . . . . . 7
|
15 | 11, 14 | syl6eq 2672 |
. . . . . 6
|
16 | 15 | 2a1d 26 |
. . . . 5
..^ Word g
Word g
|
17 | | psgnunilem4.g |
. . . . . . . . . . . . 13
|
18 | | psgnunilem4.t |
. . . . . . . . . . . . 13
pmTrsp |
19 | | simpl1 1064 |
. . . . . . . . . . . . . 14
Word g
Word
g
|
20 | | psgnunilem4.d |
. . . . . . . . . . . . . 14
|
21 | 19, 20 | syl 17 |
. . . . . . . . . . . . 13
Word g
Word
g
|
22 | | simpl3l 1116 |
. . . . . . . . . . . . 13
Word g
Word
g
Word |
23 | | eqidd 2623 |
. . . . . . . . . . . . 13
Word g
Word
g
|
24 | | wrdfin 13323 |
. . . . . . . . . . . . . . 15
Word |
25 | 22, 24 | syl 17 |
. . . . . . . . . . . . . 14
Word g
Word
g
|
26 | | simpl2 1065 |
. . . . . . . . . . . . . 14
Word g
Word
g
|
27 | | hashnncl 13157 |
. . . . . . . . . . . . . . 15
|
28 | 27 | biimpar 502 |
. . . . . . . . . . . . . 14
|
29 | 25, 26, 28 | syl2anc 693 |
. . . . . . . . . . . . 13
Word g
Word
g
|
30 | | simpl3r 1117 |
. . . . . . . . . . . . 13
Word g
Word
g
g
|
31 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . 19
|
32 | 31 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . 18
|
33 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . 19
g g |
34 | 33 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . 18
g
g
|
35 | 32, 34 | anbi12d 747 |
. . . . . . . . . . . . . . . . 17
g
g |
36 | 35 | cbvrexv 3172 |
. . . . . . . . . . . . . . . 16
Word
g
Word
g
|
37 | 36 | notbii 310 |
. . . . . . . . . . . . . . 15
Word
g
Word g |
38 | 37 | biimpi 206 |
. . . . . . . . . . . . . 14
Word
g
Word g |
39 | 38 | adantl 482 |
. . . . . . . . . . . . 13
Word g
Word
g
Word
g
|
40 | 17, 18, 21, 22, 23, 29, 30, 39 | psgnunilem3 17916 |
. . . . . . . . . . . 12
Word g
Word
g
|
41 | | iman 440 |
. . . . . . . . . . . 12
Word g
Word g
Word g
Word
g
|
42 | 40, 41 | mpbir 221 |
. . . . . . . . . . 11
Word g Word g |
43 | | df-rex 2918 |
. . . . . . . . . . 11
Word
g
Word g
|
44 | 42, 43 | sylib 208 |
. . . . . . . . . 10
Word g Word
g
|
45 | | simprl 794 |
. . . . . . . . . . . . . . . . 17
Word g
Word
g
Word |
46 | | simprrr 805 |
. . . . . . . . . . . . . . . . 17
Word g
Word
g
g
|
47 | 45, 46 | jca 554 |
. . . . . . . . . . . . . . . 16
Word g
Word
g
Word g
|
48 | | wrdfin 13323 |
. . . . . . . . . . . . . . . . . 18
Word |
49 | | hashcl 13147 |
. . . . . . . . . . . . . . . . . 18
|
50 | 45, 48, 49 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
Word g
Word
g
|
51 | | simp3l 1089 |
. . . . . . . . . . . . . . . . . . . 20
Word g Word |
52 | 51, 24 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
Word g |
53 | | simp2 1062 |
. . . . . . . . . . . . . . . . . . 19
Word g |
54 | 52, 53, 28 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
Word g |
55 | 54 | adantr 481 |
. . . . . . . . . . . . . . . . 17
Word g
Word
g
|
56 | | simprrl 804 |
. . . . . . . . . . . . . . . . . 18
Word g
Word
g
|
57 | 55 | nnred 11035 |
. . . . . . . . . . . . . . . . . . 19
Word g
Word
g
|
58 | | 2rp 11837 |
. . . . . . . . . . . . . . . . . . 19
|
59 | | ltsubrp 11866 |
. . . . . . . . . . . . . . . . . . 19
|
60 | 57, 58, 59 | sylancl 694 |
. . . . . . . . . . . . . . . . . 18
Word g
Word
g
|
61 | 56, 60 | eqbrtrd 4675 |
. . . . . . . . . . . . . . . . 17
Word g
Word
g
|
62 | | elfzo0 12508 |
. . . . . . . . . . . . . . . . 17
..^
|
63 | 50, 55, 61, 62 | syl3anbrc 1246 |
. . . . . . . . . . . . . . . 16
Word g
Word
g
..^ |
64 | | id 22 |
. . . . . . . . . . . . . . . . 17
..^ Word g
..^
Word
g
|
65 | 64 | com13 88 |
. . . . . . . . . . . . . . . 16
Word
g
..^ ..^ Word g
|
66 | 47, 63, 65 | sylc 65 |
. . . . . . . . . . . . . . 15
Word g
Word
g
..^ Word g
|
67 | 56 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
Word g
Word
g
|
68 | 12 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
Word g
Word
g
|
69 | | neg1ne0 11126 |
. . . . . . . . . . . . . . . . . . 19
|
70 | 69 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
Word g
Word
g
|
71 | | 2z 11409 |
. . . . . . . . . . . . . . . . . . 19
|
72 | 71 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
Word g
Word
g
|
73 | 55 | nnzd 11481 |
. . . . . . . . . . . . . . . . . 18
Word g
Word
g
|
74 | 68, 70, 72, 73 | expsubd 13019 |
. . . . . . . . . . . . . . . . 17
Word g
Word
g
|
75 | | neg1sqe1 12959 |
. . . . . . . . . . . . . . . . . . 19
|
76 | 75 | oveq2i 6661 |
. . . . . . . . . . . . . . . . . 18
|
77 | | m1expcl 12883 |
. . . . . . . . . . . . . . . . . . . . 21
|
78 | 77 | zcnd 11483 |
. . . . . . . . . . . . . . . . . . . 20
|
79 | 73, 78 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
Word g
Word
g
|
80 | 79 | div1d 10793 |
. . . . . . . . . . . . . . . . . 18
Word g
Word
g
|
81 | 76, 80 | syl5eq 2668 |
. . . . . . . . . . . . . . . . 17
Word g
Word
g
|
82 | 67, 74, 81 | 3eqtrd 2660 |
. . . . . . . . . . . . . . . 16
Word g
Word
g
|
83 | 82 | eqeq1d 2624 |
. . . . . . . . . . . . . . 15
Word g
Word
g
|
84 | 66, 83 | sylibd 229 |
. . . . . . . . . . . . . 14
Word g
Word
g
..^ Word g
|
85 | 84 | ex 450 |
. . . . . . . . . . . . 13
Word g Word
g
..^ Word g
|
86 | 85 | com23 86 |
. . . . . . . . . . . 12
Word g ..^ Word g
Word
g
|
87 | 86 | alimdv 1845 |
. . . . . . . . . . 11
Word g ..^ Word g
Word g |
88 | | 19.23v 1902 |
. . . . . . . . . . 11
Word g
Word g |
89 | 87, 88 | syl6ib 241 |
. . . . . . . . . 10
Word g ..^ Word g
Word g |
90 | 44, 89 | mpid 44 |
. . . . . . . . 9
Word g ..^ Word g
|
91 | 90 | 3exp 1264 |
. . . . . . . 8
Word g
..^ Word g
|
92 | 91 | com34 91 |
. . . . . . 7
..^ Word g
Word g
|
93 | 92 | com12 32 |
. . . . . 6
..^ Word g
Word g
|
94 | 93 | impd 447 |
. . . . 5
..^ Word g
Word g
|
95 | 16, 94 | pm2.61ine 2877 |
. . . 4
..^ Word g
Word g
|
96 | 95 | 3adant2 1080 |
. . 3
..^ Word g
Word g
|
97 | | eleq1 2689 |
. . . . 5
Word
Word |
98 | | oveq2 6658 |
. . . . . 6
g g |
99 | 98 | eqeq1d 2624 |
. . . . 5
g
g
|
100 | 97, 99 | anbi12d 747 |
. . . 4
Word g
Word g |
101 | | fveq2 6191 |
. . . . . 6
|
102 | 101 | oveq2d 6666 |
. . . . 5
|
103 | 102 | eqeq1d 2624 |
. . . 4
|
104 | 100, 103 | imbi12d 334 |
. . 3
Word g
Word g
|
105 | | eleq1 2689 |
. . . . 5
Word
Word |
106 | | oveq2 6658 |
. . . . . 6
g g |
107 | 106 | eqeq1d 2624 |
. . . . 5
g
g
|
108 | 105, 107 | anbi12d 747 |
. . . 4
Word g
Word g |
109 | | fveq2 6191 |
. . . . . 6
|
110 | 109 | oveq2d 6666 |
. . . . 5
|
111 | 110 | eqeq1d 2624 |
. . . 4
|
112 | 108, 111 | imbi12d 334 |
. . 3
Word g
Word g
|
113 | 1, 7, 96, 104, 112, 101, 109 | uzindi 12781 |
. 2
Word g
|
114 | 1, 2, 113 | mp2and 715 |
1
|