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 biidd 
_1 = n -> (0 < m <-> 0 < m)
2 biidd 
_1 = n -> (0 < x <-> 0 < x)
3 eqidd 
_1 = n -> x = x
4 id 
_1 = n -> _1 = n
5 3, 4 leeqd 
_1 = n -> (x <= _1 <-> x <= n)
6 2, 5 aneqd 
_1 = n -> (0 < x /\ x <= _1 <-> 0 < x /\ x <= n)
7 biidd 
_1 = n -> (x || m <-> x || m)
8 6, 7 imeqd 
_1 = n -> (0 < x /\ x <= _1 -> x || m <-> 0 < x /\ x <= n -> x || m)
9 8 aleqd 
_1 = n -> (A. x (0 < x /\ x <= _1 -> x || m) <-> A. x (0 < x /\ x <= n -> x || m))
10 1, 9 aneqd 
_1 = n -> (0 < m /\ A. x (0 < x /\ x <= _1 -> x || m) <-> 0 < m /\ A. x (0 < x /\ x <= n -> x || m))
11 10 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)))
12 biidd 
_1 = 0 -> (0 < m <-> 0 < m)
13 biidd 
_1 = 0 -> (0 < x <-> 0 < x)
14 eqidd 
_1 = 0 -> x = x
15 id 
_1 = 0 -> _1 = 0
16 14, 15 leeqd 
_1 = 0 -> (x <= _1 <-> x <= 0)
17 13, 16 aneqd 
_1 = 0 -> (0 < x /\ x <= _1 <-> 0 < x /\ x <= 0)
18 biidd 
_1 = 0 -> (x || m <-> x || m)
19 17, 18 imeqd 
_1 = 0 -> (0 < x /\ x <= _1 -> x || m <-> 0 < x /\ x <= 0 -> x || m)
20 19 aleqd 
_1 = 0 -> (A. x (0 < x /\ x <= _1 -> x || m) <-> A. x (0 < x /\ x <= 0 -> x || m))
21 12, 20 aneqd 
_1 = 0 -> (0 < m /\ A. x (0 < x /\ x <= _1 -> x || m) <-> 0 < m /\ A. x (0 < x /\ x <= 0 -> x || m))
22 21 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)))
23 biidd 
_1 = a1 -> (0 < m <-> 0 < m)
24 biidd 
_1 = a1 -> (0 < x <-> 0 < x)
25 eqidd 
_1 = a1 -> x = x
26 id 
_1 = a1 -> _1 = a1
27 25, 26 leeqd 
_1 = a1 -> (x <= _1 <-> x <= a1)
28 24, 27 aneqd 
_1 = a1 -> (0 < x /\ x <= _1 <-> 0 < x /\ x <= a1)
29 biidd 
_1 = a1 -> (x || m <-> x || m)
30 28, 29 imeqd 
_1 = a1 -> (0 < x /\ x <= _1 -> x || m <-> 0 < x /\ x <= a1 -> x || m)
31 30 aleqd 
_1 = a1 -> (A. x (0 < x /\ x <= _1 -> x || m) <-> A. x (0 < x /\ x <= a1 -> x || m))
32 23, 31 aneqd 
_1 = a1 -> (0 < m /\ A. x (0 < x /\ x <= _1 -> x || m) <-> 0 < m /\ A. x (0 < x /\ x <= a1 -> x || m))
33 32 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)))
34 biidd 
_1 = suc a1 -> (0 < m <-> 0 < m)
35 biidd 
_1 = suc a1 -> (0 < x <-> 0 < x)
36 eqidd 
_1 = suc a1 -> x = x
37 id 
_1 = suc a1 -> _1 = suc a1
38 36, 37 leeqd 
_1 = suc a1 -> (x <= _1 <-> x <= suc a1)
39 35, 38 aneqd 
_1 = suc a1 -> (0 < x /\ x <= _1 <-> 0 < x /\ x <= suc a1)
40 biidd 
_1 = suc a1 -> (x || m <-> x || m)
41 39, 40 imeqd 
_1 = suc a1 -> (0 < x /\ x <= _1 -> x || m <-> 0 < x /\ x <= suc a1 -> x || m)
42 41 aleqd 
_1 = suc a1 -> (A. x (0 < x /\ x <= _1 -> x || m) <-> A. x (0 < x /\ x <= suc a1 -> x || m))
43 34, 42 aneqd 
_1 = suc a1 -> (0 < m /\ A. x (0 < x /\ x <= _1 -> x || m) <-> 0 < m /\ A. x (0 < x /\ x <= suc a1 -> x || m))
44 43 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)))
45 leeq2 
m = 1 -> (suc 0 <= m <-> suc 0 <= 1)
46 dvdeq2 
m = 1 -> (x || m <-> x || 1)
47 46 imeq2d 
m = 1 -> (0 < x /\ x <= 0 -> x || m <-> 0 < x /\ x <= 0 -> x || 1)
48 47 aleqd 
m = 1 -> (A. x (0 < x /\ x <= 0 -> x || m) <-> A. x (0 < x /\ x <= 0 -> x || 1))
49 45, 48 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))
50 49 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))
51 50 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))
52 ian 
suc 0 <= 1 -> A. x (0 < x /\ x <= 0 -> x || 1) -> suc 0 <= 1 /\ A. x (0 < x /\ x <= 0 -> x || 1)
53 d0lt1 
0 < 1
54 53 conv lt 
suc 0 <= 1
55 52, 54 ax_mp 
A. x (0 < x /\ x <= 0 -> x || 1) -> suc 0 <= 1 /\ A. x (0 < x /\ x <= 0 -> x || 1)
56 ltnle 
0 < x <-> ~x <= 0
57 absurd 
~x <= 0 -> x <= 0 -> x || 1
58 56, 57 sylbi 
0 < x -> x <= 0 -> x || 1
59 58 imp 
0 < x /\ x <= 0 -> x || 1
60 59 ax_gen 
A. x (0 < x /\ x <= 0 -> x || 1)
61 55, 60 ax_mp 
suc 0 <= 1 /\ A. x (0 < x /\ x <= 0 -> x || 1)
62 51, 61 ax_mp 
E. m (0 < m /\ A. x (0 < x /\ x <= 0 -> x || m))
63 leeq2 
m = a -> (suc 0 <= m <-> suc 0 <= a)
64 63 conv lt 
m = a -> (0 < m <-> suc 0 <= a)
65 dvdeq2 
m = a -> (x || m <-> x || a)
66 65 imeq2d 
m = a -> (0 < x /\ x <= a1 -> x || m <-> 0 < x /\ x <= a1 -> x || a)
67 66 aleqd 
m = a -> (A. x (0 < x /\ x <= a1 -> x || m) <-> A. x (0 < x /\ x <= a1 -> x || a))
68 64, 67 aneqd 
m = a -> (0 < m /\ A. x (0 < x /\ x <= a1 -> x || m) <-> suc 0 <= a /\ A. x (0 < x /\ x <= a1 -> x || a))
69 68 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))
70 leeq2 
m = a * suc a1 -> (suc 0 <= m <-> suc 0 <= a * suc a1)
71 70 conv lt 
m = a * suc a1 -> (0 < m <-> suc 0 <= a * suc a1)
72 dvdeq2 
m = a * suc a1 -> (x || m <-> x || a * suc a1)
73 72 imeq2d 
m = a * suc a1 -> (0 < x /\ x <= suc a1 -> x || m <-> 0 < x /\ x <= suc a1 -> x || a * suc a1)
74 73 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))
75 71, 74 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))
76 75 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))
77 mulpos 
0 < a * suc a1 <-> 0 < a /\ 0 < suc a1
78 77 conv lt 
suc 0 <= a * suc a1 <-> 0 < a /\ 0 < suc a1
79 anl 
suc 0 <= a /\ A. x (0 < x /\ x <= a1 -> x || a) -> suc 0 <= a
80 79 conv lt 
suc 0 <= a /\ A. x (0 < x /\ x <= a1 -> x || a) -> 0 < a
81 lt01S 
0 < suc a1
82 81 a1i 
suc 0 <= a /\ A. x (0 < x /\ x <= a1 -> x || a) -> 0 < suc a1
83 80, 82 iand 
suc 0 <= a /\ A. x (0 < x /\ x <= a1 -> x || a) -> 0 < a /\ 0 < suc a1
84 78, 83 sylibr 
suc 0 <= a /\ A. x (0 < x /\ x <= a1 -> x || a) -> suc 0 <= a * suc a1
85 impexp 
0 < x /\ x <= a1 -> x || a <-> 0 < x -> x <= a1 -> x || a
86 impexp 
0 < x /\ x <= suc a1 -> x || a * suc a1 <-> 0 < x -> x <= suc a1 -> x || a * suc a1
87 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
88 leloe 
x <= suc a1 <-> x < suc a1 \/ x = suc a1
89 leltsuc 
x <= a1 <-> x < suc a1
90 dvdmul11 
x || a -> x || a * suc a1
91 90 imim2i 
(x <= a1 -> x || a) -> x <= a1 -> x || a * suc a1
92 89, 91 syl5bir 
(x <= a1 -> x || a) -> x < suc a1 -> x || a * suc a1
93 dvdmul1 
x || a * x
94 muleq2 
x = suc a1 -> a * x = a * suc a1
95 94 dvdeq2d 
x = suc a1 -> (x || a * x <-> x || a * suc a1)
96 93, 95 mpbii 
x = suc a1 -> x || a * suc a1
97 96 a1i 
(x <= a1 -> x || a) -> x = suc a1 -> x || a * suc a1
98 92, 97 eord 
(x <= a1 -> x || a) -> x < suc a1 \/ x = suc a1 -> x || a * suc a1
99 88, 98 syl5bi 
(x <= a1 -> x || a) -> x <= suc a1 -> x || a * suc a1
100 87, 99 ax_mp 
(0 < x -> x <= a1 -> x || a) -> 0 < x -> x <= suc a1 -> x || a * suc a1
101 86, 100 sylibr 
(0 < x -> x <= a1 -> x || a) -> 0 < x /\ x <= suc a1 -> x || a * suc a1
102 85, 101 sylbi 
(0 < x /\ x <= a1 -> x || a) -> 0 < x /\ x <= suc a1 -> x || a * suc a1
103 102 alimi 
A. x (0 < x /\ x <= a1 -> x || a) -> A. x (0 < x /\ x <= suc a1 -> x || a * suc a1)
104 103 anwr 
suc 0 <= a /\ A. x (0 < x /\ x <= a1 -> x || a) -> A. x (0 < x /\ x <= suc a1 -> x || a * suc a1)
105 76, 84, 104 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))
106 105 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))
107 69, 106 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))
108 11, 22, 33, 44, 62, 107 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)