Theorem gbowgt5 44637

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 44627	. 2 ⊢ (𝑍 ∈ GoldbachOddW ↔ (𝑍 ∈ Odd ∧ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑍 = ((𝑝 + 𝑞) + 𝑟)))
2		prmuz2 16082	. . . . . . . . 9 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ (ℤ≥‘2))
3		eluz2 12278	. . . . . . . . 9 ⊢ (𝑝 ∈ (ℤ≥‘2) ↔ (2 ∈ ℤ ∧ 𝑝 ∈ ℤ ∧ 2 ≤ 𝑝))
4	2, 3	sylib 221	. . . . . . . 8 ⊢ (𝑝 ∈ ℙ → (2 ∈ ℤ ∧ 𝑝 ∈ ℤ ∧ 2 ≤ 𝑝))
5		prmuz2 16082	. . . . . . . . 9 ⊢ (𝑞 ∈ ℙ → 𝑞 ∈ (ℤ≥‘2))
6		eluz2 12278	. . . . . . . . 9 ⊢ (𝑞 ∈ (ℤ≥‘2) ↔ (2 ∈ ℤ ∧ 𝑞 ∈ ℤ ∧ 2 ≤ 𝑞))
7	5, 6	sylib 221	. . . . . . . 8 ⊢ (𝑞 ∈ ℙ → (2 ∈ ℤ ∧ 𝑞 ∈ ℤ ∧ 2 ≤ 𝑞))
8	4, 7	anim12i 616	. . . . . . 7 ⊢ ((𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ) → ((2 ∈ ℤ ∧ 𝑝 ∈ ℤ ∧ 2 ≤ 𝑝) ∧ (2 ∈ ℤ ∧ 𝑞 ∈ ℤ ∧ 2 ≤ 𝑞)))
9		prmuz2 16082	. . . . . . . 8 ⊢ (𝑟 ∈ ℙ → 𝑟 ∈ (ℤ≥‘2))
10		eluz2 12278	. . . . . . . 8 ⊢ (𝑟 ∈ (ℤ≥‘2) ↔ (2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟))
11	9, 10	sylib 221	. . . . . . 7 ⊢ (𝑟 ∈ ℙ → (2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟))
12		zre 12014	. . . . . . . . . . . . . 14 ⊢ (𝑝 ∈ ℤ → 𝑝 ∈ ℝ)
13	12	3ad2ant2 1132	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℤ ∧ 𝑝 ∈ ℤ ∧ 2 ≤ 𝑝) → 𝑝 ∈ ℝ)
14		zre 12014	. . . . . . . . . . . . . 14 ⊢ (𝑞 ∈ ℤ → 𝑞 ∈ ℝ)
15	14	3ad2ant2 1132	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℤ ∧ 𝑞 ∈ ℤ ∧ 2 ≤ 𝑞) → 𝑞 ∈ ℝ)
16	13, 15	anim12i 616	. . . . . . . . . . . 12 ⊢ (((2 ∈ ℤ ∧ 𝑝 ∈ ℤ ∧ 2 ≤ 𝑝) ∧ (2 ∈ ℤ ∧ 𝑞 ∈ ℤ ∧ 2 ≤ 𝑞)) → (𝑝 ∈ ℝ ∧ 𝑞 ∈ ℝ))
17		2re 11738	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℝ
18	17, 17	pm3.2i 475	. . . . . . . . . . . 12 ⊢ (2 ∈ ℝ ∧ 2 ∈ ℝ)
19	16, 18	jctil 524	. . . . . . . . . . 11 ⊢ (((2 ∈ ℤ ∧ 𝑝 ∈ ℤ ∧ 2 ≤ 𝑝) ∧ (2 ∈ ℤ ∧ 𝑞 ∈ ℤ ∧ 2 ≤ 𝑞)) → ((2 ∈ ℝ ∧ 2 ∈ ℝ) ∧ (𝑝 ∈ ℝ ∧ 𝑞 ∈ ℝ)))
20		simp3 1136	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℤ ∧ 𝑝 ∈ ℤ ∧ 2 ≤ 𝑝) → 2 ≤ 𝑝)
21		simp3 1136	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℤ ∧ 𝑞 ∈ ℤ ∧ 2 ≤ 𝑞) → 2 ≤ 𝑞)
22	20, 21	anim12i 616	. . . . . . . . . . 11 ⊢ (((2 ∈ ℤ ∧ 𝑝 ∈ ℤ ∧ 2 ≤ 𝑝) ∧ (2 ∈ ℤ ∧ 𝑞 ∈ ℤ ∧ 2 ≤ 𝑞)) → (2 ≤ 𝑝 ∧ 2 ≤ 𝑞))
23		le2add 11150	. . . . . . . . . . 11 ⊢ (((2 ∈ ℝ ∧ 2 ∈ ℝ) ∧ (𝑝 ∈ ℝ ∧ 𝑞 ∈ ℝ)) → ((2 ≤ 𝑝 ∧ 2 ≤ 𝑞) → (2 + 2) ≤ (𝑝 + 𝑞)))
24	19, 22, 23	sylc 65	. . . . . . . . . 10 ⊢ (((2 ∈ ℤ ∧ 𝑝 ∈ ℤ ∧ 2 ≤ 𝑝) ∧ (2 ∈ ℤ ∧ 𝑞 ∈ ℤ ∧ 2 ≤ 𝑞)) → (2 + 2) ≤ (𝑝 + 𝑞))
25		2p2e4 11799	. . . . . . . . . . . . . . . . 17 ⊢ (2 + 2) = 4
26	25	breq1i 5037	. . . . . . . . . . . . . . . 16 ⊢ ((2 + 2) ≤ (𝑝 + 𝑞) ↔ 4 ≤ (𝑝 + 𝑞))
27		zaddcl 12051	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ) → (𝑝 + 𝑞) ∈ ℤ)
28	27	zred 12116	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ) → (𝑝 + 𝑞) ∈ ℝ)
29	28	adantr 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ) ∧ 4 ≤ (𝑝 + 𝑞)) → (𝑝 + 𝑞) ∈ ℝ)
30		zre 12014	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑟 ∈ ℤ → 𝑟 ∈ ℝ)
31	30	3ad2ant2 1132	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟) → 𝑟 ∈ ℝ)
32	29, 31	anim12i 616	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ) ∧ 4 ≤ (𝑝 + 𝑞)) ∧ (2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟)) → ((𝑝 + 𝑞) ∈ ℝ ∧ 𝑟 ∈ ℝ))
33		4re 11748	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 4 ∈ ℝ
34	33, 17	pm3.2i 475	. . . . . . . . . . . . . . . . . . . 20 ⊢ (4 ∈ ℝ ∧ 2 ∈ ℝ)
35	32, 34	jctil 524	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ) ∧ 4 ≤ (𝑝 + 𝑞)) ∧ (2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟)) → ((4 ∈ ℝ ∧ 2 ∈ ℝ) ∧ ((𝑝 + 𝑞) ∈ ℝ ∧ 𝑟 ∈ ℝ)))
36		simpr 489	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ) ∧ 4 ≤ (𝑝 + 𝑞)) → 4 ≤ (𝑝 + 𝑞))
37		simp3 1136	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟) → 2 ≤ 𝑟)
38	36, 37	anim12i 616	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ) ∧ 4 ≤ (𝑝 + 𝑞)) ∧ (2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟)) → (4 ≤ (𝑝 + 𝑞) ∧ 2 ≤ 𝑟))
39		le2add 11150	. . . . . . . . . . . . . . . . . . 19 ⊢ (((4 ∈ ℝ ∧ 2 ∈ ℝ) ∧ ((𝑝 + 𝑞) ∈ ℝ ∧ 𝑟 ∈ ℝ)) → ((4 ≤ (𝑝 + 𝑞) ∧ 2 ≤ 𝑟) → (4 + 2) ≤ ((𝑝 + 𝑞) + 𝑟)))
40	35, 38, 39	sylc 65	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ) ∧ 4 ≤ (𝑝 + 𝑞)) ∧ (2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟)) → (4 + 2) ≤ ((𝑝 + 𝑞) + 𝑟))
41		4p2e6 11817	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (4 + 2) = 6
42	41	breq1i 5037	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((4 + 2) ≤ ((𝑝 + 𝑞) + 𝑟) ↔ 6 ≤ ((𝑝 + 𝑞) + 𝑟))
43		5lt6 11845	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 5 < 6
44		5re 11751	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 5 ∈ ℝ
45	44	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ) ∧ 𝑟 ∈ ℤ) → 5 ∈ ℝ)
46		6re 11754	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 6 ∈ ℝ
47	46	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ) ∧ 𝑟 ∈ ℤ) → 6 ∈ ℝ)
48	27	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ) ∧ 𝑟 ∈ ℤ) → (𝑝 + 𝑞) ∈ ℤ)
49		simpr 489	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ) ∧ 𝑟 ∈ ℤ) → 𝑟 ∈ ℤ)
50	48, 49	zaddcld 12120	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ) ∧ 𝑟 ∈ ℤ) → ((𝑝 + 𝑞) + 𝑟) ∈ ℤ)
51	50	zred 12116	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ) ∧ 𝑟 ∈ ℤ) → ((𝑝 + 𝑞) + 𝑟) ∈ ℝ)
52		ltletr 10760	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((5 ∈ ℝ ∧ 6 ∈ ℝ ∧ ((𝑝 + 𝑞) + 𝑟) ∈ ℝ) → ((5 < 6 ∧ 6 ≤ ((𝑝 + 𝑞) + 𝑟)) → 5 < ((𝑝 + 𝑞) + 𝑟)))
53	45, 47, 51, 52	syl3anc 1369	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ) ∧ 𝑟 ∈ ℤ) → ((5 < 6 ∧ 6 ≤ ((𝑝 + 𝑞) + 𝑟)) → 5 < ((𝑝 + 𝑞) + 𝑟)))
54	43, 53	mpani 696	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ) ∧ 𝑟 ∈ ℤ) → (6 ≤ ((𝑝 + 𝑞) + 𝑟) → 5 < ((𝑝 + 𝑞) + 𝑟)))
55	42, 54	syl5bi 245	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ) ∧ 𝑟 ∈ ℤ) → ((4 + 2) ≤ ((𝑝 + 𝑞) + 𝑟) → 5 < ((𝑝 + 𝑞) + 𝑟)))
56	55	expcom 418	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑟 ∈ ℤ → ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ) → ((4 + 2) ≤ ((𝑝 + 𝑞) + 𝑟) → 5 < ((𝑝 + 𝑞) + 𝑟))))
57	56	3ad2ant2 1132	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟) → ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ) → ((4 + 2) ≤ ((𝑝 + 𝑞) + 𝑟) → 5 < ((𝑝 + 𝑞) + 𝑟))))
58	57	com12 32	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ) → ((2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟) → ((4 + 2) ≤ ((𝑝 + 𝑞) + 𝑟) → 5 < ((𝑝 + 𝑞) + 𝑟))))
59	58	adantr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ) ∧ 4 ≤ (𝑝 + 𝑞)) → ((2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟) → ((4 + 2) ≤ ((𝑝 + 𝑞) + 𝑟) → 5 < ((𝑝 + 𝑞) + 𝑟))))
60	59	imp 411	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ) ∧ 4 ≤ (𝑝 + 𝑞)) ∧ (2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟)) → ((4 + 2) ≤ ((𝑝 + 𝑞) + 𝑟) → 5 < ((𝑝 + 𝑞) + 𝑟)))
61	40, 60	mpd 15	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ) ∧ 4 ≤ (𝑝 + 𝑞)) ∧ (2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟)) → 5 < ((𝑝 + 𝑞) + 𝑟))
62	61	exp31 424	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ) → (4 ≤ (𝑝 + 𝑞) → ((2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟) → 5 < ((𝑝 + 𝑞) + 𝑟))))
63	26, 62	syl5bi 245	. . . . . . . . . . . . . . 15 ⊢ ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ) → ((2 + 2) ≤ (𝑝 + 𝑞) → ((2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟) → 5 < ((𝑝 + 𝑞) + 𝑟))))
64	63	expcom 418	. . . . . . . . . . . . . 14 ⊢ (𝑞 ∈ ℤ → (𝑝 ∈ ℤ → ((2 + 2) ≤ (𝑝 + 𝑞) → ((2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟) → 5 < ((𝑝 + 𝑞) + 𝑟)))))
65	64	3ad2ant2 1132	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℤ ∧ 𝑞 ∈ ℤ ∧ 2 ≤ 𝑞) → (𝑝 ∈ ℤ → ((2 + 2) ≤ (𝑝 + 𝑞) → ((2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟) → 5 < ((𝑝 + 𝑞) + 𝑟)))))
66	65	com12 32	. . . . . . . . . . . 12 ⊢ (𝑝 ∈ ℤ → ((2 ∈ ℤ ∧ 𝑞 ∈ ℤ ∧ 2 ≤ 𝑞) → ((2 + 2) ≤ (𝑝 + 𝑞) → ((2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟) → 5 < ((𝑝 + 𝑞) + 𝑟)))))
67	66	3ad2ant2 1132	. . . . . . . . . . 11 ⊢ ((2 ∈ ℤ ∧ 𝑝 ∈ ℤ ∧ 2 ≤ 𝑝) → ((2 ∈ ℤ ∧ 𝑞 ∈ ℤ ∧ 2 ≤ 𝑞) → ((2 + 2) ≤ (𝑝 + 𝑞) → ((2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟) → 5 < ((𝑝 + 𝑞) + 𝑟)))))
68	67	imp 411	. . . . . . . . . 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 411	. . . . . . . 8 ⊢ ((((2 ∈ ℤ ∧ 𝑝 ∈ ℤ ∧ 2 ≤ 𝑝) ∧ (2 ∈ ℤ ∧ 𝑞 ∈ ℤ ∧ 2 ≤ 𝑞)) ∧ (2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟)) → 5 < ((𝑝 + 𝑞) + 𝑟))
71		breq2 5034	. . . . . . . 8 ⊢ (𝑍 = ((𝑝 + 𝑞) + 𝑟) → (5 < 𝑍 ↔ 5 < ((𝑝 + 𝑞) + 𝑟)))
72	70, 71	syl5ibrcom 250	. . . . . . 7 ⊢ ((((2 ∈ ℤ ∧ 𝑝 ∈ ℤ ∧ 2 ≤ 𝑝) ∧ (2 ∈ ℤ ∧ 𝑞 ∈ ℤ ∧ 2 ≤ 𝑞)) ∧ (2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟)) → (𝑍 = ((𝑝 + 𝑞) + 𝑟) → 5 < 𝑍))
73	8, 11, 72	syl2an 599	. . . . . 6 ⊢ (((𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ) ∧ 𝑟 ∈ ℙ) → (𝑍 = ((𝑝 + 𝑞) + 𝑟) → 5 < 𝑍))
74	73	rexlimdva 3209	. . . . 5 ⊢ ((𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ) → (∃𝑟 ∈ ℙ 𝑍 = ((𝑝 + 𝑞) + 𝑟) → 5 < 𝑍))
75	74	adantl 486	. . . 4 ⊢ ((𝑍 ∈ Odd ∧ (𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ)) → (∃𝑟 ∈ ℙ 𝑍 = ((𝑝 + 𝑞) + 𝑟) → 5 < 𝑍))
76	75	rexlimdvva 3219	. . 3 ⊢ (𝑍 ∈ Odd → (∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑍 = ((𝑝 + 𝑞) + 𝑟) → 5 < 𝑍))
77	76	imp 411	. 2 ⊢ ((𝑍 ∈ Odd ∧ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑍 = ((𝑝 + 𝑞) + 𝑟)) → 5 < 𝑍)
78	1, 77	sylbi 220	1 ⊢ (𝑍 ∈ GoldbachOddW → 5 < 𝑍)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1085   = wceq 1539   ∈ wcel 2112  ∃wrex 3072   class class class wbr 5030  ‘cfv 6333  (class class class)co 7148  ℝcr 10564   + caddc 10568   < clt 10703   ≤ cle 10704  2c2 11719  4c4 11721  5c5 11722  6c6 11723  ℤcz 12010  ℤ_≥cuz 12272  ℙcprime 16057   Odd codd 44500   GoldbachOddW cgbow 44621

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-sep 5167  ax-nul 5174  ax-pow 5232  ax-pr 5296  ax-un 7457  ax-cnex 10621  ax-resscn 10622  ax-1cn 10623  ax-icn 10624  ax-addcl 10625  ax-addrcl 10626  ax-mulcl 10627  ax-mulrcl 10628  ax-mulcom 10629  ax-addass 10630  ax-mulass 10631  ax-distr 10632  ax-i2m1 10633  ax-1ne0 10634  ax-1rid 10635  ax-rnegex 10636  ax-rrecex 10637  ax-cnre 10638  ax-pre-lttri 10639  ax-pre-lttrn 10640  ax-pre-ltadd 10641  ax-pre-mulgt0 10642  ax-pre-sup 10643

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-nel 3057  df-ral 3076  df-rex 3077  df-reu 3078  df-rmo 3079  df-rab 3080  df-v 3412  df-sbc 3698  df-csb 3807  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-pss 3878  df-nul 4227  df-if 4419  df-pw 4494  df-sn 4521  df-pr 4523  df-tp 4525  df-op 4527  df-uni 4797  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5428  df-eprel 5433  df-po 5441  df-so 5442  df-fr 5481  df-we 5483  df-xp 5528  df-rel 5529  df-cnv 5530  df-co 5531  df-dm 5532  df-rn 5533  df-res 5534  df-ima 5535  df-pred 6124  df-ord 6170  df-on 6171  df-lim 6172  df-suc 6173  df-iota 6292  df-fun 6335  df-fn 6336  df-f 6337  df-f1 6338  df-fo 6339  df-f1o 6340  df-fv 6341  df-riota 7106  df-ov 7151  df-oprab 7152  df-mpo 7153  df-om 7578  df-2nd 7692  df-wrecs 7955  df-recs 8016  df-rdg 8054  df-1o 8110  df-2o 8111  df-er 8297  df-en 8526  df-dom 8527  df-sdom 8528  df-fin 8529  df-sup 8929  df-pnf 10705  df-mnf 10706  df-xr 10707  df-ltxr 10708  df-le 10709  df-sub 10900  df-neg 10901  df-div 11326  df-nn 11665  df-2 11727  df-3 11728  df-4 11729  df-5 11730  df-6 11731  df-n0 11925  df-z 12011  df-uz 12273  df-rp 12421  df-seq 13409  df-exp 13470  df-cj 14496  df-re 14497  df-im 14498  df-sqrt 14632  df-abs 14633  df-dvds 15646  df-prm 16058  df-gbow 44624

This theorem is referenced by:  gbowge7  44638