ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  lgsfcl2 GIF version

Theorem lgsfcl2 14595
Description: The function ๐น is closed in integers with absolute value less than 1 (namely {-1, 0, 1}, see zabsle1 14588). (Contributed by Mario Carneiro, 4-Feb-2015.)
Hypotheses
Ref Expression
lgsval.1 ๐น = (๐‘› โˆˆ โ„• โ†ฆ if(๐‘› โˆˆ โ„™, (if(๐‘› = 2, if(2 โˆฅ ๐ด, 0, if((๐ด mod 8) โˆˆ {1, 7}, 1, -1)), ((((๐ดโ†‘((๐‘› โˆ’ 1) / 2)) + 1) mod ๐‘›) โˆ’ 1))โ†‘(๐‘› pCnt ๐‘)), 1))
lgsfcl2.z ๐‘ = {๐‘ฅ โˆˆ โ„ค โˆฃ (absโ€˜๐‘ฅ) โ‰ค 1}
Assertion
Ref Expression
lgsfcl2 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โ†’ ๐น:โ„•โŸถ๐‘)
Distinct variable groups:   ๐ด,๐‘›,๐‘ฅ   ๐‘ฅ,๐น   ๐‘›,๐‘,๐‘ฅ   ๐‘›,๐‘
Allowed substitution hints:   ๐น(๐‘›)   ๐‘(๐‘ฅ)

