psetsep - ../examples/peano.mm1

Step	Hyp	Ref	Expression
1		biidd	_1 = n -> (0 < a <-> 0 < a)
2		eqsidd	_1 = n -> pset (m, a) == pset (m, a)
3		eqidd	_1 = n -> x = x
4		id	_1 = n -> _1 = n
5	3, 4	lteqd	_1 = n -> (x < _1 <-> x < n)
6		biidd	_1 = n -> (p <-> p)
7	5, 6	aneqd	_1 = n -> (x < _1 /\ p <-> x < n /\ p)
8	7	abeqd	_1 = n -> {x \| x < _1 /\ p} == {x \| x < n /\ p}
9	2, 8	eqseqd	_1 = n -> (pset (m, a) == {x \| x < _1 /\ p} <-> pset (m, a) == {x \| x < n /\ p})
10	1, 9	aneqd	_1 = n -> (0 < a /\ pset (m, a) == {x \| x < _1 /\ p} <-> 0 < a /\ pset (m, a) == {x \| x < n /\ p})
11	10	exeqd	_1 = n -> (E. a (0 < a /\ pset (m, a) == {x \| x < _1 /\ p}) <-> E. a (0 < a /\ pset (m, a) == {x \| x < n /\ p}))
12		biidd	_1 = 0 -> (0 < a <-> 0 < a)
13		eqsidd	_1 = 0 -> pset (m, a) == pset (m, a)
14		eqidd	_1 = 0 -> x = x
15		id	_1 = 0 -> _1 = 0
16	14, 15	lteqd	_1 = 0 -> (x < _1 <-> x < 0)
17		biidd	_1 = 0 -> (p <-> p)
18	16, 17	aneqd	_1 = 0 -> (x < _1 /\ p <-> x < 0 /\ p)
19	18	abeqd	_1 = 0 -> {x \| x < _1 /\ p} == {x \| x < 0 /\ p}
20	13, 19	eqseqd	_1 = 0 -> (pset (m, a) == {x \| x < _1 /\ p} <-> pset (m, a) == {x \| x < 0 /\ p})
21	12, 20	aneqd	_1 = 0 -> (0 < a /\ pset (m, a) == {x \| x < _1 /\ p} <-> 0 < a /\ pset (m, a) == {x \| x < 0 /\ p})
22	21	exeqd	_1 = 0 -> (E. a (0 < a /\ pset (m, a) == {x \| x < _1 /\ p}) <-> E. a (0 < a /\ pset (m, a) == {x \| x < 0 /\ p}))
23		biidd	_1 = v -> (0 < a <-> 0 < a)
24		eqsidd	_1 = v -> pset (m, a) == pset (m, a)
25		eqidd	_1 = v -> x = x
26		id	_1 = v -> _1 = v
27	25, 26	lteqd	_1 = v -> (x < _1 <-> x < v)
28		biidd	_1 = v -> (p <-> p)
29	27, 28	aneqd	_1 = v -> (x < _1 /\ p <-> x < v /\ p)
30	29	abeqd	_1 = v -> {x \| x < _1 /\ p} == {x \| x < v /\ p}
31	24, 30	eqseqd	_1 = v -> (pset (m, a) == {x \| x < _1 /\ p} <-> pset (m, a) == {x \| x < v /\ p})
32	23, 31	aneqd	_1 = v -> (0 < a /\ pset (m, a) == {x \| x < _1 /\ p} <-> 0 < a /\ pset (m, a) == {x \| x < v /\ p})
33	32	exeqd	_1 = v -> (E. a (0 < a /\ pset (m, a) == {x \| x < _1 /\ p}) <-> E. a (0 < a /\ pset (m, a) == {x \| x < v /\ p}))
34		biidd	_1 = suc v -> (0 < a <-> 0 < a)
35		eqsidd	_1 = suc v -> pset (m, a) == pset (m, a)
36		eqidd	_1 = suc v -> x = x
37		id	_1 = suc v -> _1 = suc v
38	36, 37	lteqd	_1 = suc v -> (x < _1 <-> x < suc v)
39		biidd	_1 = suc v -> (p <-> p)
40	38, 39	aneqd	_1 = suc v -> (x < _1 /\ p <-> x < suc v /\ p)
41	40	abeqd	_1 = suc v -> {x \| x < _1 /\ p} == {x \| x < suc v /\ p}
42	35, 41	eqseqd	_1 = suc v -> (pset (m, a) == {x \| x < _1 /\ p} <-> pset (m, a) == {x \| x < suc v /\ p})
43	34, 42	aneqd	_1 = suc v -> (0 < a /\ pset (m, a) == {x \| x < _1 /\ p} <-> 0 < a /\ pset (m, a) == {x \| x < suc v /\ p})
44	43	exeqd	_1 = suc v -> (E. a (0 < a /\ pset (m, a) == {x \| x < _1 /\ p}) <-> E. a (0 < a /\ pset (m, a) == {x \| x < suc v /\ p}))
45		lteq2	a = 1 -> (0 < a <-> 0 < 1)
46		preq2	a = 1 -> m, a = m, 1
47	46	pseteqd	a = 1 -> pset (m, a) == pset (m, 1)
48	47	eqseq1d	a = 1 -> (pset (m, a) == {x \| x < 0 /\ p} <-> pset (m, 1) == {x \| x < 0 /\ p})
49	45, 48	aneqd	a = 1 -> (0 < a /\ pset (m, a) == {x \| x < 0 /\ p} <-> 0 < 1 /\ pset (m, 1) == {x \| x < 0 /\ p})
50	49	iexe	0 < 1 /\ pset (m, 1) == {x \| x < 0 /\ p} -> E. a (0 < a /\ pset (m, a) == {x \| x < 0 /\ p})
51		ian	0 < 1 -> pset (m, 1) == {x \| x < 0 /\ p} -> 0 < 1 /\ pset (m, 1) == {x \| x < 0 /\ p}
52		d0lt1	0 < 1
53	51, 52	ax_mp	pset (m, 1) == {x \| x < 0 /\ p} -> 0 < 1 /\ pset (m, 1) == {x \| x < 0 /\ p}
54		binth	~x e. pset (m, 1) -> ~(x < 0 /\ p) -> (x e. pset (m, 1) <-> x < 0 /\ p)
55		elpset1	~x e. pset (m, 1)
56	54, 55	ax_mp	~(x < 0 /\ p) -> (x e. pset (m, 1) <-> x < 0 /\ p)
57		anl	x < 0 /\ p -> x < 0
58		lt02	~x < 0
59	57, 58	mt	~(x < 0 /\ p)
60	56, 59	ax_mp	x e. pset (m, 1) <-> x < 0 /\ p
61	60	eqab2i	pset (m, 1) == {x \| x < 0 /\ p}
62	53, 61	ax_mp	0 < 1 /\ pset (m, 1) == {x \| x < 0 /\ p}
63	50, 62	ax_mp	E. a (0 < a /\ pset (m, a) == {x \| x < 0 /\ p})
64	63	a1i	0 < m /\ A. x (0 < x /\ x <= n -> x \|\| m) -> E. a (0 < a /\ pset (m, a) == {x \| x < 0 /\ p})
65		lteq2	a = b -> (0 < a <-> 0 < b)
66		preq2	a = b -> m, a = m, b
67	66	pseteqd	a = b -> pset (m, a) == pset (m, b)
68	67	eqseq1d	a = b -> (pset (m, a) == {x \| x < suc v /\ p} <-> pset (m, b) == {x \| x < suc v /\ p})
69	65, 68	aneqd	a = b -> (0 < a /\ pset (m, a) == {x \| x < suc v /\ p} <-> 0 < b /\ pset (m, b) == {x \| x < suc v /\ p})
70	69	cbvex	E. a (0 < a /\ pset (m, a) == {x \| x < suc v /\ p}) <-> E. b (0 < b /\ pset (m, b) == {x \| x < suc v /\ p})
71		lteq2	b = a * suc (m * suc v) -> (0 < b <-> 0 < a * suc (m * suc v))
72		preq2	b = a * suc (m * suc v) -> m, b = m, a * suc (m * suc v)
73	72	pseteqd	b = a * suc (m * suc v) -> pset (m, b) == pset (m, a * suc (m * suc v))
74	73	eqseq1d	b = a * suc (m * suc v) -> (pset (m, b) == {x \| x < suc v /\ p} <-> pset (m, a * suc (m * suc v)) == {x \| x < suc v /\ p})
75	71, 74	aneqd	b = a * suc (m * suc v) -> (0 < b /\ pset (m, b) == {x \| x < suc v /\ p} <-> 0 < a * suc (m * suc v) /\ pset (m, a * suc (m * suc v)) == {x \| x < suc v /\ p})
76	75	iexe	0 < a * suc (m * suc v) /\ pset (m, a * suc (m * suc v)) == {x \| x < suc v /\ p} -> E. b (0 < b /\ pset (m, b) == {x \| x < suc v /\ p})
77		mulpos	0 < a * suc (m * suc v) <-> 0 < a /\ 0 < suc (m * suc v)
78		anrl	0 < m /\ A. x (0 < x /\ x <= n -> x \|\| m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x \| x < v /\ p}) -> 0 < a
79		lt01S	0 < suc (m * suc v)
80	79	a1i	0 < m /\ A. x (0 < x /\ x <= n -> x \|\| m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x \| x < v /\ p}) -> 0 < suc (m * suc v)
81	78, 80	iand	0 < m /\ A. x (0 < x /\ x <= n -> x \|\| m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x \| x < v /\ p}) -> 0 < a /\ 0 < suc (m * suc v)
82	77, 81	sylibr	0 < m /\ A. x (0 < x /\ x <= n -> x \|\| m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x \| x < v /\ p}) -> 0 < a * suc (m * suc v)
83		bitr	(y e. {x \| x < suc v /\ p} <-> [y / x] (x < suc v /\ p)) -> ([y / x] (x < suc v /\ p) <-> y < suc v /\ [y / x] p) -> (y e. {x \| x < suc v /\ p} <-> y < suc v /\ [y / x] p)
84		elab	y e. {x \| x < suc v /\ p} <-> [y / x] (x < suc v /\ p)
85	83, 84	ax_mp	([y / x] (x < suc v /\ p) <-> y < suc v /\ [y / x] p) -> (y e. {x \| x < suc v /\ p} <-> y < suc v /\ [y / x] p)
86		nfv	F/ x y < suc v
87		nfsb1	F/ x [y / x] p
88	86, 87	nfan	F/ x y < suc v /\ [y / x] p
89		lteq1	x = y -> (x < suc v <-> y < suc v)
90		sbq	x = y -> (p <-> [y / x] p)
91	89, 90	aneqd	x = y -> (x < suc v /\ p <-> y < suc v /\ [y / x] p)
92	88, 91	sbeh	[y / x] (x < suc v /\ p) <-> y < suc v /\ [y / x] p
93	85, 92	ax_mp	y e. {x \| x < suc v /\ p} <-> y < suc v /\ [y / x] p
94		an3l	0 < m /\ A. x (0 < x /\ x <= n -> x \|\| m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x \| x < v /\ p}) -> 0 < m /\ A. x (0 < x /\ x <= n -> x \|\| m)
95	94	anld	0 < m /\ A. x (0 < x /\ x <= n -> x \|\| m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x \| x < v /\ p}) -> 0 < m
96		lteq2	x = z -> (0 < x <-> 0 < z)
97		leeq1	x = z -> (x <= v <-> z <= v)
98	96, 97	aneqd	x = z -> (0 < x /\ x <= v <-> 0 < z /\ z <= v)
99		dvdeq1	x = z -> (x \|\| m <-> z \|\| m)
100	98, 99	imeqd	x = z -> (0 < x /\ x <= v -> x \|\| m <-> 0 < z /\ z <= v -> z \|\| m)
101	100	cbval	A. x (0 < x /\ x <= v -> x \|\| m) <-> A. z (0 < z /\ z <= v -> z \|\| m)
102	94	anrd	0 < m /\ A. x (0 < x /\ x <= n -> x \|\| m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x \| x < v /\ p}) -> A. x (0 < x /\ x <= n -> x \|\| m)
103		letr	v <= suc v -> suc v <= n -> v <= n
104		lesucid	v <= suc v
105	103, 104	ax_mp	suc v <= n -> v <= n
106		anllr	0 < m /\ A. x (0 < x /\ x <= n -> x \|\| m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x \| x < v /\ p}) -> v < n
107	106	conv lt	0 < m /\ A. x (0 < x /\ x <= n -> x \|\| m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x \| x < v /\ p}) -> suc v <= n
108	105, 107	syl	0 < m /\ A. x (0 < x /\ x <= n -> x \|\| m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x \| x < v /\ p}) -> v <= n
109		letr	x <= v -> v <= n -> x <= n
110	109	com12	v <= n -> x <= v -> x <= n
111	110	anim2d	v <= n -> 0 < x /\ x <= v -> 0 < x /\ x <= n
112	111	imim1d	v <= n -> (0 < x /\ x <= n -> x \|\| m) -> 0 < x /\ x <= v -> x \|\| m
113	112	alimd	v <= n -> A. x (0 < x /\ x <= n -> x \|\| m) -> A. x (0 < x /\ x <= v -> x \|\| m)
114	108, 113	rsyl	0 < m /\ A. x (0 < x /\ x <= n -> x \|\| m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x \| x < v /\ p}) -> A. x (0 < x /\ x <= n -> x \|\| m) -> A. x (0 < x /\ x <= v -> x \|\| m)
115	102, 114	mpd	0 < m /\ A. x (0 < x /\ x <= n -> x \|\| m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x \| x < v /\ p}) -> A. x (0 < x /\ x <= v -> x \|\| m)
116	101, 115	sylib	0 < m /\ A. x (0 < x /\ x <= n -> x \|\| m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x \| x < v /\ p}) -> A. z (0 < z /\ z <= v -> z \|\| m)
117	95, 78, 116	psetS	0 < m /\ A. x (0 < x /\ x <= n -> x \|\| m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x \| x < v /\ p}) -> (y e. pset (m, a * suc (m * suc v)) <-> y e. pset (m, a) \/ y = v)
118		bitr	(y e. {x \| x < v /\ p} <-> [y / x] (x < v /\ p)) -> ([y / x] (x < v /\ p) <-> y < v /\ [y / x] p) -> (y e. {x \| x < v /\ p} <-> y < v /\ [y / x] p)
119		elab	y e. {x \| x < v /\ p} <-> [y / x] (x < v /\ p)
120	118, 119	ax_mp	([y / x] (x < v /\ p) <-> y < v /\ [y / x] p) -> (y e. {x \| x < v /\ p} <-> y < v /\ [y / x] p)
121		nfv	F/ x y < v
122	121, 87	nfan	F/ x y < v /\ [y / x] p
123		lteq1	x = y -> (x < v <-> y < v)
124	123, 90	aneqd	x = y -> (x < v /\ p <-> y < v /\ [y / x] p)
125	122, 124	sbeh	[y / x] (x < v /\ p) <-> y < v /\ [y / x] p
126	120, 125	ax_mp	y e. {x \| x < v /\ p} <-> y < v /\ [y / x] p
127		anrr	0 < m /\ A. x (0 < x /\ x <= n -> x \|\| m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x \| x < v /\ p}) -> pset (m, a) == {x \| x < v /\ p}
128	127	eleq2d	0 < m /\ A. x (0 < x /\ x <= n -> x \|\| m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x \| x < v /\ p}) -> (y e. pset (m, a) <-> y e. {x \| x < v /\ p})
129	126, 128	syl6bb	0 < m /\ A. x (0 < x /\ x <= n -> x \|\| m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x \| x < v /\ p}) -> (y e. pset (m, a) <-> y < v /\ [y / x] p)
130	129	oreq1d	0 < m /\ A. x (0 < x /\ x <= n -> x \|\| m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x \| x < v /\ p}) -> (y e. pset (m, a) \/ y = v <-> y < v /\ [y / x] p \/ y = v)
131		bitr	(y < suc v /\ [y / x] p <-> (y < v \/ y = v) /\ [y / x] p) -> ((y < v \/ y = v) /\ [y / x] p <-> y < v /\ [y / x] p \/ y = v /\ [v / x] p) -> (y < suc v /\ [y / x] p <-> y < v /\ [y / x] p \/ y = v /\ [v / x] p)
132		bitr3	(y <= v <-> y < suc v) -> (y <= v <-> y < v \/ y = v) -> (y < suc v <-> y < v \/ y = v)
133		leltsuc	y <= v <-> y < suc v
134	132, 133	ax_mp	(y <= v <-> y < v \/ y = v) -> (y < suc v <-> y < v \/ y = v)
135		leloe	y <= v <-> y < v \/ y = v
136	134, 135	ax_mp	y < suc v <-> y < v \/ y = v
137	136	aneq1i	y < suc v /\ [y / x] p <-> (y < v \/ y = v) /\ [y / x] p
138	131, 137	ax_mp	((y < v \/ y = v) /\ [y / x] p <-> y < v /\ [y / x] p \/ y = v /\ [v / x] p) -> (y < suc v /\ [y / x] p <-> y < v /\ [y / x] p \/ y = v /\ [v / x] p)
139		bitr	((y < v \/ y = v) /\ [y / x] p <-> y < v /\ [y / x] p \/ y = v /\ [y / x] p) -> (y < v /\ [y / x] p \/ y = v /\ [y / x] p <-> y < v /\ [y / x] p \/ y = v /\ [v / x] p) -> ((y < v \/ y = v) /\ [y / x] p <-> y < v /\ [y / x] p \/ y = v /\ [v / x] p)
140		andir	(y < v \/ y = v) /\ [y / x] p <-> y < v /\ [y / x] p \/ y = v /\ [y / x] p
141	139, 140	ax_mp	(y < v /\ [y / x] p \/ y = v /\ [y / x] p <-> y < v /\ [y / x] p \/ y = v /\ [v / x] p) -> ((y < v \/ y = v) /\ [y / x] p <-> y < v /\ [y / x] p \/ y = v /\ [v / x] p)
142		aneq2a	(y = v -> ([y / x] p <-> [v / x] p)) -> (y = v /\ [y / x] p <-> y = v /\ [v / x] p)
143		sbeq1	y = v -> ([y / x] p <-> [v / x] p)
144	142, 143	ax_mp	y = v /\ [y / x] p <-> y = v /\ [v / x] p
145	144	oreq2i	y < v /\ [y / x] p \/ y = v /\ [y / x] p <-> y < v /\ [y / x] p \/ y = v /\ [v / x] p
146	141, 145	ax_mp	(y < v \/ y = v) /\ [y / x] p <-> y < v /\ [y / x] p \/ y = v /\ [v / x] p
147	138, 146	ax_mp	y < suc v /\ [y / x] p <-> y < v /\ [y / x] p \/ y = v /\ [v / x] p
148		bian2	[v / x] p -> (y = v /\ [v / x] p <-> y = v)
149		anlr	0 < m /\ A. x (0 < x /\ x <= n -> x \|\| m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x \| x < v /\ p}) -> [v / x] p
150	148, 149	syl	0 < m /\ A. x (0 < x /\ x <= n -> x \|\| m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x \| x < v /\ p}) -> (y = v /\ [v / x] p <-> y = v)
151	150	oreq2d	0 < m /\ A. x (0 < x /\ x <= n -> x \|\| m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x \| x < v /\ p}) -> (y < v /\ [y / x] p \/ y = v /\ [v / x] p <-> y < v /\ [y / x] p \/ y = v)
152	147, 151	syl5bb	0 < m /\ A. x (0 < x /\ x <= n -> x \|\| m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x \| x < v /\ p}) -> (y < suc v /\ [y / x] p <-> y < v /\ [y / x] p \/ y = v)
153	130, 152	bitr4d	0 < m /\ A. x (0 < x /\ x <= n -> x \|\| m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x \| x < v /\ p}) -> (y e. pset (m, a) \/ y = v <-> y < suc v /\ [y / x] p)
154	117, 153	bitrd	0 < m /\ A. x (0 < x /\ x <= n -> x \|\| m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x \| x < v /\ p}) -> (y e. pset (m, a * suc (m * suc v)) <-> y < suc v /\ [y / x] p)
155	93, 154	syl6bbr	0 < m /\ A. x (0 < x /\ x <= n -> x \|\| m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x \| x < v /\ p}) -> (y e. pset (m, a * suc (m * suc v)) <-> y e. {x \| x < suc v /\ p})
156	155	eqrd	0 < m /\ A. x (0 < x /\ x <= n -> x \|\| m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x \| x < v /\ p}) -> pset (m, a * suc (m * suc v)) == {x \| x < suc v /\ p}
157	82, 156	iand	0 < m /\ A. x (0 < x /\ x <= n -> x \|\| m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x \| x < v /\ p}) -> 0 < a * suc (m * suc v) /\ pset (m, a * suc (m * suc v)) == {x \| x < suc v /\ p}
158	76, 157	syl	0 < m /\ A. x (0 < x /\ x <= n -> x \|\| m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x \| x < v /\ p}) -> E. b (0 < b /\ pset (m, b) == {x \| x < suc v /\ p})
159	158	eexda	0 < m /\ A. x (0 < x /\ x <= n -> x \|\| m) /\ v < n /\ [v / x] p -> E. a (0 < a /\ pset (m, a) == {x \| x < v /\ p}) -> E. b (0 < b /\ pset (m, b) == {x \| x < suc v /\ p})
160	70, 159	syl6ibr	0 < m /\ A. x (0 < x /\ x <= n -> x \|\| m) /\ v < n /\ [v / x] p -> E. a (0 < a /\ pset (m, a) == {x \| x < v /\ p}) -> E. a (0 < a /\ pset (m, a) == {x \| x < suc v /\ p})
161		bior2	~(y = v /\ [v / x] p) -> (y < v /\ [y / x] p \/ y = v /\ [v / x] p <-> y < v /\ [y / x] p)
162		con3	(y = v /\ [v / x] p -> [v / x] p) -> ~[v / x] p -> ~(y = v /\ [v / x] p)
163		anr	y = v /\ [v / x] p -> [v / x] p
164	162, 163	ax_mp	~[v / x] p -> ~(y = v /\ [v / x] p)
165	164	anwr	0 < m /\ A. x (0 < x /\ x <= n -> x \|\| m) /\ v < n /\ ~[v / x] p -> ~(y = v /\ [v / x] p)
166	161, 165	syl	0 < m /\ A. x (0 < x /\ x <= n -> x \|\| m) /\ v < n /\ ~[v / x] p -> (y < v /\ [y / x] p \/ y = v /\ [v / x] p <-> y < v /\ [y / x] p)
167	147, 166	syl5bb	0 < m /\ A. x (0 < x /\ x <= n -> x \|\| m) /\ v < n /\ ~[v / x] p -> (y < suc v /\ [y / x] p <-> y < v /\ [y / x] p)
168	126, 167	syl6bbr	0 < m /\ A. x (0 < x /\ x <= n -> x \|\| m) /\ v < n /\ ~[v / x] p -> (y < suc v /\ [y / x] p <-> y e. {x \| x < v /\ p})
169	93, 168	syl5bb	0 < m /\ A. x (0 < x /\ x <= n -> x \|\| m) /\ v < n /\ ~[v / x] p -> (y e. {x \| x < suc v /\ p} <-> y e. {x \| x < v /\ p})
170	169	eqrd	0 < m /\ A. x (0 < x /\ x <= n -> x \|\| m) /\ v < n /\ ~[v / x] p -> {x \| x < suc v /\ p} == {x \| x < v /\ p}
171	170	eqseq2d	0 < m /\ A. x (0 < x /\ x <= n -> x \|\| m) /\ v < n /\ ~[v / x] p -> (pset (m, a) == {x \| x < suc v /\ p} <-> pset (m, a) == {x \| x < v /\ p})
172	171	aneq2d	0 < m /\ A. x (0 < x /\ x <= n -> x \|\| m) /\ v < n /\ ~[v / x] p -> (0 < a /\ pset (m, a) == {x \| x < suc v /\ p} <-> 0 < a /\ pset (m, a) == {x \| x < v /\ p})
173	172	exeqd	0 < m /\ A. x (0 < x /\ x <= n -> x \|\| m) /\ v < n /\ ~[v / x] p -> (E. a (0 < a /\ pset (m, a) == {x \| x < suc v /\ p}) <-> E. a (0 < a /\ pset (m, a) == {x \| x < v /\ p}))
174	173	bi2d	0 < m /\ A. x (0 < x /\ x <= n -> x \|\| m) /\ v < n /\ ~[v / x] p -> E. a (0 < a /\ pset (m, a) == {x \| x < v /\ p}) -> E. a (0 < a /\ pset (m, a) == {x \| x < suc v /\ p})
175	160, 174	casesda	0 < m /\ A. x (0 < x /\ x <= n -> x \|\| m) /\ v < n -> E. a (0 < a /\ pset (m, a) == {x \| x < v /\ p}) -> E. a (0 < a /\ pset (m, a) == {x \| x < suc v /\ p})
176	175	imp	0 < m /\ A. x (0 < x /\ x <= n -> x \|\| m) /\ v < n /\ E. a (0 < a /\ pset (m, a) == {x \| x < v /\ p}) -> E. a (0 < a /\ pset (m, a) == {x \| x < suc v /\ p})
177	11, 22, 33, 44, 64, 176	indlt	0 < m /\ A. x (0 < x /\ x <= n -> x \|\| m) -> E. a (0 < a /\ pset (m, a) == {x \| x < n /\ p})
178		pseteq	b = m, a -> pset b == pset (m, a)
179	178	anwr	0 < m /\ A. x (0 < x /\ x <= n -> x \|\| m) /\ (0 < a /\ pset (m, a) == {x \| x < n /\ p}) /\ b = m, a -> pset b == pset (m, a)
180		anrr	0 < m /\ A. x (0 < x /\ x <= n -> x \|\| m) /\ (0 < a /\ pset (m, a) == {x \| x < n /\ p}) -> pset (m, a) == {x \| x < n /\ p}
181	180	anwl	0 < m /\ A. x (0 < x /\ x <= n -> x \|\| m) /\ (0 < a /\ pset (m, a) == {x \| x < n /\ p}) /\ b = m, a -> pset (m, a) == {x \| x < n /\ p}
182	179, 181	eqstrd	0 < m /\ A. x (0 < x /\ x <= n -> x \|\| m) /\ (0 < a /\ pset (m, a) == {x \| x < n /\ p}) /\ b = m, a -> pset b == {x \| x < n /\ p}
183	182	iexde	0 < m /\ A. x (0 < x /\ x <= n -> x \|\| m) /\ (0 < a /\ pset (m, a) == {x \| x < n /\ p}) -> E. b pset b == {x \| x < n /\ p}
184	183	eexda	0 < m /\ A. x (0 < x /\ x <= n -> x \|\| m) -> E. a (0 < a /\ pset (m, a) == {x \| x < n /\ p}) -> E. b pset b == {x \| x < n /\ p}
185	177, 184	mpd	0 < m /\ A. x (0 < x /\ x <= n -> x \|\| m) -> E. b pset b == {x \| x < n /\ p}
186	185	eex	E. m (0 < m /\ A. x (0 < x /\ x <= n -> x \|\| m)) -> E. b pset b == {x \| x < n /\ p}
187		lcmex	E. m (0 < m /\ A. x (0 < x /\ x <= n -> x \|\| m))
188	186, 187	ax_mp	E. b pset b == {x \| x < n /\ p}

