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

Theorem fmul01 44997
Description: Multiplying a finite number of values in [ 0 , 1 ] , gives the final product itself a number in [ 0 , 1 ]. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
Hypotheses
Ref Expression
fmul01.1 โ„ฒ๐‘–๐ต
fmul01.2 โ„ฒ๐‘–๐œ‘
fmul01.3 ๐ด = seq๐ฟ( ยท , ๐ต)
fmul01.4 (๐œ‘ โ†’ ๐ฟ โˆˆ โ„ค)
fmul01.5 (๐œ‘ โ†’ ๐‘€ โˆˆ (โ„คโ‰ฅโ€˜๐ฟ))
fmul01.6 (๐œ‘ โ†’ ๐พ โˆˆ (๐ฟ...๐‘€))
fmul01.7 ((๐œ‘ โˆง ๐‘– โˆˆ (๐ฟ...๐‘€)) โ†’ (๐ตโ€˜๐‘–) โˆˆ โ„)
fmul01.8 ((๐œ‘ โˆง ๐‘– โˆˆ (๐ฟ...๐‘€)) โ†’ 0 โ‰ค (๐ตโ€˜๐‘–))
fmul01.9 ((๐œ‘ โˆง ๐‘– โˆˆ (๐ฟ...๐‘€)) โ†’ (๐ตโ€˜๐‘–) โ‰ค 1)
Assertion
Ref Expression
fmul01 (๐œ‘ โ†’ (0 โ‰ค (๐ดโ€˜๐พ) โˆง (๐ดโ€˜๐พ) โ‰ค 1))
Distinct variable groups:   ๐‘–,๐ฟ   ๐‘–,๐‘€
Allowed substitution hints:   ๐œ‘(๐‘–)   ๐ด(๐‘–)   ๐ต(๐‘–)   ๐พ(๐‘–)

