Theorem dfcop2 ≪ | index | src | ≫ 

theorem dfcop2 (a b: nat) {x: nat}:
  $ coprime a b <-> A. x (x || a -> x || b -> x = 1) $;
StepHypRefExpression
1 anll 
coprime a b /\ x || a /\ x || b -> coprime a b
2 anlr 
coprime a b /\ x || a /\ x || b -> x || a
3 anr 
coprime a b /\ x || a /\ x || b -> x || b
4 1, 2, 3 dvdcop 
coprime a b /\ x || a /\ x || b -> x = 1
5 4 exp 
coprime a b /\ x || a -> x || b -> x = 1
6 5 ialda 
coprime a b -> A. x (x || a -> x || b -> x = 1)
7 dvd11 
1 || a
8 dvdtr 
y || 1 -> 1 || a -> y || a
9 7, 8 mpi 
y || 1 -> y || a
10 dvd11 
1 || b
11 dvdtr 
y || 1 -> 1 || b -> y || b
12 10, 11 mpi 
y || 1 -> y || b
13 9, 12 iand 
y || 1 -> y || a /\ y || b
14 13 a1i 
A. x (x || a -> x || b -> x = 1) -> y || 1 -> y || a /\ y || b
15 dvd12 
y || 1 <-> y = 1
16 anrr 
A. x (x || a -> x || b -> x = 1) /\ (y || a /\ y || b) -> y || b
17 anrl 
A. x (x || a -> x || b -> x = 1) /\ (y || a /\ y || b) -> y || a
18 dvdeq1 
x = y -> (x || a <-> y || a)
19 dvdeq1 
x = y -> (x || b <-> y || b)
20 eqeq1 
x = y -> (x = 1 <-> y = 1)
21 19, 20 imeqd 
x = y -> (x || b -> x = 1 <-> y || b -> y = 1)
22 18, 21 imeqd 
x = y -> (x || a -> x || b -> x = 1 <-> y || a -> y || b -> y = 1)
23 22 eale 
A. x (x || a -> x || b -> x = 1) -> y || a -> y || b -> y = 1
24 23 anwl 
A. x (x || a -> x || b -> x = 1) /\ (y || a /\ y || b) -> y || a -> y || b -> y = 1
25 17, 24 mpd 
A. x (x || a -> x || b -> x = 1) /\ (y || a /\ y || b) -> y || b -> y = 1
26 16, 25 mpd 
A. x (x || a -> x || b -> x = 1) /\ (y || a /\ y || b) -> y = 1
27 15, 26 sylibr 
A. x (x || a -> x || b -> x = 1) /\ (y || a /\ y || b) -> y || 1
28 27 exp 
A. x (x || a -> x || b -> x = 1) -> y || a /\ y || b -> y || 1
29 14, 28 ibid 
A. x (x || a -> x || b -> x = 1) -> (y || 1 <-> y || a /\ y || b)
30 29 eqgcd 
A. x (x || a -> x || b -> x = 1) -> gcd a b = 1
31 30 conv coprime 
A. x (x || a -> x || b -> x = 1) -> coprime a b
32 6, 31 ibii 
coprime a b <-> A. x (x || a -> x || b -> x = 1)

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)