Step | Hyp | Ref
| Expression |
1 | | ax-hgprmladderOLD 41708 |
. 2
RePart ; ; ; ..^
; |
2 | | 1nn0 11308 |
. . . . . . . . . . . 12
|
3 | | 1nn 11031 |
. . . . . . . . . . . 12
|
4 | 2, 3 | decnncl 11518 |
. . . . . . . . . . 11
; |
5 | 4 | nnzi 11401 |
. . . . . . . . . 10
; |
6 | | 8nn0 11315 |
. . . . . . . . . . . . 13
|
7 | | 8nn 11191 |
. . . . . . . . . . . . 13
|
8 | 6, 7 | decnncl 11518 |
. . . . . . . . . . . 12
; |
9 | | 10nnOLD 11193 |
. . . . . . . . . . . . 13
|
10 | | 2nn0 11309 |
. . . . . . . . . . . . . . 15
|
11 | | 9nn 11192 |
. . . . . . . . . . . . . . 15
|
12 | 10, 11 | decnncl 11518 |
. . . . . . . . . . . . . 14
; |
13 | 12 | nnnn0i 11300 |
. . . . . . . . . . . . 13
; |
14 | | nnexpcl 12873 |
. . . . . . . . . . . . 13
; ; |
15 | 9, 13, 14 | mp2an 708 |
. . . . . . . . . . . 12
; |
16 | 8, 15 | nnmulcli 11044 |
. . . . . . . . . . 11
; ; |
17 | 16 | nnzi 11401 |
. . . . . . . . . 10
; ; |
18 | | 1re 10039 |
. . . . . . . . . . . . 13
|
19 | 8 | nnrei 11029 |
. . . . . . . . . . . . 13
; |
20 | 18, 19 | pm3.2i 471 |
. . . . . . . . . . . 12
; |
21 | | 0le1 10551 |
. . . . . . . . . . . . 13
|
22 | | 1lt10OLD 11238 |
. . . . . . . . . . . . . 14
|
23 | 7, 6, 2, 22 | decltiOLD 11548 |
. . . . . . . . . . . . 13
; |
24 | 21, 23 | pm3.2i 471 |
. . . . . . . . . . . 12
; |
25 | | nnexpcl 12873 |
. . . . . . . . . . . . . . 15
|
26 | 9, 2, 25 | mp2an 708 |
. . . . . . . . . . . . . 14
|
27 | 26 | nnrei 11029 |
. . . . . . . . . . . . 13
|
28 | 15 | nnrei 11029 |
. . . . . . . . . . . . 13
; |
29 | 27, 28 | pm3.2i 471 |
. . . . . . . . . . . 12
; |
30 | | 0re 10040 |
. . . . . . . . . . . . . . 15
|
31 | | 10reOLD 11109 |
. . . . . . . . . . . . . . 15
|
32 | | 10posOLD 11123 |
. . . . . . . . . . . . . . 15
|
33 | 30, 31, 32 | ltleii 10160 |
. . . . . . . . . . . . . 14
|
34 | 9 | nncni 11030 |
. . . . . . . . . . . . . . 15
|
35 | | exp1 12866 |
. . . . . . . . . . . . . . 15
|
36 | 34, 35 | ax-mp 5 |
. . . . . . . . . . . . . 14
|
37 | 33, 36 | breqtrri 4680 |
. . . . . . . . . . . . 13
|
38 | | 1z 11407 |
. . . . . . . . . . . . . . 15
|
39 | 12 | nnzi 11401 |
. . . . . . . . . . . . . . 15
; |
40 | 31, 38, 39 | 3pm3.2i 1239 |
. . . . . . . . . . . . . 14
; |
41 | | 2nn 11185 |
. . . . . . . . . . . . . . . 16
|
42 | | 9nn0 11316 |
. . . . . . . . . . . . . . . 16
|
43 | 41, 42, 2, 22 | decltiOLD 11548 |
. . . . . . . . . . . . . . 15
; |
44 | 22, 43 | pm3.2i 471 |
. . . . . . . . . . . . . 14
; |
45 | | ltexp2a 12912 |
. . . . . . . . . . . . . 14
; ; ; |
46 | 40, 44, 45 | mp2an 708 |
. . . . . . . . . . . . 13
; |
47 | 37, 46 | pm3.2i 471 |
. . . . . . . . . . . 12
; |
48 | | ltmul12a 10879 |
. . . . . . . . . . . 12
;
; ;
; ; ; |
49 | 20, 24, 29, 47, 48 | mp4an 709 |
. . . . . . . . . . 11
; ; |
50 | 26 | nnzi 11401 |
. . . . . . . . . . . . . 14
|
51 | | zmulcl 11426 |
. . . . . . . . . . . . . 14
|
52 | 38, 50, 51 | mp2an 708 |
. . . . . . . . . . . . 13
|
53 | | zltp1le 11427 |
. . . . . . . . . . . . 13
; ; ; ;
; ; |
54 | 52, 17, 53 | mp2an 708 |
. . . . . . . . . . . 12
; ;
; ; |
55 | | 1t10e1p1e11OLD 41320 |
. . . . . . . . . . . . . 14
; |
56 | 55 | eqcomi 2631 |
. . . . . . . . . . . . 13
; |
57 | 56 | breq1i 4660 |
. . . . . . . . . . . 12
; ; ; ; ; |
58 | 54, 57 | bitri 264 |
. . . . . . . . . . 11
; ; ; ; ; |
59 | 49, 58 | mpbi 220 |
. . . . . . . . . 10
; ; ; |
60 | | eluz2 11693 |
. . . . . . . . . 10
; ; ;
; ; ; ; ; ; |
61 | 5, 17, 59, 60 | mpbir3an 1244 |
. . . . . . . . 9
; ; ; |
62 | 61 | a1i 11 |
. . . . . . . 8
RePart ;
; ; ..^
; Odd
; ; ; ; ; |
63 | | 4nn 11187 |
. . . . . . . . . . . 12
|
64 | 2, 7 | decnncl 11518 |
. . . . . . . . . . . . . 14
; |
65 | 64 | nnnn0i 11300 |
. . . . . . . . . . . . 13
; |
66 | | nnexpcl 12873 |
. . . . . . . . . . . . 13
; ; |
67 | 9, 65, 66 | mp2an 708 |
. . . . . . . . . . . 12
; |
68 | 63, 67 | nnmulcli 11044 |
. . . . . . . . . . 11
; |
69 | 68 | nnzi 11401 |
. . . . . . . . . 10
; |
70 | | 4re 11097 |
. . . . . . . . . . . . 13
|
71 | 18, 70 | pm3.2i 471 |
. . . . . . . . . . . 12
|
72 | | 1lt4 11199 |
. . . . . . . . . . . . 13
|
73 | 21, 72 | pm3.2i 471 |
. . . . . . . . . . . 12
|
74 | 67 | nnrei 11029 |
. . . . . . . . . . . . 13
; |
75 | 27, 74 | pm3.2i 471 |
. . . . . . . . . . . 12
; |
76 | 64 | nnzi 11401 |
. . . . . . . . . . . . . . 15
; |
77 | 31, 38, 76 | 3pm3.2i 1239 |
. . . . . . . . . . . . . 14
; |
78 | 3, 6, 2, 22 | decltiOLD 11548 |
. . . . . . . . . . . . . . 15
; |
79 | 22, 78 | pm3.2i 471 |
. . . . . . . . . . . . . 14
; |
80 | | ltexp2a 12912 |
. . . . . . . . . . . . . 14
; ; ; |
81 | 77, 79, 80 | mp2an 708 |
. . . . . . . . . . . . 13
; |
82 | 37, 81 | pm3.2i 471 |
. . . . . . . . . . . 12
; |
83 | | ltmul12a 10879 |
. . . . . . . . . . . 12
;
; ; |
84 | 71, 73, 75, 82, 83 | mp4an 709 |
. . . . . . . . . . 11
; |
85 | | 4z 11411 |
. . . . . . . . . . . . . 14
|
86 | 67 | nnzi 11401 |
. . . . . . . . . . . . . 14
; |
87 | | zmulcl 11426 |
. . . . . . . . . . . . . 14
; ; |
88 | 85, 86, 87 | mp2an 708 |
. . . . . . . . . . . . 13
; |
89 | | zltp1le 11427 |
. . . . . . . . . . . . 13
; ;
; |
90 | 52, 88, 89 | mp2an 708 |
. . . . . . . . . . . 12
;
; |
91 | 56 | breq1i 4660 |
. . . . . . . . . . . 12
; ; ; |
92 | 90, 91 | bitri 264 |
. . . . . . . . . . 11
; ; ; |
93 | 84, 92 | mpbi 220 |
. . . . . . . . . 10
; ; |
94 | | eluz2 11693 |
. . . . . . . . . 10
; ;
; ; ; ; |
95 | 5, 69, 93, 94 | mpbir3an 1244 |
. . . . . . . . 9
; ; |
96 | 95 | a1i 11 |
. . . . . . . 8
RePart ;
; ; ..^
; Odd
; ; ; ; |
97 | | simpl 473 |
. . . . . . . . . . . 12
Even
; Even |
98 | | simprl 794 |
. . . . . . . . . . . 12
Even
; |
99 | | evenz 41543 |
. . . . . . . . . . . . . . . 16
Even |
100 | 99 | zred 11482 |
. . . . . . . . . . . . . . 15
Even |
101 | 68 | nnrei 11029 |
. . . . . . . . . . . . . . 15
; |
102 | | ltle 10126 |
. . . . . . . . . . . . . . 15
; ; ; |
103 | 100, 101,
102 | sylancl 694 |
. . . . . . . . . . . . . 14
Even ; ; |
104 | 103 | a1d 25 |
. . . . . . . . . . . . 13
Even
; ; |
105 | 104 | imp32 449 |
. . . . . . . . . . . 12
Even
; ; |
106 | | ax-bgbltosilvaOLD 41706 |
. . . . . . . . . . . 12
Even ;
GoldbachEven |
107 | 97, 98, 105, 106 | syl3anc 1326 |
. . . . . . . . . . 11
Even
; GoldbachEven |
108 | 107 | ex 450 |
. . . . . . . . . 10
Even ;
GoldbachEven |
109 | 108 | a1i 11 |
. . . . . . . . 9
RePart ;
; ; ..^
; Odd
; ; Even
;
GoldbachEven |
110 | 109 | ralrimiv 2965 |
. . . . . . . 8
RePart ;
; ; ..^
; Odd
; ; Even
;
GoldbachEven |
111 | | simpl 473 |
. . . . . . . . 9
RePart
|
112 | 111 | ad2antrr 762 |
. . . . . . . 8
RePart ;
; ; ..^
; Odd
; ; |
113 | | simpr 477 |
. . . . . . . . 9
RePart
RePart |
114 | 113 | ad2antrr 762 |
. . . . . . . 8
RePart ;
; ; ..^
; Odd
; ; RePart |
115 | | simpr 477 |
. . . . . . . . 9
; ; ; ..^
;
..^ ; |
116 | 115 | ad2antlr 763 |
. . . . . . . 8
RePart ;
; ; ..^
; Odd
; ; ..^
; |
117 | | simpl1 1064 |
. . . . . . . . 9
; ; ; ..^
; |
118 | 117 | ad2antlr 763 |
. . . . . . . 8
RePart ;
; ; ..^
; Odd
; ; |
119 | | simpl2 1065 |
. . . . . . . . 9
; ; ; ..^
; ; |
120 | 119 | ad2antlr 763 |
. . . . . . . 8
RePart ;
; ; ..^
; Odd
; ; ; |
121 | 6, 11 | decnncl 11518 |
. . . . . . . . . . . . . . 15
; |
122 | 121 | nnrei 11029 |
. . . . . . . . . . . . . 14
; |
123 | 15 | nngt0i 11054 |
. . . . . . . . . . . . . . 15
; |
124 | 28, 123 | pm3.2i 471 |
. . . . . . . . . . . . . 14
; ; |
125 | 19, 122, 124 | 3pm3.2i 1239 |
. . . . . . . . . . . . 13
; ; ; ; |
126 | | 8lt9 11222 |
. . . . . . . . . . . . . 14
|
127 | 6, 6, 11, 126 | declt 11530 |
. . . . . . . . . . . . 13
; ; |
128 | | ltmul1a 10872 |
. . . . . . . . . . . . 13
; ; ; ; ; ; ; ; ; ; |
129 | 125, 127,
128 | mp2an 708 |
. . . . . . . . . . . 12
; ; ; ; |
130 | | breq2 4657 |
. . . . . . . . . . . 12
; ; ; ;
; ; ; ; |
131 | 129, 130 | mpbiri 248 |
. . . . . . . . . . 11
; ; ; ; |
132 | 131 | 3ad2ant3 1084 |
. . . . . . . . . 10
; ; ;
; ; |
133 | 132 | adantr 481 |
. . . . . . . . 9
; ; ; ..^
; ; ; |
134 | 133 | ad2antlr 763 |
. . . . . . . 8
RePart ;
; ; ..^
; Odd
; ; ; ; |
135 | 121, 15 | nnmulcli 11044 |
. . . . . . . . . . . . 13
; ; |
136 | 135 | nnrei 11029 |
. . . . . . . . . . . 12
; ; |
137 | | eleq1 2689 |
. . . . . . . . . . . 12
; ; ; ; |
138 | 136, 137 | mpbiri 248 |
. . . . . . . . . . 11
; ; |
139 | 138 | 3ad2ant3 1084 |
. . . . . . . . . 10
; ; ;
|
140 | 139 | adantr 481 |
. . . . . . . . 9
; ; ; ..^
; |
141 | 140 | ad2antlr 763 |
. . . . . . . 8
RePart ;
; ; ..^
; Odd
; ; |
142 | 62, 96, 110, 112, 114, 116, 118, 120, 134, 141 | bgoldbtbnd 41697 |
. . . . . . 7
RePart ;
; ; ..^
; Odd
; ; Odd
; ;
GoldbachOdd |
143 | 142 | exp31 630 |
. . . . . 6
RePart
; ; ; ..^
; Odd
; ;
Odd
; ;
GoldbachOdd |
144 | 143 | rexlimdva 3031 |
. . . . 5
RePart ; ; ; ..^
; Odd
; ;
Odd
; ;
GoldbachOdd |
145 | 144 | imp 445 |
. . . 4
RePart ; ; ; ..^
; Odd
; ;
Odd ; ;
GoldbachOdd |
146 | 145 | rexlimiva 3028 |
. . 3
RePart ;
; ; ..^
; Odd
; ;
Odd
; ;
GoldbachOdd |
147 | | breq2 4657 |
. . . . . . . 8
|
148 | | breq1 4656 |
. . . . . . . 8
; ;
; ; |
149 | 147, 148 | anbi12d 747 |
. . . . . . 7
; ;
; ; |
150 | | eleq1 2689 |
. . . . . . 7
GoldbachOdd
GoldbachOdd |
151 | 149, 150 | imbi12d 334 |
. . . . . 6
; ;
GoldbachOdd
; ;
GoldbachOdd |
152 | 151 | rspcv 3305 |
. . . . 5
Odd Odd
; ;
GoldbachOdd ; ;
GoldbachOdd |
153 | 152 | com23 86 |
. . . 4
Odd ; ;
Odd
; ;
GoldbachOdd GoldbachOdd |
154 | 153 | 3impib 1262 |
. . 3
Odd ; ;
Odd
; ;
GoldbachOdd GoldbachOdd |
155 | 146, 154 | sylcom 30 |
. 2
RePart ;
; ; ..^
; Odd
; ;
GoldbachOdd |
156 | 1, 155 | ax-mp 5 |
1
Odd ; ;
GoldbachOdd |