Proof of Theorem fmul01
Dummy variables ๐‘— ๐‘˜ ๐‘™ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fmul01.6 . 2 (๐œ‘ โ†’ ๐พ โˆˆ (๐ฟ...๐‘€))
2 fveq2 6902 . . . . . 6 (๐‘˜ = ๐ฟ โ†’ (๐ดโ€˜๐‘˜) = (๐ดโ€˜๐ฟ))
32breq2d 5164 . . . . 5 (๐‘˜ = ๐ฟ โ†’ (0 โ‰ค (๐ดโ€˜๐‘˜) โ†” 0 โ‰ค (๐ดโ€˜๐ฟ)))
42breq1d 5162 . . . . 5 (๐‘˜ = ๐ฟ โ†’ ((๐ดโ€˜๐‘˜) โ‰ค 1 โ†” (๐ดโ€˜๐ฟ) โ‰ค 1))
53, 4anbi12d 630 . . . 4 (๐‘˜ = ๐ฟ โ†’ ((0 โ‰ค (๐ดโ€˜๐‘˜) โˆง (๐ดโ€˜๐‘˜) โ‰ค 1) โ†” (0 โ‰ค (๐ดโ€˜๐ฟ) โˆง (๐ดโ€˜๐ฟ) โ‰ค 1)))
65imbi2d 339 . . 3 (๐‘˜ = ๐ฟ โ†’ ((๐œ‘ โ†’ (0 โ‰ค (๐ดโ€˜๐‘˜) โˆง (๐ดโ€˜๐‘˜) โ‰ค 1)) โ†” (๐œ‘ โ†’ (0 โ‰ค (๐ดโ€˜๐ฟ) โˆง (๐ดโ€˜๐ฟ) โ‰ค 1))))
7 fveq2 6902 . . . . . 6 (๐‘˜ = ๐‘— โ†’ (๐ดโ€˜๐‘˜) = (๐ดโ€˜๐‘—))
87breq2d 5164 . . . . 5 (๐‘˜ = ๐‘— โ†’ (0 โ‰ค (๐ดโ€˜๐‘˜) โ†” 0 โ‰ค (๐ดโ€˜๐‘—)))
97breq1d 5162 . . . . 5 (๐‘˜ = ๐‘— โ†’ ((๐ดโ€˜๐‘˜) โ‰ค 1 โ†” (๐ดโ€˜๐‘—) โ‰ค 1))
108, 9anbi12d 630 . . . 4 (๐‘˜ = ๐‘— โ†’ ((0 โ‰ค (๐ดโ€˜๐‘˜) โˆง (๐ดโ€˜๐‘˜) โ‰ค 1) โ†” (0 โ‰ค (๐ดโ€˜๐‘—) โˆง (๐ดโ€˜๐‘—) โ‰ค 1)))
1110imbi2d 339 . . 3 (๐‘˜ = ๐‘— โ†’ ((๐œ‘ โ†’ (0 โ‰ค (๐ดโ€˜๐‘˜) โˆง (๐ดโ€˜๐‘˜) โ‰ค 1)) โ†” (๐œ‘ โ†’ (0 โ‰ค (๐ดโ€˜๐‘—) โˆง (๐ดโ€˜๐‘—) โ‰ค 1))))
12 fveq2 6902 . . . . . 6 (๐‘˜ = (๐‘— + 1) โ†’ (๐ดโ€˜๐‘˜) = (๐ดโ€˜(๐‘— + 1)))
1312breq2d 5164 . . . . 5 (๐‘˜ = (๐‘— + 1) โ†’ (0 โ‰ค (๐ดโ€˜๐‘˜) โ†” 0 โ‰ค (๐ดโ€˜(๐‘— + 1))))
1412breq1d 5162 . . . . 5 (๐‘˜ = (๐‘— + 1) โ†’ ((๐ดโ€˜๐‘˜) โ‰ค 1 โ†” (๐ดโ€˜(๐‘— + 1)) โ‰ค 1))
1513, 14anbi12d 630 . . . 4 (๐‘˜ = (๐‘— + 1) โ†’ ((0 โ‰ค (๐ดโ€˜๐‘˜) โˆง (๐ดโ€˜๐‘˜) โ‰ค 1) โ†” (0 โ‰ค (๐ดโ€˜(๐‘— + 1)) โˆง (๐ดโ€˜(๐‘— + 1)) โ‰ค 1)))
1615imbi2d 339 . . 3 (๐‘˜ = (๐‘— + 1) โ†’ ((๐œ‘ โ†’ (0 โ‰ค (๐ดโ€˜๐‘˜) โˆง (๐ดโ€˜๐‘˜) โ‰ค 1)) โ†” (๐œ‘ โ†’ (0 โ‰ค (๐ดโ€˜(๐‘— + 1)) โˆง (๐ดโ€˜(๐‘— + 1)) โ‰ค 1))))
17 fveq2 6902 . . . . . 6 (๐‘˜ = ๐พ โ†’ (๐ดโ€˜๐‘˜) = (๐ดโ€˜๐พ))
1817breq2d 5164 . . . . 5 (๐‘˜ = ๐พ โ†’ (0 โ‰ค (๐ดโ€˜๐‘˜) โ†” 0 โ‰ค (๐ดโ€˜๐พ)))
1917breq1d 5162 . . . . 5 (๐‘˜ = ๐พ โ†’ ((๐ดโ€˜๐‘˜) โ‰ค 1 โ†” (๐ดโ€˜๐พ) โ‰ค 1))
2018, 19anbi12d 630 . . . 4 (๐‘˜ = ๐พ โ†’ ((0 โ‰ค (๐ดโ€˜๐‘˜) โˆง (๐ดโ€˜๐‘˜) โ‰ค 1) โ†” (0 โ‰ค (๐ดโ€˜๐พ) โˆง (๐ดโ€˜๐พ) โ‰ค 1)))
2120imbi2d 339 . . 3 (๐‘˜ = ๐พ โ†’ ((๐œ‘ โ†’ (0 โ‰ค (๐ดโ€˜๐‘˜) โˆง (๐ดโ€˜๐‘˜) โ‰ค 1)) โ†” (๐œ‘ โ†’ (0 โ‰ค (๐ดโ€˜๐พ) โˆง (๐ดโ€˜๐พ) โ‰ค 1))))
22 fmul01.4 . . . . . . . 8 (๐œ‘ โ†’ ๐ฟ โˆˆ โ„ค)
23 fmul01.5 . . . . . . . . 9 (๐œ‘ โ†’ ๐‘€ โˆˆ (โ„คโ‰ฅโ€˜๐ฟ))
24 eluzelz 12870 . . . . . . . . 9 (๐‘€ โˆˆ (โ„คโ‰ฅโ€˜๐ฟ) โ†’ ๐‘€ โˆˆ โ„ค)
2523, 24syl 17 . . . . . . . 8 (๐œ‘ โ†’ ๐‘€ โˆˆ โ„ค)
2622zred 12704 . . . . . . . . 9 (๐œ‘ โ†’ ๐ฟ โˆˆ โ„)
2726leidd 11818 . . . . . . . 8 (๐œ‘ โ†’ ๐ฟ โ‰ค ๐ฟ)
28 eluz 12874 . . . . . . . . . 10 ((๐ฟ โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„ค) โ†’ (๐‘€ โˆˆ (โ„คโ‰ฅโ€˜๐ฟ) โ†” ๐ฟ โ‰ค ๐‘€))
2922, 25, 28syl2anc 582 . . . . . . . . 9 (๐œ‘ โ†’ (๐‘€ โˆˆ (โ„คโ‰ฅโ€˜๐ฟ) โ†” ๐ฟ โ‰ค ๐‘€))
3023, 29mpbid 231 . . . . . . . 8 (๐œ‘ โ†’ ๐ฟ โ‰ค ๐‘€)
3122, 25, 22, 27, 30elfzd 13532 . . . . . . 7 (๐œ‘ โ†’ ๐ฟ โˆˆ (๐ฟ...๐‘€))
3231ancli 547 . . . . . . 7 (๐œ‘ โ†’ (๐œ‘ โˆง ๐ฟ โˆˆ (๐ฟ...๐‘€)))
33 fmul01.2 . . . . . . . . . 10 โ„ฒ๐‘–๐œ‘
34 nfv 1909 . . . . . . . . . 10 โ„ฒ๐‘– ๐ฟ โˆˆ (๐ฟ...๐‘€)
3533, 34nfan 1894 . . . . . . . . 9 โ„ฒ๐‘–(๐œ‘ โˆง ๐ฟ โˆˆ (๐ฟ...๐‘€))
36 nfcv 2899 . . . . . . . . . 10 โ„ฒ๐‘–0
37 nfcv 2899 . . . . . . . . . 10 โ„ฒ๐‘– โ‰ค
38 fmul01.1 . . . . . . . . . . 11 โ„ฒ๐‘–๐ต
39 nfcv 2899 . . . . . . . . . . 11 โ„ฒ๐‘–๐ฟ
4038, 39nffv 6912 . . . . . . . . . 10 โ„ฒ๐‘–(๐ตโ€˜๐ฟ)
4136, 37, 40nfbr 5199 . . . . . . . . 9 โ„ฒ๐‘–0 โ‰ค (๐ตโ€˜๐ฟ)
4235, 41nfim 1891 . . . . . . . 8 โ„ฒ๐‘–((๐œ‘ โˆง ๐ฟ โˆˆ (๐ฟ...๐‘€)) โ†’ 0 โ‰ค (๐ตโ€˜๐ฟ))
43 eleq1 2817 . . . . . . . . . 10 (๐‘– = ๐ฟ โ†’ (๐‘– โˆˆ (๐ฟ...๐‘€) โ†” ๐ฟ โˆˆ (๐ฟ...๐‘€)))
4443anbi2d 628 . . . . . . . . 9 (๐‘– = ๐ฟ โ†’ ((๐œ‘ โˆง ๐‘– โˆˆ (๐ฟ...๐‘€)) โ†” (๐œ‘ โˆง ๐ฟ โˆˆ (๐ฟ...๐‘€))))
45 fveq2 6902 . . . . . . . . . 10 (๐‘– = ๐ฟ โ†’ (๐ตโ€˜๐‘–) = (๐ตโ€˜๐ฟ))
4645breq2d 5164 . . . . . . . . 9 (๐‘– = ๐ฟ โ†’ (0 โ‰ค (๐ตโ€˜๐‘–) โ†” 0 โ‰ค (๐ตโ€˜๐ฟ)))
4744, 46imbi12d 343 . . . . . . . 8 (๐‘– = ๐ฟ โ†’ (((๐œ‘ โˆง ๐‘– โˆˆ (๐ฟ...๐‘€)) โ†’ 0 โ‰ค (๐ตโ€˜๐‘–)) โ†” ((๐œ‘ โˆง ๐ฟ โˆˆ (๐ฟ...๐‘€)) โ†’ 0 โ‰ค (๐ตโ€˜๐ฟ))))
48 fmul01.8 . . . . . . . 8 ((๐œ‘ โˆง ๐‘– โˆˆ (๐ฟ...๐‘€)) โ†’ 0 โ‰ค (๐ตโ€˜๐‘–))
4942, 47, 48vtoclg1f 3558 . . . . . . 7 (๐ฟ โˆˆ (๐ฟ...๐‘€) โ†’ ((๐œ‘ โˆง ๐ฟ โˆˆ (๐ฟ...๐‘€)) โ†’ 0 โ‰ค (๐ตโ€˜๐ฟ)))
5031, 32, 49sylc 65 . . . . . 6 (๐œ‘ โ†’ 0 โ‰ค (๐ตโ€˜๐ฟ))
51 fmul01.3 . . . . . . . 8 ๐ด = seq๐ฟ( ยท , ๐ต)
5251fveq1i 6903 . . . . . . 7 (๐ดโ€˜๐ฟ) = (seq๐ฟ( ยท , ๐ต)โ€˜๐ฟ)
53 seq1 14019 . . . . . . . 8 (๐ฟ โˆˆ โ„ค โ†’ (seq๐ฟ( ยท , ๐ต)โ€˜๐ฟ) = (๐ตโ€˜๐ฟ))
5422, 53syl 17 . . . . . . 7 (๐œ‘ โ†’ (seq๐ฟ( ยท , ๐ต)โ€˜๐ฟ) = (๐ตโ€˜๐ฟ))
5552, 54eqtrid 2780 . . . . . 6 (๐œ‘ โ†’ (๐ดโ€˜๐ฟ) = (๐ตโ€˜๐ฟ))
5650, 55breqtrrd 5180 . . . . 5 (๐œ‘ โ†’ 0 โ‰ค (๐ดโ€˜๐ฟ))
57 nfcv 2899 . . . . . . . . . 10 โ„ฒ๐‘–1
5840, 37, 57nfbr 5199 . . . . . . . . 9 โ„ฒ๐‘–(๐ตโ€˜๐ฟ) โ‰ค 1
5935, 58nfim 1891 . . . . . . . 8 โ„ฒ๐‘–((๐œ‘ โˆง ๐ฟ โˆˆ (๐ฟ...๐‘€)) โ†’ (๐ตโ€˜๐ฟ) โ‰ค 1)
6045breq1d 5162 . . . . . . . . 9 (๐‘– = ๐ฟ โ†’ ((๐ตโ€˜๐‘–) โ‰ค 1 โ†” (๐ตโ€˜๐ฟ) โ‰ค 1))
6144, 60imbi12d 343 . . . . . . . 8 (๐‘– = ๐ฟ โ†’ (((๐œ‘ โˆง ๐‘– โˆˆ (๐ฟ...๐‘€)) โ†’ (๐ตโ€˜๐‘–) โ‰ค 1) โ†” ((๐œ‘ โˆง ๐ฟ โˆˆ (๐ฟ...๐‘€)) โ†’ (๐ตโ€˜๐ฟ) โ‰ค 1)))
62 fmul01.9 . . . . . . . 8 ((๐œ‘ โˆง ๐‘– โˆˆ (๐ฟ...๐‘€)) โ†’ (๐ตโ€˜๐‘–) โ‰ค 1)
6359, 61, 62vtoclg1f 3558 . . . . . . 7 (๐ฟ โˆˆ (๐ฟ...๐‘€) โ†’ ((๐œ‘ โˆง ๐ฟ โˆˆ (๐ฟ...๐‘€)) โ†’ (๐ตโ€˜๐ฟ) โ‰ค 1))
6431, 32, 63sylc 65 . . . . . 6 (๐œ‘ โ†’ (๐ตโ€˜๐ฟ) โ‰ค 1)
6555, 64eqbrtrd 5174 . . . . 5 (๐œ‘ โ†’ (๐ดโ€˜๐ฟ) โ‰ค 1)
6656, 65jca 510 . . . 4 (๐œ‘ โ†’ (0 โ‰ค (๐ดโ€˜๐ฟ) โˆง (๐ดโ€˜๐ฟ) โ‰ค 1))
6766a1i 11 . . 3 (๐‘€ โˆˆ (โ„คโ‰ฅโ€˜๐ฟ) โ†’ (๐œ‘ โ†’ (0 โ‰ค (๐ดโ€˜๐ฟ) โˆง (๐ดโ€˜๐ฟ) โ‰ค 1)))
68 elfzouz 13676 . . . . . . . . . 10 (๐‘— โˆˆ (๐ฟ..^๐‘€) โ†’ ๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐ฟ))
69683ad2ant1 1130 . . . . . . . . 9 ((๐‘— โˆˆ (๐ฟ..^๐‘€) โˆง (๐œ‘ โ†’ (0 โ‰ค (๐ดโ€˜๐‘—) โˆง (๐ดโ€˜๐‘—) โ‰ค 1)) โˆง ๐œ‘) โ†’ ๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐ฟ))
70 simpl3 1190 . . . . . . . . . 10 (((๐‘— โˆˆ (๐ฟ..^๐‘€) โˆง (๐œ‘ โ†’ (0 โ‰ค (๐ดโ€˜๐‘—) โˆง (๐ดโ€˜๐‘—) โ‰ค 1)) โˆง ๐œ‘) โˆง ๐‘˜ โˆˆ (๐ฟ...๐‘—)) โ†’ ๐œ‘)
71 elfzouz2 13687 . . . . . . . . . . . . 13 (๐‘— โˆˆ (๐ฟ..^๐‘€) โ†’ ๐‘€ โˆˆ (โ„คโ‰ฅโ€˜๐‘—))
72 fzss2 13581 . . . . . . . . . . . . 13 (๐‘€ โˆˆ (โ„คโ‰ฅโ€˜๐‘—) โ†’ (๐ฟ...๐‘—) โІ (๐ฟ...๐‘€))
7371, 72syl 17 . . . . . . . . . . . 12 (๐‘— โˆˆ (๐ฟ..^๐‘€) โ†’ (๐ฟ...๐‘—) โІ (๐ฟ...๐‘€))
74733ad2ant1 1130 . . . . . . . . . . 11 ((๐‘— โˆˆ (๐ฟ..^๐‘€) โˆง (๐œ‘ โ†’ (0 โ‰ค (๐ดโ€˜๐‘—) โˆง (๐ดโ€˜๐‘—) โ‰ค 1)) โˆง ๐œ‘) โ†’ (๐ฟ...๐‘—) โІ (๐ฟ...๐‘€))
7574sselda 3982 . . . . . . . . . 10 (((๐‘— โˆˆ (๐ฟ..^๐‘€) โˆง (๐œ‘ โ†’ (0 โ‰ค (๐ดโ€˜๐‘—) โˆง (๐ดโ€˜๐‘—) โ‰ค 1)) โˆง ๐œ‘) โˆง ๐‘˜ โˆˆ (๐ฟ...๐‘—)) โ†’ ๐‘˜ โˆˆ (๐ฟ...๐‘€))
76 nfv 1909 . . . . . . . . . . . . 13 โ„ฒ๐‘– ๐‘˜ โˆˆ (๐ฟ...๐‘€)
7733, 76nfan 1894 . . . . . . . . . . . 12 โ„ฒ๐‘–(๐œ‘ โˆง ๐‘˜ โˆˆ (๐ฟ...๐‘€))
78 nfcv 2899 . . . . . . . . . . . . . 14 โ„ฒ๐‘–๐‘˜
7938, 78nffv 6912 . . . . . . . . . . . . 13 โ„ฒ๐‘–(๐ตโ€˜๐‘˜)
8079nfel1 2916 . . . . . . . . . . . 12 โ„ฒ๐‘–(๐ตโ€˜๐‘˜) โˆˆ โ„
8177, 80nfim 1891 . . . . . . . . . . 11 โ„ฒ๐‘–((๐œ‘ โˆง ๐‘˜ โˆˆ (๐ฟ...๐‘€)) โ†’ (๐ตโ€˜๐‘˜) โˆˆ โ„)
82 eleq1 2817 . . . . . . . . . . . . 13 (๐‘– = ๐‘˜ โ†’ (๐‘– โˆˆ (๐ฟ...๐‘€) โ†” ๐‘˜ โˆˆ (๐ฟ...๐‘€)))
8382anbi2d 628 . . . . . . . . . . . 12 (๐‘– = ๐‘˜ โ†’ ((๐œ‘ โˆง ๐‘– โˆˆ (๐ฟ...๐‘€)) โ†” (๐œ‘ โˆง ๐‘˜ โˆˆ (๐ฟ...๐‘€))))
84 fveq2 6902 . . . . . . . . . . . . 13 (๐‘– = ๐‘˜ โ†’ (๐ตโ€˜๐‘–) = (๐ตโ€˜๐‘˜))
8584eleq1d 2814 . . . . . . . . . . . 12 (๐‘– = ๐‘˜ โ†’ ((๐ตโ€˜๐‘–) โˆˆ โ„ โ†” (๐ตโ€˜๐‘˜) โˆˆ โ„))
8683, 85imbi12d 343 . . . . . . . . . . 11 (๐‘– = ๐‘˜ โ†’ (((๐œ‘ โˆง ๐‘– โˆˆ (๐ฟ...๐‘€)) โ†’ (๐ตโ€˜๐‘–) โˆˆ โ„) โ†” ((๐œ‘ โˆง ๐‘˜ โˆˆ (๐ฟ...๐‘€)) โ†’ (๐ตโ€˜๐‘˜) โˆˆ โ„)))
87 fmul01.7 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘– โˆˆ (๐ฟ...๐‘€)) โ†’ (๐ตโ€˜๐‘–) โˆˆ โ„)
8881, 86, 87chvarfv 2228 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘˜ โˆˆ (๐ฟ...๐‘€)) โ†’ (๐ตโ€˜๐‘˜) โˆˆ โ„)
8970, 75, 88syl2anc 582 . . . . . . . . 9 (((๐‘— โˆˆ (๐ฟ..^๐‘€) โˆง (๐œ‘ โ†’ (0 โ‰ค (๐ดโ€˜๐‘—) โˆง (๐ดโ€˜๐‘—) โ‰ค 1)) โˆง ๐œ‘) โˆง ๐‘˜ โˆˆ (๐ฟ...๐‘—)) โ†’ (๐ตโ€˜๐‘˜) โˆˆ โ„)
90 remulcl 11231 . . . . . . . . . 10 ((๐‘˜ โˆˆ โ„ โˆง ๐‘™ โˆˆ โ„) โ†’ (๐‘˜ ยท ๐‘™) โˆˆ โ„)
9190adantl 480 . . . . . . . . 9 (((๐‘— โˆˆ (๐ฟ..^๐‘€) โˆง (๐œ‘ โ†’ (0 โ‰ค (๐ดโ€˜๐‘—) โˆง (๐ดโ€˜๐‘—) โ‰ค 1)) โˆง ๐œ‘) โˆง (๐‘˜ โˆˆ โ„ โˆง ๐‘™ โˆˆ โ„)) โ†’ (๐‘˜ ยท ๐‘™) โˆˆ โ„)
9269, 89, 91seqcl 14027 . . . . . . . 8 ((๐‘— โˆˆ (๐ฟ..^๐‘€) โˆง (๐œ‘ โ†’ (0 โ‰ค (๐ดโ€˜๐‘—) โˆง (๐ดโ€˜๐‘—) โ‰ค 1)) โˆง ๐œ‘) โ†’ (seq๐ฟ( ยท , ๐ต)โ€˜๐‘—) โˆˆ โ„)
93 simp3 1135 . . . . . . . . 9 ((๐‘— โˆˆ (๐ฟ..^๐‘€) โˆง (๐œ‘ โ†’ (0 โ‰ค (๐ดโ€˜๐‘—) โˆง (๐ดโ€˜๐‘—) โ‰ค 1)) โˆง ๐œ‘) โ†’ ๐œ‘)
94 fzofzp1 13769 . . . . . . . . . 10 (๐‘— โˆˆ (๐ฟ..^๐‘€) โ†’ (๐‘— + 1) โˆˆ (๐ฟ...๐‘€))
95943ad2ant1 1130 . . . . . . . . 9 ((๐‘— โˆˆ (๐ฟ..^๐‘€) โˆง (๐œ‘ โ†’ (0 โ‰ค (๐ดโ€˜๐‘—) โˆง (๐ดโ€˜๐‘—) โ‰ค 1)) โˆง ๐œ‘) โ†’ (๐‘— + 1) โˆˆ (๐ฟ...๐‘€))
96 nfv 1909 . . . . . . . . . . . . 13 โ„ฒ๐‘–(๐‘— + 1) โˆˆ (๐ฟ...๐‘€)
9733, 96nfan 1894 . . . . . . . . . . . 12 โ„ฒ๐‘–(๐œ‘ โˆง (๐‘— + 1) โˆˆ (๐ฟ...๐‘€))
98 nfcv 2899 . . . . . . . . . . . . . 14 โ„ฒ๐‘–(๐‘— + 1)
9938, 98nffv 6912 . . . . . . . . . . . . 13 โ„ฒ๐‘–(๐ตโ€˜(๐‘— + 1))
10099nfel1 2916 . . . . . . . . . . . 12 โ„ฒ๐‘–(๐ตโ€˜(๐‘— + 1)) โˆˆ โ„
10197, 100nfim 1891 . . . . . . . . . . 11 โ„ฒ๐‘–((๐œ‘ โˆง (๐‘— + 1) โˆˆ (๐ฟ...๐‘€)) โ†’ (๐ตโ€˜(๐‘— + 1)) โˆˆ โ„)
102 eleq1 2817 . . . . . . . . . . . . 13 (๐‘– = (๐‘— + 1) โ†’ (๐‘– โˆˆ (๐ฟ...๐‘€) โ†” (๐‘— + 1) โˆˆ (๐ฟ...๐‘€)))
103102anbi2d 628 . . . . . . . . . . . 12 (๐‘– = (๐‘— + 1) โ†’ ((๐œ‘ โˆง ๐‘– โˆˆ (๐ฟ...๐‘€)) โ†” (๐œ‘ โˆง (๐‘— + 1) โˆˆ (๐ฟ...๐‘€))))
104 fveq2 6902 . . . . . . . . . . . . 13 (๐‘– = (๐‘— + 1) โ†’ (๐ตโ€˜๐‘–) = (๐ตโ€˜(๐‘— + 1)))
105104eleq1d 2814 . . . . . . . . . . . 12 (๐‘– = (๐‘— + 1) โ†’ ((๐ตโ€˜๐‘–) โˆˆ โ„ โ†” (๐ตโ€˜(๐‘— + 1)) โˆˆ โ„))
106103, 105imbi12d 343 . . . . . . . . . . 11 (๐‘– = (๐‘— + 1) โ†’ (((๐œ‘ โˆง ๐‘– โˆˆ (๐ฟ...๐‘€)) โ†’ (๐ตโ€˜๐‘–) โˆˆ โ„) โ†” ((๐œ‘ โˆง (๐‘— + 1) โˆˆ (๐ฟ...๐‘€)) โ†’ (๐ตโ€˜(๐‘— + 1)) โˆˆ โ„)))
107101, 106, 87vtoclg1f 3558 . . . . . . . . . 10 ((๐‘— + 1) โˆˆ (๐ฟ...๐‘€) โ†’ ((๐œ‘ โˆง (๐‘— + 1) โˆˆ (๐ฟ...๐‘€)) โ†’ (๐ตโ€˜(๐‘— + 1)) โˆˆ โ„))
108107anabsi7 669 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘— + 1) โˆˆ (๐ฟ...๐‘€)) โ†’ (๐ตโ€˜(๐‘— + 1)) โˆˆ โ„)
10993, 95, 108syl2anc 582 . . . . . . . 8 ((๐‘— โˆˆ (๐ฟ..^๐‘€) โˆง (๐œ‘ โ†’ (0 โ‰ค (๐ดโ€˜๐‘—) โˆง (๐ดโ€˜๐‘—) โ‰ค 1)) โˆง ๐œ‘) โ†’ (๐ตโ€˜(๐‘— + 1)) โˆˆ โ„)
110 pm3.35 801 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐œ‘ โ†’ (0 โ‰ค (๐ดโ€˜๐‘—) โˆง (๐ดโ€˜๐‘—) โ‰ค 1))) โ†’ (0 โ‰ค (๐ดโ€˜๐‘—) โˆง (๐ดโ€˜๐‘—) โ‰ค 1))
111110ancoms 457 . . . . . . . . . . 11 (((๐œ‘ โ†’ (0 โ‰ค (๐ดโ€˜๐‘—) โˆง (๐ดโ€˜๐‘—) โ‰ค 1)) โˆง ๐œ‘) โ†’ (0 โ‰ค (๐ดโ€˜๐‘—) โˆง (๐ดโ€˜๐‘—) โ‰ค 1))
112 simpl 481 . . . . . . . . . . 11 ((0 โ‰ค (๐ดโ€˜๐‘—) โˆง (๐ดโ€˜๐‘—) โ‰ค 1) โ†’ 0 โ‰ค (๐ดโ€˜๐‘—))
113111, 112syl 17 . . . . . . . . . 10 (((๐œ‘ โ†’ (0 โ‰ค (๐ดโ€˜๐‘—) โˆง (๐ดโ€˜๐‘—) โ‰ค 1)) โˆง ๐œ‘) โ†’ 0 โ‰ค (๐ดโ€˜๐‘—))
1141133adant1 1127 . . . . . . . . 9 ((๐‘— โˆˆ (๐ฟ..^๐‘€) โˆง (๐œ‘ โ†’ (0 โ‰ค (๐ดโ€˜๐‘—) โˆง (๐ดโ€˜๐‘—) โ‰ค 1)) โˆง ๐œ‘) โ†’ 0 โ‰ค (๐ดโ€˜๐‘—))
11551fveq1i 6903 . . . . . . . . 9 (๐ดโ€˜๐‘—) = (seq๐ฟ( ยท , ๐ต)โ€˜๐‘—)
116114, 115breqtrdi 5193 . . . . . . . 8 ((๐‘— โˆˆ (๐ฟ..^๐‘€) โˆง (๐œ‘ โ†’ (0 โ‰ค (๐ดโ€˜๐‘—) โˆง (๐ดโ€˜๐‘—) โ‰ค 1)) โˆง ๐œ‘) โ†’ 0 โ‰ค (seq๐ฟ( ยท , ๐ต)โ€˜๐‘—))
117 simp1 1133 . . . . . . . . 9 ((๐‘— โˆˆ (๐ฟ..^๐‘€) โˆง (๐œ‘ โ†’ (0 โ‰ค (๐ดโ€˜๐‘—) โˆง (๐ดโ€˜๐‘—) โ‰ค 1)) โˆง ๐œ‘) โ†’ ๐‘— โˆˆ (๐ฟ..^๐‘€))
11894adantl 480 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘— โˆˆ (๐ฟ..^๐‘€)) โ†’ (๐‘— + 1) โˆˆ (๐ฟ...๐‘€))
119 simpl 481 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘— โˆˆ (๐ฟ..^๐‘€)) โ†’ ๐œ‘)
120119, 118jca 510 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘— โˆˆ (๐ฟ..^๐‘€)) โ†’ (๐œ‘ โˆง (๐‘— + 1) โˆˆ (๐ฟ...๐‘€)))
12136, 37, 99nfbr 5199 . . . . . . . . . . . 12 โ„ฒ๐‘–0 โ‰ค (๐ตโ€˜(๐‘— + 1))
12297, 121nfim 1891 . . . . . . . . . . 11 โ„ฒ๐‘–((๐œ‘ โˆง (๐‘— + 1) โˆˆ (๐ฟ...๐‘€)) โ†’ 0 โ‰ค (๐ตโ€˜(๐‘— + 1)))
123104breq2d 5164 . . . . . . . . . . . 12 (๐‘– = (๐‘— + 1) โ†’ (0 โ‰ค (๐ตโ€˜๐‘–) โ†” 0 โ‰ค (๐ตโ€˜(๐‘— + 1))))
124103, 123imbi12d 343 . . . . . . . . . . 11 (๐‘– = (๐‘— + 1) โ†’ (((๐œ‘ โˆง ๐‘– โˆˆ (๐ฟ...๐‘€)) โ†’ 0 โ‰ค (๐ตโ€˜๐‘–)) โ†” ((๐œ‘ โˆง (๐‘— + 1) โˆˆ (๐ฟ...๐‘€)) โ†’ 0 โ‰ค (๐ตโ€˜(๐‘— + 1)))))
125122, 124, 48vtoclg1f 3558 . . . . . . . . . 10 ((๐‘— + 1) โˆˆ (๐ฟ...๐‘€) โ†’ ((๐œ‘ โˆง (๐‘— + 1) โˆˆ (๐ฟ...๐‘€)) โ†’ 0 โ‰ค (๐ตโ€˜(๐‘— + 1))))
126118, 120, 125sylc 65 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘— โˆˆ (๐ฟ..^๐‘€)) โ†’ 0 โ‰ค (๐ตโ€˜(๐‘— + 1)))
12793, 117, 126syl2anc 582 . . . . . . . 8 ((๐‘— โˆˆ (๐ฟ..^๐‘€) โˆง (๐œ‘ โ†’ (0 โ‰ค (๐ดโ€˜๐‘—) โˆง (๐ดโ€˜๐‘—) โ‰ค 1)) โˆง ๐œ‘) โ†’ 0 โ‰ค (๐ตโ€˜(๐‘— + 1)))
12892, 109, 116, 127mulge0d 11829 . . . . . . 7 ((๐‘— โˆˆ (๐ฟ..^๐‘€) โˆง (๐œ‘ โ†’ (0 โ‰ค (๐ดโ€˜๐‘—) โˆง (๐ดโ€˜๐‘—) โ‰ค 1)) โˆง ๐œ‘) โ†’ 0 โ‰ค ((seq๐ฟ( ยท , ๐ต)โ€˜๐‘—) ยท (๐ตโ€˜(๐‘— + 1))))
129 seqp1 14021 . . . . . . . 8 (๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐ฟ) โ†’ (seq๐ฟ( ยท , ๐ต)โ€˜(๐‘— + 1)) = ((seq๐ฟ( ยท , ๐ต)โ€˜๐‘—) ยท (๐ตโ€˜(๐‘— + 1))))
13069, 129syl 17 . . . . . . 7 ((๐‘— โˆˆ (๐ฟ..^๐‘€) โˆง (๐œ‘ โ†’ (0 โ‰ค (๐ดโ€˜๐‘—) โˆง (๐ดโ€˜๐‘—) โ‰ค 1)) โˆง ๐œ‘) โ†’ (seq๐ฟ( ยท , ๐ต)โ€˜(๐‘— + 1)) = ((seq๐ฟ( ยท , ๐ต)โ€˜๐‘—) ยท (๐ตโ€˜(๐‘— + 1))))
131128, 130breqtrrd 5180 . . . . . 6 ((๐‘— โˆˆ (๐ฟ..^๐‘€) โˆง (๐œ‘ โ†’ (0 โ‰ค (๐ดโ€˜๐‘—) โˆง (๐ดโ€˜๐‘—) โ‰ค 1)) โˆง ๐œ‘) โ†’ 0 โ‰ค (seq๐ฟ( ยท , ๐ต)โ€˜(๐‘— + 1)))
13251fveq1i 6903 . . . . . 6 (๐ดโ€˜(๐‘— + 1)) = (seq๐ฟ( ยท , ๐ต)โ€˜(๐‘— + 1))
133131, 132breqtrrdi 5194 . . . . 5 ((๐‘— โˆˆ (๐ฟ..^๐‘€) โˆง (๐œ‘ โ†’ (0 โ‰ค (๐ดโ€˜๐‘—) โˆง (๐ดโ€˜๐‘—) โ‰ค 1)) โˆง ๐œ‘) โ†’ 0 โ‰ค (๐ดโ€˜(๐‘— + 1)))
13492, 109remulcld 11282 . . . . . . . 8 ((๐‘— โˆˆ (๐ฟ..^๐‘€) โˆง (๐œ‘ โ†’ (0 โ‰ค (๐ดโ€˜๐‘—) โˆง (๐ดโ€˜๐‘—) โ‰ค 1)) โˆง ๐œ‘) โ†’ ((seq๐ฟ( ยท , ๐ต)โ€˜๐‘—) ยท (๐ตโ€˜(๐‘— + 1))) โˆˆ โ„)
135 1red 11253 . . . . . . . 8 ((๐‘— โˆˆ (๐ฟ..^๐‘€) โˆง (๐œ‘ โ†’ (0 โ‰ค (๐ดโ€˜๐‘—) โˆง (๐ดโ€˜๐‘—) โ‰ค 1)) โˆง ๐œ‘) โ†’ 1 โˆˆ โ„)
13693, 95jca 510 . . . . . . . . . . 11 ((๐‘— โˆˆ (๐ฟ..^๐‘€) โˆง (๐œ‘ โ†’ (0 โ‰ค (๐ดโ€˜๐‘—) โˆง (๐ดโ€˜๐‘—) โ‰ค 1)) โˆง ๐œ‘) โ†’ (๐œ‘ โˆง (๐‘— + 1) โˆˆ (๐ฟ...๐‘€)))
13799, 37, 57nfbr 5199 . . . . . . . . . . . . 13 โ„ฒ๐‘–(๐ตโ€˜(๐‘— + 1)) โ‰ค 1
13897, 137nfim 1891 . . . . . . . . . . . 12 โ„ฒ๐‘–((๐œ‘ โˆง (๐‘— + 1) โˆˆ (๐ฟ...๐‘€)) โ†’ (๐ตโ€˜(๐‘— + 1)) โ‰ค 1)
139104breq1d 5162 . . . . . . . . . . . . 13 (๐‘– = (๐‘— + 1) โ†’ ((๐ตโ€˜๐‘–) โ‰ค 1 โ†” (๐ตโ€˜(๐‘— + 1)) โ‰ค 1))
140103, 139imbi12d 343 . . . . . . . . . . . 12 (๐‘– = (๐‘— + 1) โ†’ (((๐œ‘ โˆง ๐‘– โˆˆ (๐ฟ...๐‘€)) โ†’ (๐ตโ€˜๐‘–) โ‰ค 1) โ†” ((๐œ‘ โˆง (๐‘— + 1) โˆˆ (๐ฟ...๐‘€)) โ†’ (๐ตโ€˜(๐‘— + 1)) โ‰ค 1)))
141138, 140, 62vtoclg1f 3558 . . . . . . . . . . 11 ((๐‘— + 1) โˆˆ (๐ฟ...๐‘€) โ†’ ((๐œ‘ โˆง (๐‘— + 1) โˆˆ (๐ฟ...๐‘€)) โ†’ (๐ตโ€˜(๐‘— + 1)) โ‰ค 1))
14295, 136, 141sylc 65 . . . . . . . . . 10 ((๐‘— โˆˆ (๐ฟ..^๐‘€) โˆง (๐œ‘ โ†’ (0 โ‰ค (๐ดโ€˜๐‘—) โˆง (๐ดโ€˜๐‘—) โ‰ค 1)) โˆง ๐œ‘) โ†’ (๐ตโ€˜(๐‘— + 1)) โ‰ค 1)
143109, 135, 92, 116, 142lemul2ad 12192 . . . . . . . . 9 ((๐‘— โˆˆ (๐ฟ..^๐‘€) โˆง (๐œ‘ โ†’ (0 โ‰ค (๐ดโ€˜๐‘—) โˆง (๐ดโ€˜๐‘—) โ‰ค 1)) โˆง ๐œ‘) โ†’ ((seq๐ฟ( ยท , ๐ต)โ€˜๐‘—) ยท (๐ตโ€˜(๐‘— + 1))) โ‰ค ((seq๐ฟ( ยท , ๐ต)โ€˜๐‘—) ยท 1))
14492recnd 11280 . . . . . . . . . 10 ((๐‘— โˆˆ (๐ฟ..^๐‘€) โˆง (๐œ‘ โ†’ (0 โ‰ค (๐ดโ€˜๐‘—) โˆง (๐ดโ€˜๐‘—) โ‰ค 1)) โˆง ๐œ‘) โ†’ (seq๐ฟ( ยท , ๐ต)โ€˜๐‘—) โˆˆ โ„‚)
145144mulridd 11269 . . . . . . . . 9 ((๐‘— โˆˆ (๐ฟ..^๐‘€) โˆง (๐œ‘ โ†’ (0 โ‰ค (๐ดโ€˜๐‘—) โˆง (๐ดโ€˜๐‘—) โ‰ค 1)) โˆง ๐œ‘) โ†’ ((seq๐ฟ( ยท , ๐ต)โ€˜๐‘—) ยท 1) = (seq๐ฟ( ยท , ๐ต)โ€˜๐‘—))
146143, 145breqtrd 5178 . . . . . . . 8 ((๐‘— โˆˆ (๐ฟ..^๐‘€) โˆง (๐œ‘ โ†’ (0 โ‰ค (๐ดโ€˜๐‘—) โˆง (๐ดโ€˜๐‘—) โ‰ค 1)) โˆง ๐œ‘) โ†’ ((seq๐ฟ( ยท , ๐ต)โ€˜๐‘—) ยท (๐ตโ€˜(๐‘— + 1))) โ‰ค (seq๐ฟ( ยท , ๐ต)โ€˜๐‘—))
147 simp2 1134 . . . . . . . . . 10 ((๐‘— โˆˆ (๐ฟ..^๐‘€) โˆง (๐œ‘ โ†’ (0 โ‰ค (๐ดโ€˜๐‘—) โˆง (๐ดโ€˜๐‘—) โ‰ค 1)) โˆง ๐œ‘) โ†’ (๐œ‘ โ†’ (0 โ‰ค (๐ดโ€˜๐‘—) โˆง (๐ดโ€˜๐‘—) โ‰ค 1)))
148110simprd 494 . . . . . . . . . 10 ((๐œ‘ โˆง (๐œ‘ โ†’ (0 โ‰ค (๐ดโ€˜๐‘—) โˆง (๐ดโ€˜๐‘—) โ‰ค 1))) โ†’ (๐ดโ€˜๐‘—) โ‰ค 1)
14993, 147, 148syl2anc 582 . . . . . . . . 9 ((๐‘— โˆˆ (๐ฟ..^๐‘€) โˆง (๐œ‘ โ†’ (0 โ‰ค (๐ดโ€˜๐‘—) โˆง (๐ดโ€˜๐‘—) โ‰ค 1)) โˆง ๐œ‘) โ†’ (๐ดโ€˜๐‘—) โ‰ค 1)
150115, 149eqbrtrrid 5188 . . . . . . . 8 ((๐‘— โˆˆ (๐ฟ..^๐‘€) โˆง (๐œ‘ โ†’ (0 โ‰ค (๐ดโ€˜๐‘—) โˆง (๐ดโ€˜๐‘—) โ‰ค 1)) โˆง ๐œ‘) โ†’ (seq๐ฟ( ยท , ๐ต)โ€˜๐‘—) โ‰ค 1)
151134, 92, 135, 146, 150letrd 11409 . . . . . . 7 ((๐‘— โˆˆ (๐ฟ..^๐‘€) โˆง (๐œ‘ โ†’ (0 โ‰ค (๐ดโ€˜๐‘—) โˆง (๐ดโ€˜๐‘—) โ‰ค 1)) โˆง ๐œ‘) โ†’ ((seq๐ฟ( ยท , ๐ต)โ€˜๐‘—) ยท (๐ตโ€˜(๐‘— + 1))) โ‰ค 1)
152130, 151eqbrtrd 5174 . . . . . 6 ((๐‘— โˆˆ (๐ฟ..^๐‘€) โˆง (๐œ‘ โ†’ (0 โ‰ค (๐ดโ€˜๐‘—) โˆง (๐ดโ€˜๐‘—) โ‰ค 1)) โˆง ๐œ‘) โ†’ (seq๐ฟ( ยท , ๐ต)โ€˜(๐‘— + 1)) โ‰ค 1)
153132, 152eqbrtrid 5187 . . . . 5 ((๐‘— โˆˆ (๐ฟ..^๐‘€) โˆง (๐œ‘ โ†’ (0 โ‰ค (๐ดโ€˜๐‘—) โˆง (๐ดโ€˜๐‘—) โ‰ค 1)) โˆง ๐œ‘) โ†’ (๐ดโ€˜(๐‘— + 1)) โ‰ค 1)
154133, 153jca 510 . . . 4 ((๐‘— โˆˆ (๐ฟ..^๐‘€) โˆง (๐œ‘ โ†’ (0 โ‰ค (๐ดโ€˜๐‘—) โˆง (๐ดโ€˜๐‘—) โ‰ค 1)) โˆง ๐œ‘) โ†’ (0 โ‰ค (๐ดโ€˜(๐‘— + 1)) โˆง (๐ดโ€˜(๐‘— + 1)) โ‰ค 1))
1551543exp 1116 . . 3 (๐‘— โˆˆ (๐ฟ..^๐‘€) โ†’ ((๐œ‘ โ†’ (0 โ‰ค (๐ดโ€˜๐‘—) โˆง (๐ดโ€˜๐‘—) โ‰ค 1)) โ†’ (๐œ‘ โ†’ (0 โ‰ค (๐ดโ€˜(๐‘— + 1)) โˆง (๐ดโ€˜(๐‘— + 1)) โ‰ค 1))))
1566, 11, 16, 21, 67, 155fzind2 13790 . 2 (๐พ โˆˆ (๐ฟ...๐‘€) โ†’ (๐œ‘ โ†’ (0 โ‰ค (๐ดโ€˜๐พ) โˆง (๐ดโ€˜๐พ) โ‰ค 1)))
1571, 156mpcom 38 1 (๐œ‘ โ†’ (0 โ‰ค (๐ดโ€˜๐พ) โˆง (๐ดโ€˜๐พ) โ‰ค 1))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 394   โˆง w3a 1084   = wceq 1533  โ„ฒwnf 1777   โˆˆ wcel 2098  โ„ฒwnfc 2879   โІ wss 3949   class class class wbr 5152  โ€˜cfv 6553  (class class class)co 7426  โ„cr 11145  0cc0 11146  1c1 11147   + caddc 11149   ยท cmul 11151   โ‰ค cle 11287  โ„คcz 12596  โ„คโ‰ฅcuz 12860  ...cfz 13524  ..^cfzo 13667  seqcseq 14006
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2699  ax-sep 5303  ax-nul 5310  ax-pow 5369  ax-pr 5433  ax-un 7746  ax-cnex 11202  ax-resscn 11203  ax-1cn 11204  ax-icn 11205  ax-addcl 11206  ax-addrcl 11207  ax-mulcl 11208  ax-mulrcl 11209  ax-mulcom 11210  ax-addass 11211  ax-mulass 11212  ax-distr 11213  ax-i2m1 11214  ax-1ne0 11215  ax-1rid 11216  ax-rnegex 11217  ax-rrecex 11218  ax-cnre 11219  ax-pre-lttri 11220  ax-pre-lttrn 11221  ax-pre-ltadd 11222  ax-pre-mulgt0 11223
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-reu 3375  df-rab 3431  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-iun 5002  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6310  df-ord 6377  df-on 6378  df-lim 6379  df-suc 6380  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-riota 7382  df-ov 7429  df-oprab 7430  df-mpo 7431  df-om 7877  df-1st 7999  df-2nd 8000  df-frecs 8293  df-wrecs 8324  df-recs 8398  df-rdg 8437  df-er 8731  df-en 8971  df-dom 8972  df-sdom 8973  df-pnf 11288  df-mnf 11289  df-xr 11290  df-ltxr 11291  df-le 11292  df-sub 11484  df-neg 11485  df-nn 12251  df-n0 12511  df-z 12597  df-uz 12861  df-fz 13525  df-fzo 13668  df-seq 14007
This theorem is referenced by:  fmul01lt1lem1  45001  fmul01lt1lem2  45002
  Copyright terms: Public domain W3C validator