Theorem aalioulem2 23301

Description: Lemma for aaliou 23306. (Contributed by Stefan O'Rear, 15-Nov-2014.) (Proof shortened by AV, 28-Sep-2020.)

Hypotheses

Ref	Expression
aalioulem2.a	|- N = (deg ` F )
aalioulem2.b	|- ( ph -> F e. (Poly ` ZZ ) )
aalioulem2.c	|- ( ph -> N e. NN )
aalioulem2.d	|- ( ph -> A e. RR )

Assertion

Ref	Expression
aalioulem2	|- ( ph -> E. x e. RR+ A. p e. ZZ A. q e. NN ( ( F ` ( p / q ) ) = 0 -> ( A = ( p / q ) \/ ( x / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) )

Distinct variable groups:   ph, x, p, q   x, A, p, q   x, F, p, q

Allowed substitution hints:   N( x, q, p)

Proof of Theorem aalioulem2

Dummy variables r a b c d are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		1rp 11296	. . . . . . 7 |- 1 e. RR+
2		snssi 4085	. . . . . . 7 |- ( 1 e. RR+ -> { 1 } C_ RR+ )
3	1, 2	ax-mp 5	. . . . . 6 |- { 1 } C_ RR+
4		ssrab2 3482	. . . . . 6 |- { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } C_ RR+
5	3, 4	unssi 3577	. . . . 5 |- ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) C_ RR+
6		ltso 9701	. . . . . . 7 |- < Or RR
7	6	a1i 11	. . . . . 6 |- ( ph -> < Or RR )
8		snfi 7637	. . . . . . 7 |- { 1 } e. Fin
9		aalioulem2.b	. . . . . . . . . . 11 |- ( ph -> F e. (Poly ` ZZ ) )
10		aalioulem2.c	. . . . . . . . . . . . . 14 |- ( ph -> N e. NN )
11	10	nnne0d 10643	. . . . . . . . . . . . 13 |- ( ph -> N =/= 0 )
12		aalioulem2.a	. . . . . . . . . . . . . 14 |- N = (deg ` F )
13	12	eqcomi 2461	. . . . . . . . . . . . 13 |- (deg ` F ) = N
14		dgr0 23228	. . . . . . . . . . . . 13 |- (deg ` 0p ) = 0
15	11, 13, 14	3netr4g 2703	. . . . . . . . . . . 12 |- ( ph -> (deg ` F ) =/= (deg ` 0p ) )
16		fveq2 5848	. . . . . . . . . . . . 13 |- ( F = 0p -> (deg ` F ) = (deg ` 0p ) )
17	16	necon3i 2656	. . . . . . . . . . . 12 |- ( (deg ` F ) =/= (deg ` 0p ) -> F =/= 0p )
18	15, 17	syl 17	. . . . . . . . . . 11 |- ( ph -> F =/= 0p )
19		eqid 2452	. . . . . . . . . . . 12 |- ( `' F " { 0 } ) = ( `' F " { 0 } )
20	19	fta1 23273	. . . . . . . . . . 11 |- ( ( F e. (Poly ` ZZ ) /\ F =/= 0p ) -> ( ( `' F " { 0 } ) e. Fin /\ ( # ` ( `' F " { 0 } ) ) <_ (deg ` F ) ) )
21	9, 18, 20	syl2anc 671	. . . . . . . . . 10 |- ( ph -> ( ( `' F " { 0 } ) e. Fin /\ ( # ` ( `' F " { 0 } ) ) <_ (deg ` F ) ) )
22	21	simpld 465	. . . . . . . . 9 |- ( ph -> ( `' F " { 0 } ) e. Fin )
23		abrexfi 7861	. . . . . . . . 9 |- ( ( `' F " { 0 } ) e. Fin -> { a | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } e. Fin )
24	22, 23	syl 17	. . . . . . . 8 |- ( ph -> { a | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } e. Fin )
25		rabssab 3484	. . . . . . . 8 |- { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } C_ { a | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) }
26		ssfi 7779	. . . . . . . 8 |- ( ( { a | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } e. Fin /\ { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } C_ { a | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) -> { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } e. Fin )
27	24, 25, 26	sylancl 673	. . . . . . 7 |- ( ph -> { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } e. Fin )
28		unfi 7825	. . . . . . 7 |- ( ( { 1 } e. Fin /\ { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } e. Fin ) -> ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) e. Fin )
29	8, 27, 28	sylancr 674	. . . . . 6 |- ( ph -> ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) e. Fin )
30		1ex 9625	. . . . . . . . 9 |- 1 e. _V
31	30	snid 3964	. . . . . . . 8 |- 1 e. { 1 }
32		elun1 3569	. . . . . . . 8 |- ( 1 e. { 1 } -> 1 e. ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) )
33		ne0i 3705	. . . . . . . 8 |- ( 1 e. ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) -> ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) =/= (/) )
34	31, 32, 33	mp2b 10	. . . . . . 7 |- ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) =/= (/)
35	34	a1i 11	. . . . . 6 |- ( ph -> ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) =/= (/) )
36		rpssre 11302	. . . . . . . 8 |- RR+ C_ RR
37	5, 36	sstri 3409	. . . . . . 7 |- ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) C_ RR
38	37	a1i 11	. . . . . 6 |- ( ph -> ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) C_ RR )
39		fiinfcl 8004	. . . . . 6 |- ( ( < Or RR /\ ( ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) e. Fin /\ ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) =/= (/) /\ ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) C_ RR ) ) -> inf ( ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) , RR , < ) e. ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) )
40	7, 29, 35, 38, 39	syl13anc 1273	. . . . 5 |- ( ph -> inf ( ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) , RR , < ) e. ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) )
41	5, 40	sseldi 3398	. . . 4 |- ( ph -> inf ( ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) , RR , < ) e. RR+ )
42	37	a1i 11	. . . . . . . . 9 |- ( ( ( ph /\ r e. RR ) /\ ( ( F ` r ) = 0 /\ -. A = r ) ) -> ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) C_ RR )
43		0re 9630	. . . . . . . . . . . 12 |- 0 e. RR
44		rpge0 11304	. . . . . . . . . . . . 13 |- ( d e. RR+ -> 0 <_ d )
45	44	rgen 2747	. . . . . . . . . . . 12 |- A. d e. RR+ 0 <_ d
46		breq1 4377	. . . . . . . . . . . . . 14 |- ( c = 0 -> ( c <_ d <-> 0 <_ d ) )
47	46	ralbidv 2810	. . . . . . . . . . . . 13 |- ( c = 0 -> ( A. d e. RR+ c <_ d <-> A. d e. RR+ 0 <_ d ) )
48	47	rspcev 3118	. . . . . . . . . . . 12 |- ( ( 0 e. RR /\ A. d e. RR+ 0 <_ d ) -> E. c e. RR A. d e. RR+ c <_ d )
49	43, 45, 48	mp2an 683	. . . . . . . . . . 11 |- E. c e. RR A. d e. RR+ c <_ d
50		ssralv 3461	. . . . . . . . . . . . 13 |- ( ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) C_ RR+ -> ( A. d e. RR+ c <_ d -> A. d e. ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) c <_ d ) )
51	5, 50	ax-mp 5	. . . . . . . . . . . 12 |- ( A. d e. RR+ c <_ d -> A. d e. ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) c <_ d )
52	51	reximi 2833	. . . . . . . . . . 11 |- ( E. c e. RR A. d e. RR+ c <_ d -> E. c e. RR A. d e. ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) c <_ d )
53	49, 52	ax-mp 5	. . . . . . . . . 10 |- E. c e. RR A. d e. ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) c <_ d
54	53	a1i 11	. . . . . . . . 9 |- ( ( ( ph /\ r e. RR ) /\ ( ( F ` r ) = 0 /\ -. A = r ) ) -> E. c e. RR A. d e. ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) c <_ d )
55		aalioulem2.d	. . . . . . . . . . . . . . 15 |- ( ph -> A e. RR )
56	55	ad2antrr 737	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ r e. RR ) /\ ( ( F ` r ) = 0 /\ -. A = r ) ) -> A e. RR )
57		simplr 767	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ r e. RR ) /\ ( ( F ` r ) = 0 /\ -. A = r ) ) -> r e. RR )
58	56, 57	resubcld 10036	. . . . . . . . . . . . 13 |- ( ( ( ph /\ r e. RR ) /\ ( ( F ` r ) = 0 /\ -. A = r ) ) -> ( A - r ) e. RR )
59	58	recnd 9656	. . . . . . . . . . . 12 |- ( ( ( ph /\ r e. RR ) /\ ( ( F ` r ) = 0 /\ -. A = r ) ) -> ( A - r ) e. CC )
60	55	ad2antrr 737	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ r e. RR ) /\ ( F ` r ) = 0 ) -> A e. RR )
61	60	recnd 9656	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ r e. RR ) /\ ( F ` r ) = 0 ) -> A e. CC )
62		simplr 767	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ r e. RR ) /\ ( F ` r ) = 0 ) -> r e. RR )
63	62	recnd 9656	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ r e. RR ) /\ ( F ` r ) = 0 ) -> r e. CC )
64	61, 63	subeq0ad 9983	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ r e. RR ) /\ ( F ` r ) = 0 ) -> ( ( A - r ) = 0 <-> A = r ) )
65	64	necon3abid 2660	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ r e. RR ) /\ ( F ` r ) = 0 ) -> ( ( A - r ) =/= 0 <-> -. A = r ) )
66	65	biimprd 231	. . . . . . . . . . . . 13 |- ( ( ( ph /\ r e. RR ) /\ ( F ` r ) = 0 ) -> ( -. A = r -> ( A - r ) =/= 0 ) )
67	66	impr 629	. . . . . . . . . . . 12 |- ( ( ( ph /\ r e. RR ) /\ ( ( F ` r ) = 0 /\ -. A = r ) ) -> ( A - r ) =/= 0 )
68	59, 67	absrpcld 13521	. . . . . . . . . . 11 |- ( ( ( ph /\ r e. RR ) /\ ( ( F ` r ) = 0 /\ -. A = r ) ) -> ( abs ` ( A - r ) ) e. RR+ )
69	57	recnd 9656	. . . . . . . . . . . . 13 |- ( ( ( ph /\ r e. RR ) /\ ( ( F ` r ) = 0 /\ -. A = r ) ) -> r e. CC )
70		simprl 769	. . . . . . . . . . . . 13 |- ( ( ( ph /\ r e. RR ) /\ ( ( F ` r ) = 0 /\ -. A = r ) ) -> ( F ` r ) = 0 )
71		plyf 23164	. . . . . . . . . . . . . . . . 17 |- ( F e. (Poly ` ZZ ) -> F : CC --> CC )
72	9, 71	syl 17	. . . . . . . . . . . . . . . 16 |- ( ph -> F : CC --> CC )
73		ffn 5711	. . . . . . . . . . . . . . . 16 |- ( F : CC --> CC -> F Fn CC )
74	72, 73	syl 17	. . . . . . . . . . . . . . 15 |- ( ph -> F Fn CC )
75	74	ad2antrr 737	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ r e. RR ) /\ ( ( F ` r ) = 0 /\ -. A = r ) ) -> F Fn CC )
76		fniniseg 5987	. . . . . . . . . . . . . 14 |- ( F Fn CC -> ( r e. ( `' F " { 0 } ) <-> ( r e. CC /\ ( F ` r ) = 0 ) ) )
77	75, 76	syl 17	. . . . . . . . . . . . 13 |- ( ( ( ph /\ r e. RR ) /\ ( ( F ` r ) = 0 /\ -. A = r ) ) -> ( r e. ( `' F " { 0 } ) <-> ( r e. CC /\ ( F ` r ) = 0 ) ) )
78	69, 70, 77	mpbir2and 933	. . . . . . . . . . . 12 |- ( ( ( ph /\ r e. RR ) /\ ( ( F ` r ) = 0 /\ -. A = r ) ) -> r e. ( `' F " { 0 } ) )
79		eqid 2452	. . . . . . . . . . . 12 |- ( abs ` ( A - r ) ) = ( abs ` ( A - r ) )
80		oveq2 6284	. . . . . . . . . . . . . . 15 |- ( b = r -> ( A - b ) = ( A - r ) )
81	80	fveq2d 5852	. . . . . . . . . . . . . 14 |- ( b = r -> ( abs ` ( A - b ) ) = ( abs ` ( A - r ) ) )
82	81	eqeq2d 2462	. . . . . . . . . . . . 13 |- ( b = r -> ( ( abs ` ( A - r ) ) = ( abs ` ( A - b ) ) <-> ( abs ` ( A - r ) ) = ( abs ` ( A - r ) ) ) )
83	82	rspcev 3118	. . . . . . . . . . . 12 |- ( ( r e. ( `' F " { 0 } ) /\ ( abs ` ( A - r ) ) = ( abs ` ( A - r ) ) ) -> E. b e. ( `' F " { 0 } ) ( abs ` ( A - r ) ) = ( abs ` ( A - b ) ) )
84	78, 79, 83	sylancl 673	. . . . . . . . . . 11 |- ( ( ( ph /\ r e. RR ) /\ ( ( F ` r ) = 0 /\ -. A = r ) ) -> E. b e. ( `' F " { 0 } ) ( abs ` ( A - r ) ) = ( abs ` ( A - b ) ) )
85		eqeq1 2456	. . . . . . . . . . . . 13 |- ( a = ( abs ` ( A - r ) ) -> ( a = ( abs ` ( A - b ) ) <-> ( abs ` ( A - r ) ) = ( abs ` ( A - b ) ) ) )
86	85	rexbidv 2873	. . . . . . . . . . . 12 |- ( a = ( abs ` ( A - r ) ) -> ( E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) <-> E. b e. ( `' F " { 0 } ) ( abs ` ( A - r ) ) = ( abs ` ( A - b ) ) ) )
87	86	elrab 3164	. . . . . . . . . . 11 |- ( ( abs ` ( A - r ) ) e. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } <-> ( ( abs ` ( A - r ) ) e. RR+ /\ E. b e. ( `' F " { 0 } ) ( abs ` ( A - r ) ) = ( abs ` ( A - b ) ) ) )
88	68, 84, 87	sylanbrc 675	. . . . . . . . . 10 |- ( ( ( ph /\ r e. RR ) /\ ( ( F ` r ) = 0 /\ -. A = r ) ) -> ( abs ` ( A - r ) ) e. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } )
89		elun2 3570	. . . . . . . . . 10 |- ( ( abs ` ( A - r ) ) e. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } -> ( abs ` ( A - r ) ) e. ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) )
90	88, 89	syl 17	. . . . . . . . 9 |- ( ( ( ph /\ r e. RR ) /\ ( ( F ` r ) = 0 /\ -. A = r ) ) -> ( abs ` ( A - r ) ) e. ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) )
91		infrelb 10585	. . . . . . . . 9 |- ( ( ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) C_ RR /\ E. c e. RR A. d e. ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) c <_ d /\ ( abs ` ( A - r ) ) e. ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) ) -> inf ( ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) , RR , < ) <_ ( abs ` ( A - r ) ) )
92	42, 54, 90, 91	syl3anc 1271	. . . . . . . 8 |- ( ( ( ph /\ r e. RR ) /\ ( ( F ` r ) = 0 /\ -. A = r ) ) -> inf ( ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) , RR , < ) <_ ( abs ` ( A - r ) ) )
93	92	expr 624	. . . . . . 7 |- ( ( ( ph /\ r e. RR ) /\ ( F ` r ) = 0 ) -> ( -. A = r -> inf ( ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) , RR , < ) <_ ( abs ` ( A - r ) ) ) )
94	93	orrd 384	. . . . . 6 |- ( ( ( ph /\ r e. RR ) /\ ( F ` r ) = 0 ) -> ( A = r \/ inf ( ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) , RR , < ) <_ ( abs ` ( A - r ) ) ) )
95	94	ex 440	. . . . 5 |- ( ( ph /\ r e. RR ) -> ( ( F ` r ) = 0 -> ( A = r \/ inf ( ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) , RR , < ) <_ ( abs ` ( A - r ) ) ) ) )
96	95	ralrimiva 2790	. . . 4 |- ( ph -> A. r e. RR ( ( F ` r ) = 0 -> ( A = r \/ inf ( ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) , RR , < ) <_ ( abs ` ( A - r ) ) ) ) )
97		breq1 4377	. . . . . . . 8 |- ( x = inf ( ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) , RR , < ) -> ( x <_ ( abs ` ( A - r ) ) <-> inf ( ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) , RR , < ) <_ ( abs ` ( A - r ) ) ) )
98	97	orbi2d 713	. . . . . . 7 |- ( x = inf ( ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) , RR , < ) -> ( ( A = r \/ x <_ ( abs ` ( A - r ) ) ) <-> ( A = r \/ inf ( ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) , RR , < ) <_ ( abs ` ( A - r ) ) ) ) )
99	98	imbi2d 322	. . . . . 6 |- ( x = inf ( ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) , RR , < ) -> ( ( ( F ` r ) = 0 -> ( A = r \/ x <_ ( abs ` ( A - r ) ) ) ) <-> ( ( F ` r ) = 0 -> ( A = r \/ inf ( ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) , RR , < ) <_ ( abs ` ( A - r ) ) ) ) ) )
100	99	ralbidv 2810	. . . . 5 |- ( x = inf ( ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) , RR , < ) -> ( A. r e. RR ( ( F ` r ) = 0 -> ( A = r \/ x <_ ( abs ` ( A - r ) ) ) ) <-> A. r e. RR ( ( F ` r ) = 0 -> ( A = r \/ inf ( ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) , RR , < ) <_ ( abs ` ( A - r ) ) ) ) ) )
101	100	rspcev 3118	. . . 4 |- ( (inf ( ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) , RR , < ) e. RR+ /\ A. r e. RR ( ( F ` r ) = 0 -> ( A = r \/ inf ( ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) , RR , < ) <_ ( abs ` ( A - r ) ) ) ) ) -> E. x e. RR+ A. r e. RR ( ( F ` r ) = 0 -> ( A = r \/ x <_ ( abs ` ( A - r ) ) ) ) )
102	41, 96, 101	syl2anc 671	. . 3 |- ( ph -> E. x e. RR+ A. r e. RR ( ( F ` r ) = 0 -> ( A = r \/ x <_ ( abs ` ( A - r ) ) ) ) )
103		znq 11258	. . . . . . . 8 |- ( ( p e. ZZ /\ q e. NN ) -> ( p / q ) e. QQ )
104		qre 11259	. . . . . . . 8 |- ( ( p / q ) e. QQ -> ( p / q ) e. RR )
105	103, 104	syl 17	. . . . . . 7 |- ( ( p e. ZZ /\ q e. NN ) -> ( p / q ) e. RR )
106		fveq2 5848	. . . . . . . . . 10 |- ( r = ( p / q ) -> ( F ` r ) = ( F ` ( p / q ) ) )
107	106	eqeq1d 2454	. . . . . . . . 9 |- ( r = ( p / q ) -> ( ( F ` r ) = 0 <-> ( F ` ( p / q ) ) = 0 ) )
108		eqeq2 2463	. . . . . . . . . 10 |- ( r = ( p / q ) -> ( A = r <-> A = ( p / q ) ) )
109		oveq2 6284	. . . . . . . . . . . 12 |- ( r = ( p / q ) -> ( A - r ) = ( A - ( p / q ) ) )
110	109	fveq2d 5852	. . . . . . . . . . 11 |- ( r = ( p / q ) -> ( abs ` ( A - r ) ) = ( abs ` ( A - ( p / q ) ) ) )
111	110	breq2d 4386	. . . . . . . . . 10 |- ( r = ( p / q ) -> ( x <_ ( abs ` ( A - r ) ) <-> x <_ ( abs ` ( A - ( p / q ) ) ) ) )
112	108, 111	orbi12d 721	. . . . . . . . 9 |- ( r = ( p / q ) -> ( ( A = r \/ x <_ ( abs ` ( A - r ) ) ) <-> ( A = ( p / q ) \/ x <_ ( abs ` ( A - ( p / q ) ) ) ) ) )
113	107, 112	imbi12d 326	. . . . . . . 8 |- ( r = ( p / q ) -> ( ( ( F ` r ) = 0 -> ( A = r \/ x <_ ( abs ` ( A - r ) ) ) ) <-> ( ( F ` ( p / q ) ) = 0 -> ( A = ( p / q ) \/ x <_ ( abs ` ( A - ( p / q ) ) ) ) ) ) )
114	113	rspcv 3114	. . . . . . 7 |- ( ( p / q ) e. RR -> ( A. r e. RR ( ( F ` r ) = 0 -> ( A = r \/ x <_ ( abs ` ( A - r ) ) ) ) -> ( ( F ` ( p / q ) ) = 0 -> ( A = ( p / q ) \/ x <_ ( abs ` ( A - ( p / q ) ) ) ) ) ) )
115	105, 114	syl 17	. . . . . 6 |- ( ( p e. ZZ /\ q e. NN ) -> ( A. r e. RR ( ( F ` r ) = 0 -> ( A = r \/ x <_ ( abs ` ( A - r ) ) ) ) -> ( ( F ` ( p / q ) ) = 0 -> ( A = ( p / q ) \/ x <_ ( abs ` ( A - ( p / q ) ) ) ) ) ) )
116	115	com12 32	. . . . 5 |- ( A. r e. RR ( ( F ` r ) = 0 -> ( A = r \/ x <_ ( abs ` ( A - r ) ) ) ) -> ( ( p e. ZZ /\ q e. NN ) -> ( ( F ` ( p / q ) ) = 0 -> ( A = ( p / q ) \/ x <_ ( abs ` ( A - ( p / q ) ) ) ) ) ) )
117	116	ralrimivv 2794	. . . 4 |- ( A. r e. RR ( ( F ` r ) = 0 -> ( A = r \/ x <_ ( abs ` ( A - r ) ) ) ) -> A. p e. ZZ A. q e. NN ( ( F ` ( p / q ) ) = 0 -> ( A = ( p / q ) \/ x <_ ( abs ` ( A - ( p / q ) ) ) ) ) )
118	117	reximi 2833	. . 3 |- ( E. x e. RR+ A. r e. RR ( ( F ` r ) = 0 -> ( A = r \/ x <_ ( abs ` ( A - r ) ) ) ) -> E. x e. RR+ A. p e. ZZ A. q e. NN ( ( F ` ( p / q ) ) = 0 -> ( A = ( p / q ) \/ x <_ ( abs ` ( A - ( p / q ) ) ) ) ) )
119	102, 118	syl 17	. 2 |- ( ph -> E. x e. RR+ A. p e. ZZ A. q e. NN ( ( F ` ( p / q ) ) = 0 -> ( A = ( p / q ) \/ x <_ ( abs ` ( A - ( p / q ) ) ) ) ) )
120		simplr 767	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> x e. RR+ )
121		simprr 771	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> q e. NN )
122	10	nnnn0d 10915	. . . . . . . . . . . . . 14 |- ( ph -> N e. NN0 )
123	122	ad2antrr 737	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> N e. NN0 )
124	121, 123	nnexpcld 12431	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( q ^ N ) e. NN )
125	124	nnrpd 11329	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( q ^ N ) e. RR+ )
126	120, 125	rpdivcld 11348	. . . . . . . . . 10 |- ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( x / ( q ^ N ) ) e. RR+ )
127	126	rpred 11331	. . . . . . . . 9 |- ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( x / ( q ^ N ) ) e. RR )
128	127	adantr 471	. . . . . . . 8 |- ( ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) /\ x <_ ( abs ` ( A - ( p / q ) ) ) ) -> ( x / ( q ^ N ) ) e. RR )
129		simpllr 774	. . . . . . . . 9 |- ( ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) /\ x <_ ( abs ` ( A - ( p / q ) ) ) ) -> x e. RR+ )
130	129	rpred 11331	. . . . . . . 8 |- ( ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) /\ x <_ ( abs ` ( A - ( p / q ) ) ) ) -> x e. RR )
131	55	ad2antrr 737	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> A e. RR )
132	105	adantl 472	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( p / q ) e. RR )
133	131, 132	resubcld 10036	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( A - ( p / q ) ) e. RR )
134	133	recnd 9656	. . . . . . . . . 10 |- ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( A - ( p / q ) ) e. CC )
135	134	abscld 13509	. . . . . . . . 9 |- ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( abs ` ( A - ( p / q ) ) ) e. RR )
136	135	adantr 471	. . . . . . . 8 |- ( ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) /\ x <_ ( abs ` ( A - ( p / q ) ) ) ) -> ( abs ` ( A - ( p / q ) ) ) e. RR )
137		rpre 11298	. . . . . . . . . . 11 |- ( x e. RR+ -> x e. RR )
138	137	ad2antlr 738	. . . . . . . . . 10 |- ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> x e. RR )
139	120	rpcnne0d 11340	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( x e. CC /\ x =/= 0 ) )
140		divid 10286	. . . . . . . . . . . 12 |- ( ( x e. CC /\ x =/= 0 ) -> ( x / x ) = 1 )
141	139, 140	syl 17	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( x / x ) = 1 )
142	124	nnge1d 10641	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> 1 <_ ( q ^ N ) )
143	141, 142	eqbrtrd 4395	. . . . . . . . . 10 |- ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( x / x ) <_ ( q ^ N ) )
144	138, 120, 125, 143	lediv23d 11394	. . . . . . . . 9 |- ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( x / ( q ^ N ) ) <_ x )
145	144	adantr 471	. . . . . . . 8 |- ( ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) /\ x <_ ( abs ` ( A - ( p / q ) ) ) ) -> ( x / ( q ^ N ) ) <_ x )
146		simpr 467	. . . . . . . 8 |- ( ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) /\ x <_ ( abs ` ( A - ( p / q ) ) ) ) -> x <_ ( abs ` ( A - ( p / q ) ) ) )
147	128, 130, 136, 145, 146	letrd 9779	. . . . . . 7 |- ( ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) /\ x <_ ( abs ` ( A - ( p / q ) ) ) ) -> ( x / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) )
148	147	ex 440	. . . . . 6 |- ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( x <_ ( abs ` ( A - ( p / q ) ) ) -> ( x / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) )
149	148	orim2d 855	. . . . 5 |- ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( ( A = ( p / q ) \/ x <_ ( abs ` ( A - ( p / q ) ) ) ) -> ( A = ( p / q ) \/ ( x / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) )
150	149	imim2d 54	. . . 4 |- ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( ( ( F ` ( p / q ) ) = 0 -> ( A = ( p / q ) \/ x <_ ( abs ` ( A - ( p / q ) ) ) ) ) -> ( ( F ` ( p / q ) ) = 0 -> ( A = ( p / q ) \/ ( x / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) ) )
151	150	ralimdvva 2788	. . 3 |- ( ( ph /\ x e. RR+ ) -> ( A. p e. ZZ A. q e. NN ( ( F ` ( p / q ) ) = 0 -> ( A = ( p / q ) \/ x <_ ( abs ` ( A - ( p / q ) ) ) ) ) -> A. p e. ZZ A. q e. NN ( ( F ` ( p / q ) ) = 0 -> ( A = ( p / q ) \/ ( x / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) ) )
152	151	reximdva 2839	. 2 |- ( ph -> ( E. x e. RR+ A. p e. ZZ A. q e. NN ( ( F ` ( p / q ) ) = 0 -> ( A = ( p / q ) \/ x <_ ( abs ` ( A - ( p / q ) ) ) ) ) -> E. x e. RR+ A. p e. ZZ A. q e. NN ( ( F ` ( p / q ) ) = 0 -> ( A = ( p / q ) \/ ( x / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) ) )
153	119, 152	mpd 15	1 |- ( ph -> E. x e. RR+ A. p e. ZZ A. q e. NN ( ( F ` ( p / q ) ) = 0 -> ( A = ( p / q ) \/ ( x / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 189   \/ wo 374   /\ wa 375   = wceq 1448   e. wcel 1891   {cab 2438   =/= wne 2622   A.wral 2737   E.wrex 2738   {crab 2741   u. cun 3370   C_ wss 3372   (/)c0 3699   {csn 3936   class class class wbr 4374   Or wor 4732   `'ccnv 4811   "cima 4815   Fn wfn 5556   -->wf 5557   ` cfv 5561  (class class class)co 6276   Fincfn 7556  infcinf 7942   CCcc 9524   RRcr 9525   0cc0 9526   1c1 9527   < clt 9662   <_ cle 9663   - cmin 9847   / cdiv 10258   NNcn 10598   NN0cn0 10859   ZZcz 10927   QQcq 11254   RR+crp 11292   ^cexp 12266   #chash 12509   abscabs 13308   0pc0p 22639  Polycply 23150  degcdgr 23153

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-5 1762  ax-6 1809  ax-7 1855  ax-8 1893  ax-9 1900  ax-10 1919  ax-11 1924  ax-12 1937  ax-13 2092  ax-ext 2432  ax-rep 4487  ax-sep 4497  ax-nul 4506  ax-pow 4554  ax-pr 4612  ax-un 6571  ax-inf2 8133  ax-cnex 9582  ax-resscn 9583  ax-1cn 9584  ax-icn 9585  ax-addcl 9586  ax-addrcl 9587  ax-mulcl 9588  ax-mulrcl 9589  ax-mulcom 9590  ax-addass 9591  ax-mulass 9592  ax-distr 9593  ax-i2m1 9594  ax-1ne0 9595  ax-1rid 9596  ax-rnegex 9597  ax-rrecex 9598  ax-cnre 9599  ax-pre-lttri 9600  ax-pre-lttrn 9601  ax-pre-ltadd 9602  ax-pre-mulgt0 9603  ax-pre-sup 9604  ax-addf 9605

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 987  df-3an 988  df-tru 1451  df-fal 1454  df-ex 1668  df-nf 1672  df-sb 1802  df-eu 2304  df-mo 2305  df-clab 2439  df-cleq 2445  df-clel 2448  df-nfc 2582  df-ne 2624  df-nel 2625  df-ral 2742  df-rex 2743  df-reu 2744  df-rmo 2745  df-rab 2746  df-v 3015  df-sbc 3236  df-csb 3332  df-dif 3375  df-un 3377  df-in 3379  df-ss 3386  df-pss 3388  df-nul 3700  df-if 3850  df-pw 3921  df-sn 3937  df-pr 3939  df-tp 3941  df-op 3943  df-uni 4169  df-int 4205  df-iun 4250  df-br 4375  df-opab 4434  df-mpt 4435  df-tr 4470  df-eprel 4723  df-id 4727  df-po 4733  df-so 4734  df-fr 4771  df-se 4772  df-we 4773  df-xp 4818  df-rel 4819  df-cnv 4820  df-co 4821  df-dm 4822  df-rn 4823  df-res 4824  df-ima 4825  df-pred 5359  df-ord 5405  df-on 5406  df-lim 5407  df-suc 5408  df-iota 5525  df-fun 5563  df-fn 5564  df-f 5565  df-f1 5566  df-fo 5567  df-f1o 5568  df-fv 5569  df-isom 5570  df-riota 6238  df-ov 6279  df-oprab 6280  df-mpt2 6281  df-of 6519  df-om 6681  df-1st 6781  df-2nd 6782  df-wrecs 7015  df-recs 7077  df-rdg 7115  df-1o 7169  df-oadd 7173  df-er 7350  df-map 7461  df-pm 7462  df-en 7557  df-dom 7558  df-sdom 7559  df-fin 7560  df-sup 7943  df-inf 7944  df-oi 8012  df-card 8360  df-cda 8585  df-pnf 9664  df-mnf 9665  df-xr 9666  df-ltxr 9667  df-le 9668  df-sub 9849  df-neg 9850  df-div 10259  df-nn 10599  df-2 10657  df-3 10658  df-n0 10860  df-z 10928  df-uz 11150  df-q 11255  df-rp 11293  df-fz 11776  df-fzo 11909  df-fl 12022  df-seq 12208  df-exp 12267  df-hash 12510  df-cj 13173  df-re 13174  df-im 13175  df-sqrt 13309  df-abs 13310  df-clim 13563  df-rlim 13564  df-sum 13764  df-0p 22640  df-ply 23154  df-idp 23155  df-coe 23156  df-dgr 23157  df-quot 23256

This theorem is referenced by:  aalioulem6  23305