gbowgt5 - Mathbox for Alexander van der Vekens

	Mathbox for Alexander van der Vekens		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > gbowgt5		Structured version Visualization version GIF version

Theorem gbowgt5 48253

Description: Any weak odd Goldbach number is greater than 5. (Contributed by AV, 20-Jul-2020.)

**Assertion**
Ref	Expression
gbowgt5	⊢ (𝑍 ∈ GoldbachOddW → 5 < 𝑍)

Proof of Theorem gbowgt5 Dummy variables 𝑝 𝑞 𝑟 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		isgbow 48243	. 2 ⊢ (𝑍 ∈ GoldbachOddW ↔ (𝑍 ∈ Odd ∧ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑍 = ((𝑝 + 𝑞) + 𝑟)))
2		prmuz2 16656	. . . . . . . . 9 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ (ℤ_≥‘2))
3		eluz2 12785	. . . . . . . . 9 ⊢ (𝑝 ∈ (ℤ_≥‘2) ↔ (2 ∈ ℤ ∧ 𝑝 ∈ ℤ ∧ 2 ≤ 𝑝))
4	2, 3	sylib 219	. . . . . . . 8 ⊢ (𝑝 ∈ ℙ → (2 ∈ ℤ ∧ 𝑝 ∈ ℤ ∧ 2 ≤ 𝑝))
5		prmuz2 16656	. . . . . . . . 9 ⊢ (𝑞 ∈ ℙ → 𝑞 ∈ (ℤ_≥‘2))
6		eluz2 12785	. . . . . . . . 9 ⊢ (𝑞 ∈ (ℤ_≥‘2) ↔ (2 ∈ ℤ ∧ 𝑞 ∈ ℤ ∧ 2 ≤ 𝑞))
7	5, 6	sylib 219	. . . . . . . 8 ⊢ (𝑞 ∈ ℙ → (2 ∈ ℤ ∧ 𝑞 ∈ ℤ ∧ 2 ≤ 𝑞))
8	4, 7	anim12i 619	. . . . . . 7 ⊢ ((𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ) → ((2 ∈ ℤ ∧ 𝑝 ∈ ℤ ∧ 2 ≤ 𝑝) ∧ (2 ∈ ℤ ∧ 𝑞 ∈ ℤ ∧ 2 ≤ 𝑞)))
9		prmuz2 16656	. . . . . . . 8 ⊢ (𝑟 ∈ ℙ → 𝑟 ∈ (ℤ_≥‘2))
10		eluz2 12785	. . . . . . . 8 ⊢ (𝑟 ∈ (ℤ_≥‘2) ↔ (2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟))
11	9, 10	sylib 219	. . . . . . 7 ⊢ (𝑟 ∈ ℙ → (2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟))
12		zre 12519	. . . . . . . . . . . . . 14 ⊢ (𝑝 ∈ ℤ → 𝑝 ∈ ℝ)
13	12	3ad2ant2 1140	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℤ ∧ 𝑝 ∈ ℤ ∧ 2 ≤ 𝑝) → 𝑝 ∈ ℝ)
14		zre 12519	. . . . . . . . . . . . . 14 ⊢ (𝑞 ∈ ℤ → 𝑞 ∈ ℝ)
15	14	3ad2ant2 1140	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℤ ∧ 𝑞 ∈ ℤ ∧ 2 ≤ 𝑞) → 𝑞 ∈ ℝ)
16	13, 15	anim12i 619	. . . . . . . . . . . 12 ⊢ (((2 ∈ ℤ ∧ 𝑝 ∈ ℤ ∧ 2 ≤ 𝑝) ∧ (2 ∈ ℤ ∧ 𝑞 ∈ ℤ ∧ 2 ≤ 𝑞)) → (𝑝 ∈ ℝ ∧ 𝑞 ∈ ℝ))
17		2re 12246	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℝ
18	17, 17	pm3.2i 471	. . . . . . . . . . . 12 ⊢ (2 ∈ ℝ ∧ 2 ∈ ℝ)
19	16, 18	jctil 524	. . . . . . . . . . 11 ⊢ (((2 ∈ ℤ ∧ 𝑝 ∈ ℤ ∧ 2 ≤ 𝑝) ∧ (2 ∈ ℤ ∧ 𝑞 ∈ ℤ ∧ 2 ≤ 𝑞)) → ((2 ∈ ℝ ∧ 2 ∈ ℝ) ∧ (𝑝 ∈ ℝ ∧ 𝑞 ∈ ℝ)))
20		simp3 1144	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℤ ∧ 𝑝 ∈ ℤ ∧ 2 ≤ 𝑝) → 2 ≤ 𝑝)
21		simp3 1144	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℤ ∧ 𝑞 ∈ ℤ ∧ 2 ≤ 𝑞) → 2 ≤ 𝑞)
22	20, 21	anim12i 619	. . . . . . . . . . 11 ⊢ (((2 ∈ ℤ ∧ 𝑝 ∈ ℤ ∧ 2 ≤ 𝑝) ∧ (2 ∈ ℤ ∧ 𝑞 ∈ ℤ ∧ 2 ≤ 𝑞)) → (2 ≤ 𝑝 ∧ 2 ≤ 𝑞))
23		le2add 11623	. . . . . . . . . . 11 ⊢ (((2 ∈ ℝ ∧ 2 ∈ ℝ) ∧ (𝑝 ∈ ℝ ∧ 𝑞 ∈ ℝ)) → ((2 ≤ 𝑝 ∧ 2 ≤ 𝑞) → (2 + 2) ≤ (𝑝 + 𝑞)))
24	19, 22, 23	sylc 65	. . . . . . . . . 10 ⊢ (((2 ∈ ℤ ∧ 𝑝 ∈ ℤ ∧ 2 ≤ 𝑝) ∧ (2 ∈ ℤ ∧ 𝑞 ∈ ℤ ∧ 2 ≤ 𝑞)) → (2 + 2) ≤ (𝑝 + 𝑞))
25		2p2e4 12302	. . . . . . . . . . . . . . . . 17 ⊢ (2 + 2) = 4
26	25	breq1i 5079	. . . . . . . . . . . . . . . 16 ⊢ ((2 + 2) ≤ (𝑝 + 𝑞) ↔ 4 ≤ (𝑝 + 𝑞))
27		zaddcl 12558	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ) → (𝑝 + 𝑞) ∈ ℤ)
28	27	zred 12624	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ) → (𝑝 + 𝑞) ∈ ℝ)
29	28	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ) ∧ 4 ≤ (𝑝 + 𝑞)) → (𝑝 + 𝑞) ∈ ℝ)
30		zre 12519	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑟 ∈ ℤ → 𝑟 ∈ ℝ)
31	30	3ad2ant2 1140	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟) → 𝑟 ∈ ℝ)
32	29, 31	anim12i 619	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ) ∧ 4 ≤ (𝑝 + 𝑞)) ∧ (2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟)) → ((𝑝 + 𝑞) ∈ ℝ ∧ 𝑟 ∈ ℝ))
33		4re 12256	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 4 ∈ ℝ
34	33, 17	pm3.2i 471	. . . . . . . . . . . . . . . . . . . 20 ⊢ (4 ∈ ℝ ∧ 2 ∈ ℝ)
35	32, 34	jctil 524	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ) ∧ 4 ≤ (𝑝 + 𝑞)) ∧ (2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟)) → ((4 ∈ ℝ ∧ 2 ∈ ℝ) ∧ ((𝑝 + 𝑞) ∈ ℝ ∧ 𝑟 ∈ ℝ)))
36		simpr 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ) ∧ 4 ≤ (𝑝 + 𝑞)) → 4 ≤ (𝑝 + 𝑞))
37		simp3 1144	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟) → 2 ≤ 𝑟)
38	36, 37	anim12i 619	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ) ∧ 4 ≤ (𝑝 + 𝑞)) ∧ (2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟)) → (4 ≤ (𝑝 + 𝑞) ∧ 2 ≤ 𝑟))
39		le2add 11623	. . . . . . . . . . . . . . . . . . 19 ⊢ (((4 ∈ ℝ ∧ 2 ∈ ℝ) ∧ ((𝑝 + 𝑞) ∈ ℝ ∧ 𝑟 ∈ ℝ)) → ((4 ≤ (𝑝 + 𝑞) ∧ 2 ≤ 𝑟) → (4 + 2) ≤ ((𝑝 + 𝑞) + 𝑟)))
40	35, 38, 39	sylc 65	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ) ∧ 4 ≤ (𝑝 + 𝑞)) ∧ (2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟)) → (4 + 2) ≤ ((𝑝 + 𝑞) + 𝑟))
41		4p2e6 12320	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (4 + 2) = 6
42	41	breq1i 5079	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((4 + 2) ≤ ((𝑝 + 𝑞) + 𝑟) ↔ 6 ≤ ((𝑝 + 𝑞) + 𝑟))
43		5lt6 12348	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 5 < 6
44		5re 12259	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 5 ∈ ℝ
45	44	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ) ∧ 𝑟 ∈ ℤ) → 5 ∈ ℝ)
46		6re 12262	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 6 ∈ ℝ
47	46	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ) ∧ 𝑟 ∈ ℤ) → 6 ∈ ℝ)
48	27	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ) ∧ 𝑟 ∈ ℤ) → (𝑝 + 𝑞) ∈ ℤ)
49		simpr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ) ∧ 𝑟 ∈ ℤ) → 𝑟 ∈ ℤ)
50	48, 49	zaddcld 12628	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ) ∧ 𝑟 ∈ ℤ) → ((𝑝 + 𝑞) + 𝑟) ∈ ℤ)
51	50	zred 12624	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ) ∧ 𝑟 ∈ ℤ) → ((𝑝 + 𝑞) + 𝑟) ∈ ℝ)
52		ltletr 11229	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((5 ∈ ℝ ∧ 6 ∈ ℝ ∧ ((𝑝 + 𝑞) + 𝑟) ∈ ℝ) → ((5 < 6 ∧ 6 ≤ ((𝑝 + 𝑞) + 𝑟)) → 5 < ((𝑝 + 𝑞) + 𝑟)))
53	45, 47, 51, 52	syl3anc 1379	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ) ∧ 𝑟 ∈ ℤ) → ((5 < 6 ∧ 6 ≤ ((𝑝 + 𝑞) + 𝑟)) → 5 < ((𝑝 + 𝑞) + 𝑟)))
54	43, 53	mpani 702	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ) ∧ 𝑟 ∈ ℤ) → (6 ≤ ((𝑝 + 𝑞) + 𝑟) → 5 < ((𝑝 + 𝑞) + 𝑟)))
55	42, 54	biimtrid 243	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ) ∧ 𝑟 ∈ ℤ) → ((4 + 2) ≤ ((𝑝 + 𝑞) + 𝑟) → 5 < ((𝑝 + 𝑞) + 𝑟)))
56	55	expcom 414	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑟 ∈ ℤ → ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ) → ((4 + 2) ≤ ((𝑝 + 𝑞) + 𝑟) → 5 < ((𝑝 + 𝑞) + 𝑟))))
57	56	3ad2ant2 1140	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟) → ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ) → ((4 + 2) ≤ ((𝑝 + 𝑞) + 𝑟) → 5 < ((𝑝 + 𝑞) + 𝑟))))
58	57	com12 32	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ) → ((2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟) → ((4 + 2) ≤ ((𝑝 + 𝑞) + 𝑟) → 5 < ((𝑝 + 𝑞) + 𝑟))))
59	58	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ) ∧ 4 ≤ (𝑝 + 𝑞)) → ((2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟) → ((4 + 2) ≤ ((𝑝 + 𝑞) + 𝑟) → 5 < ((𝑝 + 𝑞) + 𝑟))))
60	59	imp 407	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ) ∧ 4 ≤ (𝑝 + 𝑞)) ∧ (2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟)) → ((4 + 2) ≤ ((𝑝 + 𝑞) + 𝑟) → 5 < ((𝑝 + 𝑞) + 𝑟)))
61	40, 60	mpd 15	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ) ∧ 4 ≤ (𝑝 + 𝑞)) ∧ (2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟)) → 5 < ((𝑝 + 𝑞) + 𝑟))
62	61	exp31 420	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ) → (4 ≤ (𝑝 + 𝑞) → ((2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟) → 5 < ((𝑝 + 𝑞) + 𝑟))))
63	26, 62	biimtrid 243	. . . . . . . . . . . . . . 15 ⊢ ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ) → ((2 + 2) ≤ (𝑝 + 𝑞) → ((2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟) → 5 < ((𝑝 + 𝑞) + 𝑟))))
64	63	expcom 414	. . . . . . . . . . . . . 14 ⊢ (𝑞 ∈ ℤ → (𝑝 ∈ ℤ → ((2 + 2) ≤ (𝑝 + 𝑞) → ((2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟) → 5 < ((𝑝 + 𝑞) + 𝑟)))))
65	64	3ad2ant2 1140	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℤ ∧ 𝑞 ∈ ℤ ∧ 2 ≤ 𝑞) → (𝑝 ∈ ℤ → ((2 + 2) ≤ (𝑝 + 𝑞) → ((2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟) → 5 < ((𝑝 + 𝑞) + 𝑟)))))
66	65	com12 32	. . . . . . . . . . . 12 ⊢ (𝑝 ∈ ℤ → ((2 ∈ ℤ ∧ 𝑞 ∈ ℤ ∧ 2 ≤ 𝑞) → ((2 + 2) ≤ (𝑝 + 𝑞) → ((2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟) → 5 < ((𝑝 + 𝑞) + 𝑟)))))
67	66	3ad2ant2 1140	. . . . . . . . . . 11 ⊢ ((2 ∈ ℤ ∧ 𝑝 ∈ ℤ ∧ 2 ≤ 𝑝) → ((2 ∈ ℤ ∧ 𝑞 ∈ ℤ ∧ 2 ≤ 𝑞) → ((2 + 2) ≤ (𝑝 + 𝑞) → ((2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟) → 5 < ((𝑝 + 𝑞) + 𝑟)))))
68	67	imp 407	. . . . . . . . . 10 ⊢ (((2 ∈ ℤ ∧ 𝑝 ∈ ℤ ∧ 2 ≤ 𝑝) ∧ (2 ∈ ℤ ∧ 𝑞 ∈ ℤ ∧ 2 ≤ 𝑞)) → ((2 + 2) ≤ (𝑝 + 𝑞) → ((2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟) → 5 < ((𝑝 + 𝑞) + 𝑟))))
69	24, 68	mpd 15	. . . . . . . . 9 ⊢ (((2 ∈ ℤ ∧ 𝑝 ∈ ℤ ∧ 2 ≤ 𝑝) ∧ (2 ∈ ℤ ∧ 𝑞 ∈ ℤ ∧ 2 ≤ 𝑞)) → ((2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟) → 5 < ((𝑝 + 𝑞) + 𝑟)))
70	69	imp 407	. . . . . . . 8 ⊢ ((((2 ∈ ℤ ∧ 𝑝 ∈ ℤ ∧ 2 ≤ 𝑝) ∧ (2 ∈ ℤ ∧ 𝑞 ∈ ℤ ∧ 2 ≤ 𝑞)) ∧ (2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟)) → 5 < ((𝑝 + 𝑞) + 𝑟))
71		breq2 5076	. . . . . . . 8 ⊢ (𝑍 = ((𝑝 + 𝑞) + 𝑟) → (5 < 𝑍 ↔ 5 < ((𝑝 + 𝑞) + 𝑟)))
72	70, 71	syl5ibrcom 248	. . . . . . 7 ⊢ ((((2 ∈ ℤ ∧ 𝑝 ∈ ℤ ∧ 2 ≤ 𝑝) ∧ (2 ∈ ℤ ∧ 𝑞 ∈ ℤ ∧ 2 ≤ 𝑞)) ∧ (2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟)) → (𝑍 = ((𝑝 + 𝑞) + 𝑟) → 5 < 𝑍))
73	8, 11, 72	syl2an 602	. . . . . 6 ⊢ (((𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ) ∧ 𝑟 ∈ ℙ) → (𝑍 = ((𝑝 + 𝑞) + 𝑟) → 5 < 𝑍))
74	73	rexlimdva 3140	. . . . 5 ⊢ ((𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ) → (∃𝑟 ∈ ℙ 𝑍 = ((𝑝 + 𝑞) + 𝑟) → 5 < 𝑍))
75	74	adantl 482	. . . 4 ⊢ ((𝑍 ∈ Odd ∧ (𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ)) → (∃𝑟 ∈ ℙ 𝑍 = ((𝑝 + 𝑞) + 𝑟) → 5 < 𝑍))
76	75	rexlimdvva 3196	. . 3 ⊢ (𝑍 ∈ Odd → (∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑍 = ((𝑝 + 𝑞) + 𝑟) → 5 < 𝑍))
77	76	imp 407	. 2 ⊢ ((𝑍 ∈ Odd ∧ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑍 = ((𝑝 + 𝑞) + 𝑟)) → 5 < 𝑍)
78	1, 77	sylbi 218	1 ⊢ (𝑍 ∈ GoldbachOddW → 5 < 𝑍)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1092 = wceq 1547 ∈ wcel 2119 ∃wrex 3063 class class class wbr 5072 ‘cfv 6485 (class class class)co 7356 ℝcr 11028 + caddc 11032 < clt 11170 ≤ cle 11171 2c2 12227 4c4 12229 5c5 12230 6c6 12231 ℤcz 12515 ℤ_≥cuz 12779 ℙcprime 16631 Odd codd 48116 GoldbachOddW cgbow 48237

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-11 2168 ax-12 2189 ax-ext 2711 ax-sep 5218 ax-nul 5228 ax-pow 5294 ax-pr 5362 ax-un 7678 ax-cnex 11085 ax-resscn 11086 ax-1cn 11087 ax-icn 11088 ax-addcl 11089 ax-addrcl 11090 ax-mulcl 11091 ax-mulrcl 11092 ax-mulcom 11093 ax-addass 11094 ax-mulass 11095 ax-distr 11096 ax-i2m1 11097 ax-1ne0 11098 ax-1rid 11099 ax-rnegex 11100 ax-rrecex 11101 ax-cnre 11102 ax-pre-lttri 11103 ax-pre-lttrn 11104 ax-pre-ltadd 11105 ax-pre-mulgt0 11106 ax-pre-sup 11107

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3or 1093 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2718 df-cleq 2731 df-clel 2814 df-nfc 2888 df-ne 2935 df-nel 3039 df-ral 3054 df-rex 3064 df-rmo 3344 df-reu 3345 df-rab 3392 df-v 3433 df-sbc 3724 df-csb 3832 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3903 df-nul 4262 df-if 4455 df-pw 4531 df-sn 4556 df-pr 4558 df-op 4562 df-uni 4839 df-iun 4923 df-br 5073 df-opab 5135 df-mpt 5154 df-tr 5180 df-id 5513 df-eprel 5518 df-po 5526 df-so 5527 df-fr 5571 df-we 5573 df-xp 5624 df-rel 5625 df-cnv 5626 df-co 5627 df-dm 5628 df-rn 5629 df-res 5630 df-ima 5631 df-pred 6252 df-ord 6313 df-on 6314 df-lim 6315 df-suc 6316 df-iota 6441 df-fun 6487 df-fn 6488 df-f 6489 df-f1 6490 df-fo 6491 df-f1o 6492 df-fv 6493 df-riota 7313 df-ov 7359 df-oprab 7360 df-mpo 7361 df-om 7807 df-2nd 7932 df-frecs 8221 df-wrecs 8252 df-recs 8301 df-rdg 8339 df-1o 8395 df-2o 8396 df-er 8633 df-en 8884 df-dom 8885 df-sdom 8886 df-fin 8887 df-sup 9345 df-pnf 11172 df-mnf 11173 df-xr 11174 df-ltxr 11175 df-le 11176 df-sub 11370 df-neg 11371 df-div 11799 df-nn 12166 df-2 12235 df-3 12236 df-4 12237 df-5 12238 df-6 12239 df-n0 12429 df-z 12516 df-uz 12780 df-rp 12934 df-seq 13955 df-exp 14015 df-cj 15052 df-re 15053 df-im 15054 df-sqrt 15188 df-abs 15189 df-dvds 16213 df-prm 16632 df-gbow 48240

This theorem is referenced by: gbowge7 48254

W3C validator