Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fmul01lt1lem2 Structured version   Visualization version   GIF version

Theorem fmul01lt1lem2 44896
Description: Given a finite multiplication of values betweeen 0 and 1, a value ๐ธ larger than any multiplicand, is larger than the whole multiplication. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
Hypotheses
Ref Expression
fmul01lt1lem2.1 โ„ฒ๐‘–๐ต
fmul01lt1lem2.2 โ„ฒ๐‘–๐œ‘
fmul01lt1lem2.3 ๐ด = seq๐ฟ( ยท , ๐ต)
fmul01lt1lem2.4 (๐œ‘ โ†’ ๐ฟ โˆˆ โ„ค)
fmul01lt1lem2.5 (๐œ‘ โ†’ ๐‘€ โˆˆ (โ„คโ‰ฅโ€˜๐ฟ))
fmul01lt1lem2.6 ((๐œ‘ โˆง ๐‘– โˆˆ (๐ฟ...๐‘€)) โ†’ (๐ตโ€˜๐‘–) โˆˆ โ„)
fmul01lt1lem2.7 ((๐œ‘ โˆง ๐‘– โˆˆ (๐ฟ...๐‘€)) โ†’ 0 โ‰ค (๐ตโ€˜๐‘–))
fmul01lt1lem2.8 ((๐œ‘ โˆง ๐‘– โˆˆ (๐ฟ...๐‘€)) โ†’ (๐ตโ€˜๐‘–) โ‰ค 1)
fmul01lt1lem2.9 (๐œ‘ โ†’ ๐ธ โˆˆ โ„+)
fmul01lt1lem2.10 (๐œ‘ โ†’ ๐ฝ โˆˆ (๐ฟ...๐‘€))
fmul01lt1lem2.11 (๐œ‘ โ†’ (๐ตโ€˜๐ฝ) < ๐ธ)
Assertion
Ref Expression
fmul01lt1lem2 (๐œ‘ โ†’ (๐ดโ€˜๐‘€) < ๐ธ)
Distinct variable groups:   ๐‘–,๐ฝ   ๐‘–,๐ฟ   ๐‘–,๐‘€
Allowed substitution hints:   ๐œ‘(๐‘–)   ๐ด(๐‘–)   ๐ต(๐‘–)   ๐ธ(๐‘–)

