Theorem 9gbo 42338

Description: 9 is an odd Goldbach number. (Contributed by AV, 26-Jul-2020.)

Assertion

Ref	Expression
9gbo	⊢ 9 ∈ GoldbachOdd

Proof of Theorem 9gbo

Dummy variables 𝑞 𝑝 𝑟 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-9 11342	. . 3 ⊢ 9 = (8 + 1)
2		8even 42298	. . . 4 ⊢ 8 ∈ Even
3		evenp1odd 42229	. . . 4 ⊢ (8 ∈ Even → (8 + 1) ∈ Odd )
4	2, 3	ax-mp 5	. . 3 ⊢ (8 + 1) ∈ Odd
5	1, 4	eqeltri 2840	. 2 ⊢ 9 ∈ Odd
6		3prm 15686	. . 3 ⊢ 3 ∈ ℙ
7		3odd 42293	. . . . . 6 ⊢ 3 ∈ Odd
8	7, 7, 7	3pm3.2i 1438	. . . . 5 ⊢ (3 ∈ Odd ∧ 3 ∈ Odd ∧ 3 ∈ Odd )
9		gbpart9 42333	. . . . 5 ⊢ 9 = ((3 + 3) + 3)
10	8, 9	pm3.2i 462	. . . 4 ⊢ ((3 ∈ Odd ∧ 3 ∈ Odd ∧ 3 ∈ Odd ) ∧ 9 = ((3 + 3) + 3))
11		eleq1 2832	. . . . . . 7 ⊢ (𝑟 = 3 → (𝑟 ∈ Odd ↔ 3 ∈ Odd ))
12	11	3anbi3d 1566	. . . . . 6 ⊢ (𝑟 = 3 → ((3 ∈ Odd ∧ 3 ∈ Odd ∧ 𝑟 ∈ Odd ) ↔ (3 ∈ Odd ∧ 3 ∈ Odd ∧ 3 ∈ Odd )))
13		oveq2 6850	. . . . . . 7 ⊢ (𝑟 = 3 → ((3 + 3) + 𝑟) = ((3 + 3) + 3))
14	13	eqeq2d 2775	. . . . . 6 ⊢ (𝑟 = 3 → (9 = ((3 + 3) + 𝑟) ↔ 9 = ((3 + 3) + 3)))
15	12, 14	anbi12d 624	. . . . 5 ⊢ (𝑟 = 3 → (((3 ∈ Odd ∧ 3 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 9 = ((3 + 3) + 𝑟)) ↔ ((3 ∈ Odd ∧ 3 ∈ Odd ∧ 3 ∈ Odd ) ∧ 9 = ((3 + 3) + 3))))
16	15	rspcev 3461	. . . 4 ⊢ ((3 ∈ ℙ ∧ ((3 ∈ Odd ∧ 3 ∈ Odd ∧ 3 ∈ Odd ) ∧ 9 = ((3 + 3) + 3))) → ∃𝑟 ∈ ℙ ((3 ∈ Odd ∧ 3 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 9 = ((3 + 3) + 𝑟)))
17	6, 10, 16	mp2an 683	. . 3 ⊢ ∃𝑟 ∈ ℙ ((3 ∈ Odd ∧ 3 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 9 = ((3 + 3) + 𝑟))
18		eleq1 2832	. . . . . . 7 ⊢ (𝑝 = 3 → (𝑝 ∈ Odd ↔ 3 ∈ Odd ))
19	18	3anbi1d 1564	. . . . . 6 ⊢ (𝑝 = 3 → ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ↔ (3 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd )))
20		oveq1 6849	. . . . . . . 8 ⊢ (𝑝 = 3 → (𝑝 + 𝑞) = (3 + 𝑞))
21	20	oveq1d 6857	. . . . . . 7 ⊢ (𝑝 = 3 → ((𝑝 + 𝑞) + 𝑟) = ((3 + 𝑞) + 𝑟))
22	21	eqeq2d 2775	. . . . . 6 ⊢ (𝑝 = 3 → (9 = ((𝑝 + 𝑞) + 𝑟) ↔ 9 = ((3 + 𝑞) + 𝑟)))
23	19, 22	anbi12d 624	. . . . 5 ⊢ (𝑝 = 3 → (((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 9 = ((𝑝 + 𝑞) + 𝑟)) ↔ ((3 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 9 = ((3 + 𝑞) + 𝑟))))
24	23	rexbidv 3199	. . . 4 ⊢ (𝑝 = 3 → (∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 9 = ((𝑝 + 𝑞) + 𝑟)) ↔ ∃𝑟 ∈ ℙ ((3 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 9 = ((3 + 𝑞) + 𝑟))))
25		eleq1 2832	. . . . . . 7 ⊢ (𝑞 = 3 → (𝑞 ∈ Odd ↔ 3 ∈ Odd ))
26	25	3anbi2d 1565	. . . . . 6 ⊢ (𝑞 = 3 → ((3 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ↔ (3 ∈ Odd ∧ 3 ∈ Odd ∧ 𝑟 ∈ Odd )))
27		oveq2 6850	. . . . . . . 8 ⊢ (𝑞 = 3 → (3 + 𝑞) = (3 + 3))
28	27	oveq1d 6857	. . . . . . 7 ⊢ (𝑞 = 3 → ((3 + 𝑞) + 𝑟) = ((3 + 3) + 𝑟))
29	28	eqeq2d 2775	. . . . . 6 ⊢ (𝑞 = 3 → (9 = ((3 + 𝑞) + 𝑟) ↔ 9 = ((3 + 3) + 𝑟)))
30	26, 29	anbi12d 624	. . . . 5 ⊢ (𝑞 = 3 → (((3 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 9 = ((3 + 𝑞) + 𝑟)) ↔ ((3 ∈ Odd ∧ 3 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 9 = ((3 + 3) + 𝑟))))
31	30	rexbidv 3199	. . . 4 ⊢ (𝑞 = 3 → (∃𝑟 ∈ ℙ ((3 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 9 = ((3 + 𝑞) + 𝑟)) ↔ ∃𝑟 ∈ ℙ ((3 ∈ Odd ∧ 3 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 9 = ((3 + 3) + 𝑟))))
32	24, 31	rspc2ev 3476	. . 3 ⊢ ((3 ∈ ℙ ∧ 3 ∈ ℙ ∧ ∃𝑟 ∈ ℙ ((3 ∈ Odd ∧ 3 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 9 = ((3 + 3) + 𝑟))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 9 = ((𝑝 + 𝑞) + 𝑟)))
33	6, 6, 17, 32	mp3an 1585	. 2 ⊢ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 9 = ((𝑝 + 𝑞) + 𝑟))
34		isgbo 42317	. 2 ⊢ (9 ∈ GoldbachOdd ↔ (9 ∈ Odd ∧ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 9 = ((𝑝 + 𝑞) + 𝑟))))
35	5, 33, 34	mpbir2an 702	1 ⊢ 9 ∈ GoldbachOdd

Syntax hints:   ∧ wa 384   ∧ w3a 1107   = wceq 1652   ∈ wcel 2155  ∃wrex 3056  (class class class)co 6842  1c1 10190   + caddc 10192  3c3 11328  8c8 11333  9c9 11334  ℙcprime 15665   Even ceven 42213   Odd codd 42214   GoldbachOdd cgbo 42311

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-cnex 10245  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266  ax-pre-sup 10267

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-iun 4678  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-om 7264  df-1st 7366  df-2nd 7367  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-1o 7764  df-2o 7765  df-er 7947  df-en 8161  df-dom 8162  df-sdom 8163  df-fin 8164  df-sup 8555  df-inf 8556  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523  df-div 10939  df-nn 11275  df-2 11335  df-3 11336  df-4 11337  df-5 11338  df-6 11339  df-7 11340  df-8 11341  df-9 11342  df-n0 11539  df-z 11625  df-uz 11887  df-rp 12029  df-fz 12534  df-seq 13009  df-exp 13068  df-cj 14124  df-re 14125  df-im 14126  df-sqrt 14260  df-abs 14261  df-dvds 15266  df-prm 15666  df-even 42215  df-odd 42216  df-gbo 42314

This theorem is referenced by:  bgoldbtbndlem1  42369