Theorem rpnnen1lem3

Description: Lemma for rpnnen1 . (Contributed by Mario Carneiro, 12-May-2013) (Revised by NM, 13-Aug-2021) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	rpnnen1lem.1	|- T = { n e. ZZ | ( n / k ) < x }
	rpnnen1lem.2	|- F = ( x e. RR |-> ( k e. NN |-> ( sup ( T , RR , < ) / k ) ) )
	rpnnen1lem.n	|- NN e. _V
	rpnnen1lem.q	|- QQ e. _V
Assertion	rpnnen1lem3	|- ( x e. RR -> A. n e. ran ( F ` x ) n <_ x )

Proof

Step	Hyp	Ref	Expression
1		rpnnen1lem.1	|- T = { n e. ZZ | ( n / k ) < x }
2		rpnnen1lem.2	|- F = ( x e. RR |-> ( k e. NN |-> ( sup ( T , RR , < ) / k ) ) )
3		rpnnen1lem.n	|- NN e. _V
4		rpnnen1lem.q	|- QQ e. _V
5	3	mptex	|- ( k e. NN |-> ( sup ( T , RR , < ) / k ) ) e. _V
6	2	fvmpt2	|- ( ( x e. RR /\ ( k e. NN |-> ( sup ( T , RR , < ) / k ) ) e. _V ) -> ( F ` x ) = ( k e. NN |-> ( sup ( T , RR , < ) / k ) ) )
7	5 6	mpan2	|- ( x e. RR -> ( F ` x ) = ( k e. NN |-> ( sup ( T , RR , < ) / k ) ) )
8	7	fveq1d	|- ( x e. RR -> ( ( F ` x ) ` k ) = ( ( k e. NN |-> ( sup ( T , RR , < ) / k ) ) ` k ) )
9		ovex	|- ( sup ( T , RR , < ) / k ) e. _V
10		eqid	|- ( k e. NN |-> ( sup ( T , RR , < ) / k ) ) = ( k e. NN |-> ( sup ( T , RR , < ) / k ) )
11	10	fvmpt2	|- ( ( k e. NN /\ ( sup ( T , RR , < ) / k ) e. _V ) -> ( ( k e. NN |-> ( sup ( T , RR , < ) / k ) ) ` k ) = ( sup ( T , RR , < ) / k ) )
12	9 11	mpan2	|- ( k e. NN -> ( ( k e. NN |-> ( sup ( T , RR , < ) / k ) ) ` k ) = ( sup ( T , RR , < ) / k ) )
13	8 12	sylan9eq	|- ( ( x e. RR /\ k e. NN ) -> ( ( F ` x ) ` k ) = ( sup ( T , RR , < ) / k ) )
14	1	rabeq2i	|- ( n e. T <-> ( n e. ZZ /\ ( n / k ) < x ) )
15		zre	|- ( n e. ZZ -> n e. RR )
16	15	adantl	|- ( ( ( x e. RR /\ k e. NN ) /\ n e. ZZ ) -> n e. RR )
17		simpll	|- ( ( ( x e. RR /\ k e. NN ) /\ n e. ZZ ) -> x e. RR )
18		nnre	|- ( k e. NN -> k e. RR )
19		nngt0	|- ( k e. NN -> 0 < k )
20	18 19	jca	|- ( k e. NN -> ( k e. RR /\ 0 < k ) )
21	20	ad2antlr	|- ( ( ( x e. RR /\ k e. NN ) /\ n e. ZZ ) -> ( k e. RR /\ 0 < k ) )
22		ltdivmul	|- ( ( n e. RR /\ x e. RR /\ ( k e. RR /\ 0 < k ) ) -> ( ( n / k ) < x <-> n < ( k x. x ) ) )
23	16 17 21 22	syl3anc	|- ( ( ( x e. RR /\ k e. NN ) /\ n e. ZZ ) -> ( ( n / k ) < x <-> n < ( k x. x ) ) )
24	18	ad2antlr	|- ( ( ( x e. RR /\ k e. NN ) /\ n e. ZZ ) -> k e. RR )
25		remulcl	|- ( ( k e. RR /\ x e. RR ) -> ( k x. x ) e. RR )
26	24 17 25	syl2anc	|- ( ( ( x e. RR /\ k e. NN ) /\ n e. ZZ ) -> ( k x. x ) e. RR )
27		ltle	|- ( ( n e. RR /\ ( k x. x ) e. RR ) -> ( n < ( k x. x ) -> n <_ ( k x. x ) ) )
28	16 26 27	syl2anc	|- ( ( ( x e. RR /\ k e. NN ) /\ n e. ZZ ) -> ( n < ( k x. x ) -> n <_ ( k x. x ) ) )
29	23 28	sylbid	|- ( ( ( x e. RR /\ k e. NN ) /\ n e. ZZ ) -> ( ( n / k ) < x -> n <_ ( k x. x ) ) )
30	29	impr	|- ( ( ( x e. RR /\ k e. NN ) /\ ( n e. ZZ /\ ( n / k ) < x ) ) -> n <_ ( k x. x ) )
31	14 30	sylan2b	|- ( ( ( x e. RR /\ k e. NN ) /\ n e. T ) -> n <_ ( k x. x ) )
32	31	ralrimiva	|- ( ( x e. RR /\ k e. NN ) -> A. n e. T n <_ ( k x. x ) )
33		ssrab2	|- { n e. ZZ | ( n / k ) < x } C_ ZZ
34	1 33	eqsstri	|- T C_ ZZ
35		zssre	|- ZZ C_ RR
36	34 35	sstri	|- T C_ RR
37	36	a1i	|- ( ( x e. RR /\ k e. NN ) -> T C_ RR )
38	25	ancoms	|- ( ( x e. RR /\ k e. RR ) -> ( k x. x ) e. RR )
39	18 38	sylan2	|- ( ( x e. RR /\ k e. NN ) -> ( k x. x ) e. RR )
40		btwnz	|- ( ( k x. x ) e. RR -> ( E. n e. ZZ n < ( k x. x ) /\ E. n e. ZZ ( k x. x ) < n ) )
41	40	simpld	|- ( ( k x. x ) e. RR -> E. n e. ZZ n < ( k x. x ) )
42	39 41	syl	|- ( ( x e. RR /\ k e. NN ) -> E. n e. ZZ n < ( k x. x ) )
43	23	rexbidva	|- ( ( x e. RR /\ k e. NN ) -> ( E. n e. ZZ ( n / k ) < x <-> E. n e. ZZ n < ( k x. x ) ) )
44	42 43	mpbird	|- ( ( x e. RR /\ k e. NN ) -> E. n e. ZZ ( n / k ) < x )
45		rabn0	|- ( { n e. ZZ | ( n / k ) < x } =/= (/) <-> E. n e. ZZ ( n / k ) < x )
46	44 45	sylibr	|- ( ( x e. RR /\ k e. NN ) -> { n e. ZZ | ( n / k ) < x } =/= (/) )
47	1	neeq1i	|- ( T =/= (/) <-> { n e. ZZ | ( n / k ) < x } =/= (/) )
48	46 47	sylibr	|- ( ( x e. RR /\ k e. NN ) -> T =/= (/) )
49		breq2	|- ( y = ( k x. x ) -> ( n <_ y <-> n <_ ( k x. x ) ) )
50	49	ralbidv	|- ( y = ( k x. x ) -> ( A. n e. T n <_ y <-> A. n e. T n <_ ( k x. x ) ) )
51	50	rspcev	|- ( ( ( k x. x ) e. RR /\ A. n e. T n <_ ( k x. x ) ) -> E. y e. RR A. n e. T n <_ y )
52	39 32 51	syl2anc	|- ( ( x e. RR /\ k e. NN ) -> E. y e. RR A. n e. T n <_ y )
53		suprleub	|- ( ( ( T C_ RR /\ T =/= (/) /\ E. y e. RR A. n e. T n <_ y ) /\ ( k x. x ) e. RR ) -> ( sup ( T , RR , < ) <_ ( k x. x ) <-> A. n e. T n <_ ( k x. x ) ) )
54	37 48 52 39 53	syl31anc	|- ( ( x e. RR /\ k e. NN ) -> ( sup ( T , RR , < ) <_ ( k x. x ) <-> A. n e. T n <_ ( k x. x ) ) )
55	32 54	mpbird	|- ( ( x e. RR /\ k e. NN ) -> sup ( T , RR , < ) <_ ( k x. x ) )
56	1 2	rpnnen1lem2	|- ( ( x e. RR /\ k e. NN ) -> sup ( T , RR , < ) e. ZZ )
57	56	zred	|- ( ( x e. RR /\ k e. NN ) -> sup ( T , RR , < ) e. RR )
58		simpl	|- ( ( x e. RR /\ k e. NN ) -> x e. RR )
59	20	adantl	|- ( ( x e. RR /\ k e. NN ) -> ( k e. RR /\ 0 < k ) )
60		ledivmul	|- ( ( sup ( T , RR , < ) e. RR /\ x e. RR /\ ( k e. RR /\ 0 < k ) ) -> ( ( sup ( T , RR , < ) / k ) <_ x <-> sup ( T , RR , < ) <_ ( k x. x ) ) )
61	57 58 59 60	syl3anc	|- ( ( x e. RR /\ k e. NN ) -> ( ( sup ( T , RR , < ) / k ) <_ x <-> sup ( T , RR , < ) <_ ( k x. x ) ) )
62	55 61	mpbird	|- ( ( x e. RR /\ k e. NN ) -> ( sup ( T , RR , < ) / k ) <_ x )
63	13 62	eqbrtrd	|- ( ( x e. RR /\ k e. NN ) -> ( ( F ` x ) ` k ) <_ x )
64	63	ralrimiva	|- ( x e. RR -> A. k e. NN ( ( F ` x ) ` k ) <_ x )
65	1 2 3 4	rpnnen1lem1	|- ( x e. RR -> ( F ` x ) e. ( QQ ^m NN ) )
66	4 3	elmap	|- ( ( F ` x ) e. ( QQ ^m NN ) <-> ( F ` x ) : NN --> QQ )
67	65 66	sylib	|- ( x e. RR -> ( F ` x ) : NN --> QQ )
68		ffn	|- ( ( F ` x ) : NN --> QQ -> ( F ` x ) Fn NN )
69		breq1	|- ( n = ( ( F ` x ) ` k ) -> ( n <_ x <-> ( ( F ` x ) ` k ) <_ x ) )
70	69	ralrn	|- ( ( F ` x ) Fn NN -> ( A. n e. ran ( F ` x ) n <_ x <-> A. k e. NN ( ( F ` x ) ` k ) <_ x ) )
71	67 68 70	3syl	|- ( x e. RR -> ( A. n e. ran ( F ` x ) n <_ x <-> A. k e. NN ( ( F ` x ) ` k ) <_ x ) )
72	64 71	mpbird	|- ( x e. RR -> A. n e. ran ( F ` x ) n <_ x )