Theorem fprodntriv 15973

Description: A non-triviality lemma for finite sequences. (Contributed by Scott Fenton, 16-Dec-2017.)

Hypotheses

Ref	Expression
fprodntriv.1	⊢ 𝑍 = (ℤ≥‘𝑀)
fprodntriv.2	⊢ (𝜑 → 𝑁 ∈ 𝑍)
fprodntriv.3	⊢ (𝜑 → 𝐴 ⊆ (𝑀...𝑁))

Assertion

Ref	Expression
fprodntriv	⊢ (𝜑 → ∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ 𝑍 ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦))

Distinct variable groups:   𝐴,𝑘,𝑛,𝑦   𝐵,𝑛,𝑦   𝑘,𝑛,𝑦   𝑛,𝑁   𝜑,𝑛   𝑦,𝑛,𝑁   𝑘,𝑍,𝑛,𝑦

Allowed substitution hints:   𝜑(𝑦,𝑘)   𝐵(𝑘)   𝑀(𝑦,𝑘,𝑛)   𝑁(𝑘)

Proof of Theorem fprodntriv

Dummy variable 𝑚 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fprodntriv.2	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ 𝑍)
2		fprodntriv.1	. . . . 5 ⊢ 𝑍 = (ℤ≥‘𝑀)
3	1, 2	eleqtrdi 2873	. . . 4 ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))
4		peano2uz 12903	. . . 4 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 + 1) ∈ (ℤ≥‘𝑀))
5	3, 4	syl 17	. . 3 ⊢ (𝜑 → (𝑁 + 1) ∈ (ℤ≥‘𝑀))
6	5, 2	eleqtrrdi 2874	. 2 ⊢ (𝜑 → (𝑁 + 1) ∈ 𝑍)
7		ax-1ne0 11143	. . 3 ⊢ 1 ≠ 0
8		eqid 2763	. . . 4 ⊢ (ℤ≥‘(𝑁 + 1)) = (ℤ≥‘(𝑁 + 1))
9		eluzelz 12850	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℤ)
10	9, 2	eleq2s 2881	. . . . . 6 ⊢ (𝑁 ∈ 𝑍 → 𝑁 ∈ ℤ)
11	1, 10	syl 17	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ ℤ)
12	11	peano2zd 12681	. . . 4 ⊢ (𝜑 → (𝑁 + 1) ∈ ℤ)
13		seqex 14017	. . . . 5 ⊢ seq(𝑁 + 1)( · , (𝑘 ∈ 𝑍 ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ∈ V
14	13	a1i 11	. . . 4 ⊢ (𝜑 → seq(𝑁 + 1)( · , (𝑘 ∈ 𝑍 ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ∈ V)
15		1cnd 11176	. . . 4 ⊢ (𝜑 → 1 ∈ ℂ)
16		simpr 488	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) → 𝑛 ∈ (ℤ≥‘(𝑁 + 1)))
17		fprodntriv.3	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ⊆ (𝑀...𝑁))
18	17	ad2antrr 736	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑚 ∈ ((𝑁 + 1)...𝑛)) → 𝐴 ⊆ (𝑀...𝑁))
19	11	ad2antrr 736	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑚 ∈ ((𝑁 + 1)...𝑛)) → 𝑁 ∈ ℤ)
20	19	zred 12678	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑚 ∈ ((𝑁 + 1)...𝑛)) → 𝑁 ∈ ℝ)
21	19	peano2zd 12681	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑚 ∈ ((𝑁 + 1)...𝑛)) → (𝑁 + 1) ∈ ℤ)
22	21	zred 12678	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑚 ∈ ((𝑁 + 1)...𝑛)) → (𝑁 + 1) ∈ ℝ)
23		elfzelz 13530	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ ((𝑁 + 1)...𝑛) → 𝑚 ∈ ℤ)
24	23	adantl 485	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑚 ∈ ((𝑁 + 1)...𝑛)) → 𝑚 ∈ ℤ)
25	24	zred 12678	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑚 ∈ ((𝑁 + 1)...𝑛)) → 𝑚 ∈ ℝ)
26	20	ltp1d 12123	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑚 ∈ ((𝑁 + 1)...𝑛)) → 𝑁 < (𝑁 + 1))
27		elfzle1 13533	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ ((𝑁 + 1)...𝑛) → (𝑁 + 1) ≤ 𝑚)
28	27	adantl 485	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑚 ∈ ((𝑁 + 1)...𝑛)) → (𝑁 + 1) ≤ 𝑚)
29	20, 22, 25, 26, 28	ltletrd 11344	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑚 ∈ ((𝑁 + 1)...𝑛)) → 𝑁 < 𝑚)
30	20, 25	ltnled 11331	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑚 ∈ ((𝑁 + 1)...𝑛)) → (𝑁 < 𝑚 ↔ ¬ 𝑚 ≤ 𝑁))
31	29, 30	mpbid 234	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑚 ∈ ((𝑁 + 1)...𝑛)) → ¬ 𝑚 ≤ 𝑁)
32	31	intnand 492	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑚 ∈ ((𝑁 + 1)...𝑛)) → ¬ (𝑀 ≤ 𝑚 ∧ 𝑚 ≤ 𝑁))
33	32	intnand 492	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑚 ∈ ((𝑁 + 1)...𝑛)) → ¬ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℤ) ∧ (𝑀 ≤ 𝑚 ∧ 𝑚 ≤ 𝑁)))
34		elfz2 13520	. . . . . . . . . 10 ⊢ (𝑚 ∈ (𝑀...𝑁) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℤ) ∧ (𝑀 ≤ 𝑚 ∧ 𝑚 ≤ 𝑁)))
35	33, 34	sylnibr 331	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑚 ∈ ((𝑁 + 1)...𝑛)) → ¬ 𝑚 ∈ (𝑀...𝑁))
36	18, 35	ssneldd 3940	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑚 ∈ ((𝑁 + 1)...𝑛)) → ¬ 𝑚 ∈ 𝐴)
37	36	iffalsed 4492	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑚 ∈ ((𝑁 + 1)...𝑛)) → if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 1) = 1)
38		fzssuz 13571	. . . . . . . . . 10 ⊢ ((𝑁 + 1)...𝑛) ⊆ (ℤ≥‘(𝑁 + 1))
39	5	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) → (𝑁 + 1) ∈ (ℤ≥‘𝑀))
40		uzss 12863	. . . . . . . . . . . 12 ⊢ ((𝑁 + 1) ∈ (ℤ≥‘𝑀) → (ℤ≥‘(𝑁 + 1)) ⊆ (ℤ≥‘𝑀))
41	39, 40	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) → (ℤ≥‘(𝑁 + 1)) ⊆ (ℤ≥‘𝑀))
42	41, 2	sseqtrrdi 3978	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) → (ℤ≥‘(𝑁 + 1)) ⊆ 𝑍)
43	38, 42	sstrid 3948	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) → ((𝑁 + 1)...𝑛) ⊆ 𝑍)
44	43	sselda 3937	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑚 ∈ ((𝑁 + 1)...𝑛)) → 𝑚 ∈ 𝑍)
45		ax-1cn 11132	. . . . . . . . 9 ⊢ 1 ∈ ℂ
46	37, 45	eqeltrdi 2871	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑚 ∈ ((𝑁 + 1)...𝑛)) → if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 1) ∈ ℂ)
47		nfcv 2925	. . . . . . . . 9 ⊢ Ⅎ𝑘𝑚
48		nfv 1935	. . . . . . . . . 10 ⊢ Ⅎ𝑘 𝑚 ∈ 𝐴
49		nfcsb1v 3877	. . . . . . . . . 10 ⊢ Ⅎ𝑘⦋𝑚 / 𝑘⦌𝐵
50		nfcv 2925	. . . . . . . . . 10 ⊢ Ⅎ𝑘1
51	48, 49, 50	nfif 4512	. . . . . . . . 9 ⊢ Ⅎ𝑘if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 1)
52		eleq1w 2846	. . . . . . . . . 10 ⊢ (𝑘 = 𝑚 → (𝑘 ∈ 𝐴 ↔ 𝑚 ∈ 𝐴))
53		csbeq1a 3867	. . . . . . . . . 10 ⊢ (𝑘 = 𝑚 → 𝐵 = ⦋𝑚 / 𝑘⦌𝐵)
54	52, 53	ifbieq1d 4506	. . . . . . . . 9 ⊢ (𝑘 = 𝑚 → if(𝑘 ∈ 𝐴, 𝐵, 1) = if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 1))
55		eqid 2763	. . . . . . . . 9 ⊢ (𝑘 ∈ 𝑍 ↦ if(𝑘 ∈ 𝐴, 𝐵, 1)) = (𝑘 ∈ 𝑍 ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))
56	47, 51, 54, 55	fvmptf 6998	. . . . . . . 8 ⊢ ((𝑚 ∈ 𝑍 ∧ if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 1) ∈ ℂ) → ((𝑘 ∈ 𝑍 ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑚) = if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 1))
57	44, 46, 56	syl2anc 593	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑚 ∈ ((𝑁 + 1)...𝑛)) → ((𝑘 ∈ 𝑍 ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑚) = if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 1))
58		elfzuz 13526	. . . . . . . . 9 ⊢ (𝑚 ∈ ((𝑁 + 1)...𝑛) → 𝑚 ∈ (ℤ≥‘(𝑁 + 1)))
59	58	adantl 485	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑚 ∈ ((𝑁 + 1)...𝑛)) → 𝑚 ∈ (ℤ≥‘(𝑁 + 1)))
60		1ex 11177	. . . . . . . . 9 ⊢ 1 ∈ V
61	60	fvconst2 7189	. . . . . . . 8 ⊢ (𝑚 ∈ (ℤ≥‘(𝑁 + 1)) → (((ℤ≥‘(𝑁 + 1)) × {1})‘𝑚) = 1)
62	59, 61	syl 17	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑚 ∈ ((𝑁 + 1)...𝑛)) → (((ℤ≥‘(𝑁 + 1)) × {1})‘𝑚) = 1)
63	37, 57, 62	3eqtr4d 2808	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑚 ∈ ((𝑁 + 1)...𝑛)) → ((𝑘 ∈ 𝑍 ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑚) = (((ℤ≥‘(𝑁 + 1)) × {1})‘𝑚))
64	16, 63	seqfveq 14040	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) → (seq(𝑁 + 1)( · , (𝑘 ∈ 𝑍 ↦ if(𝑘 ∈ 𝐴, 𝐵, 1)))‘𝑛) = (seq(𝑁 + 1)( · , ((ℤ≥‘(𝑁 + 1)) × {1}))‘𝑛))
65	8	prodf1 15922	. . . . . 6 ⊢ (𝑛 ∈ (ℤ≥‘(𝑁 + 1)) → (seq(𝑁 + 1)( · , ((ℤ≥‘(𝑁 + 1)) × {1}))‘𝑛) = 1)
66	65	adantl 485	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) → (seq(𝑁 + 1)( · , ((ℤ≥‘(𝑁 + 1)) × {1}))‘𝑛) = 1)
67	64, 66	eqtrd 2798	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) → (seq(𝑁 + 1)( · , (𝑘 ∈ 𝑍 ↦ if(𝑘 ∈ 𝐴, 𝐵, 1)))‘𝑛) = 1)
68	8, 12, 14, 15, 67	climconst 15571	. . 3 ⊢ (𝜑 → seq(𝑁 + 1)( · , (𝑘 ∈ 𝑍 ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 1)
69		neeq1 3020	. . . . 5 ⊢ (𝑦 = 1 → (𝑦 ≠ 0 ↔ 1 ≠ 0))
70		breq2 5105	. . . . 5 ⊢ (𝑦 = 1 → (seq(𝑁 + 1)( · , (𝑘 ∈ 𝑍 ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦 ↔ seq(𝑁 + 1)( · , (𝑘 ∈ 𝑍 ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 1))
71	69, 70	anbi12d 641	. . . 4 ⊢ (𝑦 = 1 → ((𝑦 ≠ 0 ∧ seq(𝑁 + 1)( · , (𝑘 ∈ 𝑍 ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ↔ (1 ≠ 0 ∧ seq(𝑁 + 1)( · , (𝑘 ∈ 𝑍 ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 1)))
72	60, 71	spcev 3566	. . 3 ⊢ ((1 ≠ 0 ∧ seq(𝑁 + 1)( · , (𝑘 ∈ 𝑍 ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 1) → ∃𝑦(𝑦 ≠ 0 ∧ seq(𝑁 + 1)( · , (𝑘 ∈ 𝑍 ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦))
73	7, 68, 72	sylancr 596	. 2 ⊢ (𝜑 → ∃𝑦(𝑦 ≠ 0 ∧ seq(𝑁 + 1)( · , (𝑘 ∈ 𝑍 ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦))
74		seqeq1 14018	. . . . . 6 ⊢ (𝑛 = (𝑁 + 1) → seq𝑛( · , (𝑘 ∈ 𝑍 ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) = seq(𝑁 + 1)( · , (𝑘 ∈ 𝑍 ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))))
75	74	breq1d 5111	. . . . 5 ⊢ (𝑛 = (𝑁 + 1) → (seq𝑛( · , (𝑘 ∈ 𝑍 ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦 ↔ seq(𝑁 + 1)( · , (𝑘 ∈ 𝑍 ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦))
76	75	anbi2d 639	. . . 4 ⊢ (𝑛 = (𝑁 + 1) → ((𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ 𝑍 ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ↔ (𝑦 ≠ 0 ∧ seq(𝑁 + 1)( · , (𝑘 ∈ 𝑍 ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦)))
77	76	exbidv 1942	. . 3 ⊢ (𝑛 = (𝑁 + 1) → (∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ 𝑍 ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ↔ ∃𝑦(𝑦 ≠ 0 ∧ seq(𝑁 + 1)( · , (𝑘 ∈ 𝑍 ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦)))
78	77	rspcev 3582	. 2 ⊢ (((𝑁 + 1) ∈ 𝑍 ∧ ∃𝑦(𝑦 ≠ 0 ∧ seq(𝑁 + 1)( · , (𝑘 ∈ 𝑍 ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦)) → ∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ 𝑍 ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦))
79	6, 73, 78	syl2anc 593	1 ⊢ (𝜑 → ∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ 𝑍 ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   ∧ w3a 1099   = wceq 1561  ∃wex 1800   ∈ wcel 2143   ≠ wne 2958  ∃wrex 3087  Vcvv 3455  ⦋csb 3853   ⊆ wss 3905  ifcif 4481  {csn 4583   class class class wbr 5101   ↦ cmpt 5182   × cxp 5646  ‘cfv 6522  (class class class)co 7397  ℂcc 11072  0cc0 11074  1c1 11075   + caddc 11077   · cmul 11079   < clt 11217   ≤ cle 11218  ℤcz 12569  ℤ_≥cuz 12840  ...cfz 13513  seqcseq 14015   ⇝ cli 15512

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-rep 5228  ax-sep 5247  ax-nul 5257  ax-pow 5323  ax-pr 5391  ax-un 7719  ax-inf2 9597  ax-cnex 11130  ax-resscn 11131  ax-1cn 11132  ax-icn 11133  ax-addcl 11134  ax-addrcl 11135  ax-mulcl 11136  ax-mulrcl 11137  ax-mulcom 11138  ax-addass 11139  ax-mulass 11140  ax-distr 11141  ax-i2m1 11142  ax-1ne0 11143  ax-1rid 11144  ax-rnegex 11145  ax-rrecex 11146  ax-cnre 11147  ax-pre-lttri 11148  ax-pre-lttrn 11149  ax-pre-ltadd 11150  ax-pre-mulgt0 11151

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1100  df-3an 1101  df-tru 1564  df-fal 1574  df-ex 1801  df-nf 1805  df-sb 2092  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3063  df-ral 3078  df-rex 3088  df-rmo 3368  df-reu 3369  df-rab 3416  df-v 3457  df-sbc 3746  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-iun 4952  df-br 5102  df-opab 5164  df-mpt 5183  df-tr 5209  df-id 5543  df-eprel 5548  df-po 5556  df-so 5557  df-fr 5601  df-we 5603  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-rn 5659  df-res 5660  df-ima 5661  df-pred 6289  df-ord 6350  df-on 6351  df-lim 6352  df-suc 6353  df-iota 6478  df-fun 6524  df-fn 6525  df-f 6526  df-f1 6527  df-fo 6528  df-f1o 6529  df-fv 6530  df-riota 7354  df-ov 7400  df-oprab 7401  df-mpo 7402  df-om 7848  df-1st 7971  df-2nd 7972  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-rdg 8382  df-er 8679  df-en 8929  df-dom 8930  df-sdom 8931  df-pnf 11219  df-mnf 11220  df-xr 11221  df-ltxr 11222  df-le 11223  df-sub 11417  df-neg 11418  df-div 11846  df-nn 12212  df-2 12281  df-n0 12483  df-z 12570  df-uz 12841  df-rp 12995  df-fz 13514  df-seq 14016  df-exp 14076  df-cj 15127  df-re 15128  df-im 15129  df-sqrt 15263  df-abs 15264  df-clim 15516

This theorem is referenced by:  fprodss  15979