Step | Hyp | Ref
| Expression |
1 | | simpr1 1067 |
. . . 4
Word Word
Word
Word |
2 | | simpr2 1068 |
. . . 4
Word Word
|
3 | | simpl 473 |
. . . 4
Word Word
|
4 | | swrdsb0eq 13447 |
. . . 4
Word
Word
substr substr |
5 | 1, 2, 3, 4 | syl3anc 1326 |
. . 3
Word Word
substr
substr |
6 | | ral0 4076 |
. . . . . . 7
|
7 | | nn0z 11400 |
. . . . . . . . . 10
|
8 | | nn0z 11400 |
. . . . . . . . . 10
|
9 | | fzon 12489 |
. . . . . . . . . 10
..^ |
10 | 7, 8, 9 | syl2an 494 |
. . . . . . . . 9
..^ |
11 | 10 | biimpa 501 |
. . . . . . . 8
..^ |
12 | 11 | raleqdv 3144 |
. . . . . . 7
..^
|
13 | 6, 12 | mpbiri 248 |
. . . . . 6
..^ |
14 | 13 | ex 450 |
. . . . 5
..^ |
15 | 14 | 3ad2ant2 1083 |
. . . 4
Word
Word
..^ |
16 | 15 | impcom 446 |
. . 3
Word Word
..^ |
17 | 5, 16 | 2thd 255 |
. 2
Word Word
substr substr ..^ |
18 | | swrdcl 13419 |
. . . . . 6
Word substr Word |
19 | | swrdcl 13419 |
. . . . . 6
Word substr Word |
20 | | eqwrd 13346 |
. . . . . 6
substr Word substr Word
substr substr substr substr
..^ substr substr substr |
21 | 18, 19, 20 | syl2an 494 |
. . . . 5
Word
Word substr substr substr substr
..^ substr substr substr |
22 | 21 | 3ad2ant1 1082 |
. . . 4
Word
Word
substr
substr substr substr
..^ substr substr substr |
23 | 22 | adantl 482 |
. . 3
Word Word
substr substr substr substr
..^ substr substr substr |
24 | | swrdsbslen 13448 |
. . . . 5
Word
Word
substr substr |
25 | 24 | adantl 482 |
. . . 4
Word Word
substr substr |
26 | 25 | biantrurd 529 |
. . 3
Word Word
..^ substr substr substr substr substr
..^ substr substr substr |
27 | | nn0re 11301 |
. . . . . . 7
|
28 | | nn0re 11301 |
. . . . . . 7
|
29 | | ltnle 10117 |
. . . . . . . 8
|
30 | | ltle 10126 |
. . . . . . . 8
|
31 | 29, 30 | sylbird 250 |
. . . . . . 7
|
32 | 27, 28, 31 | syl2an 494 |
. . . . . 6
|
33 | 32 | 3ad2ant2 1083 |
. . . . 5
Word
Word
|
34 | | simpl1l 1112 |
. . . . . . . . . . 11
Word Word
Word |
35 | | simpl 473 |
. . . . . . . . . . . . . 14
|
36 | 35 | 3ad2ant2 1083 |
. . . . . . . . . . . . 13
Word
Word
|
37 | 36 | adantr 481 |
. . . . . . . . . . . 12
Word Word
|
38 | 7, 8 | anim12i 590 |
. . . . . . . . . . . . . . . 16
|
39 | 38 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . 15
Word
Word
|
40 | 39 | anim1i 592 |
. . . . . . . . . . . . . 14
Word Word
|
41 | | df-3an 1039 |
. . . . . . . . . . . . . 14
|
42 | 40, 41 | sylibr 224 |
. . . . . . . . . . . . 13
Word Word
|
43 | | eluz2 11693 |
. . . . . . . . . . . . 13
|
44 | 42, 43 | sylibr 224 |
. . . . . . . . . . . 12
Word Word
|
45 | 37, 44 | jca 554 |
. . . . . . . . . . 11
Word Word
|
46 | | simpl 473 |
. . . . . . . . . . . . 13
|
47 | 46 | 3ad2ant3 1084 |
. . . . . . . . . . . 12
Word
Word
|
48 | 47 | adantr 481 |
. . . . . . . . . . 11
Word Word
|
49 | 34, 45, 48 | 3jca 1242 |
. . . . . . . . . 10
Word Word
Word
|
50 | | swrdlen2 13445 |
. . . . . . . . . 10
Word
substr |
51 | 49, 50 | syl 17 |
. . . . . . . . 9
Word Word
substr |
52 | 51 | oveq2d 6666 |
. . . . . . . 8
Word Word
..^ substr ..^ |
53 | 52 | raleqdv 3144 |
. . . . . . 7
Word Word
..^ substr substr substr
..^ substr substr |
54 | | 0zd 11389 |
. . . . . . . . . 10
Word
Word
|
55 | | zsubcl 11419 |
. . . . . . . . . . . 12
|
56 | 8, 7, 55 | syl2anr 495 |
. . . . . . . . . . 11
|
57 | 56 | 3ad2ant2 1083 |
. . . . . . . . . 10
Word
Word
|
58 | 7 | adantr 481 |
. . . . . . . . . . 11
|
59 | 58 | 3ad2ant2 1083 |
. . . . . . . . . 10
Word
Word
|
60 | | fzoshftral 12585 |
. . . . . . . . . 10
..^ substr substr
..^ substr substr |
61 | 54, 57, 59, 60 | syl3anc 1326 |
. . . . . . . . 9
Word
Word
..^ substr substr
..^ substr substr |
62 | 61 | adantr 481 |
. . . . . . . 8
Word Word
..^ substr substr
..^ substr substr |
63 | | nn0cn 11302 |
. . . . . . . . . . . . 13
|
64 | | nn0cn 11302 |
. . . . . . . . . . . . 13
|
65 | | addid2 10219 |
. . . . . . . . . . . . . . 15
|
66 | 65 | adantl 482 |
. . . . . . . . . . . . . 14
|
67 | | npcan 10290 |
. . . . . . . . . . . . . 14
|
68 | 66, 67 | oveq12d 6668 |
. . . . . . . . . . . . 13
..^ ..^ |
69 | 63, 64, 68 | syl2anr 495 |
. . . . . . . . . . . 12
..^ ..^ |
70 | 69 | 3ad2ant2 1083 |
. . . . . . . . . . 11
Word
Word
..^ ..^ |
71 | 70 | adantr 481 |
. . . . . . . . . 10
Word Word
..^ ..^ |
72 | 71 | raleqdv 3144 |
. . . . . . . . 9
Word Word
..^ substr substr
..^ substr
substr |
73 | | ovex 6678 |
. . . . . . . . . . . 12
|
74 | | sbceqg 3984 |
. . . . . . . . . . . . 13
substr substr substr substr
|
75 | | csbfv2g 6232 |
. . . . . . . . . . . . . . 15
substr
substr |
76 | | csbvarg 4003 |
. . . . . . . . . . . . . . . 16
|
77 | 76 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
substr
substr |
78 | 75, 77 | eqtrd 2656 |
. . . . . . . . . . . . . 14
substr
substr |
79 | | csbfv2g 6232 |
. . . . . . . . . . . . . . 15
substr
substr |
80 | 76 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
substr
substr |
81 | 79, 80 | eqtrd 2656 |
. . . . . . . . . . . . . 14
substr
substr |
82 | 78, 81 | eqeq12d 2637 |
. . . . . . . . . . . . 13
substr substr
substr substr |
83 | 74, 82 | bitrd 268 |
. . . . . . . . . . . 12
substr substr substr substr |
84 | 73, 83 | mp1i 13 |
. . . . . . . . . . 11
Word Word
..^
substr substr substr substr |
85 | | swrdfv2 13446 |
. . . . . . . . . . . . 13
Word ..^
substr |
86 | 49, 85 | sylan 488 |
. . . . . . . . . . . 12
Word Word
..^
substr |
87 | | simpl1r 1113 |
. . . . . . . . . . . . . 14
Word Word
Word |
88 | | simpl3r 1117 |
. . . . . . . . . . . . . 14
Word Word
|
89 | 87, 45, 88 | 3jca 1242 |
. . . . . . . . . . . . 13
Word Word
Word
|
90 | | swrdfv2 13446 |
. . . . . . . . . . . . 13
Word ..^
substr |
91 | 89, 90 | sylan 488 |
. . . . . . . . . . . 12
Word Word
..^
substr |
92 | 86, 91 | eqeq12d 2637 |
. . . . . . . . . . 11
Word Word
..^
substr
substr |
93 | 84, 92 | bitrd 268 |
. . . . . . . . . 10
Word Word
..^
substr substr |
94 | 93 | ralbidva 2985 |
. . . . . . . . 9
Word Word
..^ substr
substr
..^ |
95 | 72, 94 | bitrd 268 |
. . . . . . . 8
Word Word
..^ substr substr
..^ |
96 | 62, 95 | bitrd 268 |
. . . . . . 7
Word Word
..^ substr substr
..^ |
97 | 53, 96 | bitrd 268 |
. . . . . 6
Word Word
..^ substr substr substr
..^ |
98 | 97 | ex 450 |
. . . . 5
Word
Word
..^ substr substr substr
..^ |
99 | 33, 98 | syld 47 |
. . . 4
Word
Word
..^ substr substr substr
..^ |
100 | 99 | impcom 446 |
. . 3
Word Word
..^ substr substr substr
..^ |
101 | 23, 26, 100 | 3bitr2d 296 |
. 2
Word Word
substr substr ..^ |
102 | 17, 101 | pm2.61ian 831 |
1
Word
Word
substr
substr ..^ |