Theorem lcmex ≪ | index | src | ≫ 

theorem lcmex {m: nat} (n: nat) {x: nat}:
  $ E. m (0 < m /\ A. x (0 < x /\ x <= n -> x || m)) $;
StepHypRefExpression
1 id 
_1 = n -> _1 = n
2 1 leeq2d 
_1 = n -> (x <= _1 <-> x <= n)
3 2 aneq2d 
_1 = n -> (0 < x /\ x <= _1 <-> 0 < x /\ x <= n)
4 3 imeq1d 
_1 = n -> (0 < x /\ x <= _1 -> x || m <-> 0 < x /\ x <= n -> x || m)
5 4 aleqd 
_1 = n -> (A. x (0 < x /\ x <= _1 -> x || m) <-> A. x (0 < x /\ x <= n -> x || m))
6 5 aneq2d 
_1 = n -> (0 < m /\ A. x (0 < x /\ x <= _1 -> x || m) <-> 0 < m /\ A. x (0 < x /\ x <= n -> x || m))
7 6 exeqd 
_1 = n -> (E. m (0 < m /\ A. x (0 < x /\ x <= _1 -> x || m)) <-> E. m (0 < m /\ A. x (0 < x /\ x <= n -> x || m)))
8 id 
_1 = 0 -> _1 = 0
9 8 leeq2d 
_1 = 0 -> (x <= _1 <-> x <= 0)
10 9 aneq2d 
_1 = 0 -> (0 < x /\ x <= _1 <-> 0 < x /\ x <= 0)
11 10 imeq1d 
_1 = 0 -> (0 < x /\ x <= _1 -> x || m <-> 0 < x /\ x <= 0 -> x || m)
12 11 aleqd 
_1 = 0 -> (A. x (0 < x /\ x <= _1 -> x || m) <-> A. x (0 < x /\ x <= 0 -> x || m))
13 12 aneq2d 
_1 = 0 -> (0 < m /\ A. x (0 < x /\ x <= _1 -> x || m) <-> 0 < m /\ A. x (0 < x /\ x <= 0 -> x || m))
14 13 exeqd 
_1 = 0 -> (E. m (0 < m /\ A. x (0 < x /\ x <= _1 -> x || m)) <-> E. m (0 < m /\ A. x (0 < x /\ x <= 0 -> x || m)))
15 id 
_1 = a1 -> _1 = a1
16 15 leeq2d 
_1 = a1 -> (x <= _1 <-> x <= a1)
17 16 aneq2d 
_1 = a1 -> (0 < x /\ x <= _1 <-> 0 < x /\ x <= a1)
18 17 imeq1d 
_1 = a1 -> (0 < x /\ x <= _1 -> x || m <-> 0 < x /\ x <= a1 -> x || m)
19 18 aleqd 
_1 = a1 -> (A. x (0 < x /\ x <= _1 -> x || m) <-> A. x (0 < x /\ x <= a1 -> x || m))
20 19 aneq2d 
_1 = a1 -> (0 < m /\ A. x (0 < x /\ x <= _1 -> x || m) <-> 0 < m /\ A. x (0 < x /\ x <= a1 -> x || m))
21 20 exeqd 
_1 = a1 -> (E. m (0 < m /\ A. x (0 < x /\ x <= _1 -> x || m)) <-> E. m (0 < m /\ A. x (0 < x /\ x <= a1 -> x || m)))
22 id 
_1 = suc a1 -> _1 = suc a1
23 22 leeq2d 
_1 = suc a1 -> (x <= _1 <-> x <= suc a1)
24 23 aneq2d 
_1 = suc a1 -> (0 < x /\ x <= _1 <-> 0 < x /\ x <= suc a1)
25 24 imeq1d 
_1 = suc a1 -> (0 < x /\ x <= _1 -> x || m <-> 0 < x /\ x <= suc a1 -> x || m)
26 25 aleqd 
_1 = suc a1 -> (A. x (0 < x /\ x <= _1 -> x || m) <-> A. x (0 < x /\ x <= suc a1 -> x || m))
27 26 aneq2d 
_1 = suc a1 -> (0 < m /\ A. x (0 < x /\ x <= _1 -> x || m) <-> 0 < m /\ A. x (0 < x /\ x <= suc a1 -> x || m))
28 27 exeqd 
_1 = suc a1 -> (E. m (0 < m /\ A. x (0 < x /\ x <= _1 -> x || m)) <-> E. m (0 < m /\ A. x (0 < x /\ x <= suc a1 -> x || m)))
29 leeq2 
m = 1 -> (suc 0 <= m <-> suc 0 <= 1)
30 dvdeq2 
m = 1 -> (x || m <-> x || 1)
31 30 imeq2d 
m = 1 -> (0 < x /\ x <= 0 -> x || m <-> 0 < x /\ x <= 0 -> x || 1)
32 31 aleqd 
m = 1 -> (A. x (0 < x /\ x <= 0 -> x || m) <-> A. x (0 < x /\ x <= 0 -> x || 1))
33 29, 32 aneqd 
m = 1 -> (suc 0 <= m /\ A. x (0 < x /\ x <= 0 -> x || m) <-> suc 0 <= 1 /\ A. x (0 < x /\ x <= 0 -> x || 1))
34 33 iexe 
suc 0 <= 1 /\ A. x (0 < x /\ x <= 0 -> x || 1) -> E. m (suc 0 <= m /\ A. x (0 < x /\ x <= 0 -> x || m))
35 34 conv lt 
suc 0 <= 1 /\ A. x (0 < x /\ x <= 0 -> x || 1) -> E. m (0 < m /\ A. x (0 < x /\ x <= 0 -> x || m))
36 ian 
suc 0 <= 1 -> A. x (0 < x /\ x <= 0 -> x || 1) -> suc 0 <= 1 /\ A. x (0 < x /\ x <= 0 -> x || 1)
37 d0lt1 
0 < 1
38 37 conv lt 
suc 0 <= 1
39 36, 38 ax_mp 
A. x (0 < x /\ x <= 0 -> x || 1) -> suc 0 <= 1 /\ A. x (0 < x /\ x <= 0 -> x || 1)
40 ltnle 
0 < x <-> ~x <= 0
41 absurd 
~x <= 0 -> x <= 0 -> x || 1
42 40, 41 sylbi 
0 < x -> x <= 0 -> x || 1
43 42 imp 
0 < x /\ x <= 0 -> x || 1
44 43 ax_gen 
A. x (0 < x /\ x <= 0 -> x || 1)
45 39, 44 ax_mp 
suc 0 <= 1 /\ A. x (0 < x /\ x <= 0 -> x || 1)
46 35, 45 ax_mp 
E. m (0 < m /\ A. x (0 < x /\ x <= 0 -> x || m))
47 leeq2 
m = a -> (suc 0 <= m <-> suc 0 <= a)
48 47 conv lt 
m = a -> (0 < m <-> suc 0 <= a)
49 dvdeq2 
m = a -> (x || m <-> x || a)
50 49 imeq2d 
m = a -> (0 < x /\ x <= a1 -> x || m <-> 0 < x /\ x <= a1 -> x || a)
51 50 aleqd 
m = a -> (A. x (0 < x /\ x <= a1 -> x || m) <-> A. x (0 < x /\ x <= a1 -> x || a))
52 48, 51 aneqd 
m = a -> (0 < m /\ A. x (0 < x /\ x <= a1 -> x || m) <-> suc 0 <= a /\ A. x (0 < x /\ x <= a1 -> x || a))
53 52 cbvex 
E. m (0 < m /\ A. x (0 < x /\ x <= a1 -> x || m)) <-> E. a (suc 0 <= a /\ A. x (0 < x /\ x <= a1 -> x || a))
54 leeq2 
m = a * suc a1 -> (suc 0 <= m <-> suc 0 <= a * suc a1)
55 54 conv lt 
m = a * suc a1 -> (0 < m <-> suc 0 <= a * suc a1)
56 dvdeq2 
m = a * suc a1 -> (x || m <-> x || a * suc a1)
57 56 imeq2d 
m = a * suc a1 -> (0 < x /\ x <= suc a1 -> x || m <-> 0 < x /\ x <= suc a1 -> x || a * suc a1)
58 57 aleqd 
m = a * suc a1 -> (A. x (0 < x /\ x <= suc a1 -> x || m) <-> A. x (0 < x /\ x <= suc a1 -> x || a * suc a1))
59 55, 58 aneqd 
m = a * suc a1 -> (0 < m /\ A. x (0 < x /\ x <= suc a1 -> x || m) <-> suc 0 <= a * suc a1 /\ A. x (0 < x /\ x <= suc a1 -> x || a * suc a1))
60 59 iexe 
suc 0 <= a * suc a1 /\ A. x (0 < x /\ x <= suc a1 -> x || a * suc a1) -> E. m (0 < m /\ A. x (0 < x /\ x <= suc a1 -> x || m))
61 mulpos 
0 < a * suc a1 <-> 0 < a /\ 0 < suc a1
62 61 conv lt 
suc 0 <= a * suc a1 <-> 0 < a /\ 0 < suc a1
63 anl 
suc 0 <= a /\ A. x (0 < x /\ x <= a1 -> x || a) -> suc 0 <= a
64 63 conv lt 
suc 0 <= a /\ A. x (0 < x /\ x <= a1 -> x || a) -> 0 < a
65 lt01S 
0 < suc a1
66 65 a1i 
suc 0 <= a /\ A. x (0 < x /\ x <= a1 -> x || a) -> 0 < suc a1
67 64, 66 iand 
suc 0 <= a /\ A. x (0 < x /\ x <= a1 -> x || a) -> 0 < a /\ 0 < suc a1
68 62, 67 sylibr 
suc 0 <= a /\ A. x (0 < x /\ x <= a1 -> x || a) -> suc 0 <= a * suc a1
69 impexp 
0 < x /\ x <= a1 -> x || a <-> 0 < x -> x <= a1 -> x || a
70 impexp 
0 < x /\ x <= suc a1 -> x || a * suc a1 <-> 0 < x -> x <= suc a1 -> x || a * suc a1
71 imim2 
((x <= a1 -> x || a) -> x <= suc a1 -> x || a * suc a1) -> (0 < x -> x <= a1 -> x || a) -> 0 < x -> x <= suc a1 -> x || a * suc a1
72 leloe 
x <= suc a1 <-> x < suc a1 \/ x = suc a1
73 leltsuc 
x <= a1 <-> x < suc a1
74 dvdmul11 
x || a -> x || a * suc a1
75 74 imim2i 
(x <= a1 -> x || a) -> x <= a1 -> x || a * suc a1
76 73, 75 syl5bir 
(x <= a1 -> x || a) -> x < suc a1 -> x || a * suc a1
77 dvdmul1 
x || a * x
78 muleq2 
x = suc a1 -> a * x = a * suc a1
79 78 dvdeq2d 
x = suc a1 -> (x || a * x <-> x || a * suc a1)
80 77, 79 mpbii 
x = suc a1 -> x || a * suc a1
81 80 a1i 
(x <= a1 -> x || a) -> x = suc a1 -> x || a * suc a1
82 76, 81 eord 
(x <= a1 -> x || a) -> x < suc a1 \/ x = suc a1 -> x || a * suc a1
83 72, 82 syl5bi 
(x <= a1 -> x || a) -> x <= suc a1 -> x || a * suc a1
84 71, 83 ax_mp 
(0 < x -> x <= a1 -> x || a) -> 0 < x -> x <= suc a1 -> x || a * suc a1
85 70, 84 sylibr 
(0 < x -> x <= a1 -> x || a) -> 0 < x /\ x <= suc a1 -> x || a * suc a1
86 69, 85 sylbi 
(0 < x /\ x <= a1 -> x || a) -> 0 < x /\ x <= suc a1 -> x || a * suc a1
87 86 alimi 
A. x (0 < x /\ x <= a1 -> x || a) -> A. x (0 < x /\ x <= suc a1 -> x || a * suc a1)
88 87 anwr 
suc 0 <= a /\ A. x (0 < x /\ x <= a1 -> x || a) -> A. x (0 < x /\ x <= suc a1 -> x || a * suc a1)
89 60, 68, 88 sylan 
suc 0 <= a /\ A. x (0 < x /\ x <= a1 -> x || a) -> E. m (0 < m /\ A. x (0 < x /\ x <= suc a1 -> x || m))
90 89 eex 
E. a (suc 0 <= a /\ A. x (0 < x /\ x <= a1 -> x || a)) -> E. m (0 < m /\ A. x (0 < x /\ x <= suc a1 -> x || m))
91 53, 90 sylbi 
E. m (0 < m /\ A. x (0 < x /\ x <= a1 -> x || m)) -> E. m (0 < m /\ A. x (0 < x /\ x <= suc a1 -> x || m))
92 7, 14, 21, 28, 46, 91 ind 
E. m (0 < m /\ A. x (0 < x /\ x <= n -> x || m))

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_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)