Most Recent Proofs - Intuitionistic Logic Explorer

Most recent proofs    These are the 100 (Unicode, GIF) or 1000 (Unicode, GIF) most recent proofs in the iset.mm database for the Intuitionistic Logic Explorer. The iset.mm database is maintained on GitHub with master (stable) and develop (development) versions. This page was created from the commit given on the MPE Most Recent Proofs page. The database from that commit is also available here: iset.mm.

See the MPE Most Recent Proofs page for news and some useful links.

Last updated on 25-Jan-2020 at 1:16 PM ET.

Recent Additions to the Intuitionistic Logic Explorer

Date	Label	Description
Theorem
17-Jan-2020	addcom 6737	Addition commutes. (Contributed by Jim Kingdon, 17-Jan-2020.)
|- ((A e. CC /\ B e. CC) -> (A + B) = (B + A))
17-Jan-2020	ax-addcom 6584	Addition commutes. Axiom for real and complex numbers, justified by theorem axaddcom 6558. Proofs should normally use addcom 6737 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 17-Jan-2020.)
|- ((A e. CC /\ B e. CC) -> (A + B) = (B + A))
17-Jan-2020	axaddcom 6558	Addition commutes. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-addcom 6584 be used later. Instead, use addcom 6737. In the Metamath Proof Explorer this is not a complex number axiom but is instead proved from other axioms. That proof relies on real number trichotomy and it is not known whether it is possible to prove this from the other axioms without it. (Contributed by Jim Kingdon, 17-Jan-2020.) (New usage is discouraged.)
|- ((A e. CC /\ B e. CC) -> (A + B) = (B + A))
16-Jan-2020	addid1 6738	0 is an additive identity. (Contributed by Jim Kingdon, 16-Jan-2020.)
|- (A e. CC -> (A + 0) = A)
16-Jan-2020	ax-0id 6592	0 is an identity element for real addition. Axiom for real and complex numbers, justified by theorem ax0id 6566. Proofs should normally use addid1 6738 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 16-Jan-2020.)
|- (A e. CC -> (A + 0) = A)
16-Jan-2020	ax0id 6566	0 is an identity element for real addition. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-0id 6592. In the Metamath Proof Explorer this is not a complex number axiom but is instead proved from other axioms. That proof relies on excluded middle and it is not known whether it is possible to prove this from the other axioms without excluded middle. (Contributed by Jim Kingdon, 16-Jan-2020.) (New usage is discouraged.)
|- (A e. CC -> (A + 0) = A)
15-Jan-2020	axltwlin 6682	Real number less-than is weakly linear. Axiom for real and complex numbers, derived from set theory. This restates ax-pre-ltwlin 6597 with ordering on the extended reals. (Contributed by Jim Kingdon, 15-Jan-2020.)
|- ((A e. RR /\ B e. RR /\ C e. RR) -> (A < B -> (A < C \/ C < B)))
15-Jan-2020	axltirr 6681	Real number less-than is irreflexive. Axiom for real and complex numbers, derived from set theory. This restates ax-pre-ltirr 6596 with ordering on the extended reals. New proofs should use ltnr 6689 instead for naming consistency. (New usage is discouraged.) (Contributed by Jim Kingdon, 15-Jan-2020.)
|- (A e. RR -> -. A < A)
14-Jan-2020	2pwuninelg 5816	The power set of the power set of the union of a set does not belong to the set. This theorem provides a way of constructing a new set that doesn't belong to a given set. (Contributed by Jim Kingdon, 14-Jan-2020.)
|- (A e. V -> -. ~P ~P U.A e. A)
13-Jan-2020	1re 6622	1 is a real number. (Contributed by Jim Kingdon, 13-Jan-2020.)
|- 1 e. RR
13-Jan-2020	ax-1re 6578	1 is a real number. Axiom for real and complex numbers, justified by theorem ax1re 6552. Proofs should use 1re 6622 instead. (Contributed by Jim Kingdon, 13-Jan-2020.) (New usage is discouraged.)
|- 1 e. RR
13-Jan-2020	ax1re 6552	1 is a real number. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-1re 6578. In the Metamath Proof Explorer, this is not a complex number axiom but is proved from ax-1cn 6577 and the other axioms. It is not known whether we can do so here, but the Metamath Proof Explorer proof (accessed 13-Jan-2020) uses excluded middle. (Contributed by Jim Kingdon, 13-Jan-2020.) (New usage is discouraged.)
|- 1 e. RR
12-Jan-2020	ax-pre-ltwlin 6597	Real number less-than is weakly linear. Axiom for real and complex numbers, justified by theorem axpre-ltwlin 6571. (Contributed by Jim Kingdon, 12-Jan-2020.)
|- ((A e. RR /\ B e. RR /\ C e. RR) -> (A <RR B -> (A <RR C \/ C <RR B)))
12-Jan-2020	ax-pre-ltirr 6596	Real number less-than is irreflexive. Axiom for real and complex numbers, justified by theorem ax-pre-ltirr 6596. (Contributed by Jim Kingdon, 12-Jan-2020.)
|- (A e. RR -> -. A <RR A)
12-Jan-2020	ax-precex 6594	Existence of reciprocal of positive real number. Axiom for real and complex numbers, justified by theorem axprecex 6568. In treatments which assume excluded middle, the 0 <RR A condition is generally replaced by A =/= 0. (Contributed by Jim Kingdon, 12-Jan-2020.)
|- ((A e. RR /\ 0 <RR A) -> E.x e. RR (A x. x) = 1)
12-Jan-2020	ax-0lt1 6590	0 is less than 1. Axiom for real and complex numbers, justified by theorem ax0lt1 6564. Proofs should normally use 0lt1 6728 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 12-Jan-2020.)
|- 0 <RR 1
12-Jan-2020	axpre-ltwlin 6571	Real number less-than is weakly linear. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-ltwlin 6597. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.)
|- ((A e. RR /\ B e. RR /\ C e. RR) -> (A <RR B -> (A <RR C \/ C <RR B)))
12-Jan-2020	axpre-ltirr 6570	Real number less-than is irreflexive. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-ltirr 6596. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.)
|- (A e. RR -> -. A <RR A)
12-Jan-2020	axprecex 6568	Existence of reciprocal of positive real number. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-precex 6594. In treatments which assume excluded middle, the 0 <RR A condition is generally replaced by A =/= 0. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.)
|- ((A e. RR /\ 0 <RR A) -> E.x e. RR (A x. x) = 1)
12-Jan-2020	ax0lt1 6564	0 is less than 1. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-0lt1 6590. The version of this axiom in the Metamath Proof Explorer reads 1 =/= 0; here we change it to 0 <RR 1. The proof of 0 <RR 1 from 1 =/= 0 in the Metamath Proof Explorer (accessed 12-Jan-2020) relies on real number trichotomy. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.)
|- 0 <RR 1
8-Jan-2020	ecidg 6077	A set is equal to its converse epsilon coset. (Note: converse epsilon is not an equivalence relation.) (Contributed by Jim Kingdon, 8-Jan-2020.)
|- (A e. V -> [A] `' _E = A)
5-Jan-2020	1idsr 6509	1 is an identity element for multiplication. (Contributed by Jim Kingdon, 5-Jan-2020.)
|- (A e. R. -> (A .R 1R) = A)
4-Jan-2020	distrsrg 6500	Multiplication of signed reals is distributive. (Contributed by Jim Kingdon, 4-Jan-2020.)
|- ((A e. R. /\ B e. R. /\ C e. R.) -> (A .R (B +R C)) = ((A .R B) +R (A .R C)))
3-Jan-2020	mulasssrg 6499	Multiplication of signed reals is associative. (Contributed by Jim Kingdon, 3-Jan-2020.)
|- ((A e. R. /\ B e. R. /\ C e. R.) -> ((A .R B) .R C) = (A .R (B .R C)))
3-Jan-2020	mulcomsrg 6498	Multiplication of signed reals is commutative. (Contributed by Jim Kingdon, 3-Jan-2020.)
|- ((A e. R. /\ B e. R.) -> (A .R B) = (B .R A))
3-Jan-2020	addasssrg 6497	Addition of signed reals is associative. (Contributed by Jim Kingdon, 3-Jan-2020.)
|- ((A e. R. /\ B e. R. /\ C e. R.) -> ((A +R B) +R C) = (A +R (B +R C)))
3-Jan-2020	addcomsrg 6496	Addition of signed reals is commutative. (Contributed by Jim Kingdon, 3-Jan-2020.)
|- ((A e. R. /\ B e. R.) -> (A +R B) = (B +R A))
3-Jan-2020	caovlem2d 5612	Rearrangement of expression involving multiplication ( G) and addition ( F). (Contributed by Jim Kingdon, 3-Jan-2020.)
|- ((ph /\ (x e. S /\ y e. S)) -> (x Gy) = (y Gx))   &   |- ((ph /\ (x e. S /\ y e. S /\ z e. S)) -> ((x Fy) Gz) = ((x Gz) F(y Gz)))   &   |- ((ph /\ (x e. S /\ y e. S /\ z e. S)) -> ((x Gy) Gz) = (x G(y Gz)))   &   |- ((ph /\ (x e. S /\ y e. S)) -> (x Gy) e. S)   &   |- (ph -> A e. S)   &   |- (ph -> B e. S)   &   |- (ph -> C e. S)   &   |- (ph -> D e. S)   &   |- (ph -> H e. S)   &   |- (ph -> R e. S)   &   |- ((ph /\ (x e. S /\ y e. S)) -> (x Fy) = (y Fx))   &   |- ((ph /\ (x e. S /\ y e. S /\ z e. S)) -> ((x Fy) Fz) = (x F(y Fz)))   &   |- ((ph /\ (x e. S /\ y e. S)) -> (x Fy) e. S)   =>   |- (ph -> ((((A G C) F(B G D)) G H) F(((A G D) F(B G C)) G R)) = ((A G(( C G H) F( D G R))) F(B G(( C G R) F( D G H)))))
2-Jan-2020	bj-d0clsepcl 7287	Δ0-classical logic and separation implies classical logic. (Contributed by BJ, 2-Jan-2020.) (Proof modification is discouraged.)
|- (ph \/ -. ph)
2-Jan-2020	ax-bj-d0cl 7286	Axiom for Δ0-classical logic. (Contributed by BJ, 2-Jan-2020.)
|- BOUNDED ph   =>   |- (ph \/ -. ph)
1-Jan-2020	mulcmpblnrlemg 6481	Lemma used in lemma showing compatibility of multiplication. (Contributed by Jim Kingdon, 1-Jan-2020.)
|- ((((A e. P. /\ B e. P.) /\ ( C e. P. /\ D e. P.)) /\ (( F e. P. /\ G e. P.) /\ ( R e. P. /\ S e. P.))) -> (((A +P. D) = (B +P. C) /\ ( F +P. S) = ( G +P. R)) -> (( D .P. F) +P. (((A .P. F) +P. (B .P. G)) +P. (( C .P. S) +P. ( D .P. R)))) = (( D .P. F) +P. (((A .P. G) +P. (B .P. F)) +P. (( C .P. R) +P. ( D .P. S))))))
31-Dec-2019	eceq1d 6049	Equality theorem for equivalence class (deduction form). (Contributed by Jim Kingdon, 31-Dec-2019.)
|- (ph -> A = B)   =>   |- (ph -> [A] C = [B] C)
30-Dec-2019	mulsrmo 6485	There is at most one result from multiplying signed reals. (Contributed by Jim Kingdon, 30-Dec-2019.)
|- ((A e. (( P. X. P.) /. ~R ) /\ B e. (( P. X. P.) /. ~R )) -> E*zE.wE.vE.uE. t((A = [ <.w , v >.] ~R /\ B = [ <.u , t >.] ~R ) /\ z = [ <.((w .P. u) +P. (v .P. t)) , ((w .P. t) +P. (v .P. u)) >.] ~R ))
30-Dec-2019	addsrmo 6484	There is at most one result from adding signed reals. (Contributed by Jim Kingdon, 30-Dec-2019.)
|- ((A e. (( P. X. P.) /. ~R ) /\ B e. (( P. X. P.) /. ~R )) -> E*zE.wE.vE.uE. t((A = [ <.w , v >.] ~R /\ B = [ <.u , t >.] ~R ) /\ z = [ <.(w +P. u) , (v +P. t) >.] ~R ))
30-Dec-2019	prsrlem1 6483	Decomposing signed reals into positive reals. Lemma for addsrpr 6486 and mulsrpr 6487. (Contributed by Jim Kingdon, 30-Dec-2019.)
|- (((A e. (( P. X. P.) /. ~R ) /\ B e. (( P. X. P.) /. ~R )) /\ ((A = [ <.w , v >.] ~R /\ B = [ <.u , t >.] ~R ) /\ (A = [ <. s , f >.] ~R /\ B = [ <.g , h >.] ~R ))) -> ((((w e. P. /\ v e. P.) /\ ( s e. P. /\ f e. P.)) /\ ((u e. P. /\ t e. P.) /\ (g e. P. /\ h e. P.))) /\ ((w +P. f) = (v +P. s) /\ (u +P. h) = ( t +P. g))))
29-Dec-2019	bj-omelon 7320	The set om is an ordinal. Constructive proof of omelon 4254. (Contributed by BJ, 29-Dec-2019.) (Proof modification is discouraged.)
|- om e. On
29-Dec-2019	bj-omord 7319	The set om is an ordinal. (Contributed by BJ, 29-Dec-2019.) (Proof modification is discouraged.)
|- Ord om
29-Dec-2019	bj-omtrans2 7318	The set om is transitive. (Contributed by BJ, 29-Dec-2019.) (Proof modification is discouraged.)
|- Tr om
29-Dec-2019	bj-omtrans 7317	The set om is transitive. A natural number is included in om. The idea is to use bounded induction with the formula x C_ om. This formula, in a logic with terms, is bounded. So in our logic without terms, we need to temporarily replace it with x C_ a and then deduce the original claim. (Contributed by BJ, 29-Dec-2019.) (Proof modification is discouraged.)
|- (A e. om -> A C_ om)
29-Dec-2019	ltrnqg 6271	Ordering property of reciprocal for positive fractions. For a simplified version of the forward implication, see ltrnqi 6272. (Contributed by Jim Kingdon, 29-Dec-2019.)
|- ((A e. Q. /\ B e. Q.) -> (A <Q B <-> ( *Q ` B) <Q ( *Q ` A)))
29-Dec-2019	rec1nq 6248	Reciprocal of positive fraction one. (Contributed by Jim Kingdon, 29-Dec-2019.)
|- ( *Q ` 1Q) = 1Q
28-Dec-2019	recexprlemupu 6456	The upper cut of B is upper. Lemma for recexpr 6466. (Contributed by Jim Kingdon, 28-Dec-2019.)
|- B = <. {x | E.y(x <Q y /\ ( *Q ` y) e. ( 2nd ` A)) } , {x | E.y(y <Q x /\ ( *Q ` y) e. ( 1st ` A)) } >.   =>   |- ((A e. P. /\ r e. Q.) -> (E. q e. Q. ( q <Q r /\ q e. ( 2nd ` B)) -> r e. ( 2nd ` B)))
28-Dec-2019	recexprlemopu 6455	The upper cut of B is open. Lemma for recexpr 6466. (Contributed by Jim Kingdon, 28-Dec-2019.)
|- B = <. {x | E.y(x <Q y /\ ( *Q ` y) e. ( 2nd ` A)) } , {x | E.y(y <Q x /\ ( *Q ` y) e. ( 1st ` A)) } >.   =>   |- ((A e. P. /\ r e. Q. /\ r e. ( 2nd ` B)) -> E. q e. Q. ( q <Q r /\ q e. ( 2nd ` B)))
28-Dec-2019	recexprlemlol 6454	The lower cut of B is lower. Lemma for recexpr 6466. (Contributed by Jim Kingdon, 28-Dec-2019.)
|- B = <. {x | E.y(x <Q y /\ ( *Q ` y) e. ( 2nd ` A)) } , {x | E.y(y <Q x /\ ( *Q ` y) e. ( 1st ` A)) } >.   =>   |- ((A e. P. /\ q e. Q.) -> (E. r e. Q. ( q <Q r /\ r e. ( 1st ` B)) -> q e. ( 1st ` B)))
28-Dec-2019	recexprlemopl 6453	The lower cut of B is open. Lemma for recexpr 6466. (Contributed by Jim Kingdon, 28-Dec-2019.)
|- B = <. {x | E.y(x <Q y /\ ( *Q ` y) e. ( 2nd ` A)) } , {x | E.y(y <Q x /\ ( *Q ` y) e. ( 1st ` A)) } >.   =>   |- ((A e. P. /\ q e. Q. /\ q e. ( 1st ` B)) -> E. r e. Q. ( q <Q r /\ r e. ( 1st ` B)))
28-Dec-2019	prmuloc2 6405	Positive reals are multiplicatively located. This is a variation of prmuloc 6404 which only constructs one (named) point and is therefore often easier to work with. It states that given a ratio B, there are elements of the lower and upper cut which have exactly that ratio between them. (Contributed by Jim Kingdon, 28-Dec-2019.)
|- (( <. L , U >. e. P. /\ 1Q <Q B) -> E.x e. L (x .Q B) e. U)
28-Dec-2019	1pru 6400	The upper cut of the positive real number 'one'. (Contributed by Jim Kingdon, 28-Dec-2019.)
|- ( 2nd ` 1P) = {x | 1Q <Q x }
28-Dec-2019	1prl 6399	The lower cut of the positive real number 'one'. (Contributed by Jim Kingdon, 28-Dec-2019.)
|- ( 1st ` 1P) = {x | x <Q 1Q }
27-Dec-2019	recexprlemex 6465	B is the reciprocal of A. Lemma for recexpr 6466. (Contributed by Jim Kingdon, 27-Dec-2019.)
|- B = <. {x | E.y(x <Q y /\ ( *Q ` y) e. ( 2nd ` A)) } , {x | E.y(y <Q x /\ ( *Q ` y) e. ( 1st ` A)) } >.   =>   |- (A e. P. -> (A .P. B) = 1P)
27-Dec-2019	recexprlemss1u 6464	The upper cut of A .P. B is a subset of the upper cut of one. Lemma for recexpr 6466. (Contributed by Jim Kingdon, 27-Dec-2019.)
|- B = <. {x | E.y(x <Q y /\ ( *Q ` y) e. ( 2nd ` A)) } , {x | E.y(y <Q x /\ ( *Q ` y) e. ( 1st ` A)) } >.   =>   |- (A e. P. -> ( 2nd ` (A .P. B)) C_ ( 2nd ` 1P))
27-Dec-2019	recexprlemss1l 6463	The lower cut of A .P. B is a subset of the lower cut of one. Lemma for recexpr 6466. (Contributed by Jim Kingdon, 27-Dec-2019.)
|- B = <. {x | E.y(x <Q y /\ ( *Q ` y) e. ( 2nd ` A)) } , {x | E.y(y <Q x /\ ( *Q ` y) e. ( 1st ` A)) } >.   =>   |- (A e. P. -> ( 1st ` (A .P. B)) C_ ( 1st ` 1P))
27-Dec-2019	recexprlem1ssu 6462	The upper cut of one is a subset of the upper cut of A .P. B. Lemma for recexpr 6466. (Contributed by Jim Kingdon, 27-Dec-2019.)
|- B = <. {x | E.y(x <Q y /\ ( *Q ` y) e. ( 2nd ` A)) } , {x | E.y(y <Q x /\ ( *Q ` y) e. ( 1st ` A)) } >.   =>   |- (A e. P. -> ( 2nd ` 1P) C_ ( 2nd ` (A .P. B)))
27-Dec-2019	recexprlem1ssl 6461	The lower cut of one is a subset of the lower cut of A .P. B. Lemma for recexpr 6466. (Contributed by Jim Kingdon, 27-Dec-2019.)
|- B = <. {x | E.y(x <Q y /\ ( *Q ` y) e. ( 2nd ` A)) } , {x | E.y(y <Q x /\ ( *Q ` y) e. ( 1st ` A)) } >.   =>   |- (A e. P. -> ( 1st ` 1P) C_ ( 1st ` (A .P. B)))
27-Dec-2019	recexprlempr 6460	B is a positive real. Lemma for recexpr 6466. (Contributed by Jim Kingdon, 27-Dec-2019.)
|- B = <. {x | E.y(x <Q y /\ ( *Q ` y) e. ( 2nd ` A)) } , {x | E.y(y <Q x /\ ( *Q ` y) e. ( 1st ` A)) } >.   =>   |- (A e. P. -> B e. P.)
27-Dec-2019	recexprlemloc 6459	B is located. Lemma for recexpr 6466. (Contributed by Jim Kingdon, 27-Dec-2019.)
|- B = <. {x | E.y(x <Q y /\ ( *Q ` y) e. ( 2nd ` A)) } , {x | E.y(y <Q x /\ ( *Q ` y) e. ( 1st ` A)) } >.   =>   |- (A e. P. -> A. q e. Q. A. r e. Q. ( q <Q r -> ( q e. ( 1st ` B) \/ r e. ( 2nd ` B))))
27-Dec-2019	recexprlemdisj 6458	B is disjoint. Lemma for recexpr 6466. (Contributed by Jim Kingdon, 27-Dec-2019.)
|- B = <. {x | E.y(x <Q y /\ ( *Q ` y) e. ( 2nd ` A)) } , {x | E.y(y <Q x /\ ( *Q ` y) e. ( 1st ` A)) } >.   =>   |- (A e. P. -> A. q e. Q. -. ( q e. ( 1st ` B) /\ q e. ( 2nd ` B)))
27-Dec-2019	recexprlemrnd 6457	B is rounded. Lemma for recexpr 6466. (Contributed by Jim Kingdon, 27-Dec-2019.)
|- B = <. {x | E.y(x <Q y /\ ( *Q ` y) e. ( 2nd ` A)) } , {x | E.y(y <Q x /\ ( *Q ` y) e. ( 1st ` A)) } >.   =>   |- (A e. P. -> (A. q e. Q. ( q e. ( 1st ` B) <-> E. r e. Q. ( q <Q r /\ r e. ( 1st ` B))) /\ A. r e. Q. ( r e. ( 2nd ` B) <-> E. q e. Q. ( q <Q r /\ q e. ( 2nd ` B)))))
27-Dec-2019	recexprlemm 6452	B is inhabited. Lemma for recexpr 6466. (Contributed by Jim Kingdon, 27-Dec-2019.)
|- B = <. {x | E.y(x <Q y /\ ( *Q ` y) e. ( 2nd ` A)) } , {x | E.y(y <Q x /\ ( *Q ` y) e. ( 1st ` A)) } >.   =>   |- (A e. P. -> (E. q e. Q. q e. ( 1st ` B) /\ E. r e. Q. r e. ( 2nd ` B)))
27-Dec-2019	recexprlemelu 6451	Membership in the upper cut of B. Lemma for recexpr 6466. (Contributed by Jim Kingdon, 27-Dec-2019.)
|- B = <. {x | E.y(x <Q y /\ ( *Q ` y) e. ( 2nd ` A)) } , {x | E.y(y <Q x /\ ( *Q ` y) e. ( 1st ` A)) } >.   =>   |- ( C e. ( 2nd ` B) <-> E.y(y <Q C /\ ( *Q ` y) e. ( 1st ` A)))
27-Dec-2019	recexprlemell 6450	Membership in the lower cut of B. Lemma for recexpr 6466. (Contributed by Jim Kingdon, 27-Dec-2019.)
|- B = <. {x | E.y(x <Q y /\ ( *Q ` y) e. ( 2nd ` A)) } , {x | E.y(y <Q x /\ ( *Q ` y) e. ( 1st ` A)) } >.   =>   |- ( C e. ( 1st ` B) <-> E.y( C <Q y /\ ( *Q ` y) e. ( 2nd ` A)))
26-Dec-2019	ltaprg 6449	Ordering property of addition. Proposition 9-3.5(v) of [Gleason] p. 123. Part of Definition 11.2.7(vi) of [HoTT]], p. (varies). (Contributed by Jim Kingdon, 26-Dec-2019.)
|- ((A e. P. /\ B e. P. /\ C e. P.) -> (A <P B <-> ( C +P. A) <P ( C +P. B)))
26-Dec-2019	prarloc2 6352	A Dedekind cut is arithmetically located. This is a variation of prarloc 6351 which only constructs one (named) point and is therefore often easier to work with. It states that given a tolerance P, there are elements of the lower and upper cut which are exactly that tolerance from each other. (Contributed by Jim Kingdon, 26-Dec-2019.)
|- (( <. L , U >. e. P. /\ P e. Q.) -> E. a e. L ( a +Q P) e. U)
25-Dec-2019	addcanprlemu 6446	Lemma for addcanprg 6447. (Contributed by Jim Kingdon, 25-Dec-2019.)
|- (((A e. P. /\ B e. P. /\ C e. P.) /\ (A +P. B) = (A +P. C)) -> ( 2nd ` B) C_ ( 2nd ` C))
25-Dec-2019	addcanprleml 6445	Lemma for addcanprg 6447. (Contributed by Jim Kingdon, 25-Dec-2019.)
|- (((A e. P. /\ B e. P. /\ C e. P.) /\ (A +P. B) = (A +P. C)) -> ( 1st ` B) C_ ( 1st ` C))
24-Dec-2019	addcanprg 6447	Addition cancellation law for positive reals. Proposition 9-3.5(vi) of [Gleason] p. 123. (Contributed by Jim Kingdon, 24-Dec-2019.)
|- ((A e. P. /\ B e. P. /\ C e. P.) -> ((A +P. B) = (A +P. C) -> B = C))
23-Dec-2019	ltprordil 6422	If a positive real is less than a second positive real, its lower cut is a subset of the second's lower cut. (Contributed by Jim Kingdon, 23-Dec-2019.)
|- (A <P B -> ( 1st ` A) C_ ( 1st ` B))
22-Dec-2019	bj-findis 7336	Principle of induction, using implicit substitutions (the biconditional versions of the hypotheses are implicit substitutions, and we have weakened them to implications). Constructive proof (from CZF). See bj-bdfindis 7308 for a bounded version not requiring ax-setind 4200. See finds 4246 for a proof in IZF. From this version, it is easy to prove of finds 4246, finds2 4247, finds1 4248. (Contributed by BJ, 22-Dec-2019.) (Proof modification is discouraged.)
|- F/xps   &   |- F/xch   &   |- F/xth   &   |- (x = (/) -> (ps -> ph))   &   |- (x = y -> (ph -> ch))   &   |- (x = suc y -> (th -> ph))   =>   |- ((ps /\ A.y e. om (ch -> th)) -> A.x e. om ph)
21-Dec-2019	ltexprlemupu 6435	The upper cut of our constructed difference is upper. Lemma for ltexpri 6444. (Contributed by Jim Kingdon, 21-Dec-2019.)
|- C = <. {x e. Q. | E.y(y e. ( 2nd ` A) /\ (y +Q x) e. ( 1st ` B)) } , {x e. Q. | E.y(y e. ( 1st ` A) /\ (y +Q x) e. ( 2nd ` B)) } >.   =>   |- ((A <P B /\ r e. Q.) -> (E. q e. Q. ( q <Q r /\ q e. ( 2nd ` C)) -> r e. ( 2nd ` C)))
21-Dec-2019	ltexprlemopu 6434	The upper cut of our constructed difference is open. Lemma for ltexpri 6444. (Contributed by Jim Kingdon, 21-Dec-2019.)
|- C = <. {x e. Q. | E.y(y e. ( 2nd ` A) /\ (y +Q x) e. ( 1st ` B)) } , {x e. Q. | E.y(y e. ( 1st ` A) /\ (y +Q x) e. ( 2nd ` B)) } >.   =>   |- ((A <P B /\ r e. Q. /\ r e. ( 2nd ` C)) -> E. q e. Q. ( q <Q r /\ q e. ( 2nd ` C)))
21-Dec-2019	ltexprlemlol 6433	The lower cut of our constructed difference is lower. Lemma for ltexpri 6444. (Contributed by Jim Kingdon, 21-Dec-2019.)
|- C = <. {x e. Q. | E.y(y e. ( 2nd ` A) /\ (y +Q x) e. ( 1st ` B)) } , {x e. Q. | E.y(y e. ( 1st ` A) /\ (y +Q x) e. ( 2nd ` B)) } >.   =>   |- ((A <P B /\ q e. Q.) -> (E. r e. Q. ( q <Q r /\ r e. ( 1st ` C)) -> q e. ( 1st ` C)))
21-Dec-2019	ltexprlemopl 6432	The lower cut of our constructed difference is open. Lemma for ltexpri 6444. (Contributed by Jim Kingdon, 21-Dec-2019.)
|- C = <. {x e. Q. | E.y(y e. ( 2nd ` A) /\ (y +Q x) e. ( 1st ` B)) } , {x e. Q. | E.y(y e. ( 1st ` A) /\ (y +Q x) e. ( 2nd ` B)) } >.   =>   |- ((A <P B /\ q e. Q. /\ q e. ( 1st ` C)) -> E. r e. Q. ( q <Q r /\ r e. ( 1st ` C)))
21-Dec-2019	ltexprlemelu 6430	Element in upper cut of the constructed difference. Lemma for ltexpri 6444. (Contributed by Jim Kingdon, 21-Dec-2019.)
|- C = <. {x e. Q. | E.y(y e. ( 2nd ` A) /\ (y +Q x) e. ( 1st ` B)) } , {x e. Q. | E.y(y e. ( 1st ` A) /\ (y +Q x) e. ( 2nd ` B)) } >.   =>   |- ( r e. ( 2nd ` C) <-> ( r e. Q. /\ E.y(y e. ( 1st ` A) /\ (y +Q r) e. ( 2nd ` B))))
21-Dec-2019	ltexprlemell 6429	Element in lower cut of the constructed difference. Lemma for ltexpri 6444. (Contributed by Jim Kingdon, 21-Dec-2019.)
|- C = <. {x e. Q. | E.y(y e. ( 2nd ` A) /\ (y +Q x) e. ( 1st ` B)) } , {x e. Q. | E.y(y e. ( 1st ` A) /\ (y +Q x) e. ( 2nd ` B)) } >.   =>   |- ( q e. ( 1st ` C) <-> ( q e. Q. /\ E.y(y e. ( 2nd ` A) /\ (y +Q q) e. ( 1st ` B))))
17-Dec-2019	ltexprlemru 6443	Lemma for ltexpri 6444. One direction of our result for upper cuts. (Contributed by Jim Kingdon, 17-Dec-2019.)
|- C = <. {x e. Q. | E.y(y e. ( 2nd ` A) /\ (y +Q x) e. ( 1st ` B)) } , {x e. Q. | E.y(y e. ( 1st ` A) /\ (y +Q x) e. ( 2nd ` B)) } >.   =>   |- (A <P B -> ( 2nd ` B) C_ ( 2nd ` (A +P. C)))
17-Dec-2019	ltexprlemfu 6442	Lemma for ltexpri 6444. One direction of our result for upper cuts. (Contributed by Jim Kingdon, 17-Dec-2019.)
|- C = <. {x e. Q. | E.y(y e. ( 2nd ` A) /\ (y +Q x) e. ( 1st ` B)) } , {x e. Q. | E.y(y e. ( 1st ` A) /\ (y +Q x) e. ( 2nd ` B)) } >.   =>   |- (A <P B -> ( 2nd ` (A +P. C)) C_ ( 2nd ` B))
17-Dec-2019	ltexprlemrl 6441	Lemma for ltexpri 6444. Reverse directon of our result for lower cuts. (Contributed by Jim Kingdon, 17-Dec-2019.)
|- C = <. {x e. Q. | E.y(y e. ( 2nd ` A) /\ (y +Q x) e. ( 1st ` B)) } , {x e. Q. | E.y(y e. ( 1st ` A) /\ (y +Q x) e. ( 2nd ` B)) } >.   =>   |- (A <P B -> ( 1st ` B) C_ ( 1st ` (A +P. C)))
17-Dec-2019	ltexprlemfl 6440	Lemma for ltexpri 6444. One directon of our result for lower cuts. (Contributed by Jim Kingdon, 17-Dec-2019.)
|- C = <. {x e. Q. | E.y(y e. ( 2nd ` A) /\ (y +Q x) e. ( 1st ` B)) } , {x e. Q. | E.y(y e. ( 1st ` A) /\ (y +Q x) e. ( 2nd ` B)) } >.   =>   |- (A <P B -> ( 1st ` (A +P. C)) C_ ( 1st ` B))
17-Dec-2019	ltexprlempr 6439	Our constructed difference is a positive real. Lemma for ltexpri 6444. (Contributed by Jim Kingdon, 17-Dec-2019.)
|- C = <. {x e. Q. | E.y(y e. ( 2nd ` A) /\ (y +Q x) e. ( 1st ` B)) } , {x e. Q. | E.y(y e. ( 1st ` A) /\ (y +Q x) e. ( 2nd ` B)) } >.   =>   |- (A <P B -> C e. P.)
17-Dec-2019	ltexprlemloc 6438	Our constructed difference is located. Lemma for ltexpri 6444. (Contributed by Jim Kingdon, 17-Dec-2019.)
|- C = <. {x e. Q. | E.y(y e. ( 2nd ` A) /\ (y +Q x) e. ( 1st ` B)) } , {x e. Q. | E.y(y e. ( 1st ` A) /\ (y +Q x) e. ( 2nd ` B)) } >.   =>   |- (A <P B -> A. q e. Q. A. r e. Q. ( q <Q r -> ( q e. ( 1st ` C) \/ r e. ( 2nd ` C))))
17-Dec-2019	ltexprlemdisj 6437	Our constructed difference is disjoint. Lemma for ltexpri 6444. (Contributed by Jim Kingdon, 17-Dec-2019.)
|- C = <. {x e. Q. | E.y(y e. ( 2nd ` A) /\ (y +Q x) e. ( 1st ` B)) } , {x e. Q. | E.y(y e. ( 1st ` A) /\ (y +Q x) e. ( 2nd ` B)) } >.   =>   |- (A <P B -> A. q e. Q. -. ( q e. ( 1st ` C) /\ q e. ( 2nd ` C)))
17-Dec-2019	ltexprlemrnd 6436	Our constructed difference is rounded. Lemma for ltexpri 6444. (Contributed by Jim Kingdon, 17-Dec-2019.)
|- C = <. {x e. Q. | E.y(y e. ( 2nd ` A) /\ (y +Q x) e. ( 1st ` B)) } , {x e. Q. | E.y(y e. ( 1st ` A) /\ (y +Q x) e. ( 2nd ` B)) } >.   =>   |- (A <P B -> (A. q e. Q. ( q e. ( 1st ` C) <-> E. r e. Q. ( q <Q r /\ r e. ( 1st ` C))) /\ A. r e. Q. ( r e. ( 2nd ` C) <-> E. q e. Q. ( q <Q r /\ q e. ( 2nd ` C)))))
17-Dec-2019	ltexprlemm 6431	Our constructed difference is inhabited. Lemma for ltexpri 6444. (Contributed by Jim Kingdon, 17-Dec-2019.)
|- C = <. {x e. Q. | E.y(y e. ( 2nd ` A) /\ (y +Q x) e. ( 1st ` B)) } , {x e. Q. | E.y(y e. ( 1st ` A) /\ (y +Q x) e. ( 2nd ` B)) } >.   =>   |- (A <P B -> (E. q e. Q. q e. ( 1st ` C) /\ E. r e. Q. r e. ( 2nd ` C)))
16-Dec-2019	bj-sbime 7159	A strengthening of sbie 1652 (same proof). (Contributed by BJ, 16-Dec-2019.)
|- F/xps   &   |- (x = y -> (ph -> ps))   =>   |- ([y / x]ph -> ps)
16-Dec-2019	bj-sbimeh 7158	A strengthening of sbieh 1651 (same proof). (Contributed by BJ, 16-Dec-2019.)
|- (ps -> A.xps)   &   |- (x = y -> (ph -> ps))   =>   |- ([y / x]ph -> ps)
16-Dec-2019	bj-sbimedh 7157	A strengthening of sbiedh 1648 (same proof). (Contributed by BJ, 16-Dec-2019.)
|- (ph -> A.xph)   &   |- (ph -> (ch -> A.xch))   &   |- (ph -> (x = y -> (ps -> ch)))   =>   |- (ph -> ([y / x]ps -> ch))
16-Dec-2019	ltsopr 6427	Positive real 'less than' is a weak linear order (in the sense of df-iso 4004). Proposition 11.2.3 of [HoTT], p. (varies). (Contributed by Jim Kingdon, 16-Dec-2019.)
|- <P Or P.
15-Dec-2019	ltpopr 6426	Positive real 'less than' is a partial ordering. Remark ("< is transitive and irreflexive") preceding Proposition 11.2.3 of [HoTT], p. (varies). Lemma for ltsopr 6427. (Contributed by Jim Kingdon, 15-Dec-2019.)
|- <P Po P.
15-Dec-2019	ltdfpr 6354	More convenient form of df-iltp 6318. (Contributed by Jim Kingdon, 15-Dec-2019.)
|- ((A e. P. /\ B e. P.) -> (A <P B <-> E. q e. Q. ( q e. ( 2nd ` A) /\ q e. ( 1st ` B))))
15-Dec-2019	prdisj 6340	A Dedekind cut is disjoint. (Contributed by Jim Kingdon, 15-Dec-2019.)
|- (( <. L , U >. e. P. /\ A e. Q.) -> -. (A e. L /\ A e. U))
13-Dec-2019	1idpru 6424	Lemma for 1idpr 6425. (Contributed by Jim Kingdon, 13-Dec-2019.)
|- (A e. P. -> ( 2nd ` (A .P. 1P)) = ( 2nd ` A))
13-Dec-2019	1idprl 6423	Lemma for 1idpr 6425. (Contributed by Jim Kingdon, 13-Dec-2019.)
|- (A e. P. -> ( 1st ` (A .P. 1P)) = ( 1st ` A))
13-Dec-2019	gtnqex 6397	The class of rationals greater than a given rational is a set. (Contributed by Jim Kingdon, 13-Dec-2019.)
|- {x | A <Q x } e. _V
13-Dec-2019	ltnqex 6396	The class of rationals less than a given rational is a set. (Contributed by Jim Kingdon, 13-Dec-2019.)
|- {x | x <Q A } e. _V
13-Dec-2019	sotritrieq 4032	A trichotomy relationship, given a trichotomous order. (Contributed by Jim Kingdon, 13-Dec-2019.)
|- R Or A   &   |- ((B e. A /\ C e. A) -> (B R C \/ B = C \/ C RB))   =>   |- ((B e. A /\ C e. A) -> (B = C <-> -. (B R C \/ C RB)))
12-Dec-2019	distrprg 6421	Multiplication of positive reals is distributive. Proposition 9-3.7(iii) of [Gleason] p. 124. (Contributed by Jim Kingdon, 12-Dec-2019.)
|- ((A e. P. /\ B e. P. /\ C e. P.) -> (A .P. (B +P. C)) = ((A .P. B) +P. (A .P. C)))
12-Dec-2019	distrlem5pru 6420	Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.)
|- ((A e. P. /\ B e. P. /\ C e. P.) -> ( 2nd ` ((A .P. B) +P. (A .P. C))) C_ ( 2nd ` (A .P. (B +P. C))))
12-Dec-2019	distrlem5prl 6419	Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.)
|- ((A e. P. /\ B e. P. /\ C e. P.) -> ( 1st ` ((A .P. B) +P. (A .P. C))) C_ ( 1st ` (A .P. (B +P. C))))
12-Dec-2019	distrlem4pru 6418	Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.)
|- (((A e. P. /\ B e. P. /\ C e. P.) /\ ((x e. ( 2nd ` A) /\ y e. ( 2nd ` B)) /\ (f e. ( 2nd ` A) /\ z e. ( 2nd ` C)))) -> ((x .Q y) +Q (f .Q z)) e. ( 2nd ` (A .P. (B +P. C))))
12-Dec-2019	distrlem4prl 6417	Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.)
|- (((A e. P. /\ B e. P. /\ C e. P.) /\ ((x e. ( 1st ` A) /\ y e. ( 1st ` B)) /\ (f e. ( 1st ` A) /\ z e. ( 1st ` C)))) -> ((x .Q y) +Q (f .Q z)) e. ( 1st ` (A .P. (B +P. C))))
12-Dec-2019	distrlem1pru 6416	Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.)
|- ((A e. P. /\ B e. P. /\ C e. P.) -> ( 2nd ` (A .P. (B +P. C))) C_ ( 2nd ` ((A .P. B) +P. (A .P. C))))
12-Dec-2019	distrlem1prl 6415	Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.)
|- ((A e. P. /\ B e. P. /\ C e. P.) -> ( 1st ` (A .P. (B +P. C))) C_ ( 1st ` ((A .P. B) +P. (A .P. C))))
12-Dec-2019	ltdcnq 6250	Less-than for positive fractions is decidable. (Contributed by Jim Kingdon, 12-Dec-2019.)
|- ((A e. Q. /\ B e. Q.) -> DECID A <Q B)
12-Dec-2019	ltdcpi 6177	Less-than for positive integers is decidable. (Contributed by Jim Kingdon, 12-Dec-2019.)
|- ((A e. N. /\ B e. N.) -> DECID A <N B)
11-Dec-2019	mulassprg 6414	Multiplication of positive reals is associative. Proposition 9-3.7(i) of [Gleason] p. 124. (Contributed by Jim Kingdon, 11-Dec-2019.)
|- ((A e. P. /\ B e. P. /\ C e. P.) -> ((A .P. B) .P. C) = (A .P. (B .P. C)))
11-Dec-2019	mulcomprg 6413	Multiplication of positive reals is commutative. Proposition 9-3.7(ii) of [Gleason] p. 124. (Contributed by Jim Kingdon, 11-Dec-2019.)
|- ((A e. P. /\ B e. P.) -> (A .P. B) = (B .P. A))
11-Dec-2019	addassprg 6412	Addition of positive reals is associative. Proposition 9-3.5(i) of [Gleason] p. 123. (Contributed by Jim Kingdon, 11-Dec-2019.)
|- ((A e. P. /\ B e. P. /\ C e. P.) -> ((A +P. B) +P. C) = (A +P. (B +P. C)))
11-Dec-2019	addcomprg 6411	Addition of positive reals is commutative. Proposition 9-3.5(ii) of [Gleason] p. 123. (Contributed by Jim Kingdon, 11-Dec-2019.)
|- ((A e. P. /\ B e. P.) -> (A +P. B) = (B +P. A))
11-Dec-2019	genpassg 6375	Associativity of an operation on reals. (Contributed by Jim Kingdon, 11-Dec-2019.)
|- F = (w e. P. , v e. P. |-> <. {x e. Q. | E.y e. Q. E.z e. Q. (y e. ( 1st ` w) /\ z e. ( 1st ` v) /\ x = (y Gz)) } , {x e. Q. | E.y e. Q. E.z e. Q. (y e. ( 2nd ` w) /\ z e. ( 2nd ` v) /\ x = (y Gz)) } >.)   &   |- ((y e. Q. /\ z e. Q.) -> (y Gz) e. Q.)   &   |- dom F = ( P. X. P.)   &   |- ((f e. P. /\ g e. P.) -> (f Fg) e. P.)   &   |- ((f e. Q. /\ g e. Q. /\ h e. Q.) -> ((f Gg) G h) = (f G(g G h)))   =>   |- ((A e. P. /\ B e. P. /\ C e. P.) -> ((A FB) F C) = (A F(B F C)))
11-Dec-2019	genpassu 6374	Associativity of upper cuts. Lemma for genpassg 6375. (Contributed by Jim Kingdon, 11-Dec-2019.)
|- F = (w e. P. , v e. P. |-> <. {x e. Q. | E.y e. Q. E.z e. Q. (y e. ( 1st ` w) /\ z e. ( 1st ` v) /\ x = (y Gz)) } , {x e. Q. | E.y e. Q. E.z e. Q. (y e. ( 2nd ` w) /\ z e. ( 2nd ` v) /\ x = (y Gz)) } >.)   &   |- ((y e. Q. /\ z e. Q.) -> (y Gz) e. Q.)   &   |- dom F = ( P. X. P.)   &   |- ((f e. P. /\ g e. P.) -> (f Fg) e. P.)   &   |- ((f e. Q. /\ g e. Q. /\ h e. Q.) -> ((f Gg) G h) = (f G(g G h)))   =>   |- ((A e. P. /\ B e. P. /\ C e. P.) -> ( 2nd ` ((A FB) F C)) = ( 2nd ` (A F(B F C))))
11-Dec-2019	genpassl 6373	Associativity of lower cuts. Lemma for genpassg 6375. (Contributed by Jim Kingdon, 11-Dec-2019.)
|- F = (w e. P. , v e. P. |-> <. {x e. Q. | E.y e. Q. E.z e. Q. (y e. ( 1st ` w) /\ z e. ( 1st ` v) /\ x = (y Gz)) } , {x e. Q. | E.y e. Q. E.z e. Q. (y e. ( 2nd ` w) /\ z e. ( 2nd ` v) /\ x = (y Gz)) } >.)   &   |- ((y e. Q. /\ z e. Q.) -> (y Gz) e. Q.)   &   |- dom F = ( P. X. P.)   &   |- ((f e. P. /\ g e. P.) -> (f Fg) e. P.)   &   |- ((f e. Q. /\ g e. Q. /\ h e. Q.) -> ((f Gg) G h) = (f G(g G h)))   =>   |- ((A e. P. /\ B e. P. /\ C e. P.) -> ( 1st ` ((A FB) F C)) = ( 1st ` (A F(B F C))))
11-Dec-2019	preqlu 6320	Two reals are equal if and only if their lower and upper cuts are. (Contributed by Jim Kingdon, 11-Dec-2019.)
|- ((A e. P. /\ B e. P.) -> (A = B <-> (( 1st ` A) = ( 1st ` B) /\ ( 2nd ` A) = ( 2nd ` B))))
10-Dec-2019	mullocprlem 6408	Calculations for mullocpr 6409. (Contributed by Jim Kingdon, 10-Dec-2019.)
|- (ph -> (A e. P. /\ B e. P.))   &   |- (ph -> ( U .Q Q) <Q ( E .Q ( D .Q U)))   &   |- (ph -> ( E .Q ( D .Q U)) <Q ( T .Q ( D .Q U)))   &   |- (ph -> ( T .Q ( D .Q U)) <Q ( D .Q R))   &   |- (ph -> ( Q e. Q. /\ R e. Q.))   &   |- (ph -> ( D e. Q. /\ U e. Q.))   &   |- (ph -> ( D e. ( 1st ` A) /\ U e. ( 2nd ` A)))   &   |- (ph -> ( E e. Q. /\ T e. Q.))   =>   |- (ph -> ( Q e. ( 1st ` (A .P. B)) \/ R e. ( 2nd ` (A .P. B))))
10-Dec-2019	mulnqpru 6407	Lemma to prove upward closure in positive real multiplication. (Contributed by Jim Kingdon, 10-Dec-2019.)
|- ((((A e. P. /\ G e. ( 2nd ` A)) /\ (B e. P. /\ H e. ( 2nd ` B))) /\ X e. Q.) -> (( G .Q H) <Q X -> X e. ( 2nd ` (A .P. B))))
10-Dec-2019	mulnqprl 6406	Lemma to prove downward closure in positive real multiplication. (Contributed by Jim Kingdon, 10-Dec-2019.)
|- ((((A e. P. /\ G e. ( 1st ` A)) /\ (B e. P. /\ H e. ( 1st ` B))) /\ X e. Q.) -> ( X <Q ( G .Q H) -> X e. ( 1st ` (A .P. B))))
9-Dec-2019	prmuloclemcalc 6403	Calculations for prmuloc 6404. (Contributed by Jim Kingdon, 9-Dec-2019.)
|- (ph -> R <Q U)   &   |- (ph -> U <Q ( D +Q P))   &   |- (ph -> (A +Q X) = B)   &   |- (ph -> ( P .Q B) <Q ( R .Q X))   &   |- (ph -> A e. Q.)   &   |- (ph -> B e. Q.)   &   |- (ph -> D e. Q.)   &   |- (ph -> P e. Q.)   &   |- (ph -> X e. Q.)   =>   |- (ph -> ( U .Q A) <Q ( D .Q B))
9-Dec-2019	appdiv0nq 6402	Approximate division for positive rationals. This can be thought of as a variation of appdivnq 6401 in which A is zero, although it can be stated and proved in terms of positive rationals alone, without zero as such. (Contributed by Jim Kingdon, 9-Dec-2019.)
|- ((B e. Q. /\ C e. Q.) -> E. m e. Q. ( m .Q C) <Q B)
9-Dec-2019	ltmnqi 6256	Ordering property of multiplication for positive fractions. One direction of ltmnqg 6254. (Contributed by Jim Kingdon, 9-Dec-2019.)
|- ((A <Q B /\ C e. Q.) -> ( C .Q A) <Q ( C .Q B))
9-Dec-2019	ltanqi 6255	Ordering property of addition for positive fractions. One direction of ltanqg 6253. (Contributed by Jim Kingdon, 9-Dec-2019.)
|- ((A <Q B /\ C e. Q.) -> ( C +Q A) <Q ( C +Q B))
8-Dec-2019	bj-nn0sucALT 7335	Alternate proof of bj-nn0suc 7321, also constructive but from ax-inf2 7333, hence requiring ax-bdsetind 7325. (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (A e. om <-> (A = (/) \/ E.x e. om A = suc x))
8-Dec-2019	bj-omex2 7334	Using bounded set induction and the strong axiom of infinity, om is a set, that is, we recover ax-infvn 7302 (see bj-2inf 7299 for the equivalence of the latter with bj-omex 7303). (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- om e. _V
8-Dec-2019	bj-inf2vn2 7332	A sufficient condition for om to be a set; unbounded version of bj-inf2vn 7331. (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.)
|- (A e. V -> (A.x(x e. A <-> (x = (/) \/ E.y e. A x = suc y)) -> A = om))
8-Dec-2019	bj-inf2vn 7331	A sufficient condition for om to be a set. See bj-inf2vn2 7332 for the unbounded version from full set induction. (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.)
|- BOUNDED A   =>   |- (A e. V -> (A.x(x e. A <-> (x = (/) \/ E.y e. A x = suc y)) -> A = om))
8-Dec-2019	bj-inf2vnlem4 7330	Lemma for bj-inf2vn2 7332. (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.)
|- (A.x e. A (x = (/) \/ E.y e. A x = suc y) -> (Ind Z -> A C_ Z))
8-Dec-2019	bj-inf2vnlem3 7329	Lemma for bj-inf2vn 7331. (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.)
|- BOUNDED A   &   |- BOUNDED Z   =>   |- (A.x e. A (x = (/) \/ E.y e. A x = suc y) -> (Ind Z -> A C_ Z))
8-Dec-2019	bj-inf2vnlem2 7328	Lemma for bj-inf2vnlem3 7329 and bj-inf2vnlem4 7330. Remark: unoptimized proof (have to use more deduction style). (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.)
|- (A.x e. A (x = (/) \/ E.y e. A x = suc y) -> (Ind Z -> A.u(A. t e. u ( t e. A -> t e. Z) -> (u e. A -> u e. Z))))
8-Dec-2019	bj-inf2vnlem1 7327	Lemma for bj-inf2vn 7331. Remark: unoptimized proof (have to use more deduction style). (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.)
|- (A.x(x e. A <-> (x = (/) \/ E.y e. A x = suc y)) -> Ind A)
8-Dec-2019	bj-bdcel 7203	Boundedness of a membership formula. (Contributed by BJ, 8-Dec-2019.)
|- BOUNDED y = A   =>   |- BOUNDED A e. x
8-Dec-2019	bj-ex 7148	Existential generalization. (Contributed by BJ, 8-Dec-2019.) Proof modification is discouraged because there are shorter proofs, but using less basic results (like exlimiv 1467 and 19.9ht 1510 or 19.23ht 1363). (Proof modification is discouraged.)
|- (E.xph -> ph)
8-Dec-2019	mullocpr 6409	Locatedness of multiplication on positive reals. Lemma 12.9 in [BauerTaylor], p. 56 (but where both A and B are positive, not just A). (Contributed by Jim Kingdon, 8-Dec-2019.)
|- ((A e. P. /\ B e. P.) -> A. q e. Q. A. r e. Q. ( q <Q r -> ( q e. ( 1st ` (A .P. B)) \/ r e. ( 2nd ` (A .P. B)))))
8-Dec-2019	prmuloc 6404	Positive reals are multiplicatively located. Lemma 12.8 of [BauerTaylor], p. 56. (Contributed by Jim Kingdon, 8-Dec-2019.)
|- (( <. L , U >. e. P. /\ A <Q B) -> E. d e. Q. E.u e. Q. ( d e. L /\ u e. U /\ (u .Q A) <Q ( d .Q B)))
8-Dec-2019	appdivnq 6401	Approximate division for positive rationals. Proposition 12.7 of [BauerTaylor], p. 55 (a special case where A and B are positive, as well as C). Our proof is simpler than the one in BauerTaylor because we have reciprocals. (Contributed by Jim Kingdon, 8-Dec-2019.)
|- ((A <Q B /\ C e. Q.) -> E. m e. Q. (A <Q ( m .Q C) /\ ( m .Q C) <Q B))
8-Dec-2019	nqprlu 6395	The canonical embedding of the rationals into the reals. (Contributed by Jim Kingdon, 8-Dec-2019.)
|- (A e. Q. -> <. {x | x <Q A } , {x | A <Q x } >. e. P.)
8-Dec-2019	nqprloc 6394	A cut produced from a rational is located. Lemma for nqprlu 6395. (Contributed by Jim Kingdon, 8-Dec-2019.)
|- (A e. Q. -> A. q e. Q. A. r e. Q. ( q <Q r -> ( q e. {x | x <Q A } \/ r e. {x | A <Q x })))
8-Dec-2019	nqprdisj 6393	A cut produced from a rational is disjoint. Lemma for nqprlu 6395. (Contributed by Jim Kingdon, 8-Dec-2019.)
|- (A e. Q. -> A. q e. Q. -. ( q e. {x | x <Q A } /\ q e. {x | A <Q x }))
8-Dec-2019	nqprrnd 6392	A cut produced from a rational is rounded. Lemma for nqprlu 6395. (Contributed by Jim Kingdon, 8-Dec-2019.)
|- (A e. Q. -> (A. q e. Q. ( q e. {x | x <Q A } <-> E. r e. Q. ( q <Q r /\ r e. {x | x <Q A })) /\ A. r e. Q. ( r e. {x | A <Q x } <-> E. q e. Q. ( q <Q r /\ q e. {x | A <Q x }))))
8-Dec-2019	nqprm 6391	A cut produced from a rational is inhabited. Lemma for nqprlu 6395. (Contributed by Jim Kingdon, 8-Dec-2019.)
|- (A e. Q. -> (E. q e. Q. q e. {x | x <Q A } /\ E. r e. Q. r e. {x | A <Q x }))
8-Dec-2019	mpvlu 6388	Value of multiplication on positive reals. (Contributed by Jim Kingdon, 8-Dec-2019.)
|- ((A e. P. /\ B e. P.) -> (A .P. B) = <. {x e. Q. | E.y e. ( 1st ` A)E.z e. ( 1st ` B)x = (y .Q z) } , {x e. Q. | E.y e. ( 2nd ` A)E.z e. ( 2nd ` B)x = (y .Q z) } >.)
8-Dec-2019	plpvlu 6387	Value of addition on positive reals. (Contributed by Jim Kingdon, 8-Dec-2019.)
|- ((A e. P. /\ B e. P.) -> (A +P. B) = <. {x e. Q. | E.y e. ( 1st ` A)E.z e. ( 1st ` B)x = (y +Q z) } , {x e. Q. | E.y e. ( 2nd ` A)E.z e. ( 2nd ` B)x = (y +Q z) } >.)
7-Dec-2019	addlocprlemeqgt 6381	Lemma for addlocpr 6385. This is a step used in both the Q = ( D +Q E) and ( D +Q E) <Q Q cases. (Contributed by Jim Kingdon, 7-Dec-2019.)
|- (ph -> A e. P.)   &   |- (ph -> B e. P.)   &   |- (ph -> Q <Q R)   &   |- (ph -> P e. Q.)   &   |- (ph -> ( Q +Q ( P +Q P)) = R)   &   |- (ph -> D e. ( 1st ` A))   &   |- (ph -> U e. ( 2nd ` A))   &   |- (ph -> U <Q ( D +Q P))   &   |- (ph -> E e. ( 1st ` B))   &   |- (ph -> T e. ( 2nd ` B))   &   |- (ph -> T <Q ( E +Q P))   =>   |- (ph -> ( U +Q T) <Q (( D +Q E) +Q ( P +Q P)))
7-Dec-2019	addnqprulem 6377	Lemma to prove upward closure in positive real addition. (Contributed by Jim Kingdon, 7-Dec-2019.)
|- ((( <. L , U >. e. P. /\ G e. U) /\ X e. Q.) -> ( S <Q X -> (( X .Q ( *Q ` S)) .Q G) e. U))
7-Dec-2019	addnqprllem 6376	Lemma to prove downward closure in positive real addition. (Contributed by Jim Kingdon, 7-Dec-2019.)
|- ((( <. L , U >. e. P. /\ G e. L) /\ X e. Q.) -> ( X <Q S -> (( X .Q ( *Q ` S)) .Q G) e. L))
7-Dec-2019	lt2addnq 6257	Ordering property of addition for positive fractions. (Contributed by Jim Kingdon, 7-Dec-2019.)
|- (((A e. Q. /\ B e. Q.) /\ ( C e. Q. /\ D e. Q.)) -> ((A <Q B /\ C <Q D) -> (A +Q C) <Q (B +Q D)))
6-Dec-2019	addlocprlem 6384	Lemma for addlocpr 6385. The result, in deduction form. (Contributed by Jim Kingdon, 6-Dec-2019.)
|- (ph -> A e. P.)   &   |- (ph -> B e. P.)   &   |- (ph -> Q <Q R)   &   |- (ph -> P e. Q.)   &   |- (ph -> ( Q +Q ( P +Q P)) = R)   &   |- (ph -> D e. ( 1st ` A))   &   |- (ph -> U e. ( 2nd ` A))   &   |- (ph -> U <Q ( D +Q P))   &   |- (ph -> E e. ( 1st ` B))   &   |- (ph -> T e. ( 2nd ` B))   &   |- (ph -> T <Q ( E +Q P))   =>   |- (ph -> ( Q e. ( 1st ` (A +P. B)) \/ R e. ( 2nd ` (A +P. B))))
6-Dec-2019	addlocprlemgt 6383	Lemma for addlocpr 6385. The ( D +Q E) <Q Q case. (Contributed by Jim Kingdon, 6-Dec-2019.)
|- (ph -> A e. P.)   &   |- (ph -> B e. P.)   &   |- (ph -> Q <Q R)   &   |- (ph -> P e. Q.)   &   |- (ph -> ( Q +Q ( P +Q P)) = R)   &   |- (ph -> D e. ( 1st ` A))   &   |- (ph -> U e. ( 2nd ` A))   &   |- (ph -> U <Q ( D +Q P))   &   |- (ph -> E e. ( 1st ` B))   &   |- (ph -> T e. ( 2nd ` B))   &   |- (ph -> T <Q ( E +Q P))   =>   |- (ph -> (( D +Q E) <Q Q -> R e. ( 2nd ` (A +P. B))))
6-Dec-2019	addlocprlemeq 6382	Lemma for addlocpr 6385. The Q = ( D +Q E) case. (Contributed by Jim Kingdon, 6-Dec-2019.)
|- (ph -> A e. P.)   &   |- (ph -> B e. P.)   &   |- (ph -> Q <Q R)   &   |- (ph -> P e. Q.)   &   |- (ph -> ( Q +Q ( P +Q P)) = R)   &   |- (ph -> D e. ( 1st ` A))   &   |- (ph -> U e. ( 2nd ` A))   &   |- (ph -> U <Q ( D +Q P))   &   |- (ph -> E e. ( 1st ` B))   &   |- (ph -> T e. ( 2nd ` B))   &   |- (ph -> T <Q ( E +Q P))   =>   |- (ph -> ( Q = ( D +Q E) -> R e. ( 2nd ` (A +P. B))))
6-Dec-2019	addlocprlemlt 6380	Lemma for addlocpr 6385. The Q <Q ( D +Q E) case. (Contributed by Jim Kingdon, 6-Dec-2019.)
|- (ph -> A e. P.)   &   |- (ph -> B e. P.)   &   |- (ph -> Q <Q R)   &   |- (ph -> P e. Q.)   &   |- (ph -> ( Q +Q ( P +Q P)) = R)   &   |- (ph -> D e. ( 1st ` A))   &   |- (ph -> U e. ( 2nd ` A))   &   |- (ph -> U <Q ( D +Q P))   &   |- (ph -> E e. ( 1st ` B))   &   |- (ph -> T e. ( 2nd ` B))   &   |- (ph -> T <Q ( E +Q P))   =>   |- (ph -> ( Q <Q ( D +Q E) -> Q e. ( 1st ` (A +P. B))))
5-Dec-2019	addlocpr 6385	Locatedness of addition on positive reals. Lemma 11.16 in [BauerTaylor], p. 53. The proof in BauerTaylor relies on signed rationals, so we replace it with another proof which applies prarloc 6351 to both A and B, and uses nqtri3or 6249 rather than prloc 6339 to decide whether q is too big to be in the lower cut of A +P. B (and deduce that if it is, then r must be in the upper cut). What the two proofs have in common is that they take the difference between q and r to determine how tight a range they need around the real numbers. (Contributed by Jim Kingdon, 5-Dec-2019.)
|- ((A e. P. /\ B e. P.) -> A. q e. Q. A. r e. Q. ( q <Q r -> ( q e. ( 1st ` (A +P. B)) \/ r e. ( 2nd ` (A +P. B)))))
5-Dec-2019	addnqpru 6379	Lemma to prove upward closure in positive real addition. (Contributed by Jim Kingdon, 5-Dec-2019.)
|- ((((A e. P. /\ G e. ( 2nd ` A)) /\ (B e. P. /\ H e. ( 2nd ` B))) /\ X e. Q.) -> (( G +Q H) <Q X -> X e. ( 2nd ` (A +P. B))))
5-Dec-2019	addnqprl 6378	Lemma to prove downward closure in positive real addition. (Contributed by Jim Kingdon, 5-Dec-2019.)
|- ((((A e. P. /\ G e. ( 1st ` A)) /\ (B e. P. /\ H e. ( 1st ` B))) /\ X e. Q.) -> ( X <Q ( G +Q H) -> X e. ( 1st ` (A +P. B))))
5-Dec-2019	genpmu 6367	The upper cut produced by addition or multiplication on positive reals is inhabited. (Contributed by Jim Kingdon, 5-Dec-2019.)
|- F = (w e. P. , v e. P. |-> <. {x e. Q. | E.y e. Q. E.z e. Q. (y e. ( 1st ` w) /\ z e. ( 1st ` v) /\ x = (y Gz)) } , {x e. Q. | E.y e. Q. E.z e. Q. (y e. ( 2nd ` w) /\ z e. ( 2nd ` v) /\ x = (y Gz)) } >.)   &   |- ((y e. Q. /\ z e. Q.) -> (y Gz) e. Q.)   =>   |- ((A e. P. /\ B e. P.) -> E. q e. Q. q e. ( 2nd ` (A FB)))
5-Dec-2019	genpelxp 6359	Set containing the result of adding or multiplying positive reals. (Contributed by Jim Kingdon, 5-Dec-2019.)
|- F = (w e. P. , v e. P. |-> <. {x e. Q. | E.y e. Q. E.z e. Q. (y e. ( 1st ` w) /\ z e. ( 1st ` v) /\ x = (y Gz)) } , {x e. Q. | E.y e. Q. E.z e. Q. (y e. ( 2nd ` w) /\ z e. ( 2nd ` v) /\ x = (y Gz)) } >.)   =>   |- ((A e. P. /\ B e. P.) -> (A FB) e. ( ~P Q. X. ~P Q.))
3-Dec-2019	addassnq0lemcl 6310	A natural number closure law. Lemma for addassnq0 6311. (Contributed by Jim Kingdon, 3-Dec-2019.)
|- ((( I e. om /\ J e. N.) /\ ( K e. om /\ L e. N.)) -> ((( I .o L) +o ( J .o K)) e. om /\ ( J .o L) e. N.))
3-Dec-2019	nndir 5980	Distributive law for natural numbers (right-distributivity). (Contributed by Jim Kingdon, 3-Dec-2019.)
|- ((A e. om /\ B e. om /\ C e. om) -> ((A +o B) .o C) = ((A .o C) +o (B .o C)))
1-Dec-2019	nnanq0 6307	Addition of non-negative fractions with a common denominator. You can add two fractions with the same denominator by adding their numerators and keeping the same denominator. (Contributed by Jim Kingdon, 1-Dec-2019.)
|- (( N e. om /\ M e. om /\ A e. N.) -> [ <.( N +o M) , A >.] ~Q0 = ([ <. N , A >.] ~Q0 +Q0 [ <. M , A >.] ~Q0 ))
1-Dec-2019	archnqq 6268	For any fraction, there is an integer that is greater than it. This is also known as the "archimedean property". (Contributed by Jim Kingdon, 1-Dec-2019.)
|- (A e. Q. -> E.x e. N. A <Q [ <.x , 1o >.] ~Q )
30-Nov-2019	bj-2inf 7299	Two formulations of the axiom of infinity (see ax-infvn 7302 and bj-omex 7303) . (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.)
|- ( om e. _V <-> E.x(Ind x /\ A.y(Ind y -> x C_ y)))
30-Nov-2019	bj-om 7298	A set is equal to om if and only if it is the smallest inductive set. (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.)
|- (A e. V -> (A = om <-> (Ind A /\ A.x(Ind x -> A C_ x))))
30-Nov-2019	bj-ssom 7297	A characterization of subclasses of om. (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.)
|- (A.x(Ind x -> A C_ x) <-> A C_ om)
30-Nov-2019	bj-omssind 7296	om is included in all the inductive sets (but for the moment, we cannot prove that it is included in all the inductive classes). (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.)
|- (A e. V -> (Ind A -> om C_ A))
30-Nov-2019	bj-omind 7295	om is an inductive class. (Contributed by BJ, 30-Nov-2019.)
|- Ind om
30-Nov-2019	bj-dfom 7294	Alternate definition of om, as the intersection of all the inductive sets. Proposal: make this the definition. (Contributed by BJ, 30-Nov-2019.)
|- om = |^| {x | Ind x }
30-Nov-2019	bj-indint 7293	The property of being an inductive class is closed under intersections. (Contributed by BJ, 30-Nov-2019.)
|- Ind |^| {x e. A | Ind x }
30-Nov-2019	bj-bdind 7292	Boundedness of the formula "the setvar x is an inductive class". (Contributed by BJ, 30-Nov-2019.)
|- BOUNDED Ind x
30-Nov-2019	bj-indeq 7291	Equality property for Ind. (Contributed by BJ, 30-Nov-2019.)
|- (A = B -> (Ind A <-> Ind B))
30-Nov-2019	bj-indsuc 7290	A direct consequence of the definition of Ind. (Contributed by BJ, 30-Nov-2019.)
|- (Ind A -> (B e. A -> suc B e. A))
30-Nov-2019	df-bj-ind 7289	Define the property of being an inductive class. (Contributed by BJ, 30-Nov-2019.)
|- (Ind A <-> ( (/) e. A /\ A.x e. A suc x e. A))
30-Nov-2019	bj-bdsucel 7248	Boundedness of the formula "the successor of the setvar x belongs to the setvar y". (Contributed by BJ, 30-Nov-2019.)
|- BOUNDED suc x e. y
30-Nov-2019	bj-bd0el 7234	Boundedness of the formula "the empty set belongs to the setvar x". (Contributed by BJ, 30-Nov-2019.)
|- BOUNDED (/) e. x
30-Nov-2019	bj-sseq 7177	If two converse inclusions are characterized each by a formula, then equality is characterized by the conjunction of these formulas. (Contributed by BJ, 30-Nov-2019.)
|- (ph -> (ps <-> A C_ B))   &   |- (ph -> (ch <-> B C_ A))   =>   |- (ph -> ((ps /\ ch) <-> A = B))
30-Nov-2019	nqpnq0nq 6302	A positive fraction plus a non-negative fraction is a positive fraction. (Contributed by Jim Kingdon, 30-Nov-2019.)
|- ((A e. Q. /\ B e. Q0) -> (A +Q0 B) e. Q.)
30-Nov-2019	mulclnq0 6301	Closure of multiplication on non-negative fractions. (Contributed by Jim Kingdon, 30-Nov-2019.)
|- ((A e. Q0 /\ B e. Q0) -> (A ·Q0 B) e. Q0)
30-Nov-2019	prarloclemarch 6269	A version of the Archimedean property. This variation is "stronger" than archnqq 6268 in the sense that we provide an integer which is larger than a given rational A even after being multiplied by a second rational B. (Contributed by Jim Kingdon, 30-Nov-2019.)
|- ((A e. Q. /\ B e. Q.) -> E.x e. N. A <Q ([ <.x , 1o >.] ~Q .Q B))
29-Nov-2019	bj-elssuniab 7176	Version of elssuni 3578 using a class abstraction and explicit substitution. (Contributed by BJ, 29-Nov-2019.)
|- F/_xA   =>   |- (A e. V -> ( [.A / x ].ph -> A C_ U. {x | ph }))
29-Nov-2019	bj-intabssel1 7175	Version of intss1 3600 using a class abstraction and implicit substitution. Closed form of intmin3 3612. (Contributed by BJ, 29-Nov-2019.)
|- F/_xA   &   |- F/xps   &   |- (x = A -> (ps -> ph))   =>   |- (A e. V -> (ps -> |^| {x | ph } C_ A))
29-Nov-2019	bj-intabssel 7174	Version of intss1 3600 using a class abstraction and explicit substitution. (Contributed by BJ, 29-Nov-2019.)
|- F/_xA   =>   |- (A e. V -> ( [.A / x ].ph -> |^| {x | ph } C_ A))
29-Nov-2019	nq02m 6313	Multiply a non-negative fraction by two. (Contributed by Jim Kingdon, 29-Nov-2019.)
|- (A e. Q0 -> ([ <. 2o , 1o >.] ~Q0 ·Q0 A) = (A +Q0 A))
29-Nov-2019	distnq0r 6312	Multiplication of non-negative fractions is distributive. Version of distrnq0 6308 with the multiplications commuted. (Contributed by Jim Kingdon, 29-Nov-2019.)
|- ((A e. Q0 /\ B e. Q0 /\ C e. Q0) -> ((B +Q0 C) ·Q0 A) = ((B ·Q0 A) +Q0 ( C ·Q0 A)))
29-Nov-2019	addassnq0 6311	Addition of non-negaative fractions is associative. (Contributed by Jim Kingdon, 29-Nov-2019.)
|- ((A e. Q0 /\ B e. Q0 /\ C e. Q0) -> ((A +Q0 B) +Q0 C) = (A +Q0 (B +Q0 C)))
29-Nov-2019	addclnq0 6300	Closure of addition on non-negative fractions. (Contributed by Jim Kingdon, 29-Nov-2019.)
|- ((A e. Q0 /\ B e. Q0) -> (A +Q0 B) e. Q0)
29-Nov-2019	mulcanenq0ec 6294	Lemma for distributive law: cancellation of common factor. (Contributed by Jim Kingdon, 29-Nov-2019.)
|- ((A e. N. /\ B e. om /\ C e. N.) -> [ <.(A .o B) , (A .o C) >.] ~Q0 = [ <.B , C >.] ~Q0 )
28-Nov-2019	ax-bdsetind 7325	Axiom of bounded set induction. (Contributed by BJ, 28-Nov-2019.)
|- BOUNDED ph   =>   |- (A. a(A.y e. a [y / a]ph -> ph) -> A. aph)
28-Nov-2019	bj-peano4 7316	Remove from peano4 4243 dependency on ax-setind 4200. Therefore, it only requires core constructive axioms (albeit more of them). (Contributed by BJ, 28-Nov-2019.) (Proof modification is discouraged.)
|- ((A e. om /\ B e. om) -> ( suc A = suc B <-> A = B))
28-Nov-2019	bj-nnen2lp 7315	A version of en2lp 4212 for natural numbers, which does not require ax-setind 4200. Note: using this theorem and bj-nnelirr 7314, one can remove dependency on ax-setind 4200 from nntri2 5984 and nndcel 5987; one can actually remove more dependencies from these. (Contributed by BJ, 28-Nov-2019.) (Proof modification is discouraged.)
|- ((A e. om /\ B e. om) -> -. (A e. B /\ B e. A))
27-Nov-2019	mulcomnq0 6309	Multiplication of non-negative fractions is commutative. (Contributed by Jim Kingdon, 27-Nov-2019.)
|- ((A e. Q0 /\ B e. Q0) -> (A ·Q0 B) = (B ·Q0 A))
27-Nov-2019	distrnq0 6308	Multiplication of non-negative fractions is distributive. (Contributed by Jim Kingdon, 27-Nov-2019.)
|- ((A e. Q0 /\ B e. Q0 /\ C e. Q0) -> (A ·Q0 (B +Q0 C)) = ((A ·Q0 B) +Q0 (A ·Q0 C)))
25-Nov-2019	prcunqu 6333	An upper cut is closed upwards under the positive fractions. (Contributed by Jim Kingdon, 25-Nov-2019.)
|- (( <. L , U >. e. P. /\ C e. U) -> ( C <Q B -> B e. U))
25-Nov-2019	prarloclemarch2 6270	Like prarloclemarch 6269 but the integer must be at least two, and there is also B added to the right hand side. These details follow straightforwardly but are chosen to be helpful in the proof of prarloc 6351. (Contributed by Jim Kingdon, 25-Nov-2019.)
|- ((A e. Q. /\ B e. Q. /\ C e. Q.) -> E.x e. N. ( 1o <N x /\ A <Q (B +Q ([ <.x , 1o >.] ~Q .Q C))))
25-Nov-2019	subhalfnqq 6265	There is a number which is less than half of any positive fraction. The case where A is one is Lemma 11.4 of [BauerTaylor], p. 50, and they use the word "approximate half" for such a number (since there may be constructions, for some structures other than the rationals themselves, which rely on such an approximate half but do not require division by two as seen at halfnqq 6261). (Contributed by Jim Kingdon, 25-Nov-2019.)
|- (A e. Q. -> E.x e. Q. (x +Q x) <Q A)
24-Nov-2019	bj-nnelirr 7314	A natural number does not belong to itself. Version of elirr 4204 for natural numbers, which does not require ax-setind 4200. (Contributed by BJ, 24-Nov-2019.) (Proof modification is discouraged.)
|- (A e. om -> -. A e. A)
24-Nov-2019	bdcriota 7249	A class given by a restricted definition binder is bounded, under the given hypotheses. (Contributed by BJ, 24-Nov-2019.)
|- BOUNDED ph   &   |- E!x e. y ph   =>   |- BOUNDED ( iota_x e. y ph)
24-Nov-2019	nq0nn 6291	Decomposition of a non-negative fraction into numerator and denominator. (Contributed by Jim Kingdon, 24-Nov-2019.)
|- (A e. Q0 -> E.wE.v((w e. om /\ v e. N.) /\ A = [ <.w , v >.] ~Q0 ))
24-Nov-2019	enq0eceq 6286	Equivalence class equality of non-negative fractions in terms of natural numbers. (Contributed by Jim Kingdon, 24-Nov-2019.)
|- (((A e. om /\ B e. N.) /\ ( C e. om /\ D e. N.)) -> ([ <.A , B >.] ~Q0 = [ <. C , D >.] ~Q0 <-> (A .o D) = (B .o C)))
24-Nov-2019	dfplq0qs 6279	Addition on non-negative fractions. This definition is similar to df-plq0 6276 but expands Q0 (Contributed by Jim Kingdon, 24-Nov-2019.)
|- +Q0 = { <. <.x , y >. , z >. | ((x e. (( om X. N.) /. ~Q0 ) /\ y e. (( om X. N.) /. ~Q0 )) /\ E.wE.vE.uE.f((x = [ <.w , v >.] ~Q0 /\ y = [ <.u , f >.] ~Q0 ) /\ z = [ <.((w .o f) +o (v .o u)) , (v .o f) >.] ~Q0 )) }
23-Nov-2019	addnq0mo 6296	There is at most one result from adding non-negative fractions. (Contributed by Jim Kingdon, 23-Nov-2019.)
|- ((A e. (( om X. N.) /. ~Q0 ) /\ B e. (( om X. N.) /. ~Q0 )) -> E*zE.wE.vE.uE. t((A = [ <.w , v >.] ~Q0 /\ B = [ <.u , t >.] ~Q0 ) /\ z = [ <.((w .o t) +o (v .o u)) , (v .o t) >.] ~Q0 ))
23-Nov-2019	nnnq0lem1 6295	Decomposing non-negative fractions into natural numbers. Lemma for addnnnq0 6298 and mulnnnq0 6299. (Contributed by Jim Kingdon, 23-Nov-2019.)
|- (((A e. (( om X. N.) /. ~Q0 ) /\ B e. (( om X. N.) /. ~Q0 )) /\ (((A = [ <.w , v >.] ~Q0 /\ B = [ <.u , t >.] ~Q0 ) /\ z = [ C] ~Q0 ) /\ ((A = [ <. s , f >.] ~Q0 /\ B = [ <.g , h >.] ~Q0 ) /\ q = [ D] ~Q0 ))) -> ((((w e. om /\ v e. N.) /\ ( s e. om /\ f e. N.)) /\ ((u e. om /\ t e. N.) /\ (g e. om /\ h e. N.))) /\ ((w .o f) = (v .o s) /\ (u .o h) = ( t .o g))))
23-Nov-2019	addcmpblnq0 6292	Lemma showing compatibility of addition on non-negative fractions. (Contributed by Jim Kingdon, 23-Nov-2019.)
|- ((((A e. om /\ B e. N.) /\ ( C e. om /\ D e. N.)) /\ (( F e. om /\ G e. N.) /\ ( R e. om /\ S e. N.))) -> (((A .o D) = (B .o C) /\ ( F .o S) = ( G .o R)) -> <.((A .o G) +o (B .o F)) , (B .o G) >. ~Q0 <.(( C .o S) +o ( D .o R)) , ( D .o S) >.))
23-Nov-2019	ee8anv 1788	Rearrange existential quantifiers. (Contributed by Jim Kingdon, 23-Nov-2019.)
|- (E.xE.yE.zE.wE.vE.uE. tE. s(ph /\ ps) <-> (E.xE.yE.zE.wph /\ E.vE.uE. tE. sps))
23-Nov-2019	19.42vvvv 1768	Theorem 19.42 of [Margaris] p. 90 with 4 quantifiers. (Contributed by Jim Kingdon, 23-Nov-2019.)
|- (E.wE.xE.yE.z(ph /\ ps) <-> (ph /\ E.wE.xE.yE.zps))
22-Nov-2019	bdsetindis 7326	Axiom of bounded set induction using implicit substitutions. (Contributed by BJ, 22-Nov-2019.) (Proof modification is discouraged.)
|- BOUNDED ph   &   |- F/xps   &   |- F/xch   &   |- F/yph   &   |- F/yps   &   |- (x = z -> (ph -> ps))   &   |- (x = y -> (ch -> ph))   =>   |- (A.y(A.z e. y ps -> ch) -> A.xph)
22-Nov-2019	setindis 7324	Axiom of set induction using implicit substitutions. (Contributed by BJ, 22-Nov-2019.)
|- F/xps   &   |- F/xch   &   |- F/yph   &   |- F/yps   &   |- (x = z -> (ph -> ps))   &   |- (x = y -> (ch -> ph))   =>   |- (A.y(A.z e. y ps -> ch) -> A.xph)
22-Nov-2019	setindf 7323	Axiom of set-induction with a DV condition replaced with a non-freeness hypothesis (Contributed by BJ, 22-Nov-2019.)
|- F/yph   =>   |- (A.x(A.y e. x [y / x]ph -> ph) -> A.xph)
22-Nov-2019	setindft 7322	Axiom of set-induction with a DV condition replaced with a non-freeness hypothesis (Contributed by BJ, 22-Nov-2019.)
|- (A.x F/yph -> (A.x(A.y e. x [y / x]ph -> ph) -> A.xph))
22-Nov-2019	bj-nntrans2 7313	A natural number is a transitive set. (Contributed by BJ, 22-Nov-2019.) (Proof modification is discouraged.)
|- (A e. om -> Tr A)
22-Nov-2019	bj-nntrans 7312	A natural number is a transitive set. (Contributed by BJ, 22-Nov-2019.) (Proof modification is discouraged.)
|- (A e. om -> (B e. A -> B C_ A))
22-Nov-2019	bdfind 7307	Bounded induction (principle of induction when A is assumed to be bounded), proved from basic constructive axioms. See find 4245 for a nonconstructive proof of the general case. See findset 7306 for a proof when A is assumed to be a set. (Contributed by BJ, 22-Nov-2019.) (Proof modification is discouraged.)
|- BOUNDED A   =>   |- ((A C_ om /\ (/) e. A /\ A.x e. A suc x e. A) -> A = om)
22-Nov-2019	findset 7306	Bounded induction (principle of induction when A is assumed to be a set) allowing a proof from basic constructive axioms. See find 4245 for a nonconstructive proof of the general case. See bdfind 7307 for a proof when A is assumed to be bounded. (Contributed by BJ, 22-Nov-2019.) (Proof modification is discouraged.)
|- (A e. V -> ((A C_ om /\ (/) e. A /\ A.x e. A suc x e. A) -> A = om))
22-Nov-2019	cbvrald 7173	Rule used to change bound variables, using implicit substitution. (Contributed by BJ, 22-Nov-2019.)
|- F/xph   &   |- F/yph   &   |- (ph -> F/yps)   &   |- (ph -> F/xch)   &   |- (ph -> (x = y -> (ps <-> ch)))   =>   |- (ph -> (A.x e. A ps <-> A.y e. A ch))
22-Nov-2019	addnnnq0 6298	Addition of non-negative fractions in terms of natural numbers. (Contributed by Jim Kingdon, 22-Nov-2019.)
|- (((A e. om /\ B e. N.) /\ ( C e. om /\ D e. N.)) -> ([ <.A , B >.] ~Q0 +Q0 [ <. C , D >.] ~Q0 ) = [ <.((A .o D) +o (B .o C)) , (B .o D) >.] ~Q0 )
22-Nov-2019	dfmq0qs 6278	Multiplication on non-negative fractions. This definition is similar to df-mq0 6277 but expands Q0 (Contributed by Jim Kingdon, 22-Nov-2019.)
|- ·Q0 = { <. <.x , y >. , z >. | ((x e. (( om X. N.) /. ~Q0 ) /\ y e. (( om X. N.) /. ~Q0 )) /\ E.wE.vE.uE.f((x = [ <.w , v >.] ~Q0 /\ y = [ <.u , f >.] ~Q0 ) /\ z = [ <.(w .o u) , (v .o f) >.] ~Q0 )) }
21-Nov-2019	bj-findes 7338	Principle of induction, using explicit substitutions. Constructive proof (from CZF). See the comment of bj-findis 7336 for explanations. From this version, it is easy to prove findes 4249. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.)
|- (( [. (/) / x ].ph /\ A.x e. om (ph -> [. suc x / x ].ph)) -> A.x e. om ph)
21-Nov-2019	bj-findisg 7337	Version of bj-findis 7336 using a class term in the consequent. Constructive proof (from CZF). See the comment of bj-findis 7336 for explanations. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.)
|- F/xps   &   |- F/xch   &   |- F/xth   &   |- (x = (/) -> (ps -> ph))   &   |- (x = y -> (ph -> ch))   &   |- (x = suc y -> (th -> ph))   &   |- F/_xA   &   |- F/xta   &   |- (x = A -> (ph -> ta))   =>   |- ((ps /\ A.y e. om (ch -> th)) -> (A e. om -> ta))
21-Nov-2019	bj-bdfindes 7310	Bounded induction (principle of induction for bounded formulas), using explicit substitutions. Constructive proof (from CZF). See the comment of bj-bdfindis 7308 for explanations. From this version, it is easy to prove the bounded version of findes 4249. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.)
|- BOUNDED ph   =>   |- (( [. (/) / x ].ph /\ A.x e. om (ph -> [. suc x / x ].ph)) -> A.x e. om ph)
21-Nov-2019	bj-bdfindisg 7309	Version of bj-bdfindis 7308 using a class term in the consequent. Constructive proof (from CZF). See the comment of bj-bdfindis 7308 for explanations. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.)
|- BOUNDED ph   &   |- F/xps   &   |- F/xch   &   |- F/xth   &   |- (x = (/) -> (ps -> ph))   &   |- (x = y -> (ph -> ch))   &   |- (x = suc y -> (th -> ph))   &   |- F/_xA   &   |- F/xta   &   |- (x = A -> (ph -> ta))   =>   |- ((ps /\ A.y e. om (ch -> th)) -> (A e. om -> ta))
21-Nov-2019	bj-bdfindis 7308	Bounded induction (principle of induction for bounded formulas), using implicit substitutions (the biconditional versions of the hypotheses are implicit substitutions, and we have weakened them to implications). Constructive proof (from CZF). See finds 4246 for a proof of full induction in IZF. From this version, it is easy to prove bounded versions of finds 4246, finds2 4247, finds1 4248. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.)
|- BOUNDED ph   &   |- F/xps   &   |- F/xch   &   |- F/xth   &   |- (x = (/) -> (ps -> ph))   &   |- (x = y -> (ph -> ch))   &   |- (x = suc y -> (th -> ph))   =>   |- ((ps /\ A.y e. om (ch -> th)) -> A.x e. om ph)
21-Nov-2019	bdeqsuc 7247	Boundedness of the formula expressing that a setvar is equal to the successor of another. (Contributed by BJ, 21-Nov-2019.)
|- BOUNDED x = suc y
21-Nov-2019	bdop 7241	The ordered pair of two setvars is a bounded class. (Contributed by BJ, 21-Nov-2019.)
|- BOUNDED <.x , y >.
21-Nov-2019	bdeq0 7233	Boundedness of the formula expressing that a setvar is equal to the empty class. (Contributed by BJ, 21-Nov-2019.)
|- BOUNDED x = (/)
21-Nov-2019	bj-rspg 7172	Restricted specialization, generalized. Weakens a hypothesis of rspccv 2626 and seems to have a shorter proof. (Contributed by BJ, 21-Nov-2019.)
|- F/_xA   &   |- F/_xB   &   |- F/xps   &   |- (x = A -> (ph -> ps))   =>   |- (A.x e. B ph -> (A e. B -> ps))
21-Nov-2019	bj-rspgt 7171	Restricted specialization, generalized. Weakens a hypothesis of rspccv 2626 and seems to have a shorter proof. (Contributed by BJ, 21-Nov-2019.)
|- F/_xA   &   |- F/_xB   &   |- F/xps   =>   |- (A.x(x = A -> (ph -> ps)) -> (A.x e. B ph -> (A e. B -> ps)))
21-Nov-2019	elabg2 7170	One implication of elabg 2661. (Contributed by BJ, 21-Nov-2019.)
|- (x = A -> (ps -> ph))   =>   |- (A e. V -> (ps -> A e. {x | ph }))
21-Nov-2019	elab2a 7169	One implication of elab 2660. (Contributed by BJ, 21-Nov-2019.)
|- A e. _V   &   |- (x = A -> (ps -> ph))   =>   |- (ps -> A e. {x | ph })
21-Nov-2019	elab1 7168	One implication of elab 2660. (Contributed by BJ, 21-Nov-2019.)
|- (x = A -> (ph -> ps))   =>   |- (A e. {x | ph } -> ps)
21-Nov-2019	elabf2 7167	One implication of elabf 2659. (Contributed by BJ, 21-Nov-2019.)
|- F/xps   &   |- A e. _V   &   |- (x = A -> (ps -> ph))   =>   |- (ps -> A e. {x | ph })
21-Nov-2019	elabf1 7166	One implication of elabf 2659. (Contributed by BJ, 21-Nov-2019.)
|- F/xps   &   |- (x = A -> (ph -> ps))   =>   |- (A e. {x | ph } -> ps)
21-Nov-2019	elabgf2 7165	One implication of elabgf 2658. (Contributed by BJ, 21-Nov-2019.)
|- F/_xA   &   |- F/xps   &   |- (x = A -> (ps -> ph))   =>   |- (A e. B -> (ps -> A e. {x | ph }))
21-Nov-2019	elabgf1 7164	One implication of elabgf 2658. (Contributed by BJ, 21-Nov-2019.)
|- F/_xA   &   |- F/xps   &   |- (x = A -> (ph -> ps))   =>   |- (A e. {x | ph } -> ps)
21-Nov-2019	elabgft1 7163	One implication of elabgf 2658, in closed form. (Contributed by BJ, 21-Nov-2019.)
|- F/_xA   &   |- F/xps   =>   |- (A.x(x = A -> (ph -> ps)) -> (A e. {x | ph } -> ps))
21-Nov-2019	elabgf0 7162	Lemma for elabgf 2658. (Contributed by BJ, 21-Nov-2019.)
|- (x = A -> (A e. {x | ph } <-> ph))
21-Nov-2019	bj-vtoclgf 7161	Weakening two hypotheses of vtoclgf 2585. (Contributed by BJ, 21-Nov-2019.)
|- F/_xA   &   |- F/xps   &   |- (x = A -> ph)   &   |- (x = A -> (ph -> ps))   =>   |- (A e. V -> ps)
21-Nov-2019	bj-vtoclgft 7160	Weakening two hypotheses of vtoclgf 2585. (Contributed by BJ, 21-Nov-2019.)
|- F/_xA   &   |- F/xps   &   |- (x = A -> ph)   =>   |- (A.x(x = A -> (ph -> ps)) -> (A e. V -> ps))
21-Nov-2019	bj-exlimmpi 7156	Lemma for bj-vtoclgf 7161. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.)
|- F/xps   &   |- (ch -> ph)   &   |- (ch -> (ph -> ps))   =>   |- (E.xch -> ps)
21-Nov-2019	bj-exlimmp 7155	Lemma for bj-vtoclgf 7161. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.)
|- F/xps   &   |- (ch -> ph)   =>   |- (A.x(ch -> (ph -> ps)) -> (E.xch -> ps))
20-Nov-2019	mulnq0mo 6297	There is at most one result from multiplying non-negative fractions. (Contributed by Jim Kingdon, 20-Nov-2019.)
|- ((A e. (( om X. N.) /. ~Q0 ) /\ B e. (( om X. N.) /. ~Q0 )) -> E*zE.wE.vE.uE. t((A = [ <.w , v >.] ~Q0 /\ B = [ <.u , t >.] ~Q0 ) /\ z = [ <.(w .o u) , (v .o t) >.] ~Q0 ))
20-Nov-2019	mulcmpblnq0 6293	Lemma showing compatibility of multiplication on non-negative fractions. (Contributed by Jim Kingdon, 20-Nov-2019.)
|- ((((A e. om /\ B e. N.) /\ ( C e. om /\ D e. N.)) /\ (( F e. om /\ G e. N.) /\ ( R e. om /\ S e. N.))) -> (((A .o D) = (B .o C) /\ ( F .o S) = ( G .o R)) -> <.(A .o F) , (B .o G) >. ~Q0 <.( C .o R) , ( D .o S) >.))
19-Nov-2019	bj-nn0suc 7321	Proof of (biconditional form of) nn0suc 4250 from the core axioms of CZF. See also bj-nn0sucALT 7335. As a characterization of the elements of om, this could be labeled "elom". (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.)
|- (A e. om <-> (A = (/) \/ E.x e. om A = suc x))
19-Nov-2019	bj-nn0suc0 7311	Constructive proof of a variant of nn0suc 4250. For a constructive proof of nn0suc 4250, see bj-nn0suc 7321. (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.)
|- (A e. om -> (A = (/) \/ E.x e. A A = suc x))
19-Nov-2019	speano5 7305	Version of peano5 4244 when A is assumed to be a set, allowing a proof from the core axioms of CZF. (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.)
|- ((A e. V /\ (/) e. A /\ A.x e. om (x e. A -> suc x e. A)) -> om C_ A)
19-Nov-2019	bdpeano5 7304	Bounded version of peano5 4244. (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.)
|- BOUNDED A   =>   |- (( (/) e. A /\ A.x e. om (x e. A -> suc x e. A)) -> om C_ A)
19-Nov-2019	peano5set 7301	Version of peano5 4244 when om i^i A is assumed to be a set, allowing a proof from the core axioms of CZF. (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.)
|- (( om i^i A) e. V -> (( (/) e. A /\ A.x e. om (x e. A -> suc x e. A)) -> om C_ A))
19-Nov-2019	bj-inex 7269	The intersection of two sets is a set, from bounded separation. (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.)
|- ((A e. V /\ B e. W) -> (A i^i B) e. _V)
19-Nov-2019	bdrabexg 7268	Bounded version of rabexg 3870. (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.)
|- BOUNDED ph   &   |- BOUNDED A   =>   |- (A e. V -> {x e. A | ph } e. _V)
19-Nov-2019	bds 7217	Boundedness of a formula resulting from implicit substitution in a bounded formula. Note that the proof does not use ax-bdsb 7188; therefore, using implicit instead of explicit substitution when boundedness is important, one might avoid using ax-bdsb 7188. (Contributed by BJ, 19-Nov-2019.)
|- BOUNDED ph   &   |- (x = y -> (ph <-> ps))   =>   |- BOUNDED ps
19-Nov-2019	mulnnnq0 6299	Multiplication of non-negative fractions in terms of natural numbers. (Contributed by Jim Kingdon, 19-Nov-2019.)
|- (((A e. om /\ B e. N.) /\ ( C e. om /\ D e. N.)) -> ([ <.A , B >.] ~Q0 ·Q0 [ <. C , D >.] ~Q0 ) = [ <.(A .o C) , (B .o D) >.] ~Q0 )
18-Nov-2019	bj-peano2 7300	Constructive proof of peano2 4241. Temporary note: another possibility is to simply replace sucexg 4170 with bj-sucexg 7284 in the proof of peano2 4241. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
|- (A e. om -> suc A e. om)
18-Nov-2019	bj-intnexr 7271	vnex 3860 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
|- ( |^|A = _V -> -. |^|A e. _V)
18-Nov-2019	bj-intexr 7270	vnex 3860 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
|- ( |^|A e. _V -> A =/= (/))
18-Nov-2019	bj-vnex 7260	vnex 3860 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
|- -. E.x x = _V
18-Nov-2019	bj-nvel 7259	nvel 3859 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
|- -. _V e. A
18-Nov-2019	bj-vprc 7258	vprc 3858 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
|- -. _V e. _V
18-Nov-2019	bj-nalset 7257	nalset 3857 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
|- -. E.xA.y y e. x
18-Nov-2019	nqnq0 6290	A positive fraction is a non-negative fraction. (Contributed by Jim Kingdon, 18-Nov-2019.)
|- Q. C_ Q0
18-Nov-2019	nq0ex 6289	The class of positive fractions exists. (Contributed by Jim Kingdon, 18-Nov-2019.)
|- Q0 e. _V
18-Nov-2019	enq0ex 6288	The equivalence relation for positive fractions exists. (Contributed by Jim Kingdon, 18-Nov-2019.)
|- ~Q0 e. _V
14-Nov-2019	ax-inf2 7333	Another axiom of infinity in a constructive setting (see ax-infvn 7302). (Contributed by BJ, 14-Nov-2019.) (New usage is discouraged.)
|- E. aA.x(x e. a <-> (x = (/) \/ E.y e. a x = suc y))
14-Nov-2019	bj-omex 7303	Proof of omex 4239 from ax-infvn 7302. (Contributed by BJ, 14-Nov-2019.) (Proof modification is discouraged.)
|- om e. _V
14-Nov-2019	ax-infvn 7302	Axiom of infinity in a constructive setting. This asserts the existence of the special set we want (the set of natural numbers), instead of the existence of a set with some properties (ax-iinf 4234) from which one then proves (omex 4239) using full separation that the wanted set exists. "vn" is for "Von Neumann". (Contributed by BJ, 14-Nov-2019.)
|- E.x(Ind x /\ A.y(Ind y -> x C_ y))
14-Nov-2019	enq0tr 6283	The equivalence relation for non-negative fractions is transitive. Lemma for enq0er 6284. (Contributed by Jim Kingdon, 14-Nov-2019.)
|- ((f ~Q0 g /\ g ~Q0 h) -> f ~Q0 h)
14-Nov-2019	enq0ref 6282	The equivalence relation for non-negative fractions is reflexive. Lemma for enq0er 6284. (Contributed by Jim Kingdon, 14-Nov-2019.)
|- (f e. ( om X. N.) <-> f ~Q0 f)
14-Nov-2019	enq0sym 6281	The equivalence relation for non-negative fractions is symmetric. Lemma for enq0er 6284. (Contributed by Jim Kingdon, 14-Nov-2019.)
|- (f ~Q0 g -> g ~Q0 f)
13-Nov-2019	bj-sucex 7285	sucex 4171 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- A e. _V   =>   |- suc A e. _V
13-Nov-2019	bj-sucexg 7284	sucexg 4170 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- (A e. V -> suc A e. _V)
13-Nov-2019	bj-unexg 7283	unexg 4124 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- ((A e. V /\ B e. W) -> (A u. B) e. _V)
13-Nov-2019	bdunexb 7282	Bounded version of unexb 4123. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- BOUNDED A   &   |- BOUNDED B   =>   |- ((A e. _V /\ B e. _V) <-> (A u. B) e. _V)
13-Nov-2019	bj-unex 7281	unex 4122 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- A e. _V   &   |- B e. _V   =>   |- (A u. B) e. _V
13-Nov-2019	bj-uniexg 7280	uniexg 4121 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- (A e. V -> U.A e. _V)
13-Nov-2019	bj-uniex 7279	uniex 4120 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- A e. _V   =>   |- U.A e. _V
13-Nov-2019	bdssexd 7267	Bounded version of ssexd 3867. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- (ph -> B e. C)   &   |- (ph -> A C_ B)   &   |- BOUNDED A   =>   |- (ph -> A e. _V)
13-Nov-2019	bdssexg 7266	Bounded version of ssexg 3866. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- BOUNDED A   =>   |- ((A C_ B /\ B e. C) -> A e. _V)
13-Nov-2019	bdssexi 7265	Bounded version of ssexi 3865. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- BOUNDED A   &   |- B e. _V   &   |- A C_ B   =>   |- A e. _V
13-Nov-2019	bdssex 7264	Bounded version of ssex 3864. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- BOUNDED A   &   |- B e. _V   =>   |- (A C_ B -> A e. _V)
13-Nov-2019	bdinex1g 7263	Bounded version of inex1g 3863. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- BOUNDED B   =>   |- (A e. V -> (A i^i B) e. _V)
13-Nov-2019	bdinex2 7262	Bounded version of inex2 3862. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- BOUNDED B   &   |- A e. _V   =>   |- (B i^i A) e. _V
13-Nov-2019	bdinex1 7261	Bounded version of inex1 3861. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- BOUNDED B   &   |- A e. _V   =>   |- (A i^i B) e. _V
13-Nov-2019	bdzfauscl 7255	Closed form of the version of zfauscl 3847 for bounded formulas using bounded separation. (Contributed by BJ, 13-Nov-2019.)
|- BOUNDED ph   =>   |- (A e. V -> E.yA.x(x e. y <-> (x e. A /\ ph)))
12-Nov-2019	enq0er 6284	The equivalence relation for non-negative fractions is an equivalence relation. (Contributed by Jim Kingdon, 12-Nov-2019.)
|- ~Q0 Er ( om X. N.)
12-Nov-2019	enq0enq 6280	Equivalence on positive fractions in terms of equivalence on non-negative fractions. (Contributed by Jim Kingdon, 12-Nov-2019.)
|- ~Q = ( ~Q0 i^i (( N. X. N.) X. ( N. X. N.)))
10-Nov-2019	prarloclemup 6343	Contracting the upper side of an interval which straddles a Dedekind cut. Lemma for prarloc 6351. (Contributed by Jim Kingdon, 10-Nov-2019.)
|- ((( X e. om /\ ( <. L , U >. e. P. /\ A e. L /\ P e. Q.)) /\ y e. om) -> ((A +Q ([ <.((y +o 2o) +o X) , 1o >.] ~Q .Q P)) e. U -> (((A +Q0 ([ <.y , 1o >.] ~Q0 ·Q0 P)) e. L /\ (A +Q ([ <.((y +o 2o) +o suc X) , 1o >.] ~Q .Q P)) e. U) -> E.y e. om ((A +Q0 ([ <.y , 1o >.] ~Q0 ·Q0 P)) e. L /\ (A +Q ([ <.((y +o 2o) +o X) , 1o >.] ~Q .Q P)) e. U))))
10-Nov-2019	prarloclemlo 6342	Contracting the lower side of an interval which straddles a Dedekind cut. Lemma for prarloc 6351. (Contributed by Jim Kingdon, 10-Nov-2019.)
|- ((( X e. om /\ ( <. L , U >. e. P. /\ A e. L /\ P e. Q.)) /\ y e. om) -> ((A +Q ([ <.(y +o 1o) , 1o >.] ~Q .Q P)) e. L -> (((A +Q0 ([ <.y , 1o >.] ~Q0 ·Q0 P)) e. L /\ (A +Q ([ <.((y +o 2o) +o suc X) , 1o >.] ~Q .Q P)) e. U) -> E.y e. om ((A +Q0 ([ <.y , 1o >.] ~Q0 ·Q0 P)) e. L /\ (A +Q ([ <.((y +o 2o) +o X) , 1o >.] ~Q .Q P)) e. U))))
10-Nov-2019	prarloclemlt 6341	Two possible ways of contracting an interval which straddles a Dedekind cut. Lemma for prarloc 6351. (Contributed by Jim Kingdon, 10-Nov-2019.)
|- ((( X e. om /\ ( <. L , U >. e. P. /\ A e. L /\ P e. Q.)) /\ y e. om) -> (A +Q ([ <.(y +o 1o) , 1o >.] ~Q .Q P)) <Q (A +Q ([ <.((y +o 2o) +o X) , 1o >.] ~Q .Q P)))
10-Nov-2019	nqnq0m 6304	Multiplication of positive fractions is equal with .Q or ·Q0. (Contributed by Jim Kingdon, 10-Nov-2019.)
|- ((A e. Q. /\ B e. Q.) -> (A .Q B) = (A ·Q0 B))
10-Nov-2019	nqnq0a 6303	Addition of positive fractions is equal with +Q or +Q0. (Contributed by Jim Kingdon, 10-Nov-2019.)
|- ((A e. Q. /\ B e. Q.) -> (A +Q B) = (A +Q0 B))
10-Nov-2019	nqnq0pi 6287	A non-negative fraction is a positive fraction if its numerator and denominator are positive integers. (Contributed by Jim Kingdon, 10-Nov-2019.)
|- ((A e. N. /\ B e. N.) -> [ <.A , B >.] ~Q0 = [ <.A , B >.] ~Q )
10-Nov-2019	nnppipi 6196	A natural number plus a positive integer is a positive integer. (Contributed by Jim Kingdon, 10-Nov-2019.)
|- ((A e. om /\ B e. N.) -> (A +o B) e. N.)
9-Nov-2019	prarloclem3step 6344	Induction step for prarloclem3 6345. (Contributed by Jim Kingdon, 9-Nov-2019.)
|- ((( X e. om /\ ( <. L , U >. e. P. /\ A e. L /\ P e. Q.)) /\ E.y e. om ((A +Q0 ([ <.y , 1o >.] ~Q0 ·Q0 P)) e. L /\ (A +Q ([ <.((y +o 2o) +o suc X) , 1o >.] ~Q .Q P)) e. U)) -> E.y e. om ((A +Q0 ([ <.y , 1o >.] ~Q0 ·Q0 P)) e. L /\ (A +Q ([ <.((y +o 2o) +o X) , 1o >.] ~Q .Q P)) e. U))
8-Nov-2019	genpcuu 6369	Upward closure of an operation on positive reals. (Contributed by Jim Kingdon, 8-Nov-2019.)
|- F = (w e. P. , v e. P. |-> <. {x e. Q. | E.y e. Q. E.z e. Q. (y e. ( 1st ` w) /\ z e. ( 1st ` v) /\ x = (y Gz)) } , {x e. Q. | E.y e. Q. E.z e. Q. (y e. ( 2nd ` w) /\ z e. ( 2nd ` v) /\ x = (y Gz)) } >.)   &   |- ((y e. Q. /\ z e. Q.) -> (y Gz) e. Q.)   &   |- ((((A e. P. /\ g e. ( 2nd ` A)) /\ (B e. P. /\ h e. ( 2nd ` B))) /\ x e. Q.) -> ((g G h) <Q x -> x e. ( 2nd ` (A FB))))   =>   |- ((A e. P. /\ B e. P.) -> (f e. ( 2nd ` (A FB)) -> (f <Q x -> x e. ( 2nd ` (A FB)))))
7-Nov-2019	genppreclu 6363	Pre-closure law for general operation on upper cuts. (Contributed by Jim Kingdon, 7-Nov-2019.)
|- F = (w e. P. , v e. P. |-> <. {x e. Q. | E.y e. Q. E.z e. Q. (y e. ( 1st ` w) /\ z e. ( 1st ` v) /\ x = (y Gz)) } , {x e. Q. | E.y e. Q. E.z e. Q. (y e. ( 2nd ` w) /\ z e. ( 2nd ` v) /\ x = (y Gz)) } >.)   &   |- ((y e. Q. /\ z e. Q.) -> (y Gz) e. Q.)   =>   |- ((A e. P. /\ B e. P.) -> (( C e. ( 2nd ` A) /\ D e. ( 2nd ` B)) -> ( C G D) e. ( 2nd ` (A FB))))
7-Nov-2019	prnminu 6337	An upper cut has no smallest member. (Contributed by Jim Kingdon, 7-Nov-2019.)
|- (( <. L , U >. e. P. /\ B e. U) -> E.x e. U x <Q B)
5-Nov-2019	prarloclemn 6347	Subtracting two from a positive integer. Lemma for prarloc 6351. (Contributed by Jim Kingdon, 5-Nov-2019.)
|- (( N e. N. /\ 1o <N N) -> E.x e. om ( 2o +o x) = N)
5-Nov-2019	nq0a0 6306	Addition with zero for non-negative fractions. (Contributed by Jim Kingdon, 5-Nov-2019.)
|- (A e. Q0 -> (A +Q0 0Q0) = A)
5-Nov-2019	nq0m0r 6305	Multiplication with zero for non-negative fractions. (Contributed by Jim Kingdon, 5-Nov-2019.)
|- (A e. Q0 -> (0Q0 ·Q0 A) = 0Q0)
5-Nov-2019	df-0nq0 6275	Define non-negative fraction constant 0. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. (Contributed by Jim Kingdon, 5-Nov-2019.)
|- 0Q0 = [ <. (/) , 1o >.] ~Q0
4-Nov-2019	prarloclem5 6348	A substitution of zero for y and N minus two for x. Lemma for prarloc 6351. (Contributed by Jim Kingdon, 4-Nov-2019.)
|- ((( <. L , U >. e. P. /\ A e. L) /\ ( N e. N. /\ P e. Q. /\ 1o <N N) /\ (A +Q ([ <. N , 1o >.] ~Q .Q P)) e. U) -> E.x e. om E.y e. om ((A +Q0 ([ <.y , 1o >.] ~Q0 ·Q0 P)) e. L /\ (A +Q ([ <.((y +o 2o) +o x) , 1o >.] ~Q .Q P)) e. U))
4-Nov-2019	prarloclem4 6346	A slight rearrangement of prarloclem3 6345. Lemma for prarloc 6351. (Contributed by Jim Kingdon, 4-Nov-2019.)
|- ((( <. L , U >. e. P. /\ A e. L) /\ P e. Q.) -> (E.x e. om E.y e. om ((A +Q0 ([ <.y , 1o >.] ~Q0 ·Q0 P)) e. L /\ (A +Q ([ <.((y +o 2o) +o x) , 1o >.] ~Q .Q P)) e. U) -> E. j e. om ((A +Q0 ([ <. j , 1o >.] ~Q0 ·Q0 P)) e. L /\ (A +Q ([ <.( j +o 2o) , 1o >.] ~Q .Q P