Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  fprodmodd Structured version   Visualization version   GIF version

Theorem fprodmodd 15346
 Description: If all factors of two finite products are equal modulo 𝑀, the products are equal modulo 𝑀. (Contributed by AV, 7-Jul-2021.)
Hypotheses
Ref Expression
fprodmodd.a (𝜑𝐴 ∈ Fin)
fprodmodd.b ((𝜑𝑘𝐴) → 𝐵 ∈ ℤ)
fprodmodd.c ((𝜑𝑘𝐴) → 𝐶 ∈ ℤ)
fprodmodd.m (𝜑𝑀 ∈ ℕ)
fprodmodd.p ((𝜑𝑘𝐴) → (𝐵 mod 𝑀) = (𝐶 mod 𝑀))
Assertion
Ref Expression
fprodmodd (𝜑 → (∏𝑘𝐴 𝐵 mod 𝑀) = (∏𝑘𝐴 𝐶 mod 𝑀))
Distinct variable groups:   𝐴,𝑘   𝑘,𝑀   𝜑,𝑘
Allowed substitution hints:   𝐵(𝑘)   𝐶(𝑘)

Proof of Theorem fprodmodd
Dummy variables 𝑖 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 prodeq1 15258 . . . 4 (𝑥 = ∅ → ∏𝑘𝑥 𝐵 = ∏𝑘 ∈ ∅ 𝐵)
21oveq1d 7151 . . 3 (𝑥 = ∅ → (∏𝑘𝑥 𝐵 mod 𝑀) = (∏𝑘 ∈ ∅ 𝐵 mod 𝑀))
3 prodeq1 15258 . . . 4 (𝑥 = ∅ → ∏𝑘𝑥 𝐶 = ∏𝑘 ∈ ∅ 𝐶)
43oveq1d 7151 . . 3 (𝑥 = ∅ → (∏𝑘𝑥 𝐶 mod 𝑀) = (∏𝑘 ∈ ∅ 𝐶 mod 𝑀))
52, 4eqeq12d 2814 . 2 (𝑥 = ∅ → ((∏𝑘𝑥 𝐵 mod 𝑀) = (∏𝑘𝑥 𝐶 mod 𝑀) ↔ (∏𝑘 ∈ ∅ 𝐵 mod 𝑀) = (∏𝑘 ∈ ∅ 𝐶 mod 𝑀)))
6 prodeq1 15258 . . . 4 (𝑥 = 𝑦 → ∏𝑘𝑥 𝐵 = ∏𝑘𝑦 𝐵)
76oveq1d 7151 . . 3 (𝑥 = 𝑦 → (∏𝑘𝑥 𝐵 mod 𝑀) = (∏𝑘𝑦 𝐵 mod 𝑀))
8 prodeq1 15258 . . . 4 (𝑥 = 𝑦 → ∏𝑘𝑥 𝐶 = ∏𝑘𝑦 𝐶)
98oveq1d 7151 . . 3 (𝑥 = 𝑦 → (∏𝑘𝑥 𝐶 mod 𝑀) = (∏𝑘𝑦 𝐶 mod 𝑀))
107, 9eqeq12d 2814 . 2 (𝑥 = 𝑦 → ((∏𝑘𝑥 𝐵 mod 𝑀) = (∏𝑘𝑥 𝐶 mod 𝑀) ↔ (∏𝑘𝑦 𝐵 mod 𝑀) = (∏𝑘𝑦 𝐶 mod 𝑀)))
11 prodeq1 15258 . . . 4 (𝑥 = (𝑦 ∪ {𝑖}) → ∏𝑘𝑥 𝐵 = ∏𝑘 ∈ (𝑦 ∪ {𝑖})𝐵)
1211oveq1d 7151 . . 3 (𝑥 = (𝑦 ∪ {𝑖}) → (∏𝑘𝑥 𝐵 mod 𝑀) = (∏𝑘 ∈ (𝑦 ∪ {𝑖})𝐵 mod 𝑀))
13 prodeq1 15258 . . . 4 (𝑥 = (𝑦 ∪ {𝑖}) → ∏𝑘𝑥 𝐶 = ∏𝑘 ∈ (𝑦 ∪ {𝑖})𝐶)
1413oveq1d 7151 . . 3 (𝑥 = (𝑦 ∪ {𝑖}) → (∏𝑘𝑥 𝐶 mod 𝑀) = (∏𝑘 ∈ (𝑦 ∪ {𝑖})𝐶 mod 𝑀))
1512, 14eqeq12d 2814 . 2 (𝑥 = (𝑦 ∪ {𝑖}) → ((∏𝑘𝑥 𝐵 mod 𝑀) = (∏𝑘𝑥 𝐶 mod 𝑀) ↔ (∏𝑘 ∈ (𝑦 ∪ {𝑖})𝐵 mod 𝑀) = (∏𝑘 ∈ (𝑦 ∪ {𝑖})𝐶 mod 𝑀)))
16 prodeq1 15258 . . . 4 (𝑥 = 𝐴 → ∏𝑘𝑥 𝐵 = ∏𝑘𝐴 𝐵)
1716oveq1d 7151 . . 3 (𝑥 = 𝐴 → (∏𝑘𝑥 𝐵 mod 𝑀) = (∏𝑘𝐴 𝐵 mod 𝑀))
18 prodeq1 15258 . . . 4 (𝑥 = 𝐴 → ∏𝑘𝑥 𝐶 = ∏𝑘𝐴 𝐶)
1918oveq1d 7151 . . 3 (𝑥 = 𝐴 → (∏𝑘𝑥 𝐶 mod 𝑀) = (∏𝑘𝐴 𝐶 mod 𝑀))
2017, 19eqeq12d 2814 . 2 (𝑥 = 𝐴 → ((∏𝑘𝑥 𝐵 mod 𝑀) = (∏𝑘𝑥 𝐶 mod 𝑀) ↔ (∏𝑘𝐴 𝐵 mod 𝑀) = (∏𝑘𝐴 𝐶 mod 𝑀)))
21 prod0 15292 . . . . 5 𝑘 ∈ ∅ 𝐵 = 1
2221a1i 11 . . . 4 (𝜑 → ∏𝑘 ∈ ∅ 𝐵 = 1)
2322oveq1d 7151 . . 3 (𝜑 → (∏𝑘 ∈ ∅ 𝐵 mod 𝑀) = (1 mod 𝑀))
24 prod0 15292 . . . . 5 𝑘 ∈ ∅ 𝐶 = 1
2524eqcomi 2807 . . . 4 1 = ∏𝑘 ∈ ∅ 𝐶
2625oveq1i 7146 . . 3 (1 mod 𝑀) = (∏𝑘 ∈ ∅ 𝐶 mod 𝑀)
2723, 26eqtrdi 2849 . 2 (𝜑 → (∏𝑘 ∈ ∅ 𝐵 mod 𝑀) = (∏𝑘 ∈ ∅ 𝐶 mod 𝑀))
28 nfv 1915 . . . . . . 7 𝑘(𝜑 ∧ (𝑦𝐴𝑖 ∈ (𝐴𝑦)))
29 nfcsb1v 3852 . . . . . . 7 𝑘𝑖 / 𝑘𝐵
30 ssfi 8725 . . . . . . . . . . 11 ((𝐴 ∈ Fin ∧ 𝑦𝐴) → 𝑦 ∈ Fin)
3130ex 416 . . . . . . . . . 10 (𝐴 ∈ Fin → (𝑦𝐴𝑦 ∈ Fin))
32 fprodmodd.a . . . . . . . . . 10 (𝜑𝐴 ∈ Fin)
3331, 32syl11 33 . . . . . . . . 9 (𝑦𝐴 → (𝜑𝑦 ∈ Fin))
3433adantr 484 . . . . . . . 8 ((𝑦𝐴𝑖 ∈ (𝐴𝑦)) → (𝜑𝑦 ∈ Fin))
3534impcom 411 . . . . . . 7 ((𝜑 ∧ (𝑦𝐴𝑖 ∈ (𝐴𝑦))) → 𝑦 ∈ Fin)
36 simpr 488 . . . . . . . 8 ((𝑦𝐴𝑖 ∈ (𝐴𝑦)) → 𝑖 ∈ (𝐴𝑦))
3736adantl 485 . . . . . . 7 ((𝜑 ∧ (𝑦𝐴𝑖 ∈ (𝐴𝑦))) → 𝑖 ∈ (𝐴𝑦))
38 eldifn 4055 . . . . . . . . 9 (𝑖 ∈ (𝐴𝑦) → ¬ 𝑖𝑦)
3938adantl 485 . . . . . . . 8 ((𝑦𝐴𝑖 ∈ (𝐴𝑦)) → ¬ 𝑖𝑦)
4039adantl 485 . . . . . . 7 ((𝜑 ∧ (𝑦𝐴𝑖 ∈ (𝐴𝑦))) → ¬ 𝑖𝑦)
41 simpll 766 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝐴𝑖 ∈ (𝐴𝑦))) ∧ 𝑘𝑦) → 𝜑)
42 ssel 3908 . . . . . . . . . . . 12 (𝑦𝐴 → (𝑘𝑦𝑘𝐴))
4342adantr 484 . . . . . . . . . . 11 ((𝑦𝐴𝑖 ∈ (𝐴𝑦)) → (𝑘𝑦𝑘𝐴))
4443adantl 485 . . . . . . . . . 10 ((𝜑 ∧ (𝑦𝐴𝑖 ∈ (𝐴𝑦))) → (𝑘𝑦𝑘𝐴))
4544imp 410 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝐴𝑖 ∈ (𝐴𝑦))) ∧ 𝑘𝑦) → 𝑘𝐴)
46 fprodmodd.b . . . . . . . . 9 ((𝜑𝑘𝐴) → 𝐵 ∈ ℤ)
4741, 45, 46syl2anc 587 . . . . . . . 8 (((𝜑 ∧ (𝑦𝐴𝑖 ∈ (𝐴𝑦))) ∧ 𝑘𝑦) → 𝐵 ∈ ℤ)
4847zcnd 12079 . . . . . . 7 (((𝜑 ∧ (𝑦𝐴𝑖 ∈ (𝐴𝑦))) ∧ 𝑘𝑦) → 𝐵 ∈ ℂ)
49 csbeq1a 3842 . . . . . . 7 (𝑘 = 𝑖𝐵 = 𝑖 / 𝑘𝐵)
50 eldifi 4054 . . . . . . . . . 10 (𝑖 ∈ (𝐴𝑦) → 𝑖𝐴)
5150adantl 485 . . . . . . . . 9 ((𝑦𝐴𝑖 ∈ (𝐴𝑦)) → 𝑖𝐴)
5246ralrimiva 3149 . . . . . . . . 9 (𝜑 → ∀𝑘𝐴 𝐵 ∈ ℤ)
53 rspcsbela 4343 . . . . . . . . 9 ((𝑖𝐴 ∧ ∀𝑘𝐴 𝐵 ∈ ℤ) → 𝑖 / 𝑘𝐵 ∈ ℤ)
5451, 52, 53syl2anr 599 . . . . . . . 8 ((𝜑 ∧ (𝑦𝐴𝑖 ∈ (𝐴𝑦))) → 𝑖 / 𝑘𝐵 ∈ ℤ)
5554zcnd 12079 . . . . . . 7 ((𝜑 ∧ (𝑦𝐴𝑖 ∈ (𝐴𝑦))) → 𝑖 / 𝑘𝐵 ∈ ℂ)
5628, 29, 35, 37, 40, 48, 49, 55fprodsplitsn 15338 . . . . . 6 ((𝜑 ∧ (𝑦𝐴𝑖 ∈ (𝐴𝑦))) → ∏𝑘 ∈ (𝑦 ∪ {𝑖})𝐵 = (∏𝑘𝑦 𝐵 · 𝑖 / 𝑘𝐵))
5756oveq1d 7151 . . . . 5 ((𝜑 ∧ (𝑦𝐴𝑖 ∈ (𝐴𝑦))) → (∏𝑘 ∈ (𝑦 ∪ {𝑖})𝐵 mod 𝑀) = ((∏𝑘𝑦 𝐵 · 𝑖 / 𝑘𝐵) mod 𝑀))
5857adantr 484 . . . 4 (((𝜑 ∧ (𝑦𝐴𝑖 ∈ (𝐴𝑦))) ∧ (∏𝑘𝑦 𝐵 mod 𝑀) = (∏𝑘𝑦 𝐶 mod 𝑀)) → (∏𝑘 ∈ (𝑦 ∪ {𝑖})𝐵 mod 𝑀) = ((∏𝑘𝑦 𝐵 · 𝑖 / 𝑘𝐵) mod 𝑀))
5935, 47fprodzcl 15303 . . . . . 6 ((𝜑 ∧ (𝑦𝐴𝑖 ∈ (𝐴𝑦))) → ∏𝑘𝑦 𝐵 ∈ ℤ)
6059adantr 484 . . . . 5 (((𝜑 ∧ (𝑦𝐴𝑖 ∈ (𝐴𝑦))) ∧ (∏𝑘𝑦 𝐵 mod 𝑀) = (∏𝑘𝑦 𝐶 mod 𝑀)) → ∏𝑘𝑦 𝐵 ∈ ℤ)
61 fprodmodd.c . . . . . . . 8 ((𝜑𝑘𝐴) → 𝐶 ∈ ℤ)
6241, 45, 61syl2anc 587 . . . . . . 7 (((𝜑 ∧ (𝑦𝐴𝑖 ∈ (𝐴𝑦))) ∧ 𝑘𝑦) → 𝐶 ∈ ℤ)
6335, 62fprodzcl 15303 . . . . . 6 ((𝜑 ∧ (𝑦𝐴𝑖 ∈ (𝐴𝑦))) → ∏𝑘𝑦 𝐶 ∈ ℤ)
6463adantr 484 . . . . 5 (((𝜑 ∧ (𝑦𝐴𝑖 ∈ (𝐴𝑦))) ∧ (∏𝑘𝑦 𝐵 mod 𝑀) = (∏𝑘𝑦 𝐶 mod 𝑀)) → ∏𝑘𝑦 𝐶 ∈ ℤ)
6554adantr 484 . . . . 5 (((𝜑 ∧ (𝑦𝐴𝑖 ∈ (𝐴𝑦))) ∧ (∏𝑘𝑦 𝐵 mod 𝑀) = (∏𝑘𝑦 𝐶 mod 𝑀)) → 𝑖 / 𝑘𝐵 ∈ ℤ)
6661ralrimiva 3149 . . . . . . 7 (𝜑 → ∀𝑘𝐴 𝐶 ∈ ℤ)
67 rspcsbela 4343 . . . . . . 7 ((𝑖𝐴 ∧ ∀𝑘𝐴 𝐶 ∈ ℤ) → 𝑖 / 𝑘𝐶 ∈ ℤ)
6851, 66, 67syl2anr 599 . . . . . 6 ((𝜑 ∧ (𝑦𝐴𝑖 ∈ (𝐴𝑦))) → 𝑖 / 𝑘𝐶 ∈ ℤ)
6968adantr 484 . . . . 5 (((𝜑 ∧ (𝑦𝐴𝑖 ∈ (𝐴𝑦))) ∧ (∏𝑘𝑦 𝐵 mod 𝑀) = (∏𝑘𝑦 𝐶 mod 𝑀)) → 𝑖 / 𝑘𝐶 ∈ ℤ)
70 fprodmodd.m . . . . . . . 8 (𝜑𝑀 ∈ ℕ)
7170nnrpd 12420 . . . . . . 7 (𝜑𝑀 ∈ ℝ+)
7271adantr 484 . . . . . 6 ((𝜑 ∧ (𝑦𝐴𝑖 ∈ (𝐴𝑦))) → 𝑀 ∈ ℝ+)
7372adantr 484 . . . . 5 (((𝜑 ∧ (𝑦𝐴𝑖 ∈ (𝐴𝑦))) ∧ (∏𝑘𝑦 𝐵 mod 𝑀) = (∏𝑘𝑦 𝐶 mod 𝑀)) → 𝑀 ∈ ℝ+)
74 simpr 488 . . . . 5 (((𝜑 ∧ (𝑦𝐴𝑖 ∈ (𝐴𝑦))) ∧ (∏𝑘𝑦 𝐵 mod 𝑀) = (∏𝑘𝑦 𝐶 mod 𝑀)) → (∏𝑘𝑦 𝐵 mod 𝑀) = (∏𝑘𝑦 𝐶 mod 𝑀))
75 fprodmodd.p . . . . . . . . . 10 ((𝜑𝑘𝐴) → (𝐵 mod 𝑀) = (𝐶 mod 𝑀))
7675ralrimiva 3149 . . . . . . . . 9 (𝜑 → ∀𝑘𝐴 (𝐵 mod 𝑀) = (𝐶 mod 𝑀))
77 rspsbca 3809 . . . . . . . . 9 ((𝑖𝐴 ∧ ∀𝑘𝐴 (𝐵 mod 𝑀) = (𝐶 mod 𝑀)) → [𝑖 / 𝑘](𝐵 mod 𝑀) = (𝐶 mod 𝑀))
7851, 76, 77syl2anr 599 . . . . . . . 8 ((𝜑 ∧ (𝑦𝐴𝑖 ∈ (𝐴𝑦))) → [𝑖 / 𝑘](𝐵 mod 𝑀) = (𝐶 mod 𝑀))
79 vex 3444 . . . . . . . . 9 𝑖 ∈ V
80 sbceqg 4317 . . . . . . . . 9 (𝑖 ∈ V → ([𝑖 / 𝑘](𝐵 mod 𝑀) = (𝐶 mod 𝑀) ↔ 𝑖 / 𝑘(𝐵 mod 𝑀) = 𝑖 / 𝑘(𝐶 mod 𝑀)))
8179, 80mp1i 13 . . . . . . . 8 ((𝜑 ∧ (𝑦𝐴𝑖 ∈ (𝐴𝑦))) → ([𝑖 / 𝑘](𝐵 mod 𝑀) = (𝐶 mod 𝑀) ↔ 𝑖 / 𝑘(𝐵 mod 𝑀) = 𝑖 / 𝑘(𝐶 mod 𝑀)))
8278, 81mpbid 235 . . . . . . 7 ((𝜑 ∧ (𝑦𝐴𝑖 ∈ (𝐴𝑦))) → 𝑖 / 𝑘(𝐵 mod 𝑀) = 𝑖 / 𝑘(𝐶 mod 𝑀))
83 csbov1g 7181 . . . . . . . 8 (𝑖 ∈ V → 𝑖 / 𝑘(𝐵 mod 𝑀) = (𝑖 / 𝑘𝐵 mod 𝑀))
8483elv 3446 . . . . . . 7 𝑖 / 𝑘(𝐵 mod 𝑀) = (𝑖 / 𝑘𝐵 mod 𝑀)
85 csbov1g 7181 . . . . . . . 8 (𝑖 ∈ V → 𝑖 / 𝑘(𝐶 mod 𝑀) = (𝑖 / 𝑘𝐶 mod 𝑀))
8685elv 3446 . . . . . . 7 𝑖 / 𝑘(𝐶 mod 𝑀) = (𝑖 / 𝑘𝐶 mod 𝑀)
8782, 84, 863eqtr3g 2856 . . . . . 6 ((𝜑 ∧ (𝑦𝐴𝑖 ∈ (𝐴𝑦))) → (𝑖 / 𝑘𝐵 mod 𝑀) = (𝑖 / 𝑘𝐶 mod 𝑀))
8887adantr 484 . . . . 5 (((𝜑 ∧ (𝑦𝐴𝑖 ∈ (𝐴𝑦))) ∧ (∏𝑘𝑦 𝐵 mod 𝑀) = (∏𝑘𝑦 𝐶 mod 𝑀)) → (𝑖 / 𝑘𝐵 mod 𝑀) = (𝑖 / 𝑘𝐶 mod 𝑀))
8960, 64, 65, 69, 73, 74, 88modmul12d 13291 . . . 4 (((𝜑 ∧ (𝑦𝐴𝑖 ∈ (𝐴𝑦))) ∧ (∏𝑘𝑦 𝐵 mod 𝑀) = (∏𝑘𝑦 𝐶 mod 𝑀)) → ((∏𝑘𝑦 𝐵 · 𝑖 / 𝑘𝐵) mod 𝑀) = ((∏𝑘𝑦 𝐶 · 𝑖 / 𝑘𝐶) mod 𝑀))
90 nfcsb1v 3852 . . . . . . . 8 𝑘𝑖 / 𝑘𝐶
9162zcnd 12079 . . . . . . . 8 (((𝜑 ∧ (𝑦𝐴𝑖 ∈ (𝐴𝑦))) ∧ 𝑘𝑦) → 𝐶 ∈ ℂ)
92 csbeq1a 3842 . . . . . . . 8 (𝑘 = 𝑖𝐶 = 𝑖 / 𝑘𝐶)
9368zcnd 12079 . . . . . . . 8 ((𝜑 ∧ (𝑦𝐴𝑖 ∈ (𝐴𝑦))) → 𝑖 / 𝑘𝐶 ∈ ℂ)
9428, 90, 35, 37, 40, 91, 92, 93fprodsplitsn 15338 . . . . . . 7 ((𝜑 ∧ (𝑦𝐴𝑖 ∈ (𝐴𝑦))) → ∏𝑘 ∈ (𝑦 ∪ {𝑖})𝐶 = (∏𝑘𝑦 𝐶 · 𝑖 / 𝑘𝐶))
9594oveq1d 7151 . . . . . 6 ((𝜑 ∧ (𝑦𝐴𝑖 ∈ (𝐴𝑦))) → (∏𝑘 ∈ (𝑦 ∪ {𝑖})𝐶 mod 𝑀) = ((∏𝑘𝑦 𝐶 · 𝑖 / 𝑘𝐶) mod 𝑀))
9695eqcomd 2804 . . . . 5 ((𝜑 ∧ (𝑦𝐴𝑖 ∈ (𝐴𝑦))) → ((∏𝑘𝑦 𝐶 · 𝑖 / 𝑘𝐶) mod 𝑀) = (∏𝑘 ∈ (𝑦 ∪ {𝑖})𝐶 mod 𝑀))
9796adantr 484 . . . 4 (((𝜑 ∧ (𝑦𝐴𝑖 ∈ (𝐴𝑦))) ∧ (∏𝑘𝑦 𝐵 mod 𝑀) = (∏𝑘𝑦 𝐶 mod 𝑀)) → ((∏𝑘𝑦 𝐶 · 𝑖 / 𝑘𝐶) mod 𝑀) = (∏𝑘 ∈ (𝑦 ∪ {𝑖})𝐶 mod 𝑀))
9858, 89, 973eqtrd 2837 . . 3 (((𝜑 ∧ (𝑦𝐴𝑖 ∈ (𝐴𝑦))) ∧ (∏𝑘𝑦 𝐵 mod 𝑀) = (∏𝑘𝑦 𝐶 mod 𝑀)) → (∏𝑘 ∈ (𝑦 ∪ {𝑖})𝐵 mod 𝑀) = (∏𝑘 ∈ (𝑦 ∪ {𝑖})𝐶 mod 𝑀))
9998ex 416 . 2 ((𝜑 ∧ (𝑦𝐴𝑖 ∈ (𝐴𝑦))) → ((∏𝑘𝑦 𝐵 mod 𝑀) = (∏𝑘𝑦 𝐶 mod 𝑀) → (∏𝑘 ∈ (𝑦 ∪ {𝑖})𝐵 mod 𝑀) = (∏𝑘 ∈ (𝑦 ∪ {𝑖})𝐶 mod 𝑀)))
1005, 10, 15, 20, 27, 99, 32findcard2d 8747 1 (𝜑 → (∏𝑘𝐴 𝐵 mod 𝑀) = (∏𝑘𝐴 𝐶 mod 𝑀))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111  ∀wral 3106  Vcvv 3441  [wsbc 3720  ⦋csb 3828   ∖ cdif 3878   ∪ cun 3879   ⊆ wss 3881  ∅c0 4243  {csn 4525  (class class class)co 7136  Fincfn 8495  1c1 10530   · cmul 10534  ℕcn 11628  ℤcz 11972  ℝ+crp 12380   mod cmo 13235  ∏cprod 15254 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5155  ax-sep 5168  ax-nul 5175  ax-pow 5232  ax-pr 5296  ax-un 7444  ax-inf2 9091  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606  ax-pre-sup 10607 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4802  df-int 4840  df-iun 4884  df-br 5032  df-opab 5094  df-mpt 5112  df-tr 5138  df-id 5426  df-eprel 5431  df-po 5439  df-so 5440  df-fr 5479  df-se 5480  df-we 5481  df-xp 5526  df-rel 5527  df-cnv 5528  df-co 5529  df-dm 5530  df-rn 5531  df-res 5532  df-ima 5533  df-pred 6117  df-ord 6163  df-on 6164  df-lim 6165  df-suc 6166  df-iota 6284  df-fun 6327  df-fn 6328  df-f 6329  df-f1 6330  df-fo 6331  df-f1o 6332  df-fv 6333  df-isom 6334  df-riota 7094  df-ov 7139  df-oprab 7140  df-mpo 7141  df-om 7564  df-1st 7674  df-2nd 7675  df-wrecs 7933  df-recs 7994  df-rdg 8032  df-1o 8088  df-oadd 8092  df-er 8275  df-en 8496  df-dom 8497  df-sdom 8498  df-fin 8499  df-sup 8893  df-inf 8894  df-oi 8961  df-card 9355  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-div 11290  df-nn 11629  df-2 11691  df-3 11692  df-n0 11889  df-z 11973  df-uz 12235  df-rp 12381  df-fz 12889  df-fzo 13032  df-fl 13160  df-mod 13236  df-seq 13368  df-exp 13429  df-hash 13690  df-cj 14453  df-re 14454  df-im 14455  df-sqrt 14589  df-abs 14590  df-clim 14840  df-prod 15255 This theorem is referenced by:  gausslemma2dlem5a  25964
 Copyright terms: Public domain W3C validator