Metamath Proof Explorer

Theorem sgoldbeven3prm

Description: If the binary Goldbach conjecture is valid, then an even integer greater than 5 can be expressed as the sum of three primes: Since ( N - 2 ) is even iff N is even, there would be primes p and q with ( N - 2 ) = ( p + q ) , and therefore N = ( ( p + q ) + 2 ) . (Contributed by AV, 24-Dec-2021)

Ref Expression
Assertion sgoldbeven3prm ⊢∀n∈Even4<n→n∈GoldbachEven→N∈Even∧6≤N→∃p∈ℙ∃q∈ℙ∃r∈ℙN=p+q+r

Proof

Step Hyp Ref Expression
1 sbgoldbb ⊢∀n∈Even4<n→n∈GoldbachEven→∀n∈Even2<n→∃p∈ℙ∃q∈ℙn=p+q
2 2p2e4 ⊢2+2=4
3 evenz ⊢N∈Even→N∈ℤ
4 3 zred ⊢N∈Even→N∈ℝ
5 4lt6 ⊢4<6
6 4re ⊢4∈ℝ
7 6re ⊢6∈ℝ
8 ltletr ⊢4∈ℝ∧6∈ℝ∧N∈ℝ→4<6∧6≤N→4<N
9 6 7 8 mp3an12 ⊢N∈ℝ→4<6∧6≤N→4<N
10 5 9 mpani ⊢N∈ℝ→6≤N→4<N
11 4 10 syl ⊢N∈Even→6≤N→4<N
12 11 imp ⊢N∈Even∧6≤N→4<N
13 2 12 eqbrtrid ⊢N∈Even∧6≤N→2+2<N
14 2re ⊢2∈ℝ
15 14 a1i ⊢N∈Even∧6≤N→2∈ℝ
16 4 adantr ⊢N∈Even∧6≤N→N∈ℝ
17 15 15 16 ltaddsub2d ⊢N∈Even∧6≤N→2+2<N↔2<N−2
18 13 17 mpbid ⊢N∈Even∧6≤N→2<N−2
19 2evenALTV ⊢2∈Even
20 emee ⊢N∈Even∧2∈Even→N−2∈Even
21 19 20 mpan2 ⊢N∈Even→N−2∈Even
22 breq2 ⊢n=N−2→2<n↔2<N−2
23 eqeq1 ⊢n=N−2→n=p+q↔N−2=p+q
24 23 2rexbidv ⊢n=N−2→∃p∈ℙ∃q∈ℙn=p+q↔∃p∈ℙ∃q∈ℙN−2=p+q
25 22 24 imbi12d ⊢n=N−2→2<n→∃p∈ℙ∃q∈ℙn=p+q↔2<N−2→∃p∈ℙ∃q∈ℙN−2=p+q
26 25 rspcv ⊢N−2∈Even→∀n∈Even2<n→∃p∈ℙ∃q∈ℙn=p+q→2<N−2→∃p∈ℙ∃q∈ℙN−2=p+q
27 2prm ⊢2∈ℙ
28 27 a1i ⊢N∈Even∧N−2=p+q→2∈ℙ
29 oveq2 ⊢r=2→p+q+r=p+q+2
30 29 eqeq2d ⊢r=2→N=p+q+r↔N=p+q+2
31 30 adantl ⊢N∈Even∧N−2=p+q∧r=2→N=p+q+r↔N=p+q+2
32 3 zcnd ⊢N∈Even→N∈ℂ
33 2cnd ⊢N∈Even→2∈ℂ
34 npcan ⊢N∈ℂ∧2∈ℂ→N-2+2=N
35 34 eqcomd ⊢N∈ℂ∧2∈ℂ→N=N-2+2
36 32 33 35 syl2anc ⊢N∈Even→N=N-2+2
37 36 adantr ⊢N∈Even∧N−2=p+q→N=N-2+2
38 simpr ⊢N∈Even∧N−2=p+q→N−2=p+q
39 38 oveq1d ⊢N∈Even∧N−2=p+q→N-2+2=p+q+2
40 37 39 eqtrd ⊢N∈Even∧N−2=p+q→N=p+q+2
41 28 31 40 rspcedvd ⊢N∈Even∧N−2=p+q→∃r∈ℙN=p+q+r
42 41 ex ⊢N∈Even→N−2=p+q→∃r∈ℙN=p+q+r
43 42 reximdv ⊢N∈Even→∃q∈ℙN−2=p+q→∃q∈ℙ∃r∈ℙN=p+q+r
44 43 reximdv ⊢N∈Even→∃p∈ℙ∃q∈ℙN−2=p+q→∃p∈ℙ∃q∈ℙ∃r∈ℙN=p+q+r
45 44 imim2d ⊢N∈Even→2<N−2→∃p∈ℙ∃q∈ℙN−2=p+q→2<N−2→∃p∈ℙ∃q∈ℙ∃r∈ℙN=p+q+r
46 26 45 syl9r ⊢N∈Even→N−2∈Even→∀n∈Even2<n→∃p∈ℙ∃q∈ℙn=p+q→2<N−2→∃p∈ℙ∃q∈ℙ∃r∈ℙN=p+q+r
47 21 46 mpd ⊢N∈Even→∀n∈Even2<n→∃p∈ℙ∃q∈ℙn=p+q→2<N−2→∃p∈ℙ∃q∈ℙ∃r∈ℙN=p+q+r
48 47 adantr ⊢N∈Even∧6≤N→∀n∈Even2<n→∃p∈ℙ∃q∈ℙn=p+q→2<N−2→∃p∈ℙ∃q∈ℙ∃r∈ℙN=p+q+r
49 18 48 mpid ⊢N∈Even∧6≤N→∀n∈Even2<n→∃p∈ℙ∃q∈ℙn=p+q→∃p∈ℙ∃q∈ℙ∃r∈ℙN=p+q+r
50 1 49 syl5com ⊢∀n∈Even4<n→n∈GoldbachEven→N∈Even∧6≤N→∃p∈ℙ∃q∈ℙ∃r∈ℙN=p+q+r