Metamath Proof Explorer


Theorem jm2.27a

Description: Lemma for jm2.27 . Reverse direction after existential quantifiers are expanded. (Contributed by Stefan O'Rear, 4-Oct-2014)

Ref Expression
Hypotheses jm2.27a1 φ A 2
jm2.27a2 φ B
jm2.27a3 φ C
jm2.27a4 φ D 0
jm2.27a5 φ E 0
jm2.27a6 φ F 0
jm2.27a7 φ G 0
jm2.27a8 φ H 0
jm2.27a9 φ I 0
jm2.27a10 φ J 0
jm2.27a11 φ D 2 A 2 1 C 2 = 1
jm2.27a12 φ F 2 A 2 1 E 2 = 1
jm2.27a13 φ G 2
jm2.27a14 φ I 2 G 2 1 H 2 = 1
jm2.27a15 φ E = J + 1 2 C 2
jm2.27a16 φ F G A
jm2.27a17 φ 2 C G 1
jm2.27a18 φ F H C
jm2.27a19 φ 2 C H B
jm2.27a20 φ B C
jm2.27a21 φ P
jm2.27a22 φ D = A X rm P
jm2.27a23 φ C = A Y rm P
jm2.27a24 φ Q
jm2.27a25 φ F = A X rm Q
jm2.27a26 φ E = A Y rm Q
jm2.27a27 φ R
jm2.27a28 φ I = G X rm R
jm2.27a29 φ H = G Y rm R
Assertion jm2.27a φ C = A Y rm B

Proof

Step Hyp Ref Expression
1 jm2.27a1 φ A 2
2 jm2.27a2 φ B
3 jm2.27a3 φ C
4 jm2.27a4 φ D 0
5 jm2.27a5 φ E 0
6 jm2.27a6 φ F 0
7 jm2.27a7 φ G 0
8 jm2.27a8 φ H 0
9 jm2.27a9 φ I 0
10 jm2.27a10 φ J 0
11 jm2.27a11 φ D 2 A 2 1 C 2 = 1
12 jm2.27a12 φ F 2 A 2 1 E 2 = 1
13 jm2.27a13 φ G 2
14 jm2.27a14 φ I 2 G 2 1 H 2 = 1
15 jm2.27a15 φ E = J + 1 2 C 2
16 jm2.27a16 φ F G A
17 jm2.27a17 φ 2 C G 1
18 jm2.27a18 φ F H C
19 jm2.27a19 φ 2 C H B
20 jm2.27a20 φ B C
21 jm2.27a21 φ P
22 jm2.27a22 φ D = A X rm P
23 jm2.27a23 φ C = A Y rm P
24 jm2.27a24 φ Q
25 jm2.27a25 φ F = A X rm Q
26 jm2.27a26 φ E = A Y rm Q
27 jm2.27a27 φ R
28 jm2.27a28 φ I = G X rm R
29 jm2.27a29 φ H = G Y rm R
30 2z 2
31 3 nnzd φ C
32 zmulcl 2 C 2 C
33 30 31 32 sylancr φ 2 C
34 2 nnzd φ B
35 8 nn0zd φ H
36 congsym 2 C H B 2 C H B 2 C B H
37 33 35 34 19 36 syl22anc φ 2 C B H
38 7 nn0zd φ G
39 peano2zm G G 1
40 38 39 syl φ G 1
41 35 27 zsubcld φ H R
42 8 nn0ge0d φ 0 H
43 rmy0 G 2 G Y rm 0 = 0
44 13 43 syl φ G Y rm 0 = 0
45 29 eqcomd φ G Y rm R = H
46 42 44 45 3brtr4d φ G Y rm 0 G Y rm R
47 0zd φ 0
48 lermy G 2 0 R 0 R G Y rm 0 G Y rm R
49 13 47 27 48 syl3anc φ 0 R G Y rm 0 G Y rm R
50 46 49 mpbird φ 0 R
51 elnn0z R 0 R 0 R
52 27 50 51 sylanbrc φ R 0
53 jm2.16nn0 G 2 R 0 G 1 G Y rm R R
54 13 52 53 syl2anc φ G 1 G Y rm R R
55 29 oveq1d φ H R = G Y rm R R
56 54 55 breqtrrd φ G 1 H R
57 33 40 41 17 56 dvdstrd φ 2 C H R
58 congtr 2 C B H R 2 C B H 2 C H R 2 C B R
59 33 34 35 27 37 57 58 syl222anc φ 2 C B R
60 59 orcd φ 2 C B R 2 C B R
61 zmulcl 2 Q 2 Q
62 30 24 61 sylancr φ 2 Q
63 zsqcl C C 2
64 31 63 syl φ C 2
65 dvdsmul2 2 C 2 C 2 2 C 2
66 30 64 65 sylancr φ C 2 2 C 2
67 10 nn0zd φ J
68 67 peano2zd φ J + 1
69 zmulcl 2 C 2 2 C 2
70 30 64 69 sylancr φ 2 C 2
71 dvdsmultr2 C 2 J + 1 2 C 2 C 2 2 C 2 C 2 J + 1 2 C 2
72 64 68 70 71 syl3anc φ C 2 2 C 2 C 2 J + 1 2 C 2
73 66 72 mpd φ C 2 J + 1 2 C 2
74 23 oveq1d φ C 2 = A Y rm P 2
75 15 26 eqtr3d φ J + 1 2 C 2 = A Y rm Q
76 73 74 75 3brtr3d φ A Y rm P 2 A Y rm Q
77 68 zred φ J + 1
78 70 zred φ 2 C 2
79 nn0p1nn J 0 J + 1
80 10 79 syl φ J + 1
81 80 nngt0d φ 0 < J + 1
82 2nn 2
83 3 nnsqcld φ C 2
84 nnmulcl 2 C 2 2 C 2
85 82 83 84 sylancr φ 2 C 2
86 85 nngt0d φ 0 < 2 C 2
87 77 78 81 86 mulgt0d φ 0 < J + 1 2 C 2
88 87 15 breqtrrd φ 0 < E
89 rmy0 A 2 A Y rm 0 = 0
90 1 89 syl φ A Y rm 0 = 0
91 26 eqcomd φ A Y rm Q = E
92 88 90 91 3brtr4d φ A Y rm 0 < A Y rm Q
93 ltrmy A 2 0 Q 0 < Q A Y rm 0 < A Y rm Q
94 1 47 24 93 syl3anc φ 0 < Q A Y rm 0 < A Y rm Q
95 92 94 mpbird φ 0 < Q
96 elnnz Q Q 0 < Q
97 24 95 96 sylanbrc φ Q
98 3 nngt0d φ 0 < C
99 23 eqcomd φ A Y rm P = C
100 98 90 99 3brtr4d φ A Y rm 0 < A Y rm P
101 ltrmy A 2 0 P 0 < P A Y rm 0 < A Y rm P
102 1 47 21 101 syl3anc φ 0 < P A Y rm 0 < A Y rm P
103 100 102 mpbird φ 0 < P
104 elnnz P P 0 < P
105 21 103 104 sylanbrc φ P
106 jm2.20nn A 2 Q P A Y rm P 2 A Y rm Q P A Y rm P Q
107 1 97 105 106 syl3anc φ A Y rm P 2 A Y rm Q P A Y rm P Q
108 76 107 mpbid φ P A Y rm P Q
109 23 31 eqeltrrd φ A Y rm P
110 muldvds2 P A Y rm P Q P A Y rm P Q A Y rm P Q
111 21 109 24 110 syl3anc φ P A Y rm P Q A Y rm P Q
112 108 111 mpd φ A Y rm P Q
113 23 112 eqbrtrd φ C Q
114 30 a1i φ 2
115 dvdscmul C Q 2 C Q 2 C 2 Q
116 31 24 114 115 syl3anc φ C Q 2 C 2 Q
117 113 116 mpd φ 2 C 2 Q
118 6 nn0zd φ F
119 25 118 eqeltrrd φ A X rm Q
120 frmy Y rm : 2 ×
121 120 fovcl A 2 R A Y rm R
122 1 27 121 syl2anc φ A Y rm R
123 29 35 eqeltrrd φ G Y rm R
124 eluzelz A 2 A
125 1 124 syl φ A
126 125 38 zsubcld φ A G
127 122 123 zsubcld φ A Y rm R G Y rm R
128 congsym F G A F G A F A G
129 118 38 125 16 128 syl22anc φ F A G
130 25 129 eqbrtrrd φ A X rm Q A G
131 jm2.15nn0 A 2 G 2 R 0 A G A Y rm R G Y rm R
132 1 13 52 131 syl3anc φ A G A Y rm R G Y rm R
133 119 126 127 130 132 dvdstrd φ A X rm Q A Y rm R G Y rm R
134 29 23 oveq12d φ H C = G Y rm R A Y rm P
135 18 25 134 3brtr3d φ A X rm Q G Y rm R A Y rm P
136 congtr A X rm Q A Y rm R G Y rm R A Y rm P A X rm Q A Y rm R G Y rm R A X rm Q G Y rm R A Y rm P A X rm Q A Y rm R A Y rm P
137 119 122 123 109 133 135 136 syl222anc φ A X rm Q A Y rm R A Y rm P
138 137 orcd φ A X rm Q A Y rm R A Y rm P A X rm Q A Y rm R A Y rm P
139 jm2.26 A 2 Q R P A X rm Q A Y rm R A Y rm P A X rm Q A Y rm R A Y rm P 2 Q R P 2 Q R P
140 1 97 27 21 139 syl22anc φ A X rm Q A Y rm R A Y rm P A X rm Q A Y rm R A Y rm P 2 Q R P 2 Q R P
141 138 140 mpbid φ 2 Q R P 2 Q R P
142 dvdsacongtr 2 Q R P 2 C 2 C 2 Q 2 Q R P 2 Q R P 2 C R P 2 C R P
143 62 27 21 33 117 141 142 syl222anc φ 2 C R P 2 C R P
144 acongtr 2 C B R P 2 C B R 2 C B R 2 C R P 2 C R P 2 C B P 2 C B P
145 33 34 27 21 60 143 144 syl222anc φ 2 C B P 2 C B P
146 2 nnnn0d φ B 0
147 3 nnnn0d φ C 0
148 elfz2nn0 B 0 C B 0 C 0 B C
149 146 147 20 148 syl3anbrc φ B 0 C
150 105 nnnn0d φ P 0
151 rmygeid A 2 P 0 P A Y rm P
152 1 150 151 syl2anc φ P A Y rm P
153 152 23 breqtrrd φ P C
154 elfz2nn0 P 0 C P 0 C 0 P C
155 150 147 153 154 syl3anbrc φ P 0 C
156 acongeq C B 0 C P 0 C B = P 2 C B P 2 C B P
157 3 149 155 156 syl3anc φ B = P 2 C B P 2 C B P
158 145 157 mpbird φ B = P
159 158 oveq2d φ A Y rm B = A Y rm P
160 23 159 eqtr4d φ C = A Y rm B