1

_1 = n -> (0 < a <-> 0 < a)

2

eqsidd

_1 = n -> pset (m, a) == pset (m, a)

3

eqidd

_1 = n -> x = x

4

id

_1 = n -> _1 = n

5

3, 4

lteqd

_1 = n -> (x < _1 <-> x < n)

6

biidd

_1 = n -> (p <-> p)

7

5, 6

aneqd

_1 = n -> (x < _1 /\ p <-> x < n /\ p)

8

7

abeqd

_1 = n -> {x | x < _1 /\ p} == {x | x < n /\ p}

9

2, 8

eqseqd

_1 = n -> (pset (m, a) == {x | x < _1 /\ p} <-> pset (m, a) == {x | x < n /\ p})

10

1, 9

aneqd

_1 = n -> (0 < a /\ pset (m, a) == {x | x < _1 /\ p} <-> 0 < a /\ pset (m, a) == {x | x < n /\ p})

11

10

exeqd

_1 = n -> (E. a (0 < a /\ pset (m, a) == {x | x < _1 /\ p}) <-> E. a (0 < a /\ pset (m, a) == {x | x < n /\ p}))

12

biidd

_1 = 0 -> (0 < a <-> 0 < a)

13

eqsidd

_1 = 0 -> pset (m, a) == pset (m, a)

