Proof of Theorem bnj594
Step | Hyp | Ref
| Expression |
1 | | bnj594.3 |
. . . . . . . . 9
|
2 | 1 | simp2bi 1077 |
. . . . . . . 8
|
3 | | bnj594.1 |
. . . . . . . 8
|
4 | 2, 3 | sylib 208 |
. . . . . . 7
|
5 | | bnj594.11 |
. . . . . . . . 9
|
6 | 5 | simp2bi 1077 |
. . . . . . . 8
|
7 | | bnj594.9 |
. . . . . . . 8
|
8 | 6, 7 | sylib 208 |
. . . . . . 7
|
9 | | eqtr3 2643 |
. . . . . . 7
|
10 | 4, 8, 9 | syl2an 494 |
. . . . . 6
|
11 | 10 | 3adant1 1079 |
. . . . 5
|
12 | | fveq2 6191 |
. . . . . 6
|
13 | | fveq2 6191 |
. . . . . 6
|
14 | 12, 13 | eqeq12d 2637 |
. . . . 5
|
15 | 11, 14 | syl5ibr 236 |
. . . 4
|
16 | | bnj594.15 |
. . . 4
|
17 | 15, 16 | sylibr 224 |
. . 3
|
18 | 17 | a1d 25 |
. 2
|
19 | | bnj253 30770 |
. . . . . 6
|
20 | | bnj252 30769 |
. . . . . 6
|
21 | | anidm 676 |
. . . . . . 7
|
22 | 21 | 3anbi1i 1253 |
. . . . . 6
|
23 | 19, 20, 22 | 3bitr3i 290 |
. . . . 5
|
24 | | df-bnj17 30753 |
. . . . . . . . . 10
|
25 | | bnj594.17 |
. . . . . . . . . . . 12
|
26 | 25 | bnj1095 30852 |
. . . . . . . . . . 11
|
27 | 26 | bnj1352 30898 |
. . . . . . . . . 10
|
28 | 24, 27 | hbxfrbi 1752 |
. . . . . . . . 9
|
29 | | bnj170 30764 |
. . . . . . . . . . . 12
|
30 | | bnj594.7 |
. . . . . . . . . . . . . . 15
|
31 | 30 | bnj923 30838 |
. . . . . . . . . . . . . 14
|
32 | | elnn 7075 |
. . . . . . . . . . . . . 14
|
33 | 31, 32 | sylan2 491 |
. . . . . . . . . . . . 13
|
34 | 33 | anim1i 592 |
. . . . . . . . . . . 12
|
35 | 29, 34 | sylbi 207 |
. . . . . . . . . . 11
|
36 | | nnsuc 7082 |
. . . . . . . . . . 11
|
37 | | rexex 3002 |
. . . . . . . . . . 11
|
38 | 35, 36, 37 | 3syl 18 |
. . . . . . . . . 10
|
39 | 38 | bnj721 30827 |
. . . . . . . . 9
|
40 | 28, 39 | bnj596 30816 |
. . . . . . . 8
|
41 | | bnj667 30822 |
. . . . . . . . . . 11
|
42 | 41 | anim1i 592 |
. . . . . . . . . 10
|
43 | | bnj258 30774 |
. . . . . . . . . 10
|
44 | 42, 43 | sylibr 224 |
. . . . . . . . 9
|
45 | | df-bnj17 30753 |
. . . . . . . . . . . . . . 15
|
46 | | bnj219 30801 |
. . . . . . . . . . . . . . . . . 18
|
47 | 46 | 3ad2ant3 1084 |
. . . . . . . . . . . . . . . . 17
|
48 | 47 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
49 | | vex 3203 |
. . . . . . . . . . . . . . . . . . 19
|
50 | 49 | bnj216 30800 |
. . . . . . . . . . . . . . . . . 18
|
51 | | df-3an 1039 |
. . . . . . . . . . . . . . . . . . . 20
|
52 | | 3anrot 1043 |
. . . . . . . . . . . . . . . . . . . 20
|
53 | | ancom 466 |
. . . . . . . . . . . . . . . . . . . 20
|
54 | 51, 52, 53 | 3bitr3i 290 |
. . . . . . . . . . . . . . . . . . 19
|
55 | | eldifi 3732 |
. . . . . . . . . . . . . . . . . . . . . 22
|
56 | 55, 30 | eleq2s 2719 |
. . . . . . . . . . . . . . . . . . . . 21
|
57 | | nnord 7073 |
. . . . . . . . . . . . . . . . . . . . 21
|
58 | | ordtr1 5767 |
. . . . . . . . . . . . . . . . . . . . 21
|
59 | 56, 57, 58 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
|
60 | 59 | imp 445 |
. . . . . . . . . . . . . . . . . . 19
|
61 | 54, 60 | sylbi 207 |
. . . . . . . . . . . . . . . . . 18
|
62 | 50, 61 | syl3an3 1361 |
. . . . . . . . . . . . . . . . 17
|
63 | | rsp 2929 |
. . . . . . . . . . . . . . . . . 18
|
64 | 25, 63 | sylbi 207 |
. . . . . . . . . . . . . . . . 17
|
65 | 62, 64 | mpan9 486 |
. . . . . . . . . . . . . . . 16
|
66 | 48, 65 | mpd 15 |
. . . . . . . . . . . . . . 15
|
67 | 45, 66 | sylbi 207 |
. . . . . . . . . . . . . 14
|
68 | 67 | anim1i 592 |
. . . . . . . . . . . . 13
|
69 | | bnj252 30769 |
. . . . . . . . . . . . 13
|
70 | 68, 69 | sylibr 224 |
. . . . . . . . . . . 12
|
71 | | bnj446 30783 |
. . . . . . . . . . . . 13
|
72 | | bnj594.16 |
. . . . . . . . . . . . . 14
|
73 | | pm3.35 611 |
. . . . . . . . . . . . . 14
|
74 | 72, 73 | sylan2b 492 |
. . . . . . . . . . . . 13
|
75 | 71, 74 | sylbi 207 |
. . . . . . . . . . . 12
|
76 | | iuneq1 4534 |
. . . . . . . . . . . 12
|
77 | 70, 75, 76 | 3syl 18 |
. . . . . . . . . . 11
|
78 | | bnj658 30821 |
. . . . . . . . . . . . 13
|
79 | 1 | simp3bi 1078 |
. . . . . . . . . . . . . 14
|
80 | 5 | simp3bi 1078 |
. . . . . . . . . . . . . 14
|
81 | 79, 80 | bnj240 30765 |
. . . . . . . . . . . . 13
|
82 | 78, 81 | anim12i 590 |
. . . . . . . . . . . 12
|
83 | | simpl 473 |
. . . . . . . . . . . . 13
|
84 | 83 | anim2i 593 |
. . . . . . . . . . . 12
|
85 | | simp3 1063 |
. . . . . . . . . . . . . 14
|
86 | 85 | anim1i 592 |
. . . . . . . . . . . . 13
|
87 | | simpl1 1064 |
. . . . . . . . . . . . . 14
|
88 | | df-3an 1039 |
. . . . . . . . . . . . . . . . 17
|
89 | | ancom 466 |
. . . . . . . . . . . . . . . . 17
|
90 | 88, 89 | bitri 264 |
. . . . . . . . . . . . . . . 16
|
91 | | elnn 7075 |
. . . . . . . . . . . . . . . . 17
|
92 | 50, 33, 91 | syl2an 494 |
. . . . . . . . . . . . . . . 16
|
93 | 90, 92 | sylbi 207 |
. . . . . . . . . . . . . . 15
|
94 | | bnj594.2 |
. . . . . . . . . . . . . . . . 17
|
95 | 94 | bnj589 30979 |
. . . . . . . . . . . . . . . 16
|
96 | 95 | bnj590 30980 |
. . . . . . . . . . . . . . 15
|
97 | 93, 96 | mpan9 486 |
. . . . . . . . . . . . . 14
|
98 | 87, 97 | mpd 15 |
. . . . . . . . . . . . 13
|
99 | 86, 98 | syldan 487 |
. . . . . . . . . . . 12
|
100 | 82, 84, 99 | 3syl 18 |
. . . . . . . . . . 11
|
101 | | simpr 477 |
. . . . . . . . . . . . 13
|
102 | 101 | anim2i 593 |
. . . . . . . . . . . 12
|
103 | 85 | anim1i 592 |
. . . . . . . . . . . . 13
|
104 | | simpl1 1064 |
. . . . . . . . . . . . . 14
|
105 | | bnj594.10 |
. . . . . . . . . . . . . . . . 17
|
106 | 105 | bnj589 30979 |
. . . . . . . . . . . . . . . 16
|
107 | 106 | bnj590 30980 |
. . . . . . . . . . . . . . 15
|
108 | 93, 107 | mpan9 486 |
. . . . . . . . . . . . . 14
|
109 | 104, 108 | mpd 15 |
. . . . . . . . . . . . 13
|
110 | 103, 109 | syldan 487 |
. . . . . . . . . . . 12
|
111 | 82, 102, 110 | 3syl 18 |
. . . . . . . . . . 11
|
112 | 77, 100, 111 | 3eqtr4d 2666 |
. . . . . . . . . 10
|
113 | 112 | ex 450 |
. . . . . . . . 9
|
114 | 44, 113 | syl 17 |
. . . . . . . 8
|
115 | 40, 114 | bnj593 30815 |
. . . . . . 7
|
116 | | bnj258 30774 |
. . . . . . 7
|
117 | | 19.9v 1896 |
. . . . . . 7
|
118 | 115, 116,
117 | 3imtr3i 280 |
. . . . . 6
|
119 | 118 | expimpd 629 |
. . . . 5
|
120 | 23, 119 | syl5bir 233 |
. . . 4
|
121 | 120, 16 | sylibr 224 |
. . 3
|
122 | 121 | 3expib 1268 |
. 2
|
123 | 18, 122 | pm2.61ine 2877 |
1
|