Step | Hyp | Ref
| Expression |
1 | | oveq2 6658 |
. . . . . . 7
|
2 | 1 | eleq2d 2687 |
. . . . . 6
|
3 | | elfz1eq 12352 |
. . . . . . 7
|
4 | | elfz1eq 12352 |
. . . . . . . . 9
|
5 | | swrd00 13418 |
. . . . . . . . . . 11
++ substr
|
6 | | swrd00 13418 |
. . . . . . . . . . 11
substr |
7 | 5, 6 | eqtr4i 2647 |
. . . . . . . . . 10
++ substr
substr |
8 | | opeq1 4402 |
. . . . . . . . . . 11
|
9 | 8 | oveq2d 6666 |
. . . . . . . . . 10
++ substr ++ substr
|
10 | 8 | oveq2d 6666 |
. . . . . . . . . 10
substr
substr |
11 | 7, 9, 10 | 3eqtr4a 2682 |
. . . . . . . . 9
++ substr substr |
12 | 4, 11 | syl 17 |
. . . . . . . 8
++ substr substr |
13 | | oveq2 6658 |
. . . . . . . . . 10
|
14 | 13 | eleq2d 2687 |
. . . . . . . . 9
|
15 | | opeq2 4403 |
. . . . . . . . . . 11
|
16 | 15 | oveq2d 6666 |
. . . . . . . . . 10
++ substr ++ substr |
17 | 15 | oveq2d 6666 |
. . . . . . . . . 10
substr substr |
18 | 16, 17 | eqeq12d 2637 |
. . . . . . . . 9
++ substr substr ++ substr
substr |
19 | 14, 18 | imbi12d 334 |
. . . . . . . 8
++ substr substr
++ substr substr |
20 | 12, 19 | mpbiri 248 |
. . . . . . 7
++ substr substr |
21 | 3, 20 | syl 17 |
. . . . . 6
++ substr substr |
22 | 2, 21 | syl6bi 243 |
. . . . 5
++ substr substr |
23 | 22 | com23 86 |
. . . 4
++ substr substr |
24 | 23 | impd 447 |
. . 3
++ substr substr |
25 | 24 | a1d 25 |
. 2
Word
Word
++ substr substr |
26 | | ccatcl 13359 |
. . . . . . . 8
Word
Word ++ Word |
27 | 26 | adantl 482 |
. . . . . . 7
Word
Word
++ Word |
28 | 27 | adantr 481 |
. . . . . 6
Word Word
++ Word
|
29 | | simprl 794 |
. . . . . 6
Word Word
|
30 | | elfzelfzccat 13364 |
. . . . . . . . . 10
Word
Word
++ |
31 | 30 | adantl 482 |
. . . . . . . . 9
Word
Word
++ |
32 | 31 | com12 32 |
. . . . . . . 8
Word Word ++ |
33 | 32 | adantl 482 |
. . . . . . 7
Word Word
++ |
34 | 33 | impcom 446 |
. . . . . 6
Word Word
++ |
35 | | swrdvalfn 13426 |
. . . . . 6
++ Word
++ ++ substr ..^ |
36 | 28, 29, 34, 35 | syl3anc 1326 |
. . . . 5
Word Word
++ substr ..^ |
37 | | 3anass 1042 |
. . . . . . . . 9
Word
Word |
38 | 37 | simplbi2 655 |
. . . . . . . 8
Word Word |
39 | 38 | ad2antrl 764 |
. . . . . . 7
Word
Word
Word
|
40 | 39 | imp 445 |
. . . . . 6
Word Word
Word |
41 | | swrdvalfn 13426 |
. . . . . 6
Word
substr
..^ |
42 | 40, 41 | syl 17 |
. . . . 5
Word Word
substr ..^ |
43 | | simprl 794 |
. . . . . . . 8
Word
Word
Word |
44 | 43 | ad2antrr 762 |
. . . . . . 7
Word Word
..^ Word |
45 | | simprr 796 |
. . . . . . . 8
Word
Word
Word |
46 | 45 | ad2antrr 762 |
. . . . . . 7
Word Word
..^ Word |
47 | | elfzo0 12508 |
. . . . . . . . . 10
..^
|
48 | | elfz2nn0 12431 |
. . . . . . . . . . . . . 14
|
49 | | nn0addcl 11328 |
. . . . . . . . . . . . . . . 16
|
50 | 49 | expcom 451 |
. . . . . . . . . . . . . . 15
|
51 | 50 | 3ad2ant1 1082 |
. . . . . . . . . . . . . 14
|
52 | 48, 51 | sylbi 207 |
. . . . . . . . . . . . 13
|
53 | 52 | ad2antrl 764 |
. . . . . . . . . . . 12
Word Word
|
54 | 53 | com12 32 |
. . . . . . . . . . 11
Word Word
|
55 | 54 | 3ad2ant1 1082 |
. . . . . . . . . 10
Word
Word |
56 | 47, 55 | sylbi 207 |
. . . . . . . . 9
..^
Word Word
|
57 | 56 | impcom 446 |
. . . . . . . 8
Word Word
..^ |
58 | | lencl 13324 |
. . . . . . . . . . . 12
Word |
59 | | df-ne 2795 |
. . . . . . . . . . . . 13
|
60 | | elnnne0 11306 |
. . . . . . . . . . . . . 14
|
61 | 60 | simplbi2 655 |
. . . . . . . . . . . . 13
|
62 | 59, 61 | syl5bir 233 |
. . . . . . . . . . . 12
|
63 | 58, 62 | syl 17 |
. . . . . . . . . . 11
Word |
64 | 63 | adantr 481 |
. . . . . . . . . 10
Word
Word |
65 | 64 | impcom 446 |
. . . . . . . . 9
Word
Word
|
66 | 65 | ad2antrr 762 |
. . . . . . . 8
Word Word
..^ |
67 | | elfz2nn0 12431 |
. . . . . . . . . . . . . . . 16
|
68 | | nn0re 11301 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
69 | 68 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
70 | | nn0re 11301 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
71 | 70 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
72 | 71 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
73 | | nn0re 11301 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
74 | 73 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
75 | 69, 72, 74 | ltaddsubd 10627 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
76 | | nn0re 11301 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
77 | 49, 76 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
78 | 77 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
79 | | nn0re 11301 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
80 | 79 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
81 | 80 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
82 | | ltletr 10129 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
83 | 78, 74, 81, 82 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
84 | 83 | expd 452 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
85 | 75, 84 | sylbird 250 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
86 | 85 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . 22
|
87 | 86 | com24 95 |
. . . . . . . . . . . . . . . . . . . . 21
|
88 | 87 | 3impia 1261 |
. . . . . . . . . . . . . . . . . . . 20
|
89 | 88 | com13 88 |
. . . . . . . . . . . . . . . . . . 19
|
90 | 89 | impancom 456 |
. . . . . . . . . . . . . . . . . 18
|
91 | 90 | 3adant2 1080 |
. . . . . . . . . . . . . . . . 17
|
92 | 91 | com13 88 |
. . . . . . . . . . . . . . . 16
|
93 | 67, 92 | sylbi 207 |
. . . . . . . . . . . . . . 15
|
94 | 93 | com12 32 |
. . . . . . . . . . . . . 14
|
95 | 94 | 3ad2ant1 1082 |
. . . . . . . . . . . . 13
|
96 | 48, 95 | sylbi 207 |
. . . . . . . . . . . 12
|
97 | 96 | a1i 11 |
. . . . . . . . . . 11
Word
Word
|
98 | 97 | imp32 449 |
. . . . . . . . . 10
Word Word
|
99 | 47, 98 | syl5bi 232 |
. . . . . . . . 9
Word Word
..^ |
100 | 99 | imp 445 |
. . . . . . . 8
Word Word
..^ |
101 | | elfzo0 12508 |
. . . . . . . 8
..^
|
102 | 57, 66, 100, 101 | syl3anbrc 1246 |
. . . . . . 7
Word Word
..^ ..^ |
103 | | ccatval1 13361 |
. . . . . . 7
Word
Word ..^ ++ |
104 | 44, 46, 102, 103 | syl3anc 1326 |
. . . . . 6
Word Word
..^ ++ |
105 | 27 | ad2antrr 762 |
. . . . . . . 8
Word Word
..^ ++ Word
|
106 | 29 | adantr 481 |
. . . . . . . 8
Word Word
..^ |
107 | 34 | adantr 481 |
. . . . . . . 8
Word Word
..^ ++ |
108 | 105, 106,
107 | 3jca 1242 |
. . . . . . 7
Word Word
..^ ++ Word
++ |
109 | | swrdfv 13424 |
. . . . . . 7
++ Word
++ ..^
++ substr ++ |
110 | 108, 109 | sylancom 701 |
. . . . . 6
Word Word
..^ ++ substr ++ |
111 | | swrdfv 13424 |
. . . . . . 7
Word
..^ substr |
112 | 40, 111 | sylan 488 |
. . . . . 6
Word Word
..^ substr |
113 | 104, 110,
112 | 3eqtr4d 2666 |
. . . . 5
Word Word
..^ ++ substr substr |
114 | 36, 42, 113 | eqfnfvd 6314 |
. . . 4
Word Word
++ substr substr |
115 | 114 | ex 450 |
. . 3
Word
Word
++ substr substr |
116 | 115 | ex 450 |
. 2
Word Word
++ substr substr |
117 | 25, 116 | pm2.61i 176 |
1
Word
Word
++ substr substr |