14

eqidd

_1 = 0 -> x = x

15

id

_1 = 0 -> _1 = 0

16

14, 15

lteqd

_1 = 0 -> (x < _1 <-> x < 0)

17

biidd

_1 = 0 -> (p <-> p)

18

16, 17

aneqd

_1 = 0 -> (x < _1 /\ p <-> x < 0 /\ p)

19

18

abeqd

_1 = 0 -> {x | x < _1 /\ p} == {x | x < 0 /\ p}

20

13, 19

eqseqd

_1 = 0 -> (pset (m, a) == {x | x < _1 /\ p} <-> pset (m, a) == {x | x < 0 /\ p})

21

12, 20

aneqd

_1 = 0 -> (0 < a /\ pset (m, a) == {x | x < _1 /\ p} <-> 0 < a /\ pset (m, a) == {x | x < 0 /\ p})

22

21

exeqd

_1 = 0 -> (E. a (0 < a /\ pset (m, a) == {x | x < _1 /\ p}) <-> E. a (0 < a /\ pset (m, a) == {x | x < 0 /\ p}))

23

biidd

_1 = v -> (0 < a <-> 0 < a)

24

eqsidd

_1 = v -> pset (m, a) == pset (m, a)

25

eqidd

_1 = v -> x = x

26

id

