Metamath Proof Explorer

Theorem bezoutlem3

Description: Lemma for bezout . (Contributed by Mario Carneiro, 22-Feb-2014) ( Revised by AV, 30-Sep-2020.)

Ref Expression
Hypotheses bezout.1 
|- M = { z e. NN | E. x e. ZZ E. y e. ZZ z = ( ( A x. x ) + ( B x. y ) ) }
bezout.3 
|- ( ph -> A e. ZZ )
bezout.4 
|- ( ph -> B e. ZZ )
bezout.2 
|- G = inf ( M , RR , < )
bezout.5 
|- ( ph -> -. ( A = 0 /\ B = 0 ) )
Assertion bezoutlem3 
|- ( ph -> ( C e. M -> G || C ) )

Proof

Step Hyp Ref Expression
1 bezout.1 
 |-  M = { z e. NN | E. x e. ZZ E. y e. ZZ z = ( ( A x. x ) + ( B x. y ) ) }
2 bezout.3 
 |-  ( ph -> A e. ZZ )
3 bezout.4 
 |-  ( ph -> B e. ZZ )
4 bezout.2 
 |-  G = inf ( M , RR , < )
5 bezout.5 
 |-  ( ph -> -. ( A = 0 /\ B = 0 ) )
6 simpr 
 |-  ( ( ph /\ C e. M ) -> C e. M )
7 eqeq1 
 |-  ( z = C -> ( z = ( ( A x. x ) + ( B x. y ) ) <-> C = ( ( A x. x ) + ( B x. y ) ) ) )
8 7 2rexbidv 
 |-  ( z = C -> ( E. x e. ZZ E. y e. ZZ z = ( ( A x. x ) + ( B x. y ) ) <-> E. x e. ZZ E. y e. ZZ C = ( ( A x. x ) + ( B x. y ) ) ) )
9 oveq2 
 |-  ( x = s -> ( A x. x ) = ( A x. s ) )
10 9 oveq1d 
 |-  ( x = s -> ( ( A x. x ) + ( B x. y ) ) = ( ( A x. s ) + ( B x. y ) ) )
11 10 eqeq2d 
 |-  ( x = s -> ( C = ( ( A x. x ) + ( B x. y ) ) <-> C = ( ( A x. s ) + ( B x. y ) ) ) )
12 oveq2 
 |-  ( y = t -> ( B x. y ) = ( B x. t ) )
13 12 oveq2d 
 |-  ( y = t -> ( ( A x. s ) + ( B x. y ) ) = ( ( A x. s ) + ( B x. t ) ) )
14 13 eqeq2d 
 |-  ( y = t -> ( C = ( ( A x. s ) + ( B x. y ) ) <-> C = ( ( A x. s ) + ( B x. t ) ) ) )
15 11 14 cbvrex2vw 
 |-  ( E. x e. ZZ E. y e. ZZ C = ( ( A x. x ) + ( B x. y ) ) <-> E. s e. ZZ E. t e. ZZ C = ( ( A x. s ) + ( B x. t ) ) )
16 8 15 bitrdi 
 |-  ( z = C -> ( E. x e. ZZ E. y e. ZZ z = ( ( A x. x ) + ( B x. y ) ) <-> E. s e. ZZ E. t e. ZZ C = ( ( A x. s ) + ( B x. t ) ) ) )
17 16 1 elrab2 
 |-  ( C e. M <-> ( C e. NN /\ E. s e. ZZ E. t e. ZZ C = ( ( A x. s ) + ( B x. t ) ) ) )
18 6 17 sylib 
 |-  ( ( ph /\ C e. M ) -> ( C e. NN /\ E. s e. ZZ E. t e. ZZ C = ( ( A x. s ) + ( B x. t ) ) ) )
19 18 simpld 
 |-  ( ( ph /\ C e. M ) -> C e. NN )
20 19 nnred 
 |-  ( ( ph /\ C e. M ) -> C e. RR )
21 1 2 3 4 5 bezoutlem2 
 |-  ( ph -> G e. M )
22 oveq2 
 |-  ( x = u -> ( A x. x ) = ( A x. u ) )
23 22 oveq1d 
 |-  ( x = u -> ( ( A x. x ) + ( B x. y ) ) = ( ( A x. u ) + ( B x. y ) ) )
24 23 eqeq2d 
 |-  ( x = u -> ( z = ( ( A x. x ) + ( B x. y ) ) <-> z = ( ( A x. u ) + ( B x. y ) ) ) )
