ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mulgval GIF version
Theorem mulgval 12986
Description: Value of the group multiple (exponentiation) operation. (Contributed by Mario Carneiro, 11-Dec-2014.)
Hypotheses
Ref Expression
mulgval.b 𝐡 = (Baseβ€˜πΊ)
mulgval.p + = (+gβ€˜πΊ)
mulgval.o 0 = (0gβ€˜πΊ)
mulgval.i 𝐼 = (invgβ€˜πΊ)
mulgval.t Β· = (.gβ€˜πΊ)
mulgval.s 𝑆 = seq1( + , (β„• Γ— {𝑋}))
Assertion
Ref Expression
mulgval ((𝑁 ∈ β„€ ∧ 𝑋 ∈ 𝐡) β†’ (𝑁 Β· 𝑋) = if(𝑁 = 0, 0 , if(0 < 𝑁, (π‘†β€˜π‘), (πΌβ€˜(π‘†β€˜-𝑁)))))
Proof of Theorem mulgval
Dummy variables π‘₯ 𝑛 𝑒 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mulgval.b . . . 4 𝐡 = (Baseβ€˜πΊ)
21basmex 12521 . . 3 (𝑋 ∈ 𝐡 β†’ 𝐺 ∈ V)
32adantl 277 . 2 ((𝑁 ∈ β„€ ∧ 𝑋 ∈ 𝐡) β†’ 𝐺 ∈ V)
4 mulgval.p . . . . 5 + = (+gβ€˜πΊ)
5 mulgval.o . . . . 5 0 = (0gβ€˜πΊ)
6 mulgval.i . . . . 5 𝐼 = (invgβ€˜πΊ)
7 mulgval.t . . . . 5 Β· = (.gβ€˜πΊ)
81, 4, 5, 6, 7mulgfvalg 12985 . . . 4 (𝐺 ∈ V β†’ Β· = (𝑛 ∈ β„€, π‘₯ ∈ 𝐡 ↦ if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (β„• Γ— {π‘₯}))β€˜π‘›), (πΌβ€˜(seq1( + , (β„• Γ— {π‘₯}))β€˜-𝑛))))))
98adantl 277 . . 3 (((𝑁 ∈ β„€ ∧ 𝑋 ∈ 𝐡) ∧ 𝐺 ∈ V) β†’ Β· = (𝑛 ∈ β„€, π‘₯ ∈ 𝐡 ↦ if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (β„• Γ— {π‘₯}))β€˜π‘›), (πΌβ€˜(seq1( + , (β„• Γ— {π‘₯}))β€˜-𝑛))))))
10 simpl 109 . . . . . 6 ((𝑛 = 𝑁 ∧ π‘₯ = 𝑋) β†’ 𝑛 = 𝑁)
1110eqeq1d 2186 . . . . 5 ((𝑛 = 𝑁 ∧ π‘₯ = 𝑋) β†’ (𝑛 = 0 ↔ 𝑁 = 0))
1210breq2d 4016 . . . . . 6 ((𝑛 = 𝑁 ∧ π‘₯ = 𝑋) β†’ (0 < 𝑛 ↔ 0 < 𝑁))
13 simpr 110 . . . . . . . . . . 11 ((𝑛 = 𝑁 ∧ π‘₯ = 𝑋) β†’ π‘₯ = 𝑋)
1413sneqd 3606 . . . . . . . . . 10 ((𝑛 = 𝑁 ∧ π‘₯ = 𝑋) β†’ {π‘₯} = {𝑋})
1514xpeq2d 4651 . . . . . . . . 9 ((𝑛 = 𝑁 ∧ π‘₯ = 𝑋) β†’ (β„• Γ— {π‘₯}) = (β„• Γ— {𝑋}))
1615seqeq3d 10453 . . . . . . . 8 ((𝑛 = 𝑁 ∧ π‘₯ = 𝑋) β†’ seq1( + , (β„• Γ— {π‘₯})) = seq1( + , (β„• Γ— {𝑋})))
17 mulgval.s . . . . . . . 8 𝑆 = seq1( + , (β„• Γ— {𝑋}))
1816, 17eqtr4di 2228 . . . . . . 7 ((𝑛 = 𝑁 ∧ π‘₯ = 𝑋) β†’ seq1( + , (β„• Γ— {π‘₯})) = 𝑆)
1918, 10fveq12d 5523 . . . . . 6 ((𝑛 = 𝑁 ∧ π‘₯ = 𝑋) β†’ (seq1( + , (β„• Γ— {π‘₯}))β€˜π‘›) = (π‘†β€˜π‘))
2010negeqd 8152 . . . . . . . 8 ((𝑛 = 𝑁 ∧ π‘₯ = 𝑋) β†’ -𝑛 = -𝑁)
2118, 20fveq12d 5523 . . . . . . 7 ((𝑛 = 𝑁 ∧ π‘₯ = 𝑋) β†’ (seq1( + , (β„• Γ— {π‘₯}))β€˜-𝑛) = (π‘†β€˜-𝑁))
2221fveq2d 5520 . . . . . 6 ((𝑛 = 𝑁 ∧ π‘₯ = 𝑋) β†’ (πΌβ€˜(seq1( + , (β„• Γ— {π‘₯}))β€˜-𝑛)) = (πΌβ€˜(π‘†β€˜-𝑁)))
2312, 19, 22ifbieq12d 3561 . . . . 5 ((𝑛 = 𝑁 ∧ π‘₯ = 𝑋) β†’ if(0 < 𝑛, (seq1( + , (β„• Γ— {π‘₯}))β€˜π‘›), (πΌβ€˜(seq1( + , (β„• Γ— {π‘₯}))β€˜-𝑛))) = if(0 < 𝑁, (π‘†β€˜π‘), (πΌβ€˜(π‘†β€˜-𝑁))))
2411, 23ifbieq2d 3559 . . . 4 ((𝑛 = 𝑁 ∧ π‘₯ = 𝑋) β†’ if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (β„• Γ— {π‘₯}))β€˜π‘›), (πΌβ€˜(seq1( + , (β„• Γ— {π‘₯}))β€˜-𝑛)))) = if(𝑁 = 0, 0 , if(0 < 𝑁, (π‘†β€˜π‘), (πΌβ€˜(π‘†β€˜-𝑁)))))
2524adantl 277 . . 3 ((((𝑁 ∈ β„€ ∧ 𝑋 ∈ 𝐡) ∧ 𝐺 ∈ V) ∧ (𝑛 = 𝑁 ∧ π‘₯ = 𝑋)) β†’ if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (β„• Γ— {π‘₯}))β€˜π‘›), (πΌβ€˜(seq1( + , (β„• Γ— {π‘₯}))β€˜-𝑛)))) = if(𝑁 = 0, 0 , if(0 < 𝑁, (π‘†β€˜π‘), (πΌβ€˜(π‘†β€˜-𝑁)))))
26 simpll 527 . . 3 (((𝑁 ∈ β„€ ∧ 𝑋 ∈ 𝐡) ∧ 𝐺 ∈ V) β†’ 𝑁 ∈ β„€)
27 simplr 528 . . 3 (((𝑁 ∈ β„€ ∧ 𝑋 ∈ 𝐡) ∧ 𝐺 ∈ V) β†’ 𝑋 ∈ 𝐡)
28 fn0g 12794 . . . . . . 7 0g Fn V
29 funfvex 5533 . . . . . . . 8 ((Fun 0g ∧ 𝐺 ∈ dom 0g) β†’ (0gβ€˜πΊ) ∈ V)
3029funfni 5317 . . . . . . 7 ((0g Fn V ∧ 𝐺 ∈ V) β†’ (0gβ€˜πΊ) ∈ V)
3128, 30mpan 424 . . . . . 6 (𝐺 ∈ V β†’ (0gβ€˜πΊ) ∈ V)
325, 31eqeltrid 2264 . . . . 5 (𝐺 ∈ V β†’ 0 ∈ V)
3332ad2antlr 489 . . . 4 ((((𝑁 ∈ β„€ ∧ 𝑋 ∈ 𝐡) ∧ 𝐺 ∈ V) ∧ 𝑁 = 0) β†’ 0 ∈ V)
34 nnuz 9563 . . . . . . . . 9 β„• = (β„€β‰₯β€˜1)
35 1zzd 9280 . . . . . . . . 9 ((𝑋 ∈ 𝐡 ∧ 𝐺 ∈ V) β†’ 1 ∈ β„€)
36 fvconst2g 5731 . . . . . . . . . . . 12 ((𝑋 ∈ 𝐡 ∧ 𝑒 ∈ β„•) β†’ ((β„• Γ— {𝑋})β€˜π‘’) = 𝑋)
37 simpl 109 . . . . . . . . . . . 12 ((𝑋 ∈ 𝐡 ∧ 𝑒 ∈ β„•) β†’ 𝑋 ∈ 𝐡)
3836, 37eqeltrd 2254 . . . . . . . . . . 11 ((𝑋 ∈ 𝐡 ∧ 𝑒 ∈ β„•) β†’ ((β„• Γ— {𝑋})β€˜π‘’) ∈ 𝐡)
3938elexd 2751 . . . . . . . . . 10 ((𝑋 ∈ 𝐡 ∧ 𝑒 ∈ β„•) β†’ ((β„• Γ— {𝑋})β€˜π‘’) ∈ V)
4039adantlr 477 . . . . . . . . 9 (((𝑋 ∈ 𝐡 ∧ 𝐺 ∈ V) ∧ 𝑒 ∈ β„•) β†’ ((β„• Γ— {𝑋})β€˜π‘’) ∈ V)
41 simprl 529 . . . . . . . . . 10 (((𝑋 ∈ 𝐡 ∧ 𝐺 ∈ V) ∧ (𝑒 ∈ V ∧ 𝑣 ∈ V)) β†’ 𝑒 ∈ V)
42 plusgslid 12571 . . . . . . . . . . . . 13 (+g = Slot (+gβ€˜ndx) ∧ (+gβ€˜ndx) ∈ β„•)
4342slotex 12489 . . . . . . . . . . . 12 (𝐺 ∈ V β†’ (+gβ€˜πΊ) ∈ V)
444, 43eqeltrid 2264 . . . . . . . . . . 11 (𝐺 ∈ V β†’ + ∈ V)
4544ad2antlr 489 . . . . . . . . . 10 (((𝑋 ∈ 𝐡 ∧ 𝐺 ∈ V) ∧ (𝑒 ∈ V ∧ 𝑣 ∈ V)) β†’ + ∈ V)
46 simprr 531 . . . . . . . . . 10 (((𝑋 ∈ 𝐡 ∧ 𝐺 ∈ V) ∧ (𝑒 ∈ V ∧ 𝑣 ∈ V)) β†’ 𝑣 ∈ V)
47 ovexg 5909 . . . . . . . . . 10 ((𝑒 ∈ V ∧ + ∈ V ∧ 𝑣 ∈ V) β†’ (𝑒 + 𝑣) ∈ V)
4841, 45, 46, 47syl3anc 1238 . . . . . . . . 9 (((𝑋 ∈ 𝐡 ∧ 𝐺 ∈ V) ∧ (𝑒 ∈ V ∧ 𝑣 ∈ V)) β†’ (𝑒 + 𝑣) ∈ V)
4934, 35, 40, 48seqf 10461 . . . . . . . 8 ((𝑋 ∈ 𝐡 ∧ 𝐺 ∈ V) β†’ seq1( + , (β„• Γ— {𝑋})):β„•βŸΆV)
5017feq1i 5359 . . . . . . . 8 (𝑆:β„•βŸΆV ↔ seq1( + , (β„• Γ— {𝑋})):β„•βŸΆV)
5149, 50sylibr 134 . . . . . . 7 ((𝑋 ∈ 𝐡 ∧ 𝐺 ∈ V) β†’ 𝑆:β„•βŸΆV)
5251ad5ant23 522 . . . . . 6 (((((𝑁 ∈ β„€ ∧ 𝑋 ∈ 𝐡) ∧ 𝐺 ∈ V) ∧ Β¬ 𝑁 = 0) ∧ 0 < 𝑁) β†’ 𝑆:β„•βŸΆV)
53 simp-4l 541 . . . . . . 7 (((((𝑁 ∈ β„€ ∧ 𝑋 ∈ 𝐡) ∧ 𝐺 ∈ V) ∧ Β¬ 𝑁 = 0) ∧ 0 < 𝑁) β†’ 𝑁 ∈ β„€)
54 simpr 110 . . . . . . 7 (((((𝑁 ∈ β„€ ∧ 𝑋 ∈ 𝐡) ∧ 𝐺 ∈ V) ∧ Β¬ 𝑁 = 0) ∧ 0 < 𝑁) β†’ 0 < 𝑁)
55 elnnz 9263 . . . . . . 7 (𝑁 ∈ β„• ↔ (𝑁 ∈ β„€ ∧ 0 < 𝑁))
5653, 54, 55sylanbrc 417 . . . . . 6 (((((𝑁 ∈ β„€ ∧ 𝑋 ∈ 𝐡) ∧ 𝐺 ∈ V) ∧ Β¬ 𝑁 = 0) ∧ 0 < 𝑁) β†’ 𝑁 ∈ β„•)
5752, 56ffvelcdmd 5653 . . . . 5 (((((𝑁 ∈ β„€ ∧ 𝑋 ∈ 𝐡) ∧ 𝐺 ∈ V) ∧ Β¬ 𝑁 = 0) ∧ 0 < 𝑁) β†’ (π‘†β€˜π‘) ∈ V)
581, 6grpinvfng 12917 . . . . . . . 8 (𝐺 ∈ V β†’ 𝐼 Fn 𝐡)
59 basfn 12520 . . . . . . . . . 10 Base Fn V
60 funfvex 5533 . . . . . . . . . . 11 ((Fun Base ∧ 𝐺 ∈ dom Base) β†’ (Baseβ€˜πΊ) ∈ V)
6160funfni 5317 . . . . . . . . . 10 ((Base Fn V ∧ 𝐺 ∈ V) β†’ (Baseβ€˜πΊ) ∈ V)
6259, 61mpan 424 . . . . . . . . 9 (𝐺 ∈ V β†’ (Baseβ€˜πΊ) ∈ V)
631, 62eqeltrid 2264 . . . . . . . 8 (𝐺 ∈ V β†’ 𝐡 ∈ V)
64 fnex 5739 . . . . . . . 8 ((𝐼 Fn 𝐡 ∧ 𝐡 ∈ V) β†’ 𝐼 ∈ V)
6558, 63, 64syl2anc 411 . . . . . . 7 (𝐺 ∈ V β†’ 𝐼 ∈ V)
6665ad3antlr 493 . . . . . 6 (((((𝑁 ∈ β„€ ∧ 𝑋 ∈ 𝐡) ∧ 𝐺 ∈ V) ∧ Β¬ 𝑁 = 0) ∧ Β¬ 0 < 𝑁) β†’ 𝐼 ∈ V)
6751ad5ant23 522 . . . . . . 7 (((((𝑁 ∈ β„€ ∧ 𝑋 ∈ 𝐡) ∧ 𝐺 ∈ V) ∧ Β¬ 𝑁 = 0) ∧ Β¬ 0 < 𝑁) β†’ 𝑆:β„•βŸΆV)
68 znegcl 9284 . . . . . . . . 9 (𝑁 ∈ β„€ β†’ -𝑁 ∈ β„€)
6968ad4antr 494 . . . . . . . 8 (((((𝑁 ∈ β„€ ∧ 𝑋 ∈ 𝐡) ∧ 𝐺 ∈ V) ∧ Β¬ 𝑁 = 0) ∧ Β¬ 0 < 𝑁) β†’ -𝑁 ∈ β„€)
70 simplr 528 . . . . . . . . . 10 (((((𝑁 ∈ β„€ ∧ 𝑋 ∈ 𝐡) ∧ 𝐺 ∈ V) ∧ Β¬ 𝑁 = 0) ∧ Β¬ 0 < 𝑁) β†’ Β¬ 𝑁 = 0)
71 simpr 110 . . . . . . . . . 10 (((((𝑁 ∈ β„€ ∧ 𝑋 ∈ 𝐡) ∧ 𝐺 ∈ V) ∧ Β¬ 𝑁 = 0) ∧ Β¬ 0 < 𝑁) β†’ Β¬ 0 < 𝑁)
72 ztri3or0 9295 . . . . . . . . . . 11 (𝑁 ∈ β„€ β†’ (𝑁 < 0 ∨ 𝑁 = 0 ∨ 0 < 𝑁))
7372ad4antr 494 . . . . . . . . . 10 (((((𝑁 ∈ β„€ ∧ 𝑋 ∈ 𝐡) ∧ 𝐺 ∈ V) ∧ Β¬ 𝑁 = 0) ∧ Β¬ 0 < 𝑁) β†’ (𝑁 < 0 ∨ 𝑁 = 0 ∨ 0 < 𝑁))
7470, 71, 73ecase23d 1350 . . . . . . . . 9 (((((𝑁 ∈ β„€ ∧ 𝑋 ∈ 𝐡) ∧ 𝐺 ∈ V) ∧ Β¬ 𝑁 = 0) ∧ Β¬ 0 < 𝑁) β†’ 𝑁 < 0)
75 zre 9257 . . . . . . . . . . 11 (𝑁 ∈ β„€ β†’ 𝑁 ∈ ℝ)
7675ad4antr 494 . . . . . . . . . 10 (((((𝑁 ∈ β„€ ∧ 𝑋 ∈ 𝐡) ∧ 𝐺 ∈ V) ∧ Β¬ 𝑁 = 0) ∧ Β¬ 0 < 𝑁) β†’ 𝑁 ∈ ℝ)
7776lt0neg1d 8472 . . . . . . . . 9 (((((𝑁 ∈ β„€ ∧ 𝑋 ∈ 𝐡) ∧ 𝐺 ∈ V) ∧ Β¬ 𝑁 = 0) ∧ Β¬ 0 < 𝑁) β†’ (𝑁 < 0 ↔ 0 < -𝑁))
7874, 77mpbid 147 . . . . . . . 8 (((((𝑁 ∈ β„€ ∧ 𝑋 ∈ 𝐡) ∧ 𝐺 ∈ V) ∧ Β¬ 𝑁 = 0) ∧ Β¬ 0 < 𝑁) β†’ 0 < -𝑁)
79 elnnz 9263 . . . . . . . 8 (-𝑁 ∈ β„• ↔ (-𝑁 ∈ β„€ ∧ 0 < -𝑁))
8069, 78, 79sylanbrc 417 . . . . . . 7 (((((𝑁 ∈ β„€ ∧ 𝑋 ∈ 𝐡) ∧ 𝐺 ∈ V) ∧ Β¬ 𝑁 = 0) ∧ Β¬ 0 < 𝑁) β†’ -𝑁 ∈ β„•)
8167, 80ffvelcdmd 5653 . . . . . 6 (((((𝑁 ∈ β„€ ∧ 𝑋 ∈ 𝐡) ∧ 𝐺 ∈ V) ∧ Β¬ 𝑁 = 0) ∧ Β¬ 0 < 𝑁) β†’ (π‘†β€˜-𝑁) ∈ V)
82 fvexg 5535 . . . . . 6 ((𝐼 ∈ V ∧ (π‘†β€˜-𝑁) ∈ V) β†’ (πΌβ€˜(π‘†β€˜-𝑁)) ∈ V)
8366, 81, 82syl2anc 411 . . . . 5 (((((𝑁 ∈ β„€ ∧ 𝑋 ∈ 𝐡) ∧ 𝐺 ∈ V) ∧ Β¬ 𝑁 = 0) ∧ Β¬ 0 < 𝑁) β†’ (πΌβ€˜(π‘†β€˜-𝑁)) ∈ V)
84 0zd 9265 . . . . . 6 ((((𝑁 ∈ β„€ ∧ 𝑋 ∈ 𝐡) ∧ 𝐺 ∈ V) ∧ Β¬ 𝑁 = 0) β†’ 0 ∈ β„€)
85 simplll 533 . . . . . 6 ((((𝑁 ∈ β„€ ∧ 𝑋 ∈ 𝐡) ∧ 𝐺 ∈ V) ∧ Β¬ 𝑁 = 0) β†’ 𝑁 ∈ β„€)
86 zdclt 9330 . . . . . 6 ((0 ∈ β„€ ∧ 𝑁 ∈ β„€) β†’ DECID 0 < 𝑁)
8784, 85, 86syl2anc 411 . . . . 5 ((((𝑁 ∈ β„€ ∧ 𝑋 ∈ 𝐡) ∧ 𝐺 ∈ V) ∧ Β¬ 𝑁 = 0) β†’ DECID 0 < 𝑁)
8857, 83, 87ifcldadc 3564 . . . 4 ((((𝑁 ∈ β„€ ∧ 𝑋 ∈ 𝐡) ∧ 𝐺 ∈ V) ∧ Β¬ 𝑁 = 0) β†’ if(0 < 𝑁, (π‘†β€˜π‘), (πΌβ€˜(π‘†β€˜-𝑁))) ∈ V)
89 0zd 9265 . . . . 5 (((𝑁 ∈ β„€ ∧ 𝑋 ∈ 𝐡) ∧ 𝐺 ∈ V) β†’ 0 ∈ β„€)
90 zdceq 9328 . . . . 5 ((𝑁 ∈ β„€ ∧ 0 ∈ β„€) β†’ DECID 𝑁 = 0)
9126, 89, 90syl2anc 411 . . . 4 (((𝑁 ∈ β„€ ∧ 𝑋 ∈ 𝐡) ∧ 𝐺 ∈ V) β†’ DECID 𝑁 = 0)
9233, 88, 91ifcldadc 3564 . . 3 (((𝑁 ∈ β„€ ∧ 𝑋 ∈ 𝐡) ∧ 𝐺 ∈ V) β†’ if(𝑁 = 0, 0 , if(0 < 𝑁, (π‘†β€˜π‘), (πΌβ€˜(π‘†β€˜-𝑁)))) ∈ V)
939, 25, 26, 27, 92ovmpod 6002 . 2 (((𝑁 ∈ β„€ ∧ 𝑋 ∈ 𝐡) ∧ 𝐺 ∈ V) β†’ (𝑁 Β· 𝑋) = if(𝑁 = 0, 0 , if(0 < 𝑁, (π‘†β€˜π‘), (πΌβ€˜(π‘†β€˜-𝑁)))))
943, 93mpdan 421 1 ((𝑁 ∈ β„€ ∧ 𝑋 ∈ 𝐡) β†’ (𝑁 Β· 𝑋) = if(𝑁 = 0, 0 , if(0 < 𝑁, (π‘†β€˜π‘), (πΌβ€˜(π‘†β€˜-𝑁)))))
Colors of variables: wff set class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 104  DECID wdc 834   ∨ w3o 977   = wceq 1353   ∈ wcel 2148  Vcvv 2738  ifcif 3535  {csn 3593   class class class wbr 4004   Γ— cxp 4625   Fn wfn 5212  βŸΆwf 5213  β€˜cfv 5217  (class class class)co 5875   ∈ cmpo 5877  β„cr 7810  0cc0 7811  1c1 7812   < clt 7992  -cneg 8129  β„•cn 8919  β„€cz 9253  seqcseq 10445  Basecbs 12462  +gcplusg 12536  0gc0g 12705  invgcminusg 12878  .gcmg 12983
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 4119  ax-sep 4122  ax-nul 4130  ax-pow 4175  ax-pr 4210  ax-un 4434  ax-setind 4537  ax-iinf 4588  ax-cnex 7902  ax-resscn 7903  ax-1cn 7904  ax-1re 7905  ax-icn 7906  ax-addcl 7907  ax-addrcl 7908  ax-mulcl 7909  ax-addcom 7911  ax-addass 7913  ax-distr 7915  ax-i2m1 7916  ax-0lt1 7917  ax-0id 7919  ax-rnegex 7920  ax-cnre 7922  ax-pre-ltirr 7923  ax-pre-ltwlin 7924  ax-pre-lttrn 7925  ax-pre-ltadd 7927
This theorem depends on definitions:  df-bi 117  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  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-rab 2464  df-v 2740  df-sbc 2964  df-csb 3059  df-dif 3132  df-un 3134  df-in 3136  df-ss 3143  df-nul 3424  df-if 3536  df-pw 3578  df-sn 3599  df-pr 3600  df-op 3602  df-uni 3811  df-int 3846  df-iun 3889  df-br 4005  df-opab 4066  df-mpt 4067  df-tr 4103  df-id 4294  df-iord 4367  df-on 4369  df-ilim 4370  df-suc 4372  df-iom 4591  df-xp 4633  df-rel 4634  df-cnv 4635  df-co 4636  df-dm 4637  df-rn 4638  df-res 4639  df-ima 4640  df-iota 5179  df-fun 5219  df-fn 5220  df-f 5221  df-f1 5222  df-fo 5223  df-f1o 5224  df-fv 5225  df-riota 5831  df-ov 5878  df-oprab 5879  df-mpo 5880  df-1st 6141  df-2nd 6142  df-recs 6306  df-frec 6392  df-pnf 7994  df-mnf 7995  df-xr 7996  df-ltxr 7997  df-le 7998  df-sub 8130  df-neg 8131  df-inn 8920  df-2 8978  df-n0 9177  df-z 9254  df-uz 9529  df-seqfrec 10446  df-ndx 12465  df-slot 12466  df-base 12468  df-plusg 12549  df-0g 12707  df-minusg 12881  df-mulg 12984
This theorem is referenced by:  mulg0  12988  mulgnn  12989  mulgnegnn  12993  subgmulg  13048
  Copyright terms: Public domain W3C validator