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 \in ℤ_{\geq 2} \land N \leq 8) \to \exists d \in ℕ \exists f \in (ℙ^{(1 \dots d)}) (d \leq 3 \land N = \sum_{k = 1}^{d} f (k))$

Proof

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

Metamath Proof Explorer

Theorem nnsum3primesle9

Proof