25 oveq2 
 |-  ( y = v -> ( B x. y ) = ( B x. v ) )
26 25 oveq2d 
 |-  ( y = v -> ( ( A x. u ) + ( B x. y ) ) = ( ( A x. u ) + ( B x. v ) ) )
27 26 eqeq2d 
 |-  ( y = v -> ( z = ( ( A x. u ) + ( B x. y ) ) <-> z = ( ( A x. u ) + ( B x. v ) ) ) )
28 24 27 cbvrex2vw 
 |-  ( E. x e. ZZ E. y e. ZZ z = ( ( A x. x ) + ( B x. y ) ) <-> E. u e. ZZ E. v e. ZZ z = ( ( A x. u ) + ( B x. v ) ) )
29 eqeq1 
 |-  ( z = G -> ( z = ( ( A x. u ) + ( B x. v ) ) <-> G = ( ( A x. u ) + ( B x. v ) ) ) )
30 29 2rexbidv 
 |-  ( z = G -> ( E. u e. ZZ E. v e. ZZ z = ( ( A x. u ) + ( B x. v ) ) <-> E. u e. ZZ E. v e. ZZ G = ( ( A x. u ) + ( B x. v ) ) ) )
31 28 30 syl5bb 
 |-  ( z = G -> ( E. x e. ZZ E. y e. ZZ z = ( ( A x. x ) + ( B x. y ) ) <-> E. u e. ZZ E. v e. ZZ G = ( ( A x. u ) + ( B x. v ) ) ) )
32 31 1 elrab2 
 |-  ( G e. M <-> ( G e. NN /\ E. u e. ZZ E. v e. ZZ G = ( ( A x. u ) + ( B x. v ) ) ) )
33 21 32 sylib 
 |-  ( ph -> ( G e. NN /\ E. u e. ZZ E. v e. ZZ G = ( ( A x. u ) + ( B x. v ) ) ) )
34 33 simpld 
 |-  ( ph -> G e. NN )
35 34 nnrpd 
 |-  ( ph -> G e. RR+ )
36 35 adantr 
 |-  ( ( ph /\ C e. M ) -> G e. RR+ )
37 modlt 
 |-  ( ( C e. RR /\ G e. RR+ ) -> ( C mod G ) < G )
38 20 36 37 syl2anc 
 |-  ( ( ph /\ C e. M ) -> ( C mod G ) < G )
39 19 nnzd 
 |-  ( ( ph /\ C e. M ) -> C e. ZZ )
40 34 adantr 
 |-  ( ( ph /\ C e. M ) -> G e. NN )
41 39 40 zmodcld 
 |-  ( ( ph /\ C e. M ) -> ( C mod G ) e. NN0 )
42 41 nn0red 
 |-  ( ( ph /\ C e. M ) -> ( C mod G ) e. RR )
43 34 nnred 
 |-  ( ph -> G e. RR )
44 43 adantr 
 |-  ( ( ph /\ C e. M ) -> G e. RR )
45 42 44 ltnled 
 |-  ( ( ph /\ C e. M ) -> ( ( C mod G ) < G <-> -. G <_ ( C mod G ) ) )
46 38 45 mpbid 
 |-  ( ( ph /\ C e. M ) -> -. G <_ ( C mod G ) )
47 18 simprd 
 |-  ( ( ph /\ C e. M ) -> E. s e. ZZ E. t e. ZZ C = ( ( A x. s ) + ( B x. t ) ) )
48 33 simprd 
 |-  ( ph -> E. u e. ZZ E. v e. ZZ G = ( ( A x. u ) + ( B x. v ) ) )
49 48 ad2antrr 
 |-  ( ( ( ph /\ C e. M ) /\ ( s e. ZZ /\ t e. ZZ ) ) -> E. u e. ZZ E. v e. ZZ G = ( ( A x. u ) + ( B x. v ) ) )
50 simprll 
 |-  ( ( ( ph /\ C e. M ) /\ ( ( s e. ZZ /\ t e. ZZ ) /\ ( u e. ZZ /\ v e. ZZ ) ) ) -> s e. ZZ )
51 simprrl 
 |-  ( ( ( ph /\ C e. M ) /\ ( ( s e. ZZ /\ t e. ZZ ) /\ ( u e. ZZ /\ v e. ZZ ) ) ) -> u e. ZZ )
52 20 40 nndivred 
 |-  ( ( ph /\ C e. M ) -> ( C / G ) e. RR )
