Theorem prarloclemarch2 6402

Description: Like prarloclemarch 6401 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 6486. (Contributed by Jim Kingdon, 25-Nov-2019.)

Assertion

Ref	Expression
prarloclemarch2	|- ((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))))

Distinct variable groups:   x,A   x,B   x, C

Proof of Theorem prarloclemarch2

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		prarloclemarch 6401	. . 3 |- ((A e. Q. /\ C e. Q.) -> E.z e. N. A <Q ([ <.z , 1o >.] ~Q .Q C))
2	1	3adant2 922	. 2 |- ((A e. Q. /\ B e. Q. /\ C e. Q.) -> E.z e. N. A <Q ([ <.z , 1o >.] ~Q .Q C))
3		pinn 6293	. . . . . . . 8 |- (z e. N. -> z e. om)
4		1pi 6299	. . . . . . . . . . . 12 |- 1o e. N.
5	4	elexi 2561	. . . . . . . . . . 11 |- 1o e. _V
6	5	sucid 4120	. . . . . . . . . 10 |- 1o e. suc 1o
7		df-2o 5941	. . . . . . . . . 10 |- 2o = suc 1o
8	6, 7	eleqtrri 2110	. . . . . . . . 9 |- 1o e. 2o
9		2onn 6030	. . . . . . . . . . 11 |- 2o e. om
10		nnaword2 6023	. . . . . . . . . . 11 |- (( 2o e. om /\ z e. om) -> 2o C_ (z +o 2o))
11	9, 10	mpan 400	. . . . . . . . . 10 |- (z e. om -> 2o C_ (z +o 2o))
12	11	sseld 2938	. . . . . . . . 9 |- (z e. om -> ( 1o e. 2o -> 1o e. (z +o 2o)))
13	8, 12	mpi 15	. . . . . . . 8 |- (z e. om -> 1o e. (z +o 2o))
14	3, 13	syl 14	. . . . . . 7 |- (z e. N. -> 1o e. (z +o 2o))
15		o1p1e2 5987	. . . . . . . . 9 |- ( 1o +o 1o) = 2o
16		addpiord 6300	. . . . . . . . . . 11 |- (( 1o e. N. /\ 1o e. N.) -> ( 1o +N 1o) = ( 1o +o 1o))
17	4, 4, 16	mp2an 402	. . . . . . . . . 10 |- ( 1o +N 1o) = ( 1o +o 1o)
18		addclpi 6311	. . . . . . . . . . 11 |- (( 1o e. N. /\ 1o e. N.) -> ( 1o +N 1o) e. N.)
19	4, 4, 18	mp2an 402	. . . . . . . . . 10 |- ( 1o +N 1o) e. N.
20	17, 19	eqeltrri 2108	. . . . . . . . 9 |- ( 1o +o 1o) e. N.
21	15, 20	eqeltrri 2108	. . . . . . . 8 |- 2o e. N.
22		addpiord 6300	. . . . . . . 8 |- ((z e. N. /\ 2o e. N.) -> (z +N 2o) = (z +o 2o))
23	21, 22	mpan2 401	. . . . . . 7 |- (z e. N. -> (z +N 2o) = (z +o 2o))
24	14, 23	eleqtrrd 2114	. . . . . 6 |- (z e. N. -> 1o e. (z +N 2o))
25		addclpi 6311	. . . . . . . 8 |- ((z e. N. /\ 2o e. N.) -> (z +N 2o) e. N.)
26	21, 25	mpan2 401	. . . . . . 7 |- (z e. N. -> (z +N 2o) e. N.)
27		ltpiord 6303	. . . . . . . 8 |- (( 1o e. N. /\ (z +N 2o) e. N.) -> ( 1o <N (z +N 2o) <-> 1o e. (z +N 2o)))
28	4, 27	mpan 400	. . . . . . 7 |- ((z +N 2o) e. N. -> ( 1o <N (z +N 2o) <-> 1o e. (z +N 2o)))
29	26, 28	syl 14	. . . . . 6 |- (z e. N. -> ( 1o <N (z +N 2o) <-> 1o e. (z +N 2o)))
30	24, 29	mpbird 156	. . . . 5 |- (z e. N. -> 1o <N (z +N 2o))
31	30	adantl 262	. . . 4 |- (((A e. Q. /\ B e. Q. /\ C e. Q.) /\ z e. N.) -> 1o <N (z +N 2o))
32	31	adantrr 448	. . 3 |- (((A e. Q. /\ B e. Q. /\ C e. Q.) /\ (z e. N. /\ A <Q ([ <.z , 1o >.] ~Q .Q C))) -> 1o <N (z +N 2o))
33		nna0 5992	. . . . . . . . . . . . . . . . 17 |- (z e. om -> (z +o (/)) = z)
34		0lt1o 5962	. . . . . . . . . . . . . . . . . . . 20 |- (/) e. 1o
35		1on 5947	. . . . . . . . . . . . . . . . . . . . . 22 |- 1o e. On
36	35	onsuci 4207	. . . . . . . . . . . . . . . . . . . . 21 |- suc 1o e. On
37		ontr1 4092	. . . . . . . . . . . . . . . . . . . . 21 |- ( suc 1o e. On -> (( (/) e. 1o /\ 1o e. suc 1o) -> (/) e. suc 1o))
38	36, 37	ax-mp 7	. . . . . . . . . . . . . . . . . . . 20 |- (( (/) e. 1o /\ 1o e. suc 1o) -> (/) e. suc 1o)
39	34, 6, 38	mp2an 402	. . . . . . . . . . . . . . . . . . 19 |- (/) e. suc 1o
40	39, 7	eleqtrri 2110	. . . . . . . . . . . . . . . . . 18 |- (/) e. 2o
41		nnaordi 6017	. . . . . . . . . . . . . . . . . . 19 |- (( 2o e. om /\ z e. om) -> ( (/) e. 2o -> (z +o (/)) e. (z +o 2o)))
42	9, 41	mpan 400	. . . . . . . . . . . . . . . . . 18 |- (z e. om -> ( (/) e. 2o -> (z +o (/)) e. (z +o 2o)))
43	40, 42	mpi 15	. . . . . . . . . . . . . . . . 17 |- (z e. om -> (z +o (/)) e. (z +o 2o))
44	33, 43	eqeltrrd 2112	. . . . . . . . . . . . . . . 16 |- (z e. om -> z e. (z +o 2o))
45	3, 44	syl 14	. . . . . . . . . . . . . . 15 |- (z e. N. -> z e. (z +o 2o))
46	45, 23	eleqtrrd 2114	. . . . . . . . . . . . . 14 |- (z e. N. -> z e. (z +N 2o))
47		ltpiord 6303	. . . . . . . . . . . . . . 15 |- ((z e. N. /\ (z +N 2o) e. N.) -> (z <N (z +N 2o) <-> z e. (z +N 2o)))
48	26, 47	mpdan 398	. . . . . . . . . . . . . 14 |- (z e. N. -> (z <N (z +N 2o) <-> z e. (z +N 2o)))
49	46, 48	mpbird 156	. . . . . . . . . . . . 13 |- (z e. N. -> z <N (z +N 2o))
50		mulidpi 6302	. . . . . . . . . . . . 13 |- (z e. N. -> (z .N 1o) = z)
51		mulcompig 6315	. . . . . . . . . . . . . . . 16 |- (((z +N 2o) e. N. /\ 1o e. N.) -> ((z +N 2o) .N 1o) = ( 1o .N (z +N 2o)))
52	4, 51	mpan2 401	. . . . . . . . . . . . . . 15 |- ((z +N 2o) e. N. -> ((z +N 2o) .N 1o) = ( 1o .N (z +N 2o)))
53	26, 52	syl 14	. . . . . . . . . . . . . 14 |- (z e. N. -> ((z +N 2o) .N 1o) = ( 1o .N (z +N 2o)))
54		mulidpi 6302	. . . . . . . . . . . . . . 15 |- ((z +N 2o) e. N. -> ((z +N 2o) .N 1o) = (z +N 2o))
55	26, 54	syl 14	. . . . . . . . . . . . . 14 |- (z e. N. -> ((z +N 2o) .N 1o) = (z +N 2o))
56	53, 55	eqtr3d 2071	. . . . . . . . . . . . 13 |- (z e. N. -> ( 1o .N (z +N 2o)) = (z +N 2o))
57	49, 50, 56	3brtr4d 3785	. . . . . . . . . . . 12 |- (z e. N. -> (z .N 1o) <N ( 1o .N (z +N 2o)))
58		ordpipqqs 6358	. . . . . . . . . . . . . . 15 |- (((z e. N. /\ 1o e. N.) /\ ((z +N 2o) e. N. /\ 1o e. N.)) -> ([ <.z , 1o >.] ~Q <Q [ <.(z +N 2o) , 1o >.] ~Q <-> (z .N 1o) <N ( 1o .N (z +N 2o))))
59	4, 58	mpanl2 411	. . . . . . . . . . . . . 14 |- ((z e. N. /\ ((z +N 2o) e. N. /\ 1o e. N.)) -> ([ <.z , 1o >.] ~Q <Q [ <.(z +N 2o) , 1o >.] ~Q <-> (z .N 1o) <N ( 1o .N (z +N 2o))))
60	4, 59	mpanr2 414	. . . . . . . . . . . . 13 |- ((z e. N. /\ (z +N 2o) e. N.) -> ([ <.z , 1o >.] ~Q <Q [ <.(z +N 2o) , 1o >.] ~Q <-> (z .N 1o) <N ( 1o .N (z +N 2o))))
61	26, 60	mpdan 398	. . . . . . . . . . . 12 |- (z e. N. -> ([ <.z , 1o >.] ~Q <Q [ <.(z +N 2o) , 1o >.] ~Q <-> (z .N 1o) <N ( 1o .N (z +N 2o))))
62	57, 61	mpbird 156	. . . . . . . . . . 11 |- (z e. N. -> [ <.z , 1o >.] ~Q <Q [ <.(z +N 2o) , 1o >.] ~Q )
63	62	adantl 262	. . . . . . . . . 10 |- (( C e. Q. /\ z e. N.) -> [ <.z , 1o >.] ~Q <Q [ <.(z +N 2o) , 1o >.] ~Q )
64		opelxpi 4319	. . . . . . . . . . . . . . . 16 |- (((z +N 2o) e. N. /\ 1o e. N.) -> <.(z +N 2o) , 1o >. e. ( N. X. N.))
65	4, 64	mpan2 401	. . . . . . . . . . . . . . 15 |- ((z +N 2o) e. N. -> <.(z +N 2o) , 1o >. e. ( N. X. N.))
66		enqex 6344	. . . . . . . . . . . . . . . 16 |- ~Q e. _V
67	66	ecelqsi 6096	. . . . . . . . . . . . . . 15 |- ( <.(z +N 2o) , 1o >. e. ( N. X. N.) -> [ <.(z +N 2o) , 1o >.] ~Q e. (( N. X. N.) /. ~Q ))
68	26, 65, 67	3syl 17	. . . . . . . . . . . . . 14 |- (z e. N. -> [ <.(z +N 2o) , 1o >.] ~Q e. (( N. X. N.) /. ~Q ))
69		df-nqqs 6332	. . . . . . . . . . . . . 14 |- Q. = (( N. X. N.) /. ~Q )
70	68, 69	syl6eleqr 2128	. . . . . . . . . . . . 13 |- (z e. N. -> [ <.(z +N 2o) , 1o >.] ~Q e. Q.)
71		opelxpi 4319	. . . . . . . . . . . . . . . . 17 |- ((z e. N. /\ 1o e. N.) -> <.z , 1o >. e. ( N. X. N.))
72	4, 71	mpan2 401	. . . . . . . . . . . . . . . 16 |- (z e. N. -> <.z , 1o >. e. ( N. X. N.))
73	66	ecelqsi 6096	. . . . . . . . . . . . . . . 16 |- ( <.z , 1o >. e. ( N. X. N.) -> [ <.z , 1o >.] ~Q e. (( N. X. N.) /. ~Q ))
74	72, 73	syl 14	. . . . . . . . . . . . . . 15 |- (z e. N. -> [ <.z , 1o >.] ~Q e. (( N. X. N.) /. ~Q ))
75	74, 69	syl6eleqr 2128	. . . . . . . . . . . . . 14 |- (z e. N. -> [ <.z , 1o >.] ~Q e. Q.)
76		ltmnqg 6385	. . . . . . . . . . . . . 14 |- (([ <.z , 1o >.] ~Q e. Q. /\ [ <.(z +N 2o) , 1o >.] ~Q e. Q. /\ C e. Q.) -> ([ <.z , 1o >.] ~Q <Q [ <.(z +N 2o) , 1o >.] ~Q <-> ( C .Q [ <.z , 1o >.] ~Q ) <Q ( C .Q [ <.(z +N 2o) , 1o >.] ~Q )))
77	75, 76	syl3an1 1167	. . . . . . . . . . . . 13 |- ((z e. N. /\ [ <.(z +N 2o) , 1o >.] ~Q e. Q. /\ C e. Q.) -> ([ <.z , 1o >.] ~Q <Q [ <.(z +N 2o) , 1o >.] ~Q <-> ( C .Q [ <.z , 1o >.] ~Q ) <Q ( C .Q [ <.(z +N 2o) , 1o >.] ~Q )))
78	70, 77	syl3an2 1168	. . . . . . . . . . . 12 |- ((z e. N. /\ z e. N. /\ C e. Q.) -> ([ <.z , 1o >.] ~Q <Q [ <.(z +N 2o) , 1o >.] ~Q <-> ( C .Q [ <.z , 1o >.] ~Q ) <Q ( C .Q [ <.(z +N 2o) , 1o >.] ~Q )))
79	78	3anidm12 1191	. . . . . . . . . . 11 |- ((z e. N. /\ C e. Q.) -> ([ <.z , 1o >.] ~Q <Q [ <.(z +N 2o) , 1o >.] ~Q <-> ( C .Q [ <.z , 1o >.] ~Q ) <Q ( C .Q [ <.(z +N 2o) , 1o >.] ~Q )))
80	79	ancoms 255	. . . . . . . . . 10 |- (( C e. Q. /\ z e. N.) -> ([ <.z , 1o >.] ~Q <Q [ <.(z +N 2o) , 1o >.] ~Q <-> ( C .Q [ <.z , 1o >.] ~Q ) <Q ( C .Q [ <.(z +N 2o) , 1o >.] ~Q )))
81	63, 80	mpbid 135	. . . . . . . . 9 |- (( C e. Q. /\ z e. N.) -> ( C .Q [ <.z , 1o >.] ~Q ) <Q ( C .Q [ <.(z +N 2o) , 1o >.] ~Q ))
82		mulcomnqg 6367	. . . . . . . . . 10 |- (( C e. Q. /\ [ <.z , 1o >.] ~Q e. Q.) -> ( C .Q [ <.z , 1o >.] ~Q ) = ([ <.z , 1o >.] ~Q .Q C))
83	75, 82	sylan2 270	. . . . . . . . 9 |- (( C e. Q. /\ z e. N.) -> ( C .Q [ <.z , 1o >.] ~Q ) = ([ <.z , 1o >.] ~Q .Q C))
84		mulcomnqg 6367	. . . . . . . . . 10 |- (( C e. Q. /\ [ <.(z +N 2o) , 1o >.] ~Q e. Q.) -> ( C .Q [ <.(z +N 2o) , 1o >.] ~Q ) = ([ <.(z +N 2o) , 1o >.] ~Q .Q C))
85	70, 84	sylan2 270	. . . . . . . . 9 |- (( C e. Q. /\ z e. N.) -> ( C .Q [ <.(z +N 2o) , 1o >.] ~Q ) = ([ <.(z +N 2o) , 1o >.] ~Q .Q C))
86	81, 83, 85	3brtr3d 3784	. . . . . . . 8 |- (( C e. Q. /\ z e. N.) -> ([ <.z , 1o >.] ~Q .Q C) <Q ([ <.(z +N 2o) , 1o >.] ~Q .Q C))
87	86	3ad2antl3 1067	. . . . . . 7 |- (((A e. Q. /\ B e. Q. /\ C e. Q.) /\ z e. N.) -> ([ <.z , 1o >.] ~Q .Q C) <Q ([ <.(z +N 2o) , 1o >.] ~Q .Q C))
88	87	adantrr 448	. . . . . 6 |- (((A e. Q. /\ B e. Q. /\ C e. Q.) /\ (z e. N. /\ A <Q ([ <.z , 1o >.] ~Q .Q C))) -> ([ <.z , 1o >.] ~Q .Q C) <Q ([ <.(z +N 2o) , 1o >.] ~Q .Q C))
89		ltsonq 6382	. . . . . . . . . 10 |- <Q Or Q.
90		ltrelnq 6349	. . . . . . . . . 10 |- <Q C_ ( Q. X. Q.)
91	89, 90	sotri 4663	. . . . . . . . 9 |- ((A <Q ([ <.z , 1o >.] ~Q .Q C) /\ ([ <.z , 1o >.] ~Q .Q C) <Q ([ <.(z +N 2o) , 1o >.] ~Q .Q C)) -> A <Q ([ <.(z +N 2o) , 1o >.] ~Q .Q C))
92	91	ex 108	. . . . . . . 8 |- (A <Q ([ <.z , 1o >.] ~Q .Q C) -> (([ <.z , 1o >.] ~Q .Q C) <Q ([ <.(z +N 2o) , 1o >.] ~Q .Q C) -> A <Q ([ <.(z +N 2o) , 1o >.] ~Q .Q C)))
93	92	adantl 262	. . . . . . 7 |- ((z e. N. /\ A <Q ([ <.z , 1o >.] ~Q .Q C)) -> (([ <.z , 1o >.] ~Q .Q C) <Q ([ <.(z +N 2o) , 1o >.] ~Q .Q C) -> A <Q ([ <.(z +N 2o) , 1o >.] ~Q .Q C)))
94	93	adantl 262	. . . . . 6 |- (((A e. Q. /\ B e. Q. /\ C e. Q.) /\ (z e. N. /\ A <Q ([ <.z , 1o >.] ~Q .Q C))) -> (([ <.z , 1o >.] ~Q .Q C) <Q ([ <.(z +N 2o) , 1o >.] ~Q .Q C) -> A <Q ([ <.(z +N 2o) , 1o >.] ~Q .Q C)))
95	88, 94	mpd 13	. . . . 5 |- (((A e. Q. /\ B e. Q. /\ C e. Q.) /\ (z e. N. /\ A <Q ([ <.z , 1o >.] ~Q .Q C))) -> A <Q ([ <.(z +N 2o) , 1o >.] ~Q .Q C))
96		mulclnq 6360	. . . . . . . . . 10 |- (([ <.(z +N 2o) , 1o >.] ~Q e. Q. /\ C e. Q.) -> ([ <.(z +N 2o) , 1o >.] ~Q .Q C) e. Q.)
97	70, 96	sylan 267	. . . . . . . . 9 |- ((z e. N. /\ C e. Q.) -> ([ <.(z +N 2o) , 1o >.] ~Q .Q C) e. Q.)
98	97	ancoms 255	. . . . . . . 8 |- (( C e. Q. /\ z e. N.) -> ([ <.(z +N 2o) , 1o >.] ~Q .Q C) e. Q.)
99	98	3ad2antl3 1067	. . . . . . 7 |- (((A e. Q. /\ B e. Q. /\ C e. Q.) /\ z e. N.) -> ([ <.(z +N 2o) , 1o >.] ~Q .Q C) e. Q.)
100		simpl2 907	. . . . . . 7 |- (((A e. Q. /\ B e. Q. /\ C e. Q.) /\ z e. N.) -> B e. Q.)
101		ltaddnq 6390	. . . . . . 7 |- ((([ <.(z +N 2o) , 1o >.] ~Q .Q C) e. Q. /\ B e. Q.) -> ([ <.(z +N 2o) , 1o >.] ~Q .Q C) <Q (([ <.(z +N 2o) , 1o >.] ~Q .Q C) +Q B))
102	99, 100, 101	syl2anc 391	. . . . . 6 |- (((A e. Q. /\ B e. Q. /\ C e. Q.) /\ z e. N.) -> ([ <.(z +N 2o) , 1o >.] ~Q .Q C) <Q (([ <.(z +N 2o) , 1o >.] ~Q .Q C) +Q B))
103	102	adantrr 448	. . . . 5 |- (((A e. Q. /\ B e. Q. /\ C e. Q.) /\ (z e. N. /\ A <Q ([ <.z , 1o >.] ~Q .Q C))) -> ([ <.(z +N 2o) , 1o >.] ~Q .Q C) <Q (([ <.(z +N 2o) , 1o >.] ~Q .Q C) +Q B))
104	89, 90	sotri 4663	. . . . 5 |- ((A <Q ([ <.(z +N 2o) , 1o >.] ~Q .Q C) /\ ([ <.(z +N 2o) , 1o >.] ~Q .Q C) <Q (([ <.(z +N 2o) , 1o >.] ~Q .Q C) +Q B)) -> A <Q (([ <.(z +N 2o) , 1o >.] ~Q .Q C) +Q B))
105	95, 103, 104	syl2anc 391	. . . 4 |- (((A e. Q. /\ B e. Q. /\ C e. Q.) /\ (z e. N. /\ A <Q ([ <.z , 1o >.] ~Q .Q C))) -> A <Q (([ <.(z +N 2o) , 1o >.] ~Q .Q C) +Q B))
106		addcomnqg 6365	. . . . . . 7 |- ((([ <.(z +N 2o) , 1o >.] ~Q .Q C) e. Q. /\ B e. Q.) -> (([ <.(z +N 2o) , 1o >.] ~Q .Q C) +Q B) = (B +Q ([ <.(z +N 2o) , 1o >.] ~Q .Q C)))
107	99, 100, 106	syl2anc 391	. . . . . 6 |- (((A e. Q. /\ B e. Q. /\ C e. Q.) /\ z e. N.) -> (([ <.(z +N 2o) , 1o >.] ~Q .Q C) +Q B) = (B +Q ([ <.(z +N 2o) , 1o >.] ~Q .Q C)))
108	107	breq2d 3767	. . . . 5 |- (((A e. Q. /\ B e. Q. /\ C e. Q.) /\ z e. N.) -> (A <Q (([ <.(z +N 2o) , 1o >.] ~Q .Q C) +Q B) <-> A <Q (B +Q ([ <.(z +N 2o) , 1o >.] ~Q .Q C))))
109	108	adantrr 448	. . . 4 |- (((A e. Q. /\ B e. Q. /\ C e. Q.) /\ (z e. N. /\ A <Q ([ <.z , 1o >.] ~Q .Q C))) -> (A <Q (([ <.(z +N 2o) , 1o >.] ~Q .Q C) +Q B) <-> A <Q (B +Q ([ <.(z +N 2o) , 1o >.] ~Q .Q C))))
110	105, 109	mpbid 135	. . 3 |- (((A e. Q. /\ B e. Q. /\ C e. Q.) /\ (z e. N. /\ A <Q ([ <.z , 1o >.] ~Q .Q C))) -> A <Q (B +Q ([ <.(z +N 2o) , 1o >.] ~Q .Q C)))
111		simpr 103	. . . . 5 |- (((A e. Q. /\ B e. Q. /\ C e. Q.) /\ z e. N.) -> z e. N.)
112		breq2 3759	. . . . . . . 8 |- (x = (z +N 2o) -> ( 1o <N x <-> 1o <N (z +N 2o)))
113		opeq1 3540	. . . . . . . . . . . 12 |- (x = (z +N 2o) -> <.x , 1o >. = <.(z +N 2o) , 1o >.)
114	113	eceq1d 6078	. . . . . . . . . . 11 |- (x = (z +N 2o) -> [ <.x , 1o >.] ~Q = [ <.(z +N 2o) , 1o >.] ~Q )
115	114	oveq1d 5470	. . . . . . . . . 10 |- (x = (z +N 2o) -> ([ <.x , 1o >.] ~Q .Q C) = ([ <.(z +N 2o) , 1o >.] ~Q .Q C))
116	115	oveq2d 5471	. . . . . . . . 9 |- (x = (z +N 2o) -> (B +Q ([ <.x , 1o >.] ~Q .Q C)) = (B +Q ([ <.(z +N 2o) , 1o >.] ~Q .Q C)))
117	116	breq2d 3767	. . . . . . . 8 |- (x = (z +N 2o) -> (A <Q (B +Q ([ <.x , 1o >.] ~Q .Q C)) <-> A <Q (B +Q ([ <.(z +N 2o) , 1o >.] ~Q .Q C))))
118	112, 117	anbi12d 442	. . . . . . 7 |- (x = (z +N 2o) -> (( 1o <N x /\ A <Q (B +Q ([ <.x , 1o >.] ~Q .Q C))) <-> ( 1o <N (z +N 2o) /\ A <Q (B +Q ([ <.(z +N 2o) , 1o >.] ~Q .Q C)))))
119	118	rspcev 2650	. . . . . 6 |- (((z +N 2o) e. N. /\ ( 1o <N (z +N 2o) /\ A <Q (B +Q ([ <.(z +N 2o) , 1o >.] ~Q .Q C)))) -> E.x e. N. ( 1o <N x /\ A <Q (B +Q ([ <.x , 1o >.] ~Q .Q C))))
120	119	ex 108	. . . . 5 |- ((z +N 2o) e. N. -> (( 1o <N (z +N 2o) /\ A <Q (B +Q ([ <.(z +N 2o) , 1o >.] ~Q .Q C))) -> E.x e. N. ( 1o <N x /\ A <Q (B +Q ([ <.x , 1o >.] ~Q .Q C)))))
121	111, 26, 120	3syl 17	. . . 4 |- (((A e. Q. /\ B e. Q. /\ C e. Q.) /\ z e. N.) -> (( 1o <N (z +N 2o) /\ A <Q (B +Q ([ <.(z +N 2o) , 1o >.] ~Q .Q C))) -> E.x e. N. ( 1o <N x /\ A <Q (B +Q ([ <.x , 1o >.] ~Q .Q C)))))
122	121	adantrr 448	. . 3 |- (((A e. Q. /\ B e. Q. /\ C e. Q.) /\ (z e. N. /\ A <Q ([ <.z , 1o >.] ~Q .Q C))) -> (( 1o <N (z +N 2o) /\ A <Q (B +Q ([ <.(z +N 2o) , 1o >.] ~Q .Q C))) -> E.x e. N. ( 1o <N x /\ A <Q (B +Q ([ <.x , 1o >.] ~Q .Q C)))))
123	32, 110, 122	mp2and 409	. 2 |- (((A e. Q. /\ B e. Q. /\ C e. Q.) /\ (z e. N. /\ A <Q ([ <.z , 1o >.] ~Q .Q C))) -> E.x e. N. ( 1o <N x /\ A <Q (B +Q ([ <.x , 1o >.] ~Q .Q C))))
124	2, 123	rexlimddv 2431	1 |- ((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))))

