# 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+ )`
` |-  ( ( 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 )`
` |-  ( ( 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 )`
` |-  ( ( 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 ) ) )`
` |-  ( ( ( 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 )`
` |-  ( ( ( 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 )`
` |-  ( ( ( 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 )`
` |-  ( ( ( 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 )`
` |-  ( ( ( 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 ) )`