gausslemma2dlem3 - Metamath Proof Explorer

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

Theorem gausslemma2dlem3 25263

Description: Lemma 3 for gausslemma2d 25269. (Contributed by AV, 4-Jul-2021.)

**Hypotheses**
Ref	Expression
gausslemma2d.p	⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))
gausslemma2d.h	⊢ 𝐻 = ((𝑃 − 1) / 2)
gausslemma2d.r	⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))
gausslemma2d.m	⊢ 𝑀 = (⌊‘(𝑃 / 4))

**Assertion**
Ref	Expression
gausslemma2dlem3	⊢ (𝜑 → ∀𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) = (𝑃 − (𝑘 · 2)))

Distinct variable groups: 𝑥,𝐻 𝑥,𝑃 𝜑,𝑥 𝑘,𝐻 𝑅,𝑘 𝜑,𝑘 𝑥,𝑀 𝑥,𝑘 Allowed substitution hints: 𝑃(𝑘) 𝑅(𝑥) 𝑀(𝑘)

**Proof of Theorem gausslemma2dlem3**
Step	Hyp	Ref	Expression
1		gausslemma2d.r	. . . 4 ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))
2	1	a1i 11	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))))
3		oveq1 6808	. . . . . . 7 ⊢ (𝑥 = 𝑘 → (𝑥 · 2) = (𝑘 · 2))
4	3	breq1d 4802	. . . . . 6 ⊢ (𝑥 = 𝑘 → ((𝑥 · 2) < (𝑃 / 2) ↔ (𝑘 · 2) < (𝑃 / 2)))
5	3	oveq2d 6817	. . . . . 6 ⊢ (𝑥 = 𝑘 → (𝑃 − (𝑥 · 2)) = (𝑃 − (𝑘 · 2)))
6	4, 3, 5	ifbieq12d 4245	. . . . 5 ⊢ (𝑥 = 𝑘 → if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) = if((𝑘 · 2) < (𝑃 / 2), (𝑘 · 2), (𝑃 − (𝑘 · 2))))
7	6	adantl 473	. . . 4 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) ∧ 𝑥 = 𝑘) → if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) = if((𝑘 · 2) < (𝑃 / 2), (𝑘 · 2), (𝑃 − (𝑘 · 2))))
8		gausslemma2d.p	. . . . . . . 8 ⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))
9	8	gausslemma2dlem0a 25251	. . . . . . 7 ⊢ (𝜑 → 𝑃 ∈ ℕ)
10		elfz2 12497	. . . . . . . . . 10 ⊢ (𝑘 ∈ ((𝑀 + 1)...𝐻) ↔ (((𝑀 + 1) ∈ ℤ ∧ 𝐻 ∈ ℤ ∧ 𝑘 ∈ ℤ) ∧ ((𝑀 + 1) ≤ 𝑘 ∧ 𝑘 ≤ 𝐻)))
11		gausslemma2d.m	. . . . . . . . . . . . . . . . 17 ⊢ 𝑀 = (⌊‘(𝑃 / 4))
12	11	oveq1i 6811	. . . . . . . . . . . . . . . 16 ⊢ (𝑀 + 1) = ((⌊‘(𝑃 / 4)) + 1)
13	12	breq1i 4799	. . . . . . . . . . . . . . 15 ⊢ ((𝑀 + 1) ≤ 𝑘 ↔ ((⌊‘(𝑃 / 4)) + 1) ≤ 𝑘)
14		nnre 11190	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑃 ∈ ℕ → 𝑃 ∈ ℝ)
15		4re 11260	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 4 ∈ ℝ
16	15	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑃 ∈ ℕ → 4 ∈ ℝ)
17		4ne0 11280	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 4 ≠ 0
18	17	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑃 ∈ ℕ → 4 ≠ 0)
19	14, 16, 18	redivcld 11016	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑃 ∈ ℕ → (𝑃 / 4) ∈ ℝ)
20	19	adantl 473	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) → (𝑃 / 4) ∈ ℝ)
21		fllelt 12763	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑃 / 4) ∈ ℝ → ((⌊‘(𝑃 / 4)) ≤ (𝑃 / 4) ∧ (𝑃 / 4) < ((⌊‘(𝑃 / 4)) + 1)))
22	20, 21	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) → ((⌊‘(𝑃 / 4)) ≤ (𝑃 / 4) ∧ (𝑃 / 4) < ((⌊‘(𝑃 / 4)) + 1)))
23	19	flcld 12764	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑃 ∈ ℕ → (⌊‘(𝑃 / 4)) ∈ ℤ)
24	23	zred 11645	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑃 ∈ ℕ → (⌊‘(𝑃 / 4)) ∈ ℝ)
25		peano2re 10372	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((⌊‘(𝑃 / 4)) ∈ ℝ → ((⌊‘(𝑃 / 4)) + 1) ∈ ℝ)
26	24, 25	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑃 ∈ ℕ → ((⌊‘(𝑃 / 4)) + 1) ∈ ℝ)
27	26	adantl 473	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) → ((⌊‘(𝑃 / 4)) + 1) ∈ ℝ)
28		zre 11544	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 ∈ ℤ → 𝑘 ∈ ℝ)
29	28	adantr 472	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) → 𝑘 ∈ ℝ)
30		ltleletr 10293	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑃 / 4) ∈ ℝ ∧ ((⌊‘(𝑃 / 4)) + 1) ∈ ℝ ∧ 𝑘 ∈ ℝ) → (((𝑃 / 4) < ((⌊‘(𝑃 / 4)) + 1) ∧ ((⌊‘(𝑃 / 4)) + 1) ≤ 𝑘) → (𝑃 / 4) ≤ 𝑘))
31	20, 27, 29, 30	syl3anc 1463	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) → (((𝑃 / 4) < ((⌊‘(𝑃 / 4)) + 1) ∧ ((⌊‘(𝑃 / 4)) + 1) ≤ 𝑘) → (𝑃 / 4) ≤ 𝑘))
32	31	expd 451	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) → ((𝑃 / 4) < ((⌊‘(𝑃 / 4)) + 1) → (((⌊‘(𝑃 / 4)) + 1) ≤ 𝑘 → (𝑃 / 4) ≤ 𝑘)))
33	32	adantld 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) → (((⌊‘(𝑃 / 4)) ≤ (𝑃 / 4) ∧ (𝑃 / 4) < ((⌊‘(𝑃 / 4)) + 1)) → (((⌊‘(𝑃 / 4)) + 1) ≤ 𝑘 → (𝑃 / 4) ≤ 𝑘)))
34	22, 33	mpd 15	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) → (((⌊‘(𝑃 / 4)) + 1) ≤ 𝑘 → (𝑃 / 4) ≤ 𝑘))
35	34	imp 444	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) ∧ ((⌊‘(𝑃 / 4)) + 1) ≤ 𝑘) → (𝑃 / 4) ≤ 𝑘)
36	14	rehalfcld 11442	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑃 ∈ ℕ → (𝑃 / 2) ∈ ℝ)
37	36	adantl 473	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) → (𝑃 / 2) ∈ ℝ)
38		2re 11253	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 2 ∈ ℝ
39	38	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 ∈ ℤ → 2 ∈ ℝ)
40	28, 39	remulcld 10233	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 ∈ ℤ → (𝑘 · 2) ∈ ℝ)
41	40	adantr 472	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) → (𝑘 · 2) ∈ ℝ)
42		2pos 11275	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 0 < 2
43	38, 42	pm3.2i 470	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (2 ∈ ℝ ∧ 0 < 2)
44	43	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) → (2 ∈ ℝ ∧ 0 < 2))
45		lediv1 11051	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑃 / 2) ∈ ℝ ∧ (𝑘 · 2) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((𝑃 / 2) ≤ (𝑘 · 2) ↔ ((𝑃 / 2) / 2) ≤ ((𝑘 · 2) / 2)))
46	37, 41, 44, 45	syl3anc 1463	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) → ((𝑃 / 2) ≤ (𝑘 · 2) ↔ ((𝑃 / 2) / 2) ≤ ((𝑘 · 2) / 2)))
47		nncn 11191	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑃 ∈ ℕ → 𝑃 ∈ ℂ)
48		2cnne0 11405	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (2 ∈ ℂ ∧ 2 ≠ 0)
49	48	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑃 ∈ ℕ → (2 ∈ ℂ ∧ 2 ≠ 0))
50		divdiv1 10899	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑃 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((𝑃 / 2) / 2) = (𝑃 / (2 · 2)))
51	47, 49, 49, 50	syl3anc 1463	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑃 ∈ ℕ → ((𝑃 / 2) / 2) = (𝑃 / (2 · 2)))
52		2t2e4 11340	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (2 · 2) = 4
53	52	oveq2i 6812	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑃 / (2 · 2)) = (𝑃 / 4)
54	51, 53	syl6eq 2798	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑃 ∈ ℕ → ((𝑃 / 2) / 2) = (𝑃 / 4))
55		zcn 11545	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 ∈ ℤ → 𝑘 ∈ ℂ)
56		2cnd 11256	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 ∈ ℤ → 2 ∈ ℂ)
57		2ne0 11276	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 2 ≠ 0
58	57	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 ∈ ℤ → 2 ≠ 0)
59	55, 56, 58	divcan4d 10970	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ ℤ → ((𝑘 · 2) / 2) = 𝑘)
60	54, 59	breqan12rd 4809	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) → (((𝑃 / 2) / 2) ≤ ((𝑘 · 2) / 2) ↔ (𝑃 / 4) ≤ 𝑘))
61	46, 60	bitrd 268	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) → ((𝑃 / 2) ≤ (𝑘 · 2) ↔ (𝑃 / 4) ≤ 𝑘))
62	61	adantr 472	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) ∧ ((⌊‘(𝑃 / 4)) + 1) ≤ 𝑘) → ((𝑃 / 2) ≤ (𝑘 · 2) ↔ (𝑃 / 4) ≤ 𝑘))
63	35, 62	mpbird 247	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) ∧ ((⌊‘(𝑃 / 4)) + 1) ≤ 𝑘) → (𝑃 / 2) ≤ (𝑘 · 2))
64	63	exp31 631	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ℤ → (𝑃 ∈ ℕ → (((⌊‘(𝑃 / 4)) + 1) ≤ 𝑘 → (𝑃 / 2) ≤ (𝑘 · 2))))
65	64	com23 86	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℤ → (((⌊‘(𝑃 / 4)) + 1) ≤ 𝑘 → (𝑃 ∈ ℕ → (𝑃 / 2) ≤ (𝑘 · 2))))
66	13, 65	syl5bi 232	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℤ → ((𝑀 + 1) ≤ 𝑘 → (𝑃 ∈ ℕ → (𝑃 / 2) ≤ (𝑘 · 2))))
67	66	3ad2ant3 1127	. . . . . . . . . . . . 13 ⊢ (((𝑀 + 1) ∈ ℤ ∧ 𝐻 ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((𝑀 + 1) ≤ 𝑘 → (𝑃 ∈ ℕ → (𝑃 / 2) ≤ (𝑘 · 2))))
68	67	com12 32	. . . . . . . . . . . 12 ⊢ ((𝑀 + 1) ≤ 𝑘 → (((𝑀 + 1) ∈ ℤ ∧ 𝐻 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑃 ∈ ℕ → (𝑃 / 2) ≤ (𝑘 · 2))))
69	68	adantr 472	. . . . . . . . . . 11 ⊢ (((𝑀 + 1) ≤ 𝑘 ∧ 𝑘 ≤ 𝐻) → (((𝑀 + 1) ∈ ℤ ∧ 𝐻 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑃 ∈ ℕ → (𝑃 / 2) ≤ (𝑘 · 2))))
70	69	impcom 445	. . . . . . . . . 10 ⊢ ((((𝑀 + 1) ∈ ℤ ∧ 𝐻 ∈ ℤ ∧ 𝑘 ∈ ℤ) ∧ ((𝑀 + 1) ≤ 𝑘 ∧ 𝑘 ≤ 𝐻)) → (𝑃 ∈ ℕ → (𝑃 / 2) ≤ (𝑘 · 2)))
71	10, 70	sylbi 207	. . . . . . . . 9 ⊢ (𝑘 ∈ ((𝑀 + 1)...𝐻) → (𝑃 ∈ ℕ → (𝑃 / 2) ≤ (𝑘 · 2)))
72	71	impcom 445	. . . . . . . 8 ⊢ ((𝑃 ∈ ℕ ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → (𝑃 / 2) ≤ (𝑘 · 2))
73		elfzelz 12506	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ((𝑀 + 1)...𝐻) → 𝑘 ∈ ℤ)
74	73	zred 11645	. . . . . . . . . 10 ⊢ (𝑘 ∈ ((𝑀 + 1)...𝐻) → 𝑘 ∈ ℝ)
75	38	a1i 11	. . . . . . . . . 10 ⊢ (𝑘 ∈ ((𝑀 + 1)...𝐻) → 2 ∈ ℝ)
76	74, 75	remulcld 10233	. . . . . . . . 9 ⊢ (𝑘 ∈ ((𝑀 + 1)...𝐻) → (𝑘 · 2) ∈ ℝ)
77		lenlt 10279	. . . . . . . . 9 ⊢ (((𝑃 / 2) ∈ ℝ ∧ (𝑘 · 2) ∈ ℝ) → ((𝑃 / 2) ≤ (𝑘 · 2) ↔ ¬ (𝑘 · 2) < (𝑃 / 2)))
78	36, 76, 77	syl2an 495	. . . . . . . 8 ⊢ ((𝑃 ∈ ℕ ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → ((𝑃 / 2) ≤ (𝑘 · 2) ↔ ¬ (𝑘 · 2) < (𝑃 / 2)))
79	72, 78	mpbid 222	. . . . . . 7 ⊢ ((𝑃 ∈ ℕ ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → ¬ (𝑘 · 2) < (𝑃 / 2))
80	9, 79	sylan 489	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → ¬ (𝑘 · 2) < (𝑃 / 2))
81	80	adantr 472	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) ∧ 𝑥 = 𝑘) → ¬ (𝑘 · 2) < (𝑃 / 2))
82	81	iffalsed 4229	. . . 4 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) ∧ 𝑥 = 𝑘) → if((𝑘 · 2) < (𝑃 / 2), (𝑘 · 2), (𝑃 − (𝑘 · 2))) = (𝑃 − (𝑘 · 2)))
83	7, 82	eqtrd 2782	. . 3 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) ∧ 𝑥 = 𝑘) → if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) = (𝑃 − (𝑘 · 2)))
84	8, 11	gausslemma2dlem0d 25254	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℕ₀)
85		nn0p1nn 11495	. . . . . . 7 ⊢ (𝑀 ∈ ℕ₀ → (𝑀 + 1) ∈ ℕ)
86		nnuz 11887	. . . . . . 7 ⊢ ℕ = (ℤ_≥‘1)
87	85, 86	syl6eleq 2837	. . . . . 6 ⊢ (𝑀 ∈ ℕ₀ → (𝑀 + 1) ∈ (ℤ_≥‘1))
88	84, 87	syl 17	. . . . 5 ⊢ (𝜑 → (𝑀 + 1) ∈ (ℤ_≥‘1))
89		fzss1 12544	. . . . 5 ⊢ ((𝑀 + 1) ∈ (ℤ_≥‘1) → ((𝑀 + 1)...𝐻) ⊆ (1...𝐻))
90	88, 89	syl 17	. . . 4 ⊢ (𝜑 → ((𝑀 + 1)...𝐻) ⊆ (1...𝐻))
91	90	sselda 3732	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → 𝑘 ∈ (1...𝐻))
92		ovexd 6831	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → (𝑃 − (𝑘 · 2)) ∈ V)
93	2, 83, 91, 92	fvmptd 6438	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → (𝑅‘𝑘) = (𝑃 − (𝑘 · 2)))
94	93	ralrimiva 3092	1 ⊢ (𝜑 → ∀𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) = (𝑃 − (𝑘 · 2)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∧ wa 383 ∧ w3a 1072 = wceq 1620 ∈ wcel 2127 ≠ wne 2920 ∀wral 3038 Vcvv 3328 ∖ cdif 3700 ⊆ wss 3703 ifcif 4218 {csn 4309 class class class wbr 4792 ↦ cmpt 4869 ‘cfv 6037 (class class class)co 6801 ℂcc 10097 ℝcr 10098 0cc0 10099 1c1 10100 + caddc 10102 · cmul 10104 < clt 10237 ≤ cle 10238 − cmin 10429 / cdiv 10847 ℕcn 11183 2c2 11233 4c4 11235 ℕ₀cn0 11455 ℤcz 11540 ℤ_≥cuz 11850 ...cfz 12490 ⌊cfl 12756 ℙcprime 15558

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1859 ax-4 1874 ax-5 1976 ax-6 2042 ax-7 2078 ax-8 2129 ax-9 2136 ax-10 2156 ax-11 2171 ax-12 2184 ax-13 2379 ax-ext 2728 ax-sep 4921 ax-nul 4929 ax-pow 4980 ax-pr 5043 ax-un 7102 ax-cnex 10155 ax-resscn 10156 ax-1cn 10157 ax-icn 10158 ax-addcl 10159 ax-addrcl 10160 ax-mulcl 10161 ax-mulrcl 10162 ax-mulcom 10163 ax-addass 10164 ax-mulass 10165 ax-distr 10166 ax-i2m1 10167 ax-1ne0 10168 ax-1rid 10169 ax-rnegex 10170 ax-rrecex 10171 ax-cnre 10172 ax-pre-lttri 10173 ax-pre-lttrn 10174 ax-pre-ltadd 10175 ax-pre-mulgt0 10176 ax-pre-sup 10177

This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1073 df-3an 1074 df-tru 1623 df-ex 1842 df-nf 1847 df-sb 2035 df-eu 2599 df-mo 2600 df-clab 2735 df-cleq 2741 df-clel 2744 df-nfc 2879 df-ne 2921 df-nel 3024 df-ral 3043 df-rex 3044 df-reu 3045 df-rmo 3046 df-rab 3047 df-v 3330 df-sbc 3565 df-csb 3663 df-dif 3706 df-un 3708 df-in 3710 df-ss 3717 df-pss 3719 df-nul 4047 df-if 4219 df-pw 4292 df-sn 4310 df-pr 4312 df-tp 4314 df-op 4316 df-uni 4577 df-iun 4662 df-br 4793 df-opab 4853 df-mpt 4870 df-tr 4893 df-id 5162 df-eprel 5167 df-po 5175 df-so 5176 df-fr 5213 df-we 5215 df-xp 5260 df-rel 5261 df-cnv 5262 df-co 5263 df-dm 5264 df-rn 5265 df-res 5266 df-ima 5267 df-pred 5829 df-ord 5875 df-on 5876 df-lim 5877 df-suc 5878 df-iota 6000 df-fun 6039 df-fn 6040 df-f 6041 df-f1 6042 df-fo 6043 df-f1o 6044 df-fv 6045 df-riota 6762 df-ov 6804 df-oprab 6805 df-mpt2 6806 df-om 7219 df-1st 7321 df-2nd 7322 df-wrecs 7564 df-recs 7625 df-rdg 7663 df-1o 7717 df-2o 7718 df-er 7899 df-en 8110 df-dom 8111 df-sdom 8112 df-fin 8113 df-sup 8501 df-inf 8502 df-pnf 10239 df-mnf 10240 df-xr 10241 df-ltxr 10242 df-le 10243 df-sub 10431 df-neg 10432 df-div 10848 df-nn 11184 df-2 11242 df-3 11243 df-4 11244 df-n0 11456 df-z 11541 df-uz 11851 df-rp 11997 df-fz 12491 df-fl 12758 df-seq 12967 df-exp 13026 df-cj 14009 df-re 14010 df-im 14011 df-sqrt 14145 df-abs 14146 df-dvds 15154 df-prm 15559

This theorem is referenced by: gausslemma2dlem5a 25265 gausslemma2dlem6 25267

W3C validator