Step | Hyp | Ref
| Expression |
1 | | oddz 38754 |
. . . 4
 Odd   |
2 | | 5nn 10767 |
. . . . . . . 8
 |
3 | 2 | nnzi 10958 |
. . . . . . 7
 |
4 | | zltp1le 10983 |
. . . . . . 7
 
       |
5 | 3, 4 | mpan 675 |
. . . . . 6
 
     |
6 | | 5p1e6 10734 |
. . . . . . . . 9
   |
7 | 6 | breq1i 4408 |
. . . . . . . 8
  
  |
8 | | 6re 10687 |
. . . . . . . . . 10
 |
9 | 8 | a1i 11 |
. . . . . . . . 9
   |
10 | | zre 10938 |
. . . . . . . . 9
   |
11 | 9, 10 | leloed 9775 |
. . . . . . . 8
 
     |
12 | 7, 11 | syl5bb 261 |
. . . . . . 7
   
     |
13 | | 6nn 10768 |
. . . . . . . . . . . . 13
 |
14 | 13 | nnzi 10958 |
. . . . . . . . . . . 12
 |
15 | | zltp1le 10983 |
. . . . . . . . . . . 12
 
       |
16 | 14, 15 | mpan 675 |
. . . . . . . . . . 11
 
     |
17 | | 6p1e7 10735 |
. . . . . . . . . . . . . 14
   |
18 | 17 | breq1i 4408 |
. . . . . . . . . . . . 13
  
  |
19 | | 7re 10689 |
. . . . . . . . . . . . . . 15
 |
20 | 19 | a1i 11 |
. . . . . . . . . . . . . 14
   |
21 | 20, 10 | leloed 9775 |
. . . . . . . . . . . . 13
 
     |
22 | 18, 21 | syl5bb 261 |
. . . . . . . . . . . 12
   
     |
23 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . 20
  
 Odd Odd  |
24 | | 3odd 38829 |
. . . . . . . . . . . . . . . . . . . 20
Odd |
25 | 23, 24 | jctir 541 |
. . . . . . . . . . . . . . . . . . 19
  
 Odd  Odd
Odd   |
26 | | omoeALTV 38808 |
. . . . . . . . . . . . . . . . . . 19
  Odd Odd
  Even  |
27 | | breq2 4405 |
. . . . . . . . . . . . . . . . . . . . 21
   
     |
28 | | eleq1 2516 |
. . . . . . . . . . . . . . . . . . . . 21
   
GoldbachEven   GoldbachEven   |
29 | 27, 28 | imbi12d 322 |
. . . . . . . . . . . . . . . . . . . 20
    
GoldbachEven
     GoldbachEven    |
30 | 29 | rspcv 3145 |
. . . . . . . . . . . . . . . . . . 19
   Even   Even 
GoldbachEven 
   
GoldbachEven    |
31 | 25, 26, 30 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
  
 Odd   Even 
GoldbachEven 
   
GoldbachEven    |
32 | | 4p3e7 10742 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   |
33 | 32 | eqcomi 2459 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
34 | 33 | breq1i 4408 |
. . . . . . . . . . . . . . . . . . . . . 22

    |
35 | | 4re 10683 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 |
36 | 35 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
37 | | 3re 10680 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 |
38 | 37 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
39 | | ltaddsub 10085 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
   
     |
40 | 39 | biimpd 211 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
   
     |
41 | 36, 38, 10, 40 | syl3anc 1267 |
. . . . . . . . . . . . . . . . . . . . . 22
   
     |
42 | 34, 41 | syl5bi 221 |
. . . . . . . . . . . . . . . . . . . . 21
 
     |
43 | 42 | impcom 432 |
. . . . . . . . . . . . . . . . . . . 20
 
     |
44 | 43 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
  
 Odd     |
45 | | pm2.27 40 |
. . . . . . . . . . . . . . . . . . 19
         GoldbachEven  
GoldbachEven   |
46 | 44, 45 | syl 17 |
. . . . . . . . . . . . . . . . . 18
  
 Odd    
  GoldbachEven   GoldbachEven   |
47 | | isgbe 38846 |
. . . . . . . . . . . . . . . . . . 19
   GoldbachEven    Even    Odd
Odd         |
48 | | 3prm 14634 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 |
49 | 48 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   |
50 | | zcn 10939 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
   |
51 | | 3cn 10681 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
 |
52 | 50, 51 | jctir 541 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
 
   |
53 | | npcan 9881 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
 
       |
54 | 53 | eqcomd 2456 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
 
       |
55 | 52, 54 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
       |
56 | | oveq2 6296 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
           |
57 | 56 | eqcoms 2458 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
           |
58 | 55, 57 | sylan9eq 2504 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 
       |
59 | 49, 58 | rspcedeq2vd 3156 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
        |
60 | | oveq1 6295 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
               |
61 | 60 | eqeq2d 2460 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
         
       |
62 | 61 | rexbidv 2900 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
      
   
        |
63 | 59, 62 | syl5ib 223 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
              |
64 | 63 | 3ad2ant3 1030 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
  Odd Odd     

        |
65 | 64 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   Odd
Odd              |
66 | 65 | ad4antlr 738 |
. . . . . . . . . . . . . . . . . . . . . . . 24
      Odd 
   Odd