_1 = v -> _1 = v

27

25, 26

lteqd

_1 = v -> (x < _1 <-> x < v)

28

biidd

_1 = v -> (p <-> p)

29

27, 28

aneqd

_1 = v -> (x < _1 /\ p <-> x < v /\ p)

30

29

abeqd

_1 = v -> {x | x < _1 /\ p} == {x | x < v /\ p}

31

24, 30

eqseqd

_1 = v -> (pset (m, a) == {x | x < _1 /\ p} <-> pset (m, a) == {x | x < v /\ p})

32

23, 31

aneqd

_1 = v -> (0 < a /\ pset (m, a) == {x | x < _1 /\ p} <-> 0 < a /\ pset (m, a) == {x | x < v /\ p})

33

32

exeqd

_1 = v -> (E. a (0 < a /\ pset (m, a) == {x | x < _1 /\ p}) <-> E. a (0 < a /\ pset (m, a) == {x | x < v /\ p}))

34

biidd

_1 = suc v -> (0 < a <-> 0 < a)

35

eqsidd

_1 = suc v -> pset (m, a) == pset (m, a)

36

eqidd

_1 = suc v -> x = x

37

id

_1 = suc v -> _1 = suc v

38

36, 37

lteqd

_1 = suc v -> (x < _1 <-> x < suc v)