Syntax hints:   -> wi 4   /\ wa 97   <-> wb 98   /\ w3a 884   = wceq 1242   e. wcel 1390  E.wrex 2301   C_ wss 2911   (/)c0 3218   <.cop 3370   class class class wbr 3755   Oncon0 4066   suc csuc 4068   omcom 4256   X. cxp 4286  (class class class)co 5455   1oc1o 5933   2oc2o 5934   +o coa 5937  [cec 6040   /.cqs 6041   N.cnpi 6256   +N cpli 6257   .N cmi 6258   <N clti 6259   ~Q ceq 6263   Q.cnq 6264   +Q cplq 6266   .Q cmq 6267   <Q cltq 6269

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-13 1401  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-coll 3863  ax-sep 3866  ax-nul 3874  ax-pow 3918  ax-pr 3935  ax-un 4136  ax-setind 4220  ax-iinf 4254

This theorem depends on definitions:  df-bi 110  df-dc 742  df-3or 885  df-3an 886  df-tru 1245  df-fal 1248  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ne 2203  df-ral 2305  df-rex 2306  df-reu 2307  df-rab 2309  df-v 2553  df-sbc 2759  df-csb 2847  df-dif 2914  df-un 2916  df-in 2918  df-ss 2925  df-nul 3219  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-int 3607  df-iun 3650  df-br 3756  df-opab 3810  df-mpt 3811  df-tr 3846  df-eprel 4017  df-id 4021  df-po 4024  df-iso 4025  df-iord 4069  df-on 4071  df-suc 4074  df-iom 4257  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-rn 4299  df-res 4300  df-ima 4301  df-iota 4810  df-fun 4847  df-fn 4848  df-f 4849  df-f1 4850  df-fo 4851  df-f1o 4852  df-fv 4853  df-ov 5458  df-oprab 5459  df-mpt2 5460  df-1st 5709  df-2nd 5710  df-recs 5861  df-irdg 5897  df-1o 5940  df-2o 5941  df-oadd 5944  df-omul 5945  df-er 6042  df-ec 6044  df-qs 6048  df-ni 6288  df-pli 6289  df-mi 6290  df-lti 6291  df-plpq 6328  df-mpq 6329  df-enq 6331  df-nqqs 6332  df-plqqs 6333  df-mqqs 6334  df-1nqqs 6335  df-rq 6336  df-ltnqqs 6337

This theorem is referenced by:  prarloc  6486