Theorem copdvdmul2 ≪ | index | src | ≫ 

theorem copdvdmul2 (G: wff) (a b c: nat):
  $ G -> coprime a b $ >
  $ G -> a || b * c $ >
  $ G -> a || c $;
StepHypRefExpression
1 mul11 
1 * c = c
2 gcd01 
gcd 0 b = b
3 gcdeq1 
a = 0 -> gcd a b = gcd 0 b
4 2, 3 syl6eq 
a = 0 -> gcd a b = b
5 4 anwr 
G /\ a = 0 -> gcd a b = b
6 hyp h1 
G -> coprime a b
7 6 conv coprime 
G -> gcd a b = 1
8 7 anwl 
G /\ a = 0 -> gcd a b = 1
9 5, 8 eqtr3d 
G /\ a = 0 -> b = 1
10 9 muleq1d 
G /\ a = 0 -> b * c = 1 * c
11 1, 10 syl6eq 
G /\ a = 0 -> b * c = c
12 11 dvdeq2d 
G /\ a = 0 -> (a || b * c <-> a || c)
13 hyp h2 
G -> a || b * c
14 13 anwl 
G /\ a = 0 -> a || b * c
15 12, 14 mpbid 
G /\ a = 0 -> a || c
16 6 anwl 
G /\ ~a = 0 -> coprime a b
17 anr 
G /\ ~a = 0 -> ~a = 0
18 17 conv ne 
G /\ ~a = 0 -> a != 0
19 16, 18 copbezout 
G /\ ~a = 0 -> E. x E. y x * a = y * b + 1
20 dvdadd1 
a || b * c * y -> (a || c <-> a || b * c * y + c)
21 dvdmul11 
a || b * c -> a || b * c * y
22 13 anwll 
G /\ ~a = 0 /\ x * a = y * b + 1 -> a || b * c
23 21, 22 syl 
G /\ ~a = 0 /\ x * a = y * b + 1 -> a || b * c * y
24 20, 23 syl 
G /\ ~a = 0 /\ x * a = y * b + 1 -> (a || c <-> a || b * c * y + c)
25 dvdmul1 
a || x * c * a
26 mulrass 
x * c * a = x * a * c
27 addeq 
b * y * c = b * c * y -> 1 * c = c -> b * y * c + 1 * c = b * c * y + c
28 mulrass 
b * y * c = b * c * y
29 27, 28 ax_mp 
1 * c = c -> b * y * c + 1 * c = b * c * y + c
30 29, 1 ax_mp 
b * y * c + 1 * c = b * c * y + c
31 addmul 
(b * y + 1) * c = b * y * c + 1 * c
32 addeq1 
y * b = b * y -> y * b + 1 = b * y + 1
33 mulcom 
y * b = b * y
34 32, 33 ax_mp 
y * b + 1 = b * y + 1
35 anr 
G /\ ~a = 0 /\ x * a = y * b + 1 -> x * a = y * b + 1
36 34, 35 syl6eq 
G /\ ~a = 0 /\ x * a = y * b + 1 -> x * a = b * y + 1
37 36 muleq1d 
G /\ ~a = 0 /\ x * a = y * b + 1 -> x * a * c = (b * y + 1) * c
38 31, 37 syl6eq 
G /\ ~a = 0 /\ x * a = y * b + 1 -> x * a * c = b * y * c + 1 * c
39 30, 38 syl6eq 
G /\ ~a = 0 /\ x * a = y * b + 1 -> x * a * c = b * c * y + c
40 26, 39 syl5eq 
G /\ ~a = 0 /\ x * a = y * b + 1 -> x * c * a = b * c * y + c
41 40 dvdeq2d 
G /\ ~a = 0 /\ x * a = y * b + 1 -> (a || x * c * a <-> a || b * c * y + c)
42 25, 41 mpbii 
G /\ ~a = 0 /\ x * a = y * b + 1 -> a || b * c * y + c
43 24, 42 mpbird 
G /\ ~a = 0 /\ x * a = y * b + 1 -> a || c
44 43 eexda 
G /\ ~a = 0 -> E. y x * a = y * b + 1 -> a || c
45 44 eexd 
G /\ ~a = 0 -> E. x E. y x * a = y * b + 1 -> a || c
46 19, 45 mpd 
G /\ ~a = 0 -> a || c
47 15, 46 casesda 
G -> a || c

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_set (elab, ax_8), axs_the (theid, the0), axs_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)