39

biidd

_1 = suc v -> (p <-> p)

40

38, 39

aneqd

_1 = suc v -> (x < _1 /\ p <-> x < suc v /\ p)

41

40

abeqd

_1 = suc v -> {x | x < _1 /\ p} == {x | x < suc v /\ p}

42

35, 41

eqseqd

_1 = suc v -> (pset (m, a) == {x | x < _1 /\ p} <-> pset (m, a) == {x | x < suc v /\ p})

43

34, 42

aneqd

_1 = suc v -> (0 < a /\ pset (m, a) == {x | x < _1 /\ p} <-> 0 < a /\ pset (m, a) == {x | x < suc v /\ p})

44

43

exeqd

_1 = suc v -> (E. a (0 < a /\ pset (m, a) == {x | x < _1 /\ p}) <-> E. a (0 < a /\ pset (m, a) == {x | x < suc v /\ p}))

45

lteq2

a = 1 -> (0 < a <-> 0 < 1)

46

preq2

a = 1 -> m, a = m, 1

47

46

pseteqd

a = 1 -> pset (m, a) == pset (m, 1)

48

47

eqseq1d

a = 1 -> (pset (m, a) == {x | x < 0 /\ p} <-> pset (m, 1) == {x | x < 0 /\ p})

49

45, 48

