Theorem caucvgrelemcau 11341

Description: Lemma for caucvgre 11342. Converting the Cauchy condition. (Contributed by Jim Kingdon, 20-Jul-2021.)

Hypotheses

Ref	Expression
caucvgre.f	|- ( ph -> F : NN --> RR )
caucvgre.cau	|- ( ph -> A. n e. NN A. k e. ( ZZ>= ` n ) ( ( F ` n ) < ( ( F ` k ) + ( 1 / n ) ) /\ ( F ` k ) < ( ( F ` n ) + ( 1 / n ) ) ) )

Assertion

Ref	Expression
caucvgrelemcau	|- ( ph -> A. n e. NN A. k e. NN ( n <RR k -> ( ( F ` n ) <RR ( ( F ` k ) + ( iota_ r e. RR ( n x. r ) = 1 ) ) /\ ( F ` k ) <RR ( ( F ` n ) + ( iota_ r e. RR ( n x. r ) = 1 ) ) ) ) )

Distinct variable groups:   k, F, n   ph, k, n   k, r, n

Allowed substitution hints:   ph( r)   F( r)

Proof of Theorem caucvgrelemcau

Step	Hyp	Ref	Expression
1		simplr 528	. . . . . . 7 |- ( ( ( ph /\ n e. NN ) /\ k e. NN ) -> n e. NN )
2	1	nnred 9062	. . . . . 6 |- ( ( ( ph /\ n e. NN ) /\ k e. NN ) -> n e. RR )
3		simpr 110	. . . . . . 7 |- ( ( ( ph /\ n e. NN ) /\ k e. NN ) -> k e. NN )
4	3	nnred 9062	. . . . . 6 |- ( ( ( ph /\ n e. NN ) /\ k e. NN ) -> k e. RR )
5		ltle 8173	. . . . . 6 |- ( ( n e. RR /\ k e. RR ) -> ( n < k -> n <_ k ) )
6	2, 4, 5	syl2anc 411	. . . . 5 |- ( ( ( ph /\ n e. NN ) /\ k e. NN ) -> ( n < k -> n <_ k ) )
7		eluznn 9734	. . . . . . . . . . . 12 |- ( ( n e. NN /\ k e. ( ZZ>= ` n ) ) -> k e. NN )
8	7	ex 115	. . . . . . . . . . 11 |- ( n e. NN -> ( k e. ( ZZ>= ` n ) -> k e. NN ) )
9		nnz 9404	. . . . . . . . . . . . 13 |- ( n e. NN -> n e. ZZ )
10		eluz1 9665	. . . . . . . . . . . . 13 |- ( n e. ZZ -> ( k e. ( ZZ>= ` n ) <-> ( k e. ZZ /\ n <_ k ) ) )
11	9, 10	syl 14	. . . . . . . . . . . 12 |- ( n e. NN -> ( k e. ( ZZ>= ` n ) <-> ( k e. ZZ /\ n <_ k ) ) )
12		simpr 110	. . . . . . . . . . . 12 |- ( ( k e. ZZ /\ n <_ k ) -> n <_ k )
13	11, 12	biimtrdi 163	. . . . . . . . . . 11 |- ( n e. NN -> ( k e. ( ZZ>= ` n ) -> n <_ k ) )
14	8, 13	jcad 307	. . . . . . . . . 10 |- ( n e. NN -> ( k e. ( ZZ>= ` n ) -> ( k e. NN /\ n <_ k ) ) )
15		nnz 9404	. . . . . . . . . . . 12 |- ( k e. NN -> k e. ZZ )
16	15	anim1i 340	. . . . . . . . . . 11 |- ( ( k e. NN /\ n <_ k ) -> ( k e. ZZ /\ n <_ k ) )
17	16, 11	imbitrrid 156	. . . . . . . . . 10 |- ( n e. NN -> ( ( k e. NN /\ n <_ k ) -> k e. ( ZZ>= ` n ) ) )
18	14, 17	impbid 129	. . . . . . . . 9 |- ( n e. NN -> ( k e. ( ZZ>= ` n ) <-> ( k e. NN /\ n <_ k ) ) )
19	18	adantl 277	. . . . . . . 8 |- ( ( ph /\ n e. NN ) -> ( k e. ( ZZ>= ` n ) <-> ( k e. NN /\ n <_ k ) ) )
20	19	biimpar 297	. . . . . . 7 |- ( ( ( ph /\ n e. NN ) /\ ( k e. NN /\ n <_ k ) ) -> k e. ( ZZ>= ` n ) )
21		caucvgre.cau	. . . . . . . . 9 |- ( ph -> A. n e. NN A. k e. ( ZZ>= ` n ) ( ( F ` n ) < ( ( F ` k ) + ( 1 / n ) ) /\ ( F ` k ) < ( ( F ` n ) + ( 1 / n ) ) ) )
22	21	r19.21bi 2595	. . . . . . . 8 |- ( ( ph /\ n e. NN ) -> A. k e. ( ZZ>= ` n ) ( ( F ` n ) < ( ( F ` k ) + ( 1 / n ) ) /\ ( F ` k ) < ( ( F ` n ) + ( 1 / n ) ) ) )
23	22	r19.21bi 2595	. . . . . . 7 |- ( ( ( ph /\ n e. NN ) /\ k e. ( ZZ>= ` n ) ) -> ( ( F ` n ) < ( ( F ` k ) + ( 1 / n ) ) /\ ( F ` k ) < ( ( F ` n ) + ( 1 / n ) ) ) )
24	20, 23	syldan 282	. . . . . 6 |- ( ( ( ph /\ n e. NN ) /\ ( k e. NN /\ n <_ k ) ) -> ( ( F ` n ) < ( ( F ` k ) + ( 1 / n ) ) /\ ( F ` k ) < ( ( F ` n ) + ( 1 / n ) ) ) )
25	24	expr 375	. . . . 5 |- ( ( ( ph /\ n e. NN ) /\ k e. NN ) -> ( n <_ k -> ( ( F ` n ) < ( ( F ` k ) + ( 1 / n ) ) /\ ( F ` k ) < ( ( F ` n ) + ( 1 / n ) ) ) ) )
26	6, 25	syld 45	. . . 4 |- ( ( ( ph /\ n e. NN ) /\ k e. NN ) -> ( n < k -> ( ( F ` n ) < ( ( F ` k ) + ( 1 / n ) ) /\ ( F ` k ) < ( ( F ` n ) + ( 1 / n ) ) ) ) )
27		ltxrlt 8151	. . . . 5 |- ( ( n e. RR /\ k e. RR ) -> ( n < k <-> n <RR k ) )
28	2, 4, 27	syl2anc 411	. . . 4 |- ( ( ( ph /\ n e. NN ) /\ k e. NN ) -> ( n < k <-> n <RR k ) )
29		caucvgre.f	. . . . . . . . 9 |- ( ph -> F : NN --> RR )
30	29	ad2antrr 488	. . . . . . . 8 |- ( ( ( ph /\ n e. NN ) /\ k e. NN ) -> F : NN --> RR )
31	30, 1	ffvelcdmd 5726	. . . . . . 7 |- ( ( ( ph /\ n e. NN ) /\ k e. NN ) -> ( F ` n ) e. RR )
32	30, 3	ffvelcdmd 5726	. . . . . . . 8 |- ( ( ( ph /\ n e. NN ) /\ k e. NN ) -> ( F ` k ) e. RR )
33	1	nnrecred 9096	. . . . . . . 8 |- ( ( ( ph /\ n e. NN ) /\ k e. NN ) -> ( 1 / n ) e. RR )
34	32, 33	readdcld 8115	. . . . . . 7 |- ( ( ( ph /\ n e. NN ) /\ k e. NN ) -> ( ( F ` k ) + ( 1 / n ) ) e. RR )
35		ltxrlt 8151	. . . . . . 7 |- ( ( ( F ` n ) e. RR /\ ( ( F ` k ) + ( 1 / n ) ) e. RR ) -> ( ( F ` n ) < ( ( F ` k ) + ( 1 / n ) ) <-> ( F ` n ) <RR ( ( F ` k ) + ( 1 / n ) ) ) )
36	31, 34, 35	syl2anc 411	. . . . . 6 |- ( ( ( ph /\ n e. NN ) /\ k e. NN ) -> ( ( F ` n ) < ( ( F ` k ) + ( 1 / n ) ) <-> ( F ` n ) <RR ( ( F ` k ) + ( 1 / n ) ) ) )
37		nnap0 9078	. . . . . . . . . 10 |- ( n e. NN -> n # 0 )
38	1, 37	syl 14	. . . . . . . . 9 |- ( ( ( ph /\ n e. NN ) /\ k e. NN ) -> n # 0 )
39		caucvgrelemrec 11340	. . . . . . . . 9 |- ( ( n e. RR /\ n # 0 ) -> ( iota_ r e. RR ( n x. r ) = 1 ) = ( 1 / n ) )
40	2, 38, 39	syl2anc 411	. . . . . . . 8 |- ( ( ( ph /\ n e. NN ) /\ k e. NN ) -> ( iota_ r e. RR ( n x. r ) = 1 ) = ( 1 / n ) )
41	40	oveq2d 5970	. . . . . . 7 |- ( ( ( ph /\ n e. NN ) /\ k e. NN ) -> ( ( F ` k ) + ( iota_ r e. RR ( n x. r ) = 1 ) ) = ( ( F ` k ) + ( 1 / n ) ) )
42	41	breq2d 4060	. . . . . 6 |- ( ( ( ph /\ n e. NN ) /\ k e. NN ) -> ( ( F ` n ) <RR ( ( F ` k ) + ( iota_ r e. RR ( n x. r ) = 1 ) ) <-> ( F ` n ) <RR ( ( F ` k ) + ( 1 / n ) ) ) )
43	36, 42	bitr4d 191	. . . . 5 |- ( ( ( ph /\ n e. NN ) /\ k e. NN ) -> ( ( F ` n ) < ( ( F ` k ) + ( 1 / n ) ) <-> ( F ` n ) <RR ( ( F ` k ) + ( iota_ r e. RR ( n x. r ) = 1 ) ) ) )
44	31, 33	readdcld 8115	. . . . . . 7 |- ( ( ( ph /\ n e. NN ) /\ k e. NN ) -> ( ( F ` n ) + ( 1 / n ) ) e. RR )
45		ltxrlt 8151	. . . . . . 7 |- ( ( ( F ` k ) e. RR /\ ( ( F ` n ) + ( 1 / n ) ) e. RR ) -> ( ( F ` k ) < ( ( F ` n ) + ( 1 / n ) ) <-> ( F ` k ) <RR ( ( F ` n ) + ( 1 / n ) ) ) )
46	32, 44, 45	syl2anc 411	. . . . . 6 |- ( ( ( ph /\ n e. NN ) /\ k e. NN ) -> ( ( F ` k ) < ( ( F ` n ) + ( 1 / n ) ) <-> ( F ` k ) <RR ( ( F ` n ) + ( 1 / n ) ) ) )
47	40	oveq2d 5970	. . . . . . 7 |- ( ( ( ph /\ n e. NN ) /\ k e. NN ) -> ( ( F ` n ) + ( iota_ r e. RR ( n x. r ) = 1 ) ) = ( ( F ` n ) + ( 1 / n ) ) )
48	47	breq2d 4060	. . . . . 6 |- ( ( ( ph /\ n e. NN ) /\ k e. NN ) -> ( ( F ` k ) <RR ( ( F ` n ) + ( iota_ r e. RR ( n x. r ) = 1 ) ) <-> ( F ` k ) <RR ( ( F ` n ) + ( 1 / n ) ) ) )
49	46, 48	bitr4d 191	. . . . 5 |- ( ( ( ph /\ n e. NN ) /\ k e. NN ) -> ( ( F ` k ) < ( ( F ` n ) + ( 1 / n ) ) <-> ( F ` k ) <RR ( ( F ` n ) + ( iota_ r e. RR ( n x. r ) = 1 ) ) ) )
50	43, 49	anbi12d 473	. . . 4 |- ( ( ( ph /\ n e. NN ) /\ k e. NN ) -> ( ( ( F ` n ) < ( ( F ` k ) + ( 1 / n ) ) /\ ( F ` k ) < ( ( F ` n ) + ( 1 / n ) ) ) <-> ( ( F ` n ) <RR ( ( F ` k ) + ( iota_ r e. RR ( n x. r ) = 1 ) ) /\ ( F ` k ) <RR ( ( F ` n ) + ( iota_ r e. RR ( n x. r ) = 1 ) ) ) ) )
51	26, 28, 50	3imtr3d 202	. . 3 |- ( ( ( ph /\ n e. NN ) /\ k e. NN ) -> ( n <RR k -> ( ( F ` n ) <RR ( ( F ` k ) + ( iota_ r e. RR ( n x. r ) = 1 ) ) /\ ( F ` k ) <RR ( ( F ` n ) + ( iota_ r e. RR ( n x. r ) = 1 ) ) ) ) )
52	51	ralrimiva 2580	. 2 |- ( ( ph /\ n e. NN ) -> A. k e. NN ( n <RR k -> ( ( F ` n ) <RR ( ( F ` k ) + ( iota_ r e. RR ( n x. r ) = 1 ) ) /\ ( F ` k ) <RR ( ( F ` n ) + ( iota_ r e. RR ( n x. r ) = 1 ) ) ) ) )
53	52	ralrimiva 2580	1 |- ( ph -> A. n e. NN A. k e. NN ( n <RR k -> ( ( F ` n ) <RR ( ( F ` k ) + ( iota_ r e. RR ( n x. r ) = 1 ) ) /\ ( F ` k ) <RR ( ( F ` n ) + ( iota_ r e. RR ( n x. r ) = 1 ) ) ) ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1373   e. wcel 2177   A.wral 2485   class class class wbr 4048   -->wf 5273   ` cfv 5277   iota_crio 5908  (class class class)co 5954   RRcr 7937   0cc0 7938   1c1 7939   + caddc 7941   <RR cltrr 7942   x. cmul 7943   < clt 8120   <_ cle 8121   # cap 8667   / cdiv 8758   NNcn 9049   ZZcz 9385   ZZ>=cuz 9661

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-13 2179  ax-14 2180  ax-ext 2188  ax-sep 4167  ax-pow 4223  ax-pr 4258  ax-un 4485  ax-setind 4590  ax-cnex 8029  ax-resscn 8030  ax-1cn 8031  ax-1re 8032  ax-icn 8033  ax-addcl 8034  ax-addrcl 8035  ax-mulcl 8036  ax-mulrcl 8037  ax-addcom 8038  ax-mulcom 8039  ax-addass 8040  ax-mulass 8041  ax-distr 8042  ax-i2m1 8043  ax-0lt1 8044  ax-1rid 8045  ax-0id 8046  ax-rnegex 8047  ax-precex 8048  ax-cnre 8049  ax-pre-ltirr 8050  ax-pre-ltwlin 8051  ax-pre-lttrn 8052  ax-pre-apti 8053  ax-pre-ltadd 8054  ax-pre-mulgt0 8055  ax-pre-mulext 8056

This theorem depends on definitions:  df-bi 117  df-3or 982  df-3an 983  df-tru 1376  df-fal 1379  df-nf 1485  df-sb 1787  df-eu 2058  df-mo 2059  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ne 2378  df-nel 2473  df-ral 2490  df-rex 2491  df-reu 2492  df-rmo 2493  df-rab 2494  df-v 2775  df-sbc 3001  df-dif 3170  df-un 3172  df-in 3174  df-ss 3181  df-pw 3620  df-sn 3641  df-pr 3642  df-op 3644  df-uni 3854  df-int 3889  df-br 4049  df-opab 4111  df-mpt 4112  df-id 4345  df-po 4348  df-iso 4349  df-xp 4686  df-rel 4687  df-cnv 4688  df-co 4689  df-dm 4690  df-rn 4691  df-res 4692  df-ima 4693  df-iota 5238  df-fun 5279  df-fn 5280  df-f 5281  df-fv 5285  df-riota 5909  df-ov 5957  df-oprab 5958  df-mpo 5959  df-pnf 8122  df-mnf 8123  df-xr 8124  df-ltxr 8125  df-le 8126  df-sub 8258  df-neg 8259  df-reap 8661  df-ap 8668  df-div 8759  df-inn 9050  df-z 9386  df-uz 9662

This theorem is referenced by:  caucvgre  11342