Proof of Theorem lgsfcl2
Dummy variables ๐‘Ž ๐‘ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 0z 9267 . . . . . . . . 9 0 โˆˆ โ„ค
2 0le1 8441 . . . . . . . . 9 0 โ‰ค 1
3 fveq2 5517 . . . . . . . . . . . 12 (๐‘ฅ = 0 โ†’ (absโ€˜๐‘ฅ) = (absโ€˜0))
4 abs0 11070 . . . . . . . . . . . 12 (absโ€˜0) = 0
53, 4eqtrdi 2226 . . . . . . . . . . 11 (๐‘ฅ = 0 โ†’ (absโ€˜๐‘ฅ) = 0)
65breq1d 4015 . . . . . . . . . 10 (๐‘ฅ = 0 โ†’ ((absโ€˜๐‘ฅ) โ‰ค 1 โ†” 0 โ‰ค 1))
7 lgsfcl2.z . . . . . . . . . 10 ๐‘ = {๐‘ฅ โˆˆ โ„ค โˆฃ (absโ€˜๐‘ฅ) โ‰ค 1}
86, 7elrab2 2898 . . . . . . . . 9 (0 โˆˆ ๐‘ โ†” (0 โˆˆ โ„ค โˆง 0 โ‰ค 1))
91, 2, 8mpbir2an 942 . . . . . . . 8 0 โˆˆ ๐‘
109a1i 9 . . . . . . 7 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โ†’ 0 โˆˆ ๐‘)
11 1z 9282 . . . . . . . . . 10 1 โˆˆ โ„ค
12 1le1 8532 . . . . . . . . . 10 1 โ‰ค 1
13 fveq2 5517 . . . . . . . . . . . . 13 (๐‘ฅ = 1 โ†’ (absโ€˜๐‘ฅ) = (absโ€˜1))
14 abs1 11084 . . . . . . . . . . . . 13 (absโ€˜1) = 1
1513, 14eqtrdi 2226 . . . . . . . . . . . 12 (๐‘ฅ = 1 โ†’ (absโ€˜๐‘ฅ) = 1)
1615breq1d 4015 . . . . . . . . . . 11 (๐‘ฅ = 1 โ†’ ((absโ€˜๐‘ฅ) โ‰ค 1 โ†” 1 โ‰ค 1))
1716, 7elrab2 2898 . . . . . . . . . 10 (1 โˆˆ ๐‘ โ†” (1 โˆˆ โ„ค โˆง 1 โ‰ค 1))
1811, 12, 17mpbir2an 942 . . . . . . . . 9 1 โˆˆ ๐‘
1918a1i 9 . . . . . . . 8 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โ†’ 1 โˆˆ ๐‘)
20 neg1z 9288 . . . . . . . . . 10 -1 โˆˆ โ„ค
21 fveq2 5517 . . . . . . . . . . . . 13 (๐‘ฅ = -1 โ†’ (absโ€˜๐‘ฅ) = (absโ€˜-1))
22 ax-1cn 7907 . . . . . . . . . . . . . . 15 1 โˆˆ โ„‚
2322absnegi 11159 . . . . . . . . . . . . . 14 (absโ€˜-1) = (absโ€˜1)
2423, 14eqtri 2198 . . . . . . . . . . . . 13 (absโ€˜-1) = 1
2521, 24eqtrdi 2226 . . . . . . . . . . . 12 (๐‘ฅ = -1 โ†’ (absโ€˜๐‘ฅ) = 1)
2625breq1d 4015 . . . . . . . . . . 11 (๐‘ฅ = -1 โ†’ ((absโ€˜๐‘ฅ) โ‰ค 1 โ†” 1 โ‰ค 1))
2726, 7elrab2 2898 . . . . . . . . . 10 (-1 โˆˆ ๐‘ โ†” (-1 โˆˆ โ„ค โˆง 1 โ‰ค 1))
2820, 12, 27mpbir2an 942 . . . . . . . . 9 -1 โˆˆ ๐‘
2928a1i 9 . . . . . . . 8 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โ†’ -1 โˆˆ ๐‘)
30 simp1 997 . . . . . . . . . . . . 13 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โ†’ ๐ด โˆˆ โ„ค)
31 8nn 9089 . . . . . . . . . . . . . 14 8 โˆˆ โ„•
3231a1i 9 . . . . . . . . . . . . 13 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โ†’ 8 โˆˆ โ„•)
3330, 32zmodcld 10348 . . . . . . . . . . . 12 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โ†’ (๐ด mod 8) โˆˆ โ„•0)
3433nn0zd 9376 . . . . . . . . . . 11 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โ†’ (๐ด mod 8) โˆˆ โ„ค)
35 zdceq 9331 . . . . . . . . . . 11 (((๐ด mod 8) โˆˆ โ„ค โˆง 1 โˆˆ โ„ค) โ†’ DECID (๐ด mod 8) = 1)
3634, 11, 35sylancl 413 . . . . . . . . . 10 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โ†’ DECID (๐ด mod 8) = 1)
37 7nn 9088 . . . . . . . . . . . 12 7 โˆˆ โ„•
3837nnzi 9277 . . . . . . . . . . 11 7 โˆˆ โ„ค
39 zdceq 9331 . . . . . . . . . . 11 (((๐ด mod 8) โˆˆ โ„ค โˆง 7 โˆˆ โ„ค) โ†’ DECID (๐ด mod 8) = 7)
4034, 38, 39sylancl 413 . . . . . . . . . 10 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โ†’ DECID (๐ด mod 8) = 7)
41 dcor 935 . . . . . . . . . 10 (DECID (๐ด mod 8) = 1 โ†’ (DECID (๐ด mod 8) = 7 โ†’ DECID ((๐ด mod 8) = 1 โˆจ (๐ด mod 8) = 7)))
4236, 40, 41sylc 62 . . . . . . . . 9 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โ†’ DECID ((๐ด mod 8) = 1 โˆจ (๐ด mod 8) = 7))
43 elprg 3614 . . . . . . . . . . 11 ((๐ด mod 8) โˆˆ โ„•0 โ†’ ((๐ด mod 8) โˆˆ {1, 7} โ†” ((๐ด mod 8) = 1 โˆจ (๐ด mod 8) = 7)))
4433, 43syl 14 . . . . . . . . . 10 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โ†’ ((๐ด mod 8) โˆˆ {1, 7} โ†” ((๐ด mod 8) = 1 โˆจ (๐ด mod 8) = 7)))
4544dcbid 838 . . . . . . . . 9 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โ†’ (DECID (๐ด mod 8) โˆˆ {1, 7} โ†” DECID ((๐ด mod 8) = 1 โˆจ (๐ด mod 8) = 7)))
4642, 45mpbird 167 . . . . . . . 8 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โ†’ DECID (๐ด mod 8) โˆˆ {1, 7})
4719, 29, 46ifcldcd 3572 . . . . . . 7 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โ†’ if((๐ด mod 8) โˆˆ {1, 7}, 1, -1) โˆˆ ๐‘)
48 2nn 9083 . . . . . . . . 9 2 โˆˆ โ„•
4948a1i 9 . . . . . . . 8 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โ†’ 2 โˆˆ โ„•)
50 dvdsdc 11808 . . . . . . . 8 ((2 โˆˆ โ„• โˆง ๐ด โˆˆ โ„ค) โ†’ DECID 2 โˆฅ ๐ด)
5149, 30, 50syl2anc 411 . . . . . . 7 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โ†’ DECID 2 โˆฅ ๐ด)
5210, 47, 51ifcldcd 3572 . . . . . 6 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โ†’ if(2 โˆฅ ๐ด, 0, if((๐ด mod 8) โˆˆ {1, 7}, 1, -1)) โˆˆ ๐‘)
5352ad3antrrr 492 . . . . 5 (((((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โˆง ๐‘› โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„™) โˆง ๐‘› = 2) โ†’ if(2 โˆฅ ๐ด, 0, if((๐ด mod 8) โˆˆ {1, 7}, 1, -1)) โˆˆ ๐‘)
54 simpl1 1000 . . . . . . 7 (((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โˆง ๐‘› โˆˆ โ„•) โ†’ ๐ด โˆˆ โ„ค)
5554ad2antrr 488 . . . . . 6 (((((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โˆง ๐‘› โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„™) โˆง ยฌ ๐‘› = 2) โ†’ ๐ด โˆˆ โ„ค)
56 simplr 528 . . . . . . 7 (((((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โˆง ๐‘› โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„™) โˆง ยฌ ๐‘› = 2) โ†’ ๐‘› โˆˆ โ„™)
57 simpr 110 . . . . . . . 8 (((((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โˆง ๐‘› โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„™) โˆง ยฌ ๐‘› = 2) โ†’ ยฌ ๐‘› = 2)
5857neqned 2354 . . . . . . 7 (((((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โˆง ๐‘› โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„™) โˆง ยฌ ๐‘› = 2) โ†’ ๐‘› โ‰  2)
59 eldifsn 3721 . . . . . . 7 (๐‘› โˆˆ (โ„™ โˆ– {2}) โ†” (๐‘› โˆˆ โ„™ โˆง ๐‘› โ‰  2))
6056, 58, 59sylanbrc 417 . . . . . 6 (((((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โˆง ๐‘› โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„™) โˆง ยฌ ๐‘› = 2) โ†’ ๐‘› โˆˆ (โ„™ โˆ– {2}))
617lgslem4 14592 . . . . . 6 ((๐ด โˆˆ โ„ค โˆง ๐‘› โˆˆ (โ„™ โˆ– {2})) โ†’ ((((๐ดโ†‘((๐‘› โˆ’ 1) / 2)) + 1) mod ๐‘›) โˆ’ 1) โˆˆ ๐‘)
6255, 60, 61syl2anc 411 . . . . 5 (((((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โˆง ๐‘› โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„™) โˆง ยฌ ๐‘› = 2) โ†’ ((((๐ดโ†‘((๐‘› โˆ’ 1) / 2)) + 1) mod ๐‘›) โˆ’ 1) โˆˆ ๐‘)
63 simplr 528 . . . . . . 7 ((((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โˆง ๐‘› โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„™) โ†’ ๐‘› โˆˆ โ„•)
6463nnzd 9377 . . . . . 6 ((((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โˆง ๐‘› โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„™) โ†’ ๐‘› โˆˆ โ„ค)
65 2z 9284 . . . . . 6 2 โˆˆ โ„ค
66 zdceq 9331 . . . . . 6 ((๐‘› โˆˆ โ„ค โˆง 2 โˆˆ โ„ค) โ†’ DECID ๐‘› = 2)
6764, 65, 66sylancl 413 . . . . 5 ((((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โˆง ๐‘› โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„™) โ†’ DECID ๐‘› = 2)
6853, 62, 67ifcldadc 3565 . . . 4 ((((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โˆง ๐‘› โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„™) โ†’ if(๐‘› = 2, if(2 โˆฅ ๐ด, 0, if((๐ด mod 8) โˆˆ {1, 7}, 1, -1)), ((((๐ดโ†‘((๐‘› โˆ’ 1) / 2)) + 1) mod ๐‘›) โˆ’ 1)) โˆˆ ๐‘)
69 simpr 110 . . . . 5 ((((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โˆง ๐‘› โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„™) โ†’ ๐‘› โˆˆ โ„™)
70 simpll2 1037 . . . . 5 ((((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โˆง ๐‘› โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„™) โ†’ ๐‘ โˆˆ โ„ค)
71 simpll3 1038 . . . . 5 ((((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โˆง ๐‘› โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„™) โ†’ ๐‘ โ‰  0)
72 pczcl 12301 . . . . 5 ((๐‘› โˆˆ โ„™ โˆง (๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0)) โ†’ (๐‘› pCnt ๐‘) โˆˆ โ„•0)
7369, 70, 71, 72syl12anc 1236 . . . 4 ((((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โˆง ๐‘› โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„™) โ†’ (๐‘› pCnt ๐‘) โˆˆ โ„•0)
747ssrab3 3243 . . . . . 6 ๐‘ โІ โ„ค
75 zsscn 9264 . . . . . 6 โ„ค โІ โ„‚
7674, 75sstri 3166 . . . . 5 ๐‘ โІ โ„‚
777lgslem3 14591 . . . . 5 ((๐‘Ž โˆˆ ๐‘ โˆง ๐‘ โˆˆ ๐‘) โ†’ (๐‘Ž ยท ๐‘) โˆˆ ๐‘)
7876, 77, 18expcllem 10534 . . . 4 ((if(๐‘› = 2, if(2 โˆฅ ๐ด, 0, if((๐ด mod 8) โˆˆ {1, 7}, 1, -1)), ((((๐ดโ†‘((๐‘› โˆ’ 1) / 2)) + 1) mod ๐‘›) โˆ’ 1)) โˆˆ ๐‘ โˆง (๐‘› pCnt ๐‘) โˆˆ โ„•0) โ†’ (if(๐‘› = 2, if(2 โˆฅ ๐ด, 0, if((๐ด mod 8) โˆˆ {1, 7}, 1, -1)), ((((๐ดโ†‘((๐‘› โˆ’ 1) / 2)) + 1) mod ๐‘›) โˆ’ 1))โ†‘(๐‘› pCnt ๐‘)) โˆˆ ๐‘)
7968, 73, 78syl2anc 411 . . 3 ((((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โˆง ๐‘› โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„™) โ†’ (if(๐‘› = 2, if(2 โˆฅ ๐ด, 0, if((๐ด mod 8) โˆˆ {1, 7}, 1, -1)), ((((๐ดโ†‘((๐‘› โˆ’ 1) / 2)) + 1) mod ๐‘›) โˆ’ 1))โ†‘(๐‘› pCnt ๐‘)) โˆˆ ๐‘)
8018a1i 9 . . 3 ((((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘› โˆˆ โ„™) โ†’ 1 โˆˆ ๐‘)
81 simpr 110 . . . 4 (((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โˆง ๐‘› โˆˆ โ„•) โ†’ ๐‘› โˆˆ โ„•)
82 prmdc 12133 . . . 4 (๐‘› โˆˆ โ„• โ†’ DECID ๐‘› โˆˆ โ„™)
8381, 82syl 14 . . 3 (((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โˆง ๐‘› โˆˆ โ„•) โ†’ DECID ๐‘› โˆˆ โ„™)
8479, 80, 83ifcldadc 3565 . 2 (((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โˆง ๐‘› โˆˆ โ„•) โ†’ if(๐‘› โˆˆ โ„™, (if(๐‘› = 2, if(2 โˆฅ ๐ด, 0, if((๐ด mod 8) โˆˆ {1, 7}, 1, -1)), ((((๐ดโ†‘((๐‘› โˆ’ 1) / 2)) + 1) mod ๐‘›) โˆ’ 1))โ†‘(๐‘› pCnt ๐‘)), 1) โˆˆ ๐‘)
85 lgsval.1 . 2 ๐น = (๐‘› โˆˆ โ„• โ†ฆ if(๐‘› โˆˆ โ„™, (if(๐‘› = 2, if(2 โˆฅ ๐ด, 0, if((๐ด mod 8) โˆˆ {1, 7}, 1, -1)), ((((๐ดโ†‘((๐‘› โˆ’ 1) / 2)) + 1) mod ๐‘›) โˆ’ 1))โ†‘(๐‘› pCnt ๐‘)), 1))
8684, 85fmptd 5673 1 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โ†’ ๐น:โ„•โŸถ๐‘)
Colors of variables: wff set class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โˆง wa 104   โ†” wb 105   โˆจ wo 708  DECID wdc 834   โˆง w3a 978   = wceq 1353   โˆˆ wcel 2148   โ‰  wne 2347  {crab 2459   โˆ– cdif 3128  ifcif 3536  {csn 3594  {cpr 3595   class class class wbr 4005   โ†ฆ cmpt 4066  โŸถwf 5214  โ€˜cfv 5218  (class class class)co 5878  โ„‚cc 7812  0cc0 7814  1c1 7815   + caddc 7817   โ‰ค cle 7996   โˆ’ cmin 8131  -cneg 8132   / cdiv 8632  โ„•cn 8922  2c2 8973  7c7 8978  8c8 8979  โ„•0cn0 9179  โ„คcz 9256   mod cmo 10325  โ†‘cexp 10522  abscabs 11009   โˆฅ cdvds 11797  โ„™cprime 12110   pCnt cpc 12287
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 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4120  ax-sep 4123  ax-nul 4131  ax-pow 4176  ax-pr 4211  ax-un 4435  ax-setind 4538  ax-iinf 4589  ax-cnex 7905  ax-resscn 7906  ax-1cn 7907  ax-1re 7908  ax-icn 7909  ax-addcl 7910  ax-addrcl 7911  ax-mulcl 7912  ax-mulrcl 7913  ax-addcom 7914  ax-mulcom 7915  ax-addass 7916  ax-mulass 7917  ax-distr 7918  ax-i2m1 7919  ax-0lt1 7920  ax-1rid 7921  ax-0id 7922  ax-rnegex 7923  ax-precex 7924  ax-cnre 7925  ax-pre-ltirr 7926  ax-pre-ltwlin 7927  ax-pre-lttrn 7928  ax-pre-apti 7929  ax-pre-ltadd 7930  ax-pre-mulgt0 7931  ax-pre-mulext 7932  ax-arch 7933  ax-caucvg 7934
This theorem depends on definitions:  df-bi 117  df-stab 831  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-xor 1376  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-reu 2462  df-rmo 2463  df-rab 2464  df-v 2741  df-sbc 2965  df-csb 3060  df-dif 3133  df-un 3135  df-in 3137  df-ss 3144  df-nul 3425  df-if 3537  df-pw 3579  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-int 3847  df-iun 3890  df-br 4006  df-opab 4067  df-mpt 4068  df-tr 4104  df-id 4295  df-po 4298  df-iso 4299  df-iord 4368  df-on 4370  df-ilim 4371  df-suc 4373  df-iom 4592  df-xp 4634  df-rel 4635  df-cnv 4636  df-co 4637  df-dm 4638  df-rn 4639  df-res 4640  df-ima 4641  df-iota 5180  df-fun 5220  df-fn 5221  df-f 5222  df-f1 5223  df-fo 5224  df-f1o 5225  df-fv 5226  df-isom 5227  df-riota 5834  df-ov 5881  df-oprab 5882  df-mpo 5883  df-1st 6144  df-2nd 6145  df-recs 6309  df-irdg 6374  df-frec 6395  df-1o 6420  df-2o 6421  df-oadd 6424  df-er 6538  df-en 6744  df-dom 6745  df-fin 6746  df-sup 6986  df-inf 6987  df-pnf 7997  df-mnf 7998  df-xr 7999  df-ltxr 8000  df-le 8001  df-sub 8133  df-neg 8134  df-reap 8535  df-ap 8542  df-div 8633  df-inn 8923  df-2 8981  df-3 8982  df-4 8983  df-5 8984  df-6 8985  df-7 8986  df-8 8987  df-n0 9180  df-z 9257  df-uz 9532  df-q 9623  df-rp 9657  df-fz 10012  df-fzo 10146  df-fl 10273  df-mod 10326  df-seqfrec 10449  df-exp 10523  df-ihash 10759  df-cj 10854  df-re 10855  df-im 10856  df-rsqrt 11010  df-abs 11011  df-clim 11290  df-proddc 11562  df-dvds 11798  df-gcd 11947  df-prm 12111  df-phi 12214  df-pc 12288
This theorem is referenced by:  lgscllem  14596  lgsfcl  14597  lgsfle1  14598
  Copyright terms: Public domain W3C validator