This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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