Metamath Proof Explorer

Theorem nnsum3primesle9

Description: Every integer greater than 1 and less than or equal to 8 is the sum of at most 3 primes. (Contributed by AV, 2-Aug-2020)

Ref Expression
Assertion nnsum3primesle9 ⊢N∈ℤ≥2∧N≤8→∃d∈ℕ∃f∈ℙ1…dd≤3∧N=∑k=1df⁡k

Proof

Step Hyp Ref Expression
1 eluzelre ⊢N∈ℤ≥2→N∈ℝ
2 8re ⊢8∈ℝ
3 2 a1i ⊢N∈ℤ≥2→8∈ℝ
4 1 3 leloed ⊢N∈ℤ≥2→N≤8↔N<8∨N=8
5 eluzelz ⊢N∈ℤ≥2→N∈ℤ
6 7nn ⊢7∈ℕ
7 6 nnzi ⊢7∈ℤ
8 zleltp1 ⊢N∈ℤ∧7∈ℤ→N≤7↔N<7+1
9 5 7 8 sylancl ⊢N∈ℤ≥2→N≤7↔N<7+1
10 7re ⊢7∈ℝ
11 10 a1i ⊢N∈ℤ≥2→7∈ℝ
12 1 11 leloed ⊢N∈ℤ≥2→N≤7↔N<7∨N=7
13 7p1e8 ⊢7+1=8
14 13 breq2i ⊢N<7+1↔N<8
15 14 a1i ⊢N∈ℤ≥2→N<7+1↔N<8
16 9 12 15 3bitr3rd ⊢N∈ℤ≥2→N<8↔N<7∨N=7
17 6nn ⊢6∈ℕ
18 17 nnzi ⊢6∈ℤ
19 zleltp1 ⊢N∈ℤ∧6∈ℤ→N≤6↔N<6+1
20 5 18 19 sylancl ⊢N∈ℤ≥2→N≤6↔N<6+1
21 6re ⊢6∈ℝ
22 21 a1i ⊢N∈ℤ≥2→6∈ℝ
23 1 22 leloed ⊢N∈ℤ≥2→N≤6↔N<6∨N=6
24 6p1e7 ⊢6+1=7
25 24 breq2i ⊢N<6+1↔N<7
26 25 a1i ⊢N∈ℤ≥2→N<6+1↔N<7
27 20 23 26 3bitr3rd ⊢N∈ℤ≥2→N<7↔N<6∨N=6
28 5nn ⊢5∈ℕ
29 28 nnzi ⊢5∈ℤ
30 zleltp1 ⊢N∈ℤ∧5∈ℤ→N≤5↔N<5+1
31 5 29 30 sylancl ⊢N∈ℤ≥2→N≤5↔N<5+1
32 5re ⊢5∈ℝ
33 32 a1i ⊢N∈ℤ≥2→5∈ℝ
34 1 33 leloed ⊢N∈ℤ≥2→N≤5↔N<5∨N=5
35 5p1e6 ⊢5+1=6
36 35 breq2i ⊢N<5+1↔N<6
37 36 a1i ⊢N∈ℤ≥2→N<5+1↔N<6
38 31 34 37 3bitr3rd ⊢N∈ℤ≥2→N<6↔N<5∨N=5
39 4z ⊢4∈ℤ
40 zleltp1 ⊢N∈ℤ∧4∈ℤ→N≤4↔N<4+1
41 5 39 40 sylancl ⊢N∈ℤ≥2→N≤4↔N<4+1
42 4re ⊢4∈ℝ
43 42 a1i ⊢N∈ℤ≥2→4∈ℝ
44 1 43 leloed ⊢N∈ℤ≥2→N≤4↔N<4∨N=4
45 4p1e5 ⊢4+1=5
46 45 breq2i ⊢N<4+1↔N<5
47 46 a1i ⊢N∈ℤ≥2→N<4+1↔N<5
48 41 44 47 3bitr3rd ⊢N∈ℤ≥2→N<5↔N<4∨N=4
49 3z ⊢3∈ℤ
50 zleltp1 ⊢N∈ℤ∧3∈ℤ→N≤3↔N<3+1
51 5 49 50 sylancl ⊢N∈ℤ≥2→N≤3↔N<3+1
52 3re ⊢3∈ℝ
53 52 a1i ⊢N∈ℤ≥2→3∈ℝ
54 1 53 leloed ⊢N∈ℤ≥2→N≤3↔N<3∨N=3
55 3p1e4 ⊢3+1=4
56 55 breq2i ⊢N<3+1↔N<4
57 56 a1i ⊢N∈ℤ≥2→N<3+1↔N<4
58 51 54 57 3bitr3rd ⊢N∈ℤ≥2→N<4↔N<3∨N=3
59 eluz2 ⊢N∈ℤ≥2↔2∈ℤ∧N∈ℤ∧2≤N
60 2re ⊢2∈ℝ
61 60 a1i ⊢N∈ℤ→2∈ℝ
62 zre ⊢N∈ℤ→N∈ℝ
63 61 62 leloed ⊢N∈ℤ→2≤N↔2<N∨2=N
64 3m1e2 ⊢3−1=2
65 64 eqcomi ⊢2=3−1
66 65 breq1i ⊢2<N↔3−1<N
67 zlem1lt ⊢3∈ℤ∧N∈ℤ→3≤N↔3−1<N
68 49 67 mpan ⊢N∈ℤ→3≤N↔3−1<N
69 68 biimprd ⊢N∈ℤ→3−1<N→3≤N
70 66 69 biimtrid ⊢N∈ℤ→2<N→3≤N
71 52 a1i ⊢N∈ℤ→3∈ℝ
72 71 62 lenltd ⊢N∈ℤ→3≤N↔¬N<3
73 pm2.21 ⊢¬N<3→N<3→N=2
74 72 73 syl6bi ⊢N∈ℤ→3≤N→N<3→N=2
75 70 74 syldc ⊢2<N→N∈ℤ→N<3→N=2
76 eqcom ⊢2=N↔N=2
77 76 biimpi ⊢2=N→N=2
78 77 2a1d ⊢2=N→N∈ℤ→N<3→N=2
79 75 78 jaoi ⊢2<N∨2=N→N∈ℤ→N<3→N=2
80 79 com12 ⊢N∈ℤ→2<N∨2=N→N<3→N=2
81 63 80 sylbid ⊢N∈ℤ→2≤N→N<3→N=2
82 81 imp ⊢N∈ℤ∧2≤N→N<3→N=2
83 2lt3 ⊢2<3
84 breq1 ⊢N=2→N<3↔2<3
85 83 84 mpbiri ⊢N=2→N<3
86 82 85 impbid1 ⊢N∈ℤ∧2≤N→N<3↔N=2
87 86 3adant1 ⊢2∈ℤ∧N∈ℤ∧2≤N→N<3↔N=2
88 59 87 sylbi ⊢N∈ℤ≥2→N<3↔N=2
89 88 orbi1d ⊢N∈ℤ≥2→N<3∨N=3↔N=2∨N=3
90 58 89 bitrd ⊢N∈ℤ≥2→N<4↔N=2∨N=3
91 90 orbi1d ⊢N∈ℤ≥2→N<4∨N=4↔N=2∨N=3∨N=4
92 48 91 bitrd ⊢N∈ℤ≥2→N<5↔N=2∨N=3∨N=4
93 92 orbi1d ⊢N∈ℤ≥2→N<5∨N=5↔N=2∨N=3∨N=4∨N=5
94 38 93 bitrd ⊢N∈ℤ≥2→N<6↔N=2∨N=3∨N=4∨N=5
95 94 orbi1d ⊢N∈ℤ≥2→N<6∨N=6↔N=2∨N=3∨N=4∨N=5∨N=6
96 27 95 bitrd ⊢N∈ℤ≥2→N<7↔N=2∨N=3∨N=4∨N=5∨N=6
97 96 orbi1d ⊢N∈ℤ≥2→N<7∨N=7↔N=2∨N=3∨N=4∨N=5∨N=6∨N=7
98 16 97 bitrd ⊢N∈ℤ≥2→N<8↔N=2∨N=3∨N=4∨N=5∨N=6∨N=7
99 98 orbi1d ⊢N∈ℤ≥2→N<8∨N=8↔N=2∨N=3∨N=4∨N=5∨N=6∨N=7∨N=8
100 99 biimpd ⊢N∈ℤ≥2→N<8∨N=8→N=2∨N=3∨N=4∨N=5∨N=6∨N=7∨N=8
101 4 100 sylbid ⊢N∈ℤ≥2→N≤8→N=2∨N=3∨N=4∨N=5∨N=6∨N=7∨N=8
102 101 imp ⊢N∈ℤ≥2∧N≤8→N=2∨N=3∨N=4∨N=5∨N=6∨N=7∨N=8
103 2prm ⊢2∈ℙ
104 eleq1 ⊢N=2→N∈ℙ↔2∈ℙ
105 103 104 mpbiri ⊢N=2→N∈ℙ
106 nnsum3primesprm ⊢N∈ℙ→∃d∈ℕ∃f∈ℙ1…dd≤3∧N=∑k=1df⁡k
107 105 106 syl ⊢N=2→∃d∈ℕ∃f∈ℙ1…dd≤3∧N=∑k=1df⁡k
108 3prm ⊢3∈ℙ
109 eleq1 ⊢N=3→N∈ℙ↔3∈ℙ
110 108 109 mpbiri ⊢N=3→N∈ℙ
111 110 106 syl ⊢N=3→∃d∈ℕ∃f∈ℙ1…dd≤3∧N=∑k=1df⁡k
112 107 111 jaoi ⊢N=2∨N=3→∃d∈ℕ∃f∈ℙ1…dd≤3∧N=∑k=1df⁡k
113 nnsum3primes4 ⊢∃d∈ℕ∃f∈ℙ1…dd≤3∧4=∑k=1df⁡k
114 eqeq1 ⊢N=4→N=∑k=1df⁡k↔4=∑k=1df⁡k
115 114 anbi2d ⊢N=4→d≤3∧N=∑k=1df⁡k↔d≤3∧4=∑k=1df⁡k
116 115 2rexbidv ⊢N=4→∃d∈ℕ∃f∈ℙ1…dd≤3∧N=∑k=1df⁡k↔∃d∈ℕ∃f∈ℙ1…dd≤3∧4=∑k=1df⁡k
117 113 116 mpbiri ⊢N=4→∃d∈ℕ∃f∈ℙ1…dd≤3∧N=∑k=1df⁡k
118 112 117 jaoi ⊢N=2∨N=3∨N=4→∃d∈ℕ∃f∈ℙ1…dd≤3∧N=∑k=1df⁡k
119 5prm ⊢5∈ℙ
120 eleq1 ⊢N=5→N∈ℙ↔5∈ℙ
121 119 120 mpbiri ⊢N=5→N∈ℙ
122 121 106 syl ⊢N=5→∃d∈ℕ∃f∈ℙ1…dd≤3∧N=∑k=1df⁡k
123 118 122 jaoi ⊢N=2∨N=3∨N=4∨N=5→∃d∈ℕ∃f∈ℙ1…dd≤3∧N=∑k=1df⁡k
124 6gbe ⊢6∈GoldbachEven
125 eleq1 ⊢N=6→N∈GoldbachEven↔6∈GoldbachEven
126 124 125 mpbiri ⊢N=6→N∈GoldbachEven
127 nnsum3primesgbe ⊢N∈GoldbachEven→∃d∈ℕ∃f∈ℙ1…dd≤3∧N=∑k=1df⁡k
128 126 127 syl ⊢N=6→∃d∈ℕ∃f∈ℙ1…dd≤3∧N=∑k=1df⁡k
129 123 128 jaoi ⊢N=2∨N=3∨N=4∨N=5∨N=6→∃d∈ℕ∃f∈ℙ1…dd≤3∧N=∑k=1df⁡k
130 7prm ⊢7∈ℙ
131 eleq1 ⊢N=7→N∈ℙ↔7∈ℙ
132 130 131 mpbiri ⊢N=7→N∈ℙ
133 132 106 syl ⊢N=7→∃d∈ℕ∃f∈ℙ1…dd≤3∧N=∑k=1df⁡k
134 129 133 jaoi ⊢N=2∨N=3∨N=4∨N=5∨N=6∨N=7→∃d∈ℕ∃f∈ℙ1…dd≤3∧N=∑k=1df⁡k
135 8gbe ⊢8∈GoldbachEven
136 eleq1 ⊢N=8→N∈GoldbachEven↔8∈GoldbachEven
137 135 136 mpbiri ⊢N=8→N∈GoldbachEven
138 137 127 syl ⊢N=8→∃d∈ℕ∃f∈ℙ1…dd≤3∧N=∑k=1df⁡k
139 134 138 jaoi ⊢N=2∨N=3∨N=4∨N=5∨N=6∨N=7∨N=8→∃d∈ℕ∃f∈ℙ1…dd≤3∧N=∑k=1df⁡k
140 102 139 syl ⊢N∈ℤ≥2∧N≤8→∃d∈ℕ∃f∈ℙ1…dd≤3∧N=∑k=1df⁡k