metakunt29 - Mathbox for metakunt

	Mathbox for metakunt		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > metakunt29		Structured version Visualization version GIF version

Theorem metakunt29 42235

Description: Construction of one solution of the increment equation system. (Contributed by metakunt, 7-Jul-2024.)

**Hypotheses**
Ref	Expression
metakunt29.1	⊢ (𝜑 → 𝑀 ∈ ℕ)
metakunt29.2	⊢ (𝜑 → 𝐼 ∈ ℕ)
metakunt29.3	⊢ (𝜑 → 𝐼 ≤ 𝑀)
metakunt29.4	⊢ (𝜑 → 𝑋 ∈ (1...𝑀))
metakunt29.5	⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))
metakunt29.6	⊢ 𝐵 = (𝑧 ∈ (1...𝑀) ↦ if(𝑧 = 𝑀, 𝑀, if(𝑧 < 𝐼, (𝑧 + (𝑀 − 𝐼)), (𝑧 + (1 − 𝐼)))))
metakunt29.7	⊢ (𝜑 → ¬ 𝑋 = 𝐼)
metakunt29.8	⊢ (𝜑 → 𝑋 < 𝐼)
metakunt29.9	⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))))
metakunt29.10	⊢ 𝐻 = if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0)

**Assertion**
Ref	Expression
metakunt29	⊢ (𝜑 → (𝐶‘(𝐵‘(𝐴‘𝑋))) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))

Distinct variable groups: 𝑦,𝐻 𝑦,𝐼 𝑧,𝐼 𝑥,𝑀 𝑦,𝑀 𝑧,𝑀 𝑥,𝑋 𝑦,𝑋 𝑧,𝑋 𝜑,𝑥 𝜑,𝑦 𝜑,𝑧 Allowed substitution hints: 𝐴(𝑥,𝑦,𝑧) 𝐵(𝑥,𝑦,𝑧) 𝐶(𝑥,𝑦,𝑧) 𝐻(𝑥,𝑧) 𝐼(𝑥)

