Metamath Proof Explorer

Theorem gbowgt5

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

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

Proof

Step Hyp Ref Expression
1 isgbow ⊢ ( 𝑍 ∈ GoldbachOddW ↔ ( 𝑍 ∈ Odd ∧ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑍 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
2 prmuz2 ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ( ℤ≥ ‘ 2 ) )
3 eluz2 ⊢ ( 𝑝 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 2 ∈ ℤ ∧ 𝑝 ∈ ℤ ∧ 2 ≤ 𝑝 ) )
4 2 3 sylib ⊢ ( 𝑝 ∈ ℙ → ( 2 ∈ ℤ ∧ 𝑝 ∈ ℤ ∧ 2 ≤ 𝑝 ) )
5 prmuz2 ⊢ ( 𝑞 ∈ ℙ → 𝑞 ∈ ( ℤ≥ ‘ 2 ) )
6 eluz2 ⊢ ( 𝑞 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 2 ∈ ℤ ∧ 𝑞 ∈ ℤ ∧ 2 ≤ 𝑞 ) )
7 5 6 sylib ⊢ ( 𝑞 ∈ ℙ → ( 2 ∈ ℤ ∧ 𝑞 ∈ ℤ ∧ 2 ≤ 𝑞 ) )
8 4 7 anim12i ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) → ( ( 2 ∈ ℤ ∧ 𝑝 ∈ ℤ ∧ 2 ≤ 𝑝 ) ∧ ( 2 ∈ ℤ ∧ 𝑞 ∈ ℤ ∧ 2 ≤ 𝑞 ) ) )
9 prmuz2 ⊢ ( 𝑟 ∈ ℙ → 𝑟 ∈ ( ℤ≥ ‘ 2 ) )
10 eluz2 ⊢ ( 𝑟 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟 ) )
11 9 10 sylib ⊢ ( 𝑟 ∈ ℙ → ( 2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟 ) )
12 zre ⊢ ( 𝑝 ∈ ℤ → 𝑝 ∈ ℝ )
13 12 3ad2ant2 ⊢ ( ( 2 ∈ ℤ ∧ 𝑝 ∈ ℤ ∧ 2 ≤ 𝑝 ) → 𝑝 ∈ ℝ )
14 zre ⊢ ( 𝑞 ∈ ℤ → 𝑞 ∈ ℝ )
15 14 3ad2ant2 ⊢ ( ( 2 ∈ ℤ ∧ 𝑞 ∈ ℤ ∧ 2 ≤ 𝑞 ) → 𝑞 ∈ ℝ )
16 13 15 anim12i ⊢ ( ( ( 2 ∈ ℤ ∧ 𝑝 ∈ ℤ ∧ 2 ≤ 𝑝 ) ∧ ( 2 ∈ ℤ ∧ 𝑞 ∈ ℤ ∧ 2 ≤ 𝑞 ) ) → ( 𝑝 ∈ ℝ ∧ 𝑞 ∈ ℝ ) )
17 2re ⊢ 2 ∈ ℝ
18 17 17 pm3.2i ⊢ ( 2 ∈ ℝ ∧ 2 ∈ ℝ )
19 16 18 jctil ⊢ ( ( ( 2 ∈ ℤ ∧ 𝑝 ∈ ℤ ∧ 2 ≤ 𝑝 ) ∧ ( 2 ∈ ℤ ∧ 𝑞 ∈ ℤ ∧ 2 ≤ 𝑞 ) ) → ( ( 2 ∈ ℝ ∧ 2 ∈ ℝ ) ∧ ( 𝑝 ∈ ℝ ∧ 𝑞 ∈ ℝ ) ) )
20 simp3 ⊢ ( ( 2 ∈ ℤ ∧ 𝑝 ∈ ℤ ∧ 2 ≤ 𝑝 ) → 2 ≤ 𝑝 )
21 simp3 ⊢ ( ( 2 ∈ ℤ ∧ 𝑞 ∈ ℤ ∧ 2 ≤ 𝑞 ) → 2 ≤ 𝑞 )
22 20 21 anim12i ⊢ ( ( ( 2 ∈ ℤ ∧ 𝑝 ∈ ℤ ∧ 2 ≤ 𝑝 ) ∧ ( 2 ∈ ℤ ∧ 𝑞 ∈ ℤ ∧ 2 ≤ 𝑞 ) ) → ( 2 ≤ 𝑝 ∧ 2 ≤ 𝑞 ) )
23 le2add ⊢ ( ( ( 2 ∈ ℝ ∧ 2 ∈ ℝ ) ∧ ( 𝑝 ∈ ℝ ∧ 𝑞 ∈ ℝ ) ) → ( ( 2 ≤ 𝑝 ∧ 2 ≤ 𝑞 ) → ( 2 + 2 ) ≤ ( 𝑝 + 𝑞 ) ) )
24 19 22 23 sylc ⊢ ( ( ( 2 ∈ ℤ ∧ 𝑝 ∈ ℤ ∧ 2 ≤ 𝑝 ) ∧ ( 2 ∈ ℤ ∧ 𝑞 ∈ ℤ ∧ 2 ≤ 𝑞 ) ) → ( 2 + 2 ) ≤ ( 𝑝 + 𝑞 ) )
25 2p2e4 ⊢ ( 2 + 2 ) = 4
26 25 breq1i ⊢ ( ( 2 + 2 ) ≤ ( 𝑝 + 𝑞 ) ↔ 4 ≤ ( 𝑝 + 𝑞 ) )
27 zaddcl ⊢ ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ ) → ( 𝑝 + 𝑞 ) ∈ ℤ )
28 27 zred ⊢ ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ ) → ( 𝑝 + 𝑞 ) ∈ ℝ )
29 28 adantr ⊢ ( ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ ) ∧ 4 ≤ ( 𝑝 + 𝑞 ) ) → ( 𝑝 + 𝑞 ) ∈ ℝ )
30 zre ⊢ ( 𝑟 ∈ ℤ → 𝑟 ∈ ℝ )
31 30 3ad2ant2 ⊢ ( ( 2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟 ) → 𝑟 ∈ ℝ )
32 29 31 anim12i ⊢ ( ( ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ ) ∧ 4 ≤ ( 𝑝 + 𝑞 ) ) ∧ ( 2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟 ) ) → ( ( 𝑝 + 𝑞 ) ∈ ℝ ∧ 𝑟 ∈ ℝ ) )
33 4re ⊢ 4 ∈ ℝ
34 33 17 pm3.2i ⊢ ( 4 ∈ ℝ ∧ 2 ∈ ℝ )
35 32 34 jctil ⊢ ( ( ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ ) ∧ 4 ≤ ( 𝑝 + 𝑞 ) ) ∧ ( 2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟 ) ) → ( ( 4 ∈ ℝ ∧ 2 ∈ ℝ ) ∧ ( ( 𝑝 + 𝑞 ) ∈ ℝ ∧ 𝑟 ∈ ℝ ) ) )
36 simpr ⊢ ( ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ ) ∧ 4 ≤ ( 𝑝 + 𝑞 ) ) → 4 ≤ ( 𝑝 + 𝑞 ) )
37 simp3 ⊢ ( ( 2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟 ) → 2 ≤ 𝑟 )
38 36 37 anim12i ⊢ ( ( ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ ) ∧ 4 ≤ ( 𝑝 + 𝑞 ) ) ∧ ( 2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟 ) ) → ( 4 ≤ ( 𝑝 + 𝑞 ) ∧ 2 ≤ 𝑟 ) )
39 le2add ⊢ ( ( ( 4 ∈ ℝ ∧ 2 ∈ ℝ ) ∧ ( ( 𝑝 + 𝑞 ) ∈ ℝ ∧ 𝑟 ∈ ℝ ) ) → ( ( 4 ≤ ( 𝑝 + 𝑞 ) ∧ 2 ≤ 𝑟 ) → ( 4 + 2 ) ≤ ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
40 35 38 39 sylc ⊢ ( ( ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ ) ∧ 4 ≤ ( 𝑝 + 𝑞 ) ) ∧ ( 2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟 ) ) → ( 4 + 2 ) ≤ ( ( 𝑝 + 𝑞 ) + 𝑟 ) )
41 4p2e6 ⊢ ( 4 + 2 ) = 6
42 41 breq1i ⊢ ( ( 4 + 2 ) ≤ ( ( 𝑝 + 𝑞 ) + 𝑟 ) ↔ 6 ≤ ( ( 𝑝 + 𝑞 ) + 𝑟 ) )
43 5lt6 ⊢ 5 < 6
44 5re ⊢ 5 ∈ ℝ
45 44 a1i ⊢ ( ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ ) ∧ 𝑟 ∈ ℤ ) → 5 ∈ ℝ )
46 6re ⊢ 6 ∈ ℝ
47 46 a1i ⊢ ( ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ ) ∧ 𝑟 ∈ ℤ ) → 6 ∈ ℝ )
48 27 adantr ⊢ ( ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ ) ∧ 𝑟 ∈ ℤ ) → ( 𝑝 + 𝑞 ) ∈ ℤ )
49 simpr ⊢ ( ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ ) ∧ 𝑟 ∈ ℤ ) → 𝑟 ∈ ℤ )
50 48 49 zaddcld ⊢ ( ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ ) ∧ 𝑟 ∈ ℤ ) → ( ( 𝑝 + 𝑞 ) + 𝑟 ) ∈ ℤ )
51 50 zred ⊢ ( ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ ) ∧ 𝑟 ∈ ℤ ) → ( ( 𝑝 + 𝑞 ) + 𝑟 ) ∈ ℝ )
52 ltletr ⊢ ( ( 5 ∈ ℝ ∧ 6 ∈ ℝ ∧ ( ( 𝑝 + 𝑞 ) + 𝑟 ) ∈ ℝ ) → ( ( 5 < 6 ∧ 6 ≤ ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) → 5 < ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
53 45 47 51 52 syl3anc ⊢ ( ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ ) ∧ 𝑟 ∈ ℤ ) → ( ( 5 < 6 ∧ 6 ≤ ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) → 5 < ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
54 43 53 mpani ⊢ ( ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ ) ∧ 𝑟 ∈ ℤ ) → ( 6 ≤ ( ( 𝑝 + 𝑞 ) + 𝑟 ) → 5 < ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
55 42 54 syl5bi ⊢ ( ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ ) ∧ 𝑟 ∈ ℤ ) → ( ( 4 + 2 ) ≤ ( ( 𝑝 + 𝑞 ) + 𝑟 ) → 5 < ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
56 55 expcom ⊢ ( 𝑟 ∈ ℤ → ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ ) → ( ( 4 + 2 ) ≤ ( ( 𝑝 + 𝑞 ) + 𝑟 ) → 5 < ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ) )
57 56 3ad2ant2 ⊢ ( ( 2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟 ) → ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ ) → ( ( 4 + 2 ) ≤ ( ( 𝑝 + 𝑞 ) + 𝑟 ) → 5 < ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ) )
58 57 com12 ⊢ ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ ) → ( ( 2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟 ) → ( ( 4 + 2 ) ≤ ( ( 𝑝 + 𝑞 ) + 𝑟 ) → 5 < ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ) )
59 58 adantr ⊢ ( ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ ) ∧ 4 ≤ ( 𝑝 + 𝑞 ) ) → ( ( 2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟 ) → ( ( 4 + 2 ) ≤ ( ( 𝑝 + 𝑞 ) + 𝑟 ) → 5 < ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ) )
60 59 imp ⊢ ( ( ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ ) ∧ 4 ≤ ( 𝑝 + 𝑞 ) ) ∧ ( 2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟 ) ) → ( ( 4 + 2 ) ≤ ( ( 𝑝 + 𝑞 ) + 𝑟 ) → 5 < ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
61 40 60 mpd ⊢ ( ( ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ ) ∧ 4 ≤ ( 𝑝 + 𝑞 ) ) ∧ ( 2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟 ) ) → 5 < ( ( 𝑝 + 𝑞 ) + 𝑟 ) )
62 61 exp31 ⊢ ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ ) → ( 4 ≤ ( 𝑝 + 𝑞 ) → ( ( 2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟 ) → 5 < ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ) )
63 26 62 syl5bi ⊢ ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ ) → ( ( 2 + 2 ) ≤ ( 𝑝 + 𝑞 ) → ( ( 2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟 ) → 5 < ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ) )
64 63 expcom ⊢ ( 𝑞 ∈ ℤ → ( 𝑝 ∈ ℤ → ( ( 2 + 2 ) ≤ ( 𝑝 + 𝑞 ) → ( ( 2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟 ) → 5 < ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ) ) )
65 64 3ad2ant2 ⊢ ( ( 2 ∈ ℤ ∧ 𝑞 ∈ ℤ ∧ 2 ≤ 𝑞 ) → ( 𝑝 ∈ ℤ → ( ( 2 + 2 ) ≤ ( 𝑝 + 𝑞 ) → ( ( 2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟 ) → 5 < ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ) ) )
66 65 com12 ⊢ ( 𝑝 ∈ ℤ → ( ( 2 ∈ ℤ ∧ 𝑞 ∈ ℤ ∧ 2 ≤ 𝑞 ) → ( ( 2 + 2 ) ≤ ( 𝑝 + 𝑞 ) → ( ( 2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟 ) → 5 < ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ) ) )
67 66 3ad2ant2 ⊢ ( ( 2 ∈ ℤ ∧ 𝑝 ∈ ℤ ∧ 2 ≤ 𝑝 ) → ( ( 2 ∈ ℤ ∧ 𝑞 ∈ ℤ ∧ 2 ≤ 𝑞 ) → ( ( 2 + 2 ) ≤ ( 𝑝 + 𝑞 ) → ( ( 2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟 ) → 5 < ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ) ) )
68 67 imp ⊢ ( ( ( 2 ∈ ℤ ∧ 𝑝 ∈ ℤ ∧ 2 ≤ 𝑝 ) ∧ ( 2 ∈ ℤ ∧ 𝑞 ∈ ℤ ∧ 2 ≤ 𝑞 ) ) → ( ( 2 + 2 ) ≤ ( 𝑝 + 𝑞 ) → ( ( 2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟 ) → 5 < ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ) )
69 24 68 mpd ⊢ ( ( ( 2 ∈ ℤ ∧ 𝑝 ∈ ℤ ∧ 2 ≤ 𝑝 ) ∧ ( 2 ∈ ℤ ∧ 𝑞 ∈ ℤ ∧ 2 ≤ 𝑞 ) ) → ( ( 2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟 ) → 5 < ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
70 69 imp ⊢ ( ( ( ( 2 ∈ ℤ ∧ 𝑝 ∈ ℤ ∧ 2 ≤ 𝑝 ) ∧ ( 2 ∈ ℤ ∧ 𝑞 ∈ ℤ ∧ 2 ≤ 𝑞 ) ) ∧ ( 2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟 ) ) → 5 < ( ( 𝑝 + 𝑞 ) + 𝑟 ) )
71 breq2 ⊢ ( 𝑍 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) → ( 5 < 𝑍 ↔ 5 < ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
72 70 71 syl5ibrcom ⊢ ( ( ( ( 2 ∈ ℤ ∧ 𝑝 ∈ ℤ ∧ 2 ≤ 𝑝 ) ∧ ( 2 ∈ ℤ ∧ 𝑞 ∈ ℤ ∧ 2 ≤ 𝑞 ) ) ∧ ( 2 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 2 ≤ 𝑟 ) ) → ( 𝑍 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) → 5 < 𝑍 ) )
73 8 11 72 syl2an ⊢ ( ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) ∧ 𝑟 ∈ ℙ ) → ( 𝑍 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) → 5 < 𝑍 ) )
74 73 rexlimdva ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) → ( ∃ 𝑟 ∈ ℙ 𝑍 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) → 5 < 𝑍 ) )
75 74 adantl ⊢ ( ( 𝑍 ∈ Odd ∧ ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) ) → ( ∃ 𝑟 ∈ ℙ 𝑍 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) → 5 < 𝑍 ) )
76 75 rexlimdvva ⊢ ( 𝑍 ∈ Odd → ( ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑍 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) → 5 < 𝑍 ) )
77 76 imp ⊢ ( ( 𝑍 ∈ Odd ∧ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑍 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) → 5 < 𝑍 )
78 1 77 sylbi ⊢ ( 𝑍 ∈ GoldbachOddW → 5 < 𝑍 )