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 syl6bb
 |-  ( 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 ) )