**Proof of Theorem metakunt29**
Step	Hyp	Ref	Expression
1		metakunt29.1	. . . 4 ⊢ (𝜑 → 𝑀 ∈ ℕ)
2		metakunt29.2	. . . 4 ⊢ (𝜑 → 𝐼 ∈ ℕ)
3		metakunt29.3	. . . 4 ⊢ (𝜑 → 𝐼 ≤ 𝑀)
4		metakunt29.4	. . . 4 ⊢ (𝜑 → 𝑋 ∈ (1...𝑀))
5		metakunt29.5	. . . 4 ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))
6		metakunt29.6	. . . 4 ⊢ 𝐵 = (𝑧 ∈ (1...𝑀) ↦ if(𝑧 = 𝑀, 𝑀, if(𝑧 < 𝐼, (𝑧 + (𝑀 − 𝐼)), (𝑧 + (1 − 𝐼)))))
7		metakunt29.7	. . . 4 ⊢ (𝜑 → ¬ 𝑋 = 𝐼)
8		metakunt29.8	. . . 4 ⊢ (𝜑 → 𝑋 < 𝐼)
9	1, 2, 3, 4, 5, 6, 7, 8	metakunt27 42233	. . 3 ⊢ (𝜑 → (𝐵‘(𝐴‘𝑋)) = (𝑋 + (𝑀 − 𝐼)))
10	9	fveq2d 6909	. 2 ⊢ (𝜑 → (𝐶‘(𝐵‘(𝐴‘𝑋))) = (𝐶‘(𝑋 + (𝑀 − 𝐼))))
11		metakunt29.9	. . . 4 ⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))))
12	11	a1i 11	. . 3 ⊢ (𝜑 → 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)))))
13		elfznn 13594	. . . . . . . . . . . 12 ⊢ (𝑋 ∈ (1...𝑀) → 𝑋 ∈ ℕ)
14	4, 13	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ∈ ℕ)
15		nnre 12274	. . . . . . . . . . 11 ⊢ (𝑋 ∈ ℕ → 𝑋 ∈ ℝ)
16	14, 15	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ∈ ℝ)
17	1	nnred 12282	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ ℝ)
18	2	nnred 12282	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐼 ∈ ℝ)
19	17, 18	resubcld 11692	. . . . . . . . . 10 ⊢ (𝜑 → (𝑀 − 𝐼) ∈ ℝ)
20	16, 19	readdcld 11291	. . . . . . . . 9 ⊢ (𝜑 → (𝑋 + (𝑀 − 𝐼)) ∈ ℝ)
21	16	recnd 11290	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ∈ ℂ)
22	17	recnd 11290	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ ℂ)
23	18	recnd 11290	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐼 ∈ ℂ)
24	21, 22, 23	addsub12d 11644	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋 + (𝑀 − 𝐼)) = (𝑀 + (𝑋 − 𝐼)))
25	22, 23, 21	subsub2d 11650	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑀 − (𝐼 − 𝑋)) = (𝑀 + (𝑋 − 𝐼)))
26	18, 16	resubcld 11692	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐼 − 𝑋) ∈ ℝ)
27	16, 18	posdifd 11851	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋 < 𝐼 ↔ 0 < (𝐼 − 𝑋)))
28	8, 27	mpbid 232	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 < (𝐼 − 𝑋))
29	26, 28	elrpd 13075	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐼 − 𝑋) ∈ ℝ⁺)
30	17, 29	ltsubrpd 13110	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑀 − (𝐼 − 𝑋)) < 𝑀)
31	25, 30	eqbrtrrd 5166	. . . . . . . . . 10 ⊢ (𝜑 → (𝑀 + (𝑋 − 𝐼)) < 𝑀)
32	24, 31	eqbrtrd 5164	. . . . . . . . 9 ⊢ (𝜑 → (𝑋 + (𝑀 − 𝐼)) < 𝑀)
33	20, 32	ltned 11398	. . . . . . . 8 ⊢ (𝜑 → (𝑋 + (𝑀 − 𝐼)) ≠ 𝑀)
34	33	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) → (𝑋 + (𝑀 − 𝐼)) ≠ 𝑀)
35		simpr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) → 𝑦 = (𝑋 + (𝑀 − 𝐼)))
36	35	neeq1d 2999	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) → (𝑦 ≠ 𝑀 ↔ (𝑋 + (𝑀 − 𝐼)) ≠ 𝑀))
37	34, 36	mpbird 257	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) → 𝑦 ≠ 𝑀)
38	37	neneqd 2944	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) → ¬ 𝑦 = 𝑀)
39	38	iffalsed 4535	. . . 4 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) → if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))) = if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)))
40		simpr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 𝐼 ≤ (𝑋 + (𝑀 − 𝐼)))
41	18	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 𝐼 ∈ ℝ)
42	16	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 𝑋 ∈ ℝ)
43	17	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 𝑀 ∈ ℝ)
44	43, 41	resubcld 11692	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝑀 − 𝐼) ∈ ℝ)
45	42, 44	readdcld 11291	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝑋 + (𝑀 − 𝐼)) ∈ ℝ)
46	41, 45	lenltd 11408	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝐼 ≤ (𝑋 + (𝑀 − 𝐼)) ↔ ¬ (𝑋 + (𝑀 − 𝐼)) < 𝐼))
47	40, 46	mpbid 232	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → ¬ (𝑋 + (𝑀 − 𝐼)) < 𝐼)
48	47	3adant2 1131	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → ¬ (𝑋 + (𝑀 − 𝐼)) < 𝐼)
49		simp2 1137	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 𝑦 = (𝑋 + (𝑀 − 𝐼)))
50	49	breq1d 5152	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝑦 < 𝐼 ↔ (𝑋 + (𝑀 − 𝐼)) < 𝐼))
51	50	notbid 318	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (¬ 𝑦 < 𝐼 ↔ ¬ (𝑋 + (𝑀 − 𝐼)) < 𝐼))
52	48, 51	mpbird 257	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → ¬ 𝑦 < 𝐼)
53	52	iffalsed 4535	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = (𝑦 + 1))
54	49	oveq1d 7447	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝑦 + 1) = ((𝑋 + (𝑀 − 𝐼)) + 1))
55	53, 54	eqtrd 2776	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = ((𝑋 + (𝑀 − 𝐼)) + 1))
56		simp3 1138	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 𝐼 ≤ (𝑋 + (𝑀 − 𝐼)))
57	56	iftrued 4532	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0) = 1)
58	57	eqcomd 2742	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 1 = if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0))
59		metakunt29.10	. . . . . . . . 9 ⊢ 𝐻 = if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0)
60	58, 59	eqtr4di 2794	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 1 = 𝐻)
61	60	oveq2d 7448	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → ((𝑋 + (𝑀 − 𝐼)) + 1) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
62	55, 61	eqtrd 2776	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
63	62	3expa 1118	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
64	20, 18	ltnled 11409	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑋 + (𝑀 − 𝐼)) < 𝐼 ↔ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))))
65	64	biimprd 248	. . . . . . . . . . 11 ⊢ (𝜑 → (¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼)) → (𝑋 + (𝑀 − 𝐼)) < 𝐼))
66	65	imp 406	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝑋 + (𝑀 − 𝐼)) < 𝐼)
67	66	3adant2 1131	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝑋 + (𝑀 − 𝐼)) < 𝐼)
68		simp2 1137	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 𝑦 = (𝑋 + (𝑀 − 𝐼)))
69	68	breq1d 5152	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝑦 < 𝐼 ↔ (𝑋 + (𝑀 − 𝐼)) < 𝐼))
70	67, 69	mpbird 257	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 𝑦 < 𝐼)
71	70	iftrued 4532	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = 𝑦)
72	21	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → 𝑋 ∈ ℂ)
73	22	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → 𝑀 ∈ ℂ)
74	23	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → 𝐼 ∈ ℂ)
75	73, 74	subcld 11621	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → (𝑀 − 𝐼) ∈ ℂ)
76	72, 75	addcld 11281	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → (𝑋 + (𝑀 − 𝐼)) ∈ ℂ)
77	76	addridd 11462	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → ((𝑋 + (𝑀 − 𝐼)) + 0) = (𝑋 + (𝑀 − 𝐼)))
78	77	eqcomd 2742	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → (𝑋 + (𝑀 − 𝐼)) = ((𝑋 + (𝑀 − 𝐼)) + 0))
79	64	biimpa 476	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼)))
80	79	iffalsed 4535	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0) = 0)
81	80	eqcomd 2742	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → 0 = if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0))
82	59	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → 𝐻 = if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0))
83	82	eqcomd 2742	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0) = 𝐻)
84	81, 83	eqtrd 2776	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → 0 = 𝐻)
85	84	oveq2d 7448	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → ((𝑋 + (𝑀 − 𝐼)) + 0) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
86	78, 85	eqtrd 2776	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → (𝑋 + (𝑀 − 𝐼)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
87	86	ex 412	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑋 + (𝑀 − 𝐼)) < 𝐼 → (𝑋 + (𝑀 − 𝐼)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻)))
88	65, 87	syld 47	. . . . . . . . . 10 ⊢ (𝜑 → (¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼)) → (𝑋 + (𝑀 − 𝐼)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻)))
89	88	imp 406	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝑋 + (𝑀 − 𝐼)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
90	89	3adant2 1131	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝑋 + (𝑀 − 𝐼)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
91	68, 90	eqtrd 2776	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 𝑦 = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
92	71, 91	eqtrd 2776	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
93	92	3expa 1118	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
94	63, 93	pm2.61dan 812	. . . 4 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
95	39, 94	eqtrd 2776	. . 3 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) → if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
96		1zzd 12650	. . . 4 ⊢ (𝜑 → 1 ∈ ℤ)
97	1	nnzd 12642	. . . 4 ⊢ (𝜑 → 𝑀 ∈ ℤ)
98	14	nnzd 12642	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ ℤ)
99	2	nnzd 12642	. . . . . 6 ⊢ (𝜑 → 𝐼 ∈ ℤ)
100	97, 99	zsubcld 12729	. . . . 5 ⊢ (𝜑 → (𝑀 − 𝐼) ∈ ℤ)
101	98, 100	zaddcld 12728	. . . 4 ⊢ (𝜑 → (𝑋 + (𝑀 − 𝐼)) ∈ ℤ)
102		1p0e1 12391	. . . . 5 ⊢ (1 + 0) = 1
103		1red 11263	. . . . . 6 ⊢ (𝜑 → 1 ∈ ℝ)
104		0red 11265	. . . . . 6 ⊢ (𝜑 → 0 ∈ ℝ)
105	14	nnge1d 12315	. . . . . 6 ⊢ (𝜑 → 1 ≤ 𝑋)
106	17, 18	subge0d 11854	. . . . . . 7 ⊢ (𝜑 → (0 ≤ (𝑀 − 𝐼) ↔ 𝐼 ≤ 𝑀))
107	3, 106	mpbird 257	. . . . . 6 ⊢ (𝜑 → 0 ≤ (𝑀 − 𝐼))
108	103, 104, 16, 19, 105, 107	le2addd 11883	. . . . 5 ⊢ (𝜑 → (1 + 0) ≤ (𝑋 + (𝑀 − 𝐼)))
109	102, 108	eqbrtrrid 5178	. . . 4 ⊢ (𝜑 → 1 ≤ (𝑋 + (𝑀 − 𝐼)))
110	20, 17, 32	ltled 11410	. . . 4 ⊢ (𝜑 → (𝑋 + (𝑀 − 𝐼)) ≤ 𝑀)
111	96, 97, 101, 109, 110	elfzd 13556	. . 3 ⊢ (𝜑 → (𝑋 + (𝑀 − 𝐼)) ∈ (1...𝑀))
112	111	elfzelzd 13566	. . . 4 ⊢ (𝜑 → (𝑋 + (𝑀 − 𝐼)) ∈ ℤ)
113		0zd 12627	. . . . . 6 ⊢ (𝜑 → 0 ∈ ℤ)
114	96, 113	ifcld 4571	. . . . 5 ⊢ (𝜑 → if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0) ∈ ℤ)
115	59	a1i 11	. . . . . 6 ⊢ (𝜑 → 𝐻 = if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0))
116	115	eleq1d 2825	. . . . 5 ⊢ (𝜑 → (𝐻 ∈ ℤ ↔ if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0) ∈ ℤ))
117	114, 116	mpbird 257	. . . 4 ⊢ (𝜑 → 𝐻 ∈ ℤ)
118	112, 117	zaddcld 12728	. . 3 ⊢ (𝜑 → ((𝑋 + (𝑀 − 𝐼)) + 𝐻) ∈ ℤ)
119	12, 95, 111, 118	fvmptd 7022	. 2 ⊢ (𝜑 → (𝐶‘(𝑋 + (𝑀 − 𝐼))) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
120	10, 119	eqtrd 2776	1 ⊢ (𝜑 → (𝐶‘(𝐵‘(𝐴‘𝑋))) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∧ w3a 1086 = wceq 1539 ∈ wcel 2107 ≠ wne 2939 ifcif 4524 class class class wbr 5142 ↦ cmpt 5224 ‘cfv 6560 (class class class)co 7432 ℂcc 11154 ℝcr 11155 0cc0 11156 1c1 11157 + caddc 11159 < clt 11296 ≤ cle 11297 − cmin 11493 ℕcn 12267 ℤcz 12615 ...cfz 13548

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-10 2140 ax-11 2156 ax-12 2176 ax-ext 2707 ax-sep 5295 ax-nul 5305 ax-pow 5364 ax-pr 5431 ax-un 7756 ax-cnex 11212 ax-resscn 11213 ax-1cn 11214 ax-icn 11215 ax-addcl 11216 ax-addrcl 11217 ax-mulcl 11218 ax-mulrcl 11219 ax-mulcom 11220 ax-addass 11221 ax-mulass 11222 ax-distr 11223 ax-i2m1 11224 ax-1ne0 11225 ax-1rid 11226 ax-rnegex 11227 ax-rrecex 11228 ax-cnre 11229 ax-pre-lttri 11230 ax-pre-lttrn 11231 ax-pre-ltadd 11232 ax-pre-mulgt0 11233

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-nf 1783 df-sb 2064 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2728 df-clel 2815 df-nfc 2891 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-reu 3380 df-rab 3436 df-v 3481 df-sbc 3788 df-csb 3899 df-dif 3953 df-un 3955 df-in 3957 df-ss 3967 df-pss 3970 df-nul 4333 df-if 4525 df-pw 4601 df-sn 4626 df-pr 4628 df-op 4632 df-uni 4907 df-iun 4992 df-br 5143 df-opab 5205 df-mpt 5225 df-tr 5259 df-id 5577 df-eprel 5583 df-po 5591 df-so 5592 df-fr 5636 df-we 5638 df-xp 5690 df-rel 5691 df-cnv 5692 df-co 5693 df-dm 5694 df-rn 5695 df-res 5696 df-ima 5697 df-pred 6320 df-ord 6386 df-on 6387 df-lim 6388 df-suc 6389 df-iota 6513 df-fun 6562 df-fn 6563 df-f 6564 df-f1 6565 df-fo 6566 df-f1o 6567 df-fv 6568 df-riota 7389 df-ov 7435 df-oprab 7436 df-mpo 7437 df-om 7889 df-1st 8015 df-2nd 8016 df-frecs 8307 df-wrecs 8338 df-recs 8412 df-rdg 8451 df-er 8746 df-en 8987 df-dom 8988 df-sdom 8989 df-pnf 11298 df-mnf 11299 df-xr 11300 df-ltxr 11301 df-le 11302 df-sub 11495 df-neg 11496 df-nn 12268 df-n0 12529 df-z 12616 df-uz 12880 df-rp 13036 df-fz 13549

This theorem is referenced by: metakunt31 42237

W3C validator