53 52 flcld 
 |-  ( ( ph /\ C e. M ) -> ( |_ ` ( C / G ) ) e. ZZ )
54 53 adantr 
 |-  ( ( ( ph /\ C e. M ) /\ ( ( s e. ZZ /\ t e. ZZ ) /\ ( u e. ZZ /\ v e. ZZ ) ) ) -> ( |_ ` ( C / G ) ) e. ZZ )
55 51 54 zmulcld 
 |-  ( ( ( ph /\ C e. M ) /\ ( ( s e. ZZ /\ t e. ZZ ) /\ ( u e. ZZ /\ v e. ZZ ) ) ) -> ( u x. ( |_ ` ( C / G ) ) ) e. ZZ )
56 50 55 zsubcld 
 |-  ( ( ( ph /\ C e. M ) /\ ( ( s e. ZZ /\ t e. ZZ ) /\ ( u e. ZZ /\ v e. ZZ ) ) ) -> ( s - ( u x. ( |_ ` ( C / G ) ) ) ) e. ZZ )
57 simprlr 
 |-  ( ( ( ph /\ C e. M ) /\ ( ( s e. ZZ /\ t e. ZZ ) /\ ( u e. ZZ /\ v e. ZZ ) ) ) -> t e. ZZ )
58 simprrr 
 |-  ( ( ( ph /\ C e. M ) /\ ( ( s e. ZZ /\ t e. ZZ ) /\ ( u e. ZZ /\ v e. ZZ ) ) ) -> v e. ZZ )
59 58 54 zmulcld 
 |-  ( ( ( ph /\ C e. M ) /\ ( ( s e. ZZ /\ t e. ZZ ) /\ ( u e. ZZ /\ v e. ZZ ) ) ) -> ( v x. ( |_ ` ( C / G ) ) ) e. ZZ )
60 57 59 zsubcld 
 |-  ( ( ( ph /\ C e. M ) /\ ( ( s e. ZZ /\ t e. ZZ ) /\ ( u e. ZZ /\ v e. ZZ ) ) ) -> ( t - ( v x. ( |_ ` ( C / G ) ) ) ) e. ZZ )
61 2 zcnd 
 |-  ( ph -> A e. CC )
62 61 ad2antrr 
 |-  ( ( ( ph /\ C e. M ) /\ ( ( s e. ZZ /\ t e. ZZ ) /\ ( u e. ZZ /\ v e. ZZ ) ) ) -> A e. CC )
63 50 zcnd 
 |-  ( ( ( ph /\ C e. M ) /\ ( ( s e. ZZ /\ t e. ZZ ) /\ ( u e. ZZ /\ v e. ZZ ) ) ) -> s e. CC )
64 62 63 mulcld 
 |-  ( ( ( ph /\ C e. M ) /\ ( ( s e. ZZ /\ t e. ZZ ) /\ ( u e. ZZ /\ v e. ZZ ) ) ) -> ( A x. s ) e. CC )
65 3 zcnd 
 |-  ( ph -> B e. CC )
66 65 ad2antrr 
 |-  ( ( ( ph /\ C e. M ) /\ ( ( s e. ZZ /\ t e. ZZ ) /\ ( u e. ZZ /\ v e. ZZ ) ) ) -> B e. CC )
67 57 zcnd 
 |-  ( ( ( ph /\ C e. M ) /\ ( ( s e. ZZ /\ t e. ZZ ) /\ ( u e. ZZ /\ v e. ZZ ) ) ) -> t e. CC )
68 66 67 mulcld 
 |-  ( ( ( ph /\ C e. M ) /\ ( ( s e. ZZ /\ t e. ZZ ) /\ ( u e. ZZ /\ v e. ZZ ) ) ) -> ( B x. t ) e. CC )
69 55 zcnd 
 |-  ( ( ( ph /\ C e. M ) /\ ( ( s e. ZZ /\ t e. ZZ ) /\ ( u e. ZZ /\ v e. ZZ ) ) ) -> ( u x. ( |_ ` ( C / G ) ) ) e. CC )
70 62 69 mulcld 
 |-  ( ( ( ph /\ C e. M ) /\ ( ( s e. ZZ /\ t e. ZZ ) /\ ( u e. ZZ /\ v e. ZZ ) ) ) -> ( A x. ( u x. ( |_ ` ( C / G ) ) ) ) e. CC )