aneqd

a = 1 -> (0 < a /\ pset (m, a) == {x | x < 0 /\ p} <-> 0 < 1 /\ pset (m, 1) == {x | x < 0 /\ p})

50

49

iexe

0 < 1 /\ pset (m, 1) == {x | x < 0 /\ p} -> E. a (0 < a /\ pset (m, a) == {x | x < 0 /\ p})

51

ian

0 < 1 -> pset (m, 1) == {x | x < 0 /\ p} -> 0 < 1 /\ pset (m, 1) == {x | x < 0 /\ p}

52

d0lt1

0 < 1

53

51, 52

ax_mp

pset (m, 1) == {x | x < 0 /\ p} -> 0 < 1 /\ pset (m, 1) == {x | x < 0 /\ p}

54

binth

~x e. pset (m, 1) -> ~(x < 0 /\ p) -> (x e. pset (m, 1) <-> x < 0 /\ p)

55

elpset1

~x e. pset (m, 1)

56

54, 55

ax_mp

~(x < 0 /\ p) -> (x e. pset (m, 1) <-> x < 0 /\ p)

57

anl

x < 0 /\ p -> x < 0

58

lt02

~x < 0

59

57, 58

mt

~(x < 0 /\ p)

60

56, 59

ax_mp

x e. pset (m, 1) <-> x < 0 /\ p

61

60

eqab2i

pset (m, 1) == {x | x < 0 /\ p}

62

53, 61

ax_mp

0 < 1 /\ pset (m, 1) == {x | x < 0 /\ p}

63

50, 62

ax_mp

E. a (0 < a /\ pset (m, a) == {x | x < 0 /\ p})

64

63

a1i

0 < m /\ A. x (0 < x /\ x <= n -> x || m) -> E. a (0 < a /\ pset (m, a) == {x | x < 0 /\ p})

65

lteq2

a = b -> (0 < a <-> 0 < b)

66

preq2

a = b -> m, a = m, b

67

66

pseteqd

a = b -> pset (m, a) == pset (m, b)

68

67

eqseq1d

a = b -> (pset (m, a) == {x | x < suc v /\ p} <-> pset (m, b) == {x | x < suc v /\ p})

69

65, 68

aneqd

a = b -> (0 < a /\ pset (m, a) == {x | x < suc v /\ p} <-> 0 < b /\ pset (m, b) == {x | x < suc v /\ p})

70

69

cbvex

E. a (0 < a /\ pset (m, a) == {x | x < suc v /\ p}) <-> E. b (0 < b /\ pset (m, b) == {x | x < suc v /\ p})

71

lteq2

b = a * suc (m * suc v) -> (0 < b <-> 0 < a * suc (m * suc v))

72

preq2

b = a * suc (m * suc v) -> m, b = m, a * suc (m * suc v)

73

72

pseteqd

b = a * suc (m * suc v) -> pset (m, b) == pset (m, a * suc (m * suc v))

74

73

eqseq1d

b = a * suc (m * suc v) -> (pset (m, b) == {x | x < suc v /\ p} <-> pset (m, a * suc (m * suc v)) == {x | x < suc v /\ p})

75

71, 74

aneqd

b = a * suc (m * suc v) -> (0 < b /\ pset (m, b) == {x | x < suc v /\ p} <-> 0 < a * suc (m * suc v) /\ pset (m, a * suc (m * suc v)) == {x | x < suc v /\ p})

76

75

iexe

0 < a * suc (m * suc v) /\ pset (m, a * suc (m * suc v)) == {x | x < suc v /\ p} -> E. b (0 < b /\ pset (m, b) == {x | x < suc v /\ p})

77

mulpos

0 < a * suc (m * suc v) <-> 0 < a /\ 0 < suc (m * suc v)

78

anrl

0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x | x < v /\ p}) -> 0 < a

79

lt01S

0 < suc (m * suc v)

80

79

a1i

0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x | x < v /\ p}) -> 0 < suc (m * suc v)

81

78, 80

iand

0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x | x < v /\ p}) -> 0 < a /\ 0 < suc (m * suc v)

82

77, 81

sylibr

0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x | x < v /\ p}) -> 0 < a * suc (m * suc v)

83

bitr

(y e. {x | x < suc v /\ p} <-> [y / x] (x < suc v /\ p)) ->
  ([y / x] (x < suc v /\ p) <-> y < suc v /\ [y / x] p) ->
  (y e. {x | x < suc v /\ p} <-> y < suc v /\ [y / x] p)

84

elab

y e. {x | x < suc v /\ p} <-> [y / x] (x < suc v /\ p)

85

83, 84

ax_mp

([y / x] (x < suc v /\ p) <-> y < suc v /\ [y / x] p) -> (y e. {x | x < suc v /\ p} <-> y < suc v /\ [y / x] p)

86

nfv

F/ x y < suc v

87

nfsb1

F/ x [y / x] p

88

86, 87

nfan

F/ x y < suc v /\ [y / x] p

89

lteq1

x = y -> (x < suc v <-> y < suc v)

90

sbq

x = y -> (p <-> [y / x] p)

91

89, 90

aneqd

x = y -> (x < suc v /\ p <-> y < suc v /\ [y / x] p)

92

88, 91

sbeh

[y / x] (x < suc v /\ p) <-> y < suc v /\ [y / x] p

93

85, 92

ax_mp

y e. {x | x < suc v /\ p} <-> y < suc v /\ [y / x] p

94

an3l

0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x | x < v /\ p}) -> 0 < m /\ A. x (0 < x /\ x <= n -> x || m)

95

94

anld

0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x | x < v /\ p}) -> 0 < m

96

lteq2

x = z -> (0 < x <-> 0 < z)

97

leeq1

x = z -> (x <= v <-> z <= v)

98

96, 97

aneqd

x = z -> (0 < x /\ x <= v <-> 0 < z /\ z <= v)

99