Odd              |
67 | 66 | reximdva 2861 |
. . . . . . . . . . . . . . . . . . . . . . 23
   

Odd 
   Odd
Odd     
         |
68 | 67 | reximdva 2861 |
. . . . . . . . . . . . . . . . . . . . . 22
  
 Odd     Odd Odd     
          |
69 | 68, 23 | jctild 546 |
. . . . . . . . . . . . . . . . . . . . 21
  
 Odd     Odd Odd     
 Odd            |
70 | | isgbo 38847 |
. . . . . . . . . . . . . . . . . . . . 21
 GoldbachOdd  Odd           |
71 | 69, 70 | syl6ibr 231 |
. . . . . . . . . . . . . . . . . . . 20
  
 Odd     Odd Odd     
GoldbachOdd   |
72 | 71 | adantld 469 |
. . . . . . . . . . . . . . . . . . 19
  
 Odd     Even    Odd
Odd       GoldbachOdd   |
73 | 47, 72 | syl5bi 221 |
. . . . . . . . . . . . . . . . . 18
  
 Odd    GoldbachEven GoldbachOdd   |
74 | 31, 46, 73 | 3syld 57 |
. . . . . . . . . . . . . . . . 17
  
 Odd   Even 
GoldbachEven GoldbachOdd   |
75 | 74 | ex 436 |
. . . . . . . . . . . . . . . 16
 
  Odd   Even 
GoldbachEven
GoldbachOdd    |
76 | 75 | com23 81 |
. . . . . . . . . . . . . . 15
 
   Even 
GoldbachEven  Odd
GoldbachOdd    |
77 | 76 | ex 436 |
. . . . . . . . . . . . . 14
    Even 
GoldbachEven
 Odd GoldbachOdd     |
78 | | 7gbo 38867 |
. . . . . . . . . . . . . . . . . 18
GoldbachOdd |
79 | | eleq1 2516 |
. . . . . . . . . . . . . . . . . 18
 
GoldbachOdd
GoldbachOdd   |
80 | 78, 79 | mpbii 215 |
. . . . . . . . . . . . . . . . 17
 GoldbachOdd  |
81 | 80 | a1d 26 |
. . . . . . . . . . . . . . . 16
  Odd
GoldbachOdd   |
82 | 81 | a1d 26 |
. . . . . . . . . . . . . . 15
  
Even  GoldbachEven
 Odd GoldbachOdd    |
83 | 82 | a1d 26 |
. . . . . . . . . . . . . 14
    Even 
GoldbachEven
 Odd GoldbachOdd     |
84 | 77, 83 | jaoi 381 |
. . . . . . . . . . . . 13
   
 
Even 
GoldbachEven  Odd
GoldbachOdd     |
85 | 84 | com12 32 |
. . . . . . . . . . . 12
  

 
Even 
GoldbachEven  Odd
GoldbachOdd     |
86 | 22, 85 | sylbid 219 |
. . . . . . . . . . 11
   
  Even 
GoldbachEven
 Odd GoldbachOdd     |
87 | 16, 86 | sylbid 219 |
. . . . . . . . . 10
 
  Even 
GoldbachEven
 Odd GoldbachOdd     |
88 | 87 | com12 32 |
. . . . . . . . 9
    Even 
GoldbachEven
 Odd GoldbachOdd     |
89 | | eleq1 2516 |
. . . . . . . . . . . 12
  Odd
Odd   |
90 | | 6even 38832 |
. . . . . . . . . . . . 13
Even |
91 | | evennodd 38767 |
. . . . . . . . . . . . . 14
 Even
Odd  |
92 | 91 | pm2.21d 110 |
. . . . . . . . . . . . 13
 Even  Odd
GoldbachOdd   |
93 | 90, 92 | ax-mp 5 |
. . . . . . . . . . . 12
 Odd GoldbachOdd  |
94 | 89, 93 | syl6bir 233 |
. . . . . . . . . . 11
  Odd
GoldbachOdd   |
95 | 94 | a1d 26 |
. . . . . . . . . 10
  
Even  GoldbachEven
 Odd GoldbachOdd    |
96 | 95 | a1d 26 |
. . . . . . . . 9
    Even 
GoldbachEven
 Odd GoldbachOdd     |
97 | 88, 96 | jaoi 381 |
. . . . . . . 8
   
 
Even 
GoldbachEven  Odd
GoldbachOdd     |
98 | 97 | com12 32 |
. . . . . . 7
  

 
Even 
GoldbachEven  Odd
GoldbachOdd     |
99 | 12, 98 | sylbid 219 |
. . . . . 6
   
  Even 
GoldbachEven
 Odd GoldbachOdd     |
100 | 5, 99 | sylbid 219 |
. . . . 5
 
  Even 
GoldbachEven
 Odd GoldbachOdd     |
101 | 100 | com24 90 |
. . . 4
  Odd
 
Even 
GoldbachEven 
GoldbachOdd     |
102 | 1, 101 | mpcom 37 |
. . 3
 Odd   Even 
GoldbachEven 
GoldbachOdd    |
103 | 102 | impcom 432 |
. 2
   Even 
GoldbachEven Odd
 GoldbachOdd   |
104 | 103 | ralrimiva 2801 |
1
 
Even 
GoldbachEven  Odd 
GoldbachOdd   |