Proof of Theorem fmul01lt1lem2
Dummy variables ๐‘Ž ๐‘ ๐‘ ๐‘— are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fmul01lt1lem2.1 . . 3 โ„ฒ๐‘–๐ต
2 fmul01lt1lem2.2 . . . 4 โ„ฒ๐‘–๐œ‘
3 nfv 1910 . . . 4 โ„ฒ๐‘– ๐ฝ = ๐ฟ
42, 3nfan 1895 . . 3 โ„ฒ๐‘–(๐œ‘ โˆง ๐ฝ = ๐ฟ)
5 fmul01lt1lem2.3 . . 3 ๐ด = seq๐ฟ( ยท , ๐ต)
6 fmul01lt1lem2.4 . . . 4 (๐œ‘ โ†’ ๐ฟ โˆˆ โ„ค)
76adantr 480 . . 3 ((๐œ‘ โˆง ๐ฝ = ๐ฟ) โ†’ ๐ฟ โˆˆ โ„ค)
8 fmul01lt1lem2.5 . . . 4 (๐œ‘ โ†’ ๐‘€ โˆˆ (โ„คโ‰ฅโ€˜๐ฟ))
98adantr 480 . . 3 ((๐œ‘ โˆง ๐ฝ = ๐ฟ) โ†’ ๐‘€ โˆˆ (โ„คโ‰ฅโ€˜๐ฟ))
10 fmul01lt1lem2.6 . . . 4 ((๐œ‘ โˆง ๐‘– โˆˆ (๐ฟ...๐‘€)) โ†’ (๐ตโ€˜๐‘–) โˆˆ โ„)
1110adantlr 714 . . 3 (((๐œ‘ โˆง ๐ฝ = ๐ฟ) โˆง ๐‘– โˆˆ (๐ฟ...๐‘€)) โ†’ (๐ตโ€˜๐‘–) โˆˆ โ„)
12 fmul01lt1lem2.7 . . . 4 ((๐œ‘ โˆง ๐‘– โˆˆ (๐ฟ...๐‘€)) โ†’ 0 โ‰ค (๐ตโ€˜๐‘–))
1312adantlr 714 . . 3 (((๐œ‘ โˆง ๐ฝ = ๐ฟ) โˆง ๐‘– โˆˆ (๐ฟ...๐‘€)) โ†’ 0 โ‰ค (๐ตโ€˜๐‘–))
14 fmul01lt1lem2.8 . . . 4 ((๐œ‘ โˆง ๐‘– โˆˆ (๐ฟ...๐‘€)) โ†’ (๐ตโ€˜๐‘–) โ‰ค 1)
1514adantlr 714 . . 3 (((๐œ‘ โˆง ๐ฝ = ๐ฟ) โˆง ๐‘– โˆˆ (๐ฟ...๐‘€)) โ†’ (๐ตโ€˜๐‘–) โ‰ค 1)
16 fmul01lt1lem2.9 . . . 4 (๐œ‘ โ†’ ๐ธ โˆˆ โ„+)
1716adantr 480 . . 3 ((๐œ‘ โˆง ๐ฝ = ๐ฟ) โ†’ ๐ธ โˆˆ โ„+)
18 simpr 484 . . . . 5 ((๐œ‘ โˆง ๐ฝ = ๐ฟ) โ†’ ๐ฝ = ๐ฟ)
1918fveq2d 6895 . . . 4 ((๐œ‘ โˆง ๐ฝ = ๐ฟ) โ†’ (๐ตโ€˜๐ฝ) = (๐ตโ€˜๐ฟ))
20 fmul01lt1lem2.11 . . . . 5 (๐œ‘ โ†’ (๐ตโ€˜๐ฝ) < ๐ธ)
2120adantr 480 . . . 4 ((๐œ‘ โˆง ๐ฝ = ๐ฟ) โ†’ (๐ตโ€˜๐ฝ) < ๐ธ)
2219, 21eqbrtrrd 5166 . . 3 ((๐œ‘ โˆง ๐ฝ = ๐ฟ) โ†’ (๐ตโ€˜๐ฟ) < ๐ธ)
231, 4, 5, 7, 9, 11, 13, 15, 17, 22fmul01lt1lem1 44895 . 2 ((๐œ‘ โˆง ๐ฝ = ๐ฟ) โ†’ (๐ดโ€˜๐‘€) < ๐ธ)
245fveq1i 6892 . . 3 (๐ดโ€˜๐‘€) = (seq๐ฟ( ยท , ๐ต)โ€˜๐‘€)
25 nfv 1910 . . . . . . . . 9 โ„ฒ๐‘– ๐‘Ž โˆˆ (๐ฟ...๐‘€)
262, 25nfan 1895 . . . . . . . 8 โ„ฒ๐‘–(๐œ‘ โˆง ๐‘Ž โˆˆ (๐ฟ...๐‘€))
27 nfcv 2898 . . . . . . . . . 10 โ„ฒ๐‘–๐‘Ž
281, 27nffv 6901 . . . . . . . . 9 โ„ฒ๐‘–(๐ตโ€˜๐‘Ž)
2928nfel1 2914 . . . . . . . 8 โ„ฒ๐‘–(๐ตโ€˜๐‘Ž) โˆˆ โ„
3026, 29nfim 1892 . . . . . . 7 โ„ฒ๐‘–((๐œ‘ โˆง ๐‘Ž โˆˆ (๐ฟ...๐‘€)) โ†’ (๐ตโ€˜๐‘Ž) โˆˆ โ„)
31 eleq1w 2811 . . . . . . . . 9 (๐‘– = ๐‘Ž โ†’ (๐‘– โˆˆ (๐ฟ...๐‘€) โ†” ๐‘Ž โˆˆ (๐ฟ...๐‘€)))
3231anbi2d 628 . . . . . . . 8 (๐‘– = ๐‘Ž โ†’ ((๐œ‘ โˆง ๐‘– โˆˆ (๐ฟ...๐‘€)) โ†” (๐œ‘ โˆง ๐‘Ž โˆˆ (๐ฟ...๐‘€))))
33 fveq2 6891 . . . . . . . . 9 (๐‘– = ๐‘Ž โ†’ (๐ตโ€˜๐‘–) = (๐ตโ€˜๐‘Ž))
3433eleq1d 2813 . . . . . . . 8 (๐‘– = ๐‘Ž โ†’ ((๐ตโ€˜๐‘–) โˆˆ โ„ โ†” (๐ตโ€˜๐‘Ž) โˆˆ โ„))
3532, 34imbi12d 344 . . . . . . 7 (๐‘– = ๐‘Ž โ†’ (((๐œ‘ โˆง ๐‘– โˆˆ (๐ฟ...๐‘€)) โ†’ (๐ตโ€˜๐‘–) โˆˆ โ„) โ†” ((๐œ‘ โˆง ๐‘Ž โˆˆ (๐ฟ...๐‘€)) โ†’ (๐ตโ€˜๐‘Ž) โˆˆ โ„)))
3630, 35, 10chvarfv 2226 . . . . . 6 ((๐œ‘ โˆง ๐‘Ž โˆˆ (๐ฟ...๐‘€)) โ†’ (๐ตโ€˜๐‘Ž) โˆˆ โ„)
37 remulcl 11215 . . . . . . 7 ((๐‘Ž โˆˆ โ„ โˆง ๐‘— โˆˆ โ„) โ†’ (๐‘Ž ยท ๐‘—) โˆˆ โ„)
3837adantl 481 . . . . . 6 ((๐œ‘ โˆง (๐‘Ž โˆˆ โ„ โˆง ๐‘— โˆˆ โ„)) โ†’ (๐‘Ž ยท ๐‘—) โˆˆ โ„)
398, 36, 38seqcl 14011 . . . . 5 (๐œ‘ โ†’ (seq๐ฟ( ยท , ๐ต)โ€˜๐‘€) โˆˆ โ„)
4039adantr 480 . . . 4 ((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โ†’ (seq๐ฟ( ยท , ๐ต)โ€˜๐‘€) โˆˆ โ„)
41 fmul01lt1lem2.10 . . . . . . 7 (๐œ‘ โ†’ ๐ฝ โˆˆ (๐ฟ...๐‘€))
42 elfzuz3 13522 . . . . . . 7 (๐ฝ โˆˆ (๐ฟ...๐‘€) โ†’ ๐‘€ โˆˆ (โ„คโ‰ฅโ€˜๐ฝ))
4341, 42syl 17 . . . . . 6 (๐œ‘ โ†’ ๐‘€ โˆˆ (โ„คโ‰ฅโ€˜๐ฝ))
44 nfv 1910 . . . . . . . . 9 โ„ฒ๐‘– ๐‘Ž โˆˆ (๐ฝ...๐‘€)
452, 44nfan 1895 . . . . . . . 8 โ„ฒ๐‘–(๐œ‘ โˆง ๐‘Ž โˆˆ (๐ฝ...๐‘€))
4645, 29nfim 1892 . . . . . . 7 โ„ฒ๐‘–((๐œ‘ โˆง ๐‘Ž โˆˆ (๐ฝ...๐‘€)) โ†’ (๐ตโ€˜๐‘Ž) โˆˆ โ„)
47 eleq1w 2811 . . . . . . . . 9 (๐‘– = ๐‘Ž โ†’ (๐‘– โˆˆ (๐ฝ...๐‘€) โ†” ๐‘Ž โˆˆ (๐ฝ...๐‘€)))
4847anbi2d 628 . . . . . . . 8 (๐‘– = ๐‘Ž โ†’ ((๐œ‘ โˆง ๐‘– โˆˆ (๐ฝ...๐‘€)) โ†” (๐œ‘ โˆง ๐‘Ž โˆˆ (๐ฝ...๐‘€))))
4948, 34imbi12d 344 . . . . . . 7 (๐‘– = ๐‘Ž โ†’ (((๐œ‘ โˆง ๐‘– โˆˆ (๐ฝ...๐‘€)) โ†’ (๐ตโ€˜๐‘–) โˆˆ โ„) โ†” ((๐œ‘ โˆง ๐‘Ž โˆˆ (๐ฝ...๐‘€)) โ†’ (๐ตโ€˜๐‘Ž) โˆˆ โ„)))
506adantr 480 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘– โˆˆ (๐ฝ...๐‘€)) โ†’ ๐ฟ โˆˆ โ„ค)
51 eluzelz 12854 . . . . . . . . . . 11 (๐‘€ โˆˆ (โ„คโ‰ฅโ€˜๐ฟ) โ†’ ๐‘€ โˆˆ โ„ค)
528, 51syl 17 . . . . . . . . . 10 (๐œ‘ โ†’ ๐‘€ โˆˆ โ„ค)
5352adantr 480 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘– โˆˆ (๐ฝ...๐‘€)) โ†’ ๐‘€ โˆˆ โ„ค)
54 elfzelz 13525 . . . . . . . . . 10 (๐‘– โˆˆ (๐ฝ...๐‘€) โ†’ ๐‘– โˆˆ โ„ค)
5554adantl 481 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘– โˆˆ (๐ฝ...๐‘€)) โ†’ ๐‘– โˆˆ โ„ค)
566zred 12688 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐ฟ โˆˆ โ„)
5756adantr 480 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘– โˆˆ (๐ฝ...๐‘€)) โ†’ ๐ฟ โˆˆ โ„)
58 elfzelz 13525 . . . . . . . . . . . . 13 (๐ฝ โˆˆ (๐ฟ...๐‘€) โ†’ ๐ฝ โˆˆ โ„ค)
5941, 58syl 17 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐ฝ โˆˆ โ„ค)
6059zred 12688 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐ฝ โˆˆ โ„)
6160adantr 480 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘– โˆˆ (๐ฝ...๐‘€)) โ†’ ๐ฝ โˆˆ โ„)
6254zred 12688 . . . . . . . . . . 11 (๐‘– โˆˆ (๐ฝ...๐‘€) โ†’ ๐‘– โˆˆ โ„)
6362adantl 481 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘– โˆˆ (๐ฝ...๐‘€)) โ†’ ๐‘– โˆˆ โ„)
64 elfzle1 13528 . . . . . . . . . . . 12 (๐ฝ โˆˆ (๐ฟ...๐‘€) โ†’ ๐ฟ โ‰ค ๐ฝ)
6541, 64syl 17 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐ฟ โ‰ค ๐ฝ)
6665adantr 480 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘– โˆˆ (๐ฝ...๐‘€)) โ†’ ๐ฟ โ‰ค ๐ฝ)
67 elfzle1 13528 . . . . . . . . . . 11 (๐‘– โˆˆ (๐ฝ...๐‘€) โ†’ ๐ฝ โ‰ค ๐‘–)
6867adantl 481 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘– โˆˆ (๐ฝ...๐‘€)) โ†’ ๐ฝ โ‰ค ๐‘–)
6957, 61, 63, 66, 68letrd 11393 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘– โˆˆ (๐ฝ...๐‘€)) โ†’ ๐ฟ โ‰ค ๐‘–)
70 elfzle2 13529 . . . . . . . . . 10 (๐‘– โˆˆ (๐ฝ...๐‘€) โ†’ ๐‘– โ‰ค ๐‘€)
7170adantl 481 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘– โˆˆ (๐ฝ...๐‘€)) โ†’ ๐‘– โ‰ค ๐‘€)
7250, 53, 55, 69, 71elfzd 13516 . . . . . . . 8 ((๐œ‘ โˆง ๐‘– โˆˆ (๐ฝ...๐‘€)) โ†’ ๐‘– โˆˆ (๐ฟ...๐‘€))
7372, 10syldan 590 . . . . . . 7 ((๐œ‘ โˆง ๐‘– โˆˆ (๐ฝ...๐‘€)) โ†’ (๐ตโ€˜๐‘–) โˆˆ โ„)
7446, 49, 73chvarfv 2226 . . . . . 6 ((๐œ‘ โˆง ๐‘Ž โˆˆ (๐ฝ...๐‘€)) โ†’ (๐ตโ€˜๐‘Ž) โˆˆ โ„)
7543, 74, 38seqcl 14011 . . . . 5 (๐œ‘ โ†’ (seq๐ฝ( ยท , ๐ต)โ€˜๐‘€) โˆˆ โ„)
7675adantr 480 . . . 4 ((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โ†’ (seq๐ฝ( ยท , ๐ต)โ€˜๐‘€) โˆˆ โ„)
7716rpred 13040 . . . . 5 (๐œ‘ โ†’ ๐ธ โˆˆ โ„)
7877adantr 480 . . . 4 ((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โ†’ ๐ธ โˆˆ โ„)
79 remulcl 11215 . . . . . . . . 9 ((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โ†’ (๐‘Ž ยท ๐‘) โˆˆ โ„)
8079adantl 481 . . . . . . . 8 (((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โˆง (๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„)) โ†’ (๐‘Ž ยท ๐‘) โˆˆ โ„)
81 simp1 1134 . . . . . . . . . . 11 ((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โ†’ ๐‘Ž โˆˆ โ„)
8281recnd 11264 . . . . . . . . . 10 ((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โ†’ ๐‘Ž โˆˆ โ„‚)
83 simp2 1135 . . . . . . . . . . 11 ((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โ†’ ๐‘ โˆˆ โ„)
8483recnd 11264 . . . . . . . . . 10 ((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โ†’ ๐‘ โˆˆ โ„‚)
85 simp3 1136 . . . . . . . . . . 11 ((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โ†’ ๐‘ โˆˆ โ„)
8685recnd 11264 . . . . . . . . . 10 ((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โ†’ ๐‘ โˆˆ โ„‚)
8782, 84, 86mulassd 11259 . . . . . . . . 9 ((๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โ†’ ((๐‘Ž ยท ๐‘) ยท ๐‘) = (๐‘Ž ยท (๐‘ ยท ๐‘)))
8887adantl 481 . . . . . . . 8 (((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โˆง (๐‘Ž โˆˆ โ„ โˆง ๐‘ โˆˆ โ„ โˆง ๐‘ โˆˆ โ„)) โ†’ ((๐‘Ž ยท ๐‘) ยท ๐‘) = (๐‘Ž ยท (๐‘ ยท ๐‘)))
8959zcnd 12689 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐ฝ โˆˆ โ„‚)
90 1cnd 11231 . . . . . . . . . . . 12 (๐œ‘ โ†’ 1 โˆˆ โ„‚)
9189, 90npcand 11597 . . . . . . . . . . 11 (๐œ‘ โ†’ ((๐ฝ โˆ’ 1) + 1) = ๐ฝ)
9291fveq2d 6895 . . . . . . . . . 10 (๐œ‘ โ†’ (โ„คโ‰ฅโ€˜((๐ฝ โˆ’ 1) + 1)) = (โ„คโ‰ฅโ€˜๐ฝ))
9343, 92eleqtrrd 2831 . . . . . . . . 9 (๐œ‘ โ†’ ๐‘€ โˆˆ (โ„คโ‰ฅโ€˜((๐ฝ โˆ’ 1) + 1)))
9493adantr 480 . . . . . . . 8 ((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โ†’ ๐‘€ โˆˆ (โ„คโ‰ฅโ€˜((๐ฝ โˆ’ 1) + 1)))
956adantr 480 . . . . . . . . 9 ((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โ†’ ๐ฟ โˆˆ โ„ค)
9659adantr 480 . . . . . . . . . 10 ((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โ†’ ๐ฝ โˆˆ โ„ค)
97 1zzd 12615 . . . . . . . . . 10 ((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โ†’ 1 โˆˆ โ„ค)
9896, 97zsubcld 12693 . . . . . . . . 9 ((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โ†’ (๐ฝ โˆ’ 1) โˆˆ โ„ค)
99 simpr 484 . . . . . . . . . . . 12 ((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โ†’ ยฌ ๐ฝ = ๐ฟ)
100 eqcom 2734 . . . . . . . . . . . 12 (๐ฝ = ๐ฟ โ†” ๐ฟ = ๐ฝ)
10199, 100sylnib 328 . . . . . . . . . . 11 ((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โ†’ ยฌ ๐ฟ = ๐ฝ)
10256, 60leloed 11379 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐ฟ โ‰ค ๐ฝ โ†” (๐ฟ < ๐ฝ โˆจ ๐ฟ = ๐ฝ)))
10365, 102mpbid 231 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐ฟ < ๐ฝ โˆจ ๐ฟ = ๐ฝ))
104103adantr 480 . . . . . . . . . . 11 ((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โ†’ (๐ฟ < ๐ฝ โˆจ ๐ฟ = ๐ฝ))
105 orel2 889 . . . . . . . . . . 11 (ยฌ ๐ฟ = ๐ฝ โ†’ ((๐ฟ < ๐ฝ โˆจ ๐ฟ = ๐ฝ) โ†’ ๐ฟ < ๐ฝ))
106101, 104, 105sylc 65 . . . . . . . . . 10 ((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โ†’ ๐ฟ < ๐ฝ)
107 zltlem1 12637 . . . . . . . . . . . 12 ((๐ฟ โˆˆ โ„ค โˆง ๐ฝ โˆˆ โ„ค) โ†’ (๐ฟ < ๐ฝ โ†” ๐ฟ โ‰ค (๐ฝ โˆ’ 1)))
1086, 59, 107syl2anc 583 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐ฟ < ๐ฝ โ†” ๐ฟ โ‰ค (๐ฝ โˆ’ 1)))
109108adantr 480 . . . . . . . . . 10 ((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โ†’ (๐ฟ < ๐ฝ โ†” ๐ฟ โ‰ค (๐ฝ โˆ’ 1)))
110106, 109mpbid 231 . . . . . . . . 9 ((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โ†’ ๐ฟ โ‰ค (๐ฝ โˆ’ 1))
111 eluz2 12850 . . . . . . . . 9 ((๐ฝ โˆ’ 1) โˆˆ (โ„คโ‰ฅโ€˜๐ฟ) โ†” (๐ฟ โˆˆ โ„ค โˆง (๐ฝ โˆ’ 1) โˆˆ โ„ค โˆง ๐ฟ โ‰ค (๐ฝ โˆ’ 1)))
11295, 98, 110, 111syl3anbrc 1341 . . . . . . . 8 ((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โ†’ (๐ฝ โˆ’ 1) โˆˆ (โ„คโ‰ฅโ€˜๐ฟ))
113 nfv 1910 . . . . . . . . . . . 12 โ„ฒ๐‘– ยฌ ๐ฝ = ๐ฟ
1142, 113nfan 1895 . . . . . . . . . . 11 โ„ฒ๐‘–(๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ)
115114, 25nfan 1895 . . . . . . . . . 10 โ„ฒ๐‘–((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โˆง ๐‘Ž โˆˆ (๐ฟ...๐‘€))
116115, 29nfim 1892 . . . . . . . . 9 โ„ฒ๐‘–(((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โˆง ๐‘Ž โˆˆ (๐ฟ...๐‘€)) โ†’ (๐ตโ€˜๐‘Ž) โˆˆ โ„)
11731anbi2d 628 . . . . . . . . . 10 (๐‘– = ๐‘Ž โ†’ (((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โˆง ๐‘– โˆˆ (๐ฟ...๐‘€)) โ†” ((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โˆง ๐‘Ž โˆˆ (๐ฟ...๐‘€))))
118117, 34imbi12d 344 . . . . . . . . 9 (๐‘– = ๐‘Ž โ†’ ((((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โˆง ๐‘– โˆˆ (๐ฟ...๐‘€)) โ†’ (๐ตโ€˜๐‘–) โˆˆ โ„) โ†” (((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โˆง ๐‘Ž โˆˆ (๐ฟ...๐‘€)) โ†’ (๐ตโ€˜๐‘Ž) โˆˆ โ„)))
11910adantlr 714 . . . . . . . . 9 (((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โˆง ๐‘– โˆˆ (๐ฟ...๐‘€)) โ†’ (๐ตโ€˜๐‘–) โˆˆ โ„)
120116, 118, 119chvarfv 2226 . . . . . . . 8 (((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โˆง ๐‘Ž โˆˆ (๐ฟ...๐‘€)) โ†’ (๐ตโ€˜๐‘Ž) โˆˆ โ„)
12180, 88, 94, 112, 120seqsplit 14024 . . . . . . 7 ((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โ†’ (seq๐ฟ( ยท , ๐ต)โ€˜๐‘€) = ((seq๐ฟ( ยท , ๐ต)โ€˜(๐ฝ โˆ’ 1)) ยท (seq((๐ฝ โˆ’ 1) + 1)( ยท , ๐ต)โ€˜๐‘€)))
12291adantr 480 . . . . . . . . . 10 ((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โ†’ ((๐ฝ โˆ’ 1) + 1) = ๐ฝ)
123122seqeq1d 13996 . . . . . . . . 9 ((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โ†’ seq((๐ฝ โˆ’ 1) + 1)( ยท , ๐ต) = seq๐ฝ( ยท , ๐ต))
124123fveq1d 6893 . . . . . . . 8 ((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โ†’ (seq((๐ฝ โˆ’ 1) + 1)( ยท , ๐ต)โ€˜๐‘€) = (seq๐ฝ( ยท , ๐ต)โ€˜๐‘€))
125124oveq2d 7430 . . . . . . 7 ((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โ†’ ((seq๐ฟ( ยท , ๐ต)โ€˜(๐ฝ โˆ’ 1)) ยท (seq((๐ฝ โˆ’ 1) + 1)( ยท , ๐ต)โ€˜๐‘€)) = ((seq๐ฟ( ยท , ๐ต)โ€˜(๐ฝ โˆ’ 1)) ยท (seq๐ฝ( ยท , ๐ต)โ€˜๐‘€)))
126121, 125eqtrd 2767 . . . . . 6 ((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โ†’ (seq๐ฟ( ยท , ๐ต)โ€˜๐‘€) = ((seq๐ฟ( ยท , ๐ต)โ€˜(๐ฝ โˆ’ 1)) ยท (seq๐ฝ( ยท , ๐ต)โ€˜๐‘€)))
127 nfv 1910 . . . . . . . . . . 11 โ„ฒ๐‘– ๐‘Ž โˆˆ (๐ฟ...(๐ฝ โˆ’ 1))
128114, 127nfan 1895 . . . . . . . . . 10 โ„ฒ๐‘–((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โˆง ๐‘Ž โˆˆ (๐ฟ...(๐ฝ โˆ’ 1)))
129128, 29nfim 1892 . . . . . . . . 9 โ„ฒ๐‘–(((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โˆง ๐‘Ž โˆˆ (๐ฟ...(๐ฝ โˆ’ 1))) โ†’ (๐ตโ€˜๐‘Ž) โˆˆ โ„)
130 eleq1w 2811 . . . . . . . . . . 11 (๐‘– = ๐‘Ž โ†’ (๐‘– โˆˆ (๐ฟ...(๐ฝ โˆ’ 1)) โ†” ๐‘Ž โˆˆ (๐ฟ...(๐ฝ โˆ’ 1))))
131130anbi2d 628 . . . . . . . . . 10 (๐‘– = ๐‘Ž โ†’ (((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โˆง ๐‘– โˆˆ (๐ฟ...(๐ฝ โˆ’ 1))) โ†” ((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โˆง ๐‘Ž โˆˆ (๐ฟ...(๐ฝ โˆ’ 1)))))
132131, 34imbi12d 344 . . . . . . . . 9 (๐‘– = ๐‘Ž โ†’ ((((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โˆง ๐‘– โˆˆ (๐ฟ...(๐ฝ โˆ’ 1))) โ†’ (๐ตโ€˜๐‘–) โˆˆ โ„) โ†” (((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โˆง ๐‘Ž โˆˆ (๐ฟ...(๐ฝ โˆ’ 1))) โ†’ (๐ตโ€˜๐‘Ž) โˆˆ โ„)))
1336adantr 480 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘– โˆˆ (๐ฟ...(๐ฝ โˆ’ 1))) โ†’ ๐ฟ โˆˆ โ„ค)
13452adantr 480 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘– โˆˆ (๐ฟ...(๐ฝ โˆ’ 1))) โ†’ ๐‘€ โˆˆ โ„ค)
135 elfzelz 13525 . . . . . . . . . . . . 13 (๐‘– โˆˆ (๐ฟ...(๐ฝ โˆ’ 1)) โ†’ ๐‘– โˆˆ โ„ค)
136135adantl 481 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘– โˆˆ (๐ฟ...(๐ฝ โˆ’ 1))) โ†’ ๐‘– โˆˆ โ„ค)
137 elfzle1 13528 . . . . . . . . . . . . 13 (๐‘– โˆˆ (๐ฟ...(๐ฝ โˆ’ 1)) โ†’ ๐ฟ โ‰ค ๐‘–)
138137adantl 481 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘– โˆˆ (๐ฟ...(๐ฝ โˆ’ 1))) โ†’ ๐ฟ โ‰ค ๐‘–)
139135zred 12688 . . . . . . . . . . . . . 14 (๐‘– โˆˆ (๐ฟ...(๐ฝ โˆ’ 1)) โ†’ ๐‘– โˆˆ โ„)
140139adantl 481 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘– โˆˆ (๐ฟ...(๐ฝ โˆ’ 1))) โ†’ ๐‘– โˆˆ โ„)
14160adantr 480 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘– โˆˆ (๐ฟ...(๐ฝ โˆ’ 1))) โ†’ ๐ฝ โˆˆ โ„)
14252zred 12688 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ๐‘€ โˆˆ โ„)
143142adantr 480 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘– โˆˆ (๐ฟ...(๐ฝ โˆ’ 1))) โ†’ ๐‘€ โˆˆ โ„)
144 1red 11237 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ 1 โˆˆ โ„)
14560, 144resubcld 11664 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (๐ฝ โˆ’ 1) โˆˆ โ„)
146145adantr 480 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘– โˆˆ (๐ฟ...(๐ฝ โˆ’ 1))) โ†’ (๐ฝ โˆ’ 1) โˆˆ โ„)
147 elfzle2 13529 . . . . . . . . . . . . . . 15 (๐‘– โˆˆ (๐ฟ...(๐ฝ โˆ’ 1)) โ†’ ๐‘– โ‰ค (๐ฝ โˆ’ 1))
148147adantl 481 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘– โˆˆ (๐ฟ...(๐ฝ โˆ’ 1))) โ†’ ๐‘– โ‰ค (๐ฝ โˆ’ 1))
14960lem1d 12169 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (๐ฝ โˆ’ 1) โ‰ค ๐ฝ)
150149adantr 480 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘– โˆˆ (๐ฟ...(๐ฝ โˆ’ 1))) โ†’ (๐ฝ โˆ’ 1) โ‰ค ๐ฝ)
151140, 146, 141, 148, 150letrd 11393 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘– โˆˆ (๐ฟ...(๐ฝ โˆ’ 1))) โ†’ ๐‘– โ‰ค ๐ฝ)
152 elfzle2 13529 . . . . . . . . . . . . . . 15 (๐ฝ โˆˆ (๐ฟ...๐‘€) โ†’ ๐ฝ โ‰ค ๐‘€)
15341, 152syl 17 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ๐ฝ โ‰ค ๐‘€)
154153adantr 480 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘– โˆˆ (๐ฟ...(๐ฝ โˆ’ 1))) โ†’ ๐ฝ โ‰ค ๐‘€)
155140, 141, 143, 151, 154letrd 11393 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘– โˆˆ (๐ฟ...(๐ฝ โˆ’ 1))) โ†’ ๐‘– โ‰ค ๐‘€)
156133, 134, 136, 138, 155elfzd 13516 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘– โˆˆ (๐ฟ...(๐ฝ โˆ’ 1))) โ†’ ๐‘– โˆˆ (๐ฟ...๐‘€))
157156, 10syldan 590 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘– โˆˆ (๐ฟ...(๐ฝ โˆ’ 1))) โ†’ (๐ตโ€˜๐‘–) โˆˆ โ„)
158157adantlr 714 . . . . . . . . 9 (((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โˆง ๐‘– โˆˆ (๐ฟ...(๐ฝ โˆ’ 1))) โ†’ (๐ตโ€˜๐‘–) โˆˆ โ„)
159129, 132, 158chvarfv 2226 . . . . . . . 8 (((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โˆง ๐‘Ž โˆˆ (๐ฟ...(๐ฝ โˆ’ 1))) โ†’ (๐ตโ€˜๐‘Ž) โˆˆ โ„)
16037adantl 481 . . . . . . . 8 (((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โˆง (๐‘Ž โˆˆ โ„ โˆง ๐‘— โˆˆ โ„)) โ†’ (๐‘Ž ยท ๐‘—) โˆˆ โ„)
161112, 159, 160seqcl 14011 . . . . . . 7 ((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โ†’ (seq๐ฟ( ยท , ๐ต)โ€˜(๐ฝ โˆ’ 1)) โˆˆ โ„)
162 1red 11237 . . . . . . 7 ((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โ†’ 1 โˆˆ โ„)
163 eqid 2727 . . . . . . . . 9 seq๐ฝ( ยท , ๐ต) = seq๐ฝ( ยท , ๐ต)
16443adantr 480 . . . . . . . . 9 ((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โ†’ ๐‘€ โˆˆ (โ„คโ‰ฅโ€˜๐ฝ))
165 eluzfz2 13533 . . . . . . . . . . 11 (๐‘€ โˆˆ (โ„คโ‰ฅโ€˜๐ฝ) โ†’ ๐‘€ โˆˆ (๐ฝ...๐‘€))
16643, 165syl 17 . . . . . . . . . 10 (๐œ‘ โ†’ ๐‘€ โˆˆ (๐ฝ...๐‘€))
167166adantr 480 . . . . . . . . 9 ((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โ†’ ๐‘€ โˆˆ (๐ฝ...๐‘€))
16873adantlr 714 . . . . . . . . 9 (((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โˆง ๐‘– โˆˆ (๐ฝ...๐‘€)) โ†’ (๐ตโ€˜๐‘–) โˆˆ โ„)
16972, 12syldan 590 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘– โˆˆ (๐ฝ...๐‘€)) โ†’ 0 โ‰ค (๐ตโ€˜๐‘–))
170169adantlr 714 . . . . . . . . 9 (((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โˆง ๐‘– โˆˆ (๐ฝ...๐‘€)) โ†’ 0 โ‰ค (๐ตโ€˜๐‘–))
17172, 14syldan 590 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘– โˆˆ (๐ฝ...๐‘€)) โ†’ (๐ตโ€˜๐‘–) โ‰ค 1)
172171adantlr 714 . . . . . . . . 9 (((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โˆง ๐‘– โˆˆ (๐ฝ...๐‘€)) โ†’ (๐ตโ€˜๐‘–) โ‰ค 1)
1731, 114, 163, 96, 164, 167, 168, 170, 172fmul01 44891 . . . . . . . 8 ((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โ†’ (0 โ‰ค (seq๐ฝ( ยท , ๐ต)โ€˜๐‘€) โˆง (seq๐ฝ( ยท , ๐ต)โ€˜๐‘€) โ‰ค 1))
174173simpld 494 . . . . . . 7 ((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โ†’ 0 โ‰ค (seq๐ฝ( ยท , ๐ต)โ€˜๐‘€))
175 eqid 2727 . . . . . . . . 9 seq๐ฟ( ยท , ๐ต) = seq๐ฟ( ยท , ๐ต)
1768adantr 480 . . . . . . . . 9 ((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โ†’ ๐‘€ โˆˆ (โ„คโ‰ฅโ€˜๐ฟ))
177 1zzd 12615 . . . . . . . . . . . . 13 (๐œ‘ โ†’ 1 โˆˆ โ„ค)
17859, 177zsubcld 12693 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐ฝ โˆ’ 1) โˆˆ โ„ค)
1796, 52, 1783jca 1126 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐ฟ โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„ค โˆง (๐ฝ โˆ’ 1) โˆˆ โ„ค))
180179adantr 480 . . . . . . . . . 10 ((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โ†’ (๐ฟ โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„ค โˆง (๐ฝ โˆ’ 1) โˆˆ โ„ค))
181145, 60, 1423jca 1126 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((๐ฝ โˆ’ 1) โˆˆ โ„ โˆง ๐ฝ โˆˆ โ„ โˆง ๐‘€ โˆˆ โ„))
182181adantr 480 . . . . . . . . . . . 12 ((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โ†’ ((๐ฝ โˆ’ 1) โˆˆ โ„ โˆง ๐ฝ โˆˆ โ„ โˆง ๐‘€ โˆˆ โ„))
18360adantr 480 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โ†’ ๐ฝ โˆˆ โ„)
184183lem1d 12169 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โ†’ (๐ฝ โˆ’ 1) โ‰ค ๐ฝ)
185153adantr 480 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โ†’ ๐ฝ โ‰ค ๐‘€)
186184, 185jca 511 . . . . . . . . . . . 12 ((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โ†’ ((๐ฝ โˆ’ 1) โ‰ค ๐ฝ โˆง ๐ฝ โ‰ค ๐‘€))
187 letr 11330 . . . . . . . . . . . 12 (((๐ฝ โˆ’ 1) โˆˆ โ„ โˆง ๐ฝ โˆˆ โ„ โˆง ๐‘€ โˆˆ โ„) โ†’ (((๐ฝ โˆ’ 1) โ‰ค ๐ฝ โˆง ๐ฝ โ‰ค ๐‘€) โ†’ (๐ฝ โˆ’ 1) โ‰ค ๐‘€))
188182, 186, 187sylc 65 . . . . . . . . . . 11 ((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โ†’ (๐ฝ โˆ’ 1) โ‰ค ๐‘€)
189110, 188jca 511 . . . . . . . . . 10 ((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โ†’ (๐ฟ โ‰ค (๐ฝ โˆ’ 1) โˆง (๐ฝ โˆ’ 1) โ‰ค ๐‘€))
190 elfz2 13515 . . . . . . . . . 10 ((๐ฝ โˆ’ 1) โˆˆ (๐ฟ...๐‘€) โ†” ((๐ฟ โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„ค โˆง (๐ฝ โˆ’ 1) โˆˆ โ„ค) โˆง (๐ฟ โ‰ค (๐ฝ โˆ’ 1) โˆง (๐ฝ โˆ’ 1) โ‰ค ๐‘€)))
191180, 189, 190sylanbrc 582 . . . . . . . . 9 ((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โ†’ (๐ฝ โˆ’ 1) โˆˆ (๐ฟ...๐‘€))
19212adantlr 714 . . . . . . . . 9 (((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โˆง ๐‘– โˆˆ (๐ฟ...๐‘€)) โ†’ 0 โ‰ค (๐ตโ€˜๐‘–))
19314adantlr 714 . . . . . . . . 9 (((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โˆง ๐‘– โˆˆ (๐ฟ...๐‘€)) โ†’ (๐ตโ€˜๐‘–) โ‰ค 1)
1941, 114, 175, 95, 176, 191, 119, 192, 193fmul01 44891 . . . . . . . 8 ((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โ†’ (0 โ‰ค (seq๐ฟ( ยท , ๐ต)โ€˜(๐ฝ โˆ’ 1)) โˆง (seq๐ฟ( ยท , ๐ต)โ€˜(๐ฝ โˆ’ 1)) โ‰ค 1))
195194simprd 495 . . . . . . 7 ((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โ†’ (seq๐ฟ( ยท , ๐ต)โ€˜(๐ฝ โˆ’ 1)) โ‰ค 1)
196161, 162, 76, 174, 195lemul1ad 12175 . . . . . 6 ((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โ†’ ((seq๐ฟ( ยท , ๐ต)โ€˜(๐ฝ โˆ’ 1)) ยท (seq๐ฝ( ยท , ๐ต)โ€˜๐‘€)) โ‰ค (1 ยท (seq๐ฝ( ยท , ๐ต)โ€˜๐‘€)))
197126, 196eqbrtrd 5164 . . . . 5 ((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โ†’ (seq๐ฟ( ยท , ๐ต)โ€˜๐‘€) โ‰ค (1 ยท (seq๐ฝ( ยท , ๐ต)โ€˜๐‘€)))
19876recnd 11264 . . . . . 6 ((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โ†’ (seq๐ฝ( ยท , ๐ต)โ€˜๐‘€) โˆˆ โ„‚)
199198mullidd 11254 . . . . 5 ((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โ†’ (1 ยท (seq๐ฝ( ยท , ๐ต)โ€˜๐‘€)) = (seq๐ฝ( ยท , ๐ต)โ€˜๐‘€))
200197, 199breqtrd 5168 . . . 4 ((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โ†’ (seq๐ฟ( ยท , ๐ต)โ€˜๐‘€) โ‰ค (seq๐ฝ( ยท , ๐ต)โ€˜๐‘€))
2011, 2, 163, 59, 43, 73, 169, 171, 16, 20fmul01lt1lem1 44895 . . . . 5 (๐œ‘ โ†’ (seq๐ฝ( ยท , ๐ต)โ€˜๐‘€) < ๐ธ)
202201adantr 480 . . . 4 ((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โ†’ (seq๐ฝ( ยท , ๐ต)โ€˜๐‘€) < ๐ธ)
20340, 76, 78, 200, 202lelttrd 11394 . . 3 ((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โ†’ (seq๐ฟ( ยท , ๐ต)โ€˜๐‘€) < ๐ธ)
20424, 203eqbrtrid 5177 . 2 ((๐œ‘ โˆง ยฌ ๐ฝ = ๐ฟ) โ†’ (๐ดโ€˜๐‘€) < ๐ธ)
20523, 204pm2.61dan 812 1 (๐œ‘ โ†’ (๐ดโ€˜๐‘€) < ๐ธ)
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 395   โˆจ wo 846   โˆง w3a 1085   = wceq 1534  โ„ฒwnf 1778   โˆˆ wcel 2099  โ„ฒwnfc 2878   class class class wbr 5142  โ€˜cfv 6542  (class class class)co 7414  โ„cr 11129  0cc0 11130  1c1 11131   + caddc 11133   ยท cmul 11135   < clt 11270   โ‰ค cle 11271   โˆ’ cmin 11466  โ„คcz 12580  โ„คโ‰ฅcuz 12844  โ„+crp 12998  ...cfz 13508  seqcseq 13990
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734  ax-cnex 11186  ax-resscn 11187  ax-1cn 11188  ax-icn 11189  ax-addcl 11190  ax-addrcl 11191  ax-mulcl 11192  ax-mulrcl 11193  ax-mulcom 11194  ax-addass 11195  ax-mulass 11196  ax-distr 11197  ax-i2m1 11198  ax-1ne0 11199  ax-1rid 11200  ax-rnegex 11201  ax-rrecex 11202  ax-cnre 11203  ax-pre-lttri 11204  ax-pre-lttrn 11205  ax-pre-ltadd 11206  ax-pre-mulgt0 11207
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-nel 3042  df-ral 3057  df-rex 3066  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7370  df-ov 7417  df-oprab 7418  df-mpo 7419  df-om 7865  df-1st 7987  df-2nd 7988  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-er 8718  df-en 8956  df-dom 8957  df-sdom 8958  df-pnf 11272  df-mnf 11273  df-xr 11274  df-ltxr 11275  df-le 11276  df-sub 11468  df-neg 11469  df-nn 12235  df-n0 12495  df-z 12581  df-uz 12845  df-rp 12999  df-fz 13509  df-fzo 13652  df-seq 13991
This theorem is referenced by:  fmul01lt1  44897
  Copyright terms: Public domain W3C validator