dvdeq1

x = z -> (x || m <-> z || m)

100

98, 99

imeqd

x = z -> (0 < x /\ x <= v -> x || m <-> 0 < z /\ z <= v -> z || m)

101

100

cbval

A. x (0 < x /\ x <= v -> x || m) <-> A. z (0 < z /\ z <= v -> z || m)

102

94

anrd

0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x | x < v /\ p}) -> A. x (0 < x /\ x <= n -> x || m)

103

letr

v <= suc v -> suc v <= n -> v <= n

104

lesucid

v <= suc v

105

103, 104

ax_mp

suc v <= n -> v <= n

106

anllr

0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x | x < v /\ p}) -> v < n

108

105, 107

syl

0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x | x < v /\ p}) -> v <= n

109

letr

x <= v -> v <= n -> x <= n

110

109

com12

v <= n -> x <= v -> x <= n

111

110

anim2d

v <= n -> 0 < x /\ x <= v -> 0 < x /\ x <= n

112

111

imim1d

v <= n -> (0 < x /\ x <= n -> x || m) -> 0 < x /\ x <= v -> x || m

113

112

alimd

v <= n -> A. x (0 < x /\ x <= n -> x || m) -> A. x (0 < x /\ x <= v -> x || m)

114

108, 113

rsyl

0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x | x < v /\ p}) ->
  A. x (0 < x /\ x <= n -> x || m) ->
  A. x (0 < x /\ x <= v -> x || m)

115

102, 114

mpd

0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x | x < v /\ p}) -> A. x (0 < x /\ x <= v -> x || m)

116

101, 115

sylib

0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x | x < v /\ p}) -> A. z (0 < z /\ z <= v -> z || m)

117

95, 78, 116

psetS

0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x | x < v /\ p}) ->
  (y e. pset (m, a * suc (m * suc v)) <-> y e. pset (m, a) \/ y = v)

118

bitr

(y e. {x | x < v /\ p} <-> [y / x] (x < v /\ p)) -> ([y / x] (x < v /\ p) <-> y < v /\ [y / x] p) -> (y e. {x | x < v /\ p} <-> y < v /\ [y / x] p)

119

elab

y e. {x | x < v /\ p} <-> [y / x] (x < v /\ p)

120

118, 119

ax_mp

([y / x] (x < v /\ p) <-> y < v /\ [y / x] p) -> (y e. {x | x < v /\ p} <-> y < v /\ [y / x] p)

121

nfv

F/ x y < v

122

121, 87

nfan

F/ x y < v /\ [y / x] p

123

lteq1

x = y -> (x < v <-> y < v)

124

123, 90

aneqd

x = y -> (x < v /\ p <-> y < v /\ [y / x] p)

125

122, 124

sbeh

[y / x] (x < v /\ p) <-> y < v /\ [y / x] p

126

120, 125

ax_mp

y e. {x | x < v /\ p} <-> y < v /\ [y / x] p

127

anrr

0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x | x < v /\ p}) -> pset (m, a) == {x | x < v /\ p}

128

127

eleq2d

0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x | x < v /\ p}) -> (y e. pset (m, a) <-> y e. {x | x < v /\ p})

129

126, 128

syl6bb

0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x | x < v /\ p}) -> (y e. pset (m, a) <-> y < v /\ [y / x] p)

130

129

oreq1d

0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x | x < v /\ p}) ->
  (y e. pset (m, a) \/ y = v <-> y < v /\ [y / x] p \/ y = v)

131

bitr

(y < suc v /\ [y / x] p <-> (y < v \/ y = v) /\ [y / x] p) ->
  ((y < v \/ y = v) /\ [y / x] p <-> y < v /\ [y / x] p \/ y = v /\ [v / x] p) ->
  (y < suc v /\ [y / x] p <-> y < v /\ [y / x] p \/ y = v /\ [v / x] p)

132

bitr3

(y <= v <-> y < suc v) -> (y <= v <-> y < v \/ y = v) -> (y < suc v <-> y < v \/ y = v)

133

leltsuc

y <= v <-> y < suc v

134

132, 133

ax_mp

(y <= v <-> y < v \/ y = v) -> (y < suc v <-> y < v \/ y = v)

135

leloe

y <= v <-> y < v \/ y = v

136

134, 135

ax_mp

y < suc v <-> y < v \/ y = v

137

136

aneq1i

y < suc v /\ [y / x] p <-> (y < v \/ y = v) /\ [y / x] p

138

131, 137

ax_mp

((y < v \/ y = v) /\ [y / x] p <-> y < v /\ [y / x] p \/ y = v /\ [v / x] p) -> (y < suc v /\ [y / x] p <-> y < v /\ [y / x] p \/ y = v /\ [v / x] p)

139

bitr

((y < v \/ y = v) /\ [y / x] p <-> y < v /\ [y / x] p \/ y = v /\ [y / x] p) ->
  (y < v /\ [y / x] p \/ y = v /\ [y / x] p <-> y < v /\ [y / x] p \/ y = v /\ [v / x] p) ->
  ((y < v \/ y = v) /\ [y / x] p <-> y < v /\ [y / x] p \/ y = v /\ [v / x] p)

140

andir

(y < v \/ y = v) /\ [y / x] p <-> y < v /\ [y / x] p \/ y = v /\ [y / x] p

141

139, 140

ax_mp

(y < v /\ [y / x] p \/ y = v /\ [y / x] p <-> y < v /\ [y / x] p \/ y = v /\ [v / x] p) ->
  ((y < v \/ y = v) /\ [y / x] p <-> y < v /\ [y / x] p \/ y = v /\ [v / x] p)

142

aneq2a

(y = v -> ([y / x] p <-> [v / x] p)) -> (y = v /\ [y / x] p <-> y = v /\ [v / x] p)

143

sbeq1

y = v -> ([y / x] p <-> [v / x] p)

144

142, 143

ax_mp

y = v /\ [y / x] p <-> y = v /\ [v / x] p

145

144

oreq2i

y < v /\ [y / x] p \/ y = v /\ [y / x] p <-> y < v /\ [y / x] p \/ y = v /\ [v / x] p

146

141, 145

ax_mp

(y < v \/ y = v) /\ [y / x] p <-> y < v /\ [y / x] p \/ y = v /\ [v / x] p

147

138, 146

ax_mp

y < suc v /\ [y / x] p <-> y < v /\ [y / x] p \/ y = v /\ [v / x] p

148

bian2

[v / x] p -> (y = v /\ [v / x] p <-> y = v)

149

anlr