71 59 zcnd 
 |-  ( ( ( ph /\ C e. M ) /\ ( ( s e. ZZ /\ t e. ZZ ) /\ ( u e. ZZ /\ v e. ZZ ) ) ) -> ( v x. ( |_ ` ( C / G ) ) ) e. CC )
72 66 71 mulcld 
 |-  ( ( ( ph /\ C e. M ) /\ ( ( s e. ZZ /\ t e. ZZ ) /\ ( u e. ZZ /\ v e. ZZ ) ) ) -> ( B x. ( v x. ( |_ ` ( C / G ) ) ) ) e. CC )
73 64 68 70 72 addsub4d 
 |-  ( ( ( ph /\ C e. M ) /\ ( ( s e. ZZ /\ t e. ZZ ) /\ ( u e. ZZ /\ v e. ZZ ) ) ) -> ( ( ( A x. s ) + ( B x. t ) ) - ( ( A x. ( u x. ( |_ ` ( C / G ) ) ) ) + ( B x. ( v x. ( |_ ` ( C / G ) ) ) ) ) ) = ( ( ( A x. s ) - ( A x. ( u x. ( |_ ` ( C / G ) ) ) ) ) + ( ( B x. t ) - ( B x. ( v x. ( |_ ` ( C / G ) ) ) ) ) ) )
74 51 zcnd 
 |-  ( ( ( ph /\ C e. M ) /\ ( ( s e. ZZ /\ t e. ZZ ) /\ ( u e. ZZ /\ v e. ZZ ) ) ) -> u e. CC )
75 62 74 mulcld 
 |-  ( ( ( ph /\ C e. M ) /\ ( ( s e. ZZ /\ t e. ZZ ) /\ ( u e. ZZ /\ v e. ZZ ) ) ) -> ( A x. u ) e. CC )
76 53 zcnd 
 |-  ( ( ph /\ C e. M ) -> ( |_ ` ( C / G ) ) e. CC )
77 76 adantr 
 |-  ( ( ( ph /\ C e. M ) /\ ( ( s e. ZZ /\ t e. ZZ ) /\ ( u e. ZZ /\ v e. ZZ ) ) ) -> ( |_ ` ( C / G ) ) e. CC )
78 58 zcnd 
 |-  ( ( ( ph /\ C e. M ) /\ ( ( s e. ZZ /\ t e. ZZ ) /\ ( u e. ZZ /\ v e. ZZ ) ) ) -> v e. CC )
79 66 78 mulcld 
 |-  ( ( ( ph /\ C e. M ) /\ ( ( s e. ZZ /\ t e. ZZ ) /\ ( u e. ZZ /\ v e. ZZ ) ) ) -> ( B x. v ) e. CC )
80 62 74 77 mulassd 
 |-  ( ( ( ph /\ C e. M ) /\ ( ( s e. ZZ /\ t e. ZZ ) /\ ( u e. ZZ /\ v e. ZZ ) ) ) -> ( ( A x. u ) x. ( |_ ` ( C / G ) ) ) = ( A x. ( u x. ( |_ ` ( C / G ) ) ) ) )
81 66 78 77 mulassd 
 |-  ( ( ( ph /\ C e. M ) /\ ( ( s e. ZZ /\ t e. ZZ ) /\ ( u e. ZZ /\ v e. ZZ ) ) ) -> ( ( B x. v ) x. ( |_ ` ( C / G ) ) ) = ( B x. ( v x. ( |_ ` ( C / G ) ) ) ) )
82 80 81 oveq12d 
 |-  ( ( ( ph /\ C e. M ) /\ ( ( s e. ZZ /\ t e. ZZ ) /\ ( u e. ZZ /\ v e. ZZ ) ) ) -> ( ( ( A x. u ) x. ( |_ ` ( C / G ) ) ) + ( ( B x. v ) x. ( |_ ` ( C / G ) ) ) ) = ( ( A x. ( u x. ( |_ ` ( C / G ) ) ) ) + ( B x. ( v x. ( |_ ` ( C / G ) ) ) ) ) )
