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 
|- ( ph -> A e. ( ZZ>= ` 2 ) )
jm2.27a2 
|- ( ph -> B e. NN )
jm2.27a3 
|- ( ph -> C e. NN )
jm2.27a4 
|- ( ph -> D e. NN0 )
jm2.27a5 
|- ( ph -> E e. NN0 )
jm2.27a6 
|- ( ph -> F e. NN0 )
jm2.27a7 
|- ( ph -> G e. NN0 )
jm2.27a8 
|- ( ph -> H e. NN0 )
jm2.27a9 
|- ( ph -> I e. NN0 )
jm2.27a10 
|- ( ph -> J e. NN0 )
jm2.27a11 
|- ( ph -> ( ( D ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 )
jm2.27a12 
|- ( ph -> ( ( F ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( E ^ 2 ) ) ) = 1 )
jm2.27a13 
|- ( ph -> G e. ( ZZ>= ` 2 ) )
jm2.27a14 
|- ( ph -> ( ( I ^ 2 ) - ( ( ( G ^ 2 ) - 1 ) x. ( H ^ 2 ) ) ) = 1 )
jm2.27a15 
|- ( ph -> E = ( ( J + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) )
jm2.27a16 
|- ( ph -> F || ( G - A ) )
jm2.27a17 
|- ( ph -> ( 2 x. C ) || ( G - 1 ) )
jm2.27a18 
|- ( ph -> F || ( H - C ) )
jm2.27a19 
|- ( ph -> ( 2 x. C ) || ( H - B ) )
jm2.27a20 
|- ( ph -> B <_ C )
jm2.27a21 
|- ( ph -> P e. ZZ )
jm2.27a22 
|- ( ph -> D = ( A rmX P ) )
jm2.27a23 
|- ( ph -> C = ( A rmY P ) )
jm2.27a24 
|- ( ph -> Q e. ZZ )
jm2.27a25 
|- ( ph -> F = ( A rmX Q ) )
jm2.27a26 
|- ( ph -> E = ( A rmY Q ) )
jm2.27a27 
|- ( ph -> R e. ZZ )
jm2.27a28 
|- ( ph -> I = ( G rmX R ) )
jm2.27a29 
|- ( ph -> H = ( G rmY R ) )
Assertion jm2.27a 
|- ( ph -> C = ( A rmY B ) )

Proof

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