0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x | x < v /\ p}) -> [v / x] p

150

148, 149

syl

0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x | x < v /\ p}) -> (y = v /\ [v / x] p <-> y = v)

151

150

oreq2d

0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x | x < v /\ p}) ->
  (y < v /\ [y / x] p \/ y = v /\ [v / x] p <-> y < v /\ [y / x] p \/ y = v)

152

147, 151

syl5bb

0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x | x < v /\ p}) ->
  (y < suc v /\ [y / x] p <-> y < v /\ [y / x] p \/ y = v)

153

130, 152

bitr4d

0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x | x < v /\ p}) ->
  (y e. pset (m, a) \/ y = v <-> y < suc v /\ [y / x] p)

154

117, 153

bitrd

0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x | x < v /\ p}) ->
  (y e. pset (m, a * suc (m * suc v)) <-> y < suc v /\ [y / x] p)

155

93, 154

syl6bbr

0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x | x < v /\ p}) ->
  (y e. pset (m, a * suc (m * suc v)) <-> y e. {x | x < suc v /\ p})

156

155

eqrd

0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x | x < v /\ p}) ->
  pset (m, a * suc (m * suc v)) == {x | x < suc v /\ p}

157

82, 156

iand

0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x | x < v /\ p}) ->
  0 < a * suc (m * suc v) /\ pset (m, a * suc (m * suc v)) == {x | x < suc v /\ p}

158

76, 157

syl

0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ [v / x] p /\ (0 < a /\ pset (m, a) == {x | x < v /\ p}) ->
  E. b (0 < b /\ pset (m, b) == {x | x < suc v /\ p})

159

158

eexda

0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ [v / x] p ->
  E. a (0 < a /\ pset (m, a) == {x | x < v /\ p}) ->
  E. b (0 < b /\ pset (m, b) == {x | x < suc v /\ p})

160

70, 159

syl6ibr

0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ [v / x] p ->
  E. a (0 < a /\ pset (m, a) == {x | x < v /\ p}) ->
  E. a (0 < a /\ pset (m, a) == {x | x < suc v /\ p})

161

bior2

~(y = v /\ [v / x] p) -> (y < v /\ [y / x] p \/ y = v /\ [v / x] p <-> y < v /\ [y / x] p)

162

con3

(y = v /\ [v / x] p -> [v / x] p) -> ~[v / x] p -> ~(y = v /\ [v / x] p)

163

anr

y = v /\ [v / x] p -> [v / x] p

164

162, 163

ax_mp

~[v / x] p -> ~(y = v /\ [v / x] p)

165

164

anwr

0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ ~[v / x] p -> ~(y = v /\ [v / x] p)

166

161, 165

syl

0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ ~[v / x] p -> (y < v /\ [y / x] p \/ y = v /\ [v / x] p <-> y < v /\ [y / x] p)

167

147, 166

syl5bb

0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ ~[v / x] p -> (y < suc v /\ [y / x] p <-> y < v /\ [y / x] p)

168

126, 167

syl6bbr

0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ ~[v / x] p -> (y < suc v /\ [y / x] p <-> y e. {x | x < v /\ p})

169

93, 168

syl5bb

0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ ~[v / x] p -> (y e. {x | x < suc v /\ p} <-> y e. {x | x < v /\ p})

170

169

eqrd

0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ ~[v / x] p -> {x | x < suc v /\ p} == {x | x < v /\ p}

171

170

eqseq2d

0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ ~[v / x] p -> (pset (m, a) == {x | x < suc v /\ p} <-> pset (m, a) == {x | x < v /\ p})

172

171

aneq2d

0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ ~[v / x] p -> (0 < a /\ pset (m, a) == {x | x < suc v /\ p} <-> 0 < a /\ pset (m, a) == {x | x < v /\ p})

173

172

exeqd

0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ ~[v / x] p ->
  (E. a (0 < a /\ pset (m, a) == {x | x < suc v /\ p}) <-> E. a (0 < a /\ pset (m, a) == {x | x < v /\ p}))

174

173

bi2d

0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ ~[v / x] p ->
  E. a (0 < a /\ pset (m, a) == {x | x < v /\ p}) ->
  E. a (0 < a /\ pset (m, a) == {x | x < suc v /\ p})

175

160, 174

casesda

0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n -> E. a (0 < a /\ pset (m, a) == {x | x < v /\ p}) -> E. a (0 < a /\ pset (m, a) == {x | x < suc v /\ p})

176

175

imp

0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ v < n /\ E. a (0 < a /\ pset (m, a) == {x | x < v /\ p}) -> E. a (0 < a /\ pset (m, a) == {x | x < suc v /\ p})

177

11, 22, 33, 44, 64, 176

indlt

0 < m /\ A. x (0 < x /\ x <= n -> x || m) -> E. a (0 < a /\ pset (m, a) == {x | x < n /\ p})

178

pseteq

b = m, a -> pset b == pset (m, a)

179

178

anwr

0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ (0 < a /\ pset (m, a) == {x | x < n /\ p}) /\ b = m, a -> pset b == pset (m, a)

180

anrr

0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ (0 < a /\ pset (m, a) == {x | x < n /\ p}) -> pset (m, a) == {x | x < n /\ p}

181

180

anwl

0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ (0 < a /\ pset (m, a) == {x | x < n /\ p}) /\ b = m, a -> pset (m, a) == {x | x < n /\ p}

182

179, 181

eqstrd

0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ (0 < a /\ pset (m, a) == {x | x < n /\ p}) /\ b = m, a -> pset b == {x | x < n /\ p}

183

182

iexde

0 < m /\ A. x (0 < x /\ x <= n -> x || m) /\ (0 < a /\ pset (m, a) == {x | x < n /\ p}) -> E. b pset b == {x | x < n /\ p}

184

183

eexda

0 < m /\ A. x (0 < x /\ x <= n -> x || m) -> E. a (0 < a /\ pset (m, a) == {x | x < n /\ p}) -> E. b pset b == {x | x < n /\ p}

185

177, 184

mpd

0 < m /\ A. x (0 < x /\ x <= n -> x || m) -> E. b pset b == {x | x < n /\ p}

186

185

eex

E. m (0 < m /\ A. x (0 < x /\ x <= n -> x || m)) -> E. b pset b == {x | x < n /\ p}

187

lcmex

E. m (0 < m /\ A. x (0 < x /\ x <= n -> x || m))

188

186, 187

ax_mp

E. b pset b == {x | x < n /\ p}

Theorem psetsep ≪ | index | src | ≫

Axiom use