Metamath Proof Explorer

Theorem mogoldbblem

Description: Lemma for mogoldbb . (Contributed by AV, 26-Dec-2021)

Ref Expression
Assertion mogoldbblem ⊢P∈ℙ∧Q∈ℙ∧R∈ℙ∧N∈Even∧N+2=P+Q+R→∃p∈ℙ∃q∈ℙN=p+q

Proof

Step Hyp Ref Expression
1 2evenALTV ⊢2∈Even
2 epee ⊢N∈Even∧2∈Even→N+2∈Even
3 1 2 mpan2 ⊢N∈Even→N+2∈Even
4 3 3ad2ant2 ⊢P∈ℙ∧Q∈ℙ∧R∈ℙ∧N∈Even∧N+2=P+Q+R→N+2∈Even
5 simp1 ⊢P∈ℙ∧Q∈ℙ∧R∈ℙ∧N∈Even∧N+2=P+Q+R→P∈ℙ∧Q∈ℙ∧R∈ℙ
6 simp3 ⊢P∈ℙ∧Q∈ℙ∧R∈ℙ∧N∈Even∧N+2=P+Q+R→N+2=P+Q+R
7 even3prm2 ⊢N+2∈Even∧P∈ℙ∧Q∈ℙ∧R∈ℙ∧N+2=P+Q+R→P=2∨Q=2∨R=2
8 4 5 6 7 syl3anc ⊢P∈ℙ∧Q∈ℙ∧R∈ℙ∧N∈Even∧N+2=P+Q+R→P=2∨Q=2∨R=2
9 oveq1 ⊢P=2→P+Q=2+Q
10 9 oveq1d ⊢P=2→P+Q+R=2+Q+R
11 10 eqeq2d ⊢P=2→N+2=P+Q+R↔N+2=2+Q+R
12 2cnd ⊢Q∈ℙ∧R∈ℙ→2∈ℂ
13 prmz ⊢Q∈ℙ→Q∈ℤ
14 13 zcnd ⊢Q∈ℙ→Q∈ℂ
15 14 adantr ⊢Q∈ℙ∧R∈ℙ→Q∈ℂ
16 prmz ⊢R∈ℙ→R∈ℤ
17 16 zcnd ⊢R∈ℙ→R∈ℂ
18 17 adantl ⊢Q∈ℙ∧R∈ℙ→R∈ℂ
19 simp1 ⊢2∈ℂ∧Q∈ℂ∧R∈ℂ→2∈ℂ
20 addcl ⊢Q∈ℂ∧R∈ℂ→Q+R∈ℂ
21 20 3adant1 ⊢2∈ℂ∧Q∈ℂ∧R∈ℂ→Q+R∈ℂ
22 addass ⊢2∈ℂ∧Q∈ℂ∧R∈ℂ→2+Q+R=2+Q+R
23 19 21 22 comraddd ⊢2∈ℂ∧Q∈ℂ∧R∈ℂ→2+Q+R=Q+R+2
24 12 15 18 23 syl3anc ⊢Q∈ℙ∧R∈ℙ→2+Q+R=Q+R+2
25 24 eqeq2d ⊢Q∈ℙ∧R∈ℙ→N+2=2+Q+R↔N+2=Q+R+2
26 25 adantr ⊢Q∈ℙ∧R∈ℙ∧N∈Even→N+2=2+Q+R↔N+2=Q+R+2
27 evenz ⊢N∈Even→N∈ℤ
28 27 zcnd ⊢N∈Even→N∈ℂ
29 28 adantl ⊢Q∈ℙ∧R∈ℙ∧N∈Even→N∈ℂ
30 zaddcl ⊢Q∈ℤ∧R∈ℤ→Q+R∈ℤ
31 13 16 30 syl2an ⊢Q∈ℙ∧R∈ℙ→Q+R∈ℤ
32 31 zcnd ⊢Q∈ℙ∧R∈ℙ→Q+R∈ℂ
33 32 adantr ⊢Q∈ℙ∧R∈ℙ∧N∈Even→Q+R∈ℂ
34 2cnd ⊢Q∈ℙ∧R∈ℙ∧N∈Even→2∈ℂ
35 29 33 34 addcan2d ⊢Q∈ℙ∧R∈ℙ∧N∈Even→N+2=Q+R+2↔N=Q+R
36 26 35 bitrd ⊢Q∈ℙ∧R∈ℙ∧N∈Even→N+2=2+Q+R↔N=Q+R
37 simpll ⊢Q∈ℙ∧R∈ℙ∧N=Q+R→Q∈ℙ
38 oveq1 ⊢p=Q→p+q=Q+q
39 38 eqeq2d ⊢p=Q→N=p+q↔N=Q+q
40 39 rexbidv ⊢p=Q→∃q∈ℙN=p+q↔∃q∈ℙN=Q+q
41 40 adantl ⊢Q∈ℙ∧R∈ℙ∧N=Q+R∧p=Q→∃q∈ℙN=p+q↔∃q∈ℙN=Q+q
42 simplr ⊢Q∈ℙ∧R∈ℙ∧N=Q+R→R∈ℙ
43 simpr ⊢Q∈ℙ∧R∈ℙ∧N=Q+R→N=Q+R
44 oveq2 ⊢q=R→Q+q=Q+R
45 44 eqcomd ⊢q=R→Q+R=Q+q
46 43 45 sylan9eq ⊢Q∈ℙ∧R∈ℙ∧N=Q+R∧q=R→N=Q+q
47 42 46 rspcedeq2vd ⊢Q∈ℙ∧R∈ℙ∧N=Q+R→∃q∈ℙN=Q+q
48 37 41 47 rspcedvd ⊢Q∈ℙ∧R∈ℙ∧N=Q+R→∃p∈ℙ∃q∈ℙN=p+q
49 48 ex ⊢Q∈ℙ∧R∈ℙ→N=Q+R→∃p∈ℙ∃q∈ℙN=p+q
50 49 adantr ⊢Q∈ℙ∧R∈ℙ∧N∈Even→N=Q+R→∃p∈ℙ∃q∈ℙN=p+q
51 36 50 sylbid ⊢Q∈ℙ∧R∈ℙ∧N∈Even→N+2=2+Q+R→∃p∈ℙ∃q∈ℙN=p+q
52 51 com12 ⊢N+2=2+Q+R→Q∈ℙ∧R∈ℙ∧N∈Even→∃p∈ℙ∃q∈ℙN=p+q
53 11 52 syl6bi ⊢P=2→N+2=P+Q+R→Q∈ℙ∧R∈ℙ∧N∈Even→∃p∈ℙ∃q∈ℙN=p+q
54 53 com13 ⊢Q∈ℙ∧R∈ℙ∧N∈Even→N+2=P+Q+R→P=2→∃p∈ℙ∃q∈ℙN=p+q
55 54 ex ⊢Q∈ℙ∧R∈ℙ→N∈Even→N+2=P+Q+R→P=2→∃p∈ℙ∃q∈ℙN=p+q
56 55 3adant1 ⊢P∈ℙ∧Q∈ℙ∧R∈ℙ→N∈Even→N+2=P+Q+R→P=2→∃p∈ℙ∃q∈ℙN=p+q
57 56 3imp ⊢P∈ℙ∧Q∈ℙ∧R∈ℙ∧N∈Even∧N+2=P+Q+R→P=2→∃p∈ℙ∃q∈ℙN=p+q
58 57 com12 ⊢P=2→P∈ℙ∧Q∈ℙ∧R∈ℙ∧N∈Even∧N+2=P+Q+R→∃p∈ℙ∃q∈ℙN=p+q
59 oveq2 ⊢Q=2→P+Q=P+2
60 59 oveq1d ⊢Q=2→P+Q+R=P+2+R
61 60 eqeq2d ⊢Q=2→N+2=P+Q+R↔N+2=P+2+R
62 prmz ⊢P∈ℙ→P∈ℤ
63 62 zcnd ⊢P∈ℙ→P∈ℂ
64 63 adantr ⊢P∈ℙ∧R∈ℙ→P∈ℂ
65 2cnd ⊢P∈ℙ∧R∈ℙ→2∈ℂ
66 17 adantl ⊢P∈ℙ∧R∈ℙ→R∈ℂ
67 64 65 66 3jca ⊢P∈ℙ∧R∈ℙ→P∈ℂ∧2∈ℂ∧R∈ℂ
68 67 adantr ⊢P∈ℙ∧R∈ℙ∧N∈Even→P∈ℂ∧2∈ℂ∧R∈ℂ
69 add32 ⊢P∈ℂ∧2∈ℂ∧R∈ℂ→P+2+R=P+R+2
70 68 69 syl ⊢P∈ℙ∧R∈ℙ∧N∈Even→P+2+R=P+R+2
71 70 eqeq2d ⊢P∈ℙ∧R∈ℙ∧N∈Even→N+2=P+2+R↔N+2=P+R+2
72 28 adantl ⊢P∈ℙ∧R∈ℙ∧N∈Even→N∈ℂ
73 zaddcl ⊢P∈ℤ∧R∈ℤ→P+R∈ℤ
74 62 16 73 syl2an ⊢P∈ℙ∧R∈ℙ→P+R∈ℤ
75 74 zcnd ⊢P∈ℙ∧R∈ℙ→P+R∈ℂ
76 75 adantr ⊢P∈ℙ∧R∈ℙ∧N∈Even→P+R∈ℂ
77 2cnd ⊢P∈ℙ∧R∈ℙ∧N∈Even→2∈ℂ
78 72 76 77 addcan2d ⊢P∈ℙ∧R∈ℙ∧N∈Even→N+2=P+R+2↔N=P+R
79 71 78 bitrd ⊢P∈ℙ∧R∈ℙ∧N∈Even→N+2=P+2+R↔N=P+R
80 simpll ⊢P∈ℙ∧R∈ℙ∧N=P+R→P∈ℙ
81 oveq1 ⊢p=P→p+q=P+q
82 81 eqeq2d ⊢p=P→N=p+q↔N=P+q
83 82 rexbidv ⊢p=P→∃q∈ℙN=p+q↔∃q∈ℙN=P+q
84 83 adantl ⊢P∈ℙ∧R∈ℙ∧N=P+R∧p=P→∃q∈ℙN=p+q↔∃q∈ℙN=P+q
85 simplr ⊢P∈ℙ∧R∈ℙ∧N=P+R→R∈ℙ
86 simpr ⊢P∈ℙ∧R∈ℙ∧N=P+R→N=P+R
87 oveq2 ⊢q=R→P+q=P+R
88 87 eqcomd ⊢q=R→P+R=P+q
89 86 88 sylan9eq ⊢P∈ℙ∧R∈ℙ∧N=P+R∧q=R→N=P+q
90 85 89 rspcedeq2vd ⊢P∈ℙ∧R∈ℙ∧N=P+R→∃q∈ℙN=P+q
91 80 84 90 rspcedvd ⊢P∈ℙ∧R∈ℙ∧N=P+R→∃p∈ℙ∃q∈ℙN=p+q
92 91 ex ⊢P∈ℙ∧R∈ℙ→N=P+R→∃p∈ℙ∃q∈ℙN=p+q
93 92 adantr ⊢P∈ℙ∧R∈ℙ∧N∈Even→N=P+R→∃p∈ℙ∃q∈ℙN=p+q
94 79 93 sylbid ⊢P∈ℙ∧R∈ℙ∧N∈Even→N+2=P+2+R→∃p∈ℙ∃q∈ℙN=p+q
95 94 com12 ⊢N+2=P+2+R→P∈ℙ∧R∈ℙ∧N∈Even→∃p∈ℙ∃q∈ℙN=p+q
96 61 95 syl6bi ⊢Q=2→N+2=P+Q+R→P∈ℙ∧R∈ℙ∧N∈Even→∃p∈ℙ∃q∈ℙN=p+q
97 96 com13 ⊢P∈ℙ∧R∈ℙ∧N∈Even→N+2=P+Q+R→Q=2→∃p∈ℙ∃q∈ℙN=p+q
98 97 ex ⊢P∈ℙ∧R∈ℙ→N∈Even→N+2=P+Q+R→Q=2→∃p∈ℙ∃q∈ℙN=p+q
99 98 3adant2 ⊢P∈ℙ∧Q∈ℙ∧R∈ℙ→N∈Even→N+2=P+Q+R→Q=2→∃p∈ℙ∃q∈ℙN=p+q
100 99 3imp ⊢P∈ℙ∧Q∈ℙ∧R∈ℙ∧N∈Even∧N+2=P+Q+R→Q=2→∃p∈ℙ∃q∈ℙN=p+q
101 100 com12 ⊢Q=2→P∈ℙ∧Q∈ℙ∧R∈ℙ∧N∈Even∧N+2=P+Q+R→∃p∈ℙ∃q∈ℙN=p+q
102 oveq2 ⊢R=2→P+Q+R=P+Q+2
103 102 eqeq2d ⊢R=2→N+2=P+Q+R↔N+2=P+Q+2
104 28 adantl ⊢P∈ℙ∧Q∈ℙ∧N∈Even→N∈ℂ
105 zaddcl ⊢P∈ℤ∧Q∈ℤ→P+Q∈ℤ
106 62 13 105 syl2an ⊢P∈ℙ∧Q∈ℙ→P+Q∈ℤ
107 106 zcnd ⊢P∈ℙ∧Q∈ℙ→P+Q∈ℂ
108 107 adantr ⊢P∈ℙ∧Q∈ℙ∧N∈Even→P+Q∈ℂ
109 2cnd ⊢P∈ℙ∧Q∈ℙ∧N∈Even→2∈ℂ
110 104 108 109 addcan2d ⊢P∈ℙ∧Q∈ℙ∧N∈Even→N+2=P+Q+2↔N=P+Q
111 simpll ⊢P∈ℙ∧Q∈ℙ∧N=P+Q→P∈ℙ
112 83 adantl ⊢P∈ℙ∧Q∈ℙ∧N=P+Q∧p=P→∃q∈ℙN=p+q↔∃q∈ℙN=P+q
113 simplr ⊢P∈ℙ∧Q∈ℙ∧N=P+Q→Q∈ℙ
114 simpr ⊢P∈ℙ∧Q∈ℙ∧N=P+Q→N=P+Q
115 oveq2 ⊢q=Q→P+q=P+Q
116 115 eqcomd ⊢q=Q→P+Q=P+q
117 114 116 sylan9eq ⊢P∈ℙ∧Q∈ℙ∧N=P+Q∧q=Q→N=P+q
118 113 117 rspcedeq2vd ⊢P∈ℙ∧Q∈ℙ∧N=P+Q→∃q∈ℙN=P+q
119 111 112 118 rspcedvd ⊢P∈ℙ∧Q∈ℙ∧N=P+Q→∃p∈ℙ∃q∈ℙN=p+q
120 119 ex ⊢P∈ℙ∧Q∈ℙ→N=P+Q→∃p∈ℙ∃q∈ℙN=p+q
121 120 adantr ⊢P∈ℙ∧Q∈ℙ∧N∈Even→N=P+Q→∃p∈ℙ∃q∈ℙN=p+q
122 110 121 sylbid ⊢P∈ℙ∧Q∈ℙ∧N∈Even→N+2=P+Q+2→∃p∈ℙ∃q∈ℙN=p+q
123 122 com12 ⊢N+2=P+Q+2→P∈ℙ∧Q∈ℙ∧N∈Even→∃p∈ℙ∃q∈ℙN=p+q
124 103 123 syl6bi ⊢R=2→N+2=P+Q+R→P∈ℙ∧Q∈ℙ∧N∈Even→∃p∈ℙ∃q∈ℙN=p+q
125 124 com13 ⊢P∈ℙ∧Q∈ℙ∧N∈Even→N+2=P+Q+R→R=2→∃p∈ℙ∃q∈ℙN=p+q
126 125 ex ⊢P∈ℙ∧Q∈ℙ→N∈Even→N+2=P+Q+R→R=2→∃p∈ℙ∃q∈ℙN=p+q
127 126 3adant3 ⊢P∈ℙ∧Q∈ℙ∧R∈ℙ→N∈Even→N+2=P+Q+R→R=2→∃p∈ℙ∃q∈ℙN=p+q
128 127 3imp ⊢P∈ℙ∧Q∈ℙ∧R∈ℙ∧N∈Even∧N+2=P+Q+R→R=2→∃p∈ℙ∃q∈ℙN=p+q
129 128 com12 ⊢R=2→P∈ℙ∧Q∈ℙ∧R∈ℙ∧N∈Even∧N+2=P+Q+R→∃p∈ℙ∃q∈ℙN=p+q
130 58 101 129 3jaoi ⊢P=2∨Q=2∨R=2→P∈ℙ∧Q∈ℙ∧R∈ℙ∧N∈Even∧N+2=P+Q+R→∃p∈ℙ∃q∈ℙN=p+q
131 8 130 mpcom ⊢P∈ℙ∧Q∈ℙ∧R∈ℙ∧N∈Even∧N+2=P+Q+R→∃p∈ℙ∃q∈ℙN=p+q