Metamath Proof Explorer

Theorem tgoldbachgt

Description: Odd integers greater than ( ; 1 0 ^ ; 2 7 ) have at least a representation as a sum of three odd primes. Final statement in section 7.4 of Helfgott p. 70 , expressed using the set G of odd numbers which can be written as a sum of three odd primes. (Contributed by Thierry Arnoux, 22-Dec-2021)

Ref Expression
Hypotheses tgoldbachgt.o ⊢ 𝑂 = { 𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧 }
tgoldbachgt.g ⊢ 𝐺 = { 𝑧 ∈ 𝑂 ∣ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ ( ( 𝑝 ∈ 𝑂 ∧ 𝑞 ∈ 𝑂 ∧ 𝑟 ∈ 𝑂 ) ∧ 𝑧 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) }
Assertion tgoldbachgt ∃ 𝑚 ∈ ℕ ( 𝑚 ≤ ( 1 0 ↑ 2 7 ) ∧ ∀ 𝑛 ∈ 𝑂 ( 𝑚 < 𝑛 → 𝑛 ∈ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 tgoldbachgt.o ⊢ 𝑂 = { 𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧 }
2 tgoldbachgt.g ⊢ 𝐺 = { 𝑧 ∈ 𝑂 ∣ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ ( ( 𝑝 ∈ 𝑂 ∧ 𝑞 ∈ 𝑂 ∧ 𝑟 ∈ 𝑂 ) ∧ 𝑧 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) }
3 10nn ⊢ 1 0 ∈ ℕ
4 2nn0 ⊢ 2 ∈ ℕ0
5 7nn0 ⊢ 7 ∈ ℕ0
6 4 5 deccl ⊢ 2 7 ∈ ℕ0
7 nnexpcl ⊢ ( ( 1 0 ∈ ℕ ∧ 2 7 ∈ ℕ0 ) → ( 1 0 ↑ 2 7 ) ∈ ℕ )
8 3 6 7 mp2an ⊢ ( 1 0 ↑ 2 7 ) ∈ ℕ
9 8 nnrei ⊢ ( 1 0 ↑ 2 7 ) ∈ ℝ
10 9 leidi ⊢ ( 1 0 ↑ 2 7 ) ≤ ( 1 0 ↑ 2 7 )
11 simpl ⊢ ( ( 𝑛 ∈ 𝑂 ∧ ( 1 0 ↑ 2 7 ) < 𝑛 ) → 𝑛 ∈ 𝑂 )
12 inss2 ⊢ ( 𝑂 ∩ ℙ ) ⊆ ℙ
13 prmssnn ⊢ ℙ ⊆ ℕ
14 12 13 sstri ⊢ ( 𝑂 ∩ ℙ ) ⊆ ℕ
15 14 a1i ⊢ ( ( ( 𝑛 ∈ 𝑂 ∧ ( 1 0 ↑ 2 7 ) < 𝑛 ) ∧ 𝑐 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑛 ) ) → ( 𝑂 ∩ ℙ ) ⊆ ℕ )
16 1 eleq2i ⊢ ( 𝑛 ∈ 𝑂 ↔ 𝑛 ∈ { 𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧 } )
17 elrabi ⊢ ( 𝑛 ∈ { 𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧 } → 𝑛 ∈ ℤ )
18 16 17 sylbi ⊢ ( 𝑛 ∈ 𝑂 → 𝑛 ∈ ℤ )
19 18 ad2antrr ⊢ ( ( ( 𝑛 ∈ 𝑂 ∧ ( 1 0 ↑ 2 7 ) < 𝑛 ) ∧ 𝑐 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑛 ) ) → 𝑛 ∈ ℤ )
20 3nn0 ⊢ 3 ∈ ℕ0
21 20 a1i ⊢ ( ( ( 𝑛 ∈ 𝑂 ∧ ( 1 0 ↑ 2 7 ) < 𝑛 ) ∧ 𝑐 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑛 ) ) → 3 ∈ ℕ0 )
22 simpr ⊢ ( ( ( 𝑛 ∈ 𝑂 ∧ ( 1 0 ↑ 2 7 ) < 𝑛 ) ∧ 𝑐 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑛 ) ) → 𝑐 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑛 ) )
23 15 19 21 22 reprf ⊢ ( ( ( 𝑛 ∈ 𝑂 ∧ ( 1 0 ↑ 2 7 ) < 𝑛 ) ∧ 𝑐 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑛 ) ) → 𝑐 : ( 0 ..^ 3 ) ⟶ ( 𝑂 ∩ ℙ ) )
24 c0ex ⊢ 0 ∈ V
25 24 tpid1 ⊢ 0 ∈ { 0 , 1 , 2 }
26 fzo0to3tp ⊢ ( 0 ..^ 3 ) = { 0 , 1 , 2 }
27 25 26 eleqtrri ⊢ 0 ∈ ( 0 ..^ 3 )
28 27 a1i ⊢ ( ( ( 𝑛 ∈ 𝑂 ∧ ( 1 0 ↑ 2 7 ) < 𝑛 ) ∧ 𝑐 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑛 ) ) → 0 ∈ ( 0 ..^ 3 ) )
29 23 28 ffvelcdmd ⊢ ( ( ( 𝑛 ∈ 𝑂 ∧ ( 1 0 ↑ 2 7 ) < 𝑛 ) ∧ 𝑐 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑛 ) ) → ( 𝑐 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) )
30 29 elin2d ⊢ ( ( ( 𝑛 ∈ 𝑂 ∧ ( 1 0 ↑ 2 7 ) < 𝑛 ) ∧ 𝑐 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑛 ) ) → ( 𝑐 ‘ 0 ) ∈ ℙ )
31 1ex ⊢ 1 ∈ V
32 31 tpid2 ⊢ 1 ∈ { 0 , 1 , 2 }
33 32 26 eleqtrri ⊢ 1 ∈ ( 0 ..^ 3 )
34 33 a1i ⊢ ( ( ( 𝑛 ∈ 𝑂 ∧ ( 1 0 ↑ 2 7 ) < 𝑛 ) ∧ 𝑐 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑛 ) ) → 1 ∈ ( 0 ..^ 3 ) )
35 23 34 ffvelcdmd ⊢ ( ( ( 𝑛 ∈ 𝑂 ∧ ( 1 0 ↑ 2 7 ) < 𝑛 ) ∧ 𝑐 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑛 ) ) → ( 𝑐 ‘ 1 ) ∈ ( 𝑂 ∩ ℙ ) )
36 35 elin2d ⊢ ( ( ( 𝑛 ∈ 𝑂 ∧ ( 1 0 ↑ 2 7 ) < 𝑛 ) ∧ 𝑐 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑛 ) ) → ( 𝑐 ‘ 1 ) ∈ ℙ )
37 2ex ⊢ 2 ∈ V
38 37 tpid3 ⊢ 2 ∈ { 0 , 1 , 2 }
39 38 26 eleqtrri ⊢ 2 ∈ ( 0 ..^ 3 )
40 39 a1i ⊢ ( ( ( 𝑛 ∈ 𝑂 ∧ ( 1 0 ↑ 2 7 ) < 𝑛 ) ∧ 𝑐 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑛 ) ) → 2 ∈ ( 0 ..^ 3 ) )
41 23 40 ffvelcdmd ⊢ ( ( ( 𝑛 ∈ 𝑂 ∧ ( 1 0 ↑ 2 7 ) < 𝑛 ) ∧ 𝑐 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑛 ) ) → ( 𝑐 ‘ 2 ) ∈ ( 𝑂 ∩ ℙ ) )
42 41 elin2d ⊢ ( ( ( 𝑛 ∈ 𝑂 ∧ ( 1 0 ↑ 2 7 ) < 𝑛 ) ∧ 𝑐 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑛 ) ) → ( 𝑐 ‘ 2 ) ∈ ℙ )
43 29 elin1d ⊢ ( ( ( 𝑛 ∈ 𝑂 ∧ ( 1 0 ↑ 2 7 ) < 𝑛 ) ∧ 𝑐 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑛 ) ) → ( 𝑐 ‘ 0 ) ∈ 𝑂 )
44 35 elin1d ⊢ ( ( ( 𝑛 ∈ 𝑂 ∧ ( 1 0 ↑ 2 7 ) < 𝑛 ) ∧ 𝑐 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑛 ) ) → ( 𝑐 ‘ 1 ) ∈ 𝑂 )
45 41 elin1d ⊢ ( ( ( 𝑛 ∈ 𝑂 ∧ ( 1 0 ↑ 2 7 ) < 𝑛 ) ∧ 𝑐 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑛 ) ) → ( 𝑐 ‘ 2 ) ∈ 𝑂 )
46 43 44 45 3jca ⊢ ( ( ( 𝑛 ∈ 𝑂 ∧ ( 1 0 ↑ 2 7 ) < 𝑛 ) ∧ 𝑐 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑛 ) ) → ( ( 𝑐 ‘ 0 ) ∈ 𝑂 ∧ ( 𝑐 ‘ 1 ) ∈ 𝑂 ∧ ( 𝑐 ‘ 2 ) ∈ 𝑂 ) )
47 26 a1i ⊢ ( ( ( 𝑛 ∈ 𝑂 ∧ ( 1 0 ↑ 2 7 ) < 𝑛 ) ∧ 𝑐 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑛 ) ) → ( 0 ..^ 3 ) = { 0 , 1 , 2 } )
48 47 sumeq1d ⊢ ( ( ( 𝑛 ∈ 𝑂 ∧ ( 1 0 ↑ 2 7 ) < 𝑛 ) ∧ 𝑐 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑛 ) ) → Σ 𝑖 ∈ ( 0 ..^ 3 ) ( 𝑐 ‘ 𝑖 ) = Σ 𝑖 ∈ { 0 , 1 , 2 } ( 𝑐 ‘ 𝑖 ) )
49 15 19 21 22 reprsum ⊢ ( ( ( 𝑛 ∈ 𝑂 ∧ ( 1 0 ↑ 2 7 ) < 𝑛 ) ∧ 𝑐 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑛 ) ) → Σ 𝑖 ∈ ( 0 ..^ 3 ) ( 𝑐 ‘ 𝑖 ) = 𝑛 )
50 fveq2 ⊢ ( 𝑖 = 0 → ( 𝑐 ‘ 𝑖 ) = ( 𝑐 ‘ 0 ) )
51 fveq2 ⊢ ( 𝑖 = 1 → ( 𝑐 ‘ 𝑖 ) = ( 𝑐 ‘ 1 ) )
52 fveq2 ⊢ ( 𝑖 = 2 → ( 𝑐 ‘ 𝑖 ) = ( 𝑐 ‘ 2 ) )
53 14 29 sselid ⊢ ( ( ( 𝑛 ∈ 𝑂 ∧ ( 1 0 ↑ 2 7 ) < 𝑛 ) ∧ 𝑐 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑛 ) ) → ( 𝑐 ‘ 0 ) ∈ ℕ )
54 53 nncnd ⊢ ( ( ( 𝑛 ∈ 𝑂 ∧ ( 1 0 ↑ 2 7 ) < 𝑛 ) ∧ 𝑐 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑛 ) ) → ( 𝑐 ‘ 0 ) ∈ ℂ )
55 14 35 sselid ⊢ ( ( ( 𝑛 ∈ 𝑂 ∧ ( 1 0 ↑ 2 7 ) < 𝑛 ) ∧ 𝑐 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑛 ) ) → ( 𝑐 ‘ 1 ) ∈ ℕ )
56 55 nncnd ⊢ ( ( ( 𝑛 ∈ 𝑂 ∧ ( 1 0 ↑ 2 7 ) < 𝑛 ) ∧ 𝑐 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑛 ) ) → ( 𝑐 ‘ 1 ) ∈ ℂ )
57 14 41 sselid ⊢ ( ( ( 𝑛 ∈ 𝑂 ∧ ( 1 0 ↑ 2 7 ) < 𝑛 ) ∧ 𝑐 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑛 ) ) → ( 𝑐 ‘ 2 ) ∈ ℕ )
58 57 nncnd ⊢ ( ( ( 𝑛 ∈ 𝑂 ∧ ( 1 0 ↑ 2 7 ) < 𝑛 ) ∧ 𝑐 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑛 ) ) → ( 𝑐 ‘ 2 ) ∈ ℂ )
59 54 56 58 3jca ⊢ ( ( ( 𝑛 ∈ 𝑂 ∧ ( 1 0 ↑ 2 7 ) < 𝑛 ) ∧ 𝑐 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑛 ) ) → ( ( 𝑐 ‘ 0 ) ∈ ℂ ∧ ( 𝑐 ‘ 1 ) ∈ ℂ ∧ ( 𝑐 ‘ 2 ) ∈ ℂ ) )
60 24 a1i ⊢ ( ( ( 𝑛 ∈ 𝑂 ∧ ( 1 0 ↑ 2 7 ) < 𝑛 ) ∧ 𝑐 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑛 ) ) → 0 ∈ V )
61 31 a1i ⊢ ( ( ( 𝑛 ∈ 𝑂 ∧ ( 1 0 ↑ 2 7 ) < 𝑛 ) ∧ 𝑐 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑛 ) ) → 1 ∈ V )
62 37 a1i ⊢ ( ( ( 𝑛 ∈ 𝑂 ∧ ( 1 0 ↑ 2 7 ) < 𝑛 ) ∧ 𝑐 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑛 ) ) → 2 ∈ V )
63 60 61 62 3jca ⊢ ( ( ( 𝑛 ∈ 𝑂 ∧ ( 1 0 ↑ 2 7 ) < 𝑛 ) ∧ 𝑐 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑛 ) ) → ( 0 ∈ V ∧ 1 ∈ V ∧ 2 ∈ V ) )
64 0ne1 ⊢ 0 ≠ 1
65 64 a1i ⊢ ( ( ( 𝑛 ∈ 𝑂 ∧ ( 1 0 ↑ 2 7 ) < 𝑛 ) ∧ 𝑐 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑛 ) ) → 0 ≠ 1 )
66 0ne2 ⊢ 0 ≠ 2
67 66 a1i ⊢ ( ( ( 𝑛 ∈ 𝑂 ∧ ( 1 0 ↑ 2 7 ) < 𝑛 ) ∧ 𝑐 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑛 ) ) → 0 ≠ 2 )
68 1ne2 ⊢ 1 ≠ 2
69 68 a1i ⊢ ( ( ( 𝑛 ∈ 𝑂 ∧ ( 1 0 ↑ 2 7 ) < 𝑛 ) ∧ 𝑐 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑛 ) ) → 1 ≠ 2 )
70 50 51 52 59 63 65 67 69 sumtp ⊢ ( ( ( 𝑛 ∈ 𝑂 ∧ ( 1 0 ↑ 2 7 ) < 𝑛 ) ∧ 𝑐 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑛 ) ) → Σ 𝑖 ∈ { 0 , 1 , 2 } ( 𝑐 ‘ 𝑖 ) = ( ( ( 𝑐 ‘ 0 ) + ( 𝑐 ‘ 1 ) ) + ( 𝑐 ‘ 2 ) ) )
71 48 49 70 3eqtr3d ⊢ ( ( ( 𝑛 ∈ 𝑂 ∧ ( 1 0 ↑ 2 7 ) < 𝑛 ) ∧ 𝑐 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑛 ) ) → 𝑛 = ( ( ( 𝑐 ‘ 0 ) + ( 𝑐 ‘ 1 ) ) + ( 𝑐 ‘ 2 ) ) )
72 46 71 jca ⊢ ( ( ( 𝑛 ∈ 𝑂 ∧ ( 1 0 ↑ 2 7 ) < 𝑛 ) ∧ 𝑐 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑛 ) ) → ( ( ( 𝑐 ‘ 0 ) ∈ 𝑂 ∧ ( 𝑐 ‘ 1 ) ∈ 𝑂 ∧ ( 𝑐 ‘ 2 ) ∈ 𝑂 ) ∧ 𝑛 = ( ( ( 𝑐 ‘ 0 ) + ( 𝑐 ‘ 1 ) ) + ( 𝑐 ‘ 2 ) ) ) )
73 eleq1 ⊢ ( 𝑝 = ( 𝑐 ‘ 0 ) → ( 𝑝 ∈ 𝑂 ↔ ( 𝑐 ‘ 0 ) ∈ 𝑂 ) )
74 73 3anbi1d ⊢ ( 𝑝 = ( 𝑐 ‘ 0 ) → ( ( 𝑝 ∈ 𝑂 ∧ 𝑞 ∈ 𝑂 ∧ 𝑟 ∈ 𝑂 ) ↔ ( ( 𝑐 ‘ 0 ) ∈ 𝑂 ∧ 𝑞 ∈ 𝑂 ∧ 𝑟 ∈ 𝑂 ) ) )
75 oveq1 ⊢ ( 𝑝 = ( 𝑐 ‘ 0 ) → ( 𝑝 + 𝑞 ) = ( ( 𝑐 ‘ 0 ) + 𝑞 ) )
76 75 oveq1d ⊢ ( 𝑝 = ( 𝑐 ‘ 0 ) → ( ( 𝑝 + 𝑞 ) + 𝑟 ) = ( ( ( 𝑐 ‘ 0 ) + 𝑞 ) + 𝑟 ) )
77 76 eqeq2d ⊢ ( 𝑝 = ( 𝑐 ‘ 0 ) → ( 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ↔ 𝑛 = ( ( ( 𝑐 ‘ 0 ) + 𝑞 ) + 𝑟 ) ) )
78 74 77 anbi12d ⊢ ( 𝑝 = ( 𝑐 ‘ 0 ) → ( ( ( 𝑝 ∈ 𝑂 ∧ 𝑞 ∈ 𝑂 ∧ 𝑟 ∈ 𝑂 ) ∧ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ↔ ( ( ( 𝑐 ‘ 0 ) ∈ 𝑂 ∧ 𝑞 ∈ 𝑂 ∧ 𝑟 ∈ 𝑂 ) ∧ 𝑛 = ( ( ( 𝑐 ‘ 0 ) + 𝑞 ) + 𝑟 ) ) ) )
79 eleq1 ⊢ ( 𝑞 = ( 𝑐 ‘ 1 ) → ( 𝑞 ∈ 𝑂 ↔ ( 𝑐 ‘ 1 ) ∈ 𝑂 ) )
80 79 3anbi2d ⊢ ( 𝑞 = ( 𝑐 ‘ 1 ) → ( ( ( 𝑐 ‘ 0 ) ∈ 𝑂 ∧ 𝑞 ∈ 𝑂 ∧ 𝑟 ∈ 𝑂 ) ↔ ( ( 𝑐 ‘ 0 ) ∈ 𝑂 ∧ ( 𝑐 ‘ 1 ) ∈ 𝑂 ∧ 𝑟 ∈ 𝑂 ) ) )
81 oveq2 ⊢ ( 𝑞 = ( 𝑐 ‘ 1 ) → ( ( 𝑐 ‘ 0 ) + 𝑞 ) = ( ( 𝑐 ‘ 0 ) + ( 𝑐 ‘ 1 ) ) )
82 81 oveq1d ⊢ ( 𝑞 = ( 𝑐 ‘ 1 ) → ( ( ( 𝑐 ‘ 0 ) + 𝑞 ) + 𝑟 ) = ( ( ( 𝑐 ‘ 0 ) + ( 𝑐 ‘ 1 ) ) + 𝑟 ) )
83 82 eqeq2d ⊢ ( 𝑞 = ( 𝑐 ‘ 1 ) → ( 𝑛 = ( ( ( 𝑐 ‘ 0 ) + 𝑞 ) + 𝑟 ) ↔ 𝑛 = ( ( ( 𝑐 ‘ 0 ) + ( 𝑐 ‘ 1 ) ) + 𝑟 ) ) )
84 80 83 anbi12d ⊢ ( 𝑞 = ( 𝑐 ‘ 1 ) → ( ( ( ( 𝑐 ‘ 0 ) ∈ 𝑂 ∧ 𝑞 ∈ 𝑂 ∧ 𝑟 ∈ 𝑂 ) ∧ 𝑛 = ( ( ( 𝑐 ‘ 0 ) + 𝑞 ) + 𝑟 ) ) ↔ ( ( ( 𝑐 ‘ 0 ) ∈ 𝑂 ∧ ( 𝑐 ‘ 1 ) ∈ 𝑂 ∧ 𝑟 ∈ 𝑂 ) ∧ 𝑛 = ( ( ( 𝑐 ‘ 0 ) + ( 𝑐 ‘ 1 ) ) + 𝑟 ) ) ) )
85 eleq1 ⊢ ( 𝑟 = ( 𝑐 ‘ 2 ) → ( 𝑟 ∈ 𝑂 ↔ ( 𝑐 ‘ 2 ) ∈ 𝑂 ) )
86 85 3anbi3d ⊢ ( 𝑟 = ( 𝑐 ‘ 2 ) → ( ( ( 𝑐 ‘ 0 ) ∈ 𝑂 ∧ ( 𝑐 ‘ 1 ) ∈ 𝑂 ∧ 𝑟 ∈ 𝑂 ) ↔ ( ( 𝑐 ‘ 0 ) ∈ 𝑂 ∧ ( 𝑐 ‘ 1 ) ∈ 𝑂 ∧ ( 𝑐 ‘ 2 ) ∈ 𝑂 ) ) )
87 oveq2 ⊢ ( 𝑟 = ( 𝑐 ‘ 2 ) → ( ( ( 𝑐 ‘ 0 ) + ( 𝑐 ‘ 1 ) ) + 𝑟 ) = ( ( ( 𝑐 ‘ 0 ) + ( 𝑐 ‘ 1 ) ) + ( 𝑐 ‘ 2 ) ) )
88 87 eqeq2d ⊢ ( 𝑟 = ( 𝑐 ‘ 2 ) → ( 𝑛 = ( ( ( 𝑐 ‘ 0 ) + ( 𝑐 ‘ 1 ) ) + 𝑟 ) ↔ 𝑛 = ( ( ( 𝑐 ‘ 0 ) + ( 𝑐 ‘ 1 ) ) + ( 𝑐 ‘ 2 ) ) ) )
89 86 88 anbi12d ⊢ ( 𝑟 = ( 𝑐 ‘ 2 ) → ( ( ( ( 𝑐 ‘ 0 ) ∈ 𝑂 ∧ ( 𝑐 ‘ 1 ) ∈ 𝑂 ∧ 𝑟 ∈ 𝑂 ) ∧ 𝑛 = ( ( ( 𝑐 ‘ 0 ) + ( 𝑐 ‘ 1 ) ) + 𝑟 ) ) ↔ ( ( ( 𝑐 ‘ 0 ) ∈ 𝑂 ∧ ( 𝑐 ‘ 1 ) ∈ 𝑂 ∧ ( 𝑐 ‘ 2 ) ∈ 𝑂 ) ∧ 𝑛 = ( ( ( 𝑐 ‘ 0 ) + ( 𝑐 ‘ 1 ) ) + ( 𝑐 ‘ 2 ) ) ) ) )
90 78 84 89 rspc3ev ⊢ ( ( ( ( 𝑐 ‘ 0 ) ∈ ℙ ∧ ( 𝑐 ‘ 1 ) ∈ ℙ ∧ ( 𝑐 ‘ 2 ) ∈ ℙ ) ∧ ( ( ( 𝑐 ‘ 0 ) ∈ 𝑂 ∧ ( 𝑐 ‘ 1 ) ∈ 𝑂 ∧ ( 𝑐 ‘ 2 ) ∈ 𝑂 ) ∧ 𝑛 = ( ( ( 𝑐 ‘ 0 ) + ( 𝑐 ‘ 1 ) ) + ( 𝑐 ‘ 2 ) ) ) ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ ( ( 𝑝 ∈ 𝑂 ∧ 𝑞 ∈ 𝑂 ∧ 𝑟 ∈ 𝑂 ) ∧ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
91 30 36 42 72 90 syl31anc ⊢ ( ( ( 𝑛 ∈ 𝑂 ∧ ( 1 0 ↑ 2 7 ) < 𝑛 ) ∧ 𝑐 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑛 ) ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ ( ( 𝑝 ∈ 𝑂 ∧ 𝑞 ∈ 𝑂 ∧ 𝑟 ∈ 𝑂 ) ∧ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
92 91 adantr ⊢ ( ( ( ( 𝑛 ∈ 𝑂 ∧ ( 1 0 ↑ 2 7 ) < 𝑛 ) ∧ 𝑐 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑛 ) ) ∧ ⊤ ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ ( ( 𝑝 ∈ 𝑂 ∧ 𝑞 ∈ 𝑂 ∧ 𝑟 ∈ 𝑂 ) ∧ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
93 8 a1i ⊢ ( ( 𝑛 ∈ 𝑂 ∧ ( 1 0 ↑ 2 7 ) < 𝑛 ) → ( 1 0 ↑ 2 7 ) ∈ ℕ )
94 93 nnred ⊢ ( ( 𝑛 ∈ 𝑂 ∧ ( 1 0 ↑ 2 7 ) < 𝑛 ) → ( 1 0 ↑ 2 7 ) ∈ ℝ )
95 18 zred ⊢ ( 𝑛 ∈ 𝑂 → 𝑛 ∈ ℝ )
96 95 adantr ⊢ ( ( 𝑛 ∈ 𝑂 ∧ ( 1 0 ↑ 2 7 ) < 𝑛 ) → 𝑛 ∈ ℝ )
97 simpr ⊢ ( ( 𝑛 ∈ 𝑂 ∧ ( 1 0 ↑ 2 7 ) < 𝑛 ) → ( 1 0 ↑ 2 7 ) < 𝑛 )
98 94 96 97 ltled ⊢ ( ( 𝑛 ∈ 𝑂 ∧ ( 1 0 ↑ 2 7 ) < 𝑛 ) → ( 1 0 ↑ 2 7 ) ≤ 𝑛 )
99 1 11 98 tgoldbachgtd ⊢ ( ( 𝑛 ∈ 𝑂 ∧ ( 1 0 ↑ 2 7 ) < 𝑛 ) → 0 < ( ♯ ‘ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑛 ) ) )
100 ovex ⊢ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑛 ) ∈ V
101 hashneq0 ⊢ ( ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑛 ) ∈ V → ( 0 < ( ♯ ‘ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑛 ) ) ↔ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑛 ) ≠ ∅ ) )
102 100 101 ax-mp ⊢ ( 0 < ( ♯ ‘ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑛 ) ) ↔ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑛 ) ≠ ∅ )
103 99 102 sylib ⊢ ( ( 𝑛 ∈ 𝑂 ∧ ( 1 0 ↑ 2 7 ) < 𝑛 ) → ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑛 ) ≠ ∅ )
104 103 neneqd ⊢ ( ( 𝑛 ∈ 𝑂 ∧ ( 1 0 ↑ 2 7 ) < 𝑛 ) → ¬ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑛 ) = ∅ )
105 neq0 ⊢ ( ¬ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑛 ) = ∅ ↔ ∃ 𝑐 𝑐 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑛 ) )
106 104 105 sylib ⊢ ( ( 𝑛 ∈ 𝑂 ∧ ( 1 0 ↑ 2 7 ) < 𝑛 ) → ∃ 𝑐 𝑐 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑛 ) )
107 tru ⊢ ⊤
108 106 107 jctil ⊢ ( ( 𝑛 ∈ 𝑂 ∧ ( 1 0 ↑ 2 7 ) < 𝑛 ) → ( ⊤ ∧ ∃ 𝑐 𝑐 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑛 ) ) )
109 19.42v ⊢ ( ∃ 𝑐 ( ⊤ ∧ 𝑐 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑛 ) ) ↔ ( ⊤ ∧ ∃ 𝑐 𝑐 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑛 ) ) )
110 108 109 sylibr ⊢ ( ( 𝑛 ∈ 𝑂 ∧ ( 1 0 ↑ 2 7 ) < 𝑛 ) → ∃ 𝑐 ( ⊤ ∧ 𝑐 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑛 ) ) )
111 exancom ⊢ ( ∃ 𝑐 ( ⊤ ∧ 𝑐 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑛 ) ) ↔ ∃ 𝑐 ( 𝑐 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑛 ) ∧ ⊤ ) )
112 110 111 sylib ⊢ ( ( 𝑛 ∈ 𝑂 ∧ ( 1 0 ↑ 2 7 ) < 𝑛 ) → ∃ 𝑐 ( 𝑐 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑛 ) ∧ ⊤ ) )
113 df-rex ⊢ ( ∃ 𝑐 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑛 ) ⊤ ↔ ∃ 𝑐 ( 𝑐 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑛 ) ∧ ⊤ ) )
114 112 113 sylibr ⊢ ( ( 𝑛 ∈ 𝑂 ∧ ( 1 0 ↑ 2 7 ) < 𝑛 ) → ∃ 𝑐 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑛 ) ⊤ )
115 92 114 r19.29a ⊢ ( ( 𝑛 ∈ 𝑂 ∧ ( 1 0 ↑ 2 7 ) < 𝑛 ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ ( ( 𝑝 ∈ 𝑂 ∧ 𝑞 ∈ 𝑂 ∧ 𝑟 ∈ 𝑂 ) ∧ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
116 2 eleq2i ⊢ ( 𝑛 ∈ 𝐺 ↔ 𝑛 ∈ { 𝑧 ∈ 𝑂 ∣ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ ( ( 𝑝 ∈ 𝑂 ∧ 𝑞 ∈ 𝑂 ∧ 𝑟 ∈ 𝑂 ) ∧ 𝑧 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) } )
117 eqeq1 ⊢ ( 𝑧 = 𝑛 → ( 𝑧 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ↔ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
118 117 anbi2d ⊢ ( 𝑧 = 𝑛 → ( ( ( 𝑝 ∈ 𝑂 ∧ 𝑞 ∈ 𝑂 ∧ 𝑟 ∈ 𝑂 ) ∧ 𝑧 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ↔ ( ( 𝑝 ∈ 𝑂 ∧ 𝑞 ∈ 𝑂 ∧ 𝑟 ∈ 𝑂 ) ∧ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ) )
119 118 rexbidv ⊢ ( 𝑧 = 𝑛 → ( ∃ 𝑟 ∈ ℙ ( ( 𝑝 ∈ 𝑂 ∧ 𝑞 ∈ 𝑂 ∧ 𝑟 ∈ 𝑂 ) ∧ 𝑧 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ↔ ∃ 𝑟 ∈ ℙ ( ( 𝑝 ∈ 𝑂 ∧ 𝑞 ∈ 𝑂 ∧ 𝑟 ∈ 𝑂 ) ∧ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ) )
120 119 rexbidv ⊢ ( 𝑧 = 𝑛 → ( ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ ( ( 𝑝 ∈ 𝑂 ∧ 𝑞 ∈ 𝑂 ∧ 𝑟 ∈ 𝑂 ) ∧ 𝑧 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ↔ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ ( ( 𝑝 ∈ 𝑂 ∧ 𝑞 ∈ 𝑂 ∧ 𝑟 ∈ 𝑂 ) ∧ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ) )
121 120 rexbidv ⊢ ( 𝑧 = 𝑛 → ( ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ ( ( 𝑝 ∈ 𝑂 ∧ 𝑞 ∈ 𝑂 ∧ 𝑟 ∈ 𝑂 ) ∧ 𝑧 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ↔ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ ( ( 𝑝 ∈ 𝑂 ∧ 𝑞 ∈ 𝑂 ∧ 𝑟 ∈ 𝑂 ) ∧ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ) )
122 121 elrab3 ⊢ ( 𝑛 ∈ 𝑂 → ( 𝑛 ∈ { 𝑧 ∈ 𝑂 ∣ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ ( ( 𝑝 ∈ 𝑂 ∧ 𝑞 ∈ 𝑂 ∧ 𝑟 ∈ 𝑂 ) ∧ 𝑧 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) } ↔ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ ( ( 𝑝 ∈ 𝑂 ∧ 𝑞 ∈ 𝑂 ∧ 𝑟 ∈ 𝑂 ) ∧ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ) )
123 116 122 bitrid ⊢ ( 𝑛 ∈ 𝑂 → ( 𝑛 ∈ 𝐺 ↔ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ ( ( 𝑝 ∈ 𝑂 ∧ 𝑞 ∈ 𝑂 ∧ 𝑟 ∈ 𝑂 ) ∧ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ) )
124 123 biimpar ⊢ ( ( 𝑛 ∈ 𝑂 ∧ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ ( ( 𝑝 ∈ 𝑂 ∧ 𝑞 ∈ 𝑂 ∧ 𝑟 ∈ 𝑂 ) ∧ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ) → 𝑛 ∈ 𝐺 )
125 11 115 124 syl2anc ⊢ ( ( 𝑛 ∈ 𝑂 ∧ ( 1 0 ↑ 2 7 ) < 𝑛 ) → 𝑛 ∈ 𝐺 )
126 125 ex ⊢ ( 𝑛 ∈ 𝑂 → ( ( 1 0 ↑ 2 7 ) < 𝑛 → 𝑛 ∈ 𝐺 ) )
127 126 rgen ⊢ ∀ 𝑛 ∈ 𝑂 ( ( 1 0 ↑ 2 7 ) < 𝑛 → 𝑛 ∈ 𝐺 )
128 10 127 pm3.2i ⊢ ( ( 1 0 ↑ 2 7 ) ≤ ( 1 0 ↑ 2 7 ) ∧ ∀ 𝑛 ∈ 𝑂 ( ( 1 0 ↑ 2 7 ) < 𝑛 → 𝑛 ∈ 𝐺 ) )
129 breq1 ⊢ ( 𝑚 = ( 1 0 ↑ 2 7 ) → ( 𝑚 ≤ ( 1 0 ↑ 2 7 ) ↔ ( 1 0 ↑ 2 7 ) ≤ ( 1 0 ↑ 2 7 ) ) )
130 breq1 ⊢ ( 𝑚 = ( 1 0 ↑ 2 7 ) → ( 𝑚 < 𝑛 ↔ ( 1 0 ↑ 2 7 ) < 𝑛 ) )
131 130 imbi1d ⊢ ( 𝑚 = ( 1 0 ↑ 2 7 ) → ( ( 𝑚 < 𝑛 → 𝑛 ∈ 𝐺 ) ↔ ( ( 1 0 ↑ 2 7 ) < 𝑛 → 𝑛 ∈ 𝐺 ) ) )
132 131 ralbidv ⊢ ( 𝑚 = ( 1 0 ↑ 2 7 ) → ( ∀ 𝑛 ∈ 𝑂 ( 𝑚 < 𝑛 → 𝑛 ∈ 𝐺 ) ↔ ∀ 𝑛 ∈ 𝑂 ( ( 1 0 ↑ 2 7 ) < 𝑛 → 𝑛 ∈ 𝐺 ) ) )
133 129 132 anbi12d ⊢ ( 𝑚 = ( 1 0 ↑ 2 7 ) → ( ( 𝑚 ≤ ( 1 0 ↑ 2 7 ) ∧ ∀ 𝑛 ∈ 𝑂 ( 𝑚 < 𝑛 → 𝑛 ∈ 𝐺 ) ) ↔ ( ( 1 0 ↑ 2 7 ) ≤ ( 1 0 ↑ 2 7 ) ∧ ∀ 𝑛 ∈ 𝑂 ( ( 1 0 ↑ 2 7 ) < 𝑛 → 𝑛 ∈ 𝐺 ) ) ) )
134 133 rspcev ⊢ ( ( ( 1 0 ↑ 2 7 ) ∈ ℕ ∧ ( ( 1 0 ↑ 2 7 ) ≤ ( 1 0 ↑ 2 7 ) ∧ ∀ 𝑛 ∈ 𝑂 ( ( 1 0 ↑ 2 7 ) < 𝑛 → 𝑛 ∈ 𝐺 ) ) ) → ∃ 𝑚 ∈ ℕ ( 𝑚 ≤ ( 1 0 ↑ 2 7 ) ∧ ∀ 𝑛 ∈ 𝑂 ( 𝑚 < 𝑛 → 𝑛 ∈ 𝐺 ) ) )
135 8 128 134 mp2an ⊢ ∃ 𝑚 ∈ ℕ ( 𝑚 ≤ ( 1 0 ↑ 2 7 ) ∧ ∀ 𝑛 ∈ 𝑂 ( 𝑚 < 𝑛 → 𝑛 ∈ 𝐺 ) )