83 75 77 79 82 joinlmuladdmuld 
 |-  ( ( ( ph /\ C e. M ) /\ ( ( s e. ZZ /\ t e. ZZ ) /\ ( u e. ZZ /\ v e. ZZ ) ) ) -> ( ( ( A x. u ) + ( B x. v ) ) x. ( |_ ` ( C / G ) ) ) = ( ( A x. ( u x. ( |_ ` ( C / G ) ) ) ) + ( B x. ( v x. ( |_ ` ( C / G ) ) ) ) ) )
84 83 oveq2d 
 |-  ( ( ( ph /\ C e. M ) /\ ( ( s e. ZZ /\ t e. ZZ ) /\ ( u e. ZZ /\ v e. ZZ ) ) ) -> ( ( ( A x. s ) + ( B x. t ) ) - ( ( ( A x. u ) + ( B x. v ) ) x. ( |_ ` ( C / G ) ) ) ) = ( ( ( A x. s ) + ( B x. t ) ) - ( ( A x. ( u x. ( |_ ` ( C / G ) ) ) ) + ( B x. ( v x. ( |_ ` ( C / G ) ) ) ) ) ) )
85 62 63 69 subdid 
 |-  ( ( ( ph /\ C e. M ) /\ ( ( s e. ZZ /\ t e. ZZ ) /\ ( u e. ZZ /\ v e. ZZ ) ) ) -> ( A x. ( s - ( u x. ( |_ ` ( C / G ) ) ) ) ) = ( ( A x. s ) - ( A x. ( u x. ( |_ ` ( C / G ) ) ) ) ) )
86 66 67 71 subdid 
 |-  ( ( ( ph /\ C e. M ) /\ ( ( s e. ZZ /\ t e. ZZ ) /\ ( u e. ZZ /\ v e. ZZ ) ) ) -> ( B x. ( t - ( v x. ( |_ ` ( C / G ) ) ) ) ) = ( ( B x. t ) - ( B x. ( v x. ( |_ ` ( C / G ) ) ) ) ) )
87 85 86 oveq12d 
 |-  ( ( ( ph /\ C e. M ) /\ ( ( s e. ZZ /\ t e. ZZ ) /\ ( u e. ZZ /\ v e. ZZ ) ) ) -> ( ( A x. ( s - ( u x. ( |_ ` ( C / G ) ) ) ) ) + ( B x. ( t - ( v x. ( |_ ` ( C / G ) ) ) ) ) ) = ( ( ( A x. s ) - ( A x. ( u x. ( |_ ` ( C / G ) ) ) ) ) + ( ( B x. t ) - ( B x. ( v x. ( |_ ` ( C / G ) ) ) ) ) ) )
