Metamath Proof Explorer

Theorem sbgoldbm

Description: If the strong binary Goldbach conjecture is valid, the modern version of the original formulation of the Goldbach conjecture also holds: Every integer greater than 5 can be expressed as the sum of three primes. (Contributed by AV, 24-Dec-2021)

Ref Expression
Assertion sbgoldbm ( ∀ 𝑛 ∈ Even ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ∀ 𝑛 ∈ ( ℤ≥ ‘ 6 ) ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) )

Proof

Step Hyp Ref Expression
1 breq2 ⊢ ( 𝑛 = 𝑚 → ( 4 < 𝑛 ↔ 4 < 𝑚 ) )
2 eleq1w ⊢ ( 𝑛 = 𝑚 → ( 𝑛 ∈ GoldbachEven ↔ 𝑚 ∈ GoldbachEven ) )
3 1 2 imbi12d ⊢ ( 𝑛 = 𝑚 → ( ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) ↔ ( 4 < 𝑚 → 𝑚 ∈ GoldbachEven ) ) )
4 3 cbvralvw ⊢ ( ∀ 𝑛 ∈ Even ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) ↔ ∀ 𝑚 ∈ Even ( 4 < 𝑚 → 𝑚 ∈ GoldbachEven ) )
5 eluz2 ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 6 ) ↔ ( 6 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 6 ≤ 𝑛 ) )
6 zeoALTV ⊢ ( 𝑛 ∈ ℤ → ( 𝑛 ∈ Even ∨ 𝑛 ∈ Odd ) )
7 sgoldbeven3prm ⊢ ( ∀ 𝑚 ∈ Even ( 4 < 𝑚 → 𝑚 ∈ GoldbachEven ) → ( ( 𝑛 ∈ Even ∧ 6 ≤ 𝑛 ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
8 7 expdcom ⊢ ( 𝑛 ∈ Even → ( 6 ≤ 𝑛 → ( ∀ 𝑚 ∈ Even ( 4 < 𝑚 → 𝑚 ∈ GoldbachEven ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ) )
9 sbgoldbwt ⊢ ( ∀ 𝑚 ∈ Even ( 4 < 𝑚 → 𝑚 ∈ GoldbachEven ) → ∀ 𝑛 ∈ Odd ( 5 < 𝑛 → 𝑛 ∈ GoldbachOddW ) )
10 rspa ⊢ ( ( ∀ 𝑛 ∈ Odd ( 5 < 𝑛 → 𝑛 ∈ GoldbachOddW ) ∧ 𝑛 ∈ Odd ) → ( 5 < 𝑛 → 𝑛 ∈ GoldbachOddW ) )
11 df-6 ⊢ 6 = ( 5 + 1 )
12 11 breq1i ⊢ ( 6 ≤ 𝑛 ↔ ( 5 + 1 ) ≤ 𝑛 )
13 5nn ⊢ 5 ∈ ℕ
14 13 nnzi ⊢ 5 ∈ ℤ
15 oddz ⊢ ( 𝑛 ∈ Odd → 𝑛 ∈ ℤ )
16 zltp1le ⊢ ( ( 5 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( 5 < 𝑛 ↔ ( 5 + 1 ) ≤ 𝑛 ) )
17 14 15 16 sylancr ⊢ ( 𝑛 ∈ Odd → ( 5 < 𝑛 ↔ ( 5 + 1 ) ≤ 𝑛 ) )
18 17 biimprd ⊢ ( 𝑛 ∈ Odd → ( ( 5 + 1 ) ≤ 𝑛 → 5 < 𝑛 ) )
19 12 18 syl5bi ⊢ ( 𝑛 ∈ Odd → ( 6 ≤ 𝑛 → 5 < 𝑛 ) )
20 19 imp ⊢ ( ( 𝑛 ∈ Odd ∧ 6 ≤ 𝑛 ) → 5 < 𝑛 )
21 isgbow ⊢ ( 𝑛 ∈ GoldbachOddW ↔ ( 𝑛 ∈ Odd ∧ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
22 21 simprbi ⊢ ( 𝑛 ∈ GoldbachOddW → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) )
23 22 a1i ⊢ ( ( 𝑛 ∈ Odd ∧ 6 ≤ 𝑛 ) → ( 𝑛 ∈ GoldbachOddW → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
24 20 23 embantd ⊢ ( ( 𝑛 ∈ Odd ∧ 6 ≤ 𝑛 ) → ( ( 5 < 𝑛 → 𝑛 ∈ GoldbachOddW ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
25 24 ex ⊢ ( 𝑛 ∈ Odd → ( 6 ≤ 𝑛 → ( ( 5 < 𝑛 → 𝑛 ∈ GoldbachOddW ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ) )
26 25 com23 ⊢ ( 𝑛 ∈ Odd → ( ( 5 < 𝑛 → 𝑛 ∈ GoldbachOddW ) → ( 6 ≤ 𝑛 → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ) )
27 26 adantl ⊢ ( ( ∀ 𝑛 ∈ Odd ( 5 < 𝑛 → 𝑛 ∈ GoldbachOddW ) ∧ 𝑛 ∈ Odd ) → ( ( 5 < 𝑛 → 𝑛 ∈ GoldbachOddW ) → ( 6 ≤ 𝑛 → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ) )
28 10 27 mpd ⊢ ( ( ∀ 𝑛 ∈ Odd ( 5 < 𝑛 → 𝑛 ∈ GoldbachOddW ) ∧ 𝑛 ∈ Odd ) → ( 6 ≤ 𝑛 → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
29 28 ex ⊢ ( ∀ 𝑛 ∈ Odd ( 5 < 𝑛 → 𝑛 ∈ GoldbachOddW ) → ( 𝑛 ∈ Odd → ( 6 ≤ 𝑛 → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ) )
30 29 com23 ⊢ ( ∀ 𝑛 ∈ Odd ( 5 < 𝑛 → 𝑛 ∈ GoldbachOddW ) → ( 6 ≤ 𝑛 → ( 𝑛 ∈ Odd → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ) )
31 9 30 syl ⊢ ( ∀ 𝑚 ∈ Even ( 4 < 𝑚 → 𝑚 ∈ GoldbachEven ) → ( 6 ≤ 𝑛 → ( 𝑛 ∈ Odd → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ) )
32 31 com13 ⊢ ( 𝑛 ∈ Odd → ( 6 ≤ 𝑛 → ( ∀ 𝑚 ∈ Even ( 4 < 𝑚 → 𝑚 ∈ GoldbachEven ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ) )
33 8 32 jaoi ⊢ ( ( 𝑛 ∈ Even ∨ 𝑛 ∈ Odd ) → ( 6 ≤ 𝑛 → ( ∀ 𝑚 ∈ Even ( 4 < 𝑚 → 𝑚 ∈ GoldbachEven ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ) )
34 6 33 syl ⊢ ( 𝑛 ∈ ℤ → ( 6 ≤ 𝑛 → ( ∀ 𝑚 ∈ Even ( 4 < 𝑚 → 𝑚 ∈ GoldbachEven ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ) )
35 34 imp ⊢ ( ( 𝑛 ∈ ℤ ∧ 6 ≤ 𝑛 ) → ( ∀ 𝑚 ∈ Even ( 4 < 𝑚 → 𝑚 ∈ GoldbachEven ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
36 35 3adant1 ⊢ ( ( 6 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 6 ≤ 𝑛 ) → ( ∀ 𝑚 ∈ Even ( 4 < 𝑚 → 𝑚 ∈ GoldbachEven ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
37 5 36 sylbi ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 6 ) → ( ∀ 𝑚 ∈ Even ( 4 < 𝑚 → 𝑚 ∈ GoldbachEven ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
38 37 impcom ⊢ ( ( ∀ 𝑚 ∈ Even ( 4 < 𝑚 → 𝑚 ∈ GoldbachEven ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 6 ) ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) )
39 38 ralrimiva ⊢ ( ∀ 𝑚 ∈ Even ( 4 < 𝑚 → 𝑚 ∈ GoldbachEven ) → ∀ 𝑛 ∈ ( ℤ≥ ‘ 6 ) ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) )
40 4 39 sylbi ⊢ ( ∀ 𝑛 ∈ Even ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ∀ 𝑛 ∈ ( ℤ≥ ‘ 6 ) ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) )