Step |
Hyp |
Ref |
Expression |
1 |
|
isgbo |
⊢ ( 𝑍 ∈ GoldbachOdd ↔ ( 𝑍 ∈ Odd ∧ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑍 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ) ) |
2 |
|
df-3an |
⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ∧ 𝑟 ∈ ℙ ) ↔ ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) ∧ 𝑟 ∈ ℙ ) ) |
3 |
|
an6 |
⊢ ( ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ∧ 𝑟 ∈ ℙ ) ∧ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ) ↔ ( ( 𝑝 ∈ ℙ ∧ 𝑝 ∈ Odd ) ∧ ( 𝑞 ∈ ℙ ∧ 𝑞 ∈ Odd ) ∧ ( 𝑟 ∈ ℙ ∧ 𝑟 ∈ Odd ) ) ) |
4 |
|
oddprmuzge3 |
⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑝 ∈ Odd ) → 𝑝 ∈ ( ℤ≥ ‘ 3 ) ) |
5 |
|
oddprmuzge3 |
⊢ ( ( 𝑞 ∈ ℙ ∧ 𝑞 ∈ Odd ) → 𝑞 ∈ ( ℤ≥ ‘ 3 ) ) |
6 |
|
oddprmuzge3 |
⊢ ( ( 𝑟 ∈ ℙ ∧ 𝑟 ∈ Odd ) → 𝑟 ∈ ( ℤ≥ ‘ 3 ) ) |
7 |
|
6p3e9 |
⊢ ( 6 + 3 ) = 9 |
8 |
|
eluzelz |
⊢ ( 𝑝 ∈ ( ℤ≥ ‘ 3 ) → 𝑝 ∈ ℤ ) |
9 |
|
eluzelz |
⊢ ( 𝑞 ∈ ( ℤ≥ ‘ 3 ) → 𝑞 ∈ ℤ ) |
10 |
|
zaddcl |
⊢ ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ ) → ( 𝑝 + 𝑞 ) ∈ ℤ ) |
11 |
8 9 10
|
syl2an |
⊢ ( ( 𝑝 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑞 ∈ ( ℤ≥ ‘ 3 ) ) → ( 𝑝 + 𝑞 ) ∈ ℤ ) |
12 |
11
|
zred |
⊢ ( ( 𝑝 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑞 ∈ ( ℤ≥ ‘ 3 ) ) → ( 𝑝 + 𝑞 ) ∈ ℝ ) |
13 |
|
eluzelre |
⊢ ( 𝑟 ∈ ( ℤ≥ ‘ 3 ) → 𝑟 ∈ ℝ ) |
14 |
12 13
|
anim12i |
⊢ ( ( ( 𝑝 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑞 ∈ ( ℤ≥ ‘ 3 ) ) ∧ 𝑟 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( 𝑝 + 𝑞 ) ∈ ℝ ∧ 𝑟 ∈ ℝ ) ) |
15 |
14
|
3impa |
⊢ ( ( 𝑝 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑞 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑟 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( 𝑝 + 𝑞 ) ∈ ℝ ∧ 𝑟 ∈ ℝ ) ) |
16 |
|
6re |
⊢ 6 ∈ ℝ |
17 |
|
3re |
⊢ 3 ∈ ℝ |
18 |
16 17
|
pm3.2i |
⊢ ( 6 ∈ ℝ ∧ 3 ∈ ℝ ) |
19 |
15 18
|
jctil |
⊢ ( ( 𝑝 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑞 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑟 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( 6 ∈ ℝ ∧ 3 ∈ ℝ ) ∧ ( ( 𝑝 + 𝑞 ) ∈ ℝ ∧ 𝑟 ∈ ℝ ) ) ) |
20 |
|
3p3e6 |
⊢ ( 3 + 3 ) = 6 |
21 |
|
eluzelre |
⊢ ( 𝑝 ∈ ( ℤ≥ ‘ 3 ) → 𝑝 ∈ ℝ ) |
22 |
|
eluzelre |
⊢ ( 𝑞 ∈ ( ℤ≥ ‘ 3 ) → 𝑞 ∈ ℝ ) |
23 |
21 22
|
anim12i |
⊢ ( ( 𝑝 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑞 ∈ ( ℤ≥ ‘ 3 ) ) → ( 𝑝 ∈ ℝ ∧ 𝑞 ∈ ℝ ) ) |
24 |
17 17
|
pm3.2i |
⊢ ( 3 ∈ ℝ ∧ 3 ∈ ℝ ) |
25 |
23 24
|
jctil |
⊢ ( ( 𝑝 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑞 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( 3 ∈ ℝ ∧ 3 ∈ ℝ ) ∧ ( 𝑝 ∈ ℝ ∧ 𝑞 ∈ ℝ ) ) ) |
26 |
|
eluzle |
⊢ ( 𝑝 ∈ ( ℤ≥ ‘ 3 ) → 3 ≤ 𝑝 ) |
27 |
|
eluzle |
⊢ ( 𝑞 ∈ ( ℤ≥ ‘ 3 ) → 3 ≤ 𝑞 ) |
28 |
26 27
|
anim12i |
⊢ ( ( 𝑝 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑞 ∈ ( ℤ≥ ‘ 3 ) ) → ( 3 ≤ 𝑝 ∧ 3 ≤ 𝑞 ) ) |
29 |
|
le2add |
⊢ ( ( ( 3 ∈ ℝ ∧ 3 ∈ ℝ ) ∧ ( 𝑝 ∈ ℝ ∧ 𝑞 ∈ ℝ ) ) → ( ( 3 ≤ 𝑝 ∧ 3 ≤ 𝑞 ) → ( 3 + 3 ) ≤ ( 𝑝 + 𝑞 ) ) ) |
30 |
25 28 29
|
sylc |
⊢ ( ( 𝑝 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑞 ∈ ( ℤ≥ ‘ 3 ) ) → ( 3 + 3 ) ≤ ( 𝑝 + 𝑞 ) ) |
31 |
20 30
|
eqbrtrrid |
⊢ ( ( 𝑝 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑞 ∈ ( ℤ≥ ‘ 3 ) ) → 6 ≤ ( 𝑝 + 𝑞 ) ) |
32 |
31
|
3adant3 |
⊢ ( ( 𝑝 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑞 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑟 ∈ ( ℤ≥ ‘ 3 ) ) → 6 ≤ ( 𝑝 + 𝑞 ) ) |
33 |
|
eluzle |
⊢ ( 𝑟 ∈ ( ℤ≥ ‘ 3 ) → 3 ≤ 𝑟 ) |
34 |
33
|
3ad2ant3 |
⊢ ( ( 𝑝 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑞 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑟 ∈ ( ℤ≥ ‘ 3 ) ) → 3 ≤ 𝑟 ) |
35 |
32 34
|
jca |
⊢ ( ( 𝑝 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑞 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑟 ∈ ( ℤ≥ ‘ 3 ) ) → ( 6 ≤ ( 𝑝 + 𝑞 ) ∧ 3 ≤ 𝑟 ) ) |
36 |
|
le2add |
⊢ ( ( ( 6 ∈ ℝ ∧ 3 ∈ ℝ ) ∧ ( ( 𝑝 + 𝑞 ) ∈ ℝ ∧ 𝑟 ∈ ℝ ) ) → ( ( 6 ≤ ( 𝑝 + 𝑞 ) ∧ 3 ≤ 𝑟 ) → ( 6 + 3 ) ≤ ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ) |
37 |
19 35 36
|
sylc |
⊢ ( ( 𝑝 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑞 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑟 ∈ ( ℤ≥ ‘ 3 ) ) → ( 6 + 3 ) ≤ ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) |
38 |
7 37
|
eqbrtrrid |
⊢ ( ( 𝑝 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑞 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑟 ∈ ( ℤ≥ ‘ 3 ) ) → 9 ≤ ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) |
39 |
4 5 6 38
|
syl3an |
⊢ ( ( ( 𝑝 ∈ ℙ ∧ 𝑝 ∈ Odd ) ∧ ( 𝑞 ∈ ℙ ∧ 𝑞 ∈ Odd ) ∧ ( 𝑟 ∈ ℙ ∧ 𝑟 ∈ Odd ) ) → 9 ≤ ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) |
40 |
3 39
|
sylbi |
⊢ ( ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ∧ 𝑟 ∈ ℙ ) ∧ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ) → 9 ≤ ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) |
41 |
2 40
|
sylanbr |
⊢ ( ( ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) ∧ 𝑟 ∈ ℙ ) ∧ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ) → 9 ≤ ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) |
42 |
|
breq2 |
⊢ ( 𝑍 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) → ( 9 ≤ 𝑍 ↔ 9 ≤ ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ) |
43 |
41 42
|
syl5ibrcom |
⊢ ( ( ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) ∧ 𝑟 ∈ ℙ ) ∧ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ) → ( 𝑍 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) → 9 ≤ 𝑍 ) ) |
44 |
43
|
expimpd |
⊢ ( ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) ∧ 𝑟 ∈ ℙ ) → ( ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑍 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) → 9 ≤ 𝑍 ) ) |
45 |
44
|
rexlimdva |
⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) → ( ∃ 𝑟 ∈ ℙ ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑍 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) → 9 ≤ 𝑍 ) ) |
46 |
45
|
a1i |
⊢ ( 𝑍 ∈ Odd → ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) → ( ∃ 𝑟 ∈ ℙ ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑍 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) → 9 ≤ 𝑍 ) ) ) |
47 |
46
|
rexlimdvv |
⊢ ( 𝑍 ∈ Odd → ( ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑍 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) → 9 ≤ 𝑍 ) ) |
48 |
47
|
imp |
⊢ ( ( 𝑍 ∈ Odd ∧ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑍 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ) → 9 ≤ 𝑍 ) |
49 |
1 48
|
sylbi |
⊢ ( 𝑍 ∈ GoldbachOdd → 9 ≤ 𝑍 ) |