88 73 84 87 3eqtr4d 
 |-  ( ( ( ph /\ C e. M ) /\ ( ( s e. ZZ /\ t e. ZZ ) /\ ( u e. ZZ /\ v e. ZZ ) ) ) -> ( ( ( A x. s ) + ( B x. t ) ) - ( ( ( A x. u ) + ( B x. v ) ) x. ( |_ ` ( C / G ) ) ) ) = ( ( A x. ( s - ( u x. ( |_ ` ( C / G ) ) ) ) ) + ( B x. ( t - ( v x. ( |_ ` ( C / G ) ) ) ) ) ) )
89 oveq2 
 |-  ( x = ( s - ( u x. ( |_ ` ( C / G ) ) ) ) -> ( A x. x ) = ( A x. ( s - ( u x. ( |_ ` ( C / G ) ) ) ) ) )
90 89 oveq1d 
 |-  ( x = ( s - ( u x. ( |_ ` ( C / G ) ) ) ) -> ( ( A x. x ) + ( B x. y ) ) = ( ( A x. ( s - ( u x. ( |_ ` ( C / G ) ) ) ) ) + ( B x. y ) ) )
91 90 eqeq2d 
 |-  ( x = ( s - ( u x. ( |_ ` ( C / G ) ) ) ) -> ( ( ( ( A x. s ) + ( B x. t ) ) - ( ( ( A x. u ) + ( B x. v ) ) x. ( |_ ` ( C / G ) ) ) ) = ( ( A x. x ) + ( B x. y ) ) <-> ( ( ( A x. s ) + ( B x. t ) ) - ( ( ( A x. u ) + ( B x. v ) ) x. ( |_ ` ( C / G ) ) ) ) = ( ( A x. ( s - ( u x. ( |_ ` ( C / G ) ) ) ) ) + ( B x. y ) ) ) )
92 oveq2 
 |-  ( y = ( t - ( v x. ( |_ ` ( C / G ) ) ) ) -> ( B x. y ) = ( B x. ( t - ( v x. ( |_ ` ( C / G ) ) ) ) ) )
93 92 oveq2d 
 |-  ( y = ( t - ( v x. ( |_ ` ( C / G ) ) ) ) -> ( ( A x. ( s - ( u x. ( |_ ` ( C / G ) ) ) ) ) + ( B x. y ) ) = ( ( A x. ( s - ( u x. ( |_ ` ( C / G ) ) ) ) ) + ( B x. ( t - ( v x. ( |_ ` ( C / G ) ) ) ) ) ) )
94 93 eqeq2d 
 |-  ( y = ( t - ( v x. ( |_ ` ( C / G ) ) ) ) -> ( ( ( ( A x. s ) + ( B x. t ) ) - ( ( ( A x. u ) + ( B x. v ) ) x. ( |_ ` ( C / G ) ) ) ) = ( ( A x. ( s - ( u x. ( |_ ` ( C / G ) ) ) ) ) + ( B x. y ) ) <-> ( ( ( A x. s ) + ( B x. t ) ) - ( ( ( A x. u ) + ( B x. v ) ) x. ( |_ ` ( C / G ) ) ) ) = ( ( A x. ( s - ( u x. ( |_ ` ( C / G ) ) ) ) ) + ( B x. ( t - ( v x. ( |_ ` ( C / G ) ) ) ) ) ) ) )
95 91 94 rspc2ev 
 |-  ( ( ( s - ( u x. ( |_ ` ( C / G ) ) ) ) e. ZZ /\ ( t - ( v x. ( |_ ` ( C / G ) ) ) ) e. ZZ /\ ( ( ( A x. s ) + ( B x. t ) ) - ( ( ( A x. u ) + ( B x. v ) ) x. ( |_ ` ( C / G ) ) ) ) = ( ( A x. ( s - ( u x. ( |_ ` ( C / G ) ) ) ) ) + ( B x. ( t - ( v x. ( |_ ` ( C / G ) ) ) ) ) ) ) -> E. x e. ZZ E. y e. ZZ ( ( ( A x. s ) + ( B x. t ) ) - ( ( ( A x. u ) + ( B x. v ) ) x. ( |_ ` ( C / G ) ) ) ) = ( ( A x. x ) + ( B x. y ) ) )
96 56 60 88 95 syl3anc 
 |-  ( ( ( ph /\ C e. M ) /\ ( ( s e. ZZ /\ t e. ZZ ) /\ ( u e. ZZ /\ v e. ZZ ) ) ) -> E. x e. ZZ E. y e. ZZ ( ( ( A x. s ) + ( B x. t ) ) - ( ( ( A x. u ) + ( B x. v ) ) x. ( |_ ` ( C / G ) ) ) ) = ( ( A x. x ) + ( B x. y ) ) )
97 oveq1 
 |-  ( G = ( ( A x. u ) + ( B x. v ) ) -> ( G x. ( |_ ` ( C / G ) ) ) = ( ( ( A x. u ) + ( B x. v ) ) x. ( |_ ` ( C / G ) ) ) )
98 oveq12 
 |-  ( ( C = ( ( A x. s ) + ( B x. t ) ) /\ ( G x. ( |_ ` ( C / G ) ) ) = ( ( ( A x. u ) + ( B x. v ) ) x. ( |_ ` ( C / G ) ) ) ) -> ( C - ( G x. ( |_ ` ( C / G ) ) ) ) = ( ( ( A x. s ) + ( B x. t ) ) - ( ( ( A x. u ) + ( B x. v ) ) x. ( |_ ` ( C / G ) ) ) ) )
99 97 98 sylan2 
 |-  ( ( C = ( ( A x. s ) + ( B x. t ) ) /\ G = ( ( A x. u ) + ( B x. v ) ) ) -> ( C - ( G x. ( |_ ` ( C / G ) ) ) ) = ( ( ( A x. s ) + ( B x. t ) ) - ( ( ( A x. u ) + ( B x. v ) ) x. ( |_ ` ( C / G ) ) ) ) )
100 99 eqeq1d 
 |-  ( ( C = ( ( A x. s ) + ( B x. t ) ) /\ G = ( ( A x. u ) + ( B x. v ) ) ) -> ( ( C - ( G x. ( |_ ` ( C / G ) ) ) ) = ( ( A x. x ) + ( B x. y ) ) <-> ( ( ( A x. s ) + ( B x. t ) ) - ( ( ( A x. u ) + ( B x. v ) ) x. ( |_ ` ( C / G ) ) ) ) = ( ( A x. x ) + ( B x. y ) ) ) )
101 100 2rexbidv 
 |-  ( ( C = ( ( A x. s ) + ( B x. t ) ) /\ G = ( ( A x. u ) + ( B x. v ) ) ) -> ( E. x e. ZZ E. y e. ZZ ( C - ( G x. ( |_ ` ( C / G ) ) ) ) = ( ( A x. x ) + ( B x. y ) ) <-> E. x e. ZZ E. y e. ZZ ( ( ( A x. s ) + ( B x. t ) ) - ( ( ( A x. u ) + ( B x. v ) ) x. ( |_ ` ( C / G ) ) ) ) = ( ( A x. x ) + ( B x. y ) ) ) )
102 96 101 syl5ibrcom 
 |-  ( ( ( ph /\ C e. M ) /\ ( ( s e. ZZ /\ t e. ZZ ) /\ ( u e. ZZ /\ v e. ZZ ) ) ) -> ( ( C = ( ( A x. s ) + ( B x. t ) ) /\ G = ( ( A x. u ) + ( B x. v ) ) ) -> E. x e. ZZ E. y e. ZZ ( C - ( G x. ( |_ ` ( C / G ) ) ) ) = ( ( A x. x ) + ( B x. y ) ) ) )
103 102 expcomd 
 |-  ( ( ( ph /\ C e. M ) /\ ( ( s e. ZZ /\ t e. ZZ ) /\ ( u e. ZZ /\ v e. ZZ ) ) ) -> ( G = ( ( A x. u ) + ( B x. v ) ) -> ( C = ( ( A x. s ) + ( B x. t ) ) -> E. x e. ZZ E. y e. ZZ ( C - ( G x. ( |_ ` ( C / G ) ) ) ) = ( ( A x. x ) + ( B x. y ) ) ) ) )
104 103 expr 
 |-  ( ( ( ph /\ C e. M ) /\ ( s e. ZZ /\ t e. ZZ ) ) -> ( ( u e. ZZ /\ v e. ZZ ) -> ( G = ( ( A x. u ) + ( B x. v ) ) -> ( C = ( ( A x. s ) + ( B x. t ) ) -> E. x e. ZZ E. y e. ZZ ( C - ( G x. ( |_ ` ( C / G ) ) ) ) = ( ( A x. x ) + ( B x. y ) ) ) ) ) )
105 104 rexlimdvv 
 |-  ( ( ( ph /\ C e. M ) /\ ( s e. ZZ /\ t e. ZZ ) ) -> ( E. u e. ZZ E. v e. ZZ G = ( ( A x. u ) + ( B x. v ) ) -> ( C = ( ( A x. s ) + ( B x. t ) ) -> E. x e. ZZ E. y e. ZZ ( C - ( G x. ( |_ ` ( C / G ) ) ) ) = ( ( A x. x ) + ( B x. y ) ) ) ) )
106 49 105 mpd 
 |-  ( ( ( ph /\ C e. M ) /\ ( s e. ZZ /\ t e. ZZ ) ) -> ( C = ( ( A x. s ) + ( B x. t ) ) -> E. x e. ZZ E. y e. ZZ ( C - ( G x. ( |_ ` ( C / G ) ) ) ) = ( ( A x. x ) + ( B x. y ) ) ) )
107 106 ex 
 |-  ( ( ph /\ C e. M ) -> ( ( s e. ZZ /\ t e. ZZ ) -> ( C = ( ( A x. s ) + ( B x. t ) ) -> E. x e. ZZ E. y e. ZZ ( C - ( G x. ( |_ ` ( C / G ) ) ) ) = ( ( A x. x ) + ( B x. y ) ) ) ) )
108 107 rexlimdvv 
 |-  ( ( ph /\ C e. M ) -> ( E. s e. ZZ E. t e. ZZ C = ( ( A x. s ) + ( B x. t ) ) -> E. x e. ZZ E. y e. ZZ ( C - ( G x. ( |_ ` ( C / G ) ) ) ) = ( ( A x. x ) + ( B x. y ) ) ) )
109 47 108 mpd 
 |-  ( ( ph /\ C e. M ) -> E. x e. ZZ E. y e. ZZ ( C - ( G x. ( |_ ` ( C / G ) ) ) ) = ( ( A x. x ) + ( B x. y ) ) )
110 modval 
 |-  ( ( C e. RR /\ G e. RR+ ) -> ( C mod G ) = ( C - ( G x. ( |_ ` ( C / G ) ) ) ) )
111 20 36 110 syl2anc 
 |-  ( ( ph /\ C e. M ) -> ( C mod G ) = ( C - ( G x. ( |_ ` ( C / G ) ) ) ) )
112 111 eqcomd 
 |-  ( ( ph /\ C e. M ) -> ( C - ( G x. ( |_ ` ( C / G ) ) ) ) = ( C mod G ) )
113 112 eqeq1d 
 |-  ( ( ph /\ C e. M ) -> ( ( C - ( G x. ( |_ ` ( C / G ) ) ) ) = ( ( A x. x ) + ( B x. y ) ) <-> ( C mod G ) = ( ( A x. x ) + ( B x. y ) ) ) )
114 113 2rexbidv 
 |-  ( ( ph /\ C e. M ) -> ( E. x e. ZZ E. y e. ZZ ( C - ( G x. ( |_ ` ( C / G ) ) ) ) = ( ( A x. x ) + ( B x. y ) ) <-> E. x e. ZZ E. y e. ZZ ( C mod G ) = ( ( A x. x ) + ( B x. y ) ) ) )
115 109 114 mpbid 
 |-  ( ( ph /\ C e. M ) -> E. x e. ZZ E. y e. ZZ ( C mod G ) = ( ( A x. x ) + ( B x. y ) ) )
116 eqeq1 
 |-  ( z = ( C mod G ) -> ( z = ( ( A x. x ) + ( B x. y ) ) <-> ( C mod G ) = ( ( A x. x ) + ( B x. y ) ) ) )
117 116 2rexbidv 
 |-  ( z = ( C mod G ) -> ( E. x e. ZZ E. y e. ZZ z = ( ( A x. x ) + ( B x. y ) ) <-> E. x e. ZZ E. y e. ZZ ( C mod G ) = ( ( A x. x ) + ( B x. y ) ) ) )
118 117 1 elrab2 
 |-  ( ( C mod G ) e. M <-> ( ( C mod G ) e. NN /\ E. x e. ZZ E. y e. ZZ ( C mod G ) = ( ( A x. x ) + ( B x. y ) ) ) )
119 118 simplbi2com 
 |-  ( E. x e. ZZ E. y e. ZZ ( C mod G ) = ( ( A x. x ) + ( B x. y ) ) -> ( ( C mod G ) e. NN -> ( C mod G ) e. M ) )
120 115 119 syl 
 |-  ( ( ph /\ C e. M ) -> ( ( C mod G ) e. NN -> ( C mod G ) e. M ) )
121 1 ssrab3 
 |-  M C_ NN
122 nnuz 
 |-  NN = ( ZZ>= ` 1 )
123 121 122 sseqtri 
 |-  M C_ ( ZZ>= ` 1 )
124 infssuzle 
 |-  ( ( M C_ ( ZZ>= ` 1 ) /\ ( C mod G ) e. M ) -> inf ( M , RR , < ) <_ ( C mod G ) )
125 123 124 mpan 
 |-  ( ( C mod G ) e. M -> inf ( M , RR , < ) <_ ( C mod G ) )
126 4 125 eqbrtrid 
 |-  ( ( C mod G ) e. M -> G <_ ( C mod G ) )
127 120 126 syl6 
 |-  ( ( ph /\ C e. M ) -> ( ( C mod G ) e. NN -> G <_ ( C mod G ) ) )
128 46 127 mtod 
 |-  ( ( ph /\ C e. M ) -> -. ( C mod G ) e. NN )
129 elnn0 
 |-  ( ( C mod G ) e. NN0 <-> ( ( C mod G ) e. NN \/ ( C mod G ) = 0 ) )
130 41 129 sylib 
 |-  ( ( ph /\ C e. M ) -> ( ( C mod G ) e. NN \/ ( C mod G ) = 0 ) )
131 130 ord 
 |-  ( ( ph /\ C e. M ) -> ( -. ( C mod G ) e. NN -> ( C mod G ) = 0 ) )
132 128 131 mpd 
 |-  ( ( ph /\ C e. M ) -> ( C mod G ) = 0 )
133 dvdsval3 
 |-  ( ( G e. NN /\ C e. ZZ ) -> ( G || C <-> ( C mod G ) = 0 ) )
134 40 39 133 syl2anc 
 |-  ( ( ph /\ C e. M ) -> ( G || C <-> ( C mod G ) = 0 ) )
135 132 134 mpbird 
 |-  ( ( ph /\ C e. M ) -> G || C )
136 135 ex 
 |-  ( ph -> ( C e. M -> G || C ) )