Metamath Proof Explorer

Theorem mogoldbblem

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

Ref Expression
Assertion mogoldbblem 
|- ( ( ( P e. Prime /\ Q e. Prime /\ R e. Prime ) /\ N e. Even /\ ( N + 2 ) = ( ( P + Q ) + R ) ) -> E. p e. Prime E. q e. Prime N = ( p + q ) )

Proof

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