Metamath Proof Explorer


Theorem sbgoldbalt

Description: An alternate (related to the original) formulation of the binary Goldbach conjecture: Every even integer greater than 2 can be expressed as the sum of two primes. (Contributed by AV, 22-Jul-2020)

Ref Expression
Assertion sbgoldbalt ( ∀ 𝑛 ∈ Even ( 4 < 𝑛𝑛 ∈ GoldbachEven ) ↔ ∀ 𝑛 ∈ Even ( 2 < 𝑛 → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) )

Proof

Step Hyp Ref Expression
1 2z 2 ∈ ℤ
2 evenz ( 𝑛 ∈ Even → 𝑛 ∈ ℤ )
3 zltp1le ( ( 2 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( 2 < 𝑛 ↔ ( 2 + 1 ) ≤ 𝑛 ) )
4 1 2 3 sylancr ( 𝑛 ∈ Even → ( 2 < 𝑛 ↔ ( 2 + 1 ) ≤ 𝑛 ) )
5 2p1e3 ( 2 + 1 ) = 3
6 5 breq1i ( ( 2 + 1 ) ≤ 𝑛 ↔ 3 ≤ 𝑛 )
7 3re 3 ∈ ℝ
8 7 a1i ( 𝑛 ∈ Even → 3 ∈ ℝ )
9 2 zred ( 𝑛 ∈ Even → 𝑛 ∈ ℝ )
10 8 9 leloed ( 𝑛 ∈ Even → ( 3 ≤ 𝑛 ↔ ( 3 < 𝑛 ∨ 3 = 𝑛 ) ) )
11 3z 3 ∈ ℤ
12 zltp1le ( ( 3 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( 3 < 𝑛 ↔ ( 3 + 1 ) ≤ 𝑛 ) )
13 11 2 12 sylancr ( 𝑛 ∈ Even → ( 3 < 𝑛 ↔ ( 3 + 1 ) ≤ 𝑛 ) )
14 3p1e4 ( 3 + 1 ) = 4
15 14 breq1i ( ( 3 + 1 ) ≤ 𝑛 ↔ 4 ≤ 𝑛 )
16 4re 4 ∈ ℝ
17 16 a1i ( 𝑛 ∈ Even → 4 ∈ ℝ )
18 17 9 leloed ( 𝑛 ∈ Even → ( 4 ≤ 𝑛 ↔ ( 4 < 𝑛 ∨ 4 = 𝑛 ) ) )
19 pm3.35 ( ( 4 < 𝑛 ∧ ( 4 < 𝑛𝑛 ∈ GoldbachEven ) ) → 𝑛 ∈ GoldbachEven )
20 isgbe ( 𝑛 ∈ GoldbachEven ↔ ( 𝑛 ∈ Even ∧ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑛 = ( 𝑝 + 𝑞 ) ) ) )
21 simp3 ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑛 = ( 𝑝 + 𝑞 ) ) → 𝑛 = ( 𝑝 + 𝑞 ) )
22 21 a1i ( ( ( 𝑛 ∈ Even ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) → ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑛 = ( 𝑝 + 𝑞 ) ) → 𝑛 = ( 𝑝 + 𝑞 ) ) )
23 22 reximdva ( ( 𝑛 ∈ Even ∧ 𝑝 ∈ ℙ ) → ( ∃ 𝑞 ∈ ℙ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑛 = ( 𝑝 + 𝑞 ) ) → ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) )
24 23 reximdva ( 𝑛 ∈ Even → ( ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑛 = ( 𝑝 + 𝑞 ) ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) )
25 24 imp ( ( 𝑛 ∈ Even ∧ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑛 = ( 𝑝 + 𝑞 ) ) ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) )
26 20 25 sylbi ( 𝑛 ∈ GoldbachEven → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) )
27 26 a1d ( 𝑛 ∈ GoldbachEven → ( 𝑛 ∈ Even → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) )
28 19 27 syl ( ( 4 < 𝑛 ∧ ( 4 < 𝑛𝑛 ∈ GoldbachEven ) ) → ( 𝑛 ∈ Even → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) )
29 28 ex ( 4 < 𝑛 → ( ( 4 < 𝑛𝑛 ∈ GoldbachEven ) → ( 𝑛 ∈ Even → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) ) )
30 29 com23 ( 4 < 𝑛 → ( 𝑛 ∈ Even → ( ( 4 < 𝑛𝑛 ∈ GoldbachEven ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) ) )
31 2prm 2 ∈ ℙ
32 2p2e4 ( 2 + 2 ) = 4
33 32 eqcomi 4 = ( 2 + 2 )
34 rspceov ( ( 2 ∈ ℙ ∧ 2 ∈ ℙ ∧ 4 = ( 2 + 2 ) ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 4 = ( 𝑝 + 𝑞 ) )
35 31 31 33 34 mp3an 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 4 = ( 𝑝 + 𝑞 )
36 eqeq1 ( 4 = 𝑛 → ( 4 = ( 𝑝 + 𝑞 ) ↔ 𝑛 = ( 𝑝 + 𝑞 ) ) )
37 36 2rexbidv ( 4 = 𝑛 → ( ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 4 = ( 𝑝 + 𝑞 ) ↔ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) )
38 35 37 mpbii ( 4 = 𝑛 → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) )
39 38 a1d ( 4 = 𝑛 → ( ( 4 < 𝑛𝑛 ∈ GoldbachEven ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) )
40 39 a1d ( 4 = 𝑛 → ( 𝑛 ∈ Even → ( ( 4 < 𝑛𝑛 ∈ GoldbachEven ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) ) )
41 30 40 jaoi ( ( 4 < 𝑛 ∨ 4 = 𝑛 ) → ( 𝑛 ∈ Even → ( ( 4 < 𝑛𝑛 ∈ GoldbachEven ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) ) )
42 41 com12 ( 𝑛 ∈ Even → ( ( 4 < 𝑛 ∨ 4 = 𝑛 ) → ( ( 4 < 𝑛𝑛 ∈ GoldbachEven ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) ) )
43 18 42 sylbid ( 𝑛 ∈ Even → ( 4 ≤ 𝑛 → ( ( 4 < 𝑛𝑛 ∈ GoldbachEven ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) ) )
44 15 43 syl5bi ( 𝑛 ∈ Even → ( ( 3 + 1 ) ≤ 𝑛 → ( ( 4 < 𝑛𝑛 ∈ GoldbachEven ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) ) )
45 13 44 sylbid ( 𝑛 ∈ Even → ( 3 < 𝑛 → ( ( 4 < 𝑛𝑛 ∈ GoldbachEven ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) ) )
46 45 com12 ( 3 < 𝑛 → ( 𝑛 ∈ Even → ( ( 4 < 𝑛𝑛 ∈ GoldbachEven ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) ) )
47 3odd 3 ∈ Odd
48 eleq1 ( 3 = 𝑛 → ( 3 ∈ Odd ↔ 𝑛 ∈ Odd ) )
49 47 48 mpbii ( 3 = 𝑛𝑛 ∈ Odd )
50 oddneven ( 𝑛 ∈ Odd → ¬ 𝑛 ∈ Even )
51 49 50 syl ( 3 = 𝑛 → ¬ 𝑛 ∈ Even )
52 51 pm2.21d ( 3 = 𝑛 → ( 𝑛 ∈ Even → ( ( 4 < 𝑛𝑛 ∈ GoldbachEven ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) ) )
53 46 52 jaoi ( ( 3 < 𝑛 ∨ 3 = 𝑛 ) → ( 𝑛 ∈ Even → ( ( 4 < 𝑛𝑛 ∈ GoldbachEven ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) ) )
54 53 com12 ( 𝑛 ∈ Even → ( ( 3 < 𝑛 ∨ 3 = 𝑛 ) → ( ( 4 < 𝑛𝑛 ∈ GoldbachEven ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) ) )
55 10 54 sylbid ( 𝑛 ∈ Even → ( 3 ≤ 𝑛 → ( ( 4 < 𝑛𝑛 ∈ GoldbachEven ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) ) )
56 6 55 syl5bi ( 𝑛 ∈ Even → ( ( 2 + 1 ) ≤ 𝑛 → ( ( 4 < 𝑛𝑛 ∈ GoldbachEven ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) ) )
57 4 56 sylbid ( 𝑛 ∈ Even → ( 2 < 𝑛 → ( ( 4 < 𝑛𝑛 ∈ GoldbachEven ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) ) )
58 57 com23 ( 𝑛 ∈ Even → ( ( 4 < 𝑛𝑛 ∈ GoldbachEven ) → ( 2 < 𝑛 → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) ) )
59 2lt4 2 < 4
60 2re 2 ∈ ℝ
61 60 a1i ( 𝑛 ∈ Even → 2 ∈ ℝ )
62 lttr ( ( 2 ∈ ℝ ∧ 4 ∈ ℝ ∧ 𝑛 ∈ ℝ ) → ( ( 2 < 4 ∧ 4 < 𝑛 ) → 2 < 𝑛 ) )
63 61 17 9 62 syl3anc ( 𝑛 ∈ Even → ( ( 2 < 4 ∧ 4 < 𝑛 ) → 2 < 𝑛 ) )
64 59 63 mpani ( 𝑛 ∈ Even → ( 4 < 𝑛 → 2 < 𝑛 ) )
65 64 imp ( ( 𝑛 ∈ Even ∧ 4 < 𝑛 ) → 2 < 𝑛 )
66 simpll ( ( ( 𝑛 ∈ Even ∧ 4 < 𝑛 ) ∧ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) → 𝑛 ∈ Even )
67 simpr ( ( ( 𝑛 ∈ Even ∧ 4 < 𝑛 ) ∧ 𝑝 ∈ ℙ ) → 𝑝 ∈ ℙ )
68 67 anim1i ( ( ( ( 𝑛 ∈ Even ∧ 4 < 𝑛 ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) → ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) )
69 68 adantr ( ( ( ( ( 𝑛 ∈ Even ∧ 4 < 𝑛 ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) ∧ 𝑛 = ( 𝑝 + 𝑞 ) ) → ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) )
70 simpll ( ( ( ( 𝑛 ∈ Even ∧ 4 < 𝑛 ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) → ( 𝑛 ∈ Even ∧ 4 < 𝑛 ) )
71 70 anim1i ( ( ( ( ( 𝑛 ∈ Even ∧ 4 < 𝑛 ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) ∧ 𝑛 = ( 𝑝 + 𝑞 ) ) → ( ( 𝑛 ∈ Even ∧ 4 < 𝑛 ) ∧ 𝑛 = ( 𝑝 + 𝑞 ) ) )
72 df-3an ( ( 𝑛 ∈ Even ∧ 4 < 𝑛𝑛 = ( 𝑝 + 𝑞 ) ) ↔ ( ( 𝑛 ∈ Even ∧ 4 < 𝑛 ) ∧ 𝑛 = ( 𝑝 + 𝑞 ) ) )
73 71 72 sylibr ( ( ( ( ( 𝑛 ∈ Even ∧ 4 < 𝑛 ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) ∧ 𝑛 = ( 𝑝 + 𝑞 ) ) → ( 𝑛 ∈ Even ∧ 4 < 𝑛𝑛 = ( 𝑝 + 𝑞 ) ) )
74 sbgoldbaltlem2 ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) → ( ( 𝑛 ∈ Even ∧ 4 < 𝑛𝑛 = ( 𝑝 + 𝑞 ) ) → ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ) ) )
75 69 73 74 sylc ( ( ( ( ( 𝑛 ∈ Even ∧ 4 < 𝑛 ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) ∧ 𝑛 = ( 𝑝 + 𝑞 ) ) → ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ) )
76 simpr ( ( ( ( ( 𝑛 ∈ Even ∧ 4 < 𝑛 ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) ∧ 𝑛 = ( 𝑝 + 𝑞 ) ) → 𝑛 = ( 𝑝 + 𝑞 ) )
77 df-3an ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑛 = ( 𝑝 + 𝑞 ) ) ↔ ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ) ∧ 𝑛 = ( 𝑝 + 𝑞 ) ) )
78 75 76 77 sylanbrc ( ( ( ( ( 𝑛 ∈ Even ∧ 4 < 𝑛 ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) ∧ 𝑛 = ( 𝑝 + 𝑞 ) ) → ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑛 = ( 𝑝 + 𝑞 ) ) )
79 78 ex ( ( ( ( 𝑛 ∈ Even ∧ 4 < 𝑛 ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) → ( 𝑛 = ( 𝑝 + 𝑞 ) → ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑛 = ( 𝑝 + 𝑞 ) ) ) )
80 79 reximdva ( ( ( 𝑛 ∈ Even ∧ 4 < 𝑛 ) ∧ 𝑝 ∈ ℙ ) → ( ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) → ∃ 𝑞 ∈ ℙ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑛 = ( 𝑝 + 𝑞 ) ) ) )
81 80 reximdva ( ( 𝑛 ∈ Even ∧ 4 < 𝑛 ) → ( ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑛 = ( 𝑝 + 𝑞 ) ) ) )
82 81 imp ( ( ( 𝑛 ∈ Even ∧ 4 < 𝑛 ) ∧ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑛 = ( 𝑝 + 𝑞 ) ) )
83 66 82 jca ( ( ( 𝑛 ∈ Even ∧ 4 < 𝑛 ) ∧ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) → ( 𝑛 ∈ Even ∧ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑛 = ( 𝑝 + 𝑞 ) ) ) )
84 83 ex ( ( 𝑛 ∈ Even ∧ 4 < 𝑛 ) → ( ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) → ( 𝑛 ∈ Even ∧ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑛 = ( 𝑝 + 𝑞 ) ) ) ) )
85 84 20 syl6ibr ( ( 𝑛 ∈ Even ∧ 4 < 𝑛 ) → ( ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) → 𝑛 ∈ GoldbachEven ) )
86 65 85 embantd ( ( 𝑛 ∈ Even ∧ 4 < 𝑛 ) → ( ( 2 < 𝑛 → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) → 𝑛 ∈ GoldbachEven ) )
87 86 ex ( 𝑛 ∈ Even → ( 4 < 𝑛 → ( ( 2 < 𝑛 → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) → 𝑛 ∈ GoldbachEven ) ) )
88 87 com23 ( 𝑛 ∈ Even → ( ( 2 < 𝑛 → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) → ( 4 < 𝑛𝑛 ∈ GoldbachEven ) ) )
89 58 88 impbid ( 𝑛 ∈ Even → ( ( 4 < 𝑛𝑛 ∈ GoldbachEven ) ↔ ( 2 < 𝑛 → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) ) )
90 89 ralbiia ( ∀ 𝑛 ∈ Even ( 4 < 𝑛𝑛 ∈ GoldbachEven ) ↔ ∀ 𝑛 ∈ Even ( 2 < 𝑛 → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) )